author | huffman |
Fri, 27 Feb 2009 18:34:20 -0800 | |
changeset 30157 | 40919ebde2c9 |
parent 30132 | 243a05a67c41 |
child 30158 | 83c50c62cf23 |
permissions | -rw-r--r-- |
23152 | 1 |
(* Title: HOLCF/Tools/fixrec_package.ML |
2 |
Author: Amber Telfer and Brian Huffman |
|
3 |
||
4 |
Recursive function definition package for HOLCF. |
|
5 |
*) |
|
6 |
||
7 |
signature FIXREC_PACKAGE = |
|
8 |
sig |
|
9 |
val legacy_infer_term: theory -> term -> term |
|
10 |
val legacy_infer_prop: theory -> term -> term |
|
30132 | 11 |
|
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
12 |
val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory |
29581 | 13 |
val add_fixrec_i: bool -> ((binding * attribute list) * term) list list -> theory -> theory |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
14 |
val add_fixpat: Attrib.binding * string list -> theory -> theory |
29581 | 15 |
val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
16 |
val add_matchers: (string * string) list -> theory -> theory |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
17 |
val setup: theory -> theory |
23152 | 18 |
end; |
19 |
||
20 |
structure FixrecPackage: FIXREC_PACKAGE = |
|
21 |
struct |
|
22 |
||
23 |
(* legacy type inference *) |
|
30132 | 24 |
(* used by the domain package *) |
23152 | 25 |
fun legacy_infer_term thy t = |
24493
d4380e9b287b
replaced ProofContext.infer_types by general Syntax.check_terms;
wenzelm
parents:
23779
diff
changeset
|
26 |
singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); |
23152 | 27 |
|
24680 | 28 |
fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); |
23152 | 29 |
|
30 |
||
26045 | 31 |
val fix_eq2 = @{thm fix_eq2}; |
32 |
val def_fix_ind = @{thm def_fix_ind}; |
|
23152 | 33 |
|
34 |
||
35 |
fun fixrec_err s = error ("fixrec definition error:\n" ^ s); |
|
36 |
fun fixrec_eq_err thy s eq = |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26343
diff
changeset
|
37 |
fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq)); |
23152 | 38 |
|
30132 | 39 |
(*************************************************************************) |
40 |
(***************************** building types ****************************) |
|
41 |
(*************************************************************************) |
|
42 |
||
23152 | 43 |
(* ->> is taken from holcf_logic.ML *) |
30132 | 44 |
fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]); |
45 |
||
46 |
infixr 6 ->>; val (op ->>) = cfunT; |
|
47 |
||
48 |
fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) |
|
49 |
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); |
|
50 |
||
51 |
fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U |
|
52 |
| binder_cfun _ = []; |
|
53 |
||
54 |
fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U |
|
55 |
| body_cfun T = T; |
|
23152 | 56 |
|
30132 | 57 |
fun strip_cfun T : typ list * typ = |
58 |
(binder_cfun T, body_cfun T); |
|
59 |
||
60 |
fun maybeT T = Type(@{type_name "maybe"}, [T]); |
|
61 |
||
62 |
fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T |
|
63 |
| dest_maybeT T = raise TYPE ("dest_maybeT", [T], []); |
|
64 |
||
65 |
fun tupleT [] = @{typ "unit"} |
|
66 |
| tupleT [T] = T |
|
67 |
| tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts); |
|
68 |
||
69 |
fun matchT T = body_cfun T ->> maybeT (tupleT (binder_cfun T)); |
|
70 |
||
71 |
(*************************************************************************) |
|
72 |
(***************************** building terms ****************************) |
|
73 |
(*************************************************************************) |
|
23152 | 74 |
|
75 |
val mk_trp = HOLogic.mk_Trueprop; |
|
76 |
||
77 |
(* splits a cterm into the right and lefthand sides of equality *) |
|
78 |
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); |
|
79 |
||
80 |
(* similar to Thm.head_of, but for continuous application *) |
|
26045 | 81 |
fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f |
23152 | 82 |
| chead_of u = u; |
83 |
||
30132 | 84 |
fun capply_const (S, T) = |
85 |
Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T)); |
|
86 |
||
87 |
fun cabs_const (S, T) = |
|
88 |
Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T)); |
|
89 |
||
90 |
fun mk_capply (t, u) = |
|
91 |
let val (S, T) = |
|
92 |
case Term.fastype_of t of |
|
93 |
Type(@{type_name "->"}, [S, T]) => (S, T) |
|
94 |
| _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); |
|
95 |
in capply_const (S, T) $ t $ u end; |
|
96 |
||
97 |
infix 0 ==; val (op ==) = Logic.mk_equals; |
|
98 |
infix 1 ===; val (op ===) = HOLogic.mk_eq; |
|
99 |
infix 9 ` ; val (op `) = mk_capply; |
|
100 |
||
101 |
||
102 |
fun mk_cpair (t, u) = |
|
103 |
let val T = Term.fastype_of t |
|
104 |
val U = Term.fastype_of u |
|
105 |
val cpairT = T ->> U ->> HOLogic.mk_prodT (T, U) |
|
106 |
in Const(@{const_name cpair}, cpairT) ` t ` u end; |
|
107 |
||
108 |
fun mk_cfst t = |
|
109 |
let val T = Term.fastype_of t; |
|
110 |
val (U, _) = HOLogic.dest_prodT T; |
|
111 |
in Const(@{const_name cfst}, T ->> U) ` t end; |
|
112 |
||
113 |
fun mk_csnd t = |
|
114 |
let val T = Term.fastype_of t; |
|
115 |
val (_, U) = HOLogic.dest_prodT T; |
|
116 |
in Const(@{const_name csnd}, T ->> U) ` t end; |
|
117 |
||
118 |
fun mk_csplit t = |
|
119 |
let val (S, TU) = dest_cfunT (Term.fastype_of t); |
|
120 |
val (T, U) = dest_cfunT TU; |
|
121 |
val csplitT = (S ->> T ->> U) ->> HOLogic.mk_prodT (S, T) ->> U; |
|
122 |
in Const(@{const_name csplit}, csplitT) ` t end; |
|
23152 | 123 |
|
124 |
(* builds the expression (LAM v. rhs) *) |
|
30132 | 125 |
fun big_lambda v rhs = |
126 |
cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs; |
|
23152 | 127 |
|
128 |
(* builds the expression (LAM v1 v2 .. vn. rhs) *) |
|
129 |
fun big_lambdas [] rhs = rhs |
|
130 |
| big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); |
|
131 |
||
132 |
(* builds the expression (LAM <v1,v2,..,vn>. rhs) *) |
|
30132 | 133 |
fun lambda_ctuple [] rhs = big_lambda (Free("unit", HOLogic.unitT)) rhs |
23152 | 134 |
| lambda_ctuple (v::[]) rhs = big_lambda v rhs |
135 |
| lambda_ctuple (v::vs) rhs = |
|
30132 | 136 |
mk_csplit (big_lambda v (lambda_ctuple vs rhs)); |
23152 | 137 |
|
138 |
(* builds the expression <v1,v2,..,vn> *) |
|
30132 | 139 |
fun mk_ctuple [] = @{term "UU::unit"} |
23152 | 140 |
| mk_ctuple (t::[]) = t |
30132 | 141 |
| mk_ctuple (t::ts) = mk_cpair (t, mk_ctuple ts); |
142 |
||
143 |
fun mk_return t = |
|
144 |
let val T = Term.fastype_of t |
|
145 |
in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end; |
|
146 |
||
147 |
fun mk_bind (t, u) = |
|
148 |
let val (T, mU) = dest_cfunT (Term.fastype_of u); |
|
149 |
val bindT = maybeT T ->> (T ->> mU) ->> mU; |
|
150 |
in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end; |
|
151 |
||
152 |
fun mk_mplus (t, u) = |
|
153 |
let val mT = Term.fastype_of t |
|
154 |
in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end; |
|
155 |
||
156 |
fun mk_run t = |
|
157 |
let val mT = Term.fastype_of t |
|
158 |
val T = dest_maybeT mT |
|
159 |
in Const(@{const_name Fixrec.run}, mT ->> T) ` t end; |
|
160 |
||
161 |
fun mk_fix t = |
|
162 |
let val (T, _) = dest_cfunT (Term.fastype_of t) |
|
163 |
in Const(@{const_name fix}, (T ->> T) ->> T) ` t end; |
|
23152 | 164 |
|
165 |
(*************************************************************************) |
|
166 |
(************* fixed-point definitions and unfolding theorems ************) |
|
167 |
(*************************************************************************) |
|
168 |
||
169 |
fun add_fixdefs eqs thy = |
|
170 |
let |
|
171 |
val (lhss,rhss) = ListPair.unzip (map dest_eqs eqs); |
|
30132 | 172 |
val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss)); |
23152 | 173 |
|
174 |
fun one_def (l as Const(n,T)) r = |
|
175 |
let val b = Sign.base_name n in (b, (b^"_def", l == r)) end |
|
176 |
| one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"; |
|
177 |
fun defs [] _ = [] |
|
178 |
| defs (l::[]) r = [one_def l r] |
|
30132 | 179 |
| defs (l::ls) r = one_def l (mk_cfst r) :: defs ls (mk_csnd r); |
180 |
val (names, fixdefs) = ListPair.unzip (defs lhss fixpoint); |
|
23152 | 181 |
|
182 |
val (fixdef_thms, thy') = |
|
29585 | 183 |
PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) fixdefs) thy; |
25132 | 184 |
val ctuple_fixdef_thm = foldr1 (fn (x,y) => @{thm cpair_equalI} OF [x,y]) fixdef_thms; |
23152 | 185 |
|
30132 | 186 |
val ctuple_unfold = mk_trp (mk_ctuple lhss === mk_ctuple rhss); |
23152 | 187 |
val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold |
188 |
(fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1, |
|
189 |
simp_tac (simpset_of thy') 1]); |
|
190 |
val ctuple_induct_thm = |
|
191 |
(space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind); |
|
192 |
||
193 |
fun unfolds [] thm = [] |
|
194 |
| unfolds (n::[]) thm = [(n^"_unfold", thm)] |
|
195 |
| unfolds (n::ns) thm = let |
|
25132 | 196 |
val thmL = thm RS @{thm cpair_eqD1}; |
197 |
val thmR = thm RS @{thm cpair_eqD2}; |
|
23152 | 198 |
in (n^"_unfold", thmL) :: unfolds ns thmR end; |
199 |
val unfold_thms = unfolds names ctuple_unfold_thm; |
|
200 |
val thms = ctuple_induct_thm :: unfold_thms; |
|
29585 | 201 |
val (_, thy'') = PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name) thms) thy'; |
23152 | 202 |
in |
203 |
(thy'', names, fixdef_thms, map snd unfold_thms) |
|
204 |
end; |
|
205 |
||
206 |
(*************************************************************************) |
|
207 |
(*********** monadic notation and pattern matching compilation ***********) |
|
208 |
(*************************************************************************) |
|
209 |
||
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
210 |
structure FixrecMatchData = TheoryDataFun ( |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
211 |
type T = string Symtab.table; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
212 |
val empty = Symtab.empty; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
213 |
val copy = I; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
214 |
val extend = I; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
215 |
fun merge _ tabs : T = Symtab.merge (K true) tabs; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
216 |
); |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
217 |
|
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
218 |
(* associate match functions with pattern constants *) |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
219 |
fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms); |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
220 |
|
30157 | 221 |
fun taken_names (t : term) : bstring list = |
222 |
let |
|
223 |
fun taken (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs |
|
224 |
| taken (Free(a,_) , bs) = insert (op =) a bs |
|
225 |
| taken (f $ u , bs) = taken (f, taken (u, bs)) |
|
226 |
| taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs) |
|
227 |
| taken (_ , bs) = bs; |
|
228 |
in |
|
229 |
taken (t, []) |
|
230 |
end; |
|
23152 | 231 |
|
232 |
(* builds a monadic term for matching a constructor pattern *) |
|
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
233 |
fun pre_build match_name pat rhs vs taken = |
23152 | 234 |
case pat of |
26045 | 235 |
Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) => |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
236 |
pre_build match_name f rhs (v::vs) taken |
26045 | 237 |
| Const(@{const_name Rep_CFun},_)$f$x => |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
238 |
let val (rhs', v, taken') = pre_build match_name x rhs [] taken; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
239 |
in pre_build match_name f rhs' (v::vs) taken' end |
23152 | 240 |
| Const(c,T) => |
241 |
let |
|
242 |
val n = Name.variant taken "v"; |
|
26045 | 243 |
fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs |
23152 | 244 |
| result_type T _ = T; |
245 |
val v = Free(n, result_type T vs); |
|
30132 | 246 |
val m = Const(match_name c, matchT T); |
23152 | 247 |
val k = lambda_ctuple vs rhs; |
248 |
in |
|
30132 | 249 |
(mk_bind (m`v, k), v, n::taken) |
23152 | 250 |
end |
251 |
| Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n) |
|
252 |
| _ => fixrec_err "pre_build: invalid pattern"; |
|
253 |
||
254 |
(* builds a monadic term for matching a function definition pattern *) |
|
255 |
(* returns (name, arity, matcher) *) |
|
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
256 |
fun building match_name pat rhs vs taken = |
23152 | 257 |
case pat of |
26045 | 258 |
Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) => |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
259 |
building match_name f rhs (v::vs) taken |
26045 | 260 |
| Const(@{const_name Rep_CFun}, _)$f$x => |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
261 |
let val (rhs', v, taken') = pre_build match_name x rhs [] taken; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
262 |
in building match_name f rhs' (v::vs) taken' end |
30132 | 263 |
| Const(name,_) => (pat, length vs, big_lambdas vs rhs) |
23152 | 264 |
| _ => fixrec_err "function is not declared as constant in theory"; |
265 |
||
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
266 |
fun match_eq match_name eq = |
23152 | 267 |
let val (lhs,rhs) = dest_eqs eq; |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
268 |
in |
30157 | 269 |
building match_name lhs (mk_return rhs) [] (taken_names eq) |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
270 |
end; |
23152 | 271 |
|
272 |
(* returns the sum (using +++) of the terms in ms *) |
|
273 |
(* also applies "run" to the result! *) |
|
274 |
fun fatbar arity ms = |
|
275 |
let |
|
30132 | 276 |
fun LAM_Ts 0 t = ([], Term.fastype_of t) |
277 |
| LAM_Ts n (_ $ Abs(_,T,t)) = |
|
278 |
let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end |
|
279 |
| LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; |
|
23152 | 280 |
fun unLAM 0 t = t |
281 |
| unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t |
|
282 |
| unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; |
|
30132 | 283 |
fun reLAM ([], U) t = t |
284 |
| reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t)); |
|
285 |
val msum = foldr1 mk_mplus (map (unLAM arity) ms); |
|
286 |
val (Ts, U) = LAM_Ts arity (hd ms) |
|
23152 | 287 |
in |
30132 | 288 |
reLAM (rev Ts, dest_maybeT U) (mk_run msum) |
23152 | 289 |
end; |
290 |
||
291 |
fun unzip3 [] = ([],[],[]) |
|
292 |
| unzip3 ((x,y,z)::ts) = |
|
293 |
let val (xs,ys,zs) = unzip3 ts |
|
294 |
in (x::xs, y::ys, z::zs) end; |
|
295 |
||
296 |
(* this is the pattern-matching compiler function *) |
|
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
297 |
fun compile_pats match_name eqs = |
23152 | 298 |
let |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
299 |
val ((n::names),(a::arities),mats) = unzip3 (map (match_eq match_name) eqs); |
23152 | 300 |
val cname = if forall (fn x => n=x) names then n |
301 |
else fixrec_err "all equations in block must define the same function"; |
|
302 |
val arity = if forall (fn x => a=x) arities then a |
|
303 |
else fixrec_err "all equations in block must have the same arity"; |
|
304 |
val rhs = fatbar arity mats; |
|
305 |
in |
|
30132 | 306 |
mk_trp (cname === rhs) |
23152 | 307 |
end; |
308 |
||
309 |
(*************************************************************************) |
|
310 |
(********************** Proving associated theorems **********************) |
|
311 |
(*************************************************************************) |
|
312 |
||
313 |
(* proves a block of pattern matching equations as theorems, using unfold *) |
|
314 |
fun make_simps thy (unfold_thm, eqns) = |
|
315 |
let |
|
25132 | 316 |
val tacs = [rtac (unfold_thm RS @{thm ssubst_lhs}) 1, asm_simp_tac (simpset_of thy) 1]; |
23152 | 317 |
fun prove_term t = Goal.prove_global thy [] [] t (K (EVERY tacs)); |
318 |
fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts); |
|
319 |
in |
|
320 |
map prove_eqn eqns |
|
321 |
end; |
|
322 |
||
323 |
(*************************************************************************) |
|
324 |
(************************* Main fixrec function **************************) |
|
325 |
(*************************************************************************) |
|
326 |
||
327 |
fun gen_add_fixrec prep_prop prep_attrib strict blocks thy = |
|
328 |
let |
|
329 |
val eqns = List.concat blocks; |
|
330 |
val lengths = map length blocks; |
|
331 |
||
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27691
diff
changeset
|
332 |
val ((bindings, srcss), strings) = apfst split_list (split_list eqns); |
29006 | 333 |
val names = map Binding.base_name bindings; |
23152 | 334 |
val atts = map (map (prep_attrib thy)) srcss; |
335 |
val eqn_ts = map (prep_prop thy) strings; |
|
336 |
val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq))) |
|
337 |
handle TERM _ => fixrec_eq_err thy "not a proper equation" eq) eqn_ts; |
|
25557 | 338 |
val (_, eqn_ts') = OldPrimrecPackage.unify_consts thy rec_ts eqn_ts; |
23152 | 339 |
|
340 |
fun unconcat [] _ = [] |
|
341 |
| unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n)); |
|
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
342 |
val matcher_tab = FixrecMatchData.get thy; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
343 |
fun match_name c = |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
344 |
case Symtab.lookup matcher_tab c of SOME m => m |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
345 |
| NONE => fixrec_err ("unknown pattern constructor: " ^ c); |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
346 |
|
23152 | 347 |
val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts'); |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
348 |
val compiled_ts = |
30132 | 349 |
map (compile_pats match_name) pattern_blocks; |
23152 | 350 |
val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs compiled_ts thy; |
351 |
in |
|
352 |
if strict then let (* only prove simp rules if strict = true *) |
|
353 |
val eqn_blocks = unconcat lengths ((names ~~ eqn_ts') ~~ atts); |
|
29585 | 354 |
val simps = maps (make_simps thy') (unfold_thms ~~ eqn_blocks); |
355 |
val (simp_thms, thy'') = PureThy.add_thms ((map o apfst o apfst) Binding.name simps) thy'; |
|
23152 | 356 |
|
357 |
val simp_names = map (fn name => name^"_simps") cnames; |
|
358 |
val simp_attribute = rpair [Simplifier.simp_add]; |
|
359 |
val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms); |
|
360 |
in |
|
29585 | 361 |
(snd o PureThy.add_thmss ((map o apfst o apfst) Binding.name simps')) thy'' |
23152 | 362 |
end |
363 |
else thy' |
|
364 |
end; |
|
365 |
||
24707 | 366 |
val add_fixrec = gen_add_fixrec Syntax.read_prop_global Attrib.attribute; |
23152 | 367 |
val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I); |
368 |
||
369 |
||
370 |
(*************************************************************************) |
|
371 |
(******************************** Fixpat *********************************) |
|
372 |
(*************************************************************************) |
|
373 |
||
374 |
fun fix_pat thy t = |
|
375 |
let |
|
376 |
val T = fastype_of t; |
|
377 |
val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T)); |
|
378 |
val cname = case chead_of t of Const(c,_) => c | _ => |
|
379 |
fixrec_err "function is not declared as constant in theory"; |
|
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
380 |
val unfold_thm = PureThy.get_thm thy (cname^"_unfold"); |
23152 | 381 |
val simp = Goal.prove_global thy [] [] eq |
382 |
(fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]); |
|
383 |
in simp end; |
|
384 |
||
385 |
fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = |
|
386 |
let |
|
387 |
val atts = map (prep_attrib thy) srcs; |
|
388 |
val ts = map (prep_term thy) strings; |
|
389 |
val simps = map (fix_pat thy) ts; |
|
390 |
in |
|
29585 | 391 |
(snd o PureThy.add_thmss [((name, simps), atts)]) thy |
23152 | 392 |
end; |
393 |
||
24707 | 394 |
val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute; |
23152 | 395 |
val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I); |
396 |
||
397 |
||
398 |
(*************************************************************************) |
|
399 |
(******************************** Parsers ********************************) |
|
400 |
(*************************************************************************) |
|
401 |
||
402 |
local structure P = OuterParse and K = OuterKeyword in |
|
403 |
||
404 |
val fixrec_eqn = SpecParse.opt_thm_name ":" -- P.prop; |
|
405 |
||
406 |
val fixrec_strict = P.opt_keyword "permissive" >> not; |
|
407 |
||
408 |
val fixrec_decl = fixrec_strict -- P.and_list1 (Scan.repeat1 fixrec_eqn); |
|
409 |
||
410 |
(* this builds a parser for a new keyword, fixrec, whose functionality |
|
411 |
is defined by add_fixrec *) |
|
24867 | 412 |
val _ = |
23152 | 413 |
OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl |
414 |
(fixrec_decl >> (Toplevel.theory o uncurry add_fixrec)); |
|
415 |
||
416 |
(* fixpat parser *) |
|
417 |
val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop; |
|
418 |
||
24867 | 419 |
val _ = |
23152 | 420 |
OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl |
421 |
(fixpat_decl >> (Toplevel.theory o add_fixpat)); |
|
422 |
||
26045 | 423 |
end; (* local structure *) |
23152 | 424 |
|
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
425 |
val setup = FixrecMatchData.init; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
426 |
|
24867 | 427 |
end; |