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/5c39f5f86c900334e4c038ccd61bf43fbf1…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/5c39f5f86c900334e4c038ccd61bf43fbf1…
You're receiving this email because of your account on gitlab.com.
