diff options
| -rw-r--r-- | parsing/g_basevernac.ml4 | 7 | ||||
| -rw-r--r-- | theories/Init/DatatypesSyntax.v | 4 | ||||
| -rw-r--r-- | theories/Init/SpecifSyntax.v | 42 | ||||
| -rw-r--r-- | theories/Reals/Rsyntax.v | 10 | ||||
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 8 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 31 | ||||
| -rw-r--r-- | toplevel/metasyntax.mli | 14 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 10 |
9 files changed, 68 insertions, 60 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index be3d3fe26..293d81590 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -232,12 +232,17 @@ GEXTEND Gram | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = qualid; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc) | IDENT "Notation"; a = entry_prec; n = natural; s = STRING; c = constr; - sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (a,n,s,c,sc) + precl = [ "("; l = LIST1 var_precedence SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc ] -> + VernacNotation (a,n,s,c,precl,sc) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) ] ] ; + var_precedence: + [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> (x,n) ] ] + ; opt_scope: [ [ IDENT "_" -> None | sc = IDENT -> Some sc ] ] ; diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v index d51e7acbc..71785ce70 100644 --- a/theories/Init/DatatypesSyntax.v +++ b/theories/Init/DatatypesSyntax.v @@ -25,8 +25,8 @@ with constr0 := [ (pair ? ? $lc1 $lc2) ] . -Infix 7 "+" sum. -Infix RIGHTA 6 "*" prod. +Infix 3 "+" sum. +Infix RIGHTA 2 "*" prod. (** Pretty-printing of things in Datatypes.v *) diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index 50c3df5de..89bda6138 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -14,25 +14,25 @@ Require Specif. (** Parsing of things in Specif.v *) (* To accept {x:A|P}*B without parentheses *) -Grammar constr constr6 := +Grammar constr constr2 := sigprod [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" - "*" constr6($c) ] + "*" constr2($c) ] -> [ (prod (sig $c1 [$lc : $c1]$c2) $c) ] | sig2prod [ "{" lconstr($lc) ":" lconstr($c1) - "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr6($c) ] + "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr2($c) ] -> [ (prod (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ] | sigSprod [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" - "*" constr6($c)] + "*" constr2($c)] -> [ (prod (sigS $c1 [$lc : $c1]$c2) $c) ] | sigS2prod [ "{" lconstr($lc) ":" lconstr($c1) - "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr6($c) ] + "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr2($c) ] -> [ (prod (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ]. (* To factor with {A}+{B} *) -Grammar constr constr6 := +Grammar constr constr2 := sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ] -> [ (sig $c1 [$lc : $c1]$c2) ] @@ -47,25 +47,21 @@ Grammar constr constr6 := "&" lconstr($c2) "&" lconstr($c3) "}" ] -> [ (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ]. -Grammar constr constr6 := - sumbool [ "{" lconstr($lc) "}" "+" "{" lconstr($lc2) "}" ] -> - [ (sumbool $lc $lc2) ]. +Notation 2 "{ x } + { y }" (sumbool x y). +Notation LEFTA 3 " x + { y }" (sumor x y). -Grammar constr constr7 := - sumor [ constr7($c1) "+" "{" lconstr($c2) "}" ] -> - [ (sumor $c1 $c2) ] - -| sumsig [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ] -> +Grammar constr constr3 := + sumsig [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ] -> [ (sum $c (sig $c1 [$lc : $c1]$c2)) ] -| sumsig2 [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1) +| sumsig2 [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "&" lconstr($c3) "}" ] -> [ (sum $c (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ] -| sumsigS [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ] +| sumsigS [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ] -> [ (sum $c (sigS $c1 [$lc : $c1]$c2)) ] -| sumsigS2 [ constr7($c) "+" "{" lconstr($lc) ":" constr($c1) +| sumsigS2 [ constr3($c) "+" "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "&" lconstr($c3) "}" ] -> [ (sum $c (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ] . @@ -118,19 +114,9 @@ Syntax constr (** Pretty-printing of [projS1] and [projS2] *) | projS1_imp [ (projS1 ? ? $a) ] -> ["(ProjS1 " $a:E ")"] | projS2_imp [ (projS2 ? ? $a) ] -> ["(ProjS2 " $a:E ")"] - ; - -(** Pretty-printing of [sumbool] and [sumor] *) - level 7: - sumbool [ (sumbool $t1 $t2) ] - -> [ [<hov 0> "{" $t1:E "}" [0 1] "+" "{" $t2:L "}"] ] - | sumor [ (sumor $t1 $t2) ] - -> [ [<hov 0> $t1:E [0 1] "+" "{" $t2:L "}"] ] - ; (** Pretty-printing of [except] *) - level 1: - Except_imp [ (except $1 $t2) ] -> [ [<hov 0> "Except " $t2 ] ] + | Except_imp [ (except $1 $t2) ] -> [ [<hov 0> "Except " $t2 ] ] (** Pretty-printing of [error] and [value] *) | Error_imp [ (error $t1) ] -> [ [<hov 0> "Error" ] ] diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index e18cfdd76..0e9d174b7 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -203,11 +203,11 @@ Infix 3 "+" Rplus : R_scope. Infix 3 "-" Rminus : R_scope. Infix 2 "*" Rmult : R_scope. Distfix 0 "- _" Ropp : R_scope. -Notation NONA 4 "x == y == z" (eqT R x y)/\(eqT R y z) : R_scope. -Notation NONA 4 "x <= y <= z" (Rle x y)/\(Rle y z) : R_scope. -Notation NONA 4 "x <= y < z" (Rle x y)/\(Rlt y z) : R_scope. -Notation NONA 4 "x < y < z" (Rlt x y)/\(Rlt y z) : R_scope. -Notation NONA 4 "x < y <= z" (Rlt x y)/\(Rle y z) : R_scope. +Notation NONA 4 "x == y == z" (eqT R x y)/\(eqT R y z) (y at level 3): R_scope. +Notation NONA 4 "x <= y <= z" (Rle x y)/\(Rle y z) (y at level 3) : R_scope. +Notation NONA 4 "x <= y < z" (Rle x y)/\(Rlt y z) (y at level 3) : R_scope. +Notation NONA 4 "x < y < z" (Rlt x y)/\(Rlt y z) (y at level 3) : R_scope. +Notation NONA 4 "x < y <= z" (Rlt x y)/\(Rle y z) (y at level 3) : R_scope. Notation NONA 4 "x <> y" ~(eqT R x y) : R_scope. Infix LEFTA 2 "/" Rdiv : R_scope. Distfix 0 "/ _" Rinv : R_scope. diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 8314d25a5..77930d10d 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -229,10 +229,10 @@ Infix 3 "+" Zplus : Z_scope. Infix 3 "-" Zminus : Z_scope. Infix 2 "*" Zmult : Z_scope. Distfix 0 "- _" Zopp : Z_scope. -Notation NONA 4 "x <= y <= z" (Zle x y)/\(Zle y z) : Z_scope. -Notation NONA 4 "x <= y < z" (Zle x y)/\(Zlt y z) : Z_scope. -Notation NONA 4 "x < y < z" (Zlt x y)/\(Zlt y z) : Z_scope. -Notation NONA 4 "x < y <= z" (Zlt x y)/\(Zle y z) : Z_scope. +Notation NONA 4 "x <= y <= z" (Zle x y)/\(Zle y z) (y at level 3) : Z_scope. +Notation NONA 4 "x <= y < z" (Zle x y)/\(Zlt y z) (y at level 3) : Z_scope. +Notation NONA 4 "x < y < z" (Zlt x y)/\(Zlt y z) (y at level 3) : Z_scope. +Notation NONA 4 "x < y <= z" (Zlt x y)/\(Zle y z) (y at level 3) : Z_scope. Notation NONA 4 "x <> y" ~(eq Z x y) : Z_scope. (* Notation NONA 1 "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*) Notation NONA 1 "|| x ||" (Zabs x) : Z_scope. diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 67eb2d379..cb05a5c7d 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -207,7 +207,7 @@ let prec_assoc = function let constr_tab = [| "constr0"; "constr1"; "constr2"; "constr3"; "lassoc_constr4"; - "constr5"; "constr6"; "constr7"; "constr8"; "constr9"; "constr10"; + "constr5"; "constr6"; "constr7"; "constr8"; "constr9"; "lconstr"; "pattern" |] let constr_rule (n,p) = @@ -237,8 +237,11 @@ let make_hunks symbols = UNP_BRK (n, 1) :: RO s :: l) symbols [] +let string_of_prec (n,p) = + (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "") + let string_of_symbol = function - | NonTerminal _ -> "_" + | NonTerminal (lp,_) -> "_:"^(string_of_prec lp) | Terminal s -> s let string_of_assoc = function @@ -285,24 +288,29 @@ let strip s = let n = String.length s in if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s -let rec find_symbols c_first c_next c_last vars new_var = function +let rec find_symbols c_first c_next c_last vars new_var varprecl = function | [] -> (vars, []) | x::sl when is_letter x.[0] -> let id = Names.id_of_string x in if List.mem_assoc id vars then error ("Variable "^x^" occurs more than once"); - let prec = if sl = [] then c_last else c_first in - let (vars,l) = find_symbols c_next c_next c_last vars (new_var+1) sl in + let prec = + try (List.assoc x varprecl,E) + with Not_found -> if sl = [] then c_last else c_first in + let (vars,l) = + find_symbols c_next c_next c_last vars (new_var+1) varprecl sl in let meta = create_meta new_var in ((id,ope ("META",[num new_var]))::vars, NonTerminal (prec, meta) :: l) | "_"::sl -> warning "Found '_'"; let prec = if sl = [] then c_last else c_first in - let (vars,l) = find_symbols c_next c_next c_last vars (new_var+1) sl in + let (vars,l) = + find_symbols c_next c_next c_last vars (new_var+1) varprecl sl in let meta = create_meta new_var in (vars, NonTerminal (prec, meta) :: l) | s :: sl -> - let (vars,l) = find_symbols c_next c_next c_last vars new_var sl in + let (vars,l) = + find_symbols c_next c_next c_last vars new_var varprecl sl in (vars, Terminal (strip s) :: l) let make_grammar_pattern symbols ntn = @@ -365,10 +373,11 @@ let rec reify_meta_ast = function (* Distfix, Infix, Notations *) -let add_notation assoc n df ast sc = +let add_notation assoc n df ast varprecl sc = let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in let (lp,rp) = prec_assoc assoc in - let (subst,symbols) = find_symbols (n,lp) (n,L) (n,rp) [] 1 (split df) in + let (subst,symbols) = + find_symbols (n,lp) (10,E) (n,rp) [] 1 varprecl (split df) in let notation = make_symbolic assoc n symbols in let rule_name = notation^"_"^scope^"_notation" in (* To globalize... *) @@ -403,7 +412,7 @@ let add_distfix assoc n df astf sc = let (vars,l) = rename "x" [] 1 (split df) in let df = String.concat " " l in let ast = ope("APPLIST",astf::vars) in - add_notation assoc n df ast sc + add_notation assoc n df ast [] sc let add_infix assoc n inf qid sc = let pr = Astterm.globalize_qualid qid in @@ -418,7 +427,7 @@ let add_infix assoc n inf qid sc = *) let metas = [inject_var "x"; inject_var "y"] in let ast = ope("APPLIST",pr::metas) in - add_notation assoc n ("x "^(quote inf)^" y") ast sc + add_notation assoc n ("x "^(quote inf)^" y") ast [] sc (* Delimiters *) let load_delimiters _ (_,(_,_,scope,dlm)) = diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 07d1db0e3..1b667918a 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -9,7 +9,10 @@ (*i $Id$ i*) (*i*) +open Util +open Libnames open Extend +open Tacexpr open Vernacexpr open Symbols (*i*) @@ -20,19 +23,20 @@ val add_syntax_obj : string -> syntax_entry_ast list -> unit val add_grammar_obj : string -> grammar_entry_ast list -> unit val add_token_obj : string -> unit -val add_tactic_grammar : (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list -> unit +val add_tactic_grammar : + (string * (string * grammar_production list) * raw_tactic_expr) list -> unit val add_infix : - Gramext.g_assoc option -> int -> string -> Libnames.qualid Util.located + Gramext.g_assoc option -> precedence -> string -> qualid located -> scope_name option -> unit val add_distfix : - Gramext.g_assoc option -> int -> string -> Coqast.t + Gramext.g_assoc option -> precedence -> string -> Coqast.t -> scope_name option -> unit val add_delimiters : scope_name -> delimiters -> unit val add_notation : - Gramext.g_assoc option -> int -> string -> Coqast.t - -> scope_name option -> unit + Gramext.g_assoc option -> precedence -> string -> Coqast.t + -> (string * precedence) list -> scope_name option -> unit val print_grammar : string -> string -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b3825dd93..49aae75bb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1038,7 +1038,7 @@ let interp c = match c with | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl | VernacInfix (assoc,n,inf,qid,sc) -> vernac_infix assoc n inf qid sc | VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc - | VernacNotation (assoc,n,inf,c,sc) -> vernac_notation assoc n inf c sc + | VernacNotation (assoc,n,inf,c,pl,sc) -> vernac_notation assoc n inf c pl sc (* Gallina *) | VernacDefinition (k,id,d,f) -> vernac_definition k id d f diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index d2ad10bb6..7ea61dd6e 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -165,6 +165,7 @@ type local_decl_expr = | AssumExpr of identifier * constr_ast | DefExpr of identifier * constr_ast * constr_ast option +type precedence = int type grammar_entry_ast = (loc * string) * Ast.entry_type option * grammar_associativity * raw_grammar_rule list @@ -188,11 +189,14 @@ type vernac_expr = | VernacDelimiters of scope_name * (string * string) | VernacArgumentsScope of qualid located * scope_name option list | VernacInfix of - grammar_associativity * int * string * qualid located * scope_name option + grammar_associativity * precedence * string * qualid located + * scope_name option | VernacDistfix of - grammar_associativity * int * string * qualid located * scope_name option + grammar_associativity * precedence * string * qualid located + * scope_name option | VernacNotation of - grammar_associativity * int * string * constr_ast * scope_name option + grammar_associativity * precedence * string * constr_ast + * (string * precedence) list * scope_name option (* Gallina *) | VernacDefinition of definition_kind * identifier * definition_expr * |