module N = NotationPt
module G = GrafiteAst
-module L = LexiconAst
module LE = LexiconEngine
-exception NoInclusionPerformed of string (* full path *)
-
type 'a localized_option =
LSome of 'a
| LNone of G.loc
if (try ignore (NReference.reference_of_string uri); true
with NReference.IllFormedReference _ -> false)
then
- L.Ident_alias (id, uri)
+ G.Ident_alias (id, uri)
else
raise
(HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
let instance =
match instance with Some i -> i | None -> 0
in
- L.Symbol_alias (symbol, instance, dsc)
+ G.Symbol_alias (symbol, instance, dsc)
| IDENT "num";
instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
SYMBOL "="; dsc = QSTRING ->
let instance =
match instance with Some i -> i | None -> 0
in
- L.Number_alias (instance, dsc)
+ G.Number_alias (instance, dsc)
]
];
argument: [
include_command: [ [
IDENT "include" ; path = QSTRING ->
- loc,path,true,L.WithPreferences
- | IDENT "include" ; IDENT "source" ; path = QSTRING ->
- loc,path,false,L.WithPreferences
+ loc,path,G.WithPreferences
| IDENT "include'" ; path = QSTRING ->
- loc,path,true,L.WithoutPreferences
+ loc,path,G.WithoutPreferences
]];
grafite_ncommand: [ [
m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
G.NCopy (loc,s,NUri.uri_of_string u,
List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
+ | lc = lexicon_command -> lc
]];
lexicon_command: [ [
IDENT "alias" ; spec = alias_spec ->
- L.Alias (loc, spec)
+ G.Alias (loc, spec)
| IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
- L.Notation (loc, dir, l1, assoc, prec, l2)
+ G.Notation (loc, dir, l1, assoc, prec, l2)
| IDENT "interpretation"; id = QSTRING;
(symbol, args, l3) = interpretation ->
- L.Interpretation (loc, id, (symbol, args), l3)
+ G.Interpretation (loc, id, (symbol, args), l3)
]];
executable: [
[ ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
];
statement: [
[ ex = executable ->
- LSome (G.Executable (loc, ex))
+ LSome (G.Executable (loc, ex))
| com = comment ->
- LSome (G.Comment (loc, com))
- | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
- LSome (G.Executable
- (loc,G.Command (loc,G.Include (iloc,fname,(),""))))
- | scom = lexicon_command ; SYMBOL "." ->
- assert false
-(*
- fun ?(never_include=false) ~include_paths status ->
- let status = LE.eval_command status scom in
- status, LNone loc
-*)
+ LSome (G.Comment (loc, com))
+ | (iloc,fname,mode) = include_command ; SYMBOL "." ->
+ LSome (G.Executable (loc,G.NCommand (loc,G.Include (iloc,mode,fname))))
| EOI -> raise End_of_file
]
];
class type g_status =
object
- inherit LexiconEngine.g_status
+ inherit LexiconTypes.g_status
method parser_db: db
end
class status =
- let lstatus = assert false in
- let grammar = CicNotationParser.level2_ast_grammar lstatus in
- object
- inherit LexiconEngine.status
- val db =
- mk_parser (Grammar.Entry.create grammar "statement") lstatus
- method parser_db = db
- method set_parser_db v = {< db = v >}
+ object(self)
+ inherit LexiconTypes.status as super
+ val mutable db = None
+ method parser_db = match db with None -> assert false | Some x -> x
+ method set_parser_db v = {< db = Some v >}
method set_parser_status
: 'status. #g_status as 'status -> 'self
- = fun o -> {< db = o#parser_db >}#set_lexicon_engine_status o
+ = fun o -> {< db = Some o#parser_db >}#set_lexicon_engine_status o
+ initializer
+ let grammar = CicNotationParser.level2_ast_grammar self in
+ db <- Some (mk_parser (Grammar.Entry.create grammar "statement") self)
end
+let extend status l1 action =
+ let status = CicNotationParser.extend status l1 action in
+ let grammar = CicNotationParser.level2_ast_grammar status in
+ status#set_parser_db
+ (mk_parser (Grammar.Entry.create grammar "statement") status)
+;;
+
+
let parse_statement status =
parse_statement status#parser_db