1structure DefnBase :> DefnBase =
2struct
3
4open HolKernel
5
6val ERR = mk_HOL_ERR "DefnBase";
7
8(*---------------------------------------------------------------------------
9    The type of definitions. This is an attempt to gather all the
10    information about a definition in one place.
11 ---------------------------------------------------------------------------*)
12
13datatype defn
14   = ABBREV  of {eqn:thm, bind:string}
15   | PRIMREC of {eqs:thm, ind:thm, bind:string}
16   | NONREC  of {eqs:thm, ind:thm, SV:term list, stem:string}
17   | STDREC  of {eqs:thm list, ind:thm, R:term,SV:term list,stem:string}
18   | MUTREC  of {eqs:thm list, ind:thm, R:term, SV:term list,
19                 stem:string,union:defn}
20   | NESTREC of {eqs:thm list, ind:thm, R:term, SV:term list,
21                 stem:string, aux:defn}
22   | TAILREC of {eqs:thm list, ind:thm, R:term, SV:term list, stem:string}
23
24fun all_terms d =
25  case d of
26      ABBREV{eqn,...} => [concl eqn]
27    | PRIMREC {eqs,ind,...} => [concl eqs, concl ind]
28    | NONREC {eqs,ind,SV,...} => concl eqs::concl ind::SV
29    | STDREC {eqs,ind,R,SV,...} => R :: concl ind :: map concl eqs @ SV
30    | MUTREC {eqs,ind,R,SV,union,...} =>
31        R :: concl ind :: map concl eqs @ SV @ all_terms union
32    | NESTREC {eqs,ind,R,SV,aux,...} =>
33        R :: concl ind :: map concl eqs @ SV @ all_terms aux
34    | TAILREC {eqs,ind,R,SV,...} => R :: concl ind :: map concl eqs @ SV
35
36local open Portable
37      fun kind (ABBREV _)  = "abbreviation"
38        | kind (NONREC  _) = "non-recursive"
39        | kind (STDREC  _) = "recursive"
40        | kind (PRIMREC _) = "primitive recursion"
41        | kind (MUTREC  _) = "mutual recursion"
42        | kind (NESTREC _) = "nested recursion"
43        | kind (TAILREC _) = "nonterminating tail recursion"
44      fun hyps thl = HOLset.listItems
45                       (foldl (fn (th,s) => HOLset.union(hypset th, s))
46                              empty_tmset thl)
47in
48fun pp_defn d =
49  let open smpp
50      val pp_term = lift Parse.pp_term
51      val pp_thm  = lift Parse.pp_thm
52      fun pp_rec (eqs,ind,tcs) =
53        block CONSISTENT 0 (
54          add_string "Equation(s) :" >>
55          add_break(1,0) >>
56          pr_list pp_thm add_newline eqs >>
57          add_newline >> add_newline >>
58          add_string "Induction :" >>
59          add_break(1,0) >>
60          pp_thm ind >>
61          (if null tcs then nothing
62           else
63             (add_newline >> add_newline >>
64              add_string "Termination conditions :" >>
65              add_break(1,2) >>
66              block CONSISTENT 0 (
67                 pr_list (fn (n,tm) =>
68                             block CONSISTENT 3 (
69                               add_string (Lib.int_to_string n^". ") >>
70                               pp_term tm
71                             )
72                         )
73                         add_newline
74                         (Lib.enumerate 0 tcs)
75               ))
76          )
77        )
78   fun pp (ABBREV {eqn, ...}) =
79          block CONSISTENT 0 (
80            add_string "Equation :" >>
81            add_break(1,0) >>
82            pp_thm eqn
83          )
84     | pp (PRIMREC{eqs, ind, bind}) =
85          block CONSISTENT 0 (
86            add_string "Equation(s) :" >>
87            add_break(1,0) >>
88            pp_thm eqs
89          )
90     | pp (NONREC {eqs, ind, SV, stem}) =
91          block CONSISTENT 0 (
92             add_string "Equation(s) :" >>
93             add_break(1,0) >>
94             pp_thm eqs >>
95             add_newline >> add_newline >>
96             add_string "Case analysis:" >>
97             add_break(1,0) >> pp_thm ind
98          )
99     | pp (STDREC {eqs, ind, R, SV, stem})        = pp_rec(eqs,ind, hyps eqs)
100     | pp (NESTREC{eqs, ind, R, SV, aux, stem})   = pp_rec(eqs,ind, hyps eqs)
101     | pp (MUTREC {eqs, ind, R, SV, union, stem}) = pp_rec(eqs,ind, hyps eqs)
102     | pp (TAILREC{eqs, ind, R, SV, stem})        = pp_rec(eqs,ind, hyps eqs)
103   val m =
104     block CONSISTENT 0 (
105       add_string "HOL function definition " >>
106       add_string (String.concat ["(",kind d,")"]) >>
107       add_newline >> add_newline >>
108       pp d
109     )
110  in
111    Parse.mlower m
112  end
113end;
114
115
116(*---------------------------------------------------------------------------
117    Congruence rules for termination condition extraction. Before
118    t.c. extraction is performed, the theorems in "non_datatype_congs"
119    are added to the congruence rules arising from datatype definitions,
120    which are held in the TypeBase.
121 ---------------------------------------------------------------------------*)
122
123
124local open boolTheory
125      val non_datatype_congs =
126        ref [LET_CONG, COND_CONG, IMP_CONG, literal_case_CONG]
127in
128  fun read_congs() = !non_datatype_congs
129  fun write_congs L = (non_datatype_congs := L)
130end;
131
132fun add_cong thm = write_congs (thm :: read_congs());
133
134fun drop_cong c =
135 let open boolSyntax
136     val P = same_const c
137     val (cong,rst) =
138         pluck (fn th => P (fst(strip_comb(lhs(snd
139                             (strip_imp(snd(strip_forall(concl th)))))))))
140               (read_congs())
141     val _ = write_congs rst
142 in
143   cong
144 end
145 handle e => raise wrap_exn "DefnBase.drop_cong"
146    (case total dest_thy_const c
147      of NONE => "expected a constant"
148       | SOME{Thy,Name,...} =>
149           ("congruence rule for "
150            ^Lib.quote(Thy^"$"^Name)
151            ^" was not found")) e;
152
153val {export = export_cong,...} =
154    ThmSetData.new_exporter "defncong"
155                            (fn _ (* thy *) => fn namedthms =>
156                                app (add_cong o #2) namedthms)
157
158end
159