diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-29 23:37:05 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-29 23:37:05 +0000 |
commit | 3da96601446a2bb5a3b9a469ab13306947d4a933 (patch) | |
tree | 5b6a6d44e791686152751c6a2bf6919f6b2d1234 | |
parent | 7264f8df4300014b945294fc21cecb1c4ad07513 (diff) |
Raffinement syntaxe Infix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3344 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/interface/xlate.ml | 2 | ||||
-rw-r--r-- | parsing/g_basevernac.ml4 | 8 | ||||
-rw-r--r-- | toplevel/metasyntax.ml | 40 | ||||
-rw-r--r-- | toplevel/metasyntax.mli | 4 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 2 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 2 |
6 files changed, 36 insertions, 22 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 57e7189a7..6358a3e59 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1932,7 +1932,7 @@ let xlate_vernac = | VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented" - | VernacInfix (str_assoc, n, str, id, None) -> + | VernacInfix (str_assoc, n, str, id, false, None) -> CT_infix ( (match str_assoc with | Some Gramext.LeftA -> CT_lefta diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 24499fb2d..9ef698ad1 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -232,8 +232,12 @@ GEXTEND Gram | IDENT "Arguments"; IDENT "Scope"; qid = global; "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl) - | IDENT "Infix"; a = entry_prec; n = natural; op = STRING; p = global; - sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (a,n,op,p,sc) + | IDENT "Infix"; a = entry_prec; n = OPT natural; op = STRING; + p = global; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc ] -> + let (a,n,b) = Metasyntax.interp_infix_modifiers a n modl in + VernacInfix (a,n,op,p,b,sc) | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc) | IDENT "Notation"; s = IDENT; ":="; c = constr -> diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e527fafd8..564fc48d8 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -441,12 +441,11 @@ let (inSyntaxExtension, outSyntaxExtension) = classify_function = (fun (_,o) -> Substitute o); export_function = (fun x -> Some x)} -let interp_syntax_modifiers = +let interp_modifiers a n = let onlyparsing = ref false in let rec interp assoc level etyps = function | [] -> let n = match level with None -> 1 | Some n -> n in - let assoc = match assoc with None -> Some Gramext.NonA | a -> a in (assoc,n,etyps,!onlyparsing) | SetEntryType (s,typ) :: l -> let id = id_of_string s in @@ -471,7 +470,21 @@ let interp_syntax_modifiers = | SetOnlyParsing :: l -> onlyparsing := true; interp assoc level etyps l - in interp None None [] + in interp a n [] + +(* Infix defaults to LEFTA (cf doc) *) +let interp_infix_modifiers a n l = + let (assoc,n,t,b) = interp_modifiers a n l in + if t <> [] then + error "explicit entry level or type unexpected in infix notation"; + let assoc = match assoc with None -> Some Gramext.LeftA | a -> a in + (assoc,n,b) + +(* Notation defaults to NONA *) +let interp_notation_modifiers modl = + let (assoc,n,t,b) = interp_modifiers None None modl in + let assoc = match assoc with None -> Some Gramext.NonA | a -> a in + (assoc,n,t,b) (* 2nd list of types has priority *) let rec merge_entry_types etyps' = function @@ -503,7 +516,7 @@ let recompute_assoc typs = | _ -> Some Gramext.NonA let add_syntax_extension df modifiers = - let (assoc,n,etyps,onlyparse) = interp_syntax_modifiers modifiers in + let (assoc,n,etyps,onlyparse) = interp_notation_modifiers modifiers in let (typs,symbs) = find_symbols (n,BorderProd(true,assoc)) (10,InternalProd) (n,BorderProd(false,assoc)) @@ -576,8 +589,7 @@ let make_old_pp_rule n symbols typs r ntn scope vars = let rule_name = ntn^"_"^scope^"_notation" in make_syntax_rule n rule_name symbols typs ast ntn scope -let add_notation_in_scope df a modifiers sc toks = - let (assoc,n,etyps,onlyparse) = interp_syntax_modifiers modifiers in +let add_notation_in_scope df a (assoc,n,etyps,onlyparse) sc toks = let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in let (typs,symbols) = find_symbols @@ -613,7 +625,7 @@ let add_notation df a modifiers sc = let ident = id_of_string (strip x) in Syntax_def.declare_syntactic_definition ident (interp_aconstr a) | _ -> - add_notation_in_scope df a modifiers sc toks + add_notation_in_scope df a (interp_notation_modifiers modifiers) sc toks (* TODO add boxes information in the expression *) @@ -636,12 +648,10 @@ let add_distfix assoc n df r sc = let (vars,l) = rename "x" [] 1 (split df) in let df = String.concat " " l in let a = mkAppC (mkRefC r, vars) in - let assoc = match assoc with - | None -> [SetAssoc Gramext.LeftA] - | Some a -> [SetAssoc a] in - add_notation df a (SetLevel n :: assoc) sc + let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in + add_notation_in_scope df a (Some assoc,n,[],false) sc (split df) -let add_infix assoc n inf pr sc = +let add_infix assoc n inf pr onlyparse sc = (* let pr = Astterm.globalize_qualid pr in*) (* check the precedence *) if n<1 or n>10 then @@ -654,10 +664,8 @@ let add_infix assoc n inf pr sc = *) let metas = [inject_var "x"; inject_var "y"] in let a = mkAppC (mkRefC pr,metas) in - let assoc = match assoc with - | None -> [SetAssoc Gramext.LeftA] - | Some a -> [SetAssoc a] in - add_notation ("x "^(quote inf)^" y") a (SetLevel n :: assoc) sc + let df = "x "^(quote inf)^" y" in + add_notation_in_scope df a (assoc,n,[],onlyparse) sc (split df) (* Delimiters *) let load_delimiters _ (_,(scope,dlm)) = diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index a63d1dea9..08a4d3c06 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -29,7 +29,7 @@ val add_tactic_grammar : (string * (string * grammar_production list) * raw_tactic_expr) list -> unit val add_infix : - grammar_associativity -> precedence -> string -> reference + grammar_associativity -> precedence -> string -> reference -> bool -> scope_name option -> unit val add_distfix : grammar_associativity -> precedence -> string -> reference @@ -43,3 +43,5 @@ val add_syntax_extension : string -> syntax_modifier list -> unit val print_grammar : string -> string -> unit +val interp_infix_modifiers : Gramext.g_assoc option -> int option -> + syntax_modifier list -> Gramext.g_assoc option * int * bool diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 35ef1e620..0a3e28c6c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1014,7 +1014,7 @@ let interp c = match c with | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacOpenScope sc -> vernac_open_scope sc | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl - | VernacInfix (assoc,n,inf,qid,sc) -> vernac_infix assoc n inf qid sc + | VernacInfix (assoc,n,inf,qid,b,sc) -> vernac_infix assoc n inf qid b sc | VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc | VernacNotation (inf,c,pl,sc) -> vernac_notation inf c pl sc diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 6076184b8..36c277b95 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -158,7 +158,7 @@ type vernac_expr = | VernacDelimiters of scope_name * string | VernacArgumentsScope of reference * scope_name option list | VernacInfix of - grammar_associativity * precedence * string * reference * + grammar_associativity * precedence * string * reference * bool * scope_name option | VernacDistfix of grammar_associativity * precedence * string * reference * |