From fcf9d69625a32a27c2a37e93ecd8de5bb9494c51 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 20 May 2009 20:44:49 +0000 Subject: [PATCH] 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 :) --- helm/software/components/acic_procedural/procedural2.ml | 9 ++++++--- .../components/acic_procedural/proceduralOptimizer.ml | 9 +++++++-- 2 files changed, 13 insertions(+), 5 deletions(-) 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 = -- 2.39.2