Replaced "flat" by the Basis Library function List.concat
authorpaulson
Fri Feb 21 15:31:47 1997 +0100 (1997-02-21)
changeset 267285d7e800d754
parent 2671 510d94c71dda
child 2673 1b266c161134
Replaced "flat" by the Basis Library function List.concat
src/Pure/axclass.ML
src/Pure/deriv.ML
src/Pure/drule.ML
src/Pure/net.ML
src/Pure/search.ML
src/Pure/sign.ML
src/Pure/symtab.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/axclass.ML	Fri Feb 21 15:30:41 1997 +0100
     1.2 +++ b/src/Pure/axclass.ML	Fri Feb 21 15:31:47 1997 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4            else err_bad_axsort name class
     1.5        | _ => err_bad_tfrees name);
     1.6  
     1.7 -    val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms));
     1.8 +    val axS = Sign.norm_sort sign (logicC :: List.concat(map axm_sort axioms))
     1.9  
    1.10      val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
    1.11      fun inclass c = Logic.mk_inclass (aT axS, c);
     2.1 --- a/src/Pure/deriv.ML	Fri Feb 21 15:30:41 1997 +0100
     2.2 +++ b/src/Pure/deriv.ML	Fri Feb 21 15:31:47 1997 +0100
     2.3 @@ -38,7 +38,7 @@
     2.4  	Join (Bicompose arg, linear rder) :: rev_deriv sder
     2.5    | rev_deriv (Join (_, [der]))	= rev_deriv der
     2.6    | rev_deriv (Join (rl, der::ders)) =	(*catch-all case; doubtful?*)
     2.7 -        Join(rl, flat (map linear ders)) :: rev_deriv der
     2.8 +        Join(rl, List.concat (map linear ders)) :: rev_deriv der
     2.9  and linear der 	= rev (rev_deriv der);
    2.10  
    2.11  
     3.1 --- a/src/Pure/drule.ML	Fri Feb 21 15:30:41 1997 +0100
     3.2 +++ b/src/Pure/drule.ML	Fri Feb 21 15:31:47 1997 +0100
     3.3 @@ -80,10 +80,10 @@
     3.4  (*results may contain duplicates!*)
     3.5  
     3.6  fun ancestry_of thy =
     3.7 -  thy :: flat (map ancestry_of (parents_of thy));
     3.8 +  thy :: List.concat (map ancestry_of (parents_of thy));
     3.9  
    3.10  val all_axioms_of =
    3.11 -  flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
    3.12 +  List.concat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
    3.13  
    3.14  
    3.15  (* clash_types, clash_consts *)
    3.16 @@ -389,7 +389,7 @@
    3.17  fun thas RLN (i,thbs) =
    3.18    let val resolve = biresolution false (map (pair false) thas) i
    3.19        fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
    3.20 -  in  flat (map resb thbs)  end;
    3.21 +  in  List.concat (map resb thbs)  end;
    3.22  
    3.23  fun thas RL thbs = thas RLN (1,thbs);
    3.24  
     4.1 --- a/src/Pure/net.ML	Fri Feb 21 15:30:41 1997 +0100
     4.2 +++ b/src/Pure/net.ML	Fri Feb 21 15:31:47 1997 +0100
     4.3 @@ -203,7 +203,7 @@
     4.4  	     | _ => rands t (net, var::nets)	(*var could match also*)
     4.5    end;
     4.6  
     4.7 -fun extract_leaves l = flat (map (fn Leaf(xs) => xs) l);
     4.8 +fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);
     4.9  
    4.10  (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
    4.11  fun match_term net t = 
     5.1 --- a/src/Pure/search.ML	Fri Feb 21 15:30:41 1997 +0100
     5.2 +++ b/src/Pure/search.ML	Fri Feb 21 15:31:47 1997 +0100
     5.3 @@ -5,8 +5,13 @@
     5.4  Search tacticals
     5.5  *)
     5.6  
     5.7 +infix 1 THEN_MAYBE THEN_MAYBE';
     5.8 +
     5.9  signature SEARCH =
    5.10    sig
    5.11 +  val THEN_MAYBE	: tactic * tactic -> tactic
    5.12 +  val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
    5.13 +
    5.14    val trace_DEPTH_FIRST	: bool ref
    5.15    val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic
    5.16    val DEPTH_SOLVE	: tactic -> tactic
    5.17 @@ -57,6 +62,14 @@
    5.18  (*Apply a tactic if subgoals remain, else do nothing.*)
    5.19  val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
    5.20  
    5.21 +(*Execute tac1, but only execute tac2 if there are at least as many subgoals
    5.22 +  as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    5.23 +fun tac1 THEN_MAYBE tac2 = STATE
    5.24 +    (fn st => tac1  THEN  
    5.25 +	 COND (has_fewer_prems (nprems_of st)) all_tac tac2);
    5.26 +
    5.27 +fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
    5.28 +
    5.29  (*Tactical to reduce the number of premises by 1.
    5.30    If no subgoals then it must fail! *)
    5.31  fun DEPTH_SOLVE_1 tac = STATE
    5.32 @@ -198,7 +211,7 @@
    5.33  	      ([],[]) => []
    5.34  	    | ([],nonsats) => 
    5.35  		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
    5.36 -		   bfs (flat (map tacf nonsats)))
    5.37 +		   bfs (List.concat (map tacf nonsats)))
    5.38  	    | (sats,_)  => sats)
    5.39    in (fn st => Sequence.s_of_list (bfs [st])) end;
    5.40  
     6.1 --- a/src/Pure/sign.ML	Fri Feb 21 15:30:41 1997 +0100
     6.2 +++ b/src/Pure/sign.ML	Fri Feb 21 15:31:47 1997 +0100
     6.3 @@ -197,7 +197,7 @@
     6.4      Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons));
     6.5      Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
     6.6      Pretty.writeln (Pretty.big_list "arities:"
     6.7 -                      (flat (map pretty_arities arities)));
     6.8 +                      (List.concat (map pretty_arities arities)));
     6.9      Pretty.writeln (Pretty.big_list "consts:"
    6.10                        (map (pretty_const syn) (Symtab.dest const_tab)))
    6.11    end;
     7.1 --- a/src/Pure/symtab.ML	Fri Feb 21 15:30:41 1997 +0100
     7.2 +++ b/src/Pure/symtab.ML	Fri Feb 21 15:31:47 1997 +0100
     7.3 @@ -157,7 +157,7 @@
     7.4    balance (foldr cons_entry (alst, Tip));
     7.5  
     7.6  fun dest_multi tab =
     7.7 -  flat (map (fn (key, entries) => map (pair key) entries) (dest tab));
     7.8 +  List.concat (map (fn (key, entries) => map (pair key) entries) (dest tab));
     7.9  
    7.10  
    7.11  (* map tables *)
     8.1 --- a/src/Pure/tactic.ML	Fri Feb 21 15:30:41 1997 +0100
     8.2 +++ b/src/Pure/tactic.ML	Fri Feb 21 15:31:47 1997 +0100
     8.3 @@ -61,6 +61,7 @@
     8.4    val net_biresolve_tac: (bool*thm) list -> int -> tactic
     8.5    val net_match_tac: thm list -> int -> tactic
     8.6    val net_resolve_tac: thm list -> int -> tactic
     8.7 +  val orderlist: (int * 'a) list -> 'a list
     8.8    val PRIMITIVE: (thm -> thm) -> tactic  
     8.9    val PRIMSEQ: (thm -> thm Sequence.seq) -> tactic  
    8.10    val prune_params_tac: tactic
    8.11 @@ -387,7 +388,7 @@
    8.12        let val hyps = Logic.strip_assums_hyp prem
    8.13            and concl = Logic.strip_assums_concl prem 
    8.14            val kbrls = Net.unify_term inet concl @
    8.15 -                      flat (map (Net.unify_term enet) hyps)
    8.16 +                      List.concat (map (Net.unify_term enet) hyps)
    8.17        in PRIMSEQ (biresolution match (orderlist kbrls) i) end);
    8.18  
    8.19  (*versions taking pre-built nets*)
    8.20 @@ -527,11 +528,8 @@
    8.21  
    8.22  (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
    8.23    right to left if n is positive, and from left to right if n is negative.*)
    8.24 -fun rotate_tac n =
    8.25 -  let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
    8.26 -  in if n >= 0 then rot n
    8.27 -     else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i)
    8.28 -  end;
    8.29 +fun rotate_tac 0 i = all_tac
    8.30 +  | rotate_tac k i = PRIMITIVE (rotate_rule k i);
    8.31  
    8.32  end;
    8.33  
     9.1 --- a/src/Pure/tctical.ML	Fri Feb 21 15:30:41 1997 +0100
     9.2 +++ b/src/Pure/tctical.ML	Fri Feb 21 15:31:47 1997 +0100
     9.3 @@ -6,7 +6,7 @@
     9.4  Tacticals
     9.5  *)
     9.6  
     9.7 -infix 1 THEN THEN' THEN_MAYBE THEN_MAYBE';
     9.8 +infix 1 THEN THEN';
     9.9  infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
    9.10  infix 0 THEN_ELSE;
    9.11  
    9.12 @@ -55,8 +55,6 @@
    9.13    val suppress_tracing  : bool ref
    9.14    val THEN              : tactic * tactic -> tactic
    9.15    val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    9.16 -  val THEN_MAYBE	: tactic * tactic -> tactic
    9.17 -  val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
    9.18    val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
    9.19    val traced_tac        : (thm -> (thm * thm Sequence.seq) option) -> tactic
    9.20    val tracify           : bool ref -> tactic -> thm -> thm Sequence.seq
    9.21 @@ -148,21 +146,34 @@
    9.22  (*Do the tactic or else do nothing*)
    9.23  fun TRY tac = tac ORELSE all_tac;
    9.24  
    9.25 -(*Execute tac1, but only execute tac2 if there are at least as many subgoals
    9.26 -  as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    9.27 -fun tac1 THEN_MAYBE tac2 = let fun has_fewer_prems n rule = (nprems_of rule < n)
    9.28 -in STATE (fn state => tac1  THEN  
    9.29 -	 COND (has_fewer_prems (nprems_of state)) all_tac tac2) end;
    9.30 -fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
    9.31 +(*** List-oriented tactics ***)
    9.32 +
    9.33 +local
    9.34 +  (*This version of EVERY avoids backtracking over repeated states*)
    9.35 +
    9.36 +  fun EVY (trail, []) st = 
    9.37 +	Sequence.seqof (fn()=> Some(st, 
    9.38 +			Sequence.seqof (fn()=> Sequence.pull (evyBack trail))))
    9.39 +    | EVY (trail, tac::tacs) st = 
    9.40 +	  case Sequence.pull(tac st) of
    9.41 +	      None    => evyBack trail              (*failed: backtrack*)
    9.42 +	    | Some(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
    9.43 +  and evyBack [] = Sequence.null (*no alternatives*)
    9.44 +    | evyBack ((st',q,tacs)::trail) =
    9.45 +	  case Sequence.pull q of
    9.46 +	      None        => evyBack trail
    9.47 +	    | Some(st,q') => if eq_thm (st',st) 
    9.48 +			     then evyBack ((st',q',tacs)::trail)
    9.49 +			     else EVY ((st,q',tacs)::trail, tacs) st
    9.50 +in
    9.51 +
    9.52 +(* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)
    9.53 +fun EVERY tacs = EVY ([], tacs);
    9.54 +end;
    9.55  
    9.56  
    9.57 -(*** List-oriented tactics ***)
    9.58 -
    9.59 -(* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)
    9.60 -fun EVERY tacs = foldr (op THEN) (tacs, all_tac);
    9.61 -
    9.62  (* EVERY' [tac1,...,tacn] i  equals    tac1 i THEN ... THEN tacn i   *)
    9.63 -fun EVERY' tacs = foldr (op THEN') (tacs, K all_tac);
    9.64 +fun EVERY' tacs i = EVERY (map (fn f => f i) tacs);
    9.65  
    9.66  (*Apply every tactic to 1*)
    9.67  fun EVERY1 tacs = EVERY' tacs 1;
    10.1 --- a/src/Pure/type.ML	Fri Feb 21 15:30:41 1997 +0100
    10.2 +++ b/src/Pure/type.ML	Fri Feb 21 15:31:47 1997 +0100
    10.3 @@ -758,7 +758,8 @@
    10.4    let
    10.5      val TySg {classes, subclass, default, tycons, arities, abbrs} = tsig;
    10.6      val arities1 =
    10.7 -      flat (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
    10.8 +      List.concat 
    10.9 +          (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
   10.10      val arities2 = foldl (coregular (classes, subclass, tycons))
   10.11                           (arities, min_domain subclass arities1)
   10.12        |> close subclass;