# HG changeset patch # User paulson # Date 824469587 -3600 # Node ID b2de3b3277b8ff9fc9e5db6278d1cba3a0199eec # Parent 01fdd1ea632445a5ee4aa245d5c2b672f0580ce8 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted. diff -r 01fdd1ea6324 -r b2de3b3277b8 src/Pure/envir.ML --- a/src/Pure/envir.ML Fri Feb 16 12:08:49 1996 +0100 +++ b/src/Pure/envir.ML Fri Feb 16 12:19:47 1996 +0100 @@ -33,10 +33,9 @@ val vupdate : (indexname * term) * env -> env end; -functor EnvirFun () : ENVIR = +structure Envir : ENVIR = struct - (*association lists with keys in ascending order, no repeated keys*) datatype 'a xolist = Olist of (indexname * 'a) list; @@ -154,69 +153,61 @@ fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol; -(*Beta normal form for terms (not eta normal form). - Chases variables in env; Does not exploit sharing of variable bindings - Does not check types, so could loop. *) -local - (*raised when norm has no effect on a term, - to encourage sharing instead of copying*) - exception SAME; +(*** Beta normal form for terms (not eta normal form). + Chases variables in env; Does not exploit sharing of variable bindings + Does not check types, so could loop. ***) + +(*raised when norm has no effect on a term, to do sharing instead of copying*) +exception SAME; - fun norm_term1 (asol,t) : term = - let fun norm (Var (w,T)) = - (case xsearch(asol,w) of - Some u => normh u - | None => raise SAME) - | norm (Abs(a,T,body)) = Abs(a, T, norm body) - | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body)) - | norm (f $ t) = - ((case norm f of - Abs(_,_,body) => normh(subst_bounds([t], body)) - | nf => nf $ normh t) - handle SAME => f $ norm t) - | norm _ = raise SAME - and normh t = (norm t) handle SAME => t - in normh t end +fun norm_term1 (asol,t) : term = + let fun norm (Var (w,T)) = + (case xsearch(asol,w) of + Some u => normh u + | None => raise SAME) + | norm (Abs(a,T,body)) = Abs(a, T, norm body) + | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body)) + | norm (f $ t) = + ((case norm f of + Abs(_,_,body) => normh(subst_bounds([t], body)) + | nf => nf $ normh t) + handle SAME => f $ norm t) + | norm _ = raise SAME + and normh t = (norm t) handle SAME => t + in normh t end - and norm_term2(asol,iTs,t) : term = - let fun normT(Type(a,Ts)) = Type(a, normTs Ts) - | normT(TFree _) = raise SAME - | normT(TVar(v,_)) = (case assoc(iTs,v) of - Some(U) => normTh U - | None => raise SAME) - and normTh T = ((normT T) handle SAME => T) - and normTs([]) = raise SAME - | normTs(T::Ts) = ((normT T :: normTsh Ts) - handle SAME => T :: normTs Ts) - and normTsh Ts = ((normTs Ts) handle SAME => Ts) - and norm(Const(a,T)) = Const(a, normT T) - | norm(Free(a,T)) = Free(a, normT T) - | norm(Var (w,T)) = - (case xsearch(asol,w) of - Some u => normh u - | None => Var(w,normT T)) - | norm(Abs(a,T,body)) = - (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body)) - | norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body)) - | norm(f $ t) = - ((case norm f of - Abs(_,_,body) => normh(subst_bounds([t], body)) - | nf => nf $ normh t) - handle SAME => f $ norm t) - | norm _ = raise SAME - and normh t = (norm t) handle SAME => t - in normh t end; - -in +and norm_term2(asol,iTs,t) : term = + let fun normT(Type(a,Ts)) = Type(a, normTs Ts) + | normT(TFree _) = raise SAME + | normT(TVar(v,_)) = (case assoc(iTs,v) of + Some(U) => normTh U + | None => raise SAME) + and normTh T = ((normT T) handle SAME => T) + and normTs([]) = raise SAME + | normTs(T::Ts) = ((normT T :: normTsh Ts) + handle SAME => T :: normTs Ts) + and normTsh Ts = ((normTs Ts) handle SAME => Ts) + and norm(Const(a,T)) = Const(a, normT T) + | norm(Free(a,T)) = Free(a, normT T) + | norm(Var (w,T)) = + (case xsearch(asol,w) of + Some u => normh u + | None => Var(w,normT T)) + | norm(Abs(a,T,body)) = + (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body)) + | norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body)) + | norm(f $ t) = + ((case norm f of + Abs(_,_,body) => normh(subst_bounds([t], body)) + | nf => nf $ normh t) + handle SAME => f $ norm t) + | norm _ = raise SAME + and normh t = (norm t) handle SAME => t + in normh t end; (*curried version might be slower in recursive calls*) fun norm_term (env as Envir{asol,iTs,...}) t : term = if null iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t) -fun norm_ter (env as Envir{asol,iTs,...}) t : term = - if null iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t) - end; -end; - diff -r 01fdd1ea6324 -r b2de3b3277b8 src/Pure/goals.ML --- a/src/Pure/goals.ML Fri Feb 16 12:08:49 1996 +0100 +++ b/src/Pure/goals.ML Fri Feb 16 12:19:47 1996 +0100 @@ -12,8 +12,6 @@ signature GOALS = sig - structure Tactical: TACTICAL - local open Tactical Tactical.Thm in type proof val ba : int -> unit val back : unit -> unit @@ -66,17 +64,10 @@ val save_proof : unit -> proof val topthm : unit -> thm val undo : unit -> unit - end end; -functor GoalsFun (structure Logic: LOGIC and Drule: DRULE and Tactic: TACTIC - and Pattern:PATTERN - sharing type Pattern.type_sig = Drule.Thm.Sign.Type.type_sig - and Drule.Thm = Tactic.Tactical.Thm) : GOALS = +structure Goals : GOALS = struct -structure Tactical = Tactic.Tactical -local open Tactic Tactic.Tactical Tactic.Tactical.Thm Drule -in (*Each level of goal stack includes a proof state and alternative states, the output of the tactic applied to the preceeding level. *) @@ -154,7 +145,7 @@ cat_lines (map (Sign.string_of_term sign) hyps)) else if not (null xshyps) then result_error state ("Extra sort hypotheses: " ^ - commas (map Sign.Type.str_of_sort xshyps)) + commas (map Type.str_of_sort xshyps)) else if Pattern.matches (#tsig(Sign.rep_sg sign)) (term_of chorn, prop) then standard th @@ -199,7 +190,7 @@ let val (prems, st0, mkresult) = prepare_proof rths chorn val tac = EVERY (tacsf prems) fun statef() = - (case Sequence.pull (tapply(tac,st0)) of + (case Sequence.pull (tac st0) of Some(st,_) => st | _ => error ("prove_goal: tactic failed")) in mkresult (true, cond_timeit (!proof_timing) statef) end @@ -270,7 +261,7 @@ local exception GETHYPS of thm list in fun gethyps i = - (tapply(METAHYPS (fn hyps => raise (GETHYPS hyps)) i, topthm()); []) + (METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm()); []) handle GETHYPS hyps => hyps end; @@ -316,7 +307,7 @@ (*Proof step "by" the given tactic -- apply tactic to the proof state*) fun by_com tac ((th,ths), pairs) : gstack = - (case Sequence.pull(tapply(tac, th)) of + (case Sequence.pull(tac th) of None => error"by: tactic failed" | Some(th2,ths2) => (if eq_thm(th,th2) @@ -444,4 +435,5 @@ fun print_exn e = (print_sign_exn_unit (top_sg()) e; raise e); end; -end; + +open Goals; diff -r 01fdd1ea6324 -r b2de3b3277b8 src/Pure/logic.ML --- a/src/Pure/logic.ML Fri Feb 16 12:08:49 1996 +0100 +++ b/src/Pure/logic.ML Fri Feb 16 12:19:47 1996 +0100 @@ -49,12 +49,9 @@ val varify : term -> term end; -functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC = +structure Logic : LOGIC = struct -structure Sign = Unify.Sign; -structure Type = Sign.Type; - (*** Abstract syntax operations on the meta-connectives ***) (** equality **) diff -r 01fdd1ea6324 -r b2de3b3277b8 src/Pure/net.ML --- a/src/Pure/net.ML Fri Feb 16 12:08:49 1996 +0100 +++ b/src/Pure/net.ML Fri Feb 16 12:19:47 1996 +0100 @@ -31,7 +31,7 @@ end; -functor NetFun () : NET = +structure Net : NET = struct datatype key = CombK | VarK | AtomK of string;