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
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;
+ sym_table: ([ `Sym of string | `Kwd of 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;
}
~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
raise (Level_not_found precedence);
string_of_int precedence
-let add_symbol_to_grammar_explicit level2_ast_grammar
- sym_attributes sym_table s =
+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 s sym_table
+ 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 ("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,
- [ [Gramext.Stoken ("SYMBOL",s)], (* concrete l1 syntax *)
- (Gramext.action (fun _ loc -> None, loc))
- ; [Gramext.Stoken ("ATAG","")
+ [ [stok], (* 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)
+ ;stok
;Gramext.Stoken ("ATAGEND","")],
- (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc))
+ (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc)) *)
]]];
(* prerr_endline ("adding to grammar symbol " ^ s); *)
- (s,entry)::sym_table
+ (item,entry)::sym_table
-let add_symbol_to_grammar status s =
+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_symbol_to_grammar_explicit level2_ast_grammar sym_attributes sym_table s
+ 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 }
let gram_symbol status s =
let sym_table = status#notation_parser_db.grammars.sym_table in
let entry =
- try List.assoc s sym_table
+ 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 -> "\"" ^ x ^ "\"") syms in
- prerr_endline ("new symbol non-terminals: " ^ (String.concat ", " syms));
- prerr_endline ("unable to find symbol \"" ^ s ^ "\""); assert false)
+ 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
+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 ->
let gram_of_literal status =
function
| `Symbol (s,_) -> gram_symbol status s
- | `Keyword (s,_) -> gram_keyword s
+ | `Keyword (s,_) -> gram_keyword status s
| `Number (s,_) -> gram_number s
let make_action status action bindings =
let rec aux (vl : NotationEnv.t) =
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
- | NoBinding :: tl ->
+ | NoBinding csym :: tl ->
Gramext.action
- (fun (_,(loc: Ast.location)) ->
+ (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 (loc,uri,desc)))::vl) tl)
+ 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
assert false
and aux_literal status =
function
- | `Symbol (s,_) -> add_symbol_to_grammar status s
- | `Keyword _ -> status
- | `Number _ -> status
+ | _,`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.List0 (p, s)
| Ast.List1 (p, s) ->
let status =
- match s with None -> status | Some s' -> aux_literal status s'
+ match s with None -> status | Some s' -> aux_literal status (None,s')
in
aux status p
| _ -> assert false
assert false
and aux_literal =
function
- | `Symbol (s,_) -> [NoBinding, gram_symbol status 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 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.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 status "\\root "] @ aux p2
- @ [NoBinding, gram_symbol status "\\of "] @ aux p1
- | Ast.Sqrt p -> [NoBinding, gram_symbol status "\\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)
| 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),
| 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 ] ];
l1_magic_pattern: [
[ "list0"; p = l1_simple_pattern; sep = OPT 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
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
grammars
;;
+
let initial_grammars loctable keywords =
let lexers = CicNotationLexer.mk_lexers loctable keywords in
let level1_pattern_grammar =
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
+ (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
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;
[ None,
Some (*Gramext.NonA*) Gramext.NonA,
[ p_atoms, (* concrete l1 syntax *)
- (make_action status
+ (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