* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Printf
exception RefineFailure of string Lazy.t;;
exception Uncertain of string Lazy.t;;
exception AssertFailure of string Lazy.t;;
+let insert_coercions = ref true
+
let debug_print = fun _ -> ()
let profiler = HExtlib.profile "CicRefine.fo_unif"
| _ -> assert false
;;
+
let rec type_of_constant uri ugraph =
let module C = Cic in
let module R = CicReduction in
C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
with
exn ->
- enrich localization_tbl t
+ enrich localization_tbl te'
~f:(fun _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst'' te
+ CicMetaSubst.ppterm_in_context subst'' te'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst'' inferredty
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst'' ty context)) exn
+ CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
)
| C.Prod (name,s,t) ->
let carr t subst context = CicMetaSubst.apply_subst subst t in
- let coerce_to_sort
- in_source tgt_sort t type_to_coerce subst ctx metasenv uragph
+ let coerce_to_sort in_source tgt_sort t type_to_coerce
+ subst context metasenv uragph
=
- let coercion_src = carr type_to_coerce subst ctx in
- match coercion_src with
- | Cic.Sort _ ->
- t,type_to_coerce,subst,metasenv,ugraph
-(*
- | Cic.Meta _ as meta when not in_source ->
- let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
- let subst, metasenv, ugraph =
- fo_unif_subst
- subst ctx metasenv meta coercion_tgt ugraph
- in
- t, Cic.Sort tgt_sort, subst, metasenv, ugraph
-*)
- | Cic.Meta _ as meta ->
- t, meta, subst, metasenv, ugraph
- | Cic.Cast _ as cast ->
- t, cast, subst, metasenv, ugraph
- | term ->
- let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
- let search = CoercGraph.look_for_coercion in
- let boh = search coercion_src coercion_tgt in
- (match boh with
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl s
- (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl s
- (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
- | CoercGraph.SomeCoercion c ->
- Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
+ if not !insert_coercions then
+ t,type_to_coerce,subst,metasenv,ugraph
+ else
+ let coercion_src = carr type_to_coerce subst context in
+ match coercion_src with
+ | Cic.Sort _ ->
+ t,type_to_coerce,subst,metasenv,ugraph
+ | Cic.Meta _ as meta ->
+ t, meta, subst, metasenv, ugraph
+ | Cic.Cast _ as cast ->
+ t, cast, subst, metasenv, ugraph
+ | term ->
+ let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
+ let search = CoercGraph.look_for_coercion in
+ let boh = search coercion_src coercion_tgt in
+ (match boh with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst t context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.NotMetaClosed ->
+ enrich localization_tbl t
+ (Uncertain
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst t context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.SomeCoercion c ->
+ let newt, tty, subst, metasenv, ugraph =
+ avoid_double_coercion
+ subst metasenv ugraph
+ (Cic.Appl[c;t]) coercion_tgt
+ in
+ newt, tty, subst, metasenv, ugraph)
in
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph in
- let s',sort1 =
- match CicReduction.whd ~subst:subst' context sort1 with
- C.Meta _
- | C.Sort _ -> s',sort1
- | coercion_src ->
- let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in
- let search = CoercGraph.look_for_coercion in
- let boh = search coercion_src coercion_tgt in
- match boh with
- | CoercGraph.SomeCoercion c ->
- Cic.Appl [c;s'], coercion_tgt
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _
- | CoercGraph.NotMetaClosed ->
- raise (RefineFailure (lazy (sprintf
- "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))))
+ let s',sort1,subst',metasenv',ugraph1 =
+ if not !insert_coercions then
+ s',sort1, subst', metasenv', ugraph1
+ else
+ match CicReduction.whd ~subst:subst' context sort1 with
+ | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
+ | coercion_src ->
+ let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
+ let search = CoercGraph.look_for_coercion in
+ let boh = search coercion_src coercion_tgt in
+ match boh with
+ | CoercGraph.SomeCoercion c ->
+ let newt, tty, subst', metasenv', ugraph1 =
+ avoid_double_coercion
+ subst' metasenv' ugraph1
+ (Cic.Appl[c;s']) coercion_tgt
+ in
+ newt, tty, subst', metasenv', ugraph1
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
+ enrich localization_tbl s'
+ (RefineFailure
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst s' context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.NotMetaClosed ->
+ enrich localization_tbl s'
+ (Uncertain
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst s' context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^ " that is not a sort")))
in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
let t',type2,subst'',metasenv'',ugraph2 =
eat_prods true subst'' metasenv'' context
hetype tlbody_and_type ugraph2
in
- C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
- | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
+ avoid_double_coercion
+ subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
+ | C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
let exp_named_subst',subst',metasenv',ugraph1 =
check_exp_named_subst subst metasenv context
C.InductiveDefinition (l,expl_params,parsno,_) ->
List.nth l i , expl_params, parsno, u
| _ ->
- raise
- (RefineFailure
- (lazy ("Unkown mutual inductive definition " ^
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy ("Unkown mutual inductive definition " ^
U.string_of_uri uri)))
in
let rec count_prod t =
in
let actual_type = CicReduction.whd ~subst context actual_type in
let subst,metasenv,ugraph3 =
+ try
fo_unif_subst subst context metasenv
expected_type' actual_type ugraph2
+ with
+ exn ->
+ enrich localization_tbl term' exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst term'
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst actual_type
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst expected_type' context))
in
let rec instantiate_prod t =
function
relocalize localization_tbl t t';
res
+ and avoid_double_coercion subst metasenv ugraph t ty =
+ match t with
+ | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when
+ CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
+ let source_carr = CoercGraph.source_of c2 in
+ let tgt_carr = CicMetaSubst.apply_subst subst ty in
+ (match CoercGraph.look_for_coercion source_carr tgt_carr
+ with
+ | CoercGraph.SomeCoercion c ->
+ Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph
+ | _ -> assert false) (* the composite coercion must exist *)
+ | _ -> t, ty, subst, metasenv, ugraph
+
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
with the actual context *)
and eat_prods
allow_coercions subst metasenv context hetype tlbody_and_type ugraph
=
- let rec mk_prod metasenv context =
+ let rec mk_prod metasenv context' =
function
[] ->
let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context
+ CicMkImplicit.mk_implicit_type metasenv subst context'
in
let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
+ CicMkImplicit.identity_relocation_list_for_metavariable context'
in
metasenv,Cic.Meta (idx, irl)
| (_,argty)::tl ->
let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context
+ CicMkImplicit.mk_implicit_type metasenv subst context'
in
let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
+ CicMkImplicit.identity_relocation_list_for_metavariable context'
in
let meta = Cic.Meta (idx,irl) in
let name =
(* Nevertheless, argty is well-typed only in context. *)
(* Thus I generate a name (name_hint) in context and *)
(* then I generate a name --- using the hint name_hint *)
- (* --- that is fresh in (context'@context). *)
+ (* --- that is fresh in context'. *)
let name_hint =
(* Cic.Name "pippo" *)
FreshNamesGenerator.mk_fresh_name ~subst metasenv
in
(* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
FreshNamesGenerator.mk_fresh_name ~subst
- [] context name_hint ~typ:(Cic.Sort Cic.Prop)
+ [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
in
let metasenv,target =
- mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+ mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
in
metasenv,Cic.Prod (name,meta,target)
in
fo_unif_subst subst context metasenv hety s ugraph
in
hete,subst,metasenv,ugraph1
- with exn when allow_coercions ->
+ with exn when allow_coercions && !insert_coercions ->
(* we search a coercion from hety to s *)
- let coer =
+ let coer, tgt_carr =
let carr t subst context =
CicMetaSubst.apply_subst subst t
in
let c_hety = carr hety subst context in
let c_s = carr s subst context in
- CoercGraph.look_for_coercion c_hety c_s
+ CoercGraph.look_for_coercion c_hety c_s, c_s
in
- match coer with
+ (match coer with
| CoercGraph.NoCoercion
| CoercGraph.NotHandled _ ->
- let msg _e =
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*))
- in
- enrich localization_tbl hete ~f:msg exn
+ enrich localization_tbl hete
+ (RefineFailure
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*))))
| CoercGraph.NotMetaClosed ->
- raise (Uncertain (lazy "Coercions on meta"))
+ enrich localization_tbl hete
+ (Uncertain
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*))))
| CoercGraph.SomeCoercion c ->
- (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
+ let newt, _, subst, metasenv, ugraph =
+ avoid_double_coercion
+ subst metasenv ugraph
+ (Cic.Appl[c;hete]) tgt_carr in
+ try
+ let newty,newhety,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context newt ugraph in
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst subst context metasenv
+ newhety s ugraph
+ in
+ newt, subst, metasenv, ugraph
+ with exn ->
+ enrich localization_tbl hete
+ ~f:(fun _ ->
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*)))) exn)
+ | exn ->
+ enrich localization_tbl hete
+ ~f:(fun _ ->
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*)))) exn
in
let coerced_args,metasenv',subst',t',ugraph2 =
eat_prods metasenv subst context
let metasenv,ugraph,cl' =
List.fold_right
(fun (name,ty) (metasenv,ugraph,res) ->
- let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
+ let ty =
+ CicTypeChecker.debrujin_constructor
+ ~cb:(relocalize localization_tbl) uri typesno ty in
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
let ty' = undebrujin uri typesno tys ty' in
projects / helm.git / blobdiff