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
|
open Ast
open Util
(* Some errors *)
let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v)
let no_variable e = error ("No such variable: " ^ e)
let type_error e = error ("Type error: " ^ e)
let invalid_arity e = error ("Invalid arity (" ^ e ^ ")")
(* Utility : find declaration of a const / a node *)
let find_const_decl p id =
match List.find (function
| AST_const_decl (c, _) when c.c_name = id -> true
| _ -> false)
p with
| AST_const_decl d -> d
| _ -> assert false
let find_node_decl p id =
match List.find (function
| AST_node_decl (c, _) when c.n_name = id -> true
| _ -> false)
p with
| AST_node_decl d -> d
| _ -> assert false
let extract_const_decls =
List.fold_left
(fun l d -> match d with
| AST_const_decl d -> d::l
| _ -> l)
[]
(* Utility : find instances declared in an expression *)
(* extract_instances :
prog -> expr ext -> (id * id * eqs * (var_def * expr ext) list) list
*)
let rec extract_instances p e = match fst e with
| AST_idconst _ | AST_identifier _
| AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
| AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> extract_instances p e'
| AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
| AST_arrow(e1, e2) ->
extract_instances p e1 @ extract_instances p e2
| AST_if(e1, e2, e3) ->
extract_instances p e1 @ extract_instances p e2 @ extract_instances p e3
| AST_instance((f, _), args, id) ->
let more = List.flatten (List.map (extract_instances p) args) in
let (node, _) = find_node_decl p f in
let args_x = List.map2 (fun id arg -> id, arg) node.args args in
(f, id, node.body, args_x)::more
| AST_tuple x -> List.flatten (List.map (extract_instances p) x)
(* Utility : find pre declarations in an expression *)
(* extract_pre : expr ext -> (id * expr ext) list *)
let rec extract_pre e = match fst e with
| AST_identifier _ | AST_idconst _
| AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
| AST_unary (_, e') | AST_not e' -> extract_pre e'
| AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
| AST_arrow(e1, e2) ->
extract_pre e1 @ extract_pre e2
| AST_if(e1, e2, e3) ->
extract_pre e1 @ extract_pre e2 @ extract_pre e3
| AST_instance((f, _), args, id) ->
List.flatten (List.map extract_pre args)
| AST_tuple x -> List.flatten (List.map extract_pre x)
| AST_pre(e', n) ->
(n, e')::(extract_pre e')
|
