Source file outcome_rewrites.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
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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
module Big_int = Nat_big_num
open Ast
open Ast_defs
open Ast_util
open Type_check
open Type_error
open Rewriter
let rec in_substs id = function
| IS_aux (IS_id (id_from, _), _) :: _ when Id.compare id id_from = 0 -> true
| _ :: substs -> in_substs id substs
| [] -> false
let rec instantiate_id id = function
| IS_aux (IS_id (id_from, id_to), _) :: _ when Id.compare id id_from = 0 -> id_to
| _ :: substs -> instantiate_id id substs
| [] -> id
let instantiate_typ substs typ =
List.fold_left
(fun typ -> function kid, (_, subst_arg) -> typ_subst kid subst_arg typ)
typ (KBindings.bindings substs)
let instantiate_typquant substs typq =
List.fold_left
(fun typq -> function kid, (_, subst_arg) -> typquant_subst kid subst_arg typq)
typq (KBindings.bindings substs)
let instantiate_def target id substs = function
| DEF_aux (DEF_impl (FCL_aux (FCL_funcl (target_id, pexp), (fcl_def_annot, tannot))), def_annot)
when string_of_id target_id = target ->
let l = gen_loc (id_loc id) in
Some
(DEF_aux
( DEF_fundef
(FD_aux
( FD_function
( Rec_aux (Rec_nonrec, l),
Typ_annot_opt_aux (Typ_annot_opt_none, l),
[FCL_aux (FCL_funcl (id, pexp), (fcl_def_annot, tannot))]
),
(l, tannot)
)
),
def_annot
)
)
| def -> None
let rec instantiated_or_abstract l = function
| [] -> None
| None :: xs -> instantiated_or_abstract l xs
| Some def :: xs ->
if List.for_all Option.is_none xs then Some def
else raise (Reporting.err_general l "Multiple instantiations found for target")
let instantiate target ast =
let process_def outcomes = function
| DEF_aux (DEF_outcome (OV_aux (OV_outcome (id, TypSchm_aux (TypSchm_ts (typq, typ), _), args), l), outcome_defs), _)
->
(Bindings.add id (typq, typ, args, l, outcome_defs) outcomes, [])
| DEF_aux (DEF_instantiation (IN_aux (IN_id id, annot), id_substs), def_annot) ->
let l = gen_loc (id_loc id) in
let env = env_of_annot annot in
let substs = Env.get_outcome_instantiation env in
let typq, typ, args, outcome_l, outcome_defs =
match Bindings.find_opt id outcomes with
| Some outcome -> outcome
| None ->
Reporting.unreachable (id_loc id) __POS__
("Outcome for instantiation " ^ string_of_id id ^ " does not exist")
in
let rewrite_p_aux (pat, annot) =
match pat with
| P_typ (typ, pat) -> P_aux (P_typ (instantiate_typ substs typ, pat), annot)
| pat -> P_aux (pat, annot)
in
let rewrite_e_aux (exp, annot) =
match exp with
| E_app (f, args) -> E_aux (E_app (instantiate_id f id_substs, args), annot)
| E_typ (typ, exp) -> E_aux (E_typ (instantiate_typ substs typ, exp), annot)
| E_constraint (NC_aux (NC_var v, _)) -> (
match KBindings.find_opt v substs with
| Some (_, A_aux (A_bool nc, _)) -> E_aux (E_constraint nc, annot)
| _ -> Reporting.unreachable (id_loc id) __POS__ "Failed to instantiate constraint"
)
| E_sizeof (Nexp_aux (Nexp_var v, _)) -> (
match KBindings.find_opt v substs with
| Some (_, A_aux (A_nexp n, _)) -> E_aux (E_sizeof n, annot)
| _ -> Reporting.unreachable (id_loc id) __POS__ "Failed to instantiate constraint"
)
| _ -> E_aux (exp, annot)
in
let pat_alg = { id_pat_alg with p_aux = rewrite_p_aux } in
let rewrite_pat rw pat = fold_pat pat_alg pat in
let rewrite_exp _ exp = fold_exp { id_exp_alg with e_aux = rewrite_e_aux; pat_alg } exp in
let valspec is_extern =
let extern = if is_extern then Some { pure = false; bindings = [("_", string_of_id id)] } else None in
DEF_aux
( DEF_val
(VS_aux
( VS_val_spec
( TypSchm_aux (TypSchm_ts (instantiate_typquant substs typq, instantiate_typ substs typ), l),
id,
extern
),
(l, empty_uannot)
)
),
strip_def_annot def_annot
)
in
let instantiated_def =
rewrite_ast_defs { rewriters_base with rewrite_pat; rewrite_exp } outcome_defs
|> List.map (instantiate_def target id id_substs)
|> instantiated_or_abstract (id_loc id)
in
let outcome_defs, _ =
( match instantiated_def with
| None ->
[
DEF_aux
( DEF_pragma ("abstract", Pragma_line (string_of_id id, gen_loc (id_loc id))),
mk_def_annot (gen_loc (id_loc id)) ()
);
valspec true;
]
| Some def -> [valspec false; strip_def def]
)
|> Type_error.check_defs env
in
(outcomes, outcome_defs)
| def -> (outcomes, [def])
in
{ ast with defs = snd (Util.fold_left_concat_map process_def Bindings.empty ast.defs) }