1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
open Catala_utils
open Shared_ast
type location = scopelang glocation
module LocationSet : Set.S with type elt = location Mark.pos = Set.Make (struct
type t = location Mark.pos
let compare = Expr.compare_location
end)
type 'm expr = (scopelang, 'm) gexpr
let rec locations_used (e : 'm expr) : LocationSet.t =
match e with
| ELocation l, pos -> LocationSet.singleton (l, Expr.mark_pos pos)
| EAbs { binder; _ }, _ ->
let _, body = Bindlib.unmbind binder in
locations_used body
| e ->
Expr.shallow_fold
(fun e -> LocationSet.union (locations_used e))
e LocationSet.empty
type 'm rule =
| Definition of location Mark.pos * typ * Desugared.Ast.io * 'm expr
| Assertion of 'm expr
| Call of ScopeName.t * SubScopeName.t * 'm mark
type scope_var_ty = {
svar_in_ty : typ;
svar_out_ty : typ;
svar_io : Desugared.Ast.io;
}
type 'm scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : scope_var_ty ScopeVar.Map.t;
scope_decl_rules : 'm rule list;
scope_options : Desugared.Ast.catala_option Mark.pos list;
}
type 'm program = {
program_module_name : ModuleName.t option;
program_ctx : decl_ctx;
program_modules : nil scope_decl Mark.pos ScopeName.Map.t ModuleName.Map.t;
program_scopes : 'm scope_decl Mark.pos ScopeName.Map.t;
program_topdefs : ('m expr * typ) TopdefName.Map.t;
program_lang : Cli.backend_lang;
}
let type_rule decl_ctx env = function
| Definition (loc, typ, io, expr) ->
let expr' = Typing.expr ~leave_unresolved:false decl_ctx ~env ~typ expr in
Definition (loc, typ, io, Expr.unbox expr')
| Assertion expr ->
let typ = Mark.add (Expr.pos expr) (TLit TBool) in
let expr' = Typing.expr ~leave_unresolved:false decl_ctx ~env ~typ expr in
Assertion (Expr.unbox expr')
| Call (sc_name, ssc_name, m) ->
let pos = Expr.mark_pos m in
Call (sc_name, ssc_name, Typed { pos; ty = Mark.add pos TAny })
let type_program (type m) (prg : m program) : typed program =
let env = Typing.Env.empty prg.program_ctx in
let env =
TopdefName.Map.fold
(fun name ty env -> Typing.Env.add_toplevel_var name ty env)
prg.program_ctx.ctx_topdefs env
in
let env =
ScopeName.Map.fold
(fun scope_name _info env ->
let scope_sig =
match ScopeName.path scope_name with
| [] ->
(Mark.remove (ScopeName.Map.find scope_name prg.program_scopes))
.scope_sig
| p ->
let m = List.hd (List.rev p) in
let scope =
ScopeName.Map.find scope_name
(ModuleName.Map.find m prg.program_modules)
in
(Mark.remove scope).scope_sig
in
let vars =
ScopeVar.Map.map (fun { svar_out_ty; _ } -> svar_out_ty) scope_sig
in
let in_vars =
ScopeVar.Map.map (fun { svar_in_ty; _ } -> svar_in_ty) scope_sig
in
Typing.Env.add_scope scope_name ~vars ~in_vars env)
prg.program_ctx.ctx_scopes env
in
let program_topdefs =
TopdefName.Map.map
(fun (expr, typ) ->
( Expr.unbox
(Typing.expr prg.program_ctx ~leave_unresolved:false ~env ~typ expr),
typ ))
prg.program_topdefs
in
let program_scopes =
ScopeName.Map.map
(Mark.map (fun scope_decl ->
let env =
ScopeVar.Map.fold
(fun svar { svar_out_ty; _ } env ->
Typing.Env.add_scope_var svar svar_out_ty env)
scope_decl.scope_sig env
in
let scope_decl_rules =
List.map
(type_rule prg.program_ctx env)
scope_decl.scope_decl_rules
in
{ scope_decl with scope_decl_rules }))
prg.program_scopes
in
{ prg with program_topdefs; program_scopes }