(** {2 Grammar extension} *)
+let level_of precedence associativity =
+ if precedence < min_precedence || precedence > max_precedence then
+ raise (Level_not_found precedence);
+ let assoc_string =
+ match associativity with
+ | Gramext.NonA -> "N"
+ | Gramext.LeftA -> "L"
+ | Gramext.RightA -> "R"
+ in
+ string_of_int precedence ^ assoc_string
+
let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
let gram_ident s = Gramext.Stoken ("IDENT", s)
let gram_number s = Gramext.Stoken ("NUMBER", s)
let gram_keyword s = Gramext.Stoken ("", s)
-let gram_term = Gramext.Sself
+let gram_term = function
+ | None -> Gramext.Sself
+ | Some (precedence, associativity) ->
+ Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence associativity)
+;;
let gram_of_literal =
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
| NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
(* LUCA: DEFCON 3 BEGIN *)
- | Binding (name, Env.TermType) :: tl ->
+ | Binding (name, Env.TermType l) :: tl ->
Gramext.action
(fun (v:Ast.term) ->
- aux ((name, (Env.TermType, Env.TermValue v))::vl) tl)
+ aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl)
| Binding (name, Env.StringType) :: tl ->
Gramext.action
(fun (v:string) ->
and aux_variable =
function
| Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
- | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
+ | Ast.TermVar (s,level) ->
+ [Binding (s, Env.TermType level), gram_term level]
| Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
| Ast.Ascription (p, s) -> assert false (* TODO *)
| Ast.FreshVar _ -> assert false
in
aux pattern
-let level_of precedence associativity =
- if precedence < min_precedence || precedence > max_precedence then
- raise (Level_not_found precedence);
- let assoc_string =
- match associativity with
- | Gramext.NonA -> "N"
- | Gramext.LeftA -> "L"
- | Gramext.RightA -> "R"
- in
- string_of_int precedence ^ assoc_string
-
type rule_id = Grammar.token Gramext.g_symbol list
(* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
| "opt"; p = l1_simple_pattern -> Ast.Opt p
]
];
+ l1_associativity : [
+ [ IDENT "L" -> Gramext.LeftA
+ | IDENT "N" -> Gramext.NonA
+ | IDENT "R" -> Gramext.RightA
+ ]
+ ];
l1_pattern_variable: [
- [ "term"; id = IDENT -> Ast.TermVar id
+ [ "term"; precedence = NUMBER; assoc = l1_associativity ; id = IDENT ->
+ Ast.TermVar (id, Some (int_of_string precedence,assoc))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
]
return_term loc (CicNotationUtil.group p)
]
| "simple" NONA
- [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar i))
+ [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar (i,None)))
| m = l1_magic_pattern -> return_term loc (Ast.Magic m)
| v = l1_pattern_variable -> return_term loc (Ast.Variable v)
| l = literal -> return_term loc (Ast.Literal l)
(* {{{ Grammar for ast magics, notation level 2 *)
EXTEND
GLOBAL: level2_meta;
+ l2_associativity : [
+ [ IDENT "L" -> Gramext.LeftA
+ | IDENT "N" -> Gramext.NonA
+ | IDENT "R" -> Gramext.RightA
+ ]
+ ];
l2_variable: [
- [ "term"; id = IDENT -> Ast.TermVar id
+ [ "term"; precedence = NUMBER; assoc = l2_associativity; id = IDENT ->
+ Ast.TermVar (id,Some (int_of_string precedence, assoc))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
| "fresh"; id = IDENT -> Ast.FreshVar id
- | "anonymous" -> Ast.TermVar "_"
- | id = IDENT -> Ast.TermVar id
+ | "anonymous" -> Ast.TermVar ("_",None)
+ | id = IDENT -> Ast.TermVar (id,None)
]
];
l2_magic: [
let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in
match meta with
| Ast.Variable (Ast.FreshVar _) -> [meta], None
- | Ast.Variable (Ast.TermVar "_") -> [Ast.Ident ("_", None)], None
+ | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
| _ -> failwith "Invalid bound name."
]
];
match meta with
| Ast.Variable (Ast.FreshVar _)
| Ast.Variable (Ast.IdentVar _) -> meta
- | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
+ | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
| _ -> failwith "Invalid index name."
]
];