module Ast = NotationPt
module Env = NotationEnv
+module StringSet = Set.Make(String)
+
+(* let prerr_endline _ = () *)
+
exception Parse_error of string
exception Level_not_found of int
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: ([ `Sym of string | `Kwd of string ] * Stdpp.location Grammar.Entry.e) list;
let_defs: 'c Grammar.Entry.e;
- located: Stdpp.location Grammar.Entry.e;
+ let_codefs: 'c Grammar.Entry.e;
protected_binder_vars: 'd Grammar.Entry.e;
level2_meta: 'b Grammar.Entry.e;
}
~refresh_uri_in_reference t, n)
type binding =
- | NoBinding
+ | NoBinding of string option (* name of Ast.Symbol associated to this literal *)
| Binding of string * Env.value_type
| Env of (string * Env.value_type) list
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_item_to_grammar_explicit level2_ast_grammar
+ sym_attributes sym_table item =
+ let stok, nonterm = match item with
+ | `Sym sy -> Gramext.Stoken ("SYMBOL",sy), "sym" ^ sy
+ | `Kwd i -> Gramext.Stoken("",i), "kwd" ^ i
+ in
+ try
+ let _ = List.assoc item sym_table
+ in sym_table
+ with Not_found ->
+(* let entry = Grammar.Entry.create level2_ast_grammar ("sym" ^ s) in *)
+ let entry = Grammar.Entry.create level2_ast_grammar nonterm in
+ Grammar.extend
+ [ Grammar.Entry.obj entry,
+ None,
+ [ None,
+ Some (*Gramext.NonA*) Gramext.NonA,
+ [ [stok], (* concrete l1 syntax *)
+ (Gramext.action (fun _ loc -> (* None, *) loc))
+(* ; [Gramext.Stoken ("ATAG","")
+ ;Gramext.Snterm (Grammar.Entry.obj sym_attributes)
+ ;Gramext.Stoken ("SYMBOL","\005")
+ ;stok
+ ;Gramext.Stoken ("ATAGEND","")],
+ (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc)) *)
+ ]]];
+(* prerr_endline ("adding to grammar symbol " ^ s); *)
+ (item,entry)::sym_table
-let gram_ident status =
- Gramext.Snterm (Grammar.Entry.obj
+
+let add_item_to_grammar status item =
+ 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_item_to_grammar_explicit level2_ast_grammar sym_attributes sym_table
+ item
+ 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 (`Sym 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 -> match x with `Sym x | `Kwd x -> "\"" ^ x ^ "\"") syms in
+ prerr_endline ("new symbol/keyword non-terminals: " ^ (String.concat ", " syms));
+ prerr_endline ("unable to find symbol \"" ^ s ^ "\"");
+ (* XXX: typing error
+ * Gramext.Stoken("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))
(*Gramext.Stoken ("IDENT", s)*)
let gram_number s = Gramext.Stoken ("NUMBER", s)
-let gram_keyword s = Gramext.Stoken ("", s)
+let gram_keyword status s =
+ let sym_table = status#notation_parser_db.grammars.sym_table in
+ try Gramext.Snterm (Grammar.Entry.obj
+ (List.assoc (`Kwd 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 -> match x with `Sym x | `Kwd x -> "\"" ^ x ^ "\"") syms in
+ (* prerr_endline ("new symbol/keyword non-terminals: " ^ (String.concat ", " syms));
+ prerr_endline ("unable to find keyword \"" ^ s ^ "\""); *)
+ Gramext.Stoken("", s))
+
let gram_term status = function
| Ast.Self _ -> Gramext.Sself
| Ast.Level precedence ->
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 status 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 csym :: tl ->
+ Gramext.action
+ (fun ((*_,*)(loc: Ast.location)) ->
+ let uri,desc =
+ try
+ let a,b = HExtlib.loc_of_floc loc in
+ CicNotationLexer.LocalizeEnv.find loc
+ !(status#notation_parser_db.loctable)
+ with Not_found -> None, None
+ in aux (("",(Env.NoType,
+ Env.DisambiguationValue (csym,loc,uri,desc)))::vl) tl)
(* LUCA: DEFCON 3 BEGIN *)
| Binding (name, Env.TermType l) :: tl ->
Gramext.action
let rec aux acc =
function
[] -> List.rev acc
- | NoBinding :: tl -> aux acc tl
+ | NoBinding _ :: tl -> aux acc tl
| Env names :: tl -> aux (List.rev names @ acc) tl
| Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
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_item_to_grammar status (`Sym s)
+ | _,`Keyword (s,_) ->
+ if not (List.mem s CicNotationLexer.initial_keywords)
+ then add_item_to_grammar status (`Kwd s)
+ else 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 (None,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 ->
+ | csym,`Symbol (s,_) -> [NoBinding csym, gram_symbol status s]
+ | csym,`Keyword (s,_) ->
(* assumption: s will be registered as a keyword with the lexer *)
- [NoBinding, gram_keyword s]
- | `Number s -> [NoBinding, gram_number s]
+ [NoBinding csym, gram_keyword status s]
+ | csym,`Number (s,_) -> [NoBinding csym, 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 None, gram_symbol status "\\sub "] @ aux p2
+ | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sup "] @ aux p2
+ | Ast.Below (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\below "] @ aux p2
+ | Ast.Above (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\above "] @ aux p2
+ | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\frac "] @ aux p2
+ | Ast.InfRule (p1, p2, p3) -> [NoBinding None, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3
+ | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\atop "] @ aux p2
+ | Ast.Over (p1, p2) -> aux p1 @ [NoBinding None, 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 None, gram_symbol status "\\root "] @ aux p2
+ @ [NoBinding None, gram_symbol status "\\of "] @ aux p1
+ | Ast.Sqrt p -> [NoBinding None, 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,true)
+ | Ast.List1 (_, Some l) ->
+ Gramext.Slist1sep (s, gram_of_literal status l,true)
| _ -> 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))
+ ]
+ ];
+ rliteral: [
+ [ csymname = OPT [ "ref" ; csymname = CSYMBOL ->
+ prerr_endline ("parser in rliteral (ref " ^ csymname ^ ")");
+ csymname ];
+ lit = literal ->
+ csymname, lit
]
];
sep: [ [ "sep"; sep = literal -> sep ] ];
return_term_of_level loc (fun l -> Ast.Magic (m l))
| v = l1_pattern_variable ->
return_term_of_level loc (fun _ -> Ast.Variable v)
- | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l)
+ | l = rliteral -> return_term_of_level loc (fun _ -> Ast.Literal l)
]
];
END
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 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;
+ GLOBAL: level2_ast term let_defs let_codefs 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_item_to_grammar_explicit level2_ast_grammar sym_attributes)
+ [] (List.map (fun s -> `Sym s) 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
- 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;
+ let_codefs=let_codefs;
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) ]]];
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
projects / helm.git / blobdiff