diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Provers/blast.ML --- a/src/Provers/blast.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Provers/blast.ML Tue Sep 29 16:24:36 2009 +0200 @@ -66,9 +66,9 @@ exception TRANS of string (*reports translation errors*) datatype term = Const of string * term list - | Skolem of string * term option ref list + | Skolem of string * term option Unsynchronized.ref list | Free of string - | Var of term option ref + | Var of term option Unsynchronized.ref | Bound of int | Abs of string*term | $ of term*term; @@ -78,10 +78,10 @@ val blast_tac : claset -> int -> tactic val setup : theory -> theory (*debugging tools*) - val stats : bool ref - val trace : bool ref - val fullTrace : branch list list ref - val fromType : (indexname * term) list ref -> Term.typ -> term + val stats : bool Unsynchronized.ref + val trace : bool Unsynchronized.ref + val fullTrace : branch list list Unsynchronized.ref + val fromType : (indexname * term) list Unsynchronized.ref -> Term.typ -> term val fromTerm : theory -> Term.term -> term val fromSubgoal : theory -> Term.term -> term val instVars : term -> (unit -> unit) @@ -98,14 +98,14 @@ type claset = Data.claset; -val trace = ref false -and stats = ref false; (*for runtime and search statistics*) +val trace = Unsynchronized.ref false +and stats = Unsynchronized.ref false; (*for runtime and search statistics*) datatype term = Const of string * term list (*typargs constant--as a terms!*) - | Skolem of string * term option ref list + | Skolem of string * term option Unsynchronized.ref list | Free of string - | Var of term option ref + | Var of term option Unsynchronized.ref | Bound of int | Abs of string*term | op $ of term*term; @@ -115,7 +115,7 @@ {pairs: ((term*bool) list * (*safe formulae on this level*) (term*bool) list) list, (*haz formulae on this level*) lits: term list, (*literals: irreducible formulae*) - vars: term option ref list, (*variables occurring in branch*) + vars: term option Unsynchronized.ref list, (*variables occurring in branch*) lim: int}; (*resource limit*) @@ -123,11 +123,11 @@ datatype state = State of {thy: theory, - fullTrace: branch list list ref, - trail: term option ref list ref, - ntrail: int ref, - nclosed: int ref, - ntried: int ref} + fullTrace: branch list list Unsynchronized.ref, + trail: term option Unsynchronized.ref list Unsynchronized.ref, + ntrail: int Unsynchronized.ref, + nclosed: int Unsynchronized.ref, + ntried: int Unsynchronized.ref} fun reject_const thy c = is_some (Sign.const_type thy c) andalso @@ -138,11 +138,11 @@ reject_const thy "*False*"; State {thy = thy, - fullTrace = ref [], - trail = ref [], - ntrail = ref 0, - nclosed = ref 0, (*branches closed: number of branches closed during the search*) - ntried = ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*) + fullTrace = Unsynchronized.ref [], + trail = Unsynchronized.ref [], + ntrail = Unsynchronized.ref 0, + nclosed = Unsynchronized.ref 0, (*branches closed: number of branches closed during the search*) + ntried = Unsynchronized.ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*) @@ -199,7 +199,7 @@ | fromType alist (Term.TFree(a,_)) = Free a | fromType alist (Term.TVar (ixn,_)) = (case (AList.lookup (op =) (!alist) ixn) of - NONE => let val t' = Var(ref NONE) + NONE => let val t' = Var (Unsynchronized.ref NONE) in alist := (ixn, t') :: !alist; t' end | SOME v => v) @@ -209,11 +209,11 @@ (*Tests whether 2 terms are alpha-convertible; chases instantiations*) -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 - | t aconv (Var(ref(SOME u))) = t aconv u +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 (Unsynchronized.ref(SOME t))) aconv u = t aconv u + | t aconv (Var (Unsynchronized.ref (SOME u))) = t aconv u | (Var v) aconv (Var w) = v=w (*both Vars are un-assigned*) | (Bound i) aconv (Bound j) = i=j | (Abs(_,t)) aconv (Abs(_,u)) = t aconv u @@ -229,7 +229,7 @@ fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; -fun mem_var (v: term option ref, []) = false +fun mem_var (v: term option Unsynchronized.ref, []) = false | mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs); fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs; @@ -238,19 +238,19 @@ (** Vars **) (*Accumulates the Vars in the term, suppressing duplicates*) -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 (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 +fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars) + | add_term_vars (Var (v as Unsynchronized.ref NONE), vars) = ins_var (v, vars) + | add_term_vars (Var (Unsynchronized.ref (SOME u)), vars) = add_term_vars (u, 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 (*Term list version. [The fold functionals are slow]*) and add_terms_vars ([], vars) = vars | add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars)) (*Var list version.*) -and add_vars_vars ([], vars) = vars - | add_vars_vars (ref (SOME u) :: vs, vars) = +and add_vars_vars ([], vars) = vars + | add_vars_vars (Unsynchronized.ref (SOME u) :: vs, vars) = add_vars_vars (vs, add_term_vars(u,vars)) | add_vars_vars (v::vs, vars) = (*v must be a ref NONE*) add_vars_vars (vs, ins_var (v, vars)); @@ -297,10 +297,10 @@ (*Normalize...but not the bodies of ABSTRACTIONS*) fun norm t = case t of - Skolem (a,args) => Skolem(a, vars_in_vars args) - | Const(a,ts) => Const(a, map norm ts) - | (Var (ref NONE)) => t - | (Var (ref (SOME u))) => norm u + Skolem (a, args) => Skolem (a, vars_in_vars args) + | Const (a, ts) => Const (a, map norm ts) + | (Var (Unsynchronized.ref NONE)) => t + | (Var (Unsynchronized.ref (SOME u))) => norm u | (f $ u) => (case norm f of Abs(_,body) => norm (subst_bound (u, body)) | nf => nf $ norm u) @@ -394,14 +394,14 @@ (*Convert from "real" terms to prototerms; eta-contract. Code is similar to fromSubgoal.*) fun fromTerm thy t = - let val alistVar = ref [] - and alistTVar = ref [] + let val alistVar = Unsynchronized.ref [] + and alistTVar = Unsynchronized.ref [] fun from (Term.Const aT) = fromConst thy alistTVar aT | from (Term.Free (a,_)) = Free a | from (Term.Bound i) = Bound i | from (Term.Var (ixn,T)) = (case (AList.lookup (op =) (!alistVar) ixn) of - NONE => let val t' = Var(ref NONE) + NONE => let val t' = Var (Unsynchronized.ref NONE) in alistVar := (ixn, t') :: !alistVar; t' end | SOME v => v) @@ -417,10 +417,10 @@ (*A debugging function: replaces all Vars by dummy Frees for visual inspection of whether they are distinct. Function revert undoes the assignments.*) fun instVars t = - let val name = ref "a" - val updated = ref [] + let val name = Unsynchronized.ref "a" + val updated = Unsynchronized.ref [] fun inst (Const(a,ts)) = List.app inst ts - | inst (Var(v as ref NONE)) = (updated := v :: (!updated); + | inst (Var(v as Unsynchronized.ref NONE)) = (updated := v :: (!updated); v := SOME (Free ("?" ^ !name)); name := Symbol.bump_string (!name)) | inst (Abs(a,t)) = inst t @@ -450,7 +450,7 @@ fun delete_concl [] = raise ElimBadPrem | delete_concl (P :: Ps) = (case P of - Const (c, _) $ Var (ref (SOME (Const ("*False*", _)))) => + Const (c, _) $ Var (Unsynchronized.ref (SOME (Const ("*False*", _)))) => if c = "*Goal*" orelse c = Data.not_name then Ps else P :: delete_concl Ps | _ => P :: delete_concl Ps); @@ -606,10 +606,10 @@ (*Convert from prototerms to ordinary terms with dummy types for tracing*) 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 - | showTerm d (Var(ref(SOME u))) = showTerm d u - | showTerm d (Var(ref NONE)) = dummyVar2 + | showTerm d (Free a) = Term.Free (a,dummyT) + | showTerm d (Bound i) = Term.Bound i + | showTerm d (Var (Unsynchronized.ref(SOME u))) = showTerm d u + | showTerm d (Var (Unsynchronized.ref NONE)) = dummyVar2 | showTerm d (Abs(a,t)) = if d=0 then dummyVar else Term.Abs(a, dummyT, showTerm (d-1) t) | showTerm d (f $ u) = if d=0 then dummyVar @@ -687,10 +687,10 @@ (*Replace the ATOMIC term "old" by "new" in t*) fun subst_atomic (old,new) t = - let fun subst (Var(ref(SOME u))) = subst u - | subst (Abs(a,body)) = Abs(a, subst body) - | subst (f$t) = subst f $ subst t - | subst t = if t aconv old then new else t + let fun subst (Var(Unsynchronized.ref(SOME u))) = subst u + | subst (Abs(a,body)) = Abs(a, subst body) + | subst (f$t) = subst f $ subst t + | subst t = if t aconv old then new else t in subst t end; (*Eta-contract a term from outside: just enough to reduce it to an atom*) @@ -723,11 +723,11 @@ Skolem(_,vars) => vars | _ => [] fun occEq u = (t aconv u) orelse occ u - and occ (Var(ref(SOME u))) = occEq u - | occ (Var v) = not (mem_var (v, vars)) - | occ (Abs(_,u)) = occEq u - | occ (f$u) = occEq u orelse occEq f - | occ (_) = false; + and occ (Var(Unsynchronized.ref(SOME u))) = occEq u + | occ (Var v) = not (mem_var (v, vars)) + | occ (Abs(_,u)) = occEq u + | occ (f$u) = occEq u orelse occEq f + | occ _ = false; in occEq end; exception DEST_EQ; @@ -1199,8 +1199,8 @@ (*Translation of a subgoal: Skolemize all parameters*) fun fromSubgoal thy t = - let val alistVar = ref [] - and alistTVar = ref [] + let val alistVar = Unsynchronized.ref [] + and alistTVar = Unsynchronized.ref [] fun hdvar ((ix,(v,is))::_) = v fun from lev t = let val (ht,ts) = Term.strip_comb t @@ -1219,7 +1219,7 @@ | Term.Bound i => apply (Bound i) | Term.Var (ix,_) => (case (AList.lookup (op =) (!alistVar) ix) of - NONE => (alistVar := (ix, (ref NONE, bounds ts)) + NONE => (alistVar := (ix, (Unsynchronized.ref NONE, bounds ts)) :: !alistVar; Var (hdvar(!alistVar))) | SOME(v,is) => if is=bounds ts then Var v @@ -1290,7 +1290,7 @@ (*** For debugging: these apply the prover to a subgoal and return the resulting tactics, trace, etc. ***) -val fullTrace = ref ([]: branch list list); +val fullTrace = Unsynchronized.ref ([]: branch list list); (*Read a string to make an initial, singleton branch*) fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;