|
1 (* Title: TFL/dcterm.ML |
|
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 Copyright 1997 University of Cambridge |
|
5 *) |
|
6 |
|
7 (*--------------------------------------------------------------------------- |
|
8 * Derived efficient cterm destructors. |
|
9 *---------------------------------------------------------------------------*) |
|
10 |
|
11 signature DCTERM = |
|
12 sig |
|
13 val dest_comb: cterm -> cterm * cterm |
|
14 val dest_abs: string option -> cterm -> cterm * cterm |
|
15 val capply: cterm -> cterm -> cterm |
|
16 val cabs: cterm -> cterm -> cterm |
|
17 val mk_conj: cterm * cterm -> cterm |
|
18 val mk_disj: cterm * cterm -> cterm |
|
19 val mk_exists: cterm * cterm -> cterm |
|
20 val dest_conj: cterm -> cterm * cterm |
|
21 val dest_const: cterm -> {Name: string, Ty: typ} |
|
22 val dest_disj: cterm -> cterm * cterm |
|
23 val dest_eq: cterm -> cterm * cterm |
|
24 val dest_exists: cterm -> cterm * cterm |
|
25 val dest_forall: cterm -> cterm * cterm |
|
26 val dest_imp: cterm -> cterm * cterm |
|
27 val dest_let: cterm -> cterm * cterm |
|
28 val dest_neg: cterm -> cterm |
|
29 val dest_pair: cterm -> cterm * cterm |
|
30 val dest_var: cterm -> {Name:string, Ty:typ} |
|
31 val is_conj: cterm -> bool |
|
32 val is_cons: cterm -> bool |
|
33 val is_disj: cterm -> bool |
|
34 val is_eq: cterm -> bool |
|
35 val is_exists: cterm -> bool |
|
36 val is_forall: cterm -> bool |
|
37 val is_imp: cterm -> bool |
|
38 val is_let: cterm -> bool |
|
39 val is_neg: cterm -> bool |
|
40 val is_pair: cterm -> bool |
|
41 val list_mk_disj: cterm list -> cterm |
|
42 val strip_abs: cterm -> cterm list * cterm |
|
43 val strip_comb: cterm -> cterm * cterm list |
|
44 val strip_disj: cterm -> cterm list |
|
45 val strip_exists: cterm -> cterm list * cterm |
|
46 val strip_forall: cterm -> cterm list * cterm |
|
47 val strip_imp: cterm -> cterm list * cterm |
|
48 val drop_prop: cterm -> cterm |
|
49 val mk_prop: cterm -> cterm |
|
50 end; |
|
51 |
|
52 structure Dcterm: DCTERM = |
|
53 struct |
|
54 |
|
55 structure U = Utils; |
|
56 |
|
57 fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg}; |
|
58 |
|
59 |
|
60 fun dest_comb t = Thm.dest_comb t |
|
61 handle CTERM msg => raise ERR "dest_comb" msg; |
|
62 |
|
63 fun dest_abs a t = Thm.dest_abs a t |
|
64 handle CTERM msg => raise ERR "dest_abs" msg; |
|
65 |
|
66 fun capply t u = Thm.capply t u |
|
67 handle CTERM msg => raise ERR "capply" msg; |
|
68 |
|
69 fun cabs a t = Thm.cabs a t |
|
70 handle CTERM msg => raise ERR "cabs" msg; |
|
71 |
|
72 |
|
73 (*--------------------------------------------------------------------------- |
|
74 * Some simple constructor functions. |
|
75 *---------------------------------------------------------------------------*) |
|
76 |
|
77 val mk_hol_const = Thm.cterm_of (Theory.sign_of HOL.thy) o Const; |
|
78 |
|
79 fun mk_exists (r as (Bvar, Body)) = |
|
80 let val ty = #T(rep_cterm Bvar) |
|
81 val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT) |
|
82 in capply c (uncurry cabs r) end; |
|
83 |
|
84 |
|
85 local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) |
|
86 in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2 |
|
87 end; |
|
88 |
|
89 local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) |
|
90 in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2 |
|
91 end; |
|
92 |
|
93 |
|
94 (*--------------------------------------------------------------------------- |
|
95 * The primitives. |
|
96 *---------------------------------------------------------------------------*) |
|
97 fun dest_const ctm = |
|
98 (case #t(rep_cterm ctm) |
|
99 of Const(s,ty) => {Name = s, Ty = ty} |
|
100 | _ => raise ERR "dest_const" "not a constant"); |
|
101 |
|
102 fun dest_var ctm = |
|
103 (case #t(rep_cterm ctm) |
|
104 of Var((s,i),ty) => {Name=s, Ty=ty} |
|
105 | Free(s,ty) => {Name=s, Ty=ty} |
|
106 | _ => raise ERR "dest_var" "not a variable"); |
|
107 |
|
108 |
|
109 (*--------------------------------------------------------------------------- |
|
110 * Derived destructor operations. |
|
111 *---------------------------------------------------------------------------*) |
|
112 |
|
113 fun dest_monop expected tm = |
|
114 let |
|
115 fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected); |
|
116 val (c, N) = dest_comb tm handle U.ERR _ => err (); |
|
117 val name = #Name (dest_const c handle U.ERR _ => err ()); |
|
118 in if name = expected then N else err () end; |
|
119 |
|
120 fun dest_binop expected tm = |
|
121 let |
|
122 fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected); |
|
123 val (M, N) = dest_comb tm handle U.ERR _ => err () |
|
124 in (dest_monop expected M, N) handle U.ERR _ => err () end; |
|
125 |
|
126 fun dest_binder expected tm = |
|
127 dest_abs None (dest_monop expected tm) |
|
128 handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected); |
|
129 |
|
130 |
|
131 val dest_neg = dest_monop "not" |
|
132 val dest_pair = dest_binop "Pair"; |
|
133 val dest_eq = dest_binop "op =" |
|
134 val dest_imp = dest_binop "op -->" |
|
135 val dest_conj = dest_binop "op &" |
|
136 val dest_disj = dest_binop "op |" |
|
137 val dest_cons = dest_binop "Cons" |
|
138 val dest_let = Library.swap o dest_binop "Let"; |
|
139 val dest_select = dest_binder "Eps" |
|
140 val dest_exists = dest_binder "Ex" |
|
141 val dest_forall = dest_binder "All" |
|
142 |
|
143 (* Query routines *) |
|
144 |
|
145 val is_eq = can dest_eq |
|
146 val is_imp = can dest_imp |
|
147 val is_select = can dest_select |
|
148 val is_forall = can dest_forall |
|
149 val is_exists = can dest_exists |
|
150 val is_neg = can dest_neg |
|
151 val is_conj = can dest_conj |
|
152 val is_disj = can dest_disj |
|
153 val is_pair = can dest_pair |
|
154 val is_let = can dest_let |
|
155 val is_cons = can dest_cons |
|
156 |
|
157 |
|
158 (*--------------------------------------------------------------------------- |
|
159 * Iterated creation. |
|
160 *---------------------------------------------------------------------------*) |
|
161 val list_mk_disj = U.end_itlist (fn d1 => fn tm => mk_disj (d1, tm)); |
|
162 |
|
163 (*--------------------------------------------------------------------------- |
|
164 * Iterated destruction. (To the "right" in a term.) |
|
165 *---------------------------------------------------------------------------*) |
|
166 fun strip break tm = |
|
167 let fun dest (p as (ctm,accum)) = |
|
168 let val (M,N) = break ctm |
|
169 in dest (N, M::accum) |
|
170 end handle U.ERR _ => p |
|
171 in dest (tm,[]) |
|
172 end; |
|
173 |
|
174 fun rev2swap (x,l) = (rev l, x); |
|
175 |
|
176 val strip_comb = strip (Library.swap o dest_comb) (* Goes to the "left" *) |
|
177 val strip_imp = rev2swap o strip dest_imp |
|
178 val strip_abs = rev2swap o strip (dest_abs None) |
|
179 val strip_forall = rev2swap o strip dest_forall |
|
180 val strip_exists = rev2swap o strip dest_exists |
|
181 |
|
182 val strip_disj = rev o (op::) o strip dest_disj |
|
183 |
|
184 |
|
185 (*--------------------------------------------------------------------------- |
|
186 * Going into and out of prop |
|
187 *---------------------------------------------------------------------------*) |
|
188 |
|
189 fun mk_prop ctm = |
|
190 let val {t, sign, ...} = Thm.rep_cterm ctm in |
|
191 if can HOLogic.dest_Trueprop t then ctm |
|
192 else Thm.cterm_of sign (HOLogic.mk_Trueprop t) |
|
193 end |
|
194 handle TYPE (msg, _, _) => raise ERR "mk_prop" msg |
|
195 | TERM (msg, _) => raise ERR "mk_prop" msg; |
|
196 |
|
197 fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm; |
|
198 |
|
199 |
|
200 end; |