From: Stefano Zacchiroli Date: Fri, 5 Sep 2003 15:36:28 +0000 (+0000) Subject: Defs in context may now have an optional type (when unknown). X-Git-Tag: v0_0_1~31 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c706b1cb2c7cbdd23a3281d35d3f0b10c3a684cf 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 9144f4740..448c83a18 100644 --- 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 4226364fc..d934e83bf 100644 --- 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 29e81bffb..ed62e254c 100644 --- 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 362422cac..03227ef9b 100644 --- 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 d7d06ae42..a35c8d6c7 100644 --- 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 81668203d..d6293d243 100644 --- 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