diff options
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 1379 |
1 files changed, 0 insertions, 1379 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml deleted file mode 100644 index 008d5cf9..00000000 --- a/toplevel/metasyntax.ml +++ /dev/null @@ -1,1379 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open Flags -open CErrors -open Util -open Names -open Constrexpr -open Constrexpr_ops -open Notation_term -open Notation_ops -open Ppextend -open Extend -open Libobject -open Constrintern -open Vernacexpr -open Pcoq -open Libnames -open Tok -open Egramcoq -open Notation -open Nameops - -(**********************************************************************) -(* Tokens *) - -let cache_token (_,s) = CLexer.add_keyword s - -let inToken : string -> obj = - declare_object {(default_object "TOKEN") with - open_function = (fun i o -> if Int.equal i 1 then cache_token o); - cache_function = cache_token; - subst_function = Libobject.ident_subst_function; - classify_function = (fun o -> Substitute o)} - -let add_token_obj s = Lib.add_anonymous_leaf (inToken s) - -(**********************************************************************) -(* Printing grammar entries *) - -let entry_buf = Buffer.create 64 - -let pr_entry e = - let () = Buffer.clear entry_buf in - let ft = Format.formatter_of_buffer entry_buf in - let () = Gram.entry_print ft e in - str (Buffer.contents entry_buf) - -let pr_grammar = function - | "constr" | "operconstr" | "binder_constr" -> - str "Entry constr is" ++ fnl () ++ - pr_entry Pcoq.Constr.constr ++ - str "and lconstr is" ++ fnl () ++ - pr_entry Pcoq.Constr.lconstr ++ - str "where binder_constr is" ++ fnl () ++ - pr_entry Pcoq.Constr.binder_constr ++ - str "and operconstr is" ++ fnl () ++ - pr_entry Pcoq.Constr.operconstr - | "pattern" -> - pr_entry Pcoq.Constr.pattern - | "tactic" -> - str "Entry tactic_expr is" ++ fnl () ++ - pr_entry Pcoq.Tactic.tactic_expr ++ - str "Entry binder_tactic is" ++ fnl () ++ - pr_entry Pcoq.Tactic.binder_tactic ++ - str "Entry simple_tactic is" ++ fnl () ++ - pr_entry Pcoq.Tactic.simple_tactic ++ - str "Entry tactic_arg is" ++ fnl () ++ - pr_entry Pcoq.Tactic.tactic_arg - | "vernac" -> - str "Entry vernac is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.vernac ++ - str "Entry command is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.command ++ - str "Entry syntax is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.syntax ++ - str "Entry gallina is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.gallina ++ - str "Entry gallina_ext is" ++ fnl () ++ - pr_entry 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) *) - -let parse_format ((loc, str) : lstring) = - let str = " "^str in - let l = String.length str in - let push_token a = function - | cur::l -> (a::cur)::l - | [] -> [[a]] in - let push_white n l = - if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in - let close_box i b = function - | a::(_::_ as l) -> push_token (UnpBox (b,a)) l - | _ -> error "Non terminated box in format." in - let close_quotation i = - if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ') - then i+1 - else error "Incorrectly terminated quoted expression." in - let rec spaces n i = - if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1) - else n in - let rec nonspaces quoted n i = - if i < String.length str && str.[i] != ' ' then - if str.[i] == '\'' && quoted && - (i+1 >= String.length str || str.[i+1] == ' ') - then if Int.equal n 0 then error "Empty quoted token." else n - else nonspaces quoted (n+1) (i+1) - else - if quoted then error "Spaces are not allowed in (quoted) symbols." - else n in - let rec parse_non_format i = - let n = nonspaces false 0 i in - push_token (UnpTerminal (String.sub str i n)) (parse_token (i+n)) - and parse_quoted n i = - if i < String.length str then match str.[i] with - (* Parse " // " *) - | '/' when i <= String.length str && str.[i+1] == '/' -> - (* We forget the useless n spaces... *) - push_token (UnpCut PpFnl) - (parse_token (close_quotation (i+2))) - (* Parse " .. / .. " *) - | '/' when i <= String.length str -> - let p = spaces 0 (i+1) in - push_token (UnpCut (PpBrk (n,p))) - (parse_token (close_quotation (i+p+1))) - | c -> - (* The spaces are real spaces *) - push_white n (match c with - | '[' -> - if i <= String.length str then match str.[i+1] with - (* Parse " [h .. ", *) - | 'h' when i+1 <= String.length str && str.[i+2] == 'v' -> - (parse_box (fun n -> PpHVB n) (i+3)) - (* Parse " [v .. ", *) - | 'v' -> - parse_box (fun n -> PpVB n) (i+2) - (* Parse " [ .. ", *) - | ' ' | '\'' -> - parse_box (fun n -> PpHOVB n) (i+1) - | _ -> error "\"v\", \"hv\", \" \" expected after \"[\" in format." - else error "\"v\", \"hv\" or \" \" expected after \"[\" in format." - (* Parse "]" *) - | ']' -> - ([] :: parse_token (close_quotation (i+1))) - (* Parse a non formatting token *) - | c -> - let n = nonspaces true 0 i in - push_token (UnpTerminal (String.sub str (i-1) (n+2))) - (parse_token (close_quotation (i+n)))) - else - if Int.equal n 0 then [] - else error "Ending spaces non part of a format annotation." - and parse_box box i = - let n = spaces 0 i in - close_box i (box n) (parse_token (close_quotation (i+n))) - and parse_token i = - let n = spaces 0 i in - let i = i+n in - if i < l then match str.[i] with - (* Parse a ' *) - | '\'' when i+1 >= String.length str || str.[i+1] == ' ' -> - push_white (n-1) (push_token (UnpTerminal "'") (parse_token (i+1))) - (* Parse the beginning of a quoted expression *) - | '\'' -> - parse_quoted (n-1) (i+1) - (* Otherwise *) - | _ -> - push_white (n-1) (parse_non_format i) - else push_white n [[]] - in - try - if not (String.is_empty str) then match parse_token 0 with - | [l] -> l - | _ -> error "Box closed without being opened in format." - else - error "Empty format." - with reraise -> - let (e, info) = CErrors.push reraise in - let info = Loc.add_loc info loc in - iraise (e, info) - -(***********************) -(* Analyzing notations *) - -type symbol_token = WhiteSpace of int | String of string - -let split_notation_string str = - let push_token beg i l = - if Int.equal beg i then l else - let s = String.sub str beg (i - beg) in - String s :: l - in - let push_whitespace beg i l = - if Int.equal beg i then l else WhiteSpace (i-beg) :: l - in - let rec loop beg i = - if i < String.length str then - if str.[i] == ' ' then - push_token beg i (loop_on_whitespace (i+1) (i+1)) - else - loop beg (i+1) - else - push_token beg i [] - and loop_on_whitespace beg i = - if i < String.length str then - if str.[i] != ' ' then - push_whitespace beg i (loop i (i+1)) - else - loop_on_whitespace beg (i+1) - else - push_whitespace beg i [] - in - loop 0 0 - -(* Interpret notations with a recursive component *) - -let out_nt = function NonTerminal x -> x | _ -> assert false - -let msg_expected_form_of_recursive_notation = - "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"." - -let rec find_pattern nt xl = function - | Break n as x :: l, Break n' :: l' when Int.equal n n' -> - find_pattern nt (x::xl) (l,l') - | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' -> - find_pattern nt (x::xl) (l,l') - | [], NonTerminal x' :: l' -> - (out_nt nt,x',List.rev xl),l' - | _, Break s :: _ | Break s :: _, _ -> - error ("A break occurs on one side of \"..\" but not on the other side.") - | _, Terminal s :: _ | Terminal s :: _, _ -> - errorlabstrm "Metasyntax.find_pattern" - (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") - | _, [] -> - error msg_expected_form_of_recursive_notation - | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> - anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right") - -let rec interp_list_parser hd = function - | [] -> [], List.rev hd - | NonTerminal id :: tl when Id.equal id ldots_var -> - if List.is_empty hd then error msg_expected_form_of_recursive_notation; - let hd = List.rev hd in - let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in - let xyl,tl'' = interp_list_parser [] tl' in - (* We remember each pair of variable denoting a recursive part to *) - (* remove the second copy of it afterwards *) - (x,y)::xyl, SProdList (x,sl) :: tl'' - | (Terminal _ | Break _) as s :: tl -> - if List.is_empty 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 xyl,tl' = interp_list_parser [x] tl in - xyl, List.rev_append hd tl' - | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser") - - -(* Find non-terminal tokens of notation *) - -(* To protect alphabetic tokens and quotes from being seen as variables *) -let quote_notation_token x = - let n = String.length x in - let norm = CLexer.is_ident x in - if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'" - else x - -let rec raw_analyze_notation_tokens = function - | [] -> [] - | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl - | String "_" :: _ -> error "_ must be quoted." - | String x :: sl when CLexer.is_ident x -> - NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl - | String s :: sl -> - Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl - | WhiteSpace n :: sl -> - Break n :: raw_analyze_notation_tokens sl - -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 Failure _ -> false) - | _ -> - false - -let rec get_notation_vars = function - | [] -> [] - | NonTerminal id :: sl -> - let vars = get_notation_vars sl in - if Id.equal id ldots_var then vars else - if Id.List.mem id vars then - errorlabstrm "Metasyntax.get_notation_vars" - (str "Variable " ++ pr_id id ++ str " occurs more than once.") - else - id::vars - | (Terminal _ | Break _) :: sl -> get_notation_vars sl - | SProdList _ :: _ -> assert false - -let analyze_notation_tokens l = - let l = raw_analyze_notation_tokens l in - let vars = get_notation_vars l in - let recvars,l = interp_list_parser [] l in - recvars, List.subtract Id.equal vars (List.map snd recvars), l - -let error_not_same_scope x y = - errorlabstrm "Metasyntax.error_not_name_scope" - (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.") - -(**********************************************************************) -(* Build pretty-printing rules *) - -let prec_assoc = function - | RightA -> (L,E) - | LeftA -> (E,L) - | NonA -> (L,L) - -let precedence_of_entry_type from = function - | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n - | 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 - | _ -> 0, E (* ?? *) - -(* Some breaking examples *) -(* "x = y" : "x /1 = y" (breaks before any symbol) *) -(* "x =S y" : "x /1 =S /1 y" (protect from confusion; each side for symmetry)*) -(* "+ {" : "+ {" may breaks reversibility without space but oth. not elegant *) -(* "x y" : "x spc y" *) -(* "{ x } + { y }" : "{ x } / + { y }" *) -(* "< x , y > { z , t }" : "< x , / y > / { z , / t }" *) - -let starts_with_left_bracket s = - let l = String.length s in not (Int.equal l 0) && - (s.[0] == '{' || s.[0] == '[' || s.[0] == '(') - -let ends_with_right_bracket s = - let l = String.length s in not (Int.equal l 0) && - (s.[l-1] == '}' || s.[l-1] == ']' || s.[l-1] == ')') - -let is_left_bracket s = - starts_with_left_bracket s && not (ends_with_right_bracket s) - -let is_right_bracket s = - not (starts_with_left_bracket s) && ends_with_right_bracket s - -let is_comma s = - let l = String.length s in not (Int.equal l 0) && - (s.[0] == ',' || s.[0] == ';') - -let is_operator s = - let l = String.length s in not (Int.equal l 0) && - (s.[0] == '+' || s.[0] == '*' || s.[0] == '=' || - s.[0] == '-' || s.[0] == '/' || s.[0] == '<' || s.[0] == '>' || - s.[0] == '@' || s.[0] == '\\' || s.[0] == '&' || s.[0] == '~' || s.[0] == '$') - -let is_non_terminal = function - | NonTerminal _ | SProdList _ -> true - | _ -> false - -let is_next_non_terminal = function -| [] -> false -| pr :: _ -> is_non_terminal pr - -let is_next_terminal = function Terminal _ :: _ -> true | _ -> false - -let is_next_break = function Break _ :: _ -> true | _ -> false - -let add_break n l = UnpCut (PpBrk(n,0)) :: l - -let add_break_if_none n = function - | ((UnpCut (PpBrk _) :: _) | []) as l -> l - | l -> UnpCut (PpBrk(n,0)) :: l - -let check_open_binder isopen sl m = - let pr_token = function - | Terminal s -> str s - | Break n -> str "␣" - | _ -> assert false - in - if isopen && not (List.is_empty sl) then - errorlabstrm "" (str "as " ++ pr_id m ++ - str " is a non-closed binder, no such \"" ++ - prlist_with_sep spc pr_token sl - ++ strbrk "\" is allowed to occur.") - -(* Heuristics for building default printing rules *) - -let index_id id l = List.index Id.equal id l - -let make_hunks etyps symbols from = - let vars,typs = List.split etyps in - let rec make = function - | NonTerminal m :: prods -> - let i = index_id m vars in - let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in - let u = UnpMetaVar (i,prec) in - if is_next_non_terminal prods then - u :: add_break_if_none 1 (make prods) - else - u :: make_with_space prods - | Terminal s :: prods when List.exists is_non_terminal prods -> - if (is_comma s || is_operator s) then - (* Always a breakable space after comma or separator *) - UnpTerminal s :: add_break_if_none 1 (make prods) - else if is_right_bracket s && is_next_terminal prods then - (* Always no space after right bracked, but possibly a break *) - UnpTerminal s :: add_break_if_none 0 (make prods) - else if is_left_bracket s && is_next_non_terminal prods then - UnpTerminal s :: make prods - else if not (is_next_break prods) then - (* Add rigid space, no break, unless user asked for something *) - UnpTerminal (s^" ") :: make prods - else - (* Rely on user spaces *) - UnpTerminal s :: make prods - - | Terminal s :: prods -> - (* Separate but do not cut a trailing sequence of terminal *) - (match prods with - | Terminal _ :: _ -> UnpTerminal (s^" ") :: make prods - | _ -> UnpTerminal s :: make prods) - - | Break n :: prods -> - add_break n (make prods) - - | SProdList (m,sl) :: prods -> - let i = index_id m vars in - let typ = List.nth typs (i-1) in - let _,prec = precedence_of_entry_type from typ in - let sl' = - (* If no separator: add a break *) - if List.is_empty sl then add_break 1 [] - (* We add NonTerminal for simulation but remove it afterwards *) - else snd (List.sep_last (make (sl@[NonTerminal m]))) in - let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,sl') - | ETBinder isopen -> - check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,sl') - | _ -> assert false in - hunk :: make_with_space prods - - | [] -> [] - - and make_with_space prods = - match prods with - | Terminal s' :: prods'-> - if is_operator s' then - (* A rigid space before operator and a breakable after *) - UnpTerminal (" "^s') :: add_break_if_none 1 (make prods') - else if is_comma s' then - (* No space whatsoever before comma *) - make prods - else if is_right_bracket s' then - make prods - else - (* A breakable space between any other two terminals *) - add_break_if_none 1 (make prods) - | (NonTerminal _ | SProdList _) :: _ -> - (* A breakable space before a non-terminal *) - add_break_if_none 1 (make prods) - | Break _ :: _ -> - (* Rely on user wish *) - make prods - | [] -> [] - - in make 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 - | UnpTerminal s :: fmt when String.equal s (Id.to_string ldots_var) -> List.rev hd, fmt - | u :: fmt -> - check_no_ldots_in_box u; - split_format_at_ldots (u::hd) fmt - | [] -> raise Exit - -and check_no_ldots_in_box = function - | UnpBox (_,fmt) -> - (try - let _ = split_format_at_ldots [] fmt in - error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.") - with Exit -> ()) - | _ -> () - -let skip_var_in_recursive_format = function - | UnpTerminal _ :: sl (* skip first var *) -> - (* To do, though not so important: check that the names match - the names in the notation *) - sl - | _ -> error_format () - -let read_recursive_format sl fmt = - let get_head fmt = - let sl = skip_var_in_recursive_format fmt in - try split_format_at_ldots [] sl with Exit -> error_format () in - let rec get_tail = function - | a :: sepfmt, b :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *) - | [], tail -> skip_var_in_recursive_format tail - | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"." in - let slfmt, fmt = get_head fmt in - slfmt, get_tail (slfmt, fmt) - -let hunks_of_format (from,(vars,typs)) symfmt = - let rec aux = function - | symbs, (UnpTerminal s' as u) :: fmt - when String.equal s' (String.make (String.length s') ' ') -> - let symbs, l = aux (symbs,fmt) in symbs, u :: l - | Terminal s :: symbs, (UnpTerminal s') :: fmt - when String.equal s (String.drop_simple_quotes s') -> - let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l - | NonTerminal s :: symbs, UnpTerminal s' :: fmt when Id.equal s (Id.of_string s') -> - let i = index_id s vars in - let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in - let symbs, l = aux (symbs,fmt) in symbs, UnpMetaVar (i,prec) :: l - | symbs, UnpBox (a,b) :: fmt -> - let symbs', b' = aux (symbs,b) in - let symbs', l = aux (symbs',fmt) in - symbs', UnpBox (a,b') :: l - | symbs, (UnpCut _ as u) :: fmt -> - let symbs, l = aux (symbs,fmt) in symbs, u :: l - | SProdList (m,sl) :: symbs, fmt -> - let i = index_id m vars in - let typ = List.nth typs (i-1) in - let _,prec = precedence_of_entry_type from typ in - let slfmt,fmt = read_recursive_format sl fmt in - let sl, slfmt = aux (sl,slfmt) in - if not (List.is_empty sl) then error_format (); - let symbs, l = aux (symbs,fmt) in - let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,slfmt) - | ETBinder isopen -> - check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,slfmt) - | _ -> assert false in - symbs, hunk :: l - | symbs, [] -> symbs, [] - | _, _ -> error_format () - in - match aux symfmt with - | [], l -> l - | _ -> error_format () - -(**********************************************************************) -(* Build parsing rules *) - -let assoc_of_type n (_,typ) = precedence_of_entry_type n typ - -let is_not_small_constr = function - ETConstr _ -> true - | ETOther("constr","binder_constr") -> true - | _ -> false - -let rec define_keywords_aux = function - | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l - when is_not_small_constr e -> - Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); - CLexer.add_keyword k; - n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l - | n :: l -> n :: define_keywords_aux l - | [] -> [] - - (* Ensure that IDENT articulation terminal symbols are keywords *) -let define_keywords = function - | GramConstrTerminal(IDENT k)::l -> - Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); - CLexer.add_keyword k; - GramConstrTerminal(KEYWORD k) :: define_keywords_aux l - | l -> define_keywords_aux l - -let distribute a ll = List.map (fun l -> a @ l) ll - - (* Expand LIST1(t,sep) into the combination of t and t;sep;LIST1(t,sep) - as many times as expected in [n] argument *) -let rec expand_list_rule typ tkl x n i hds ll = - if Int.equal i n then - let hds = - GramConstrListMark (n,true) :: hds - @ [GramConstrNonTerminal (ETConstrList (typ,tkl), Some x)] in - distribute hds ll - else - let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in - let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in - let tks = List.map (fun x -> GramConstrTerminal x) tkl in - distribute (GramConstrListMark (i+1,false) :: hds @ [main]) ll @ - expand_list_rule typ tkl x n (i+1) (main :: tks @ hds) ll - -let make_production etyps symbols = - let prod = - List.fold_right - (fun t ll -> match t with - | NonTerminal m -> - let typ = List.assoc m etyps in - distribute [GramConstrNonTerminal (typ, Some m)] ll - | Terminal s -> - distribute [GramConstrTerminal (CLexer.terminal s)] ll - | Break _ -> - ll - | SProdList (x,sl) -> - let tkl = List.flatten - (List.map (function Terminal s -> [CLexer.terminal s] - | Break _ -> [] - | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in - match List.assoc x etyps with - | ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll - | ETBinder o -> - distribute - [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll - | _ -> - error "Components of recursive patterns in notation must be terms or binders.") - symbols [[]] in - List.map define_keywords prod - -let rec find_symbols c_current c_next c_last = function - | [] -> [] - | NonTerminal id :: sl -> - let prec = if not (List.is_empty sl) then c_current else c_last in - (id, prec) :: (find_symbols c_next c_next c_last sl) - | Terminal s :: sl -> find_symbols c_next c_next c_last sl - | Break n :: sl -> find_symbols c_current c_next c_last sl - | SProdList (x,_) :: sl' -> - (x,c_next)::(find_symbols c_next c_next c_last sl') - -let border = function - | (_,ETConstr(_,BorderProd (_,a))) :: _ -> a - | _ -> None - -let recompute_assoc typs = - match border typs, border (List.rev typs) with - | Some LeftA, Some RightA -> assert false - | Some LeftA, _ -> Some LeftA - | _, Some RightA -> Some RightA - | _ -> None - -(**************************************************************************) -(* Registration of syntax extensions (parsing/printing, no interpretation)*) - -let pr_arg_level from = function - | (n,L) when Int.equal n from -> str "at next level" - | (n,E) -> str "at level " ++ int n - | (n,L) -> str "at level below " ++ int n - | (n,Prec m) when Int.equal m n -> str "at level " ++ int n - | (n,_) -> str "Unknown level" - -let pr_level ntn (from,args) = - str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++ - prlist_with_sep pr_comma (pr_arg_level from) args - -let error_incompatible_level ntn oldprec prec = - errorlabstrm "" - (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++ - pr_level ntn oldprec ++ - spc() ++ str "while it is now required to be" ++ spc() ++ - pr_level ntn prec ++ str ".") - -type syntax_extension = { - synext_level : Notation.level; - synext_notation : notation; - synext_notgram : notation_grammar; - synext_unparsing : unparsing list; - synext_extra : (string * string) list; - synext_compat : Flags.compat_version option; -} - -let is_active_compat = function -| None -> true -| Some v -> 0 <= Flags.version_compare v !Flags.compat_version - -type syntax_extension_obj = locality_flag * syntax_extension list - -let cache_one_syntax_extension se = - let ntn = se.synext_notation in - let prec = se.synext_level in - let onlyprint = se.synext_notgram.notgram_onlyprinting in - try - let oldprec = Notation.level_of_notation ntn in - if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec - with Not_found -> - if is_active_compat se.synext_compat then begin - (* Reserve the notation level *) - Notation.declare_notation_level ntn prec; - (* Declare the parsing rule *) - if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; - (* Declare the notation rule *) - Notation.declare_notation_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram - end - -let cache_syntax_extension (_, (_, sy)) = - List.iter cache_one_syntax_extension sy - -let subst_parsing_rule subst x = x - -let subst_printing_rule subst x = x - -let subst_syntax_extension (subst, (local, sy)) = - let map sy = { sy with - synext_notgram = subst_parsing_rule subst sy.synext_notgram; - synext_unparsing = subst_printing_rule subst sy.synext_unparsing; - } in - (local, List.map map sy) - -let classify_syntax_definition (local, _ as o) = - if local then Dispose else Substitute o - -let inSyntaxExtension : syntax_extension_obj -> obj = - declare_object {(default_object "SYNTAX-EXTENSION") with - open_function = (fun i o -> if Int.equal i 1 then cache_syntax_extension o); - cache_function = cache_syntax_extension; - subst_function = subst_syntax_extension; - classify_function = classify_syntax_definition} - -(**************************************************************************) -(* Precedences *) - -(* Interpreting user-provided modifiers *) - -let interp_modifiers modl = - let onlyparsing = ref false in - let onlyprinting = ref false in - let compat = ref None in - let rec interp assoc level etyps format extra = function - | [] -> - (assoc,level,etyps,!onlyparsing,!onlyprinting,!compat,format,extra) - | SetEntryType (s,typ) :: l -> - let id = Id.of_string s in - if Id.List.mem_assoc id etyps then - errorlabstrm "Metasyntax.interp_modifiers" - (str s ++ str " is already assigned to an entry or constr level."); - interp assoc level ((id,typ)::etyps) format extra l - | SetItemLevel ([],n) :: l -> - interp assoc level etyps format extra l - | SetItemLevel (s::idl,n) :: l -> - let id = Id.of_string s in - if Id.List.mem_assoc id etyps then - errorlabstrm "Metasyntax.interp_modifiers" - (str s ++ str " is already assigned to an entry or constr level."); - let typ = ETConstr (n,()) in - interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l) - | SetLevel n :: l -> - if not (Option.is_empty level) then error "A level is given more than once."; - interp assoc (Some n) etyps format extra l - | SetAssoc a :: l -> - if not (Option.is_empty assoc) then error"An associativity is given more than once."; - interp (Some a) level etyps format extra l - | SetOnlyParsing :: l -> - onlyparsing := true; - interp assoc level etyps format extra l - | SetOnlyPrinting :: l -> - onlyprinting := true; - interp assoc level etyps format extra l - | SetCompatVersion v :: l -> - compat := Some v; - interp assoc level etyps format extra l - | SetFormat ("text",s) :: l -> - if not (Option.is_empty format) then error "A format is given more than once."; - interp assoc level etyps (Some s) extra l - | SetFormat (k,(_,s)) :: l -> - interp assoc level etyps format ((k,s) :: extra) l - in interp None None [] None [] modl - -let check_infix_modifiers modifiers = - let (_, _, t, _, _, _, _, _) = interp_modifiers modifiers in - if not (List.is_empty t) then - error "Explicit entry level or type unexpected in infix notation." - -let check_useless_entry_types recvars mainvars etyps = - let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in - match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with - | (x,_)::_ -> errorlabstrm "Metasyntax.check_useless_entry_types" - (pr_id x ++ str " is unbound in the notation.") - | _ -> () - -let not_a_syntax_modifier = function -| SetOnlyParsing -> true -| SetOnlyPrinting -> true -| SetCompatVersion _ -> true -| _ -> false - -let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods - -let is_only_parsing mods = - let test = function SetOnlyParsing -> true | _ -> false in - List.exists test mods - -let is_only_printing mods = - let test = function SetOnlyPrinting -> true | _ -> false in - List.exists test mods - -let get_compat_version mods = - let test = function SetCompatVersion v -> Some v | _ -> None in - try Some (List.find_map test mods) with Not_found -> None - -(* Compute precedences from modifiers (or find default ones) *) - -let set_entry_type etyps (x,typ) = - let typ = try - match List.assoc x etyps, typ with - | ETConstr (n,()), (_,BorderProd (left,_)) -> - ETConstr (n,BorderProd (left,None)) - | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd) - | (ETPattern | ETName | ETBigint | ETOther _ | - ETReference | ETBinder _ as t), _ -> t - | (ETBinderList _ |ETConstrList _), _ -> assert false - with Not_found -> ETConstr typ - in (x,typ) - -let join_auxiliary_recursive_types recvars etyps = - List.fold_right (fun (x,y) typs -> - let xtyp = try Some (List.assoc x etyps) with Not_found -> None in - let ytyp = try Some (List.assoc y etyps) with Not_found -> None in - match xtyp,ytyp with - | None, None -> typs - | Some _, None -> typs - | None, Some ytyp -> (x,ytyp)::typs - | Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *) - | Some xtyp, Some ytyp -> - errorlabstrm "" - (strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++ - strbrk ", both ends have incompatible types.")) - recvars etyps - -let internalization_type_of_entry_type = function - | ETConstr _ -> NtnInternTypeConstr - | ETBigint | ETReference -> NtnInternTypeConstr - | ETBinder _ -> NtnInternTypeBinder - | ETName -> NtnInternTypeIdent - | ETPattern | ETOther _ -> error "Not supported." - | ETBinderList _ | ETConstrList _ -> assert false - -let set_internalization_type typs = - List.map (fun (_, e) -> internalization_type_of_entry_type e) typs - -let make_internalization_vars recvars mainvars typs = - let maintyps = List.combine mainvars typs in - let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in - maintyps @ extratyps - -let make_interpretation_type isrec isonlybinding = function - | NtnInternTypeConstr when isrec -> NtnTypeConstrList - | NtnInternTypeConstr | NtnInternTypeIdent -> - if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr - | NtnInternTypeBinder when isrec -> NtnTypeBinderList - | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders." - -let make_interpretation_vars recvars allvars = - let eq_subscope (sc1, l1) (sc2, l2) = - Option.equal String.equal sc1 sc2 && - List.equal String.equal l1 l2 - in - let check (x, y) = - let (_,scope1, _) = Id.Map.find x allvars in - let (_,scope2, _) = Id.Map.find y allvars in - if not (eq_subscope scope1 scope2) then error_not_same_scope x y - in - let () = List.iter check recvars in - let useless_recvars = List.map snd recvars in - let mainvars = - Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in - Id.Map.mapi (fun x (isonlybinding, sc, typ) -> - (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars - -let check_rule_productivity l = - if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then - error "A notation must include at least one symbol."; - if (match l with SProdList _ :: _ -> true | _ -> false) then - error "A recursive notation must start with at least one symbol." - -let warn_notation_bound_to_variable = - CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing" - (fun () -> - strbrk "This notation will not be used for printing as it is bound to a single variable.") - -let warn_non_reversible_notation = - CWarnings.create ~name:"non-reversible-notation" ~category:"parsing" - (fun () -> - strbrk "This notation will not be used for printing as it is not reversible.") - -let is_not_printable onlyparse nonreversible = function -| NVar _ -> - if not onlyparse then warn_notation_bound_to_variable (); - true -| _ -> - if not onlyparse && nonreversible then - (warn_non_reversible_notation (); true) - else onlyparse - -let find_precedence lev etyps symbols = - let first_symbol = - let rec aux = function - | Break _ :: t -> aux t - | h :: t -> h - | [] -> assert false (* rule is known to be productive *) in - aux symbols in - let last_is_terminal () = - let rec aux b = function - | Break _ :: t -> aux b t - | Terminal _ :: t -> aux true t - | _ :: t -> aux false t - | [] -> b in - aux false symbols in - match first_symbol with - | NonTerminal x -> - (try match List.assoc x etyps with - | ETConstr _ -> - error "The level of the leftmost non-terminal cannot be changed." - | ETName | ETBigint | ETReference -> - begin match lev with - | None -> - ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0) - | Some 0 -> - ([],0) - | _ -> - error "A notation starting with an atomic expression must be at level 0." - end - | ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *) - if Option.is_empty lev then - error "Need an explicit level." - else [],Option.get lev - | ETConstrList _ | ETBinderList _ -> - assert false (* internally used in grammar only *) - with Not_found -> - if Option.is_empty lev then - error "A left-recursive notation must have an explicit level." - else [],Option.get lev) - | Terminal _ when last_is_terminal () -> - if Option.is_empty lev then - ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0) - else [],Option.get lev - | _ -> - if Option.is_empty lev then error "Cannot determine the level."; - [],Option.get lev - -let check_curly_brackets_notation_exists () = - 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." - -let warn_skip_spaces_curly = - CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing" - (fun () ->strbrk "Skipping spaces inside curly brackets") - -(* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *) -let remove_curly_brackets l = - let rec skip_break acc = function - | Break _ as br :: l -> skip_break (br::acc) l - | l -> List.rev acc, l in - let rec aux deb = function - | [] -> [] - | Terminal "{" as t1 :: l -> - let br,next = skip_break [] l in - (match next with - | NonTerminal _ as x :: l' as l0 -> - let br',next' = skip_break [] l' in - (match next' with - | Terminal "}" as t2 :: l'' as l1 -> - if not (List.equal Notation.symbol_eq l l0) || - not (List.equal Notation.symbol_eq l' l1) then - warn_skip_spaces_curly (); - if deb && List.is_empty l'' then [t1;x;t2] else begin - check_curly_brackets_notation_exists (); - x :: aux false l'' - end - | l1 -> t1 :: br @ x :: br' @ aux false l1) - | l0 -> t1 :: aux false l0) - | x :: l -> x :: aux false l - in aux true l - -let compute_syntax_data df modifiers = - let (assoc,n,etyps,onlyparse,onlyprint,compat,fmt,extra) = interp_modifiers modifiers in - let assoc = match assoc with None -> (* default *) Some NonA | a -> a in - let toks = split_notation_string df in - let (recvars,mainvars,symbols) = analyze_notation_tokens toks in - let _ = check_useless_entry_types recvars mainvars etyps in - let ntn_for_interp = make_notation_key symbols in - let symbols' = remove_curly_brackets symbols in - let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in - let ntn_for_grammar = make_notation_key symbols' in - check_rule_productivity symbols'; - let msgs,n = find_precedence n etyps symbols' in - let innerlevel = NumLevel 200 in - let typs = - find_symbols - (NumLevel n,BorderProd(Left,assoc)) - (innerlevel,InternalProd) - (NumLevel n,BorderProd(Right,assoc)) - symbols' in - (* To globalize... *) - let etyps = join_auxiliary_recursive_types recvars etyps in - let sy_typs = List.map (set_entry_type etyps) typs in - let prec = (n,List.map (assoc_of_type n) sy_typs) in - let i_typs = set_internalization_type sy_typs in - let sy_data = (n,sy_typs,symbols',fmt) in - let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in - let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in - let i_data = (onlyparse,onlyprint,compat,recvars,mainvars,(ntn_for_interp,df')) in - (* Return relevant data for interpretation and for parsing/printing *) - (msgs,i_data,i_typs,sy_fulldata,extra) - -let compute_pure_syntax_data df mods = - let (msgs,(onlyparse,onlyprint,_,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in - let msgs = - if onlyparse then - (Feedback.msg_warning ?loc:None, - strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs - else msgs in - msgs, sy_data, extra, onlyprint - -(**********************************************************************) -(* Registration of notations interpretation *) - -type notation_obj = { - notobj_local : bool; - notobj_scope : scope_name option; - notobj_interp : interpretation; - notobj_onlyparse : bool; - notobj_onlyprint : bool; - notobj_compat : Flags.compat_version option; - notobj_notation : notation * notation_location; -} - -let load_notation _ (_, nobj) = - Option.iter Notation.declare_scope nobj.notobj_scope - -let open_notation i (_, nobj) = - let scope = nobj.notobj_scope in - let (ntn, df) = nobj.notobj_notation in - let pat = nobj.notobj_interp in - let fresh = not (Notation.exists_notation_in_scope scope ntn pat) in - let active = is_active_compat nobj.notobj_compat in - if Int.equal i 1 && fresh && active then begin - (* Declare the interpretation *) - let onlyprint = nobj.notobj_onlyprint in - let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in - (* Declare the uninterpretation *) - if not nobj.notobj_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, nobj) = - { nobj with notobj_interp = subst_interpretation subst nobj.notobj_interp; } - -let classify_notation nobj = - if nobj.notobj_local then Dispose else Substitute nobj - -let inNotation : notation_obj -> obj = - declare_object {(default_object "NOTATION") with - open_function = open_notation; - cache_function = cache_notation; - subst_function = subst_notation; - load_function = load_notation; - classify_function = classify_notation} - -(**********************************************************************) - -let with_lib_stk_protection f x = - let fs = Lib.freeze `No in - try let a = f x in Lib.unfreeze fs; a - with reraise -> - let reraise = CErrors.push reraise in - let () = Lib.unfreeze fs in - iraise reraise - -let with_syntax_protection f x = - with_lib_stk_protection - (with_grammar_rule_protection - (with_notation_protection f)) x - -(**********************************************************************) -(* Recovering existing syntax *) - -let contract_notation ntn = - if String.equal ntn "{ _ }" then ntn else - let rec aux ntn i = - if i <= String.length ntn - 5 then - let ntn' = - if String.is_sub "{ _ }" ntn i && - (i = 0 || ntn.[i-1] = ' ') && - (i = String.length ntn - 5 || ntn.[i+5] = ' ') - then - String.sub ntn 0 i ^ "_" ^ - String.sub ntn (i+5) (String.length ntn -i-5) - else ntn in - aux ntn' (i+1) - else ntn in - aux ntn 0 - -exception NoSyntaxRule - -let recover_syntax ntn = - try - let prec = Notation.level_of_notation ntn in - let pp_rule,_ = Notation.find_notation_printing_rule ntn in - let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in - let pa_rule = Notation.find_notation_parsing_rules ntn in - { synext_level = prec; - synext_notation = ntn; - synext_notgram = pa_rule; - synext_unparsing = pp_rule; - synext_extra = pp_extra_rules; - synext_compat = None; - } - with Not_found -> - raise NoSyntaxRule - -let recover_squash_syntax sy = - let sq = recover_syntax "{ _ }" in - [sy; sq] - -let recover_notation_syntax rawntn = - let ntn = contract_notation rawntn in - let sy = recover_syntax ntn in - let need_squash = not (String.equal ntn rawntn) in - let rules = if need_squash then recover_squash_syntax sy else [sy] in - sy.synext_notgram.notgram_typs, rules, sy.synext_notgram.notgram_onlyprinting - -(**********************************************************************) -(* Main entry point for building parsing and printing rules *) - -let make_pa_rule i_typs (n,typs,symbols,_) ntn onlyprint = - let assoc = recompute_assoc typs in - let prod = make_production typs symbols in - { notgram_level = n; - notgram_assoc = assoc; - notgram_notation = ntn; - notgram_prods = prod; - notgram_typs = i_typs; - notgram_onlyprinting = onlyprint; - } - -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 (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint compat = - let pa_rule = make_pa_rule i_typs sy_data ntn onlyprint in - let pp_rule = make_pp_rule sy_data in - let sy = { - synext_level = prec; - synext_notation = ntn; - synext_notgram = pa_rule; - synext_unparsing = pp_rule; - synext_extra = extra; - synext_compat = compat; - } 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 recover_squash_syntax sy else [sy] - -(**********************************************************************) -(* Main functions about notations *) - -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 (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in - (* Prepare the interpretation *) - let (onlyparse, onlyprint, compat, recvars,mainvars, df') = i_data in - (* Prepare the parsing and printing rules *) - let sy_rules = make_syntax_rules sy_data extra onlyprint compat in - let i_vars = make_internalization_vars recvars mainvars i_typs in - let nenv = { - ninterp_var_type = to_map i_vars; - ninterp_rec_vars = to_map recvars; - } in - let (acvars, ac, reversible) = interp_notation_constr 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 - let notation = { - notobj_local = local; - notobj_scope = scope; - notobj_interp = (List.map_filter map i_vars, ac); - (** Order is important here! *) - notobj_onlyparse = onlyparse; - notobj_onlyprint = onlyprint; - notobj_compat = compat; - notobj_notation = df'; - } in - (* Ready to change the global state *) - Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; - Lib.add_anonymous_leaf (inSyntaxExtension (local, sy_rules)); - Lib.add_anonymous_leaf (inNotation notation); - df' - -let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = - let dfs = split_notation_string df in - let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in - (* Recover types of variables and pa/pp rules; redeclare them if needed *) - let i_typs, onlyprint = if not (is_numeral symbs) then begin - let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in - let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)) in - (** If the only printing flag has been explicitly requested, put it back *) - let onlyprint = onlyprint || onlyprint' in - i_typs, onlyprint - end else [], false in - (* Declare interpretation *) - let path = (Lib.library_dp(),Lib.current_dirpath true) in - let df' = (make_notation_key symbs,(path,df)) in - let i_vars = make_internalization_vars recvars mainvars i_typs in - let nenv = { - 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 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 - let notation = { - notobj_local = local; - notobj_scope = scope; - notobj_interp = (List.map_filter map i_vars, ac); - (** Order is important here! *) - notobj_onlyparse = onlyparse; - notobj_onlyprint = onlyprint; - notobj_compat = compat; - notobj_notation = df'; - } in - Lib.add_anonymous_leaf (inNotation notation); - df' - -(* Notations without interpretation (Reserved Notation) *) - -let add_syntax_extension local ((loc,df),mods) = - let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in - let sy_rules = make_syntax_rules sy_data extra onlyprint None in - Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; - Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) - -(* 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 - Dumpglob.dump_notation (loc,df') sc true - -let set_notation_for_interpretation impls ((_,df),c,sc) = - (try ignore - (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); - with NoSyntaxRule -> - error "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 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 - 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 - in - Dumpglob.dump_notation (loc,df') sc true - -let add_notation_extra_printing_rule df k v = - let notk = - let dfs = split_notation_string df in - let _,_, symbs = analyze_notation_tokens dfs in - make_notation_key symbs in - Notation.add_notation_extra_printing_rule notk k v - -(* Infix notations *) - -let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x),None) - -let add_infix local ((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 - -(**********************************************************************) -(* Delimiters and classes bound to scopes *) - -type scope_command = - | ScopeDelim of string - | ScopeClasses of scope_class list - | ScopeRemove - -let load_scope_command _ (_,(scope,dlm)) = - Notation.declare_scope scope - -let open_scope_command i (_,(scope,o)) = - if Int.equal i 1 then - match o with - | ScopeDelim dlm -> Notation.declare_delimiters scope dlm - | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl - | ScopeRemove -> Notation.remove_delimiters scope - -let cache_scope_command o = - load_scope_command 1 o; - open_scope_command 1 o - -let subst_scope_command (subst,(scope,o as x)) = match o with - | ScopeClasses cl -> - let cl' = List.map_filter (subst_scope_class subst) cl in - let cl' = - if List.for_all2eq (==) cl cl' then cl - else cl' in - scope, ScopeClasses cl' - | _ -> x - -let inScopeCommand : scope_name * scope_command -> obj = - declare_object {(default_object "DELIMITERS") with - cache_function = cache_scope_command; - open_function = open_scope_command; - load_function = load_scope_command; - subst_function = subst_scope_command; - classify_function = (fun obj -> Substitute obj)} - -let add_delimiters scope key = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key)) - -let remove_delimiters scope = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove)) - -let add_class_scope scope cl = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl)) - -(* Check if abbreviation to a name and avoid early insertion of - maximal implicit arguments *) -let try_interp_name_alias = function - | [], CRef (ref,_) -> intern_reference ref - | _ -> raise Not_found - -let add_syntactic_definition ident (vars,c) local onlyparse = - let nonprintable = ref false in - let vars,pat = - try [], NRef (try_interp_name_alias (vars,c)) - with Not_found -> - let fold accu id = Id.Map.add id NtnInternTypeConstr accu in - let i_vars = List.fold_left fold Id.Map.empty vars in - let nenv = { - ninterp_var_type = i_vars; - ninterp_rec_vars = Id.Map.empty; - } in - let nvars, pat, reversible = interp_notation_constr 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 - in - let onlyparse = match onlyparse with - | None when (is_not_printable false !nonprintable pat) -> Some Flags.Current - | p -> p - in - Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) - |