Stefan pushed to branch master at Stefan / Typer
Commits: 5c39f5f8 by Stefan Monnier at 2018-12-05T00:32:16Z Consolidate and rename Parser.* built-ins
* btl/builtins.typer (Parser_default, Parser_newest): Remove. (Reader_parse): Rename from Parser_custom.
* btl/do.typer (get-decl): Add `ctx` arg. Use Reader_parse. (do): Pass it Elab_getenv.
* src/eval.ml (parser_default, parser_newest): Remove. (reader_parse): Rename from parser_custom.
- - - - -
3 changed files:
- btl/builtins.typer - btl/do.typer - src/eval.ml
Changes:
===================================== btl/builtins.typer ===================================== @@ -209,25 +209,9 @@ Sexp_dispatch = Built-in "Sexp.dispatch" -> a ;
%% -%% Parse an Sexp with the default context -%% default context include builtins.typer and pervasive.typer -%% but nothing else +%% Parse a block using the grammar in the passed context %% -%% It was implemented to parse Sexp block in a macro -%% -Parser_default = Built-in "Parser.default" : Sexp -> List Sexp; - -%% -%% Same as `Parser_default` but with a custom context -%% -Parser_custom = Built-in "Parser.custom" : Elab_Context -> Sexp -> List Sexp; - -%% -%% Parse an Sexp with the latest context -%% -%% (Previous top level definition should be in the context) -%% -Parser_newest = Built-in "Parser.newest" : Sexp -> List Sexp; +Reader_parse = Built-in "Reader.parse" : Elab_Context -> Sexp -> List Sexp;
%%%% Array (without IO, but they could be added easily)
===================================== btl/do.typer ===================================== @@ -73,8 +73,8 @@ in if (Sexp_eq op (Sexp_symbol "")) then Sexp_error else op; %% Takes a block (`{...}`) %% Parse the block and returns the list of command inside the block %% -get-decl : List Sexp -> List Sexp; -get-decl args = let +get-decl : Elab_Context -> List Sexp -> List Sexp; +get-decl ctx args = let
err = lambda _ -> cons Sexp_error nil;
@@ -82,10 +82,9 @@ get-decl args = let
node = Sexp_dispatch (List_nth 0 args Sexp_error)
- (lambda _ _ -> cons Sexp_error nil) err err err err + (K err) err err err err
- %% `Parser_newest` use the most recent environment - (lambda l -> Parser_newest l); + (lambda block -> Reader_parse ctx block);
in node;
@@ -131,8 +130,8 @@ in helper (Sexp_symbol "") args; % return Unit if no command given %%
do = macro (lambda args -> - (IO_return (set-fun (get-decl args))) -); + IO_bind (Elab_getenv unit) + (lambda ctx -> IO_return (set-fun (get-decl ctx args))));
%% %% Next are example command
===================================== src/eval.ml ===================================== @@ -296,25 +296,12 @@ let make_block loc depth args_val = match args_val with | [Vstring str] -> Vsexp (Block (loc, (Prelexer.prelex_string str), loc)) | _ -> error loc "Sexp.block expects one string as argument"
-let parser_default loc depth args_val = match args_val with - | [Vsexp (Block (_,toks,_))] -> - o2v_list (sexp_parse_all_to_list default_grammar (Lexer.lex default_stt toks) (Some ";")) - | [s] -> (warning loc "Parser.default do nothing without a Block"; s) - | _ -> error loc "Parser.default expects a Block as argument" - -let parser_custom loc depth args_val = match args_val with +let reader_parse loc depth args_val = match args_val with | [Velabctx ectx; Vsexp (Block (_,toks,_))] -> let grm = ectx_get_grammar ectx in o2v_list (sexp_parse_all_to_list grm (Lexer.lex default_stt toks) (Some ";")) - | [Velabctx _; s] -> (warning loc "Parser.custom do nothing without a Block"; s) - | _ -> error loc "Parser.custom expects an ElabContext and a Block as argument" - -let parser_newest loc depth args_val = match args_val with - | [Vsexp (Block (_,toks,_))] -> - let grm = ectx_get_grammar (!macro_monad_elab_context) in - o2v_list (sexp_parse_all_to_list grm (Lexer.lex default_stt toks) (Some ";")) - | [s] -> (warning loc "Parser.newest do nothing without a Block"; s) - | _ -> error loc "Parser.newest expects a Block as argument" + | [Velabctx _; s] -> (warning loc "Reader.parse do nothing without a Block"; s) + | _ -> error loc "Reader.parse expects an ElabContext and a Block as argument"
let string_eq loc depth args_val = match args_val with | [Vstring s1; Vstring s2] -> o2v_bool (s1 = s2) @@ -994,9 +981,7 @@ let register_builtin_functions () = ("Sexp.dispatch" , sexp_dispatch, 7); ("TypeLevel.succ" , typelevel_succ, 1); ("TypeLevel.⊔" , typelevel_lub, 2); - ("Parser.default", parser_default,1); - ("Parser.custom" , parser_custom,2); - ("Parser.newest" , parser_newest,1); + ("Reader.parse" , reader_parse,2); ("String.=" , string_eq, 2); ("String.concat" , string_concat, 2); ("String.sub" , string_sub, 3);
View it on GitLab: https://gitlab.com/monnier/typer/commit/5c39f5f86c900334e4c038ccd61bf43fbf15...