snapshot (first version in which some extensions work, e.g. infix +)

[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 ea29f46fa456e2a4cde51ba1806bdb4d6a873c81..6bfced57e2ad69ed44982773a8bdb85961372ff1 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
@@ -367,9 +367,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
            function
               [] -> []
             | (Some (n,C.Decl t))::tl ->
-               (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) 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.lift_meta l (S.lift i t)),None)))::
+               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
                 (aux (i+1) tl)
             | None::tl -> None::(aux (i+1) tl)
             | (Some (_,C.Def (_,Some _)))::_ -> assert false
@@ -398,13 +398,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           in
            let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
             (* Checks suppressed *)
-            CicSubstitution.lift_meta l ty
+            CicSubstitution.subst_meta l ty
      | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
-        let t' = CicUniv.fresh() in
-        if not (CicUniv.add_gt t' t ) then
-         assert false (* t' is fresh! an error in CicUniv *)
-       else
-          C.Sort (C.Type t')
+         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) ->
@@ -541,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))
@@ -639,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
@@ -675,11 +682,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
-       (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
-       let t' = CicUniv.fresh() in
-       if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
-         assert false ; (* not possible, error in CicUniv *)
-       C.Sort (C.Type t')
+       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? *)