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"
| (CicUnification.Uncertain msg) -> raise (Uncertain msg)
;;
-let enrich loc f exn =
+let enrich localization_tbl t ?(f = fun msg -> msg) exn =
let exn' =
match exn with
RefineFailure msg -> RefineFailure (f msg)
| Uncertain msg -> Uncertain (f msg)
- | _ -> assert false
+ | _ -> assert false in
+ let loc =
+ try
+ Cic.CicHash.find localization_tbl t
+ with Not_found ->
+ prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
+ assert false
in
- match loc with
- None -> raise exn'
- | Some loc -> raise (HExtlib.Localized (loc,exn'))
+ raise (HExtlib.Localized (loc,exn'))
let relocalize localization_tbl oldt newt =
try
| _ -> assert false
;;
+
let rec type_of_constant uri ugraph =
let module C = Cic in
let module R = CicReduction in
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
- (* this stops on binders, so we have to call it every time *)
+ let (t',_,_,_,_) as res =
match t with
(* function *)
C.Rel n ->
(S.lift n bo) ugraph
in
t,ty,subst,metasenv,ugraph
- | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis"))
+ | None ->
+ enrich localization_tbl t
+ (RefineFailure (lazy "Rel to hidden hypothesis"))
with
- _ -> raise (RefineFailure (lazy "Not a close term")))
+ _ ->
+ enrich localization_tbl t
+ (RefineFailure (lazy "Not a close term")))
| C.Var (uri,exp_named_subst) ->
let exp_named_subst',subst',metasenv',ugraph1 =
check_exp_named_subst
let te',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv' context te ugraph1
in
- let subst''',metasenv''',ugraph3 =
- fo_unif_subst subst'' context metasenv''
- inferredty ty' ugraph2
- in
- C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
+ (try
+ let subst''',metasenv''',ugraph3 =
+ fo_unif_subst subst'' context metasenv''
+ inferredty ty' ugraph2
+ in
+ C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
+ with
+ exn ->
+ enrich localization_tbl te'
+ ~f:(fun _ ->
+ lazy ("The term " ^
+ 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
+ )
| 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 _ ->
- raise
- (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
- | CoercGraph.NotMetaClosed ->
- raise
- (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 =
let x',ty,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context x ugraph
in
- relocalize localization_tbl x x';
(x', ty)::res,subst',metasenv',ugraph1
) tl ([],subst',metasenv',ugraph1)
in
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
its instances
*)
+ let outtype,outtypety, subst, metasenv,ugraph4 =
+ type_of_aux subst metasenv context outtype ugraph4 in
(match outtype with
| C.Meta (n,l) ->
(let candidate,ugraph5,metasenv,subst =
(Cic.Appl (outtype::right_args@[term']))),
subst,metasenv,ugraph)
| _ -> (* easy case *)
- let outtype,outtypety, subst, metasenv,ugraph4 =
- type_of_aux subst metasenv context outtype ugraph4
- in
let tlbody_and_type,subst,metasenv,ugraph4 =
List.fold_right
(fun x (res,subst,metasenv,ugraph) ->
fl_ty' fl_bo' fl
in
C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
+ in
+ 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]) ]) as t 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 -
| (uri,t)::tl ->
let ty_uri,ugraph1 = type_of_variable uri ugraph in
let typeofvar =
-prerr_endline ("<<<" ^ CicPp.ppterm ty_uri);
CicSubstitution.subst_vars substs ty_uri in
(* CSC: why was this code here? it is wrong
(match CicEnvironment.get_cooked_obj ~trust:false uri with
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
- (try Some (Cic.CicHash.find localization_tbl hete) with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm hete); None)
- 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
+ newt, subst, metasenv, ugraph)
+ | 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
(*CSC: this is a very rough approximation; to be finished *)
let are_all_occurrences_positive metasenv ugraph uri tys leftno =
- let number_of_types = List.length tys in
let subst,metasenv,ugraph,tys =
List.fold_right
(fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
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