(Gramext.action (fun _ loc -> None, loc))
; [Gramext.Stoken ("ATAG","")
;Gramext.Snterm (Grammar.Entry.obj sym_attributes)
- ;Gramext.Stoken ("SYMBOL",">")
+ ;Gramext.Stoken ("SYMBOL","\005")
;Gramext.Stoken ("SYMBOL",s)
;Gramext.Stoken ("ATAGEND","")],
(Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc))
]]];
- prerr_endline ("adding to grammar symbol " ^ s);
+(* prerr_endline ("adding to grammar symbol " ^ s); *)
(s,entry)::sym_table
let gram_of_literal status =
function
- | `Symbol s -> gram_symbol status s
- | `Keyword s -> gram_keyword s
- | `Number s -> gram_number s
+ | `Symbol (s,_) -> gram_symbol status s
+ | `Keyword (s,_) -> gram_keyword s
+ | `Number (s,_) -> gram_number s
let make_action status action bindings =
let rec aux (vl : NotationEnv.t) =
assert false
and aux_literal status =
function
- | `Symbol s -> add_symbol_to_grammar status s
- | `Keyword s -> status
- | `Number s -> status
+ | `Symbol (s,_) -> add_symbol_to_grammar status s
+ | `Keyword _ -> status
+ | `Number _ -> status
and aux_layout status = function
| Ast.Sub (p1, p2) -> aux (aux status p1) p2
| Ast.Sup (p1, p2) -> aux (aux status p1) p2
assert false
and aux_literal =
function
- | `Symbol s -> [NoBinding, gram_symbol status s]
- | `Keyword s ->
+ | `Symbol (s,_) -> [NoBinding, gram_symbol status s]
+ | `Keyword (s,_) ->
(* assumption: s will be registered as a keyword with the lexer *)
[NoBinding, gram_keyword s]
- | `Number s -> [NoBinding, gram_number s]
+ | `Number (s,_) -> [NoBinding, gram_number s]
and aux_layout = function
| Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2
| Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sup "] @ aux p2
fun l -> List.map (fun x -> x l) p ]
];
literal: [
- [ s = SYMBOL -> `Symbol s
- | k = QKEYWORD -> `Keyword k
- | n = NUMBER -> `Number n
+ [ s = SYMBOL -> `Symbol (s, (None,None))
+ | k = QKEYWORD -> `Keyword (k, (None,None))
+ | n = NUMBER -> `Number (n,(None,None))
]
];
sep: [ [ "sep"; sep = literal -> sep ] ];
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 -> id, `Ambiguous ]];
+ | 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 -> n,None ]];
arg: [
[ LPAREN; names = LIST1 gident SEP SYMBOL ",";
SYMBOL ":"; ty = term; RPAREN ->
(* CSC: new NCicPp.status is the best I can do here
without changing the return type *)
Ast.fail loc (sprintf "Argument %s not found"
- (NotationPp.pp_term (new NCicPp.status) name))
+ (NotationPp.pp_term (new NCicPp.status None) name))
| (l,_) :: tl ->
(match position_of name 0 l with
| None, len -> find_arg name (n + len) tl
| 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
db.loctable := CicNotationLexer.LocalizeEnv.empty
end
-class virtual status ~keywords:kwds =
+class virtual status uid ~keywords:kwds =
object
- inherit NCic.status
+ inherit NCic.status uid
inherit status0 kwds
end