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

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

diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml
index 3df6802ffa7f84b47f65d33b4bc36e30809447ef..d2d305ed4cffc959e107a274479389d42cfb8f64 100644 (file)
--- a/components/acic_procedural/proceduralConversion.ml
+++ b/components/acic_procedural/proceduralConversion.ml
@@ -29,6 +29,7 @@ module Un   = CicUniv
 module TC   = CicTypeChecker 
 module D    = Deannotate
 module UM   = UriManager
+module Rd   = CicReduction
 
 module P    = ProceduralPreprocess
 module T    = ProceduralTypes
@@ -63,7 +64,6 @@ let rec list_sub start length = function
    | hd :: tl when length > 0 -> hd :: list_sub start (pred length) tl
    | _                        -> []
     
-
 (* proof construction *******************************************************)
 
 let lift k n =
@@ -140,12 +140,15 @@ let fake_annotate c =
 
 let clear_absts m =
    let rec aux k n = function
+      | C.AImplicit (_, None) as t         -> t
       | C.ALambda (id, s, v, t) when k > 0 -> 
          C.ALambda (id, s, v, aux (pred k) n t)
-      | C.ALambda (_, _, _, t) when n > 0 -> 
+      | C.ALambda (_, _, _, t) when n > 0  -> 
          aux 0 (pred n) (lift 1 (-1) t)
-      | t                      when n > 0 -> assert false
-      | t                                 -> t
+      | t                      when n > 0  ->
+           Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (cic t));
+           assert false 
+      | t                                  -> t
    in 
    aux m
 
@@ -158,7 +161,7 @@ try
    in
    let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in
    let inty, _ = TC.type_of_aux' [] context (cic arg) Un.empty_ugraph in
-   let ps = match inty with
+   let ps = match Rd.whd ~delta:true context inty with
       | C.MutInd _                  -> []
       | C.Appl (C.MutInd _ :: args) -> List.map (fake_annotate context) args
       | _                           -> assert false
@@ -212,7 +215,7 @@ let generalize n =
       | C.AMutConstruct (id, _, _, _, _)
       | C.AMeta (id, _, _) -> meta id
       | C.ARel (id, _, m, _) -> 
-         if m = succ (n - k) then hole id else meta id
+         if m = succ (k - n) then hole id else meta id
       | C.AAppl (id, ts) -> 
          let ts = List.map (gen_term k) ts in
          if is_meta ts then meta id else C.AAppl (id, ts)