discontinued continuations to simplify control flow; dropped optimization in scnp

--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Tue Oct 05 14:19:38 2010 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Tue Oct 05 14:19:40 2010 +0200
@@ -343,7 +343,7 @@
   end)
 end
 
-fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+fun single_scnp_tac use_tags orders ctxt D = Termination.CALLS (fn (cs, i) =>
   let
     val ms_configured = is_some (Multiset_Setup.get (ProofContext.theory_of ctxt))
     val orders' = if ms_configured then orders
@@ -352,56 +352,40 @@
     val certificate = generate_certificate use_tags orders' gp
   in
     case certificate
-     of NONE => err_cont D i
+     of NONE => no_tac
       | SOME cert =>
           SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
-          THEN (rtac @{thm wf_empty} i ORELSE cont D i)
+          THEN TRY (rtac @{thm wf_empty} i)
   end)
 
-fun gen_decomp_scnp_tac orders autom_tac ctxt err_cont =
-  let
-    open Termination
-    val derive_diag = Termination.derive_diag ctxt autom_tac
-    val derive_all = Termination.derive_all ctxt autom_tac
-    val decompose = Termination.decompose_tac ctxt autom_tac
-    val scnp_no_tags = single_scnp_tac false orders ctxt
-    val scnp_full = single_scnp_tac true orders ctxt
-
-    fun first_round c e =
-        derive_diag (REPEAT scnp_no_tags c e)
-
-    val second_round =
-        REPEAT (fn c => fn e => decompose (scnp_no_tags c c) e)
+local open Termination in
 
-    val third_round =
-        derive_all oo
-        REPEAT (fn c => fn e =>
-          scnp_full (decompose c c) e)
-
-    fun Then s1 s2 c e = s1 (s2 c c) (s2 c e)
+fun gen_decomp_scnp_tac orders autom_tac ctxt =
+TERMINATION ctxt autom_tac (fn D => 
+  let
+    val decompose = decompose_tac D
+    val scnp_full = single_scnp_tac true orders ctxt D
+  in
+    REPEAT_ALL_NEW (scnp_full ORELSE' decompose)
+  end)
+end
 
-    val strategy = Then (Then first_round second_round) third_round
-
-  in
-    TERMINATION ctxt autom_tac (strategy err_cont err_cont)
-  end
-
-fun gen_sizechange_tac orders autom_tac ctxt err_cont =
+fun gen_sizechange_tac orders autom_tac ctxt =
   TRY (Function_Common.apply_termination_rule ctxt 1)
   THEN TRY (Termination.wf_union_tac ctxt)
   THEN
    (rtac @{thm wf_empty} 1
-    ORELSE gen_decomp_scnp_tac orders autom_tac ctxt err_cont 1)
+    ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
 
 fun sizechange_tac ctxt autom_tac =
-  gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt (K (K all_tac))
+  gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt
 
 fun decomp_scnp_tac orders ctxt =
   let
     val extra_simps = Function_Common.Termination_Simps.get ctxt
     val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps)
   in
-     gen_sizechange_tac orders autom_tac ctxt (print_error ctxt)
+     gen_sizechange_tac orders autom_tac ctxt
   end
 
 

--- a/src/HOL/Tools/Function/termination.ML	Tue Oct 05 14:19:38 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Tue Oct 05 14:19:40 2010 +0200
@@ -9,7 +9,7 @@
 sig
 
   type data
-  datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm
+  datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm
 
   val mk_sumcases : data -> typ -> term list -> term
 
@@ -17,7 +17,6 @@
   val get_types      : data -> int -> typ
   val get_measures   : data -> int -> term list
 
-  (* read from cache *)
   val get_chain      : data -> term -> term -> thm option option
   val get_descent    : data -> term -> term -> term -> cell option
 
@@ -25,23 +24,14 @@
 
   val CALLS : (term list * int -> tactic) -> int -> tactic
 
-  (* Termination tactics. Sequential composition via continuations. (2nd argument is the error continuation) *)
-  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+  (* Termination tactics *)
+  type ttac = data -> int -> tactic
 
-  val TERMINATION : Proof.context -> tactic -> (data -> int -> tactic) -> int -> tactic
-
-  val REPEAT : ttac -> ttac
+  val TERMINATION : Proof.context -> tactic -> ttac -> int -> tactic
 
   val wf_union_tac : Proof.context -> tactic
 
