From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- pretyping/coercion.ml | 64 ++++++++++++++++++++++++++++----------------------- 1 file changed, 35 insertions(+), 29 deletions(-) (limited to 'pretyping/coercion.ml') diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 489a311b..913e80f3 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -14,7 +14,7 @@ Corbineau, Feb 2008 *) (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *) -open Errors +open CErrors open Util open Names open Term @@ -63,7 +63,7 @@ let apply_coercion_args env evd check isproj argl funj = { uj_val = applist (j_val funj,argl); uj_type = typ } | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *) - match kind_of_term (whd_betadeltaiota env evd typ) with + match kind_of_term (whd_all env evd typ) with | Prod (_,c1,c2) -> if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then raise NoCoercion; @@ -90,8 +90,9 @@ let inh_pattern_coerce_to loc env pat ind1 ind2 = open Program -let make_existential loc ?(opaque = Evar_kinds.Define true) env evdref c = - Evarutil.e_new_evar env evdref ~src:(loc, Evar_kinds.QuestionMark opaque) c +let make_existential loc ?(opaque = not (get_proofs_transparency ())) env evdref c = + let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in + Evarutil.e_new_evar env evdref ~src c let app_opt env evdref f t = whd_betaiota !evdref (app_opt f t) @@ -115,7 +116,7 @@ let disc_subset x = exception NoSubtacCoercion -let hnf env evd c = whd_betadeltaiota env evd c +let hnf env evd c = whd_all env evd c let hnf_nodelta env evd c = whd_betaiota evd c let lift_args n sign = @@ -129,7 +130,7 @@ let mu env evdref t = let rec aux v = let v' = hnf env !evdref v in match disc_subset v' with - Some (u, p) -> + | Some (u, p) -> let f, ct = aux u in let p = hnf_nodelta env !evdref p in (Some (fun x -> @@ -142,6 +143,7 @@ let mu env evdref t = and coerce loc env evdref (x : Term.constr) (y : Term.constr) : (Term.constr -> Term.constr) option = + let open Context.Rel.Declaration in let rec coerce_unify env x y = let x = hnf env !evdref x and y = hnf env !evdref y in try @@ -151,8 +153,9 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env evdref x y in let dest_prod c = + let open Context.Rel.Declaration in match Reductionops.splay_prod_n env ( !evdref) 1 c with - | [(na,b,t)], c -> (na,t), c + | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c | _ -> raise NoSubtacCoercion in let coerce_application typ typ' c c' l l' = @@ -187,9 +190,9 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some (fun x -> let term = co x in - Typing.solve_evars env evdref term) + Typing.e_solve_evars env evdref term) in - if isEvar c || isEvar c' then + if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then (* Second-order unification needed. *) raise NoSubtacCoercion; aux [] typ typ' 0 (fun x -> x) @@ -205,7 +208,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let name' = Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env)) in - let env' = push_rel (name', None, a') env in + let env' = push_rel (LocalAssum (name', a')) env in let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) let coec1 = app_opt env' evdref c1 (mkRel 1) in @@ -241,9 +244,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let remove_head a c = match kind_of_term c with | Lambda (n, t, t') -> c, t' - (*| Prod (n, t, t') -> t'*) | Evar (k, args) -> - let (evs, t) = Evarutil.define_evar_as_lambda env !evdref (k,args) in + let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in evdref := evs; let (n, dom, rng) = destLambda t in let dom = whd_evar !evdref dom in @@ -255,7 +257,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) | _ -> raise NoSubtacCoercion in let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in - let env' = push_rel (Name Namegen.default_dependent_ident, None, a) env in + let env' = push_rel (LocalAssum (Name Namegen.default_dependent_ident, a)) env in let c2 = coerce_unify env' b b' in match c1, c2 with | None, None -> None @@ -278,7 +280,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let c1 = coerce_unify env a a' in let c2 = coerce_unify env b b' in match c1, c2 with - None, None -> None + | None, None -> None | _, _ -> Some (fun x -> @@ -297,9 +299,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) with NoSubtacCoercion -> let typ = Typing.unsafe_type_of env evm c in let typ' = Typing.unsafe_type_of env evm c' in - (* if not (is_arity env evm typ) then *) coerce_application typ typ' c c' l l') - (* else subco () *) else subco () | x, y when Constr.equal c c' -> @@ -307,9 +307,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let evm = !evdref in let lam_type = Typing.unsafe_type_of env evm c in let lam_type' = Typing.unsafe_type_of env evm c' in - (* if not (is_arity env evm lam_type) then ( *) coerce_application lam_type lam_type' c c' l l' - (* ) else subco () *) else subco () | _ -> subco ()) | _, _ -> subco () @@ -335,10 +333,17 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) raise NoSubtacCoercion in coerce_unify env x y +let app_coercion env evdref coercion v = + match coercion with + | None -> v + | Some f -> + let v' = Typing.e_solve_evars env evdref (f v) in + whd_betaiota !evdref v' + let coerce_itf loc env evd v t c1 = let evdref = ref evd in let coercion = coerce loc env evdref t c1 in - let t = Option.map (app_opt env evdref coercion) v in + let t = Option.map (app_coercion env evdref coercion) v in !evdref, t let saturate_evd env evd = @@ -365,15 +370,15 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion") + | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = - let t = whd_betadeltaiota env evd j.uj_type in + let t = whd_all env evd j.uj_type in match kind_of_term t with | Prod (_,_,_) -> (evd,j) | Evar ev -> - let (evd',t) = define_evar_as_product evd ev in + let (evd',t) = Evardefine.define_evar_as_product evd ev in (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> try let t,p = @@ -410,11 +415,11 @@ let inh_tosort_force loc env evd j = error_not_a_type_loc loc env evd j let inh_coerce_to_sort loc env evd j = - let typ = whd_betadeltaiota env evd j.uj_type in + let typ = whd_all env evd j.uj_type in match kind_of_term typ with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined evd (fst ev)) -> - let (evd',s) = define_evar_as_sort env evd ev in + let (evd',s) = Evardefine.define_evar_as_sort env evd ev in (evd',{ utj_val = j.uj_val; utj_type = s }) | _ -> inh_tosort_force loc env evd j @@ -424,7 +429,7 @@ let inh_coerce_to_base loc env evd j = let evdref = ref evd in let ct, typ' = mu env evdref j.uj_type in let res = - { uj_val = app_opt env evdref ct j.uj_val; + { uj_val = app_coercion env evdref ct j.uj_val; uj_type = typ' } in !evdref, res else (evd, j) @@ -462,8 +467,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match - kind_of_term (whd_betadeltaiota env evd t), - kind_of_term (whd_betadeltaiota env evd c1) + kind_of_term (whd_all env evd t), + kind_of_term (whd_all env evd c1) with | Prod (name,t1,t2), Prod (_,u1,u2) -> (* Conversion did not work, we may succeed with a coercion. *) @@ -475,7 +480,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = let name = match name with | Anonymous -> Name Namegen.default_dependent_ident | _ -> name in - let env1 = push_rel (name,None,u1) env in + let open Context.Rel.Declaration in + let env1 = push_rel (LocalAssum (name,u1)) env in let (evd', v1) = inh_conv_coerce_to_fail loc env1 evd rigidonly (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in @@ -508,7 +514,7 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = error_actual_type_loc loc env best_failed_evd cj t e else inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercionNoUnifier (best_failed_evd,e) -> + with NoCoercionNoUnifier (_evd,_error) -> error_actual_type_loc loc env best_failed_evd cj t e in let val' = match val' with Some v -> v | None -> assert(false) in -- cgit v1.2.3