ocaml 3.09 transition

[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 d6293d2434ad61af36b7c94203a0cf7b6c8641c7..68dec37d6b04230f1468665e0a6f77516ccdb365 100644 (file)
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -23,9 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception ReferenceToVariable;;
-exception RferenceToCurrentProof;;
-exception ReferenceToInductiveDefinition;;
+exception ReferenceToNonVariable;;
 
 let prerr_endline _ = ();;
 
@@ -132,7 +130,11 @@ let fix_according_to_type ty hd tl =
   let rec aux n ty tl res =
     if n = 0 then
       (match tl with 
-         [] -> C.Appl res
+         [] ->
+          (match res with
+              [] -> assert false
+            | [res] -> res
+            | _ -> C.Appl res)
        | _ -> 
           match res with
             [] -> assert false
@@ -163,7 +165,7 @@ let fix_according_to_type ty hd tl =
   aux expected_arity ty tl [hd]
 ;;
 
-let eta_fix metasenv t =
+let eta_fix metasenv context t =
  let rec eta_fix' context t = 
   (* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); 
   flush stderr ; *)
@@ -172,16 +174,11 @@ let eta_fix metasenv t =
   match t with
      C.Rel n -> C.Rel n 
    | C.Var (uri,exp_named_subst) ->
-      let exp_named_subst' =
-       List.map
-        (function i,t -> i, (eta_fix' context t)) exp_named_subst
-      in
-      C.Var (uri,exp_named_subst')
+      let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
+       C.Var (uri,exp_named_subst')
    | C.Meta (n,l) ->
-      let (_,canonical_context,_) =
-       List.find (function (m,_,_) -> n = m) metasenv
-       in
-       let l' =
+      let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
+      let l' =
         List.map2
          (fun ct t ->
           match (ct, t) with
@@ -192,7 +189,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 
@@ -207,48 +204,47 @@ let eta_fix metasenv t =
        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 
+               CicUniv.empty_ugraph 
+           in
+              fix_according_to_type ty he tl
+(*
          C.Const(uri,exp_named_subst)::l'' ->
            let constant_type =
              (match CicEnvironment.get_obj uri with
                C.Constant (_,_,ty,_) -> ty
              | C.Variable _ -> raise ReferenceToVariable
-             | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof
+             | C.CurrentProof (_,_,_,_,params) -> raise ReferenceToCurrentProof
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-             )
-           in
-            fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
-        | _ -> 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
-        (function i,t -> i, (eta_fix' context t)) exp_named_subst
-       in
-       C.Const (uri,exp_named_subst')
+       let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
+        C.Const (uri,exp_named_subst')
    | C.MutInd (uri,tyno,exp_named_subst) ->
-       let exp_named_subst' =
-       List.map
-        (function i,t -> i, (eta_fix' context t)) exp_named_subst
-       in
+       let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
         C.MutInd (uri, tyno, exp_named_subst')
    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
-       let exp_named_subst' =
-       List.map
-        (function i,t -> i, (eta_fix' context t)) exp_named_subst
-       in
+       let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
         C.MutConstruct (uri, tyno, consno, exp_named_subst')
    | C.MutCase (uri, tyno, outty, term, patterns) as prima ->
        let outty' =  eta_fix' context outty in
        let term' = eta_fix' context term in
        let patterns' = List.map (eta_fix' context) patterns in
        let inductive_types,noparams =
-           (match CicEnvironment.get_obj uri with
+        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+           (match o with
                Cic.Constant _ -> assert false
              | Cic.Variable _ -> assert false
              | Cic.CurrentProof _ -> assert false
-             | Cic.InductiveDefinition (l,_,n) -> l,n 
+             | 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 
@@ -260,11 +256,21 @@ 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
+               CicUniv.empty_ugraph 
+            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
@@ -285,11 +291,21 @@ let eta_fix metasenv t =
         List.map
          (fun (name, ty, bo) ->
            (name, eta_fix' context ty, eta_fix' (fun_types@context) bo)) funs)
-   in
-   eta_fix' [] t
+  and fix_exp_named_subst context exp_named_subst =
+   List.rev
+    (List.fold_left
+      (fun newsubst (uri,t) ->
+        let t' = eta_fix' context t in
+        let ty =
+         let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+            match o with
+               Cic.Variable (_,_,ty,_,_) -> 
+                 CicSubstitution.subst_vars newsubst ty
+              | _ ->  raise ReferenceToNonVariable 
+       in
+        let t'' = fix_according_to_type ty t' [] in
+         (uri,t'')::newsubst
+      ) [] exp_named_subst)
+  in
+   eta_fix' context t
 ;;
-
-
-
-
-