diff options
Diffstat (limited to 'pretyping')
70 files changed, 927 insertions, 767 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 36f35a67c3..a9eb77b239 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,7 +11,6 @@ (*i*) open Names open Globnames -open Term open Constr open Context open Environ @@ -78,14 +77,14 @@ let rename_type ty ref = let rec rename_type_aux c = function | [] -> c | rename :: rest as renamings -> - match kind_of_type c with - | ProdType (old, s, t) -> + match Constr.kind c with + | Prod (old, s, t) -> mkProd (name_override old rename, s, rename_type_aux t rest) - | LetInType(old, s, b, t) -> + | LetIn (old, s, b, t) -> mkLetIn (old ,s, b, rename_type_aux t renamings) - | CastType (t,_) -> rename_type_aux t renamings - | SortType _ -> c - | AtomicType _ -> c in + | Cast (t,_, _) -> rename_type_aux t renamings + | _ -> c + in try rename_type_aux ty (arguments_names ref) with Not_found -> ty diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index f1c84cb63b..fa3b64779b 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aa6ec1c941..fc64022ed4 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -73,11 +73,11 @@ let error_wrong_numarg_inductive ?loc env c n = let list_try_compile f l = let rec aux errors = function - | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors) + | [] -> if errors = [] then anomaly (str "try_find_f.") else Exninfo.iraise (List.last errors) | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> - let e = CErrors.push e in + let e = Exninfo.capture e in aux (e::errors) t in aux [] l @@ -436,7 +436,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = | exception Evarconv.UnableToUnify _ -> sigma, current | sigma -> sigma, current else - let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in + let sigma, j, _trace = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in sigma, j.uj_val in sigma, (current, try_find_ind !!(pb.env) sigma indt names)) @@ -1817,6 +1817,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t = List.rev_append patl patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> let pat,acc = make_patvar t acc in + let typ = lift n typ in let d = LocalAssum (annotR (alias_of_pat pat),typ) in let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env)) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in @@ -1955,8 +1956,12 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon = match tycon with - | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma - ~flags:(default_flags_of TransparentState.full) j p + | Some p -> + let (evd,v,_trace) = + Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma + ~flags:(default_flags_of TransparentState.full) j p + in + (evd,v) | None -> sigma, j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) @@ -2122,11 +2127,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 = @@ -2160,7 +2160,7 @@ let constr_of_pat env sigma arsign pat avoid = let IndType (indf, _) = try find_rectype env sigma (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env sigma - {uj_val = ty; uj_type = Typing.unsafe_type_of env sigma ty} + {uj_val = ty; uj_type = Retyping.get_type_of env sigma ty} in let (ind,u), params = dest_ind_family indf in let params = List.map EConstr.of_constr params in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 3db019d827..8b1ec3aba0 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 2b7ccbbcad..f816599a17 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -196,7 +196,6 @@ let cofixp_reducible flgs _ stk = let get_debug_cbv = Goptions.declare_bool_option_and_ref ~depr:false ~value:false - ~name:"cbv visited constants display" ~key:["Debug";"Cbv"] (* Reduction of primitives *) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 16c4364f17..fdd4370613 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f0e73bdb29..2a844402a8 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -27,7 +27,7 @@ open EConstr open Vars open Reductionops open Pretype_errors -open Classops +open Coercionops open Evarutil open Evarconv open Evd @@ -36,7 +36,6 @@ open Globnames let get_use_typeclasses_for_conversion = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"use typeclass resolution during conversion" ~key:["Typeclass"; "Resolution"; "For"; "Conversion"] ~value:true @@ -93,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)) @@ -126,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 @@ -136,362 +139,403 @@ let lift_args n sign = in liftrec (List.length sign) sign -let mu env evdref t = - let rec aux v = - let v' = hnf env !evdref v in - match disc_subset !evdref v' with - | Some (u, p) -> - let f, ct = aux u in - let p = hnf_nodelta env !evdref p in - (Some (fun x -> - app_opt env evdref - f (papp evdref sig_proj1 [| u; p; x |])), - ct) - | None -> (None, v) - in aux t - -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 + | PrimProjCoe of { + proj : Projection.Repr.t; + args : econstr list; + previous : coercion_trace; + } + | Coe of { + head : econstr; + args : econstr list; + previous : coercion_trace; + } + | ProdCoe of { na : Name.t binder_annot; ty : econstr; dom : coercion_trace; body : coercion_trace } + +let empty_coercion_trace = IdCoe + +(* similar to iterated apply_coercion_args *) +let rec reapply_coercions sigma trace c = match trace with + | IdCoe -> c + | PrimProjCoe { proj; args; previous } -> + let c = reapply_coercions sigma previous c in + let args = args@[c] in + let head, args = match args with [] -> assert false | hd :: tl -> hd, tl in + applist (mkProj (Projection.make proj false, head), args) + | Coe {head; args; previous} -> + let c = reapply_coercions sigma previous c in + let args = args@[c] in + applist (head, args) + | ProdCoe { na; ty; dom; body } -> + let x = reapply_coercions sigma dom (mkRel 1) in + let c = beta_applist sigma (lift 1 c, [x]) in + let c = reapply_coercions sigma body c in + mkLambda (na, ty, c) (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = - let j,t,evd = + let j,t,trace,sigma = List.fold_left - (fun (ja,typ_cl,sigma) i -> + (fun (ja,typ_cl,trace,sigma) i -> let isid = i.coe_is_identity in let isproj = i.coe_is_projection in let sigma, c = new_global sigma i.coe_value in let typ = Retyping.get_type_of env sigma c in let fv = make_judge c typ in - let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in - let sigma, jres = - apply_coercion_args env sigma true isproj argl fv + let argl = class_args_of env sigma typ_cl in + let trace = + if isid then trace + else match isproj with + | None -> Coe {head=fv.uj_val;args=argl;previous=trace} + | Some proj -> + let args = List.skipn (Projection.Repr.npars proj) argl in + PrimProjCoe {proj; args; previous=trace } in - (if isid then + let argl = argl@[ja.uj_val] in + let sigma, jres = apply_coercion_args env sigma true isproj argl fv in + let jres = + if isid then { uj_val = ja.uj_val; uj_type = jres.uj_type } else - jres), - jres.uj_type,sigma) - (hj,typ_cl,sigma) p - in evd, j + jres + in + jres, jres.uj_type, trace, sigma) + (hj,typ_cl,IdCoe,sigma) p + in sigma, j, trace + +let mu env sigma t = + let rec aux v = + let v' = hnf env sigma v in + match disc_subset sigma v' with + | Some (u, p) -> + let sigma, (f, ct, trace) = aux u in + let p = hnf_nodelta env sigma p in + let p1 = delayed_force sig_proj1 in + 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 -> 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) +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 }) + 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 = mu env evdref t in - let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in - (!evdref, res) + 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) + (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) + || 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) + 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 = 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' = 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' = 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' = + let sigma, v', t', trace = try - let t2,t1,p = lookup_path_between env evd (t,c1) in - let evd,j = - 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 + sigma, j.uj_val, j.uj_type, trace with Not_found -> raise NoCoercion in - try (unify_leq_delay ~flags env evd t' c1, v') + 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) - 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. *) @@ -505,41 +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) = - 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') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in - (evd'', mkLambda (name, u1, v2')) - | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) + 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 + (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') = +let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env sigma cj t = + let (sigma, val', otrace) = try - inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t - 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 - coerce_itf ?loc env evd cj.uj_val cj.uj_type t + 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 - inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t - 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 }) + (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/coercion.mli b/pretyping/coercion.mli index fe93a26f4f..afdf28d75c 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,13 +16,19 @@ open Glob_term (** {6 Coercions. } *) +type coercion_trace + +val empty_coercion_trace : coercion_trace + +val reapply_coercions : evar_map -> coercion_trace -> EConstr.t -> EConstr.t + (** [inh_app_fun resolve_tc env isevars j] coerces [j] to a function; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type a product; it returns [j] if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing) *) val inh_app_fun : program_mode:bool -> bool -> - env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment * coercion_trace (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as @@ -48,11 +54,11 @@ val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool -> val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool -> env -> evar_map -> ?flags:Evarconv.unify_flags -> - unsafe_judgment -> types -> evar_map * unsafe_judgment + unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool -> env -> evar_map -> ?flags:Evarconv.unify_flags -> - unsafe_judgment -> types -> evar_map * unsafe_judgment + unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; diff --git a/pretyping/classops.ml b/pretyping/coercionops.ml index 16021b66f8..d6458e1409 100644 --- a/pretyping/classops.ml +++ b/pretyping/coercionops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/classops.mli b/pretyping/coercionops.mli index 9f633843eb..247ef4df75 100644 --- a/pretyping/classops.mli +++ b/pretyping/coercionops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 7d1bb5e3b1..f85635528d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 88001bba6e..1b16e2effb 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 862865bd90..73be36d031 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -228,7 +228,6 @@ let force_wildcard () = !wildcard_value let () = declare_bool_option { optdepr = false; - optname = "forced wildcard"; optkey = ["Printing";"Wildcard"]; optread = force_wildcard; optwrite = (:=) wildcard_value } @@ -237,7 +236,6 @@ let fast_name_generation = ref false let () = declare_bool_option { optdepr = false; - optname = "fast bound name generation algorithm"; optkey = ["Fast";"Name";"Printing"]; optread = (fun () -> !fast_name_generation); optwrite = (:=) fast_name_generation; @@ -248,7 +246,6 @@ let synthetize_type () = !synth_type_value let () = declare_bool_option { optdepr = false; - optname = "pattern matching return type synthesizability"; optkey = ["Printing";"Synth"]; optread = synthetize_type; optwrite = (:=) synth_type_value } @@ -258,7 +255,6 @@ let reverse_matching () = !reverse_matching_value let () = declare_bool_option { optdepr = false; - optname = "pattern-matching reversibility"; optkey = ["Printing";"Matching"]; optread = reverse_matching; optwrite = (:=) reverse_matching_value } @@ -268,7 +264,6 @@ let print_primproj_params () = !print_primproj_params_value let () = declare_bool_option { optdepr = false; - optname = "printing of primitive projection parameters"; optkey = ["Printing";"Primitive";"Projection";"Parameters"]; optread = print_primproj_params; optwrite = (:=) print_primproj_params_value } @@ -348,7 +343,6 @@ let print_factorize_match_patterns = ref true let () = declare_bool_option { optdepr = false; - optname = "factorization of \"match\" patterns in printing"; optkey = ["Printing";"Factorizable";"Match";"Patterns"]; optread = (fun () -> !print_factorize_match_patterns); optwrite = (fun b -> print_factorize_match_patterns := b) } @@ -358,7 +352,6 @@ let print_allow_match_default_clause = ref true let () = declare_bool_option { optdepr = false; - optname = "possible use of \"match\" default pattern in printing"; optkey = ["Printing";"Allow";"Match";"Default";"Clause"]; optread = (fun () -> !print_allow_match_default_clause); optwrite = (fun b -> print_allow_match_default_clause := b) } @@ -455,7 +448,9 @@ let rec decomp_branch tags nal flags (avoid,env as e) sigma c = (avoid', add_name_opt na' body t env) sigma c let rec build_tree na isgoal e sigma ci cl = - let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in + let mkpat n rhs pl = + let na = update_name sigma na rhs in + na, DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,na) in let cnl = ci.ci_pp_info.cstr_tags in List.flatten (List.init (Array.length cl) @@ -485,7 +480,9 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with and contract_branch isgoal e sigma (cdn,mkpat,rhs) = let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in let mat = align_tree nal isgoal rhs sigma in - List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat + List.map (fun (ids,hd,rhs) -> + let na, pat = mkpat rhs hd in + (Nameops.Name.fold_right Id.Set.add na ids, pat, rhs)) mat (**********************************************************************) (* Transform internal representation of pattern-matching into list of *) @@ -692,7 +689,7 @@ let detype_universe sigma u = if Univ.Level.is_set l then GSet else GType (hack_qualid_of_univ_level sigma l) in (s, n) in - Univ.Universe.map fn u + List.map fn (Univ.Universe.repr u) let detype_sort sigma = function | SProp -> UNamed [GSProp,0] diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 21957b4775..5723b47715 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2130d4ce90..26bf02aa25 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -50,8 +50,6 @@ let default_flags env = let debug_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print states sent to Evarconv unification"; optkey = ["Debug";"Unification"]; optread = (fun () -> !debug_unification); optwrite = (fun a -> debug_unification:=a); @@ -60,8 +58,6 @@ let () = Goptions.(declare_bool_option { let debug_ho_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print higher-order unification debug information"; optkey = ["Debug";"HO";"Unification"]; optread = (fun () -> !debug_ho_unification); optwrite = (fun a -> debug_ho_unification:=a); @@ -269,7 +265,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let sk2 = Stack.append_app args sk2 in lookup_canonical_conversion (proji, Const_cs c2), sk2 | _ -> - let (c2, _) = Termops.global_of_constr sigma t2 in + let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in lookup_canonical_conversion (proji, Const_cs c2),sk2 with Not_found -> let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in @@ -1337,8 +1333,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = try let evi = Evd.find_undefined evd evk in let evi = nf_evar_info evd evi in - let env_evar_unf = evar_env evi in - let env_evar = evar_filtered_env evi in + let env_evar_unf = evar_env env_rhs evi in + let env_evar = evar_filtered_env env_rhs evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in if !debug_ho_unification then @@ -1473,16 +1469,16 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | Some [t] -> if not (noccur_evar env_rhs evd ev (EConstr.of_constr t)) then raise (TypingFailed evd); - instantiate_evar evar_unify flags evd ev (EConstr.of_constr t) + instantiate_evar evar_unify flags env_rhs evd ev (EConstr.of_constr t) | Some l when abstract = Abstraction.Abstract && List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> - instantiate_evar evar_unify flags evd ev vid + instantiate_evar evar_unify flags env_rhs evd ev vid | _ -> evd) with e -> user_err (Pp.str "Cannot find an instance") else ((if !debug_ho_unification then let evi = Evd.find evd evk in - let env = Evd.evar_env evi in + let env = Evd.evar_env env_rhs evi in Feedback.msg_debug Pp.(str"evar is defined: " ++ int (Evar.repr evk) ++ spc () ++ prc env evd (match evar_body evi with Evar_defined c -> c @@ -1498,7 +1494,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = (if !debug_ho_unification then begin let evi = Evd.find evd evk in - let evenv = evar_env evi in + let evenv = evar_env env_rhs evi in let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv evd body) end; @@ -1506,7 +1502,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = else try let evi = Evd.find_undefined evd evk in - let evenv = evar_env evi in + let evenv = evar_env env_rhs evi in let rhs' = nf_evar evd rhs' in if !debug_ho_unification then Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ @@ -1517,7 +1513,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = if !debug_ho_unification then Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')); let flags = default_flags_of TransparentState.full in - Evarsolve.instantiate_evar evar_unify flags evd evk rhs' + Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs' with IllTypedInstance _ -> raise (TypingFailed evd) in let evd = abstract_free_holes evd subst in @@ -1664,7 +1660,7 @@ let max_undefined_with_candidates evd = with MaxUndefined ans -> Some ans -let rec solve_unconstrained_evars_with_candidates flags evd = +let rec solve_unconstrained_evars_with_candidates flags env evd = (* max_undefined is supposed to return the most recent, hence possibly most dependent evar *) match max_undefined_with_candidates evd with @@ -1675,9 +1671,9 @@ let rec solve_unconstrained_evars_with_candidates flags evd = | a::l -> (* In case of variables, most recent ones come first *) try - let evd = instantiate_evar evar_unify flags evd evk a in + let evd = instantiate_evar evar_unify flags env evd evk a in match reconsider_unif_constraints evar_unify flags evd with - | Success evd -> solve_unconstrained_evars_with_candidates flags evd + | Success evd -> solve_unconstrained_evars_with_candidates flags env evd | UnifFailure _ -> aux l with | IllTypedInstance _ -> aux l @@ -1685,7 +1681,7 @@ let rec solve_unconstrained_evars_with_candidates flags evd = (* Expected invariant: most dependent solutions come first *) (* so as to favor progress when used with the refine tactics *) let evd = aux l in - solve_unconstrained_evars_with_candidates flags evd + solve_unconstrained_evars_with_candidates flags env evd let solve_unconstrained_impossible_cases env evd = Evd.fold_undefined (fun evk ev_info evd' -> @@ -1695,18 +1691,18 @@ let solve_unconstrained_impossible_cases env evd = let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in let ty = j_type j in let flags = default_flags env in - instantiate_evar evar_unify flags evd' evk ty + instantiate_evar evar_unify flags env evd' evk ty | _ -> evd') evd evd let solve_unif_constraints_with_heuristics env ?(flags=default_flags env) ?(with_ho=false) evd = - let evd = solve_unconstrained_evars_with_candidates flags evd in + let evd = solve_unconstrained_evars_with_candidates flags env evd in let rec aux evd pbs progress stuck = match pbs with | (pbty,env,t1,t2 as pb) :: pbs -> (match apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 with | Success evd' -> - let evd' = solve_unconstrained_evars_with_candidates flags evd' in + let evd' = solve_unconstrained_evars_with_candidates flags env evd' in let (evd', rest) = extract_all_conv_pbs evd' in begin match rest with | [] -> aux evd' pbs true stuck diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index a1acf8b382..767a173131 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index aebdd14396..50187d82cc 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -76,7 +76,7 @@ let idx = Namegen.default_dependent_ident let define_pure_evar_as_product env evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in - let evenv = evar_env evi in + let evenv = evar_env env evi in let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) in let concl = Reductionops.whd_all evenv evd evi.evar_concl in let s = destSort evd concl in @@ -129,7 +129,7 @@ let define_evar_as_product env evd (evk,args) = let define_pure_evar_as_lambda env evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in - let evenv = evar_env evi in + let evenv = evar_env env evi in let typ = Reductionops.whd_all evenv evd (evar_concl evi) in let evd1,(na,dom,rng) = match EConstr.kind evd typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) @@ -170,7 +170,7 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function let define_evar_as_sort env evd (ev,args) = let evd, s = new_sort_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in - let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in + let concl = Reductionops.whd_all (evar_env env evi) evd evi.evar_concl in let sort = destSort evd concl in let evd' = Evd.define ev (mkSort s) evd in Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index 3dc3e45068..a4169c2298 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 5a23525fb0..4eae0cf86c 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -78,9 +78,9 @@ let get_polymorphic_positions env sigma f = match EConstr.kind sigma f with | Ind (ind, u) | Construct ((ind, _), u) -> let mib,oib = Inductive.lookup_mind_specif env ind in - (match oib.mind_arity with - | RegularArity _ -> assert false - | TemplateArity templ -> templ.template_param_levels) + (match mib.mind_template with + | None -> assert false + | Some templ -> templ.template_param_levels) | _ -> assert false let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) @@ -311,21 +311,47 @@ let eq_alias a b = match a, b with | VarAlias id1, VarAlias id2 -> Id.equal id1 id2 | _ -> false -type aliasing = EConstr.t option * alias list +type 'a aliasing = 'a option * alias list let empty_aliasing = None, [] let make_aliasing c = Some c, [] let push_alias (alias, l) a = (alias, a :: l) + +module Alias = +struct +type t = { mutable lift : int; mutable data : EConstr.t } + +let make c = { lift = 0; data = c } + +let lift n { lift; data } = { lift = lift + n; data } + +let eval alias = + let c = EConstr.Vars.lift alias.lift alias.data in + let () = alias.lift <- 0 in + let () = alias.data <- c in + c + +let repr sigma alias = match EConstr.kind sigma alias.data with +| Rel n -> Some (RelAlias (n + alias.lift)) +| Var id -> Some (VarAlias id) +| _ -> None + +end + let lift_aliasing n (alias, l) = let map a = match a with | VarAlias _ -> a | RelAlias m -> RelAlias (m + n) in - (Option.map (fun c -> lift n c) alias, List.map map l) + (Option.map (fun c -> Alias.lift n c) alias, List.map map l) + +let cast_aliasing (alias, l) = match alias with +| None -> (None, l) +| Some c -> (Some (Alias.make c), l) type aliases = { - rel_aliases : aliasing Int.Map.t; - var_aliases : aliasing Id.Map.t; + rel_aliases : Alias.t aliasing Int.Map.t; + var_aliases : EConstr.t aliasing Id.Map.t; (** Only contains [VarAlias] *) } @@ -359,13 +385,14 @@ let compute_rel_aliases var_aliases rels sigma = | Var id' -> let aliases_of_n = try Id.Map.find id' var_aliases with Not_found -> empty_aliasing in - Int.Map.add n (push_alias aliases_of_n (VarAlias id')) aliases + Int.Map.add n (push_alias (cast_aliasing aliases_of_n) (VarAlias id')) aliases | Rel p -> let aliases_of_n = try Int.Map.find (p+n) aliases with Not_found -> empty_aliasing in Int.Map.add n (push_alias aliases_of_n (RelAlias (p+n))) aliases | _ -> - Int.Map.add n (make_aliasing (lift n (mkCast(t,DEFAULTcast,u)))) aliases) + let alias = Alias.lift n (Alias.make @@ mkCast(t,DEFAULTcast, u)) in + Int.Map.add n (make_aliasing alias) aliases) | LocalAssum _ -> aliases) ) rels @@ -387,7 +414,7 @@ let lift_aliases n aliases = let get_alias_chain_of sigma aliases x = match x with | RelAlias n -> (try Int.Map.find n aliases.rel_aliases with Not_found -> empty_aliasing) - | VarAlias id -> (try Id.Map.find id aliases.var_aliases with Not_found -> empty_aliasing) + | VarAlias id -> (try cast_aliasing (Id.Map.find id aliases.var_aliases) with Not_found -> empty_aliasing) let normalize_alias_opt_alias sigma aliases x = match get_alias_chain_of sigma aliases x with @@ -420,13 +447,14 @@ let extend_alias sigma decl { var_aliases; rel_aliases } = | Var id' -> let aliases_of_binder = try Id.Map.find id' var_aliases with Not_found -> empty_aliasing in - Int.Map.add 1 (push_alias aliases_of_binder (VarAlias id')) rel_aliases + Int.Map.add 1 (push_alias (cast_aliasing aliases_of_binder) (VarAlias id')) rel_aliases | Rel p -> let aliases_of_binder = try Int.Map.find (p+1) rel_aliases with Not_found -> empty_aliasing in Int.Map.add 1 (push_alias aliases_of_binder (RelAlias (p+1))) rel_aliases | _ -> - Int.Map.add 1 (make_aliasing (lift 1 t)) rel_aliases) + let alias = Alias.lift 1 (Alias.make t) in + Int.Map.add 1 (make_aliasing alias) rel_aliases) | LocalAssum _ -> rel_aliases in { var_aliases; rel_aliases } @@ -434,7 +462,7 @@ let expand_alias_once sigma aliases x = match get_alias_chain_of sigma aliases x with | None, [] -> None | Some a, [] -> Some a - | _, l -> Some (of_alias (List.last l)) + | _, l -> Some (Alias.make (of_alias (List.last l))) let expansions_of_var sigma aliases x = let (_, l) = get_alias_chain_of sigma aliases x in @@ -442,9 +470,9 @@ let expansions_of_var sigma aliases x = let expansion_of_var sigma aliases x = match get_alias_chain_of sigma aliases x with - | None, [] -> (false, of_alias x) - | Some a, _ -> (true, a) - | None, a :: _ -> (true, of_alias a) + | None, [] -> (false, Some x) + | Some a, _ -> (true, Alias.repr sigma a) + | None, a :: _ -> (true, Some a) let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t with | Rel n -> of_alias (normalize_alias sigma aliases (RelAlias n)) @@ -482,10 +510,10 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c = match ck with | VarAlias id -> acc4 := Id.Set.add id !acc4 | RelAlias n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3); - match EConstr.kind sigma c' with - | Var id -> acc2 := Id.Set.add id !acc2 - | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1 - | _ -> frec (aliases,depth) c end + match c' with + | Some (VarAlias id) -> acc2 := Id.Set.add id !acc2 + | Some (RelAlias n) -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1 + | None -> frec (aliases,depth) c end | Const _ | Ind _ | Construct _ -> acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2 | _ -> @@ -764,9 +792,9 @@ let restrict_upon_filter evd evk p args = let len = Array.length args in Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i)) -let check_evar_instance unify flags evd evk1 body = +let check_evar_instance unify flags env evd evk1 body = let evi = Evd.find evd evk1 in - let evenv = evar_env evi in + let evenv = evar_env env evi in (* FIXME: The body might be ill-typed when this is called from w_merge *) (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = @@ -915,7 +943,7 @@ let rec find_solution_type evarenv = function let rec do_projection_effects unify flags define_fun env ty evd = function | ProjectVar -> evd | ProjectEvar ((evk,argsv),evi,id,p) -> - let evd = check_evar_instance unify flags evd evk (mkVar id) in + let evd = check_evar_instance unify flags env evd evk (mkVar id) in let evd = Evd.define evk (EConstr.mkVar id) evd in (* TODO: simplify constraints involving evk *) let evd = do_projection_effects unify flags define_fun env ty evd p in @@ -971,7 +999,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_ with Not_found -> match expand_alias_once evd aliases t with | None -> raise Not_found - | Some c -> aux k (lift k c) in + | Some c -> aux k (Alias.eval (Alias.lift k c)) in try let c = aux 0 c_in_env_extended_with_k_binders in Invertible (UniqueProjection (c,!effects)) @@ -1223,7 +1251,7 @@ let rec is_constrainable_in top env evd k (ev,(fv_rels,fv_ids) as g) t = let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t = match to_alias evd t with | Some t -> - let expanded, t' = expansion_of_var evd aliases t in + let expanded, _ = expansion_of_var evd aliases t in if expanded then (* t is a local definition, we keep it only if appears in the list *) (* of let-in variables effectively occurring on the right-hand side, *) @@ -1284,7 +1312,7 @@ let solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 (evk2,_ as update_evar_info evk2 (fst (destEvar evd' body)) evd' else evd' in - check_evar_instance unify flags evd' evk2 body + check_evar_instance unify flags env evd' evk2 body with EvarSolvedOnTheFly (evd,c) -> f env evd pbty ev2 c @@ -1329,12 +1357,12 @@ let solve_evar_evar ?(force=false) f unify flags env evd pbty (evk1,args1 as ev1 try (* ?X : ΠΔ. Type i = ?Y : ΠΔ'. Type j. The body of ?X and ?Y just has to be of type ΠΔ. Type k for some k <= i, j. *) - let evienv = Evd.evar_env evi in + let evienv = Evd.evar_env env evi in let concl1 = EConstr.Unsafe.to_constr evi.evar_concl in let ctx1, i = Reduction.dest_arity evienv concl1 in let ctx1 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx1 in let evi2 = Evd.find evd evk2 in - let evi2env = Evd.evar_env evi2 in + let evi2env = Evd.evar_env env evi2 in let concl2 = EConstr.Unsafe.to_constr evi2.evar_concl in let ctx2, j = Reduction.dest_arity evi2env concl2 in let ctx2 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx2 in @@ -1418,7 +1446,7 @@ let solve_candidates unify flags env evd (evk,argsv) rhs = (* time and the evar been solved by the filtering process *) if Evd.is_undefined evd evk then let evd' = Evd.define evk c evd in - check_evar_instance unify flags evd' evk c + check_evar_instance unify flags env evd' evk c else evd | l when List.length l < List.length l' -> let candidates = List.map fst l in @@ -1442,11 +1470,11 @@ let occur_evar_upto_types sigma n c = in try occur_rec c; false with Occur -> true -let instantiate_evar unify flags evd evk body = +let instantiate_evar unify flags env evd evk body = (* Check instance freezing the evar to be defined, as checking could involve the same evar definition problem again otherwise *) let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in - let evd' = check_evar_instance unify flags evd evk body in + let evd' = check_evar_instance unify flags env evd evk body in Evd.define evk body evd' (* We try to instantiate the evar assuming the body won't depend @@ -1508,7 +1536,7 @@ let rec invert_definition unify flags choose imitate_defs raise (NotEnoughInformationToProgress sols); (* No unique projection but still restrict to where it is possible *) (* materializing is necessary, but is restricting useful? *) - let ty = find_solution_type (evar_filtered_env evi) sols in + let ty = find_solution_type (evar_filtered_env env evi) sols in let ty' = instantiate_evar_array evi ty argsv in let (evd,evar,(evk',argsv' as ev')) = materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty' in @@ -1571,7 +1599,7 @@ let rec invert_definition unify flags choose imitate_defs try let evd,body = project_evar_on_evar false unify flags env' evd aliases 0 None ev'' ev' in let evd = Evd.define evk' body evd in - check_evar_instance unify flags evd evk' body + check_evar_instance unify flags env' evd evk' body with | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *) | CannotProject (evd,ev'') -> @@ -1638,7 +1666,7 @@ let rec invert_definition unify flags choose imitate_defs else let t' = imitate (env,0) rhs in if !progress then - (recheck_applications unify flags (evar_env evi) evdref t'; t') + (recheck_applications unify flags (evar_env env evi) evdref t'; t') else t' in (!evdref,body) @@ -1670,7 +1698,7 @@ and evar_define unify flags ?(choose=false) ?(imitate_defs=true) env evd pbty (e if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body)); (* needed only if an inferred type *) let evd', body = refresh_universes pbty env evd' body in - instantiate_evar unify flags evd' evk body + instantiate_evar unify flags env evd' evk body with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd pbty ev sols rhs diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 908adac7e4..0a1b731e6b 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -77,7 +77,7 @@ type conversion_check = unify_flags -> unification_kind -> - [c] does not contain any Meta(_) *) -val instantiate_evar : unifier -> unify_flags -> evar_map -> +val instantiate_evar : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), @@ -125,7 +125,7 @@ exception IllTypedInstance of env * types * types (* May raise IllTypedInstance if types are not convertible *) val check_evar_instance : unifier -> unify_flags -> - evar_map -> Evar.t -> constr -> evar_map + env -> evar_map -> Evar.t -> constr -> evar_map val remove_instance_local_defs : evar_map -> Evar.t -> 'a array -> 'a list diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 2d64692cc6..bd717e2d1f 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 6f9dac400f..436b730a88 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml index b9128aa107..89fed7334f 100644 --- a/pretyping/geninterp.ml +++ b/pretyping/geninterp.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli index 088f97271b..7297684160 100644 --- a/pretyping/geninterp.mli +++ b/pretyping/geninterp.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index aebe47a7a7..fad41614b4 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index a49ac80f47..023e24e6d8 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 02c2fc4a13..a006c82993 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -68,8 +68,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Explicit, Explicit -> true - | Implicit, Implicit -> true - | (Explicit | Implicit), _ -> false + | NonMaxImplicit, NonMaxImplicit -> true + | MaxImplicit, MaxImplicit -> true + | (Explicit | NonMaxImplicit | MaxImplicit), _ -> false let case_style_eq s1 s2 = let open Constr in match s1, s2 with | LetStyle, LetStyle -> true diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 20ac35888e..14bf2f6764 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 44323441b6..bccc30ad62 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -65,7 +65,7 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t type cases_pattern = [ `any ] cases_pattern_g -type binding_kind = Explicit | Implicit +type binding_kind = Explicit | MaxImplicit | NonMaxImplicit (** Representation of an internalized (or in other words globalized) term. *) type 'a glob_constr_r = diff --git a/pretyping/heads.ml b/pretyping/heads.ml index 7740628c21..908b8b00d6 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/heads.mli b/pretyping/heads.mli index bb096a846e..179255ce05 100644 --- a/pretyping/heads.mli +++ b/pretyping/heads.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 1d240db33c..b5d81f762a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -530,22 +530,25 @@ let change_sort_arity sort = corresponding eta-expanded term *) let weaken_sort_scheme env evd set sort npars term ty = let evdref = ref evd in - let rec drec np elim = + let rec drec ctx np elim = match kind elim with | Prod (n,t,c) -> + let ctx = LocalAssum (n, t) :: ctx in if Int.equal np 0 then let osort, t' = change_sort_arity sort t in evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) env !evdref sort osort; mkProd (n, t', c), - mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) + mkLambda (n, t', mkApp(term, Context.Rel.to_extended_vect mkRel 0 ctx)) else - let c',term' = drec (np-1) c in + let c',term' = drec ctx (np-1) c in mkProd (n, t, c'), mkLambda (n, t, term') - | LetIn (n,b,t,c) -> let c',term' = drec np c in - mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') + | LetIn (n,b,t,c) -> + let ctx = LocalDef (n, b, t) :: ctx in + let c',term' = drec ctx np c in + mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.") in - let ty, term = drec npars ty in + let ty, term = drec [] npars ty in !evdref, ty, term (**********************************************************************) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index ae23fc4ee6..c07e311941 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 36b405e981..c7110d7a91 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -28,14 +28,14 @@ open Context.Rel.Declaration let type_of_inductive env (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps; - Inductive.type_of_inductive env (specif,u) + Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; + Inductive.type_of_inductive (specif,u) (* Return type as quoted by the user *) let type_of_constructor env (cstr,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps; + Typeops.check_hyps_inclusion env (GlobRef.ConstructRef cstr) mib.mind_hyps; Inductive.type_of_constructor (cstr,u) specif (* Return constructor types in user form *) @@ -681,13 +681,17 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = match mip.mind_arity with | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity) | TemplateArity ar -> + let templ = match mib.mind_template with + | None -> assert false + | Some t -> t + in let _,scl = splay_arity env sigma conclty in let scl = EConstr.ESorts.kind sigma scl in let ctx = List.rev mip.mind_arity_ctxt in let evdref = ref sigma in let ctx = instantiate_universes - env evdref scl ar.template_level (ctx,ar.template_param_levels) in + env evdref scl ar.template_level (ctx,templ.template_param_levels) in !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl)) let type_of_projection_constant env (p,u) = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 06466cc67d..ab69629595 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/keys.ml b/pretyping/keys.ml index 39a4a525ef..1e4f2f2340 100644 --- a/pretyping/keys.ml +++ b/pretyping/keys.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/keys.mli b/pretyping/keys.mli index a7adf7791b..c6a9d0f026 100644 --- a/pretyping/keys.mli +++ b/pretyping/keys.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/locus.ml b/pretyping/locus.ml index afb4cc708a..d43c377cf9 100644 --- a/pretyping/locus.ml +++ b/pretyping/locus.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index ffb29bb38c..86352eb79a 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index 47d2ffe797..911ccc1a38 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 2db674d397..7be34d4cf1 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -26,6 +26,10 @@ open Context.Rel.Declaration exception Find_at of int +(* timing *) + +let timing_enabled = ref false + (* profiling *) let profiling_enabled = ref false @@ -79,6 +83,12 @@ let get_profiling_enabled () = let set_profiling_enabled b = profiling_enabled := b +let get_timing_enabled () = + !timing_enabled + +let set_timing_enabled b = + timing_enabled := b + let invert_tag cst tag reloc_tbl = try for j = 0 to Array.length reloc_tbl - 1 do @@ -496,19 +506,23 @@ let native_norm env sigma c ty = let ml_filename, prefix = Nativelib.get_ml_filename () in let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in let profile = get_profiling_enabled () in + let print_timing = get_timing_enabled () in + let tc0 = Sys.time () in let fn = Nativelib.compile ml_filename code ~profile:profile in - if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ..."); + let tc1 = Sys.time () in + let time_info = Format.sprintf "native_compute: Compilation done in %.5f@." (tc1 -. tc0) in + if print_timing then Feedback.msg_info (Pp.str time_info); let profiler_pid = if profile then start_profiler () else None in let t0 = Sys.time () in Nativelib.call_linker ~fatal:true env ~prefix fn (Some upd); let t1 = Sys.time () in if profile then stop_profiler profiler_pid; - let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + let time_info = Format.sprintf "native_compute: Evaluation done in %.5f@." (t1 -. t0) in + if print_timing then Feedback.msg_info (Pp.str time_info); let res = nf_val env sigma !Nativelib.rt1 ty in let t2 = Sys.time () in - let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + let time_info = Format.sprintf "native_compute: Reification done in %.5f@." (t2 -. t1) in + if print_timing then Feedback.msg_info (Pp.str time_info); EConstr.of_constr res let native_conv_generic pb sigma t = diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 02de034fcb..4f18174261 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -20,6 +20,9 @@ val set_profile_filename : string -> unit val get_profiling_enabled : unit -> bool val set_profiling_enabled : bool -> unit +val get_timing_enabled : unit -> bool +val set_timing_enabled : bool -> unit + val native_norm : env -> evar_map -> constr -> types -> constr diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 2d7a152817..3f2e690da5 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 9ca3529b5c..b8635d03b7 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 342891d65f..96c808b84c 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index c1b05014c0..6994a7b78f 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index af2d75a19d..7086584642 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0364e1b61f..ded159e484 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -47,7 +47,7 @@ open Evarconv module NamedDecl = Context.Named.Declaration -type typing_constraint = OfType of types | IsType | WithoutTypeConstraint +type typing_constraint = UnknownIfTermOrType | IsType | OfType of types | WithoutTypeConstraint let (!!) env = GlobEnv.env env @@ -87,9 +87,9 @@ let search_guard ?loc env possible_indexes fixdefs = let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with reraise -> - let (e, info) = CErrors.push reraise in + let (e, info) = Exninfo.capture reraise in let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in - iraise (e, info)); + Exninfo.iraise (e, info)); indexes else (* we now search recursively among all combinations *) @@ -125,7 +125,6 @@ let esearch_guard ?loc env sigma indexes fix = let is_strict_universe_declarations = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"strict universe declaration" ~key:["Strict";"Universe";"Declaration"] ~value:true @@ -188,7 +187,7 @@ let interp_sort_info ?loc evd l = in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l -type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr +type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option type inference_flags = { use_typeclasses : bool; @@ -248,17 +247,16 @@ let apply_typeclasses ~program_mode env sigma frozen fail_evar = else sigma in sigma -let apply_inference_hook hook env sigma frozen = match frozen with +let apply_inference_hook (hook : inference_hook) env sigma frozen = match frozen with | FrozenId _ -> sigma | FrozenProgress (lazy (_, pending)) -> Evar.Set.fold (fun evk sigma -> if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then - try - let sigma, c = hook env sigma evk in + match hook env sigma evk with + | Some (sigma, c) -> Evd.define evk c sigma - with Exit -> - sigma + | None -> sigma else sigma) pending sigma @@ -267,8 +265,8 @@ let apply_heuristics env sigma fail_evar = let flags = default_flags_of (Typeclasses.classes_transparent_state ()) in try solve_unif_constraints_with_heuristics ~flags env sigma with e when CErrors.noncritical e -> - let e = CErrors.push e in - if fail_evar then iraise e else sigma + let e = Exninfo.capture e in + if fail_evar then Exninfo.iraise e else sigma let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen = (* Naive way, call resolution again with failure flag *) @@ -361,7 +359,7 @@ let adjust_evar_source sigma na c = (* coerce to tycon if any *) let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = function - | None -> sigma, j + | None -> sigma, j, Some Coercion.empty_coercion_trace | Some t -> Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t @@ -446,7 +444,7 @@ let pretype_ref ?loc sigma env ref us = Pretype_errors.error_var_not_found ?loc !!env sigma id) | ref -> let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in - let ty = unsafe_type_of !!env sigma c in + let sigma, ty = type_of !!env sigma c in sigma, make_judge c ty let interp_sort ?loc evd : glob_sort -> _ = function @@ -604,16 +602,18 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk module Default = struct + let discard_trace (sigma,t,otrace) = sigma, t + let pretype_ref self (ref, u) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let sigma, t_ref = pretype_ref ?loc sigma env ref u in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon let pretype_var self id = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let pretype tycon env sigma t = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t in let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma = (* Ne faudrait-il pas s'assurer que hyps est bien un @@ -626,7 +626,7 @@ struct let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in let c = mkEvar (evk, args) in let j = Retyping.get_judgment_of !!env sigma c in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon let pretype_patvar self kind ?loc ~program_mode ~poly resolve_tc tycon env sigma = let sigma, ty = @@ -752,17 +752,17 @@ struct let cofix = (i, fixdecls) in (try check_cofix !!env (i, nf_fix sigma fixdecls) with reraise -> - let (e, info) = CErrors.push reraise in + let (e, info) = Exninfo.capture reraise in let info = Option.cata (Loc.add_loc info) info loc in - iraise (e, info)); + Exninfo.iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon let pretype_sort self s = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let sigma, j = pretype_sort ?loc sigma s in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon let pretype_app self (f, args) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -771,12 +771,15 @@ struct let floc = loc_of_glob_constr f in let length = List.length args in let nargs_before_bidi = + if Option.is_empty tycon then length + (* We apply bidirectionality hints only if an expected type is specified *) + else (* if `f` is a global, we retrieve bidirectionality hints *) - try - let (gr,_) = destRef sigma fj.uj_val in - Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints - with DestKO -> - length + try + let (gr,_) = destRef sigma fj.uj_val in + Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints + with DestKO -> + length in let candargs = (* Bidirectional typechecking hint: @@ -813,24 +816,38 @@ struct else fun f v -> applist (f, [v]) | _ -> fun _ f v -> applist (f, [v]) in - let rec apply_rec env sigma n resj candargs bidiargs = function - | [] -> sigma, resj, List.rev bidiargs + let refresh_template env sigma resj = + (* Special case for inductive type applications that must be + refreshed right away. *) + match EConstr.kind sigma resj.uj_val with + | App (f,args) -> + if Termops.is_template_polymorphic_ind !!env sigma f then + let c = mkApp (f, args) in + let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in + let t = Retyping.get_type_of !!env sigma c in + sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t + else sigma, resj + | _ -> sigma, resj + in + let rec apply_rec env sigma n resj resj_before_bidi candargs bidiargs = function + | [] -> sigma, resj, resj_before_bidi, List.rev bidiargs | c::rest -> let bidi = n >= nargs_before_bidi in let argloc = loc_of_glob_constr c in - let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in + let sigma, resj, trace = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in let resty = whd_all !!env sigma resj.uj_type in match EConstr.kind sigma resty with | Prod (na,c1,c2) -> - let tycon = Some c1 in let (sigma, hj), bidiargs = - if bidi && Option.has_some tycon then + if bidi then (* We want to get some typing information from the context before typing the argument, so we replace it by an existential variable *) let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in - (sigma, make_judge c_hole c1), (c_hole, c) :: bidiargs - else pretype tycon env sigma c, bidiargs + (sigma, make_judge c_hole c1), (c_hole, c, trace) :: bidiargs + else + let tycon = Some c1 in + pretype tycon env sigma c, bidiargs in let sigma, candargs, ujval = match candargs with @@ -845,29 +862,18 @@ struct in let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in - let j = { uj_val = value; uj_type = typ } in - apply_rec env sigma (n+1) j candargs bidiargs rest + let resj = { uj_val = value; uj_type = typ } in + let resj_before_bidi = if bidi then resj_before_bidi else resj in + apply_rec env sigma (n+1) resj resj_before_bidi candargs bidiargs rest | _ -> let sigma, hj = pretype empty_tycon env sigma c in error_cant_apply_not_functional ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|] in - let sigma, resj, bidiargs = apply_rec env sigma 0 fj candargs [] args in - let sigma, resj = - match EConstr.kind sigma resj.uj_val with - | App (f,args) -> - if Termops.is_template_polymorphic_ind !!env sigma f then - (* Special case for inductive type applications that must be - refreshed right away. *) - let c = mkApp (f, args) in - let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in - let t = Retyping.get_type_of !!env sigma c in - sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t - else sigma, resj - | _ -> sigma, resj - in - let sigma, t = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in - let refine_arg sigma (newarg,origarg) = + let sigma, resj, resj_before_bidi, bidiargs = apply_rec env sigma 0 fj fj candargs [] args in + let sigma, resj = refresh_template env sigma resj in + let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in + let refine_arg n (sigma,t) (newarg,origarg,trace) = (* Refine an argument (originally `origarg`) represented by an evar (`newarg`) to use typing information from the context *) (* Recover the expected type of the argument *) @@ -876,12 +882,25 @@ struct let sigma, j = pretype (Some ty) env sigma origarg in (* Unify the (possibly refined) existential variable with the (typechecked) original value *) - Evarconv.unify_delay !!env sigma newarg (j_val j) + let sigma = Evarconv.unify_delay !!env sigma newarg (j_val j) in + sigma, app_f n (Coercion.reapply_coercions sigma trace t) (j_val j) in (* We now refine any arguments whose typing was delayed for bidirectionality *) - let sigma = List.fold_left refine_arg sigma bidiargs in - (sigma, t) + let t = resj_before_bidi.uj_val in + let sigma, t = List.fold_left_i refine_arg nargs_before_bidi (sigma,t) bidiargs in + (* If we did not get a coercion trace (e.g. with `Program` coercions, we + replaced user-provided arguments with inferred ones. Otherwise, we apply + the coercion trace to the user-provided arguments. *) + let resj = + match otrace with + | None -> resj + | Some trace -> + let resj = { resj with uj_val = t } in + let sigma, resj = refresh_template env sigma resj in + { resj with uj_val = Coercion.reapply_coercions sigma trace t } + in + (sigma, resj) let pretype_lambda self (name, bk, c1, c2) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -903,7 +922,7 @@ struct let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in let name = get_name var' in let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_prod self (name, bk, c1, c2) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -926,10 +945,10 @@ struct try judge_of_product !!env name j j' with TypeError _ as e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let info = Option.cata (Loc.add_loc info) info loc in - iraise (e, info) in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + Exninfo.iraise (e, info) in + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_letin self (name, c1, t, c2) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1122,7 +1141,7 @@ struct mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon let pretype_cast self (c, k) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1165,7 +1184,7 @@ struct in let v = mkCast (cj.uj_val, k, tval) in sigma, { uj_val = v; uj_type = tval } - in inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon + in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon let pretype_int self i = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1174,7 +1193,7 @@ struct with Invalid_argument _ -> user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.") in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_float self f = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1183,7 +1202,7 @@ struct with Invalid_argument _ -> user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.") in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon (* [pretype_type valcon env sigma c] coerces [c] into a type *) let pretype_type self c ?loc ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma = match DAst.get c with @@ -1269,7 +1288,7 @@ let ise_pretype_gen flags env sigma lvar kind c = in let env = GlobEnv.make ~hypnaming env sigma lvar in let sigma', c', c'_ty = match kind with - | WithoutTypeConstraint -> + | WithoutTypeConstraint | UnknownIfTermOrType -> let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in sigma, j.uj_val, j.uj_type | OfType exptyp -> @@ -1326,7 +1345,7 @@ let understand_ltac flags env sigma lvar kind c = (sigma, c) let path_convertible env sigma i p q = - let open Classops in + let open Coercionops in let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in let mkGVar id = DAst.make @@ Glob_term.GVar(id) in let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in @@ -1379,4 +1398,4 @@ let path_convertible env sigma i p q = let _ = Evarconv.unify_delay env sigma tp tq in true with Evarconv.UnableToUnify _ | PretypeError _ -> false -let _ = Classops.install_path_comparator path_convertible +let _ = Coercionops.install_path_comparator path_convertible diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 18e416596e..abbb745161 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -38,9 +38,11 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> val search_guard : ?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array -type typing_constraint = OfType of types | IsType | WithoutTypeConstraint - -type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr +type typing_constraint = + | UnknownIfTermOrType (** E.g., unknown if manual implicit arguments allowed *) + | IsType (** Necessarily a type *) + | OfType of types (** A term of the expected type *) + | WithoutTypeConstraint (** A term of unknown expected type *) type inference_flags = { use_typeclasses : bool; @@ -99,13 +101,17 @@ val understand_ltac : inference_flags -> val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context +(** [hook env sigma ev] returns [Some (sigma', term)] if [ev] can be + instantiated with a solution, [None] otherwise. Used to extend + [solve_remaining_evars] below. *) +type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option + (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver hook depending on given flags. *) (* For simplicity, it is assumed that current map has no other evars with candidate and no other conversion problems that the one in [pending], however, it can contain more evars than the pending ones. *) - val solve_remaining_evars : ?hook:inference_hook -> inference_flags -> env -> ?initial:evar_map -> (* current map *) evar_map -> evar_map diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 7e140f4399..07154d4e03 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -26,7 +26,7 @@ Constr_matching Tacred Typeclasses_errors Typeclasses -Classops +Coercionops Program Coercion Detyping diff --git a/pretyping/program.ml b/pretyping/program.ml index 1bc31646dd..df5df5a209 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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" @@ -78,7 +77,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "preferred transparency of Program obligations"; optkey = ["Transparent";"Obligations"]; optread = get_proofs_transparency; optwrite = set_proofs_transparency; } @@ -86,7 +84,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "program cases"; optkey = ["Program";"Cases"]; optread = (fun () -> !program_cases); optwrite = (:=) program_cases } @@ -94,7 +91,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "program generalized coercion"; optkey = ["Program";"Generalized";"Coercion"]; optread = (fun () -> !program_generalized_coercion); optwrite = (:=) program_generalized_coercion } diff --git a/pretyping/program.mli b/pretyping/program.mli index 6604b3a854..a2619c1c35 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 5b416a99f9..a8e934d3c6 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,7 +19,6 @@ open CErrors open Util open Pp open Names -open Globnames open Constr open Mod_subst open Reductionops @@ -80,7 +79,7 @@ let subst_structure subst (id, kl, projs as obj) = (Option.Smart.map (subst_constant subst)) projs in - let id' = subst_constructor subst id in + let id' = Globnames.subst_constructor subst id in if projs' == projs && id' == id then obj else (id',kl,projs') @@ -114,7 +113,7 @@ let find_primitive_projection c = (* the effective components of a structure and the projections of the *) (* structure *) -(* Table des definitions "object" : pour chaque object c, +(* Table of "object" definitions: for each object c, c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n) @@ -127,16 +126,19 @@ let find_primitive_projection c = that maps the pair (Li,ci) to the following data + o_ORIGIN = c (the constant name which this conversion rule is + synthesized from) o_DEF = c o_TABS = B1...Bk o_INJ = Some n (when ci is a reference to the parameter xi) - o_PARAMS = a1...am - o_NARAMS = m + o_TPARAMS = a1...am + o_NPARAMS = m o_TCOMP = ui1...uir *) type obj_typ = { + o_ORIGIN : GlobRef.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) @@ -187,13 +189,13 @@ let rec cs_pattern_of_constr env t = let _, params = Inductive.find_rectype env ty in Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] | Sort s -> Sort_cs (Sorts.family s), None, [] - | _ -> Const_cs (global_of_constr t) , None, [] + | _ -> Const_cs (fst @@ destRef t) , None, [] let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" - (fun (sign,env,t,con,proji_sp) -> + (fun (sign,env,t,ref,proji_sp) -> let env = Termops.push_rels_assum sign env in - let con_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef con) in + let con_pp = Nametab.pr_global_env Id.Set.empty ref in let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in strbrk "Projection value has no head constant: " @@ -201,11 +203,17 @@ let warn_projection_no_head_constant = ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) -let compute_canonical_projections env ~warn (con,ind) = - let o_CTX = Environ.constant_context env con in - let u = Univ.make_abstract_instance o_CTX in - let o_DEF = mkConstU (con, u) in - let c = Environ.constant_value_in env (con,u) in +let compute_canonical_projections env ~warn (gref,ind) = + let o_CTX = Environ.universes_of_global env gref in + let o_DEF, c = + match gref with + | GlobRef.ConstRef con -> + let u = Univ.make_abstract_instance o_CTX in + mkConstU (con, u), Environ.constant_value_in env (con,u) + | GlobRef.VarRef id -> + mkVar id, Option.get (Environ.named_body id env) + | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false + in let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in @@ -224,10 +232,10 @@ let compute_canonical_projections env ~warn (con,ind) = match cs_pattern_of_constr nenv t with | patt, o_INJ, o_TCOMPS -> ((GlobRef.ConstRef proji_sp, (patt, t)), - { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) + { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc - | exception Not_found -> - if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp); + | exception DestKO -> + if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp); acc ) acc spopt else acc @@ -263,12 +271,17 @@ let register_canonical_structure ~warn env sigma o = warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s) ) -let subst_canonical_structure subst (cst,ind as obj) = +type cs = GlobRef.t * inductive + +let subst_canonical_structure subst (gref,ind as obj) = (* invariant: cst is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - let cst' = subst_constant subst cst in - let ind' = subst_ind subst ind in - if cst' == cst && ind' == ind then obj else (cst',ind') + match gref with + | GlobRef.ConstRef cst -> + let cst' = subst_constant subst cst in + let ind' = subst_ind subst ind in + if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind') + | _ -> assert false (*s High-level declaration of a canonical structure *) @@ -279,15 +292,20 @@ let error_not_structure ref description = description)) let check_and_decompose_canonical_structure env sigma ref = - let sp = + let vc = match ref with - GlobRef.ConstRef sp -> sp - | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") + | GlobRef.ConstRef sp -> + let u = Univ.make_abstract_instance (Environ.constant_context env sp) in + begin match Environ.constant_opt_value_in env (sp, u) with + | Some vc -> vc + | None -> error_not_structure ref (str "Could not find its value in the global environment.") end + | GlobRef.VarRef id -> + begin match Environ.named_body id env with + | Some b -> b + | None -> error_not_structure ref (str "Could not find its value in the global environment.") end + | GlobRef.IndRef _ | GlobRef.ConstructRef _ -> + error_not_structure ref (str "Expected an instance of a record or structure.") in - let u = Univ.make_abstract_instance (Environ.constant_context env sp) in - let vc = match Environ.constant_opt_value_in env (sp, u) with - | Some vc -> vc - | None -> error_not_structure ref (str "Could not find its value in the global environment.") in let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with @@ -305,7 +323,7 @@ let check_and_decompose_canonical_structure env sigma ref = let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref (str "Got too few arguments to the record or structure constructor."); - (sp,indsp) + (ref,indsp) let lookup_canonical_conversion (proj,pat) = assoc_pat pat (GlobRef.Map.find proj !object_table) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index e8b0d771aa..955a4e7aae 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -73,6 +73,7 @@ type cs_pattern = | Default_cs type obj_typ = { + o_ORIGIN : GlobRef.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) @@ -86,13 +87,15 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co val pr_cs_pattern : cs_pattern -> Pp.t +type cs = GlobRef.t * inductive + val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> - Constant.t * inductive -> unit -val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive + cs -> unit +val subst_canonical_structure : Mod_subst.substitution -> cs -> cs val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool val canonical_projections : unit -> ((GlobRef.t * cs_pattern) * obj_typ) list -val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive +val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> cs diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4d4fe13983..1e4b537117 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,8 +32,6 @@ exception Elimconst let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Generate weak constraints between Irrelevant universes"; optkey = ["Cumulativity";"Weak";"Constraints"]; optread = (fun () -> not !UState.drop_weak_constraints); optwrite = (fun a -> UState.drop_weak_constraints:=not a); @@ -722,32 +720,31 @@ let magicaly_constant_of_fixbody env sigma reference bd = function | Name.Anonymous -> bd | Name.Name id -> let open UnivProblem in - try - let (cst_mod,_) = Constant.repr2 reference in - let cst = Constant.make2 cst_mod (Label.of_id id) in + let (cst_mod,_) = Constant.repr2 reference in + let cst = Constant.make2 cst_mod (Label.of_id id) in + if not (Environ.mem_constant cst env) then bd + else let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in begin match csts with - | Some csts -> - let subst = Set.fold (fun cst acc -> - let l, r = match cst with - | ULub (u, v) | UWeak (u, v) -> u, v - | UEq (u, v) | ULe (u, v) -> - let get u = Option.get (Universe.level u) in - get u, get v - in - Univ.LMap.add l r acc) - csts Univ.LMap.empty - in - let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in - mkConstU (cst, EInstance.make inst) - | None -> bd + | Some csts -> + let subst = Set.fold (fun cst acc -> + let l, r = match cst with + | ULub (u, v) | UWeak (u, v) -> u, v + | UEq (u, v) | ULe (u, v) -> + let get u = Option.get (Universe.level u) in + get u, get v + in + Univ.LMap.add l r acc) + csts Univ.LMap.empty + in + let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in + mkConstU (cst, EInstance.make inst) + | None -> bd end - with - | Not_found -> bd let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in @@ -973,8 +970,6 @@ module CredNative = RedNative(CNativeEntries) let debug_RAKAM = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print states of the Reductionops abstract machine"; optkey = ["Debug";"RAKAM"]; optread = (fun () -> !debug_RAKAM); optwrite = (fun a -> debug_RAKAM:=a); @@ -1462,12 +1457,15 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV -let report_anomaly e = - let msg = Pp.(str "Conversion test raised an anomaly:" ++ - spc () ++ CErrors.print e) in - let e = UserError (None,msg) in - let e = CErrors.push e in - iraise e +let report_anomaly (e, info) = + let e = + if is_anomaly e then + let msg = Pp.(str "Conversion test raised an anomaly:" ++ + spc () ++ CErrors.print e) in + UserError (None, msg) + else e + in + Exninfo.iraise (e, info) let f_conv ?l2r ?reds env ?evars x y = let inj = EConstr.Unsafe.to_constr in @@ -1483,7 +1481,9 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in true with Reduction.NotConvertible -> false - | e when is_anomaly e -> report_anomaly e + | e -> + let e = Exninfo.capture e in + report_anomaly e let is_conv ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv reds env sigma let is_conv_leq ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma @@ -1499,7 +1499,9 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y = try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true with Reduction.NotConvertible -> false | Univ.UniverseInconsistency _ -> false - | e when is_anomaly e -> report_anomaly e + | e -> + let e = Exninfo.capture e in + report_anomaly e let sigma_compare_sorts env pb s0 s1 sigma = match pb with @@ -1552,7 +1554,9 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) with | Reduction.NotConvertible -> None | Univ.UniverseInconsistency _ when catch_incon -> None - | e when is_anomaly e -> report_anomaly e + | e -> + let e = Exninfo.capture e in + report_anomaly e let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> Reduction.generic_conv pb ~l2r (safe_evar_value sigma)) @@ -1712,7 +1716,7 @@ let splay_arity env sigma c = let l, c = splay_prod env sigma c in match EConstr.kind sigma c with | Sort s -> l,s - | _ -> invalid_arg "splay_arity" + | _ -> raise Reduction.NotArity let sort_of_arity env sigma c = snd (splay_arity env sigma c) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index e72f5f2793..5202380a13 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -236,12 +236,20 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr val splay_prod : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr +val splay_prod_assum : env -> evar_map -> constr -> rel_context * constr + val splay_arity : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t +(** Raises [Reduction.NotArity] *) + val sort_of_arity : env -> evar_map -> constr -> ESorts.t +(** Raises [Reduction.NotArity] *) + val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr +(** Raises [Invalid_argument] *) + val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr -val splay_prod_assum : - env -> evar_map -> constr -> rel_context * constr +(** Raises [Invalid_argument] *) + type 'a miota_args = { mP : constr; (** the result type *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index d2af957b54..821c57d033 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -168,15 +168,21 @@ let retype ?(polyprop=true) sigma = | _ -> decomp_sort env sigma (type_of env t) and type_of_global_reference_knowing_parameters env c args = - let argtyps = - Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in match EConstr.kind sigma c with | Ind (ind, u) -> let u = EInstance.kind sigma u in let mip = lookup_mind_specif env ind in - EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters - ~polyprop env (mip, u) argtyps - with Reduction.NotArity -> retype_error NotAnArity) + let paramtyps = Array.map_to_list (fun arg () -> + let t = type_of env arg in + let s = try Reductionops.sort_of_arity env sigma t + with Reduction.NotArity -> retype_error NotAnArity + in + Sorts.univ_of_sort (ESorts.kind sigma s)) + args + in + EConstr.of_constr + (Inductive.type_of_inductive_knowing_parameters + ~polyprop (mip, u) paramtyps) | Construct (cstr, u) -> let u = EInstance.kind sigma u in EConstr.of_constr (type_of_constructor env (cstr, u)) @@ -267,8 +273,8 @@ let relevance_of_term env sigma c = | Rel n -> let len = Range.length rels in if n <= len then Range.get rels (n - 1) - else Retypeops.relevance_of_rel env (n - len) - | Var x -> Retypeops.relevance_of_var env x + else Relevanceops.relevance_of_rel env (n - len) + | Var x -> Relevanceops.relevance_of_var env x | Sort _ -> Sorts.Relevant | Cast (c, _, _) -> aux rels c | Prod ({binder_relevance=r}, _, codom) -> @@ -278,13 +284,13 @@ let relevance_of_term env sigma c = | LetIn ({binder_relevance=r}, _, _, bdy) -> aux (Range.cons r rels) bdy | App (c, _) -> aux rels c - | Const (c,_) -> Retypeops.relevance_of_constant env c + | Const (c,_) -> Relevanceops.relevance_of_constant env c | Ind _ -> Sorts.Relevant - | Construct (c,_) -> Retypeops.relevance_of_constructor env c + | Construct (c,_) -> Relevanceops.relevance_of_constructor env c | Case (ci, _, _, _) -> ci.ci_relevance | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance - | Proj (p, _) -> Retypeops.relevance_of_projection env p + | Proj (p, _) -> Relevanceops.relevance_of_projection env p | Int _ | Float _ -> Sorts.Relevant | Meta _ | Evar _ -> Sorts.Relevant diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 68a88df194..16bc251c2a 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 10e8cf7e0f..70605d58ab 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -1009,11 +1009,11 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in let app' = f acc app in let a' = f acc a in - (match EConstr.kind sigma app' with - | App (hdf', al') when hdf' == hdf -> - (* Still the same projection, we ignore the change in parameters *) - mkProj (p, a') - | _ -> mkApp (app', [| a' |])) + let hdf', _ = decompose_app_vect sigma app' in + if hdf' == hdf then + (* Still the same projection, we ignore the change in parameters *) + mkProj (p, a') + else mkApp (app', [| a' |]) | _ -> map_constr_with_binders_left_to_right sigma g f acc c let e_contextually byhead (occs,c) f = begin fun env sigma t -> @@ -1197,7 +1197,7 @@ let abstract_scheme env sigma (locc,a) (c, sigma) = let pattern_occs loccs_trm = begin fun env sigma c -> let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in try - let _ = Typing.unsafe_type_of env sigma abstr_trm in + let sigma, _ = Typing.type_of env sigma abstr_trm in (sigma, applist(abstr_trm, List.map snd loccs_trm)) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) @@ -1311,11 +1311,9 @@ let reduce_to_ref_gen allow_product env sigma ref t = else error_cannot_recognize ref | _ -> - try - if GlobRef.equal (fst (global_of_constr sigma c)) ref - then it_mkProd_or_LetIn t l - else raise Not_found - with Not_found -> + if isRefX sigma ref c + then it_mkProd_or_LetIn t l + else try let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in elimrec env t' l diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index be4c681cc7..65e3421736 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 1541e96635..afd6c33821 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -31,13 +31,9 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen let get_typeclasses_unique_solutions = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"check that typeclasses proof search returns unique solutions" ~key:["Typeclasses";"Unique";"Solutions"] ~value:false -let (set_typeclass_transparency, set_typeclass_transparency_hook) = Hook.make () -let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency gr local c - let (classes_transparent_state, classes_transparent_state_hook) = Hook.make () let classes_transparent_state () = Hook.get classes_transparent_state () @@ -107,9 +103,9 @@ let class_info env sigma c = not_a_class env sigma (EConstr.of_constr (printable_constr_of_global c)) let global_class_of_constr env sigma c = - try let gr, u = Termops.global_of_constr sigma c in + try let gr, u = EConstr.destRef sigma c in GlobRef.Map.find gr !classes, u - with Not_found -> not_a_class env sigma c + with DestKO | Not_found -> not_a_class env sigma c let dest_class_app env sigma c = let cl, args = EConstr.decompose_app sigma c in @@ -125,9 +121,9 @@ let class_of_constr env sigma c = with e when CErrors.noncritical e -> None let is_class_constr sigma c = - try let gr, u = Termops.global_of_constr sigma c in + try let gr, u = EConstr.destRef sigma c in GlobRef.Map.mem gr !classes - with Not_found -> false + with DestKO | Not_found -> false let rec is_class_type evd c = let c, _ = Termops.decompose_app_vect evd c in @@ -140,9 +136,9 @@ let is_class_evar evd evi = is_class_type evd evi.Evd.evar_concl let is_class_constr sigma c = - try let gr, u = Termops.global_of_constr sigma c in + try let gr, u = EConstr.destRef sigma c in GlobRef.Map.mem gr !classes - with Not_found -> false + with DestKO | Not_found -> false let rec is_maybe_class_type evd c = let c, _ = Termops.decompose_app_vect evd c in diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 2715c1eda5..9de8083276 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -122,9 +122,6 @@ val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr -val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t -val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit - val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t val classes_transparent_state : unit -> TransparentState.t diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index a335ba8b0b..967be723f3 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 3b58b4a16e..1e6796839a 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index a15134f58d..99a35849e0 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -27,6 +27,8 @@ open Arguments_renaming open Pretype_errors open Context.Rel.Declaration +module GR = Names.GlobRef + let meta_type evd mv = let ty = try Evd.meta_ftype evd mv @@ -36,8 +38,11 @@ let meta_type evd mv = let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in - let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in - Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp + let paramstyp = Array.map_to_list (fun j () -> + let s = Reductionops.sort_of_arity env sigma j.uj_type in + Sorts.univ_of_sort (EConstr.ESorts.kind sigma s)) jl + in + Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with @@ -253,6 +258,9 @@ let judge_of_type u = let judge_of_relative env v = Environ.on_judgment EConstr.of_constr (judge_of_relative env v) +let type_of_variable env id = + EConstr.of_constr (type_of_variable env id) + let judge_of_variable env id = Environ.on_judgment EConstr.of_constr (judge_of_variable env id) @@ -284,37 +292,36 @@ let judge_of_letin env name defj typj j = { uj_val = mkLetIn (make_annot name r, defj.uj_val, typj.utj_val, j.uj_val) ; uj_type = subst1 defj.uj_val j.uj_type } -let check_hyps_inclusion env sigma f x hyps = +let check_hyps_inclusion env sigma x hyps = let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in - let f x = EConstr.Unsafe.to_constr (f x) in - Typeops.check_hyps_inclusion env ~evars f x hyps + Typeops.check_hyps_inclusion env ~evars x hyps let type_of_constant env sigma (c,u) = let open Declarations in let cb = Environ.lookup_constant c env in - let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in + let () = check_hyps_inclusion env sigma (GR.ConstRef c) cb.const_hyps in let u = EInstance.kind sigma u in let ty, csts = Environ.constant_type env (c,u) in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c))) + sigma, (EConstr.of_constr (rename_type ty (GR.ConstRef c))) let type_of_inductive env sigma (ind,u) = let open Declarations in let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in + let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in - let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in + let ty, csts = Inductive.constrained_type_of_inductive (specif,u) in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind))) + sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind))) let type_of_constructor env sigma ((ind,_ as ctor),u) = let open Declarations in let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in + let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor))) + sigma, (EConstr.of_constr (rename_type ty (GR.ConstructRef ctor))) let judge_of_int env v = Environ.on_judgment EConstr.of_constr (judge_of_int env v) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1b07b2bb78..96222f7bf6 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,6 +19,7 @@ open Evd (** Typecheck a term and return its type. May trigger an evarmap leak. *) val unsafe_type_of : env -> evar_map -> constr -> types +[@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) @@ -30,6 +31,9 @@ val sort_of : env -> evar_map -> types -> evar_map * Sorts.t (** Typecheck a term has a given type (assuming the type is OK) *) val check : env -> evar_map -> constr -> types -> evar_map +(** Type of a variable. *) +val type_of_variable : env -> variable -> types + (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 48d5fac321..ec3fb0758e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -46,7 +46,6 @@ module NamedDecl = Context.Named.Declaration let keyed_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Unification is keyed"; optkey = ["Keyed";"Unification"]; optread = (fun () -> !keyed_unification); optwrite = (fun a -> keyed_unification:=a); @@ -57,8 +56,6 @@ let is_keyed_unification () = !keyed_unification let debug_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print states sent to tactic unification"; optkey = ["Debug";"Tactic";"Unification"]; optread = (fun () -> !debug_unification); optwrite = (fun a -> debug_unification:=a); @@ -1152,10 +1149,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); a with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); - iraise e - + Exninfo.iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env @@ -1274,12 +1270,14 @@ let applyHead env evd n c = else match EConstr.kind evd (whd_all env evd cty) with | Prod (_,c1,c2) -> - let (evd',evar) = - Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in - apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' + let (evd,evar) = + Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 + in + apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd | _ -> user_err Pp.(str "Apply_Head_Then") in - apprec n c (Typing.unsafe_type_of env evd c) evd + let evd, t = Typing.type_of env evd c in + apprec n c t evd let is_mimick_head sigma ts f = match EConstr.kind sigma f with @@ -1290,7 +1288,7 @@ let is_mimick_head sigma ts f = let try_to_coerce env evd c cty tycon = let j = make_judge c cty in - let (evd',j') = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in + let (evd',j',_trace) = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in (evd',j'.uj_val) diff --git a/pretyping/unification.mli b/pretyping/unification.mli index e66234b4ae..f9a969a253 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 885fc8980d..64068724af 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -98,7 +98,7 @@ let construct_of_constr_const env tag typ = let construct_of_constr_block = construct_of_constr false let type_of_ind env (ind, u) = - type_of_inductive env (Inductive.lookup_mind_specif env ind, u) + type_of_inductive (Inductive.lookup_mind_specif env ind, u) let build_branches_type env sigma (mind,_ as _ind) mib mip u params p = let rtbl = mip.mind_reloc_tbl in diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index 07f1696032..ae36a8275a 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |