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).
| _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
;;
| _ -> 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 *)
(* 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 *)
let module R = CicReduction in
let module S = CicSubstitution in
let module U = UriManager in
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 ->
let synthesized =
match t with
C.Rel n ->
ty
in
let synthesized' = beta_reduce synthesized in
ty
in
let synthesized' = beta_reduce synthesized in
+ let synthesized' = !pack_coercion metasenv context synthesized' in
let types,res =
match expectedty with
None ->
let types,res =
match expectedty with
None ->
type types = {synthesized : Cic.term ; expected : Cic.term option};;
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
val double_type_of :
Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
types Cic.CicHash.t
let typecheck ~localization_tbl metasenv uri obj =
profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
let typecheck ~localization_tbl metasenv uri obj =
profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
+
+let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
val insert_coercions: bool ref (* initially true *)
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
val pack_coercion_obj: Cic.obj -> Cic.obj