From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 20 May 2009 20:44:49 +0000 (+0000)
Subject: we catch the refiner errors in the critical step and fall back to the non-criticall... 
X-Git-Tag: make_still_working~3954
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fcf9d69625a32a27c2a37e93ecd8de5bb9494c51;p=helm.git

we catch the refiner errors in the critical step and fall back to the non-criticall version (this is just for debugging)
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 e41dd101b..e736842b7 100644
--- 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 a397de41e..8a7e5bea5 100644
--- 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 =