--- 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)