1(*  Title:      HOL/Tools/Function/function_common.ML
2    Author:     Alexander Krauss, TU Muenchen
3
4Common definitions and other infrastructure for the function package.
5*)
6
7signature FUNCTION_COMMON =
8sig
9  type info =
10   {is_partial : bool,
11    defname : binding,
12      (*contains no logical entities: invariant under morphisms:*)
13    add_simps : (binding -> binding) -> string -> (binding -> binding) ->
14      Token.src list -> thm list -> local_theory -> thm list * local_theory,
15    fnames : binding list,
16    case_names : string list,
17    fs : term list,
18    R : term,
19    dom: term,
20    psimps: thm list,
21    pinducts: thm list,
22    simps : thm list option,
23    inducts : thm list option,
24    termination : thm,
25    totality : thm option,
26    cases : thm list,
27    pelims: thm list list,
28    elims: thm list list option}
29  val profile : bool Unsynchronized.ref
30  val PROFILE : string -> ('a -> 'b) -> 'a -> 'b
31  val mk_acc : typ -> term -> term
32  val split_def : Proof.context -> (string -> 'a) -> term ->
33    string * (string * typ) list * term list * term list * term
34  val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit
35  type fixes = ((string * typ) * mixfix) list
36  type 'a spec = (Attrib.binding * 'a list) list
37  datatype function_config = FunctionConfig of
38   {sequential: bool,
39    default: string option,
40    domintros: bool,
41    partials: bool}
42  type preproc = function_config -> Proof.context -> fixes -> term spec ->
43    term list * (thm list -> thm spec) * (thm list -> thm list list) * string list
44  val fname_of : term -> string
45  val mk_case_names : int -> string -> int -> string list
46  val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) ->
47    preproc
48  val termination_rule_tac : Proof.context -> int -> tactic
49  val store_termination_rule : thm -> Context.generic -> Context.generic
50  val retrieve_function_data : Proof.context -> term -> (term * info) list
51  val add_function_data : info -> Context.generic -> Context.generic
52  val termination_prover_tac : bool -> Proof.context -> tactic
53  val set_termination_prover : (bool -> Proof.context -> tactic) -> Context.generic ->
54    Context.generic
55  val get_preproc: Proof.context -> preproc
56  val set_preproc: preproc -> Context.generic -> Context.generic
57  datatype function_result = FunctionResult of
58   {fs: term list,
59    G: term,
60    R: term,
61    dom: term,
62    psimps : thm list,
63    simple_pinducts : thm list,
64    cases : thm list,
65    pelims : thm list list,
66    termination : thm,
67    domintros : thm list option}
68  val transform_function_data : morphism -> info -> info
69  val import_function_data : term -> Proof.context -> info option
70  val import_last_function : Proof.context -> info option
71  val default_config : function_config
72  val function_parser : function_config ->
73    (function_config * ((binding * string option * mixfix) list * Specification.multi_specs_cmd)) parser
74end
75
76structure Function_Common : FUNCTION_COMMON =
77struct
78
79local open Function_Lib in
80
81(* info *)
82
83type info =
84 {is_partial : bool,
85  defname : binding,
86    (*contains no logical entities: invariant under morphisms:*)
87  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
88    Token.src list -> thm list -> local_theory -> thm list * local_theory,
89  fnames : binding list,
90  case_names : string list,
91  fs : term list,
92  R : term,
93  dom: term,
94  psimps: thm list,
95  pinducts: thm list,
96  simps : thm list option,
97  inducts : thm list option,
98  termination : thm,
99  totality : thm option,
100  cases : thm list,
101  pelims : thm list list,
102  elims : thm list list option}
103
104fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
105  simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
106    let
107      val term = Morphism.term phi
108      val thm = Morphism.thm phi
109      val fact = Morphism.fact phi
110    in
111      { add_simps = add_simps, case_names = case_names, fnames = fnames,
112        fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
113        pinducts = fact pinducts, simps = Option.map fact simps,
114        inducts = Option.map fact inducts, termination = thm termination,
115        totality = Option.map thm totality, defname = Morphism.binding phi defname,
116        is_partial = is_partial, cases = fact cases,
117        elims = Option.map (map fact) elims, pelims = map fact pelims }
118    end
119
120
121(* profiling *)
122
123val profile = Unsynchronized.ref false
124
125fun PROFILE msg = if !profile then timeap_msg msg else I
126
127val acc_const_name = \<^const_name>\<open>Wellfounded.accp\<close>
128fun mk_acc domT R =
129  Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R
130
131
132(* analyzing function equations *)
133
134fun split_def ctxt check_head geq =
135  let
136    fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
137    val qs = Term.strip_qnt_vars \<^const_name>\<open>Pure.all\<close> geq
138    val imp = Term.strip_qnt_body \<^const_name>\<open>Pure.all\<close> geq
139    val (gs, eq) = Logic.strip_horn imp
140
141    val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
142      handle TERM _ => error (input_error "Not an equation")
143
144    val (head, args) = strip_comb f_args
145
146    val fname = fst (dest_Free head) handle TERM _ => ""
147    val _ = check_head fname
148  in
149    (fname, qs, gs, args, rhs)
150  end
151
152(*check for various errors in the input*)
153fun check_defs ctxt fixes eqs =
154  let
155    val fnames = map (fst o fst) fixes
156
157    fun check geq =
158      let
159        fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
160
161        fun check_head fname =
162          member (op =) fnames fname orelse
163          input_error ("Illegal equation head. Expected " ^ commas_quote fnames)
164
165        val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
166
167        val _ = length args > 0 orelse input_error "Function has no arguments:"
168
169        fun add_bvs t is = add_loose_bnos (t, 0, is)
170        val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
171                    |> map (fst o nth (rev qs))
172
173        val _ = null rvs orelse input_error
174          ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
175           " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
176
177        val _ = forall (not o Term.exists_subterm
178          (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args)
179          orelse input_error "Defined function may not occur in premises or arguments"
180
181        val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
182        val funvars =
183          filter
184            (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
185        val _ = null funvars orelse (warning (cat_lines
186          ["Bound variable" ^ plural " " "s " funvars ^
187          commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
188          " in function position.", "Misspelled constructor???"]); true)
189      in
190        (fname, length args)
191      end
192
193    val grouped_args = AList.group (op =) (map check eqs)
194    val _ = grouped_args
195      |> map (fn (fname, ars) =>
196        length (distinct (op =) ars) = 1 orelse
197          error ("Function " ^ quote fname ^
198            " has different numbers of arguments in different equations"))
199
200    val not_defined = subtract (op =) (map fst grouped_args) fnames
201    val _ = null not_defined
202      orelse error ("No defining equations for function" ^
203        plural " " "s " not_defined ^ commas_quote not_defined)
204  in () end
205
206
207(* preprocessors *)
208
209type fixes = ((string * typ) * mixfix) list
210type 'a spec = (Attrib.binding * 'a list) list
211
212datatype function_config = FunctionConfig of
213 {sequential: bool,
214  default: string option,
215  domintros: bool,
216  partials: bool}
217
218type preproc = function_config -> Proof.context -> fixes -> term spec ->
219  term list * (thm list -> thm spec) * (thm list -> thm list list) * string list
220
221val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o
222  HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
223
224fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
225  | mk_case_names _ _ 0 = []
226  | mk_case_names _ n 1 = [n]
227  | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
228
229fun empty_preproc check (_: function_config) (ctxt: Proof.context) (fixes: fixes) spec =
230  let
231    val (bnds, tss) = split_list spec
232    val ts = flat tss
233    val _ = check ctxt fixes ts
234    val fnames = map (fst o fst) fixes
235    val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
236
237    fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1)
238      (indices ~~ xs) |> map (map snd)
239
240    (* using theorem names for case name currently disabled *)
241    val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
242  in
243    (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
244  end
245
246
247(* context data *)
248
249structure Data = Generic_Data
250(
251  type T =
252    thm list *
253    (term * info) Item_Net.T *
254    (bool -> Proof.context -> tactic) *
255    preproc
256  val empty: T =
257   ([],
258    Item_Net.init (op aconv o apply2 fst) (single o fst),
259    fn _ => error "Termination prover not configured",
260    empty_preproc check_defs)
261  val extend = I
262  fun merge
263   ((termination_rules1, functions1, termination_prover1, preproc1),
264    (termination_rules2, functions2, _, _)) : T =
265   (Thm.merge_thms (termination_rules1, termination_rules2),
266    Item_Net.merge (functions1, functions2),
267    termination_prover1,
268    preproc1)
269)
270
271fun termination_rule_tac ctxt = resolve_tac ctxt (#1 (Data.get (Context.Proof ctxt)))
272
273val store_termination_rule = Data.map o @{apply 4(1)} o cons o Thm.trim_context
274
275val get_functions = #2 o Data.get o Context.Proof
276
277fun retrieve_function_data ctxt t =
278  Item_Net.retrieve (get_functions ctxt) t
279  |> (map o apsnd) (transform_function_data (Morphism.transfer_morphism' ctxt));
280
281val add_function_data =
282  transform_function_data Morphism.trim_context_morphism #>
283  (fn info as {fs, termination, ...} =>
284    (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs)
285    #> store_termination_rule termination)
286
287fun termination_prover_tac quiet ctxt = #3 (Data.get (Context.Proof ctxt)) quiet ctxt
288val set_termination_prover = Data.map o @{apply 4(3)} o K
289
290val get_preproc = #4 o Data.get o Context.Proof
291val set_preproc = Data.map o @{apply 4(4)} o K
292
293
294(* function definition result data *)
295
296datatype function_result = FunctionResult of
297 {fs: term list,
298  G: term,
299  R: term,
300  dom: term,
301  psimps : thm list,
302  simple_pinducts : thm list,
303  cases : thm list,
304  pelims : thm list list,
305  termination : thm,
306  domintros : thm list option}
307
308fun import_function_data t ctxt =
309  let
310    val ct = Thm.cterm_of ctxt t
311    fun inst_morph u =
312      Morphism.instantiate_morphism (Thm.match (Thm.cterm_of ctxt u, ct))
313    fun match (u, data) =
314      SOME (transform_function_data (inst_morph u) data) handle Pattern.MATCH => NONE
315  in
316    get_first match (retrieve_function_data ctxt t)
317  end
318
319fun import_last_function ctxt =
320  (case Item_Net.content (get_functions ctxt) of
321    [] => NONE
322  | (t, _) :: _ =>
323      let val ([t'], ctxt') = Variable.import_terms true [t] ctxt
324      in import_function_data t' ctxt' end)
325
326
327(* configuration management *)
328
329datatype function_opt =
330    Sequential
331  | Default of string
332  | DomIntros
333  | No_Partials
334
335fun apply_opt Sequential (FunctionConfig {sequential = _, default, domintros, partials}) =
336      FunctionConfig
337        {sequential = true, default = default, domintros = domintros, partials = partials}
338  | apply_opt (Default d) (FunctionConfig {sequential, default = _, domintros, partials}) =
339      FunctionConfig
340        {sequential = sequential, default = SOME d, domintros = domintros, partials = partials}
341  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros = _, partials}) =
342      FunctionConfig
343        {sequential = sequential, default = default, domintros = true, partials = partials}
344  | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials = _}) =
345      FunctionConfig
346        {sequential = sequential, default = default, domintros = domintros, partials = false}
347
348val default_config =
349  FunctionConfig { sequential=false, default=NONE,
350    domintros=false, partials=true}
351
352local
353  val option_parser = Parse.group (fn () => "option")
354    ((Parse.reserved "sequential" >> K Sequential)
355     || ((Parse.reserved "default" |-- Parse.term) >> Default)
356     || (Parse.reserved "domintros" >> K DomIntros)
357     || (Parse.reserved "no_partials" >> K No_Partials))
358
359  fun config_parser default =
360    (Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.list1 option_parser) --| \<^keyword>\<open>)\<close>) [])
361     >> (fn opts => fold apply_opt opts default)
362in
363  fun function_parser default_cfg =
364      config_parser default_cfg -- Parse_Spec.specification
365end
366
367
368end
369end
370