X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=66037155292c62d75ca540971d7af292daee07eb;hb=48c011f52853dd106dbf9cbbd1b9da61277fba3b;hp=e34b690d311a37f16e76891c0fc6a8950d6d8d5f;hpb=237f4bfbb6d79b38e9417b776495b068b54aff6a;p=helm.git diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index e34b690d3..660371552 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -30,6 +30,10 @@ open Printf 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 @@ -43,8 +47,9 @@ 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; level2_meta: 'b Grammar.Entry.e; } @@ -58,7 +63,7 @@ let refresh_uri_in_checked_l1_pattern ~refresh_uri_in_term ~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 @@ -87,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 } @@ -131,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 -> @@ -158,23 +182,24 @@ 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 = 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 @@ -207,7 +232,7 @@ let flatten_opt = 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 @@ -226,9 +251,12 @@ let update_sym_grammar status pattern = 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 @@ -252,7 +280,7 @@ let update_sym_grammar status pattern = | 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 @@ -273,24 +301,24 @@ let extract_term_production status pattern = 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) @@ -321,9 +349,9 @@ let extract_term_production status pattern = | Ast.List0 (_, None) -> Gramext.Slist0 s | Ast.List1 (_, None) -> Gramext.Slist1 s | Ast.List0 (_, Some l) -> - Gramext.Slist0sep (s, gram_of_literal status l, true) + Gramext.Slist0sep (s, gram_of_literal status l,true) | Ast.List1 (_, Some l) -> - Gramext.Slist1sep (s, gram_of_literal status l, true) + Gramext.Slist1sep (s, gram_of_literal status l,true) | _ -> assert false in [ Env (List.map Env.list_declaration p_names), @@ -533,6 +561,14 @@ EXTEND | 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 -> @@ -622,7 +658,7 @@ EXTEND 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 @@ -672,10 +708,11 @@ 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 @@ -912,6 +949,7 @@ END grammars ;; + let initial_grammars loctable keywords = let lexers = CicNotationLexer.mk_lexers loctable keywords in let level1_pattern_grammar = @@ -934,10 +972,11 @@ 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 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 @@ -949,6 +988,7 @@ let initial_grammars loctable keywords = 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; @@ -995,7 +1035,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) ]]]; @@ -1025,6 +1065,7 @@ let level2_ast_grammar status = 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