# HG changeset patch # User krauss # Date 1174567017 -3600 # Node ID 62cdd4b3e96bfc0f5e744521f6ddcc8317c65bc6 # Parent 1fe951654cee2ee4c04d7c6138466b5930b663d3 made function syntax strict, requiring | to separate equations; cleanup diff -r 1fe951654cee -r 62cdd4b3e96b src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Thu Mar 22 13:36:56 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_common.ML Thu Mar 22 13:36:57 2007 +0100 @@ -9,27 +9,23 @@ structure FundefCommon = struct -(* Theory Dependencies *) -val acc_const_name = "Accessible_Part.acc" - +(* Profiling *) val profile = ref false; fun PROFILE msg = if !profile then timeap_msg msg else I + +val acc_const_name = "Accessible_Part.acc" fun mk_acc domT R = Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R -(* FIXME, unused *) val function_name = suffix "C" val graph_name = suffix "_graph" val rel_name = suffix "_rel" val dom_name = suffix "_dom" -val dest_rel_name = unsuffix "_rel" - type depgraph = int IntGraph.T - datatype ctx_tree = Leaf of term | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list) @@ -160,30 +156,38 @@ | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true } +fun target_of (FundefConfig {target, ...}) = target -local structure P = OuterParse and K = OuterKeyword in - -val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false +local + structure P = OuterParse and K = OuterKeyword -val option_parser = (P.$$$ "sequential" >> K Sequential) - || ((P.reserved "default" |-- P.term) >> Default) - || (P.reserved "domintros" >> K DomIntros) - || (P.reserved "tailrec" >> K Tailrec) - || ((P.$$$ "in" |-- P.xname) >> Target) + val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false + + val option_parser = (P.$$$ "sequential" >> K Sequential) + || ((P.reserved "default" |-- P.term) >> Default) + || (P.reserved "domintros" >> K DomIntros) + || (P.reserved "tailrec" >> K Tailrec) + || ((P.$$$ "in" |-- P.xname) >> Target) -fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") []) + fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") []) >> (fn opts => fold apply_opt opts def) + fun pipe_list1 s = P.enum1 "|" s + + val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" + + fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t]))) + + val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false) + --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("","")) + + val statements_ow = pipe_list1 statement_ow +in + fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow end - - - - end - - (* Common Abbreviations *) structure FundefAbbrev = @@ -191,32 +195,13 @@ fun implies_elim_swp x y = implies_elim y x -(* Some HOL things frequently used *) +(* HOL abbreviations *) val boolT = HOLogic.boolT val mk_prod = HOLogic.mk_prod -val mk_mem = HOLogic.mk_mem val mk_eq = HOLogic.mk_eq val eq_const = HOLogic.eq_const val Trueprop = HOLogic.mk_Trueprop - val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT -fun mk_relmem (x,y) R = Trueprop (mk_mem (mk_prod (x, y), R)) - -fun mk_subset T A B = - let val sT = HOLogic.mk_setT T - in Const ("Orderings.less_eq", sT --> sT --> boolT) $ A $ B end - - -(* with explicit types: Needed with loose bounds *) -fun mk_relmemT xT yT (x,y) R = - let - val pT = HOLogic.mk_prodT (xT, yT) - val RT = HOLogic.mk_setT pT - in - Const ("op :", [pT, RT] ---> boolT) - $ (HOLogic.pair_const xT yT $ x $ y) - $ R - end fun free_to_var (Free (v,T)) = Var ((v,0),T) | free_to_var _ = raise Match diff -r 1fe951654cee -r 62cdd4b3e96b src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Thu Mar 22 13:36:56 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Thu Mar 22 13:36:57 2007 +0100 @@ -181,25 +181,18 @@ local structure P = OuterParse and K = OuterKeyword in - -fun or_list1 s = P.enum1 "|" s -val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" -val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false)) -val statements_ow = or_list1 statement_ow - - -fun fun_cmd fixes statements lthy = +fun fun_cmd config fixes statements lthy = lthy - |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config + |> FundefPackage.add_fundef fixes statements config ||> by_pat_completeness_simp |-> termination_by_lexicographic_order val funP = OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl - ((P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow) - >> (fn ((target, fixes), statements) => - (Toplevel.local_theory target (fun_cmd fixes statements)))); + (fundef_parser FundefCommon.fun_config + >> (fn ((config, fixes), statements) => + (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements)))); val _ = OuterSyntax.add_parsers [funP]; end diff -r 1fe951654cee -r 62cdd4b3e96b src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Thu Mar 22 13:36:56 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Mar 22 13:36:57 2007 +0100 @@ -10,13 +10,13 @@ signature FUNDEF_PACKAGE = sig val add_fundef : (string * string option * mixfix) list - -> ((bstring * Attrib.src list) * (string * bool) list) list list + -> ((bstring * Attrib.src list) * (string * bool)) list -> FundefCommon.fundef_config -> local_theory -> string * Proof.state val add_fundef_i: (string * typ option * mixfix) list - -> ((bstring * Attrib.src list) * (term * bool) list) list list + -> ((bstring * Attrib.src list) * (term * bool)) list -> FundefCommon.fundef_config -> local_theory -> string * Proof.state @@ -47,15 +47,15 @@ in xs ~~ f ys end fun restore_spec_structure reps spec = - (burrow o burrow_snd o burrow o K) reps spec + (burrow_snd o burrow o K) reps spec fun add_simps fixes spec sort label moreatts simps lthy = let val fnames = map (fst o fst) fixes val (saved_spec_simps, lthy) = - fold_map (fold_map note_theorem) (restore_spec_structure simps spec) lthy - val saved_simps = flat (map snd (flat saved_spec_simps)) + fold_map note_theorem (restore_spec_structure simps spec) lthy + val saved_simps = flat (map snd saved_spec_simps) val simps_by_f = sort saved_simps @@ -99,21 +99,21 @@ fun prep_with_flags prep fixspec eqnss_flags global_flag lthy = let - val eqnss = map (map (apsnd (map fst))) eqnss_flags - val flags = map (map (map (fn (_, f) => global_flag orelse f) o snd)) eqnss_flags + val flags = map (fn x => global_flag orelse (snd (snd x))) eqnss_flags + val eqns = map (apsnd (single o fst)) eqnss_flags val ((fixes, _), ctxt') = prep fixspec [] lthy - val spec = map (fn eqns => snd (fst (prep [] eqns ctxt'))) eqnss - |> map (map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)))) (* Add quantifiers *) - |> map2 (map2 (fn fs => fn (r, thms) => (r, fs ~~ thms))) flags - |> (burrow o burrow_snd o burrow) - (FundefSplit.split_some_equations lthy) - |> map (map (apsnd flat)) + + fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt'))) + |> apsnd the_single + + val spec = map prep_eqn eqns + |> map (apsnd (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)) (* Add quantifiers *) + |> burrow_snd (fn ts => FundefSplit.split_some_equations ctxt' (flags ~~ ts)) in ((fixes, spec), ctxt') end - fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy = let val FundefConfig {sequential, default, tailrec, ...} = config @@ -122,8 +122,7 @@ val defname = mk_defname fixes - val t_eqns = spec - |> flat |> map snd |> flat (* flatten external structure *) + val t_eqns = spec |> map snd |> flat (* flatten external structure *) val ((goalstate, cont, sort_cont), lthy) = FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy @@ -225,26 +224,13 @@ local structure P = OuterParse and K = OuterKeyword in - - -fun or_list1 s = P.enum1 "|" s - -val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false - -val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" -val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false)) -val statements_ow = or_list1 statement_ow - - val functionP = OuterSyntax.command "function" "define general recursive functions" K.thy_goal - ((config_parser default_config -- P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow) - >> (fn (((config, target), fixes), statements) => - Toplevel.local_theory_to_proof target (add_fundef fixes statements config #> snd) + (fundef_parser default_config + >> (fn ((config, fixes), statements) => + Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config #> snd) #> Toplevel.print)); - - val terminationP = OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal (P.opt_target -- Scan.option P.name @@ -252,7 +238,6 @@ Toplevel.print o Toplevel.local_theory_to_proof target (setup_termination_proof name))); - val _ = OuterSyntax.add_parsers [functionP]; val _ = OuterSyntax.add_parsers [terminationP]; val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];