we catch the refiner errors in the critical step and fall back to the non-criticall...

bug-fix in elimination recognition euristics

now nat/orders.ma and nat/times.ma are fully reconstructed :)

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index e41dd101b896b8f64bea8fbae0a22d6331d15c84..e736842b71ac8183dd8fa70caf6b1fc55bf8b39c 100644 (file)
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -340,7 +340,10 @@ and proc_appl st what hd tl =
       let parsno, argsno = List.length classes, List.length tl in
       let decurry = parsno - argsno in
       let diff = goal_arity - decurry in
-      if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (H.cic hd)));
+      if diff < 0 then 
+         let text = Printf.sprintf "partial application: %i" diff in
+        [T.Exact (what, dtext ^ text)]
+      else
       let classes = Cl.adjust st.context tl ?goal classes in
       let rec mk_synth a n =
          if n < 0 then a else mk_synth (I.S.add n a) (pred n)
@@ -350,7 +353,7 @@ and proc_appl st what hd tl =
       let script = List.rev (mk_arg st hd) in
       let tactic b t n = if b then T.Apply (t, n) else T.Exact (t, n) in
       match rc with
-         | Some (i, j, uri, tyno) ->
+         | Some (i, j, uri, tyno) when decurry = 0 ->
            let classes2, tl2, _, where = split2_last classes tl in
            let script2 = List.rev (mk_arg st where) @ script in
            let synth2 = I.S.add 1 synth in
@@ -370,7 +373,7 @@ and proc_appl st what hd tl =
               let using = Some hd in
               script2 @ 
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
-        | None        ->
+        | _                                       ->
            let names = get_sub_names hd tl in
            let qs = proc_bkd_proofs (next st) synth names classes tl in
            let b, hd = mk_exp_args hd tl classes synth in

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index a397de41e8fa3b8b82b930968a1ef1251d45baec..8a7e5bea5047cd0e3bcdddc9b9d50e130834751d 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -211,8 +211,13 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases =
    in
    let lifted_cases = List.map2 map2 cases constructors in
    let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
-   let x = H.refine c (C.Appl args) in
-   opt_proof g (info st "Optimizer: remove 3") es c x
+   try 
+      let x = H.refine c (C.Appl args) in
+      opt_proof g (info st "Optimizer: remove 3") es c x        
+   with e ->
+(* FG: the transformation is not possible, we fall back into the plain case *)
+      let st = info st ("Optimizer: refine_error: " ^ Printexc.to_string e) in
+      opt_mutcase_plain g st es c uri tyno outty arg cases
 
 and opt_mutcase_plain g st es c uri tyno outty arg cases =
    let g st v =