Source file disambiguate.ml
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
open Shared_ast
open Ast
let expr ctx env e =
Typing.check_expr ctx ~env (Expr.unbox e)
let rule ctx env rule =
let env =
match rule.rule_parameter with
| None -> env
| Some (vars_and_types, _) ->
ListLabels.fold_right vars_and_types ~init:env ~f:(fun ((v, _), t) ->
Typing.Env.add_var v t)
in
{
rule with
rule_just = expr ctx env rule.rule_just;
rule_cons = expr ctx env rule.rule_cons;
}
let scope ctx env scope =
let env = Typing.Env.open_scope scope.scope_uid env in
let scope_defs =
ScopeDefMap.map
(fun def ->
let scope_def_rules =
RuleName.Map.map (rule ctx env) def.scope_def_rules
in
{ def with scope_def_rules })
scope.scope_defs
in
let scope_assertions = List.map (expr ctx env) scope.scope_assertions in
{ scope with scope_defs; scope_assertions }
let program prg =
let env =
TopdefName.Map.fold
(fun name (_e, ty) env -> Typing.Env.add_toplevel_var name ty env)
prg.program_topdefs Typing.Env.empty
in
let program_topdefs =
TopdefName.Map.map
(fun (e, ty) -> Expr.unbox (expr prg.program_ctx env (Expr.box e)), ty)
prg.program_topdefs
in
let env =
ScopeName.Map.fold
(fun scope_name scope env ->
let vars =
ScopeDefMap.fold
(fun var def vars ->
match var with
| Var (v, _states) -> ScopeVar.Map.add v def.scope_def_typ vars
| SubScopeVar _ -> vars)
scope.scope_defs ScopeVar.Map.empty
in
Typing.Env.add_scope scope_name ~vars env)
prg.program_scopes env
in
let program_scopes =
ScopeName.Map.map (scope prg.program_ctx env) prg.program_scopes
in
{ prg with program_topdefs; program_scopes }