module Ast = NotationPt
module Env = NotationEnv
+let prerr_endline _ = ()
+
exception Parse_error of string
exception Level_not_found of int
sym_attributes: (string option * string option) Grammar.Entry.e;
sym_table: (string * Stdpp.location Grammar.Entry.e) list;
let_defs: 'c Grammar.Entry.e;
+ let_codefs: 'c Grammar.Entry.e;
protected_binder_vars: 'd Grammar.Entry.e;
level2_meta: 'b Grammar.Entry.e;
}
| Ast.List0 (_, None) -> Gramext.Slist0 s
| Ast.List1 (_, None) -> Gramext.Slist1 s
| Ast.List0 (_, Some l) ->
- Gramext.Slist0sep (s, gram_of_literal status l)
+ Gramext.Slist0sep (s, gram_of_literal status l,true)
| Ast.List1 (_, Some l) ->
- Gramext.Slist1sep (s, gram_of_literal status l)
+ Gramext.Slist1sep (s, gram_of_literal status l,true)
| _ -> assert false
in
[ Env (List.map Env.list_declaration p_names),
let term = grammars.term in
let atag_attributes = grammars.sym_attributes in
let let_defs = grammars.let_defs in
+ let let_codefs = grammars.let_codefs in
let ident = grammars.ident in
let protected_binder_vars = grammars.protected_binder_vars in
EXTEND
- GLOBAL: level2_ast term let_defs protected_binder_vars ident atag_attributes;
+ GLOBAL: level2_ast term let_defs let_codefs protected_binder_vars ident atag_attributes;
level2_ast: [ [ p = term -> p ] ];
sort: [
[ "Prop" -> `Prop
let uri,_ = CicNotationLexer.LocalizeEnv.find loc
!loctable in
match uri with
- | Some u -> id, `Uri u
- | None -> id, `Ambiguous
+ | Some u ->
+ prerr_endline ("trovata interpretazione per " ^ id ^ ": " ^ u);
+ id, `Uri u
+ | None ->
+ prerr_endline ("identificatore ambiguo: " ^ id);
+ id, `Ambiguous
+ with
+ | Not_found ->
+ prerr_endline ("identificatore non trovato: " ^ id);
+ id, `Ambiguous ]];
+ gnum: [
+ [ n = NUMBER ->
+ try
+ match CicNotationLexer.LocalizeEnv.find loc !loctable with
+ | _uri, Some interpr -> n, Some (Some "cic:/fakeuri.def(1)",interpr)
+ | _ -> n,None
with
- | Not_found -> id, `Ambiguous ]];
+ | Not_found -> n,None ]];
arg: [
[ LPAREN; names = LIST1 gident SEP SYMBOL ",";
SYMBOL ":"; ty = term; RPAREN ->
| u = URI -> return_term loc (Ast.Ident
(NUri.name_of_uri (NUri.uri_of_string u), `Uri u))
| r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
- | n = NUMBER -> return_term loc (Ast.Num (n, None))
+ | (n,interpr) = gnum -> return_term loc (Ast.Num (n, interpr))
| IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
| SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
| PLACEHOLDER -> return_term loc Ast.UserInput
[] initial_symbols
in
let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
+ let let_codefs = Grammar.Entry.create level2_ast_grammar "let_codefs" 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
sym_table=sym_table;
sym_attributes=sym_attributes;
let_defs=let_defs;
+ let_codefs=let_codefs;
protected_binder_vars=protected_binder_vars;
level2_meta=level2_meta;
level2_ast_grammar=level2_ast_grammar;
status#notation_parser_db.grammars.level2_ast_grammar
let term status = status#notation_parser_db.grammars.term
let let_defs status = status#notation_parser_db.grammars.let_defs
+let let_codefs status = status#notation_parser_db.grammars.let_codefs
let protected_binder_vars status =
status#notation_parser_db.grammars.protected_binder_vars