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
open Ast
open Ast_defs
open Ast_util
let scan_ast { defs; _ } =
let scan (ids, specs) (DEF_aux (aux, _) as def) =
match aux with
| DEF_fundef fd -> (IdSet.add (id_of_fundef fd) ids, specs)
| DEF_val (VS_aux (VS_val_spec (_, id, _), _) as vs) -> (ids, Bindings.add id vs specs)
| DEF_pragma (("file_start" | "file_end"), _) -> (ids, specs)
| _ -> raise (Reporting.err_general (def_loc def) "Definition in splice file isn't a spec or function")
in
List.fold_left scan (IdSet.empty, Bindings.empty) defs
let filter_old_ast repl_ids repl_specs { defs; _ } =
let check (rdefs, specs_found) (DEF_aux (aux, def_annot) as def) =
match aux with
| DEF_fundef fd ->
let id = id_of_fundef fd in
if IdSet.mem id repl_ids then
( DEF_aux (DEF_pragma ("spliced_function#", Pragma_line (string_of_id id, def_annot.loc)), def_annot) :: rdefs,
specs_found
)
else (def :: rdefs, specs_found)
| DEF_val (VS_aux (VS_val_spec (_, id, _), _)) -> (
match Bindings.find_opt id repl_specs with
| Some vs -> (DEF_aux (DEF_val vs, def_annot) :: rdefs, IdSet.add id specs_found)
| None -> (def :: rdefs, specs_found)
)
| _ -> (def :: rdefs, specs_found)
in
let rdefs, specs_found = List.fold_left check ([], IdSet.empty) defs in
(List.rev rdefs, specs_found)
let filter_replacements spec_found { defs; _ } =
let not_found = function
| DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, _), _)), _) -> not (IdSet.mem id spec_found)
| _ -> true
in
List.filter not_found defs
let move_replacement_fundefs ast =
let rec aux acc = function
| DEF_aux (DEF_pragma ("spliced_function#", Pragma_line (id, _)), _) :: defs ->
let is_replacement = function
| DEF_aux (DEF_fundef fd, _) -> string_of_id (id_of_fundef fd) = id
| _ -> false
in
let replacement, other_defs = List.partition is_replacement defs in
aux (replacement @ acc) other_defs
| def :: defs -> aux (def :: acc) defs
| [] -> List.rev acc
in
{ ast with defs = aux [] ast.defs }
let annotate_ast ast =
let annotate_def (DEF_aux (d, a)) =
DEF_aux (d, add_def_attribute a.loc "spliced" None a)
|> map_def_def_annot (def_annot_map_env (fun _ -> Type_check.Env.empty))
in
{ ast with defs = List.map annotate_def ast.defs }
let splice ctx ast file =
let parsed_ast = Initial_check.parse_file file |> snd in
let repl_ast, _ = Initial_check.process_ast ctx (Parse_ast.Defs [(Some file, parsed_ast)]) in
let repl_ast = map_ast_annot (fun (l, _) -> (l, Type_check.empty_tannot)) repl_ast in
let repl_ast = annotate_ast repl_ast in
let repl_ids, repl_specs = scan_ast repl_ast in
let defs1, specs_found = filter_old_ast repl_ids repl_specs ast in
let defs2 = filter_replacements specs_found repl_ast in
{ ast with defs = defs1 @ defs2 }
let splice_files ctx ast files =
let spliced_ast = List.fold_left (fun ast file -> splice ctx ast file) ast files in
let checked_ast, env = Type_error.check Type_check.initial_env (Type_check.strip_ast spliced_ast) in
let sorted_ast = Callgraph.top_sort_defs (move_replacement_fundefs checked_ast) in
(sorted_ast, env)