Defs in context may now have an optional type (when unknown).

[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 362422cac59fa61509a66f76d5ce2fda950702c8..03227ef9b75df7af38c9bcac6db2f8e9d201d737 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -31,6 +31,21 @@ exception WrongUriToMutualInductiveDefinitions of string;;
 exception ListTooShort;;
 exception RelToHiddenHypothesis;;
 
+let type_of_aux'_add_time = ref 0.0;;
+let number_new_type_of_aux'_double_work = ref 0;;
+let number_new_type_of_aux' = ref 0;;
+let number_new_type_of_aux'_prop = ref 0;;
+
+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 t2 = Sys.time () in
+ type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
+ res
+;;
+
 type types = {synthesized : Cic.term ; expected : Cic.term option};;
 
 (* does_not_occur n te                              *)
@@ -160,8 +175,7 @@ let rec head_beta_reduce =
         C.CoFix (i,fl')
 ;;
 
-(* syntactic_equality up to cookingsno for uris *)
-(* (which is often syntactically irrilevant),   *)
+(* syntactic_equality up to the                 *)
 (* distinction between fake dependent products  *)
 (* and non-dependent products, alfa-conversion  *)
 (*CSC: must alfa-conversion be considered or not? *)
@@ -325,8 +339,10 @@ 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 bo) -> type_of_aux context (S.lift n bo) expectedty
-          | None -> raise RelToHiddenHypothesis
+           | 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
          with
           _ -> raise (NotWellTyped "Not a close term")
         )
@@ -344,9 +360,11 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
               [] -> []
             | (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.Def t))::tl ->
-               (Some (n,C.Def (S.lift_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)))::
+                (aux (i+1) tl)
             | None::tl -> None::(aux (i+1) tl)
+            | (Some (_,C.Def (_,Some _)))::_ -> assert false
           in
            aux 1 canonical_context
          in
@@ -355,10 +373,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
             (fun t ct ->
               match t,ct with
                  _,None -> ()
-               | Some t,Some (_,C.Def ct) ->
+               | Some t,Some (_,C.Def (ct,_)) ->
                   let expected_type =
                    R.whd context
-                    (CicTypeChecker.type_of_aux' metasenv context ct)
+                    (xxx_type_of_aux' metasenv context ct)
                   in
                    (* Maybe I am a bit too paranoid, because   *)
                    (* if the term is well-typed than t and ct  *)
@@ -411,10 +429,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
 (*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 _ = type_of_aux context s None in
+        let ty = type_of_aux context s None in
          let t_typ =
           (* Checks suppressed *)
-          type_of_aux ((Some (n,(C.Def s)))::context) t None
+          type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
          in
           if does_not_occur 1 t_typ then
            (* since [Rel 1] does not occur in typ, substituting any term *)
@@ -427,7 +445,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          (* Inefficient, the head is computed twice. But I know *)
          (* of no other solution.                               *)
          (head_beta_reduce
-          (R.whd context (CicTypeChecker.type_of_aux' metasenv context he)))
+          (R.whd context (xxx_type_of_aux' metasenv context he)))
         in
          let hetype = type_of_aux context he (Some expected_hetype) in
          let tlbody_and_type =
@@ -479,7 +497,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         in
         let (parameters, arguments,exp_named_subst) =
          let type_of_term =
-          CicTypeChecker.type_of_aux' metasenv context term
+          xxx_type_of_aux' metasenv context term
          in
           match
            R.whd context (type_of_aux context term
@@ -516,7 +534,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
               in
                let expectedtype =
                 type_of_branch context parsno need_dummy outtype cons
-                  (CicTypeChecker.type_of_aux' metasenv context cons)
+                  (xxx_type_of_aux' metasenv context cons)
                in
                 ignore (type_of_aux context p
                  (Some (head_beta_reduce expectedtype))) ;