From 7dc9e84cd0e40d8ff6847aabe780a4196e30be36 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 13 Apr 2006 11:17:10 +0000 Subject: [PATCH] Ugly solution to the "we proved T that is equivalent to T" problem: we use pack_coercion (defined into cicRefine) inside doubleTypeInference (that is well below in the module hierarchy :-( This is also supposed to be quite expensive (since pack_coercion uses the refiner and coercion packing is applied to every expected/synthesized type). --- helm/software/components/cic_acic/doubleTypeInference.ml | 7 +++++++ helm/software/components/cic_acic/doubleTypeInference.mli | 2 ++ helm/software/components/cic_unification/cicRefine.ml | 2 ++ helm/software/components/cic_unification/cicRefine.mli | 1 - 4 files changed, 11 insertions(+), 1 deletion(-) diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml index 30a8f5c29..214f656c3 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.ml +++ b/helm/software/components/cic_acic/doubleTypeInference.ml @@ -319,6 +319,8 @@ let type_of_mutual_inductive_constr uri i j = | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) ;; +let pack_coercion = ref (fun _ _ _ -> assert false);; + (* type_of_aux' is just another name (with a different scope) for type_of_aux *) let rec type_of_aux' subterms_to_types metasenv context t expectedty = (* Coscoy's double type-inference algorithm *) @@ -330,6 +332,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let module R = CicReduction in let module S = CicSubstitution in let module U = UriManager in + let expectedty = + match expectedty with + None -> None + | Some t -> Some (!pack_coercion metasenv context t) in let synthesized = match t with C.Rel n -> @@ -609,6 +615,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = ty in let synthesized' = beta_reduce synthesized in + let synthesized' = !pack_coercion metasenv context synthesized' in let types,res = match expectedty with None -> diff --git a/helm/software/components/cic_acic/doubleTypeInference.mli b/helm/software/components/cic_acic/doubleTypeInference.mli index 892e09f8a..86d8b23fa 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.mli +++ b/helm/software/components/cic_acic/doubleTypeInference.mli @@ -14,6 +14,8 @@ val number_new_type_of_aux'_prop: int ref type types = {synthesized : Cic.term ; expected : Cic.term option};; +val pack_coercion : (Cic.metasenv -> Cic.context -> Cic.term -> Cic.term) ref;; + val double_type_of : Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types Cic.CicHash.t diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 6065d24bd..3443c9b6e 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1645,3 +1645,5 @@ let type_of_aux' ?localization_tbl metasenv context term ugraph = let typecheck ~localization_tbl metasenv uri obj = profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj + +let _ = DoubleTypeInference.pack_coercion := pack_coercion;; diff --git a/helm/software/components/cic_unification/cicRefine.mli b/helm/software/components/cic_unification/cicRefine.mli index c3ab49e0a..be1069e71 100644 --- a/helm/software/components/cic_unification/cicRefine.mli +++ b/helm/software/components/cic_unification/cicRefine.mli @@ -46,6 +46,5 @@ val typecheck : val insert_coercions: bool ref (* initially true *) -(* given a closed term returns it with all coercions packed *) val pack_coercion_obj: Cic.obj -> Cic.obj -- 2.39.2