exception Parse_error of string
exception Level_not_found of int
-let level1_pattern_grammar =
- Grammar.gcreate CicNotationLexer.level1_pattern_lexer
-let level2_ast_grammar = Grammar.gcreate CicNotationLexer.level2_ast_lexer
-let level2_meta_grammar = Grammar.gcreate CicNotationLexer.level2_meta_lexer
-
let min_precedence = 0
let max_precedence = 100
-let level1_pattern =
- Grammar.Entry.create level1_pattern_grammar "level1_pattern"
-let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast"
-let term = Grammar.Entry.create level2_ast_grammar "term"
-let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"
-let protected_binder_vars = Grammar.Entry.create level2_ast_grammar "protected_binder_vars"
-let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
+type ('a,'b,'c,'d) grammars = {
+ level1_pattern: 'a Grammar.Entry.e;
+ level2_ast: 'b Grammar.Entry.e;
+ level2_ast_grammar : Grammar.g;
+ term: 'b Grammar.Entry.e;
+ let_defs: 'c Grammar.Entry.e;
+ protected_binder_vars: 'd Grammar.Entry.e;
+ level2_meta: 'b Grammar.Entry.e;
+}
+
+let initial_grammars () =
+ let level1_pattern_grammar =
+ Grammar.gcreate (CicNotationLexer.level1_pattern_lexer ()) in
+ let level2_ast_grammar =
+ Grammar.gcreate (CicNotationLexer.level2_ast_lexer ()) in
+ let level2_meta_grammar =
+ Grammar.gcreate (CicNotationLexer.level2_meta_lexer ()) in
+ let level1_pattern =
+ Grammar.Entry.create level1_pattern_grammar "level1_pattern" in
+ let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" in
+ let term = Grammar.Entry.create level2_ast_grammar "term" in
+ let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
+ let protected_binder_vars =
+ Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in
+ let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" in
+ { level1_pattern=level1_pattern;
+ level2_ast=level2_ast;
+ term=term;
+ let_defs=let_defs;
+ protected_binder_vars=protected_binder_vars;
+ level2_meta=level2_meta;
+ level2_ast_grammar=level2_ast_grammar;
+}
+;;
+
+let grammars = ref (initial_grammars ());;
let int_of_string s =
try
| Ast.Self _ -> Gramext.Sself
| Ast.Level precedence ->
Gramext.Snterml
- (Grammar.Entry.obj (term: 'a Grammar.Entry.e), level_of precedence)
+ (Grammar.Entry.obj (!grammars.term: 'a Grammar.Entry.e),
+ level_of precedence)
;;
let gram_of_literal =
| Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
| Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
| Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
- | Ast.InfRule (p1, p2, p3) -> aux p1 @ [NoBinding, gram_symbol "\\infrule"] @ aux p2 @ aux p3
+ | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule"] @ aux p1 @ aux p2 @ aux p3
| Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
| Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
| Ast.Root (p1, p2) ->
| Ast.Break -> []
| Ast.Box (_, pl) -> List.flatten (List.map aux pl)
| Ast.Group pl -> List.flatten (List.map aux pl)
+ | Ast.Mstyle (_,pl) -> List.flatten (List.map aux pl)
+ | Ast.Mpadded (_,pl) -> List.flatten (List.map aux pl)
and aux_magic magic =
match magic with
| Ast.Opt p ->
type rule_id = Grammar.token Gramext.g_symbol list
+let compare_rule_id x y =
+ let rec aux = function
+ | [],[] -> 0
+ | [],_ -> ~-1
+ | _,[] -> 1
+ | ((s1::tl1) as x),((s2::tl2) as y) ->
+ if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
+ else Pervasives.compare x y
+ in
+ aux (x,y)
+
(* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
-let owned_keywords = Hashtbl.create 23
+let initial_owned_keywords () = Hashtbl.create 23
+let owned_keywords = ref (initial_owned_keywords ())
type checked_l1_pattern = CL1P of CicNotationPt.term * int
| Ast.Break as t -> t
| Ast.Box (b, pl) -> Ast.Box(b, List.map aux pl)
| Ast.Group pl -> Ast.Group (List.map aux pl)
+ | Ast.Mstyle (l,pl) -> Ast.Mstyle (l, List.map aux pl)
+ | Ast.Mpadded (l,pl) -> Ast.Mpadded (l, List.map aux pl)
and aux_magic magic =
match magic with
| Ast.Opt p -> Ast.Opt (aux p)
let level = level_of precedence in
let _ =
Grammar.extend
- [ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
+ [ Grammar.Entry.obj (!grammars.term: 'a Grammar.Entry.e),
Some (Gramext.Level level),
[ None,
Some (*Gramext.NonA*) Gramext.NonA,
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 [] *)
+ 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
+ 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
+ Grammar.delete_rule !grammars.term atoms
(** {2 Grammar} *)
Ast.AttributedTerm (`Loc loc, term l)
(* create empty precedence level for "term" *)
-let _ =
+let initialize_grammars () =
let dummy_action =
Gramext.action (fun _ ->
failwith "internal error, lexer generated a dummy token")
aux [] last
in
Grammar.extend
- [ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
+ [ Grammar.Entry.obj (!grammars.term: 'a Grammar.Entry.e),
None,
- mk_level_list min_precedence max_precedence ]
-
+ mk_level_list min_precedence max_precedence ];
(* {{{ Grammar for concrete syntax patterns, notation level 1 *)
+ begin
+ let level1_pattern = !grammars.level1_pattern in
EXTEND
GLOBAL: level1_pattern;
| "ident"; id = IDENT -> Ast.IdentVar id
]
];
+ mstyle: [
+ [ id = IDENT;
+ v = [ IDENT | NUMBER | COLOR | FLOATWITHUNIT ] -> id, v]];
+ mpadded: [
+ [ id = IDENT;
+ v = [ PERCENTAGE ] -> id, v]];
l1_simple_pattern:
[ "layout" LEFTA
[ p1 = SELF; SYMBOL "\\sub"; p2 = SELF ->
| p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l)))
- | SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
+ | p1 = SELF; SYMBOL "\\frac"; p2 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
| SYMBOL "\\infrule"; p1 = SELF; p2 = SELF; p3 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Box ((Ast.HOV, false, false), p l)))
| "break" -> return_term_of_level loc (fun _ -> Ast.Layout Ast.Break)
+ | "mstyle"; m = LIST1 mstyle ; LPAREN; t = l1_pattern; RPAREN ->
+ return_term_of_level loc
+ (fun l ->
+ Ast.Layout (Ast.Mstyle (m, t l)))
+ | "mpadded"; m = LIST1 mpadded ; LPAREN; t = l1_pattern; RPAREN ->
+ return_term_of_level loc
+ (fun l ->
+ Ast.Layout (Ast.Mpadded (m, t l)))
| LPAREN; p = l1_pattern; RPAREN ->
return_term_of_level loc (fun l -> CicNotationUtil.group (p l))
]
]
];
END
+ end;
(* }}} *)
-
(* {{{ Grammar for ast magics, notation level 2 *)
+ begin
+ let level2_meta = !grammars.level2_meta in
EXTEND
GLOBAL: level2_meta;
l2_variable: [
]
];
END
+ end;
(* }}} *)
-
(* {{{ Grammar for ast patterns, notation level 2 *)
+ begin
+ let level2_ast = !grammars.level2_ast in
+ let term = !grammars.term in
+ let let_defs = !grammars.let_defs in
+ let protected_binder_vars = !grammars.protected_binder_vars in
EXTEND
GLOBAL: level2_ast term let_defs protected_binder_vars;
level2_ast: [ [ p = term -> p ] ];
sort: [
[ "Prop" -> `Prop
| "Set" -> `Set
+ | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n
| "Type" -> `Type (CicUniv.fresh ())
| "CProp" -> `CProp (CicUniv.fresh ())
]
]
];
END
+ end
(* }}} *)
+;;
+
+let _ = initialize_grammars ();;
+
+let history = ref [];;
+
+let push () =
+ CicNotationLexer.push ();
+ history := (!owned_keywords,!grammars) :: !history;
+ owned_keywords := (initial_owned_keywords ());
+ grammars := initial_grammars ();
+ initialize_grammars ()
+;;
+
+let pop () =
+ CicNotationLexer.pop ();
+ match !history with
+ | [] -> assert false
+ | (kw,gram) :: old_history ->
+ owned_keywords := kw;
+ grammars := gram;
+ history := old_history
+;;
(** {2 API implementation} *)
let parse_level1_pattern precedence lexbuf =
exc_located_wrapper
- (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf) precedence)
+ (fun () -> Grammar.Entry.parse !grammars.level1_pattern (Obj.magic lexbuf) precedence)
let parse_level2_ast lexbuf =
exc_located_wrapper
- (fun () -> Grammar.Entry.parse level2_ast (Obj.magic lexbuf))
+ (fun () -> Grammar.Entry.parse !grammars.level2_ast (Obj.magic lexbuf))
let parse_level2_meta lexbuf =
exc_located_wrapper
- (fun () -> Grammar.Entry.parse level2_meta (Obj.magic lexbuf))
+ (fun () -> Grammar.Entry.parse !grammars.level2_meta (Obj.magic lexbuf))
let _ =
parse_level1_pattern_ref := parse_level1_pattern;
let parse_term lexbuf =
exc_located_wrapper
- (fun () -> (Grammar.Entry.parse term (Obj.magic lexbuf)))
+ (fun () -> (Grammar.Entry.parse !grammars.term (Obj.magic lexbuf)))
+
+let level2_ast_grammar () = !grammars.level2_ast_grammar
+let term () = !grammars.term
+let let_defs () = !grammars.let_defs
+let protected_binder_vars () = !grammars.protected_binder_vars
+
(** {2 Debugging} *)
let print_l2_pattern () =
- Grammar.print_entry Format.std_formatter (Grammar.Entry.obj term);
+ Grammar.print_entry Format.std_formatter (Grammar.Entry.obj !grammars.term);
Format.pp_print_flush Format.std_formatter ();
- flush stdout
+ flush stdout
(* vim:set encoding=utf8 foldmethod=marker: *)