forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcfHeapsBaseSyntax.sml
129 lines (104 loc) · 3.91 KB
/
cfHeapsBaseSyntax.sml
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
structure cfHeapsBaseSyntax = struct
open preamble
open set_sepTheory helperLib
open cfHeapsBaseTheory
val ERR = mk_HOL_ERR"cfHeapsBaseSyntax";
val ffi_proj_format = packLib.unpack_type ffi_proj_pack
val ffi_varty = mk_vartype "'ffi"
fun mk_ffi_proj_ty arg_ty =
type_subst [ffi_varty |-> arg_ty] ffi_proj_format
fun dest_ffi_proj ty =
if can (match_type ffi_proj_format) ty then hd (type_vars ty)
else fail()
fun is_ffi_proj ty = can dest_ffi_proj ty
val heap_part_ty =
mk_thy_type {Thy = "cfHeapsBase", Tyop = "heap_part", Args = []}
val res_ty =
mk_thy_type {Thy = "cfHeapsBase", Tyop = "res", Args = []}
val heap_ty = packLib.unpack_type heap_pack
val hprop_ty = packLib.unpack_type hprop_pack
fun dest_sep_imp tm = let
val format = (fst o dest_eq o concl o SPEC_ALL) SEP_IMP_def
in if can (match_term format) tm then (cdr (car tm), cdr tm) else fail() end
fun dest_cell tm = let
val format = (fst o dest_eq o concl o SPEC_ALL) cell_def
in if can (match_term format) tm then (cdr (car tm), cdr tm) else fail() end
fun dest_REF tm = let
val format = (fst o dest_eq o concl o SPEC_ALL) REF_def
in if can (match_term format) tm then (cdr (car tm), cdr tm) else fail() end
fun dest_ARRAY tm = let
val format = (fst o dest_eq o concl o SPEC_ALL) ARRAY_def
in if can (match_term format) tm then (cdr (car tm), cdr tm) else fail() end
fun dest_W8ARRAY tm = let
val format = (fst o dest_eq o concl o SPEC_ALL) W8ARRAY_def
in if can (match_term format) tm then (cdr (car tm), cdr tm) else fail() end
fun dest_IO tm = let
val format = (fst o dest_eq o concl o SPEC_ALL) IO_def
in if can (match_term format) tm then (cdr (car (car tm)), cdr (car tm), cdr tm)
else fail() end
fun is_cell tm = can dest_cell tm
fun is_REF tm = can dest_REF tm
fun is_ARRAY tm = can dest_ARRAY tm
fun is_W8ARRAY tm = can dest_W8ARRAY tm
fun is_IO tm = can dest_IO tm
fun is_sep_imp tm = can dest_sep_imp tm
fun is_sep_imppost tm = let
val format = (fst o dest_eq o concl o SPEC_ALL) SEP_IMPPOST_def
in can (match_term format) tm end
fun is_cond tm = let
val format = (fst o dest_eq o concl o SPEC_ALL) cond_def
in can (match_term format) tm end
fun is_sep_exists tm = let
val se = (fst o dest_eq o concl o SPEC_ALL) SEP_EXISTS
in (ignore (match_term se (dest_comb tm |> fst)); true)
handle HOL_ERR _ => false
end
fun mk_cond t =
SPEC t (INST_TYPE [alpha |-> heap_part_ty] cond_def)
|> concl |> lhs
val emp_tm =
inst [alpha |-> heap_part_ty]
(emp_def |> concl |> lhs)
val postv_tm = prim_mk_const{Name="POSTv",Thy="cfHeapsBase"};
val dest_postv = dest_binder postv_tm (ERR "dest_postv" "Not a POSTv abstraction");
val is_postv = can dest_postv;
fun mk_postv (postv_v, c) = mk_binder postv_tm "mk_postv" (postv_v, c);
val poste_tm = prim_mk_const{Name="POSTe",Thy="cfHeapsBase"};
val dest_poste = dest_binder poste_tm (ERR "dest_poste" "Not a POSTe abstraction");
val is_poste = can dest_poste;
fun mk_poste (poste_v, c) = mk_binder poste_tm "mk_poste" (poste_v, c);
val post_tm = prim_mk_const{Name="POST",Thy="cfHeapsBase"};
fun dest_post c =
let
val (c', poste_abs) = dest_comb c
val (ptm, postv_abs) = dest_comb c'
in
if same_const ptm post_tm then
let
val (postv_v, postv_pred) = dest_abs postv_abs
val (poste_v, poste_pred) = dest_abs poste_abs
in
(postv_v, postv_pred, poste_v, poste_pred)
end
else
raise (ERR "" "")
end
handle HOL_ERR _ => raise (ERR "dest_post" "Not a POST abstraction");
fun is_post c =
let
val (c', poste_abs) = dest_comb c
val (ptm, postv_abs) = dest_comb c'
in
same_const ptm post_tm
end
handle HOL_ERR _ => false;
fun mk_post (postv_v, postv_abs, poste_v, poste_abs) =
let
val postv_pred = mk_abs (postv_v, postv_abs)
val poste_pred = mk_abs (poste_v, poste_abs)
val post_cond_pre = mk_comb (post_tm, postv_pred)
val post_cond = mk_comb (post_cond_pre, poste_pred)
in
post_cond
end;
end