--- a/src/Pure/axclass.ML Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/axclass.ML Fri Feb 21 15:31:47 1997 +0100
@@ -199,7 +199,7 @@
else err_bad_axsort name class
| _ => err_bad_tfrees name);
- val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms));
+ val axS = Sign.norm_sort sign (logicC :: List.concat(map axm_sort axioms))
val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
fun inclass c = Logic.mk_inclass (aT axS, c);
--- a/src/Pure/deriv.ML Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/deriv.ML Fri Feb 21 15:31:47 1997 +0100
@@ -38,7 +38,7 @@
Join (Bicompose arg, linear rder) :: rev_deriv sder
| rev_deriv (Join (_, [der])) = rev_deriv der
| rev_deriv (Join (rl, der::ders)) = (*catch-all case; doubtful?*)
- Join(rl, flat (map linear ders)) :: rev_deriv der
+ Join(rl, List.concat (map linear ders)) :: rev_deriv der
and linear der = rev (rev_deriv der);
--- a/src/Pure/drule.ML Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/drule.ML Fri Feb 21 15:31:47 1997 +0100
@@ -80,10 +80,10 @@
(*results may contain duplicates!*)
fun ancestry_of thy =
- thy :: flat (map ancestry_of (parents_of thy));
+ thy :: List.concat (map ancestry_of (parents_of thy));
val all_axioms_of =
- flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
+ List.concat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
(* clash_types, clash_consts *)
@@ -389,7 +389,7 @@
fun thas RLN (i,thbs) =
let val resolve = biresolution false (map (pair false) thas) i
fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
- in flat (map resb thbs) end;
+ in List.concat (map resb thbs) end;
fun thas RL thbs = thas RLN (1,thbs);
--- a/src/Pure/net.ML Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/net.ML Fri Feb 21 15:31:47 1997 +0100
@@ -203,7 +203,7 @@
| _ => rands t (net, var::nets) (*var could match also*)
end;
-fun extract_leaves l = flat (map (fn Leaf(xs) => xs) l);
+fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);
(*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
fun match_term net t =
--- a/src/Pure/search.ML Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/search.ML Fri Feb 21 15:31:47 1997 +0100
@@ -5,8 +5,13 @@
Search tacticals
*)
+infix 1 THEN_MAYBE THEN_MAYBE';
+
signature SEARCH =
sig
+ val THEN_MAYBE : tactic * tactic -> tactic
+ val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
+
val trace_DEPTH_FIRST : bool ref
val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic
val DEPTH_SOLVE : tactic -> tactic
@@ -57,6 +62,14 @@
(*Apply a tactic if subgoals remain, else do nothing.*)
val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
+(*Execute tac1, but only execute tac2 if there are at least as many subgoals
+ as before. This ensures that tac2 is only applied to an outcome of tac1.*)
+fun tac1 THEN_MAYBE tac2 = STATE
+ (fn st => tac1 THEN
+ COND (has_fewer_prems (nprems_of st)) all_tac tac2);
+
+fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
+
(*Tactical to reduce the number of premises by 1.
If no subgoals then it must fail! *)
fun DEPTH_SOLVE_1 tac = STATE
@@ -198,7 +211,7 @@
([],[]) => []
| ([],nonsats) =>
(prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
- bfs (flat (map tacf nonsats)))
+ bfs (List.concat (map tacf nonsats)))
| (sats,_) => sats)
in (fn st => Sequence.s_of_list (bfs [st])) end;
--- a/src/Pure/sign.ML Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/sign.ML Fri Feb 21 15:31:47 1997 +0100
@@ -197,7 +197,7 @@
Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons));
Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
Pretty.writeln (Pretty.big_list "arities:"
- (flat (map pretty_arities arities)));
+ (List.concat (map pretty_arities arities)));
Pretty.writeln (Pretty.big_list "consts:"
(map (pretty_const syn) (Symtab.dest const_tab)))
end;
--- a/src/Pure/symtab.ML Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/symtab.ML Fri Feb 21 15:31:47 1997 +0100
@@ -157,7 +157,7 @@
balance (foldr cons_entry (alst, Tip));
fun dest_multi tab =
- flat (map (fn (key, entries) => map (pair key) entries) (dest tab));
+ List.concat (map (fn (key, entries) => map (pair key) entries) (dest tab));
(* map tables *)
--- a/src/Pure/tactic.ML Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/tactic.ML Fri Feb 21 15:31:47 1997 +0100
@@ -61,6 +61,7 @@
val net_biresolve_tac: (bool*thm) list -> int -> tactic
val net_match_tac: thm list -> int -> tactic
val net_resolve_tac: thm list -> int -> tactic
+ val orderlist: (int * 'a) list -> 'a list
val PRIMITIVE: (thm -> thm) -> tactic
val PRIMSEQ: (thm -> thm Sequence.seq) -> tactic
val prune_params_tac: tactic
@@ -387,7 +388,7 @@
let val hyps = Logic.strip_assums_hyp prem
and concl = Logic.strip_assums_concl prem
val kbrls = Net.unify_term inet concl @
- flat (map (Net.unify_term enet) hyps)
+ List.concat (map (Net.unify_term enet) hyps)
in PRIMSEQ (biresolution match (orderlist kbrls) i) end);
(*versions taking pre-built nets*)
@@ -527,11 +528,8 @@
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
right to left if n is positive, and from left to right if n is negative.*)
-fun rotate_tac n =
- let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
- in if n >= 0 then rot n
- else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i)
- end;
+fun rotate_tac 0 i = all_tac
+ | rotate_tac k i = PRIMITIVE (rotate_rule k i);
end;
--- a/src/Pure/tctical.ML Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/tctical.ML Fri Feb 21 15:31:47 1997 +0100
@@ -6,7 +6,7 @@
Tacticals
*)
-infix 1 THEN THEN' THEN_MAYBE THEN_MAYBE';
+infix 1 THEN THEN';
infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
infix 0 THEN_ELSE;
@@ -55,8 +55,6 @@
val suppress_tracing : bool ref
val THEN : tactic * tactic -> tactic
val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
- val THEN_MAYBE : tactic * tactic -> tactic
- val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
val THEN_ELSE : tactic * (tactic*tactic) -> tactic
val traced_tac : (thm -> (thm * thm Sequence.seq) option) -> tactic
val tracify : bool ref -> tactic -> thm -> thm Sequence.seq
@@ -148,21 +146,34 @@
(*Do the tactic or else do nothing*)
fun TRY tac = tac ORELSE all_tac;
-(*Execute tac1, but only execute tac2 if there are at least as many subgoals
- as before. This ensures that tac2 is only applied to an outcome of tac1.*)
-fun tac1 THEN_MAYBE tac2 = let fun has_fewer_prems n rule = (nprems_of rule < n)
-in STATE (fn state => tac1 THEN
- COND (has_fewer_prems (nprems_of state)) all_tac tac2) end;
-fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
+(*** List-oriented tactics ***)
+
+local
+ (*This version of EVERY avoids backtracking over repeated states*)
+
+ fun EVY (trail, []) st =
+ Sequence.seqof (fn()=> Some(st,
+ Sequence.seqof (fn()=> Sequence.pull (evyBack trail))))
+ | EVY (trail, tac::tacs) st =
+ case Sequence.pull(tac st) of
+ None => evyBack trail (*failed: backtrack*)
+ | Some(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
+ and evyBack [] = Sequence.null (*no alternatives*)
+ | evyBack ((st',q,tacs)::trail) =
+ case Sequence.pull q of
+ None => evyBack trail
+ | Some(st,q') => if eq_thm (st',st)
+ then evyBack ((st',q',tacs)::trail)
+ else EVY ((st,q',tacs)::trail, tacs) st
+in
+
+(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *)
+fun EVERY tacs = EVY ([], tacs);
+end;
-(*** List-oriented tactics ***)
-
-(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *)
-fun EVERY tacs = foldr (op THEN) (tacs, all_tac);
-
(* EVERY' [tac1,...,tacn] i equals tac1 i THEN ... THEN tacn i *)
-fun EVERY' tacs = foldr (op THEN') (tacs, K all_tac);
+fun EVERY' tacs i = EVERY (map (fn f => f i) tacs);
(*Apply every tactic to 1*)
fun EVERY1 tacs = EVERY' tacs 1;
--- a/src/Pure/type.ML Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/type.ML Fri Feb 21 15:31:47 1997 +0100
@@ -758,7 +758,8 @@
let
val TySg {classes, subclass, default, tycons, arities, abbrs} = tsig;
val arities1 =
- flat (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
+ List.concat
+ (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
val arities2 = foldl (coregular (classes, subclass, tycons))
(arities, min_domain subclass arities1)
|> close subclass;