Never commit before trying to compile... stupid typo fixed.

[helm.git] / helm / software / components / cic_acic / doubleTypeInference.ml

diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index 905d1e6bc0be63568a8998ac6936f48cb59d2a78..6fa7cce5ad03827939c836564b5b037da4646eb6 100644 (file)
--- a/helm/software/components/cic_acic/doubleTypeInference.ml
+++ b/helm/software/components/cic_acic/doubleTypeInference.ml
@@ -37,7 +37,7 @@ exception RelToHiddenHypothesis;;
 
 let xxx_type_of_aux' m c t =
  try 
-   Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph))
+   Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph))
  with
  | CicTypeChecker.TypeCheckerFailure _ -> None (* because eta_expansion *)
 ;;
@@ -64,9 +64,10 @@ let rec does_not_occur n =
    | C.Lambda (name,so,dest) ->
       does_not_occur n so &&
        does_not_occur (n + 1) dest
-   | C.LetIn (name,so,dest) ->
+   | C.LetIn (name,so,ty,dest) ->
       does_not_occur n so &&
-       does_not_occur (n + 1) dest
+       does_not_occur n ty &&
+        does_not_occur (n + 1) dest
    | C.Appl l ->
       List.fold_right (fun x i -> i && does_not_occur n x) l true
    | C.Var (_,exp_named_subst)
@@ -119,8 +120,8 @@ let rec beta_reduce =
        C.Prod (n, beta_reduce s, beta_reduce t)
     | C.Lambda (n,s,t) ->
        C.Lambda (n, beta_reduce s, beta_reduce t)
-    | C.LetIn (n,s,t) ->
-       C.LetIn (n, beta_reduce s, beta_reduce t)
+    | C.LetIn (n,s,ty,t) ->
+       C.LetIn (n, beta_reduce s, beta_reduce ty, beta_reduce t)
     | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
        let he' = S.subst he t in
         if tl = [] then
@@ -179,9 +180,9 @@ let type_of_constant uri =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+   match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,_) ->
        raise (NotWellTyped "Reference to an unchecked constant")
   in
    match cobj with
@@ -194,9 +195,9 @@ let type_of_variable uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+  match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
      CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
-   | CicEnvironment.UncheckedObj (C.Variable _) ->
+   | CicEnvironment.UncheckedObj (C.Variable _,_) ->
       raise (NotWellTyped "Reference to an unchecked variable")
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 ;;
@@ -206,9 +207,9 @@ let type_of_mutual_inductive_defs uri i =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+   match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,_) ->
        raise (NotWellTyped "Reference to an unchecked inductive type")
   in
    match cobj with
@@ -223,9 +224,9 @@ let type_of_mutual_inductive_constr uri i j =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+   match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
-    | CicEnvironment.UncheckedObj uobj ->
+    | CicEnvironment.UncheckedObj (uobj,_) ->
        raise (NotWellTyped "Reference to an unchecked constructor")
   in
    match cobj with
@@ -271,10 +272,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         (try
           match List.nth context (n - 1) with
              Some (_,C.Decl t) -> S.lift n t
-           | Some (_,C.Def (_,Some ty)) -> S.lift n ty
-           | Some (_,C.Def (bo,None)) ->
-              type_of_aux context (S.lift n bo) expectedty
-                | None -> raise RelToHiddenHypothesis
+           | Some (_,C.Def (_,ty)) -> S.lift n ty
+          | None -> raise RelToHiddenHypothesis
          with
           _ -> raise (NotWellTyped "Not a close term")
         )
@@ -290,11 +289,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
               [] -> []
             | (Some (n,C.Decl t))::tl ->
                (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
-            | (Some (n,C.Def (t,None)))::tl ->
-               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
-                (aux (i+1) tl)
+            | (Some (n,C.Def (t,ty)))::tl ->
+               (Some (n,
+                C.Def
+                 ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i t))))::
+                  (aux (i+1) tl)
             | None::tl -> None::(aux (i+1) tl)
-            | (Some (_,C.Def (_,Some _)))::_ -> assert false
           in
            aux 1 canonical_context
          in
@@ -356,21 +356,22 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           in
            (* Checks suppressed *)
            C.Prod (n,s,type2)
-     | C.LetIn (n,s,t) ->
+     | C.LetIn (n,s,ty,t) ->
 (*CSC: What are the right expected types for the source and *)
 (*CSC: target of a LetIn? None used.                        *)
         (* Let's visit all the subterms that will not be visited later *)
-        let ty = type_of_aux context s None in
+        let _ = type_of_aux context ty None in
+        let _ = type_of_aux context s (Some ty) in
          let t_typ =
           (* Checks suppressed *)
-          type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
+          type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None
          in  (* CicSubstitution.subst s t_typ *)
           if does_not_occur 1 t_typ then
            (* since [Rel 1] does not occur in typ, substituting any term *)
            (* in place of [Rel 1] is equivalent to delifting once        *)
            CicSubstitution.subst (C.Implicit None) t_typ
           else
-           C.LetIn (n,s,t_typ)
+           C.LetIn (n,s,ty,t_typ)
      | C.Appl (he::tl) when List.length tl > 0 ->
         (* 
         let expected_hetype =
@@ -463,7 +464,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          let (cl,parsno) =
            let obj,_ =
              try
-               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+               CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
              with Not_found -> assert false
            in
           match obj with
@@ -572,7 +573,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
   let uris_and_types =
      let obj,_ =
        try
-         CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+         CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
        with Not_found -> assert false
      in
     let params = CicUtil.params_of_obj obj in
@@ -580,7 +581,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
       (function uri ->
          let obj,_ =
            try
-             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+             CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
            with Not_found -> assert false
          in
          match obj with
@@ -590,7 +591,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
   in
    let rec check uris_and_types subst =
     match uris_and_types,subst with
-       _,[] -> []
+       _,[] -> ()
      | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
         ignore (type_of_aux context t (Some ty)) ;
         let tytl' =