diff options
| -rw-r--r-- | dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh | 6 | ||||
| -rw-r--r-- | pretyping/cases.ml | 5 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 611 | ||||
| -rw-r--r-- | pretyping/program.ml | 7 | ||||
| -rw-r--r-- | pretyping/program.mli | 3 |
5 files changed, 316 insertions, 316 deletions
diff --git a/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh b/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh new file mode 100644 index 0000000000..87dad61dbc --- /dev/null +++ b/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10204" ] || [ "$CI_BRANCH" = "rm-unsafe-type-of-coercion" ]; then + + paramcoq_CI_REF=fix-papp + paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq + +fi diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 29d6726262..abc16f621e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2126,11 +2126,6 @@ let eq_id avoid id = let hid' = next_ident_away hid avoid in hid' -let papp sigma gr args = - let evdref = ref sigma in - let ans = papp evdref gr args in - !evdref, ans - let mk_eq sigma typ x y = papp sigma coq_eq_ind [| typ; x ; y |] let mk_eq_refl sigma typ x = papp sigma coq_eq_refl [| typ; x |] let mk_JMeq sigma typ x typ' y = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index c4aa3479bf..62bc27cd3c 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -92,19 +92,23 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 = open Program -let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c = +let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env sigma c = let src = Loc.tag ?loc (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define opaque; Evar_kinds.qm_name=na; }) in - let evd, v = Evarutil.new_evar env !evdref ~src c in - let evd = Evd.set_obligation_evar evd (fst (destEvar evd v)) in - evdref := evd; - v - -let app_opt env evdref f t = - whd_betaiota !evdref (app_opt f t) + let sigma, v = Evarutil.new_evar env sigma ~src c in + let sigma = Evd.set_obligation_evar sigma (fst (destEvar sigma v)) in + sigma, v + +let app_opt env sigma f t = + let sigma, t = + match f with + | None -> sigma, t + | Some f -> f sigma t + in + sigma, whd_betaiota sigma t let pair_of_array a = (a.(0), a.(1)) @@ -125,8 +129,8 @@ let disc_subset sigma x = exception NoSubtacCoercion -let hnf env evd c = whd_all env evd c -let hnf_nodelta env evd c = whd_betaiota evd c +let hnf env sigma c = whd_all env sigma c +let hnf_nodelta env sigma c = whd_betaiota sigma c let lift_args n sign = let rec liftrec k = function @@ -135,222 +139,219 @@ let lift_args n sign = in liftrec (List.length sign) sign -let coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) - : (EConstr.constr -> EConstr.constr) option - = +let coerce ?loc env sigma (x : EConstr.constr) (y : EConstr.constr) + : evar_map * (evar_map -> EConstr.constr -> evar_map * EConstr.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 - evdref := Evarconv.unify_leq_delay env !evdref x y; - None - with UnableToUnify _ -> coerce' env x y - and coerce' env x y : (EConstr.constr -> EConstr.constr) option = - let subco () = subset_coerce env evdref x y in + let rec coerce_unify env sigma x y = + let x = hnf env sigma x and y = hnf env sigma y in + try + (Evarconv.unify_leq_delay env sigma x y, None) + with UnableToUnify _ -> coerce' env sigma x y + and coerce' env sigma x y : evar_map * (evar_map -> EConstr.constr -> evar_map * EConstr.constr) option = + let subco sigma = subset_coerce env sigma x y in let dest_prod c = - match Reductionops.splay_prod_n env (!evdref) 1 c with + match Reductionops.splay_prod_n env sigma 1 c with | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, t), c | _ -> raise NoSubtacCoercion in - let coerce_application typ typ' c c' l l' = + let coerce_application sigma typ typ' c c' l l' = let len = Array.length l in - let rec aux tele typ typ' i co = + let rec aux sigma tele typ typ' i co = if i < len then let hdx = l.(i) and hdy = l'.(i) in - try evdref := unify_leq_delay env !evdref hdx hdy; - let (n, eqT), restT = dest_prod typ in - let (n', eqT'), restT' = dest_prod typ' in - aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co - with UnableToUnify _ -> - let (n, eqT), restT = dest_prod typ in - let (n', eqT'), restT' = dest_prod typ' in - let () = - try evdref := unify_leq_delay env !evdref eqT eqT' - with UnableToUnify _ -> raise NoSubtacCoercion - in - (* Disallow equalities on arities *) - if Reductionops.is_arity env !evdref eqT then raise NoSubtacCoercion; - let restargs = lift_args 1 - (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) - in - let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in - let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in - let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in - let evar = make_existential ?loc n.binder_name env evdref eq in - let eq_app x = papp evdref coq_eq_rect - [| eqT; hdx; pred; x; hdy; evar|] - in - aux (hdy :: tele) (subst1 hdx restT) - (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) - else Some (fun x -> - let term = co x in - let sigma, term = Typing.solve_evars env !evdref term in - evdref := sigma; term) + try + let sigma = unify_leq_delay env sigma hdx hdy in + let (n, eqT), restT = dest_prod typ in + let (n', eqT'), restT' = dest_prod typ' in + aux sigma (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co + with UnableToUnify _ -> + let (n, eqT), restT = dest_prod typ in + let (n', eqT'), restT' = dest_prod typ' in + let sigma = + try + unify_leq_delay env sigma eqT eqT' + with UnableToUnify _ -> raise NoSubtacCoercion + in + (* Disallow equalities on arities *) + if Reductionops.is_arity env sigma eqT then raise NoSubtacCoercion; + let restargs = lift_args 1 + (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) + in + let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in + let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in + let sigma, eq = papp sigma coq_eq_ind [| eqT; hdx; hdy |] in + let sigma, evar = make_existential ?loc n.binder_name env sigma eq in + let eq_app sigma x = papp sigma coq_eq_rect + [| eqT; hdx; pred; x; hdy; evar|] + in + aux sigma (hdy :: tele) (subst1 hdx restT) + (subst1 hdy restT') (succ i) (fun sigma x -> let sigma, x = co sigma x in eq_app sigma x) + else + sigma, Some (fun sigma x -> + let sigma, term = co sigma x in + let sigma, term = Typing.solve_evars env sigma term in + sigma, term) in - if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then - (* Second-order unification needed. *) - raise NoSubtacCoercion; - aux [] typ typ' 0 (fun x -> x) + if isEvar sigma c || isEvar sigma c' || not (Program.is_program_generalized_coercion ()) then + (* Second-order unification needed. *) + raise NoSubtacCoercion; + aux sigma [] typ typ' 0 (fun sigma x -> sigma, x) in - match (EConstr.kind !evdref x, EConstr.kind !evdref y) with - | Sort s, Sort s' -> - (match ESorts.kind !evdref s, ESorts.kind !evdref s' with - | Prop, Prop | Set, Set -> None - | (Prop | Set), Type _ -> None - | Type x, Type y when Univ.Universe.equal x y -> None (* false *) - | _ -> subco ()) - | Prod (name, a, b), Prod (name', a', b') -> - let name' = - {name' with - binder_name = - Name (Namegen.next_ident_away - Namegen.default_dependent_ident (Termops.vars_of_env 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 - (* 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' *) - (match c1, c2 with - | None, None -> None - | _, _ -> - Some - (fun f -> - mkLambda (name', a', - app_opt env' evdref c2 - (mkApp (lift 1 f, [| coec1 |]))))) - - | App (c, l), App (c', l') -> - (match EConstr.kind !evdref c, EConstr.kind !evdref c' with - Ind (i, u), Ind (i', u') -> (* Inductive types *) - let len = Array.length l in - let sigT = delayed_force sigT_typ in - let prod = delayed_force prod_typ in - (* Sigma types *) - if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i' - && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod)) - then - if eq_ind i (destIndRef sigT) - then - begin - let (a, pb), (a', pb') = - pair_of_array l, pair_of_array l' - in - let c1 = coerce_unify env a a' in - let remove_head a c = - match EConstr.kind !evdref c with - | Lambda (n, t, t') -> c, t' - | Evar (k, args) -> - let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in - evdref := evs; - let (n, dom, rng) = destLambda !evdref t in - if isEvar !evdref dom then - let (domk, args) = destEvar !evdref dom in - evdref := define domk a !evdref; - else (); - t, rng - | _ -> raise NoSubtacCoercion - in - let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in - let ra = Retyping.relevance_of_type env !evdref a in - let env' = push_rel - (LocalAssum (make_annot (Name Namegen.default_dependent_ident) ra, a)) - env - in - let c2 = coerce_unify env' b b' in - match c1, c2 with - | None, None -> None - | _, _ -> - Some - (fun x -> - let x, y = - app_opt env' evdref c1 (papp evdref sigT_proj1 - [| a; pb; x |]), - app_opt env' evdref c2 (papp evdref sigT_proj2 - [| a; pb; x |]) - in - papp evdref sigT_intro [| a'; pb'; x ; y |]) - end - else - begin - let (a, b), (a', b') = - pair_of_array l, pair_of_array l' - in - let c1 = coerce_unify env a a' in - let c2 = coerce_unify env b b' in - match c1, c2 with - | None, None -> None - | _, _ -> - Some - (fun x -> - let x, y = - app_opt env evdref c1 (papp evdref prod_proj1 - [| a; b; x |]), - app_opt env evdref c2 (papp evdref prod_proj2 - [| a; b; x |]) - in - papp evdref prod_intro [| a'; b'; x ; y |]) - end - else - if eq_ind i i' && Int.equal len (Array.length l') then - let evm = !evdref in - (try subco () - with NoSubtacCoercion -> - let typ = Typing.unsafe_type_of env evm c in - let typ' = Typing.unsafe_type_of env evm c' in - coerce_application typ typ' c c' l l') - else - subco () - | x, y when EConstr.eq_constr !evdref c c' -> - if Int.equal (Array.length l) (Array.length l') then - 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 - coerce_application lam_type lam_type' c c' l l' - else subco () - | _ -> subco ()) - | _, _ -> subco () - - and subset_coerce env evdref x y = - match disc_subset !evdref x with - Some (u, p) -> - let c = coerce_unify env u y in - let f x = - app_opt env evdref c (papp evdref sig_proj1 [| u; p; x |]) - in Some f + match (EConstr.kind sigma x, EConstr.kind sigma y) with + | Sort s, Sort s' -> + (match ESorts.kind sigma s, ESorts.kind sigma s' with + | Prop, Prop | Set, Set -> sigma, None + | (Prop | Set), Type _ -> sigma, None + | Type x, Type y when Univ.Universe.equal x y -> sigma, None (* false *) + | _ -> subco sigma) + | Prod (name, a, b), Prod (name', a', b') -> + let name' = + {name' with + binder_name = + Name (Namegen.next_ident_away + Namegen.default_dependent_ident (Termops.vars_of_env env))} + in + let env' = push_rel (LocalAssum (name', a')) env in + let sigma, c1 = coerce_unify env' sigma (lift 1 a') (lift 1 a) in + (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) + let sigma, coec1 = app_opt env' sigma c1 (mkRel 1) in + (* env, x : a' |- c1[x] : lift 1 a *) + let sigma, c2 = coerce_unify env' sigma (subst1 coec1 (liftn 1 2 b)) b' in + (* env, x : a' |- c2 : b[c1[x]/x]] > b' *) + (match c1, c2 with + | None, None -> sigma, None + | _, _ -> + sigma, + Some (fun sigma f -> + let sigma, t = app_opt env' sigma c2 + (mkApp (lift 1 f, [| coec1 |])) in + sigma, mkLambda (name', a', t))) + + | App (c, l), App (c', l') -> + (match EConstr.kind sigma c, EConstr.kind sigma c' with + Ind (i, u), Ind (i', u') -> (* Inductive types *) + let len = Array.length l in + let sigT = delayed_force sigT_typ in + let prod = delayed_force prod_typ in + (* Sigma types *) + if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i' + && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod)) + then + if eq_ind i (destIndRef sigT) + then + begin + let (a, pb), (a', pb') = + pair_of_array l, pair_of_array l' + in + let sigma, c1 = coerce_unify env sigma a a' in + let remove_head sigma a c = + match EConstr.kind sigma c with + | Lambda (n, t, t') -> sigma, (c, t') + | Evar (k, args) -> + let (sigma, t) = Evardefine.define_evar_as_lambda env sigma (k,args) in + let (n, dom, rng) = destLambda sigma t in + let sigma = + if isEvar sigma dom then + let (domk, args) = destEvar sigma dom in + define domk a sigma + else sigma + in + sigma, (t, rng) + | _ -> raise NoSubtacCoercion + in + let sigma, (pb, b) = remove_head sigma a pb in + let sigma, (pb', b') = remove_head sigma a' pb' in + let ra = Retyping.relevance_of_type env sigma a in + let env' = push_rel + (LocalAssum (make_annot (Name Namegen.default_dependent_ident) ra, a)) + env + in + let sigma, c2 = coerce_unify env' sigma b b' in + match c1, c2 with + | None, None -> sigma, None + | _, _ -> + sigma, + Some (fun sigma x -> + let sigma, t1 = papp sigma sigT_proj1 [| a; pb; x |] in + let sigma, t2 = papp sigma sigT_proj2 [| a; pb; x |] in + let sigma, x = app_opt env' sigma c1 t1 in + let sigma, y = app_opt env' sigma c2 t2 in + papp sigma sigT_intro [| a'; pb'; x ; y |]) + end + else + begin + let (a, b), (a', b') = + pair_of_array l, pair_of_array l' + in + let sigma, c1 = coerce_unify env sigma a a' in + let sigma, c2 = coerce_unify env sigma b b' in + match c1, c2 with + | None, None -> sigma, None + | _, _ -> + sigma, + Some (fun sigma x -> + let sigma, t1 = papp sigma prod_proj1 [| a; b; x |] in + let sigma, t2 = papp sigma prod_proj2 [| a; b; x |] in + let sigma, x = app_opt env sigma c1 t1 in + let sigma, y = app_opt env sigma c2 t2 in + papp sigma prod_intro [| a'; b'; x ; y |]) + end + else + if eq_ind i i' && Int.equal len (Array.length l') then + (try subco sigma + with NoSubtacCoercion -> + let sigma, typ = Typing.type_of env sigma c in + let sigma, typ' = Typing.type_of env sigma c' in + coerce_application sigma typ typ' c c' l l') + else + subco sigma + | x, y when EConstr.eq_constr sigma c c' -> + if Int.equal (Array.length l) (Array.length l') then + let sigma, lam_type = Typing.type_of env sigma c in + let sigma, lam_type' = Typing.type_of env sigma c' in + coerce_application sigma lam_type lam_type' c c' l l' + else subco sigma + | _ -> subco sigma) + | _, _ -> subco sigma + + and subset_coerce env sigma x y = + match disc_subset sigma x with + Some (u, p) -> + let sigma, c = coerce_unify env sigma u y in + let f sigma x = + let sigma, t = papp sigma sig_proj1 [| u; p; x |] in + app_opt env sigma c t + in sigma, Some f | None -> - match disc_subset !evdref y with + match disc_subset sigma y with Some (u, p) -> - let c = coerce_unify env x u in - Some - (fun x -> - let cx = app_opt env evdref c x in - let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |])) - in - (papp evdref sig_intro [| u; p; cx; evar |])) - | None -> - raise NoSubtacCoercion - in coerce_unify env x y - -let app_coercion env evdref coercion v = + let sigma, c = coerce_unify env sigma x u in + sigma, Some + (fun sigma x -> + let sigma, cx = app_opt env sigma c x in + let sigma, evar = make_existential ?loc Anonymous env sigma (mkApp (p, [| cx |])) + in + (papp sigma sig_intro [| u; p; cx; evar |])) + | None -> + raise NoSubtacCoercion + in coerce_unify env sigma x y + +let app_coercion env sigma coercion v = match coercion with - | None -> v + | None -> sigma, v | Some f -> - let sigma, v' = Typing.solve_evars env !evdref (f v) in - evdref := sigma; - whd_betaiota !evdref v' + let sigma, v' = f sigma v in + let sigma, v' = Typing.solve_evars env sigma v' in + sigma, whd_betaiota sigma 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 = app_coercion env evdref coercion v in - !evdref, t +let coerce_itf ?loc env sigma v t c1 = + let sigma, coercion = coerce ?loc env sigma t c1 in + app_coercion env sigma coercion v -let saturate_evd env evd = +let saturate_evd env sigma = Typeclasses.resolve_typeclasses - ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd + ~filter:Typeclasses.no_goals ~split:true ~fail:false env sigma type coercion_trace = | IdCoe @@ -388,7 +389,7 @@ let rec reapply_coercions sigma trace c = match trace with (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = - let j,t,trace,evd = + let j,t,trace,sigma = List.fold_left (fun (ja,typ_cl,trace,sigma) i -> let isid = i.coe_is_identity in @@ -415,129 +416,126 @@ let apply_coercion env sigma p hj typ_cl = in jres, jres.uj_type, trace, sigma) (hj,typ_cl,IdCoe,sigma) p - in evd, j, trace + in sigma, j, trace -let mu env evdref t = +let mu env sigma t = let rec aux v = - let v' = hnf env !evdref v in - match disc_subset !evdref v' with + let v' = hnf env sigma v in + match disc_subset sigma v' with | Some (u, p) -> - let f, ct, trace = aux u in - let p = hnf_nodelta env !evdref p in + let sigma, (f, ct, trace) = aux u in + let p = hnf_nodelta env sigma p in let p1 = delayed_force sig_proj1 in - let evd, p1 = Evarutil.new_global !evdref p1 in - evdref := evd; - (Some (fun x -> - app_opt env evdref + let sigma, p1 = Evarutil.new_global sigma p1 in + sigma, + (Some (fun sigma x -> + app_opt env sigma f (mkApp (p1, [| u; p; x |]))), ct, Coe {head=p1; args=[u;p]; previous=trace}) - | None -> (None, v, IdCoe) + | None -> sigma, (None, v, IdCoe) in aux t (* Try to coerce to a funclass; raise NoCoercion if not possible *) -let inh_app_fun_core ~program_mode env evd j = - let t = whd_all env evd j.uj_type in - match EConstr.kind evd t with - | Prod _ -> (evd,j,IdCoe) +let inh_app_fun_core ~program_mode env sigma j = + let t = whd_all env sigma j.uj_type in + match EConstr.kind sigma t with + | Prod _ -> (sigma,j,IdCoe) | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product env evd ev in - (evd',{ uj_val = j.uj_val; uj_type = t },IdCoe) + let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in + (sigma,{ uj_val = j.uj_val; uj_type = t },IdCoe) | _ -> try let t,p = - lookup_path_to_fun_from env evd j.uj_type in - apply_coercion env evd p j t + lookup_path_to_fun_from env sigma j.uj_type in + apply_coercion env sigma p j t with Not_found | NoCoercion -> if program_mode then try - let evdref = ref evd in - let coercef, t, trace = mu env evdref t in - let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in - (!evdref, res, trace) + let sigma, (coercef, t, trace) = mu env sigma t in + let sigma, uj_val = app_opt env sigma coercef j.uj_val in + let res = { uj_val ; uj_type = t } in + (sigma, res, trace) with NoSubtacCoercion | NoCoercion -> - (evd,j,IdCoe) + (sigma,j,IdCoe) else raise NoCoercion (* Try to coerce to a funclass; returns [j] if no coercion is applicable *) -let inh_app_fun ~program_mode resolve_tc env evd j = - try inh_app_fun_core ~program_mode env evd j +let inh_app_fun ~program_mode resolve_tc env sigma j = + try inh_app_fun_core ~program_mode env sigma j with | NoCoercion when not resolve_tc - || not (get_use_typeclasses_for_conversion ()) -> (evd, j, IdCoe) + || not (get_use_typeclasses_for_conversion ()) -> (sigma, j, IdCoe) | NoCoercion -> - try inh_app_fun_core ~program_mode env (saturate_evd env evd) j - with NoCoercion -> (evd, j, IdCoe) + try inh_app_fun_core ~program_mode env (saturate_evd env sigma) j + with NoCoercion -> (sigma, j, IdCoe) let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind sigma s } | _ -> error_not_a_type env sigma j -let inh_tosort_force ?loc env evd j = +let inh_tosort_force ?loc env sigma j = try - let t,p = lookup_path_to_sort_from env evd j.uj_type in - let evd,j1,_trace = apply_coercion env evd p j t in - let j2 = Environ.on_judgment_type (whd_evar evd) j1 in - (evd,type_judgment env evd j2) + let t,p = lookup_path_to_sort_from env sigma j.uj_type in + let sigma,j1,_trace = apply_coercion env sigma p j t in + let j2 = Environ.on_judgment_type (whd_evar sigma) j1 in + (sigma,type_judgment env sigma j2) with Not_found | NoCoercion -> - error_not_a_type ?loc env evd j + error_not_a_type ?loc env sigma j -let inh_coerce_to_sort ?loc env evd j = - let typ = whd_all env evd j.uj_type in - match EConstr.kind evd typ with - | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = ESorts.kind evd s }) +let inh_coerce_to_sort ?loc env sigma j = + let typ = whd_all env sigma j.uj_type in + match EConstr.kind sigma typ with + | Sort s -> (sigma,{ utj_val = j.uj_val; utj_type = ESorts.kind sigma s }) | Evar ev -> - let (evd',s) = Evardefine.define_evar_as_sort env evd ev in - (evd',{ utj_val = j.uj_val; utj_type = s }) + let (sigma,s) = Evardefine.define_evar_as_sort env sigma ev in + (sigma,{ utj_val = j.uj_val; utj_type = s }) | _ -> - inh_tosort_force ?loc env evd j + inh_tosort_force ?loc env sigma j -let inh_coerce_to_base ?loc ~program_mode env evd j = +let inh_coerce_to_base ?loc ~program_mode env sigma j = if program_mode then - let evdref = ref evd in - let ct, typ', trace = mu env evdref j.uj_type in - let res = - { uj_val = (app_coercion env evdref ct j.uj_val); - uj_type = typ' } - in !evdref, res - else (evd, j) - -let inh_coerce_to_prod ?loc ~program_mode env evd t = + let sigma, (ct, typ', _trace) = mu env sigma j.uj_type in + let sigma, uj_val = app_coercion env sigma ct j.uj_val in + let res = { uj_val; uj_type = typ' } in + sigma, res + else (sigma, j) + +let inh_coerce_to_prod ?loc ~program_mode env sigma t = if program_mode then - let evdref = ref evd in - let _, typ', _trace = mu env evdref t in - !evdref, typ' - else (evd, t) + let sigma, (_, typ', _trace) = mu env sigma t in + sigma, typ' + else (sigma, t) -let inh_coerce_to_fail flags env evd rigidonly v t c1 = +let inh_coerce_to_fail flags env sigma rigidonly v t c1 = if rigidonly && not (Heads.is_rigid env (EConstr.Unsafe.to_constr c1) && Heads.is_rigid env (EConstr.Unsafe.to_constr t)) then raise NoCoercion else - let evd, v', t', trace = + let sigma, v', t', trace = try - let t2,t1,p = lookup_path_between env evd (t,c1) in - let evd,j,trace = - apply_coercion env evd p + let t2,t1,p = lookup_path_between env sigma (t,c1) in + let sigma,j,trace = + apply_coercion env sigma p {uj_val = v; uj_type = t} t2 in - evd, j.uj_val, j.uj_type, trace + sigma, j.uj_val, j.uj_type, trace with Not_found -> raise NoCoercion in - try (unify_leq_delay ~flags env evd t' c1, v', trace) + try (unify_leq_delay ~flags env sigma t' c1, v', trace) with UnableToUnify _ -> raise NoCoercion let default_flags_of env = default_flags_of TransparentState.full -let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 = - try (unify_leq_delay ~flags env evd t c1, v, IdCoe) - with UnableToUnify (best_failed_evd,e) -> - try inh_coerce_to_fail flags env evd rigidonly v t c1 +let rec inh_conv_coerce_to_fail ?loc env sigma ?(flags=default_flags_of env) rigidonly v t c1 = + try (unify_leq_delay ~flags env sigma t c1, v, IdCoe) + with UnableToUnify (best_failed_sigma,e) -> + try inh_coerce_to_fail flags env sigma rigidonly v t c1 with NoCoercion -> match - EConstr.kind evd (whd_all env evd t), - EConstr.kind evd (whd_all env evd c1) + EConstr.kind sigma (whd_all env sigma t), + EConstr.kind sigma (whd_all env sigma c1) with | Prod (name,t1,t2), Prod (_,u1,u2) -> (* Conversion did not work, we may succeed with a coercion. *) @@ -551,45 +549,46 @@ let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigid | na -> na) name in let open Context.Rel.Declaration in let env1 = push_rel (LocalAssum (name,u1)) env in - let (evd', v1, trace1) = - inh_conv_coerce_to_fail ?loc env1 evd rigidonly + let (sigma, v1, trace1) = + inh_conv_coerce_to_fail ?loc env1 sigma rigidonly (mkRel 1) (lift 1 u1) (lift 1 t1) in - let v2 = beta_applist evd' (lift 1 v,[v1]) in - let t2 = Retyping.get_type_of env1 evd' v2 in - let (evd'',v2',trace2) = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in + let v2 = beta_applist sigma (lift 1 v,[v1]) in + let t2 = Retyping.get_type_of env1 sigma v2 in + let (sigma,v2',trace2) = inh_conv_coerce_to_fail ?loc env1 sigma rigidonly v2 t2 u2 in let trace = ProdCoe { na=name; ty=u1; dom=trace1; body=trace2 } in - (evd'', mkLambda (name, u1, v2'), trace) - | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) + (sigma, mkLambda (name, u1, v2'), trace) + | _ -> raise (NoCoercionNoUnifier (best_failed_sigma,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) -let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd cj t = - let (evd', val', otrace) = +let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env sigma cj t = + let (sigma, val', otrace) = try - let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t in - (evd', val', Some trace) - with NoCoercionNoUnifier (best_failed_evd,e) -> + let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc env sigma ~flags rigidonly cj.uj_val cj.uj_type t in + (sigma, val', Some trace) + with NoCoercionNoUnifier (best_failed_sigma,e) -> try if program_mode then - let (evd', val') = coerce_itf ?loc env evd cj.uj_val cj.uj_type t in - (evd', val', None) + let (sigma, val') = coerce_itf ?loc env sigma cj.uj_val cj.uj_type t in + (sigma, val', None) else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) -> - error_actual_type ?loc env best_failed_evd cj t e + error_actual_type ?loc env best_failed_sigma cj t e | NoSubtacCoercion -> - let evd' = saturate_evd env evd in + let sigma' = saturate_evd env sigma in try - if evd' == evd then - error_actual_type ?loc env best_failed_evd cj t e + if sigma' == sigma then + error_actual_type ?loc env best_failed_sigma cj t e else - let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t in - (evd', val', Some trace) - with NoCoercionNoUnifier (_evd,_error) -> - error_actual_type ?loc env best_failed_evd cj t e + let sigma = sigma' in + let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc env sigma rigidonly cj.uj_val cj.uj_type t in + (sigma, val', Some trace) + with NoCoercionNoUnifier (_sigma,_error) -> + error_actual_type ?loc env best_failed_sigma cj t e in - (evd',{ uj_val = val'; uj_type = t },otrace) + (sigma,{ uj_val = val'; uj_type = t },otrace) -let inh_conv_coerce_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = - inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env evd -let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = - inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc true flags env evd +let inh_conv_coerce_to ?loc ~program_mode resolve_tc env sigma ?(flags=default_flags_of env) = + inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env sigma +let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc env sigma ?(flags=default_flags_of env) = + inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc true flags env sigma diff --git a/pretyping/program.ml b/pretyping/program.ml index 9c478844aa..909ba6e44a 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -11,12 +11,11 @@ open CErrors open Util -let papp evdref r args = +let papp sigma r args = let open EConstr in let gr = delayed_force r in - let evd, hd = Evarutil.new_global !evdref gr in - evdref := evd; - mkApp (hd, args) + let evd, hd = Evarutil.new_global sigma gr in + sigma, mkApp (hd, args) let sig_typ () = Coqlib.lib_ref "core.sig.type" let sig_intro () = Coqlib.lib_ref "core.sig.intro" diff --git a/pretyping/program.mli b/pretyping/program.mli index 6604b3a854..7da0da1297 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -10,6 +10,7 @@ open Names open EConstr +open Evd (** A bunch of Coq constants used by Program *) @@ -38,7 +39,7 @@ val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr (** Polymorphic application of delayed references *) -val papp : Evd.evar_map ref -> (unit -> GlobRef.t) -> constr array -> constr +val papp : evar_map -> (unit -> GlobRef.t) -> constr array -> evar_map * constr val get_proofs_transparency : unit -> bool val is_program_cases : unit -> bool |