level2_ast_grammar : Grammar.g;
term: 'b Grammar.Entry.e;
ident: 'e Grammar.Entry.e;
+ sym_attributes: (string option * string option) Grammar.Entry.e;
+ sym_table: (string * Stdpp.location Grammar.Entry.e) list;
let_defs: 'c Grammar.Entry.e;
- located: Stdpp.location Grammar.Entry.e;
protected_binder_vars: 'd Grammar.Entry.e;
level2_meta: 'b Grammar.Entry.e;
}
Ast.term Ast.capture_variable * Ast.term * int) list,
Ast.term list * Ast.term option, Env.ident_or_var) grammars;
keywords: string list;
- items: (string * Ast.term * (NotationEnv.t -> Ast.location -> Ast.term)) list
+ items: (string * Ast.term * (NotationEnv.t -> Ast.location -> Ast.term)) list;
+ loctable: (string option * string option) CicNotationLexer.LocalizeEnv.t ref
}
let int_of_string s =
raise (Level_not_found precedence);
string_of_int precedence
-let gram_symbol s =
- Gramext.srules
- [ [ Gramext.Stoken ("SYMBOL",s) ], Gramext.action (fun _ loc -> loc) ]
+let add_symbol_to_grammar_explicit level2_ast_grammar
+ sym_attributes sym_table s =
+ try
+ let _ = List.assoc s sym_table
+ in sym_table
+ with Not_found ->
+ let entry = Grammar.Entry.create level2_ast_grammar ("sym" ^ s) in
+ Grammar.extend
+ [ Grammar.Entry.obj entry,
+ None,
+ [ None,
+ Some (*Gramext.NonA*) Gramext.NonA,
+ [ [Gramext.Stoken ("SYMBOL",s)], (* concrete l1 syntax *)
+ (Gramext.action (fun _ loc -> None, loc))
+ ; [Gramext.Stoken ("ATAG","")
+ ;Gramext.Snterm (Grammar.Entry.obj sym_attributes)
+ ;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); *)
+ (s,entry)::sym_table
+
+let add_symbol_to_grammar status s =
+ let sym_attributes = status#notation_parser_db.grammars.sym_attributes in
+ let sym_table = status#notation_parser_db.grammars.sym_table in
+ let level2_ast_grammar =
+ status#notation_parser_db.grammars.level2_ast_grammar
+ in
+ let sym_table =
+ add_symbol_to_grammar_explicit level2_ast_grammar sym_attributes sym_table s
+ in
+ let grammars =
+ { status#notation_parser_db.grammars with sym_table = sym_table }
+ in
+ let notation_parser_db =
+ { status#notation_parser_db with grammars = grammars } in
+ status#set_notation_parser_db notation_parser_db
+
+let gram_symbol status s =
+ let sym_table = status#notation_parser_db.grammars.sym_table in
+ let entry =
+ try List.assoc s sym_table
+ with Not_found ->
+ (let syms = List.map fst (status#notation_parser_db.grammars.sym_table) in
+ let syms = List.map (fun x -> "\"" ^ x ^ "\"") syms in
+ prerr_endline ("new symbol non-terminals: " ^ (String.concat ", " syms));
+ prerr_endline ("unable to find symbol \"" ^ s ^ "\""); assert false)
+ in
+ Gramext.Snterm (Grammar.Entry.obj entry)
+
let gram_ident status =
Gramext.Snterm (Grammar.Entry.obj
(status#notation_parser_db.grammars.ident : 'a Grammar.Entry.e))
level_of precedence)
;;
-let gram_of_literal =
+let gram_of_literal status =
function
- | `Symbol s -> gram_symbol 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 action bindings =
+let make_action status action bindings =
let rec aux (vl : NotationEnv.t) =
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
- | NoBinding :: tl -> Gramext.action
- (fun (loc: Ast.location) ->
- aux (("",(Env.NoType,Env.LocValue loc))::vl) tl)
+ | NoBinding :: tl ->
+ Gramext.action
+ (fun (_,(loc: Ast.location)) ->
+ let uri,desc =
+ try
+ CicNotationLexer.LocalizeEnv.find loc
+ !(status#notation_parser_db.loctable)
+ with Not_found -> None, None
+ in aux (("",(Env.NoType,
+ Env.DisambiguationValue (loc,uri,desc)))::vl) tl)
(* LUCA: DEFCON 3 BEGIN *)
| Binding (name, Env.TermType l) :: tl ->
Gramext.action
in
aux []
+(* given a level 1 pattern, adds productions for symbols when needed *)
+let update_sym_grammar status pattern =
+ let rec aux status = function
+ | Ast.AttributedTerm (_, t) -> aux status t
+ | Ast.Literal l -> aux_literal status l
+ | Ast.Layout l -> aux_layout status l
+ | Ast.Magic m -> aux_magic status m
+ | Ast.Variable v -> aux_variable status v
+ | t ->
+ prerr_endline (NotationPp.pp_term status t);
+ assert false
+ and aux_literal status =
+ function
+ | `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
+ | Ast.Below (p1, p2) -> aux (aux status p1) p2
+ | Ast.Above (p1, p2) -> aux (aux status p1) p2
+ | Ast.Frac (p1, p2) -> aux (aux status p1) p2
+ | Ast.InfRule (p1, p2, p3) -> aux (aux (aux status p1) p2) p3
+ | Ast.Atop (p1, p2) -> aux (aux status p1) p2
+ | Ast.Over (p1, p2) -> aux (aux status p1) p2
+ | Ast.Root (p1, p2) -> aux (aux status p1) p2
+ | Ast.Sqrt p -> aux status p
+ | Ast.Break -> status
+ | Ast.Box (_, pl) -> List.fold_left aux status pl
+ | Ast.Group pl -> List.fold_left aux status pl
+ | Ast.Mstyle (_,pl) -> List.fold_left aux status pl
+ | Ast.Mpadded (_,pl) -> List.fold_left aux status pl
+ | Ast.Maction l -> List.fold_left aux status l
+ and aux_magic status magic =
+ match magic with
+ | Ast.Opt p -> aux status p
+ | Ast.List0 (p, s)
+ | Ast.List1 (p, s) ->
+ let status =
+ match s with None -> status | Some s' -> aux_literal status s'
+ in
+ aux status p
+ | _ -> assert false
+ and aux_variable status _ = status
+ in
+ aux status pattern
+
(* given a level 1 pattern computes the new RHS of "term" grammar entry *)
let extract_term_production status pattern =
let rec aux = function
assert false
and aux_literal =
function
- | `Symbol s -> [NoBinding, gram_symbol 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 "\\sub "] @ aux p2
- | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup "] @ aux p2
- | 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) -> [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.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
+ | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\below "] @ aux p2
+ | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\above "] @ aux p2
+ | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\frac "] @ aux p2
+ | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3
+ | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\atop "] @ aux p2
+ | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\over "] @ aux p2
| Ast.Root (p1, p2) ->
- [NoBinding, gram_symbol "\\root "] @ aux p2
- @ [NoBinding, gram_symbol "\\of "] @ aux p1
- | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt "] @ aux p
+ [NoBinding, gram_symbol status "\\root "] @ aux p2
+ @ [NoBinding, gram_symbol status "\\of "] @ aux p1
+ | Ast.Sqrt p -> [NoBinding, gram_symbol status "\\sqrt "] @ aux p
| Ast.Break -> []
| Ast.Box (_, pl) -> List.flatten (List.map aux pl)
| Ast.Group pl -> List.flatten (List.map aux pl)
match magic with
| Ast.List0 (_, None) -> Gramext.Slist0 s
| Ast.List1 (_, None) -> Gramext.Slist1 s
- | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
- | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+ | Ast.List0 (_, Some l) ->
+ Gramext.Slist0sep (s, gram_of_literal status l)
+ | Ast.List1 (_, Some l) ->
+ Gramext.Slist1sep (s, gram_of_literal status l)
| _ -> assert false
in
[ Env (List.map Env.list_declaration p_names),
let p_bindings, p_atoms = List.split (aux p) in
let p_names = flatten_opt p_bindings in
let action =
- make_action (fun (env : NotationEnv.t) (loc : Ast.location) -> env)
- p_bindings
+ make_action status
+ (fun (env : NotationEnv.t) (loc : Ast.location) -> env) p_bindings
in
p_bindings, p_atoms, p_names, action
in
let parse_level2_ast grammars lexbuf =
exc_located_wrapper
- (fun () -> Grammar.Entry.parse grammars.level2_ast (Obj.magic lexbuf))
+ (fun () ->
+ Grammar.Entry.parse grammars.level2_ast (Obj.magic lexbuf))
let parse_level2_meta grammars lexbuf =
exc_located_wrapper
(fun () -> Grammar.Entry.parse grammars.level2_meta (Obj.magic lexbuf))
(* create empty precedence level for "term" *)
-let initialize_grammars grammars =
+let initialize_grammars loctable grammars =
let dummy_action =
Gramext.action (fun _ ->
failwith "internal error, lexer generated a dummy token")
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 ] ];
begin
let level2_ast = grammars.level2_ast in
let term = grammars.term in
+ let atag_attributes = grammars.sym_attributes in
let let_defs = grammars.let_defs 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;
+ GLOBAL: level2_ast term let_defs protected_binder_vars ident atag_attributes;
level2_ast: [ [ p = term -> p ] ];
sort: [
[ "Prop" -> `Prop
| SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
]
];
- tident: [
- [ uri = HREF;
- id = IDENT;
- HREFEND -> (id, `Uri uri) ]];
gident: [
- [ fullident = tident -> fullident;
- | id = IDENT -> (id, `Ambiguous) ]];
+ [ id = IDENT ->
+ try
+ let uri,_ = CicNotationLexer.LocalizeEnv.find loc
+ !loctable in
+ match uri with
+ | 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 -> n,None ]];
arg: [
[ LPAREN; names = LIST1 gident SEP SYMBOL ",";
SYMBOL ":"; ty = term; RPAREN ->
| _ -> failwith ("Invalid index name: " ^ blob)
]
];
- located: [
- [ s = SYMBOL -> loc ]
- ];
let_defs: [
[ defs = LIST1 [
name = single_arg;
(* 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
grammars
;;
-let initial_grammars keywords =
- let lexers = CicNotationLexer.mk_lexers keywords in
+let initial_grammars loctable keywords =
+ let lexers = CicNotationLexer.mk_lexers loctable keywords in
let level1_pattern_grammar =
Grammar.gcreate lexers.CicNotationLexer.level1_pattern_lexer in
let level2_ast_grammar =
let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" in
let term = Grammar.Entry.create level2_ast_grammar "term" in
let ident = Grammar.Entry.create level2_ast_grammar "ident" in
- let located = Grammar.Entry.create level2_ast_grammar "located" in
+ (* unexpanded TeX macros terminated by a space (see comment in
+ * CicNotationLexer) *)
+ let initial_symbols =
+ ["\\sub ";"\\sup ";"\\below ";"\\above ";"\\frac "
+ ;"\\infrule ";"\\atop ";"\\over ";"\\root ";"\\of ";"\\sqrt "] in
+ let sym_attributes =
+ Grammar.Entry.create level2_ast_grammar "atag_attributes" in
+ let sym_table =
+ List.fold_left
+ (add_symbol_to_grammar_explicit level2_ast_grammar sym_attributes)
+ [] initial_symbols
+ 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
- initialize_grammars { level1_pattern=level1_pattern;
+ initialize_grammars loctable
+ { level1_pattern=level1_pattern;
level2_ast=level2_ast;
term=term;
ident=ident;
+ sym_table=sym_table;
+ sym_attributes=sym_attributes;
let_defs=let_defs;
- located=located;
protected_binder_vars=protected_binder_vars;
level2_meta=level2_meta;
level2_ast_grammar=level2_ast_grammar;
class status0 ~keywords:kwds =
object
- val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] }
+ val db =
+ let lt = ref CicNotationLexer.LocalizeEnv.empty in
+ { grammars = initial_grammars lt kwds; keywords = kwds;
+ items = []; loctable = lt }
method notation_parser_db = db
method set_notation_parser_db v = {< db = v >}
method set_notation_parser_status
: 'status. #g_status as 'status -> 'self
= fun o -> {< db = o#notation_parser_db >}
+ method reset_loctable () =
+ 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
let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
(* move inside constructor XXX *)
let add1item status (level, level1_pattern, action) =
+ let status = update_sym_grammar status level1_pattern in
let p_bindings, p_atoms =
- List.split (extract_term_production status level1_pattern) in
+ List.split (extract_term_production status level1_pattern)
+ in
Grammar.extend
[ Grammar.Entry.obj
(status#notation_parser_db.grammars.term : 'a Grammar.Entry.e),
[ None,
Some (*Gramext.NonA*) Gramext.NonA,
[ p_atoms, (* concrete l1 syntax *)
- (make_action
+ (make_action status
(fun (env: NotationEnv.t) (loc: Ast.location) ->
(action env loc))
p_bindings) ]]];
projects / helm.git / blobdiff