fix universe handling, newly encountered objects are typed in an empty ugraph

that after the cleanup phase is committed into the cic_environement and merged
with the current one.

minor reformatting of sources and some more for_all

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index bcdb340bd1d137af0393fbd1cf2cfe6fc028fc17..44cf6d24ad1c03bda2f5a61605fb092b4537a3c9 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -141,12 +141,12 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri n
 
 exception CicEnvironmentError;;
 
-let rec type_of_constant ~logger uri (ugraph as orig_ugraph) =
+let rec type_of_constant ~logger uri orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
  let cobj,ugraph =
-   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+   match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
     | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
        logger#log (`Start_type_checking uri) ;
@@ -154,7 +154,7 @@ let rec type_of_constant ~logger uri (ugraph as orig_ugraph) =
        let inferred_ugraph = 
          match uobj with
            C.Constant (_,Some te,ty,_,_) ->
-           let _,ugraph = type_of ~logger ty ugraph in
+           let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
            let type_of_te,ugraph = type_of ~logger te ugraph in
               let b,ugraph = R.are_convertible [] type_of_te ty ugraph in
               if not b then
@@ -166,17 +166,17 @@ let rec type_of_constant ~logger uri (ugraph as orig_ugraph) =
                 ugraph
          | C.Constant (_,None,ty,_,_) ->
            (* only to check that ty is well-typed *)
-           let _,ugraph = type_of ~logger ty ugraph in 
+           let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in 
            ugraph
          | C.CurrentProof (_,conjs,te,ty,_,_) ->
              let _,ugraph =
               List.fold_left
                (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
                  let _,ugraph = 
-                  type_of_aux' ~logger metasenv context ty ugraph 
+                 type_of_aux' ~logger metasenv context ty ugraph 
                 in
                  (metasenv @ [conj],ugraph)
-               ) ([],ugraph) conjs
+               ) ([],CicUniv.empty_ugraph) conjs
              in
              let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
              let type_of_te,ugraph = type_of_aux' ~logger conjs [] te ugraph in
@@ -205,17 +205,19 @@ let rec type_of_constant ~logger uri (ugraph as orig_ugraph) =
     | _ ->
         raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
 
-and type_of_variable ~logger uri (ugraph as orig_ugraph) =
+and type_of_variable ~logger uri orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   (* 0 because a variable is never cooked => no partial cooking at one level *)
-  match CicEnvironment.is_type_checked ~trust:true ugraph uri with
-     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
-   | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_) as uobj, unchecked_ugraph) ->
+  match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
+  | CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
+  | CicEnvironment.UncheckedObj 
+     (C.Variable (_,bo,ty,_,_) as uobj, unchecked_ugraph) 
+    ->
       logger#log (`Start_type_checking uri) ;
       (* only to check that ty is well-typed *)
-      let _,ugraph = type_of ~logger ty ugraph in
+      let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
       let inferred_ugraph = 
        match bo with
            None -> ugraph
@@ -228,7 +230,9 @@ and type_of_variable ~logger uri (ugraph as orig_ugraph) =
             else
               ugraph 
       in
-       let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+       let ugraph, ul, obj = 
+         check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj 
+       in
        CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
        logger#log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
@@ -236,7 +240,8 @@ and type_of_variable ~logger uri (ugraph as orig_ugraph) =
          | CicEnvironment.CheckedObj _ 
          | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError)
    |  _ ->
-       raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
+       raise (TypeCheckerFailure (lazy 
+          ("Unknown variable:" ^ U.string_of_uri uri)))
 
 and does_not_occur ?(subst=[]) context n nn te =
  let module C = Cic in
@@ -264,14 +269,15 @@ and does_not_occur ?(subst=[]) context n nn te =
         with
          CicUtil.Subst_not_found _ -> true)
     | C.Cast (te,ty) ->
-       does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
+       does_not_occur ~subst context n nn te && 
+       does_not_occur ~subst context n nn ty
     | C.Prod (name,so,dest) ->
        does_not_occur ~subst context n nn so &&
         does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1)
          (nn + 1) dest
     | C.Lambda (name,so,dest) ->
        does_not_occur ~subst context n nn so &&
-        does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+        does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1)
          dest
     | C.LetIn (name,so,ty,dest) ->
        does_not_occur ~subst context n nn so &&
@@ -279,16 +285,17 @@ and does_not_occur ?(subst=[]) context n nn te =
          does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
           (n + 1) (nn + 1) dest
     | C.Appl l ->
-       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
+       List.for_all (does_not_occur ~subst context n nn) l
     | C.Var (_,exp_named_subst)
     | C.Const (_,exp_named_subst)
     | C.MutInd (_,_,exp_named_subst)
     | C.MutConstruct (_,_,_,exp_named_subst) ->
-       List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x)
-        exp_named_subst true
+       List.for_all (fun (_,x) -> does_not_occur ~subst context n nn x)
+        exp_named_subst
     | C.MutCase (_,_,out,te,pl) ->
-       does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te &&
-        List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true
+       does_not_occur ~subst context n nn out && 
+       does_not_occur ~subst context n nn te &&
+       List.for_all (does_not_occur ~subst context n nn) pl
     | C.Fix (_,fl) ->
        let len = List.length fl in
         let n_plus_len = n + len in
@@ -595,16 +602,18 @@ and check_mutual_inductive_defs uri obj ugraph =
                lazy ("Unknown mutual inductive definition:" ^
                 UriManager.string_of_uri uri)))
 
-and type_of_mutual_inductive_defs ~logger uri i (ugraph as orig_ugraph) =
+and type_of_mutual_inductive_defs ~logger uri i orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   let cobj,ugraph1 =
-   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+   match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
      | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
         logger#log (`Start_type_checking uri) ;
-        let inferred_ugraph = check_mutual_inductive_defs ~logger uri uobj ugraph in
+        let inferred_ugraph = 
+           check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph 
+         in
          let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
         CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
         logger#log (`Type_checking_completed uri) ;
@@ -613,25 +622,25 @@ and type_of_mutual_inductive_defs ~logger uri i (ugraph as orig_ugraph) =
            | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
         )
   in
-    match cobj with
-       C.InductiveDefinition (dl,_,_,_) ->
-         let (_,_,arity,_) = List.nth dl i in
-           arity,ugraph1
-      | _ ->
-         raise (TypeCheckerFailure
-           (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
+  match cobj with
+  | C.InductiveDefinition (dl,_,_,_) ->
+      let (_,_,arity,_) = List.nth dl i in
+        arity,ugraph1
+  | _ ->
+     raise (TypeCheckerFailure
+      (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
            
-and type_of_mutual_inductive_constr ~logger uri i j (ugraph as orig_ugraph) =
+and type_of_mutual_inductive_constr ~logger uri i j orig_ugraph =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
   let cobj,ugraph1 =
-    match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+    match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
       | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
          logger#log (`Start_type_checking uri) ;
          let inferred_ugraph = 
-           check_mutual_inductive_defs ~logger uri uobj ugraph 
+           check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph 
          in
           let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
          CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);