Gradual switching to Basis Library functions nth, drop, etc.
authorpaulson
Tue Feb 04 10:33:58 1997 +0100 (1997-02-04)
changeset 2580e3f680709487
parent 2579 4af1023fc6bf
child 2581 e08c25821e08
Gradual switching to Basis Library functions nth, drop, etc.
src/Pure/goals.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/goals.ML	Tue Feb 04 08:59:50 1997 +0100
     1.2 +++ b/src/Pure/goals.ML	Tue Feb 04 10:33:58 1997 +0100
     1.3 @@ -42,6 +42,7 @@
     1.4    val goalw_cterm	: thm list -> cterm -> thm list
     1.5    val pop_proof		: unit -> thm list
     1.6    val pr		: unit -> unit
     1.7 +  val prlev		: int -> unit
     1.8    val prlim		: int -> unit
     1.9    val pr_latex		: unit -> unit
    1.10    val printgoal_latex	: int -> unit
    1.11 @@ -52,7 +53,6 @@
    1.12    val pprint_typ	: typ -> pprint_args -> unit
    1.13    val print_exn		: exn -> 'a
    1.14    val print_sign_exn	: Sign.sg -> exn -> 'a
    1.15 -  val prlev		: int -> unit
    1.16    val proof_timing	: bool ref
    1.17    val prove_goal	: theory -> string -> (thm list -> tactic list) -> thm
    1.18    val prove_goalw      : theory->thm list->string->(thm list->tactic list)->thm
    1.19 @@ -260,10 +260,8 @@
    1.20  fun uresult () = !curr_mkresult (false, topthm());
    1.21  
    1.22  (*Get subgoal i from goal stack*)
    1.23 -fun getgoal i = 
    1.24 -      (case  drop (i-1, prems_of (topthm()))  of
    1.25 -	    [] => error"getgoal: Goal number out of range"
    1.26 -	  | Q::_ => Q);
    1.27 +fun getgoal i = List.nth (prems_of (topthm()), i-1)
    1.28 +                handle Subscript => error"getgoal: Goal number out of range";
    1.29  
    1.30  (*Return subgoal i's hypotheses as meta-level assumptions.
    1.31    For debugging uses of METAHYPS*)
    1.32 @@ -281,9 +279,9 @@
    1.33  fun chop_level n (pair,pairs) = 
    1.34    let val level = length pairs
    1.35    in  if n<0 andalso ~n <= level
    1.36 -      then  drop (~n, pair::pairs) 
    1.37 +      then  List.drop (pair::pairs, ~n) 
    1.38        else if 0<=n andalso n<= level
    1.39 -      then  drop (level - n, pair::pairs) 
    1.40 +      then  List.drop (pair::pairs, level - n) 
    1.41        else  error ("Level number must lie between 0 and " ^ 
    1.42  		   string_of_int level)
    1.43    end;
     2.1 --- a/src/Pure/tactic.ML	Tue Feb 04 08:59:50 1997 +0100
     2.2 +++ b/src/Pure/tactic.ML	Tue Feb 04 10:33:58 1997 +0100
     2.3 @@ -123,9 +123,9 @@
     2.4  fun defer_tac i state = 
     2.5      let val (state',thaw) = freeze_thaw state
     2.6  	val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
     2.7 -	val hyp::hyps' = drop(i-1,hyps)
     2.8 +	val hyp::hyps' = List.drop(hyps, i-1)
     2.9      in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
    2.10 -        |> implies_intr_list (take(i-1,hyps) @ hyps')
    2.11 +        |> implies_intr_list (List.take(hyps, i-1) @ hyps')
    2.12          |> thaw
    2.13          |> Sequence.single
    2.14      end
     3.1 --- a/src/Pure/tctical.ML	Tue Feb 04 08:59:50 1997 +0100
     3.2 +++ b/src/Pure/tctical.ML	Tue Feb 04 10:33:58 1997 +0100
     3.3 @@ -304,10 +304,8 @@
     3.4  
     3.5  
     3.6  (*Make a tactic for subgoal i, if there is one.  *)
     3.7 -fun SUBGOAL goalfun i st = 
     3.8 -  case drop(i-1, prems_of st) of
     3.9 -      [] => Sequence.null
    3.10 -    | prem::_ => goalfun (prem,i) st;
    3.11 +fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1),  i) st
    3.12 +                             handle Subscript => Sequence.null;
    3.13  
    3.14  
    3.15  (*** SELECT_GOAL ***)
    3.16 @@ -346,9 +344,8 @@
    3.17  
    3.18  (*Does the work of SELECT_GOAL. *)
    3.19  fun select tac st0 i =
    3.20 -  let val cprem::_ = drop(i-1, cprems_of st0)
    3.21 -      val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
    3.22 -                                eq_trivial (adjust_maxidx cprem)
    3.23 +  let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
    3.24 +	  eq_trivial (adjust_maxidx (List.nth(cprems_of st0, i-1)))
    3.25        fun next st = bicompose false (false, restore st, nprems_of st) i st0
    3.26    in  Sequence.flats (Sequence.maps next (tac eq_cprem))
    3.27    end;
    3.28 @@ -365,7 +362,7 @@
    3.29          handle _ => error"SELECT_GOAL -- impossible error???";
    3.30  
    3.31  fun SELECT_GOAL tac i st = 
    3.32 -  case (i, drop(i-1, prems_of st)) of
    3.33 +  case (i, List.drop(prems_of st, i-1)) of
    3.34        (_,[]) => Sequence.null
    3.35      | (1,[_]) => tac st         (*If i=1 and only one subgoal do nothing!*)
    3.36      | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i
     4.1 --- a/src/Pure/term.ML	Tue Feb 04 08:59:50 1997 +0100
     4.2 +++ b/src/Pure/term.ML	Tue Feb 04 10:33:58 1997 +0100
     4.3 @@ -294,10 +294,9 @@
     4.4  fun subst_bounds (args: term list, t) : term = 
     4.5    let val n = length args;
     4.6        fun subst (t as Bound i, lev) =
     4.7 - 	    if i<lev then  t    (*var is locally bound*)
     4.8 -	    else  (case (drop (i-lev,args)) of
     4.9 -		  []     => Bound(i-n)  (*loose: change it*)
    4.10 -	        | arg::_ => incr_boundvars lev arg)
    4.11 + 	   (if i<lev then  t    (*var is locally bound*)
    4.12 +	    else  incr_boundvars lev (List.nth(args, i-lev))
    4.13 +		    handle Subscript => Bound(i-n)  (*loose: change it*))
    4.14  	| subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
    4.15  	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
    4.16  	| subst (t,lev) = t