X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=66037155292c62d75ca540971d7af292daee07eb;hb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;hp=53c60820c78632bd58f3b8527d697897537c92ff;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 53c60820c..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 @@ -42,7 +46,10 @@ type ('a,'b,'c,'d,'e) grammars = { 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; + let_codefs: 'c Grammar.Entry.e; protected_binder_vars: 'd Grammar.Entry.e; level2_meta: 'b Grammar.Entry.e; } @@ -56,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 @@ -68,7 +75,8 @@ type db = { 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 = @@ -84,13 +92,84 @@ let level_of precedence = raise (Level_not_found precedence); string_of_int precedence -let gram_symbol s = Gramext.Stoken ("SYMBOL", s) -let gram_ident status = - Gramext.Snterm (Grammar.Entry.obj +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 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 -> @@ -100,17 +179,27 @@ let gram_term status = function 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 _ -> aux 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 @@ -134,6 +223,7 @@ let make_action action bindings = aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl) | Env _ :: tl -> Gramext.action (fun (v:NotationEnv.t) -> aux (v @ vl) tl) + | _ (* Binding (_,NoType) *) -> assert false (* LUCA: DEFCON 3 END *) in aux [] (List.rev bindings) @@ -142,12 +232,62 @@ 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 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 @@ -161,24 +301,24 @@ let extract_term_production status pattern = 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) @@ -208,8 +348,10 @@ let extract_term_production status pattern = 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), @@ -229,8 +371,8 @@ let extract_term_production status pattern = 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 @@ -338,7 +480,7 @@ let fold_exists terms ty body = List.fold_right (fun term body -> let lambda = Ast.Binder (`Lambda, (term, ty), body) in - Ast.Appl [ Ast.Symbol ("exists", 0); lambda ]) + Ast.Appl [ Ast.Symbol ("exists", None); lambda ]) terms body let fold_binder binder pt_names body = @@ -369,14 +511,15 @@ let parse_level1_pattern grammars precedence lexbuf = 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") @@ -413,9 +556,17 @@ EXTEND 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 ] ]; @@ -507,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 @@ -555,11 +706,13 @@ 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 @@ -568,16 +721,6 @@ EXTEND | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n ] ]; - explicit_subst: [ - [ SYMBOL "\\subst "; (* to avoid catching frequent "a [1]" cases *) - SYMBOL "["; - substs = LIST1 [ - i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) - ] SEP SYMBOL ";"; - SYMBOL "]" -> - substs - ] - ]; meta_subst: [ [ s = SYMBOL "_" -> None | p = term -> Some p ] @@ -589,12 +732,12 @@ EXTEND [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN -> id, Some typ | arg = single_arg -> arg, None - | id = PIDENT -> Ast.Ident (id, None), None - | SYMBOL "_" -> Ast.Ident ("_", None), None + | id = PIDENT -> Ast.Ident (id, `Ambiguous), None + | SYMBOL "_" -> Ast.Ident ("_", `Ambiguous), None | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN -> - Ast.Ident (id, None), Some typ + Ast.Ident (id, `Ambiguous), Some typ | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN -> - Ast.Ident ("_", None), Some typ + Ast.Ident ("_", `Ambiguous), Some typ ] ]; match_pattern: [ @@ -612,27 +755,51 @@ EXTEND | SYMBOL <:unicode> (* λ *) -> `Lambda ] ]; + gident: [ + [ 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 IDENT SEP SYMBOL ","; + [ LPAREN; names = LIST1 gident SEP SYMBOL ","; SYMBOL ":"; ty = term; RPAREN -> - List.map (fun n -> Ast.Ident (n, None)) names, Some ty - | name = IDENT -> [Ast.Ident (name, None)], None + List.map (fun (n,u) -> Ast.Ident (n,u)) names, Some ty + | (name,uri) = gident -> [Ast.Ident (name,uri)], None | blob = UNPARSED_META -> let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in match meta with | Ast.Variable (Ast.FreshVar _) -> [meta], None - | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None + | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", `Ambiguous)], None | _ -> failwith "Invalid bound name." ] ]; single_arg: [ - [ name = IDENT -> Ast.Ident (name, None) + [ (name,uri) = gident -> Ast.Ident (name,uri) | blob = UNPARSED_META -> let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in match meta with | Ast.Variable (Ast.FreshVar _) | Ast.Variable (Ast.IdentVar _) -> meta - | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None) + | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", `Ambiguous) | _ -> failwith "Invalid index name." ] ]; @@ -666,7 +833,7 @@ EXTEND (* 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 @@ -692,7 +859,7 @@ EXTEND [ vars = [ l = [ l = LIST1 single_arg SEP SYMBOL "," -> l | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," -> - List.map (fun x -> Ast.Ident(x,None)) l + List.map (fun x -> Ast.Ident(x,`Ambiguous)) l ] -> l ]; typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ) ] @@ -712,8 +879,8 @@ EXTEND var = [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN -> id, Some typ - | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] -> - Ast.Ident(id,None), ty ]; + | (id,uri) = gident; ty = OPT [ SYMBOL ":"; typ = term -> typ] -> + Ast.Ident (id,uri), ty ]; SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (Ast.LetIn (var, p1, p2)) @@ -745,13 +912,12 @@ EXTEND ]; term: LEVEL "90" [ - [ id = IDENT -> return_term loc (Ast.Ident (id, None)) - | id = IDENT; s = explicit_subst -> - return_term loc (Ast.Ident (id, Some s)) - | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0)) - | u = URI -> return_term loc (Ast.Uri (u, None)) + [ (id,uri) = gident -> return_term loc (Ast.Ident (id,uri)) + | s = CSYMBOL -> return_term loc (Ast.Symbol (s, None)) + | 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, 0)) + | (n,interpr) = gnum -> return_term loc (Ast.Num (n, interpr)) | IMPLICIT -> return_term loc (Ast.Implicit `JustOne) | SYMBOL <:unicode> -> return_term loc (Ast.Implicit `Vector) | PLACEHOLDER -> return_term loc Ast.UserInput @@ -783,8 +949,9 @@ END 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 = @@ -796,15 +963,32 @@ let initial_grammars keywords = 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 + (* 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; + let_codefs=let_codefs; protected_binder_vars=protected_binder_vars; level2_meta=level2_meta; level2_ast_grammar=level2_ast_grammar; @@ -818,33 +1002,40 @@ class type g_status = 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), Some (Gramext.Level level), [ None, Some (*Gramext.NonA*) Gramext.NonA, - [ p_atoms, - (make_action + [ p_atoms, (* concrete l1 syntax *) + (make_action status (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc)) p_bindings) ]]]; @@ -874,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