(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* 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 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
(* This file contains the syntax-directed part of the type inference algorithm introduced by Murthy in Coq V5.10, 1995; the type inference algorithm was initially developed in a file named trad.ml which formerly contained a simple concrete-to-abstract syntax translation function introduced in CoC V4.10 for implementing the
"exact" tactic, 1989 *) (* Support for typing term in Ltac environment by David Delahaye, 2000 *) (* Type inference algorithm made a functor of the coercion and
pattern-matching compilation by Matthieu Sozeau, March 2006 *) (* Fixpoint guard index computation by Pierre Letouzey, July 2007 *)
open Pp open CErrors open Util open Names open Evd open Constr open Context open Termops open Environ open EConstr open Vars open Reductionops open Type_errors open Typing open Evarutil open Evardefine open Pretype_errors open Glob_term open Glob_ops open GlobEnv open Evarconv
module NamedDecl = Context.Named.Declaration
type typing_constraint = IsType | OfType of types | WithoutTypeConstraint
let (!!) env = GlobEnv.env env
let bidi_hints =
Summary.ref (GlobRef.Map.empty : int GlobRef.Map.t) ~name:"bidirectionalityhints"
let add_bidirectionality_hint gr n =
bidi_hints := GlobRef.Map.add gr n !bidi_hints
let get_bidirectionality_hint gr =
GlobRef.Map.find_opt gr !bidi_hints
let clear_bidirectionality_hint gr =
bidi_hints := GlobRef.Map.remove gr !bidi_hints
(************************************************************************) (* This concerns Cases *) open Inductive open Inductiveops
(* An auxiliary function for searching for fixpoint guard indices *)
(* Tells the possible indices liable to guard a fixpoint *) type possible_fix_indices = int listlist
(* Tells if possibly a cofixpoint or a fixpoint over the given list of possible indices *) type possible_guard = {
possibly_cofix : bool;
possible_fix_indices : possible_fix_indices;
} (* Note: if no fix indices are given, it has to be a cofix *)
exception Found of int array option
let nf_fix sigma (nas, cs, ts) = let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
(Array.map EConstr.Unsafe.to_binder_annot nas, Array.map inj cs, Array.map inj ts)
let search_guard ?loc ?evars env {possibly_cofix; possible_fix_indices} fixdefs = let is_singleton = function [_] -> true | _ -> falsein let one_fix_possibility = List.for_all is_singleton possible_fix_indices in if one_fix_possibility && not possibly_cofix then let indexes = Array.of_list (List.mapList.hd possible_fix_indices) in let fix = ((indexes, 0), fixdefs) in trylet () = check_fix ?evars env fix in Some indexes with reraise -> let (e, info) = Exninfo.capture reraise in let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
Exninfo.iraise (e, info) else let zero_fix_possibility = List.for_all List.is_empty possible_fix_indices in if zero_fix_possibility && possibly_cofix then (* Maybe can we skip this check since it will be done in the kernel again *) let cofix = (0, fixdefs) in trylet () = check_cofix ?evars env cofix in None with reraise -> let (e, info) = Exninfo.capture reraise in let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
Exninfo.iraise (e, info) else (* we now search recursively among all combinations *) let combinations = List.combinations possible_fix_indices in let flags = { (typing_flags env) with Declarations.check_guarded = true } in let env = Environ.set_typing_flags flags env in try let () = List.iter
(fun l -> let indexes = Array.of_list l in let fix = ((indexes, 0),fixdefs) in (* spiwack: We search for a unspecified structural argument under the assumption that we need to check the guardedness condition (otherwise the first inductive argument will be chosen). A more robust solution may be to raise an error when totality is assumed but the strutural argument is
not specified. *) try let () = check_fix ?evars env fix inraise (Found (Some indexes)) with TypeError _ -> ())
combinations in let () = if possibly_cofix then (* Maybe can we skip this check since it will be done in the kernel again *) trylet () = check_cofix env (0, fixdefs) inraise (Found None) with TypeError _ -> () in let errmsg = "Cannot guess decreasing argument of fix."in
user_err ?loc (Pp.str errmsg) with Found indexes -> indexes
let esearch_guard ?loc env sigma indexes fix = (* not sure if we still need to nf_fix when calling search_guard with ~evars (here and other callers through the code) OTOH search_guard needs to go through the whole term to see possible recursive calls
so we may as well upfront normalize *) let fix = nf_fix sigma fix in let evars = Evd.evar_handler sigma in try search_guard ?loc ~evars env indexes fix with TypeError (env,err) ->
Loc.raise ?loc (PretypeError (env,sigma,TypingError (of_type_error err)))
let universe_level_name evd ({CAst.v=id} as lid) = try evd, Evd.universe_of_name evd id with Not_found -> ifnot (is_strict_universe_declarations ()) then
new_univ_level_variable ?loc:lid.CAst.loc ~name:id univ_rigid evd else user_err ?loc:lid.CAst.loc
(Pp.(str "Undeclared universe: " ++ Id.print id ++ str "."))
let level_name sigma = function
| GSProp | GProp -> None
| GSet -> Some (sigma, Univ.Level.set)
| GUniv u -> Some (sigma, u)
| GRawUniv u -> let sigma = try Evd.add_forgotten_univ sigma u with UGraph.AlreadyDeclared -> sigma in
Some (sigma, u)
| GLocalUniv l -> let sigma, u = universe_level_name sigma l in
Some (sigma, u)
let glob_level ?loc evd : glob_level -> _ = function
| UAnonymous {rigid} ->
assert (rigid <> UnivFlexible true);
new_univ_level_variable ?loc rigid evd
| UNamed s -> match level_name evd s with
| None ->
user_err ?loc
(str "Universe instances cannot contain non-Set small levels," ++ spc() ++
str "polymorphic universe instances must be greater or equal to Set.");
| Some r -> r
let glob_qvar ?loc evd : glob_qvar -> _ = function
| GQVar q -> evd, q
| GLocalQVar {v=Anonymous} -> let evd, q = new_quality_variable ?loc evd in
evd, q
| GRawQVar q -> let evd = Evd.merge_sort_variables ~sideff:true evd (Sorts.QVar.Set.singleton q) in
evd, q
| GLocalQVar {v=Name id; loc} -> try evd, (Evd.quality_of_name evd id) with Not_found -> ifnot (is_strict_universe_declarations()) then let evd, q = new_quality_variable ?loc evd in
evd, q else user_err ?loc Pp.(str "Undeclared quality: " ++ Id.print id ++ str".")
let glob_quality ?loc evd = letopen Sorts.Quality in function
| GQConstant q -> evd, QConstant q
| GQualVar (GQVar _ | GLocalQVar _ | GRawQVar _ as q) -> let evd, q = glob_qvar ?loc evd q in
evd, QVar q
let glob_opt_qvar ?loc ~flags sigma = function
| None -> if flags.unconstrained_sorts then let sigma, q = new_quality_variable ?loc sigma in
sigma, Some q else sigma, None
| Some q -> let sigma, q = glob_qvar ?loc sigma q in
sigma, Some q
let sort ?loc ~flags sigma (q, l) = match l with
| UNamed [] -> assert false
| UNamed [GSProp, 0] -> assert (Option.is_empty q); sigma, ESorts.sprop
| UNamed [GProp, 0] -> assert (Option.is_empty q); sigma, ESorts.prop
| UNamed [GSet, 0] when Option.is_empty q -> sigma, ESorts.set
| UNamed ((u, n) :: us) -> letopen Pp in let sigma, q = glob_opt_qvar ?loc ~flags sigma q in let get_level sigma u n = match level_name sigma u with
| None ->
user_err ?loc
(str "Non-Set small universes cannot be used in algebraic expressions.")
| Some (sigma, u) -> let u = Univ.Universe.make u in let u = match n with
| 0 -> u
| 1 -> Univ.Universe.super u
| n ->
user_err ?loc
(str "Cannot interpret universe increment +" ++ int n ++ str ".") in
(sigma, u) in let fold (sigma, u) (l, n) = let sigma, u' = get_level sigma l n in
(sigma, Univ.Universe.sup u u') in let (sigma, u) = get_level sigma u n in let (sigma, u) = List.fold_left fold (sigma, u) us in let s = match q with
| None -> Sorts.sort_of_univ u
| Some q -> Sorts.qsort q u in
sigma, ESorts.make s
| UAnonymous {rigid} -> let sigma, q = glob_opt_qvar ?loc ~flags sigma q in let sigma, l = new_univ_level_variable ?loc rigid sigma in let u = Univ.Universe.make l in let s = match q with
| None -> Sorts.sort_of_univ u
| Some q -> Sorts.qsort q u in
sigma, ESorts.make s
(* Compute the set of still-undefined initial evars up to restriction (e.g. clearing) and the set of yet-unsolved evars freshly created in the extension [sigma'] of [sigma] (excluding the restrictions of the undefined evars of [sigma] to be freshly created evars of [sigma']). Otherwise said, we partition the undefined evars of [sigma'] into those already in [sigma] or deriving from an evar in
[sigma] by restriction, and the evars properly created in [sigma'] *)
type frozen_and_pending =
Frz : 'a Evar.Map.t (* Undefined from [sigma']. This is used only as a set, guaranteed by the existential type 'a, but we do not use
Evar.Set to avoid reallocating. *)
* Evar.Set.t Lazy.t option (* Undefined evars in [sigma'] which are neither in [sigma] or aliases thereof.
[None] means empty.*)
-> frozen_and_pending
let frozen_and_pending_holes (sigma, sigma') term = let undefined0 = Option.cata Evd.undefined_map Evar.Map.empty sigma in let included = Option.cata (Evd.evars_of_term sigma') Evar.Set.empty term in let pending = if undefined0 == Evd.undefined_map sigma' && Evar.Set.is_empty included then None else
Some (lazy begin let pending, aliases =
Evar.Map.symmetric_diff_fold (fun ev v v' (pending,aliases as acc) -> match v, v'with
| None, None -> assert false
| Some _, None -> (* ev got defined in sigma', but is it an alias? *) beginmatch advance sigma' ev with
| None -> acc
| Some ev -> pending, Evar.Set.add ev aliases end
| None, Some _ -> (* ev is new in sigma' *)
Evar.Set.add ev pending, aliases
| Some _, Some _ -> (* ev is still undefined in sigma' *) acc)
undefined0
(Evd.undefined_map sigma')
(Evar.Set.empty, Evar.Set.empty) in
Evar.Set.union included (Evar.Set.diff pending aliases); end) in
Frz (Evd.undefined_map sigma', pending)
let filter_frozen frozen = match frozen with
| Frz (undf, None) -> fun evk -> Evar.Map.mem evk undf
| Frz (undf, Some (lazy pending)) -> fun evk -> not (Evar.Set.mem evk pending) && Evar.Map.mem evk undf
let typeclasses_filter ~program_mode frozen = if program_mode then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen frozen evk)) else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen frozen evk))
let apply_typeclasses ~program_mode ~fail_evar env sigma frozen = let sigma = Typeclasses.resolve_typeclasses
~filter:(typeclasses_filter ~program_mode frozen)
~fail:fail_evar env sigma in let sigma = if program_mode then(* Try optionally solving the obligations *)
Typeclasses.resolve_typeclasses
~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen frozen evk)) ~fail:false env sigma else sigma in
sigma
let apply_inference_hook (hook : inference_hook) env sigma frozen = match frozen with
| Frz (_, None) -> sigma
| Frz (_, Some (lazy pending)) ->
Evar.Set.fold (fun evk sigma -> if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then match hook env sigma evk with
| Some (sigma, c) ->
Evd.define evk c sigma
| None -> sigma else
sigma) pending sigma
let allow_all_but_patvars sigma = let p evk = try let EvarInfo evi = Evd.find sigma evk in match snd (Evd.evar_source evi) with Evar_kinds.MatchingVar _ -> false | _ -> true with Not_found -> true in
Evarsolve.AllowedEvars.from_pred p
let apply_heuristics ~patvars_abstract env sigma = (* Resolve eagerly, potentially making wrong choices *) let flags = default_flags_of (Conv_oracle.get_transp_state (Environ.oracle env)) in let flags = if patvars_abstract then { flags with allowed_evars = allow_all_but_patvars sigma } else flags in try solve_unif_constraints_with_heuristics ~flags env sigma with e when CErrors.noncritical e -> sigma
let check_typeclasses_instances_are_solved ~program_mode env sigma frozen = let tcs = Typeclasses.get_filtered_typeclass_evars
(typeclasses_filter ~program_mode frozen)
sigma in ifnot (Evar.Set.is_empty tcs) thenbegin
Typeclasses.error_unresolvable env sigma tcs end
let check_extra_evars_are_solved env current_sigma frozen = match frozen with
| Frz (_, None) -> ()
| Frz (_, Some (lazy pending)) ->
Evar.Set.iter
(fun evk -> ifnot (Evd.is_defined current_sigma evk) then let (loc,k) = evar_source (Evd.find_undefined current_sigma evk) in match k with
| Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
| _ ->
error_unsolvable_implicit ?loc env current_sigma evk None) pending
(* [check_evars] fails if some unresolved evar remains *)
let check_evars env ?initial sigma c = let rec proc_rec c = match EConstr.kind sigma c with
| Evar (evk, _) ->
(match initial with
| Some initial when Evd.mem initial evk -> ()
| _ -> let EvarInfo evi = Evd.find sigma evk in let (loc,k) = evar_source evi in beginmatch 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_problems_are_solved env sigma = function
| Frz (_, None) -> ()
| Frz (_, Some (lazy pending)) -> check_problems_are_solved ~evars:pending env sigma
let solve_remaining_evars_from ?hook (flags : inference_flags) env ?initial sigma term = let program_mode = flags.program_mode in let sigma = match flags.use_typeclasses with
| UseTC -> let frozen = frozen_and_pending_holes (initial, sigma) None in
apply_typeclasses ~program_mode ~fail_evar:false env sigma frozen
| NoUseTC | UseTCForConv -> sigma in let sigma = match hook with
| None -> sigma
| Some hook -> let frozen = frozen_and_pending_holes (initial, sigma) None in
apply_inference_hook hook env sigma frozen in let sigma = if flags.solve_unification_constraints then apply_heuristics ~patvars_abstract:flags.patvars_abstract env sigma else sigma in let () = if flags.fail_evar then let frozen = frozen_and_pending_holes (initial, sigma) None in let frozen_for_pb = frozen_and_pending_holes (initial, sigma) term in
check_evars_are_solved_from ~program_mode env sigma frozen frozen_for_pb in
sigma
let check_evars_are_solved ~program_mode env ?initial current_sigma = let frozen = frozen_and_pending_holes (initial, current_sigma) None in
check_evars_are_solved_from ~program_mode env current_sigma frozen frozen
let process_inference_flags flags env initial (sigma,c,cty) = let sigma = solve_remaining_evars_from flags env ~initial sigma (Some cty) in let c = if flags.expand_evars then nf_evar sigma c else c in
sigma,c,cty
let adjust_evar_source sigma na c = match na, kind sigma c with
| Name id, Evar (evk,args) -> let evi = Evd.find_undefined sigma evk in beginmatch Evd.evar_source evi with
| loc, Evar_kinds.QuestionMark ({ Evar_kinds.qm_name=Anonymous } as qm) -> let src = (loc,Evar_kinds.QuestionMark { qm with Evar_kinds.qm_name=na }) in (* Evd.update_source doesn't work for some reason, cf test bug_18260_1.v *) let (sigma, evk') = Evd.restrict evk (evar_filter evi) ~src sigma in
sigma, mkEvar (evk',args)
| _ -> sigma, c end
| _, _ -> sigma, c
(* coerce to tycon if any *) let inh_conv_coerce_to_tycon ?loc ~flags:{ program_mode; resolve_tc; use_coercions; patvars_abstract } env sigma j = function
| None -> sigma, j, Some Coercion.empty_coercion_trace
| Some t ->
Coercion.inh_conv_coerce_to ?loc ~program_mode ~resolve_tc ~use_coercions ~patvars_abstract !!env sigma j t
let check_instance subst = function
| [] -> ()
| (CAst.{loc;v=id},_) :: _ -> ifList.mem_assoc id subst then
user_err ?loc (Id.print id ++ str "appears more than once.") else
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 *)
let orelse_name name name' = match name with
| Anonymous -> name'
| _ -> name
let pretype_id pretype loc env sigma id = (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context !!env) in
sigma, { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> try
GlobEnv.interp_ltac_variable ?loc (fun env -> pretype env sigma) env sigma id with Not_found -> (* Check if [id] is a section or goal variable *) try
sigma, { 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 !!env sigma id
(*************************************************************************) (* Main pretyping function *)
let instance ?loc evd (ql,ul) = let evd, ql' = List.fold_left
(fun (evd, quals) l -> let evd, l = glob_quality ?loc evd l in
(evd, l :: quals)) (evd, [])
ql in let evd, ul' = List.fold_left
(fun (evd, univs) l -> let evd, l = glob_level ?loc evd l in
(evd, l :: univs)) (evd, [])
ul in
evd, Some (UVars.Instance.of_array (Array.rev_of_list ql', Array.rev_of_list ul'))
let pretype_global ?loc rigid env evd gr us = let evd, instance = match us with
| None -> evd, None
| Some l -> instance ?loc evd l in
Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr
let pretype_ref ?loc sigma env ref us = matchrefwith
| GlobRef.VarRef id -> (* Section variable *)
(try let ty = NamedDecl.get_type (lookup_named id !!env) in
(match us with
| None | Some ([],[]) -> ()
| Some (qs,us) -> letopen UnivGen in
Loc.raise ?loc (UniverseLengthMismatch {
gref = ref;
actual = List.length qs, List.length us;
expect = 0, 0;
}));
sigma, make_judge (mkVar id) ty 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 !!env sigma id)
| ref -> let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in let sigma, ty = type_of !!env sigma c in
sigma, make_judge c ty
let judge_of_sort ?loc evd s = let judge =
{ uj_val = mkSort s; uj_type = mkSort (ESorts.super evd s) } in
evd, judge
let pretype_sort ?loc ~flags sigma s = let sigma, s = sort ?loc ~flags sigma s in
judge_of_sort ?loc sigma s
let new_typed_evar env sigma ?naming ~src tycon = match tycon with
| Some ty -> let sigma, c = new_evar env sigma ~src ?naming ty in
sigma, c, ty
| None -> let sigma, ty = new_type_evar env sigma ~src in let sigma, c = new_evar env sigma ~src ?naming ty in let evk = fst (destEvar sigma c) in let ido = Evd.evar_ident evk sigma in let src = (fst src,Evar_kinds.EvarType (ido,evk)) in let sigma = update_source sigma (fst (destEvar sigma ty)) src in
sigma, c, ty
let mark_obligation_evar sigma k evc = match k with
| Evar_kinds.QuestionMark _
| Evar_kinds.ImplicitArg (_, _, false) ->
Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
| _ -> sigma
let eval_type_pretyper self ~flags tycon env sigma t =
self.pretype_type self t ~flags tycon env sigma
let pretype_instance self ~flags env sigma loc hyps evk update = let f decl (subst,update,sigma) = let id = NamedDecl.get_id decl in let b = Option.map (replace_vars sigma subst) (NamedDecl.get_value decl) in let t = replace_vars sigma subst (NamedDecl.get_type decl) in let uflags = default_flags_of TransparentState.full in let uflags = if flags.patvars_abstract then { uflags with allowed_evars = allow_all_but_patvars sigma } else uflags in let check_body sigma id c = match b, c with
| Some b, Some c -> begin try (Evarconv.unify_delay ~flags:uflags !!env sigma b c) with UnableToUnify (sigma, _) ->
user_err ?loc (str "Cannot interpret " ++
pr_existential_key !!env sigma evk ++
strbrk " in current context: binding for " ++ Id.print id ++
strbrk " is not convertible to its expected definition (cannot unify " ++
quote (Termops.Internal.print_constr_env !!env sigma b) ++
strbrk " and " ++
quote (Termops.Internal.print_constr_env !!env sigma c) ++
str ").") end
| Some b, None ->
user_err ?loc (str "Cannot interpret " ++
pr_existential_key !!env sigma evk ++
strbrk " in current context: " ++ Id.print id ++
strbrk " should be bound to a local definition.")
| None, _ -> sigma in let check_type sigma id t' = try (Evarconv.unify_delay ~flags:uflags !!env sigma t t') with UnableToUnify (sigma, _) ->
user_err ?loc (str "Cannot interpret " ++
pr_existential_key !!env sigma evk ++
strbrk " in current context: binding for " ++ Id.print id ++
strbrk " is not well-typed.") in let sigma, c, update = try let c = snd (List.find (fun (CAst.{v=id'},c) -> Id.equal id id') update) in let sigma, c = eval_pretyper self ~flags (mk_tycon t) env sigma c in let sigma = check_body sigma id (Some c.uj_val) in
sigma, c.uj_val, List.remove_first (fun (CAst.{v=id'},_) -> Id.equal id id') update with Not_found -> try let (n,b',t') = lookup_rel_id id (rel_context !!env) in let sigma = check_type sigma id (lift n t') in let sigma = check_body sigma id (Option.map (lift n) b') in
sigma, mkRel n, update with Not_found -> try let decl = lookup_named id !!env in let sigma = check_type sigma id (NamedDecl.get_type decl) in let sigma = check_body sigma id (NamedDecl.get_value decl) in
sigma, mkVar id, update with Not_found ->
user_err ?loc (str "Cannot interpret " ++
pr_existential_key !!env sigma evk ++
str " in current context: no binding for " ++ Id.print id ++ str ".") in
((id,c)::subst, update, sigma) in let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in
check_instance subst inst;
sigma, List.map snd subst
module Default = struct
let discard_trace (sigma,t,otrace) = sigma, t
let pretype_ref self (ref, u) = fun ?loc ~flags tycon env sigma -> let sigma, t_ref = pretype_ref ?loc sigma env ref u in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~flags env sigma t_ref tycon
let pretype_var self id = fun ?loc ~flags tycon env sigma -> let pretype tycon env sigma t = eval_pretyper self ~flags 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
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~flags env sigma t_id tycon
let pretype_evar self (CAst.{v=id;loc=locid}, inst) ?loc ~flags tycon env sigma = (* 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 id = interp_ltac_id env id in let sigma, evk = match Evd.evar_key id sigma with
| evk -> sigma, evk
| exception Not_found -> if flags.undeclared_evars_patvars then let k = Evar_kinds.(MatchingVar (FirstOrderPatVar id)) in let sigma, uj_val, _ = new_typed_evar env sigma ~naming:(IntroIdentifier id) ~src:(loc,k) tycon in
sigma, fst (destEvar sigma uj_val) else
error_evar_not_found ?loc:locid !!env sigma id in let EvarInfo evi = Evd.find sigma evk in let hyps = evar_filtered_context evi in let sigma, args = pretype_instance self ~flags env sigma loc hyps evk inst in let c = mkLEvar sigma (evk, args) in let j = Retyping.get_judgment_of !!env sigma c in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~flags env sigma j tycon
let pretype_patvar self kind ?loc ~flags tycon env sigma = let k = Evar_kinds.MatchingVar kind in let sigma, uj_val, uj_type = new_typed_evar env sigma ~src:(loc,k) tycon in
sigma, { uj_val; uj_type }
let pretype_hole self k ?loc ~flags tycon env sigma = letopen Namegen in let naming = naming_of_glob_kind k in let naming = match naming with
| IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id)
| IntroAnonymous -> IntroAnonymous
| IntroFresh id -> IntroFresh (interp_ltac_id env id) in let k = kind_of_glob_kind k in let sigma, uj_val, uj_type = new_typed_evar env sigma ~src:(loc,k) ~naming tycon in let sigma = if flags.program_mode then mark_obligation_evar sigma k uj_val else sigma in
sigma, { uj_val; uj_type }
let pretype_genarg self arg ?loc ~flags tycon env sigma = let j, sigma = GlobEnv.interp_glob_genarg ?loc ~poly:flags.poly env sigma tycon arg in
sigma, j
let pretype_rec self (fixkind, names, bl, lar, vdef) = fun ?loc ~flags tycon env sigma -> letopen Context.Rel.Declaration in let pretype tycon env sigma c = eval_pretyper self ~flags tycon env sigma c in let pretype_type tycon env sigma c = eval_type_pretyper self ~flags tycon env sigma c in let hypnaming = VarSet.variables (Global.env ()) in let rec type_bl env sigma ctxt = function
| [] -> sigma, ctxt
| (na,_,bk,None,ty)::bl -> let sigma, ty' = pretype_type empty_valcon env sigma ty in let rty' = ESorts.relevance_of_sort ty'.utj_type in let dcl = LocalAssum (make_annot na rty', ty'.utj_val) in let dcl', env = push_rel ~hypnaming sigma dcl env in
type_bl env sigma (Context.Rel.add dcl' ctxt) bl
| (na,_,bk,Some bd,ty)::bl -> let sigma, ty' = pretype_type empty_valcon env sigma ty in let rty' = ESorts.relevance_of_sort ty'.utj_type in let sigma, bd' = pretype (mk_tycon ty'.utj_val) env sigma bd in let dcl = LocalDef (make_annot na rty', bd'.uj_val, ty'.utj_val) in let dcl', env = push_rel ~hypnaming sigma dcl env in
type_bl env sigma (Context.Rel.add dcl' ctxt) bl in let sigma, ctxtv = Array.fold_left_map (fun sigma -> type_bl env sigma Context.Rel.empty) sigma bl in let sigma, larj =
Array.fold_left2_map
(fun sigma e ar ->
pretype_type empty_valcon (snd (push_rel_context ~hypnaming sigma e env)) sigma ar)
sigma 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 let nbfix = Array.length lar in let names = Array.map (fun id -> Name id) names in let sigma = match tycon with
| Some t -> let fixi = match fixkind with
| GFix (vn,i) -> i
| GCoFix i -> i in beginmatch Evarconv.unify_delay !!env sigma ftys.(fixi) t with
| exception Evarconv.UnableToUnify _ -> sigma
| sigma -> sigma end
| None -> sigma in let names = Array.map2 (fun na t ->
make_annot na (Retyping.relevance_of_type !!(env) sigma t))
names ftys in (* Note: bodies are not used by push_rec_types, so [||] is safe *) let names,newenv = push_rec_types ~hypnaming sigma (names,ftys) env in let sigma, vdefj =
Array.fold_left2_map_i
(fun i sigma ctxt def -> (* we lift nbfix times the type in tycon, because of
* the nbfix variables pushed to newenv *) let (ctxt,ty) =
decompose_prod_n_decls sigma (Context.Rel.length ctxt)
(lift nbfix ftys.(i)) in let ctxt,nenv = push_rel_context ~hypnaming sigma ctxt newenv in let sigma, j = pretype (mk_tycon ty) nenv sigma def in
sigma, { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
sigma ctxtv vdef in let sigma = Typing.check_type_fixpoint ?loc !!env sigma names ftys vdefj in let nf c = nf_evar sigma 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. *) (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, but doing it properly involves delta-reduction, and it finally doesn't seem worth the effort (except for huge mutual
fixpoints ?) *) let possible_fix_indices =
Array.to_list (Array.mapi
(fun i annot -> match annot with
| Some n -> [n]
| None -> List.interval 0 (Context.Rel.nhyps ctxtv.(i) - 1))
vn) in let fixdecls = (names,ftys,fdefs) in let indexes = esearch_fix_guard ?loc !!env sigma possible_fix_indices fixdecls in
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
| GCoFix i -> let fixdecls = (names,ftys,fdefs) in let cofix = (i, fixdecls) in let () = esearch_cofix_guard ?loc !!env sigma fixdecls in
make_judge (mkCoFix cofix) ftys.(i) in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~flags env sigma fixj tycon
let pretype_sort self s = fun ?loc ~flags tycon env sigma -> let sigma, j = pretype_sort ?loc ~flags sigma s in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~flags env sigma j tycon
let enforce_template_csts sigma (qbound,ubound) csts = let max_quality_opt a b = match a with
| None -> None
| Some a -> letopen Sorts.Quality in match a, b with
| QConstant QSProp, _ | _, QConstant QSProp -> assert false
| QConstant QProp, q | q, QConstant QProp -> Some q
| (QConstant QType as q), _ | _, (QConstant QType as q) -> Some q
| QVar a', QVar b' -> if Sorts.QVar.equal a' b'then Some a else None in let sigma = ref sigma in let gen_max_quality qs = let qs = List.map (UState.nf_quality (Evd.ustate !sigma)) qs in matchList.fold_left max_quality_opt (Some Sorts.Quality.qprop) qs with
| Some q -> q
| None -> match qs with
| [] -> assert false
| q :: rest -> (* all qvars or qprop with at least 2 different qvars, unify the qvars
(alternatively: return qtype?) *) let mk q = ESorts.make @@ Sorts.make q Univ.Universe.type0 in let unify sigma q' = if Sorts.Quality.(equal qprop q') then sigma else Evd.set_eq_sort sigma (mk q) (mk q') in let sigma' = List.fold_left unify !sigma rest in
sigma := sigma';
q in let qbound = Int.Map.map gen_max_quality qbound in let sigma = !sigma in let bound = qbound, ubound in let csts = Inductive.instantiate_template_constraints bound csts in let sigma = Evd.add_constraints sigma csts in
sigma, bound
let template_sort boundus (s:Sorts.t) = let s = Inductive.Template.template_subst_sort boundus s in
ESorts.make s
let bind_template bind_sort s (qsubst,usubst) = let qbind, ubind = Inductive.Template.bind_kind bind_sort in let qsubst = match qbind with
| None -> qsubst
| Some qbind -> let sq = Sorts.quality s in
Int.Map.update qbind (function
| None -> Some [sq]
| Some q0 -> Some (sq::q0))
qsubst in let usubst = match ubind with
| None -> usubst
| Some ubind -> let u = match s with
| SProp | Prop | Set -> Univ.Universe.type0
| Type u | QSort (_,u) -> u in
Int.Map.update ubind (function
| None -> Some u
| Some _ ->
CErrors.anomaly Pp.(str "Retyping.bind_template found non linear template level."))
usubst in
qsubst, usubst
let rec finish_template sigma boundus = letopen TemplateArity in function
| CtorType (csts, typ) -> let sigma, boundus = enforce_template_csts sigma boundus csts in
sigma, typ
| IndType (csts, ctx, s) -> let sigma, boundus = enforce_template_csts sigma boundus csts in let s = template_sort boundus s in
sigma, mkArity (ctx, s)
| DefParam (na, v, t, codom) -> let sigma, codom = finish_template sigma boundus codom in
sigma, mkLetIn (na,v,t,codom)
| NonTemplateArg (na,dom,codom) -> let sigma, codom = finish_template sigma boundus codom in
sigma, mkProd (na,dom,codom)
| TemplateArg (na,ctx,binder,codom) -> let boundus = bind_template binder.bind_sort binder.default boundus in let sigma, codom = finish_template sigma boundus codom in let s = ESorts.make @@ binder.default in
sigma, mkProd (na,mkArity (ctx,s),codom)
let freshen_template sigma = letopen Sorts in function
| SProp | Prop | Set -> assert false
| Type _ -> let sigma, u = Evd.new_univ_level_variable UState.univ_flexible_alg sigma in
sigma, ESorts.make (Sorts.sort_of_univ (Univ.Universe.make u))
| QSort (q,u) -> let sigma, q = match Sorts.QVar.var_index q with
| None -> sigma, q
| Some _ -> let sigma, q = Evd.new_quality_variable sigma in let sigma = Evd.set_above_prop sigma (QVar q) in
sigma, q in let sigma, u = matchOption.bind (Univ.Universe.level u) Univ.Level.var_index with
| None -> sigma, u
| Some _ -> let sigma, u = Evd.new_univ_level_variable UState.univ_flexible_alg sigma in
sigma, Univ.Universe.make u in
sigma, ESorts.make @@ Sorts.qsort q u
let rec apply_template pretype_arg arg_state env sigma body subst boundus todoargs typ = letopen TemplateArity in match todoargs, typ with
| [], _
| _, (CtorType _ | IndType _) -> let sigma, typ = finish_template sigma boundus typ in
sigma, body, subst, typ, arg_state, todoargs
| _, DefParam (_, v, _, codom) -> (* eager subst may be inefficient but template inductives with letin params are hopefully rare enough that it doesn't
matter *) let v = Vars.esubst Vars.lift_substituend subst v in let subst = Esubst.subs_cons (Vars.make_substituend v) subst in
apply_template pretype_arg arg_state env sigma body subst boundus todoargs codom
| arg :: todoargs, NonTemplateArg (na, dom, codom) -> let dom = Vars.esubst Vars.lift_substituend subst dom in let sigma, arg_state, body, arg = pretype_arg env sigma arg_state body arg na.binder_name dom in let subst = Esubst.subs_cons (Vars.make_substituend arg) subst in
apply_template pretype_arg arg_state env sigma body subst boundus todoargs codom
| arg :: todoargs, TemplateArg (na, ctx, binder, codom) -> let sigma, s = freshen_template sigma binder.bind_sort in let dom = Vars.esubst Vars.lift_substituend subst (mkArity (ctx, s)) in let sigma, arg_state, body, arg = pretype_arg env sigma arg_state body arg na.binder_name dom in let s = (* get an algebraic instead of the generated variable *) try
snd @@ Reductionops.dest_arity !!env sigma @@ Retyping.get_type_of !!env sigma arg with Reduction.NotArity -> (* delayed constraints prevent getting the sort from retyping *)
s in let boundus = bind_template binder.bind_sort (ESorts.kind sigma s) boundus in let subst = Esubst.subs_cons (Vars.make_substituend arg) subst in
apply_template pretype_arg arg_state env sigma body subst boundus todoargs codom
let pretype_app self (f, args) = fun ?loc ~flags tycon env sigma -> let pretype tycon env sigma c = eval_pretyper self ~flags tycon env sigma c in let sigma, fj = pretype empty_tycon env sigma f in let floc = loc_of_glob_constr f in let length = List.length args in let nargs_before_bidi = ifOption.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 @@ get_bidirectionality_hint gr with DestKO ->
length in let candargs = (* Bidirectional typechecking hint: parameters of a constructor are completely determined
by a typing constraint *) (* This bidirectionality machinery is the one of `Program` for constructors and is orthogonal to bidirectionality hints. However, we could probably factorize both by providing default bidirectionality hints
for constructors corresponding to their number of parameters. *) if flags.program_mode && length > 0 && isConstruct sigma fj.uj_val then match tycon with
| None -> []
| Some ty -> let ((ind, i), u) = destConstruct sigma fj.uj_val in let npars = inductive_nparams !!env ind in if Int.equal npars 0 then [] else try let IndType (indf, args) = find_rectype !!env sigma ty in let ((ind',u'),pars) = dest_ind_family indf in if QInd.equal !!env ind ind' then pars else(* Let the usual code throw an error *) [] with Not_found -> [] else [] in let pretype_arg ?(trace=Coercion.empty_coercion_trace) env sigma (n, val_before_bidi, bidiargs, candargs) body arg na tycon = (* trace is the coercion trace from coercing the body to funclass *) let bidi = n >= nargs_before_bidi in let sigma, c, bidiargs = 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) tycon in
sigma, c_hole, (c_hole, tycon, arg, trace) :: bidiargs else let sigma, j = pretype (Some tycon) env sigma arg in
sigma, j_val j, bidiargs in let sigma, candargs, c = match candargs with
| [] -> sigma, [], c
| arg :: args -> beginmatch Evarconv.unify_delay !!env sigma c arg with
| exception Evarconv.UnableToUnify (sigma,e) -> raise (PretypeError (!!env,sigma,CannotUnify (c, arg, Some e)))
| sigma ->
sigma, args, nf_evar sigma c end in let sigma, c = adjust_evar_source sigma na c in let body = Coercion.push_arg body c in let val_before_bidi = if bidi then val_before_bidi else body in
sigma, (n+1,val_before_bidi,bidiargs,candargs), body, c in let rec apply_rec env sigma arg_state body (subs, typ) = function
| [] -> let typ = Vars.esubst Vars.lift_substituend subs typ in let body = Coercion.force_app_body body in let resj = { uj_val = body; uj_type = typ } in let _,val_before_bidi, bidiargs,_ = arg_state in
sigma, resj, val_before_bidi, List.rev bidiargs
| c::rest -> let argloc = loc_of_glob_constr c in let sigma, body, na, c1, subs, c2, trace = match EConstr.kind sigma typ with
| Prod (na, c1, c2) -> (* Fast path *) let c1 = Vars.esubst Vars.lift_substituend subs c1 in
sigma, body, na, c1, subs, c2, Coercion.empty_coercion_trace
| _ -> let typ = Vars.esubst Vars.lift_substituend subs typ in let sigma, body, typ, trace = Coercion.inh_app_fun ~program_mode:flags.program_mode ~resolve_tc:flags.resolve_tc ~use_coercions:flags.use_coercions !!env sigma body typ in let resty = whd_all !!env sigma typ in let na, c1, c2 = match EConstr.kind sigma resty with
| Prod (na, c1, c2) -> (na, c1, c2)
| _ -> let sigma, hj = pretype empty_tycon env sigma c in let resj = { uj_val = Coercion.force_app_body body; uj_type = typ } in
error_cant_apply_not_functional
?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|] in
sigma, body, na, c1, Esubst.subs_id 0, c2, trace in let sigma, arg_state, body, arg =
pretype_arg env sigma arg_state ~trace body c na.binder_name c1 in let subs = Esubst.subs_cons (Vars.make_substituend arg) subs in
apply_rec env sigma arg_state body (subs, c2) rest in let body = (Coercion.start_app_body sigma fj.uj_val) in let sigma, template_arity = match EConstr.kind sigma fj.uj_val with
| Ind (ind,u) | Construct ((ind,_),u) as k
when EInstance.is_empty u && Environ.template_polymorphic_ind ind !!env -> let ctoropt = match k with
| Ind _ -> None
| Construct ((_,ctor),_) -> Some ctor
| _ -> assert false in let arity = TemplateArity.get_template_arity !!env ind ~ctoropt in
sigma, Some arity
| _ -> sigma, None in let arg_state = (0,body,[],candargs) in let subst = Esubst.subs_id 0 in let typ = fj.uj_type in let sigma, body, subst, typ, arg_state, args = match template_arity with
| None -> sigma, body, subst, typ, arg_state, args
| Some typ -> let pretype_arg env sigma arg_state body arg na tycon =
pretype_arg env sigma arg_state body arg na tycon in
apply_template pretype_arg arg_state env sigma body subst (Int.Map.empty,Int.Map.empty) args typ in let sigma, resj, val_before_bidi, bidiargs =
apply_rec env sigma arg_state body (subst,typ) args in let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~flags env sigma resj tycon in let refine_arg (sigma,t) (newarg,ty,origarg,trace) = (* Refine an argument (originally `origarg`) represented by an evar
(`newarg`) to use typing information from the context *) (* Type the argument using the expected type *) let sigma, j = pretype (Some ty) env sigma origarg in (* Unify the (possibly refined) existential variable with the
(typechecked) original value *) let sigma = try Evarconv.unify_delay !!env sigma newarg (j_val j) with Evarconv.UnableToUnify (sigma,e) -> raise (PretypeError (!!env,sigma,CannotUnify (newarg,j_val j,Some e))) in
sigma, Coercion.push_arg (Coercion.reapply_coercions_body sigma trace t) (j_val j) in (* We now refine any arguments whose typing was delayed for
bidirectionality *) let t = val_before_bidi in let sigma, t = List.fold_left refine_arg (sigma,t) bidiargs in let t = Coercion.force_app_body t 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
{ resj with uj_val = Coercion.reapply_coercions sigma trace t } in
(sigma, resj)
let pretype_proj self ((f,us), args, c) = fun ?loc ~flags tycon env sigma ->
pretype_app self (DAst.make ?loc (GRef (GlobRef.ConstRef f,us)), args @ [c])
?loc ~flags tycon env sigma
let pretype_lambda self (name, bk, c1, c2) = fun ?loc ~flags tycon env sigma -> letopen Context.Rel.Declaration in let tycon' = if flags.program_mode && flags.use_coercions thenOption.map (Coercion.remove_subset !!env sigma) tycon else tycon in let sigma,name',dom,rng = match tycon' with
| None -> sigma,Anonymous, None, None
| Some ty -> let sigma, ty = Evardefine.presplit !!env sigma ty in match EConstr.kind sigma ty with
| Prod (na,dom,rng) ->
sigma, na.binder_name, Some dom, Some rng
| Evar ev -> (* define_evar_as_product works badly when impredicativity is possible but not known (#12623). OTOH if we know we are impredicative (typically Prop) we want to keep the
information when typing the body. *) let s = Retyping.get_sort_of !!env sigma ty in if Environ.is_impredicative_sort !!env (ESorts.kind sigma s)
|| Evd.check_leq sigma ESorts.type1 s then let sigma, prod = define_evar_as_product !!env sigma ev in let na,dom,rng = destProd sigma prod in
sigma, na.binder_name, Some dom, Some rng else
sigma, Anonymous, None, None
| _ -> if Reductionops.is_head_evar !!env sigma ty then sigma, Anonymous, None, None else (* No chance of unifying with a product.
NB: Funclass cannot be a source class so no coercions. *)
error_not_product ?loc !!env sigma ty in let dom_valcon = valcon_of_tycon dom in let sigma, j = eval_type_pretyper self ~flags dom_valcon env sigma c1 in let name = {binder_name=name; binder_relevance=ESorts.relevance_of_sort j.utj_type} in let var = LocalAssum (name, j.utj_val) in let hypnaming = VarSet.variables (Global.env ()) in let var',env' = push_rel ~hypnaming sigma var env in let sigma, j' = eval_pretyper self ~flags rng env' sigma c2 in let name = get_name var' in let resj = judge_of_abstraction !!env sigma (orelse_name name name') j j'in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~flags env sigma resj tycon
let pretype_prod self (name, bk, c1, c2) = fun ?loc ~flags tycon env sigma -> letopen Context.Rel.Declaration in let pretype_type tycon env sigma c = eval_type_pretyper self ~flags tycon env sigma c in let sigma, j = pretype_type empty_valcon env sigma c1 in let hypnaming = VarSet.variables (Global.env ()) in let sigma, name, j' = match name with
| Anonymous -> let sigma, j = pretype_type empty_valcon env sigma c2 in
sigma, name, { j with utj_val = lift 1 j.utj_val }
| Name _ -> let r = ESorts.relevance_of_sort j.utj_type in let var = LocalAssum (make_annot name r, j.utj_val) in let var, env' = push_rel ~hypnaming sigma var env in let sigma, c2_j = pretype_type empty_valcon env' sigma c2 in
sigma, get_name var, c2_j in let resj = try
judge_of_product !!env sigma name j j' with TypeError _ as e -> let (e, info) = Exninfo.capture e in let info = Option.cata (Loc.add_loc info) info loc in
Exninfo.iraise (e, info) in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~flags env sigma resj tycon
let pretype_letin self (name, c1, t, c2) = fun ?loc ~flags tycon env sigma -> letopen Context.Rel.Declaration in let pretype tycon env sigma c = eval_pretyper self ~flags tycon env sigma c in let pretype_type tycon env sigma c = eval_type_pretyper self ~flags tycon env sigma c in let sigma, tycon1 = match t with
| Some t -> let sigma, t_j = pretype_type empty_valcon env sigma t in
sigma, mk_tycon t_j.utj_val
| None ->
sigma, empty_tycon in let sigma, j = pretype tycon1 env sigma c1 in let sigma, t = Evarsolve.refresh_universes
~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma j.uj_type in let r = Retyping.relevance_of_term !!env sigma j.uj_val in let var = LocalDef (make_annot name r, j.uj_val, t) in let tycon = lift_tycon 1 tycon in let hypnaming = VarSet.variables (Global.env ()) in let var, env = push_rel ~hypnaming sigma var env in let sigma, j' = pretype tycon env sigma c2 in let name = get_name var in
sigma, { uj_val = mkLetIn (make_annot name r, j.uj_val, t, j'.uj_val) ;
uj_type = subst1 j.uj_val j'.uj_type }
let pretype_lettuple self (nal, (na, po), c, d) = fun ?loc ~flags tycon env sigma -> letopen Context.Rel.Declaration in let pretype tycon env sigma c = eval_pretyper self ~flags tycon env sigma c in let pretype_type tycon env sigma c = eval_type_pretyper self ~flags tycon env sigma c in let sigma, cj = pretype empty_tycon env sigma c in let (IndType (indf,realargs)) as indty = try find_rectype !!env sigma cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in
error_case_not_inductive ?loc:cloc !!env sigma cj in let ind = fst (fst (dest_ind_family indf)) in let cstrs = get_constructors !!env indf in ifnot (Int.equal (Array.length cstrs) 1) then
user_err ?loc (str "Destructing let is only for inductive types" ++
str " with one constructor."); let cs = cstrs.(0) in ifnot (Int.equal (List.length nal) cs.cs_nargs) then
user_err ?loc:loc (str "Destructing let on this type expects " ++
int cs.cs_nargs ++ str " variables."); let fsign, record = match Environ.get_projections !!env ind with
| None -> List.map2 set_name (List.rev nal) cs.cs_args, false
| Some ps -> let rec aux n k names l = match names, l with
| na :: names, (LocalAssum (na', t) :: l) -> let proj = Projection.make (fst ps.(cs.cs_nargs - k)) truein
LocalDef ({na' with binder_name = na},
lift (cs.cs_nargs - n) (mkProj (proj, na'.binder_relevance, cj.uj_val)), t)
:: aux (n+1) (k + 1) names l
| na :: names, (decl :: l) ->
set_name na decl :: aux (n+1) k names l
| [], [] -> []
| _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, truein let fsign = Context.Rel.map (whd_betaiota !!env sigma) fsign in let hypnaming = VarSet.variables (Global.env ()) in let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in let obj indt rci p v f = ifnot record then let f = it_mkLambda_or_LetIn f fsign in let ci = make_case_info !!env (ind_of_ind_type indt) LetStyle in
mkCase (EConstr.contract_case !!env sigma (ci, (p,rci), make_case_invert !!env sigma indt ~case_relevance:rci ci, cj.uj_val,[|f|])) else it_mkLambda_or_LetIn f fsign in (* Make dependencies from arity signature impossible *) let arsgn, indr = let arsgn = get_arity !!env indf in List.map (set_name Anonymous) arsgn, Inductiveops.relevance_of_inductive_family !!env indf in let indt = build_dependent_inductive !!env indf in let psign = LocalAssum (make_annot na indr, indt) :: arsgn in(* For locating names in [po] *) let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in let nar = List.length arsgn in let psign',env_p = push_rel_context ~hypnaming ~force_names:true sigma psign predenv in
(match po with
| Some p -> let sigma, pj = pretype_type empty_valcon env_p sigma p in let ccl = nf_evar sigma pj.utj_val in let p = it_mkLambda_or_LetIn ccl psign' in let inst =
(Array.to_list cs.cs_concl_realargs)
@ [build_dependent_constructor cs] in let lp = lift cs.cs_nargs p in let fty = hnf_lam_applist !!env sigma lp inst in let sigma, fj = pretype (mk_tycon fty) env_f sigma d in let sigma, v = let ind,_ = dest_ind_family indf in let sigma, rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in
sigma, obj indty rci p cj.uj_val fj.uj_val in
sigma, { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) }
| None -> let tycon = lift_tycon cs.cs_nargs tycon in let sigma, fj = pretype tycon env_f sigma d in let ccl = nf_evar sigma fj.uj_type in let ccl = if noccur_between sigma 1 cs.cs_nargs ccl then
lift (- cs.cs_nargs) ccl else
error_cant_find_case_type ?loc !!env sigma
cj.uj_val in (* let ccl = refresh_universes ccl in *) let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign' in let sigma, v = let ind,_ = dest_ind_family indf in let sigma, rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in
sigma, obj indty rci p cj.uj_val fj.uj_val in sigma, { uj_val = v; uj_type = ccl })
let pretype_cases self (sty, po, tml, eqns) = fun ?loc ~flags tycon env sigma -> let pretype tycon env sigma c = eval_pretyper self ~flags tycon env sigma c in
Cases.compile_cases ?loc ~program_mode:flags.program_mode sty (pretype, sigma) tycon env (po,tml,eqns)
let pretype_if self (c, (na, po), b1, b2) = fun ?loc ~flags tycon env sigma -> letopen Context.Rel.Declaration in let pretype tycon env sigma c = eval_pretyper self ~flags tycon env sigma c in let sigma, cj = pretype empty_tycon env sigma c in let (IndType (indf,realargs)) as indty = try find_rectype !!env sigma cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in
error_case_not_inductive ?loc:cloc !!env sigma cj in let cstrs = get_constructors !!env indf in ifnot (Int.equal (Array.length cstrs) 2) then
user_err ?loc
(str "If is only for inductive types with two constructors.");
let arsgn, indr = let arsgn = get_arity !!env indf in (* Make dependencies from arity signature impossible *) List.map (set_name Anonymous) arsgn, Inductiveops.relevance_of_inductive_family !!env indf in let nar = List.length arsgn in let indt = build_dependent_inductive !!env indf in let psign = LocalAssum (make_annot na indr, indt) :: arsgn in(* For locating names in [po] *) let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in let hypnaming = VarSet.variables (Global.env ()) in let psign,env_p = push_rel_context ~hypnaming sigma psign predenv in let sigma, pred, p = match po with
| Some p -> let sigma, pj = eval_type_pretyper self ~flags empty_valcon env_p sigma p in let ccl = nf_evar sigma pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in let typ = lift (- nar) (beta_applist sigma (pred,[cj.uj_val])) in
sigma, pred, typ
| None -> let sigma, p = match tycon with
| Some ty -> sigma, ty
| None -> new_type_evar env sigma ~src:(loc,Evar_kinds.CasesType false) in
sigma, it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar sigma pred in let p = nf_evar sigma p in let f sigma 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 sigma (pi, [build_dependent_constructor cs]) in let cs_args = cs.cs_args in let cs_args = Context.Rel.map (whd_betaiota !!env sigma) cs_args in let csgn = List.map (set_name Anonymous) cs_args in let _,env_c = push_rel_context ~hypnaming sigma csgn env in let sigma, bj = pretype (mk_tycon pi) env_c sigma b in
sigma, it_mkLambda_or_LetIn bj.uj_val cs_args in let sigma, b1 = f sigma cstrs.(0) b1 in let sigma, b2 = f sigma cstrs.(1) b2 in let sigma, v = let ind,_ = dest_ind_family indf in let pred = nf_evar sigma pred in let sigma, rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val pred in let ci = make_case_info !!env (fst ind) IfStyle in
sigma, mkCase (EConstr.contract_case !!env sigma
(ci, (pred,rci),
make_case_invert !!env sigma indty ~case_relevance:rci ci, cj.uj_val,
[|b1;b2|])) in let cj = { uj_val = v; uj_type = p } in
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~flags env sigma cj tycon
let pretype_cast self (c, k, t) = fun ?loc ~flags tycon env sigma -> let pretype tycon env sigma c = eval_pretyper self ~flags tycon env sigma c in let sigma, cj = let sigma, tj = eval_type_pretyper self ~flags empty_valcon env sigma t in let tval = nf_evar sigma tj.utj_val in let (sigma, cj), tval = match k with
| Some VMcast -> let sigma, cj = pretype empty_tycon env sigma c in
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
