X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=9b20729103b37a0061d4f54a5b72cf4c9456b85a;hb=68d0e8729398bdb485670ed6d0e247af64d934fc;hp=876c5c6783190d7da4829bec4d8bb848dddcf038;hpb=059db27238ba60f5c6bdf229bdb2265fa194a280;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 876c5c678..9b2072910 100644
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -27,6 +27,8 @@ exception ReferenceToVariable;;
 exception RferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
+let prerr_endline _ = ();;
+
 (* 
 let rec fix_lambdas_wrt_type ty te =
  let module C = Cic in
@@ -163,8 +165,8 @@ let fix_according_to_type ty hd tl =
 
 let eta_fix metasenv t =
  let rec eta_fix' context t = 
-  prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); 
-  flush stderr ; 
+  (* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); 
+  flush stderr ; *)
   let module C = Cic in
   let module S = CicSubstitution in
   match t with
@@ -190,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 
@@ -200,11 +202,16 @@ let eta_fix metasenv t =
         (n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t)
    | C.LetIn (n,s,t) -> 
        C.LetIn 
-        (n, eta_fix' context s, eta_fix' ((Some (n,(C.Def s)))::context) t)
+        (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
    | C.Appl l as appl -> 
        let l' =  List.map (eta_fix' context) l 
        in 
        (match l' with
+           [] -> assert false
+         | he::tl ->
+            let ty = CicTypeChecker.type_of_aux' metasenv context he in
+             fix_according_to_type ty he tl
+(*
          C.Const(uri,exp_named_subst)::l'' ->
            let constant_type =
              (match CicEnvironment.get_obj uri with
@@ -212,14 +219,10 @@ let eta_fix metasenv t =
              | C.Variable _ -> raise ReferenceToVariable
              | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-             )
-           in
-           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' )
+             ) in 
+           fix_according_to_type 
+             constant_type (C.Const(uri,exp_named_subst)) l''
+        | _ -> C.Appl l' *))
    | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
        List.map
@@ -250,7 +253,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 
@@ -262,21 +264,25 @@ let eta_fix metasenv t =
           if noparams = 0 then 
             List.map (fun (_,t) -> t) constructors 
           else 
-	    let term_type = 
-              CicTypeChecker.type_of_aux' metasenv context term in
+	         let term_type = 
+            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
            constructor_types patterns in 
-       let dopo = 
-         C.MutCase (uri, tyno, outty',term',patterns2) in
-       if not (CicReduction.are_convertible [] prima dopo) then 
-             (prerr_endline ("prima :" ^(CicPp.ppterm prima)); 
-              prerr_endline ("dopo :" ^(CicPp.ppterm dopo)));
-           dopo
+         C.MutCase (uri, tyno, outty',term',patterns2)
    | C.Fix (funno, funs) ->
        let fun_types = 
          List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) funs in
@@ -300,3 +306,9 @@ let eta_fix metasenv t =
 
 
 
+
+
+
+
+
+