Procedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation

[helm.git] / components / acic_procedural / acic2Procedural.ml

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 9a5662a1dc985c23a4ad6cf3a7053e42ecd97fa1..e3545f62a7c0f3e4b831f9e0141ef1a9052d8ae9 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -154,6 +154,12 @@ try
    with Not_found -> `Type (CicUniv.fresh())
 with Invalid_argument _ -> failwith "A2P.get_sort"
 
+let get_type msg st bo =
+try   
+   let ty, _ = TC.type_of_aux' [] st.context (cic bo) Un.empty_ugraph in
+   ty
+with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
+
 (* proof construction *******************************************************)
 
 let unused_premise = "UNUSED"
@@ -178,7 +184,7 @@ let eta_expand n t =
    let ty = C.AImplicit ("", None) in
    let name i = Printf.sprintf "%s%u" expanded_premise i in 
    let lambda i t = C.ALambda (id, C.Name (name i), ty, t) in
-   let arg i n = T.mk_arel (n - i) (name (n - i - 1)) in
+   let arg i n = T.mk_arel ((* n - *) succ i) (name (n - i - 1)) in
    let rec aux i f a =
       if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
    in
@@ -246,7 +252,7 @@ and mk_fwd_proof st dtext name = function
    | C.AAppl (_, hd :: tl) as v                         -> 
       if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else
       if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else
-      let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
+      let ty = get_type "TC1" st hd in
       begin match get_inner_types st v with
          | Some (ity, _) when M.bkd st.context ty ->
            let qs = [[T.Id ""]; mk_proof (next st) v] in
@@ -299,11 +305,14 @@ and mk_proof st = function
    | C.AAppl (_, hd :: tl) as t                    ->
       let proceed, dtext = test_depth st in
       let script = if proceed then
-         let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
+         let ty = get_type "TC2" st hd in
          let (classes, rc) as h = Cl.classify st.context ty in
          let premises, _ = P.split st.context ty in
         let decurry = List.length classes - List.length tl in
-         if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
+         if decurry <> 0 then
+           Printf.eprintf "DECURRY: %u %s\n" decurry (CicPp.ppterm (cic t));
+        assert (decurry = 0);
+        if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
          if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
         let synth = I.S.singleton 0 in
          let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
@@ -330,7 +339,7 @@ and mk_proof st = function
          [T.Apply (t, dtext)]
       in
       mk_intros st script
-   | C.AMutCase (id, uri, tyno, outty, arg, cases) ->
+   | C.AMutCase (id, uri, tyno, outty, arg, cases) as t ->
       begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
          | _ (* None *)  -> 
             let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in