some improvements

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index e91c4bdfc1b9c8f24bb94c9ed83d9fef15dc418b..9a5662a1dc985c23a4ad6cf3a7053e42ecd97fa1 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -218,8 +218,8 @@ let rec mk_atomic st dtext what =
       let script = convert st ~name what in  
       script @ mk_fwd_proof st dtext name what, T.mk_arel 0 name
 
-and mk_fwd_rewrite st dtext name tl direction =
-try   
+and mk_fwd_rewrite st dtext name tl direction =   
+   assert (List.length tl = 6);
    let what, where = List.nth tl 5, List.nth tl 3 in
    let rps, predicate = [List.nth tl 4], List.nth tl 2 in
    let e = Cn.mk_pattern rps predicate in
@@ -228,7 +228,13 @@ try
          let script, what = mk_atomic st dtext what in
          T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script
       | _                         -> assert false
-with e -> failwith ("mk_fwd_rewrite: " ^ Printexc.to_string e)
+
+and mk_rewrite st dtext script t what qs tl direction = 
+   assert (List.length tl = 5);
+   let rps, predicate = [List.nth tl 4], List.nth tl 2 in
+   let e = Cn.mk_pattern rps predicate in
+   List.rev script @ convert st t @
+   [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
 
 and mk_fwd_proof st dtext name = function
    | C.ALetIn (_, n, v, t)                           ->
@@ -265,9 +271,7 @@ and mk_fwd_proof st dtext name = function
          | _             ->
             [T.LetIn (name, v, dtext)]
 
-and mk_proof st t = 
-try   
-   match t with
+and mk_proof st = function
    | C.ALambda (_, name, v, t)                     ->
       let entry = Some (name, C.Decl (cic v)) in
       let intro = get_intro name t in
@@ -310,15 +314,9 @@ try
               let synth = I.S.add 1 synth in
               let qs = mk_bkd_proofs (next st) synth classes tl in
                if is_rewrite_right hd then 
-                  let rps, predicate = [List.nth tl 4], List.nth tl 2 in
-                  let e = Cn.mk_pattern rps predicate in
-                 List.rev script @ convert st t @
-                 [T.Rewrite (false, what, None, e, dtext); T.Branch (qs, "")]
+                 mk_rewrite st dtext script t what qs tl false
               else if is_rewrite_left hd then 
-                 let rps, predicate = [List.nth tl 4], List.nth tl 2 in
-                  let e = Cn.mk_pattern rps predicate in
-                 List.rev script @ convert st t @
-                 [T.Rewrite (true, what, None, e, dtext); T.Branch (qs, "")]
+                 mk_rewrite st dtext script t what qs tl true
               else   
                  let using = Some hd in
                  List.rev script @ convert st t @
@@ -346,7 +344,6 @@ try
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
       let script = [T.Note text] in
       mk_intros st script
-with e -> failwith ("mk_proof: " ^ Printexc.to_string e)
 
 and mk_bkd_proofs st synth classes ts =
 try 

diff --git a/components/acic_procedural/proceduralPreprocess.ml b/components/acic_procedural/proceduralPreprocess.ml
index 4862db759178c25e7d66bd8524854079738c26e7..8030c403bfcf2ab40905896f56a1bc6f6f503671 100644 (file)
--- a/components/acic_procedural/proceduralPreprocess.ml
+++ b/components/acic_procedural/proceduralPreprocess.ml
@@ -99,7 +99,7 @@ let eta_fix c t proof decurry =
    if proof && decurry > 0 then eta_expand (get_tys c decurry t) t else t
 
 let rec pp_cast g ht es c t v =
-   if es then pp_proof g ht es c t else find g ht t
+   if true then pp_proof g ht es c t else find g ht t
 
 and pp_lambda g ht es c name v t =
    let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
@@ -107,7 +107,7 @@ and pp_lambda g ht es c name v t =
    let g t _ decurry = 
       let t = eta_fix (entry :: c) t true decurry in
       g (C.Lambda (name, v, t)) true 0 in
-   if es then pp_proof g ht es (entry :: c) t else find g ht t
+   if true then pp_proof g ht es (entry :: c) t else find g ht t
 
 and pp_letin g ht es c name v t =
    let entry = Some (name, C.Def (v, None)) in
@@ -119,11 +119,12 @@ and pp_letin g ht es c name v t =
            pp_proof g ht false c x 
          | v                               -> 
             let v = eta_fix c v proof d in
+(*         let t = eta_fix (entry :: c) t true decurry in *)
            g (C.LetIn (name, v, t)) true decurry
       in
-      if es then pp_term g ht es c v else find g ht v
+      if true then pp_term g ht es c v else find g ht v
    in
-   if es then pp_proof g ht es (entry :: c) t else find g ht t
+   if true then pp_proof g ht es (entry :: c) t else find g ht t
 
 and pp_appl_one g ht es c t v =
    let g t _ decurry =
@@ -147,9 +148,9 @@ and pp_appl_one g ht es c t v =
               let v = eta_fix c v proof d in
                g (C.Appl [t; v]) true (pred premsno)
       in
-      if es then pp_term g ht es c v else find g ht v
+      if true then pp_term g ht es c v else find g ht v
    in
-   if es then pp_proof g ht es c t else find g ht t
+   if true then pp_proof g ht es c t else find g ht t
 
 and pp_appl g ht es c t = function
    | []             -> pp_proof g ht es c t
@@ -159,7 +160,7 @@ and pp_appl g ht es c t = function
       pp_proof g ht es c x
 
 and pp_proof g ht es c t = 
-   let g t proof decurry = add g ht t proof decurry in
+(*   let g t proof decurry = add g ht t proof decurry in *)
    match t with
       | C.Cast (t, v)         -> pp_cast g ht es c t v
       | C.Lambda (name, v, t) -> pp_lambda g ht es c name v t