(** {2 Grammar extension} *)
-let symbol s = Gramext.Stoken ("SYMBOL", s)
-let ident s = Gramext.Stoken ("IDENT", s)
-let number s = Gramext.Stoken ("NUMBER", s)
+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 g_symbol_of_literal =
+let gram_of_literal =
function
- | `Symbol s -> symbol s
- | `Keyword s -> ident s
- | `Number s -> number s
+ | `Symbol s -> gram_symbol s
+ | `Keyword s -> gram_keyword s
+ | `Number s -> gram_number s
type binding =
| NoBinding
assert false
and aux_literal =
function
- | `Symbol s -> [NoBinding, symbol s]
- | `Keyword s -> [NoBinding, ident s]
- | `Number s -> [NoBinding, number s]
+ | `Symbol s -> [NoBinding, gram_symbol s]
+ | `Keyword s ->
+ (* assumption: s will be registered as a keyword with the lexer *)
+ [NoBinding, gram_keyword s]
+ | `Number s -> [NoBinding, gram_number s]
and aux_layout = function
- | Sub (p1, p2) -> aux p1 @ [NoBinding, symbol "\\sub"] @ aux p2
- | Sup (p1, p2) -> aux p1 @ [NoBinding, symbol "\\sup"] @ aux p2
- | Below (p1, p2) -> aux p1 @ [NoBinding, symbol "\\below"] @ aux p2
- | Above (p1, p2) -> aux p1 @ [NoBinding, symbol "\\above"] @ aux p2
- | Frac (p1, p2) -> aux p1 @ [NoBinding, symbol "\\frac"] @ aux p2
- | Atop (p1, p2) -> aux p1 @ [NoBinding, symbol "\\atop"] @ aux p2
- | Over (p1, p2) -> aux p1 @ [NoBinding, symbol "\\over"] @ aux p2
+ | Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
+ | Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
+ | Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
+ | Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
+ | Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
+ | Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
+ | Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
| Root (p1, p2) ->
- [NoBinding, symbol "\\root"] @ aux p2 @ [NoBinding, symbol "\\of"]
- @ aux p1
- | Sqrt p -> [NoBinding, symbol "\\sqrt"] @ aux p
+ [NoBinding, gram_symbol "\\root"] @ aux p2
+ @ [NoBinding, gram_symbol "\\of"] @ aux p1
+ | Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
| Break -> []
| Box (_, pl) -> List.flatten (List.map aux pl)
and aux_magic magic =
let action (env_list : CicNotationEnv.t list) (loc : location) =
CicNotationEnv.coalesce_env p_names env_list
in
- let g_symbol s =
+ let gram_of_list s =
match magic with
| List0 (_, None) -> Gramext.Slist0 s
| List1 (_, None) -> Gramext.Slist1 s
- | List0 (_, Some l) -> Gramext.Slist0sep (s, g_symbol_of_literal l)
- | List1 (_, Some l) -> Gramext.Slist1sep (s, g_symbol_of_literal l)
+ | List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
+ | List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
| _ -> assert false
in
[ Env (List.map list_declaration p_names),
Gramext.srules
- [ [ g_symbol (Gramext.srules [ p_atoms, p_action ]) ],
+ [ [ gram_of_list (Gramext.srules [ p_atoms, p_action ]) ],
Gramext.action action ] ]
| _ -> assert false
and aux_variable =
function
- | NumVar s -> [Binding (s, NumType), number ""]
- | TermVar s -> [Binding (s, TermType), Gramext.Sself]
- | IdentVar s -> [Binding (s, StringType), ident ""]
+ | NumVar s -> [Binding (s, NumType), gram_number ""]
+ | TermVar s -> [Binding (s, TermType), gram_term]
+ | IdentVar s -> [Binding (s, StringType), gram_ident ""]
| Ascription (p, s) -> assert false (* TODO *)
| FreshVar _ -> assert false
and inner_pattern p =
type rule_id = Token.t Gramext.g_symbol list
+ (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
+let owned_keywords = Hashtbl.create 23
+
let extend level1_pattern ?(precedence = default_precedence)
?associativity action
=
(fun (env: CicNotationEnv.t) (loc: location) -> (action env loc))
p_bindings) ]]]
in
- p_atoms
-
-let delete atoms = Grammar.delete_rule term atoms
+ let keywords = CicNotationUtil.keywords_of_term level1_pattern in
+ let rule_id = p_atoms in
+ List.iter CicNotationLexer.add_level2_ast_keyword keywords;
+ Hashtbl.add owned_keywords rule_id keywords; (* keywords may be [] *)
+ rule_id
+
+let delete rule_id =
+ let atoms = rule_id in
+ (try
+ let keywords = Hashtbl.find owned_keywords rule_id in
+ List.iter CicNotationLexer.remove_level2_ast_keyword keywords
+ with Not_found -> assert false);
+ Grammar.delete_rule term atoms
(** {2 Grammar} *)
(* {{{ Grammar for ast patterns, notation level 2 *)
level2_ast: [ [ p = term -> p ] ];
sort: [
- [ IDENT "Prop" -> `Prop
- | IDENT "Set" -> `Set
- | IDENT "Type" -> `Type
+ [ "Prop" -> `Prop
+ | "Set" -> `Set
+ | "Type" -> `Type
]
];
explicit_subst: [
]
];
induction_kind: [
- [ IDENT "rec" -> `Inductive
- | IDENT "corec" -> `CoInductive
+ [ "rec" -> `Inductive
+ | "corec" -> `CoInductive
]
];
let_defs: [
[ defs = LIST1 [
name = bound_name; args = bound_names;
- index_name = OPT [ IDENT "on"; id = bound_name -> id ];
+ index_name = OPT [ "on"; id = bound_name -> id ];
ty = OPT [ SYMBOL ":" ; p = term -> p ];
SYMBOL <:unicode<def>> (* ≝ *); body = term ->
let body = fold_binder `Lambda args body in
| Some name -> find_arg name 0 args
in
(name, ty), body, index
- ] SEP IDENT "and" ->
+ ] SEP "and" ->
defs
]
];
term: LEVEL "10" (* let in *)
[ "10" NONA
- [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+ [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (LetIn (var, p1, p2))
- | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
+ | "let"; k = induction_kind; defs = let_defs; "in";
body = term ->
return_term loc (LetRec (k, defs, body))
]
| m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s))
| s = sort -> return_term loc (Sort s)
| outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ];
- IDENT "match"; t = term;
+ "match"; t = term;
indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
- IDENT "with"; SYMBOL "[";
+ "with"; SYMBOL "[";
patterns = LIST0 [
lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
rhs = term ->
]
];
precedence: [
- [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
+ [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
];
notation: [
[ s = QSTRING;
| IDENT "interpretation"; (symbol, args, l3) = interpretation; SYMBOL "." ->
Interpretation ((symbol, args), l3)
| IDENT "render"; u = URI; SYMBOL "." -> Render (UriManager.uri_of_string u)
+ | IDENT "dump"; SYMBOL "." -> Dump
]
];
(* }}} *)
projects / helm.git / blobdiff