# HG changeset patch # User wenzelm # Date 1419026506 -3600 # Node ID 9312710451f5433de95ef91abc56bbe28e4038ff # Parent 05cb83f083b948ccdba973fda455a193476359e2 just one data slot per program unit; tuned signature; diff -r 05cb83f083b9 -r 9312710451f5 src/HOL/Tools/Function/fun.ML --- a/src/HOL/Tools/Function/fun.ML Fri Dec 19 22:53:43 2014 +0100 +++ b/src/HOL/Tools/Function/fun.ML Fri Dec 19 23:01:46 2014 +0100 @@ -160,7 +160,7 @@ THEN auto_tac ctxt fun prove_termination lthy = Function.prove_termination NONE - (Function_Common.get_termination_prover lthy) lthy + (Function_Common.termination_prover_tac lthy) lthy in lthy |> add pat_completeness_auto |> snd diff -r 05cb83f083b9 -r 9312710451f5 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Fri Dec 19 22:53:43 2014 +0100 +++ b/src/HOL/Tools/Function/function.ML Fri Dec 19 23:01:46 2014 +0100 @@ -279,7 +279,7 @@ val get_congs = Function_Context_Tree.get_function_congs -fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t +fun get_info ctxt t = Item_Net.retrieve (get_functions ctxt) t |> the_single |> snd diff -r 05cb83f083b9 -r 9312710451f5 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Fri Dec 19 22:53:43 2014 +0100 +++ b/src/HOL/Tools/Function/function_common.ML Fri Dec 19 23:01:46 2014 +0100 @@ -6,27 +6,25 @@ signature FUNCTION_DATA = sig - -type info = - {is_partial : bool, - defname : string, - (* contains no logical entities: invariant under morphisms: *) - add_simps : (binding -> binding) -> string -> (binding -> binding) -> - Token.src list -> thm list -> local_theory -> thm list * local_theory, - fnames : string list, - case_names : string list, - fs : term list, - R : term, - dom: term, - psimps: thm list, - pinducts: thm list, - simps : thm list option, - inducts : thm list option, - termination : thm, - cases : thm list, - pelims: thm list list, - elims: thm list list option} - + type info = + {is_partial : bool, + defname : string, + (*contains no logical entities: invariant under morphisms:*) + add_simps : (binding -> binding) -> string -> (binding -> binding) -> + Token.src list -> thm list -> local_theory -> thm list * local_theory, + fnames : string list, + case_names : string list, + fs : term list, + R : term, + dom: term, + psimps: thm list, + pinducts: thm list, + simps : thm list option, + inducts : thm list option, + termination : thm, + cases : thm list, + pelims: thm list list, + elims: thm list list option} end structure Function_Data : FUNCTION_DATA = @@ -35,7 +33,7 @@ type info = {is_partial : bool, defname : string, - (* contains no logical entities: invariant under morphisms: *) + (*contains no logical entities: invariant under morphisms:*) add_simps : (binding -> binding) -> string -> (binding -> binding) -> Token.src list -> thm list -> local_theory -> thm list * local_theory, fnames : string list, @@ -64,7 +62,30 @@ val graph_name : string -> string val rel_name : string -> string val dom_name : string -> string - val apply_termination_rule : Proof.context -> int -> tactic + val split_def : Proof.context -> (string -> 'a) -> term -> + string * (string * typ) list * term list * term list * term + val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit + type fixes = ((string * typ) * mixfix) list + type 'a spec = (Attrib.binding * 'a list) list + datatype function_config = FunctionConfig of + {sequential: bool, + default: string option, + domintros: bool, + partials: bool} + type preproc = function_config -> Proof.context -> fixes -> term spec -> + (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) + val fname_of : term -> string + val mk_case_names : int -> string -> int -> string list + val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) -> + preproc + val termination_rule_tac : Proof.context -> int -> tactic + val store_termination_rule : thm -> Context.generic -> Context.generic + val get_functions : Proof.context -> (term * info) Item_Net.T + val add_function_data : info -> Context.generic -> Context.generic + val termination_prover_tac : Proof.context -> tactic + val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic + val get_preproc: Proof.context -> preproc + val set_preproc: preproc -> Context.generic -> Context.generic datatype function_result = FunctionResult of {fs: term list, G: term, @@ -77,33 +98,12 @@ termination : thm, domintros : thm list option} val transform_function_data : info -> morphism -> info - val get_function : Proof.context -> (term * info) Item_Net.T val import_function_data : term -> Proof.context -> info option val import_last_function : Proof.context -> info option - val add_function_data : info -> Context.generic -> Context.generic - val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic - val get_termination_prover : Proof.context -> tactic - val store_termination_rule : thm -> Context.generic -> Context.generic - datatype function_config = FunctionConfig of - {sequential: bool, - default: string option, - domintros: bool, - partials: bool} val default_config : function_config - val split_def : Proof.context -> (string -> 'a) -> term -> - string * (string * typ) list * term list * term list * term - val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit - type fixes = ((string * typ) * mixfix) list - type 'a spec = (Attrib.binding * 'a list) list - type preproc = function_config -> Proof.context -> fixes -> term spec -> - (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) - val fname_of : term -> string - val mk_case_names : int -> string -> int -> string list - val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) -> preproc - val get_preproc: Proof.context -> preproc - val set_preproc: preproc -> Context.generic -> Context.generic val function_parser : function_config -> - ((function_config * (binding * string option * mixfix) list) * (Attrib.binding * string) list) parser + ((function_config * (binding * string option * mixfix) list) * + (Attrib.binding * string) list) parser end structure Function_Common : FUNCTION_COMMON = @@ -113,37 +113,188 @@ local open Function_Lib in -(* Profiling *) -val profile = Unsynchronized.ref false; + +(* profiling *) + +val profile = Unsynchronized.ref false fun PROFILE msg = if !profile then timeap_msg msg else I val acc_const_name = @{const_name Wellfounded.accp} fun mk_acc domT R = - Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R + Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R val function_name = suffix "C" val graph_name = suffix "_graph" val rel_name = suffix "_rel" val dom_name = suffix "_dom" -(* Termination rules *) + +(* analyzing function equations *) + +fun split_def ctxt check_head geq = + let + fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] + val qs = Term.strip_qnt_vars @{const_name Pure.all} geq + val imp = Term.strip_qnt_body @{const_name Pure.all} geq + val (gs, eq) = Logic.strip_horn imp + + val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) + handle TERM _ => error (input_error "Not an equation") + + val (head, args) = strip_comb f_args + + val fname = fst (dest_Free head) handle TERM _ => "" + val _ = check_head fname + in + (fname, qs, gs, args, rhs) + end + +(*check for all sorts of errors in the input*) +fun check_defs ctxt fixes eqs = + let + val fnames = map (fst o fst) fixes + + fun check geq = + let + fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) + + fun check_head fname = + member (op =) fnames fname orelse + input_error ("Illegal equation head. Expected " ^ commas_quote fnames) + + val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq + + val _ = length args > 0 orelse input_error "Function has no arguments:" + + fun add_bvs t is = add_loose_bnos (t, 0, is) + val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) + |> map (fst o nth (rev qs)) -(* FIXME just one data slot (record) per program unit *) -structure TerminationRule = Generic_Data -( - type T = thm list - val empty = [] - val extend = I - val merge = Thm.merge_thms -); + val _ = null rvs orelse input_error + ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^ + " occur" ^ plural "s" "" rvs ^ " on right hand side only:") + + val _ = forall (not o Term.exists_subterm + (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) + orelse input_error "Defined function may not occur in premises or arguments" + + val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args + val funvars = + filter + (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs + val _ = null funvars orelse (warning (cat_lines + ["Bound variable" ^ plural " " "s " funvars ^ + commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ + " in function position.", "Misspelled constructor???"]); true) + in + (fname, length args) + end -val get_termination_rules = TerminationRule.get -val store_termination_rule = TerminationRule.map o cons -val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof + val grouped_args = AList.group (op =) (map check eqs) + val _ = grouped_args + |> map (fn (fname, ars) => + length (distinct (op =) ars) = 1 orelse + error ("Function " ^ quote fname ^ + " has different numbers of arguments in different equations")) + + val not_defined = subtract (op =) (map fst grouped_args) fnames + val _ = null not_defined + orelse error ("No defining equations for function" ^ + plural " " "s " not_defined ^ commas_quote not_defined) + + fun check_sorts ((fname, fT), _) = + Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type}) + orelse error (cat_lines + ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", + Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) + + val _ = map check_sorts fixes + in + () + end -(* Function definition result data *) +(* preprocessors *) + +type fixes = ((string * typ) * mixfix) list +type 'a spec = (Attrib.binding * 'a list) list + +datatype function_config = FunctionConfig of + {sequential: bool, + default: string option, + domintros: bool, + partials: bool} + +type preproc = function_config -> Proof.context -> fixes -> term spec -> + (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) + +val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o + HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all + +fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k + | mk_case_names _ _ 0 = [] + | mk_case_names _ n 1 = [n] + | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) + +fun empty_preproc check (_: function_config) (ctxt: Proof.context) (fixes: fixes) spec = + let + val (bnds, tss) = split_list spec + val ts = flat tss + val _ = check ctxt fixes ts + val fnames = map (fst o fst) fixes + val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts + + fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) + (indices ~~ xs) |> map (map snd) + + (* using theorem names for case name currently disabled *) + val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat + in + (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) + end + + +(* context data *) + +structure Data = Generic_Data +( + type T = + thm list * + (term * info) Item_Net.T * + (Proof.context -> tactic) * + preproc + val empty: T = + ([], + Item_Net.init (op aconv o apply2 fst) (single o fst), + fn _ => error "Termination prover not configured", + empty_preproc check_defs) + val extend = I + fun merge + ((termination_rules1, functions1, termination_prover1, preproc1), + (termination_rules2, functions2, _, _)) : T = + (Thm.merge_thms (termination_rules1, termination_rules2), + Item_Net.merge (functions1, functions2), + termination_prover1, + preproc1) +) + +val termination_rule_tac = resolve_tac o #1 o Data.get o Context.Proof +val store_termination_rule = Data.map o @{apply 4(1)} o cons + +val get_functions = #2 o Data.get o Context.Proof +fun add_function_data (info : info as {fs, termination, ...}) = + (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs) + #> store_termination_rule termination + +fun termination_prover_tac ctxt = #3 (Data.get (Context.Proof ctxt)) ctxt +val set_termination_prover = Data.map o @{apply 4(3)} o K + +val get_preproc = #4 o Data.get o Context.Proof +val set_preproc = Data.map o @{apply 4(4)} o K + + +(* function definition result data *) datatype function_result = FunctionResult of {fs: term list, @@ -173,17 +324,6 @@ elims = Option.map (map fact) elims, pelims = map fact pelims } end -(* FIXME just one data slot (record) per program unit *) -structure FunctionData = Generic_Data -( - type T = (term * info) Item_Net.T; - val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst); - val extend = I; - fun merge tabs : T = Item_Net.merge tabs; -) - -val get_function = FunctionData.get o Context.Proof; - fun lift_morphism thy f = let fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t)) @@ -205,194 +345,42 @@ SOME (transform_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) handle Pattern.MATCH => NONE in - get_first match (Item_Net.retrieve (get_function ctxt) t) + get_first match (Item_Net.retrieve (get_functions ctxt) t) end fun import_last_function ctxt = - case Item_Net.content (get_function ctxt) of + (case Item_Net.content (get_functions ctxt) of [] => NONE | (t, _) :: _ => - let - val ([t'], ctxt') = Variable.import_terms true [t] ctxt - in - import_function_data t' ctxt' - end - -fun add_function_data (data : info as {fs, termination, ...}) = - FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) - #> store_termination_rule termination + let val ([t'], ctxt') = Variable.import_terms true [t] ctxt + in import_function_data t' ctxt' end) -(* Default Termination Prover *) +(* configuration management *) -(* FIXME just one data slot (record) per program unit *) -structure TerminationProver = Generic_Data -( - type T = Proof.context -> tactic - val empty = (fn _ => error "Termination prover not configured") - val extend = I - fun merge (a, _) = a -) - -val set_termination_prover = TerminationProver.put -fun get_termination_prover ctxt = TerminationProver.get (Context.Proof ctxt) ctxt - - -(* Configuration management *) -datatype function_opt - = Sequential +datatype function_opt = + Sequential | Default of string | DomIntros | No_Partials -datatype function_config = FunctionConfig of - {sequential: bool, - default: string option, - domintros: bool, - partials: bool} - -fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) = - FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials} - | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) = - FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials} - | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) = - FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials} - | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) = - FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false} +fun apply_opt Sequential (FunctionConfig {sequential = _, default, domintros, partials}) = + FunctionConfig + {sequential = true, default = default, domintros = domintros, partials = partials} + | apply_opt (Default d) (FunctionConfig {sequential, default = _, domintros, partials}) = + FunctionConfig + {sequential = sequential, default = SOME d, domintros = domintros, partials = partials} + | apply_opt DomIntros (FunctionConfig {sequential, default, domintros = _, partials}) = + FunctionConfig + {sequential = sequential, default = default, domintros = true, partials = partials} + | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials = _}) = + FunctionConfig + {sequential = sequential, default = default, domintros = domintros, partials = false} val default_config = FunctionConfig { sequential=false, default=NONE, domintros=false, partials=true} - -(* Analyzing function equations *) - -fun split_def ctxt check_head geq = - let - fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] - val qs = Term.strip_qnt_vars @{const_name Pure.all} geq - val imp = Term.strip_qnt_body @{const_name Pure.all} geq - val (gs, eq) = Logic.strip_horn imp - - val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) - handle TERM _ => error (input_error "Not an equation") - - val (head, args) = strip_comb f_args - - val fname = fst (dest_Free head) handle TERM _ => "" - val _ = check_head fname - in - (fname, qs, gs, args, rhs) - end - -(* Check for all sorts of errors in the input *) -fun check_defs ctxt fixes eqs = - let - val fnames = map (fst o fst) fixes - - fun check geq = - let - fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) - - fun check_head fname = - member (op =) fnames fname orelse - input_error ("Illegal equation head. Expected " ^ commas_quote fnames) - - val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq - - val _ = length args > 0 orelse input_error "Function has no arguments:" - - fun add_bvs t is = add_loose_bnos (t, 0, is) - val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) - |> map (fst o nth (rev qs)) - - val _ = null rvs orelse input_error - ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^ - " occur" ^ plural "s" "" rvs ^ " on right hand side only:") - - val _ = forall (not o Term.exists_subterm - (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) - orelse input_error "Defined function may not occur in premises or arguments" - - val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args - val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs - val _ = null funvars orelse (warning (cat_lines - ["Bound variable" ^ plural " " "s " funvars ^ - commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ - " in function position.", "Misspelled constructor???"]); true) - in - (fname, length args) - end - - val grouped_args = AList.group (op =) (map check eqs) - val _ = grouped_args - |> map (fn (fname, ars) => - length (distinct (op =) ars) = 1 - orelse error ("Function " ^ quote fname ^ - " has different numbers of arguments in different equations")) - - val not_defined = subtract (op =) (map fst grouped_args) fnames - val _ = null not_defined - orelse error ("No defining equations for function" ^ - plural " " "s " not_defined ^ commas_quote not_defined) - - fun check_sorts ((fname, fT), _) = - Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type}) - orelse error (cat_lines - ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", - Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) - - val _ = map check_sorts fixes - in - () - end - -(* Preprocessors *) - -type fixes = ((string * typ) * mixfix) list -type 'a spec = (Attrib.binding * 'a list) list -type preproc = function_config -> Proof.context -> fixes -> term spec -> - (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) - -val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o - HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all - -fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k - | mk_case_names _ n 0 = [] - | mk_case_names _ n 1 = [n] - | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) - -fun empty_preproc check (_: function_config) (ctxt: Proof.context) (fixes: fixes) spec = - let - val (bnds, tss) = split_list spec - val ts = flat tss - val _ = check ctxt fixes ts - val fnames = map (fst o fst) fixes - val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts - - fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) - (indices ~~ xs) |> map (map snd) - - (* using theorem names for case name currently disabled *) - val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat - in - (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) - end - -(* FIXME just one data slot (record) per program unit *) -structure Preprocessor = Generic_Data -( - type T = preproc - val empty : T = empty_preproc check_defs - val extend = I - fun merge (a, _) = a -) - -val get_preproc = Preprocessor.get o Context.Proof -val set_preproc = Preprocessor.map o K - - - local val option_parser = Parse.group (fn () => "option") ((Parse.reserved "sequential" >> K Sequential) diff -r 05cb83f083b9 -r 9312710451f5 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Fri Dec 19 22:53:43 2014 +0100 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri Dec 19 23:01:46 2014 +0100 @@ -209,7 +209,7 @@ end) 1 st; fun lexicographic_order_tac quiet ctxt = - TRY (Function_Common.apply_termination_rule ctxt 1) THEN + TRY (Function_Common.termination_rule_tac ctxt 1) THEN lex_order_tac quiet ctxt (auto_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems termination_simp}))) diff -r 05cb83f083b9 -r 9312710451f5 src/HOL/Tools/Function/relation.ML --- a/src/HOL/Tools/Function/relation.ML Fri Dec 19 22:53:43 2014 +0100 +++ b/src/HOL/Tools/Function/relation.ML Fri Dec 19 23:01:46 2014 +0100 @@ -23,7 +23,7 @@ | _ => Seq.empty; fun relation_tac ctxt rel i = - TRY (Function_Common.apply_termination_rule ctxt i) + TRY (Function_Common.termination_rule_tac ctxt i) THEN inst_state_tac rel; @@ -45,7 +45,7 @@ | _ => Seq.empty; fun relation_infer_tac ctxt rel i = - TRY (Function_Common.apply_termination_rule ctxt i) + TRY (Function_Common.termination_rule_tac ctxt i) THEN inst_state_infer_tac ctxt rel; end diff -r 05cb83f083b9 -r 9312710451f5 src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Dec 19 22:53:43 2014 +0100 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Dec 19 23:01:46 2014 +0100 @@ -314,7 +314,7 @@ end) fun gen_sizechange_tac orders autom_tac ctxt = - TRY (Function_Common.apply_termination_rule ctxt 1) + TRY (Function_Common.termination_rule_tac ctxt 1) THEN TRY (Termination.wf_union_tac ctxt) THEN (rtac @{thm wf_empty} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)