X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=e34b690d311a37f16e76891c0fc6a8950d6d8d5f;hb=237f4bfbb6d79b38e9417b776495b068b54aff6a;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..e34b690d3 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -42,6 +42,8 @@ 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: (string * Stdpp.location Grammar.Entry.e) list; let_defs: 'c Grammar.Entry.e; protected_binder_vars: 'd Grammar.Entry.e; level2_meta: 'b Grammar.Entry.e; @@ -68,7 +70,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,7 +87,59 @@ let level_of precedence = raise (Level_not_found precedence); string_of_int precedence -let gram_symbol s = Gramext.Stoken ("SYMBOL", s) +let add_symbol_to_grammar_explicit level2_ast_grammar + sym_attributes sym_table s = + try + let _ = List.assoc s sym_table + in sym_table + with Not_found -> + let entry = Grammar.Entry.create level2_ast_grammar ("sym" ^ s) 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","") + ;Gramext.Snterm (Grammar.Entry.obj sym_attributes) + ;Gramext.Stoken ("SYMBOL","\005") + ;Gramext.Stoken ("SYMBOL",s) + ;Gramext.Stoken ("ATAGEND","")], + (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc)) + ]]]; +(* prerr_endline ("adding to grammar symbol " ^ s); *) + (s,entry)::sym_table + + +let add_symbol_to_grammar status s = + 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 + 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 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) + 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)) @@ -100,17 +155,26 @@ 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 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 :: tl -> + Gramext.action + (fun (_,(loc: Ast.location)) -> + let uri,desc = + try + 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) (* LUCA: DEFCON 3 BEGIN *) | Binding (name, Env.TermType l) :: tl -> Gramext.action @@ -134,6 +198,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) @@ -148,6 +213,53 @@ let flatten_opt = 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_symbol_to_grammar status s + | `Keyword _ -> 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 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 +273,24 @@ let extract_term_production status pattern = assert false and aux_literal = function - | `Symbol s -> [NoBinding, gram_symbol s] - | `Keyword s -> + | `Symbol (s,_) -> [NoBinding, gram_symbol status s] + | `Keyword (s,_) -> (* assumption: s will be registered as a keyword with the lexer *) [NoBinding, gram_keyword s] - | `Number s -> [NoBinding, gram_number s] + | `Number (s,_) -> [NoBinding, 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, 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.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, gram_symbol status "\\root "] @ aux p2 + @ [NoBinding, gram_symbol status "\\of "] @ aux p1 + | Ast.Sqrt p -> [NoBinding, 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 +320,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 +343,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 +452,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 +483,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 +528,9 @@ 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)) ] ]; sep: [ [ "sep"; sep = literal -> sep ] ]; @@ -555,11 +670,12 @@ 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 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 protected_binder_vars ident atag_attributes; level2_ast: [ [ p = term -> p ] ]; sort: [ [ "Prop" -> `Prop @@ -568,16 +684,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 +695,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 +718,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 +796,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 +822,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 +842,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 +875,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 +912,8 @@ 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,14 +925,29 @@ 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_symbol_to_grammar_explicit level2_ast_grammar sym_attributes) + [] initial_symbols + in let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" 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; protected_binder_vars=protected_binder_vars; level2_meta=level2_meta; @@ -818,33 +962,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) ]]];