diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 836 |
1 files changed, 429 insertions, 407 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4b6d10c6..c7db802f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This file contains the syntax-directed part of the type inference @@ -27,12 +29,13 @@ open Util open Names open Evd open Term -open Vars open Termops -open Reductionops open Environ +open EConstr +open Vars +open Reductionops open Type_errors -open Typeops +open Typing open Globnames open Nameops open Evarutil @@ -41,25 +44,12 @@ open Pretype_errors open Glob_term open Glob_ops open Evarconv -open Pattern open Misctypes -open Sigma.Notations -open Context.Named.Declaration +open Ltac_pretype + +module NamedDecl = Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type var_map = constr_under_binders Id.Map.t -type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t -type ltac_var_map = { - ltac_constrs : var_map; - ltac_uconstrs : uconstr_var_map; - ltac_idents: Id.t Id.Map.t; - ltac_genargs : unbound_ltac_var_map; -} -type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * constr -type 'a delayed_open = - { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } (************************************************************************) (* This concerns Cases *) @@ -77,47 +67,46 @@ type t = { (** Delay the computation of the evar extended environment *) } -let get_extra env = +let get_extra env sigma = let open Context.Named.Declaration in let ids = List.map get_id (named_context env) in let avoid = List.fold_right Id.Set.add ids Id.Set.empty in - Context.Rel.fold_outside push_rel_decl_to_named_context - (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env) + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) + (rel_context env) ~init:(empty_csubst, avoid, named_context env) -let make_env env = { env = env; extra = lazy (get_extra env) } +let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) } let rel_context env = rel_context env.env -let push_rel d env = { +let push_rel sigma d env = { env = push_rel d env.env; - extra = lazy (push_rel_decl_to_named_context d (Lazy.force env.extra)); + extra = lazy (push_rel_decl_to_named_context sigma d (Lazy.force env.extra)); } -let pop_rel_context n env = make_env (pop_rel_context n env.env) +let pop_rel_context n env sigma = make_env (pop_rel_context n env.env) sigma -let push_rel_context ctx env = { +let push_rel_context sigma ctx env = { env = push_rel_context ctx env.env; - extra = lazy (List.fold_right push_rel_decl_to_named_context ctx (Lazy.force env.extra)); + extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx (Lazy.force env.extra)); } let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = - let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in - let inst_vars = List.map (fun d -> mkVar (get_id d)) (named_context env.env) in + let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in - let (subst, vsubst, _, nc) = Lazy.force env.extra in - let typ' = subst2 subst vsubst typ in + let (subst, _, nc) = Lazy.force env.extra in + let typ' = csubst_subst subst typ in let instance = inst_rels @ inst_vars in let sign = val_of_named_context nc in - let sigma = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in - evdref := Sigma.to_evar_map sigma; + let sigma = !evdref in + let (sigma, e) = new_evar_instance sign sigma typ' ?src ?naming instance in + evdref := sigma; e -let push_rec_types (lna,typarray,_) env = +let push_rec_types sigma (lna,typarray,_) env = let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in - Array.fold_left (fun e assum -> push_rel assum e) env ctxt + Array.fold_left (fun e assum -> push_rel sigma assum e) env ctxt end @@ -127,7 +116,11 @@ open ExtraEnv exception Found of int array -let search_guard loc env possible_indexes fixdefs = +let nf_fix sigma (nas, cs, ts) = + let inj c = EConstr.to_constr sigma c in + (nas, Array.map inj cs, Array.map inj ts) + +let search_guard ?loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in @@ -137,7 +130,7 @@ let search_guard loc env possible_indexes fixdefs = (try check_fix env fix with reraise -> let (e, info) = CErrors.push reraise in - let info = Loc.add_loc info loc in + let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in iraise (e, info)); indexes else @@ -160,7 +153,7 @@ let search_guard loc env possible_indexes fixdefs = with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in - user_err_loc (loc,"search_guard", Pp.str errmsg) + user_err ?loc ~hdr:"search_guard" (Pp.str errmsg) with Found indexes -> indexes) (* To force universe name declaration before use *) @@ -170,8 +163,7 @@ let is_strict_universe_declarations () = !strict_universe_declarations let _ = Goptions.(declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "strict universe declaration"; optkey = ["Strict";"Universe";"Declaration"]; optread = is_strict_universe_declarations; @@ -179,67 +171,86 @@ let _ = let _ = Goptions.(declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "minimization to Set"; optkey = ["Universe";"Minimization";"ToSet"]; optread = Universes.is_set_minimization; optwrite = (:=) Universes.set_minimization }) - + (** Miscellaneous interpretation functions *) -let interp_universe_level_name evd (loc,s) = - let names, _ = Universes.global_universe_names () in - if CString.string_contains s "." then - match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s) - | n :: dp -> - let num = int_of_string n in - let dp = DirPath.make (List.map Id.of_string dp) in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - else - try - let level = Evd.universe_of_name evd s in - evd, level - with Not_found -> - try - let id = try Id.of_string s with _ -> raise Not_found in - evd, snd (Idmap.find id names) - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ~loc ~name:s univ_rigid evd - else user_err_loc (loc, "interp_universe_level_name", - Pp.(str "Undeclared universe: " ++ str s)) + +let interp_known_universe_level evd r = + let qid = Libnames.qualid_of_reference r in + try + match r.CAst.v with + | Libnames.Ident id -> Evd.universe_of_name evd id + | Libnames.Qualid _ -> raise Not_found + with Not_found -> + let univ, k = Nametab.locate_universe qid.CAst.v in + Univ.Level.make univ k + +let interp_universe_level_name ~anon_rigidity evd r = + try evd, interp_known_universe_level evd r + with Not_found -> + match r with (* Qualified generated name *) + | {CAst.loc; v=Libnames.Qualid qid} -> + let dp, i = Libnames.repr_qualid qid in + let num = + try int_of_string (Id.to_string i) + with Failure _ -> + user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r)) + in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level + | {CAst.loc; v=Libnames.Ident id} -> (* Undeclared *) + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc ~name:id univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in evd, Univ.Universe.make l | l -> - List.fold_left (fun (evd, u) l -> - let evd', l = interp_universe_level_name evd l in - (evd', Univ.sup u (Univ.Universe.make l))) + List.fold_left (fun (evd, u) l -> + let evd', u' = + match l with + | Some (l,n) -> + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let anon_rigidity = univ_flexible in + let evd', l = interp_universe_level_name ~anon_rigidity evd l in + let u' = Univ.Universe.make l in + (match n with + | 0 -> evd', u' + | 1 -> evd', Univ.Universe.super u' + | _ -> + user_err ?loc ~hdr:"interp_universe" + (Pp.(str "Cannot interpret universe increment +" ++ int n))) + | None -> + let evd, l = new_univ_level_variable ?loc univ_flexible evd in + evd, Univ.Universe.make l + in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l -let interp_universe_level loc evd = function - | None -> new_univ_level_variable ~loc univ_rigid evd - | Some (loc,s) -> interp_universe_level_name evd (loc,s) - -let interp_sort ?loc evd = function - | GProp -> evd, Prop Null - | GSet -> evd, Prop Pos - | GType n -> - let evd, u = interp_universe ?loc evd n in - evd, Type u +let interp_known_level_info ?loc evd = function + | UUnknown | UAnonymous -> + user_err ?loc ~hdr:"interp_known_level_info" + (str "Anonymous universes not allowed here.") + | UNamed ref -> + try interp_known_universe_level evd ref + with Not_found -> + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) -let interp_elimination_sort = function - | GProp -> InProp - | GSet -> InSet - | GType _ -> InType +let interp_level_info ?loc evd : Misctypes.level_info -> _ = function + | UUnknown -> new_univ_level_variable ?loc univ_rigid evd + | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd + | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s -type inference_hook = env -> evar_map -> evar -> evar_map * constr +type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr type inference_flags = { use_typeclasses : bool; @@ -257,16 +268,36 @@ type inference_flags = { [sigma'] into those already in [sigma] or deriving from an evar in [sigma] by restriction, and the evars properly created in [sigma'] *) +type frozen = +| FrozenId of evar_info Evar.Map.t + (** No pending evars. We do not put a set here not to reallocate like crazy, + but the actual data of the map is not used, only keys matter. All + functions operating on this type must have the same behaviour on + [FrozenId map] and [FrozenProgress (Evar.Map.domain map, Evar.Set.empty)] *) +| FrozenProgress of (Evar.Set.t * Evar.Set.t) Lazy.t + (** Proper partition of the evar map as described above. *) + let frozen_and_pending_holes (sigma, sigma') = - let add_derivative_of evk evi acc = - match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in - let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in - let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in - let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in - (frozen,pending) + let undefined0 = Evd.undefined_map sigma in + (** Fast path when the undefined evars where not modified *) + if undefined0 == Evd.undefined_map sigma' then + FrozenId undefined0 + else + let data = lazy begin + let add_derivative_of evk evi acc = + match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in + let frozen = Evar.Map.fold add_derivative_of undefined0 Evar.Set.empty in + let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in + let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in + (frozen, pending) + end in + FrozenProgress data let apply_typeclasses env evdref frozen fail_evar = - let filter_frozen evk = Evar.Set.mem evk frozen in + let filter_frozen = match frozen with + | FrozenId map -> fun evk -> Evar.Map.mem evk map + | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen + in evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk)) @@ -276,13 +307,15 @@ let apply_typeclasses env evdref frozen fail_evar = evdref := Typeclasses.resolve_typeclasses ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref -let apply_inference_hook hook evdref pending = +let apply_inference_hook hook evdref frozen = match frozen with +| FrozenId _ -> () +| FrozenProgress (lazy (_, pending)) -> evdref := 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 sigma evk in - Evd.define evk c sigma + Evd.define evk (EConstr.Unsafe.to_constr c) sigma with Exit -> sigma else @@ -299,7 +332,9 @@ let check_typeclasses_instances_are_solved env current_sigma frozen = (* Naive way, call resolution again with failure flag *) apply_typeclasses env (ref current_sigma) frozen true -let check_extra_evars_are_solved env current_sigma pending = +let check_extra_evars_are_solved env current_sigma frozen = match frozen with +| FrozenId _ -> () +| FrozenProgress (lazy (_, pending)) -> Evar.Set.iter (fun evk -> if not (Evd.is_defined current_sigma evk) then @@ -307,67 +342,76 @@ let check_extra_evars_are_solved env current_sigma pending = match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () | _ -> - error_unsolvable_implicit loc env current_sigma evk None) pending + error_unsolvable_implicit ?loc env current_sigma evk None) pending (* [check_evars] fails if some unresolved evar remains *) let check_evars env initial_sigma sigma c = let rec proc_rec c = - match kind_of_term c with - | Evar (evk,_ as ev) -> - (match existential_opt_value sigma ev with - | Some c -> proc_rec c - | None -> - if not (Evd.mem initial_sigma evk) then - let (loc,k) = evar_source evk sigma in - match k with - | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> Pretype_errors.error_unsolvable_implicit loc env sigma evk None) - | _ -> Constr.iter proc_rec c + match EConstr.kind sigma c with + | Evar (evk, _) -> + if not (Evd.mem initial_sigma evk) then + let (loc,k) = evar_source evk sigma in + begin match k with + | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () + | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None + end + | _ -> EConstr.iter sigma proc_rec c in proc_rec c -let check_evars_are_solved env current_sigma frozen pending = +let check_evars_are_solved env current_sigma frozen = check_typeclasses_instances_are_solved env current_sigma frozen; check_problems_are_solved env current_sigma; - check_extra_evars_are_solved env current_sigma pending + check_extra_evars_are_solved env current_sigma frozen (* Try typeclasses, hooks, unification heuristics ... *) -let solve_remaining_evars flags env current_sigma pending = - let frozen,pending = frozen_and_pending_holes pending in +let solve_remaining_evars flags env current_sigma init_sigma = + let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in let evdref = ref current_sigma in if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then - apply_inference_hook (Option.get flags.use_hook env) evdref pending; + apply_inference_hook (Option.get flags.use_hook env) evdref frozen; if flags.solve_unification_constraints then apply_heuristics env evdref false; - if flags.fail_evar then check_evars_are_solved env !evdref frozen pending; + if flags.fail_evar then check_evars_are_solved env !evdref frozen; !evdref -let check_evars_are_solved env current_sigma pending = - let frozen,pending = frozen_and_pending_holes pending in - check_evars_are_solved env current_sigma frozen pending +let check_evars_are_solved env current_sigma init_sigma = + let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in + check_evars_are_solved env current_sigma frozen -let process_inference_flags flags env initial_sigma (sigma,c) = - let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in +let process_inference_flags flags env initial_sigma (sigma,c,cty) = + let sigma = solve_remaining_evars flags env sigma initial_sigma in let c = if flags.expand_evars then nf_evar sigma c else c in - sigma,c - -(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) -let allow_anonymous_refs = ref false + sigma,c,cty + +let adjust_evar_source evdref na c = + match na, kind !evdref c with + | Name id, Evar (evk,args) -> + let evi = Evd.find !evdref evk in + begin match evi.evar_source with + | loc, Evar_kinds.QuestionMark (b,Anonymous) -> + let src = (loc,Evar_kinds.QuestionMark (b,na)) in + let (evd, evk') = restrict_evar !evdref evk (evar_filter evi) ~src None in + evdref := evd; + mkEvar (evk',args) + | _ -> c + end + | _, _ -> c (* coerce to tycon if any *) -let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function +let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t + evd_comb2 (Coercion.inh_conv_coerce_to ?loc resolve_tc env.ExtraEnv.env) evdref j t let check_instance loc subst = function | [] -> () | (id,_) :: _ -> if List.mem_assoc id subst then - user_err_loc (loc,"",pr_id id ++ str "appears more than once.") + user_err ?loc (Id.print id ++ str "appears more than once.") else - user_err_loc (loc,"",str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".") + user_err ?loc (str "No such variable in the signature of the existential variable: " ++ Id.print id ++ str ".") (* used to enforce a name in Lambda when the type constraints itself is named, hence possibly dependent *) @@ -376,18 +420,7 @@ let orelse_name name name' = match name with | Anonymous -> name' | _ -> name -let ltac_interp_name { ltac_idents ; ltac_genargs } = function - | Anonymous -> Anonymous - | Name id as n -> - try Name (Id.Map.find id ltac_idents) - with Not_found -> - if Id.Map.mem id ltac_genargs then - errorlabstrm "" (str"Ltac variable"++spc()++ pr_id id ++ - spc()++str"is not bound to an identifier."++spc()++ - str"It cannot be used in a binder.") - else n - -let ltac_interp_name_env k0 lvar env = +let ltac_interp_name_env k0 lvar env sigma = (* envhd is the initial part of the env when pretype was called first *) (* (in practice is is probably 0, but we have to grant the specification of pretype which accepts to start with a non empty @@ -398,20 +431,20 @@ let ltac_interp_name_env k0 lvar env = let open Context.Rel.Declaration in let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env - else push_rel_context ctxt' (pop_rel_context n env) + else push_rel_context sigma ctxt' (pop_rel_context n env sigma) let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in try mkRel (pi1 (lookup_rel_id id' (rel_context env))) with Not_found -> - errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++ - str " depends on pattern variable name " ++ pr_id id ++ + user_err (str "Ltac variable " ++ Id.print id0 ++ + str " depends on pattern variable name " ++ Id.print id ++ str " which is not bound in current context.") let protected_get_type_of env sigma c = try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c with Retyping.RetypeError _ -> - errorlabstrm "" + user_err (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") @@ -422,7 +455,7 @@ let pretype_id pretype k0 loc env evdref lvar id = let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in (* Check if [id] is an ltac variable *) try let (ids,c) = Id.Map.find id lvar.ltac_constrs in @@ -447,136 +480,154 @@ let pretype_id pretype k0 loc env evdref lvar id = (* and build a nice error message *) if Id.Map.mem id lvar.ltac_genargs then begin let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in - user_err_loc (loc,"", - str "Variable " ++ pr_id id ++ str " should be bound to a term but is \ + user_err ?loc + (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \ bound to a " ++ Geninterp.Val.pr typ ++ str ".") end; (* Check if [id] is a section or goal variable *) try - { uj_val = mkVar id; uj_type = (get_type (lookup_named id env)) } + { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } with Not_found -> (* [id] not found, standard error message *) - error_var_not_found_loc loc id - -let evar_kind_of_term sigma c = - kind_of_term (whd_evar sigma c) + error_var_not_found ?loc id (*************************************************************************) (* Main pretyping function *) -let interp_universe_level_name loc evd l = - match l with +let interp_known_glob_level ?loc evd = function + | GProp -> Univ.Level.prop + | GSet -> Univ.Level.set + | GType s -> interp_known_level_info ?loc evd s + +let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set - | GType s -> interp_universe_level loc evd s + | GType s -> interp_level_info ?loc evd s + +let interp_instance ?loc evd ~len l = + if len != List.length l then + user_err ?loc ~hdr:"pretype" + (str "Universe instance should have length " ++ int len) + else + let evd, l' = + List.fold_left + (fun (evd, univs) l -> + let evd, l = interp_glob_level ?loc evd l in + (evd, l :: univs)) (evd, []) + l + in + if List.exists (fun l -> Univ.Level.is_prop l) l' then + user_err ?loc ~hdr:"pretype" + (str "Universe instances cannot contain Prop, polymorphic" ++ + str " universe instances must be greater or equal to Set."); + evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) -let pretype_global loc rigid env evd gr us = +let pretype_global ?loc rigid env evd gr us = let evd, instance = match us with | None -> evd, None | Some l -> - let _, ctx = Universes.unsafe_constr_of_global gr in - let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in - let len = Array.length arr in - if len != List.length l then - user_err_loc (loc, "pretype", - str "Universe instance should have length " ++ int len) - else - let evd, l' = List.fold_left (fun (evd, univs) l -> - let evd, l = interp_universe_level_name loc evd l in - (evd, l :: univs)) (evd, []) l - in - if List.exists (fun l -> Univ.Level.is_prop l) l' then - user_err_loc (loc, "pretype", - str "Universe instances cannot contain Prop, polymorphic" ++ - str " universe instances must be greater or equal to Set."); - evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) + let _, ctx = Global.constr_of_global_in_context env.ExtraEnv.env gr in + let len = Univ.AUContext.size ctx in + interp_instance ?loc evd ~len l in - Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr + let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in + (sigma, EConstr.of_constr c) -let pretype_ref loc evdref env ref us = +let pretype_ref ?loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) - (try make_judge (mkVar id) (get_type (lookup_named id env)) + (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env)) with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal variables *) - Pretype_errors.error_var_not_found_loc loc id) + Pretype_errors.error_var_not_found ?loc id) | ref -> - let evd, c = pretype_global loc univ_flexible env !evdref ref us in + let evd, c = pretype_global ?loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in + let ty = unsafe_type_of env.ExtraEnv.env evd c in make_judge c ty -let judge_of_Type loc evd s = - let evd, s = interp_universe ~loc evd s in +let judge_of_Type ?loc evd s = + let evd, s = interp_universe ?loc evd s in let judge = { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } in evd, judge -let pretype_sort loc evdref = function +let pretype_sort ?loc evdref = function | GProp -> judge_of_prop | GSet -> judge_of_set - | GType s -> evd_comb1 (judge_of_Type loc) evdref s + | GType s -> evd_comb1 (judge_of_Type ?loc) evdref s let new_type_evar env evdref loc = - let sigma = Sigma.Unsafe.of_evar_map !evdref in - let Sigma ((e, _), sigma, _) = + let sigma = !evdref in + let (sigma, (e, _)) = Evarutil.new_type_evar env.ExtraEnv.env sigma univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) in - evdref := Sigma.to_evar_map sigma; + evdref := sigma; e -let (f_genarg_interp, genarg_interp_hook) = Hook.make () +module ConstrInterpObj = +struct + type ('r, 'g, 't) obj = + unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map + let name = "constr_interp" + let default _ = None +end + +module ConstrInterp = Genarg.Register(ConstrInterpObj) + +let register_constr_interp0 = ConstrInterp.register0 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t = - let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in + let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in let open Context.Rel.Declaration in - match t with - | GRef (loc,ref,u) -> - inh_conv_coerce_to_tycon loc env evdref - (pretype_ref loc evdref env ref u) + let loc = t.CAst.loc in + match DAst.get t with + | GRef (ref,u) -> + inh_conv_coerce_to_tycon ?loc env evdref + (pretype_ref ?loc evdref env ref u) tycon - | GVar (loc, id) -> - inh_conv_coerce_to_tycon loc env evdref + | GVar id -> + inh_conv_coerce_to_tycon ?loc env evdref (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id) tycon - | GEvar (loc, id, inst) -> + | GEvar (id, inst) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) let evk = try Evd.evar_key id !evdref with Not_found -> - user_err_loc (loc,"",str "Unknown existential variable.") in + user_err ?loc (str "Unknown existential variable.") in let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in - inh_conv_coerce_to_tycon loc env evdref j tycon + inh_conv_coerce_to_tycon ?loc env evdref j tycon - | GPatVar (loc,(someta,n)) -> - let env = ltac_interp_name_env k0 lvar env in + | GPatVar kind -> + let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty | None -> new_type_evar env evdref loc in - let k = Evar_kinds.MatchingVar (someta,n) in + let k = Evar_kinds.MatchingVar kind in { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } - | GHole (loc, k, naming, None) -> - let env = ltac_interp_name_env k0 lvar env in + | GHole (k, naming, None) -> + let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty @@ -584,37 +635,40 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre new_type_evar env evdref loc in { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } - | GHole (loc, k, _naming, Some arg) -> - let env = ltac_interp_name_env k0 lvar env in + | GHole (k, _naming, Some arg) -> + let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty | None -> new_type_evar env evdref loc in + let open Genarg in let ist = lvar.ltac_genargs in - let (c, sigma) = Hook.get f_genarg_interp ty env.ExtraEnv.env !evdref ist arg in + let GenArg (Glbwit tag, arg) = arg in + let interp = ConstrInterp.obj tag in + let (c, sigma) = interp ist env.ExtraEnv.env !evdref ty arg in let () = evdref := sigma in { uj_val = c; uj_type = ty } - | GRec (loc,fixkind,names,bl,lar,vdef) -> + | GRec (fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function [] -> ctxt | (na,bk,None,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let dcl = LocalAssum (na, ty'.utj_val) in let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in - type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl + type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in - type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in + type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl in let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = Array.map2 (fun e ar -> - pretype_type empty_valcon (push_rel_context e env) evdref lvar ar) + pretype_type empty_valcon (push_rel_context !evdref e env) evdref lvar ar) ctxtv lar in let lara = Array.map (fun a -> a.utj_val) larj in let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in @@ -630,23 +684,24 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | None -> true in (* Note: bodies are not used by push_rec_types, so [||] is safe *) - let newenv = push_rec_types (names,ftys,[||]) env in + let newenv = push_rec_types !evdref (names,ftys,[||]) env in let vdefj = Array.map2_i (fun i ctxt def -> (* we lift nbfix times the type in tycon, because of * the nbfix variables pushed to newenv *) let (ctxt,ty) = - decompose_prod_n_assum (Context.Rel.length ctxt) + decompose_prod_n_assum !evdref (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in - let nenv = push_rel_context ctxt newenv in + let nenv = push_rel_context !evdref ctxt newenv in let j = pretype (mk_tycon ty) nenv evdref lvar def in { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj; - let ftys = Array.map (nf_evar !evdref) ftys in - let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in + Typing.check_type_fixpoint ?loc env.ExtraEnv.env evdref names ftys vdefj; + let nf c = nf_evar !evdref c in + let ftys = Array.map nf ftys in (** FIXME *) + let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in let fixj = match fixkind with | GFix (vn,i) -> (* First, let's find the guard indexes. *) @@ -665,25 +720,26 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - loc env.ExtraEnv.env possible_indexes fixdecls + ?loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls) in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> - let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env.ExtraEnv.env cofix + let fixdecls = (names,ftys,fdefs) in + let cofix = (i, fixdecls) in + (try check_cofix env.ExtraEnv.env (i, nf_fix !evdref fixdecls) with reraise -> let (e, info) = CErrors.push reraise in - let info = Loc.add_loc info loc in + let info = Option.cata (Loc.add_loc info) info loc in iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon loc env evdref fixj tycon + inh_conv_coerce_to_tycon ?loc env evdref fixj tycon - | GSort (loc,s) -> - let j = pretype_sort loc evdref s in - inh_conv_coerce_to_tycon loc env evdref j tycon + | GSort s -> + let j = pretype_sort ?loc evdref s in + inh_conv_coerce_to_tycon ?loc env evdref j tycon - | GApp (loc,f,args) -> + | GApp (f,args) -> let fj = pretype empty_tycon env evdref lvar f in let floc = loc_of_glob_constr f in let length = List.length args in @@ -691,24 +747,24 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* Bidirectional typechecking hint: parameters of a constructor are completely determined by a typing constraint *) - if Flags.is_program_mode () && length > 0 && isConstruct fj.uj_val then + if Flags.is_program_mode () && length > 0 && isConstruct !evdref fj.uj_val then match tycon with | None -> [] | Some ty -> - let ((ind, i), u) = destConstruct fj.uj_val in + let ((ind, i), u) = destConstruct !evdref fj.uj_val in let npars = inductive_nparams ind in if Int.equal npars 0 then [] else try let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in let ((ind',u'),pars) = dest_ind_family indf in - if eq_ind ind ind' then pars + if eq_ind ind ind' then List.map EConstr.of_constr pars else (* Let the usual code throw an error *) [] with Not_found -> [] else [] in let app_f = - match kind_of_term fj.uj_val with + match EConstr.kind !evdref fj.uj_val with | Const (p, u) when Environ.is_projection p env.ExtraEnv.env -> let p = Projection.make p false in let pb = Environ.lookup_projection p env.ExtraEnv.env in @@ -724,7 +780,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let argloc = loc_of_glob_constr c in let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in - match kind_of_term resty with + match EConstr.kind !evdref resty with | Prod (na,c1,c2) -> let tycon = Some c1 in let hj = pretype tycon env evdref lvar c in @@ -736,57 +792,56 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre args, nf_evar !evdref (j_val hj) else [], j_val hj in + let ujval = adjust_evar_source evdref na 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 (n+1) j candargs rest | _ -> let hj = pretype empty_tycon env evdref lvar c in - error_cant_apply_not_functional_loc - (Loc.merge floc argloc) env.ExtraEnv.env !evdref - resj [hj] + error_cant_apply_not_functional + ?loc:(Loc.merge_opt floc argloc) env.ExtraEnv.env !evdref + resj [|hj|] in let resj = apply_rec env 1 fj candargs args in let resj = - match evar_kind_of_term !evdref resj.uj_val with + match EConstr.kind !evdref resj.uj_val with | App (f,args) -> - let f = whd_evar !evdref f in - if is_template_polymorphic env.ExtraEnv.env f then + if is_template_polymorphic env.ExtraEnv.env !evdref f then (* Special case for inductive type applications that must be refreshed right away. *) - let sigma = !evdref in - let c = mkApp (f,Array.map (whd_evar sigma) args) in + let c = mkApp (f, args) in let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj in - inh_conv_coerce_to_tycon loc env evdref resj tycon + inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GLambda(loc,name,bk,c1,c2) -> + | GLambda(name,bk,c1,c2) -> let tycon' = evd_comb1 (fun evd tycon -> match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in + let evd, ty' = Coercion.inh_coerce_to_prod ?loc env.ExtraEnv.env evd ty in evd, Some ty') evdref tycon in - let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon ?loc env.ExtraEnv.env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) let var = LocalAssum (name, j.utj_val) in - let j' = pretype rng (push_rel var env) evdref lvar c2 in + let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in - inh_conv_coerce_to_tycon loc env evdref resj tycon + inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GProd(loc,name,bk,c1,c2) -> + | GProd(name,bk,c1,c2) -> let j = pretype_type empty_valcon env evdref lvar c1 in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are @@ -797,7 +852,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { j with utj_val = lift 1 j.utj_val } | Name _ -> let var = LocalAssum (name, j.utj_val) in - let env' = push_rel var env in + let env' = push_rel !evdref var env in pretype_type empty_valcon env' evdref lvar c2 in let name = ltac_interp_name lvar name in @@ -806,18 +861,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre judge_of_product env.ExtraEnv.env name j j' with TypeError _ as e -> let (e, info) = CErrors.push e in - let info = Loc.add_loc info loc in + let info = Option.cata (Loc.add_loc info) info loc in iraise (e, info) in - inh_conv_coerce_to_tycon loc env evdref resj tycon + inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GLetIn(loc,name,c1,c2) -> - let j = - match c1 with - | GCast (loc, c, CastConv t) -> - let tj = pretype_type empty_valcon env evdref lvar t in - pretype (mk_tycon tj.utj_val) env evdref lvar c - | _ -> pretype empty_tycon env evdref lvar c1 - in + | GLetIn(name,c1,t,c2) -> + let tycon1 = + match t with + | Some t -> + mk_tycon (pretype_type empty_valcon env evdref lvar t).utj_val + | None -> + empty_tycon in + let j = pretype tycon1 env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref j.uj_type in @@ -826,28 +881,29 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre looked up in the rel context. *) let var = LocalDef (name, j.uj_val, t) in let tycon = lift_tycon 1 tycon in - let j' = pretype tycon (push_rel var env) evdref lvar c2 in + let j' = pretype tycon (push_rel !evdref var env) evdref lvar c2 in let name = ltac_interp_name lvar name in { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } - | GLetTuple (loc,nal,(na,po),c,d) -> + | GLetTuple (nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj + error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then - user_err_loc (loc,"",str "Destructing let is only for inductive types" ++ + user_err ?loc (str "Destructing let is only for inductive types" ++ str " with one constructor."); let cs = cstrs.(0) in if not (Int.equal (List.length nal) cs.cs_nargs) then - user_err_loc (loc,"", str "Destructing let on this type expects " ++ + user_err ?loc:loc (str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); let fsign, record = + let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in match get_projections env.ExtraEnv.env indf with | None -> List.map2 set_name (List.rev nal) cs.cs_args, false @@ -855,6 +911,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let rec aux n k names l = match names, l with | na :: names, (LocalAssum (_,t) :: l) -> + let t = EConstr.of_constr t in let proj = Projection.make ps.(cs.cs_nargs - k) true in LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) :: aux (n+1) (k + 1) names l @@ -863,6 +920,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in + let fsign = if Flags.version_strictly_greater Flags.V8_6 + then Context.Rel.map (whd_betaiota !evdref) fsign + else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in let obj ind p v f = if not record then let nal = List.map (fun na -> ltac_interp_name lvar na) nal in @@ -873,26 +933,29 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in - let env_f = push_rel_context fsign env in + let env_f = push_rel_context !evdref fsign env in (* Make dependencies from arity signature impossible *) let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in - if not !allow_anonymous_refs then - List.map (set_name Anonymous) arsgn - else arsgn + List.map (set_name Anonymous) arsgn in - let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in + let indt = build_dependent_inductive env.ExtraEnv.env indf in + let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) + let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in + let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in + let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in + let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *) + let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let nar = List.length arsgn in (match po with | Some p -> - let env_p = push_rel_context psign env in - let pj = pretype_type empty_valcon env_p evdref lvar p in + let env_p = push_rel_context !evdref psign env in + let pj = pretype_type empty_valcon env_p evdref predlvar p in let ccl = nf_evar !evdref pj.utj_val in - let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) - let p = it_mkLambda_or_LetIn ccl psign in + let p = it_mkLambda_or_LetIn ccl psign' in let inst = - (Array.to_list cs.cs_concl_realargs) - @[build_dependent_constructor cs] in + (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs) + @[EConstr.of_constr (build_dependent_constructor cs)] in let lp = lift cs.cs_nargs p in let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in let fj = pretype (mk_tycon fty) env_f evdref lvar d in @@ -901,80 +964,84 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in - { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } + { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) } | None -> let tycon = lift_tycon cs.cs_nargs tycon in - let fj = pretype tycon env_f evdref lvar d in + let fj = pretype tycon env_f evdref predlvar d in let ccl = nf_evar !evdref fj.uj_type in let ccl = - if noccur_between 1 cs.cs_nargs ccl then + if noccur_between !evdref 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type_loc loc env.ExtraEnv.env !evdref + error_cant_find_case_type ?loc env.ExtraEnv.env !evdref cj.uj_val in (* let ccl = refresh_universes ccl in *) - let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in + let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign' in let v = let ind,_ = dest_ind_family indf in Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = ccl }) - | GIf (loc,c,(na,po),b1,b2) -> + | GIf (c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in + error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 2) then - user_err_loc (loc,"", - str "If is only for inductive types with two constructors."); + user_err ?loc + (str "If is only for inductive types with two constructors."); let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in - if not !allow_anonymous_refs then - (* Make dependencies from arity signature impossible *) - List.map (set_name Anonymous) arsgn - else arsgn + (* Make dependencies from arity signature impossible *) + List.map (set_name Anonymous) arsgn in let nar = List.length arsgn in - let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in + let indt = build_dependent_inductive env.ExtraEnv.env indf in + let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) + let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in + let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in + let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in + let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *) + let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let pred,p = match po with | Some p -> - let env_p = push_rel_context psign env in - let pj = pretype_type empty_valcon env_p evdref lvar p in + let env_p = push_rel_context !evdref psign env in + let pj = pretype_type empty_valcon env_p evdref predlvar p in let ccl = nf_evar !evdref pj.utj_val in - let pred = it_mkLambda_or_LetIn ccl psign in - let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in + let pred = it_mkLambda_or_LetIn ccl psign' in + let typ = lift (- nar) (beta_applist !evdref (pred,[cj.uj_val])) in pred, typ | None -> let p = match tycon with | Some ty -> ty | None -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in new_type_evar env evdref loc in - it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in + it_mkLambda_or_LetIn (lift (nar+1) p) psign', p in let pred = nf_evar !evdref pred in let p = nf_evar !evdref p in let f cs b = let n = Context.Rel.length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) - let pi = beta_applist (pi, [build_dependent_constructor cs]) in + let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in + let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in + let cs_args = + if Flags.version_strictly_greater Flags.V8_6 + then Context.Rel.map (whd_betaiota !evdref) cs_args + else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in let csgn = - if not !allow_anonymous_refs then - List.map (set_name Anonymous) cs.cs_args - else - List.map (map_name (function Name _ as n -> n - | Anonymous -> Name Namegen.default_non_dependent_ident)) - cs.cs_args - in - let env_c = push_rel_context csgn env in + List.map (set_name Anonymous) cs_args + in + let env_c = push_rel_context !evdref csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in - it_mkLambda_or_LetIn bj.uj_val cs.cs_args in + it_mkLambda_or_LetIn bj.uj_val cs_args in let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in let v = @@ -985,19 +1052,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in - inh_conv_coerce_to_tycon loc env evdref cj tycon + inh_conv_coerce_to_tycon ?loc env evdref cj tycon - | GCases (loc,sty,po,tml,eqns) -> - Cases.compile_cases loc sty - ((fun vtyc env evdref -> pretype vtyc (make_env env) evdref lvar),evdref) - tycon env.ExtraEnv.env (* loc *) (po,tml,eqns) + | GCases (sty,po,tml,eqns) -> + Cases.compile_cases ?loc sty + ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref),evdref) + tycon env.ExtraEnv.env (* loc *) lvar (po,tml,eqns) - | GCast (loc,c,k) -> + | GCast (c,k) -> let cj = match k with | CastCoerce -> let cj = pretype empty_tycon env evdref lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env.ExtraEnv.env) evdref cj + evd_comb1 (Coercion.inh_coerce_to_base ?loc env.ExtraEnv.env) evdref cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in @@ -1009,13 +1076,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | VMcast -> let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in - if not (occur_existential cty || occur_existential tval) then + if not (occur_existential !evdref cty || occur_existential !evdref tval) then let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) - else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ + else user_err ?loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in @@ -1024,7 +1091,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> @@ -1032,12 +1099,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } - in inh_conv_coerce_to_tycon loc env evdref cj tycon + in inh_conv_coerce_to_tycon ?loc env evdref cj tycon and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let f decl (subst,update) = - let id = get_id decl in - let t = replace_vars subst (get_type decl) in + let id = NamedDecl.get_id decl in + let t = replace_vars subst (EConstr.of_constr (NamedDecl.get_type decl)) in let c, update = try let c = List.assoc id update in @@ -1046,66 +1113,75 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t (lift n t') then mkRel n, update else raise Not_found with Not_found -> try - let t' = lookup_named id env |> get_type in + let t' = env |> lookup_named id |> NamedDecl.get_type in if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> - user_err_loc (loc,"",str "Cannot interpret " ++ + user_err ?loc (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ - str " in current context: no binding for " ++ pr_id id ++ str ".") in + str " in current context: no binding for " ++ Id.print id ++ str ".") in ((id,c)::subst, update) in let subst,inst = List.fold_right f hyps ([],update) in check_instance loc subst inst; Array.map_of_list snd subst (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) -and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function - | GHole (loc, knd, naming, None) -> +and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match DAst.get c with + | GHole (knd, naming, None) -> + let loc = loc_of_glob_constr c in (match valcon with | Some v -> let s = let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma v in - match kind_of_term (whd_all env.ExtraEnv.env sigma t) with - | Sort s -> s - | Evar ev when is_Type (existential_type sigma ev) -> + match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with + | Sort s -> ESorts.kind sigma s + | Evar ev when is_Type sigma (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev - | _ -> anomaly (Pp.str "Found a type constraint which is not a type") + | _ -> anomaly (Pp.str "Found a type constraint which is not a type.") in - { utj_val = v; - utj_type = s } + (* Correction of bug #5315 : we need to define an evar for *all* holes *) + let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in + let ev,_ = destEvar !evdref evkt in + evdref := Evd.define ev (to_constr !evdref v) !evdref; + (* End of correction of bug #5315 *) + { utj_val = v; + utj_type = s } | None -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) - | c -> + | _ -> let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env.ExtraEnv.env) evdref j in + let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc env.ExtraEnv.env) evdref j in match valcon with | None -> tj | Some v -> if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj else - error_unexpected_type_loc - (loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v + error_unexpected_type + ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = - let env = make_env env in + let env = make_env env sigma in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in - let c' = match kind with + let c', c'_ty = match kind with | WithoutTypeConstraint -> - (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val + let j = pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c in + j.uj_val, j.uj_type | OfType exptyp -> - (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val + let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c in + j.uj_val, j.uj_type | IsType -> - (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val + let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c in + tj.utj_val, mkSort tj.utj_type in - process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c',c'_ty) let default_inference_flags fail = { use_typeclasses = true; @@ -1124,40 +1200,9 @@ let no_classes_no_fail_inference_flags = { let all_and_fail_flags = default_inference_flags true let all_no_fail_flags = default_inference_flags false -let empty_lvar : ltac_var_map = { - ltac_constrs = Id.Map.empty; - ltac_uconstrs = Id.Map.empty; - ltac_idents = Id.Map.empty; - ltac_genargs = Id.Map.empty; -} - -let on_judgment f j = - let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in - let (c,_,t) = destCast (f c) in - {uj_val = c; uj_type = t} - -let understand_judgment env sigma c = - let env = make_env env in - let evdref = ref sigma in - let k0 = Context.Rel.length (rel_context env) in - let j = pretype k0 true empty_tycon env evdref empty_lvar c in - let j = on_judgment (fun c -> - let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in - evdref := evd; c) j - in j, Evd.evar_universe_context !evdref - -let understand_judgment_tcc env evdref c = - let env = make_env env in - let k0 = Context.Rel.length (rel_context env) in - let j = pretype k0 true empty_tycon env evdref empty_lvar c in - on_judgment (fun c -> - let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in - evdref := evd; c) j - let ise_pretype_gen_ctx flags env sigma lvar kind c = - let evd, c = ise_pretype_gen flags env sigma lvar kind c in - let evd, f = Evarutil.nf_evars_and_universes evd in - f c, Evd.evar_universe_context evd + let evd, c, _ = ise_pretype_gen flags env sigma lvar kind c in + c, Evd.evar_universe_context evd (** Entry points of the high-level type synthesis algorithm *) @@ -1167,42 +1212,19 @@ let understand env sigma c = ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c -let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = +let understand_tcc_ty ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = ise_pretype_gen flags env sigma empty_lvar expected_type c -let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c = - let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in - evdref := sigma; - c +let understand_tcc ?flags env sigma ?expected_type c = + let sigma, c, _ = understand_tcc_ty ?flags env sigma ?expected_type c in + sigma, c let understand_ltac flags env sigma lvar kind c = - ise_pretype_gen flags env sigma lvar kind c - -let constr_flags = { - use_typeclasses = true; - solve_unification_constraints = true; - use_hook = None; - fail_evar = true; - expand_evars = true } - -(* Fully evaluate an untyped constr *) -let type_uconstr ?(flags = constr_flags) - ?(expected_type = WithoutTypeConstraint) ist c = - { delayed = begin fun env sigma -> - let { closure; term } = c in - let vars = { - ltac_constrs = closure.typed; - ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents; - ltac_genargs = Id.Map.empty; - } in - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = understand_ltac flags env sigma vars expected_type term in - Sigma.Unsafe.of_pair (c, sigma) - end } + let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in + (sigma, c) let pretype k0 resolve_tc typcon env evdref lvar t = - pretype k0 resolve_tc typcon (make_env env) evdref lvar t + pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t let pretype_type k0 resolve_tc valcon env evdref lvar t = - pretype_type k0 resolve_tc valcon (make_env env) evdref lvar t + pretype_type k0 resolve_tc valcon (make_env env !evdref) evdref lvar t |