summaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/metasyntax.ml')
-rw-r--r--toplevel/metasyntax.ml832
1 files changed, 519 insertions, 313 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 5a20f1c1..161cf824 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,33 +8,34 @@
open Pp
open Flags
-open Compat
+open Errors
open Util
open Names
-open Topconstr
+open Constrexpr
+open Constrexpr_ops
+open Notation_term
+open Notation_ops
open Ppextend
open Extend
open Libobject
-open Summary
open Constrintern
open Vernacexpr
open Pcoq
-open Glob_term
open Libnames
open Tok
-open Lexer
-open Egrammar
+open Egramml
+open Egramcoq
open Notation
open Nameops
(**********************************************************************)
(* Tokens *)
-let cache_token (_,s) = add_keyword s
+let cache_token (_,s) = Lexer.add_keyword s
let inToken : string -> obj =
declare_object {(default_object "TOKEN") with
- open_function = (fun i o -> if i=1 then cache_token o);
+ 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)}
@@ -60,113 +61,184 @@ let rec make_tags = function
| GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l
| [] -> []
-let cache_tactic_notation (_,(pa,pp)) =
- Egrammar.extend_grammar (Egrammar.TacticGrammar pa);
- Pptactic.declare_extra_tactic_pprule pp
+type tactic_grammar_obj = {
+ tacobj_local : locality_flag;
+ tacobj_tacgram : tactic_grammar;
+ tacobj_tacpp : Pptactic.pp_tactic;
+ tacobj_body : Tacexpr.glob_tactic_expr
+}
-let subst_tactic_parule subst (key,n,p,(d,tac)) =
- (key,n,p,(d,Tacinterp.subst_tactic subst tac))
+let cache_tactic_notation ((_, key), tobj) =
+ Tacenv.register_alias key tobj.tacobj_body;
+ Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
+ Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
-let subst_tactic_notation (subst,(pa,pp)) =
- (subst_tactic_parule subst pa,pp)
+let open_tactic_notation i ((_, key), tobj) =
+ if Int.equal i 1 && not tobj.tacobj_local then
+ Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
-type tactic_grammar_obj =
- (string * int * grammar_prod_item list *
- (dir_path * Tacexpr.glob_tactic_expr))
- * (string * Genarg.argument_type list * (int * Pptactic.grammar_terminals))
+let load_tactic_notation i ((_, key), tobj) =
+ (** Only add the printing and interpretation rules. *)
+ Tacenv.register_alias key tobj.tacobj_body;
+ Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
+ if Int.equal i 1 && not tobj.tacobj_local then
+ Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+
+let subst_tactic_notation (subst, tobj) =
+ { tobj with tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body; }
+
+let classify_tactic_notation tacobj = Substitute tacobj
let inTacticGrammar : tactic_grammar_obj -> obj =
declare_object {(default_object "TacticGrammar") with
- open_function = (fun i o -> if i=1 then cache_tactic_notation o);
+ open_function = open_tactic_notation;
+ load_function = load_tactic_notation;
cache_function = cache_tactic_notation;
subst_function = subst_tactic_notation;
- classify_function = (fun o -> Substitute o)}
+ classify_function = classify_tactic_notation}
let cons_production_parameter l = function
| GramTerminal _ -> l
| GramNonTerminal (_,_,_,ido) -> Option.List.cons ido l
-let rec tactic_notation_key = function
- | GramTerminal id :: _ -> id
- | _ :: l -> tactic_notation_key l
- | [] -> "terminal_free_notation"
-
-let rec next_key_away key t =
- if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t
- else key
-
-let add_tactic_notation (n,prods,e) =
+let add_tactic_notation (local,n,prods,e) =
let prods = List.map (interp_prod_item n) prods in
let tags = make_tags 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 pprule = {
+ Pptactic.pptac_args = tags;
+ pptac_prods = (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 tac = Tacintern.glob_tactic_env ids (Global.env()) e in
+ let parule = {
+ tacgram_level = n;
+ tacgram_prods = prods;
+ } in
+ let tacobj = {
+ tacobj_local = local;
+ tacobj_tacgram = parule;
+ tacobj_tacpp = pprule;
+ tacobj_body = tac;
+ } in
+ Lib.add_anonymous_leaf (inTacticGrammar tacobj)
+
+(**********************************************************************)
+(* ML Tactic entries *)
+
+type atomic_entry = string * Genarg.glob_generic_argument list option
+
+type ml_tactic_grammar_obj = {
+ mltacobj_name : Tacexpr.ml_tactic_name;
+ (** ML-side unique name *)
+ mltacobj_prod : grammar_prod_item list list;
+ (** Grammar rules generating the ML tactic. *)
+}
+
+(** ML tactic notations whose use can be restricted to an identifier are added
+ as true Ltac entries. *)
+let extend_atomic_tactic name entries =
+ let add_atomic (id, args) = match args with
+ | None -> ()
+ | Some args ->
+ let body = Tacexpr.TacML (Loc.ghost, name, args) in
+ Tacenv.register_ltac false false (Names.Id.of_string id) body
+ in
+ List.iter add_atomic entries
+
+let cache_ml_tactic_notation (_, obj) =
+ extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
+
+let open_ml_tactic_notation i obj =
+ if Int.equal i 1 then cache_ml_tactic_notation obj
+
+let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
+ declare_object { (default_object "MLTacticGrammar") with
+ open_function = open_ml_tactic_notation;
+ cache_function = cache_ml_tactic_notation;
+ classify_function = (fun o -> Substitute o);
+ subst_function = (fun (_, o) -> o);
+ }
+
+let add_ml_tactic_notation name prods atomic =
+ let obj = {
+ mltacobj_name = name;
+ mltacobj_prod = prods;
+ } in
+ Lib.add_anonymous_leaf (inMLTacticGrammar obj);
+ extend_atomic_tactic name atomic
(**********************************************************************)
(* Printing grammar entries *)
-let print_grammar = function
+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" ->
- 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;
+ 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" ->
- Gram.entry_print Pcoq.Constr.pattern
+ pr_entry Pcoq.Constr.pattern
| "tactic" ->
- msgnl (str "Entry tactic_expr is");
- Gram.entry_print Pcoq.Tactic.tactic_expr;
- msgnl (str "Entry binder_tactic is");
- Gram.entry_print Pcoq.Tactic.binder_tactic;
- msgnl (str "Entry simple_tactic is");
- Gram.entry_print Pcoq.Tactic.simple_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" ->
- 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;
+ 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) =
+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 n = 0 then l else push_token (UnpTerminal (String.make n ' ')) l in
+ 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] = '\'' & (i+1 = l or str.[i+1] = ' ')
+ 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)
+ 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 or str.[i+1] = ' ')
- then if n=0 then error "Empty quoted token." else n
+ 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."
@@ -177,7 +249,7 @@ let parse_format (loc,str) =
and parse_quoted n i =
if i < String.length str then match str.[i] with
(* Parse " // " *)
- | '/' when i <= String.length str & str.[i+1] = '/' ->
+ | '/' when i <= String.length str && str.[i+1] == '/' ->
(* We forget the useless n spaces... *)
push_token (UnpCut PpFnl)
(parse_token (close_quotation (i+2)))
@@ -192,7 +264,7 @@ let parse_format (loc,str) =
| '[' ->
if i <= String.length str then match str.[i+1] with
(* Parse " [h .. ", *)
- | 'h' when i+1 <= String.length str & str.[i+2] = 'v' ->
+ | 'h' when i+1 <= String.length str && str.[i+2] == 'v' ->
(parse_box (fun n -> PpHVB n) (i+3))
(* Parse " [v .. ", *)
| 'v' ->
@@ -211,7 +283,7 @@ let parse_format (loc,str) =
push_token (UnpTerminal (String.sub str (i-1) (n+2)))
(parse_token (close_quotation (i+n))))
else
- if n = 0 then []
+ 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
@@ -221,7 +293,7 @@ let parse_format (loc,str) =
let i = i+n in
if i < l then match str.[i] with
(* Parse a ' *)
- | '\'' when i+1 >= String.length str or str.[i+1] = ' ' ->
+ | '\'' 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 *)
| '\'' ->
@@ -232,13 +304,15 @@ let parse_format (loc,str) =
else push_white n [[]]
in
try
- if str <> "" then match parse_token 0 with
+ 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 e when Errors.noncritical e ->
- Loc.raise loc e
+ with reraise ->
+ let (e, info) = Errors.push reraise in
+ let info = Loc.add_loc info loc in
+ iraise (e, info)
(***********************)
(* Analyzing notations *)
@@ -247,16 +321,16 @@ type symbol_token = WhiteSpace of int | String of string
let split_notation_string str =
let push_token beg i l =
- if beg = i then l else
+ 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 beg = i then l else WhiteSpace (i-beg) :: 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
+ if str.[i] == ' ' then
push_token beg i (loop_on_whitespace (i+1) (i+1))
else
loop beg (i+1)
@@ -264,7 +338,7 @@ let split_notation_string str =
push_token beg i []
and loop_on_whitespace beg i =
if i < String.length str then
- if str.[i] <> ' ' then
+ if str.[i] != ' ' then
push_whitespace beg i (loop i (i+1))
else
loop_on_whitespace beg (i+1)
@@ -281,25 +355,25 @@ 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 n=n' ->
+ | 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 s = s' ->
+ | 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'
- | _, Terminal s :: _ | Terminal s :: _, _ ->
- error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
| _, Break s :: _ | Break s :: _, _ ->
error ("A break occurs on one side of \"..\" but not on the other side.")
+ | _, Terminal s :: _ | Terminal s :: _, _ ->
+ error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
| _, [] ->
error msg_expected_form_of_recursive_notation
| ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
- anomaly "Only Terminal or Break expected on left, non-SProdList on right"
+ 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 = ldots_var ->
- if hd = [] then error msg_expected_form_of_recursive_notation;
+ | 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
@@ -307,7 +381,7 @@ let rec interp_list_parser hd = function
(* remove the second copy of it afterwards *)
(x,y)::xyl, SProdList (x,sl) :: tl''
| (Terminal _ | Break _) as s :: tl ->
- if hd = [] then
+ if List.is_empty hd then
let yl,tl' = interp_list_parser [] tl in
yl, s :: tl'
else
@@ -315,7 +389,7 @@ let rec interp_list_parser hd = function
| NonTerminal _ as x :: tl ->
let xyl,tl' = interp_list_parser [x] tl in
xyl, List.rev_append hd tl'
- | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
+ | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser")
(* Find non-terminal tokens of notation *)
@@ -323,26 +397,25 @@ let rec interp_list_parser hd = function
(* To protect alphabetic tokens and quotes from being seen as variables *)
let quote_notation_token x =
let n = String.length x in
- let norm = is_ident x in
- if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
+ let norm = Lexer.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 is_ident x ->
- NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl
+ | String x :: sl when Lexer.is_ident x ->
+ NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
| String s :: sl ->
- Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens 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 e when Errors.noncritical e -> false)
+ (try let _ = Bigint.of_string x in true with Failure _ -> false)
| _ ->
false
@@ -350,9 +423,9 @@ let rec get_notation_vars = function
| [] -> []
| NonTerminal id :: sl ->
let vars = get_notation_vars sl in
- if id = ldots_var then vars else
- if List.mem id vars then
- error ("Variable "^string_of_id id^" occurs more than once.")
+ if Id.equal id ldots_var then vars else
+ if Id.List.mem id vars then
+ error ("Variable "^Id.to_string id^" occurs more than once.")
else
id::vars
| (Terminal _ | Break _) :: sl -> get_notation_vars sl
@@ -362,18 +435,15 @@ 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 vars (List.map snd recvars), l
+ recvars, List.subtract Id.equal vars (List.map snd recvars), l
let error_not_same_scope x y =
- error ("Variables "^string_of_id x^" and "^string_of_id y^
+ error ("Variables "^Id.to_string x^" and "^Id.to_string y^
" must be in the same scope.")
(**********************************************************************)
(* Build pretty-printing rules *)
-type printing_precedence = int * parenRelation
-type parsing_precedence = int option
-
let prec_assoc = function
| RightA -> (L,E)
| LeftA -> (E,L)
@@ -382,7 +452,7 @@ let prec_assoc = function
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
+ 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 (* ?? *)
@@ -395,36 +465,50 @@ let precedence_of_entry_type from = function
(* "{ 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 =
- let l = String.length s in l <> 0 &
- (s.[0] = '{' or s.[0] = '[' or s.[0] = '(')
+ starts_with_left_bracket s && not (ends_with_right_bracket s)
let is_right_bracket s =
- let l = String.length s in l <> 0 &
- (s.[l-1] = '}' or s.[l-1] = ']' or s.[l-1] = ')')
+ not (starts_with_left_bracket s) && ends_with_right_bracket s
let is_comma s =
- let l = String.length s in l <> 0 &
- (s.[0] = ',' or s.[0] = ';')
+ 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 l <> 0 &
- (s.[0] = '+' or s.[0] = '*' or s.[0] = '=' or
- s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or
- s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~' or s.[0] = '$')
+ 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_prod_ident = function
- | Terminal s when is_letter s.[0] or s.[0] = '_' -> true
- | _ -> false
-
-let rec is_non_terminal = function
+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 =
- if isopen & sl <> [] then
+ 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 (function Terminal s -> str s | _ -> assert false) sl
@@ -432,84 +516,93 @@ let check_open_binder isopen sl m =
(* Heuristics for building default printing rules *)
-type previous_prod_status = NoBreak | CanBreak
+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 ws = function
+ let rec make = function
| NonTerminal m :: prods ->
- let i = list_index m vars in
+ 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 prods <> [] && is_non_terminal (List.hd prods) then
- u :: add_break 1 (make CanBreak prods)
+ if is_next_non_terminal prods then
+ u :: add_break_if_none 1 (make prods)
else
- u :: make CanBreak prods
-
+ u :: make_with_space prods
| Terminal s :: prods when List.exists is_non_terminal prods ->
- if is_comma s then
- UnpTerminal s :: add_break 1 (make NoBreak prods)
- else if is_right_bracket s then
- UnpTerminal s :: add_break 0 (make NoBreak prods)
- else if is_left_bracket s then
- if ws = CanBreak then
- add_break 1 (UnpTerminal s :: make CanBreak prods)
- else
- UnpTerminal s :: make CanBreak prods
- else if is_operator s then
- if ws = CanBreak then
- UnpTerminal (" "^s) :: add_break 1 (make NoBreak prods)
- else
- UnpTerminal s :: add_break 1 (make NoBreak prods)
- else if is_ident_tail s.[String.length s - 1] then
- let sep = if is_prod_ident (List.hd prods) then "" else " " in
- if ws = CanBreak then
- add_break 1 (UnpTerminal (s^sep) :: make CanBreak prods)
- else
- UnpTerminal (s^sep) :: make CanBreak prods
- else if ws = CanBreak then
- add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods)
- else
- UnpTerminal s :: make CanBreak 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 ->
- if is_right_bracket s then
- UnpTerminal s :: make NoBreak prods
- else if ws = CanBreak then
- add_break 1 (UnpTerminal s :: make NoBreak prods)
- else
- UnpTerminal s :: make NoBreak 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 NoBreak prods)
+ add_break n (make prods)
| SProdList (m,sl) :: prods ->
- let i = list_index m vars in
+ 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 sl = [] then add_break 1 []
+ if List.is_empty sl then add_break 1 []
(* We add NonTerminal for simulation but remove it afterwards *)
- else snd (list_sep_last (make NoBreak (sl@[NonTerminal m]))) in
+ 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 CanBreak prods
+ hunk :: make_with_space prods
| [] -> []
- in make NoBreak symbols
+ 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 s = string_of_id ldots_var -> List.rev hd, fmt
+ | 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
@@ -535,7 +628,7 @@ let read_recursive_format sl 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 a = b -> get_tail (sepfmt, fmt)
+ | 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
@@ -544,13 +637,13 @@ let read_recursive_format sl fmt =
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') ' ' ->
+ 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 s = drop_simple_quotes s' ->
+ 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 s = id_of_string s' ->
- let i = list_index s vars in
+ | 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 ->
@@ -560,12 +653,12 @@ let hunks_of_format (from,(vars,typs)) symfmt =
| symbs, (UnpCut _ as u) :: fmt ->
let symbs, l = aux (symbs,fmt) in symbs, u :: l
| SProdList (m,sl) :: symbs, fmt ->
- let i = list_index m vars in
+ 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 sl <> [] then error_format ();
+ 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)
@@ -594,7 +687,7 @@ let is_not_small_constr = function
let rec define_keywords_aux = function
| GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
when is_not_small_constr e ->
- message ("Identifier '"^k^"' now a keyword");
+ Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
Lexer.add_keyword k;
n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| n :: l -> n :: define_keywords_aux l
@@ -603,7 +696,7 @@ let rec define_keywords_aux = function
(* Ensure that IDENT articulation terminal symbols are keywords *)
let define_keywords = function
| GramConstrTerminal(IDENT k)::l ->
- message ("Identifier '"^k^"' now a keyword");
+ Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
Lexer.add_keyword k;
GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| l -> define_keywords_aux l
@@ -613,7 +706,7 @@ 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 i = n then
+ if Int.equal i n then
let hds =
GramConstrListMark (n,true) :: hds
@ [GramConstrNonTerminal (ETConstrList (typ,tkl), Some x)] in
@@ -633,14 +726,14 @@ let make_production etyps symbols =
let typ = List.assoc m etyps in
distribute [GramConstrNonTerminal (typ, Some m)] ll
| Terminal s ->
- distribute [GramConstrTerminal (terminal s)] ll
+ distribute [GramConstrTerminal (Lexer.terminal s)] ll
| Break _ ->
ll
| SProdList (x,sl) ->
let tkl = List.flatten
- (List.map (function Terminal s -> [terminal s]
+ (List.map (function Terminal s -> [Lexer.terminal s]
| Break _ -> []
- | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in
+ | _ -> 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 ->
@@ -654,7 +747,7 @@ let make_production etyps symbols =
let rec find_symbols c_current c_next c_last = function
| [] -> []
| NonTerminal id :: sl ->
- let prec = if sl <> [] then c_current else c_last in
+ 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
@@ -676,10 +769,10 @@ let recompute_assoc typs =
(* Registration of syntax extensions (parsing/printing, no interpretation)*)
let pr_arg_level from = function
- | (n,L) when n=from -> str "at next level"
+ | (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 m=n -> str "at level " ++ 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) =
@@ -693,42 +786,51 @@ let error_incompatible_level ntn oldprec prec =
spc() ++ str "while it is now required to be" ++ spc() ++
pr_level ntn prec ++ str ".")
-let cache_one_syntax_extension (typs,prec,ntn,gr,pp) =
+type syntax_extension = {
+ synext_level : Notation.level;
+ synext_notation : notation;
+ synext_notgram : notation_grammar;
+ synext_unparsing : unparsing list;
+ synext_extra : (string * string) list;
+}
+
+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
try
let oldprec = Notation.level_of_notation ntn in
- if prec <> oldprec then error_incompatible_level ntn oldprec prec
+ if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec
with Not_found ->
(* Reserve the notation level *)
Notation.declare_notation_level ntn prec;
(* Declare the parsing rule *)
- Egrammar.extend_grammar (Egrammar.Notation (prec,typs,gr));
+ Egramcoq.extend_constr_grammar prec se.synext_notgram;
(* Declare the printing rule *)
- Notation.declare_notation_printing_rule ntn (pp,fst prec)
+ Notation.declare_notation_printing_rule ntn
+ ~extra:se.synext_extra (se.synext_unparsing, fst prec)
-let cache_syntax_extension (_,(_,sy_rules)) =
- List.iter cache_one_syntax_extension sy_rules
+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)) =
- (local, List.map (fun (typs,prec,ntn,gr,pp) ->
- (typs,prec,ntn,subst_parsing_rule subst gr,subst_printing_rule subst pp))
- sy)
+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) =
+let classify_syntax_definition (local, _ as o) =
if local then Dispose else Substitute o
-type syntax_extension_obj =
- bool *
- (notation_var_internalization_type list * Notation.level *
- notation * notation_grammar * unparsing list)
- list
-
let inSyntaxExtension : syntax_extension_obj -> obj =
declare_object {(default_object "SYNTAX-EXTENSION") with
- open_function = (fun i o -> if i=1 then cache_syntax_extension o);
+ 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}
@@ -740,41 +842,49 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
let interp_modifiers modl =
let onlyparsing = ref false in
- let rec interp assoc level etyps format = function
+ let rec interp assoc level etyps format extra = function
| [] ->
- (assoc,level,etyps,!onlyparsing,format)
+ (assoc,level,etyps,!onlyparsing,format,extra)
| SetEntryType (s,typ) :: l ->
- let id = id_of_string s in
- if List.mem_assoc id etyps then
+ let id = Id.of_string s in
+ if Id.List.mem_assoc id etyps then
error (s^" is already assigned to an entry or constr level.");
- interp assoc level ((id,typ)::etyps) format l
+ interp assoc level ((id,typ)::etyps) format extra l
| SetItemLevel ([],n) :: l ->
- interp assoc level etyps format l
+ interp assoc level etyps format extra l
| SetItemLevel (s::idl,n) :: l ->
- let id = id_of_string s in
- if List.mem_assoc id etyps then
+ let id = Id.of_string s in
+ if Id.List.mem_assoc id etyps then
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)
+ interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l)
| SetLevel n :: l ->
- if level <> None then error "A level is given more than once.";
- interp assoc (Some n) etyps format 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 assoc <> None then error"An associativity is given more than once.";
- interp (Some a) level etyps format 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 l
- | SetFormat s :: l ->
- if format <> None then error "A format is given more than once.";
- interp assoc level etyps (Some s) l
- in interp None None [] None modl
+ 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 (assoc,level,t,b,fmt) = interp_modifiers modifiers in
- if t <> [] then
+ let (assoc,level,t,b,fmt,extra) = 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,_)::_ -> error (Id.to_string x ^ " is unbound in the notation.")
+ | _ -> ()
+
let no_syntax_modifiers = function
| [] | [SetOnlyParsing _] -> true
| _ -> false
@@ -805,7 +915,7 @@ let join_auxiliary_recursive_types recvars etyps =
| None, None -> typs
| Some _, None -> typs
| None, Some ytyp -> (x,ytyp)::typs
- | Some xtyp, Some ytyp when xtyp = 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 ++
@@ -821,12 +931,12 @@ let internalization_type_of_entry_type = function
| ETBinderList _ | ETConstrList _ -> assert false
let set_internalization_type typs =
- List.map (down_snd internalization_type_of_entry_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
+ maintyps @ extratyps
let make_interpretation_type isrec = function
| NtnInternTypeConstr when isrec -> NtnTypeConstrList
@@ -835,14 +945,21 @@ let make_interpretation_type isrec = function
| NtnInternTypeBinder -> error "Type not allowed in recursive notation."
let make_interpretation_vars recvars allvars =
- List.iter (fun (x,y) ->
- if fst (List.assoc x allvars) <> fst (List.assoc y allvars) then
- error_not_same_scope x y) recvars;
+ 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 =
- List.filter (fun (x,_) -> not (List.mem x useless_recvars)) allvars in
- List.map (fun (x,(sc,typ)) ->
- (x,(sc,make_interpretation_type (List.mem_assoc x recvars) typ))) mainvars
+ Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in
+ Id.Map.mapi (fun x (sc, typ) ->
+ (sc, make_interpretation_type (Id.List.mem_assoc x recvars) typ)) mainvars
let check_rule_productivity l =
if List.for_all (function NonTerminal _ -> true | _ -> false) l then
@@ -850,9 +967,17 @@ let check_rule_productivity l =
if (match l with SProdList _ :: _ -> true | _ -> false) then
error "A recursive notation must start with at least one symbol."
-let is_not_printable = function
- | AVar _ -> msg_warn "This notation will not be used for printing as it is bound to a \nsingle variable"; true
- | _ -> false
+let is_not_printable onlyparse noninjective = function
+| NVar _ ->
+ let () = if not onlyparse then
+ msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
+ in
+ true
+| _ ->
+ if not onlyparse && noninjective then
+ let () = msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
+ true
+ else onlyparse
let find_precedence lev etyps symbols =
match symbols with
@@ -861,31 +986,32 @@ let find_precedence lev etyps symbols =
| ETConstr _ ->
error "The level of the leftmost non-terminal cannot be changed."
| ETName | ETBigint | ETReference ->
- if lev = None then
- ([msgnl,str "Setting notation at level 0."],0)
- else
- if lev <> Some 0 then
+ begin match lev with
+ | None ->
+ ([msg_info,strbrk "Setting notation at level 0."],0)
+ | Some 0 ->
+ ([],0)
+ | _ ->
error "A notation starting with an atomic expression must be at level 0."
- else
- ([],0)
+ end
| ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *)
- if lev = None then
+ 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 lev = None then
+ if Option.is_empty lev then
error "A left-recursive notation must have an explicit level."
else [],Option.get lev)
| Terminal _ ::l when
- (match list_last symbols with Terminal _ -> true |_ -> false)
+ (match List.last symbols with Terminal _ -> true |_ -> false)
->
- if lev = None then
- ([msgnl,str "Setting notation at level 0."], 0)
+ if Option.is_empty lev then
+ ([msg_info,strbrk "Setting notation at level 0."], 0)
else [],Option.get lev
| _ ->
- if lev = None then error "Cannot determine the level.";
+ if Option.is_empty lev then error "Cannot determine the level.";
[],Option.get lev
let check_curly_brackets_notation_exists () =
@@ -908,9 +1034,9 @@ let remove_curly_brackets l =
let br',next' = skip_break [] l' in
(match next' with
| Terminal "}" as t2 :: l'' as l1 ->
- if l <> l0 or l' <> l1 then
- msg_warn "Skipping spaces inside curly brackets";
- if deb & l'' = [] then [t1;x;t2] else begin
+ if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then
+ msg_warning (strbrk "Skipping spaces inside curly brackets");
+ if deb && List.is_empty l'' then [t1;x;t2] else begin
check_curly_brackets_notation_exists ();
x :: aux false l''
end
@@ -919,14 +1045,15 @@ let remove_curly_brackets l =
| x :: l -> x :: aux false l
in aux true l
-let compute_syntax_data (df,modifiers) =
- let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in
+let compute_syntax_data df modifiers =
+ let (assoc,n,etyps,onlyparse,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 = (symbols <> 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
@@ -947,45 +1074,52 @@ let compute_syntax_data (df,modifiers) =
let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
let i_data = (onlyparse,recvars,mainvars,(ntn_for_interp,df')) in
(* Return relevant data for interpretation and for parsing/printing *)
- (msgs,i_data,i_typs,sy_fulldata)
+ (msgs,i_data,i_typs,sy_fulldata,extra)
-let compute_pure_syntax_data (df,mods) =
- let (msgs,(onlyparse,_,_,_),_,sy_data) = compute_syntax_data (df,mods) in
+let compute_pure_syntax_data df mods =
+ let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
let msgs =
if onlyparse then
(msg_warning,
- str "The only parsing modifier has no effect in Reserved Notation.")::msgs
+ strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
else msgs in
- msgs, sy_data
+ msgs, sy_data, extra
(**********************************************************************)
(* 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
+type notation_obj = {
+ notobj_local : bool;
+ notobj_scope : scope_name option;
+ notobj_interp : interpretation;
+ notobj_onlyparse : bool;
+ 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
+ if Int.equal i 1 then begin
(* Declare the interpretation *)
Notation.declare_notation_interpretation ntn scope pat df;
(* Declare the uninterpretation *)
- if not onlyparse then
- Notation.declare_uninterpretation (NotationRule (scope,ntn)) pat
+ 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,(lc,scope,pat,b,ndf)) =
- (lc,scope,subst_interpretation subst pat,b,ndf)
-
-let classify_notation (local,_,_,_,_ as o) =
- if local then Dispose else Substitute o
+let subst_notation (subst, nobj) =
+ { nobj with notobj_interp = subst_interpretation subst nobj.notobj_interp; }
-type notation_obj =
- bool * scope_name option * interpretation * bool *
- (notation * notation_location)
+let classify_notation nobj =
+ if nobj.notobj_local then Dispose else Substitute nobj
let inNotation : notation_obj -> obj =
declare_object {(default_object "NOTATION") with
@@ -998,9 +1132,12 @@ let inNotation : notation_obj -> obj =
(**********************************************************************)
let with_lib_stk_protection f x =
- let fs = Lib.freeze () in
+ let fs = Lib.freeze `No in
try let a = f x in Lib.unfreeze fs; a
- with reraise -> Lib.unfreeze fs; raise reraise
+ with reraise ->
+ let reraise = Errors.push reraise in
+ let () = Lib.unfreeze fs in
+ iraise reraise
let with_syntax_protection f x =
with_lib_stk_protection
@@ -1011,11 +1148,11 @@ let with_syntax_protection f x =
(* Recovering existing syntax *)
let contract_notation ntn =
- if ntn = "{ _ }" then ntn else
+ if String.equal ntn "{ _ }" then ntn else
let rec aux ntn i =
if i <= String.length ntn - 5 then
let ntn' =
- if String.sub ntn i 5 = "{ _ }" then
+ if String.is_sub "{ _ }" ntn i then
String.sub ntn 0 i ^ "_" ^
String.sub ntn (i+5) (String.length ntn -i-5)
else ntn in
@@ -1029,58 +1166,94 @@ let recover_syntax ntn =
try
let prec = Notation.level_of_notation ntn in
let pp_rule,_ = Notation.find_notation_printing_rule ntn in
- let typs,pa_rule = Egrammar.recover_notation_grammar ntn prec in
- (typs,prec,ntn,pa_rule,pp_rule)
+ let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in
+ let pa_rule = Egramcoq.recover_constr_grammar ntn prec in
+ { synext_level = prec;
+ synext_notation = ntn;
+ synext_notgram = pa_rule;
+ synext_unparsing = pp_rule;
+ synext_extra = pp_extra_rules }
with Not_found ->
raise NoSyntaxRule
-let recover_squash_syntax () = recover_syntax "{ _ }"
+let recover_squash_syntax sy =
+ let sq = recover_syntax "{ _ }" in
+ [sy; sq]
let recover_notation_syntax rawntn =
let ntn = contract_notation rawntn in
- let (typs,_,_,_,_ as sy_rule) = recover_syntax ntn in
- let need_squash = ntn<>rawntn in
- typs,if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule]
+ 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
(**********************************************************************)
(* Main entry point for building parsing and printing rules *)
-let make_pa_rule (n,typs,symbols,_) ntn =
+let make_pa_rule i_typs (n,typs,symbols,_) ntn =
let assoc = recompute_assoc typs in
let prod = make_production typs symbols in
- (n,assoc,ntn,prod)
+ { notgram_level = n;
+ notgram_assoc = assoc;
+ notgram_notation = ntn;
+ notgram_prods = prod;
+ notgram_typs = i_typs; }
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)
+ | 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) =
- let pa_rule = make_pa_rule sy_data ntn in
+let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra =
+ let pa_rule = make_pa_rule i_typs sy_data ntn in
let pp_rule = make_pp_rule sy_data in
- let sy_rule = (i_typs,prec,ntn,pa_rule,pp_rule) in
+ let sy = {
+ synext_level = prec;
+ synext_notation = ntn;
+ synext_notgram = pa_rule;
+ synext_unparsing = pp_rule;
+ synext_extra = extra;
+ } 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]
+ 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) = compute_syntax_data (df,mods) in
+ let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in
(* Prepare the parsing and printing rules *)
- let sy_rules = make_syntax_rules sy_data in
+ let sy_rules = make_syntax_rules sy_data extra in
(* Prepare the interpretation *)
- let (onlyparse,recvars,mainvars,df') = i_data in
+ let (onlyparse, recvars,mainvars, df') = i_data in
let i_vars = make_internalization_vars recvars mainvars i_typs in
- let (acvars,ac) = interp_aconstr i_vars recvars c in
- let a = (make_interpretation_vars recvars acvars,ac) in
- let onlyparse = onlyparse or is_not_printable ac in
+ let nenv = {
+ ninterp_var_type = to_map i_vars;
+ ninterp_rec_vars = to_map recvars;
+ ninterp_only_parse = false;
+ } in
+ let (acvars, ac) = 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 nenv.ninterp_only_parse 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_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 (local,scope,a,onlyparse,df'));
+ 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 =
@@ -1095,17 +1268,31 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
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 (acvars,ac) = interp_aconstr ~impls i_vars recvars c in
- let a = (make_interpretation_vars recvars acvars,ac) in
- let onlyparse = onlyparse or is_not_printable ac in
- Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'));
+ let nenv = {
+ ninterp_var_type = to_map i_vars;
+ ninterp_rec_vars = to_map recvars;
+ ninterp_only_parse = false;
+ } in
+ let (acvars, ac) = 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 nenv.ninterp_only_parse 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_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 = compute_pure_syntax_data (df,mods) in
- let sy_rules = make_syntax_rules sy_data in
+ let msgs, sy_data, extra = compute_pure_syntax_data df mods in
+ let sy_rules = make_syntax_rules sy_data extra in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
@@ -1139,9 +1326,16 @@ let add_notation local c ((loc,df),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 (dummy_loc, id_of_string x))
+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;
@@ -1154,16 +1348,16 @@ let add_infix local ((loc,inf),modifiers) pr sc =
(**********************************************************************)
(* Delimiters and classes bound to scopes *)
-type scope_command = ScopeDelim of string | ScopeClasses of Classops.cl_typ
+type scope_command = ScopeDelim of string | ScopeClasses of scope_class list
let load_scope_command _ (_,(scope,dlm)) =
Notation.declare_scope scope
let open_scope_command i (_,(scope,o)) =
- if i=1 then
+ if Int.equal i 1 then
match o with
| ScopeDelim dlm -> Notation.declare_delimiters scope dlm
- | ScopeClasses cl -> Notation.declare_class_scope scope cl
+ | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl
let cache_scope_command o =
load_scope_command 1 o;
@@ -1171,7 +1365,10 @@ let cache_scope_command o =
let subst_scope_command (subst,(scope,o as x)) = match o with
| ScopeClasses cl ->
- let cl' = Classops.subst_cl_typ subst cl in if cl'==cl then x else
+ 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
@@ -1192,19 +1389,28 @@ let add_class_scope scope 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
+ | [], 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 [], ARef (try_interp_name_alias (vars,c))
+ try [], NRef (try_interp_name_alias (vars,c))
with Not_found ->
- let i_vars = List.map (fun id -> (id,NtnInternTypeConstr)) vars in
- let vars,pat = interp_aconstr i_vars [] c in
- List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat
+ 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;
+ ninterp_only_parse = false;
+ } in
+ let nvars, pat = interp_notation_constr nenv c in
+ let () = nonprintable := nenv.ninterp_only_parse 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 pat) -> Some Flags.Current
+ | None when (is_not_printable false !nonprintable pat) -> Some Flags.Current
| p -> p
in
Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 23:52:15 +0000