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