1structure OpenTheoryReader :> OpenTheoryReader = struct
2
3open boolSyntax HolKernel Parse OpenTheoryMap OpenTheoryCommon
4
5structure Parse =
6struct
7   open Parse
8   val (Type, Term) = parse_from_grammars listTheory.list_grammars
9end
10
11local open Thm Drule in
12  fun DEDUCT_ANTISYM th1 th2 =
13    IMP_ANTISYM_RULE
14      (DISCH (concl th2) th1)
15      (DISCH (concl th1) th2)
16end
17
18val ERR = mk_HOL_ERR "OpenTheoryReader"
19
20type reader =
21{ define_tyop  : {name:thy_tyop, ax:thm, args:hol_type list, rep:thy_const, abs:thy_const} ->
22                 {rep_abs:thm, abs_rep:thm}
23, define_const : thy_const -> term -> thm
24, axiom        : thm Net.net -> (term list * term) -> thm
25, const_name   : otname -> thy_const
26, tyop_name    : otname -> thy_tyop
27}
28
29fun const_name_in_map n = Map.find(const_from_ot_map(),n)
30fun tyop_name_in_map n = Map.find(tyop_from_ot_map(),n)
31
32local
33  open Thm Drule
34  fun uneta a t = BETA_CONV(mk_comb(mk_abs(a,t),a))
35in
36  fun uneta_type_bijection th =
37  let
38    val (a,eq) = dest_forall(concl th)
39    val (l,r) = dest_eq eq
40  in
41    EXT (GEN a (TRANS (TRANS (uneta a l) (SPEC a th)) (SYM (uneta a r))))
42  end
43end
44
45fun define_tyop_in_thy
46  {name={Thy=tthy,Tyop},ax,args,
47   rep={Thy=rthy,Name=rep},abs={Thy=athy,Name=abs}} =
48let
49  open boolLib
50  val (P,t) = dest_comb (concl ax)
51  val v   = variant (free_vars P) (mk_var ("v",type_of t))
52  val ct  = current_theory()
53  val _   = if tthy = ct then () else
54            raise ERR "define_tyop_in_thy" ("wrong theory: "^ct^" (wanted "^tthy^" for "^Tyop^")")
55  val th  = new_type_definition(Tyop,EXISTS(mk_exists(v,mk_comb(P,v)),t) ax)
56  val _   = if athy = tthy andalso rthy = tthy then () else
57            raise ERR "define_tyop_in_thy" ("wrong theory: "^ct^" (given "^athy^" for "^abs^" and "^rthy^" for "^rep^")")
58  val bij = define_new_type_bijections {name=Tyop^"_bij",ABS=abs,REP=rep,tyax=th}
59  val (ar,ra) = CONJ_PAIR bij
60in {rep_abs=uneta_type_bijection ra,
61    abs_rep=uneta_type_bijection ar} end
62
63fun define_const_in_thy ML_name {Thy,Name} rhs = let
64  val ct = current_theory()
65in
66  if Thy = ct then
67    new_definition ((ML_name Name)^"_def",mk_eq(mk_var(Name,type_of rhs),rhs))
68  else raise ERR "define_const_in_thy" ("wrong theory: "^ct^" (wanted "^Thy^" for "^Name^")")
69end
70
71local
72  open boolLib BasicProvers metisLib
73  fun ins (th,n) = Net.insert (concl th,th) n
74  val imp_def = METIS_PROVE[]``$==> = (\p q. p /\ q <=> p)``;
75  val and_def = prove(``$/\ = (\p q. (\f:bool->bool->bool. f p q) = (\f. f T T))``,
76    SRW_TAC [][FUN_EQ_THM,EQ_IMP_THM]);
77  val exists_def = prove(``$? = (\P. !q. (!x. P x ==> q) ==> q)``,
78    SRW_TAC [][FUN_EQ_THM] THEN
79    SUBST_TAC [GSYM (ISPEC ``P:'a->bool`` ETA_THM)] THEN
80    METIS_TAC [])
81  val imp1 = METIS_PROVE[]``!t. t ==> t``
82  val split = (map GEN_ALL) o CONJUNCTS o SPEC_ALL
83in
84  val base_thms = foldl ins Net.empty ((CONJUNCTS NOT_CLAUSES)@(split EQ_CLAUSES)@(split IMP_CLAUSES)@(split AND_CLAUSES)@[imp_def,and_def,exists_def,imp1])
85end
86
87(* useful elsewhere? *)
88val NUMERAL_conv = let (* wrap numeric literals in NUMERAL tag *)
89  open Conv numSyntax arithmeticTheory
90  exception Nonlit
91  fun lit_conv tm = let (* detect literals, and replace 0 by ZERO *)
92    val (f,_) = dest_comb tm in
93      if f ~~ bit1_tm orelse f ~~ bit2_tm then
94        RAND_CONV lit_conv tm
95      else raise Nonlit
96  end handle HOL_ERR _ =>
97    if tm ~~ zero_tm then SYM ALT_ZERO else
98    if tm ~~ alt_zero_tm then raise UNCHANGED else
99    raise Nonlit
100  fun add_tag_conv tm = SYM (SPEC tm NUMERAL_DEF)
101  fun conv tm = let
102    val (f,_) = dest_comb tm in
103      if f ~~ bit1_tm orelse f ~~ bit2_tm then
104        (RAND_CONV lit_conv THENC add_tag_conv) tm
105      handle Nonlit => RAND_CONV conv tm
106      else if f ~~ numeral_tm then
107        raise UNCHANGED (* nb: assuming incoming NUMERAL tags are good *)
108        (* alternative: check if it's actually a literal with lit_conv, and
109        strip the tag if Nonlit is raised *)
110      else COMB_CONV conv tm
111  end handle HOL_ERR _ => ABS_CONV conv tm
112      handle HOL_ERR _ =>
113      if tm ~~ alt_zero_tm then ALT_ZERO else raise UNCHANGED
114in conv end
115
116local
117  fun eq (h,c) th =
118    aconv (concl th) c andalso
119    HOLset.equal (HOLset.addList(empty_tmset,h), hypset th)
120  fun from_net n (h,c) = Lib.first (eq (h,c)) (Net.index c n)
121in
122fun axiom_in_db ths (h,c) =
123    from_net base_thms (h,c)
124handle HOL_ERR _ =>
125  fst(snd(Lib.first (fn (_,(th,_)) => eq (h,c) th) (DB.match [] c)))
126handle HOL_ERR _ =>
127  from_net ths (h,c)
128handle HOL_ERR e => let
129  val _ = case h of [] => () | _ => raise HOL_ERR e
130  val l = !metisTools.limit
131  val _ = metisTools.limit := {time=SOME 10.0,infs=NONE}
132  val th = metisTools.METIS_PROVE [] c
133  val _ = metisTools.limit := l
134in th end
135handle HOL_ERR _ => (
136  Feedback.HOL_MESG("cheating on: ``" ^ (Parse.term_to_string c) ^ "`` CHEAT!");
137  mk_thm(h,c)
138  )
139end
140
141fun st_(st,{stack,dict,thms,line_num}) = {stack=st,dict=dict,thms=thms}
142fun push (ob,st) = st_(ob::(#stack st),st)
143local open Substring in
144  val trimlr = fn s => string(trimr 1 (triml 1 (full s)))
145  val trimr  = fn s => string(trimr 1 (full s))
146end
147
148fun raw_read_article input
149  {const_name,tyop_name,define_tyop,define_const,axiom} = let
150  val ERR = ERR "read_article"
151  fun unOTermls c = List.map (fn OTerm t => t | _ => raise ERR (c^" failed to pop a list of terms"))
152  fun unOTypels c = List.map (fn OType t => t | _ => raise ERR (c^" failed to pop a list of types"))
153  fun ot_to_const c s = const_name (string_to_otname s)
154  handle _ => raise ERR (c^": no map from "^s^" to a constant")
155  fun ot_to_tyop  c s = tyop_name (string_to_otname s)
156  handle _ => raise ERR (c^": no map from "^s^" to a type operator")
157  val mk_vartype = mk_vartype o tyvar_from_ot o string_to_otname
158  fun f "absTerm"(st as {stack=OTerm b::OVar v::os,...}) = st_(OTerm(mk_abs(v,b))::os,st)
159    | f "absThm" (st as {stack=OThm th::OVar v::os,...}) = (st_(OThm(ABS v th)::os,st)
160      handle HOL_ERR e => raise ERR "absThm: failed")
161    | f "appTerm"(st as {stack=OTerm x::OTerm f::os,...})= st_(OTerm(mk_comb(f,x))::os,st)
162    | f "appThm" (st as {stack=OThm xy::OThm fg::os,...})= let
163        val (f,g) = dest_eq(concl fg)
164        val (x,y) = dest_eq(concl xy)
165        val fxgx  = AP_THM fg x
166        val gxgy  = AP_TERM g xy
167      in st_(OThm(TRANS fxgx gxgy)::os,st) end
168    | f "assume"       (st as {stack=OTerm t::os,...})          = st_(OThm(ASSUME t)::os,st)
169    | f "axiom"        (st as {stack=OTerm t::OList ts::os,thms,...}) = st_(OThm(axiom thms (unOTermls "axiom" ts,t))::os,st)
170    | f "betaConv"     (st as {stack=OTerm t::os,...})          = st_(OThm(BETA_CONV t)::os,st)
171    | f "cons"         (st as {stack=OList t::h::os,...})       = st_(OList(h::t)::os,st)
172    | f "const"        (st as {stack=OName n::os,...})          = st_(OConst (ot_to_const "const" n)::os,st)
173    | f "constTerm"    (st as {stack=OType Ty::OConst {Thy,Name}::os,...})
174                     = st_(OTerm(mk_thy_const {Ty=Ty,Thy=Thy,Name=Name})::os,st)
175    | f "deductAntisym"(st as {stack=OThm t1::OThm t2::os,...}) = st_(OThm(DEDUCT_ANTISYM t1 t2)::os,st)
176    | f "def"         {stack=ONum k::x::os,dict,thms,...}       = {stack=x::os,dict=Map.insert(dict,k,x),thms=thms}
177    | f "defineConst" (st as {stack=OTerm t::OName n::os,...})  = let
178        val c = ot_to_const "defineConst" n
179        val def = define_const c t
180        handle Map.NotFound => raise ERR ("defineConst: no map from "^thy_const_to_string c^" to a definition function")
181      in st_(OThm def::OConst c::os,st) end
182    | f "defineTypeOp"  (st as {stack=OThm ax::OList ls::OName rep::OName abs::OName n::os,...}) = let
183        val ls = List.map (fn OName s => mk_vartype s | _ => raise ERR "defineTypeOp failed to pop a list of names") ls
184        val tyop = ot_to_tyop "defineTypeOp" n
185        val ot_to_const = ot_to_const "defineTypeOp"
186        val {abs_rep,rep_abs} = define_tyop {name=tyop,ax=ax,args=ls,rep=ot_to_const rep,abs=ot_to_const abs}
187        val (abs,foo) = dest_comb(#2(dest_abs(lhs(concl abs_rep))))
188        val (rep,_)   = dest_comb foo
189        val {Thy,Name,...} = dest_thy_const rep val rep = {Thy=Thy,Name=Name}
190        val {Thy,Name,...} = dest_thy_const abs val abs = {Thy=Thy,Name=Name}
191      in st_(OThm rep_abs::OThm abs_rep::OConst rep::OConst abs::OTypeOp tyop::os,st) end
192    | f "eqMp"   (st as {stack=OThm f::OThm fg::os,...})     = (st_(OThm(EQ_MP fg f)::os,st)
193      handle HOL_ERR e => raise ERR "EqMp failed")
194    | f "nil"    st                                          = push(OList [],st)
195    | f "opType" (st as {stack=OList ls::OTypeOp {Thy,Tyop}::os,...})
196               = st_(OType(mk_thy_type{Thy=Thy,Tyop=Tyop,Args=unOTypels "opType" ls})::os,st)
197(*
198    | f "pop"    (st as {stack=OList[OList hl,OTerm c]::OThm th::os,line_num,...}) = let
199      val hl = unOTermls "pop" hl
200      val h = HOLset.addList(empty_tmset,hl)
201      val _ = if aconv c (concl th) then () else trace
202       ("types",1) (fn () => (
203         Feedback.HOL_MESG(Parse.term_to_backend_string(c));
204         Feedback.HOL_MESG(Parse.term_to_backend_string(concl th));
205         raise ERR ("proved wrong theorem (c) line: "^(Int.toString line_num))
206         )) ()
207     val _ = if HOLset.equal(h,hypset th) then () else trace
208       ("assumptions",1) (fn() => (
209         Feedback.HOL_MESG(Parse.thm_to_backend_string(mk_thm(hl,c)));
210         Feedback.HOL_MESG(Parse.thm_to_backend_string(th));
211         raise ERR ("proved wrong theorem (h) line: "^(Int.toString line_num))
212       )) ()
213     in st_(OThm th::os,st) end
214*)
215    | f "pop"    (st as {stack=x::os,...})                   = st_(os,st)
216    | f "ref"    (st as {stack=ONum k::os,dict,...})         = st_(Map.find(dict,k)::os,st)
217    | f "refl"   (st as {stack=OTerm t::os,...})             = st_(OThm(REFL t)::os,st)
218    | f "remove" {stack=ONum k::os,dict,thms,...}            = let
219        val (dict,x) = Map.remove(dict,k)
220      in {stack=x::os,dict=dict,thms=thms} end
221    | f "subst"  (st as {stack=OThm th::OList[OList tys,OList tms]::os,...}) = let
222        val tys = List.map (fn OList [OName a, OType t] => {redex=mk_vartype a, residue=t}
223                             | _ => raise ERR "subst failed to pop a list of [name,type] pairs") tys
224        val tms = List.map (fn OList [OVar v, OTerm t] => {redex=v, residue=t}
225                             | _ => raise ERR "subst failed to pop a list of [var,term] pairs") tms
226        val th = INST_TYPE tys th
227        val th = INST tms th
228      in st_(OThm th::os,st) end
229    | f "thm"    {stack=OTerm c::OList ls::OThm th::os,dict,thms,...} = let
230        val th = EQ_MP (ALPHA (concl th) c) th
231        handle HOL_ERR _ => raise ERR "thm: desired conclusion not alpha-equivalent to theorem's conclusion"
232        fun ft (OTerm h, th) = let
233          val c = concl th
234          val th = DISCH h th
235          val c' = concl th
236        in
237          if aconv c c' then
238            Drule.ADD_ASSUM h th
239          else let
240            val (h',_) = boolSyntax.dest_imp c'
241            val h'h = ALPHA h' h
242            val th = Drule.SUBS_OCCS [([1],h'h)] th
243          in Drule.UNDISCH th end
244        end | ft _ = raise ERR "thm failed to pop a list of terms"
245        val th = List.foldl ft th ls
246      in {stack=os,dict=dict,thms=Net.insert(concl th,th)thms} end
247    | f "typeOp"  (st as {stack=OName n::os,...})          = st_(OTypeOp (ot_to_tyop "typeOp" n)::os,st)
248    | f "version" (st as {stack=ONum n::os,...})           = if n = 6 then st_(os,st) else raise ERR "unsupported article version"
249    | f "var"     (st as {stack=OType t::OName n::os,...}) = st_(OVar(mk_var(n,t))::os,st)
250    | f "varTerm" (st as {stack=OVar t::os,...})           = st_(OTerm t::os,st)
251    | f "varType" (st as {stack=OName n::os,...})          = st_(OType(mk_vartype n)::os,st)
252    | f s (st as {stack,dict,thms,line_num,...}) = let val c = String.sub(s,0) open Char Option Int
253      in if c = #"\"" then push(OName(trimlr s),st) else
254         if isDigit c then push(ONum(valOf(fromString s)),st) else
255         if c = #"#" then {stack=stack,dict=dict,thms=thms} else
256         raise ERR ("Unknown command (or bad arguments) on line "^(Int.toString line_num)^": <<"^s^">>")
257      end
258  fun loop (x as {line_num,...}) = case TextIO.inputLine input of
259    NONE => x before TextIO.closeIn(input)
260  | SOME line => let
261      val {stack,dict,thms} = f (trimr line) x
262    in loop {stack=stack,dict=dict,thms=thms,line_num=line_num+1} end
263in
264  Net.map (Conv.CONV_RULE NUMERAL_conv)
265    (#thms (loop {stack=[],dict=Map.mkDict(Int.compare),thms=Net.empty,line_num=1}))
266end
267
268fun read_article s r = raw_read_article (TextIO.openIn s) r
269
270fun delete_unused_consts thms =
271app (fn c => let
272    val find = find_term (fn t => c ~~ t)
273  in
274    if exists
275       (fn th => (can find (concl th)) orelse
276                 (isSome(HOLset.find (can find) (hypset th))))
277       thms
278    then ()
279    else delete_const (fst (dest_const c))
280  end)
281(constants "-")
282
283end
284