changed Pure/Sequence interface -- isatool fixseq;
authorwenzelm
Fri Nov 21 15:29:56 1997 +0100 (1997-11-21)
changeset 42713a82492e70c5
parent 4270 957c887b89b5
child 4272 61c6ae12ca14
changed Pure/Sequence interface -- isatool fixseq;
src/FOLP/simp.ML
src/HOL/Modelcheck/MCSyn.ML
src/HOL/ex/meson.ML
src/HOLCF/domain/theorems.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Provers/simp.ML
src/Provers/simplifier.ML
src/ZF/ROOT.ML
     1.1 --- a/src/FOLP/simp.ML	Fri Nov 21 15:27:43 1997 +0100
     1.2 +++ b/src/FOLP/simp.ML	Fri Nov 21 15:29:56 1997 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4  in mk trans_thms end;
     1.5  
     1.6  (*Applies tactic and returns the first resulting state, FAILS if none!*)
     1.7 -fun one_result(tac,thm) = case Sequence.pull(tac thm) of
     1.8 +fun one_result(tac,thm) = case Seq.pull(tac thm) of
     1.9          Some(thm',_) => thm'
    1.10        | None => raise THM("Simplifier: could not continue", 0, [thm]);
    1.11  
    1.12 @@ -211,7 +211,7 @@
    1.13  	  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    1.14  	  | _ => refl1_tac)
    1.15      val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
    1.16 -    val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
    1.17 +    val Some(thm'',_) = Seq.pull(add_norm_tac thm')
    1.18  in thm'' end;
    1.19  
    1.20  fun add_norm_tags congs =
    1.21 @@ -422,7 +422,7 @@
    1.22  fun simp_lhs(thm,ss,anet,ats,cs) =
    1.23      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
    1.24      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
    1.25 -    else case Sequence.pull(cong_tac i thm) of
    1.26 +    else case Seq.pull(cong_tac i thm) of
    1.27              Some(thm',_) =>
    1.28                      let val ps = prems_of thm and ps' = prems_of thm';
    1.29                          val n = length(ps')-length(ps);
    1.30 @@ -446,7 +446,7 @@
    1.31          (ss,thm,anet',anet::ats,cs) 
    1.32      end;
    1.33  
    1.34 -fun rew(seq,thm,ss,anet,ats,cs, more) = case Sequence.pull seq of
    1.35 +fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
    1.36        Some(thm',seq') =>
    1.37              let val n = (nprems_of thm') - (nprems_of thm)
    1.38              in pr_rew(i,n,thm,thm',more);
    1.39 @@ -460,7 +460,7 @@
    1.40              else (ss,thm,anet,ats,cs);
    1.41  
    1.42  fun try_true(thm,ss,anet,ats,cs) =
    1.43 -    case Sequence.pull(auto_tac i thm) of
    1.44 +    case Seq.pull(auto_tac i thm) of
    1.45        Some(thm',_) => (ss,thm',anet,ats,cs)
    1.46      | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
    1.47                in if !tracing
    1.48 @@ -471,7 +471,7 @@
    1.49                end;
    1.50  
    1.51  fun if_exp(thm,ss,anet,ats,cs) =
    1.52 -        case Sequence.pull (IF1_TAC (cong_tac i) i thm) of
    1.53 +        case Seq.pull (IF1_TAC (cong_tac i) i thm) of
    1.54                  Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
    1.55                | None => (ss,thm,anet,ats,cs);
    1.56  
    1.57 @@ -498,8 +498,8 @@
    1.58  let val cong_tac = net_tac cong_net
    1.59  in fn i => 
    1.60      (fn thm =>
    1.61 -     if i <= 0 orelse nprems_of thm < i then Sequence.null
    1.62 -     else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
    1.63 +     if i <= 0 orelse nprems_of thm < i then Seq.empty
    1.64 +     else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
    1.65      THEN TRY(auto_tac i)
    1.66  end;
    1.67  
     2.1 --- a/src/HOL/Modelcheck/MCSyn.ML	Fri Nov 21 15:27:43 1997 +0100
     2.2 +++ b/src/HOL/Modelcheck/MCSyn.ML	Fri Nov 21 15:29:56 1997 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  let val sign = #sign (rep_thm state)
     2.5  in 
     2.6  case drop(i-1,prems_of state) of
     2.7 -   [] => Sequence.null |
     2.8 +   [] => Seq.empty |
     2.9     subgoal::_ => 
    2.10  	let val concl = Logic.strip_imp_concl subgoal;
    2.11  	    val OraAss = invoke_oracle MCSyn.thy "mc" (sign,MCOracleExn concl);
     3.1 --- a/src/HOL/ex/meson.ML	Fri Nov 21 15:27:43 1997 +0100
     3.2 +++ b/src/HOL/ex/meson.ML	Fri Nov 21 15:29:56 1997 +0100
     3.3 @@ -162,7 +162,7 @@
     3.4  
     3.5  (*Permits forward proof from rules that discharge assumptions*)
     3.6  fun forward_res nf st =
     3.7 -  case Sequence.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
     3.8 +  case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
     3.9    of Some(th,_) => th
    3.10     | None => raise THM("forward_res", 0, [st]);
    3.11  
    3.12 @@ -247,7 +247,7 @@
    3.13          (METAHYPS (resop (cnf_nil seen)) 1) THEN
    3.14          (fn st' => st' |>
    3.15                  METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
    3.16 -    in  Sequence.list_of_s (tac (th RS disj_forward)) @ ths  end
    3.17 +    in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
    3.18  and cnf_nil seen th = cnf_aux seen (th,[]);
    3.19  
    3.20  (*Top-level call to cnf -- it's safe to reset name_ref*)
    3.21 @@ -270,7 +270,7 @@
    3.22  
    3.23  (*Forward proof, passing extra assumptions as theorems to the tactic*)
    3.24  fun forward_res2 nf hyps st =
    3.25 -  case Sequence.pull
    3.26 +  case Seq.pull
    3.27          (REPEAT 
    3.28           (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) 
    3.29           st)
    3.30 @@ -373,7 +373,7 @@
    3.31                    handle INSERT => true; 
    3.32  
    3.33  (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
    3.34 -fun TRYALL_eq_assume_tac 0 st = Sequence.single st
    3.35 +fun TRYALL_eq_assume_tac 0 st = Seq.single st
    3.36    | TRYALL_eq_assume_tac i st = TRYALL_eq_assume_tac (i-1) (eq_assumption i st)
    3.37                                  handle THM _ => TRYALL_eq_assume_tac (i-1) st;
    3.38  
    3.39 @@ -381,7 +381,7 @@
    3.40    -- if *ANY* subgoal has repeated literals*)
    3.41  fun check_tac st = 
    3.42    if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
    3.43 -  then  Sequence.null  else  Sequence.single st;
    3.44 +  then  Seq.empty  else  Seq.single st;
    3.45  
    3.46  
    3.47  (* net_resolve_tac actually made it slower... *)
     4.1 --- a/src/HOLCF/domain/theorems.ML	Fri Nov 21 15:27:43 1997 +0100
     4.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Nov 21 15:29:56 1997 +0100
     4.3 @@ -28,9 +28,9 @@
     4.4                                  | prems=> (cut_facts_tac prems 1)::tacsf);
     4.5  
     4.6  fun REPEAT_DETERM_UNTIL p tac = 
     4.7 -let fun drep st = if p st then Sequence.single st
     4.8 -                          else (case Sequence.pull(tac st) of
     4.9 -                                  None        => Sequence.null
    4.10 +let fun drep st = if p st then Seq.single st
    4.11 +                          else (case Seq.pull(tac st) of
    4.12 +                                  None        => Seq.empty
    4.13                                  | Some(st',_) => drep st')
    4.14  in drep end;
    4.15  val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
     5.1 --- a/src/Provers/blast.ML	Fri Nov 21 15:27:43 1997 +0100
     5.2 +++ b/src/Provers/blast.ML	Fri Nov 21 15:29:56 1997 +0100
     5.3 @@ -459,7 +459,7 @@
     5.4  
     5.5  
     5.6  (*Like dup_elim, but puts the duplicated major premise FIRST*)
     5.7 -fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd;
     5.8 +fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd;
     5.9  
    5.10  
    5.11  (*Count new hyps so that they can be rotated*)
    5.12 @@ -467,10 +467,10 @@
    5.13    | nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps
    5.14    | nNewHyps (P::Ps)                    = 1 + nNewHyps Ps;
    5.15  
    5.16 -fun rot_subgoals_tac [] i st      = Sequence.single st
    5.17 +fun rot_subgoals_tac [] i st      = Seq.single st
    5.18    | rot_subgoals_tac (k::ks) i st =
    5.19 -      rot_subgoals_tac ks (i+1) (Sequence.hd (rotate_tac (~k) i st))
    5.20 -      handle OPTION => Sequence.null;
    5.21 +      rot_subgoals_tac ks (i+1) (Seq.hd (rotate_tac (~k) i st))
    5.22 +      handle OPTION => Seq.empty;
    5.23  
    5.24  fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;
    5.25  
    5.26 @@ -1166,17 +1166,17 @@
    5.27           val hyps  = strip_imp_prems skoprem
    5.28           and concl = strip_imp_concl skoprem
    5.29           fun cont (tacs,_,choices) = 
    5.30 -	     (case Sequence.pull(EVERY' (rev tacs) i st) of
    5.31 +	     (case Seq.pull(EVERY' (rev tacs) i st) of
    5.32  		  None => (writeln ("PROOF FAILED for depth " ^
    5.33  				    Int.toString lim);
    5.34  			   backtrack choices)
    5.35 -		| cell => Sequence.seqof(fn()=> cell))
    5.36 +		| cell => Seq.make(fn()=> cell))
    5.37       in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
    5.38       end
    5.39 -     handle PROVE     => Sequence.null);
    5.40 +     handle PROVE     => Seq.empty);
    5.41  
    5.42  fun blast_tac cs i st = (DEEPEN (1,20) (depth_tac cs) 0) i st
    5.43 -     handle TRANS s => (warning ("Blast_tac: " ^ s); Sequence.null);
    5.44 +     handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
    5.45  
    5.46  fun Blast_tac i = blast_tac (Data.claset()) i;
    5.47  
     6.1 --- a/src/Provers/classical.ML	Fri Nov 21 15:27:43 1997 +0100
     6.2 +++ b/src/Provers/classical.ML	Fri Nov 21 15:29:56 1997 +0100
     6.3 @@ -201,7 +201,7 @@
     6.4  (*Duplication of hazardous rules, for complete provers*)
     6.5  fun dup_intr th = zero_var_indexes (th RS classical);
     6.6  
     6.7 -fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> 
     6.8 +fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd |> 
     6.9                    rule_by_tactic (TRYALL (etac revcut_rl));
    6.10  
    6.11  
     7.1 --- a/src/Provers/simp.ML	Fri Nov 21 15:27:43 1997 +0100
     7.2 +++ b/src/Provers/simp.ML	Fri Nov 21 15:29:56 1997 +0100
     7.3 @@ -129,7 +129,7 @@
     7.4  in mk trans_thms end;
     7.5  
     7.6  (*Applies tactic and returns the first resulting state, FAILS if none!*)
     7.7 -fun one_result(tac,thm) = case Sequence.pull(tac thm) of
     7.8 +fun one_result(tac,thm) = case Seq.pull(tac thm) of
     7.9  	Some(thm',_) => thm'
    7.10        | None => raise THM("Simplifier: could not continue", 0, [thm]);
    7.11  
    7.12 @@ -205,7 +205,7 @@
    7.13  	  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    7.14  	  | _ => refl1_tac))
    7.15      val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
    7.16 -    val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
    7.17 +    val Some(thm'',_) = Seq.pull(add_norm_tac thm')
    7.18  in thm'' end;
    7.19  
    7.20  fun add_norm_tags congs =
    7.21 @@ -443,7 +443,7 @@
    7.22  fun simp_lhs(thm,ss,anet,ats,cs) =
    7.23      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
    7.24      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
    7.25 -    else case Sequence.pull(cong_tac i thm) of
    7.26 +    else case Seq.pull(cong_tac i thm) of
    7.27  	    Some(thm',_) =>
    7.28  		    let val ps = prems_of thm and ps' = prems_of thm';
    7.29  			val n = length(ps')-length(ps);
    7.30 @@ -467,7 +467,7 @@
    7.31  	(ss,thm,anet',anet::ats,cs) 
    7.32      end;
    7.33  
    7.34 -fun rew(seq,thm,ss,anet,ats,cs, more) = case Sequence.pull seq of
    7.35 +fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
    7.36        Some(thm',seq') =>
    7.37  	    let val n = (nprems_of thm') - (nprems_of thm)
    7.38  	    in pr_rew(i,n,thm,thm',more);
    7.39 @@ -481,7 +481,7 @@
    7.40  	    else (ss,thm,anet,ats,cs);
    7.41  
    7.42  fun try_true(thm,ss,anet,ats,cs) =
    7.43 -    case Sequence.pull(auto_tac i thm) of
    7.44 +    case Seq.pull(auto_tac i thm) of
    7.45        Some(thm',_) => (ss,thm',anet,ats,cs)
    7.46      | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
    7.47  	      in if !tracing
    7.48 @@ -492,7 +492,7 @@
    7.49  	      end;
    7.50  
    7.51  fun split(thm,ss,anet,ats,cs) =
    7.52 -	case Sequence.pull(tapply(split_tac
    7.53 +	case Seq.pull(tapply(split_tac
    7.54                                    (cong_tac i,splits,split_consts) i,thm)) of
    7.55  		Some(thm',_) => (SIMP_LHS::SPLIT::ss,thm',anet,ats,cs)
    7.56  	      | None => (ss,thm,anet,ats,cs);
     8.1 --- a/src/Provers/simplifier.ML	Fri Nov 21 15:27:43 1997 +0100
     8.2 +++ b/src/Provers/simplifier.ML	Fri Nov 21 15:29:56 1997 +0100
     8.3 @@ -346,7 +346,7 @@
     8.4  fun simp mode (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) thm =
     8.5    let
     8.6      val tacf = solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
     8.7 -    fun prover m th = apsome fst (Sequence.pull (tacf m th));
     8.8 +    fun prover m th = apsome fst (Seq.pull (tacf m th));
     8.9    in
    8.10      Drule.rewrite_thm mode prover mss thm
    8.11    end;
     9.1 --- a/src/ZF/ROOT.ML	Fri Nov 21 15:27:43 1997 +0100
     9.2 +++ b/src/ZF/ROOT.ML	Fri Nov 21 15:29:56 1997 +0100
     9.3 @@ -15,11 +15,11 @@
     9.4  
     9.5  (*For Pure/tactic??  A crude way of adding structure to rules*)
     9.6  fun CHECK_SOLVED tac st =
     9.7 -    case Sequence.pull (tac st) of
     9.8 +    case Seq.pull (tac st) of
     9.9          None => error"DO_GOAL: tactic list failed"
    9.10        | Some(x,_) => 
    9.11                  if has_fewer_prems 1 x then
    9.12 -                    Sequence.cons(x, Sequence.null)
    9.13 +                    Seq.cons(x, Seq.empty)
    9.14                  else (writeln"DO_GOAL: unsolved goals!!";
    9.15                        writeln"Final proof state was ...";
    9.16                        print_goals (!goals_limit) x;