aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml1
-rw-r--r--interp/constrexpr_ops.ml9
-rw-r--r--interp/constrextern.ml22
-rw-r--r--interp/constrintern.ml10
-rw-r--r--interp/impargs.ml2
-rw-r--r--interp/notation.ml18
-rw-r--r--interp/notation.mli7
-rw-r--r--interp/notation_ops.ml24
-rw-r--r--interp/notation_term.ml1
9 files changed, 75 insertions, 19 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 9c4b78f4ed..c98e05370e 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -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 b087431e85..3667757a2f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -858,10 +858,17 @@ let extern_possible_prim_token (custom,scopes) r =
insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
let filter_enough_applied nargs l =
+ (* This is to ensure that notations for coercions are used only when
+ the coercion is fully applied; not explicitly done yet, but we
+ could also expect that the notation is exactly talking about the
+ coercion *)
match nargs with
| None -> l
| Some nargs ->
- List.filter (fun (keyrule,pat,n as _rule) -> match n with Some n -> n > nargs | None -> false) l
+ List.filter (fun (keyrule,pat,n as _rule) ->
+ match n with
+ | AppBoundedNotation n -> n > nargs
+ | AppUnboundedNotation | NotAppNotation -> false) l
(* Helper function for safe and optimal printing of primitive tokens *)
(* such as those for Int63 *)
@@ -1095,6 +1102,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)) =
@@ -1244,7 +1254,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
[], [] in
(* Adjust to the number of arguments expected by the notation *)
let (t,args,argsscopes,argsimpls) = match n with
- | Some n when nallargs >= n ->
+ | AppBoundedNotation n when nallargs >= n ->
let args1, args2 = List.chop n args in
let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
let args2impls =
@@ -1254,12 +1264,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
[]
else try List.skipn n argsimpls with Failure _ -> [] in
DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
- | None ->
+ | AppUnboundedNotation -> t, [], [], []
+ | NotAppNotation ->
begin match DAst.get f with
| GRef (ref,us) -> f, args, argsscopes, argsimpls
| _ -> t, [], [], []
end
- | _ -> raise No_match in
+ | AppBoundedNotation _ -> raise No_match in
(* Try matching ... *)
let terms,termlists,binders,binderlists =
match_notation_constr !print_universes t pat in
@@ -1469,6 +1480,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 d95554de56..6d4ab8b4d6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -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 =
@@ -1659,12 +1659,12 @@ let drop_notations_pattern looked_for genv =
| None -> DAst.make ?loc @@ RCPatAtom None
| Some (n, head, pl) ->
let pl =
- if get_asymmetric_patterns () then pl else
let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
- List.rev_append pars pl in
+ List.rev_append pars pl
+ in
let (_,argscs) = find_remaining_scopes [] pl head in
let pats = List.map2 (in_pat_sc scopes) argscs pl in
- DAst.make ?loc @@ RCPatCstr(head, [], pats)
+ DAst.make ?loc @@ RCPatCstr(head, pats, [])
end
| CPatCstr (head, None, pl) ->
begin
@@ -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/impargs.ml b/interp/impargs.ml
index c6405b40fc..db102470b0 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -236,7 +236,7 @@ let rec is_rigid_head sigma t = match kind sigma t 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/notation.ml b/interp/notation.ml
index e282d62396..c4e9496b95 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -293,7 +293,12 @@ let key_compare k1 k2 = match k1, k2 with
module KeyOrd = struct type t = key let compare = key_compare end
module KeyMap = Map.Make(KeyOrd)
-type notation_rule = interp_rule * interpretation * int option
+type notation_applicative_status =
+ | AppBoundedNotation of int
+ | AppUnboundedNotation
+ | NotAppNotation
+
+type notation_rule = interp_rule * interpretation * notation_applicative_status
let keymap_add key interp map =
let old = try KeyMap.find key map with Not_found -> [] in
@@ -329,13 +334,14 @@ let cases_pattern_key c = match DAst.get c with
| _ -> Oth
let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
- | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
+ | NApp (NRef ref,args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
| NList (_,_,NApp (NRef ref,args),_,_)
| NBinderList (_,_,NApp (NRef ref,args),_,_) ->
- RefKey (canonical_gr ref), Some (List.length args)
- | NRef ref -> RefKey(canonical_gr ref), None
- | NApp (_,args) -> Oth, Some (List.length args)
- | _ -> Oth, None
+ RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
+ | NRef ref -> RefKey(canonical_gr ref), NotAppNotation
+ | NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
+ | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
+ | _ -> Oth, NotAppNotation
(** Dealing with precedences *)
diff --git a/interp/notation.mli b/interp/notation.mli
index c39bfa6e28..05ddd25a62 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -239,7 +239,12 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit
val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
interpretation * (notation_location * scope_name option)
-type notation_rule = interp_rule * interpretation * int option
+type notation_applicative_status =
+ | AppBoundedNotation of int
+ | AppUnboundedNotation
+ | NotAppNotation
+
+type notation_rule = interp_rule * interpretation * notation_applicative_status
(** Return the possible notations for a given term *)
val uninterp_notations : 'a glob_constr_g -> notation_rule list
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-05-02 10:33:01 +0000