X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=fcd209307fd73e6c1202e3439a6791ef968d24c2;hb=ae6757199708cc32166961debb52d48114c0eb74;hp=6736211d4e67fbf5b88990b1bf93535f74b2d5e9;hpb=b40e4e96e85103c7072985990c6b541371fd5a48;p=helm.git diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 6736211d4..fcd209307 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -30,7 +30,9 @@ open Printf module Ast = NotationPt module Env = NotationEnv -let prerr_endline _ = () +module StringSet = Set.Make(String) + +(* let prerr_endline _ = () *) exception Parse_error of string exception Level_not_found of int @@ -45,7 +47,7 @@ type ('a,'b,'c,'d,'e) grammars = { 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; @@ -90,39 +92,45 @@ let level_of precedence = 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 } @@ -134,21 +142,34 @@ let add_symbol_to_grammar status s = 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 -> @@ -161,7 +182,7 @@ let gram_term status = function 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 = @@ -170,7 +191,7 @@ let make_action status action bindings = [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc) | NoBinding :: tl -> Gramext.action - (fun (_,(loc: Ast.location)) -> + (fun ((*_,*)(loc: Ast.location)) -> let uri,desc = try CicNotationLexer.LocalizeEnv.find loc @@ -229,8 +250,11 @@ let update_sym_grammar status pattern = assert false and aux_literal status = function - | `Symbol (s,_) -> add_symbol_to_grammar status s - | `Keyword _ -> 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 @@ -279,7 +303,7 @@ let extract_term_production status pattern = | `Symbol (s,_) -> [NoBinding, gram_symbol status s] | `Keyword (s,_) -> (* assumption: s will be registered as a keyword with the lexer *) - [NoBinding, gram_keyword s] + [NoBinding, gram_keyword status s] | `Number (s,_) -> [NoBinding, gram_number s] and aux_layout = function | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2 @@ -916,6 +940,7 @@ END grammars ;; + let initial_grammars loctable keywords = let lexers = CicNotationLexer.mk_lexers loctable keywords in let level1_pattern_grammar = @@ -938,8 +963,8 @@ let initial_grammars loctable keywords = 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 @@ -1001,7 +1026,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action = [ 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) ]]];