aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrexpr_ops.ml6
-rw-r--r--interp/constrexpr_ops.mli1
-rw-r--r--interp/constrintern.ml36
-rw-r--r--interp/notation.ml25
-rw-r--r--interp/notation.mli4
-rw-r--r--intf/constrexpr.mli8
6 files changed, 47 insertions, 33 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index a592b4cff..542f9feaf 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -263,12 +263,6 @@ let cases_pattern_expr_loc = function
| CPatDelimiters (loc,_,_) -> loc
| CPatCast(loc,_,_) -> loc
-let raw_cases_pattern_expr_loc = function
- | RCPatAlias (loc,_,_) -> loc
- | RCPatCstr (loc,_,_,_) -> loc
- | RCPatAtom (loc,_) -> loc
- | RCPatOr (loc,_) -> loc
-
let local_binder_loc = function
| CLocalAssum ((loc,_)::_,_,t)
| CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index f6d97e107..b547288e3 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -36,7 +36,6 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool
val constr_loc : constr_expr -> Loc.t
val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
val local_binders_loc : local_binder_expr list -> Loc.t
(** {6 Constructors}*)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3f99a3c7c..b18341800 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -900,6 +900,21 @@ let interp_reference vars r =
(**********************************************************************)
(** {5 Cases } *)
+(** Private internalization patterns *)
+type raw_cases_pattern_expr =
+ | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
+ | RCPatCstr of Loc.t * Globnames.global_reference
+ * raw_cases_pattern_expr list * raw_cases_pattern_expr list
+ (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
+ | RCPatAtom of Loc.t * Id.t option
+ | RCPatOr of Loc.t * raw_cases_pattern_expr list
+
+let raw_cases_pattern_expr_loc = function
+ | RCPatAlias (loc,_,_) -> loc
+ | RCPatCstr (loc,_,_,_) -> loc
+ | RCPatAtom (loc,_) -> loc
+ | RCPatOr (loc,_) -> loc
+
(** {6 Elemtary bricks } *)
let apply_scope_env env = function
| [] -> {env with tmp_scope = None}, []
@@ -1198,8 +1213,8 @@ let rec subst_pat_iterator y t p = match p with
| RCPatAtom (_,id) ->
begin match id with Some x when Id.equal x y -> t | _ -> p end
| RCPatCstr (loc,id,l1,l2) ->
- RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
- List.map (subst_pat_iterator y t) l2)
+ RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
+ List.map (subst_pat_iterator y t) l2)
| RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a)
| RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl)
@@ -1216,6 +1231,14 @@ let drop_notations_pattern looked_for =
let test_kind top =
if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
in
+ (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+ let rec rcp_of_glob = function
+ | GVar (loc,id) -> RCPatAtom (loc,Some id)
+ | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
+ | GRef (loc,g,_) -> RCPatCstr (loc, g,[],[])
+ | GApp (loc,GRef (_,g,_),l) -> RCPatCstr (loc, g, List.map rcp_of_glob l,[])
+ | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr ")
+ in
let rec drop_syndef top scopes re pats =
let (loc,qid) = qualid_of_reference re in
try
@@ -1285,8 +1308,9 @@ let drop_notations_pattern looked_for =
let (argscs1,_) = find_remaining_scopes expl_pl pl g in
RCPatCstr (loc, g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
| CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[])
- when Bigint.is_strictly_pos p ->
- fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
+ when Bigint.is_strictly_pos p ->
+ let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in
+ rcp_of_glob pat
| CPatNotation (_,"( _ )",([a],[]),[]) ->
in_pat top scopes a
| CPatNotation (loc, ntn, fullargs,extrargs) ->
@@ -1299,7 +1323,9 @@ let drop_notations_pattern looked_for =
in_not top loc scopes (subst,substlist) extrargs c
| CPatDelimiters (loc, key, e) ->
in_pat top (None,find_delimiters_scope loc key::snd scopes) e
- | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
+ | CPatPrim (loc,p) ->
+ let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes in
+ rcp_of_glob pat
| CPatAtom (loc, Some id) ->
begin
match drop_syndef top scopes id [] with
diff --git a/interp/notation.ml b/interp/notation.ml
index 6aa6f54c0..7be2fe0f0 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -444,16 +444,20 @@ let notation_of_prim_token = function
| Numeral n -> "- "^(to_string (neg n))
| String _ -> raise Not_found
-let find_prim_token g loc p sc =
+let find_prim_token check_allowed loc p sc =
(* Try for a user-defined numerical notation *)
try
let (_,c),df = find_notation (notation_of_prim_token p) sc in
- g (Notation_ops.glob_constr_of_notation_constr loc c),df
+ let pat = Notation_ops.glob_constr_of_notation_constr loc c in
+ check_allowed pat;
+ pat, df
with Not_found ->
(* Try for a primitive numerical notation *)
let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
check_required_module loc sc spdir;
- g (interp ()), ((dirpath (fst spdir),DirPath.empty),"")
+ let pat = interp () in
+ check_allowed pat;
+ pat, ((dirpath (fst spdir),DirPath.empty),"")
let interp_prim_token_gen g loc p local_scopes =
let scopes = make_current_scopes local_scopes in
@@ -466,20 +470,17 @@ let interp_prim_token_gen g loc p local_scopes =
| String s -> str "No interpretation for string " ++ qs s) ++ str ".")
let interp_prim_token =
- interp_prim_token_gen (fun x -> x)
+ interp_prim_token_gen (fun _ -> ())
-(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
-
-let rec rcp_of_glob looked_for = function
- | GVar (loc,id) -> RCPatAtom (loc,Some id)
- | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
- | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[])
+let rec check_allowed_ref_in_pat looked_for = function
+ | GVar _ | GHole _ -> ()
+ | GRef (_,g,_) -> looked_for g
| GApp (loc,GRef (_,g,_),l) ->
- looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[])
+ looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l
| _ -> raise Not_found
let interp_prim_token_cases_pattern_expr loc looked_for p =
- interp_prim_token_gen (rcp_of_glob looked_for) loc p
+ interp_prim_token_gen (check_allowed_ref_in_pat looked_for) loc p
let interp_notation loc ntn local_scopes =
let scopes = make_current_scopes local_scopes in
diff --git a/interp/notation.mli b/interp/notation.mli
index 2e92a00a8..300480ff1 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -85,8 +85,10 @@ val declare_string_interpreter : scope_name -> required_module ->
val interp_prim_token : Loc.t -> prim_token -> local_scopes ->
glob_constr * (notation_location * scope_name option)
+
+(* This function returns a glob_const representing a pattern *)
val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token ->
- local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option)
+ local_scopes -> glob_constr * (notation_location * scope_name option)
(** Return the primitive token associated to a [term]/[cases_pattern];
raise [No_match] if no such token *)
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index a4a6eb909..77f052ddb 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -36,14 +36,6 @@ type prim_token =
| Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *)
| String of string
-type raw_cases_pattern_expr =
- | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
- | RCPatCstr of Loc.t * Globnames.global_reference
- * raw_cases_pattern_expr list * raw_cases_pattern_expr list
- (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *)
- | RCPatAtom of Loc.t * Id.t option
- | RCPatOr of Loc.t * raw_cases_pattern_expr list
-
type instance_expr = Misctypes.glob_level list
type cases_pattern_expr =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 07:12:44 +0000