--- a/src/Pure/IsaMakefile Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/IsaMakefile Fri Nov 21 15:27:43 1997 +0100
@@ -19,7 +19,7 @@
Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML \
axclass.ML basis.ML deriv.ML display.ML drule.ML envir.ML \
goals.ML install_pp.ML library.ML logic.ML name_space.ML net.ML \
- pattern.ML pure_thy.ML search.ML section_utils.ML sequence.ML sign.ML \
+ pattern.ML pure_thy.ML search.ML section_utils.ML seq.ML sign.ML \
sorts.ML symtab.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \
type.ML type_infer.ML unify.ML
--- a/src/Pure/ROOT.ML Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/ROOT.ML Fri Nov 21 15:27:43 1997 +0100
@@ -27,7 +27,7 @@
use "type_infer.ML";
use "type.ML";
use "sign.ML";
-use "sequence.ML";
+use "seq.ML";
use "envir.ML";
use "pattern.ML";
use "unify.ML";
--- a/src/Pure/display.ML Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/display.ML Fri Nov 21 15:27:43 1997 +0100
@@ -24,7 +24,7 @@
val print_data : theory -> string -> unit
val print_thm : thm -> unit
val prth : thm -> thm
- val prthq : thm Sequence.seq -> thm Sequence.seq
+ val prthq : thm Seq.seq -> thm Seq.seq
val prths : thm list -> thm list
val show_hyps : bool ref
val string_of_cterm : cterm -> string
@@ -67,7 +67,7 @@
(*Print and return a sequence of theorems, separated by blank lines. *)
fun prthq thseq =
- (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq);
+ (Seq.print (fn _ => print_thm) 100000 thseq; thseq);
(*Print and return a list of theorems, separated by blank lines. *)
fun prths ths = (seq (fn th => (print_thm th; writeln "")) ths; ths);
--- a/src/Pure/drule.ML Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/drule.ML Fri Nov 21 15:27:43 1997 +0100
@@ -256,7 +256,7 @@
(*Resolution: exactly one resolvent must be produced.*)
fun tha RSN (i,thb) =
- case Sequence.chop (2, biresolution false [(false,tha)] i thb) of
+ case Seq.chop (2, biresolution false [(false,tha)] i thb) of
([th],_) => th
| ([],_) => raise THM("RSN: no unifiers", i, [tha,thb])
| _ => raise THM("RSN: multiple unifiers", i, [tha,thb]);
@@ -267,7 +267,7 @@
(*For joining lists of rules*)
fun thas RLN (i,thbs) =
let val resolve = biresolution false (map (pair false) thas) i
- fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
+ fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
in List.concat (map resb thbs) end;
fun thas RL thbs = thas RLN (1,thbs);
@@ -289,7 +289,7 @@
with no lifting or renaming! Q may contain ==> or meta-quants
ALWAYS deletes premise i *)
fun compose(tha,i,thb) =
- Sequence.list_of_s (bicompose false (false,tha,0) i thb);
+ Seq.list_of (bicompose false (false,tha,0) i thb);
(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
fun tha COMP thb =
--- a/src/Pure/goals.ML Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/goals.ML Fri Nov 21 15:27:43 1997 +0100
@@ -76,7 +76,7 @@
(*Each level of goal stack includes a proof state and alternative states,
the output of the tactic applied to the preceeding level. *)
-type gstack = (thm * thm Sequence.seq) list;
+type gstack = (thm * thm Seq.seq) list;
datatype proof = Proof of gstack list * thm list * (bool*thm->thm);
@@ -101,7 +101,7 @@
(*List of previous goal stacks, for the undo operation. Set by setstate.
A list of lists!*)
-val undo_list = ref([[(dummy, Sequence.null)]] : gstack list);
+val undo_list = ref([[(dummy, Seq.empty)]] : gstack list);
(* Stack of proof attempts *)
val proofstack = ref([]: proof list);
@@ -137,7 +137,7 @@
(*discharges assumptions from state in the order they appear in goal;
checks (if requested) that resulting theorem is equivalent to goal. *)
fun mkresult (check,state) =
- let val state = Sequence.hd (flexflex_rule state)
+ let val state = Seq.hd (flexflex_rule state)
handle THM _ => state (*smash flexflex pairs*)
val ngoals = nprems_of state
val th = strip_shyps (implies_intr_list cAs state)
@@ -199,7 +199,7 @@
let val (prems, st0, mkresult) = prepare_proof rths chorn
val tac = EVERY (tacsf prems)
fun statef() =
- (case Sequence.pull (tac st0) of
+ (case Seq.pull (tac st0) of
Some(st,_) => st
| _ => error ("prove_goal: tactic failed"))
in mkresult (true, cond_timeit (!proof_timing) statef) end
@@ -243,7 +243,7 @@
!print_current_goals_fn (length pairs) (!goals_limit) th;
(*Printing can raise exceptions, so the assignment occurs last.
- Can do setstate[(st,Sequence.null)] to set st as the state. *)
+ Can do setstate[(st,Seq.empty)] to set st as the state. *)
fun setstate newgoals =
(print_top (pop newgoals); undo_list := newgoals :: !undo_list);
@@ -307,7 +307,7 @@
fun goalw_cterm rths chorn =
let val (prems, st0, mkresult) = prepare_proof rths chorn
in undo_list := [];
- setstate [ (st0, Sequence.null) ];
+ setstate [ (st0, Seq.empty) ];
curr_prems := prems;
curr_mkresult := mkresult;
prems
@@ -324,7 +324,7 @@
(*Proof step "by" the given tactic -- apply tactic to the proof state*)
fun by_com tac ((th,ths), pairs) : gstack =
- (case Sequence.pull(tac th) of
+ (case Seq.pull(tac th) of
None => error"by: tactic failed"
| Some(th2,ths2) =>
(if eq_thm(th,th2)
@@ -346,7 +346,7 @@
If none at this level, try earlier levels*)
fun backtrack [] = error"back: no alternatives"
| backtrack ((th,thstr) :: pairs) =
- (case Sequence.pull thstr of
+ (case Seq.pull thstr of
None => (writeln"Going back a level..."; backtrack pairs)
| Some(th2,thstr2) =>
(if eq_thm(th,th2)
--- a/src/Pure/search.ML Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/search.ML Fri Nov 21 15:27:43 1997 +0100
@@ -47,14 +47,14 @@
let val tac = tracify trace_DEPTH_FIRST tac
fun depth used [] = None
| depth used (q::qs) =
- case Sequence.pull q of
+ case Seq.pull q of
None => depth used qs
| Some(st,stq) =>
if satp st andalso not (gen_mem eq_thm (st, used))
- then Some(st, Sequence.seqof
+ then Some(st, Seq.make
(fn()=> depth (st::used) (stq::qs)))
else depth used (tac st :: stq :: qs)
- in traced_tac (fn st => depth [] ([Sequence.single st])) end;
+ in traced_tac (fn st => depth [] ([Seq.single st])) end;
@@ -136,11 +136,11 @@
writeln (string_of_int np ^
implode (map (fn _ => "*") qs))
else ();
- Sequence.pull q) of
+ Seq.pull q) of
None => depth (bnd,inc) qs
| Some(st,stq) =>
if satp st (*solution!*)
- then Some(st, Sequence.seqof
+ then Some(st, Seq.make
(fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
else
@@ -185,7 +185,7 @@
(*For creating output sequence*)
fun some_of_list [] = None
- | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
+ | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
(*Best-first search for a state that satisfies satp (incl initial state)
@@ -205,8 +205,8 @@
then writeln("state size = " ^ string_of_int n ^
" queue length =" ^ string_of_int (length nprfs))
else ();
- bfs (Sequence.list_of_s (tac prf), nprfs))
- fun btac st = bfs (Sequence.list_of_s (tac0 st), [])
+ bfs (Seq.list_of (tac prf), nprfs))
+ fun btac st = bfs (Seq.list_of (tac0 st), [])
in traced_tac btac end;
(*Ordinary best-first search, with no initial tactic*)
@@ -215,7 +215,7 @@
(*Breadth-first search to satisfy satpred (including initial state)
SLOW -- SHOULD NOT USE APPEND!*)
fun BREADTH_FIRST satpred tac =
- let val tacf = Sequence.list_of_s o tac;
+ let val tacf = Seq.list_of o tac;
fun bfs prfs =
(case partition satpred prfs of
([],[]) => []
@@ -223,7 +223,7 @@
(prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
bfs (List.concat (map tacf nonsats)))
| (sats,_) => sats)
- in (fn st => Sequence.s_of_list (bfs [st])) end;
+ in (fn st => Seq.of_list (bfs [st])) end;
(* Author: Norbert Voelker, FernUniversitaet Hagen
@@ -242,7 +242,7 @@
(*For creating output sequence*)
fun some_of_list [] = None
- | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
+ | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
val trace_ASTAR = ref false;
@@ -262,8 +262,8 @@
" cost = " ^ string_of_int n ^
" queue length =" ^ string_of_int (length nprfs))
else ();
- bfs (Sequence.list_of_s (tf prf), nprfs,level+1))
- fun tf st = bfs (Sequence.list_of_s (tac0 st), [], 0)
+ bfs (Seq.list_of (tf prf), nprfs,level+1))
+ fun tf st = bfs (Seq.list_of (tac0 st), [], 0)
in traced_tac tf end;
(*Ordinary ASTAR, with no initial tactic*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/seq.ML Fri Nov 21 15:27:43 1997 +0100
@@ -0,0 +1,155 @@
+(* Title: Pure/seq.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Unbounded sequences implemented by closures. RECOMPUTES if sequence
+is re-inspected. Memoing, using polymorphic refs, was found to be
+slower! (More GCs)
+*)
+
+signature SEQ =
+sig
+ type 'a seq
+ val make: (unit -> ('a * 'a seq) option) -> 'a seq
+ val pull: 'a seq -> ('a * 'a seq) option
+ val empty: 'a seq
+ val cons: 'a * 'a seq -> 'a seq
+ val single: 'a -> 'a seq
+ val hd: 'a seq -> 'a
+ val tl: 'a seq -> 'a seq
+ val chop: int * 'a seq -> 'a list * 'a seq
+ val list_of: 'a seq -> 'a list
+ val of_list: 'a list -> 'a seq
+ val map: ('a -> 'b) -> 'a seq -> 'b seq
+ val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
+ val append: 'a seq * 'a seq -> 'a seq
+ val filter: ('a -> bool) -> 'a seq -> 'a seq
+ val flat: 'a seq seq -> 'a seq
+ val interleave: 'a seq * 'a seq -> 'a seq
+ val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
+ val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
+end;
+
+structure Seq: SEQ =
+struct
+
+
+datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
+
+(*the abstraction for making a sequence*)
+val make = Seq;
+
+(*return next sequence element as None or Some (x, xq)*)
+fun pull (Seq f) = f ();
+
+
+(*the empty sequence*)
+val empty = make (fn () => None);
+
+(*prefix an element to the sequence -- use cons (x, xq) only if
+ evaluation of xq need not be delayed, otherwise use
+ make (fn () => Some (x, xq))*)
+fun cons x_xq = make (fn () => Some x_xq);
+
+fun single x = cons (x, empty);
+
+(*head and tail -- beware of calling the sequence function twice!!*)
+fun hd xq = #1 (the (pull xq))
+and tl xq = #2 (the (pull xq));
+
+
+(*the list of the first n elements, paired with rest of sequence;
+ if length of list is less than n, then sequence had less than n elements*)
+fun chop (n, xq) =
+ if n <= 0 then ([], xq)
+ else
+ (case pull xq of
+ None => ([], xq)
+ | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
+
+(*conversion from sequence to list*)
+fun list_of xq =
+ (case pull xq of
+ None => []
+ | Some (x, xq') => x :: list_of xq');
+
+(*conversion from list to sequence*)
+fun of_list xs = foldr cons (xs, empty);
+
+
+(*map the function f over the sequence, making a new sequence*)
+fun map f xq =
+ make (fn () =>
+ (case pull xq of
+ None => None
+ | Some (x, xq') => Some (f x, map f xq')));
+
+(*map over a sequence xq, append the sequence yq*)
+fun mapp f xq yq =
+ let
+ fun copy s =
+ make (fn () =>
+ (case pull s of
+ None => pull yq
+ | Some (x, s') => Some (f x, copy s')))
+ in copy xq end;
+
+(*sequence append: put the elements of xq in front of those of yq*)
+fun append (xq, yq) =
+ let
+ fun copy s =
+ make (fn () =>
+ (case pull s of
+ None => pull yq
+ | Some (x, s') => Some (x, copy s')))
+ in copy xq end;
+
+(*filter sequence by predicate*)
+fun filter pred xq =
+ let
+ fun copy s =
+ make (fn () =>
+ (case pull s of
+ None => None
+ | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
+ in copy xq end;
+
+(*flatten a sequence of sequences to a single sequence*)
+fun flat xqq =
+ make (fn () =>
+ (case pull xqq of
+ None => None
+ | Some (xq, xqq') => pull (append (xq, flat xqq'))));
+
+(*interleave elements of xq with those of yq -- fairer than append*)
+fun interleave (xq, yq) =
+ make (fn () =>
+ (case pull xq of
+ None => pull yq
+ | Some (x, xq') => Some (x, interleave (yq, xq'))));
+
+
+(*functional to print a sequence, up to "count" elements;
+ the function prelem should print the element number and also the element*)
+fun print prelem count seq =
+ let
+ fun pr (k, xq) =
+ if k > count then ()
+ else
+ (case pull xq of
+ None => ()
+ | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
+ in pr (1, seq) end;
+
+(*accumulating a function over a sequence; this is lazy*)
+fun it_right f (xq, yq) =
+ let
+ fun its s =
+ make (fn () =>
+ (case pull s of
+ None => pull yq
+ | Some (a, s') => pull (f (a, its s'))))
+ in its xq end;
+
+
+end;
--- a/src/Pure/tactic.ML Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/tactic.ML Fri Nov 21 15:27:43 1997 +0100
@@ -68,7 +68,7 @@
val net_resolve_tac : thm list -> int -> tactic
val orderlist : (int * 'a) list -> 'a list
val PRIMITIVE : (thm -> thm) -> tactic
- val PRIMSEQ : (thm -> thm Sequence.seq) -> tactic
+ val PRIMSEQ : (thm -> thm Seq.seq) -> tactic
val prune_params_tac : tactic
val rename_tac : string -> int -> tactic
val rename_last_tac : string -> string list -> int -> tactic
@@ -99,10 +99,10 @@
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *)
fun trace_goalno_tac tac i st =
- case Sequence.pull(tac i st) of
- None => Sequence.null
+ case Seq.pull(tac i st) of
+ None => Seq.empty
| seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n");
- Sequence.seqof(fn()=> seqcell));
+ Seq.make(fn()=> seqcell));
(*Convert all Vars in a theorem to Frees. Also return a function for
@@ -137,15 +137,15 @@
in implies_intr hyp (implies_elim_list state' (map assume hyps))
|> implies_intr_list (List.take(hyps, i-1) @ hyps')
|> thaw
- |> Sequence.single
+ |> Seq.single
end
- handle _ => Sequence.null;
+ handle _ => Seq.empty;
(*Makes a rule by applying a tactic to an existing rule*)
fun rule_by_tactic tac rl =
let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
- in case Sequence.pull (tac st) of
+ in case Seq.pull (tac st) of
None => raise THM("rule_by_tactic", 0, [rl])
| Some(st',_) => Thm.varifyT (thaw st')
end;
@@ -153,10 +153,10 @@
(*** Basic tactics ***)
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
-fun PRIMSEQ thmfun st = thmfun st handle THM _ => Sequence.null;
+fun PRIMSEQ thmfun st = thmfun st handle THM _ => Seq.empty;
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
-fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
+fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
(*** The following fail if the goal number is out of range:
thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
@@ -221,7 +221,7 @@
val assumed = implies_elim_list frozth (map assume froz_prems)
val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
assumed;
- in Sequence.single (thawfn implied) end
+ in Seq.single (thawfn implied) end
end;
@@ -315,7 +315,7 @@
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)),
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
val arg = (false, rl, nprems_of rl)
- val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
+ val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
in th end
handle Bind => raise THM("make_elim_preserve", 1, [rl]);
@@ -352,12 +352,12 @@
(*Introduce the given proposition as a lemma and subgoal*)
fun subgoal_tac sprop i st =
- let val st' = Sequence.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
+ let val st' = Seq.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
in
if null (term_tvars concl') then ()
else warning"Type variables in new subgoal: add a type constraint?";
- Sequence.single st'
+ Seq.single st'
end;
(*Introduce a list of lemmas and subgoals*)
@@ -496,7 +496,7 @@
(*** Meta-Rewriting Tactics ***)
fun result1 tacf mss thm =
- apsome fst (Sequence.pull (tacf mss thm));
+ apsome fst (Seq.pull (tacf mss thm));
val simple_prover =
result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
--- a/src/Pure/tctical.ML Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/tctical.ML Fri Nov 21 15:27:43 1997 +0100
@@ -13,7 +13,7 @@
signature TACTICAL =
sig
- type tactic (* = thm -> thm Sequence.seq*)
+ type tactic (* = thm -> thm Seq.seq*)
val all_tac : tactic
val ALLGOALS : (int -> tactic) -> tactic
val APPEND : tactic * tactic -> tactic
@@ -55,8 +55,8 @@
val THEN : tactic * tactic -> tactic
val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
val THEN_ELSE : tactic * (tactic*tactic) -> tactic
- val traced_tac : (thm -> (thm * thm Sequence.seq) option) -> tactic
- val tracify : bool ref -> tactic -> thm -> thm Sequence.seq
+ val traced_tac : (thm -> (thm * thm Seq.seq) option) -> tactic
+ val tracify : bool ref -> tactic -> thm -> thm Seq.seq
val trace_REPEAT : bool ref
val TRY : tactic -> tactic
val TRYALL : (int -> tactic) -> tactic
@@ -72,45 +72,45 @@
if length of sequence = 0 then the tactic does not apply;
if length > 1 then backtracking on the alternatives can occur.*)
-type tactic = thm -> thm Sequence.seq;
+type tactic = thm -> thm Seq.seq;
(*** LCF-style tacticals ***)
(*the tactical THEN performs one tactic followed by another*)
-fun (tac1 THEN tac2) st = Sequence.flats (Sequence.maps tac2 (tac1 st));
+fun (tac1 THEN tac2) st = Seq.flat (Seq.map tac2 (tac1 st));
(*The tactical ORELSE uses the first tactic that returns a nonempty sequence.
Like in LCF, ORELSE commits to either tac1 or tac2 immediately.
Does not backtrack to tac2 if tac1 was initially chosen. *)
fun (tac1 ORELSE tac2) st =
- case Sequence.pull(tac1 st) of
+ case Seq.pull(tac1 st) of
None => tac2 st
- | sequencecell => Sequence.seqof(fn()=> sequencecell);
+ | sequencecell => Seq.make(fn()=> sequencecell);
(*The tactical APPEND combines the results of two tactics.
Like ORELSE, but allows backtracking on both tac1 and tac2.
The tactic tac2 is not applied until needed.*)
fun (tac1 APPEND tac2) st =
- Sequence.append(tac1 st,
- Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
+ Seq.append(tac1 st,
+ Seq.make(fn()=> Seq.pull (tac2 st)));
(*Like APPEND, but interleaves results of tac1 and tac2.*)
fun (tac1 INTLEAVE tac2) st =
- Sequence.interleave(tac1 st,
- Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
+ Seq.interleave(tac1 st,
+ Seq.make(fn()=> Seq.pull (tac2 st)));
(*Conditional tactic.
tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac)
*)
fun (tac THEN_ELSE (tac1, tac2)) st =
- case Sequence.pull(tac st) of
+ case Seq.pull(tac st) of
None => tac2 st (*failed; try tactic 2*)
- | seqcell => Sequence.flats (*succeeded; use tactic 1*)
- (Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell)));
+ | seqcell => Seq.flat (*succeeded; use tactic 1*)
+ (Seq.map tac1 (Seq.make(fn()=> seqcell)));
(*Versions for combining tactic-valued functions, as in
@@ -121,17 +121,17 @@
fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x;
(*passes all proofs through unchanged; identity of THEN*)
-fun all_tac st = Sequence.single st;
+fun all_tac st = Seq.single st;
(*passes no proofs through; identity of ORELSE and APPEND*)
-fun no_tac st = Sequence.null;
+fun no_tac st = Seq.empty;
(*Make a tactic deterministic by chopping the tail of the proof sequence*)
fun DETERM tac st =
- case Sequence.pull (tac st) of
- None => Sequence.null
- | Some(x,_) => Sequence.cons(x, Sequence.null);
+ case Seq.pull (tac st) of
+ None => Seq.empty
+ | Some(x,_) => Seq.cons(x, Seq.empty);
(*Conditional tactical: testfun controls which tactic to use next.
@@ -148,15 +148,15 @@
(*This version of EVERY avoids backtracking over repeated states*)
fun EVY (trail, []) st =
- Sequence.seqof (fn()=> Some(st,
- Sequence.seqof (fn()=> Sequence.pull (evyBack trail))))
+ Seq.make (fn()=> Some(st,
+ Seq.make (fn()=> Seq.pull (evyBack trail))))
| EVY (trail, tac::tacs) st =
- case Sequence.pull(tac st) of
+ case Seq.pull(tac st) of
None => evyBack trail (*failed: backtrack*)
| Some(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
- and evyBack [] = Sequence.null (*no alternatives*)
+ and evyBack [] = Seq.empty (*no alternatives*)
| evyBack ((st',q,tacs)::trail) =
- case Sequence.pull q of
+ case Seq.pull q of
None => evyBack trail
| Some(st,q') => if eq_thm (st',st)
then evyBack ((st',q',tacs)::trail)
@@ -192,13 +192,13 @@
(*Print the current proof state and pass it on.*)
val print_tac =
(fn st =>
- (print_goals (!goals_limit) st; Sequence.single st));
+ (print_goals (!goals_limit) st; Seq.single st));
(*Pause until a line is typed -- if non-empty then fail. *)
fun pause_tac st =
(prs"** Press RETURN to continue: ";
- if TextIO.inputLine TextIO.stdIn = "\n" then Sequence.single st
- else (prs"Goodbye\n"; Sequence.null));
+ if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
+ else (prs"Goodbye\n"; Seq.empty));
exception TRACE_EXIT of thm
and TRACE_QUIT;
@@ -211,7 +211,7 @@
fun exec_trace_command flag (tac, st) =
case TextIO.inputLine(TextIO.stdIn) of
"\n" => tac st
- | "f\n" => Sequence.null
+ | "f\n" => Seq.empty
| "o\n" => (flag:=false; tac st)
| "s\n" => (suppress_tracing:=true; tac st)
| "x\n" => (prs"Exiting now\n"; raise (TRACE_EXIT st))
@@ -237,8 +237,8 @@
(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
fun traced_tac seqf st =
(suppress_tracing := false;
- Sequence.seqof (fn()=> seqf st
- handle TRACE_EXIT st' => Some(st', Sequence.null)));
+ Seq.make (fn()=> seqf st
+ handle TRACE_EXIT st' => Some(st', Seq.empty)));
(*Deterministic REPEAT: only retains the first outcome;
@@ -246,10 +246,10 @@
If non-negative, n bounds the number of repetitions.*)
fun REPEAT_DETERM_N n tac =
let val tac = tracify trace_REPEAT tac
- fun drep 0 st = Some(st, Sequence.null)
+ fun drep 0 st = Some(st, Seq.empty)
| drep n st =
- (case Sequence.pull(tac st) of
- None => Some(st, Sequence.null)
+ (case Seq.pull(tac st) of
+ None => Some(st, Seq.empty)
| Some(st',_) => drep (n-1) st')
in traced_tac (drep n) end;
@@ -260,11 +260,11 @@
fun REPEAT tac =
let val tac = tracify trace_REPEAT tac
fun rep qs st =
- case Sequence.pull(tac st) of
- None => Some(st, Sequence.seqof(fn()=> repq qs))
+ case Seq.pull(tac st) of
+ None => Some(st, Seq.make(fn()=> repq qs))
| Some(st',q) => rep (q::qs) st'
and repq [] = None
- | repq(q::qs) = case Sequence.pull q of
+ | repq(q::qs) = case Seq.pull q of
None => repq qs
| Some(st,q) => rep (q::qs) st
in traced_tac (rep []) end;
@@ -277,12 +277,12 @@
(** Filtering tacticals **)
(*Returns all states satisfying the predicate*)
-fun FILTER pred tac st = Sequence.filters pred (tac st);
+fun FILTER pred tac st = Seq.filter pred (tac st);
(*Returns all changed states*)
fun CHANGED tac st =
let fun diff st' = not (eq_thm(st,st'))
- in Sequence.filters diff (tac st) end;
+ in Seq.filter diff (tac st) end;
(*** Tacticals based on subgoal numbering ***)
@@ -320,7 +320,7 @@
(*Make a tactic for subgoal i, if there is one. *)
fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1), i) st
- handle Subscript => Sequence.null;
+ handle Subscript => Seq.empty;
(*** SELECT_GOAL ***)
@@ -362,7 +362,7 @@
let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
eq_trivial (adjust_maxidx (List.nth(cprems_of st0, i-1)))
fun next st = bicompose false (false, restore st, nprems_of st) i st0
- in Sequence.flats (Sequence.maps next (tac eq_cprem))
+ in Seq.flat (Seq.map next (tac eq_cprem))
end;
(* (!!selct. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*)
@@ -373,12 +373,12 @@
(* Prevent the subgoal's assumptions from becoming additional subgoals in the
new proof state by enclosing them by a universal quantification *)
fun protect_subgoal st i =
- Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st)
+ Seq.hd (bicompose false (false,dummy_quant_rl,1) i st)
handle _ => error"SELECT_GOAL -- impossible error???";
fun SELECT_GOAL tac i st =
case (i, List.drop(prems_of st, i-1)) of
- (_,[]) => Sequence.null
+ (_,[]) => Seq.empty
| (1,[_]) => tac st (*If i=1 and only one subgoal do nothing!*)
| (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i
| (_, _::_) => select tac st i;
@@ -489,7 +489,7 @@
(*function to replace the current subgoal*)
fun next st = bicompose false (false, relift st, nprems_of st)
i state
- in Sequence.flats (Sequence.maps next (tacf subprems st0))
+ in Seq.flat (Seq.map next (tacf subprems st0))
end;
end;
--- a/src/Pure/thm.ML Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/thm.ML Fri Nov 21 15:27:43 1997 +0100
@@ -19,8 +19,7 @@
(*certified terms*)
type cterm
exception CTERM of string
- val rep_cterm : cterm -> {sign: Sign.sg, t: term, T: typ,
- maxidx: int}
+ val rep_cterm : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
val term_of : cterm -> term
val cterm_of : Sign.sg -> term -> cterm
val ctyp_of_term : cterm -> ctyp
@@ -121,7 +120,7 @@
val equal_intr : thm -> thm -> thm
val equal_elim : thm -> thm -> thm
val implies_intr_hyps : thm -> thm
- val flexflex_rule : thm -> thm Sequence.seq
+ val flexflex_rule : thm -> thm Seq.seq
val instantiate :
(indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
val trivial : cterm -> thm
@@ -131,14 +130,14 @@
val dest_state : thm * int ->
(term * term) list * term list * term * term
val lift_rule : (thm * int) -> thm -> thm
- val assumption : int -> thm -> thm Sequence.seq
+ val assumption : int -> thm -> thm Seq.seq
val eq_assumption : int -> thm -> thm
val rotate_rule : int -> int -> thm -> thm
val rename_params_rule: string list * int -> thm -> thm
val bicompose : bool -> bool * thm * int ->
- int -> thm -> thm Sequence.seq
+ int -> thm -> thm Seq.seq
val biresolution : bool -> (bool * thm) list ->
- int -> thm -> thm Sequence.seq
+ int -> thm -> thm Seq.seq
(*meta simplification*)
exception SIMPLIFIER of string * thm
@@ -1016,7 +1015,7 @@
prop = newprop})
end;
val (tpairs,_) = Logic.strip_flexpairs prop
- in Sequence.maps newthm
+ in Seq.map newthm
(Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
end;
@@ -1181,9 +1180,9 @@
Logic.rule_of (tpairs, Bs, C)
else (*normalize the new rule fully*)
Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
- fun addprfs [] = Sequence.null
- | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
- (Sequence.mapp newth
+ fun addprfs [] = Seq.empty
+ | addprfs ((t,u)::apairs) = Seq.make (fn()=> Seq.pull
+ (Seq.mapp newth
(Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
(addprfs apairs)))
in addprfs (Logic.assum_pairs Bi) end;
@@ -1349,7 +1348,7 @@
nsubgoal is the number of new subgoals (written m above).
Curried so that resolution calls dest_state only once.
*)
-local open Sequence; exception COMPOSE
+local exception COMPOSE
in
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
(eres_flg, orule, nsubgoal) =
@@ -1387,7 +1386,7 @@
shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
hyps = union_term(rhyps,shyps),
prop = Logic.rule_of normp}
- in cons(th, thq) end handle COMPOSE => thq
+ in Seq.cons(th, thq) end handle COMPOSE => thq
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
@@ -1403,23 +1402,23 @@
val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
val dpairs = BBi :: (rtpairs@stpairs);
(*elim-resolution: try each assumption in turn. Initially n=1*)
- fun tryasms (_, _, []) = null
+ fun tryasms (_, _, []) = Seq.empty
| tryasms (As, n, (t,u)::apairs) =
- (case pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of
+ (case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of
None => tryasms (As, n+1, apairs)
| cell as Some((_,tpairs),_) =>
- its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
- (seqof (fn()=> cell),
- seqof (fn()=> pull (tryasms (As, n+1, apairs)))));
+ Seq.it_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
+ (Seq.make (fn()=> cell),
+ Seq.make (fn()=> Seq.pull (tryasms (As, n+1, apairs)))));
fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
| eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1);
(*ordinary resolution*)
- fun res(None) = null
+ fun res(None) = Seq.empty
| res(cell as Some((_,tpairs),_)) =
- its_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
- (seqof (fn()=> cell), null)
+ Seq.it_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
+ (Seq.make (fn()=> cell), Seq.empty)
in if eres_flg then eres(rev rAs)
- else res(pull(Unify.unifiers(sign, env, dpairs)))
+ else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
end;
end; (*open Sequence*)
@@ -1444,14 +1443,14 @@
val B = Logic.strip_assums_concl Bi;
val Hs = Logic.strip_assums_hyp Bi;
val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
- fun res [] = Sequence.null
+ fun res [] = Seq.empty
| res ((eres_flg, rule)::brules) =
if could_bires (Hs, B, eres_flg, rule)
- then Sequence.seqof (*delay processing remainder till needed*)
+ then Seq.make (*delay processing remainder till needed*)
(fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
res brules))
else res brules
- in Sequence.flats (res brules) end;
+ in Seq.flat (res brules) end;
--- a/src/Pure/unify.ML Fri Nov 21 15:26:22 1997 +0100
+++ b/src/Pure/unify.ML Fri Nov 21 15:27:43 1997 +0100
@@ -25,9 +25,9 @@
val combound : (term*int*int) -> term
val rlist_abs: (string*typ)list * term -> term
val smash_unifiers : Sign.sg * Envir.env * (term*term)list
- -> (Envir.env Sequence.seq)
+ -> (Envir.env Seq.seq)
val unifiers: Sign.sg * Envir.env * ((term*term)list)
- -> (Envir.env * (term * term)list) Sequence.seq
+ -> (Envir.env * (term * term)list) Seq.seq
end;
structure Unify : UNIFY =
@@ -386,16 +386,16 @@
The order for trying projections is crucial in ?b'(?a)
NB "vname" is only used in the call to make_args!! *)
fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
- : (term * (Envir.env * dpair list))Sequence.seq =
+ : (term * (Envir.env * dpair list))Seq.seq =
let (*Produce copies of uarg and cons them in front of uargs*)
fun copycons uarg (uargs, (env, dpairs)) =
- Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
+ Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
(mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
(env, dpairs)));
(*Produce sequence of all possible ways of copying the arg list*)
- fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
+ fun copyargs [] = Seq.cons( ([],ed), Seq.empty)
| copyargs (uarg::uargs) =
- Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
+ Seq.flat (Seq.map (copycons uarg) (copyargs uargs));
val (uhead,uargs) = strip_comb u;
val base = body_type env (fastype env (rbinder,uhead));
fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
@@ -404,7 +404,7 @@
fun projenv (head, (Us,bary), targ, tail) =
let val env = if !trace_types then test_unify_types(base,bary,env)
else unify_types(base,bary,env)
- in Sequence.seqof (fn () =>
+ in Seq.make (fn () =>
let val (env',args) = make_args vname (Ts,env,Us);
(*higher-order projection: plug in targs for bound vars*)
fun plugin arg = list_comb(head_of arg, targs);
@@ -413,7 +413,7 @@
(*may raise exception CANTUNIFY*)
in Some ((list_comb(head,args), (env2, frigid@fflex)),
tail)
- end handle CANTUNIFY => Sequence.pull tail)
+ end handle CANTUNIFY => Seq.pull tail)
end handle CANTUNIFY => tail;
(*make a list of projections*)
fun make_projs (T::Ts, targ::targs) =
@@ -425,12 +425,12 @@
(projenv(bvar, strip_type env T, targ, matchfun projs))
| matchfun [] = (*imitation last of all*)
(case uhead of
- Const _ => Sequence.maps joinargs (copyargs uargs)
- | Free _ => Sequence.maps joinargs (copyargs uargs)
- | _ => Sequence.null) (*if Var, would be a loop!*)
+ Const _ => Seq.map joinargs (copyargs uargs)
+ | Free _ => Seq.map joinargs (copyargs uargs)
+ | _ => Seq.empty) (*if Var, would be a loop!*)
in case uhead of
Abs(a, T, body) =>
- Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed'))
+ Seq.map(fn (body', ed') => (Abs (a,T,body'), ed'))
(mc ((a,T)::rbinder,
(map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
| Var (w,uary) =>
@@ -438,7 +438,7 @@
let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
val tabs = combound(newhd, 0, length Ts)
val tsub = list_comb(newhd,targs)
- in Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs))
+ in Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs))
end
| _ => matchfun(rev(make_projs(Ts, targs)))
end
@@ -447,7 +447,7 @@
(*Call matchcopy to produce assignments to the variable in the dpair*)
fun MATCH (env, (rbinder,t,u), dpairs)
- : (Envir.env * dpair list)Sequence.seq =
+ : (Envir.env * dpair list)Seq.seq =
let val (Var(v,T), targs) = strip_comb t;
val Ts = binder_types env T;
fun new_dset (u', (env',dpairs')) =
@@ -455,7 +455,7 @@
case Envir.lookup(env',v) of
None => (Envir.update ((v, types_abs(Ts, u')), env'), dpairs')
| Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
- in Sequence.maps new_dset
+ in Seq.map new_dset
(matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
end;
@@ -620,9 +620,9 @@
Returns flex-flex disagreement pairs NOT IN normal form.
SIMPL may raise exception CANTUNIFY. *)
fun hounifiers (sg,env, tus : (term*term)list)
- : (Envir.env * (term*term)list)Sequence.seq =
+ : (Envir.env * (term*term)list)Seq.seq =
let fun add_unify tdepth ((env,dpairs), reseq) =
- Sequence.seqof (fn()=>
+ Seq.make (fn()=>
let val (env',flexflex,flexrigid) =
(if tdepth> !trace_bound andalso !trace_simp
then print_dpairs "Enter SIMPL" (env,dpairs) else ();
@@ -631,25 +631,25 @@
[] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
| dp::frigid' =>
if tdepth > !search_bound then
- (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
+ (prs"***Unification bound exceeded\n"; Seq.pull reseq)
else
(if tdepth > !trace_bound then
print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
else ();
- Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
+ Seq.pull (Seq.it_right (add_unify (tdepth+1))
(MATCH (env',dp, frigid'@flexflex), reseq)))
end
handle CANTUNIFY =>
(if tdepth > !trace_bound then writeln"Failure node" else ();
- Sequence.pull reseq));
+ Seq.pull reseq));
val dps = map (fn(t,u)=> ([],t,u)) tus
in sgr := sg;
- add_unify 1 ((env,dps), Sequence.null)
+ add_unify 1 ((env,dps), Seq.empty)
end;
fun unifiers(params) =
- Sequence.cons((Pattern.unify(params), []), Sequence.null)
- handle Pattern.Unif => Sequence.null
+ Seq.cons((Pattern.unify(params), []), Seq.empty)
+ handle Pattern.Unif => Seq.empty
| Pattern.Pattern => hounifiers(params);
@@ -682,7 +682,7 @@
foldr smash_flexflex1 (tpairs, env);
(*Returns unifiers with no remaining disagreement pairs*)
-fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq =
- Sequence.maps smash_flexflex (unifiers(sg,env,tus));
+fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq =
+ Seq.map smash_flexflex (unifiers(sg,env,tus));
end;