From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 13 Apr 2006 11:17:10 +0000 (+0000)
Subject: Ugly solution to the "we proved T that is equivalent to T" problem:
X-Git-Tag: 0.4.95@7852~1514
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=3f00ce2e2e2f2d443e942d86c394200554ba2496;p=helm.git

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

diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml
index 30a8f5c29..214f656c3 100644
--- a/components/cic_acic/doubleTypeInference.ml
+++ b/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/components/cic_acic/doubleTypeInference.mli b/components/cic_acic/doubleTypeInference.mli
index 892e09f8a..86d8b23fa 100644
--- a/components/cic_acic/doubleTypeInference.mli
+++ b/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/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 6065d24bd..3443c9b6e 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/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/components/cic_unification/cicRefine.mli b/components/cic_unification/cicRefine.mli
index c3ab49e0a..be1069e71 100644
--- a/components/cic_unification/cicRefine.mli
+++ b/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