X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=53c60820c78632bd58f3b8527d697897537c92ff;hb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;hp=b828f8bc508a974f06fac9e7c07ecb2d3ddc7eaf;hpb=f3f6b451707a3feb8245717e3fa7ca25df0ce8ef;p=helm.git diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index b828f8bc5..53c60820c 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -36,11 +36,12 @@ exception Level_not_found of int let min_precedence = 0 let max_precedence = 100 -type ('a,'b,'c,'d) grammars = { +type ('a,'b,'c,'d,'e) grammars = { level1_pattern: 'a Grammar.Entry.e; level2_ast: 'b Grammar.Entry.e; level2_ast_grammar : Grammar.g; term: 'b Grammar.Entry.e; + ident: 'e Grammar.Entry.e; let_defs: 'c Grammar.Entry.e; protected_binder_vars: 'd Grammar.Entry.e; level2_meta: 'b Grammar.Entry.e; @@ -48,14 +49,26 @@ type ('a,'b,'c,'d) grammars = { type checked_l1_pattern = CL1P of NotationPt.term * int +let refresh_uri_in_checked_l1_pattern ~refresh_uri_in_term + ~refresh_uri_in_reference (CL1P (t,n)) += + CL1P (NotationUtil.refresh_uri_in_term ~refresh_uri_in_term + ~refresh_uri_in_reference t, n) + +type binding = + | NoBinding + | Binding of string * Env.value_type + | Env of (string * Env.value_type) list + type db = { grammars: (int -> NotationPt.term, Ast.term, (Ast.term Ast.capture_variable list * Ast.term Ast.capture_variable * Ast.term * int) list, - Ast.term list * Ast.term option) grammars; - items: (checked_l1_pattern * int * Gramext.g_assoc * NotationPt.term) 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 } let int_of_string s = @@ -72,7 +85,10 @@ let level_of precedence = string_of_int precedence let gram_symbol s = Gramext.Stoken ("SYMBOL", s) -let gram_ident s = Gramext.Stoken ("IDENT", s) +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_term status = function @@ -80,7 +96,7 @@ let gram_term status = function | Ast.Level precedence -> Gramext.Snterml (Grammar.Entry.obj - (status#notation_parser_db.grammars.term: 'a Grammar.Entry.e), + (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e), level_of precedence) ;; @@ -90,11 +106,6 @@ let gram_of_literal = | `Keyword s -> gram_keyword s | `Number s -> gram_number s -type binding = - | NoBinding - | Binding of string * Env.value_type - | Env of (string * Env.value_type) list - let make_action action bindings = let rec aux (vl : NotationEnv.t) = function @@ -107,7 +118,7 @@ let make_action action bindings = aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl) | Binding (name, Env.StringType) :: tl -> Gramext.action - (fun (v:string) -> + (fun (v:Env.ident_or_var) -> aux ((name, (Env.StringType, Env.StringValue v)) :: vl) tl) | Binding (name, Env.NumType) :: tl -> Gramext.action @@ -146,7 +157,7 @@ let extract_term_production status pattern = | Ast.Magic m -> aux_magic m | Ast.Variable v -> aux_variable v | t -> - prerr_endline (NotationPp.pp_term t); + prerr_endline (NotationPp.pp_term status t); assert false and aux_literal = function @@ -211,7 +222,7 @@ let extract_term_production status pattern = | Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""] | Ast.TermVar (s,(Ast.Self level|Ast.Level level as lv)) -> [Binding (s, Env.TermType level), gram_term status lv] - | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""] + | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident status] | Ast.Ascription (p, s) -> assert false (* TODO *) | Ast.FreshVar _ -> assert false and inner_pattern p = @@ -316,43 +327,6 @@ let check_l1_pattern level1_pattern pponly level associativity = CL1P (cp,level) ;; -let extend status (CL1P (level1_pattern,precedence)) action = - assert false -(* - CicNotationParser.new_parser (); - let create_cb_old (l1, precedence, associativity, l2) = - ignore( - CicNotationParser.extend l1 - (fun env loc -> - NotationPt.AttributedTerm - (`Loc loc,TermContentPres.instantiate_level2 env l2))) - in - RefCounter.iter create_cb_old !parser_ref_counter; -*) -(* - let p_bindings, p_atoms = - List.split (extract_term_production status level1_pattern) - in - let level = level_of precedence in - let () = - 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 - (fun (env: NotationEnv.t) (loc: Ast.location) -> - (action env loc)) - p_bindings) ]]] - in - let keywords = NotationUtil.keywords_of_term level1_pattern in - let rule_id = p_atoms in - List.iter CicNotationLexer.add_level2_ast_keyword keywords; - rule_id -*) - (** {2 Grammar} *) let fold_cluster binder terms ty body = @@ -401,10 +375,6 @@ let parse_level2_meta grammars lexbuf = exc_located_wrapper (fun () -> Grammar.Entry.parse grammars.level2_meta (Obj.magic lexbuf)) -let parse_term grammars lexbuf = - exc_located_wrapper - (fun () -> (Grammar.Entry.parse grammars.term (Obj.magic lexbuf))) - (* create empty precedence level for "term" *) let initialize_grammars grammars = let dummy_action = @@ -586,9 +556,10 @@ END let level2_ast = grammars.level2_ast in let term = grammars.term 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; + GLOBAL: level2_ast term let_defs protected_binder_vars ident; level2_ast: [ [ p = term -> p ] ]; sort: [ [ "Prop" -> `Prop @@ -665,6 +636,19 @@ EXTEND | _ -> failwith "Invalid index name." ] ]; + ident: [ + [ name = IDENT -> Env.Ident name + | blob = UNPARSED_META -> + let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in + match meta with + | Ast.Variable (Ast.FreshVar _) -> + (* it makes sense: extend Env.ident_or_var *) + assert false + | Ast.Variable (Ast.IdentVar name) -> Env.Var name + | Ast.Variable (Ast.TermVar ("_",_)) -> Env.Var "_" + | _ -> failwith ("Invalid index name: " ^ blob) + ] + ]; let_defs: [ [ defs = LIST1 [ name = single_arg; @@ -679,8 +663,10 @@ EXTEND in let rec find_arg name n = function | [] -> + (* 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 name)) + (NotationPp.pp_term (new NCicPp.status) name)) | (l,_) :: tl -> (match position_of name 0 l with | None, len -> find_arg name (n + len) tl @@ -797,8 +783,8 @@ END grammars ;; -let initial_grammars = - let lexers = CicNotationLexer.mk_lexers [] in +let initial_grammars keywords = + let lexers = CicNotationLexer.mk_lexers keywords in let level1_pattern_grammar = Grammar.gcreate lexers.CicNotationLexer.level1_pattern_lexer in let level2_ast_grammar = @@ -809,6 +795,7 @@ let initial_grammars = Grammar.Entry.create level1_pattern_grammar "level1_pattern" in 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 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 @@ -816,6 +803,7 @@ let initial_grammars = initialize_grammars { level1_pattern=level1_pattern; level2_ast=level2_ast; term=term; + ident=ident; let_defs=let_defs; protected_binder_vars=protected_binder_vars; level2_meta=level2_meta; @@ -828,9 +816,9 @@ class type g_status = method notation_parser_db: db end -class status = - object(self) - val db = { grammars = initial_grammars ; items = [] } +class status0 ~keywords:kwds = + object + val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] } method notation_parser_db = db method set_notation_parser_db v = {< db = v >} method set_notation_parser_status @@ -838,14 +826,49 @@ class status = = fun o -> {< db = o#notation_parser_db >} end +class virtual status ~keywords:kwds = + object + inherit NCic.status + 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 p_bindings, p_atoms = + 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 + (fun (env: NotationEnv.t) (loc: Ast.location) -> + (action env loc)) + p_bindings) ]]]; + status + in + let current_item = + let level = level_of precedence in + level, level1_pattern, action in + let keywords = NotationUtil.keywords_of_term level1_pattern @ + status#notation_parser_db.keywords in + let items = current_item :: status#notation_parser_db.items in + let status = status#set_notation_parser_status (new status0 ~keywords) in + let status = status#set_notation_parser_db + {status#notation_parser_db with items = items} in + List.fold_left add1item status items +;; + + let parse_level1_pattern status = parse_level1_pattern status#notation_parser_db.grammars let parse_level2_ast status = parse_level2_ast status#notation_parser_db.grammars let parse_level2_meta status = parse_level2_meta status#notation_parser_db.grammars -let parse_term status = - parse_term status#notation_parser_db.grammars let level2_ast_grammar status = status#notation_parser_db.grammars.level2_ast_grammar