subst', metasenv',ugraph1)
| C.Sort (C.Type tno) ->
let tno' = CicUniv.fresh() in
- let ugraph1 = CicUniv.add_gt tno' tno ugraph in
- t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+ (try
+ let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+ t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
| C.Sort _ ->
t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
| C.Implicit infos ->
t' sort2 subst'' context_for_t metasenv'' ugraph2
in
let sop,subst''',metasenv''',ugraph3 =
- sort_of_prod subst'' metasenv''
- context (name,s') (sort1,sort2) ugraph2
+ sort_of_prod localization_tbl subst'' metasenv''
+ context (name,s') t' (sort1,sort2) ugraph2
in
C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
| C.Lambda (n,s,t) ->
check_exp_named_subst_aux metasubst metasenv [] tl ugraph
- and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
+ and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
+ ugraph
+ =
let module C = Cic in
let context_for_t2 = (Some (name,C.Decl s))::context in
let t1'' = CicReduction.whd ~subst context t1 in
C.Sort s2,subst,metasenv,ugraph
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
let t' = CicUniv.fresh() in
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.Type t'),subst,metasenv,ugraph2
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.Type t'),subst,metasenv,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
| (C.Sort _,C.Sort (C.Type t1)) ->
C.Sort (C.Type t1),subst,metasenv,ugraph
| (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
with _ -> assert false (* unification against a metavariable *)
in
t2'',subst,metasenv,ugraph1
+ | (C.Sort _,_)
+ | (C.Meta _,_) ->
+ enrich localization_tbl s
+ (RefineFailure
+ (lazy
+ (sprintf
+ "%s is supposed to be a type, but its type is %s"
+ (CicMetaSubst.ppterm_in_context subst t context)
+ (CicMetaSubst.ppterm_in_context subst t2 context))))
| _,_ ->
- raise
- (RefineFailure
- (lazy
- (sprintf
- ("Two sorts were expected, found %s " ^^
- "(that reduces to %s) and %s (that reduces to %s)")
- (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
- (CicPp.ppterm t2''))))
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy
+ (sprintf
+ "%s is supposed to be a type, but its type is %s"
+ (CicMetaSubst.ppterm_in_context subst s context)
+ (CicMetaSubst.ppterm_in_context subst t1 context))))
and avoid_double_coercion context subst metasenv ugraph t ty =
if not !pack_coercions then
(match coer with
| CoercGraph.NoCoercion
| CoercGraph.NotHandled _ ->
- enrich localization_tbl hete
- (RefineFailure
+ enrich localization_tbl hete exn
+ ~f:(fun _ ->
(lazy ("The term " ^
CicMetaSubst.ppterm_in_context subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst s context
(* "\nReason: " ^ Lazy.force e*))))
| CoercGraph.NotMetaClosed ->
- enrich localization_tbl hete
- (Uncertain
+ enrich localization_tbl hete exn
+ ~f:(fun _ ->
(lazy ("The term " ^
CicMetaSubst.ppterm_in_context subst hete
context ^ " has type " ^
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context ^
- "\nReason: " ^ Printexc.to_string exn))) exn
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Printexc.to_string exn*)))) exn
(* }}} end coercion stuff *)
in
eat_prods_and_args pristinemenv metasenv subst context pristinehe he
in
(* first we check if we are in the simple case of a meta closed term *)
let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
- if CicUtil.is_meta_closed hetype then
+ if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
(* this optimization is to postpone fix_arity (the most common case)*)
subst,metasenv,ugraph,hetype,he,args_bo_and_ty
else
merge_coercions ctx t
;;
+let pack_coercion_metasenv conjectures =
+ let module C = Cic in
+ List.map
+ (fun (i, ctx, ty) ->
+ let ctx =
+ List.fold_right
+ (fun item ctx ->
+ let item' =
+ match item with
+ Some (name, C.Decl t) ->
+ Some (name, C.Decl (pack_coercion conjectures ctx t))
+ | Some (name, C.Def (t,None)) ->
+ Some (name,C.Def (pack_coercion conjectures ctx t,None))
+ | Some (name, C.Def (t,Some ty)) ->
+ Some (name, C.Def (pack_coercion conjectures ctx t,
+ Some (pack_coercion conjectures ctx ty)))
+ | None -> None
+ in
+ item'::ctx
+ ) ctx []
+ in
+ ((i,ctx,pack_coercion conjectures ctx ty))
+ ) conjectures
+;;
+
let pack_coercion_obj obj =
let module C = Cic in
match obj with
let ty = pack_coercion [] [] ty in
C.Variable (name, body, ty, params, attrs)
| C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
- let conjectures =
- List.map
- (fun (i, ctx, ty) ->
- let ctx =
- List.fold_right
- (fun item ctx ->
- let item' =
- match item with
- Some (name, C.Decl t) ->
- Some (name, C.Decl (pack_coercion conjectures ctx t))
- | Some (name, C.Def (t,None)) ->
- Some (name,C.Def (pack_coercion conjectures ctx t,None))
- | Some (name, C.Def (t,Some ty)) ->
- Some (name, C.Def (pack_coercion conjectures ctx t,
- Some (pack_coercion conjectures ctx ty)))
- | None -> None
- in
- item'::ctx
- ) ctx []
- in
- ((i,ctx,pack_coercion conjectures ctx ty))
- ) conjectures
- in
+ let conjectures = pack_coercion_metasenv conjectures in
let body = pack_coercion conjectures [] body in
let ty = pack_coercion conjectures [] ty in
C.CurrentProof (name, conjectures, body, ty, params, attrs)