10 signature FUNCTION_DATA =

    11 sig

    13 type info =

    14  {is_partial : bool,

    15   defname : string,

    16     (* contains no logical entities: invariant under morphisms: *)

    17   add_simps : (binding -> binding) -> string -> (binding -> binding) ->

    18     Attrib.src list -> thm list -> local_theory -> thm list * local_theory,

    19   case_names : string list,

    20   fs : term list,

    21   R : term,

    22   psimps: thm list,

    23   pinducts: thm list,

    24   simps : thm list option,

    25   inducts : thm list option,

    26   termination: thm}

    27 

    28 end

    29 

    30 structure Function_Data : FUNCTION_DATA =

    31 struct

    32 

    33 type info =

    34  {is_partial : bool,

    35   defname : string,

    36     (* contains no logical entities: invariant under morphisms: *)

    37   add_simps : (binding -> binding) -> string -> (binding -> binding) ->

    38     Attrib.src list -> thm list -> local_theory -> thm list * local_theory,

    39   case_names : string list,

    40   fs : term list,

    41   R : term,

    42   psimps: thm list,

    43   pinducts: thm list,

    44   simps : thm list option,

    45   inducts : thm list option,

    46   termination: thm}

    47 

    48 end

    52 

    53 open Function_Data

    54 

    55 local open Function_Lib in

    56 

    57 (* Profiling *)

    58 val profile = Unsynchronized.ref false;

    59 

    60 fun PROFILE msg = if !profile then timeap_msg msg else I

    61 

    62 

    63 val acc_const_name = @{const_name accp}

    64 fun mk_acc domT R =

    65   Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 

    66 

    67 val function_name = suffix "C"

    68 val graph_name = suffix "_graph"

    69 val rel_name = suffix "_rel"

    70 val dom_name = suffix "_dom"

    71 

    72 (* Termination rules *)

    73 

    74 structure TerminationRule = Generic_Data

    75 (

    76   type T = thm list

    77   val empty = []

    78   val extend = I

    79   val merge = Thm.merge_thms

    80 );

    81 

    82 val get_termination_rules = TerminationRule.get

    83 val store_termination_rule = TerminationRule.map o cons

    84 val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof

    85 

    86 

    87 (* Function definition result data *)

    88 

    89 datatype function_result = FunctionResult of

    90  {fs: term list,

    91   G: term,

    92   R: term,

    93   psimps : thm list,

    94   simple_pinducts : thm list,

    95   cases : thm,

    96   termination : thm,

    97   domintros : thm list option}

    98 

    99 fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,

   100   simps, inducts, termination, defname, is_partial} : info) phi =

   101     let

   102       val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi

   103       val name = Binding.name_of o Morphism.binding phi o Binding.name

   104     in

   105       { add_simps = add_simps, case_names = case_names,

   106         fs = map term fs, R = term R, psimps = fact psimps,

   107         pinducts = fact pinducts, simps = Option.map fact simps,

   108         inducts = Option.map fact inducts, termination = thm termination,

   109         defname = name defname, is_partial=is_partial }

   110     end

   111 

   112 structure FunctionData = Generic_Data

   113 (

   114   type T = (term * info) Item_Net.T;

   115   val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);

   116   val extend = I;

   117   fun merge tabs : T = Item_Net.merge tabs;

   118 )

   119 

   120 val get_function = FunctionData.get o Context.Proof;

   121 

   122 

   123 fun lift_morphism thy f =

   124   let

   125     val term = Drule.term_rule thy f

   126   in

   127     Morphism.thm_morphism f $> Morphism.term_morphism term

   128     $> Morphism.typ_morphism (Logic.type_map term)

   129   end

   130 

   131 fun import_function_data t ctxt =

   132   let

   133     val thy = Proof_Context.theory_of ctxt

   134     val ct = cterm_of thy t

   135     val inst_morph = lift_morphism thy o Thm.instantiate

   136 

   137     fun match (trm, data) =

   138       SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))

   139       handle Pattern.MATCH => NONE

   140   in

   141     get_first match (Item_Net.retrieve (get_function ctxt) t)

   142   end

   143 

   144 fun import_last_function ctxt =

   145   case Item_Net.content (get_function ctxt) of

   146     [] => NONE

   147   | (t, data) :: _ =>

   148     let

   149       val ([t'], ctxt') = Variable.import_terms true [t] ctxt

   150     in

   151       import_function_data t' ctxt'

   152     end

   153 

   154 val all_function_data = Item_Net.content o get_function

   155 

   156 fun add_function_data (data : info as {fs, termination, ...}) =

   157   FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)

   158   #> store_termination_rule termination

   159 

   160 

   161 (* Simp rules for termination proofs *)

   162 

   163 structure Termination_Simps = Named_Thms

   164 (

   165   val name = "termination_simp"

   166   val description = "simplification rules for termination proofs"

   167 )

   168 

   169 

   170 (* Default Termination Prover *)

   171 

   172 structure TerminationProver = Generic_Data

   173 (

   174   type T = Proof.context -> tactic

   175   val empty = (fn _ => error "Termination prover not configured")

   176   val extend = I

   177   fun merge (a, _) = a

   178 )

   179 

   180 val set_termination_prover = TerminationProver.put

   181 val get_termination_prover = TerminationProver.get o Context.Proof

   219 

   220 (* Analyzing function equations *)

   221 

   222 fun split_def ctxt check_head geq =

   223   let

   224     fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]

   225     val qs = Term.strip_qnt_vars "all" geq

   226     val imp = Term.strip_qnt_body "all" geq

   227     val (gs, eq) = Logic.strip_horn imp

   228 

   229     val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)

   230       handle TERM _ => error (input_error "Not an equation")

   231 

   232     val (head, args) = strip_comb f_args

   233 

   234     val fname = fst (dest_Free head) handle TERM _ => ""

   235     val _ = check_head fname

   236   in

   237     (fname, qs, gs, args, rhs)

   238   end

   239 

   240 (* Check for all sorts of errors in the input *)

   241 fun check_defs ctxt fixes eqs =

   242   let

   243     val fnames = map (fst o fst) fixes

   244 

   245     fun check geq =

   246       let

   247         fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])

   248 

   249         fun check_head fname =

   250           member (op =) fnames fname orelse

   251           input_error ("Illegal equation head. Expected " ^ commas_quote fnames)

   252 

   253         val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq

   254 

   255         val _ = length args > 0 orelse input_error "Function has no arguments:"

   256 

   257         fun add_bvs t is = add_loose_bnos (t, 0, is)

   258         val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))

   259                     |> map (fst o nth (rev qs))

   260 

   261         val _ = null rvs orelse input_error

   262           ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^

   263            " occur" ^ plural "s" "" rvs ^ " on right hand side only:")

   264 

   265         val _ = forall (not o Term.exists_subterm

   266           (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args)

   267           orelse input_error "Defined function may not occur in premises or arguments"

   268 

   269         val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args

   270         val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs

   271         val _ = null funvars orelse (warning (cat_lines

   272           ["Bound variable" ^ plural " " "s " funvars ^

   273           commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^

   274           " in function position.", "Misspelled constructor???"]); true)

   275       in

   276         (fname, length args)

   277       end

   278 

   279     val grouped_args = AList.group (op =) (map check eqs)

   280     val _ = grouped_args

   281       |> map (fn (fname, ars) =>

   282         length (distinct (op =) ars) = 1

   283         orelse error ("Function " ^ quote fname ^

   284           " has different numbers of arguments in different equations"))

   285 

   286     val not_defined = subtract (op =) (map fst grouped_args) fnames

   287     val _ = null not_defined

   288       orelse error ("No defining equations for function" ^

   289         plural " " "s " not_defined ^ commas_quote not_defined)

   290 

   291     fun check_sorts ((fname, fT), _) =

   292       Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)

   293       orelse error (cat_lines

   294       ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",

   295        Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])

   296 

   297     val _ = map check_sorts fixes

   298   in

   299     ()

   300   end

   301 

   302 (* Preprocessors *)

   303 

   304 type fixes = ((string * typ) * mixfix) list

   305 type 'a spec = (Attrib.binding * 'a list) list

   306 type preproc = nominal_function_config -> Proof.context -> fixes -> term spec ->

   307   (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)

   308 

   309 val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o

   310   HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all

   311 

   312 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k

   313   | mk_case_names _ n 0 = []

   314   | mk_case_names _ n 1 = [n]

   315   | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)

   316 

   317 fun empty_preproc check _ ctxt fixes spec =

   318   let

   319     val (bnds, tss) = split_list spec

   320     val ts = flat tss

   321     val _ = check ctxt fixes ts

   322     val fnames = map (fst o fst) fixes

   323     val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts

   324 

   325     fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 

   326       (indices ~~ xs) |> map (map snd)

   327 

   328     (* using theorem names for case name currently disabled *)

   329     val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat

   330   in

   331     (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)

   332   end

   333 

   334 structure Preprocessor = Generic_Data

   335 (

   336   type T = preproc

   337   val empty : T = empty_preproc check_defs

   338   val extend = I

   339   fun merge (a, _) = a

   340 )

   341 

   342 val get_preproc = Preprocessor.get o Context.Proof

   343 val set_preproc = Preprocessor.map o K

   344 

   345 

   346 

   347 local

   348   val option_parser = Parse.group "option"

   349     ((Parse.reserved "sequential" >> K Sequential)

   350      || ((Parse.reserved "default" |-- Parse.term) >> Default)

   351      || (Parse.reserved "domintros" >> K DomIntros)

   352      || (Parse.reserved "no_partials" >> K No_Partials))

   353 

   354   fun config_parser default =

   355     (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])

   356      >> (fn opts => fold Nominal_Function_Common.apply_opt opts default)

   357 in

   358   fun function_parser default_cfg =

   359       config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs

   361 

   362 

   363 end

   364 end