diff options
Diffstat (limited to 'plugins/subtac/subtac_coercion.ml')
-rw-r--r-- | plugins/subtac/subtac_coercion.ml | 107 |
1 files changed, 59 insertions, 48 deletions
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 74f31a90..eb29bd04 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -27,6 +27,9 @@ open Subtac_errors open Eterm open Pp +let app_opt env evars f t = + whd_betaiota !evars (app_opt f t) + let pair_of_array a = (a.(0), a.(1)) let make_name s = Name (id_of_string s) @@ -80,7 +83,8 @@ module Coercion = struct | Type _, Prop Null -> Prop Null | _, Type _ -> s2 - let hnf env isevars c = whd_betadeltaiota env ( !isevars) c + let hnf env isevars c = whd_betadeltaiota env isevars c + let hnf_nodelta env evars c = whd_betaiota evars c let lift_args n sign = let rec liftrec k = function @@ -90,15 +94,16 @@ module Coercion = struct liftrec (List.length sign) sign let rec mu env isevars t = - let isevars = ref isevars in let rec aux v = - let v = hnf env isevars v in + let v = hnf env !isevars v in match disc_subset v with Some (u, p) -> let f, ct = aux u in + let p = hnf env !isevars p in (Some (fun x -> - app_opt f (mkApp ((delayed_force sig_).proj1, - [| u; p; x |]))), + app_opt env isevars + f (mkApp ((delayed_force sig_).proj1, + [| u; p; x |]))), ct) | None -> (None, v) in aux t @@ -106,9 +111,8 @@ module Coercion = struct and coerce loc env isevars (x : Term.constr) (y : Term.constr) : (Term.constr -> Term.constr) option = - let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in let rec coerce_unify env x y = - let x = hnf env isevars x and y = hnf env isevars y in + let x = hnf env !isevars x and y = hnf env !isevars y in try isevars := the_conv_x_leq env x y !isevars; None @@ -167,7 +171,7 @@ module Coercion = struct let env' = push_rel (name', None, 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 c1 (mkRel 1) in + let coec1 = app_opt env' isevars c1 (mkRel 1) in (* env, x : a' |- c1[x] : lift 1 a *) let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in (* env, x : a' |- c2 : b[c1[x]/x]] > b' *) @@ -177,7 +181,7 @@ module Coercion = struct Some (fun f -> mkLambda (name', a', - app_opt c2 + app_opt env' isevars c2 (mkApp (Term.lift 1 f, [| coec1 |]))))) | App (c, l), App (c', l') -> @@ -220,9 +224,9 @@ module Coercion = struct Some (fun x -> let x, y = - app_opt c1 (mkApp (existS.proj1, + app_opt env' isevars c1 (mkApp (existS.proj1, [| a; pb; x |])), - app_opt c2 (mkApp (existS.proj2, + app_opt env' isevars c2 (mkApp (existS.proj2, [| a; pb; x |])) in mkApp (existS.intro, [| a'; pb'; x ; y |])) @@ -240,9 +244,9 @@ module Coercion = struct Some (fun x -> let x, y = - app_opt c1 (mkApp (prod.proj1, + app_opt env isevars c1 (mkApp (prod.proj1, [| a; b; x |])), - app_opt c2 (mkApp (prod.proj2, + app_opt env isevars c2 (mkApp (prod.proj2, [| a; b; x |])) in mkApp (prod.intro, [| a'; b'; x ; y |])) @@ -276,7 +280,7 @@ module Coercion = struct Some (u, p) -> let c = coerce_unify env u y in let f x = - app_opt c (mkApp ((delayed_force sig_).proj1, + app_opt env isevars c (mkApp ((delayed_force sig_).proj1, [| u; p; x |])) in Some f | None -> @@ -285,7 +289,7 @@ module Coercion = struct let c = coerce_unify env x u in Some (fun x -> - let cx = app_opt c x in + let cx = app_opt env isevars c x in let evar = make_existential loc env isevars (mkApp (p, [| cx |])) in (mkApp @@ -300,7 +304,8 @@ module Coercion = struct let coerce_itf loc env isevars v t c1 = let evars = ref isevars in let coercion = coerce loc env evars t c1 in - !evars, Option.map (app_opt coercion) v + let t = Option.map (app_opt env evars coercion) v in + !evars, t (* Taken from pretyping/coercion.ml *) @@ -354,34 +359,36 @@ module Coercion = struct with _ -> anomaly "apply_coercion" let inh_app_fun env isevars j = - let t = whd_betadeltaiota env ( isevars) j.uj_type in + let isevars = ref isevars in + let t = hnf env !isevars j.uj_type in match kind_of_term t with - | Prod (_,_,_) -> (isevars,j) - | Evar ev when not (is_defined_evar isevars ev) -> - let (isevars',t) = define_evar_as_product isevars ev in + | Prod (_,_,_) -> (!isevars,j) + | Evar ev when not (is_defined_evar !isevars ev) -> + let (isevars',t) = define_evar_as_product !isevars ev in (isevars',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try let t,p = - lookup_path_to_fun_from env ( isevars) j.uj_type in - (isevars,apply_coercion env ( isevars) p j t) + lookup_path_to_fun_from env !isevars j.uj_type in + (!isevars,apply_coercion env !isevars p j t) with Not_found -> try let coercef, t = mu env isevars t in - (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t }) + let res = { uj_val = app_opt env isevars coercef j.uj_val; uj_type = t } in + (!isevars, res) with NoSubtacCoercion | NoCoercion -> - (isevars,j)) + (!isevars,j)) let inh_tosort_force loc env isevars j = try let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in let j1 = apply_coercion env ( isevars) p j t in - (isevars,type_judgment env (j_nf_evar ( isevars) j1)) + (isevars, type_judgment env (j_nf_evar ( isevars) j1)) with Not_found -> error_not_a_type_loc loc env ( isevars) j let inh_coerce_to_sort loc env isevars j = - let typ = whd_betadeltaiota env ( isevars) j.uj_type in + let typ = hnf env isevars j.uj_type in match kind_of_term typ with | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined_evar isevars ev) -> @@ -391,15 +398,19 @@ module Coercion = struct inh_tosort_force loc env isevars j let inh_coerce_to_base loc env isevars j = - let typ = whd_betadeltaiota env ( isevars) j.uj_type in + let isevars = ref isevars in + let typ = hnf env !isevars j.uj_type in let ct, typ' = mu env isevars typ in - isevars, { uj_val = app_opt ct j.uj_val; - uj_type = typ' } + let res = + { uj_val = app_opt env isevars ct j.uj_val; + uj_type = typ' } + in !isevars, res let inh_coerce_to_prod loc env isevars t = - let typ = whd_betadeltaiota env ( isevars) (snd t) in + let isevars = ref isevars in + let typ = hnf env !isevars (snd t) in let _, typ' = mu env isevars typ in - isevars, (fst t, typ') + !isevars, (fst t, typ') let inh_coerce_to_fail env evd rigidonly v t c1 = if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) @@ -452,23 +463,23 @@ module Coercion = struct (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) = match n with - None -> - let (evd', val') = - try - inh_conv_coerce_to_fail loc env evd rigidonly - (Some (nf_evar evd cj.uj_val)) - (nf_evar evd cj.uj_type) (nf_evar evd t) - with NoCoercion -> - let sigma = evd in - try - coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t - with NoSubtacCoercion -> - error_actual_type_loc loc env sigma cj t - in - let val' = match val' with Some v -> v | None -> assert(false) in - (evd',{ uj_val = val'; uj_type = t }) - | Some (init, cur) -> - (evd, cj) + | None -> + let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type } + and t = hnf_nodelta env evd t in + let (evd', val') = + try + inh_conv_coerce_to_fail loc env evd rigidonly + (Some cj.uj_val) cj.uj_type t + with NoCoercion -> + (try + coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t + with NoSubtacCoercion -> + error_actual_type_loc loc env evd cj t) + in + let val' = match val' with Some v -> v | None -> assert(false) in + (evd',{ uj_val = val'; uj_type = t }) + | Some (init, cur) -> + (evd, cj) let inh_conv_coerce_to = inh_conv_coerce_to_gen false let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true |