- changed license to lgpl

[helm.git] / helm / ocaml / cic_omdoc / doubleTypeInference.ml

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 3163dfe09bf21804932f3a4cabefad32745e1752..128da869b72a142b8cb914c80f68a02a221952ff 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -41,7 +41,7 @@ let double_work = ref 0;;
 
 let xxx_type_of_aux' m c t =
  let t1 = Sys.time () in
- let res = CicTypeChecker.type_of_aux' m c t in
+ let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
  let t2 = Sys.time () in
  type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
  res
@@ -266,14 +266,14 @@ let type_of_constant uri =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
-      CicEnvironment.CheckedObj cobj -> cobj
+   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+      CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constant")
   in
    match cobj with
-      C.Constant (_,_,ty,_) -> ty
-    | C.CurrentProof (_,_,_,ty,_) -> ty
+      C.Constant (_,_,ty,_,_) -> ty
+    | C.CurrentProof (_,_,_,ty,_,_) -> ty
     | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 ;;
 
@@ -281,8 +281,8 @@ 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 uri with
-     CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
+  match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
    | CicEnvironment.UncheckedObj (C.Variable _) ->
       raise (NotWellTyped "Reference to an unchecked variable")
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
@@ -293,13 +293,13 @@ 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 uri with
-      CicEnvironment.CheckedObj cobj -> cobj
+   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+      CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked inductive type")
   in
    match cobj with
-      C.InductiveDefinition (dl,_,_) ->
+      C.InductiveDefinition (dl,_,_,_) ->
        let (_,_,arity,_) = List.nth dl i in
         arity
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
@@ -310,13 +310,13 @@ 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 uri with
-      CicEnvironment.CheckedObj cobj -> cobj
+   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+      CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constructor")
   in
    match cobj with
-      C.InductiveDefinition (dl,_,_) ->
+      C.InductiveDefinition (dl,_,_,_) ->
        let (_,_,_,cl) = List.nth dl i in
         let (_,ty) = List.nth cl (j-1) in
          ty
@@ -361,9 +361,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
      | C.Meta (n,l) -> 
         (* Let's visit all the subterms that will not be visited later *)
-        let (_,canonical_context,_) =
-         List.find (function (m,_,_) -> n = m) metasenv
-        in
+        let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
          let lifted_canonical_context =
           let rec aux i =
            function
@@ -398,12 +396,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
                | _,_ -> assert false (* the term is not well typed!!! *)
             ) l lifted_canonical_context
           in
-           let (_,canonical_context,ty) =
-            List.find (function (m,_,_) -> n = m) metasenv
-           in
+           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
             (* Checks suppressed *)
             CicSubstitution.lift_meta l ty
-     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+     | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
+         C.Sort (C.Type (CicUniv.fresh()))
+     | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
      | C.Implicit _ -> raise (Impossible 21)
      | C.Cast (te,ty) ->
         (* Let's visit all the subterms that will not be visited later *)
@@ -539,8 +537,13 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          (* Checks suppressed *)
          (* Let's visit all the subterms that will not be visited later *)
          let (cl,parsno) =
-          match CicEnvironment.get_cooked_obj uri with
-             C.InductiveDefinition (tl,_,parsno) ->
+           let obj,_ =
+             try
+               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+             with Not_found -> assert false
+           in
+          match obj with
+             C.InductiveDefinition (tl,_,parsno,_) ->
               let (_,_,_,cl) = List.nth tl i in (cl,parsno)
            | _ ->
              raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
@@ -637,17 +640,23 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
 
  and visit_exp_named_subst context uri exp_named_subst =
   let uris_and_types =
-   match CicEnvironment.get_cooked_obj uri with
-      Cic.Constant (_,_,_,params)
-    | Cic.CurrentProof (_,_,_,_,params)
-    | Cic.Variable (_,_,_,params)
-    | Cic.InductiveDefinition (_,params,_) ->
-       List.map
-        (function uri ->
-          match CicEnvironment.get_cooked_obj uri with
-             Cic.Variable (_,None,ty,_) -> uri,ty
-           | _ -> assert false (* the theorem is well-typed *)
-        ) params
+     let obj,_ =
+       try
+         CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+       with Not_found -> assert false
+     in
+    let params = CicUtil.params_of_obj obj in
+     List.map
+      (function uri ->
+         let obj,_ =
+           try
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+           with Not_found -> assert false
+         in
+         match obj with
+           Cic.Variable (_,None,ty,_,_) -> uri,ty
+         | _ -> assert false (* the theorem is well-typed *)
+      ) params
   in
    let rec check uris_and_types subst =
     match uris_and_types,subst with
@@ -668,10 +677,19 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
    let t1' = CicReduction.whd context t1 in
    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
    match (t1', t2') with
-      (C.Sort s1, C.Sort s2)
-        when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
+      (C.Sort _, C.Sort s2)
+        when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> 
+        (* different from Coq manual!!! *)
          C.Sort s2
-    | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+    | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
+       C.Sort (C.Type (CicUniv.fresh()))
+    | (C.Sort _,C.Sort (C.Type t1)) -> 
+        (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
+       C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
+    | (C.Meta _, C.Sort _) -> t2'
+    | (C.Meta _, (C.Meta (_,_) as t))
+    | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
+        t2'
     | (_,_) ->
       raise
        (NotWellTyped