1structure IndDefLib :> IndDefLib =
2struct
3
4local open IndDefRules in end;
5
6open HolKernel Abbrev;
7
8type monoset = InductiveDefinition.monoset;
9
10val ERR = mk_HOL_ERR "IndDefLib";
11val ERRloc = mk_HOL_ERRloc "IndDefLib";
12
13local open Absyn
14      fun head clause =
15         let val appl = last (strip_imp (snd(strip_forall clause)))
16         in fst(strip_app appl)
17         end
18      fun determ M =
19          fst(Term.dest_var M handle HOL_ERR _ => Term.dest_const M)
20           handle HOL_ERR _ => raise ERR "determ" "Non-atom in antiquote"
21      fun dest (AQ (_,tm)) = determ tm
22        | dest (IDENT (_,s)) = s
23        | dest other = raise ERRloc "names_of.reln_names.dest"
24                                    (locn_of_absyn other) "Unexpected structure"
25in
26fun term_of_absyn absyn = let
27  val clauses   = strip_conj absyn
28  fun checkcl a = let
29    val nm = dest (head a)
30  in
31    if mem nm ["/\\", "\\/", "!", "?", "LET",
32               UnicodeChars.conj, UnicodeChars.disj, UnicodeChars.forall,
33               UnicodeChars.exists]
34    then
35      raise ERRloc "term_of_absyn" (locn_of_absyn a)
36                   ("Abstract syntax looks to be trying to redefine "^nm^". "^
37                     "\nThis is probably an error.\nIf you must, define with \
38                     \another name and use overload_on")
39    else nm
40  end
41  val names     = mk_set (map checkcl clauses)
42  val resdata   = List.map (fn s => (s, Parse.hide s)) names
43  fun restore() =
44      List.app (fn (s,d) => Parse.update_overload_maps s d) resdata
45  val tm =
46      Parse.absyn_to_term (Parse.term_grammar()) absyn
47      handle e => (restore(); raise e)
48in
49  restore();
50  (tm, map locn_of_absyn clauses)
51end
52
53fun term_of q = term_of_absyn (Parse.Absyn q)
54
55end;
56
57(* ----------------------------------------------------------------------
58    Store all rule inductions
59   ---------------------------------------------------------------------- *)
60
61val term_rule_map : ({Name:string,Thy:string},thm list)Binarymap.dict ref =
62    ref (Binarymap.mkDict KernelSig.name_compare)
63
64fun listdict_add (d, k, e) =
65    case Binarymap.peek(d, k) of
66      NONE => Binarymap.insert(d,k,[e])
67    | SOME l => Binarymap.insert(d,k,e::l)
68
69fun rule_induction_map() = !term_rule_map
70
71fun ind_thm_to_consts thm = let
72  open boolSyntax
73  val c = concl thm
74  val (_, bod) = strip_forall c
75  val (_, con) = dest_imp bod
76  val cons = strip_conj con
77  fun to_kname {Name,Thy,...} = {Name = Name, Thy = Thy}
78in
79  map (fn t => t |> strip_forall |> #2 |> dest_imp |> #1 |> strip_comb |> #1
80                 |> dest_thy_const |> to_kname)
81      cons
82end
83
84fun add_rule_induction th = let
85  val nm = current_theory()
86  val ts = ind_thm_to_consts th
87in
88  term_rule_map := List.foldl (fn (t,d) => listdict_add(d,t,th))
89                              (!term_rule_map)
90                              ts
91end
92
93(* making it exportable *)
94val {export = export_rule_induction, dest, ...} =
95    ThmSetData.new_exporter "rule_induction" (K (app (add_rule_induction o #2)))
96
97fun thy_rule_inductions thyname = let
98  val segdata =
99    LoadableThyData.segment_data {thy = thyname, thydataty = "rule_induction"}
100in
101  case segdata of
102    NONE => []
103  | SOME d => map #2 (valOf (dest d))
104end
105
106(* ----------------------------------------------------------------------
107    the built-in monoset, that users can update as they prove new
108    monotonicity results about their constants
109   ---------------------------------------------------------------------- *)
110
111val the_monoset = ref InductiveDefinition.bool_monoset
112
113fun mono_name th = let
114  open boolLib
115  val (_, con) = dest_imp (concl th)
116in
117  #1 (dest_const (#1 (strip_comb (#1 (dest_imp con)))))
118end
119
120fun add_mono_thm th = the_monoset := (mono_name th, th) :: (!the_monoset)
121
122(* making it exportable *)
123val {export = export_mono, dest, ...} =
124    ThmSetData.new_exporter "mono" (K (app (add_mono_thm o #2)))
125
126fun thy_monos thyname =
127    case LoadableThyData.segment_data {thy = thyname, thydataty = "mono"} of
128      NONE => []
129    | SOME d => map #2 (valOf (dest d))
130
131(*---------------------------------------------------------------------------
132  given a case theorem of the sort returned by new_inductive_definition
133  return the name of the first new constant mentioned
134  form is
135        (!x y z.  (C x y z = ...)) /\
136        (!u v w.  (D u v w = ...))
137   in which case we return ["C", "D"]
138 ---------------------------------------------------------------------------*)
139
140open InductiveDefinition
141
142fun names_from_casethm thm = let
143  open HolKernel boolSyntax
144  val forallbod = #2 o strip_forall
145  val eqns = thm |> concl |> forallbod |> strip_conj |> map forallbod
146  val cnsts = map (#1 o strip_comb o lhs) eqns
147in
148  map (#1 o dest_const) cnsts
149end
150
151val derive_mono_strong_induction = IndDefRules.derive_mono_strong_induction;
152fun derive_strong_induction (rules,ind) =
153    IndDefRules.derive_mono_strong_induction (!the_monoset) (rules, ind)
154
155fun save_theorems name (rules, indn, strong_ind, cases) = let
156in
157  save_thm(name^"_rules", rules);
158  save_thm(name^"_ind", indn);
159  save_thm(name^"_strongind", strong_ind);
160  save_thm(name^"_cases", cases);
161  export_rule_induction (name ^ "_strongind")
162end
163
164fun Hol_mono_reln name monoset tm = let
165  val _ = Lexis.ok_sml_identifier (name ^ !boolLib.def_suffix) orelse
166          raise ERR "Hol_mono_reln"
167                    ("Bad name for definition: "^ Lib.mlquote name^
168                     " (use xHol_reln to specify a better)")
169  val (rules, indn, cases) = new_inductive_definition monoset name tm
170      (* not! InductiveDefinition.bool_monoset tm *)
171  val strong_ind = derive_strong_induction (rules, indn)
172in
173  save_theorems name (rules, indn, strong_ind, cases);
174  (rules, indn, cases)
175end
176handle e => raise (wrap_exn "IndDefLib" "Hol_mono_reln" e);
177
178
179(* ----------------------------------------------------------------------
180    the standard entry-points
181   ---------------------------------------------------------------------- *)
182
183fun xHol_reln name q = Hol_mono_reln name (!the_monoset) (term_of q)
184
185fun name_from_def t = let
186  open boolSyntax
187  val cs = strip_conj t
188in
189  hd cs |> strip_forall |> #2 |> strip_imp |> #2 |> strip_comb |> #1 |>
190  dest_var |> #1
191end
192
193fun Hol_reln q = let
194  val parse = term_of |> trace ("syntax_error", 0)
195                      |> trace ("show_typecheck_errors", 0)
196              (* turn off verbiage because the Raise below will redisplay any
197                 exceptions *)
198  val def as (def_t,_) = parse q
199  val name = name_from_def def_t
200in
201  Hol_mono_reln name (!the_monoset) def
202end handle e => Raise (wrap_exn "IndDefLib" "Hol_reln" e);
203
204end
205