tuned Seq/Envir/Unify interfaces;
authorwenzelm
Mon Jun 12 21:19:00 2006 +0200 (2006-06-12)
changeset 19861620d90091788
parent 19860 6e44610bdd76
child 19862 7f29aa958b72
tuned Seq/Envir/Unify interfaces;
src/HOL/TLA/Intensional.ML
src/HOL/Tools/inductive_codegen.ML
src/Provers/IsaPlanner/isand.ML
src/Provers/IsaPlanner/zipper.ML
src/Provers/eqsubst.ML
src/Provers/induct_method.ML
src/Pure/Isar/calculation.ML
src/Pure/drule.ML
src/Pure/envir.ML
src/Pure/tctical.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/TLA/Intensional.ML	Mon Jun 12 21:18:10 2006 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.ML	Mon Jun 12 21:19:00 2006 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4    let
     1.5      (* analogous to RS, but using matching instead of resolution *)
     1.6      fun matchres tha i thb =
     1.7 -      case Seq.chop (2, biresolution true [(false,tha)] i thb) of
     1.8 +      case Seq.chop 2 (biresolution true [(false,tha)] i thb) of
     1.9            ([th],_) => th
    1.10          | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
    1.11          |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Jun 12 21:18:10 2006 +0200
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jun 12 21:19:00 2006 +0200
     2.3 @@ -225,7 +225,7 @@
     2.4  datatype indprem = Prem of term list * term | Sidecond of term;
     2.5  
     2.6  fun select_mode_prem thy modes vs ps =
     2.7 -  find_first (isSome o snd) (ps ~~ map
     2.8 +  find_first (is_some o snd) (ps ~~ map
     2.9      (fn Prem (us, t) => find_first (fn Mode ((_, is), _) =>
    2.10            let
    2.11              val (in_ts, out_ts) = get_args is 1 us;
    2.12 @@ -574,7 +574,7 @@
    2.13               [(split_prod [] ((the o AList.lookup (op =) factors) name) t, prems)]) clauses
    2.14          end;
    2.15  
    2.16 -      fun check_set (Const (s, _)) = s mem names orelse isSome (get_clauses thy s)
    2.17 +      fun check_set (Const (s, _)) = s mem names orelse is_some (get_clauses thy s)
    2.18          | check_set (Var ((s, _), _)) = s mem arg_vs
    2.19          | check_set _ = false;
    2.20  
    2.21 @@ -746,13 +746,13 @@
    2.22  infix 5 :->;
    2.23  infix 3 ++;
    2.24  
    2.25 -fun s :-> f = Seq.flat (Seq.map f s);
    2.26 +fun s :-> f = Seq.maps f s;
    2.27  
    2.28 -fun s1 ++ s2 = Seq.append (s1, s2);
    2.29 +fun s1 ++ s2 = Seq.append s1 s2;
    2.30  
    2.31  fun ?? b = if b then Seq.single () else Seq.empty;
    2.32  
    2.33 -fun ?! s = isSome (Seq.pull s);    
    2.34 +fun ?! s = is_some (Seq.pull s);
    2.35  
    2.36  fun equal__1 x = Seq.single x;
    2.37  
     3.1 --- a/src/Provers/IsaPlanner/isand.ML	Mon Jun 12 21:18:10 2006 +0200
     3.2 +++ b/src/Provers/IsaPlanner/isand.ML	Mon Jun 12 21:19:00 2006 +0200
     3.3 @@ -124,8 +124,7 @@
     3.4  fun solve_with sol th = 
     3.5      let fun solvei 0 = Seq.empty
     3.6            | solvei i = 
     3.7 -            Seq.append (bicompose false (false,sol,0) i th, 
     3.8 -                        solvei (i - 1))
     3.9 +            Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
    3.10      in
    3.11        solvei (Thm.nprems_of th)
    3.12      end;
     4.1 --- a/src/Provers/IsaPlanner/zipper.ML	Mon Jun 12 21:18:10 2006 +0200
     4.2 +++ b/src/Provers/IsaPlanner/zipper.ML	Mon Jun 12 21:19:00 2006 +0200
     4.3 @@ -321,7 +321,7 @@
     4.4              (case lzy z
     4.5                of NONE => NONE
     4.6                 | SOME (hz,mz) => 
     4.7 -                 SOME (hz, Seq.append (mz, Seq.make (lzyl more))))
     4.8 +                 SOME (hz, Seq.append mz (Seq.make (lzyl more))))
     4.9          and lzy z = lzyl (fsearch z) ()
    4.10        in Seq.make o lzyl o fsearch end;
    4.11  
    4.12 @@ -335,7 +335,7 @@
    4.13            | lzyl a ((LookIn z) :: more) () =
    4.14              (case lzy a z
    4.15                of NONE => lzyl a more ()
    4.16 -               | SOME(hz,mz) => SOME(hz,Seq.append(mz,Seq.make(lzyl a more))))
    4.17 +               | SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more))))
    4.18          and lzy a z = 
    4.19              let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end
    4.20  
    4.21 @@ -351,7 +351,7 @@
    4.22            | lzyl ((a, LookIn z) :: more) () =
    4.23              (case lzyl (fsearch a z) () of 
    4.24                 NONE => lzyl more ()
    4.25 -             | SOME (z,mz) => SOME (z,Seq.append(mz, Seq.make (lzyl more))))
    4.26 +             | SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more))))
    4.27        in Seq.make (lzyl (fsearch a0 z)) end;
    4.28  
    4.29  
     5.1 --- a/src/Provers/eqsubst.ML	Mon Jun 12 21:18:10 2006 +0200
     5.2 +++ b/src/Provers/eqsubst.ML	Mon Jun 12 21:19:00 2006 +0200
     5.3 @@ -125,7 +125,7 @@
     5.4               Envir.alist_of env);
     5.5            val initenv = Envir.Envir {asol = Vartab.empty,
     5.6                                       iTs = typinsttab, maxidx = ix2};
     5.7 -          val useq = (Unify.smash_unifiers (sgn,initenv,[a]))
     5.8 +          val useq = Unify.smash_unifiers sgn [a] initenv
     5.9  	            handle UnequalLengths => Seq.empty
    5.10  		               | Term.TERM _ => Seq.empty;
    5.11            fun clean_unify' useq () =
    5.12 @@ -380,9 +380,8 @@
    5.13                  (case searchf searchinfo occ lhs of
    5.14                     SkipMore i => occ_search i moreasms
    5.15                   | SkipSeq ss =>
    5.16 -                   Seq.append (Seq.map (Library.pair asminfo)
    5.17 -                                       (Seq.flat ss),
    5.18 -                               occ_search 1 moreasms))
    5.19 +                   Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
    5.20 +                               (occ_search 1 moreasms))
    5.21                                (* find later substs also *)
    5.22            in
    5.23              occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
     6.1 --- a/src/Provers/induct_method.ML	Mon Jun 12 21:18:10 2006 +0200
     6.2 +++ b/src/Provers/induct_method.ML	Mon Jun 12 21:19:00 2006 +0200
     6.3 @@ -228,8 +228,8 @@
     6.4          val rule' = Thm.incr_indexes (maxidx + 1) rule;
     6.5          val concl = Logic.strip_assums_concl goal;
     6.6        in
     6.7 -        Unify.smash_unifiers (thy, Envir.empty (#maxidx (Thm.rep_thm rule')),
     6.8 -          [(Thm.concl_of rule', concl)])
     6.9 +        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
    6.10 +          (Envir.empty (#maxidx (Thm.rep_thm rule')))
    6.11          |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
    6.12        end
    6.13    end handle Subscript => Seq.empty;
     7.1 --- a/src/Pure/Isar/calculation.ML	Mon Jun 12 21:18:10 2006 +0200
     7.2 +++ b/src/Pure/Isar/calculation.ML	Mon Jun 12 21:19:00 2006 +0200
     7.3 @@ -84,7 +84,7 @@
     7.4  (* symmetric *)
     7.5  
     7.6  val symmetric = Thm.rule_attribute (fn x => fn th =>
     7.7 -  (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
     7.8 +  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
     7.9      ([th'], _) => th'
    7.10    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
    7.11    | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
     8.1 --- a/src/Pure/drule.ML	Mon Jun 12 21:18:10 2006 +0200
     8.2 +++ b/src/Pure/drule.ML	Mon Jun 12 21:19:00 2006 +0200
     8.3 @@ -434,7 +434,7 @@
     8.4    This step can lose information.*)
     8.5  fun flexflex_unique th =
     8.6    if null (tpairs_of th) then th else
     8.7 -    case Seq.chop (2, flexflex_rule th) of
     8.8 +    case Seq.chop 2 (flexflex_rule th) of
     8.9        ([th],_) => th
    8.10      | ([],_)   => raise THM("flexflex_unique: impossible constraints", 0, [th])
    8.11      |      _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
    8.12 @@ -538,7 +538,7 @@
    8.13  
    8.14  (*Resolution: exactly one resolvent must be produced.*)
    8.15  fun tha RSN (i,thb) =
    8.16 -  case Seq.chop (2, biresolution false [(false,tha)] i thb) of
    8.17 +  case Seq.chop 2 (biresolution false [(false,tha)] i thb) of
    8.18        ([th],_) => th
    8.19      | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
    8.20      |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
     9.1 --- a/src/Pure/envir.ML	Mon Jun 12 21:18:10 2006 +0200
     9.2 +++ b/src/Pure/envir.ML	Mon Jun 12 21:19:00 2006 +0200
     9.3 @@ -21,7 +21,7 @@
     9.4    val update: ((indexname * typ) * term) * env -> env
     9.5    val empty: int -> env
     9.6    val is_empty: env -> bool
     9.7 -  val above: int * env -> bool
     9.8 +  val above: env -> int -> bool
     9.9    val vupdate: ((indexname * typ) * term) * env -> env
    9.10    val alist_of: env -> (indexname * (typ * term)) list
    9.11    val norm_term: env -> term -> term
    9.12 @@ -104,12 +104,9 @@
    9.13  fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
    9.14  
    9.15  (*Determine if the least index updated exceeds lim*)
    9.16 -fun above (lim, Envir {asol, iTs, ...}) =
    9.17 -  (case (Vartab.min_key asol, Vartab.min_key iTs) of
    9.18 -     (NONE, NONE) => true
    9.19 -   | (SOME (_, i), NONE) => i > lim
    9.20 -   | (NONE, SOME (_, i')) => i' > lim
    9.21 -   | (SOME (_, i), SOME (_, i')) => i > lim andalso i' > lim);
    9.22 +fun above (Envir {asol, iTs, ...}) lim =
    9.23 +  (case Vartab.min_key asol of SOME (_, i) => i > lim | NONE => true) andalso
    9.24 +  (case Vartab.min_key iTs of SOME (_, i) => i > lim | NONE => true);
    9.25  
    9.26  (*Update, checking Var-Var assignments: try to suppress higher indexes*)
    9.27  fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
    10.1 --- a/src/Pure/tctical.ML	Mon Jun 12 21:18:10 2006 +0200
    10.2 +++ b/src/Pure/tctical.ML	Mon Jun 12 21:19:00 2006 +0200
    10.3 @@ -102,8 +102,7 @@
    10.4    Like ORELSE, but allows backtracking on both tac1 and tac2.
    10.5    The tactic tac2 is not applied until needed.*)
    10.6  fun (tac1 APPEND tac2) st =
    10.7 -  Seq.append(tac1 st,
    10.8 -                  Seq.make(fn()=> Seq.pull (tac2 st)));
    10.9 +  Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st)));
   10.10  
   10.11  (*Like APPEND, but interleaves results of tac1 and tac2.*)
   10.12  fun (tac1 INTLEAVE tac2) st =
    11.1 --- a/src/Pure/thm.ML	Mon Jun 12 21:18:10 2006 +0200
    11.2 +++ b/src/Pure/thm.ML	Mon Jun 12 21:19:00 2006 +0200
    11.3 @@ -951,7 +951,7 @@
    11.4    Resulting sequence may contain multiple elements if the tpairs are
    11.5      not all flex-flex. *)
    11.6  fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
    11.7 -  Unify.smash_unifiers (Theory.deref thy_ref, Envir.empty maxidx, tpairs)
    11.8 +  Unify.smash_unifiers (Theory.deref thy_ref) tpairs (Envir.empty maxidx)
    11.9    |> Seq.map (fn env =>
   11.10        if Envir.is_empty env then th
   11.11        else
   11.12 @@ -1426,7 +1426,7 @@
   11.13               if Envir.is_empty env then (tpairs, (Bs @ As, C))
   11.14               else
   11.15               let val ntps = map (pairself normt) tpairs
   11.16 -             in if Envir.above (smax, env) then
   11.17 +             in if Envir.above env smax then
   11.18                    (*no assignments in state; normalize the rule only*)
   11.19                    if lifted
   11.20                    then (ntps, (Bs @ map (norm_term_skip env nlift) As, C))
   11.21 @@ -1439,7 +1439,7 @@
   11.22               Thm{thy_ref = thy_ref,
   11.23                   der = Pt.infer_derivs
   11.24                     ((if Envir.is_empty env then I
   11.25 -                     else if Envir.above (smax, env) then
   11.26 +                     else if Envir.above env smax then
   11.27                         (fn f => fn der => f (Pt.norm_proof' env der))
   11.28                       else
   11.29                         curry op oo (Pt.norm_proof' env))