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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
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 =
| ScopeVarDefinition of {
var : (ScopeVar.t, Pos.t list) Mark.ed;
typ : typ;
io : Desugared.Ast.io;
e : 'm expr;
}
| SubScopeVarDefinition of {
var : (ScopeVar.t, Pos.t list) Mark.ed;
var_within_origin_scope : ScopeVar.t;
typ : typ;
e : 'm expr;
}
| Assertion of 'm expr
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;
scope_visibility : visibility;
}
type 'm program = {
program_module_name : (ModuleName.t * module_intf_id) option;
program_ctx : decl_ctx;
program_modules : 'm 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 * visibility * bool) TopdefName.Map.t;
program_lang : Global.backend_lang;
}
let type_rule decl_ctx env = function
| ScopeVarDefinition ({ typ; e; _ } as def) ->
let e = Typing.expr decl_ctx ~env ~typ e in
ScopeVarDefinition { def with e = Expr.unbox e }
| SubScopeVarDefinition ({ typ; e; _ } as def) ->
let e = Typing.expr decl_ctx ~env ~typ e in
SubScopeVarDefinition { def with e = Expr.unbox e }
| Assertion e ->
let typ = Mark.add (Expr.pos e) (TLit TBool) in
let e = Typing.expr decl_ctx ~env ~typ e in
Assertion (Expr.unbox e)
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, _vis) 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, vis, is_external) ->
( Expr.unbox (Typing.expr prg.program_ctx ~env ~typ expr),
typ,
vis,
is_external ))
prg.program_topdefs
in
let type_scope scope =
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 })
scope
in
let program_scopes = ScopeName.Map.map type_scope prg.program_scopes in
let program_modules =
ModuleName.Map.map
(fun scopes -> ScopeName.Map.map type_scope scopes)
prg.program_modules
in
{ prg with program_topdefs; program_scopes; program_modules }
let type_program prg = Message.with_delayed_errors (fun () -> type_program prg)