--- 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;
-
--- 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;