split into two major parts:

[helm.git] / helm / ocaml / cic_omdoc / eta_fixing.ml

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 4a529a2bc54c536e873075d0715e209ba082aabc..24242b42675f34f4f4cdefaca68cdaa1a2f4a5d4 100644 (file)
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -192,7 +192,7 @@ let eta_fix metasenv t =
        in
        C.Meta (n,l')
    | C.Sort s -> C.Sort s
-   | C.Implicit -> C.Implicit
+   | C.Implicit _ as t -> t
    | C.Cast (v,t) -> C.Cast (eta_fix' context v, eta_fix' context t)
    | C.Prod (n,s,t) -> 
        C.Prod 
@@ -214,9 +214,15 @@ let eta_fix metasenv t =
              | C.Variable _ -> raise ReferenceToVariable
              | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-             )
-           in
-            fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
+             ) in 
+           fix_according_to_type 
+             constant_type (C.Const(uri,exp_named_subst)) l''
+(*
+           let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in
+           if not (CicReduction.are_convertible [] appl result) then 
+             (prerr_endline ("prima :" ^(CicPp.ppterm appl)); 
+              prerr_endline ("dopo :" ^(CicPp.ppterm result)));
+           result *)
         | _ -> C.Appl l' )
    | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
@@ -248,7 +254,6 @@ let eta_fix metasenv t =
              | Cic.InductiveDefinition (l,_,n) -> l,n 
            ) in
        let (_,_,_,constructors) = List.nth inductive_types tyno in
-        prerr_endline ("QUI"); 
        let constructor_types = 
          let rec clean_up t =
            function 
@@ -261,11 +266,19 @@ let eta_fix metasenv t =
             List.map (fun (_,t) -> t) constructors 
           else 
                 let term_type = 
-            TypeInference.type_of_aux' metasenv context term
+            CicTypeChecker.type_of_aux' metasenv context term
            in
             (match term_type with
                C.Appl (hd::params) -> 
-                 List.map (fun (_,t) -> clean_up t params) constructors
+                 let rec first_n n l =
+                   if n = 0 then []
+                   else 
+                     (match l with
+                        a::tl -> a::(first_n (n-1) tl)
+                     | _ -> assert false) in 
+                 List.map 
+                  (fun (_,t) -> 
+                     clean_up t (first_n noparams params)) constructors
              | _ -> prerr_endline ("QUA"); assert false) in 
        let patterns2 = 
          List.map2 fix_lambdas_wrt_type
@@ -294,3 +307,9 @@ let eta_fix metasenv t =
 
 
 
+
+
+
+
+
+