diff options
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 176 |
1 files changed, 91 insertions, 85 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 913e80f3..04cb6a59 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Hugo Herbelin for Coq V7 by isolating the coercion @@ -18,10 +20,10 @@ open CErrors open Util open Names open Term +open Environ +open EConstr open Vars open Reductionops -open Environ -open Typeops open Pretype_errors open Classops open Evarutil @@ -33,14 +35,13 @@ open Globnames let use_typeclasses_for_conversion = ref true let _ = - Goptions.declare_bool_option - { Goptions.optsync = true; - optdepr = false; + Goptions.(declare_bool_option + { optdepr = false; optname = "use typeclass resolution during conversion"; optkey = ["Typeclass"; "Resolution"; "For"; "Conversion"]; optread = (fun () -> !use_typeclasses_for_conversion); optwrite = (fun b -> use_typeclasses_for_conversion := b) } - + ) (* Typing operations dealing with coercions *) exception NoCoercion @@ -52,7 +53,7 @@ let apply_coercion_args env evd check isproj argl funj = let rec apply_rec acc typ = function | [] -> if isproj then - let cst = fst (destConst (j_val funj)) in + let cst = fst (destConst !evdref (j_val funj)) in let p = Projection.make cst false in let pb = lookup_projection p env in let args = List.skipn pb.Declarations.proj_npars argl in @@ -63,35 +64,36 @@ 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_all env evd typ) with + match EConstr.kind !evdref (whd_all env !evdref typ) with | Prod (_,c1,c2) -> - if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then + if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then raise NoCoercion; apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly (Pp.str "apply_coercion_args") + | _ -> anomaly (Pp.str "apply_coercion_args.") in let res = apply_rec [] funj.uj_type argl in !evdref, res (* appliquer le chemin de coercions de patterns p *) -let apply_pattern_coercion loc pat p = +let apply_pattern_coercion ?loc pat p = List.fold_left (fun pat (co,n) -> - let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in - Glob_term.PatCstr (loc, co, List.init (n+1) f, Anonymous)) + let f i = + if i<n then (DAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in + DAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous)) pat p (* raise Not_found if no coercion found *) -let inh_pattern_coerce_to loc env pat ind1 ind2 = +let inh_pattern_coerce_to ?loc env pat ind1 ind2 = let p = lookup_pattern_path_between env (ind1,ind2) in - apply_pattern_coercion loc pat p + apply_pattern_coercion ?loc pat p (* Program coercions *) open Program -let make_existential loc ?(opaque = not (get_proofs_transparency ())) env evdref c = - let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in +let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c = + let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in Evarutil.e_new_evar env evdref ~src c let app_opt env evdref f t = @@ -99,10 +101,10 @@ let app_opt env evdref f t = let pair_of_array a = (a.(0), a.(1)) -let disc_subset x = - match kind_of_term x with +let disc_subset sigma x = + match EConstr.kind sigma x with | App (c, l) -> - (match kind_of_term c with + (match EConstr.kind sigma c with Ind (i,_) -> let len = Array.length l in let sigty = delayed_force sig_typ in @@ -129,7 +131,7 @@ let lift_args n sign = let mu env evdref t = let rec aux v = let v' = hnf env !evdref v in - match disc_subset v' with + match disc_subset !evdref v' with | Some (u, p) -> let f, ct = aux u in let p = hnf_nodelta env !evdref p in @@ -140,8 +142,8 @@ let mu env evdref t = | None -> (None, v) in aux t -and coerce loc env evdref (x : Term.constr) (y : Term.constr) - : (Term.constr -> Term.constr) option +and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) + : (EConstr.constr -> EConstr.constr) option = let open Context.Rel.Declaration in let rec coerce_unify env x y = @@ -150,12 +152,11 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) evdref := the_conv_x_leq env x y !evdref; None with UnableToUnify _ -> coerce' env x y - and coerce' env x y : (Term.constr -> Term.constr) option = + and coerce' env x y : (EConstr.constr -> EConstr.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 - | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c + match Reductionops.splay_prod_n env (!evdref) 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' = @@ -175,14 +176,14 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) with UnableToUnify _ -> raise NoSubtacCoercion in (* Disallow equalities on arities *) - if Reduction.is_arity env eqT then raise NoSubtacCoercion; + 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, applistc (lift 1 c) args) 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 env evdref eq in + let evar = make_existential ?loc n env evdref eq in let eq_app x = papp evdref coq_eq_rect [| eqT; hdx; pred; x; hdy; evar|] in @@ -192,21 +193,21 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let term = co x in Typing.e_solve_evars env evdref term) in - if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then + 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) in - match (kind_of_term x, kind_of_term y) with + match (EConstr.kind !evdref x, EConstr.kind !evdref y) with | Sort s, Sort s' -> - (match s, s' with + (match ESorts.kind !evdref s, ESorts.kind !evdref s' with | Prop x, Prop y when x == y -> None | Prop _, 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 (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env)) + 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 @@ -225,7 +226,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) (mkApp (lift 1 f, [| coec1 |]))))) | App (c, l), App (c', l') -> - (match kind_of_term c, kind_of_term c' with + (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 @@ -242,16 +243,15 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) in let c1 = coerce_unify env a a' in let remove_head a c = - match kind_of_term c with + 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 t in - let dom = whd_evar !evdref dom in - if isEvar dom then - let (domk, args) = destEvar dom in - evdref := define domk a !evdref; + let (n, dom, rng) = destLambda !evdref t in + if isEvar !evdref dom then + let (domk, args) = destEvar !evdref dom in + evdref := define domk (EConstr.Unsafe.to_constr a) !evdref; else (); t, rng | _ -> raise NoSubtacCoercion @@ -302,7 +302,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) coerce_application typ typ' c c' l l') else subco () - | x, y when Constr.equal c c' -> + | 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 @@ -313,20 +313,20 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) | _, _ -> subco () and subset_coerce env evdref x y = - match disc_subset x with + 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 | None -> - match disc_subset y with + match disc_subset !evdref 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 env evdref (mkApp (p, [| cx |])) + let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |])) in (papp evdref sig_intro [| u; p; cx; evar |])) | None -> @@ -340,9 +340,9 @@ let app_coercion env evdref coercion v = 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 coerce_itf ?loc env evd v t c1 = let evdref = ref evd in - let coercion = coerce loc env evdref t c1 in + let coercion = coerce ?loc env evdref t c1 in let t = Option.map (app_coercion env evdref coercion) v in !evdref, t @@ -370,12 +370,12 @@ 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 CErrors.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_all env evd j.uj_type in - match kind_of_term t with + match EConstr.kind evd t with | Prod (_,_,_) -> (evd,j) | Evar ev -> let (evd',t) = Evardefine.define_evar_as_product evd ev in @@ -405,36 +405,41 @@ let inh_app_fun resolve_tc env evd j = try inh_app_fun_core env (saturate_evd env evd) j with NoCoercion -> (evd, j) -let inh_tosort_force loc env evd j = +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 = try let t,p = lookup_path_to_sort_from env evd j.uj_type in let evd,j1 = apply_coercion env evd p j t in let j2 = on_judgment_type (whd_evar evd) j1 in - (evd,type_judgment env j2) + (evd,type_judgment env evd j2) with Not_found | NoCoercion -> - error_not_a_type_loc loc env evd j + error_not_a_type ?loc env evd j -let inh_coerce_to_sort loc env evd j = +let inh_coerce_to_sort ?loc env evd j = 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)) -> + match EConstr.kind evd typ with + | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = ESorts.kind evd s }) + | Evar ev -> 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 + inh_tosort_force ?loc env evd j -let inh_coerce_to_base loc env evd j = +let inh_coerce_to_base ?loc env evd j = if Flags.is_program_mode () then let evdref = ref evd in let ct, typ' = mu env evdref j.uj_type in let res = - { uj_val = app_coercion 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) -let inh_coerce_to_prod loc env evd t = +let inh_coerce_to_prod ?loc env evd t = if Flags.is_program_mode () then let evdref = ref evd in let _, typ' = mu env evdref t in @@ -442,7 +447,7 @@ let inh_coerce_to_prod loc env evd t = else (evd, t) let inh_coerce_to_fail env evd rigidonly v t c1 = - if rigidonly && not (Heads.is_rigid env c1 && Heads.is_rigid env t) + 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 @@ -461,71 +466,72 @@ let inh_coerce_to_fail env evd rigidonly v t c1 = try (the_conv_x_leq env t' c1 evd, v') with UnableToUnify _ -> raise NoCoercion -let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = +let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 = try (the_conv_x_leq env t c1 evd, v) with UnableToUnify (best_failed_evd,e) -> try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match - kind_of_term (whd_all env evd t), - kind_of_term (whd_all env evd c1) + EConstr.kind evd (whd_all env evd t), + EConstr.kind evd (whd_all env evd c1) with | Prod (name,t1,t2), Prod (_,u1,u2) -> (* Conversion did not work, we may succeed with a coercion. *) (* We eta-expand (hence possibly modifying the original term!) *) (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *) (* has type forall (x:u1), u2 (with v' recursively obtained) *) - (* Note: we retype the term because sort-polymorphism may have *) - (* weaken its type *) + (* Note: we retype the term because template polymorphism may have *) + (* weakened its type *) let name = match name with | Anonymous -> Name Namegen.default_dependent_ident | _ -> name 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 + inh_conv_coerce_to_fail ?loc env1 evd rigidonly (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in let v1 = Option.get v1 in - let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in + let v2 = Option.map (fun v -> beta_applist evd' (lift 1 v,[v1])) v in let t2 = match v2 with - | None -> subst_term v1 t2 + | None -> subst_term evd' v1 t2 | Some v2 -> Retyping.get_type_of env1 evd' v2 in - let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in + let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) -let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = +let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t = let (evd', val') = try - inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail ?loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (best_failed_evd,e) -> try if Flags.is_program_mode () then - coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t + coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> - error_actual_type_loc loc env best_failed_evd cj t e + error_actual_type ?loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in try if evd' == evd then - error_actual_type_loc loc env best_failed_evd cj t e + error_actual_type ?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 + inh_conv_coerce_to_fail ?loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (_evd,_error) -> - error_actual_type_loc loc env best_failed_evd cj t e + error_actual_type ?loc env best_failed_evd cj t e in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) -let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false -let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true +let inh_conv_coerce_to ?loc resolve_tc = inh_conv_coerce_to_gen ?loc resolve_tc false + +let inh_conv_coerce_rigid_to ?loc resolve_tc = inh_conv_coerce_to_gen resolve_tc ?loc true -let inh_conv_coerces_to loc env evd t t' = +let inh_conv_coerces_to ?loc env evd t t' = try - fst (inh_conv_coerce_to_fail loc env evd true None t t') + fst (inh_conv_coerce_to_fail ?loc env evd true None t t') with NoCoercion -> evd (* Maybe not enough information to unify *) |