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
|
open import Interp_ast
open import Pervasives
type tannot = maybe (t * tag * list nec * effect)
let get_exp_l (E_aux e (l,annot)) = l
val pure : effect
let pure = Effect_aux(Effect_set []) Unknown
let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown
(* Workaround Lem's inability to scrap my (type classes) boilerplate.
* Implementing only Eq, and only for literals - hopefully this will
* be enough, but we should in principle implement ordering for everything in
* Interp_ast *)
val lit_eq: lit -> lit -> bool
let lit_eq (L_aux left _) (L_aux right _) =
match (left, right) with
| (L_unit, L_unit) -> true
| (L_zero, L_zero) -> true
| (L_one, L_one) -> true
| (L_true, L_true) -> true
| (L_false, L_false) -> true
| (L_num n, L_num m) -> n = m
| (L_hex h, L_hex h') -> h = h'
| (L_bin b, L_bin b') -> b = b'
| (L_undef, L_undef) -> true
| (L_string s, L_string s') -> s = s'
| (_, _) -> false
end
instance (Eq lit)
let (=) = lit_eq
let (<>) n1 n2 = not (lit_eq n1 n2)
end
let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
let rec list_to_string format sep lst = match lst with
| [] -> ""
| [last] -> format last
| one::rest -> (format one) ^ sep ^ (list_to_string format sep rest)
end
val has_rmem_effect : list base_effect -> bool
val has_barr_effect : list base_effect -> bool
val has_wmem_effect : list base_effect -> bool
let rec has_effect which efcts =
match efcts with
| [] -> false
| (BE_aux e _)::efcts ->
match (which,e) with
| (BE_rreg,BE_rreg) -> true
| (BE_wreg,BE_wreg) -> true
| (BE_rmem,BE_rmem) -> true
| (BE_wmem,BE_wmem) -> true
| (BE_barr,BE_barr) -> true
| (BE_undef,BE_undef) -> true
| (BE_unspec,BE_unspec) -> true
| (BE_nondet,BE_nondet) -> true
| _ -> has_effect which efcts
end
end
let has_rmem_effect = has_effect BE_rmem
let has_barr_effect = has_effect BE_barr
let has_wmem_effect = has_effect BE_wmem
let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
let get_effects (Typ_aux t _) =
match t with
| Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff
| _ -> []
end
val find_type_def : defs tannot -> id -> maybe (type_def tannot)
val find_function : defs tannot -> id -> maybe (list (funcl tannot))
let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls
let rec find_function (Defs defs) id =
match defs with
| [] -> Nothing
| def::defs ->
match def with
| DEF_fundef f -> match get_funcls id f with
| [] -> find_function (Defs defs) id
| funcs -> Just funcs end
| _ -> find_function (Defs defs) id
end end
let rec get_first_index_range (BF_aux i _) = match i with
| BF_single i -> i
| BF_range i j -> i
| BF_concat s _ -> get_first_index_range s
end
let rec get_index_range_size (BF_aux i _) = match i with
| BF_single _ -> 1
| BF_range i j -> (abs (i-j)) + 1
| BF_concat i j -> (get_index_range_size i) + (get_index_range_size j)
end
|
