From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Tue, 25 Apr 2017 14:31:15 +0200 Subject: Fix 4.04 warnings --- interp/notation.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 90ac7f729..6aa6f54c0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -22,7 +22,6 @@ open Glob_ops open Ppextend open Context.Named.Declaration -module NamedDecl = Context.Named.Declaration (*i*) (*s A scope is a set of notations; it includes -- cgit v1.2.3 From b643916aed4093eb7f21116aaef726cab561bc27 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 15 May 2017 01:10:54 +0200 Subject: [interp] [ast] Make raw_cases_pattern_expr private. The type `raw_cases_pattern_expr` is used only in the interpretation of notation patterns. Indeed, this should be a private type thus we make it local to `Constrintern`; it makes no sense to expose it in the public AST. The patch is routine, except for the case used to interpret primitives in patterns. We now return a `glob_constr` representing the raw pattern, instead of the private raw pattern type. This could be further refactored but have opted to be conservative here. This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754 , see the commentaries there for more information about `raw_cases_pattern_expr`. --- interp/constrexpr_ops.ml | 6 ------ interp/constrexpr_ops.mli | 1 - interp/constrintern.ml | 36 +++++++++++++++++++++++++++++++----- interp/notation.ml | 25 +++++++++++++------------ interp/notation.mli | 4 +++- intf/constrexpr.mli | 8 -------- 6 files changed, 47 insertions(+), 33 deletions(-) (limited to 'interp/notation.ml') 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 = -- cgit v1.2.3