krauss@34232: (*  Title:      HOL/Tools/Function/function_common.ML
krauss@33099:     Author:     Alexander Krauss, TU Muenchen
krauss@33099: 
krauss@41114: Common definitions and other infrastructure for the function package.
krauss@33099: *)
krauss@33099: 
krauss@34230: signature FUNCTION_DATA =
krauss@34230: sig
krauss@34230: 
krauss@34230: type info =
krauss@34230:  {is_partial : bool,
krauss@34230:   defname : string,
krauss@34230:     (* contains no logical entities: invariant under morphisms: *)
krauss@34230:   add_simps : (binding -> binding) -> string -> (binding -> binding) ->
krauss@34230:     Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
krauss@34230:   case_names : string list,
krauss@34230:   fs : term list,
krauss@34230:   R : term,
krauss@34230:   psimps: thm list,
krauss@34230:   pinducts: thm list,
krauss@34231:   simps : thm list option,
krauss@34231:   inducts : thm list option,
krauss@34232:   termination: thm}
krauss@34230: 
krauss@34230: end
krauss@34230: 
krauss@34230: structure Function_Data : FUNCTION_DATA =
krauss@34230: struct
krauss@34230: 
krauss@34230: type info =
krauss@34230:  {is_partial : bool,
krauss@34230:   defname : string,
krauss@34230:     (* contains no logical entities: invariant under morphisms: *)
krauss@34230:   add_simps : (binding -> binding) -> string -> (binding -> binding) ->
krauss@34230:     Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
krauss@34230:   case_names : string list,
krauss@34230:   fs : term list,
krauss@34230:   R : term,
krauss@34230:   psimps: thm list,
krauss@34230:   pinducts: thm list,
krauss@34231:   simps : thm list option,
krauss@34231:   inducts : thm list option,
krauss@34232:   termination: thm}
krauss@34230: 
krauss@34230: end
krauss@34230: 
krauss@33099: structure Function_Common =
krauss@33099: struct
krauss@33099: 
krauss@34230: open Function_Data
krauss@34230: 
krauss@33099: local open Function_Lib in
krauss@33099: 
krauss@33099: (* Profiling *)
krauss@33099: val profile = Unsynchronized.ref false;
krauss@33099: 
krauss@33099: fun PROFILE msg = if !profile then timeap_msg msg else I
krauss@33099: 
krauss@33099: 
krauss@33099: val acc_const_name = @{const_name accp}
krauss@33099: fun mk_acc domT R =
krauss@34232:   Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
krauss@33099: 
krauss@33099: val function_name = suffix "C"
krauss@33099: val graph_name = suffix "_graph"
krauss@33099: val rel_name = suffix "_rel"
krauss@33099: val dom_name = suffix "_dom"
krauss@33099: 
krauss@33099: (* Termination rules *)
krauss@33099: 
wenzelm@33519: structure TerminationRule = Generic_Data
krauss@33099: (
krauss@33099:   type T = thm list
krauss@33099:   val empty = []
krauss@33099:   val extend = I
wenzelm@33519:   val merge = Thm.merge_thms
krauss@33099: );
krauss@33099: 
krauss@33099: val get_termination_rules = TerminationRule.get
krauss@33099: val store_termination_rule = TerminationRule.map o cons
krauss@33099: val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
krauss@33099: 
krauss@33099: 
krauss@33099: (* Function definition result data *)
krauss@33099: 
krauss@34232: datatype function_result = FunctionResult of
krauss@34232:  {fs: term list,
krauss@34232:   G: term,
krauss@34232:   R: term,
krauss@34232:   psimps : thm list,
krauss@34232:   simple_pinducts : thm list,
krauss@34232:   cases : thm,
krauss@34232:   termination : thm,
krauss@34232:   domintros : thm list option}
krauss@33099: 
krauss@34230: fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
krauss@34231:   simps, inducts, termination, defname, is_partial} : info) phi =
krauss@33099:     let
krauss@33099:       val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
krauss@33099:       val name = Binding.name_of o Morphism.binding phi o Binding.name
krauss@33099:     in
krauss@34230:       { add_simps = add_simps, case_names = case_names,
krauss@34232:         fs = map term fs, R = term R, psimps = fact psimps,
krauss@34231:         pinducts = fact pinducts, simps = Option.map fact simps,
krauss@34231:         inducts = Option.map fact inducts, termination = thm termination,
krauss@34230:         defname = name defname, is_partial=is_partial }
krauss@33099:     end
krauss@33099: 
wenzelm@33519: structure FunctionData = Generic_Data
krauss@33099: (
krauss@34230:   type T = (term * info) Item_Net.T;
wenzelm@33373:   val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
krauss@33099:   val extend = I;
wenzelm@33519:   fun merge tabs : T = Item_Net.merge tabs;
krauss@34232: )
krauss@33099: 
krauss@33099: val get_function = FunctionData.get o Context.Proof;
krauss@33099: 
krauss@33099: 
krauss@34232: fun lift_morphism thy f =
krauss@34232:   let
krauss@34232:     val term = Drule.term_rule thy f
krauss@34232:   in
krauss@34232:     Morphism.thm_morphism f $> Morphism.term_morphism term
krauss@34232:     $> Morphism.typ_morphism (Logic.type_map term)
krauss@34232:   end
krauss@33099: 
krauss@33099: fun import_function_data t ctxt =
krauss@34232:   let
wenzelm@42361:     val thy = Proof_Context.theory_of ctxt
krauss@34232:     val ct = cterm_of thy t
krauss@34232:     val inst_morph = lift_morphism thy o Thm.instantiate
krauss@33099: 
krauss@34232:     fun match (trm, data) =
krauss@34232:       SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
krauss@34232:       handle Pattern.MATCH => NONE
krauss@34232:   in
krauss@34232:     get_first match (Item_Net.retrieve (get_function ctxt) t)
krauss@34232:   end
krauss@33099: 
krauss@33099: fun import_last_function ctxt =
krauss@34232:   case Item_Net.content (get_function ctxt) of
krauss@34232:     [] => NONE
krauss@34232:   | (t, data) :: _ =>
krauss@34232:     let
krauss@34232:       val ([t'], ctxt') = Variable.import_terms true [t] ctxt
krauss@34232:     in
krauss@34232:       import_function_data t' ctxt'
krauss@34232:     end
krauss@33099: 
krauss@33099: val all_function_data = Item_Net.content o get_function
krauss@33099: 
krauss@34230: fun add_function_data (data : info as {fs, termination, ...}) =
krauss@34232:   FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
krauss@34232:   #> store_termination_rule termination
krauss@33099: 
krauss@33099: 
krauss@33099: (* Simp rules for termination proofs *)
krauss@33099: 
krauss@33099: structure Termination_Simps = Named_Thms
krauss@33099: (
krauss@34232:   val name = "termination_simp"
wenzelm@38764:   val description = "simplification rules for termination proofs"
krauss@34232: )
krauss@33099: 
krauss@33099: 
krauss@33099: (* Default Termination Prover *)
krauss@33099: 
wenzelm@33519: structure TerminationProver = Generic_Data
krauss@33099: (
krauss@36521:   type T = Proof.context -> tactic
krauss@33099:   val empty = (fn _ => error "Termination prover not configured")
krauss@33099:   val extend = I
wenzelm@38761:   fun merge (a, _) = a
krauss@34232: )
krauss@33099: 
krauss@33099: val set_termination_prover = TerminationProver.put
krauss@33099: val get_termination_prover = TerminationProver.get o Context.Proof
krauss@33099: 
krauss@33099: 
krauss@33099: (* Configuration management *)
krauss@34232: datatype function_opt
krauss@33099:   = Sequential
krauss@33099:   | Default of string
krauss@33099:   | DomIntros
krauss@33101:   | No_Partials
krauss@33099: 
krauss@34232: datatype function_config = FunctionConfig of
krauss@34232:  {sequential: bool,
krauss@41417:   default: string option,
krauss@34232:   domintros: bool,
krauss@41846:   partials: bool}
krauss@33099: 
krauss@41846: fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846:     FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials}
krauss@41846:   | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846:     FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials}
krauss@41846:   | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846:     FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials}
krauss@41846:   | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) =
krauss@41846:     FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false}
krauss@33099: 
krauss@33099: val default_config =
krauss@41417:   FunctionConfig { sequential=false, default=NONE,
krauss@41846:     domintros=false, partials=true}
krauss@33099: 
krauss@33099: 
krauss@33099: (* Analyzing function equations *)
krauss@33099: 
krauss@39276: fun split_def ctxt check_head geq =
krauss@34232:   let
krauss@34232:     fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
krauss@34232:     val qs = Term.strip_qnt_vars "all" geq
krauss@34232:     val imp = Term.strip_qnt_body "all" geq
krauss@34232:     val (gs, eq) = Logic.strip_horn imp
krauss@33099: 
krauss@34232:     val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
krauss@34232:       handle TERM _ => error (input_error "Not an equation")
krauss@33099: 
krauss@34232:     val (head, args) = strip_comb f_args
krauss@33099: 
krauss@39276:     val fname = fst (dest_Free head) handle TERM _ => ""
krauss@39276:     val _ = check_head fname
krauss@34232:   in
krauss@34232:     (fname, qs, gs, args, rhs)
krauss@34232:   end
krauss@33099: 
krauss@33099: (* Check for all sorts of errors in the input *)
krauss@33099: fun check_defs ctxt fixes eqs =
krauss@34232:   let
krauss@34232:     val fnames = map (fst o fst) fixes
krauss@34232: 
krauss@34232:     fun check geq =
krauss@34232:       let
krauss@34232:         fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
krauss@33099: 
krauss@39276:         fun check_head fname =
krauss@39276:           member (op =) fnames fname orelse
krauss@39276:           input_error ("Illegal equation head. Expected " ^ commas_quote fnames)
krauss@34232: 
krauss@39276:         val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
krauss@34232: 
krauss@34232:         val _ = length args > 0 orelse input_error "Function has no arguments:"
krauss@34232: 
krauss@34232:         fun add_bvs t is = add_loose_bnos (t, 0, is)
wenzelm@42081:         val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
wenzelm@42081:                     |> map (fst o nth (rev qs))
krauss@34232: 
krauss@34232:         val _ = null rvs orelse input_error
krauss@34232:           ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
krauss@34232:            " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
krauss@34232: 
krauss@34232:         val _ = forall (not o Term.exists_subterm
haftmann@36692:           (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args)
krauss@34232:           orelse input_error "Defined function may not occur in premises or arguments"
krauss@33099: 
krauss@34232:         val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
krauss@34232:         val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
krauss@34232:         val _ = null funvars orelse (warning (cat_lines
krauss@34232:           ["Bound variable" ^ plural " " "s " funvars ^
krauss@34232:           commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
krauss@34232:           " in function position.", "Misspelled constructor???"]); true)
krauss@34232:       in
krauss@34232:         (fname, length args)
krauss@34232:       end
krauss@33099: 
krauss@34232:     val grouped_args = AList.group (op =) (map check eqs)
krauss@34232:     val _ = grouped_args
krauss@34232:       |> map (fn (fname, ars) =>
krauss@34232:         length (distinct (op =) ars) = 1
krauss@34232:         orelse error ("Function " ^ quote fname ^
krauss@34232:           " has different numbers of arguments in different equations"))
krauss@33099: 
krauss@34232:     val not_defined = subtract (op =) (map fst grouped_args) fnames
krauss@34232:     val _ = null not_defined
krauss@34232:       orelse error ("No defining equations for function" ^
krauss@34232:         plural " " "s " not_defined ^ commas_quote not_defined)
krauss@33751: 
krauss@34232:     fun check_sorts ((fname, fT), _) =
wenzelm@42361:       Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)
krauss@34232:       orelse error (cat_lines
krauss@34232:       ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
wenzelm@39134:        Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
krauss@33099: 
krauss@34232:     val _ = map check_sorts fixes
krauss@34232:   in
krauss@34232:     ()
krauss@34232:   end
krauss@33099: 
krauss@33099: (* Preprocessors *)
krauss@33099: 
krauss@33099: type fixes = ((string * typ) * mixfix) list
krauss@33099: type 'a spec = (Attrib.binding * 'a list) list
krauss@34232: type preproc = function_config -> Proof.context -> fixes -> term spec ->
krauss@34232:   (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
krauss@33099: 
krauss@34232: val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o
krauss@34232:   HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
krauss@33099: 
krauss@33099: fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
krauss@33099:   | mk_case_names _ n 0 = []
krauss@33099:   | mk_case_names _ n 1 = [n]
krauss@33099:   | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
krauss@33099: 
krauss@33099: fun empty_preproc check _ ctxt fixes spec =
krauss@34232:   let
krauss@34232:     val (bnds, tss) = split_list spec
krauss@34232:     val ts = flat tss
krauss@34232:     val _ = check ctxt fixes ts
krauss@34232:     val fnames = map (fst o fst) fixes
krauss@34232:     val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
krauss@33099: 
krauss@34232:     fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
krauss@34232:       (indices ~~ xs) |> map (map snd)
krauss@33099: 
krauss@34232:     (* using theorem names for case name currently disabled *)
krauss@34232:     val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
krauss@34232:   in
krauss@34232:     (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
krauss@34232:   end
krauss@33099: 
wenzelm@33519: structure Preprocessor = Generic_Data
krauss@33099: (
krauss@33099:   type T = preproc
krauss@33099:   val empty : T = empty_preproc check_defs
krauss@33099:   val extend = I
wenzelm@33519:   fun merge (a, _) = a
krauss@34232: )
krauss@33099: 
krauss@33099: val get_preproc = Preprocessor.get o Context.Proof
krauss@33099: val set_preproc = Preprocessor.map o K
krauss@33099: 
krauss@33099: 
krauss@33099: 
krauss@34232: local
wenzelm@44357:   val option_parser = Parse.group (fn () => "option")
wenzelm@36960:     ((Parse.reserved "sequential" >> K Sequential)
wenzelm@36960:      || ((Parse.reserved "default" |-- Parse.term) >> Default)
wenzelm@36960:      || (Parse.reserved "domintros" >> K DomIntros)
krauss@41846:      || (Parse.reserved "no_partials" >> K No_Partials))
krauss@33099: 
krauss@34232:   fun config_parser default =
wenzelm@36960:     (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
krauss@34232:      >> (fn opts => fold apply_opt opts default)
krauss@33099: in
krauss@34232:   fun function_parser default_cfg =
wenzelm@36960:       config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
krauss@33099: end
krauss@33099: 
krauss@33099: 
krauss@33099: end
krauss@33099: end