diff options
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 1100 |
1 files changed, 312 insertions, 788 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 4c554209..92ce6e36 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,120 +6,27 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml,v 1.105.2.12 2006/01/04 20:31:16 herbelin Exp $ *) +(* $Id: metasyntax.ml 7822 2006-01-08 17:14:56Z herbelin $ *) open Pp open Util open Names open Topconstr -open Coqast -open Ast open Ppextend open Extend -open Esyntax open Libobject -open Library open Summary open Constrintern open Vernacexpr open Pcoq open Rawterm open Libnames - -let interp_global_rawconstr_with_vars vars c = - interp_rawconstr_gen false Evd.empty (Global.env()) false (vars,[]) c - -(**********************************************************************) -(* Parsing via ast (used in Zsyntax) *) - -(* This updates default parsers for Grammar actions and Syntax *) -(* patterns by inserting globalization *) -(* Done here to get parsing/g_*.ml4 non dependent from kernel *) -let constr_to_ast a = - Termast.ast_of_rawconstr (interp_rawconstr Evd.empty (Global.env()) a) - -(* This installs default quotations parsers to escape the ast parser *) -(* "constr" is used by default in quotations found in the ast parser *) -let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr - -let _ = define_ast_quotation true "constr" constr_parser_with_glob +open Lexer +open Egrammar +open Notation (**********************************************************************) -(* Globalisation for constr_expr *) - -let globalize_ref vars ref = - match Constrintern.interp_reference (vars,[]) ref with - | RRef (loc,VarRef a) -> Ident (loc,a) - | RRef (loc,a) -> Qualid (loc,qualid_of_sp (Nametab.sp_of_global a)) - | RVar (loc,x) -> Ident (loc,x) - | _ -> anomaly "globalize_ref: not a reference" - -let globalize_ref_term vars ref = - match Constrintern.interp_reference (vars,[]) ref with - | RRef (loc,VarRef a) -> CRef (Ident (loc,a)) - | RRef (loc,a) -> CRef (Qualid (loc,qualid_of_sp (Nametab.sp_of_global a))) - | RVar (loc,x) -> CRef (Ident (loc,x)) - | c -> Constrextern.extern_rawconstr Idset.empty c - -let rec globalize_constr_expr vars = function - | CRef ref -> globalize_ref_term vars ref - | CAppExpl (_,(p,ref),l) -> - let f = - map_constr_expr_with_binders globalize_constr_expr - (fun x e -> e) vars - in - CAppExpl (dummy_loc,(p,globalize_ref vars ref), List.map f l) - | c -> - map_constr_expr_with_binders globalize_constr_expr (fun id e -> id::e) - vars c - -let without_translation f x = - let old = Options.do_translate () in - let oldv7 = !Options.v7 in - Options.make_translate false; - try let r = f x in Options.make_translate old; Options.v7:=oldv7; r - with e -> Options.make_translate old; Options.v7:=oldv7; raise e - -let _ = set_constr_globalizer - (fun vars e -> for_grammar (without_translation (globalize_constr_expr vars)) e) - -(**********************************************************************) -(** For old ast printer *) - -(* Pretty-printer state summary *) -let _ = - declare_summary "syntax" - { freeze_function = Esyntax.freeze; - unfreeze_function = Esyntax.unfreeze; - init_function = Esyntax.init; - survive_module = false; - survive_section = false } - -(* Pretty-printing objects = syntax_entry *) -let cache_syntax (_,ppobj) = Esyntax.add_ppobject ppobj - -let subst_syntax (_,subst,ppobj) = - Extend.subst_syntax_command Ast.subst_astpat subst ppobj - -let (inPPSyntax,outPPSyntax) = - declare_object {(default_object "PPSYNTAX") with - open_function = (fun i o -> if i=1 then cache_syntax o); - cache_function = cache_syntax; - subst_function = subst_syntax; - classify_function = (fun (_,o) -> Substitute o); - export_function = (fun x -> Some x) } - -(* Syntax extension functions (registered in the environnement) *) - -(* Checking the pretty-printing rules against free meta-variables. - * Note that object are checked before they are added in the environment. - * Syntax objects in compiled modules are not re-checked. *) - -let add_syntax_obj whatfor sel = -(* if not !Options.v7_only then*) - Lib.add_anonymous_leaf (inPPSyntax (interp_syntax_entry whatfor sel)) - -(* Tokens *) +(* Tokens *) let cache_token (_,s) = Pcoq.lexer.Token.using ("", s) @@ -134,69 +41,40 @@ let (inToken, outToken) = let add_token_obj s = Lib.add_anonymous_leaf (inToken s) (**********************************************************************) -(* Grammars (especially Tactic Notation) *) +(* Tactic Notation *) let make_terminal_status = function | VTerm s -> Some s | VNonTerm _ -> None -let qualified_nterm current_univ = function - | NtQual (univ, en) -> (univ, en) - | NtShort en -> (current_univ, en) - -let rec make_tags = function - | VTerm s :: l -> make_tags l +let rec make_tags lev = function + | VTerm s :: l -> make_tags lev l | VNonTerm (loc, nt, po) :: l -> - let (u,nt) = qualified_nterm "tactic" nt in - let (etyp, _) = Egrammar.interp_entry_name u nt in - etyp :: make_tags l + let (etyp, _) = Egrammar.interp_entry_name lev "tactic" nt in + etyp :: make_tags lev l | [] -> [] -let declare_pprule = function - (* Pretty-printing rules only for Grammar (Tactic Notation) *) - | Egrammar.TacticGrammar (_,pp) -> - let f (s,t,p) = - Pptactic.declare_extra_tactic_pprule true s (t,p); - Pptactic.declare_extra_tactic_pprule false s (t,p) in - List.iter f pp - | _ -> () +let cache_tactic_notation (_,(pa,pp)) = + Egrammar.extend_grammar (Egrammar.TacticGrammar pa); + Pptactic.declare_extra_tactic_pprule pp -let cache_grammar (_,a) = - Egrammar.extend_grammar a; - declare_pprule a +let subst_tactic_parule subst (key,n,p,(d,tac)) = + (key,n,p,(d,Tacinterp.subst_tactic subst tac)) -let subst_grammar (_,subst,a) = - Egrammar.subst_all_grammar_command subst a +let subst_tactic_notation (_,subst,(pa,pp)) = + (subst_tactic_parule subst pa,pp) -let (inGrammar, outGrammar) = - declare_object {(default_object "GRAMMAR") with - open_function = (fun i o -> if i=1 then cache_grammar o); - cache_function = cache_grammar; - subst_function = subst_grammar; +let (inTacticGrammar, outTacticGrammar) = + declare_object {(default_object "TacticGrammar") with + open_function = (fun i o -> if i=1 then cache_tactic_notation o); + cache_function = cache_tactic_notation; + subst_function = subst_tactic_notation; classify_function = (fun (_,o) -> Substitute o); export_function = (fun x -> Some x)} -(**********************************************************************) -(* V7 Grammar *) - -open Genarg - -let check_entry_type (u,n) = - if u = "tactic" or u = "vernac" then error "tactic and vernac not supported"; - match entry_type (get_univ u) n with - | None -> Pcoq.create_entry_if_new (get_univ u) n ConstrArgType - | Some (ConstrArgType | IdentArgType | RefArgType) -> () - | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries" - -let add_grammar_obj univ entryl = - let u = create_univ_if_new univ in - let g = interp_grammar_command univ check_entry_type entryl in - Lib.add_anonymous_leaf (inGrammar (Egrammar.Grammar g)) - -(**********************************************************************) -(* V8 Grammar *) - -(* Tactic notations *) +let cons_production_parameter l = function + | VTerm _ -> l + | VNonTerm (_,_,ido) -> option_cons ido l let rec tactic_notation_key = function | VTerm id :: _ -> id @@ -207,41 +85,49 @@ let rec next_key_away key t = if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t else key -let locate_tactic_body dir (s,(s',prods as x),e) = - let tags = make_tags prods in - let s = if s="" then next_key_away (tactic_notation_key prods) tags else s in - (s,x,(dir,e)),(s,tags,(s',List.map make_terminal_status prods)) - -let add_tactic_grammar g = - let dir = Lib.cwd () in - let pa,pp = List.split (List.map (locate_tactic_body dir) g) in - Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar (pa,pp))) - -(* Printing grammar entries *) +let add_tactic_notation (n,prods,e) = + let tags = make_tags n prods in + 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 + let parule = (key,n,prods,(Lib.cwd(),tac)) in + Lib.add_anonymous_leaf (inTacticGrammar (parule,pprule)) -let print_grammar univ entry = - if !Options.v7 then - let u = get_univ univ in - let typ = explicitize_entry (fst u) entry in - let te,_,_ = get_constr_entry false typ in - Gram.Entry.print te - else - match entry with - | "constr" | "operconstr" | "binder_constr" -> - msgnl (str "Entry constr is"); - Gram.Entry.print Pcoq.Constr.constr; - msgnl (str "and lconstr is"); - Gram.Entry.print Pcoq.Constr.lconstr; - msgnl (str "where binder_constr is"); - Gram.Entry.print Pcoq.Constr.binder_constr; - msgnl (str "and operconstr is"); - Gram.Entry.print Pcoq.Constr.operconstr; - | "pattern" -> - Gram.Entry.print Pcoq.Constr.pattern - | "tactic" -> - Gram.Entry.print Pcoq.Tactic.simple_tactic - | _ -> error "Unknown or unprintable grammar entry" +(**********************************************************************) +(* Printing grammar entries *) + +let print_grammar univ = function + | "constr" | "operconstr" | "binder_constr" -> + msgnl (str "Entry constr is"); + Gram.Entry.print Pcoq.Constr.constr; + msgnl (str "and lconstr is"); + Gram.Entry.print Pcoq.Constr.lconstr; + msgnl (str "where binder_constr is"); + Gram.Entry.print Pcoq.Constr.binder_constr; + msgnl (str "and operconstr is"); + Gram.Entry.print Pcoq.Constr.operconstr; + | "pattern" -> + Gram.Entry.print Pcoq.Constr.pattern + | "tactic" -> + msgnl (str "Entry tactic_expr is"); + Gram.Entry.print Pcoq.Tactic.tactic_expr; + msgnl (str "Entry simple_tactic is"); + Gram.Entry.print Pcoq.Tactic.simple_tactic; + | "vernac" -> + msgnl (str "Entry vernac is"); + Gram.Entry.print Pcoq.Vernac_.vernac; + msgnl (str "Entry command is"); + Gram.Entry.print Pcoq.Vernac_.command; + msgnl (str "Entry syntax is"); + Gram.Entry.print Pcoq.Vernac_.syntax; + msgnl (str "Entry gallina is"); + Gram.Entry.print Pcoq.Vernac_.gallina; + msgnl (str "Entry gallina_ext is"); + Gram.Entry.print Pcoq.Vernac_.gallina_ext; + | _ -> error "Unknown or unprintable grammar entry" +(**********************************************************************) (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) @@ -342,12 +228,12 @@ let parse_format (loc,str) = Stdpp.raise_with_loc loc e (***********************) -(* Analysing notations *) - -open Symbols +(* Analyzing notations *) type symbol_token = WhiteSpace of int | String of string +(* Decompose the notation string into tokens *) + let split_notation_string str = let push_token beg i l = if beg = i then l else @@ -376,6 +262,43 @@ let split_notation_string str = in loop 0 0 +(* Interpret notations with a recursive component *) + +let rec find_pattern xl = function + | Break n as x :: l, Break n' :: l' when n=n' -> + find_pattern (x::xl) (l,l') + | Terminal s as x :: l, Terminal s' :: l' when s = s' -> + find_pattern (x::xl) (l,l') + | [NonTerminal x], NonTerminal x' :: l' -> + (x,x',xl),l' + | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ -> + error ("The token "^s^" occurs on one side of \"..\" but not on the other side") + | [NonTerminal _], Break s :: _ | Break s :: _, _ -> + error ("A break occurs on one side of \"..\" but not on the other side") + | ((SProdList _ | NonTerminal _) :: _ | []), _ -> + error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\"") + +let rec interp_list_parser hd = function + | [] -> [], List.rev hd + | NonTerminal id :: tl when id = ldots_var -> + let ((x,y,sl),tl') = find_pattern [] (hd,tl) in + let yl,tl'' = interp_list_parser [] tl' in + (* We remember the second copy of each recursive part variable to *) + (* remove it afterwards *) + y::yl, SProdList (x,sl) :: tl'' + | (Terminal _ | Break _) as s :: tl -> + if hd = [] then + let yl,tl' = interp_list_parser [] tl in + yl, s :: tl' + else + interp_list_parser (s::hd) tl + | NonTerminal _ as x :: tl -> + let yl,tl' = interp_list_parser [x] tl in + yl, List.rev_append hd tl' + | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser" + +(* Find non-terminal tokens of notation *) + let unquote_notation_token s = let n = String.length s in if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s @@ -410,38 +333,12 @@ let rec raw_analyse_notation_tokens = function let (vars,l) = raw_analyse_notation_tokens sl in (vars, Break n :: l) -let rec find_pattern xl = function - | Break n as x :: l, Break n' :: l' when n=n' -> - find_pattern (x::xl) (l,l') - | Terminal s as x :: l, Terminal s' :: l' when s = s' -> - find_pattern (x::xl) (l,l') - | [NonTerminal x], NonTerminal x' :: l' -> - (x,x',xl),l' - | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ -> - error ("The token "^s^" occurs on one side of \"..\" but not on the other side") - | [NonTerminal _], Break s :: _ | Break s :: _, _ -> - error ("A break occurs on one side of \"..\" but not on the other side") - | ((SProdList _ | NonTerminal _) :: _ | []), _ -> - error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\"") - -let rec interp_list_parser hd = function - | [] -> [], List.rev hd - | NonTerminal id :: tl when id = ldots_var -> - let ((x,y,sl),tl') = find_pattern [] (hd,tl) in - let yl,tl'' = interp_list_parser [] tl' in - (* We remember the second copy of each recursive part variable to *) - (* remove it afterwards *) - y::yl, SProdList (x,sl) :: tl'' - | (Terminal _ | Break _) as s :: tl -> - if hd = [] then - let yl,tl' = interp_list_parser [] tl in - yl, s :: tl' - else - interp_list_parser (s::hd) tl - | NonTerminal _ as x :: tl -> - let yl,tl' = interp_list_parser [x] tl in - yl, List.rev_append hd tl' - | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser" +let is_numeral symbs = + match List.filter (function Break _ -> false | _ -> true) symbs with + | ([Terminal "-"; Terminal x] | [Terminal x]) -> + (try let _ = Bigint.of_string x in true with _ -> false) + | _ -> + false let analyse_notation_tokens l = let vars,l = raw_analyse_notation_tokens l in @@ -450,7 +347,8 @@ let analyse_notation_tokens l = let remove_vars = List.fold_right List.remove_assoc -(* Build the syntax and grammar rules *) +(**********************************************************************) +(* Build pretty-printing rules *) type printing_precedence = int * parenRelation type parsing_precedence = int option @@ -460,15 +358,10 @@ let prec_assoc = function | Gramext.LeftA -> (E,L) | Gramext.NonA -> (L,L) -(* For old ast printer *) -let meta_pattern m = Pmeta(m,Tany) - -type white_status = Juxtapose | Separate of int | NextIsTerminal - let precedence_of_entry_type from = function | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n - | ETConstr (NumLevel n,BorderProd (left,Some a)) -> - n, let (lp,rp) = prec_assoc a in if left then lp else rp + | ETConstr (NumLevel n,BorderProd (b,Some a)) -> + n, let (lp,rp) = prec_assoc a in if b=Left then lp else rp | ETConstr (NumLevel n,InternalProd) -> n, Prec n | ETConstr (NextLevel,_) -> from, L | ETOther ("constr","annot") -> 10, Prec 10 @@ -506,57 +399,15 @@ let is_operator s = s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~') -type previous_prod_status = NoBreak | CanBreak - let rec is_non_terminal = function | NonTerminal _ | SProdList _ -> true | _ -> false -let add_break n l = UNP_BRK (n,1) :: l - -(* For old ast printer *) -let make_hunks_ast symbols etyps from = - let rec make ws = function - | NonTerminal m :: prods -> - let _,lp = precedence_of_entry_type from (List.assoc m etyps) in - let u = PH (meta_pattern (string_of_id m), None, lp) in - if prods <> [] && is_non_terminal (List.hd prods) then - u :: add_break 1 (make CanBreak prods) - else - u :: make CanBreak prods - - | Terminal s :: prods when List.exists is_non_terminal prods -> - let protect = - is_letter s.[0] || - (is_non_terminal (List.hd prods) && - (is_letter (s.[String.length s -1])) || - (is_digit (s.[String.length s -1]))) in - if is_comma s || is_right_bracket s then - RO s :: add_break 0 (make NoBreak prods) - else if (is_operator s || is_left_bracket s) && ws = CanBreak then - add_break (if protect then 1 else 0) - (RO (if protect then s^" " else s) :: make CanBreak prods) - else - if protect then - (if ws = CanBreak then add_break 1 else (fun x -> x)) - (RO (s^" ") :: make CanBreak prods) - else - RO s :: make CanBreak prods - - | Terminal s :: prods -> - RO s :: make NoBreak prods - - | Break n :: prods -> - add_break n (make NoBreak prods) - - | SProdList _ :: _ -> - anomaly "Recursive notations not supported in old syntax" - - | [] -> [] +let add_break n l = UnpCut (PpBrk(n,0)) :: l - in make NoBreak symbols +(* Heuristics for building default printing rules *) -let add_break n l = UnpCut (PpBrk(n,0)) :: l +type previous_prod_status = NoBreak | CanBreak let make_hunks etyps symbols from = let vars,typs = List.split etyps in @@ -621,6 +472,8 @@ let make_hunks etyps symbols from = in make NoBreak symbols +(* Build default printing rules from explicit format *) + let error_format () = error "The format does not match the notation" let rec split_format_at_ldots hd = function @@ -656,12 +509,12 @@ let read_recursive_format sl fmt = let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) -let hunks_of_format (from,(vars,typs) as vt) symfmt = +let hunks_of_format (from,(vars,typs)) symfmt = let rec aux = function | symbs, (UnpTerminal s' as u) :: fmt when s' = String.make (String.length s') ' ' -> let symbs, l = aux (symbs,fmt) in symbs, u :: l - | Terminal s :: symbs, (UnpTerminal s' as u) :: fmt + | Terminal s :: symbs, (UnpTerminal s') :: fmt when s = unquote_notation_token s' -> let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' -> @@ -689,36 +542,31 @@ let hunks_of_format (from,(vars,typs) as vt) symfmt = | [], l -> l | _ -> error_format () -let string_of_prec (n,p) = - (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "") +(**********************************************************************) +(* Build parsing rules *) let assoc_of_type n (_,typ) = precedence_of_entry_type n typ -let string_of_assoc = function - | Some(Gramext.RightA) -> "RIGHTA" - | Some(Gramext.LeftA) | None -> "LEFTA" - | Some(Gramext.NonA) -> "NONA" - let is_not_small_constr = function ETConstr _ -> true | ETOther("constr","binder_constr") -> true | _ -> false -let rec define_keywords = function +let rec define_keywords_aux = function NonTerm(_,Some(_,e)) as n1 :: Term("IDENT",k) :: l - when not !Options.v7 && is_not_small_constr e -> + when is_not_small_constr e -> prerr_endline ("Defining '"^k^"' as keyword"); Lexer.add_token("",k); - n1 :: Term("",k) :: define_keywords l - | n :: l -> n :: define_keywords l + n1 :: Term("",k) :: define_keywords_aux l + | n :: l -> n :: define_keywords_aux l | [] -> [] let define_keywords = function - Term("IDENT",k)::l when not !Options.v7 -> + Term("IDENT",k)::l -> prerr_endline ("Defining '"^k^"' as keyword"); Lexer.add_token("",k); - Term("",k) :: define_keywords l - | l -> define_keywords l + Term("",k) :: define_keywords_aux l + | l -> define_keywords_aux l let make_production etyps symbols = let prod = @@ -728,12 +576,12 @@ let make_production etyps symbols = let typ = List.assoc m etyps in NonTerm (typ, Some (m,typ)) :: l | Terminal s -> - Term (Extend.terminal s) :: l + Term (terminal s) :: l | Break _ -> l | SProdList (x,sl) -> let sl = List.flatten - (List.map (function Terminal s -> [Extend.terminal s] + (List.map (function Terminal s -> [terminal s] | Break _ -> [] | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in let y = match List.assoc x etyps with @@ -766,44 +614,8 @@ let recompute_assoc typs = | _, Some Gramext.RightA -> Some Gramext.RightA | _ -> None -let make_grammar_rule n typs symbols ntn perm = - let assoc = recompute_assoc typs in - let prod = make_production typs symbols in - (n,assoc,ntn,prod, perm) - -(* For old ast printer *) -let metas_of sl = - List.fold_right - (fun it metatl -> match it with - | NonTerminal m -> m::metatl - | _ -> metatl) - sl [] - -(* For old ast printer *) -let make_pattern symbols ast = - let env = List.map (fun m -> (string_of_id m,ETast)) (metas_of symbols) in - fst (to_pat env ast) - -(* For old ast printer *) -let make_syntax_rule n name symbols typs ast ntn sc = - [{syn_id = name; - syn_prec = n; - syn_astpat = make_pattern symbols ast; - syn_hunks = - [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1,make_hunks_ast symbols typs n))]}] - -let make_pp_rule (n,typs,symbols,fmt) = - match fmt with - | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] - | Some fmt -> - [UnpBox (PpHOVB 0, - hunks_of_format (n,List.split typs) (symbols,parse_format fmt))] - (**************************************************************************) -(* Syntax extenstion: common parsing/printing rules and no interpretation *) - -(* v7 and translator : prec is for v7 (None if V8Notation), prec8 is for v8 *) -(* v8 : prec is for v8, prec8 is the same *) +(* Registration of syntax extensions (parsing/printing, no interpretation)*) let pr_arg_level from = function | (n,L) when n=from -> str "at next level" @@ -813,66 +625,38 @@ let pr_arg_level from = function | (n,_) -> str "Unknown level" let pr_level ntn (from,args) = - let lopen = ntn.[0] = '_' and ropen = ntn.[String.length ntn - 1] = '_' in -(* - let ppassoc, args = match args with - | [] -> mt (), [] - | (nl,lpr)::l when nl=from & fst (list_last l)=from -> - let (_,rpr),l = list_sep_last l in - match lpr, snd (list_last l) with - | L,E -> Gramext.RightA, l - | E,L -> Gramext.LeftA, l - | L,L -> Gramext.NoneA, l - | _ -> args -*) str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++ prlist_with_sep pr_coma (pr_arg_level from) args -(* In v8: prec = Some prec8 is for both parsing and printing *) -(* In v7 and translator: - prec is for parsing (None if V8Notation), - prec8 for v8 printing (v7 printing is via ast) *) -let cache_syntax_extension (_,(_,((prec,prec8),ntn,gr,se))) = +let error_incompatible_level ntn oldprec prec = + errorlabstrm "" + (str ("Notation "^ntn^" is already defined") ++ spc() ++ + pr_level ntn oldprec ++ + spc() ++ str "while it is now required to be" ++ spc() ++ + pr_level ntn prec) + +let cache_one_syntax_extension (prec,ntn,gr,pp) = try - let oldprec, oldprec8 = Symbols.level_of_notation ntn in - if prec8 <> oldprec8 & (Options.do_translate () or not !Options.v7) then - errorlabstrm "" - (str ((if Options.do_translate () then "For new syntax, notation " - else "Notation ") - ^ntn^" is already defined") ++ spc() ++ pr_level ntn oldprec8 ++ - spc() ++ str "while it is now required to be" ++ spc() ++ - pr_level ntn prec8) - else - (* Inconsistent v8 notations but not while translating; forget... *) - (); - (* V8 notations are consistent (from both translator or v8) *) - if prec <> None & !Options.v7 then begin - (* Update the V7 parsing rule *) - if oldprec <> None & out_some oldprec <> out_some prec then - (* None of them is V8Notation and they are different: warn *) - Options.if_verbose - warning ("Notation "^ntn^ - " was already assigned a different level or sublevels"); - if oldprec = None or out_some oldprec <> out_some prec then - Egrammar.extend_grammar (Egrammar.Notation (out_some prec,out_some gr)) - end + let oldprec = Notation.level_of_notation ntn in + if prec <> oldprec then error_incompatible_level ntn oldprec prec with Not_found -> (* Reserve the notation level *) - Symbols.declare_notation_level ntn (prec,prec8); + Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) - option_iter (fun gr -> - Egrammar.extend_grammar (Egrammar.Notation (out_some prec,gr))) gr; + Egrammar.extend_grammar (Egrammar.Notation (prec,gr)); (* Declare the printing rule *) - Symbols.declare_notation_printing_rule ntn (se,fst prec8) + Notation.declare_notation_printing_rule ntn (pp,fst prec) + +let cache_syntax_extension (_,(_,sy_rules)) = + List.iter cache_one_syntax_extension sy_rules -let subst_notation_grammar subst x = x +let subst_parsing_rule subst x = x let subst_printing_rule subst x = x -let subst_syntax_extension (_,subst,(local,(prec,ntn,gr,se))) = - (local,(prec,ntn, - option_app (subst_notation_grammar subst) gr, - subst_printing_rule subst se)) +let subst_syntax_extension (_,subst,(local,sy)) = + (local, List.map (fun (prec,ntn,gr,pp) -> + (prec,ntn, subst_parsing_rule subst gr, subst_printing_rule subst pp)) sy) let classify_syntax_definition (_,(local,_ as o)) = if local then Dispose else Substitute o @@ -888,6 +672,11 @@ let (inSyntaxExtension, outSyntaxExtension) = classify_function = classify_syntax_definition; export_function = export_syntax_definition} +(**************************************************************************) +(* Precedences *) + +(* Interpreting user-provided modifiers *) + let interp_modifiers modl = let onlyparsing = ref false in let rec interp assoc level etyps format = function @@ -896,23 +685,22 @@ let interp_modifiers modl = | SetEntryType (s,typ) :: l -> let id = id_of_string s in if List.mem_assoc id etyps then - error (s^" is already assigned to an entry or constr level") - else interp assoc level ((id,typ)::etyps) format l + error (s^" is already assigned to an entry or constr level"); + interp assoc level ((id,typ)::etyps) format l | SetItemLevel ([],n) :: l -> interp assoc level etyps format l | SetItemLevel (s::idl,n) :: l -> let id = id_of_string s in if List.mem_assoc id etyps then - error (s^" is already assigned to an entry or constr level") - else - let typ = ETConstr (n,()) in - interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l) + error (s^" is already assigned to an entry or constr level"); + let typ = ETConstr (n,()) in + interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l) | SetLevel n :: l -> - if level <> None then error "A level is given more than once" - else interp assoc (Some n) etyps format l + if level <> None then error "A level is given more than once"; + interp assoc (Some n) etyps format l | SetAssoc a :: l -> - if assoc <> None then error "An associativity is given more than once" - else interp (Some a) level etyps format l + if assoc <> None then error "An associativity is given more than once"; + interp (Some a) level etyps format l | SetOnlyParsing :: l -> onlyparsing := true; interp assoc level etyps format l @@ -921,21 +709,15 @@ let interp_modifiers modl = interp assoc level etyps (Some s) l in interp None None [] None modl -let merge_modifiers a n l = - (match a with None -> [] | Some a -> [SetAssoc a]) @ - (match n with None -> [] | Some n -> [SetLevel n]) @ l - -let interp_infix_modifiers modl = - let (assoc,level,t,b,fmt) = interp_modifiers modl in +let check_infix_modifiers modifiers = + let (assoc,level,t,b,fmt) = interp_modifiers modifiers in if t <> [] then - error "explicit entry level or type unexpected in infix notation"; - (assoc,level,b,fmt) + error "explicit entry level or type unexpected in infix notation" + +let no_syntax_modifiers modifiers = + modifiers = [] or modifiers = [SetOnlyParsing] -(* 2nd list of types has priority *) -let rec merge_entry_types etyps' = function - | [] -> etyps' - | (x,_ as e)::etyps -> - e :: merge_entry_types (List.remove_assoc x etyps') etyps +(* Compute precedences from modifiers (or find default ones) *) let set_entry_type etyps (x,typ) = let typ = try @@ -948,7 +730,7 @@ let set_entry_type etyps (x,typ) = with Not_found -> ETConstr typ in (x,typ) -let check_rule_reversibility l = +let check_rule_productivity l = if List.for_all (function NonTerminal _ -> true | _ -> false) l then error "A notation must include at least one symbol" @@ -956,17 +738,6 @@ let is_not_printable = function | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true | _ -> false -let find_precedence_v7 lev etyps symbols = - (match symbols with - | NonTerminal x :: _ -> - (try match List.assoc x etyps with - | ETConstr _ -> - error "The level of the leftmost non-terminal cannot be changed" - | _ -> () - with Not_found -> ()) - | _ -> ()); - if lev = None then 1 else out_some lev - let find_precedence lev etyps symbols = match symbols with | NonTerminal x :: _ -> @@ -1000,7 +771,7 @@ let find_precedence lev etyps symbols = out_some lev let check_curly_brackets_notation_exists () = - try let _ = Symbols.level_of_notation "{ _ }" in () + try let _ = Notation.level_of_notation "{ _ }" in () with Not_found -> error "Notations involving patterns of the form \"{ _ }\" are treated \n\ specially and require that the notation \"{ _ }\" is already reserved" @@ -1028,95 +799,59 @@ let remove_curly_brackets l = | x :: l -> x :: aux false l in aux true l -let compute_syntax_data forv7 (df,modifiers) = +let compute_syntax_data (df,modifiers) = let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in (* Notation defaults to NONA *) let assoc = match assoc with None -> Some Gramext.NonA | a -> a in let toks = split_notation_string df in let (recvars,vars,symbols) = analyse_notation_tokens toks in let ntn_for_interp = make_notation_key symbols in - let symbols = remove_curly_brackets symbols in - let notation = make_notation_key symbols in - check_rule_reversibility symbols; - let n = - if !Options.v7 then find_precedence_v7 n etyps symbols - else find_precedence n etyps symbols in - let innerlevel = NumLevel (if forv7 then 10 else 200) in + let symbols' = remove_curly_brackets symbols in + let need_squash = (symbols <> symbols') in + let ntn_for_grammar = make_notation_key symbols' in + check_rule_productivity symbols'; + let n = find_precedence n etyps symbols' in + let innerlevel = NumLevel 200 in let typs = find_symbols - (NumLevel n,BorderProd(true,assoc)) + (NumLevel n,BorderProd(Left,assoc)) (innerlevel,InternalProd) - (NumLevel n,BorderProd(false,assoc)) - symbols in + (NumLevel n,BorderProd(Right,assoc)) + symbols' in (* To globalize... *) let typs = List.map (set_entry_type etyps) typs in - let ppdata = (n,typs,symbols,fmt) in let prec = (n,List.map (assoc_of_type n) typs) in - ((onlyparse,recvars,vars, - ntn_for_interp,notation),prec,ppdata,(Lib.library_dp(),df)) - -(* Uninterpreted (reserved) notations *) -let add_syntax_extension local mv mv8 = - (* from v7: - if mv8 <> None: tells the translator how to print in v8 - if mv <> None: tells how to parse and, how to print in v7 - mv = None = mv8 does not occur - from v8 (mv8 is always None and mv is always Some) - mv tells how to parse and print in v8 - *) - let data8 = option_app (compute_syntax_data false) mv8 in - let data = option_app (compute_syntax_data !Options.v7) mv in - let prec,gram_rule = match data with - | None -> None, None (* Case of V8Notation from v7 *) - | Some ((_,_,_,_,notation),prec,(n,typs,symbols,_),_) -> - Some prec, Some (make_grammar_rule n typs symbols notation None) in - match data, data8 with - | None, None -> (* Nothing to do: V8Notation while not translating *) () - | _, Some d | Some d, None -> - let ((_,_,_,_,ntn),ppprec,ppdata,_) = d in (* tells how to print *) - let ntn' = match data with Some ((_,_,_,_,ntn),_,_,_) -> ntn | _ -> ntn in - let pp_rule = make_pp_rule ppdata in - Lib.add_anonymous_leaf - (inSyntaxExtension (local,((prec,ppprec),ntn',gram_rule,pp_rule))) + let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in + let df' = (Lib.library_dp(),df) in + let i_data = (onlyparse,recvars,vars,(ntn_for_interp,df')) in + (i_data,sy_data) (**********************************************************************) -(* Distfix, Infix, Symbols *) - -(* A notation comes with a grammar rule, a pretty-printing rule, an - identifiying pattern called notation and an associated scope *) -let load_notation _ (_,(_,_,ntn,scope,pat,onlyparse,_,_)) = - option_iter Symbols.declare_scope scope - -let open_notation i (_,(_,oldse,ntn,scope,pat,onlyparse,pp8only,df)) = - if i=1 then begin - let b,oldpp8only = Symbols.exists_notation_in_scope scope ntn pat in - (* Declare the old printer rule and its interpretation *) - if (not b or oldpp8only) & oldse <> None then - Esyntax.add_ppobject {sc_univ="constr";sc_entries=out_some oldse}; +(* Registration of notations interpretation *) + +let load_notation _ (_,(_,scope,pat,onlyparse,_)) = + option_iter Notation.declare_scope scope + +let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) = + if i=1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin (* Declare the interpretation *) - if not b then - Symbols.declare_notation_interpretation ntn scope pat df pp8only; - if oldpp8only & not pp8only then - Options.silently - (Symbols.declare_notation_interpretation ntn scope pat df) pp8only; - if not b & not onlyparse then - Symbols.declare_uninterpretation (NotationRule (scope,ntn)) pat + Notation.declare_notation_interpretation ntn scope pat df; + (* Declare the uninterpretation *) + if not onlyparse then + Notation.declare_uninterpretation (NotationRule (scope,ntn)) pat end let cache_notation o = load_notation 1 o; open_notation 1 o -let subst_notation (_,subst,(lc,oldse,ntn,scope,(metas,pat),b,b',df)) = - (lc,option_app - (list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst)) oldse, - ntn,scope, - (metas,subst_aconstr subst pat), b, b', df) +let subst_notation (_,subst,(lc,scope,(metas,pat),b,ndf)) = + (lc,scope,(metas,subst_aconstr subst (List.map fst metas) pat),b,ndf) -let classify_notation (_,(local,_,_,_,_,_,_,_ as o)) = +let classify_notation (_,(local,_,_,_,_ as o)) = if local then Dispose else Substitute o -let export_notation (local,_,_,_,_,_,_,_ as o) = +let export_notation (local,_,_,_,_ as o) = if local then None else Some o let (inNotation, outNotation) = @@ -1128,37 +863,8 @@ let (inNotation, outNotation) = classify_function = classify_notation; export_function = export_notation} -(* For old ast printer *) -let rec reify_meta_ast vars = function - | Smetalam (loc,s,body) -> Smetalam (loc,s,reify_meta_ast vars body) -(* | Node(loc,"META",[Num (_,n)]) -> Nmeta (loc,create_meta n)*) - | Node(loc,"ISEVAR",[]) -> Nmeta (loc,"$_") - | Node(loc,op,args) -> Node (loc,op, List.map (reify_meta_ast vars) args) - | Slam(loc,Some id,body) when List.mem id vars -> - Smetalam (loc,string_of_id id,reify_meta_ast vars body) - | Slam(loc,na,body) -> Slam(loc,na,reify_meta_ast vars body) - | Nvar (loc,id) when List.mem id vars -> Nmeta (loc,string_of_id id) - | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a - | Dynamic _ as a -> (* Hum... what to do here *) a - -(* For old ast syntax *) -let make_old_pp_rule n symbols typs r ntn scope vars = - let ast = Termast.ast_of_rawconstr r in - let ast = reify_meta_ast vars ast in - let scope_name = match scope with Some s -> s | None -> "core_scope" in - let rule_name = ntn^"_"^scope_name^"_notation" in - make_syntax_rule n rule_name symbols typs ast ntn scope - -(* maps positions in v8-notation into positions in v7-notation (used - for parsing). - For instance Notation "x < y < z" := .. V8only "y < z < x" - yields [1; 2; 0] (y is the second arg in v7; z is 3rd; x is fst) *) -let mk_permut vars7 vars8 = - if vars7=vars8 then None else - Some - (List.fold_right - (fun v8 subs -> list_index v8 vars7 - 1 :: subs) - vars8 []) +(**********************************************************************) +(* Recovering existing syntax *) let contract_notation ntn = if ntn = "{ _ }" then ntn else @@ -1173,304 +879,120 @@ let contract_notation ntn = else ntn in aux ntn 0 -let add_notation_in_scope local df c mods omodv8 scope = - let ((onlyparse,recs,vars,intnot,notation),prec,(n,typs,symbols,_ as ppdata),df')= - compute_syntax_data !Options.v7 (df,mods) in - (* Declare the parsing and printing rules if not already done *) - (* For both v7 and translate: parsing is as described for v7 in v7 file *) - (* For v8: parsing is as described in v8 file *) - (* For v7: printing is by the old printer - see below *) - (* For translate: printing is as described for v8 in v7 file *) - (* For v8: printing is as described in v8 file *) - (* In short: parsing does not depend on omodv8 *) - (* Printing depends on mv8 if defined, otherwise of mods (scaled by 10) *) - (* if in v7, or of mods without scaling if in v8 *) - let intnot,ntn,pprecvars,ppvars,ppprec,pp_rule = - match omodv8 with - | Some mv8 -> - let (_,recs8,vars8,intnot8,ntn8),p,d,_ = compute_syntax_data false mv8 in - intnot8,ntn8,recs8,vars8,p,make_pp_rule d - | None when not !Options.v7 -> - intnot,notation,recs,vars,prec,make_pp_rule ppdata - | None -> - (* means the rule already exists: recover it *) - (* occurs only with V8only flag alone *) - try - let ntn = contract_notation notation in - let _, oldprec8 = Symbols.level_of_notation ntn in - let rule,_ = Symbols.find_notation_printing_rule ntn in - notation,ntn,recs,vars,oldprec8,rule - with Not_found -> error "No known parsing rule for this notation in V8" - in - let permut = mk_permut vars ppvars in - let gram_rule = make_grammar_rule n typs symbols ntn permut in - Lib.add_anonymous_leaf - (inSyntaxExtension - (local,((Some prec,ppprec),ntn,Some gram_rule,pp_rule))); - - (* Declare interpretation *) - let (acvars,ac) = interp_aconstr [] ppvars c in - let a = (remove_vars pprecvars acvars,ac) (* For recursive parts *) in - let old_pp_rule = - (* Used only by v7; disable if contains a recursive pattern *) - if onlyparse or pprecvars <> [] or not (!Options.v7) then None - else - let r = interp_global_rawconstr_with_vars vars c in - Some (make_old_pp_rule n symbols typs r intnot scope vars) in - let onlyparse = onlyparse or !Options.v7_only or is_not_printable ac in - Lib.add_anonymous_leaf - (inNotation(local,old_pp_rule,intnot,scope,a,onlyparse,false,df')) - -let level_rule (n,p) = if p = E then n else max (n-1) 0 +exception NoSyntaxRule -let recover_syntax ntn = +let recover_syntax ntn = try - match Symbols.level_of_notation ntn with - | (Some prec,_ as pprec) -> - let rule,_ = Symbols.find_notation_printing_rule ntn in - let gr = Egrammar.recover_notation_grammar ntn prec in - Some (pprec,ntn,Some gr,rule) - | None,_ -> None - with Not_found -> None + 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 + (prec,ntn,gr,pprule) + with Not_found -> + raise NoSyntaxRule + +let recover_squash_syntax () = recover_syntax "{ _ }" let recover_notation_syntax rawntn = let ntn = contract_notation rawntn in - match recover_syntax ntn with - | None -> None - | Some gr -> Some (gr,if ntn=rawntn then None else recover_syntax "{ _ }") - -let set_data_for_v7_pp recs a vars = - if not !Options.v7 then None else - if recs=[] then Some (a,vars) - else (warning "No recursive notation in v7 syntax";None) - -let build_old_pp_rule notation scope symbs (r,vars) = - let prec = - try - let a,_ = Symbols.level_of_notation (contract_notation notation) in - if a = None then raise Not_found else out_some a - with Not_found -> - error "Parsing rule for this notation has to be previously declared" in - let typs = List.map2 - (fun id n -> - id,ETConstr (NumLevel (level_rule n),InternalProd)) vars (snd prec) in - make_old_pp_rule (fst prec) symbs typs r notation scope vars - -let add_notation_interpretation_core local symbs for_old df a scope onlyparse - onlypp gram_data = - let notation = make_notation_key symbs in - let old_pp_rule = - if !Options.v7 then - option_app (build_old_pp_rule notation scope symbs) for_old - else None in - option_iter - (fun (x,y) -> - Lib.add_anonymous_leaf (inSyntaxExtension (local,x)); - option_iter - (fun z -> Lib.add_anonymous_leaf (inSyntaxExtension (local,z))) y) - gram_data; - Lib.add_anonymous_leaf - (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp, - (Lib.library_dp(),df))) + let sy_rule = recover_syntax ntn in + let need_squash = ntn<>rawntn in + if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule] -let add_notation_interpretation df names c sc = +(**********************************************************************) +(* Main entry point for building parsing and printing rules *) + +let make_pa_rule (n,typs,symbols,_) ntn = + let assoc = recompute_assoc typs in + let prod = make_production typs symbols in + (n,assoc,ntn,prod) + +let make_pp_rule (n,typs,symbols,fmt) = + match fmt with + | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] + | Some fmt -> hunks_of_format (n,List.split typs) (symbols,parse_format fmt) + +let make_syntax_rules (ntn,prec,need_squash,sy_data) = + let pa_rule = make_pa_rule sy_data ntn in + let pp_rule = make_pp_rule sy_data in + let sy_rule = (prec,ntn,pa_rule,pp_rule) in + (* By construction, the rule for "{ _ }" is declared, but we need to + redeclare it because the file where it is declared needs not be open + when the current file opens (especially in presence of -nois) *) + if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule] + +(**********************************************************************) +(* Main functions about notations *) + +let add_notation_in_scope local df c mods scope = + let (i_data,sy_data) = compute_syntax_data (df,mods) in + (* Declare the parsing and printing rules *) + let sy_rules = make_syntax_rules sy_data in + Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)); + (* Declare interpretation *) + let (onlyparse,recvars,vars,df') = i_data in + let (acvars,ac) = interp_aconstr [] vars c in + let a = (remove_vars recvars acvars,ac) (* For recursive parts *) in + let onlyparse = onlyparse or is_not_printable ac in + Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df')) + +let add_notation_interpretation_core local df names c scope onlyparse = let (recs,vars,symbs) = analyse_notation_tokens (split_notation_string df) in - let gram_data = recover_notation_syntax (make_notation_key symbs) in - if gram_data = None then - error "Parsing rule for this notation has to be previously declared"; + (* Redeclare pa/pp rules *) + if not (is_numeral symbs) then begin + let sy_rules = recover_notation_syntax (make_notation_key symbs) in + Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)) + end; + (* Declare interpretation *) + let df' = (make_notation_key symbs,(Lib.library_dp(),df)) in let (acvars,ac) = interp_aconstr names vars c in let a = (remove_vars recs acvars,ac) (* For recursive parts *) in - let a_for_old = interp_rawconstr_with_implicits Evd.empty (Global.env()) vars names c in - let for_oldpp = set_data_for_v7_pp recs a_for_old vars in - let onlyparse = is_not_printable ac in - add_notation_interpretation_core false symbs for_oldpp df a sc onlyparse - false gram_data - -let add_notation_in_scope_v8only local df c mv8 scope = - let (_,recs,vars,intnot,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in - let pp_rule = make_pp_rule ppdata in - Lib.add_anonymous_leaf - (inSyntaxExtension(local,((None,prec),notation,None,pp_rule))); - (* Declare the interpretation *) - let (acvars,ac) = interp_aconstr [] vars c in - let a = (remove_vars recs acvars,ac) (* For recursive parts *) in - let onlyparse = is_not_printable ac in - Lib.add_anonymous_leaf - (inNotation(local,None,intnot,scope,a,onlyparse,true,df')) + let onlyparse = onlyparse or is_not_printable ac in + Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df')) -let add_notation_v8only local c (df,modifiers) sc = - let toks = split_notation_string df in - match toks with - | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) -> - (* This is a ident to be declared as a rule *) - add_notation_in_scope_v8only local df c (SetLevel 0::modifiers) sc - | _ -> - let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers in - match lev with - | None-> - if modifiers <> [] & modifiers <> [SetOnlyParsing] then - error "Parsing rule for this notation includes no level" - else - (* Declare only interpretation *) - let (recs,vars,symbs) = analyse_notation_tokens toks in - let (acvars,ac) = interp_aconstr [] vars c in - let onlyparse = modifiers = [SetOnlyParsing] - or is_not_printable ac in - let a = (remove_vars recs acvars,ac) in - add_notation_interpretation_core local symbs None df a sc - onlyparse true None - | Some n -> - (* Declare both syntax and interpretation *) - let mods = - if List.for_all (function SetAssoc _ -> false | _ -> true) - modifiers - then SetAssoc Gramext.NonA :: modifiers else modifiers in - add_notation_in_scope_v8only local df c mods sc - -let is_quoted_ident x = - let x' = unquote_notation_token x in - x <> x' & try Lexer.check_ident x'; true with _ -> false - -(* v7: dfmod=None; mv8=Some: add only v8 printing rule *) -(* dfmod=Some: add v7 parsing rule; mv8=Some: add v8 printing rule *) -(* dfmod=Some; mv8=None: same v7-parsing and v8-printing rules *) -(* v8: dfmod=Some; mv8=None: same v8 parsing and printing rules *) -let add_notation local c dfmod mv8 sc = - match dfmod with - | None -> add_notation_v8only local c (out_some mv8) sc - | Some (df,modifiers) -> - let toks = split_notation_string df in - match toks with - | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) -> - (* This is a ident to be declared as a rule *) - add_notation_in_scope local df c (SetLevel 0::modifiers) mv8 sc - | _ -> - let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers in - match lev with - | None-> - if modifiers <> [] & modifiers <> [SetOnlyParsing] then - error "Parsing rule for this notation includes no level" - else - (* Declare only interpretation *) - let (recs,vars,symbs) = analyse_notation_tokens toks in - let gram_data = - recover_notation_syntax (make_notation_key symbs) in - if gram_data <> None then - let (acvars,ac) = interp_aconstr [] vars c in - let a = (remove_vars recs acvars,ac) in - let onlyparse = modifiers = [SetOnlyParsing] - or is_not_printable ac in - let a_for_old = interp_global_rawconstr_with_vars vars c in - let for_old = set_data_for_v7_pp recs a_for_old vars in - add_notation_interpretation_core local symbs for_old df a - sc onlyparse false gram_data - else - add_notation_in_scope local df c modifiers mv8 sc - | Some n -> - (* Declare both syntax and interpretation *) - let assoc = match assoc with None -> Some Gramext.NonA | a -> a in - add_notation_in_scope local df c modifiers mv8 sc - -(* TODO add boxes information in the expression *) +(* Notations without interpretation (Reserved Notation) *) + +let add_syntax_extension local mv = + let (_,sy_data) = compute_syntax_data mv in + let sy_rules = make_syntax_rules sy_data in + Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) + +(* Notations with only interpretation *) + +let add_notation_interpretation df names c sc = + try add_notation_interpretation_core false df names c sc false + with NoSyntaxRule -> + error "Parsing rule for this notation has to be previously declared" + +(* Main entry point *) + +let add_notation local c (df,modifiers) sc = + if no_syntax_modifiers modifiers then + (* No syntax data: try to rely on a previously declared rule *) + let onlyparse = modifiers=[SetOnlyParsing] in + try add_notation_interpretation_core local df [] c sc onlyparse + with NoSyntaxRule -> + (* Try to determine a default syntax rule *) + add_notation_in_scope local df c modifiers sc + else + (* Declare both syntax and interpretation *) + add_notation_in_scope local df c modifiers sc + +(* Infix notations *) let inject_var x = CRef (Ident (dummy_loc, id_of_string x)) -let rec rename x vars n = function - | [] -> - (vars,[]) - | String "_"::l -> - let (vars,l) = rename x vars (n+1) l in - let xn = x^(string_of_int n) in - ((inject_var xn)::vars,xn::l) - | String y::l -> - let (vars,l) = rename x vars n l in (vars,(quote_notation_token y)::l) - | WhiteSpace _::l -> - rename x vars n l - -let translate_distfix assoc df r = - let (vars,l) = rename "x" [] 1 (split_notation_string df) in - let df = String.concat " " l in - let a = mkAppC (mkRefC r, vars) in - let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in - (assoc,df,a) - -let add_distfix local assoc n df r sc = - (* "x" cannot clash since r is globalized (included section vars) *) - let (vars,l) = rename "x" [] 1 (split_notation_string df) in - let df = String.concat " " l in - let a = mkAppC (mkRefC r, vars) in - let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in - add_notation_in_scope local df a [SetAssoc assoc;SetLevel n] None sc - -let make_infix_data n assoc modl mv8 = - (* Infix defaults to LEFTA in V7 (cf doc) *) - let mv = match n with None when !Options.v7 -> SetLevel 1 :: modl | _ -> modl in - let mv = match assoc with None when !Options.v7 -> SetAssoc Gramext.LeftA :: mv | _ -> mv in - let mv8 = match mv8 with - None -> None - | Some(s8,mv8) -> - if List.for_all (function SetLevel _ -> false | _ -> true) mv8 then - error "Needs a level" - else Some (("x "^quote_notation_token s8^" y"),mv8) in - mv,mv8 - -let add_infix local (inf,modl) pr mv8 sc = - if inf="" (* Code for V8Infix only *) then - let (p8,mv8) = out_some mv8 in - let (a8,n8,onlyparse,fmt) = interp_infix_modifiers mv8 in - let metas = [inject_var "x"; inject_var "y"] in - let a = mkAppC (mkRefC pr,metas) in - let df = "x "^(quote_notation_token p8)^" y" in - let toks = split_notation_string df in - if a8=None & n8=None & fmt=None then - (* Declare only interpretation *) - let (recs,vars,symbs) = analyse_notation_tokens toks in - let (acvars,ac) = interp_aconstr [] vars a in - let a' = (remove_vars recs acvars,ac) in - let a_for_old = interp_global_rawconstr_with_vars vars a in - add_notation_interpretation_core local symbs None df a' sc - onlyparse true None - else - if n8 = None then error "Needs a level" else - let mv8 = match a8 with None -> SetAssoc Gramext.NonA :: mv8 |_ -> mv8 in - add_notation_in_scope_v8only local df a mv8 sc - else begin - let (assoc,n,onlyparse,fmt) = interp_infix_modifiers modl in +let add_infix local (inf,modifiers) pr sc = + check_infix_modifiers modifiers; (* check the precedence *) - if !Options.v7 & (n<> None & (out_some n < 1 or out_some n > 10)) then - errorlabstrm "Metasyntax.infix_grammar_entry" - (str"Precedence must be between 1 and 10."); - (* - if (assoc<>None) & (n<6 or n>9) then - errorlabstrm "Vernacentries.infix_grammar_entry" - (str"Associativity Precedence must be 6,7,8 or 9."); - *) let metas = [inject_var "x"; inject_var "y"] in - let a = mkAppC (mkRefC pr,metas) in + let c = mkAppC (mkRefC pr,metas) in let df = "x "^(quote_notation_token inf)^" y" in - let toks = split_notation_string df in - if not !Options.v7 & n=None & assoc=None then - (* En v8, une notation sans information de parsing signifie *) - (* de ne déclarer que l'interprétation *) - (* Declare only interpretation *) - let (recs,vars,symbs) = analyse_notation_tokens toks in - let gram_data = recover_notation_syntax (make_notation_key symbs) in - if gram_data <> None then - let (acvars,ac) = interp_aconstr [] vars a in - let a' = (remove_vars recs acvars,ac) in - let a_for_old = interp_global_rawconstr_with_vars vars a in - let for_old = set_data_for_v7_pp recs a_for_old vars in - add_notation_interpretation_core local symbs for_old df a' sc - onlyparse false gram_data - else - let mv,mv8 = make_infix_data n assoc modl mv8 in - add_notation_in_scope local df a mv mv8 sc - else - let mv,mv8 = make_infix_data n assoc modl mv8 in - add_notation_in_scope local df a mv mv8 sc - end + add_notation local c (df,modifiers) sc + +(**********************************************************************) +(* Miscellaneous *) -let standardise_locatable_notation ntn = +let standardize_locatable_notation ntn = let unquote = function | String s -> [unquote_notation_token s] | _ -> [] in @@ -1480,17 +1002,19 @@ let standardise_locatable_notation ntn = else unquote_notation_token ntn -(* Delimiters and classes bound to scopes *) +(**********************************************************************) +(* Delimiters and classes bound to scopes *) + type scope_command = ScopeDelim of string | ScopeClasses of Classops.cl_typ let load_scope_command _ (_,(scope,dlm)) = - Symbols.declare_scope scope + Notation.declare_scope scope let open_scope_command i (_,(scope,o)) = if i=1 then match o with - | ScopeDelim dlm -> Symbols.declare_delimiters scope dlm - | ScopeClasses cl -> Symbols.declare_class_scope scope cl + | ScopeDelim dlm -> Notation.declare_delimiters scope dlm + | ScopeClasses cl -> Notation.declare_class_scope scope cl let cache_scope_command o = load_scope_command 1 o; |