-  val decompose_tac : Proof.context -> tactic -> ttac
-
-  val derive_diag : Proof.context -> tactic -> 
-    (data -> int -> tactic) -> data -> int -> tactic
-
-  val derive_all  : Proof.context -> tactic ->
-    (data -> int -> tactic) -> data -> int -> tactic
-
+  val decompose_tac : ttac
 end
 
 
@@ -119,7 +109,7 @@
 
 (** Matrix cell datatype **)
 
-datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
+datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm;
 
 
 type data =
@@ -130,12 +120,6 @@
   * (term * (term * term) -> cell)(* local descents (cached) *)
 
 
-fun map_chains f (p, T, M, C, D) = (p, T, M, f C, D)
-fun map_descent f (p, T, M, C, D) = (p, T, M, C, f D)
-
-fun note_chain c1 c2 res D = D     (*disabled*)
-fun note_descent c m1 m2 res D = D
-
 (* Build case expression *)
 fun mk_sumcases (sk, _, _, _, _) T fs =
   mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
@@ -241,15 +225,13 @@
 fun get_descent (_, _, _, _, D) c m1 m2 =
   SOME (D (c, (m1, m2)))
 
-fun derive_descent thy tac c m1 m2 D = D (* disabled *)
-
 fun CALLS tac i st =
   if Thm.no_prems st then all_tac st
   else case Thm.term_of (Thm.cprem_of st i) of
     (_ $ (_ $ rel)) => tac (Function_Lib.dest_binop_list @{const_name Lattices.sup} rel, i) st
   |_ => no_tac st
 
-type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+type ttac = data -> int -> tactic
 
 fun TERMINATION ctxt atac tac =
   SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
@@ -326,25 +308,9 @@
 end
 
 
-(* continuation passing repeat combinator *)
-fun REPEAT ttac cont err_cont =
-    ttac (fn D => fn i => (REPEAT ttac cont cont D i)) err_cont
 
 (*** DEPENDENCY GRAPHS ***)
 
-fun derive_chains ctxt chain_tac cont = cont
-(* fn D => CALLS (fn (cs, i) =>
-  let
-    val thy = ProofContext.theory_of ctxt
-
-    fun derive_chain c1 c2 D =
-      if is_some (get_chain D c1 c2) then D else
-      note_chain c1 c2 (prove_chain thy chain_tac c1 c2) D
-  in
-    cont (fold_product derive_chain cs cs D) i
-  end)
-*)
-
 fun mk_dgraph D cs =
   Term_Graph.empty
   |> fold (fn c => Term_Graph.new_node (c, ())) cs
@@ -374,53 +340,23 @@
    | _ => no_tac)
   | _ => no_tac)
 
-fun decompose_tac' cont err_cont D = CALLS (fn (cs, i) =>
+fun decompose_tac D = CALLS (fn (cs, i) =>
   let
     val G = mk_dgraph D cs
     val sccs = Term_Graph.strong_conn G
 
-    fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
+    fun split [SCC] i = TRY (solve_trivial_tac D i)
       | split (SCC::rest) i =
         regroup_calls_tac SCC i
         THEN rtac @{thm wf_union_compatible} i
         THEN rtac @{thm less_by_empty} (i + 2)
         THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
         THEN split rest (i + 1)
-        THEN (solve_trivial_tac D i ORELSE cont D i)
+        THEN TRY (solve_trivial_tac D i)
   in
     if length sccs > 1 then split sccs i
-    else solve_trivial_tac D i ORELSE err_cont D i
+    else solve_trivial_tac D i
   end)
 
-fun decompose_tac ctxt chain_tac cont err_cont =
-  derive_chains ctxt chain_tac (decompose_tac' cont err_cont)
-
-
-(*** Local Descent Proofs ***)
-
-fun gen_descent diag ctxt tac cont = cont
-(*
-  fn D => CALLS (fn (cs, i) =>
-  let
-    val thy = ProofContext.theory_of ctxt
-    val measures_of = get_measures D
-
-    fun derive c D =
-      let
-        val (_, p, _, q, _, _) = dest_call D c
-      in
-        if diag andalso p = q
-        then fold (fn m => derive_descent thy tac c m m) (measures_of p) D
-        else fold_product (derive_descent thy tac c)
-               (measures_of p) (measures_of q) D
-      end
-  in
-    cont (Function_Common.PROFILE "deriving descents" (fold derive cs) D) i
-  end)
-*)
-
-fun derive_diag ctxt = gen_descent true ctxt
-fun derive_all ctxt = gen_descent false ctxt
-
 
 end