| (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
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
+ 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 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 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 _ ->
- raise
- (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
+ | 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 ->
- raise
- (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
+ 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 ->
Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
in
| CoercGraph.SomeCoercion c ->
Cic.Appl [c;s'], coercion_tgt
| CoercGraph.NoCoercion
- | CoercGraph.NotHandled _
+ | 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 ->
- 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))))
+ 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
hetype tlbody_and_type ugraph2
in
C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
- | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
+ | 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
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
match tl with
[] -> [],metasubst,metasenv,ugraph
- | ((uri,t) as subst)::tl ->
+ | (uri,t)::tl ->
let ty_uri,ugraph1 = type_of_variable uri ugraph in
let typeofvar =
CicSubstitution.subst_vars substs ty_uri in
) ;
*)
let t',typeoft,metasubst',metasenv',ugraph2 =
- type_of_aux metasubst metasenv context t ugraph1
- in
+ type_of_aux metasubst metasenv context t ugraph1 in
+ let subst = uri,t' in
let metasubst'',metasenv'',ugraph3 =
try
fo_unif_subst
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
in
(*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) ->
projects / helm.git / blobdiff