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

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index 9144f4740e1aa52e31b71c9c978e1ab0e269947c..448c83a18fe925f0db84af9c2ded5cb45ebe8f15 100644 (file)
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -48,7 +48,7 @@ let get_context ids_to_terms ids_to_father_ids =
          | C.Prod _ -> []
          | C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
          | C.Lambda _ -> []
-         | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def s)]
+         | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def (s,None))]
          | C.LetIn _ -> []
          | C.Appl _
          | C.Const _ -> []
@@ -60,7 +60,9 @@ let get_context ids_to_terms ids_to_father_ids =
             let counter = ref 0 in
              List.rev_map
               (function (name,_,ty,bo) ->
-                let res = Some (C.Name name, (C.Def (C.Fix (!counter,ifl)))) in
+                let res =
+                 Some (C.Name name, (C.Def ((C.Fix (!counter,ifl)), Some ty)))
+                in
                  incr counter ;
                  res
               ) ifl
@@ -68,7 +70,9 @@ let get_context ids_to_terms ids_to_father_ids =
             let counter = ref 0 in
              List.rev_map
               (function (name,ty,bo) ->
-                let res = Some (C.Name name,(C.Def (C.CoFix (!counter,ifl)))) in
+                let res =
+                 Some (C.Name name,(C.Def ((C.CoFix (!counter,ifl)), Some ty)))
+                in
                  incr counter ;
                  res
               ) ifl

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 4226364fce18d56f7727b270b7e862da3bb2892f..d934e83bfa4443581c161f53ef5a5d1f80f9d79e 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -37,7 +37,7 @@ let type_of_aux'_add_time = ref 0.0;;
 
 let xxx_type_of_aux' m c t =
  let t1 = Sys.time () in
- let res = TypeInference.type_of_aux' m c t 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
@@ -212,7 +212,7 @@ Cic.Sort Cic.Type ;
                match n with
                   C.Anonymous -> n
                 | C.Name n' ->
-                   if TypeInference.does_not_occur 1 t then
+                   if DoubleTypeInference.does_not_occur 1 t then
                     C.Anonymous
                    else
                     C.Name n'

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 29e81bffb813dd3122ee097d1f9b05437e430646..ed62e254cc0b6a499560a48c1c63838273706504 100644 (file)
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -248,12 +248,13 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
                    | Some (`Definition d) ->
                       (match d with
                           {K.def_name = Some n ; K.def_term = t} ->
-                            Some (Cic.Name n, Cic.Def (deannotate t))
+                            Some (Cic.Name n, Cic.Def ((deannotate t),None))
                         | _ -> assert false)
                    | Some (`Proof d) ->
                       (match d with
                           {K.proof_name = Some n } ->
-                            Some (Cic.Name n, Cic.Def (proof2cic deannotate d))
+                            Some (Cic.Name n,
+                              Cic.Def ((proof2cic deannotate d),None))
                         | _ -> assert false)
                  ) canonical_context
                in

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))) ;

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.mli b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
index d7d06ae42346f96eb3cb89ab0128597b7d0e4d5e..a35c8d6c79d6fada2be3937a4566cbdf0e0418f7 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.mli
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
@@ -6,6 +6,11 @@ exception WrongUriToMutualInductiveDefinitions of string
 exception ListTooShort
 exception RelToHiddenHypothesis
 
+val type_of_aux'_add_time: float ref
+val number_new_type_of_aux'_double_work: int ref
+val number_new_type_of_aux': int ref
+val number_new_type_of_aux'_prop: int ref
+
 type types = {synthesized : Cic.term ; expected : Cic.term option};;
 
 module CicHash :

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 81668203dab55673c8fb2ab74c2ebbcac9a0753f..d6293d2434ad61af36b7c94203a0cf7b6c8641c7 100644 (file)
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -261,7 +261,7 @@ let eta_fix metasenv t =
             List.map (fun (_,t) -> t) constructors 
           else 
            let term_type = 
-              TypeInference.type_of_aux' metasenv context term in
+              CicTypeChecker.type_of_aux' metasenv context term in
             (match term_type with
                C.Appl (hd::params) -> 
                  List.map (fun (_,t) -> clean_up t params) constructors