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...