# HG changeset patch # User wenzelm # Date 1132159523 -3600 # Node ID 7041d038acb0732f8703b03d90b1ea341bfb7525 # Parent ae9bd644d106b90f04769fdca8b65e664f0334e7 Trueprop: use ObjectLogic.judgment etc.; uniform Const of name * typargs, removed TConst; diff -r ae9bd644d106 -r 7041d038acb0 src/Provers/blast.ML --- a/src/Provers/blast.ML Wed Nov 16 17:45:22 2005 +0100 +++ b/src/Provers/blast.ML Wed Nov 16 17:45:23 2005 +0100 @@ -44,7 +44,6 @@ (*Assumptions about constants: --The negation symbol is "Not" --The equality symbol is "op =" - --The is-true judgement symbol is "Trueprop" --There are no constants named "*Goal* or "*False*" *) signature BLAST_DATA = @@ -73,8 +72,7 @@ type claset exception TRANS of string (*reports translation errors*) datatype term = - Const of string - | TConst of string * term + Const of string * term list | Skolem of string * term option ref list | Free of string | Var of term option ref @@ -116,8 +114,7 @@ and stats = ref false; (*for runtime and search statistics*) datatype term = - Const of string - | TConst of string * term (*type of overloaded constant--as a term!*) + Const of string * term list (*typargs constant--as a terms!*) | Skolem of string * term option ref list | Free of string | Var of term option ref @@ -151,30 +148,28 @@ (** Particular constants **) -fun negate P = Const"Not" $ P; +fun negate P = Const ("Not", []) $ P; -fun mkGoal P = Const"*Goal*" $ P; +fun mkGoal P = Const ("*Goal*", []) $ P; -fun isGoal (Const"*Goal*" $ _) = true +fun isGoal (Const ("*Goal*", _) $ _) = true | isGoal _ = false; -val boolT = - case term_vars (hd (prems_of Data.notE)) of - [Term.Var(_, Type(s, []))] => s - | _ => error ("Theorem notE is ill-formed: " ^ string_of_thm Data.notE); +val TruepropC = ObjectLogic.judgment_name (the_context ()); +val TruepropT = Sign.the_const_type (the_context ()) TruepropC; -val Trueprop = Term.Const("Trueprop", Type(boolT,[])-->propT); -fun mk_tprop P = Term.$ (Trueprop, P); +fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t); -fun isTrueprop (Term.Const("Trueprop",_)) = true - | isTrueprop _ = false; +fun strip_Trueprop (tm as Const (c, _) $ t) = if c = TruepropC then t else tm + | strip_Trueprop tm = tm; + (*** Dealing with overloaded constants ***) (*alist is a map from TVar names to Vars. We need to unify the TVars faithfully in order to track overloading*) -fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, map (fromType alist) Ts) +fun fromType alist (Term.Type(a,Ts)) = list_comb (Const (a, []), map (fromType alist) Ts) | fromType alist (Term.TFree(a,_)) = Free a | fromType alist (Term.TVar (ixn,_)) = (case (AList.lookup (op =) (!alist) ixn) of @@ -186,19 +181,12 @@ (*refer to the theory in which blast is initialized*) val typargs = ref (fn ((_, T): string * typ) => [T]); -(*Convert a Term.Const to a Blast.Const or Blast.TConst, - converting its type to a Blast.term in the latter case.*) -fun fromConst alist (a as "all", _) = Const a - | fromConst alist (a, T) = - (case ! typargs (a, T) of - [] => Const a - | [T] => TConst (a, fromType alist T) - | Ts => TConst (a, list_comb (Const "*typargs*", map (fromType alist) Ts))); +fun fromConst alist (a, T) = + Const (a, map (fromType alist) (! typargs (a, T))); (*Tests whether 2 terms are alpha-convertible; chases instantiations*) -fun (Const a) aconv (Const b) = a=b - | (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb +fun (Const (a, ts)) aconv (Const (b, us)) = a=b andalso aconvs (ts, us) | (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) | (Free a) aconv (Free b) = a=b | (Var(ref(SOME t))) aconv u = t aconv u @@ -207,7 +195,10 @@ | (Bound i) aconv (Bound j) = i=j | (Abs(_,t)) aconv (Abs(_,u)) = t aconv u | (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) - | _ aconv _ = false; + | _ aconv _ = false +and aconvs ([], []) = true + | aconvs (t :: ts, u :: us) = t aconv u andalso aconvs (ts, us) + | aconvs _ = false; fun mem_term (_, []) = false @@ -227,7 +218,7 @@ fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars) | add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars) | add_term_vars (Var (ref (SOME u)), vars) = add_term_vars(u,vars) - | add_term_vars (TConst (_,t), vars) = add_term_vars(t,vars) + | add_term_vars (Const (_,ts), vars) = add_terms_vars(ts,vars) | add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) | add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) | add_term_vars (_, vars) = vars @@ -284,7 +275,7 @@ (*Normalize...but not the bodies of ABSTRACTIONS*) fun norm t = case t of Skolem (a,args) => Skolem(a, vars_in_vars args) - | TConst(a,aT) => TConst(a, norm aT) + | Const(a,ts) => Const(a, map norm ts) | (Var (ref NONE)) => t | (Var (ref (SOME u))) => norm u | (f $ u) => (case norm f of @@ -311,7 +302,6 @@ | _ => t and wkNorm t = case head_of t of Const _ => t - | TConst _ => t | Skolem(a,args) => t | Free _ => t | _ => wkNormAux t; @@ -327,7 +317,7 @@ (case !w of NONE => false | SOME u => occ lev u) | occ lev (Skolem(_,args)) = occL lev (map Var args) - (*ignore TConst, since term variables can't occur in types (?) *) + (*ignore Const, since term variables can't occur in types (?) *) | occ lev (Bound i) = lev <= i | occ lev (Abs(_,u)) = occ (lev+1) u | occ lev (f$u) = occ lev u orelse occ lev f @@ -367,12 +357,15 @@ case (wkNorm t, wkNorm u) of (nt as Var v, nu) => update(nt,nu) | (nu, nt as Var v) => update(nt,nu) - | (TConst(a,at), TConst(b,bt)) => if a=b then unifyAux(at,bt) + | (Const(a,ats), Const(b,bts)) => if a=b then unifysAux(ats,bts) else raise UNIFY | (Abs(_,t'), Abs(_,u')) => unifyAux(t',u') (*NB: can yield unifiers having dangling Bound vars!*) | (f$t', g$u') => (unifyAux(f,g); unifyAux(t',u')) | (nt, nu) => if nt aconv nu then () else raise UNIFY + and unifysAux ([], []) = () + | unifysAux (t :: ts, u :: us) = (unifyAux (t, u); unifysAux (ts, us)) + | unifysAux _ = raise UNIFY; in (unifyAux(t,u); true) handle UNIFY => (clearTo n; false) end; @@ -405,7 +398,7 @@ fun instVars t = let val name = ref "a" val updated = ref [] - fun inst (TConst(a,t)) = inst t + fun inst (Const(a,ts)) = List.app inst ts | inst (Var(v as ref NONE)) = (updated := v :: (!updated); v := SOME (Free ("?" ^ !name)); name := Symbol.bump_string (!name)) @@ -417,15 +410,13 @@ (* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) -fun strip_imp_prems (Const"==>" $ (Const"Trueprop" $ A) $ B) = - A :: strip_imp_prems B - | strip_imp_prems (Const"==>" $ A $ B) = A :: strip_imp_prems B +fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B | strip_imp_prems _ = []; (* A1==>...An==>B goes to B, where B is not an implication *) -fun strip_imp_concl (Const"==>" $ A $ B) = strip_imp_concl B - | strip_imp_concl (Const"Trueprop" $ A) = A - | strip_imp_concl A = A : term; +fun strip_imp_concl (Const ("==>", _) $ A $ B) = strip_imp_concl B + | strip_imp_concl A = strip_Trueprop A; + (*** Conversion of Elimination Rules to Tableau Operations ***) @@ -436,13 +427,13 @@ If we don't find it then the premise is ill-formed and could cause PROOF FAILED*) fun delete_concl [] = raise ElimBadPrem - | delete_concl (Const "*Goal*" $ (Var (ref (SOME (Const"*False*")))) :: Ps) = + | delete_concl (Const ("*Goal*", _) $ (Var (ref (SOME (Const ("*False*", _))))) :: Ps) = Ps - | delete_concl (Const "Not" $ (Var (ref (SOME (Const"*False*")))) :: Ps) = + | delete_concl (Const ("Not", _) $ (Var (ref (SOME (Const ("*False*", _))))) :: Ps) = Ps | delete_concl (P::Ps) = P :: delete_concl Ps; -fun skoPrem vars (Const "all" $ Abs (_, P)) = +fun skoPrem vars (Const ("all", _) $ Abs (_, P)) = skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P)) | skoPrem vars P = P; @@ -453,7 +444,7 @@ fun convertRule vars t = let val (P::Ps) = strip_imp_prems t val Var v = strip_imp_concl t - in v := SOME (Const"*False*"); + in v := SOME (Const ("*False*", [])); (P, map (convertPrem o skoPrem vars) Ps) end handle Bind => raise ElimBadConcl; @@ -467,7 +458,7 @@ local (*Count new hyps so that they can be rotated*) fun nNewHyps [] = 0 - | nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps + | nNewHyps (Const ("*Goal*", _) $ _ :: Ps) = nNewHyps Ps | nNewHyps (P::Ps) = 1 + nNewHyps Ps; fun rot_tac [] i st = Seq.single st @@ -535,8 +526,7 @@ (*Convert from prototerms to ordinary terms with dummy types Ignore abstractions; identify all Vars; STOP at given depth*) fun toTerm 0 _ = dummyVar - | toTerm d (Const a) = Term.Const (a,dummyT) - | toTerm d (TConst(a,_)) = Term.Const (a,dummyT) (*no need to convert type*) + | toTerm d (Const(a,_)) = Term.Const (a,dummyT) (*no need to convert typargs*) | toTerm d (Skolem(a,_)) = Term.Const (a,dummyT) | toTerm d (Free a) = Term.Free (a,dummyT) | toTerm d (Bound i) = Term.Bound i @@ -547,14 +537,14 @@ fun netMkRules P vars (nps: netpair list) = case P of - (Const "*Goal*" $ G) => - let val pG = mk_tprop (toTerm 2 G) + (Const ("*Goal*", _) $ G) => + let val pG = mk_Trueprop (toTerm 2 G) val intrs = List.concat (map (fn (inet,_) => Net.unify_term inet pG) nps) in map (fromIntrRule vars o #2) (Tactic.orderlist intrs) end | _ => - let val pP = mk_tprop (toTerm 3 P) + let val pP = mk_Trueprop (toTerm 3 P) val elims = List.concat (map (fn (_,enet) => Net.unify_term enet pP) nps) @@ -591,19 +581,18 @@ | showType (Var _) = dummyTVar | showType t = (case strip_comb t of - (Const a, us) => Term.Type(a, map showType us) + (Const (a, _), us) => Term.Type(a, map showType us) | _ => dummyT); (*Display top-level overloading if any*) -fun topType (TConst(a,t)) = SOME (showType t) - | topType (Abs(a,t)) = topType t - | topType (f $ u) = (case topType f of NONE => topType u | some => some) - | topType _ = NONE; +fun topType thy (Const (c, ts)) = SOME (Sign.const_instance thy (c, map showType ts)) + | topType thy (Abs(a,t)) = topType thy t + | topType thy (f $ u) = (case topType thy f of NONE => topType thy u | some => some) + | topType _ _ = NONE; (*Convert from prototerms to ordinary terms with dummy types for tracing*) -fun showTerm d (Const a) = Term.Const (a,dummyT) - | showTerm d (TConst(a,_)) = Term.Const (a,dummyT) +fun showTerm d (Const (a,_)) = Term.Const (a,dummyT) | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) | showTerm d (Free a) = Term.Free (a,dummyT) | showTerm d (Bound i) = Term.Bound i @@ -620,7 +609,7 @@ let val t' = norm t val stm = string_of sign 8 t' in - case topType t' of + case topType sign t' of NONE => stm (*no type to attach*) | SOME T => stm ^ "\t:: " ^ Sign.string_of_typ sign T end; @@ -715,10 +704,8 @@ exception DEST_EQ; -(*Take apart an equality (plain or overloaded). NO constant Trueprop*) -fun dest_eq (Const "op =" $ t $ u) = - (eta_contract_atom t, eta_contract_atom u) - | dest_eq (TConst("op =",_) $ t $ u) = +(*Take apart an equality. NO constant Trueprop*) +fun dest_eq (Const ("op =", _) $ t $ u) = (eta_contract_atom t, eta_contract_atom u) | dest_eq _ = raise DEST_EQ; @@ -782,13 +769,13 @@ val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); (*Try to unify complementary literals and return the corresponding tactic. *) -fun tryClose (Const"*Goal*" $ G, L) = +fun tryClose (Const ("*Goal*", _) $ G, L) = if unify([],G,L) then SOME eAssume_tac else NONE - | tryClose (G, Const"*Goal*" $ L) = + | tryClose (G, Const ("*Goal*", _) $ L) = if unify([],G,L) then SOME eAssume_tac else NONE - | tryClose (Const"Not" $ G, L) = + | tryClose (Const ("Not", _) $ G, L) = if unify([],G,L) then SOME eContr_tac else NONE - | tryClose (G, Const"Not" $ L) = + | tryClose (G, Const ("Not", _) $ L) = if unify([],G,L) then SOME eContr_tac else NONE | tryClose _ = NONE; @@ -806,8 +793,8 @@ (*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like Ex(P) is duplicated as the assumption ~Ex(P). *) -fun negOfGoal (Const"*Goal*" $ G) = negate G - | negOfGoal G = G; +fun negOfGoal (Const ("*Goal*", _) $ G) = negate G + | negOfGoal G = G; fun negOfGoal2 (G,md) = (negOfGoal G, md); @@ -870,21 +857,21 @@ | backtrack _ = raise PROVE; (*Add the literal G, handling *Goal* and detecting duplicates.*) -fun addLit (Const "*Goal*" $ G, lits) = +fun addLit (Const ("*Goal*", _) $ G, lits) = (*New literal is a *Goal*, so change all other Goals to Nots*) - let fun bad (Const"*Goal*" $ _) = true - | bad (Const"Not" $ G') = G aconv G' + let fun bad (Const ("*Goal*", _) $ _) = true + | bad (Const ("Not", _) $ G') = G aconv G' | bad _ = false; fun change [] = [] - | change (Const"*Goal*" $ G' :: lits) = + | change (Const ("*Goal*", _) $ G' :: lits) = if G aconv G' then change lits - else Const"Not" $ G' :: change lits - | change (Const"Not" $ G' :: lits) = + else Const ("Not", []) $ G' :: change lits + | change (Const ("Not", _) $ G' :: lits) = if G aconv G' then change lits - else Const"Not" $ G' :: change lits + else Const ("Not", []) $ G' :: change lits | change (lit::lits) = lit :: change lits in - Const "*Goal*" $ G :: (if exists bad lits then change lits else lits) + Const ("*Goal*", []) $ G :: (if exists bad lits then change lits else lits) end | addLit (G,lits) = ins_term(G, lits) @@ -897,15 +884,16 @@ (*match(t,u) says whether the term u might be an instance of the pattern t Used to detect "recursive" rules such as transitivity*) fun match (Var _) u = true - | match (Const"*Goal*") (Const"Not") = true - | match (Const"Not") (Const"*Goal*") = true - | match (Const a) (Const b) = (a=b) - | match (TConst (a,ta)) (TConst (b,tb)) = a=b andalso match ta tb + | match (Const ("*Goal*", _)) (Const ("Not", _)) = true + | match (Const ("Not", _)) (Const ("*Goal*", _)) = true + | match (Const (a,tas)) (Const (b,tbs)) = a=b andalso matchs tas tbs | match (Free a) (Free b) = (a=b) | match (Bound i) (Bound j) = (i=j) | match (Abs(_,t)) (Abs(_,u)) = match t u | match (f$t) (g$u) = match f g andalso match t u - | match t u = false; + | match t u = false +and matchs [] [] = true + | matchs (t :: ts) (u :: us) = match t u andalso matchs ts us; (*Branches closed: number of branches closed during the search @@ -1189,7 +1177,6 @@ | discard_foralls t = t; end; - (*List of variables not appearing as arguments to the given parameter*) fun getVars [] i = [] | getVars ((_,(v,is))::alist) i =