From 26f216653aed171a70513d3f5ece059ab30bcd73 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 4 Oct 2017 23:55:54 +0200 Subject: Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.). This allows e.g. the following to work: Reserved Notation "* a" (at level 70). Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m). We seize this opportunity to make main calls to Metasyntax to depend on an arbitrary env rather than on Global.env. Incidentally, this fixes a little coqdoc bug in classifying the inductive type referred to in the "where" clause. --- vernac/command.ml | 11 +++++------ vernac/metasyntax.ml | 32 ++++++++++++++++---------------- vernac/metasyntax.mli | 11 ++++++----- vernac/obligations.ml | 2 +- vernac/record.ml | 2 +- vernac/vernacentries.ml | 6 +++--- 6 files changed, 32 insertions(+), 32 deletions(-) (limited to 'vernac') diff --git a/vernac/command.ml b/vernac/command.ml index 120f9590f..1668a93f1 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -549,13 +549,12 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in - let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = Metasyntax.with_syntax_protection (fun () -> (* Temporary declaration of notations and scopes *) - List.iter (Metasyntax.set_notation_for_interpretation implsforntn) notations; + List.iter (Metasyntax.set_notation_for_interpretation env_params impls) notations; (* Interpret the constructor types *) List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl) () in @@ -707,7 +706,7 @@ let do_mutual_inductive indl cum poly prv finite = (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) - List.iter Metasyntax.add_notation_interpretation ntns; + List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) @@ -1109,7 +1108,7 @@ let interp_recursive isfix fixl notations = (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = Metasyntax.with_syntax_protection (fun () -> - List.iter (Metasyntax.set_notation_for_interpretation impls) notations; + List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; List.map4 (fun fixctximpenv -> interp_fix_body env_rec evdref (Id.Map.fold Id.Map.add fixctximpenv impls)) fixctximpenvs fixctxs fixl fixccls) @@ -1175,7 +1174,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind fixpoint_message (Some indexes) fixnames; end; (* Declare notations *) - List.iter Metasyntax.add_notation_interpretation ntns + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns = if List.exists Option.is_empty fixdefs then @@ -1206,7 +1205,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n cofixpoint_message fixnames end; (* Declare notations *) - List.iter Metasyntax.add_notation_interpretation ntns + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns let extract_decreasing_argument limit = function | (na,CStructRec) -> na diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 5298ef2e4..587c27209 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1313,7 +1313,7 @@ let to_map l = let fold accu (x, v) = Id.Map.add x v accu in List.fold_left fold Id.Map.empty l -let add_notation_in_scope local df c mods scope = +let add_notation_in_scope local df env c mods scope = let open SynData in let sd = compute_syntax_data df mods in (* Prepare the interpretation *) @@ -1324,7 +1324,7 @@ let add_notation_in_scope local df c mods scope = ninterp_var_type = to_map i_vars; ninterp_rec_vars = to_map sd.recvars; } in - let (acvars, ac, reversible) = interp_notation_constr nenv c in + let (acvars, ac, reversible) = interp_notation_constr env nenv c in let interp = make_interpretation_vars sd.recvars acvars in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in let onlyparse = is_not_printable sd.only_parsing (not reversible) ac in @@ -1344,7 +1344,7 @@ let add_notation_in_scope local df c mods scope = Lib.add_anonymous_leaf (inNotation notation); sd.info -let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = +let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = let dfs = split_notation_string df in let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) @@ -1363,7 +1363,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) ninterp_var_type = to_map i_vars; ninterp_rec_vars = to_map recvars; } in - let (acvars, ac, reversible) = interp_notation_constr ~impls nenv c in + let (acvars, ac, reversible) = interp_notation_constr env ~impls nenv c in let interp = make_interpretation_vars recvars acvars in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in let onlyparse = is_not_printable onlyparse (not reversible) ac in @@ -1390,33 +1390,33 @@ let add_syntax_extension local ((loc,df),mods) = let open SynData in (* Notations with only interpretation *) -let add_notation_interpretation ((loc,df),c,sc) = - let df' = add_notation_interpretation_core false df c sc false false None in +let add_notation_interpretation env ((loc,df),c,sc) = + let df' = add_notation_interpretation_core false df env c sc false false None in Dumpglob.dump_notation (loc,df') sc true -let set_notation_for_interpretation impls ((_,df),c,sc) = +let set_notation_for_interpretation env impls ((_,df),c,sc) = (try ignore - (Flags.silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); + (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ()); with NoSyntaxRule -> user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc (* Main entry point *) -let add_notation local c ((loc,df),modifiers) sc = +let add_notation local env c ((loc,df),modifiers) sc = let df' = if no_syntax_modifiers modifiers then (* No syntax data: try to rely on a previously declared rule *) let onlyparse = is_only_parsing modifiers in let onlyprint = is_only_printing modifiers in let compat = get_compat_version modifiers in - try add_notation_interpretation_core local df c sc onlyparse onlyprint compat + try add_notation_interpretation_core local df env c sc onlyparse onlyprint compat with NoSyntaxRule -> (* Try to determine a default syntax rule *) - add_notation_in_scope local df c modifiers sc + add_notation_in_scope local df env c modifiers sc else (* Declare both syntax and interpretation *) - add_notation_in_scope local df c modifiers sc + add_notation_in_scope local df env c modifiers sc in Dumpglob.dump_notation (loc,df') sc true @@ -1431,13 +1431,13 @@ let add_notation_extra_printing_rule df k v = let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None) -let add_infix local ((loc,inf),modifiers) pr sc = +let add_infix local env ((loc,inf),modifiers) pr sc = check_infix_modifiers modifiers; (* check the precedence *) let metas = [inject_var "x"; inject_var "y"] in let c = mkAppC (pr,metas) in let df = "x "^(quote_notation_token inf)^" y" in - add_notation local c ((loc,df),modifiers) sc + add_notation local env c ((loc,df),modifiers) sc (**********************************************************************) (* Delimiters and classes bound to scopes *) @@ -1493,7 +1493,7 @@ let try_interp_name_alias = function | [], { CAst.v = CRef (ref,_) } -> intern_reference ref | _ -> raise Not_found -let add_syntactic_definition ident (vars,c) local onlyparse = +let add_syntactic_definition env ident (vars,c) local onlyparse = let nonprintable = ref false in let vars,pat = try [], NRef (try_interp_name_alias (vars,c)) @@ -1504,7 +1504,7 @@ let add_syntactic_definition ident (vars,c) local onlyparse = ninterp_var_type = i_vars; ninterp_rec_vars = Id.Map.empty; } in - let nvars, pat, reversible = interp_notation_constr nenv c in + let nvars, pat, reversible = interp_notation_constr env nenv c in let () = nonprintable := not reversible in let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in List.map map vars, pat diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 9cd00cbcb..b3049f1b7 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -11,15 +11,16 @@ open Vernacexpr open Notation open Constrexpr open Notation_term +open Environ val add_token_obj : string -> unit (** Adding a (constr) notation in the environment*) -val add_infix : locality_flag -> (lstring * syntax_modifier list) -> +val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) -> constr_expr -> scope_name option -> unit -val add_notation : locality_flag -> constr_expr -> +val add_notation : locality_flag -> env -> constr_expr -> (lstring * syntax_modifier list) -> scope_name option -> unit val add_notation_extra_printing_rule : string -> string -> string -> unit @@ -33,11 +34,11 @@ val add_class_scope : scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) val add_notation_interpretation : - (lstring * constr_expr * scope_name option) -> unit + env -> (lstring * constr_expr * scope_name option) -> unit (** Add a notation interpretation for supporting the "where" clause *) -val set_notation_for_interpretation : Constrintern.internalization_env -> +val set_notation_for_interpretation : env -> Constrintern.internalization_env -> (lstring * constr_expr * scope_name option) -> unit (** Add only the parsing/printing rule of a notation *) @@ -47,7 +48,7 @@ val add_syntax_extension : (** Add a syntactic definition (as in "Notation f := ...") *) -val add_syntactic_definition : Id.t -> Id.t list * constr_expr -> +val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> bool -> Flags.compat_version option -> unit (** Print the Camlp4 state of a grammar *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 89b18d254..128030f68 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -556,7 +556,7 @@ let declare_mutual_definition l = let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) - List.iter Metasyntax.add_notation_interpretation first.prg_notations; + List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in let kn = match gr with ConstRef kn -> kn | _ -> assert false in diff --git a/vernac/record.ml b/vernac/record.ml index 4fb607dec..bf32cb6e6 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -72,7 +72,7 @@ let interp_fields_evars env evars impls_env nots l = | None -> LocalAssum (i,t') | Some b' -> LocalDef (i,b',t') in - List.iter (Metasyntax.set_notation_for_interpretation impls) no; + List.iter (Metasyntax.set_notation_for_interpretation env impls) no; (EConstr.push_rel d env, impl :: uimpls, d::params, impls)) (env, [], [], impls_env) nots l diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ee84ff101..f05ceb194 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -430,11 +430,11 @@ let vernac_arguments_scope locality r scl = let vernac_infix locality local = let local = enforce_module_locality locality local in - Metasyntax.add_infix local + Metasyntax.add_infix local (Global.env()) let vernac_notation locality local = let local = enforce_module_locality locality local in - Metasyntax.add_notation local + Metasyntax.add_notation local (Global.env()) (***********) (* Gallina *) @@ -953,7 +953,7 @@ let vernac_hints locality poly local lb h = let vernac_syntactic_definition locality lid x local y = Dumpglob.dump_definition lid false "syndef"; let local = enforce_module_locality locality local in - Metasyntax.add_syntactic_definition (snd lid) x local y + Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y let vernac_declare_implicits locality r l = let local = make_section_locality locality in -- cgit v1.2.3