X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=8407f8357e04d3f7f8603759cbeb7432060d58b3;hb=6248703e9f479d4c3edfcf227908ffd9d2dd7adc;hp=c3b84b60599cd280f68b6a154e72825fb3d09257;hpb=264523336352a5241b747b7e04b33630f6010aeb;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index c3b84b605..8407f8357 100644
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -27,83 +27,138 @@ exception ReferenceToVariable;;
 exception RferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
+(* 
 let rec fix_lambdas_wrt_type ty te =
  let module C = Cic in
  let module S = CicSubstitution in
-(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); 
-   flush stderr ; *)
-   (* cast e altra porcheria ???? *)
+(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
+   match ty with
+     C.Prod (_,_,ty') ->
+       (match CicReduction.whd [] te with
+          C.Lambda (n,s,te') ->
+            C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
+        | t ->
+            let rec get_sources =
+              function 
+                C.Prod (_,s,ty) -> s::(get_sources ty)
+              | _ -> [] in
+            let sources = get_sources ty in
+            let no_sources = List.length sources in
+            let rec mk_rels n shift =
+              if n = 0 then []
+            else (C.Rel (n + shift))::(mk_rels (n - 1) shift) in
+            let t' = S.lift no_sources t in
+            let t2 = 
+              match t' with
+                C.Appl l -> 
+                  C.LetIn 
+                     (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
+              | _ -> 
+                  C.Appl (t'::(mk_rels no_sources 0)) in
+                   List.fold_right
+                     (fun source t -> C.Lambda (C.Name "y",source,t)) 
+                      sources t2)
+   | _ -> te
+;; *)
+
+let rec fix_lambdas_wrt_type ty te =
+ let module C = Cic in
+ let module S = CicSubstitution in
+(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
+   match ty,te with
+     C.Prod (_,_,ty'), C.Lambda (n,s,te') ->
+       C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
+   | C.Prod (_,s,ty'), t -> 
+      let rec get_sources =
+        function 
+            C.Prod (_,s,ty) -> s::(get_sources ty)
+          | _ -> [] in
+      let sources = get_sources ty in
+      let no_sources = List.length sources in
+      let rec mk_rels n shift =
+        if n = 0 then []
+        else (C.Rel (n + shift))::(mk_rels (n - 1) shift) in
+      let t' = S.lift no_sources t in
+      let t2 = 
+         match t' with
+           C.Appl l -> 
+             C.LetIn (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
+         | _ -> C.Appl (t'::(mk_rels no_sources 0)) in
+      List.fold_right
+        (fun source t -> C.Lambda (C.Name "y",CicReduction.whd [] source,t)) sources t2
+   | _, _ -> te
+;;
+
+(*
+let rec fix_lambdas_wrt_type ty te =
+ let module C = Cic in
+ let module S = CicSubstitution in
+(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
    match ty,te with
      C.Prod (_,_,ty'), C.Lambda (n,s,te') ->
        C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
+   | C.Prod (_,s,ty'), ((C.Appl (C.Const _ ::_)) as t) -> 
+      (* const have a fixed arity *)
+      (* prerr_endline ("******** fl - eta expansion 0: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
+       let t' = S.lift 1 t in
+       C.Lambda (C.Name "x",s,
+         C.LetIn 
+          (C.Name "H", fix_lambdas_wrt_type ty' t', 
+            C.Appl [C.Rel 1;C.Rel 2])) 
    | C.Prod (_,s,ty'), C.Appl l ->
-       prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); 
-       flush stderr ;
+       (* prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
        let l' = List.map (S.lift 1) l in
         C.Lambda (C.Name "x",s,
          fix_lambdas_wrt_type ty' (C.Appl (l'@[C.Rel 1])))
    | C.Prod (_,s,ty'), _ ->
-       prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); 
+       (* prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
        flush stderr ;
        let te' = S.lift 1 te in
         C.Lambda (C.Name "x",s,
           fix_lambdas_wrt_type ty' (C.Appl [te';C.Rel 1]))
    | _, _ -> te
-;;
+;;*) 
 
 let fix_according_to_type ty hd tl =
  let module C = Cic in
  let module S = CicSubstitution in
-  let rec aux ty tl res =
-   (* prerr_endline ("entering aux_1 with type=" ^ CicPp.ppterm ty); 
-   flush stderr ; *)
-   match ty with
-      C.Rel _
-    | C.Var _
-    | C.Meta _ 
-    | C.Sort _ 
-    | C.Implicit -> 
+   let rec count_prods =
+     function
+       C.Prod (_,_,t) -> 1 + (count_prods t)
+       | _ -> 0 in
+  let expected_arity = count_prods ty in
+  let rec aux n ty tl res =
+    if n = 0 then
       (match tl with 
          [] -> C.Appl res
-       |  _ ->
-         prerr_endline ("******* fat - too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); 
-         flush stderr ;
-         C.LetIn 
-          (C.Name "H", C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
-    | C.Cast (v,t) -> aux v tl res
-    | C.Prod (n,s,t) -> 
-       (match tl with 
-          [] ->
-            prerr_endline ("******* fat - eta expansion: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); 
-         flush stderr ;
-           let res' = List.map (S.lift 1) res 
-           in 
+       | _ -> 
+          match res with
+            [] -> assert false
+          | [a] -> C.Appl (a::tl)
+          | _ ->
+              (* prerr_endline ("******* too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
+              C.LetIn 
+                (C.Name "H", 
+                  C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
+    else 
+      let name,source,target =
+        (match ty with
+           C.Prod (C.Name _ as n,s,t) -> n,s,t
+         | C.Prod (C.Anonymous, s,t) -> C.Name "z",s,t
+         | _ -> (* prods number may only increase for substitution *) 
+           assert false) in
+      match tl with 
+         [] ->
+           (* prerr_endline ("******* too few args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
+           let res' = List.map (S.lift 1) res in 
            C.Lambda 
-            (C.Name "x", (* Andrea: to do: generate a fresh name *)
-             s, 
-             aux t [] (res'@[C.Rel 1]))
+            (name, source, aux (n-1) target [] (res'@[C.Rel 1]))
         | hd::tl' -> 
-           let hd' = fix_lambdas_wrt_type s hd
-           in
-            aux (S.subst hd' t) tl' (res@[hd']))
-    | C.Lambda _ -> assert false
-    | C.LetIn (n,s,t) -> aux (S.subst s t) tl res
-    | C.Appl _
-    | C.Const _
-    | C.MutInd _ 
-    | C.MutConstruct _
-    | C.MutCase _
-    | C.Fix _
-    | C.CoFix _ -> (* ???? *)
-       (match tl with 
-         [] -> C.Appl res
-       |  _ -> (* Andrea: to do: generate a fresh name *)
-         C.LetIn 
-          (C.Name "H",
-           C.Appl res, 
-           C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
-  in
-  aux ty tl [hd]
+           let hd' = fix_lambdas_wrt_type source hd in
+            (*  (prerr_endline ("++++++prima :" ^(CicPp.ppterm hd)); 
+              prerr_endline ("++++++dopo :" ^(CicPp.ppterm hd'))); *)
+           aux (n-1) (S.subst hd' target) tl' (res@[hd']) in
+  aux expected_arity ty tl [hd]
 ;;
 
 let eta_fix metasenv t =
@@ -139,7 +194,7 @@ let eta_fix metasenv t =
    | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t)
    | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t)
    | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t)
-   | C.Appl l -> 
+   | C.Appl l as appl -> 
        let l' =  List.map eta_fix' l 
        in 
        (match l' with
@@ -152,7 +207,11 @@ let eta_fix metasenv t =
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
              )
            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' =
@@ -189,3 +248,5 @@ let eta_fix metasenv t =
    eta_fix' t
 ;;
 
+
+