diff --git a/fusion.ml b/fusion.ml index a08ad1c..7d67f20 100644 --- a/fusion.ml +++ b/fusion.ml @@ -23,6 +23,23 @@ module type Hol_kernel = type thm + type proof = private + Proof of (int * thm * proof_content) + and proof_content = private + Prefl of term + | Ptrans of proof * proof + | Pmkcomb of proof * proof + | Pabs of proof * term + | Pbeta of term + | Passume of term + | Peqmp of proof * proof + | Pdeduct of proof * proof + | Pinst of proof * (term * term) list + | Pinstt of proof * (hol_type * hol_type) list + | Paxiom of term + | Pdef of term * string * hol_type + | Pdeft of proof * term * string * hol_type + val types: unit -> (string * int)list val get_type_arity : string -> int val new_type : (string * int) -> unit @@ -85,6 +102,10 @@ module type Hol_kernel = val new_basic_definition : term -> thm val new_basic_type_definition : string -> string * string -> thm -> thm * thm + + val proofs : unit -> proof list + val proof_of : thm -> proof + val proof_at: int -> proof end;; (* ------------------------------------------------------------------------- *) @@ -101,7 +122,49 @@ module Hol : Hol_kernel = struct | Comb of term * term | Abs of term * term - type thm = Sequent of (term list * term) + + type thm = Sequent of (term list * term * int) + +(*---------------------------------------------------------------------------*) +(* Proof tracing implementation and storage. *) +(*---------------------------------------------------------------------------*) + type proof = + Proof of (int * thm * proof_content) + and proof_content = + Prefl of term + | Ptrans of proof * proof + | Pmkcomb of proof * proof + | Pabs of proof * term + | Pbeta of term + | Passume of term + | Peqmp of proof * proof + | Pdeduct of proof * proof + | Pinst of proof * (term * term) list + | Pinstt of proof * (hol_type * hol_type) list + | Paxiom of term + | Pdef of term * string * hol_type + | Pdeft of proof * term * string * hol_type + + let the_proofs = Hashtbl.create 500000 + let the_proofs_idx = ref (-1) + + let the_proofs_idx_comp p1 p2 = + let (Proof(i1,_,_),Proof(i2,_,_)) = (p1,p2) in (i1 - i2) + + let proofs() = + List.sort the_proofs_idx_comp + (Hashtbl.fold (fun idx pr acc -> pr :: acc) the_proofs []) + + let next_proof_idx() = + let idx = !the_proofs_idx + 1 in + (the_proofs_idx := idx; idx) + + let new_proof pr = + let Proof(idx,thm,content) = pr in + (Hashtbl.add the_proofs idx pr; thm) + + let proof_at p = + Hashtbl.find the_proofs p (* ------------------------------------------------------------------------- *) (* List of current type constants with their arities. *) @@ -485,43 +548,57 @@ module Hol : Hol_kernel = struct (* Basic theorem destructors. *) (* ------------------------------------------------------------------------- *) - let dest_thm (Sequent(asl,c)) = (asl,c) + let dest_thm (Sequent(asl,c,_)) = (asl,c) + + let hyp (Sequent(asl,c,_)) = asl - let hyp (Sequent(asl,c)) = asl + let concl (Sequent(asl,c,_)) = c - let concl (Sequent(asl,c)) = c + let proof_of(Sequent(_,_,p)) = Hashtbl.find the_proofs p (* ------------------------------------------------------------------------- *) (* Basic equality properties; TRANS is derivable but included for efficiency *) (* ------------------------------------------------------------------------- *) let REFL tm = - Sequent([],safe_mk_eq tm tm) + let idx = next_proof_idx() in + let th = Sequent([],safe_mk_eq tm tm,idx) in + new_proof (Proof(idx,th,Prefl tm)) - let TRANS (Sequent(asl1,c1)) (Sequent(asl2,c2)) = + let TRANS (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) = match (c1,c2) with Comb((Comb(Const("=",_),_) as eql),m1),Comb(Comb(Const("=",_),m2),r) - when alphaorder m1 m2 = 0 -> Sequent(term_union asl1 asl2,Comb(eql,r)) + when alphaorder m1 m2 = 0 -> + let idx = next_proof_idx() in + let th = Sequent(term_union asl1 asl2,Comb(eql,r),idx) in + new_proof (Proof(idx,th,Ptrans(Hashtbl.find the_proofs p1, + Hashtbl.find the_proofs p2))) | _ -> failwith "TRANS" (* ------------------------------------------------------------------------- *) (* Congruence properties of equality. *) (* ------------------------------------------------------------------------- *) - let MK_COMB(Sequent(asl1,c1),Sequent(asl2,c2)) = + let MK_COMB(Sequent(asl1,c1,p1),Sequent(asl2,c2,p2)) = match (c1,c2) with Comb(Comb(Const("=",_),l1),r1),Comb(Comb(Const("=",_),l2),r2) -> (match type_of r1 with - Tyapp("fun",[ty;_]) when Pervasives.compare ty (type_of r2) = 0 - -> Sequent(term_union asl1 asl2, - safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2))) + Tyapp("fun",[ty;_]) when Pervasives.compare ty (type_of r2) = 0 -> + let idx = next_proof_idx() in + let th = Sequent(term_union asl1 asl2, + safe_mk_eq (Comb(l1,l2)) (Comb(r1,r2)), + idx) in + new_proof (Proof(idx,th,Pmkcomb(Hashtbl.find the_proofs p1, + Hashtbl.find the_proofs p2))) | _ -> failwith "MK_COMB: types do not agree") | _ -> failwith "MK_COMB: not both equations" - let ABS v (Sequent(asl,c)) = + let ABS v (Sequent(asl,c,p)) = match (v,c) with - Var(_,_),Comb(Comb(Const("=",_),l),r) when not(exists (vfree_in v) asl) - -> Sequent(asl,safe_mk_eq (Abs(v,l)) (Abs(v,r))) + Var(_,_),Comb(Comb(Const("=",_),l),r) when not(exists (vfree_in v) asl) -> + let idx = next_proof_idx() in + let th = Sequent(asl,safe_mk_eq (Abs(v,l)) (Abs(v,r)),idx) in + new_proof (Proof(idx,th,Pabs(Hashtbl.find the_proofs p, v))) | _ -> failwith "ABS";; (* ------------------------------------------------------------------------- *) @@ -530,8 +607,10 @@ module Hol : Hol_kernel = struct let BETA tm = match tm with - Comb(Abs(v,bod),arg) when Pervasives.compare arg v = 0 - -> Sequent([],safe_mk_eq tm bod) + Comb(Abs(v,bod),arg) when Pervasives.compare arg v = 0 -> + let idx = next_proof_idx() in + let th = Sequent([],safe_mk_eq tm bod,idx) in + new_proof (Proof(idx,th,Pbeta(tm))) | _ -> failwith "BETA: not a trivial beta-redex" (* ------------------------------------------------------------------------- *) @@ -539,30 +618,43 @@ module Hol : Hol_kernel = struct (* ------------------------------------------------------------------------- *) let ASSUME tm = - if Pervasives.compare (type_of tm) bool_ty = 0 then Sequent([tm],tm) + if Pervasives.compare (type_of tm) bool_ty = 0 then + let idx = next_proof_idx() in + let th = Sequent([tm],tm,idx) in + new_proof (Proof(idx,th,Passume(tm))) else failwith "ASSUME: not a proposition" - let EQ_MP (Sequent(asl1,eq)) (Sequent(asl2,c)) = + let EQ_MP (Sequent(asl1,eq,p1)) (Sequent(asl2,c,p2)) = match eq with - Comb(Comb(Const("=",_),l),r) when alphaorder l c = 0 - -> Sequent(term_union asl1 asl2,r) + Comb(Comb(Const("=",_),l),r) when alphaorder l c = 0 -> + let idx = next_proof_idx() in + let th = Sequent(term_union asl1 asl2,r,idx) in + new_proof (Proof(idx,th,Peqmp(Hashtbl.find the_proofs p1, + Hashtbl.find the_proofs p2))) | _ -> failwith "EQ_MP" - let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1)) (Sequent(asl2,c2)) = + let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) = let asl1' = term_remove c2 asl1 and asl2' = term_remove c1 asl2 in - Sequent(term_union asl1' asl2',safe_mk_eq c1 c2) + let idx = next_proof_idx() in + let th = Sequent(term_union asl1' asl2',safe_mk_eq c1 c2,idx) in + new_proof (Proof(idx,th,Pdeduct(Hashtbl.find the_proofs p1, + Hashtbl.find the_proofs p2))) (* ------------------------------------------------------------------------- *) (* Type and term instantiation. *) (* ------------------------------------------------------------------------- *) - let INST_TYPE theta (Sequent(asl,c)) = + let INST_TYPE theta (Sequent(asl,c,p)) = + let idx = next_proof_idx() in let inst_fn = inst theta in - Sequent(term_image inst_fn asl,inst_fn c) + let th = Sequent(term_image inst_fn asl,inst_fn c,idx) in + new_proof (Proof(idx,th,Pinstt(Hashtbl.find the_proofs p,theta))) - let INST theta (Sequent(asl,c)) = + let INST theta (Sequent(asl,c,p)) = + let idx = next_proof_idx() in let inst_fun = vsubst theta in - Sequent(term_image inst_fun asl,inst_fun c) + let th = Sequent(term_image inst_fun asl,inst_fun c,idx) in + new_proof (Proof(idx,th,Pinst(Hashtbl.find the_proofs p,theta))) (* ------------------------------------------------------------------------- *) (* Handling of axioms. *) @@ -574,8 +666,10 @@ module Hol : Hol_kernel = struct let new_axiom tm = if Pervasives.compare (type_of tm) bool_ty = 0 then - let th = Sequent([],tm) in - (the_axioms := th::(!the_axioms); th) + let idx = next_proof_idx() in + let th = Sequent([],tm,idx) in + (the_axioms := th::(!the_axioms); + new_proof (Proof(idx,th,Paxiom(tm)))) else failwith "new_axiom: Not a proposition" (* ------------------------------------------------------------------------- *) @@ -593,8 +687,11 @@ module Hol : Hol_kernel = struct else if not (subset (type_vars_in_term r) (tyvars ty)) then failwith "new_definition: Type variables not reflected in constant" else let c = new_constant(cname,ty); Const(cname,ty) in - let dth = Sequent([],safe_mk_eq c r) in - the_definitions := dth::(!the_definitions); dth + let idx = next_proof_idx() in + let dtm = safe_mk_eq c r in + let dth = Sequent([],dtm,idx) in + (the_definitions := dth::(!the_definitions); + new_proof (Proof(idx,dth,Pdef(dtm,cname,ty)))) | _ -> failwith "new_basic_definition" (* ------------------------------------------------------------------------- *) @@ -610,7 +707,7 @@ module Hol : Hol_kernel = struct (* Where "abs" and "rep" are new constants with the nominated names. *) (* ------------------------------------------------------------------------- *) - let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c)) = + let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c,p)) = if exists (can get_const_type) [absname; repname] then failwith "new_basic_type_definition: Constant(s) already in use" else if not (asl = []) then @@ -630,9 +727,19 @@ module Hol : Hol_kernel = struct let abs = (new_constant(absname,absty); Const(absname,absty)) and rep = (new_constant(repname,repty); Const(repname,repty)) in let a = Var("a",aty) and r = Var("r",rty) in - Sequent([],safe_mk_eq (Comb(abs,mk_comb(rep,a))) a), - Sequent([],safe_mk_eq (Comb(P,r)) - (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r)) + let aidx = next_proof_idx() in + let atm = safe_mk_eq (Comb(abs,mk_comb(rep,a))) a in + let ath = Sequent([],atm,aidx) in + let ridx = next_proof_idx() in + let rtm = safe_mk_eq (Comb(P,r)) + (safe_mk_eq (mk_comb(rep,mk_comb(abs,r))) r) in + let rth = Sequent([],rtm,ridx) in + (new_proof (Proof(aidx, + ath, + Pdeft(Hashtbl.find the_proofs p,atm,absname,absty))), + new_proof (Proof(ridx, + rth, + Pdeft(Hashtbl.find the_proofs p,rtm,repname,repty)))) end;;