Removal of the tactical STATE
authorpaulson
Tue Jul 22 11:14:18 1997 +0200 (1997-07-22)
changeset 3538ed9de44032e0
parent 3537 79ac9b475621
child 3539 d4443afc8d28
Removal of the tactical STATE
src/HOL/datatype.ML
src/HOL/simpdata.ML
src/HOL/thy_data.ML
src/Pure/search.ML
src/Pure/tactic.ML
src/Sequents/prover.ML
     1.1 --- a/src/HOL/datatype.ML	Tue Jul 22 11:12:55 1997 +0200
     1.2 +++ b/src/HOL/datatype.ML	Tue Jul 22 11:14:18 1997 +0200
     1.3 @@ -6,10 +6,11 @@
     1.4  *)
     1.5  
     1.6  (* should go into Pure *)
     1.7 -fun ALLNEWSUBGOALS tac tacf i =
     1.8 -  STATE (fn state0 => tac i THEN
     1.9 -  STATE (fn state1 => let val d = nprems_of state1 - nprems_of state0
    1.10 -                      in EVERY(map tacf ((i+d) downto i)) end));
    1.11 +fun ALLNEWSUBGOALS tac tacf i st0 = st0 |>
    1.12 +  (tac i THEN
    1.13 +   (fn st1 => st1 |> 
    1.14 +        let val d = nprems_of st1 - nprems_of st0
    1.15 +        in EVERY(map tacf ((i+d) downto i)) end));
    1.16  
    1.17  (*used for constructor parameters*)
    1.18  datatype dt_type = dtVar of string |
    1.19 @@ -878,12 +879,11 @@
    1.20       fun exhaust_tac a =
    1.21             ALLNEWSUBGOALS (res_inst_tac [(exh_var,a)] exhaustion)
    1.22                            (rotate_tac ~1);
    1.23 -     fun induct_tac a i =
    1.24 -           STATE(fn st =>
    1.25 +     fun induct_tac a i st = st |>
    1.26               (if Datatype.occs_in_prems a i st
    1.27                then warning "Induction variable occurs also among premises!"
    1.28                else ();
    1.29 -              itac a i))
    1.30 +              itac a i)
    1.31   in
    1.32    (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
    1.33          case_const = const (ty^"_case"),
     2.1 --- a/src/HOL/simpdata.ML	Tue Jul 22 11:12:55 1997 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Tue Jul 22 11:14:18 1997 +0200
     2.3 @@ -388,20 +388,20 @@
     2.4  
     2.5  (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
     2.6     fails if there is no equaliy or if an equality is already at the front *)
     2.7 -fun rot_eq_tac i = 
     2.8 -  let fun is_eq (Const ("Trueprop", _) $ (Const("op =",_) $ _ $ _)) = true
     2.9 -	| is_eq _ = false;
    2.10 -      fun find_eq n [] = None
    2.11 -	| find_eq n (t :: ts) = if (is_eq t) then Some n 
    2.12 -				else find_eq (n + 1) ts;
    2.13 -      fun rot_eq state = 
    2.14 -	  let val (_, _, Bi, _) = dest_state (state, i) 
    2.15 -	  in  case find_eq 0 (Logic.strip_assums_hyp Bi) of
    2.16 +local
    2.17 +  fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
    2.18 +    | is_eq _ = false;
    2.19 +  fun find_eq n [] = None
    2.20 +    | find_eq n (t :: ts) = if (is_eq t) then Some n 
    2.21 +			    else find_eq (n + 1) ts;
    2.22 +in
    2.23 +val rot_eq_tac = 
    2.24 +     SUBGOAL (fn (Bi,i) => 
    2.25 +	      case find_eq 0 (Logic.strip_assums_hyp Bi) of
    2.26  		  None   => no_tac
    2.27  		| Some 0 => no_tac
    2.28 -		| Some n => rotate_tac n i
    2.29 -	  end;
    2.30 -  in STATE rot_eq end;
    2.31 +		| Some n => rotate_tac n i)
    2.32 +end;
    2.33  
    2.34  (*an unsatisfactory fix for the incomplete asm_full_simp_tac!
    2.35    better: asm_really_full_simp_tac, a yet to be implemented version of
     3.1 --- a/src/HOL/thy_data.ML	Tue Jul 22 11:12:55 1997 +0200
     3.2 +++ b/src/HOL/thy_data.ML	Tue Jul 22 11:14:18 1997 +0200
     3.3 @@ -85,23 +85,19 @@
     3.4  in
     3.5  
     3.6  (* generic induction tactic for datatypes *)
     3.7 -fun induct_tac var i =
     3.8 -  let fun induct state =
     3.9 +fun induct_tac var i state = state |>
    3.10          let val (_, _, Bi, _) = dest_state (state, i)
    3.11              val sign = #sign(rep_thm state)
    3.12              val tn = find_tname var Bi
    3.13              val ind_tac = #induct_tac(get_dt_info sign tn)
    3.14 -        in ind_tac var i end
    3.15 -  in STATE induct end;
    3.16 +        in ind_tac var i end;
    3.17  
    3.18  (* generic exhaustion tactic for datatypes *)
    3.19 -fun exhaust_tac aterm i =
    3.20 -  let fun exhaust state =
    3.21 +fun exhaust_tac aterm i state = state |>
    3.22          let val sign = #sign(rep_thm state)
    3.23              val tn = infer_tname state sign i aterm
    3.24              val exh_tac = #exhaust_tac(get_dt_info sign tn)
    3.25 -        in exh_tac aterm i end
    3.26 -  in STATE exhaust end;
    3.27 +        in exh_tac aterm i end;
    3.28  
    3.29  end;
    3.30  
     4.1 --- a/src/Pure/search.ML	Tue Jul 22 11:12:55 1997 +0200
     4.2 +++ b/src/Pure/search.ML	Tue Jul 22 11:14:18 1997 +0200
     4.3 @@ -66,19 +66,17 @@
     4.4  
     4.5  (*Execute tac1, but only execute tac2 if there are at least as many subgoals
     4.6    as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
     4.7 -fun tac1 THEN_MAYBE tac2 = STATE
     4.8 -    (fn st => tac1  THEN  
     4.9 -	 COND (has_fewer_prems (nprems_of st)) all_tac tac2);
    4.10 +fun (tac1 THEN_MAYBE tac2) st = 
    4.11 +    (tac1  THEN  COND (has_fewer_prems (nprems_of st)) all_tac tac2)  st;
    4.12  
    4.13  fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
    4.14  
    4.15  (*Tactical to reduce the number of premises by 1.
    4.16    If no subgoals then it must fail! *)
    4.17 -fun DEPTH_SOLVE_1 tac = STATE
    4.18 - (fn st => 
    4.19 +fun DEPTH_SOLVE_1 tac st = st |>
    4.20      (case nprems_of st of
    4.21  	0 => no_tac
    4.22 -      | n => DEPTH_FIRST (has_fewer_prems n) tac));
    4.23 +      | n => DEPTH_FIRST (has_fewer_prems n) tac);
    4.24  
    4.25  (*Uses depth-first search to solve ALL subgoals*)
    4.26  val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
    4.27 @@ -166,12 +164,11 @@
    4.28  (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
    4.29    using increment "inc" up to limit "lim". *)
    4.30  fun DEEPEN (inc,lim) tacf m i = 
    4.31 -  let fun dpn m = STATE(fn state => 
    4.32 -			if has_fewer_prems i state then no_tac
    4.33 -			else if m>lim then 
    4.34 -			     (writeln "Giving up..."; no_tac)
    4.35 -			else (writeln ("Depth = " ^ string_of_int m);
    4.36 -			      tacf m i  ORELSE  dpn (m+inc)))
    4.37 +  let fun dpn m st = st |> (if has_fewer_prems i st then no_tac
    4.38 +			    else if m>lim then 
    4.39 +				(writeln "Giving up..."; no_tac)
    4.40 +				 else (writeln ("Depth = " ^ string_of_int m);
    4.41 +				       tacf m i  ORELSE  dpn (m+inc)))
    4.42    in  dpn m  end;
    4.43  
    4.44  (*** Best-first search ***)
     5.1 --- a/src/Pure/tactic.ML	Tue Jul 22 11:12:55 1997 +0200
     5.2 +++ b/src/Pure/tactic.ML	Tue Jul 22 11:14:18 1997 +0200
     5.3 @@ -269,12 +269,10 @@
     5.4       subgoal.  Fails if "i" is out of range.  ***)
     5.5  
     5.6  (*compose version: arguments are as for bicompose.*)
     5.7 -fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
     5.8 -  STATE ( fn st => 
     5.9 -	   compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule),
    5.10 -			nsubgoal) i
    5.11 -	   handle TERM (msg,_) => (writeln msg;  no_tac)
    5.12 -		| THM  (msg,_,_) => (writeln msg;  no_tac) );
    5.13 +fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st = st |>
    5.14 +  (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
    5.15 +   handle TERM (msg,_)   => (writeln msg;  no_tac)
    5.16 +	| THM  (msg,_,_) => (writeln msg;  no_tac));
    5.17  
    5.18  (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
    5.19    terms that are substituted contain (term or type) unknowns from the
     6.1 --- a/src/Sequents/prover.ML	Tue Jul 22 11:12:55 1997 +0200
     6.2 +++ b/src/Sequents/prover.ML	Tue Jul 22 11:14:18 1997 +0200
     6.3 @@ -85,13 +85,13 @@
     6.4  
     6.5  fun RESOLVE_THEN rules =
     6.6    let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
     6.7 -      fun tac nextac i = STATE (fn state =>  
     6.8 -	  filseq_resolve_tac rls0 9999 i 
     6.9 -	  ORELSE
    6.10 -	  (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
    6.11 -	  ORELSE
    6.12 -	  (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
    6.13 -					THEN  TRY(nextac i)) )
    6.14 +      fun tac nextac i state = state |>
    6.15 +	     (filseq_resolve_tac rls0 9999 i 
    6.16 +	      ORELSE
    6.17 +	      (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
    6.18 +	      ORELSE
    6.19 +	      (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
    6.20 +					    THEN  TRY(nextac i)))
    6.21    in  tac  end;
    6.22  
    6.23  
    6.24 @@ -202,11 +202,11 @@
    6.25  
    6.26  fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
    6.27                                      else tf(i) THEN tac(i-1)
    6.28 -                    in STATE(fn state=> tac(nprems_of state)) end;
    6.29 +                    in fn st => tac (nprems_of st) st end;
    6.30  
    6.31  (* Depth first search bounded by d *)
    6.32 -fun solven_tac d n = STATE (fn state =>
    6.33 -        if d<0 then no_tac
    6.34 +fun solven_tac d n state = state |>
    6.35 +       (if d<0 then no_tac
    6.36          else if (nprems_of state = 0) then all_tac 
    6.37          else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
    6.38                   ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
    6.39 @@ -214,10 +214,10 @@
    6.40  
    6.41  fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
    6.42  
    6.43 -fun step_tac n = STATE (fn state =>  
    6.44 -      if (nprems_of state = 0) then all_tac 
    6.45 -      else (DETERM(fres_safe_tac n)) ORELSE 
    6.46 -           (fres_unsafe_tac n APPEND fres_bound_tac n));
    6.47 +fun step_tac n = 
    6.48 +    COND (has_fewer_prems 1) all_tac 
    6.49 +         (DETERM(fres_safe_tac n) ORELSE 
    6.50 +	  (fres_unsafe_tac n APPEND fres_bound_tac n));
    6.51  
    6.52  end;
    6.53  end;