X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=36a3fb01771bac4cfb10274087a1785dbd5b0741;hb=712af5b8dc7dab1ebfa6532b73b91c96cb4c6837;hp=f3953eb08f3e5a24302c142d38c93b15ac8e98a1;hpb=ac80c2cd2667de2942182ae0a98ad3dbadd7b559;p=helm.git diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index f3953eb08..36a3fb017 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -36,6 +36,11 @@ exception Level_not_found of int let min_precedence = 0 let max_precedence = 100 +let hash_expr e = + e + |> Hashtbl.hash + |> Printf.sprintf "%08x" + type ('a,'b,'c,'d,'e) grammars = { level1_pattern: 'a Grammar.Entry.e; level2_ast: 'b Grammar.Entry.e; @@ -43,6 +48,7 @@ type ('a,'b,'c,'d,'e) grammars = { term: 'b Grammar.Entry.e; ident: 'e Grammar.Entry.e; 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; } @@ -73,7 +79,7 @@ type db = { let int_of_string s = try - Pervasives.int_of_string s + Stdlib.int_of_string s with Failure _ -> failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s) @@ -157,7 +163,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 @@ -188,15 +194,16 @@ let extract_term_production status pattern = and aux_magic magic = match magic with | Ast.Opt p -> - let p_bindings, p_atoms, p_names, p_action = inner_pattern p in - let action (env_opt : NotationEnv.t option) (loc : Ast.location) = + let _p_bindings, p_atoms, p_names, p_action = inner_pattern p in + let action (env_opt : NotationEnv.t option) (_loc : Ast.location) = match env_opt with | Some env -> List.map Env.opt_binding_some env | None -> List.map Env.opt_binding_of_name p_names in [ Env (List.map Env.opt_declaration p_names), Gramext.srules - [ [ Gramext.Sopt (Gramext.srules [ p_atoms, p_action ]) ], + [ [ Gramext.Sopt (Gramext.srules [ p_atoms, hash_expr p_action, p_action ]) ], + hash_expr action, Gramext.action action ] ] | Ast.List0 (p, _) | Ast.List1 (p, _) -> @@ -208,13 +215,14 @@ 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 l, false) + | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l, false) | _ -> assert false in [ Env (List.map Env.list_declaration p_names), Gramext.srules - [ [ gram_of_list (Gramext.srules [ p_atoms, p_action ]) ], + [ [ gram_of_list (Gramext.srules [ p_atoms, hash_expr p_action, p_action ]) ], + hash_expr action, Gramext.action action ] ] | _ -> assert false and aux_variable = @@ -245,7 +253,7 @@ let compare_rule_id x y = | _,[] -> 1 | ((s1::tl1) as x),((s2::tl2) as y) -> if Gramext.eq_symbol s1 s2 then aux (tl1,tl2) - else Pervasives.compare x y + else Stdlib.compare x y in aux (x,y) @@ -356,11 +364,11 @@ let exc_located_wrapper f = try f () with - | Stdpp.Exc_located (floc, Stream.Error msg) -> + | Ploc.Exc (floc, Stream.Error msg) -> raise (HExtlib.Localized (floc, Parse_error msg)) - | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) -> + | Ploc.Exc (floc, HExtlib.Localized (_,exn)) -> raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) - | Stdpp.Exc_located (floc, exn) -> + | Ploc.Exc (floc, exn) -> raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) let parse_level1_pattern grammars precedence lexbuf = @@ -383,7 +391,7 @@ let initialize_grammars grammars = in (* Needed since campl4 on "delete_rule" remove the precedence level if it gets * empty after the deletion. The lexer never generate the Stoken below. *) - let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], dummy_action ] in + let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], "DUMMY", dummy_action ] in let mk_level_list first last = let rec aux acc = function | i when i < first -> acc @@ -556,10 +564,11 @@ END let level2_ast = grammars.level2_ast in let term = grammars.term 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; level2_ast: [ [ p = term -> p ] ]; sort: [ [ "Prop" -> `Prop @@ -614,7 +623,8 @@ EXTEND ]; arg: [ [ LPAREN; names = LIST1 IDENT SEP SYMBOL ","; - SYMBOL ":"; ty = term; RPAREN -> + typ = OPT [ SYMBOL ":"; typ = term -> typ] ; RPAREN -> (* FG: now type is optional *) + let ty = match typ with Some ty -> ty | None -> Ast.Implicit `JustOne in List.map (fun n -> Ast.Ident (n, None)) names, Some ty | name = IDENT -> [Ast.Ident (name, None)], None | blob = UNPARSED_META -> @@ -655,7 +665,8 @@ EXTEND args = LIST1 arg; index_name = OPT [ "on"; id = single_arg -> id ]; ty = OPT [ SYMBOL ":" ; p = term -> p ]; - SYMBOL <:unicode> (* ≝ *); body = term -> + opt_body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in let rec position_of name p = function | [] -> None, p | n :: _ when n = name -> Some p, p @@ -663,8 +674,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 @@ -686,6 +699,24 @@ EXTEND defs ] ]; + let_codefs: [ + [ defs = LIST1 [ + name = single_arg; + args = LIST0 arg; + ty = OPT [ SYMBOL ":" ; p = term -> p ]; + opt_body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in + let args = + List.concat + (List.map + (function (names,ty) -> List.map (function x -> x,ty) names + ) args) + in + args, (name, ty), body, 0 + ] SEP "and" -> + defs + ] + ]; binder_vars: [ [ vars = [ l = [ l = LIST1 single_arg SEP SYMBOL "," -> l @@ -715,12 +746,6 @@ EXTEND SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (Ast.LetIn (var, p1, p2)) - | LETCOREC; defs = let_defs; "in"; - body = term -> - return_term loc (Ast.LetRec (`CoInductive, defs, body)) - | LETREC; defs = let_defs; "in"; - body = term -> - return_term loc (Ast.LetRec (`Inductive, defs, body)) ] ]; term: LEVEL "20" @@ -795,6 +820,7 @@ let initial_grammars keywords = 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 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 @@ -803,6 +829,7 @@ let initial_grammars keywords = term=term; ident=ident; let_defs=let_defs; + let_codefs=let_codefs; protected_binder_vars=protected_binder_vars; level2_meta=level2_meta; level2_ast_grammar=level2_ast_grammar; @@ -814,7 +841,7 @@ class type g_status = method notation_parser_db: db end -class status ~keywords:kwds = +class status0 ~keywords:kwds = object val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] } method notation_parser_db = db @@ -824,6 +851,12 @@ class status ~keywords:kwds = = 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) = @@ -836,6 +869,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action = [ None, Some (*Gramext.NonA*) Gramext.NonA, [ p_atoms, + hash_expr "(make_action (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc)) p_bindings)", (make_action (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc)) @@ -848,7 +882,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action = 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 status ~keywords) 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 @@ -866,6 +900,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