aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml5
-rw-r--r--interp/constrexpr_ops.ml9
-rw-r--r--interp/constrextern.ml28
-rw-r--r--interp/constrintern.ml28
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/impargs.ml4
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/notation.ml62
-rw-r--r--interp/notation.mli22
-rw-r--r--interp/notation_ops.ml24
-rw-r--r--interp/notation_term.ml1
11 files changed, 142 insertions, 45 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 21f682ac0e..c98e05370e 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -29,10 +29,10 @@ type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of strin
type notation_key = string
(* A notation associated to a given parsing rule *)
-type notation = notation_entry_level * notation_key
+type notation = notation_entry * notation_key
(* A notation associated to a given interpretation *)
-type specific_notation = notation_with_optional_scope * notation
+type specific_notation = notation_with_optional_scope * (notation_entry * notation_key)
type 'a or_by_notation_r =
| AN of 'a
@@ -115,6 +115,7 @@ and constr_expr_r =
| CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr
+ | CArray of instance_expr option * constr_expr array * constr_expr * constr_expr
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr (* expression that is being matched *)
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3d99e1d227..ce8e7d3c2c 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -174,10 +174,14 @@ let rec constr_expr_eq e1 e2 =
| CDelimiters(s1,e1), CDelimiters(s2,e2) ->
String.equal s1 s2 &&
constr_expr_eq e1 e2
+ | CArray(u1,t1,def1,ty1), CArray(u2,t2,def2,ty2) ->
+ Array.equal constr_expr_eq t1 t2 &&
+ constr_expr_eq def1 def2 && constr_expr_eq ty1 ty2 &&
+ eq_universes u1 u2
| (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
| CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
| CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
- | CGeneralization _ | CDelimiters _ ), _ -> false
+ | CGeneralization _ | CDelimiters _ | CArray _), _ -> false
and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_ast explicitation_eq) e1 e2 &&
@@ -353,6 +357,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (_,_) ->
Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
+ | CArray (_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
)
let free_vars_of_constr_expr c =
@@ -439,6 +444,8 @@ let map_constr_expr_with_binders g f e = CAst.map (function
let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,bl',t',d')) dl)
+ | CArray (u, t, def, ty) ->
+ CArray (u, Array.map (f e) t, f e def, f e ty)
)
(* Used in constrintern *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 63079993c8..95df626d4c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -359,14 +359,14 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
(* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
| "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) ->
assert (bl=[]);
- mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
+ mknot (loc,ntn,([mknot (loc,(InConstrEntry,"( _ )"),l,[])]),[])
| _ ->
match decompose_notation_key ntn, l with
- | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
+ | (InConstrEntry,[Terminal "-"; Terminal x]), [] ->
begin match NumTok.Unsigned.parse_string x with
| Some n -> mkprim (loc, Numeral (NumTok.SMinus,n))
| None -> mknot (loc,ntn,l,bl) end
- | (InConstrEntrySomeLevel,[Terminal x]), [] ->
+ | (InConstrEntry,[Terminal x]), [] ->
begin match NumTok.Unsigned.parse_string x with
| Some n -> mkprim (loc, Numeral (NumTok.SPlus,n))
| None -> mknot (loc,ntn,l,bl) end
@@ -486,7 +486,13 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
function
| NotationRule (_,ntn as specific_ntn) ->
begin
- match availability_of_entry_coercion custom (fst ntn) with
+ let notation_entry_level = match (fst ntn) with
+ | InConstrEntry -> InConstrEntrySomeLevel
+ | InCustomEntry s ->
+ let (_,level,_) = Notation.level_of_notation ntn in
+ InCustomEntryLevel (s, level)
+ in
+ match availability_of_entry_coercion custom notation_entry_level with
| None -> raise No_match
| Some coercion ->
match availability_of_notation specific_ntn (tmp_scope,scopes) with
@@ -1089,6 +1095,9 @@ let rec extern inctx ?impargs scopes vars r =
| 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)
+
in insert_entry_coercion coercion (CAst.make ?loc c)
and extern_typ ?impargs (subentry,(_,scopes)) =
@@ -1260,7 +1269,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
(* Try availability of interpretation ... *)
match keyrule with
| NotationRule (_,ntn as specific_ntn) ->
- (match availability_of_entry_coercion custom (fst ntn) with
+ let notation_entry_level = match (fst ntn) with
+ | InConstrEntry -> InConstrEntrySomeLevel
+ | InCustomEntry s ->
+ let (_,level,_) = Notation.level_of_notation ntn in
+ InCustomEntryLevel (s, level)
+ in
+ (match availability_of_entry_coercion custom notation_entry_level with
| None -> raise No_match
| Some coercion ->
match availability_of_notation specific_ntn scopes with
@@ -1457,6 +1472,9 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| PSort Sorts.InType -> GSort (UAnonymous {rigid=true})
| PInt i -> GInt i
| PFloat f -> GFloat f
+ | PArray(t,def,ty) ->
+ let glob_of = glob_of_pat avoid env sigma in
+ GArray (None, Array.map glob_of t, glob_of def, glob_of ty)
let extern_constr_pattern env sigma pat =
extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ee041ed088..987aa63392 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -224,35 +224,35 @@ let expand_notation_string ntn n =
(* Remark: expansion of squash at definition is done in metasyntax.ml *)
let contract_curly_brackets ntn (l,ll,bl,bll) =
match ntn with
- | InCustomEntryLevel _,_ -> ntn,(l,ll,bl,bll)
- | InConstrEntrySomeLevel, ntn ->
+ | InCustomEntry _,_ -> ntn,(l,ll,bl,bll)
+ | InConstrEntry, ntn ->
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | { CAst.v = CNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
+ | { CAst.v = CNotation (None,(InConstrEntry,"{ _ }"),([a],[],[],[])) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
a::contract_squash (n+1) l in
let l = contract_squash 0 l in
(* side effect; don't inline *)
- (InConstrEntrySomeLevel,!ntn'),(l,ll,bl,bll)
+ (InConstrEntry,!ntn'),(l,ll,bl,bll)
let contract_curly_brackets_pat ntn (l,ll) =
match ntn with
- | InCustomEntryLevel _,_ -> ntn,(l,ll)
- | InConstrEntrySomeLevel, ntn ->
+ | InCustomEntry _,_ -> ntn,(l,ll)
+ | InConstrEntry, ntn ->
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | { CAst.v = CPatNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
+ | { CAst.v = CPatNotation (None,(InConstrEntry,"{ _ }"),([a],[]),[]) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
a::contract_squash (n+1) l in
let l = contract_squash 0 l in
(* side effect; don't inline *)
- (InConstrEntrySomeLevel,!ntn'),(l,ll)
+ (InConstrEntry,!ntn'),(l,ll)
type intern_env = {
ids: Names.Id.Set.t;
@@ -772,7 +772,7 @@ let rec adjust_env env = function
| NCast (c,_) -> adjust_env env c
| NApp _ -> restart_no_binders env
| NVar _ | NRef _ | NHole _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NInt _ | NFloat _
+ | NRec _ | NSort _ | NInt _ | NFloat _ | NArray _
| NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *)
let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
@@ -1688,11 +1688,11 @@ let drop_notations_pattern looked_for genv =
(* 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, [])
- | CPatNotation (_,(InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
+ | 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
rcp_of_glob scopes pat
- | CPatNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
+ | CPatNotation (_,(InConstrEntry,"( _ )"),([a],[]),[]) ->
in_pat top scopes a
| CPatNotation (_,ntn,fullargs,extrargs) ->
let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
@@ -2006,10 +2006,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
DAst.make ?loc @@
GLetIn (na.CAst.v, inc1, int,
intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
- | CNotation (_,(InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
+ | 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)))
- | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
+ | CNotation (_,(InConstrEntry,"( _ )"),([a],[],[],[])) -> intern env a
| CNotation (_,ntn,args) ->
let c = intern_notation intern env ntnvars loc ntn args in
let x, impl, scopes = find_appl_head_data c in
@@ -2204,6 +2204,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CCast (c1, c2) ->
DAst.make ?loc @@
GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2)
+ | CArray(u,t,def,ty) ->
+ DAst.make ?loc @@ GArray(u, Array.map (intern env) t, intern env def, intern env ty)
)
and intern_type env = intern (set_type_scope env)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 57ec708b07..d57c05788d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -207,7 +207,7 @@ let cook_notation (from,df) sc =
done;
let df = Bytes.sub_string ntn 0 !j in
let df_sc = match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df in
- let from_df_sc = match from with Constrexpr.InCustomEntryLevel (from,_) -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntrySomeLevel -> ":" ^ df_sc in
+ let from_df_sc = match from with Constrexpr.InCustomEntry from -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntry -> ":" ^ df_sc in
from_df_sc
let dump_notation_location posl df (((path,secpath),_),sc) =
diff --git a/interp/impargs.ml b/interp/impargs.ml
index a1b029c381..db102470b0 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -229,14 +229,14 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
let rec is_rigid_head sigma t = match kind sigma t with
| Rel _ | Evar _ -> false
| Ind _ | Const _ | Var _ | Sort _ -> true
- | Case (_,_,f,_) -> is_rigid_head sigma f
+ | Case (_,_,_,f,_) -> is_rigid_head sigma f
| Proj (p,c) -> true
| App (f,args) ->
(match kind sigma f with
| Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i)))
| _ -> is_rigid_head sigma f)
| Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
- | Prod _ | Meta _ | Cast _ | Int _ | Float _ -> assert false
+ | Prod _ | Meta _ | Cast _ | Int _ | Float _ | Array _ -> assert false
let is_rigid env sigma t =
let open Context.Rel.Declaration in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3d29da025e..4016a3600e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -92,7 +92,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
let rec aux bdvars l c = match CAst.(c.v) with
| CRef (qid,_) when qualid_is_ident qid ->
found c.CAst.loc (qualid_basename qid) bdvars l
- | CNotation (_,(InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+ | CNotation (_,(InConstrEntry,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
| _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
diff --git a/interp/notation.ml b/interp/notation.ml
index d4a44d9622..e282d62396 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -56,9 +56,9 @@ let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2
| (LastLonelyNotation | NotationInScope _), _ -> false
let notation_eq (from1,ntn1) (from2,ntn2) =
- notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
+ notation_entry_eq from1 from2 && String.equal ntn1 ntn2
-let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s
+let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntry -> mt () | InCustomEntry s -> str " in custom " ++ str s
module NotationOrd =
struct
@@ -337,6 +337,33 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
| NApp (_,args) -> Oth, Some (List.length args)
| _ -> Oth, None
+(** Dealing with precedences *)
+
+type level = notation_entry * entry_level * entry_relative_level list
+ (* first argument is InCustomEntry s for custom entries *)
+
+let entry_relative_level_eq t1 t2 = match t1, t2 with
+| LevelLt n1, LevelLt n2 -> Int.equal n1 n2
+| LevelLe n1, LevelLe n2 -> Int.equal n1 n2
+| LevelSome, LevelSome -> true
+| (LevelLt _ | LevelLe _ | LevelSome), _ -> false
+
+let level_eq (s1, l1, t1) (s2, l2, t2) =
+ notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2
+
+let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
+
+let declare_notation_level ntn level =
+ try
+ let _ = NotationMap.find ntn !notation_level_map in
+ anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
+ with Not_found ->
+ notation_level_map := NotationMap.add ntn level !notation_level_map
+
+let level_of_notation ntn =
+ NotationMap.find ntn !notation_level_map
+
+
(**********************************************************************)
(* Interpreting numbers (not in summary because functional objects) *)
@@ -1228,8 +1255,8 @@ let find_notation ntn sc =
NotationMap.find ntn (find_scope sc).notations
let notation_of_prim_token = function
- | Constrexpr.Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n
- | Constrexpr.Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n
+ | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
+ | Constrexpr.Numeral (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
| String _ -> raise Not_found
let find_prim_token check_allowed ?loc p sc =
@@ -1256,7 +1283,7 @@ let find_prim_token check_allowed ?loc p sc =
let interp_prim_token_gen ?loc g p local_scopes =
let scopes = make_current_scopes local_scopes in
- let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in
+ let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntry,"" in
try
let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in
pat, (loc,sc)
@@ -1336,7 +1363,8 @@ module EntryCoercionOrd =
module EntryCoercionMap = Map.Make(EntryCoercionOrd)
-let entry_coercion_map = ref EntryCoercionMap.empty
+let entry_coercion_map : (((entry_level option * entry_level option) * entry_coercion) list EntryCoercionMap.t) ref =
+ ref EntryCoercionMap.empty
let level_ord lev lev' =
match lev, lev' with
@@ -1349,13 +1377,18 @@ let rec search nfrom nto = function
| ((pfrom,pto),coe)::l ->
if level_ord pfrom nfrom && level_ord nto pto then coe else search nfrom nto l
-let decompose_custom_entry = function
+let make_notation_entry_level entry level =
+ match entry with
+ | InConstrEntry -> InConstrEntrySomeLevel
+ | InCustomEntry s -> InCustomEntryLevel (s,level)
+
+let decompose_notation_entry_level = function
| InConstrEntrySomeLevel -> InConstrEntry, None
| InCustomEntryLevel (s,n) -> InCustomEntry s, Some n
let availability_of_entry_coercion entry entry' =
- let entry, lev = decompose_custom_entry entry in
- let entry', lev' = decompose_custom_entry entry' in
+ let entry, lev = decompose_notation_entry_level entry in
+ let entry', lev' = decompose_notation_entry_level entry' in
if notation_entry_eq entry entry' && level_ord lev' lev then Some []
else
try Some (search lev lev' (EntryCoercionMap.find (entry,entry') !entry_coercion_map))
@@ -1377,28 +1410,27 @@ let rec insert_coercion_path path = function
else if shorter_path path path' then path::allpaths
else path'::insert_coercion_path path paths
-let declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' =
- let entry, lev = decompose_custom_entry entry in
- let entry', lev' = decompose_custom_entry entry' in
+let declare_entry_coercion (scope,(entry,key)) lev entry' =
+ let entry', lev' = decompose_notation_entry_level entry' in
(* Transitive closure *)
let toaddleft =
EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
List.fold_right (fun ((lev'',lev'''),path) l ->
if notation_entry_eq entry entry''' && level_ord lev lev''' &&
not (notation_entry_eq entry' entry'')
- then ((entry'',entry'),((lev'',lev'),path@[specific_ntn]))::l else l) paths l)
+ then ((entry'',entry'),((lev'',lev'),path@[(scope,(entry,key))]))::l else l) paths l)
!entry_coercion_map [] in
let toaddright =
EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
List.fold_right (fun ((lev'',lev'''),path) l ->
if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
- then ((entry,entry'''),((lev,lev'''),path@[specific_ntn]))::l else l) paths l)
+ then ((entry,entry'''),((lev,lev'''),path@[(scope,(entry,key))]))::l else l) paths l)
!entry_coercion_map [] in
entry_coercion_map :=
List.fold_right (fun (pair,path) ->
let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in
EntryCoercionMap.add pair (insert_coercion_path path olds))
- (((entry,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft)
+ (((entry,entry'),((lev,lev'),[(scope,(entry,key))]))::toaddright@toaddleft)
!entry_coercion_map
let entry_has_global_map = ref String.Map.empty
diff --git a/interp/notation.mli b/interp/notation.mli
index e7e917463b..c39bfa6e28 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -298,8 +298,8 @@ type symbol =
val symbol_eq : symbol -> symbol -> bool
(** Make/decompose a notation of the form "_ U _" *)
-val make_notation_key : notation_entry_level -> symbol list -> notation
-val decompose_notation_key : notation -> notation_entry_level * symbol list
+val make_notation_key : notation_entry -> symbol list -> notation
+val decompose_notation_key : notation -> notation_entry * symbol list
(** Decompose a notation of the form "a 'U' b" *)
val decompose_raw_notation : string -> symbol list
@@ -313,8 +313,10 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key ->
val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
+val make_notation_entry_level : notation_entry -> entry_level -> notation_entry_level
+
type entry_coercion = (notation_with_optional_scope * notation) list
-val declare_entry_coercion : specific_notation -> notation_entry_level -> unit
+val declare_entry_coercion : specific_notation -> entry_level option -> notation_entry_level -> unit
val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option
val declare_custom_entry_has_global : string -> int -> unit
@@ -323,6 +325,20 @@ val declare_custom_entry_has_ident : string -> int -> unit
val entry_has_global : notation_entry_level -> bool
val entry_has_ident : notation_entry_level -> bool
+(** Dealing with precedences *)
+
+type level = notation_entry * entry_level * entry_relative_level list
+ (* first argument is InCustomEntry s for custom entries *)
+
+val level_eq : level -> level -> bool
+val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool
+
+(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
+
+val declare_notation_level : notation -> level -> unit
+val level_of_notation : notation -> level
+ (** raise [Not_found] if not declared *)
+
(** Rem: printing rules for primitive token are canonical *)
val with_notation_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 54065e8b35..6422e184b5 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -92,9 +92,12 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
Uint63.equal i1 i2
| NFloat f1, NFloat f2 ->
Float64.equal f1 f2
+| NArray(t1,def1,ty1), NArray(t2,def2,ty2) ->
+ Array.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) def1 def2
+ && eq_notation_constr vars ty1 ty2
| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
| NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _), _ -> false
+ | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> false
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -249,6 +252,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
| NRef x -> GRef (x,None)
| NInt i -> GInt i
| NFloat f -> GFloat f
+ | NArray (t,def,ty) -> GArray(None, Array.map (f e) t, f e def, f e ty)
let glob_constr_of_notation_constr ?loc x =
let rec aux () x =
@@ -472,6 +476,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
if arg != None then has_ltac := true;
NHole (w, naming, arg)
| GRef (r,_) -> NRef r
+ | GArray (_u,t,def,ty) -> NArray (Array.map aux t, aux def, aux ty)
| GEvar _ | GPatVar _ ->
user_err Pp.(str "Existential variables not allowed in notations.")
) x
@@ -675,6 +680,14 @@ let rec subst_notation_constr subst bound raw =
let k' = smartmap_cast_type (subst_notation_constr subst bound) k in
if r1' == r1 && k' == k then raw else NCast(r1',k')
+ | NArray (t,def,ty) ->
+ let def' = subst_notation_constr subst bound def
+ and t' = Array.Smart.map (subst_notation_constr subst bound) t
+ and ty' = subst_notation_constr subst bound ty
+ in
+ if def' == def && t' == t && ty' == ty then raw else
+ NArray(t',def',ty')
+
let subst_interpretation subst (metas,pat) =
let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
(metas,subst_notation_constr subst bound pat)
@@ -1254,9 +1267,16 @@ let rec match_ inner u alp metas sigma a1 a2 =
match_names metas (alp,sigma) (Name id') na in
match_in u alp metas sigma (mkGApp a1 [DAst.make @@ GVar id']) b2
+ | GArray(_u,t,def,ty), NArray(nt,ndef,nty) ->
+ if Int.equal (Array.length t) (Array.length nt) then
+ let sigma = match_in u alp metas sigma def ndef in
+ let sigma = match_in u alp metas sigma ty nty in
+ Array.fold_left2 (match_in u alp metas) sigma t nt
+ else raise No_match
+
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
- | GCast _ | GInt _ | GFloat _), _ -> raise No_match
+ | GCast _ | GInt _ | GFloat _ | GArray _), _ -> raise No_match
and match_in u = match_ true u
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 4e9b8bbb17..82238b71b7 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -45,6 +45,7 @@ type notation_constr =
| NCast of notation_constr * notation_constr cast_type
| NInt of Uint63.t
| NFloat of Float64.t
+ | NArray of notation_constr array * notation_constr * notation_constr
(** Note concerning NList: first constr is iterator, second is terminator;
first id is where each argument of the list has to be substituted
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 02:37:47 +0000