renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
minor tuning;
1 (* Title: HOL/Tools/function_package/fundef_common.ML
3 Author: Alexander Krauss, TU Muenchen
5 A package for general recursive function definitions.
6 Common definitions and other infrastructure.
9 structure FundefCommon =
12 local open FundefLib in
15 val profile = ref false;
17 fun PROFILE msg = if !profile then timeap_msg msg else I
20 val acc_const_name = @{const_name "accp"}
22 Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R
24 val function_name = suffix "C"
25 val graph_name = suffix "_graph"
26 val rel_name = suffix "_rel"
27 val dom_name = suffix "_dom"
29 (* Termination rules *)
31 structure TerminationRule = GenericDataFun
36 fun merge _ = Thm.merge_thms
39 val get_termination_rules = TerminationRule.get
40 val store_termination_rule = TerminationRule.map o cons
41 val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
44 (* Function definition result data *)
46 datatype fundef_result =
54 trsimps : thm list option,
56 simple_pinducts : thm list,
59 domintros : thm list option
63 datatype fundef_context_data =
68 (* contains no logical entities: invariant under morphisms *)
69 add_simps : (string -> string) -> string -> Attrib.src list -> thm list
70 -> local_theory -> thm list * local_theory,
71 case_names : string list,
81 fun morph_fundef_data (FundefCtxData {add_simps, case_names, fs, R,
82 psimps, pinducts, termination, defname}) phi =
84 val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
85 val name = Binding.name_of o Morphism.binding phi o Binding.name
87 FundefCtxData { add_simps = add_simps, case_names = case_names,
88 fs = map term fs, R = term R, psimps = fact psimps,
89 pinducts = fact pinducts, termination = thm termination,
90 defname = name defname }
93 structure FundefData = GenericDataFun
95 type T = (term * fundef_context_data) NetRules.T;
96 val empty = NetRules.init
97 (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
101 fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
105 (* Generally useful?? *)
106 fun lift_morphism thy f =
108 val term = Drule.term_rule thy f
110 Morphism.thm_morphism f $> Morphism.term_morphism term
111 $> Morphism.typ_morphism (Logic.type_map term)
114 fun import_fundef_data t ctxt =
116 val thy = Context.theory_of ctxt
117 val ct = cterm_of thy t
118 val inst_morph = lift_morphism thy o Thm.instantiate
120 fun match (trm, data) =
121 SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
122 handle Pattern.MATCH => NONE
124 get_first match (NetRules.retrieve (FundefData.get ctxt) t)
127 fun import_last_fundef ctxt =
128 case NetRules.rules (FundefData.get ctxt) of
132 val ([t'], ctxt') = Variable.import_terms true [t] (Context.proof_of ctxt)
134 import_fundef_data t' (Context.Proof ctxt')
137 val all_fundef_data = NetRules.rules o FundefData.get
139 fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
140 FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
141 #> store_termination_rule termination
144 (* Simp rules for termination proofs *)
146 structure TerminationSimps = NamedThmsFun
148 val name = "termination_simp"
149 val description = "Simplification rule for termination proofs"
153 (* Default Termination Prover *)
155 structure TerminationProver = GenericDataFun
157 type T = (Proof.context -> Method.method)
158 val empty = (fn _ => error "Termination prover not configured")
160 fun merge _ (a,b) = b (* FIXME *)
163 val set_termination_prover = TerminationProver.put
164 val get_termination_prover = TerminationProver.get
167 (* Configuration management *)
174 datatype fundef_config
183 fun apply_opt Sequential (FundefConfig {sequential, default, domintros,tailrec}) =
184 FundefConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec}
185 | apply_opt (Default d) (FundefConfig {sequential, default, domintros,tailrec}) =
186 FundefConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec}
187 | apply_opt DomIntros (FundefConfig {sequential, default, domintros,tailrec}) =
188 FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
189 | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) =
190 FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
193 FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*),
194 domintros=false, tailrec=false }
197 (* Analyzing function equations *)
199 fun split_def ctxt geq =
201 fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
202 val qs = Term.strip_qnt_vars "all" geq
203 val imp = Term.strip_qnt_body "all" geq
204 val (gs, eq) = Logic.strip_horn imp
206 val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
207 handle TERM _ => error (input_error "Not an equation")
209 val (head, args) = strip_comb f_args
211 val fname = fst (dest_Free head)
212 handle TERM _ => error (input_error "Head symbol must not be a bound variable")
214 (fname, qs, gs, args, rhs)
217 exception ArgumentCount of string
219 fun mk_arities fqgars =
220 let fun f (fname, _, _, args, _) arities =
221 let val k = length args
223 case Symtab.lookup arities fname of
224 NONE => Symtab.update (fname, k) arities
225 | SOME i => (if i = k then arities else raise ArgumentCount fname)
228 fold f fqgars Symtab.empty
232 (* Check for all sorts of errors in the input *)
233 fun check_defs ctxt fixes eqs =
235 val fnames = map (fst o fst) fixes
239 fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
241 val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
243 val _ = fname mem fnames
245 ("Head symbol of left hand side must be "
246 ^ plural "" "one out of " fnames ^ commas_quote fnames)
248 fun add_bvs t is = add_loose_bnos (t, 0, is)
249 val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
250 |> map (fst o nth (rev qs))
252 val _ = null rvs orelse input_error
253 ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
254 ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
256 val _ = forall (not o Term.exists_subterm
257 (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
258 orelse input_error "Defined function may not occur in premises or arguments"
260 val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
261 val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
263 orelse (warning (cat_lines
264 ["Bound variable" ^ plural " " "s " funvars
265 ^ commas_quote (map fst funvars) ^
266 " occur" ^ plural "s" "" funvars ^ " in function position.",
267 "Misspelled constructor???"]); true)
272 val _ = mk_arities (map check eqs)
273 handle ArgumentCount fname =>
274 error ("Function " ^ quote fname ^
275 " has different numbers of arguments in different equations")
277 fun check_sorts ((fname, fT), _) =
278 Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
279 orelse error (cat_lines
280 ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
281 setmp show_sorts true (Syntax.string_of_typ ctxt) fT])
283 val _ = map check_sorts fixes
290 type fixes = ((string * typ) * mixfix) list
291 type 'a spec = ((bstring * Attrib.src list) * 'a list) list
292 type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec
293 -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
295 val fname_of = fst o dest_Free o fst o strip_comb o fst
296 o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
298 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
299 | mk_case_names _ n 0 = []
300 | mk_case_names _ n 1 = [n]
301 | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
303 fun empty_preproc check _ _ ctxt fixes spec =
305 val (nas,tss) = split_list spec
307 val _ = check ctxt fixes ts
308 val fnames = map (fst o fst) fixes
309 val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
311 fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1)
315 (* using theorem names for case name currently disabled *)
316 val cnames = map_index (fn (i, (n,_)) => mk_case_names i "" 1) nas |> flat
318 (ts, curry op ~~ nas o Library.unflat tss, sort, cnames)
321 structure Preprocessor = GenericDataFun
324 val empty : T = empty_preproc check_defs
326 fun merge _ (a, _) = a
329 val get_preproc = Preprocessor.get o Context.Proof
330 val set_preproc = Preprocessor.map o K
335 structure P = OuterParse and K = OuterKeyword
338 P.group "option" ((P.reserved "sequential" >> K Sequential)
339 || ((P.reserved "default" |-- P.term) >> Default)
340 || (P.reserved "domintros" >> K DomIntros)
341 || (P.reserved "tailrec" >> K Tailrec))
343 fun config_parser default =
344 (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
345 >> (fn opts => fold apply_opt opts default)
347 val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
350 P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
353 SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
354 --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
356 val statements_ow = P.enum1 "|" statement_ow
358 val flags_statements = statements_ow
359 >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
361 fun fundef_parser default_cfg =
362 config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements