1signature DefnBase =
2sig
3  type term = Term.term
4  type thm  = Thm.thm
5
6 datatype defn
7   = ABBREV  of {eqn:thm, bind:string}
8   | PRIMREC of {eqs:thm, ind:thm, bind:string}
9   | NONREC  of {eqs:thm, ind:thm, SV:term list, stem:string}
10   | STDREC  of {eqs:thm list, ind:thm, R:term,SV:term list,stem:string}
11   | MUTREC  of {eqs:thm list, ind:thm, R:term,SV:term list,
12                 stem:string,union:defn}
13   | NESTREC of {eqs:thm list, ind:thm, R:term,SV:term list,
14                 stem:string,aux:defn}
15   | TAILREC of {eqs:thm list, ind:thm, R:term, SV:term list, stem:string}
16
17
18  val pp_defn : defn Parse.pprinter
19  val all_terms : defn -> term list
20    (* conclusions of theorems, SV variables, R *)
21
22  (* Used to control context tracking during termination
23     condition extraction *)
24
25  val read_congs  : unit -> thm list
26  val write_congs : thm list -> unit
27  val add_cong    : thm -> unit
28  val drop_cong   : term -> thm
29
30  val export_cong : string -> unit
31
32  (* record various flavours of definition, keyed by constant and a
33     "tag", which is a user-choosable string. Assume that "user" and
34     "compute" exist for example.
35
36     Another might be "PMATCH", which would be the definition with
37     case constants translated into PMATCH versions.
38  *)
39  val register_defn : string -> thm -> unit
40  val lookup_defn : term -> string -> thm option
41
42  val register_indn : thm * term list -> unit
43  val lookup_indn : term -> (thm * term list) option
44
45  (* register_defn is given a tag and a theorem which is a conjunction of
46     possibly universally quantified equations.  The machinery here
47     will create a sub-conjunction of the clauses per constant (and this is
48     what is returned by lookup_defn).
49
50     Induction theorems have some number of induction variables (P1,
51     P2, ..) where each corresponds to a defined constant. This list
52     of constants is what is passed into register_indn alongside the
53     induction theorem. When a term is looked up, if lookup_indn t
54     returns SOME (th, ts), then t will be among the ts.
55   *)
56
57  val const_eq_ref : Abbrev.conv ref
58  val elim_triv_literal_CONV : Abbrev.conv
59  val one_line_ify : PmatchHeuristics.pmatch_heuristic option -> thm -> thm
60
61end
62