aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml4
-rw-r--r--interp/constrexpr_ops.ml10
-rw-r--r--interp/constrextern.ml22
-rw-r--r--interp/constrintern.ml237
-rw-r--r--interp/constrintern.mli6
-rw-r--r--interp/implicit_quantifiers.ml57
-rw-r--r--interp/notation.ml655
-rw-r--r--interp/notation.mli66
-rw-r--r--interp/notation_ops.ml37
-rw-r--r--interp/numTok.mli30
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/smartlocate.ml38
-rw-r--r--interp/smartlocate.mli12
-rw-r--r--interp/stdarg.ml6
-rw-r--r--interp/stdarg.mli3
-rw-r--r--interp/syntax_def.ml6
-rw-r--r--interp/syntax_def.mli2
17 files changed, 806 insertions, 387 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index c98e05370e..235310660b 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -58,7 +58,7 @@ type abstraction_kind = AbsLambda | AbsPi
type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
type prim_token =
- | Numeral of NumTok.Signed.t
+ | Number of NumTok.Signed.t
| String of string
type instance_expr = Glob_term.glob_level list
@@ -108,7 +108,7 @@ and constr_expr_r =
* constr_expr * constr_expr
| CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
| CPatVar of Pattern.patvar
- | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list
+ | CEvar of Glob_term.existential_name CAst.t * (lident * constr_expr) list
| CSort of Glob_term.glob_sort
| CCast of constr_expr * constr_expr Glob_term.cast_type
| CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index ce8e7d3c2c..8cc63c5d03 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -44,13 +44,13 @@ let names_of_local_binders bl =
(**********************************************************************)
(* Functions on constr_expr *)
-(* Note: redundant Numeral representations, such as -0 and +0 (and others),
+(* Note: redundant Number representations, such as -0 and +0 (and others),
are considered different here. *)
let prim_token_eq t1 t2 = match t1, t2 with
-| Numeral n1, Numeral n2 -> NumTok.Signed.equal n1 n2
+| Number n1, Number n2 -> NumTok.Signed.equal n1 n2
| String s1, String s2 -> String.equal s1 s2
-| (Numeral _ | String _), _ -> false
+| (Number _ | String _), _ -> false
let explicitation_eq ex1 ex2 = match ex1, ex2 with
| ExplByPos (i1, id1), ExplByPos (i2, id2) ->
@@ -156,7 +156,7 @@ let rec constr_expr_eq e1 e2 =
| CPatVar i1, CPatVar i2 ->
Id.equal i1 i2
| CEvar (id1, c1), CEvar (id2, c2) ->
- Id.equal id1 id2 && List.equal instance_eq c1 c2
+ Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2
| CSort s1, CSort s2 ->
Glob_ops.glob_sort_eq s1 s2
| CCast(t1,c1), CCast(t2,c2) ->
@@ -235,7 +235,7 @@ and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
List.equal (List.equal local_binder_eq) bl1 bl2
and instance_eq (x1,c1) (x2,c2) =
- Id.equal x1 x2 && constr_expr_eq c1 c2
+ Id.equal x1.CAst.v x2.CAst.v && constr_expr_eq c1 c2
and cast_expr_eq c1 c2 = match c1, c2 with
| CastConv t1, CastConv t2
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 43fef8685d..d1bec16a3f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -357,18 +357,18 @@ let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
let make_notation_gen loc ntn mknot mkprim destprim l bl =
match snd ntn,List.map destprim l with
(* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
- | "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) ->
+ | "- _", [Some (Number p)] when not (NumTok.Signed.is_zero p) ->
assert (bl=[]);
mknot (loc,ntn,([mknot (loc,(InConstrEntry,"( _ )"),l,[])]),[])
| _ ->
match decompose_notation_key ntn, l with
| (InConstrEntry,[Terminal "-"; Terminal x]), [] ->
begin match NumTok.Unsigned.parse_string x with
- | Some n -> mkprim (loc, Numeral (NumTok.SMinus,n))
+ | Some n -> mkprim (loc, Number (NumTok.SMinus,n))
| None -> mknot (loc,ntn,l,bl) end
| (InConstrEntry,[Terminal x]), [] ->
begin match NumTok.Unsigned.parse_string x with
- | Some n -> mkprim (loc, Numeral (NumTok.SPlus,n))
+ | Some n -> mkprim (loc, Number (NumTok.SPlus,n))
| None -> mknot (loc,ntn,l,bl) end
| _ -> mknot (loc,ntn,l,bl)
@@ -551,7 +551,7 @@ and extern_notation_pattern allscopes vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
try
- if is_inactive_rule keyrule then raise No_match;
+ if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match;
let loc = t.loc in
match DAst.get t with
| PatCstr (cstr,args,na) ->
@@ -568,7 +568,7 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
try
- if is_inactive_rule keyrule then raise No_match;
+ if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match;
apply_notation_to_pattern (GlobRef.IndRef ind)
(match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
with
@@ -915,7 +915,7 @@ let extern_float f scopes =
let hex = !Flags.raw_print || not (get_printing_float ()) in
if hex then Float64.to_hex_string f else Float64.to_string f in
let n = NumTok.Signed.of_string s in
- extern_prim_token_delimiter_if_required (Numeral n)
+ extern_prim_token_delimiter_if_required (Number n)
"float" "float_scope" scopes
(**********************************************************************)
@@ -978,7 +978,7 @@ let rec extern inctx ?impargs scopes vars r =
if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else
(match kind with
| Evar_kinds.SecondOrderPatVar n -> CPatVar n
- | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[]))
+ | Evar_kinds.FirstOrderPatVar n -> CEvar (CAst.make n,[]))
| GApp (f,args) ->
(match DAst.get f with
@@ -1097,13 +1097,13 @@ let rec extern inctx ?impargs scopes vars r =
| GInt i ->
extern_prim_token_delimiter_if_required
- (Numeral (NumTok.Signed.of_int_string (Uint63.to_string i)))
+ (Number (NumTok.Signed.of_int_string (Uint63.to_string i)))
"int63" "int63_scope" (snd scopes)
| GFloat f -> extern_float f (snd scopes)
| GArray(u,t,def,ty) ->
- CArray(u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty)
+ CArray(extern_universes u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty)
in insert_entry_coercion coercion (CAst.make ?loc c)
@@ -1238,7 +1238,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
| (keyrule,pat,n as _rule)::rules ->
let loc = Glob_ops.loc_of_glob_constr t in
try
- if is_inactive_rule keyrule then raise No_match;
+ if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match;
let f,args =
match DAst.get t with
| GApp (f,args) -> f,args
@@ -1391,7 +1391,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| None -> Id.of_string "__"
| Some id -> id
in
- GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l)
+ GEvar (CAst.make id,List.map (fun (id,c) -> (CAst.make id, glob_of_pat avoid env sigma c)) l)
| PRel n ->
let id = try match lookup_name_of_rel n env with
| Name id -> id
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 48fb4a4a5d..ecf2b951a2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -263,6 +263,13 @@ type intern_env = {
binder_block_names: (abstraction_kind option (* None = unknown *) * Id.Set.t) option;
}
+type pattern_intern_env = {
+ pat_scopes: Notation_term.subscopes;
+ (* ids = Some means accept local variables; this is useful for
+ terms as patterns parsed as pattersn in notations *)
+ pat_ids: Id.Set.t option;
+}
+
(**********************************************************************)
(* Remembering the parsing scope of variables in notations *)
@@ -317,6 +324,9 @@ let reset_tmp_scope env = {env with tmp_scope = None}
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, bk, t, body)
let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
@@ -420,6 +430,40 @@ let binder_status_fun = {
slide = on_snd slide_binders;
}
+(* [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
@@ -539,9 +583,9 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) =
(push_name_env ntnvars impls env locna,
(na,Explicit,term,ty))
-let intern_cases_pattern_as_binder ?loc ntnvars env p =
+let intern_cases_pattern_as_binder ?loc test_kind ntnvars env p =
let il,disjpat =
- let (il, subst_disjpat) = !intern_cases_pattern_fwd ntnvars (None,env.scopes) p in
+ let (il, subst_disjpat) = !intern_cases_pattern_fwd test_kind ntnvars (env_for_pattern (reset_tmp_scope env)) p in
let substl,disjpat = List.split subst_disjpat in
if not (List.for_all (fun subst -> Id.Map.equal Id.equal subst Id.Map.empty) substl) then
user_err ?loc (str "Unsupported nested \"as\" clause.");
@@ -568,7 +612,7 @@ let intern_local_binder_aux intern ntnvars (env,bl) = function
| Some ty -> ty
| None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None)
in
- let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in
+ let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc test_kind_tolerant ntnvars env p in
let bk = Default Explicit in
let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in
let {v=(_,bk,t)} = List.hd bl' in
@@ -661,27 +705,21 @@ let is_patvar_store store pat =
| PatVar na -> ignore(store na); true
| _ -> false
-let out_patvar pat =
- match pat.v with
+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 term_of_name = function
- | Name id -> DAst.make (GVar id)
- | Anonymous ->
- let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
- DAst.make (GHole (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st }, IntroAnonymous, None))
+ | _ -> assert false)
let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
| Anonymous -> (renaming,env), None, Anonymous
| Name id ->
let store,get = set_temporary_memory () in
+ 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,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+ let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in
let pat, na = match disjpat with
| [pat] when is_patvar_store store pat -> let na = get () in None, na
| _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
@@ -694,11 +732,11 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
if onlyident then
(* Do not try to interpret a variable as a constructor *)
let na = out_patvar pat in
- let env = push_name_env ntnvars [] env (make ?loc:pat.loc na) in
- (renaming,env), None, na
+ let env = push_name_env ntnvars [] env na in
+ (renaming,env), None, na.v
else
(* Interpret as a pattern *)
- let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+ let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in
let pat, na =
match disjpat with
| [pat] when is_patvar_store store pat -> let na = get () in None, na
@@ -829,22 +867,22 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let arg = match arg with
| None -> None
| Some arg ->
- let mk_env id (c, (tmp_scope, subscopes)) map =
- let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
+ let mk_env id (c, scopes) map =
+ let nenv = set_env_scopes env scopes in
try
let gc = intern nenv c in
Id.Map.add id (gc, None) map
with Nametab.GlobalizationError _ -> map
in
- let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
- let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
- if onlyident then
- let na = out_patvar c in term_of_name na, None
- else
- let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
- match disjpat with
- | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None)
- | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
+ let mk_env' (c, (onlyident,scopes)) =
+ let nenv = 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 _,((disjpat,_),_),_ = intern_pat test_kind ntnvars nenv c in
+ match disjpat with
+ | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None)
+ | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
in
let terms = Id.Map.fold mk_env terms Id.Map.empty in
let binders = Id.Map.map mk_env' binders in
@@ -890,20 +928,19 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
try
- let (a,(scopt,subscopes)) = Id.Map.find id terms in
- intern {env with tmp_scope = scopt;
- scopes = subscopes @ env.scopes} a
+ let (a,scopes) = Id.Map.find id terms in
+ intern (set_env_scopes env scopes) a
with Not_found ->
try
let pat,(onlyident,scopes) = Id.Map.find id binders in
- let env = set_env_scopes env scopes in
- if onlyident then
- term_of_name (out_patvar pat)
- else
- let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
- match disjpat with
- | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat
- | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
+ let nenv = 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),na = intern_pat test_kind ntnvars nenv pat in
+ 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
@@ -1570,11 +1607,11 @@ let rec subst_pat_iterator y t = DAst.(map (function
| RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
let is_non_zero c = match c with
-| { CAst.v = CPrim (Numeral p) } -> not (NumTok.Signed.is_zero p)
+| { CAst.v = CPrim (Number p) } -> not (NumTok.Signed.is_zero p)
| _ -> false
let is_non_zero_pat c = match c with
-| { CAst.v = CPatPrim (Numeral p) } -> not (NumTok.Signed.is_zero p)
+| { CAst.v = CPatPrim (Number p) } -> not (NumTok.Signed.is_zero p)
| _ -> false
let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
@@ -1582,19 +1619,14 @@ let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
~key:["Asymmetric";"Patterns"]
~value:false
-let drop_notations_pattern looked_for genv =
+let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
(* At toplevel, Constructors and Inductives are accepted, in recursive calls
only constructor are allowed *)
- let ensure_kind top loc g =
- try
- if top then looked_for g else
- match g with GlobRef.ConstructRef _ -> () | _ -> raise Not_found
+ let ensure_kind test_kind ?loc g =
+ try test_kind ?loc g
with Not_found ->
error_invalid_pattern_notation ?loc ()
in
- let test_kind top =
- if top then looked_for else function GlobRef.ConstructRef _ -> () | _ -> raise Not_found
- in
(* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
let rec rcp_of_glob scopes x = DAst.(map (function
| GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes))
@@ -1611,47 +1643,49 @@ let drop_notations_pattern looked_for genv =
end
| _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x
in
- let rec drop_syndef top scopes qid pats =
+ let rec drop_syndef test_kind ?loc scopes qid pats =
try
+ if qualid_is_ident qid && Option.cata (Id.Set.mem (qualid_basename qid)) false env.pat_ids then
+ raise Not_found;
match Nametab.locate_extended qid with
| SynDef sp ->
let filter (vars,a) =
try match a with
| NRef g ->
(* Convention: do not deactivate implicit arguments and scopes for further arguments *)
- test_kind top g;
+ test_kind ?loc g;
let () = assert (List.is_empty vars) in
let (_,argscs) = find_remaining_scopes [] pats g in
Some (g, [], List.map2 (in_pat_sc scopes) argscs pats)
| NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
- test_kind top g;
+ test_kind ?loc g;
let () = assert (List.is_empty vars) in
let (_,argscs) = find_remaining_scopes [] pats g in
Some (g, List.map2 (in_pat_sc scopes) argscs pats, [])
| NApp (NRef g,args) ->
(* Convention: do not deactivate implicit arguments and scopes for further arguments *)
- test_kind top g;
+ test_kind ?loc g;
let nvars = List.length vars in
if List.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 idspl1 = List.map (in_not false qid.loc scopes subst []) args in
+ let idspl1 = List.map (in_not test_kind_inner qid.loc scopes subst []) args in
let (_,argscs) = find_remaining_scopes pats1 pats2 g in
Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
| _ -> raise Not_found
with Not_found -> None in
Syntax_def.search_filtered_syntactic_definition filter sp
| TrueGlobal g ->
- test_kind top g;
+ test_kind ?loc g;
Dumpglob.add_glob ?loc:qid.loc g;
let (_,argscs) = find_remaining_scopes [] pats g in
Some (g,[],List.map2 (in_pat_sc scopes) argscs pats)
with Not_found -> None
- and in_pat top scopes pt =
+ and in_pat test_kind scopes pt =
let open CAst in
let loc = pt.loc in
match pt.v with
- | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id)
+ | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat test_kind scopes p, id)
| CPatRecord l ->
let sorted_fields =
sort_fields ~complete:false loc l (fun _idx fieldname constructor -> CAst.make ?loc @@ CPatAtom None) in
@@ -1668,7 +1702,7 @@ let drop_notations_pattern looked_for genv =
end
| CPatCstr (head, None, pl) ->
begin
- match drop_syndef top scopes head pl with
+ match drop_syndef test_kind ?loc scopes head pl with
| Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
| None -> Loc.raise ?loc (InternalizationError (NotAConstructor head))
end
@@ -1682,37 +1716,37 @@ let drop_notations_pattern looked_for genv =
in
if expl_pl == [] then
(* Convention: (@r) deactivates all further implicit arguments and scopes *)
- DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
+ DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat test_kind_inner scopes) pl, [])
else
(* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
(* but not scopes in expl_pl *)
let (argscs1,_) = find_remaining_scopes expl_pl pl g in
- DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
+ DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat test_kind_inner scopes) pl, [])
| CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a ->
- let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in
- let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in
+ let p = match a.CAst.v with CPatPrim (Number (_, p)) -> p | _ -> assert false in
+ let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind test_kind_inner) (Number (SMinus,p)) scopes in
rcp_of_glob scopes pat
| CPatNotation (_,(InConstrEntry,"( _ )"),([a],[]),[]) ->
- in_pat top scopes a
+ in_pat test_kind scopes a
| CPatNotation (_,ntn,fullargs,extrargs) ->
let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in
- let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in
+ let subst = split_by_type_pat ?loc ids' (terms,termlists) in
Dumpglob.dump_notation_location (patntn_loc ?loc fullargs ntn) ntn df;
- in_not top loc scopes (terms,termlists) extrargs c
+ in_not test_kind loc scopes subst extrargs c
| CPatDelimiters (key, e) ->
- in_pat top (None,find_delimiters_scope ?loc key::snd scopes) e
+ in_pat test_kind (None,find_delimiters_scope ?loc key::snd scopes) e
| CPatPrim p ->
- let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes in
+ let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc test_kind_inner p scopes in
rcp_of_glob scopes pat
| CPatAtom (Some id) ->
begin
- match drop_syndef top scopes id [] with
+ match drop_syndef test_kind ?loc scopes id [] with
| Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c)
| None -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes))
end
| CPatAtom None -> DAst.make ?loc @@ RCPatAtom None
- | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
+ | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat test_kind scopes) pl)
| CPatCast (_,_) ->
(* We raise an error if the pattern contains a cast, due to
current restrictions on casts in patterns. Cast in patterns
@@ -1725,8 +1759,8 @@ let drop_notations_pattern looked_for genv =
This check is here and not in the parser because it would require
duplicating the levels of the [pattern] rule. *)
CErrors.user_err ?loc (Pp.strbrk "Casts are not supported in this pattern.")
- and in_pat_sc scopes x = in_pat false (x,snd scopes)
- and in_not top loc scopes (subst,substlist as fullsubst) args = function
+ and in_pat_sc scopes x = in_pat test_kind_inner (x,snd scopes)
+ and in_not (test_kind:?loc:Loc.t->'a->'b) loc scopes (subst,substlist as fullsubst) args = function
| NVar id ->
let () = assert (List.is_empty args) in
begin
@@ -1734,21 +1768,21 @@ let drop_notations_pattern looked_for genv =
(* of the notations *)
try
let (a,(scopt,subscopes)) = Id.Map.find id subst in
- in_pat top (scopt,subscopes@snd scopes) a
+ in_pat test_kind (scopt,subscopes@snd scopes) a
with Not_found ->
if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((make ?loc id),scopes)) else
anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".")
end
| NRef g ->
- ensure_kind top loc g;
+ ensure_kind test_kind ?loc g;
let (_,argscs) = find_remaining_scopes [] args g in
DAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
| NApp (NRef g,pl) ->
- ensure_kind top loc g;
+ ensure_kind test_kind ?loc g;
let (argscs1,argscs2) = find_remaining_scopes pl args g in
- let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in
+ let pl = List.map2 (fun x -> in_not test_kind_inner loc (x,snd scopes) fullsubst []) argscs1 pl in
let pl = add_local_defs_and_check_length loc genv g pl args in
- let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 args in
+ let args = List.map2 (fun x -> in_pat test_kind_inner (x,snd scopes)) argscs2 args in
let pat =
if List.length pl = 0 then
(* Convention: if notation is @f, encoded as NApp(Nref g,[]), then
@@ -1763,10 +1797,10 @@ let drop_notations_pattern looked_for genv =
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (l,(scopt,subscopes)) = Id.Map.find x substlist in
- let termin = in_not top loc scopes fullsubst [] terminator in
+ let termin = in_not test_kind_inner loc scopes fullsubst [] terminator in
List.fold_right (fun a t ->
let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in
- let u = in_not false loc scopes (nsubst, substlist) [] iter in
+ let u = in_not test_kind_inner loc scopes (nsubst, substlist) [] iter in
subst_pat_iterator ldots_var t u)
(if revert then List.rev l else l) termin
with Not_found ->
@@ -1775,7 +1809,7 @@ let drop_notations_pattern looked_for genv =
let () = assert (List.is_empty args) in
DAst.make ?loc @@ RCPatAtom None
| t -> error_invalid_pattern_notation ?loc ()
- in in_pat true
+ in in_pat test_kind_top env.pat_scopes pat
let rec intern_pat genv ntnvars aliases pat =
let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 =
@@ -1816,19 +1850,30 @@ let rec intern_pat genv ntnvars aliases pat =
check_or_pat_variables loc ids (List.tl idsl);
(ids,List.flatten pl')
-let intern_cases_pattern genv ntnvars scopes aliases pat =
+let intern_cases_pattern test_kind genv ntnvars env aliases pat =
intern_pat genv ntnvars aliases
- (drop_notations_pattern (function GlobRef.ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat)
+ (drop_notations_pattern (test_kind,test_kind) genv env pat)
let _ =
intern_cases_pattern_fwd :=
- fun ntnvars scopes p -> intern_cases_pattern (Global.env ()) ntnvars scopes empty_alias p
-
-let intern_ind_pattern genv ntnvars scopes pat =
+ fun test_kind ntnvars env p ->
+ intern_cases_pattern test_kind (Global.env ()) ntnvars env empty_alias p
+
+let intern_ind_pattern genv ntnvars env pat =
+ let test_kind_top ?loc = function
+ | GlobRef.IndRef _ -> ()
+ | GlobRef.ConstructRef _ | GlobRef.ConstRef _ | GlobRef.VarRef _ ->
+ (* A non-inductive global reference at top is an error *)
+ error_invalid_pattern_notation ?loc () in
+ let test_kind_inner ?loc = function
+ | GlobRef.ConstructRef _ -> ()
+ | GlobRef.IndRef _ | GlobRef.ConstRef _ | GlobRef.VarRef _ ->
+ (* A non-constructor global reference deep in a pattern is seen as a variable *)
+ raise Not_found in
let no_not =
try
- drop_notations_pattern (function (GlobRef.IndRef _ | GlobRef.ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
- with InternalizationError(NotAConstructor _) as exn ->
+ drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat
+ with InternalizationError (NotAConstructor _) as exn ->
let _, info = Exninfo.capture exn in
error_bad_inductive_type ~info ()
in
@@ -2006,8 +2051,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
GLetIn (na.CAst.v, inc1, int,
intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
| CNotation (_,(InConstrEntry,"- _"), ([a],[],[],[])) when is_non_zero a ->
- let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
- intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
+ let p = match a.CAst.v with CPrim (Number (_, p)) -> p | _ -> assert false in
+ intern env (CAst.make ?loc @@ CPrim (Number (SMinus,p)))
| CNotation (_,(InConstrEntry,"( _ )"),([a],[],[],[])) -> intern env a
| CNotation (_,ntn,args) ->
let c = intern_notation intern env ntnvars loc ntn args in
@@ -2188,7 +2233,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
GPatVar (Evar_kinds.SecondOrderPatVar n)
| CEvar (n, []) when pattern_mode ->
DAst.make ?loc @@
- GPatVar (Evar_kinds.FirstOrderPatVar n)
+ GPatVar (Evar_kinds.FirstOrderPatVar n.CAst.v)
(* end *)
(* Parsing existential variables *)
| CEvar (n, l) ->
@@ -2221,7 +2266,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(* Expands a multiple pattern into a disjunction of multiple patterns *)
and intern_multiple_pattern env n pl =
- let idsl_pll = List.map (intern_cases_pattern globalenv ntnvars (None,env.scopes) empty_alias) pl in
+ let env = { pat_ids = None; pat_scopes = (None,env.scopes) } in
+ let idsl_pll = List.map (intern_cases_pattern test_kind_tolerant globalenv ntnvars env empty_alias) pl in
let loc = loc_of_multiple_pattern pl in
check_number_of_pattern loc n pl;
product_of_cases_patterns empty_alias idsl_pll
@@ -2262,7 +2308,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let match_td,typ = match t with
| Some t ->
let with_letin,(ind,ind_ids,alias_subst,l) =
- intern_ind_pattern globalenv ntnvars (None,env.scopes) t in
+ intern_ind_pattern globalenv ntnvars (env_for_pattern (set_type_scope env)) t in
let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in
let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in
(* for "in Vect n", we answer (["n","n"],[(loc,"n")])
@@ -2403,7 +2449,8 @@ let intern_gen kind env sigma
let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
let intern_type env sigma c = intern_gen IsType env sigma c
let intern_pattern globalenv patt =
- intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
+ let env = {pat_ids = None; pat_scopes = (None, [])} in
+ intern_cases_pattern test_kind_tolerant globalenv Id.Map.empty env empty_alias patt
(*********************************************************************)
(* Functions to parse and interpret constructions *)
@@ -2471,6 +2518,14 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
~pattern_mode:true ~ltacvars env sigma c in
pattern_of_glob_constr c
+let interp_constr_pattern env sigma ?(expected_type=WithoutTypeConstraint) c =
+ let c = intern_gen expected_type ~pattern_mode:true env sigma c in
+ let flags = { Pretyping.no_classes_no_fail_inference_flags with expand_evars = false } in
+ let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
+ (* FIXME: it is necessary to be unsafe here because of the way we handle
+ evars in the pretyper. Sometimes they get solved eagerly. *)
+ pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
+
let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
{ Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
let tmp_scope = scope_of_type_kind env sigma kind in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 898a3e09c8..11d756803f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -136,10 +136,16 @@ val interp_type_evars_impls : ?flags:inference_flags -> env -> evar_map ->
(** Interprets constr patterns *)
+(** Without typing *)
val intern_constr_pattern :
env -> evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign ->
constr_pattern_expr -> patvar list * constr_pattern
+(** With typing *)
+val interp_constr_pattern :
+ env -> evar_map -> ?expected_type:typing_constraint ->
+ constr_pattern_expr -> constr_pattern
+
(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
val intern_reference : qualid -> GlobRef.t
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4016a3600e..ee07fb6ed1 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -114,23 +114,32 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
ungeneralizable loc id) vars;
vars
-let rec make_fresh ids env x =
- if is_freevar ids env x then x else make_fresh ids env (Nameops.increment_subscript x)
+let make_fresh ids env x =
+ Namegen.next_ident_away_from x (fun x -> not (is_freevar ids env x))
let next_name_away_from na avoid =
match na with
| Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon")
| Name id -> make_fresh avoid (Global.env ()) id
+let rec is_class_arg c =
+ let open Constr in
+ match kind c with
+ | Prod (_,_,c)
+ | Cast (c,_,_)
+ | LetIn (_,_,_,c) -> is_class_arg c
+ | _ ->
+ let c, _ = decompose_appvect c in
+ match destRef c with
+ | exception DestKO -> false
+ | r, _ -> is_class r
+
let combine_params avoid applied needed =
let named, applied =
List.partition
(function
(t, Some {CAst.loc;v=ExplByName id}) ->
- let is_id (_, decl) = match RelDecl.get_name decl with
- | Name id' -> Id.equal id id'
- | Anonymous -> false
- in
+ let is_id decl = Name.equal (Name id) (RelDecl.get_name decl) in
if not (List.exists is_id needed) then
user_err ?loc (str "Wrong argument name: " ++ Id.print id);
true
@@ -141,27 +150,27 @@ let combine_params avoid applied needed =
named
in
let rec aux ids avoid app need =
- match app, need with
-
- | _, (_, LocalDef _) :: need -> aux ids avoid app need
-
- | [], [] -> List.rev ids, avoid
+ match need with
+ | [] -> begin match app with
+ | [] -> List.rev ids, avoid
+ | (x, _) :: _ -> user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
+ end
- | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named ->
- aux (Id.List.assoc id named :: ids) avoid app need
+ | LocalDef _ :: need -> aux ids avoid app need
- | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need ->
- aux (x :: ids) avoid app need
- | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
+ | LocalAssum ({binder_name=Name id}, _) :: need when Id.List.mem_assoc id named ->
+ aux (Id.List.assoc id named :: ids) avoid app need
- | _, (Some _, decl) :: need | [], (None, decl) :: need ->
- let id' = next_name_away_from (RelDecl.get_name decl) avoid in
- let t' = CAst.make @@ CRef (qualid_of_ident id',None) in
- aux (t' :: ids) (Id.Set.add id' avoid) app need
+ | decl :: need ->
+ begin match app, is_class_arg (get_type decl) with
+ | (x, _) :: app, false -> aux (x :: ids) avoid app need
- | (x,_) :: _, [] ->
- user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
+ | [], false | _, true ->
+ let id' = next_name_away_from (RelDecl.get_name decl) avoid in
+ let t' = CAst.make @@ CRef (qualid_of_ident id',None) in
+ aux (t' :: ids) (Id.Set.add id' avoid) app need
+ end
in
aux [] avoid applied needed
@@ -190,9 +199,7 @@ let implicit_application env ty =
let env = Global.env () in
let sigma = Evd.from_env env in
let c = class_info env sigma gr in
- let (ci, rd) = c.cl_context in
- let pars = List.rev (List.combine ci rd) in
- let args, avoid = combine_params avoid par pars in
+ let args, avoid = combine_params avoid par (List.rev c.cl_context) in
CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
let warn_ignoring_implicit_status =
diff --git a/interp/notation.ml b/interp/notation.ml
index 7e90e15b72..8d05fab63c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -32,7 +32,7 @@ open NumTok
fail if a number has no interpretation in the scope (e.g. there is
no interpretation for negative numbers in [nat]); interpreters both for
terms and patterns can be set; these interpreters are in permanent table
- [numeral_interpreter_tab]
+ [number_interpreter_tab]
- a set of ML printers for expressions denoting numbers parsable in
this scope
- a set of interpretations for infix (more generally distfix) notations
@@ -58,6 +58,31 @@ let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2
let notation_eq (from1,ntn1) (from2,ntn2) =
notation_entry_eq from1 from2 && String.equal ntn1 ntn2
+let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
+
+let notation_binder_source_eq s1 s2 = match s1, s2 with
+| NtnParsedAsIdent, NtnParsedAsIdent -> true
+| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
+| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
+| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
+
+let ntpe_eq t1 t2 = match t1, t2 with
+| NtnTypeConstr, NtnTypeConstr -> true
+| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2
+| NtnTypeConstrList, NtnTypeConstrList -> true
+| NtnTypeBinderList, NtnTypeBinderList -> true
+| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
+
+let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) =
+ notation_entry_level_eq entry1 entry2 &&
+ pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
+ ntpe_eq tp1 tp2
+
+let interpretation_eq (vars1, t1 as x1) (vars2, t2 as x2) =
+ x1 == x2 ||
+ List.equal var_attributes_eq vars1 vars2 &&
+ Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
+
let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntry -> mt () | InCustomEntry s -> str " in custom " ++ str s
module NotationOrd =
@@ -90,8 +115,21 @@ type notation_data = {
not_deprecation : Deprecation.t option;
}
+type activation = bool
+
+type extra_printing_notation_data =
+ (activation * notation_data) list
+
+type parsing_notation_data =
+ | NoParsingData
+ | OnlyParsingData of activation * notation_data
+ | ParsingAndPrintingData of
+ activation (* for parsing*) *
+ activation (* for printing *) *
+ notation_data (* common data for both *)
+
type scope = {
- notations: notation_data NotationMap.t;
+ notations: (parsing_notation_data * extra_printing_notation_data) NotationMap.t;
delimiters: delimiters option
}
@@ -285,7 +323,7 @@ type key =
| Oth
let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.CanOrd.compare gr1 gr2
| RefKey _, Oth -> -1
| Oth, RefKey _ -> 1
| Oth, Oth -> 0
@@ -300,16 +338,30 @@ type notation_applicative_status =
type notation_rule = interp_rule * interpretation * notation_applicative_status
+let notation_rule_eq (rule1,pat1,s1 as x1) (rule2,pat2,s2 as x2) =
+ x1 == x2 || (rule1 = rule2 && interpretation_eq pat1 pat2 && s1 = s2)
+
+let also_cases_notation_rule_eq (also_cases1,rule1) (also_cases2,rule2) =
+ (* No need in principle to compare also_cases as it is inferred *)
+ also_cases1 = also_cases2 && notation_rule_eq rule1 rule2
+
let keymap_add key interp map =
let old = try KeyMap.find key map with Not_found -> [] in
+ (* In case of re-import, no need to keep the previous copy *)
+ let old = try List.remove_first (also_cases_notation_rule_eq interp) old with Not_found -> old in
KeyMap.add key (interp :: old) map
+let keymap_remove key interp map =
+ let old = try KeyMap.find key map with Not_found -> [] in
+ KeyMap.add key (List.remove_first (also_cases_notation_rule_eq interp) old) map
+
let keymap_find key map =
try KeyMap.find key map
with Not_found -> []
(* Scopes table : interpretation -> scope_name *)
-let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
+(* Boolean = for cases pattern also *)
+let notations_key_table = ref (KeyMap.empty : (bool * notation_rule) list KeyMap.t)
let glob_prim_constr_key c = match DAst.get c with
| GRef (ref, _) -> Some (canonical_gr ref)
@@ -399,13 +451,13 @@ module InnerPrimToken = struct
let do_interp ?loc interp primtok =
match primtok, interp with
- | Numeral n, RawNumInterp interp -> interp ?loc n
- | Numeral n, BigNumInterp interp ->
+ | Number n, RawNumInterp interp -> interp ?loc n
+ | Number n, BigNumInterp interp ->
(match NumTok.Signed.to_bigint n with
| Some n -> interp ?loc n
| None -> raise Not_found)
| String s, StringInterp interp -> interp ?loc s
- | (Numeral _ | String _),
+ | (Number _ | String _),
(RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found
type uninterpreter =
@@ -419,16 +471,16 @@ module InnerPrimToken = struct
| StringUninterp f, StringUninterp f' -> f == f'
| _ -> false
- let mkNumeral n =
- Numeral (NumTok.Signed.of_bigint CDec n)
+ let mkNumber n =
+ Number (NumTok.Signed.of_bigint CDec n)
let mkString = function
| None -> None
| Some s -> if Unicode.is_utf8 s then Some (String s) else None
let do_uninterp uninterp g = match uninterp with
- | RawNumUninterp u -> Option.map (fun (s,n) -> Numeral (s,n)) (u g)
- | BigNumUninterp u -> Option.map mkNumeral (u g)
+ | RawNumUninterp u -> Option.map (fun (s,n) -> Number (s,n)) (u g)
+ | BigNumUninterp u -> Option.map mkNumber (u g)
| StringUninterp u -> mkString (u g)
end
@@ -448,7 +500,7 @@ let prim_token_uninterpreters =
(Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t)
(*******************************************************)
-(* Numeral notation interpretation *)
+(* Number notation interpretation *)
type prim_token_notation_error =
| UnexpectedTerm of Constr.t
| UnexpectedNonOptionTerm of Constr.t
@@ -472,21 +524,21 @@ type z_pos_ty =
{ z_ty : Names.inductive;
pos_ty : Names.inductive }
-type numeral_ty =
+type number_ty =
{ int : int_ty;
decimal : Names.inductive;
hexadecimal : Names.inductive;
- numeral : Names.inductive }
+ number : Names.inductive }
type target_kind =
- | Int of int_ty (* Coq.Init.Numeral.int + uint *)
- | UInt of int_ty (* Coq.Init.Numeral.uint *)
+ | Int of int_ty (* Coq.Init.Number.int + uint *)
+ | UInt of int_ty (* Coq.Init.Number.uint *)
| Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
| Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
- | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *)
+ | Number of number_ty (* Coq.Init.Number.number + uint + int *)
| DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
| DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
- | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
+ | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
type string_target_kind =
| ListByte
@@ -495,19 +547,36 @@ type string_target_kind =
type option_kind = Option | Direct
type 'target conversion_kind = 'target * option_kind
+(** A postprocessing translation [to_post] can be done after execution
+ of the [to_ty] interpreter. The reverse translation is performed
+ before the [of_ty] uninterpreter.
+
+ [to_post] is an array of [n] lists [l_i] of tuples [(f, t,
+ args)]. When the head symbol of the translated term matches one of
+ the [f] in the list [l_0] it is replaced by [t] and its arguments
+ are translated acording to [args] where [ToPostCopy] means that the
+ argument is kept unchanged and [ToPostAs k] means that the
+ argument is recursively translated according to [l_k].
+ [ToPostHole] introduces an additional implicit argument hole
+ (in the reverse translation, the corresponding argument is removed).
+ [ToPostCheck r] behaves as [ToPostCopy] except in the reverse
+ translation which fails if the copied term is not [r].
+ When [n] is null, no translation is performed. *)
+type to_post_arg = ToPostCopy | ToPostAs of int | ToPostHole | ToPostCheck of GlobRef.t
type ('target, 'warning) prim_token_notation_obj =
{ to_kind : 'target conversion_kind;
to_ty : GlobRef.t;
+ to_post : ((GlobRef.t * GlobRef.t * to_post_arg list) list) array;
of_kind : 'target conversion_kind;
of_ty : GlobRef.t;
ty_name : Libnames.qualid; (* for warnings / error messages *)
warning : 'warning }
-type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
module PrimTokenNotation = struct
-(** * Code shared between Numeral notation and String notation *)
+(** * Code shared between Number notation and String notation *)
(** Reduction
The constr [c] below isn't necessarily well-typed, since we
@@ -541,22 +610,69 @@ exception NotAValidPrimToken
to [constr] for the subset that concerns us.
Note that if you update [constr_of_glob], you should update the
- corresponding numeral notation *and* string notation doc in
+ corresponding number notation *and* string notation doc in
doc/sphinx/user-extensions/syntax-extensions.rst that describes
what it means for a term to be ground / to be able to be
considered for parsing. *)
-let rec constr_of_glob env sigma g = match DAst.get g with
- | Glob_term.GRef (GlobRef.ConstructRef c, _) ->
- let sigma,c = Evd.fresh_constructor_instance env sigma c in
- sigma,mkConstructU c
- | Glob_term.GRef (GlobRef.IndRef c, _) ->
- let sigma,c = Evd.fresh_inductive_instance env sigma c in
- sigma,mkIndU c
+let constr_of_globref allow_constant env sigma = function
+ | GlobRef.ConstructRef c ->
+ let sigma,c = Evd.fresh_constructor_instance env sigma c in
+ sigma,mkConstructU c
+ | GlobRef.IndRef c ->
+ let sigma,c = Evd.fresh_inductive_instance env sigma c in
+ sigma,mkIndU c
+ | GlobRef.ConstRef c when allow_constant ->
+ let sigma,c = Evd.fresh_constant_instance env sigma c in
+ sigma,mkConstU c
+ | _ -> raise NotAValidPrimToken
+
+let rec constr_of_glob allow_constant to_post post env sigma g = match DAst.get g with
+ | Glob_term.GRef (r, _) ->
+ let o = List.find_opt (fun (_,r',_) -> GlobRef.equal r r') post in
+ begin match o with
+ | None -> constr_of_globref allow_constant env sigma r
+ | Some (r, _, a) ->
+ (* [g] is not a GApp so check that [post]
+ does not expect any actual argument
+ (i.e., [a] contains only ToPostHole since they mean "ignore arg") *)
+ if List.exists ((<>) ToPostHole) a then raise NotAValidPrimToken;
+ constr_of_globref true env sigma r
+ end
| Glob_term.GApp (gc, gcl) ->
- let sigma,c = constr_of_glob env sigma gc in
- let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
- sigma,mkApp (c, Array.of_list cl)
+ let o = match DAst.get gc with
+ | Glob_term.GRef (r, _) -> List.find_opt (fun (_,r',_) -> GlobRef.equal r r') post
+ | _ -> None in
+ begin match o with
+ | None ->
+ let sigma,c = constr_of_glob allow_constant to_post post env sigma gc in
+ let sigma,cl = List.fold_left_map (constr_of_glob allow_constant to_post post env) sigma gcl in
+ sigma,mkApp (c, Array.of_list cl)
+ | Some (r, _, a) ->
+ let sigma,c = constr_of_globref true env sigma r in
+ let rec aux sigma a gcl = match a, gcl with
+ | [], [] -> sigma,[]
+ | ToPostCopy :: a, gc :: gcl ->
+ let sigma,c = constr_of_glob allow_constant [||] [] env sigma gc in
+ let sigma,cl = aux sigma a gcl in
+ sigma, c :: cl
+ | ToPostCheck r :: a, gc :: gcl ->
+ let () = match DAst.get gc with
+ | Glob_term.GRef (r', _) when GlobRef.equal r r' -> ()
+ | _ -> raise NotAValidPrimToken in
+ let sigma,c = constr_of_glob true [||] [] env sigma gc in
+ let sigma,cl = aux sigma a gcl in
+ sigma, c :: cl
+ | ToPostAs i :: a, gc :: gcl ->
+ let sigma,c = constr_of_glob allow_constant to_post to_post.(i) env sigma gc in
+ let sigma,cl = aux sigma a gcl in
+ sigma, c :: cl
+ | ToPostHole :: post, _ :: gcl -> aux sigma post gcl
+ | [], _ :: _ | _ :: _, [] -> raise NotAValidPrimToken
+ in
+ let sigma,cl = aux sigma a gcl in
+ sigma,mkApp (c, Array.of_list cl)
+ end
| Glob_term.GInt i -> sigma, mkInt i
| Glob_term.GSort gs ->
let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in
@@ -564,6 +680,10 @@ let rec constr_of_glob env sigma g = match DAst.get g with
| _ ->
raise NotAValidPrimToken
+let constr_of_glob to_post env sigma (Glob_term.AnyGlobConstr g) =
+ let post = match to_post with [||] -> [] | _ -> to_post.(0) in
+ constr_of_glob false to_post post env sigma g
+
let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
| App (c, ca) ->
let c = glob_of_constr token_kind ?loc env sigma c in
@@ -585,9 +705,38 @@ let no_such_prim_token uninterpreted_token_kind ?loc ty =
(str ("Cannot interpret this "^uninterpreted_token_kind^" as a value of type ") ++
pr_qualid ty)
-let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma c =
+let rec postprocess token_kind ?loc ty to_post post g =
+ let g', gl = match DAst.get g with Glob_term.GApp (g, gl) -> g, gl | _ -> g, [] in
+ let o =
+ match DAst.get g' with
+ | Glob_term.GRef (r, None) ->
+ List.find_opt (fun (r',_,_) -> GlobRef.equal r r') post
+ | _ -> None in
+ match o with None -> g | Some (_, r, a) ->
+ let rec f n a gl = match a, gl with
+ | [], [] -> []
+ | ToPostHole :: a, gl ->
+ let e = Evar_kinds.ImplicitArg (r, (n, None), true) in
+ let h = DAst.make ?loc (Glob_term.GHole (e, Namegen.IntroAnonymous, None)) in
+ h :: f (n+1) a gl
+ | (ToPostCopy | ToPostCheck _) :: a, g :: gl -> g :: f (n+1) a gl
+ | ToPostAs c :: a, g :: gl ->
+ postprocess token_kind ?loc ty to_post to_post.(c) g :: f (n+1) a gl
+ | [], _::_ | _::_, [] ->
+ no_such_prim_token token_kind ?loc ty
+ in
+ let gl = f 1 a gl in
+ let g = DAst.make ?loc (Glob_term.GRef (r, None)) in
+ DAst.make ?loc (Glob_term.GApp (g, gl))
+
+let glob_of_constr token_kind ty ?loc env sigma to_post c =
+ let g = glob_of_constr token_kind ?loc env sigma c in
+ match to_post with [||] -> g | _ ->
+ postprocess token_kind ?loc ty to_post to_post.(0) g
+
+let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma to_post c =
match Constr.kind c with
- | App (_Some, [| _; c |]) -> glob_of_constr token_kind ?loc env sigma c
+ | App (_Some, [| _; c |]) -> glob_of_constr token_kind ty ?loc env sigma to_post c
| App (_None, [| _ |]) -> no_such_prim_token uninterpreted_token_kind ?loc ty
| x -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedNonOptionTerm c))
@@ -596,13 +745,13 @@ let uninterp_option c =
| App (_Some, [| _; x |]) -> x
| _ -> raise NotAValidPrimToken
-let uninterp to_raw o (Glob_term.AnyGlobConstr n) =
+let uninterp to_raw o n =
let env = Global.env () in
let sigma = Evd.from_env env in
let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in
let of_ty = EConstr.Unsafe.to_constr of_ty in
try
- let sigma,n = constr_of_glob env sigma n in
+ let sigma,n = constr_of_glob o.to_post env sigma n in
let c = eval_constr_app env sigma of_ty n in
let c = if snd o.of_kind == Direct then c else uninterp_option c in
Some (to_raw (fst o.of_kind, c))
@@ -623,8 +772,8 @@ let rec int63_of_pos_bigint i =
(Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo))
else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)
-module Numeral = struct
-(** * Numeral notation *)
+module Numbers = struct
+(** * Number notation *)
open PrimTokenNotation
let warn_large_num =
@@ -680,7 +829,7 @@ let coqint_of_rawnum inds c (sign,n) =
let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
mkApp (mkConstruct (ind, pos_neg), [|uint|])
-let coqnumeral_of_rawnum inds c n =
+let coqnumber_of_rawnum inds c n =
let ind = match c with CDec -> inds.decimal | CHex -> inds.hexadecimal in
let i, f, e = NumTok.Signed.to_int_frac_and_exponent n in
let i = coqint_of_rawnum inds.int c i in
@@ -692,19 +841,19 @@ let coqnumeral_of_rawnum inds c n =
mkApp (mkConstruct (ind, 2), [|i; f; e|]) (* (D|Hexad)ecimalExp *)
let mkDecHex ind c n = match c with
- | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Dec *)
- | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hex *)
+ | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Decimal *)
+ | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hexadecimal *)
exception NonDecimal
-let decimal_coqnumeral_of_rawnum inds n =
+let decimal_coqnumber_of_rawnum inds n =
if NumTok.Signed.classify n <> CDec then raise NonDecimal;
- coqnumeral_of_rawnum inds CDec n
+ coqnumber_of_rawnum inds CDec n
-let coqnumeral_of_rawnum inds n =
+let coqnumber_of_rawnum inds n =
let c = NumTok.Signed.classify n in
- let n = coqnumeral_of_rawnum inds c n in
- mkDecHex inds.numeral c n
+ let n = coqnumber_of_rawnum inds c n in
+ mkDecHex inds.number c n
let decimal_coquint_of_rawnum inds n =
if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal;
@@ -754,7 +903,7 @@ let rawnum_of_coqint cl c =
| _ -> raise NotAValidPrimToken)
| _ -> raise NotAValidPrimToken
-let rawnum_of_coqnumeral cl c =
+let rawnum_of_coqnumber cl c =
let of_ife i f e =
let n = rawnum_of_coqint cl i in
let f = try Some (rawnum_of_coquint cl f) with NotAValidPrimToken -> None in
@@ -768,17 +917,17 @@ let rawnum_of_coqnumeral cl c =
let destDecHex c = match Constr.kind c with
| App (c,[|c'|]) ->
(match Constr.kind c with
- | Construct ((_,1), _) (* (UInt|Int|)Dec *) -> CDec, c'
- | Construct ((_,2), _) (* (UInt|Int|)Hex *) -> CHex, c'
+ | Construct ((_,1), _) (* (UInt|Int|)Decimal *) -> CDec, c'
+ | Construct ((_,2), _) (* (UInt|Int|)Hexadecimal *) -> CHex, c'
| _ -> raise NotAValidPrimToken)
| _ -> raise NotAValidPrimToken
-let decimal_rawnum_of_coqnumeral c =
- rawnum_of_coqnumeral CDec c
+let decimal_rawnum_of_coqnumber c =
+ rawnum_of_coqnumber CDec c
-let rawnum_of_coqnumeral c =
+let rawnum_of_coqnumber c =
let cl, c = destDecHex c in
- rawnum_of_coqnumeral cl c
+ rawnum_of_coqnumber cl c
let decimal_rawnum_of_coquint c =
rawnum_of_coquint CDec c
@@ -900,9 +1049,9 @@ let interp o ?loc n =
interp_int63 ?loc (NumTok.SignedNat.to_bigint n)
| (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ ->
no_such_prim_token "number" ?loc o.ty_name
- | Numeral numeral_ty, _ -> coqnumeral_of_rawnum numeral_ty n
- | Decimal numeral_ty, _ ->
- (try decimal_coqnumeral_of_rawnum numeral_ty n
+ | Number number_ty, _ -> coqnumber_of_rawnum number_ty n
+ | Decimal number_ty, _ ->
+ (try decimal_coqnumber_of_rawnum number_ty n
with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
in
let env = Global.env () in
@@ -912,12 +1061,13 @@ let interp o ?loc n =
match o.warning, snd o.to_kind with
| Abstract threshold, Direct when NumTok.Signed.is_bigger_int_than n threshold ->
warn_abstract_large_num (o.ty_name,o.to_ty);
- glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|]))
+ assert (Array.length o.to_post = 0);
+ glob_of_constr "number" o.ty_name ?loc env sigma o.to_post (mkApp (to_ty,[|c|]))
| _ ->
let res = eval_constr_app env sigma to_ty c in
match snd o.to_kind with
- | Direct -> glob_of_constr "numeral" ?loc env sigma res
- | Option -> interp_option "number" "numeral" o.ty_name ?loc env sigma res
+ | Direct -> glob_of_constr "number" o.ty_name ?loc env sigma o.to_post res
+ | Option -> interp_option "number" "number" o.ty_name ?loc env sigma o.to_post res
let uninterp o n =
PrimTokenNotation.uninterp
@@ -926,10 +1076,10 @@ let uninterp o n =
| (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c)
| (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c)
| (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c)
- | (Numeral _, c) -> rawnum_of_coqnumeral c
+ | (Number _, c) -> rawnum_of_coqnumber c
| (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c)
| (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c)
- | (Decimal _, c) -> decimal_rawnum_of_coqnumeral c
+ | (Decimal _, c) -> decimal_rawnum_of_coqnumber c
end o n
end
@@ -962,11 +1112,12 @@ let coqbyte_of_string ?loc byte s =
let p =
if Int.equal (String.length s) 1 then int_of_char s.[0]
else
- if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
- then int_of_string s
- else
+ let n =
+ if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
+ then int_of_string s else 256 in
+ if n < 256 then n else
user_err ?loc ~hdr:"coqbyte_of_string"
- (str "Expects a single character or a three-digits ascii code.") in
+ (str "Expects a single character or a three-digit ASCII code.") in
coqbyte_of_char_code byte p
let coqbyte_of_char byte c = coqbyte_of_char_code byte (Char.code c)
@@ -1021,8 +1172,8 @@ let interp o ?loc n =
let to_ty = EConstr.Unsafe.to_constr to_ty in
let res = eval_constr_app env sigma to_ty c in
match snd o.to_kind with
- | Direct -> glob_of_constr "string" ?loc env sigma res
- | Option -> interp_option "string" "string" o.ty_name ?loc env sigma res
+ | Direct -> glob_of_constr "string" o.ty_name ?loc env sigma o.to_post res
+ | Option -> interp_option "string" "string" o.ty_name ?loc env sigma o.to_post res
let uninterp o n =
PrimTokenNotation.uninterp
@@ -1034,21 +1185,21 @@ end
(* A [prim_token_infos], which is synchronized with the document
state, either contains a unique id pointing to an unsynchronized
- prim token function, or a numeral notation object describing how to
+ prim token function, or a number notation object describing how to
interpret and uninterpret. We provide [prim_token_infos] because
we expect plugins to provide their own interpretation functions,
- rather than going through numeral notations, which are available as
+ rather than going through number notations, which are available as
a vernacular. *)
type prim_token_interp_info =
Uid of prim_token_uid
- | NumeralNotation of numeral_notation_obj
+ | NumberNotation of number_notation_obj
| StringNotation of string_notation_obj
type prim_token_infos = {
pt_local : bool; (** Is this interpretation local? *)
pt_scope : scope_name; (** Concerned scope *)
- pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+ pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a number notation object describing (un)interp functions *)
pt_required : required_module; (** Module that should be loaded first *)
pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
pt_in_match : bool (** Is this prim token legal in match patterns ? *)
@@ -1072,7 +1223,7 @@ let hashtbl_check_and_set allow_overwrite uid f h eq =
| _ ->
user_err ~hdr:"prim_token_interpreter"
(str "Unique identifier " ++ str uid ++
- str " already used to register a numeral or string (un)interpreter.")
+ str " already used to register a number or string (un)interpreter.")
let register_gen_interpretation allow_overwrite uid (interp, uninterp) =
hashtbl_check_and_set
@@ -1100,7 +1251,6 @@ let cache_prim_token_interpretation (_,infos) =
String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos;
let add_uninterp r =
let l = try GlobRef.Map.find r !prim_token_uninterp_infos with Not_found -> [] in
- let l = List.remove_assoc_f String.equal sc l in
prim_token_uninterp_infos :=
GlobRef.Map.add r ((sc,(ptii,infos.pt_in_match)) :: l)
!prim_token_uninterp_infos in
@@ -1173,7 +1323,7 @@ let check_required_module ?loc sc (sp,d) =
(str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++
str (List.last d) ++ str ".")
-(* Look if some notation or numeral printer in [scope] can be used in
+(* Look if some notation or number printer in [scope] can be used in
the scope stack [scopes], and if yes, using delimiters or not *)
let find_with_delimiters = function
@@ -1190,7 +1340,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
| NotationInScope scope' when String.equal scope scope' ->
Some (None,None)
| _ ->
- (* If the most recently open scope has a notation/numeral printer
+ (* If the most recently open scope has a notation/number printer
but not the expected one then we need delimiters *)
if find scope then
find_with_delimiters ntn_scope
@@ -1225,39 +1375,89 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
(* The mapping between notations and their interpretation *)
+let pr_optional_scope = function
+ | LastLonelyNotation -> mt ()
+ | NotationInScope scope -> spc () ++ strbrk "in scope" ++ spc () ++ str scope
+
let warn_notation_overridden =
CWarnings.create ~name:"notation-overridden" ~category:"parsing"
- (fun (ntn,which_scope) ->
+ (fun (scope,ntn) ->
str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
- ++ strbrk "was already used" ++ which_scope ++ str ".")
+ ++ strbrk "was already used" ++ pr_optional_scope scope ++ str ".")
-let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation =
- let scope = match scopt with Some s -> s | None -> default_scope in
- let sc = find_scope scope in
- if not onlyprint then begin
- let () =
- if NotationMap.mem ntn sc.notations then
- let which_scope = match scopt with
- | None -> mt ()
- | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
- warn_notation_overridden (ntn,which_scope)
- in
- let notdata = {
- not_interp = pat;
- not_location = df;
- not_deprecation = deprecation;
- } in
- let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in
- scope_map := String.Map.add scope sc !scope_map
- end;
- begin match scopt with
- | None -> scope_stack := LonelyNotationItem ntn :: !scope_stack
- | Some _ -> ()
- end
+let warn_deprecation_overridden =
+ CWarnings.create ~name:"notation-overridden" ~category:"parsing"
+ (fun ((scope,ntn),old,now) ->
+ match old, now with
+ | None, None -> assert false
+ | None, Some _ ->
+ (str "Notation" ++ spc () ++ pr_notation ntn ++ pr_optional_scope scope ++ spc ()
+ ++ strbrk "is now marked as deprecated" ++ str ".")
+ | Some _, None ->
+ (str "Cancelling previous deprecation of notation" ++ spc () ++
+ pr_notation ntn ++ pr_optional_scope scope ++ str ".")
+ | Some _, Some _ ->
+ (str "Amending deprecation of notation" ++ spc () ++
+ pr_notation ntn ++ pr_optional_scope scope ++ str "."))
+
+type notation_use =
+ | OnlyPrinting
+ | OnlyParsing
+ | ParsingAndPrinting
+
+let warn_override_if_needed (scopt,ntn) overridden data old_data =
+ if overridden then warn_notation_overridden (scopt,ntn)
+ else
+ if data.not_deprecation <> old_data.not_deprecation then
+ warn_deprecation_overridden ((scopt,ntn),old_data.not_deprecation,data.not_deprecation)
+
+let check_parsing_override (scopt,ntn) data = function
+ | OnlyParsingData (_,old_data) ->
+ let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
+ warn_override_if_needed (scopt,ntn) overridden data old_data;
+ None, not overridden
+ | ParsingAndPrintingData (_,on_printing,old_data) ->
+ let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
+ warn_override_if_needed (scopt,ntn) overridden data old_data;
+ (if on_printing then Some old_data.not_interp else None), not overridden
+ | NoParsingData -> None, false
+
+let check_printing_override (scopt,ntn) data parsingdata printingdata =
+ let parsing_update = match parsingdata with
+ | OnlyParsingData _ | NoParsingData -> parsingdata
+ | ParsingAndPrintingData (_,on_printing,old_data) ->
+ let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
+ warn_override_if_needed (scopt,ntn) overridden data old_data;
+ if overridden then NoParsingData else parsingdata in
+ let exists = List.exists (fun (on_printing,old_data) ->
+ let exists = interpretation_eq data.not_interp old_data.not_interp in
+ if exists && data.not_deprecation <> old_data.not_deprecation then
+ warn_deprecation_overridden ((scopt,ntn),old_data.not_deprecation,data.not_deprecation);
+ exists) printingdata in
+ parsing_update, exists
+
+let remove_uninterpretation rule also_in_cases_pattern (metas,c as pat) =
+ let (key,n) = notation_constr_key c in
+ notations_key_table := keymap_remove key (also_in_cases_pattern,(rule,pat,n)) !notations_key_table
-let declare_uninterpretation rule (metas,c as pat) =
+let declare_uninterpretation ?(also_in_cases_pattern=true) rule (metas,c as pat) =
let (key,n) = notation_constr_key c in
- notations_key_table := keymap_add key (rule,pat,n) !notations_key_table
+ notations_key_table := keymap_add key (also_in_cases_pattern,(rule,pat,n)) !notations_key_table
+
+let update_notation_data (scopt,ntn) use data table =
+ let (parsingdata,printingdata) =
+ try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in
+ match use with
+ | OnlyParsing ->
+ let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
+ NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists
+ | ParsingAndPrinting ->
+ let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
+ NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists
+ | OnlyPrinting ->
+ let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in
+ let printingdata = if exists then printingdata else (true,data) :: printingdata in
+ NotationMap.add ntn (parsingdata, printingdata) table, None, exists
let rec find_interpretation ntn find = function
| [] -> raise Not_found
@@ -1273,11 +1473,13 @@ let rec find_interpretation ntn find = function
find_interpretation ntn find scopes
let find_notation ntn sc =
- NotationMap.find ntn (find_scope sc).notations
+ match fst (NotationMap.find ntn (find_scope sc).notations) with
+ | OnlyParsingData (true,data) | ParsingAndPrintingData (true,_,data) -> data
+ | _ -> raise Not_found
let notation_of_prim_token = function
- | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
- | Constrexpr.Numeral (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
+ | Constrexpr.Number (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
+ | Constrexpr.Number (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
| String _ -> raise Not_found
let find_prim_token check_allowed ?loc p sc =
@@ -1295,7 +1497,7 @@ let find_prim_token check_allowed ?loc p sc =
check_required_module ?loc sc spdir;
let interp = match info with
| Uid uid -> Hashtbl.find prim_token_interpreters uid
- | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o)
+ | NumberNotation o -> InnerPrimToken.RawNumInterp (Numbers.interp o)
| StringNotation o -> InnerPrimToken.StringInterp (Strings.interp o)
in
let pat = InnerPrimToken.do_interp ?loc interp p in
@@ -1312,8 +1514,8 @@ let interp_prim_token_gen ?loc g p local_scopes =
let _, info = Exninfo.capture exn in
user_err ?loc ~info ~hdr:"interp_prim_token"
((match p with
- | Numeral _ ->
- str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p)
+ | Number _ ->
+ str "No interpretation for number " ++ pr_notation (notation_of_prim_token p)
| String s -> str "No interpretation for string " ++ qs s) ++ str ".")
let interp_prim_token ?loc =
@@ -1349,19 +1551,49 @@ let interp_notation ?loc ntn local_scopes =
(str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
let uninterp_notations c =
- List.map_append (fun key -> keymap_find key !notations_key_table)
+ List.map_append (fun key -> List.map snd (keymap_find key !notations_key_table))
(glob_constr_keys c)
+let filter_also_for_pattern =
+ List.map_filter (function (true,x) -> Some x | _ -> None)
+
let uninterp_cases_pattern_notations c =
- keymap_find (cases_pattern_key c) !notations_key_table
+ filter_also_for_pattern (keymap_find (cases_pattern_key c) !notations_key_table)
let uninterp_ind_pattern_notations ind =
- keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table
+ filter_also_for_pattern (keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table)
+
+let has_active_parsing_rule_in_scope ntn sc =
+ try
+ match NotationMap.find ntn (String.Map.find sc !scope_map).notations with
+ | OnlyParsingData (active,_),_ | ParsingAndPrintingData (active,_,_),_ -> active
+ | _ -> false
+ with Not_found -> false
+
+let is_printing_active_in_scope (scope,ntn) pat =
+ let sc = match scope with NotationInScope sc -> sc | LastLonelyNotation -> default_scope in
+ let is_active extra =
+ try
+ let (_,(active,_)) = List.extract_first (fun (active,d) -> interpretation_eq d.not_interp pat) extra in
+ active
+ with Not_found -> false in
+ try
+ match NotationMap.find ntn (String.Map.find sc !scope_map).notations with
+ | ParsingAndPrintingData (_,active,d), extra ->
+ if interpretation_eq d.not_interp pat then active
+ else is_active extra
+ | _, extra -> is_active extra
+ with Not_found -> false
+
+let is_printing_inactive_rule rule pat =
+ match rule with
+ | NotationRule (scope,ntn) ->
+ not (is_printing_active_in_scope (scope,ntn) pat)
+ | SynDefRule kn ->
+ try let _ = Nametab.path_of_syndef kn in false with Not_found -> true
let availability_of_notation (ntn_scope,ntn) scopes =
- let f scope =
- NotationMap.mem ntn (String.Map.find scope !scope_map).notations in
- find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
+ find_without_delimiters (has_active_parsing_rule_in_scope ntn) (ntn_scope,Some ntn) (make_current_scopes scopes)
(* We support coercions from a custom entry at some level to an entry
at some level (possibly the same), and from and to the constr entry. E.g.:
@@ -1484,20 +1716,63 @@ let entry_has_ident = function
| InCustomEntryLevel (s,n) ->
try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
+type entry_coercion_kind =
+ | IsEntryCoercion of notation_entry_level
+ | IsEntryGlobal of string * int
+ | IsEntryIdent of string * int
+
+let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecation =
+ (* Register the interpretation *)
+ let scope = match scopt with NotationInScope s -> s | LastLonelyNotation -> default_scope in
+ let sc = find_scope scope in
+ let notdata = {
+ not_interp = pat;
+ not_location = df;
+ not_deprecation = deprecation;
+ } in
+ let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in
+ if not exists then
+ let sc = { sc with notations = notation_update } in
+ scope_map := String.Map.add scope sc !scope_map;
+ (* Update the uninterpretation cache *)
+ begin match printing_update with
+ | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) also_in_cases_pattern pat
+ | None -> ()
+ end;
+ if not exists && use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat;
+ (* Register visibility of lonely notations *)
+ if not exists then begin match scopt with
+ | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack
+ | NotationInScope _ -> ()
+ end;
+ (* Declare a possible coercion *)
+ if not exists then begin match coe with
+ | Some (IsEntryCoercion entry) ->
+ let (_,level,_) = level_of_notation ntn in
+ let level = match fst ntn with
+ | InConstrEntry -> None
+ | InCustomEntry _ -> Some level
+ in
+ declare_entry_coercion (scopt,ntn) level entry
+ | Some (IsEntryGlobal (entry,n)) -> declare_custom_entry_has_global entry n
+ | Some (IsEntryIdent (entry,n)) -> declare_custom_entry_has_ident entry n
+ | None -> ()
+ end
+
let availability_of_prim_token n printer_scope local_scopes =
let f scope =
try
let uid = snd (String.Map.find scope !prim_token_interp_infos) in
let open InnerPrimToken in
match n, uid with
- | Constrexpr.Numeral _, NumeralNotation _ -> true
- | _, NumeralNotation _ -> false
+ | Constrexpr.Number _, NumberNotation _ -> true
+ | _, NumberNotation _ -> false
| String _, StringNotation _ -> true
| _, StringNotation _ -> false
| _, Uid uid ->
let interp = Hashtbl.find prim_token_interpreters uid in
match n, interp with
- | Constrexpr.Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+ | Constrexpr.Number _, (RawNumInterp _ | BigNumInterp _) -> true
| String _, StringInterp _ -> true
| _ -> false
with Not_found -> false
@@ -1512,7 +1787,7 @@ let rec find_uninterpretation need_delim def find = function
def
| OpenScopeItem scope :: scopes ->
(try find need_delim scope
- with Not_found -> find_uninterpretation need_delim def find scopes) (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a numeral notation *)
+ with Not_found -> find_uninterpretation need_delim def find scopes) (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a number notation *)
| LonelyNotationItem ntn::scopes ->
find_uninterpretation (ntn::need_delim) def find scopes
@@ -1524,7 +1799,7 @@ let uninterp_prim_token c local_scopes =
try
let uninterp = match info with
| Uid uid -> Hashtbl.find prim_token_uninterpreters uid
- | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+ | NumberNotation o -> InnerPrimToken.RawNumUninterp (Numbers.uninterp o)
| StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
in
match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
@@ -1561,38 +1836,6 @@ let uninterp_prim_token_cases_pattern c local_scopes =
(* Miscellaneous *)
-let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
-
-let notation_binder_source_eq s1 s2 = match s1, s2 with
-| NtnParsedAsIdent, NtnParsedAsIdent -> true
-| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
-| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
-| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
-
-let ntpe_eq t1 t2 = match t1, t2 with
-| NtnTypeConstr, NtnTypeConstr -> true
-| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2
-| NtnTypeConstrList, NtnTypeConstrList -> true
-| NtnTypeBinderList, NtnTypeBinderList -> true
-| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
-
-let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) =
- notation_entry_level_eq entry1 entry2 &&
- pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
- ntpe_eq tp1 tp2
-
-let interpretation_eq (vars1, t1) (vars2, t2) =
- List.equal var_attributes_eq vars1 vars2 &&
- Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
-
-let exists_notation_in_scope scopt ntn onlyprint r =
- let scope = match scopt with Some s -> s | None -> default_scope in
- try
- let sc = String.Map.find scope !scope_map in
- let n = NotationMap.find ntn sc.notations in
- interpretation_eq n.not_interp r
- with Not_found -> false
-
let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
(**********************************************************************)
@@ -1846,38 +2089,63 @@ let pr_scope_classes sc =
| _ :: ll ->
let opt_s = match ll with [] -> mt () | _ -> str "es" in
hov 0 (str "Bound to class" ++ opt_s ++
- spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl()
+ spc() ++ prlist_with_sep spc pr_scope_class l)
let pr_notation_info prglob ntn c =
- str "\"" ++ str ntn ++ str "\" := " ++
+ str "\"" ++ str ntn ++ str "\" :=" ++ brk (1,2) ++
prglob (Notation_ops.glob_constr_of_notation_constr c)
-let pr_named_scope prglob scope sc =
+let pr_notation_status on_parsing on_printing =
+ let deactivated b = if b then [] else ["deactivated"] in
+ let l = match on_parsing, on_printing with
+ | Some on, None -> "only parsing" :: deactivated on
+ | None, Some on -> "only printing" :: deactivated on
+ | Some false, Some false -> ["deactivated"]
+ | Some true, Some false -> ["deactivated for printing"]
+ | Some false, Some true -> ["deactivated for parsing"]
+ | Some true, Some true -> []
+ | None, None -> assert false in
+ match l with
+ | [] -> mt ()
+ | l -> str "(" ++ prlist_with_sep pr_comma str l ++ str ")"
+
+let pr_non_empty spc pp =
+ if pp = mt () then mt () else spc ++ pp
+
+let pr_notation_data prglob (on_parsing,on_printing,{ not_interp = (_, r); not_location = (_, df) }) =
+ hov 0 (pr_notation_info prglob df r ++ pr_non_empty (brk(1,2)) (pr_notation_status on_parsing on_printing))
+
+let extract_notation_data (main,extra) =
+ let main = match main with
+ | NoParsingData -> []
+ | ParsingAndPrintingData (on_parsing, on_printing, d) ->
+ [Some on_parsing, Some on_printing, d]
+ | OnlyParsingData (on_parsing, d) ->
+ [Some on_parsing, None, d] in
+ let extra = List.map (fun (on_printing, d) -> (None, Some on_printing, d)) extra in
+ main @ extra
+
+let pr_named_scope prglob (scope,sc) =
(if String.equal scope default_scope then
match NotationMap.cardinal sc.notations with
| 0 -> str "No lonely notation"
| n -> str "Lonely notation" ++ (if Int.equal n 1 then mt() else str"s")
else
str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
- ++ fnl ()
- ++ pr_scope_classes scope
- ++ NotationMap.fold
- (fun ntn { not_interp = (_, r); not_location = (_, df) } strm ->
- pr_notation_info prglob df r ++ fnl () ++ strm)
- sc.notations (mt ())
+ ++ pr_non_empty (fnl ()) (pr_scope_classes scope)
+ ++ prlist (fun a -> fnl () ++ pr_notation_data prglob a)
+ (NotationMap.fold (fun ntn data l -> extract_notation_data data @ l) sc.notations [])
-let pr_scope prglob scope = pr_named_scope prglob scope (find_scope scope)
+let pr_scope prglob scope = pr_named_scope prglob (scope, find_scope scope)
let pr_scopes prglob =
- String.Map.fold
- (fun scope sc strm -> pr_named_scope prglob scope sc ++ fnl () ++ strm)
- !scope_map (mt ())
+ let l = String.Map.bindings !scope_map in
+ prlist_with_sep (fun () -> fnl () ++ fnl ()) (pr_named_scope prglob) l
let rec find_default ntn = function
| [] -> None
| OpenScopeItem scope :: scopes ->
- if NotationMap.mem ntn (find_scope scope).notations then
- Some scope
+ if has_active_parsing_rule_in_scope ntn scope then Some scope
else find_default ntn scopes
| LonelyNotationItem ntn' :: scopes ->
if notation_eq ntn ntn' then Some default_scope
@@ -1885,12 +2153,12 @@ let rec find_default ntn = function
let factorize_entries = function
| [] -> []
- | (ntn,c)::l ->
+ | (ntn,sc',c)::l ->
let (ntn,l_of_ntn,rest) =
List.fold_left
- (fun (a',l,rest) (a,c) ->
- if notation_eq a a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
- (ntn,[c],[]) l in
+ (fun (a',l,rest) (a,sc,c) ->
+ if notation_eq a a' then (a',(sc,c)::l,rest) else (a,[sc,c],(a',l)::rest))
+ (ntn,[sc',c],[]) l in
(ntn,l_of_ntn)::rest
type symbol_token = WhiteSpace of int | String of string
@@ -1961,16 +2229,18 @@ let browse_notation strict ntn map =
let l =
String.Map.fold
(fun scope_name sc ->
- NotationMap.fold (fun ntn { not_interp = (_, r); not_location = df } l ->
- if List.exists (find ntn) ntns then (ntn,(scope_name,r,df))::l else l) sc.notations)
+ NotationMap.fold (fun ntn data l ->
+ if List.exists (find ntn) ntns
+ then List.map (fun d -> (ntn,scope_name,d)) (extract_notation_data data) @ l
+ else l) sc.notations)
map [] in
- List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l
+ List.sort (fun x y -> String.compare (snd (pi1 x)) (snd (pi1 y))) l
-let global_reference_of_notation ~head test (ntn,(sc,c,_)) =
+let global_reference_of_notation ~head test (ntn,sc,(on_parsing,on_printing,{not_interp = (_,c)})) =
match c with
- | NRef ref when test ref -> Some (ntn,sc,ref)
+ | NRef ref when test ref -> Some (on_parsing,on_printing,ntn,sc,ref)
| NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref ->
- Some (ntn,sc,ref)
+ Some (on_parsing,on_printing,ntn,sc,ref)
| _ -> None
let error_ambiguous_notation ?loc _ntn =
@@ -1990,17 +2260,17 @@ let interp_notation_as_global_reference ?loc ~head test ntn sc =
let ntns = browse_notation true ntn scopes in
let refs = List.map (global_reference_of_notation ~head test) ntns in
match Option.List.flatten refs with
- | [_,_,ref] -> ref
+ | [Some true,_ (* why not if the only one? *),_,_,ref] -> ref
| [] -> error_notation_not_reference ?loc ntn
| refs ->
- let f (ntn,sc,ref) =
+ let f (on_parsing,_,ntn,sc,ref) =
let def = find_default ntn !scope_stack in
match def with
| None -> false
- | Some sc' -> String.equal sc sc'
+ | Some sc' -> on_parsing = Some true && String.equal sc sc'
in
match List.filter f refs with
- | [_,_,ref] -> ref
+ | [_,_,_,_,ref] -> ref
| [] -> error_notation_not_reference ?loc ntn
| _ -> error_ambiguous_notation ?loc ntn
@@ -2010,24 +2280,25 @@ let locate_notation prglob ntn scope =
match ntns with
| [] -> str "Unknown notation"
| _ ->
- str "Notation" ++ fnl () ++
prlist_with_sep fnl (fun (ntn,l) ->
let scope = find_default ntn scopes in
prlist_with_sep fnl
- (fun (sc,r,(_,df)) ->
+ (fun (sc,(on_parsing,on_printing,{ not_interp = (_, r); not_location = (_, df) })) ->
hov 0 (
+ str "Notation" ++ brk (1,2) ++
pr_notation_info prglob df r ++
(if String.equal sc default_scope then mt ()
- else (spc () ++ str ": " ++ str sc)) ++
+ else (brk (1,2) ++ str ": " ++ str sc)) ++
(if Option.equal String.equal (Some sc) scope
- then spc () ++ str "(default interpretation)" else mt ())))
+ then brk (1,2) ++ str "(default interpretation)" else mt ()) ++
+ pr_non_empty (brk (1,2)) (pr_notation_status on_parsing on_printing)))
l) ntns
let collect_notation_in_scope scope sc known =
assert (not (String.equal scope default_scope));
NotationMap.fold
- (fun ntn { not_interp = (_, r); not_location = (_, df) } (l,known as acc) ->
- if List.mem_f notation_eq ntn known then acc else ((df,r)::l,ntn::known))
+ (fun ntn d (l,known as acc) ->
+ if List.mem_f notation_eq ntn known then acc else (extract_notation_data d @ l,ntn::known))
sc.notations ([],known)
let collect_notations stack =
@@ -2043,13 +2314,13 @@ let collect_notations stack =
if List.mem_f notation_eq ntn knownntn then (all,knownntn)
else
try
- let { not_interp = (_, r); not_location = (_, df) } =
- NotationMap.find ntn (find_scope default_scope).notations in
+ let datas = extract_notation_data
+ (NotationMap.find ntn (find_scope default_scope).notations) in
let all' = match all with
| (s,lonelyntn)::rest when String.equal s default_scope ->
- (s,(df,r)::lonelyntn)::rest
+ (s,datas@lonelyntn)::rest
| _ ->
- (default_scope,[df,r])::all in
+ (default_scope,datas)::all in
(all',ntn::knownntn)
with Not_found -> (* e.g. if only printing *) (all,knownntn))
([],[]) stack)
@@ -2057,7 +2328,7 @@ let collect_notations stack =
let pr_visible_in_scope prglob (scope,ntns) =
let strm =
List.fold_right
- (fun (df,r) strm -> pr_notation_info prglob df r ++ fnl () ++ strm)
+ (fun d strm -> pr_notation_data prglob d ++ fnl () ++ strm)
ntns (mt ()) in
(if String.equal scope default_scope then
str "Lonely notation" ++ (match ntns with [_] -> mt () | _ -> str "s")
@@ -2066,9 +2337,7 @@ let pr_visible_in_scope prglob (scope,ntns) =
++ fnl () ++ strm
let pr_scope_stack prglob stack =
- List.fold_left
- (fun strm scntns -> strm ++ pr_visible_in_scope prglob scntns ++ fnl ())
- (mt ()) (collect_notations stack)
+ prlist_with_sep fnl (pr_visible_in_scope prglob) (collect_notations stack)
let pr_visibility prglob = function
| Some scope -> pr_scope_stack prglob (push_scope scope !scope_stack)
diff --git a/interp/notation.mli b/interp/notation.mli
index 948831b317..b8939ff87b 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -74,7 +74,7 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
(** {6 Declare and uses back and forth an interpretation of primitive token } *)
-(** A numeral interpreter is the pair of an interpreter for **(hexa)decimal**
+(** A number interpreter is the pair of an interpreter for **(hexa)decimal**
numbers in terms and an optional interpreter in pattern, if
non integer or negative numbers are not supported, the interpreter
must fail with an appropriate error message *)
@@ -84,7 +84,7 @@ type required_module = full_path * string list
type rawnum = NumTok.Signed.t
(** The unique id string below will be used to refer to a particular
- registered interpreter/uninterpreter of numeral or string notation.
+ registered interpreter/uninterpreter of number or string notation.
Using the same uid for different (un)interpreters will fail.
If at most one interpretation of prim token is used per scope,
then the scope name could be used as unique id. *)
@@ -106,7 +106,7 @@ val register_bignumeral_interpretation :
val register_string_interpretation :
?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
-(** * Numeral notation *)
+(** * Number notation *)
type prim_token_notation_error =
| UnexpectedTerm of Constr.t
@@ -131,21 +131,21 @@ type z_pos_ty =
{ z_ty : Names.inductive;
pos_ty : Names.inductive }
-type numeral_ty =
+type number_ty =
{ int : int_ty;
decimal : Names.inductive;
hexadecimal : Names.inductive;
- numeral : Names.inductive }
+ number : Names.inductive }
type target_kind =
- | Int of int_ty (* Coq.Init.Numeral.int + uint *)
- | UInt of int_ty (* Coq.Init.Numeral.uint *)
+ | Int of int_ty (* Coq.Init.Number.int + uint *)
+ | UInt of int_ty (* Coq.Init.Number.uint *)
| Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
| Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
- | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *)
+ | Number of number_ty (* Coq.Init.Number.number + uint + int *)
| DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
| DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
- | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
+ | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
type string_target_kind =
| ListByte
@@ -154,26 +154,43 @@ type string_target_kind =
type option_kind = Option | Direct
type 'target conversion_kind = 'target * option_kind
+(** A postprocessing translation [to_post] can be done after execution
+ of the [to_ty] interpreter. The reverse translation is performed
+ before the [of_ty] uninterpreter.
+
+ [to_post] is an array of [n] lists [l_i] of tuples [(f, t,
+ args)]. When the head symbol of the translated term matches one of
+ the [f] in the list [l_0] it is replaced by [t] and its arguments
+ are translated acording to [args] where [ToPostCopy] means that the
+ argument is kept unchanged and [ToPostAs k] means that the
+ argument is recursively translated according to [l_k].
+ [ToPostHole] introduces an additional implicit argument hole
+ (in the reverse translation, the corresponding argument is removed).
+ [ToPostCheck r] behaves as [ToPostCopy] except in the reverse
+ translation which fails if the copied term is not [r].
+ When [n] is null, no translation is performed. *)
+type to_post_arg = ToPostCopy | ToPostAs of int | ToPostHole | ToPostCheck of GlobRef.t
type ('target, 'warning) prim_token_notation_obj =
{ to_kind : 'target conversion_kind;
to_ty : GlobRef.t;
+ to_post : ((GlobRef.t * GlobRef.t * to_post_arg list) list) array;
of_kind : 'target conversion_kind;
of_ty : GlobRef.t;
ty_name : Libnames.qualid; (* for warnings / error messages *)
warning : 'warning }
-type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
type prim_token_interp_info =
Uid of prim_token_uid
- | NumeralNotation of numeral_notation_obj
+ | NumberNotation of number_notation_obj
| StringNotation of string_notation_obj
type prim_token_infos = {
pt_local : bool; (** Is this interpretation local? *)
pt_scope : scope_name; (** Concerned scope *)
- pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+ pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a number notation object describing (un)interp functions *)
pt_required : required_module; (** Module that should be loaded first *)
pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
pt_in_match : bool (** Is this prim token legal in match patterns ? *)
@@ -229,11 +246,24 @@ type interp_rule =
| NotationRule of specific_notation
| SynDefRule of KerName.t
-val declare_notation_interpretation : notation -> scope_name option ->
- interpretation -> notation_location -> onlyprint:bool ->
+type notation_use =
+ | OnlyPrinting
+ | OnlyParsing
+ | ParsingAndPrinting
+
+val declare_uninterpretation : ?also_in_cases_pattern:bool -> interp_rule -> interpretation -> unit
+
+type entry_coercion_kind =
+ | IsEntryCoercion of notation_entry_level
+ | IsEntryGlobal of string * int
+ | IsEntryIdent of string * int
+
+val declare_notation : notation_with_optional_scope * notation ->
+ interpretation -> notation_location -> use:notation_use ->
+ also_in_cases_pattern:bool ->
+ entry_coercion_kind option ->
Deprecation.t option -> unit
-val declare_uninterpretation : interp_rule -> interpretation -> unit
(** Return the interpretation bound to a notation *)
val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
@@ -257,16 +287,14 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list
val availability_of_notation : specific_notation -> subscopes ->
(scope_name option * delimiters option) option
+val is_printing_inactive_rule : interp_rule -> interpretation -> bool
+
(** {6 Miscellaneous} *)
(** If head is true, also allows applied global references. *)
val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) ->
notation_key -> delimiters option -> GlobRef.t
-(** Checks for already existing notations *)
-val exists_notation_in_scope : scope_name option -> notation ->
- bool -> interpretation -> bool
-
(** Declares and looks for scopes associated to arguments of a global ref *)
val declare_arguments_scope :
bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 22531b0016..2e3fa0aa0e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -27,7 +27,9 @@ open Notation_term
(* helper for NVar, NVar case in eq_notation_constr *)
let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
-let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
+let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 =
+(vars1 == vars2 && t1 == t2) ||
+match t1, t2 with
| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
| NVar id1, NVar id2 -> (
match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
@@ -56,7 +58,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
(eq_notation_constr vars) t1 t2
in
let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
- let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
+ let eq (i1, n1) (i2, n2) = Ind.CanOrd.equal i1 i2 && List.equal Name.equal n1 n2 in
(eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
in
Option.equal (eq_notation_constr vars) o1 o2 &&
@@ -799,7 +801,7 @@ let rec fold_cases_pattern_eq f x p p' =
let loc = p.CAst.loc in
match DAst.get p, DAst.get p' with
| PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na
- | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' ->
+ | PatCstr (c,l,na), PatCstr (c',l',na') when Construct.CanOrd.equal c c' ->
let x,l = fold_cases_pattern_list_eq f x l l' in
let x,na = f x na na' in
x, DAst.make ?loc @@ PatCstr (c,l,na)
@@ -816,7 +818,7 @@ and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
| PatVar na1, PatVar na2 -> Name.equal na1 na2
| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
- eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+ Construct.CanOrd.equal c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
Name.equal na1 na2
| _ -> false
@@ -939,7 +941,7 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
try
(* If already bound to a term, unify the binder and the term *)
match DAst.get (Id.List.assoc var terms) with
- | GVar id' ->
+ | GVar id' | GRef (GlobRef.VarRef id',None) ->
(if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
sigma
| t ->
@@ -1039,7 +1041,7 @@ let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1
| PatVar na1, PatVar na2 -> match_names metas acc na1 na2
| _, PatVar Anonymous when allow_catchall -> acc
| PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
- when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
+ when Construct.CanOrd.equal c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
List.fold_left2 (match_cases_pattern_binders false metas)
(match_names metas acc na1 na2) patl1 patl2
| _ -> raise No_match
@@ -1145,16 +1147,22 @@ let does_not_come_from_already_eta_expanded_var glob =
(* checked). *)
match DAst.get glob with GVar _ -> false | _ -> true
+let is_var_term = function
+ (* The kind of expressions allowed to be both a term and a binding variable *)
+ | GVar _ -> true
+ | GRef (GlobRef.VarRef _,None) -> true
+ | _ -> false
+
let rec match_ inner u alp metas sigma a1 a2 =
let open CAst in
let loc = a1.loc in
match DAst.get a1, a2 with
(* Matching notation variable *)
| r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1
- | GVar _, NVar id2 when is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+ | r1, NVar id2 when is_var_term r1 && is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1
| r1, NVar id2 when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_as_term_env alp sigma id2 a1
- | GVar _, NVar id2 when is_onlybinding_strict_meta id2 metas -> raise No_match
- | GVar _, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+ | r1, NVar id2 when is_var_term r1 && is_onlybinding_strict_meta id2 metas -> raise No_match
+ | r1, NVar id2 when is_var_term r1 && is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
| r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
(* Matching recursive notations for terms *)
@@ -1389,11 +1397,11 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
match DAst.get a1, a2 with
| r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[])
| PatVar Anonymous, NHole _ -> sigma,(false,0,[])
- | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 ->
+ | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when Construct.CanOrd.equal r1 r2 ->
let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
sigma,(false,0,l)
| PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2)
- when eq_constructor r1 r2 ->
+ when Construct.CanOrd.equal r1 r2 ->
let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
let le2 = List.length l2 in
if le2 > List.length l1
@@ -1416,10 +1424,10 @@ and match_cases_pattern_no_more_args metas sigma a1 a2 =
let match_ind_pattern metas sigma ind pats a2 =
match a2 with
- | NRef (GlobRef.IndRef r2) when eq_ind ind r2 ->
+ | NRef (GlobRef.IndRef r2) when Ind.CanOrd.equal ind r2 ->
sigma,(false,0,pats)
| NApp (NRef (GlobRef.IndRef r2),l2)
- when eq_ind ind r2 ->
+ when Ind.CanOrd.equal ind r2 ->
let le2 = List.length l2 in
if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats
then
@@ -1434,9 +1442,8 @@ let reorder_canonically_substitution terms termlists metas =
List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
match typ with
| NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists')
- | NtnTypeBinder _ -> assert false
| NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists')
- | NtnTypeBinderList -> assert false)
+ | NtnTypeBinder _ | NtnTypeBinderList -> anomaly (str "Unexpected binder in pattern notation."))
metas ([],[])
let match_notation_constr_cases_pattern c (metas,pat) =
diff --git a/interp/numTok.mli b/interp/numTok.mli
index bcfe663dd2..386a25f042 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -8,20 +8,20 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(** Numerals in different forms: signed or unsigned, possibly with
+(** Numbers in different forms: signed or unsigned, possibly with
fractional part and exponent.
- Numerals are represented using raw strings of (hexa)decimal
+ Numbers are represented using raw strings of (hexa)decimal
literals and a separate sign flag.
Note that this representation is not unique, due to possible
multiple leading or trailing zeros, and -0 = +0, for instances.
- The reason to keep the numeral exactly as it was parsed is that
- specific notations can be declared for specific numerals
+ The reason to keep the number exactly as it was parsed is that
+ specific notations can be declared for specific numbers
(e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or
[Notation "2e1" := ...]). Those notations override the generic
- interpretation as numeral. So, one has to record the form of the
- numeral which exactly matches the notation. *)
+ interpretation as number. So, one has to record the form of the
+ number which exactly matches the notation. *)
type sign = SPlus | SMinus
@@ -44,7 +44,7 @@ sig
val sprint : t -> string
val print : t -> Pp.t
- (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+ (** [sprint] and [print] returns the number as it was parsed, for printing *)
val classify : t -> num_class
@@ -69,7 +69,7 @@ sig
val to_bigint : t -> Z.t
end
-(** {6 Unsigned decimal numerals } *)
+(** {6 Unsigned decimal numbers } *)
module Unsigned :
sig
@@ -80,12 +80,12 @@ sig
val sprint : t -> string
val print : t -> Pp.t
- (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+ (** [sprint] and [print] returns the number as it was parsed, for printing *)
val parse : char Stream.t -> t
- (** Parse a positive Coq numeral.
+ (** Parse a positive Coq number.
Precondition: the first char on the stream is already known to be a digit (\[0-9\]).
- Precondition: at least two extra chars after the numeral to parse.
+ Precondition: at least two extra chars after the number to parse.
The recognized syntax is:
- integer part: \[0-9\]\[0-9_\]*
@@ -97,13 +97,13 @@ sig
- exponent part: empty or \[pP\]\[+-\]?\[0-9\]\[0-9_\]* *)
val parse_string : string -> t option
- (** Parse the string as a non negative Coq numeral, if possible *)
+ (** Parse the string as a non negative Coq number, if possible *)
val classify : t -> num_class
end
-(** {6 Signed decimal numerals } *)
+(** {6 Signed decimal numbers } *)
module Signed :
sig
@@ -117,10 +117,10 @@ sig
val sprint : t -> string
val print : t -> Pp.t
- (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+ (** [sprint] and [print] returns the number as it was parsed, for printing *)
val parse_string : string -> t option
- (** Parse the string as a signed Coq numeral, if possible *)
+ (** Parse the string as a signed Coq number, if possible *)
val of_int_string : string -> t
(** Convert from a string in the syntax of OCaml's int/int64 *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 4418a32645..1d5af3ff39 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -28,7 +28,7 @@ type key =
(** TODO: share code from Notation *)
let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.CanOrd.compare gr1 gr2
| RefKey _, Oth -> -1
| Oth, RefKey _ -> 1
| Oth, Oth -> 0
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 33d8aa6064..46baa00c74 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -50,6 +50,16 @@ let locate_global_with_alias ?(head=false) qid =
user_err ?loc:qid.CAst.loc (pr_qualid qid ++
str " is bound to a notation that does not denote a reference.")
+let global_constant_with_alias qid =
+ try match locate_global_with_alias qid with
+ | Names.GlobRef.ConstRef c -> c
+ | ref ->
+ user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+ (pr_qualid qid ++ spc () ++ str "is not a reference to a constant.")
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
+
let global_inductive_with_alias qid =
try match locate_global_with_alias qid with
| Names.GlobRef.IndRef ind -> ind
@@ -60,6 +70,16 @@ let global_inductive_with_alias qid =
let _, info = Exninfo.capture exn in
Nametab.error_global_not_found ~info qid
+let global_constructor_with_alias qid =
+ try match locate_global_with_alias qid with
+ | Names.GlobRef.ConstructRef c -> c
+ | ref ->
+ user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+ (pr_qualid qid ++ spc () ++ str "is not a constructor of an inductive type.")
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
+
let global_with_alias ?head qid =
try locate_global_with_alias ?head qid
with Not_found as exn ->
@@ -72,9 +92,17 @@ let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun
| ByNotation (ntn,sc) ->
Notation.interp_notation_as_global_reference ?loc ~head (fun _ -> true) ntn sc)
-let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
- | AN r ->
- global_inductive_with_alias r
+let smart_global_kind f dest is = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
+ | AN r -> f r
| ByNotation (ntn,sc) ->
- destIndRef
- (Notation.interp_notation_as_global_reference ?loc ~head:false isIndRef ntn sc))
+ dest
+ (Notation.interp_notation_as_global_reference ?loc ~head:false is ntn sc))
+
+let smart_global_constant =
+ smart_global_kind global_constant_with_alias destConstRef isConstRef
+
+let smart_global_inductive =
+ smart_global_kind global_inductive_with_alias destIndRef isIndRef
+
+let smart_global_constructor =
+ smart_global_kind global_constructor_with_alias destConstructRef isConstructRef
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 9b24a62086..26f2a4f36d 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -28,11 +28,23 @@ val global_of_extended_global : extended_global_reference -> GlobRef.t
a reference. *)
val global_with_alias : ?head:bool -> qualid -> GlobRef.t
+(** The same for constants *)
+val global_constant_with_alias : qualid -> Constant.t
+
(** The same for inductive types *)
val global_inductive_with_alias : qualid -> inductive
+(** The same for constructors of an inductive type *)
+val global_constructor_with_alias : qualid -> constructor
+
(** Locate a reference taking into account notations and "aliases" *)
val smart_global : ?head:bool -> qualid Constrexpr.or_by_notation -> GlobRef.t
+(** The same for constants *)
+val smart_global_constant : qualid Constrexpr.or_by_notation -> Constant.t
+
(** The same for inductive types *)
val smart_global_inductive : qualid Constrexpr.or_by_notation -> inductive
+
+(** The same for constructors of an inductive type *)
+val smart_global_constructor : qualid Constrexpr.or_by_notation -> constructor
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 343f85be03..70be55f843 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -40,8 +40,10 @@ let wit_int_or_var =
let wit_ident =
make0 "ident"
-let wit_var =
- make0 ~dyn:(val_tag (topwit wit_ident)) "var"
+let wit_hyp =
+ make0 ~dyn:(val_tag (topwit wit_ident)) "hyp"
+
+let wit_var = wit_hyp
let wit_ref = make0 "ref"
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 3ae8b7d73f..bd34af5543 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -37,7 +37,10 @@ val wit_int_or_var : (int or_var, int or_var, int) genarg_type
val wit_ident : Id.t uniform_genarg_type
+val wit_hyp : (lident, lident, Id.t) genarg_type
+
val wit_var : (lident, lident, Id.t) genarg_type
+[@@ocaml.deprecated "Use Stdarg.wit_hyp"]
val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index bd3e234a91..f3ad3546ff 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -22,6 +22,7 @@ type syndef =
{ syndef_pattern : interpretation;
syndef_onlyparsing : bool;
syndef_deprecation : Deprecation.t option;
+ syndef_also_in_cases_pattern : bool;
}
let syntax_table =
@@ -52,7 +53,7 @@ let open_syntax_constant i ((sp,kn),(_local,syndef)) =
if not syndef.syndef_onlyparsing then
(* Redeclare it to be used as (short) name in case an other (distfix)
notation was declared in between *)
- Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+ Notation.declare_uninterpretation ~also_in_cases_pattern:syndef.syndef_also_in_cases_pattern (Notation.SynDefRule kn) pat
end
let cache_syntax_constant d =
@@ -81,11 +82,12 @@ let in_syntax_constant : (bool * syndef) -> obj =
subst_function = subst_syntax_constant;
classify_function = classify_syntax_constant }
-let declare_syntactic_definition ~local deprecation id ~onlyparsing pat =
+let declare_syntactic_definition ~local ?(also_in_cases_pattern=true) deprecation id ~onlyparsing pat =
let syndef =
{ syndef_pattern = pat;
syndef_onlyparsing = onlyparsing;
syndef_deprecation = deprecation;
+ syndef_also_in_cases_pattern = also_in_cases_pattern;
}
in
let _ = add_leaf id (in_syntax_constant (local,syndef)) in ()
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 66a3132f2a..31f685152c 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,7 +13,7 @@ open Notation_term
(** Syntactic definitions. *)
-val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t ->
+val declare_syntactic_definition : local:bool -> ?also_in_cases_pattern:bool -> Deprecation.t option -> Id.t ->
onlyparsing:bool -> interpretation -> unit
val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 13:35:16 +0000