From 29b75ca42b7824f5feec24df5ecc7cd75cb78251 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 23 Dec 2005 10:43:37 +0000 Subject: Simplifification de vernac_expr li l'abandon du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/parse.ml | 1 - contrib/interface/xlate.ml | 15 ++++------- interp/notation.ml | 23 ++++++++--------- interp/notation.mli | 9 +++---- parsing/egrammar.ml | 41 ++++++++++++----------------- parsing/egrammar.mli | 8 +++--- parsing/g_vernacnew.ml4 | 8 +++--- toplevel/metasyntax.ml | 64 ++++++++++++++-------------------------------- toplevel/metasyntax.mli | 35 +++++++++---------------- toplevel/vernacentries.ml | 21 ++++----------- toplevel/vernacexpr.ml | 18 ++++--------- translate/ppvernacnew.ml | 39 +++++----------------------- 12 files changed, 90 insertions(+), 192 deletions(-) diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index a6a8937ba5..7728cf48ab 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -96,7 +96,6 @@ let execute_when_necessary ast = let execute_when_necessary v = (match v with - | VernacGrammar _ -> Vernacentries.interp v | VernacOpenCloseScope sc -> Vernacentries.interp v | VernacRequire (_,_,l) -> (try diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 69c6674d3a..54508443da 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1954,8 +1954,6 @@ let rec xlate_vernac = CT_require(ct_impexp, ct_spec, CT_coerce_STRING_to_ID_NE_LIST_OR_STRING(CT_string filename)) - | VernacSyntax (phylum, l) -> xlate_error "SYNTAX not implemented" - | VernacOpenCloseScope(true, true, s) -> CT_local_open_scope(CT_ident s) | VernacOpenCloseScope(false, true, s) -> CT_open_scope(CT_ident s) | VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s) @@ -1977,8 +1975,7 @@ let rec xlate_vernac = CT_id_ne_list(xlate_class_rawexpr a, List.map xlate_class_rawexpr l)) | VernacBindScope(id, []) -> assert false - | VernacNotation(b, c, None, _, _) -> assert false - | VernacNotation(b, c, Some(s,modif_list), _, opt_scope) -> + | VernacNotation(b, c, (s,modif_list), opt_scope) -> let translated_s = CT_string s in let formula = xlate_formula c in let translated_modif_list = @@ -1992,7 +1989,7 @@ let rec xlate_vernac = else CT_define_notation(translated_s, formula, translated_modif_list, translated_scope) - | VernacSyntaxExtension(b,Some(s,modif_list), None) -> + | VernacSyntaxExtension(b,(s,modif_list)) -> let translated_s = CT_string s in let translated_modif_list = CT_modifier_list(List.map xlate_syntax_modifier modif_list) in @@ -2000,8 +1997,7 @@ let rec xlate_vernac = CT_local_reserve_notation(translated_s, translated_modif_list) else CT_reserve_notation(translated_s, translated_modif_list) - | VernacSyntaxExtension(_, _, _) -> assert false - | VernacInfix (b,(str,modl),id,_, opt_scope) -> + | VernacInfix (b,(str,modl),id, opt_scope) -> let id1 = loc_qualid_to_ct_ID id in let modl1 = CT_modifier_list(List.map xlate_syntax_modifier modl) in let s = CT_string str in @@ -2012,7 +2008,6 @@ let rec xlate_vernac = CT_local_infix(s, id1,modl1, translated_scope) else CT_infix(s, id1,modl1, translated_scope) - | VernacGrammar _ -> xlate_error "GRAMMAR not implemented" | VernacCoercion (s, id1, id2, id3) -> let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in let local_opt = @@ -2126,8 +2121,8 @@ let rec xlate_vernac = | (VernacGlobalCheck _|VernacPrintOption _| VernacMemOption (_, _)|VernacRemoveOption (_, _) | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _| - VernacSolveExistential (_, _)|VernacCanonical _ | VernacDistfix _| - VernacTacticGrammar _) + VernacSolveExistential (_, _)|VernacCanonical _ | + VernacTacticNotation _) -> xlate_error "TODO: vernac";; let rec xlate_vernac_list = diff --git a/interp/notation.ml b/interp/notation.ml index 7874f95b38..f116f292c3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -44,7 +44,7 @@ type level = precedence * tolerability list type delimiters = string type scope = { - notations: (interpretation * (dir_path * string) * bool) Stringmap.t; + notations: (interpretation * (dir_path * string)) Stringmap.t; delimiters: delimiters option } @@ -270,13 +270,13 @@ let level_of_notation ntn = (* The mapping between notations and their interpretation *) -let declare_notation_interpretation ntn scopt pat df pp8only = +let declare_notation_interpretation ntn scopt pat df = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in if Stringmap.mem ntn sc.notations && Options.is_verbose () then warning ("Notation "^ntn^" was already used"^ (if scopt = None then "" else " in scope "^scope)); - let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in + let sc = { sc with notations = Stringmap.add ntn (pat,df) sc.notations } in scope_map := Stringmap.add scope sc !scope_map; if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack @@ -296,8 +296,7 @@ let rec find_interpretation f = function let rec interp_notation loc ntn scopes = let f sc = let scope = find_scope sc in - let (pat,df,pp8only) = Stringmap.find ntn scope.notations in - if pp8only then raise Not_found; + let (pat,df) = Stringmap.find ntn scope.notations in pat,(df,if sc = default_scope then None else Some sc) in try find_interpretation f (List.fold_right push_scope scopes !scope_stack) with Not_found -> @@ -361,9 +360,9 @@ let exists_notation_in_scope scopt ntn r = let scope = match scopt with Some s -> s | None -> default_scope in try let sc = Stringmap.find scope !scope_map in - let (r',_,pp8only) = Stringmap.find ntn sc.notations in - r' = r, pp8only - with Not_found -> false, false + let (r',_) = Stringmap.find ntn sc.notations in + r' = r + with Not_found -> false (**********************************************************************) (* Mapping classes to scopes *) @@ -506,7 +505,7 @@ let pr_named_scope prraw scope sc = ++ fnl () ++ pr_scope_classes scope ++ Stringmap.fold - (fun ntn ((_,r),(_,df),_) strm -> + (fun ntn ((_,r),(_,df)) strm -> pr_notation_info prraw df r ++ fnl () ++ strm) sc.notations (mt ()) @@ -544,7 +543,7 @@ let browse_notation ntn map = let l = Stringmap.fold (fun scope_name sc -> - Stringmap.fold (fun ntn ((_,r),df,_) l -> + Stringmap.fold (fun ntn ((_,r),df) l -> if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations) map [] in let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in @@ -572,7 +571,7 @@ let locate_notation prraw ntn = let collect_notation_in_scope scope sc known = assert (scope <> default_scope); Stringmap.fold - (fun ntn ((_,r),(_,df),_) (l,known as acc) -> + (fun ntn ((_,r),(_,df)) (l,known as acc) -> if List.mem ntn known then acc else ((df,r)::l,ntn::known)) sc.notations ([],known) @@ -588,7 +587,7 @@ let collect_notations stack = | SingleNotation ntn -> if List.mem ntn knownntn then (all,knownntn) else - let ((_,r),(_,df),_) = + let ((_,r),(_,df)) = Stringmap.find ntn (find_scope default_scope).notations in let all' = match all with | (s,lonelyntn)::rest when s = default_scope -> diff --git a/interp/notation.mli b/interp/notation.mli index 0e401acd6e..896d427932 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -88,7 +88,7 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of kernel_name val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> dir_path * string -> bool -> unit + interpretation -> dir_path * string -> unit val declare_uninterpretation : interp_rule -> interpretation -> unit @@ -111,15 +111,14 @@ val availability_of_notation : scope_name option * notation -> scopes -> (*s Declare and test the level of a (possibly uninterpreted) notation *) -val declare_notation_level : notation -> level option * level -> unit -val level_of_notation : notation -> level option * level - (* raise [Not_found] if no level *) +val declare_notation_level : notation -> level -> unit +val level_of_notation : notation -> level (* raise [Not_found] if no level *) (*s** Miscellaneous *) (* Checks for already existing notations *) val exists_notation_in_scope : scope_name option -> notation -> - interpretation -> bool * bool + interpretation -> bool (* Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope: global_reference -> scope_name option list -> unit diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index e0d877b66e..be8b1e8ad8 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -21,16 +21,14 @@ open Nameops (* State of the grammar extensions *) type notation_grammar = - int * Gramext.g_assoc option * notation * prod_item list * int list option + int * Gramext.g_assoc option * notation * prod_item list type all_grammar_command = | Notation of Notation.level * notation_grammar | Grammar of grammar_command - | TacticGrammar of - int * - (string * grammar_production list * - (Names.dir_path * Tacexpr.glob_tactic_expr)) - list + | TacticGrammar of + (string * int * grammar_production list * + (Names.dir_path * Tacexpr.glob_tactic_expr)) let (grammar_state : all_grammar_command list ref) = ref [] @@ -318,12 +316,8 @@ let extend_constr entry (n,assoc,pos,p4assoc,name) make_act (forpat,pt) = let act = make_act ntl in grammar_extend entry pos [(name, p4assoc, [symbs, act])] -let extend_constr_notation (n,assoc,ntn,rule,permut) = - let mkact = - match permut with - None -> (fun loc env -> CNotation (loc,ntn,List.map snd env)) - | Some p -> (fun loc env -> - CNotation (loc,ntn,List.map (fun i -> snd (List.nth env i)) p)) in +let extend_constr_notation (n,assoc,ntn,rule) = + let mkact loc env = CNotation (loc,ntn,List.map snd env) in let (e,level,keepassoc) = get_constr_entry false (ETConstr (n,())) in let pos,p4assoc,name = find_position false keepassoc assoc level in extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name) @@ -438,34 +432,31 @@ let get_tactic_entry n = open Tacexpr -let head_is_ident = function (_,VTerm _::_,_) -> true | _ -> false +let head_is_ident = function VTerm _::_ -> true | _ -> false -let add_tactic_entries (lev,gl) = +let add_tactic_entry (key,lev,prods,tac) = let univ = get_univ "tactic" in let entry, pos = get_tactic_entry lev in let rules = if lev = 0 then begin - if not (List.for_all head_is_ident gl) then - error "Notations for simple tactics must start with an identifier"; + if not (head_is_ident prods) then + error "Notation for simple tactic must start with an identifier"; let make_act s tac loc l = (TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in - let f (s,l,tac) = - make_rule univ (make_act s tac) (make_vprod_item lev "tactic") l in - List.map f gl end + make_rule univ (make_act key tac) (make_vprod_item lev "tactic") prods + end else let make_act s tac loc l = (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in - let f (s,l,tac) = - make_rule univ (make_act s tac) (make_vprod_item lev "tactic") l in - List.map f gl in + make_rule univ (make_act key tac) (make_vprod_item lev "tactic") prods in let _ = find_position true true None None (* to synchronise with remove *) in - grammar_extend entry pos [(None, None, List.rev rules)] + grammar_extend entry pos [(None, None, List.rev [rules])] let extend_grammar gram = (match gram with | Notation (_,a) -> extend_constr_notation a | Grammar g -> extend_grammar_rules g - | TacticGrammar (n,l) -> add_tactic_entries (n,l)); + | TacticGrammar g -> add_tactic_entry g); grammar_state := gram :: !grammar_state let reset_extend_grammars_v8 () = @@ -478,7 +469,7 @@ let reset_extend_grammars_v8 () = let recover_notation_grammar ntn prec = let l = map_succeed (function - | Notation (prec',(_,_,ntn',_,_ as x)) when prec = prec' & ntn = ntn' -> x + | Notation (prec',(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> x | _ -> failwith "") !grammar_state in assert (List.length l = 1); List.hd l diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 54e0695123..06ab2b42fb 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -21,16 +21,14 @@ open Mod_subst (*i*) type notation_grammar = - int * Gramext.g_assoc option * notation * prod_item list * int list option + int * Gramext.g_assoc option * notation * prod_item list type all_grammar_command = | Notation of (precedence * tolerability list) * notation_grammar | Grammar of grammar_command | TacticGrammar of - int * - (string * grammar_production list * - (Names.dir_path * Tacexpr.glob_tactic_expr)) - list + (string * int * grammar_production list * + (Names.dir_path * Tacexpr.glob_tactic_expr)) val extend_grammar : all_grammar_command -> unit diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 70f28a2787..21aa0c732d 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -685,22 +685,22 @@ GEXTEND Gram op = ne_string; ":="; p = global; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacInfix (local,(op,modl),p,None,sc) + VernacInfix (local,(op,modl),p,sc) | IDENT "Notation"; local = locality; id = ident; ":="; c = constr; b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] -> VernacSyntacticDefinition (id,c,local,b) | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacNotation (local,c,Some(s,modl),None,sc) + VernacNotation (local,c,(s,modl),sc) | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; pil = LIST1 production_item; ":="; t = Tactic.tactic - -> VernacTacticGrammar (n,["",pil,t]) + -> VernacTacticNotation (n,pil,t) | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (local,Some(s,l),None) + -> VernacSyntaxExtension (local,(s,l)) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 8d4f3b83f4..24bee11e12 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -88,19 +88,15 @@ let rec make_tags lev = function etyp :: make_tags lev l | [] -> [] -let declare_tactic_pprule n (s,t,p) = - Pptactic.declare_extra_tactic_pprule true s (t,p); - Pptactic.declare_extra_tactic_pprule false s (t,p) +let cache_tactic_notation (_,(pa,pp)) = + Egrammar.extend_grammar (Egrammar.TacticGrammar pa); + Pptactic.declare_extra_tactic_pprule true (pi1 pp) (pi2 pp, pi3 pp) -let cache_tactic_notation (_,((n,pa),pp)) = - Egrammar.extend_grammar (Egrammar.TacticGrammar (n,pa)); - List.iter (declare_tactic_pprule n) pp +let subst_tactic_parule subst (key,n,p,(d,tac)) = + (key,n,p,(d,Tacinterp.subst_tactic subst tac)) -let subst_one_tactic_notation subst (s,p,(d,tac)) = - (s,p,(d,Tacinterp.subst_tactic subst tac)) - -let subst_tactic_notation (_,subst,((n,pa),pp)) = - ((n,List.map (subst_one_tactic_notation subst) pa),pp) +let subst_tactic_notation (_,subst,(pa,pp)) = + (subst_tactic_parule subst pa,pp) let (inTacticGrammar, outTacticGrammar) = declare_object {(default_object "TacticGrammar") with @@ -123,23 +119,14 @@ let rec next_key_away key t = if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t else key -let make_tactic_pprule n s prods = +let add_tactic_notation (n,prods,e) = let tags = make_tags n prods in - let s = if s="" then next_key_away (tactic_notation_key prods) tags else s in - (s, tags, (n,List.map make_terminal_status prods)) - -let make_tactic_parule s prods e = + let key = next_key_away (tactic_notation_key prods) tags in + let pprule = (key,tags,(n,List.map make_terminal_status prods)) in let ids = List.fold_left cons_production_parameter [] prods in let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in - (s,prods,(Lib.cwd (),tac)) - -let locate_tactic_body n (s,prods,e) = - let (s',t,p as pp) = make_tactic_pprule n s prods in - (make_tactic_parule s' prods e, pp) - -let add_tactic_notation (n,g) = - let pa,pp = List.split (List.map (locate_tactic_body n) g) in - Lib.add_anonymous_leaf (inTacticGrammar ((n,pa),pp)) + let parule = (key,n,prods,(Lib.cwd(),tac)) in + Lib.add_anonymous_leaf (inTacticGrammar (parule,pprule)) (**********************************************************************) (* Printing grammar entries *) @@ -631,7 +618,7 @@ let recompute_assoc typs = let make_grammar_rule (n,typs,symbols,_) ntn = let assoc = recompute_assoc typs in let prod = make_production typs symbols in - (n,assoc,ntn,prod,None) + (n,assoc,ntn,prod) let make_pp_rule (n,typs,symbols,fmt) = match fmt with @@ -654,7 +641,7 @@ let pr_level ntn (from,args) = let cache_syntax_extension (_,(_,(prec,ntn,gr,pp))) = try - let _, oldprec = Notation.level_of_notation ntn in + let oldprec = Notation.level_of_notation ntn in if prec <> oldprec then errorlabstrm "" (str ("Notation "^ntn^" is already defined") ++ spc() ++ @@ -663,7 +650,7 @@ let cache_syntax_extension (_,(_,(prec,ntn,gr,pp))) = pr_level ntn prec); with Not_found -> (* Reserve the notation level *) - Notation.declare_notation_level ntn (None,prec); + Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) Egrammar.extend_grammar (Egrammar.Notation (prec,gr)); (* Declare the printing rule *) @@ -869,10 +856,10 @@ let load_notation _ (_,(_,scope,pat,onlyparse,_)) = let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) = if i=1 then begin - let exists,_ = Notation.exists_notation_in_scope scope ntn pat in + let exists = Notation.exists_notation_in_scope scope ntn pat in (* Declare the interpretation *) if not exists then - Notation.declare_notation_interpretation ntn scope pat df false; + Notation.declare_notation_interpretation ntn scope pat df; if not exists & not onlyparse then Notation.declare_uninterpretation (NotationRule (scope,ntn)) pat end @@ -929,7 +916,7 @@ let level_rule (n,p) = if p = E then n else max (n-1) 0 let recover_syntax ntn = try - let _,prec = Notation.level_of_notation ntn in + let prec = Notation.level_of_notation ntn in let pprule,_ = Notation.find_notation_printing_rule ntn in let gr = Egrammar.recover_notation_grammar ntn prec in Some (prec,ntn,gr,pprule) @@ -1022,7 +1009,7 @@ let add_infix local (inf,modl) pr sc = else add_notation_in_scope local df a modl sc toks -let standardise_locatable_notation ntn = +let standardize_locatable_notation ntn = let unquote = function | String s -> [unquote_notation_token s] | _ -> [] in @@ -1070,16 +1057,3 @@ let add_delimiters scope key = let add_class_scope scope cl = Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl)) - - -(* Temporary compatibility *) - -let translate_distfix _ = failwith "No more v7 support 1" -let add_distfix _ = failwith "No more v7 support 2" -let add_tactic_grammar = add_tactic_notation -let add_grammar_obj _ = failwith "No more v7 support 4" -let add_syntax_obj _ = failwith "No more v7 support 5" - -let add_syntax_extension local mv _ = add_syntax_extension local (out_some mv) -let add_notation local c x _ sc = add_notation local c (out_some x) sc -let add_infix local x pr _ sc = add_infix local x pr sc diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 243b6345fd..869ba00d0f 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -19,38 +19,27 @@ open Notation open Topconstr (*i*) -(* Adding grammar and pretty-printing objects in the environment *) +(* Adding parsing and pretty-printing rules in the environment *) -val add_syntax_obj : string -> raw_syntax_entry list -> unit - -val add_grammar_obj : string -> raw_grammar_entry list -> unit val add_token_obj : string -> unit -val add_tactic_grammar : - int * (string * grammar_production list * raw_tactic_expr) list -> unit + +val add_tactic_notation : + int * grammar_production list * raw_tactic_expr -> unit val add_infix : locality_flag -> (string * syntax_modifier list) -> - reference -> (string * syntax_modifier list) option -> - scope_name option -> unit -val add_distfix : locality_flag -> - grammar_associativity -> precedence -> string -> reference - -> scope_name option -> unit -val translate_distfix : grammar_associativity -> string -> reference -> - Gramext.g_assoc * string * constr_expr + reference -> scope_name option -> unit val add_delimiters : scope_name -> string -> unit val add_class_scope : scope_name -> Classops.cl_typ -> unit -val add_notation : locality_flag -> constr_expr - -> (string * syntax_modifier list) option - -> (string * syntax_modifier list) option - -> scope_name option -> unit +val add_notation : locality_flag -> constr_expr -> + (string * syntax_modifier list) -> scope_name option -> unit -val add_notation_interpretation : string -> Constrintern.implicits_env - -> constr_expr -> scope_name option -> unit +val add_notation_interpretation : string -> Constrintern.implicits_env -> + constr_expr -> scope_name option -> unit -val add_syntax_extension : locality_flag - -> (string * syntax_modifier list) option - -> (string * syntax_modifier list) option -> unit +val add_syntax_extension : + locality_flag -> (string * syntax_modifier list) -> unit val print_grammar : string -> string -> unit @@ -60,4 +49,4 @@ val merge_modifiers : Gramext.g_assoc option -> int option -> val interp_infix_modifiers : syntax_modifier list -> Gramext.g_assoc option * precedence option * bool * string located option -val standardise_locatable_notation : string -> string +val standardize_locatable_notation : string -> string diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a93e6fd5e6..fb9bb44967 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -280,10 +280,6 @@ let print_located_module r = (**********) (* Syntax *) -let vernac_syntax = Metasyntax.add_syntax_obj - -let vernac_grammar = Metasyntax.add_grammar_obj - let vernac_syntax_extension = Metasyntax.add_syntax_extension let vernac_delimiters = Metasyntax.add_delimiters @@ -298,8 +294,6 @@ let vernac_arguments_scope qid scl = let vernac_infix = Metasyntax.add_infix -let vernac_distfix = Metasyntax.add_distfix - let vernac_notation = Metasyntax.add_notation (***********) @@ -974,7 +968,7 @@ let vernac_locate = function | LocateFile f -> locate_file f | LocateNotation ntn -> ppnl (Notation.locate_notation (Constrextern.without_symbols pr_rawterm) - (Metasyntax.standardise_locatable_notation ntn)) + (Metasyntax.standardize_locatable_notation ntn)) (********************) (* Proof management *) @@ -1108,19 +1102,14 @@ let interp c = match c with | (VernacV7only _ | VernacV8only _) -> assert false (* Syntax *) - | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel - | VernacTacticGrammar (n,al) -> Metasyntax.add_tactic_grammar (n,al) - | VernacGrammar (univ,al) -> vernac_grammar univ al - | VernacSyntaxExtension (lcl,sl,l8) -> vernac_syntax_extension lcl sl l8 + | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e) + | VernacSyntaxExtension (lcl,sl) -> vernac_syntax_extension lcl sl | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl | VernacOpenCloseScope sc -> vernac_open_close_scope sc | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl - | VernacInfix (local,mv,qid,mv8,sc) -> vernac_infix local mv qid mv8 sc - | VernacDistfix (local,assoc,n,inf,qid,sc) -> - vernac_distfix local assoc n inf qid sc - | VernacNotation (local,c,infpl,mv8,sc) -> - vernac_notation local c infpl mv8 sc + | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc + | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc (* Gallina *) | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index e62288d16d..ab05f7d0df 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -172,25 +172,17 @@ type vernac_expr = | VernacVar of lident (* Syntax *) - | VernacGrammar of lstring * raw_grammar_entry list - | VernacTacticGrammar of int * - (lstring * grammar_production list * raw_tactic_expr) list - | VernacSyntax of lstring * raw_syntax_entry list - | VernacSyntaxExtension of locality_flag * - (lstring * syntax_modifier list) option - * (lstring * syntax_modifier list) option - | VernacDistfix of locality_flag * - grammar_associativity * precedence * lstring * lreference * - scope_name option + | VernacTacticNotation of int * grammar_production list * raw_tactic_expr + | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list) | VernacOpenCloseScope of (locality_flag * bool * scope_name) | VernacDelimiters of scope_name * lstring | VernacBindScope of scope_name * class_rawexpr list | VernacArgumentsScope of lreference * scope_name option list | VernacInfix of locality_flag * (lstring * syntax_modifier list) * - lreference * (lstring * syntax_modifier list) option * scope_name option + lreference * scope_name option | VernacNotation of - locality_flag * constr_expr * (lstring * syntax_modifier list) option * - (lstring * syntax_modifier list) option * scope_name option + locality_flag * constr_expr * (lstring * syntax_modifier list) * + scope_name option (* Gallina *) | VernacDefinition of definition_kind * lident * definition_expr * diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 154d23c38d..77b523333f 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -403,7 +403,7 @@ let pr_syntax_modifiers = function let print_level n = if n <> 0 then str " (at level " ++ int n ++ str ")" else mt () -let pr_grammar_tactic_rule n (name,pil,t) = +let pr_grammar_tactic_rule n (_,pil,t) = hov 2 (str "Tactic Notation" ++ print_level n ++ spc() ++ hov 0 (prlist_with_sep sep pr_production_item pil ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) @@ -520,21 +520,7 @@ let rec pr_vernac = function | VernacVar id -> pr_lident id (* Syntax *) - | VernacGrammar _ -> - msgerrnl (str"Warning : constr Grammar is discontinued; use Notation"); - str"(* : Grammar is replaced by Notation *)" - | VernacTacticGrammar (n,l) -> - prlist_with_sep (fun () -> sep_end() ++ fnl()) - (pr_grammar_tactic_rule n) l - | VernacSyntax (u,el) -> - msgerrnl (str"Warning : Syntax is discontinued; use Notation"); - str"(* : Syntax is discontinued" ++ -(* - fnl () ++ - hov 1 (str"Syntax " ++ str u ++ spc() ++ - prlist_with_sep sep_v2 pr_syntax_entry el) ++ -*) - str " *)" + | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e) | VernacOpenCloseScope (local,opening,sc) -> str (if opening then "Open " else "Close ") ++ pr_locality local ++ str "Scope" ++ spc() ++ str sc @@ -548,23 +534,14 @@ let rec pr_vernac = function | None -> str"_" | Some sc -> str sc in str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - | VernacInfix (local,(s,_),q,ov8,sn) -> (* A Verifier *) - let s,mv8 = match ov8 with Some smv8 -> smv8 | None -> (s,[]) in + | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *) hov 0 (hov 0 (str"Infix " ++ pr_locality local ++ qsnew s ++ str " :=" ++ spc() ++ pr_reference q) ++ - pr_syntax_modifiers mv8 ++ + pr_syntax_modifiers mv ++ (match sn with | None -> mt() | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) - | VernacDistfix (local,a,p,s,q,sn) -> - hov 0 (str"Distfix " ++ pr_locality local ++ pr_entry_prec a ++ int p - ++ spc() ++ qsnew s ++ spc() ++ pr_reference q ++ (match sn with - | None -> mt() - | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) - | VernacNotation (local,c,sl,mv8,opt) -> - let (s,l) = match mv8 with - None -> fst (out_some sl), [] - | Some ml -> ml in + | VernacNotation (local,c,(s,l),opt) -> let ps = let n = String.length s in if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' @@ -577,10 +554,7 @@ let rec pr_vernac = function (match opt with | None -> mt() | Some sc -> str" :" ++ spc() ++ str sc)) - | VernacSyntaxExtension (local,sl,mv8) -> - let (s,l) = match mv8 with - None -> out_some sl - | Some ml -> ml in + | VernacSyntaxExtension (local,(s,l)) -> str"Reserved Notation" ++ spc() ++ pr_locality local ++ qsnew s ++ pr_syntax_modifiers l @@ -1132,7 +1106,6 @@ let pr_vernac = function (* Pour ceux qui ont utilisé la couche "Import *_scope" de compat *) let a = Names.string_of_id a in a = "nat_scope" or a = "Z_scope" or a = "R_scope" -> mt() - | VernacSyntax _ | VernacGrammar _ as x -> pr_vernac x | VernacPrint PrintLocalContext -> warning ("\"Print.\" is discontinued"); mt () -- cgit v1.2.3