(************************************************************************) (* * 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) *) (************************************************************************)
open Pp open CErrors open Util open CAst open Names open Nameops open Namegen open Constr open Context open Libnames open Globnames open Impargs open Glob_term open Glob_ops open Patternops open Pretyping open Structures open Cases open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops open Notation open Inductiveops open Context.Rel.Declaration open NumTok
(** constr_expr -> glob_constr translation: - it adds holes for implicit arguments - it replaces notations by their value (scopes stuff are here) - it recognizes global vars from local ones - it prepares pattern matching problems (a pattern becomes a tree where nodes are constructor/variable pairs and leafs are variables)
All that at once, fasten your seatbelt!
*)
(* To interpret implicits and arg scopes of variables in inductive
types and recursive definitions and of projection names in records *)
let var_uid = let count = ref 0 in fun id -> incr count; Id.to_string id ^ ":" ^ string_of_int !count
type var_internalization_data = { (* type of the "free" variable, for coqdoc, e.g. while typing the
constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
var_intern_typ : var_internalization_type; (* signature of impargs of the variable *)
var_impls : Impargs.implicit_status list; (* subscopes of the args of the variable *)
var_scopes : scope_name listlist; (* unique ID for coqdoc links *)
var_uid : var_unique_id;
}
type internalization_error =
| VariableCapture of Id.t * Id.t
| IllegalMetavariable
| NotAConstructor of qualid
| UnboundFixName ofbool * Id.t
| NonLinearPattern of Id.t
| BadPatternsNumber of int * int
| NotAProjection of qualid
| ProjectionsOfDifferentRecords ofStructure.t * Structure.t
exception InternalizationError of internalization_error
let explain_variable_capture id id' =
Id.print id ++ str " is dependent in the type of " ++ Id.print id' ++
strbrk ": cannot interpret both of them with the same type"
let explain_illegal_metavariable =
str "Metavariables allowed only in patterns"
let explain_unbound_fix_name is_cofix id =
str "The name" ++ spc () ++ Id.print id ++
spc () ++ str "is not bound in the corresponding" ++ spc () ++
str (if is_cofix then"co"else"") ++ str "fixpoint definition"
let explain_non_linear_pattern id =
str "The variable " ++ Id.print id ++ str " is bound several times in pattern"
let explain_bad_patterns_number n1 n2 =
str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++
str " but found " ++ int n2
let inductive_of_record s = let inductive = GlobRef.IndRef (s.Structure.name) in
Nametab.shortest_qualid_of_global Id.Set.empty inductive
let explain_field_not_a_projection field_id =
pr_qualid field_id ++ str ": Not a projection"
let explain_projections_of_diff_records record1 record2 = let inductive1_id = inductive_of_record record1 in let inductive2_id = inductive_of_record record2 in
str "This record contains fields of both " ++ pr_qualid inductive1_id ++
str " and " ++ pr_qualid inductive2_id
let explain_internalization_error e = let pp = match e with
| VariableCapture (id,id') -> explain_variable_capture id id'
| IllegalMetavariable -> explain_illegal_metavariable
| NotAConstructor ref -> explain_not_a_constructor ref
| UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
| NonLinearPattern id -> explain_non_linear_pattern id
| BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
| NotAProjection field_id -> explain_field_not_a_projection field_id
| ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) ->
explain_projections_of_diff_records inductive1_id inductive2_id in pp ++ str "."
let _ = CErrors.register_handler (function
| InternalizationError e ->
Some (explain_internalization_error e)
| _ -> None)
let error_bad_inductive_type ?loc ?info () =
user_err ?loc ?info (str "This should be an inductive type applied to patterns.")
let error_parameter_not_implicit ?loc =
user_err ?loc (str "The parameters do not bind in patterns;" ++ spc () ++ str "they must be replaced by '_'.")
let error_ldots_var ?loc =
user_err ?loc (str "Special token " ++ Id.print ldots_var ++
str " is for use in the Notation command.")
(**********************************************************************) (* Pre-computing the implicit arguments and arguments scopes needed *) (* for interpretation *)
let parsing_explicit = reffalse
let empty_internalization_env = Id.Map.empty
let compute_internalization_data env sigma ?silent id ty typ impl = let impl = compute_implicits_with_manual env sigma ?silent typ (is_implicit_args()) impl in
make_var_data ty impl (compute_arguments_scope env sigma typ) (var_uid id)
let compute_internalization_env env sigma ?(impls=empty_internalization_env) ?force ty names = let force = match force with None -> List.map (fun _ -> Id.Set.empty) names | Some l -> l in let f force_ids = function {impl_pos=(na,_,_)} as impl -> match na with
| Name id when Id.Set.mem id force_ids -> {impl with impl_force = false}
| _ -> impl in List.fold_left4
(funmap id force_ids typ impl -> let var_info = compute_internalization_data env sigma id ty typ impl in let impls = List.map (Option.map (f force_ids)) var_info.var_impls in
Id.Map.add id {var_info with var_impls = impls} map)
impls names force
let implicits_of_decl_in_internalization_env id (int_env:internalization_env) = let {var_impls=impls} = Id.Map.find id int_env in impls
(**********************************************************************) (* Contracting "{ _ }" in notations *)
let rec wildcards ntn n = if Int.equal n (String.length ntn) then [] elselet l = spaces ntn (n+1) inif ntn.[n] == '_'then n::l else l and spaces ntn n = if Int.equal n (String.length ntn) then [] elseif ntn.[n] == ' 'then wildcards ntn (n+1) else spaces ntn (n+1)
let expand_notation_string ntn n = let pos = List.nth (wildcards ntn 0) n in let hd = if Int.equal pos 0 then""elseString.sub ntn 0 pos in let tl = if Int.equal pos (String.length ntn) then"" elseString.sub ntn (pos+1) (String.length ntn - pos -1) in
hd ^ "{ _ }" ^ tl
(* This contracts the special case of "{ _ }" for sumbool, sumor notations *) (* Remark: expansion of squash at definition is done in metasyntax.ml *) let contract_curly_brackets ntn (l,ll,bl,bll) = match ntn with
| InCustomEntry _,_ -> ntn,(l,ll,bl,bll)
| InConstrEntry, ntn -> let ntn' = ref ntn in let rec contract_squash n = function
| [] -> []
| { CAst.v = CNotation (None,(InConstrEntry,"{ _ }"),([a],[],[],[])) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
a::contract_squash (n+1) l in let l = contract_squash 0 l in (* side effect; don't inline *)
(InConstrEntry,!ntn'),(l,ll,bl,bll)
let contract_curly_brackets_pat ntn (l,ll,bl) = match ntn with
| InCustomEntry _,_ -> ntn,(l,ll,bl)
| InConstrEntry, ntn -> let ntn' = ref ntn in let rec contract_squash n = function
| [] -> []
| { CAst.v = CPatNotation (None,(InConstrEntry,"{ _ }"),([a],[],[]),[]) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
a::contract_squash (n+1) l in let l = contract_squash 0 l in (* side effect; don't inline *)
(InConstrEntry,!ntn'),(l,ll,bl)
type intern_env = {
ids: Id.Set.t;
strict_check: booloption; (* None = not passed via ltac yet: works as "true" unless when interpreting
ltac:() in which case we assume the default Ltac value, that is "false" *)
local_univs: local_univs;
tmp_scope: Notation_term.tmp_scope_name list;
scopes: Notation_term.scope_name list;
impls: internalization_env;
binder_block_names: abstraction_kind option(* None = unknown *) option;
ntn_binding_ids: Id.Set.t; (* subset of ids that are notation variables *)
}
type pattern_intern_env = {
pat_scopes: Notation_term.subscopes; (* ids = Some means accept local variables; this is useful for
terms as patterns parsed as patterns in notations *)
pat_ids: Id.Set.t option;
}
(**********************************************************************) (* Remembering the parsing scope of variables in notations *)
let make_current_scope tmp scopes = match tmp, scopes with
| [], scopes -> scopes
| [tmp_scope], (sc :: _) when String.equal sc tmp_scope -> scopes
| tmp_scope, scopes -> tmp_scope @ scopes
let pr_scope_stack begin_of_sentence l = let bstr x = if begin_of_sentence then str (CString.capitalize_ascii x) else str x in match l with
| [] -> bstr "the empty scope stack"
| [a] -> bstr "scope " ++ str a
| l -> bstr "scope stack " ++
str "[" ++ prlist_with_sep pr_comma str l ++ str "]"
let warn_inconsistent_scope =
CWarnings.create ~name:"inconsistent-scopes" ~category:CWarnings.CoreCategories.syntax
(fun (id,scopes1,scopes2) ->
(str "Argument " ++ Id.print id ++
strbrk " was previously inferred to be in " ++
pr_scope_stack false scopes1 ++
strbrk " but is here used in " ++
pr_scope_stack false scopes2 ++
strbrk ". " ++
pr_scope_stack true scopes1 ++
strbrk " will be used at parsing time unless you override it by" ++
strbrk " annotating the argument with an explicit scope of choice."))
let error_expect_binder_notation_type ?loc id =
user_err ?loc
(Id.print id ++
str " is expected to occur in binding position in the right-hand side.")
let set_notation_var_scope ?loc id (tmp_scope,subscopes as scopes) ntnbinders ntnvars = try let {Genintern.ntnvar_typ=typ} as status = Id.Map.find id ntnvars in match typ with
| Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id
| Notation_term.NtnInternTypeAny principal -> let () = match status.ntnvar_scopes with
| None -> status.ntnvar_scopes <- Some scopes
| Some (tmp_scope', subscopes') -> let s' = make_current_scope tmp_scope' subscopes' in let s = make_current_scope tmp_scope subscopes in ifOption.is_empty principal && not (List.equal String.equal s' s) then
warn_inconsistent_scope ?loc (id,s',s) in let () = match status.ntnvar_binding_ids with
| None -> status.ntnvar_binding_ids <- Some ntnbinders
| Some ntnbinders' -> status.ntnvar_binding_ids <- Some (Id.Set.inter ntnbinders ntnbinders') in let () = match status.ntnvar_used with
| [] -> () (* not recording if notation var is used *)
| true :: _ -> () (* already marked used *)
| false :: rest -> status.ntnvar_used <- true :: rest in
() with Not_found -> (* Not in a notation *)
()
let set_var_is_binder ?loc id ntnvars = try let status = Id.Map.find id ntnvars in
status.Genintern.ntnvar_used_as_binder <- true with Not_found -> (* Not in a notation *)
()
let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_names ()}
let reset_tmp_scope env = {env with tmp_scope = []}
let set_env_scopes env (scopt,subscopes) =
{env with tmp_scope = scopt; scopes = subscopes @ env.scopes}
let env_for_pattern env =
{pat_scopes = (env.tmp_scope, env.scopes); pat_ids = Some env.ids}
let mkGProd ?loc (na,bk,t) body = DAst.make ?loc @@ GProd (na, None, bk, t, body) let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, None, bk, t, body)
(**********************************************************************) (* Utilities for binders *)
let warn_shadowed_implicit_name =
CWarnings.create ~name:"shadowed-implicit-name" ~category:CWarnings.CoreCategories.syntax
Pp.(fun na -> str "Making shadowed name of implicit argument accessible by position.")
let exists_name na l = match na with
| Name id -> List.exists (function Some { impl_pos = (Name id', _, _) } -> Id.equal id id' | _ -> false) l
| _ -> false
let build_impls ?loc n bk na acc = let impl_status max = let na = if exists_name na acc thenbegin warn_shadowed_implicit_name ?loc na; Anonymous end else na in
Some {
impl_pos = (na, n, (*TODO, enhancement: compute dependency*) None);
impl_expl = Manual;
impl_max = max;
impl_force = true
} in match bk with
| NonMaxImplicit -> impl_status false :: acc
| MaxImplicit -> impl_status true :: acc
| Explicit -> None :: acc
let impls_binder_list = let rec aux acc n = function
| (na,_,bk,None,_) :: binders -> aux (build_impls n bk na acc) (n+1) binders
| (na,_,bk,Some _,_) :: binders -> aux acc n binders
| [] -> (n,acc) in aux []
let impls_type_list n ?(args = []) = let rec aux acc n c = match DAst.get c with
| GProd (na,_,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
| _ -> List.rev acc in aux args n
let impls_term_list n ?(args = []) = let rec aux acc n c = match DAst.get c with
| GLambda (na,_,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
| GRec (fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in let n,acc' = List.fold_left (fun (n,acc) (na, _, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in
aux acc' n bds.(nb)
|_ -> List.rev acc in aux args n
(* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *) let rec check_capture ty = letopen CAst in function
| { loc; v = Name id } :: { v = Name id' } :: _ when occur_glob_constr id ty ->
Loc.raise ?loc (InternalizationError (VariableCapture (id,id')))
| _::nal ->
check_capture ty nal
| [] ->
()
(** Status of the internalizer wrt "Arguments" of names *)
let restart_no_binders env =
{ env with binder_block_names = None} (* Not in relation with the "Arguments" of a name *)
let restart_prod_binders env =
{ env with binder_block_names = Some (Some AbsPi) } (* In a position binding a type to a name *)
let restart_lambda_binders env =
{ env with binder_block_names = Some (Some AbsLambda) } (* In a position binding a body to a name *)
let switch_prod_binders env = match env.binder_block_names with
| Some o when o <> Some AbsLambda -> restart_prod_binders env
| _ -> restart_no_binders env (* In a position switching to a type *)
let switch_lambda_binders env = match env.binder_block_names with
| Some o when o <> Some AbsPi -> restart_lambda_binders env
| _ -> restart_no_binders env (* In a position switching to a term *)
let slide_binders env = match env.binder_block_names with
| Some o when o <> Some AbsPi -> restart_prod_binders env
| _ -> restart_no_binders env (* In a position of cast *)
(* [test_kind_strict] rules out pattern which refers to global other
than constructors or variables; It is used in instances of notations *)
let test_kind_pattern_in_notation ?loc = function
| GlobRef.ConstructRef _ -> () (* We do not accept non constructors to be used as variables in
patterns *)
| GlobRef.ConstRef _ ->
user_err ?loc (str "Found a constant while a pattern was expected.")
| GlobRef.IndRef _ ->
user_err ?loc (str "Found an inductive type while a pattern was expected.")
| GlobRef.VarRef _ -> (* we accept a section variable name to be used as pattern variable *) raise Not_found
let test_kind_ident_in_notation ?loc = function
| GlobRef.ConstructRef _ ->
user_err ?loc (str "Found a constructor while a variable name was expected.")
| GlobRef.ConstRef _ ->
user_err ?loc (str "Found a constant while a variable name was expected.")
| GlobRef.IndRef _ ->
user_err ?loc (str "Found an inductive type while a variable name was expected.")
| GlobRef.VarRef _ -> (* we accept a section variable name to be used as pattern variable *) raise Not_found
(* [test_kind_tolerant] allow global reference names to be used as pattern variables *)
let test_kind_tolerant ?loc = function
| GlobRef.ConstructRef _ -> ()
| GlobRef.ConstRef _ | GlobRef.IndRef _ | GlobRef.VarRef _ -> (* A non-constructor global reference in a pattern is seen as a variable *) raise Not_found
(**)
let locate_if_hole ?loc na c = match DAst.get c with
| GHole (GNamedHole _) -> c
| GHole _ ->
(trymatch na with
| Name id -> glob_constr_of_notation_constr ?loc
(Reserve.find_reserved_type id)
| Anonymous -> raise Not_found with Not_found -> DAst.make ?loc @@ GHole (GBinderType na))
| _ -> c
let pure_push_name_env (id,implargs,is_ntn_id) env =
{env with
ids = Id.Set.add id env.ids;
impls = Id.Map.add id implargs env.impls;
ntn_binding_ids = if is_ntn_id then Id.Set.add id env.ntn_binding_ids else env.ntn_binding_ids;
}
let push_name_env ~dump ntnvars implargs env = letopen CAst in
function
| { loc; v = Anonymous } ->
env
| { loc; v = Name id } -> if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc;
set_var_is_binder ?loc id ntnvars; let uid = var_uid id in if dump then Dumpglob.dump_binding ?loc uid;
pure_push_name_env (id,(make_var_data Variable implargs [] uid),Id.Map.mem id ntnvars) env
let remember_binders_impargs env bl = List.map_filter (fun (na,_,_,_,_) -> match na with
| Anonymous -> None
| Name id -> Some (id,Id.Map.find id env.impls,Id.Set.mem id env.ntn_binding_ids)) bl
let restore_binders_impargs env l = List.fold_right pure_push_name_env l env
let warn_ignoring_unexpected_implicit_binder_declaration =
CWarnings.create ~name:"unexpected-implicit-declaration" ~category:CWarnings.CoreCategories.syntax
Pp.(fun () -> str "Ignoring implicit binder declaration in unexpected position.")
let check_implicit_meaningful ?loc k env = if k <> Explicit && env.binder_block_names = None then
(warn_ignoring_unexpected_implicit_binder_declaration ?loc (); Explicit) else
k
let intern_generalized_binder ~dump intern_type ntnvars
env {loc;v=na} b' t ty = let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in let ty, ids' = if t then ty, ids else Implicit_quantifiers.implicit_application ids ty in let ty' = intern_type {env with ids = ids; strict_check = Some false} ty in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty'in let env' = List.fold_left
(fun env {loc;v=x} -> push_name_env ~dump ntnvars [](*?*) env (make ?loc @@ Name x))
env fvs in let b' = check_implicit_meaningful ?loc b' env in let bl = List.map
CAst.(map (fun id ->
(Name id, MaxImplicit, DAst.make ?loc @@ GHole (GBinderType (Name id)))))
fvs in let na = match na with
| Anonymous -> let id = match ty with
| { v = CApp ({ v = CRef (qid,_) }, _) } when qualid_is_ident qid ->
qualid_basename qid
| _ -> default_non_dependent_ident in let ids' = List.fold_left (fun ids' lid -> Id.Set.add lid.CAst.v ids') ids' fvs in let id =
Implicit_quantifiers.make_fresh ids' (Global.env ()) id in
Name id
| _ -> na in let impls = impls_type_list 1 ty' in
(push_name_env ~dump ntnvars impls env' (make ?loc na),
(make ?loc (na,b',ty')) :: List.rev bl)
let intern_assumption ~dump intern ntnvars env nal bk ty = let intern_type env = intern (restart_prod_binders (set_type_scope env)) in match bk with
| Default k -> let ty = intern_type env ty in
check_capture ty nal; let impls = impls_type_list 1 ty in List.fold_left
(fun (env, bl) ({loc;v=na} as locna) -> let k = check_implicit_meaningful ?loc k env in
(push_name_env ~dump ntnvars impls env locna,
(make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
(env, []) nal
| Generalized (b',t) -> let env, b = intern_generalized_binder ~dump intern_type ntnvars env (List.hd nal) b' t ty in
env, b
let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
| GLocalAssum (na,r,bk,t) -> (na,None,bk,None,t)
| GLocalDef (na,r,c,Some t) -> (na,None,Explicit,Some c,t)
| GLocalDef (na,r,c,None) -> let t = DAst.make ?loc @@ GHole (GBinderType na) in
(na,None,Explicit,Some c,t)
| GLocalPattern (_,_,_,_) ->
Loc.raise ?loc (Gramlib.Grammar.Error "Pattern with quote not allowed here")
)
let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
let intern_letin_binder ~dump intern ntnvars env (({loc;v=na} as locna),def,ty) = let term = intern (reset_tmp_scope (restart_lambda_binders env)) def in let ty = Option.map (intern (set_type_scope (restart_prod_binders env))) ty in let impls = impls_term_list 1 term in
(push_name_env ~dump ntnvars impls env locna,
(na,term,ty))
let intern_cases_pattern_as_binder ~dump intern test_kind ntnvars env bk (CAst.{v=p;loc} as pv) = let p,t,tmp_scope = match p with
| CPatCast (p, t) -> (p, Some t, (* Redone later, not nice: *) Notation.compute_glob_type_scope (intern (set_type_scope env) t))
| _ -> (pv, None, []) in let il,disjpat = let (il, subst_disjpat) = !intern_cases_pattern_fwd test_kind ntnvars (env_for_pattern {env with tmp_scope}) p in let substl,disjpat = List.split subst_disjpat in ifnot (List.for_all (fun subst -> Id.Map.equal Id.equal subst Id.Map.empty) substl) then
user_err ?loc (str "Unsupported nested \"as\" clause.");
il,disjpat in let na = alias_of_pat (List.hd disjpat) in let env = List.fold_right (fun {loc;v=id} env -> push_name_env ~dump ntnvars [] env (make ?loc @@ Name id)) il env in let ienv = Name.fold_right Id.Set.remove na env.ids in let id = Namegen.next_name_away_with_default "pat" na ienv in let na = make ?loc @@ Name id in let t = match t with
| Some t -> t
| None -> CAst.make ?loc @@ CHole (Some (GBinderType na.v)) in let _, bl' = intern_assumption ~dump intern ntnvars env [na] (Default bk) t in let {v=(_,bk,t)} = List.hd bl' in let il = List.map (fun id -> id.v) il in
env,((disjpat,il),id),bk,t
let intern_local_binder_aux ~dump intern ntnvars (env,bl) = function
| CLocalAssum(nal,_,bk,ty) -> let env, bl' = intern_assumption ~dump intern ntnvars env nal bk ty in let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,None,c,t)) bl'in
env, bl' @ bl
| CLocalDef( {loc; v=na} as locna,_,def,ty) -> let env,(na,def,ty) = intern_letin_binder ~dump intern ntnvars env (locna,def,ty) in
env, (DAst.make ?loc @@ GLocalDef (na,None,def,ty)) :: bl
| CLocalPattern p -> let env, ((disjpat,il),id),bk,t = intern_cases_pattern_as_binder ~dump intern test_kind_tolerant ntnvars env Explicit p in
(env, (DAst.make ?loc:p.CAst.loc @@ GLocalPattern((disjpat,il),id,bk,t)) :: bl)
let intern_generalization intern env ntnvars loc bk c = let c = intern {env with strict_check = Some false} c in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:env.ids c in let env', c' = let abs = let pi = match Notation.current_type_scope_names () with
| [] -> false
| type_scopes -> let is_type_scope = match env.tmp_scope with
| [] -> false
| scl -> List.equal String.equal scl type_scopes in
is_type_scope || List.exists (fun sc -> String.List.mem sc env.scopes) type_scopes in if pi then
(fun {loc=loc';v=id} acc ->
DAst.make ?loc:(Loc.merge_opt loc' loc) @@
GProd (Name id, None, bk, DAst.make ?loc:loc' @@ GHole (GBinderType (Name id)), acc)) else
(fun {loc=loc';v=id} acc ->
DAst.make ?loc:(Loc.merge_opt loc' loc) @@
GLambda (Name id, None, bk, DAst.make ?loc:loc' @@ GHole (GBinderType (Name id)), acc)) in List.fold_right (fun ({loc;v=id} as lid) (env, acc) -> let env' = push_name_env ~dump:true ntnvars [] env CAst.(make @@ Name id) in
(env', abs lid acc)) fvs (env,c) in c'
let rec expand_binders ?loc mk bl c = match bl with
| [] -> c
| b :: bl -> match DAst.get b with
| GLocalDef (n, r, b, oty) ->
expand_binders ?loc mk bl (DAst.make ?loc @@ GLetIn (n, r, b, oty, c))
| GLocalAssum (n, _, bk, t) ->
expand_binders ?loc mk bl (mk ?loc (n,bk,t) c)
| GLocalPattern ((disjpat,ids), id, bk, ty) -> let tm = DAst.make ?loc (GVar id) in (* Distribute the disjunctive patterns over the shared right-hand side *) let eqnl = List.map (fun pat -> CAst.make ?loc (ids,[pat],c)) disjpat in let c = DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in
expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c)
let check_not_notation_variable f ntnvars = (* Check bug #4690 *) match DAst.get f with
| GVar id when Id.Map.mem id ntnvars ->
user_err (str "Prefix @ is not applicable to notation variables.")
| _ ->
()
let option_mem_assoc id = function
| Some (id',c) -> Id.equal id id'
| None -> false
let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = let fold1 _ (c, _) accu = Id.Set.union (free_vars_of_constr_expr c) accu in let fold2 _ (l, _) accu = let fold accu c = Id.Set.union (free_vars_of_constr_expr c) accu in List.fold_left fold accu l in let fold3 _ x accu = Id.Set.add x accu in let fvs1 = Id.Map.fold fold1 terms avoid in let fvs2 = Id.Map.fold fold2 termlists fvs1 in let fvs3 = Id.Map.fold fold3 renaming fvs2 in (* TODO binders *)
next_ident_away_from id (fun id -> Id.Set.mem id fvs3)
let is_patvar c = match DAst.get c with
| PatVar _ -> true
| _ -> false
let is_patvar_store store pat = match DAst.get pat with
| PatVar na -> ignore(store (CAst.make ?loc:pat.loc na)); true
| _ -> false
let out_patvar = CAst.map_with_loc (fun ?loc -> function
| CPatAtom (Some qid) when qualid_is_ident qid ->
Name (qualid_basename qid)
| CPatAtom None -> Anonymous
| _ -> assert false)
let canonize_type = function
| None -> None
| Some t as t' -> match DAst.get t with
| GHole (GBinderType _) -> None
| _ -> t'
let set_type ty1 ty2 = match canonize_type ty1, canonize_type ty2 with (* Not a meta-binding binder, we use the type given in the notation *)
| _, None -> ty1 (* A meta-binding binder meta-bound to a possibly-typed pattern *) (* the binder is supposed to come w/o an explicit type in the notation *)
| None, Some _ -> ty2
| Some ty1, Some t2 -> (* An explicitly typed meta-binding binder, not supposed to be a pattern; checked in interp_notation *)
user_err ?loc:t2.CAst.loc Pp.(str "Unexpected type constraint in notation already providing a type constraint.")
let cook_pattern ((disjpat, ids), id) = let store,get = set_temporary_memory () in let pat, na = match disjpat with
| [pat] when is_patvar_store store pat -> let na = get () in None, na.v
| _ -> Some ((ids,disjpat),id), Name id in
pat, na
let extract_pattern_from_binder b = match DAst.get b with
| GLocalDef _ -> user_err ?loc:b.CAst.loc (str "Local definitions not supported here.")
| GLocalAssum (na, _, bk, t) -> None, na, bk, t
| GLocalPattern (patl, id, bk, ty) -> let pat, na = cook_pattern (patl, id) in
pat, na, bk, ty
let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) binderopt avoid (renaming,env) na ty = match na with
| Anonymous -> (renaming,env), None, Anonymous, Explicit, set_type ty None
| Name id -> let test_kind = test_kind_tolerant in try (* We instantiate binder name with patterns which may be parsed as terms *) let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in let env,pat,bk,t = intern_pat test_kind ntnvars env Explicit pat in let pat, na = cook_pattern pat in
(renaming,env), pat, na, bk, set_type ty (Some t) with Not_found -> try (* Trying to associate a pattern *) let (pat,bk),(onlyident,scopes) = Id.Map.find id binders in let env = set_env_scopes env scopes in if onlyident then (* Do not try to interpret a variable as a constructor *) let na = out_patvar pat in let env = push_name_env ~dump:true ntnvars [] env na in let ty' = DAst.make @@ GHole (GBinderType na.CAst.v) in
(renaming,env), None, na.v, bk, set_type ty (Some ty') else (* Interpret as a pattern *) let env,pat,bk,t = intern_pat test_kind ntnvars env bk pat in let pat, na = cook_pattern pat in
(renaming,env), pat, na, bk, set_type ty (Some t) with Not_found -> if option_mem_assoc id binderopt then let binder = snd (Option.get binderopt) in let pat, na, bk, t = extract_pattern_from_binder binder in
(renaming,env), pat, na, bk, set_type ty (Some t) else (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) let id' = find_fresh_name renaming subst avoid id in let renaming = Id.Map.add id id' renaming in
(renaming,env), None, Name id', Explicit, set_type ty None
type binder_action =
| AddLetIn of lname * constr_expr * constr_expr option
| AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
| AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
| AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
| AddNList (* Insert a ".. term .." block *)
let dmap_with_loc f n =
CAst.map_with_loc (fun ?loc c -> f ?loc (DAst.get_thunk c)) n
let error_cannot_coerce_wildcard_term ?loc () =
user_err ?loc Pp.(str "Cannot turn \"_\" into a term.")
let error_cannot_coerce_disjunctive_pattern_term ?loc () =
user_err ?loc Pp.(str "Cannot turn a disjunctive pattern into a term.")
let terms_of_binders bl = let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function
| PatVar (Name id) -> CRef (qualid_of_ident id, None)
| PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
| PatCstr (c,l,_) -> let qid = qualid_of_path ?loc (Nametab.path_of_global (GlobRef.ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None) in let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in
CAppExpl ((qid,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with
| bnd :: l -> let loc = bnd.loc in beginmatch DAst.get bnd with
| GLocalAssum (Name id,_,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l
| GLocalDef (Name id,_,_,_) -> extract_variables l
| GLocalDef (Anonymous,_,_,_)
| GLocalAssum (Anonymous,_,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
| GLocalPattern (([u],_),_,_,_) -> term_of_pat u :: extract_variables l
| GLocalPattern ((_,_),_,_,_) -> error_cannot_coerce_disjunctive_pattern_term ?loc () end
| [] -> [] in
extract_variables bl
let flatten_generalized_binders_if_any y l = matchList.rev l with
| [] -> assert false
| l -> (* if l has more than one element, this means we had a generalized binder *) let select_iter a = match DAst.get a with
| GLocalAssum (Name id,_,_,_) when Id.equal id ldots_var -> AddNList
| _ -> AddBinderIter (y,a) in List.map select_iter l
let flatten_binders bl = let dispatch = function
| CLocalAssum (nal,r,bk,t) -> List.map (fun na -> CLocalAssum ([na],r,bk,t)) nal
| a -> [a] in List.flatten (List.map dispatch bl)
let rec adjust_env env = function (* We need to adjust scopes, binder blocks ... to the env expected
at the recursive occurrence; We do an underapproximation... *)
| NProd (_,_,c) -> adjust_env (switch_prod_binders env) c
| NLambda (_,_,c) -> adjust_env (switch_lambda_binders env) c
| NLetIn (_,_,_,c) -> adjust_env env c
| NVar id when Id.equal id ldots_var -> env
| NCast (c,_,_) -> adjust_env env c
| NApp _ -> restart_no_binders env
| NVar _ | NRef _ | NHole _ | NGenarg _ | NCases _ | NLetTuple _ | NIf _
| NRec _ | NSort _ | NProj _ | NInt _ | NFloat _ | NString _ | NArray _
| NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *)
let subst_var loc intern_pat intern ntnvars binders (terms, binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) try let (a,scopes) = Id.Map.find id terms in
intern (set_env_scopes env scopes) a with Not_found -> try let (pat,bk),(onlyident,scopes) = Id.Map.find id binders in let env = set_env_scopes env scopes in let test_kind = if onlyident then test_kind_ident_in_notation else test_kind_pattern_in_notation in let env,((disjpat,ids),id),bk,_ty = intern_pat test_kind ntnvars env bk pat in (* TODO: use cast? *) match disjpat with
| [pat] -> glob_constr_of_cases_pattern (Global.env()) pat
| _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") with Not_found -> try match binderopt with
| Some (x,binder) when Id.equal x id -> let terms = terms_of_binders [binder] in
assert (List.length terms = 1);
intern env (List.hd terms)
| _ -> raise Not_found with Not_found ->
DAst.make ?loc ( try
GVar (Id.Map.find id renaming) with Not_found -> (* Happens for local notation joint with inductive/fixpoint defs *)
GVar id)
let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let (terms,termlists,binders,binderlists) = subst in (* when called while defining a notation, avoid capturing the private binders
of the expression by variables bound by the notation (see #3892) *) let avoid = Id.Map.domain ntnvars in let rec aux (terms,binderopt,iteropt as subst') (renaming,env) c = let subinfos = renaming,{env with tmp_scope = []} in match c with
| NVar id when Id.equal id ldots_var -> (* apply the pending sequence of letin, term iterator instances,
binder iterator instances, and eventually terminator *) let rec aux_letin env = function
| [],terminator,_ -> aux (terms,None,None) (renaming,env) terminator
| AddPreBinderIter (y,binder)::rest,terminator,iter -> let env,binders = intern_local_binder_aux ~dump:true intern ntnvars (adjust_env env iter,[]) binder in let binders = flatten_generalized_binders_if_any y binders in
aux_letin env (binders@rest,terminator,iter)
| AddBinderIter (y,binder)::rest,terminator,iter -> (* [y] is the placeholder for the [binder] in [iter] *)
aux (terms,Some (y,binder),Some (rest,terminator,iter)) (renaming,env) iter
| AddTermIter nterms::rest,terminator,iter -> (* This time, the variable [y] is the placeholder for the [binder] in [iter] *)
aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter
| AddLetIn (na,c,t)::rest,terminator,iter -> let env,(na,c,t) = intern_letin_binder ~dump:true intern ntnvars (adjust_env env iter) (na,c,t) in
DAst.make ?loc (GLetIn (na,None,c,t,aux_letin env (rest,terminator,iter)))
| AddNList::rest,terminator,iter ->
DAst.make ?loc (GApp (DAst.make ?loc (GVar ldots_var), [aux_letin env (rest,terminator,iter)])) in
aux_letin env (Option.get iteropt)
| NVar id -> subst_var loc intern_pat intern ntnvars binders subst' (renaming, env) id
| NList (x,y,iter,terminator,revert) -> let l,(scopt,subscopes) = (* All elements of the list are in scopes (scopt,subscopes) *) try let l,scopes = Id.Map.find x termlists in
(if revert thenList.rev l else l),scopes with Not_found -> try let (bl,(scopt,subscopes)) = Id.Map.find x binderlists in let env,bl' = List.fold_left (intern_local_binder_aux ~dump:true intern ntnvars) (env,[]) bl in
terms_of_binders (if revert then bl' else List.rev bl'),([],[]) with Not_found ->
anomaly (Pp.str "Inconsistent substitution of recursive notation.") in let select_iter a = match a.CAst.v with
| CRef (qid,None) when qualid_is_ident qid && Id.equal (qualid_basename qid) ldots_var -> AddNList
| _ -> AddTermIter (Id.Map.add y (a,(scopt,subscopes)) terms) in let l = List.map select_iter l in
aux (terms,None,Some (l,terminator,iter)) subinfos (NVar ldots_var)
| NHole (knd) -> let knd = match knd with
| GBinderType (Name id as na) -> let na = try (coerce_to_name (fst (Id.Map.find id terms))).v with Not_found -> try Name (Id.Map.find id renaming) with Not_found -> na in
GBinderType na
| _ -> knd in
DAst.make ?loc @@ GHole (knd)
| NGenarg arg -> let glob_of_term (c, scopes) = let nenv = set_env_scopes env scopes in let gc = intern nenv c in
gc in let glob_of_binder ((c,_bk), (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in let test_kind = if onlyident then test_kind_ident_in_notation else test_kind_pattern_in_notation in let _,((disjpat,_),_),_,_ty = intern_pat test_kind ntnvars nenv Explicit c in (* TODO: use cast? *) match disjpat with
| [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat)
| _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in let get_glob id = match Id.Map.find_opt id terms with
| Some term -> Some (glob_of_term term)
| None -> match Id.Map.find_opt id binders with
| Some binder -> Some (glob_of_binder binder)
| None -> None in let arg = Genintern.generic_substitute_notation ntnvars get_glob arg in
DAst.make ?loc @@ GGenarg arg
| NBinderList (x,y,iter,terminator,revert) ->
(try (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = Id.Map.find x binderlists in (* We flatten binders so that we can interpret them at substitution time *) let bl = flatten_binders bl in let bl = if revert thenList.rev bl else bl in (* We isolate let-ins which do not contribute to the repeated pattern *) let l = List.map (function | CLocalDef (na,_,c,t) -> AddLetIn (na,c,t)
| binder -> AddPreBinderIter (y,binder)) bl in (* We stack the binders to iterate or let-ins to insert *)
aux (terms,None,Some (l,terminator,iter)) subinfos (NVar ldots_var) with Not_found ->
anomaly (Pp.str "Inconsistent substitution of recursive notation."))
| NProd (Name id, None, c') when option_mem_assoc id binderopt -> let binder = snd (Option.get binderopt) in
expand_binders ?loc mkGProd [binder] (aux subst' (renaming,env) c')
| NLambda (Name id, None, c') when option_mem_assoc id binderopt -> let binder = snd (Option.get binderopt) in
expand_binders ?loc mkGLambda [binder] (aux subst' (renaming,env) c')
| t ->
glob_constr_of_notation_constr_with_binders ?loc
(traverse_binder intern_pat ntnvars subst binderopt avoid) (aux subst') ~h:binder_status_fun subinfos t in aux (terms,None,None) infos c
(* Turning substitution coming from parsing and based on production into a substitution for interpretation and based on binding/constr
distinction *)
let cases_pattern_of_name {loc;v=na} = let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in
CAst.make ?loc (CPatAtom atom)
let cases_pattern_of_binder_as_constr a = function
| AsAnyPattern | AsStrictPattern -> coerce_to_cases_pattern_expr a
| AsIdent -> cases_pattern_of_id (coerce_to_id a)
| AsName -> cases_pattern_of_name (coerce_to_name a)
let is_onlyident = function
| AsIdent | AsName -> true
| AsAnyPattern | AsStrictPattern -> false
let split_by_type ids (subst : constr_notation_substitution) = let bind id scl l s = match l with
| [] -> assert false
| a::l -> l, Id.Map.add id (a,scl) s in let (terms,termlists,binders,binderlists),subst = List.fold_left (fun ((terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) (id,((_,scl),_,typ)) -> match typ with
| NtnTypeConstr -> let terms,terms' = bind id scl terms terms'in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
| NtnTypeBinder ntn_binder_kind -> let onlyident,a,terms,binders = match ntn_binder_kind with
| NtnBinderParsedAsConstr k -> let a,terms = List.sep_first terms in
is_onlyident k, (cases_pattern_of_binder_as_constr a k, Explicit), terms, binders
| NtnBinderParsedAsBinder -> let a,binders = List.sep_first binders in false, a, terms, binders
| NtnBinderParsedAsSomeBinderKind k -> let a,binders = List.sep_first binders in
is_onlyident k, a, terms, binders in let binders' = Id.Map.add id (a,(onlyident,scl)) binders'in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
| NtnTypeConstrList -> let termlists,termlists' = bind id scl termlists termlists'in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
| NtnTypeBinderList ntn_binder_kind -> let l,termlists,binderlists = match ntn_binder_kind with
| NtnBinderParsedAsConstr k -> let l,termlists = List.sep_first termlists in List.map (fun a -> CLocalPattern (cases_pattern_of_binder_as_constr a k)) l, termlists, binderlists
| NtnBinderParsedAsBinder | NtnBinderParsedAsSomeBinderKind _ -> let l,binderlists = List.sep_first binderlists in
l, termlists, binderlists in let binderlists' = Id.Map.add id (l,scl) binderlists'in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists'))
(subst,(Id.Map.empty,Id.Map.empty,Id.Map.empty,Id.Map.empty)) ids in
assert (terms = [] && termlists = [] && binders = [] && binderlists = []);
subst
let split_by_type_pat ?loc ids subst = let bind id (_,scopes) l s = match l with
| [] -> assert false
| a::l -> l, Id.Map.add id (a,scopes) s in let bind_binders id (_,scopes) l s = match l with
| [] -> assert false
| (a,Explicit)::l -> l, Id.Map.add id (a,scopes) s
| (a,(MaxImplicit|NonMaxImplicit))::l -> user_err (str "Implicit arguments not supported.") (* shouldn't arrive *) in let (terms,termlists,binders),subst = List.fold_left (fun ((terms,termlists,binders),(terms',termlists')) (id,(scl,_,typ)) -> match typ with
| NtnTypeConstr | NtnTypeBinder (NtnBinderParsedAsConstr _) -> let terms,terms' = bind id scl terms terms'in
(terms,termlists,binders),(terms',termlists')
| NtnTypeConstrList -> let termlists,termlists' = bind id scl termlists termlists'in
(terms,termlists,binders),(terms',termlists')
| NtnTypeBinder (NtnBinderParsedAsBinder | NtnBinderParsedAsSomeBinderKind _) -> let binders,terms' = bind_binders id scl binders terms'in
(terms,termlists,binders),(terms',termlists')
| NtnTypeBinderList _ -> error_invalid_pattern_notation ?loc ())
(subst,(Id.Map.empty,Id.Map.empty)) ids in
assert (terms = [] && termlists = [] && binders = []);
subst
let intern_notation intern env ntnvars loc ntn fullargs = (* Adjust to parsing of { } *) let ntn,fullargs = contract_curly_brackets ntn fullargs in (* Recover interpretation { } *) let ((ids,c),df) = interp_notation ?loc ntn (env.tmp_scope,env.scopes) in
Dumpglob.dump_notation_location (ntn_loc ?loc fullargs ntn) ntn df; (* Dispatch parsing substitution to an interpretation substitution *) let subst = split_by_type ids fullargs in (* Instantiate the notation *)
instantiate_notation_constr loc intern (intern_cases_pattern_as_binder ~dump:true intern) ntnvars subst (Id.Map.empty, env) c
(**********************************************************************) (* Discriminating between bound variables and global references *)
let string_of_ty = function
| Inductive -> "ind"
| Recursive -> "def"
| Method -> "meth"
| Variable -> "var"
let gvar (loc, id) us = match us with
| None | Some ([],[]) -> DAst.make ?loc @@ GVar id
| Some _ ->
user_err ?loc (str "Variable " ++ Id.print id ++
str " cannot have a universe instance")
let intern_var env (ltacvars,ntnvars) namedctx loc id us = (* Is [id] a notation variable *) if Id.Map.mem id ntnvars then begin ifnot (Id.Map.mem id env.impls) then set_notation_var_scope ?loc id (env.tmp_scope,env.scopes) env.ntn_binding_ids ntnvars;
gvar (loc,id) us end else (* Is [id] registered with implicit arguments *) try let {var_intern_typ=ty; var_uid=uid} = Id.Map.find id env.impls in let tys = string_of_ty ty in
Dumpglob.dump_reference ?loc "<>" uid tys;
gvar (loc,id) us with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) if Id.Set.mem id env.ids || Id.Set.mem id ltacvars.ltac_vars then
gvar (loc,id) us elseif Id.equal id ldots_var (* Is [id] the special variable for recursive notations? *) thenif Id.Map.is_empty ntnvars then error_ldots_var ?loc else gvar (loc,id) us elseif Id.Set.mem id ltacvars.ltac_bound then (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
user_err ?loc
(str "variable " ++ Id.print id ++ str " should be bound to a term.") else (* Is [id] a goal or section variable *) let _ = Environ.lookup_named_ctxt id namedctx in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) letref = GlobRef.VarRef id in
Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *) (* Someday we should stop relying on Dumglob raising exceptions *)
DAst.make ?loc @@ GRef (ref, us) with e when CErrors.noncritical e -> (* [id] a goal variable *)
gvar (loc,id) us
(**********************************************************************) (* Locating reference, possibly via an abbreviation *)
let locate_reference qid =
Smartlocate.global_of_extended_global (Nametab.locate_extended qid)
let is_global id = try let _ = locate_reference (qualid_of_ident id) intrue with Not_found -> false
let dump_extended_global loc = function
| TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref
| Abbrev sp -> Dumpglob.add_glob_kn ?loc sp
let intern_extended_global_of_qualid qid = let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r
let intern_reference qid = let r = try intern_extended_global_of_qualid qid with Not_found as exn -> let _, info = Exninfo.capture exn in
Nametab.error_global_not_found ~info qid in
Smartlocate.global_of_extended_global r
let intern_sort_name ~local_univs = function
| CSProp -> GSProp
| CProp -> GProp
| CSet -> GSet
| CRawType u -> GRawUniv u
| CType qid -> let is_id = qualid_is_ident qid in let local = ifnot is_id then None else Id.Map.find_opt (qualid_basename qid) (snd local_univs.bound) in match local with
| Some u -> GUniv u
| None -> try GUniv (Univ.Level.make (Nametab.locate_universe qid)) with Not_found -> if is_id && local_univs.unb_univs then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) else
CErrors.user_err ?loc:qid.loc Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".")
let intern_qvar ~local_univs = function
| CQAnon loc -> GLocalQVar (CAst.make ?loc Anonymous)
| CRawQVar q -> GRawQVar q
| CQVar qid -> let is_id = qualid_is_ident qid in let local = ifnot is_id then None else Id.Map.find_opt (qualid_basename qid) (fst local_univs.bound) in match local with
| Some u -> GQVar u
| None -> try GQVar (Sorts.QVar.make_global (Nametab.Quality.locate qid)) with Not_found -> if is_id && local_univs.unb_univs then GLocalQVar (CAst.make ?loc:qid.loc (Name (qualid_basename qid))) else
CErrors.user_err ?loc:qid.loc Pp.(str "Undeclared quality " ++ pr_qualid qid ++ str".")
let intern_quality ~local_univs q = match q with
| CQConstant q -> GQConstant q
| CQualVar q -> GQualVar (intern_qvar ~local_univs q)
let intern_sort ~local_univs (q,l) = Option.map (intern_qvar ~local_univs) q,
map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) l
let intern_instance ~local_univs = function
| None -> None
| Some (qs, us) -> let qs = List.map (intern_quality ~local_univs) qs in let us = List.map (map_glob_sort_gen (intern_sort_name ~local_univs)) us in
Some (qs, us)
let intern_name_alias = function
| { CAst.v = CRef(qid,u) } -> let r = try Some (intern_extended_global_of_qualid qid) with Not_found -> None in Option.bind r Smartlocate.global_of_extended_global |> Option.map (fun r -> r, intern_instance ~local_univs:empty_local_univs u)
| _ -> None
let intern_field_ref qid = match
Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) |> Option.map (function
| GlobRef.ConstRef c as x -> x, Structure.find_from_projection c
| _ -> raise Not_found) with
| exception Not_found ->
Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid))
| None ->
Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid))
| Some x -> x
let find_appl_head_data env (_,ntnvars) c = let loc = c.CAst.loc in match DAst.get c with
| GVar id when not (Id.Map.mem id ntnvars) ->
(try let {var_impls=impls; var_scopes=argsc} = Id.Map.find id env.impls in
Some (CAst.make ?loc (GlobRef.VarRef id)), make_implicits_list impls, argsc with Not_found -> None, [], [])
| GRef (ref,_) -> let impls = implicits_of_global refin let scopes = find_arguments_scope refin
Some (CAst.make ?loc ref), impls, scopes
| GApp (r, l) -> beginmatch DAst.get r with
| GRef (ref,_) -> let n = List.length l in let impls = implicits_of_global refin let scopes = find_arguments_scope refin
Some (CAst.make ?loc ref),
(if n = 0 then [] elseList.map (drop_first_implicits n) impls), List.skipn_at_best n scopes
| _ -> None, [], [] end
| GProj ((cst,_), l, c) -> letref = GlobRef.ConstRef cst in let n = List.length l + 1 in let impls = implicits_of_global refin let scopes = find_arguments_scope refin
Some (CAst.make ?loc (GlobRef.ConstRef cst)), List.map (drop_first_implicits n) impls, List.skipn_at_best n scopes
| _ -> None, [], []
let error_not_enough_arguments ?loc =
user_err ?loc (str "Abbreviation is not applied enough.")
let check_no_explicitation l = let is_unset (a, b) = match b with None -> false | Some _ -> truein let l = List.filter is_unset l in match l with
| [] -> ()
| (_, None) :: _ -> assert false
| (_, Some {loc}) :: _ ->
user_err ?loc (str"Unexpected explicitation of the argument of an abbreviation.")
let find_projection_data c = match DAst.get c with
| GApp (r, l) -> beginmatch DAst.get r with
| GRef (GlobRef.ConstRef cst,us) -> Some (cst, us, l, Structure.projection_nparams cst)
| _ -> None end
| GRef (GlobRef.ConstRef cst,us) -> Some (cst, us, [], Structure.projection_nparams cst)
| _ -> None
let glob_sort_of_level (level: glob_level) : glob_sort = match level with
| UAnonymous _ as l -> None, l
| UNamed id -> None, UNamed [id, 0]
(* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in match intern_extended_global_of_qualid qid with
| TrueGlobal (GlobRef.VarRef _) when no_secvar -> (* Rule out section vars since these should have been found by intern_var *) raise Not_found
| TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), Some ref, args
| Abbrev sp -> let (ids,c) = Abbreviation.search_abbreviation sp in let nids = List.length ids in ifList.length args < nids then error_not_enough_arguments ?loc; let args1,args2 = List.chop nids args in
check_no_explicitation args1; let subst = split_by_type ids (List.map fst args1,[],[],[]) in let infos = (Id.Map.empty, env) in let c = instantiate_notation_constr loc intern (intern_cases_pattern_as_binder ~dump:true intern) ntnvars subst infos c in let loc = c.loc in let err () =
user_err ?loc (str "Notation " ++ pr_qualid qid
++ str " cannot have a universe instance,"
++ str " its expanded head does not start with a reference") in let c = match us, DAst.get c with
| None, _ -> c
| Some _, GRef (ref, None) -> DAst.make ?loc @@ GRef (ref, us)
| Some _, GApp (r, arg) -> let loc' = r.CAst.loc in beginmatch DAst.get r with
| GRef (ref, None) ->
DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
| _ -> err () end
| Some ([],[s]), GSort gs when Glob_ops.(glob_sort_eq glob_Type_sort gs) ->
DAst.make ?loc @@ GSort (glob_sort_of_level s)
| Some ([],[_old_level]), GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *)
user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)
| Some _, _ -> err () in
c, None, args2
let intern_qualid_for_pattern test_global intern_not qid pats = match Nametab.locate_extended_nowarn qid with
| TrueGlobal g as xref ->
test_global g;
Nametab.is_warned_xref xref |> Option.iter (fun warn -> Nametab.warn_user_warn_xref ?loc:qid.loc warn (TrueGlobal g));
dump_extended_global qid.loc (TrueGlobal g);
(g, false, Some [], pats)
| Abbrev kn as xref -> letfilter (vars,a) = match a with
| NRef (g,_) -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
test_global g; let () = assert (List.is_empty vars) in
Some (g, Some [], pats)
| NApp (NRef (g,_),[]) -> (* special case: abbreviation for @Cstr deactivates implicit arguments *)
test_global g; let () = assert (List.is_empty vars) in
Some (g, None, pats)
| NApp (NRef (g,_),args) -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
test_global g; let nvars = List.length vars in ifList.length pats < nvars then error_not_enough_arguments ?loc:qid.loc; let pats1,pats2 = List.chop nvars pats in let subst = split_by_type_pat vars (pats1,[],[]) in let args = List.map (intern_not subst) args in
Some (g, Some args, pats2)
| _ -> None in match Abbreviation.search_filtered_abbreviation filter kn with
| Some (g, pats1, pats2) ->
Nametab.is_warned_xref xref
|> Option.iter (fun warn -> Nametab.warn_user_warn_xref ?loc:qid.loc warn (Abbrev kn));
dump_extended_global qid.loc (Abbrev kn);
(g, true, pats1, pats2)
| None -> raise Not_found
let warn_nonprimitive_projection =
CWarnings.create ~name:"nonprimitive-projection-syntax" ~category:CWarnings.CoreCategories.syntax ~default:CWarnings.Disabled
Pp.(fun f -> pr_qualid f ++ str " used as a primitive projection but is not one.")
let error_nonprojection_syntax ?loc qid =
CErrors.user_err ?loc Pp.(pr_qualid qid ++ str" is not a projection.")
let check_applied_projection isproj realref qid = if isproj then letopen GlobRef in let is_prim = match realref with
| None | Some (IndRef _ | ConstructRef _ | VarRef _) -> false
| Some (ConstRef c) -> if PrimitiveProjections.mem c thentrue elseifStructure.is_projection c thenfalse else error_nonprojection_syntax ?loc:qid.loc qid (* TODO check projargs, note we will need implicit argument info *) in ifnot is_prim then warn_nonprimitive_projection ?loc:qid.loc qid
let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us args qid = let loc = qid.CAst.loc in let us = intern_instance ~local_univs:env.local_univs us in if qualid_is_ident qid then try let res = intern_var env lvar namedctx loc (qualid_basename qid) us in
check_applied_projection isproj None qid;
res, args with Not_found -> try let res, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
check_applied_projection isproj realref qid;
res, args2 with Not_found as exn -> (* Extra allowance for non globalizing functions *) ifOption.default true env.strict_check || List.exists (fun (_,e) -> Option.has_some e) args then let _, info = Exninfo.capture exn in
Nametab.error_global_not_found ~info qid else (* check_applied_projection ?? *)
gvar (loc,qualid_basename qid) us, args else try let res, realref, args2 = intern_qualid qid intern env ntnvars us args in
check_applied_projection isproj realref qid;
res, args2 with Not_found as exn -> let _, info = Exninfo.capture exn in
Nametab.error_global_not_found ~info qid
let interp_reference vars r = let r,_ =
intern_applied_reference ~isproj:false (fun _ -> error_not_enough_arguments ?loc:None)
{ids = Id.Set.empty; strict_check = Some true;
local_univs = empty_local_univs;(* <- doesn't matter here *)
tmp_scope = []; scopes = []; impls = empty_internalization_env;
binder_block_names = None; ntn_binding_ids = Id.Set.empty}
Environ.empty_named_context_val
(vars, Id.Map.empty) None [] r in r
(** Intermediate type common to the patterns of the "in" and of the
"with" clause of "match" *)
type'a raw_cases_pattern_expr_r =
| RCPatAlias of'a raw_cases_pattern_expr * lname
| RCPatCstr of GlobRef.t * 'a raw_cases_pattern_expr list
| RCPatAtom of (lident * (Notation_term.tmp_scope_name list * Notation_term.scope_name list)) option
| RCPatOr of'a raw_cases_pattern_expr list and'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
(** {6 Elementary bricks } *)
let apply_scope_env env = function
| [] -> {env with tmp_scope = []}, []
| sc::scl -> {env with tmp_scope = sc}, scl
let rec simple_adjust_scopes n scopes = (* Note: there can be less scopes than arguments but also more scopes *) (* than arguments because extra scopes are used in the presence of *) (* coercions to funclass *) if Int.equal n 0 then [] elsematch scopes with
| [] -> [] :: simple_adjust_scopes (n-1) []
| sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
let rec adjust_to_up l l' default = match l, l' with
| l, [] -> []
| [], l -> l
| true::l, l' -> default :: adjust_to_up l l' default
| false::l, y::l' -> y :: adjust_to_up l l' default
let rec adjust_to_down l l' default = match l, l' with
| [], l -> []
| true::l, l' -> adjust_to_down l l' default
| false::l, [] -> default :: adjust_to_down l [] default
| false::l, y::l' -> y :: adjust_to_down l l' default
let check_linearity loc ids = matchList.duplicates (fun id1 id2 -> Id.equal id1.v id2.v) ids with
| id::_ ->
Loc.raise ?loc (InternalizationError (NonLinearPattern id.v))
| [] ->
()
(* Match the number of pattern against the number of matched args *) let check_number_of_pattern loc n l = let p = List.length l in ifnot (Int.equal n p) then
Loc.raise ?loc (InternalizationError (BadPatternsNumber (n,p)))
let check_or_pat_variables loc ids idsl = let eq_id {v=id} {v=id'} = Id.equal id id'in (* Collect remaining patterns which do not have the same variables as the first pattern *) let idsl = List.filter (fun ids' -> not (List.eq_set eq_id ids ids')) idsl in match idsl with
| ids'::_ -> (* Look for an [id] which is either in [ids] and not in [ids'] or in [ids'] and not in [ids] *) let ids'' = List.subtract eq_id ids ids' in let ids'' = if ids'' = [] thenList.subtract eq_id ids' ids else ids'' in
user_err ?loc
(strbrk "The components of this disjunctive pattern must bind the same variables (" ++
Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).")
| [] -> ()
let error_wrong_numarg ?loc g ~expanded ~nargs ~expected_nassums ~expected_ndecls = let env = Global.env() in match g with
| GlobRef.ConstructRef cstr -> error_wrong_numarg_constructor ?loc env ~cstr ~expanded ~nargs ~expected_nassums ~expected_ndecls
| GlobRef.IndRef ind -> error_wrong_numarg_inductive ?loc env ~ind ~expanded ~nargs ~expected_nassums ~expected_ndecls
| _ -> assert false
let error_wrong_numarg_with_notation_patterns ?loc g nargs tags =
error_wrong_numarg ?loc g ~expanded:true ~nargs
~expected_nassums:(List.count (fun x -> not x) tags)
~expected_ndecls:(List.length tags)
let check_has_letin ?loc g expanded nargs nimps tags = let expected_ndecls = List.length tags - nimps in let expected_nassums = List.count (fun x -> not x) tags - nimps in if nargs = expected_nassums thenfalse elseif nargs = expected_ndecls thentrueelse
error_wrong_numarg ?loc g ~expanded ~nargs ~expected_nassums ~expected_ndecls
(** Do not raise NotEnoughArguments thanks to preconditions*) let chop_params_pattern loc ind args with_letin = let nparams = if with_letin then Inductiveops.inductive_nparamdecls (Global.env()) ind else Inductiveops.inductive_nparams (Global.env()) ind in
assert (nparams <= List.length args); let params,args = List.chop nparams args in List.iter (fun c -> match DAst.get c with
| PatVar Anonymous -> ()
| PatVar _ | PatCstr(_,_,_) -> error_parameter_not_implicit ?loc:c.CAst.loc) params;
args
let find_constructor_head ?loc ref = letopen GlobRef in matchrefwith
| ConstructRef cstr -> cstr
| IndRef _ -> let error = str "There is an inductive name deep in a \"in\" clause."in
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.13 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.
