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
|
open import Interp_ast
open import Pervasives
open import Show_extra
let rec power (a: integer) (b: integer) : integer =
if b <= 0
then 1
else a * (power a (b-1))
let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')
(*As in the type system, the first effect is local to the expression and the second is cummulative*)
type tannot = maybe (t * tag * list nec * effect * 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 {ocaml;coq} lit_eq (L_aux left _) (L_aux right _) =
match (left, right) with
| (L_zero, L_zero) -> true
| (L_one, L_one) -> true
| (L_bin b, L_bin b') -> b = b'
| (L_hex h, L_hex h') -> h = h'
| (L_zero, L_num i) -> i = 0
| (L_num i,L_zero) -> i = 0
| (L_one, L_num i) -> i = 1
| (L_num i, L_one) -> i = 1
| (L_num n, L_num m) -> n = m
| (L_unit, L_unit) -> true
| (L_true, L_true) -> true
| (L_false, L_false) -> true
| (L_undef, L_undef) -> true
| (L_string s, L_string s') -> s = s'
| (_, _) -> false
end
let {isabelle;hol} lit_eq = unsafe_structural_equality
let {ocaml;coq} lit_ineq n1 n2 = not (lit_eq n1 n2)
let {isabelle;hol} lit_ineq = unsafe_structural_inequality
instance (Eq lit)
let (=) = lit_eq
let (<>) = lit_ineq
end
let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
let rec {ocaml} list_to_string format sep lst = match lst with
| [] -> ""
| [last] -> format last
| one::rest -> (format one) ^ sep ^ (list_to_string format sep rest)
end
let ~{ocaml} list_to_string format sep list = ""
val has_rmem_effect : list base_effect -> bool
val has_barr_effect : list base_effect -> bool
val has_wmem_effect : list base_effect -> bool
val has_depend_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_wmv,BE_wmv) -> true
| (BE_eamem,BE_eamem) -> true
| (BE_barr,BE_barr) -> true
| (BE_undef,BE_undef) -> true
| (BE_unspec,BE_unspec) -> true
| (BE_nondet,BE_nondet) -> true
| (BE_depend,BE_depend) -> 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 has_eamem_effect = has_effect BE_eamem
let has_wmv_effect = has_effect BE_wmv
let has_depend_effect = has_effect BE_depend
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
let {ocaml} string_of_tag tag = match tag with
| Tag_empty -> "empty"
| Tag_global -> "global"
| Tag_ctor -> "ctor"
| Tag_extern (Just n) -> "extern " ^ n
| Tag_extern _ -> "extern"
| Tag_default -> "default"
| Tag_spec -> "spec"
| Tag_enum i -> "enum"
| Tag_alias -> "alias"
end
let ~{ocaml} string_of_tag tag = ""
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 -> (natFromInteger i)
| BF_range i j -> (natFromInteger 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 -> (natFromInteger (abs (i-j))) + 1
| BF_concat i j -> (get_index_range_size i) + (get_index_range_size j)
end
let rec string_of_loc l = match l with
| Unknown -> "Unknown"
| Int s Nothing -> "Internal " ^ s
| Int s (Just l) -> "Internal " ^ s ^ " " ^ (string_of_loc l)
| Range file n1 n2 n3 n4 -> "File " ^ file ^ ": " ^ (show n1) ^ ": " ^ (show (n2:nat)) ^ ": " ^ (show (n3:nat)) ^ ": " ^ (show (n4:nat))
end
|
