Stefan pushed to branch graveline at Stefan / Typer
Commits: c39bd687 by Stefan Monnier at 2018-07-12T16:17:12Z * src/sexp.ml (sexp_parse_all): Fail more gracefully when encountering a stray closing token.
- - - - - abf28d5c by Stefan Monnier at 2018-07-18T17:27:27Z Be more careful about which grammar to use while parsing
* src/REPL.ml (_ieval, _raw_eval): Use grammar from ctx. Rename arg to `ectx`. * src/debug_util.ml (format_source, main): Use grammar from pervasive.
- - - - - ec47c030 by Jonathan Graveline at 2018-07-18T20:13:11Z Run macros in the IO monad
* btl/builtins.typer (Macro, Macro_expand): Return type is now `IO Sexp`.
* btl/pervasive.typer (multiarg_lambda, quote, __.__): Adjust accordingly.
* src/debruijn.ml (senv_lookup): No need to be recursive.
* src/elab.ml (get_implicit_arg, elab_macro_call, lexp_decls_macro): Macros are now run in the IO monad. (sexp_decls_macro_print): Comment out.
* src/opslexp.ml (ctx2tup.mk_lets_and_tup): Fix debindex.
* tests/eval_test.ml (test_eval_eqv_named): Don't burp on empty lists. ("Implicit Arguments"): Adjust to new type. ("Generic-typed case"): Use our own `Pair` type.
* tests/macro_test.ml ("macros base", "macros decls"): Adjust to new type.
- - - - - c7d2bbfe by Stefan Monnier at 2018-07-18T21:01:03Z Merge branch 'trunk' into graveline
- - - - -
8 changed files:
- btl/builtins.typer - btl/pervasive.typer - src/REPL.ml - src/debug_util.ml - src/elab.ml - src/sexp.ml - tests/eval_test.ml - tests/macro_test.ml
Changes:
===================================== btl/builtins.typer ===================================== @@ -1,6 +1,6 @@ %%% builtins.typer --- Initialize the builtin functions
-%% Copyright (C) 2011-2017 Free Software Foundation, Inc. +%% Copyright (C) 2011-2018 Free Software Foundation, Inc. %% %% Author: Pierre Delaunay pierre.delaunay@hec.ca %% Keywords: languages, lisp, dependent types.
===================================== btl/pervasive.typer ===================================== @@ -1,6 +1,6 @@ %%% pervasive --- Always available definitions
-%% Copyright (C) 2011-2017 Free Software Foundation, Inc. +%% Copyright (C) 2011-2018 Free Software Foundation, Inc. %% %% Author: Pierre Delaunay pierre.delaunay@hec.ca %% Keywords: languages, lisp, dependent types. @@ -121,25 +121,23 @@ multiarg_lambda = let sym = (Sexp_symbol name); mklambda = lambda arg -> lambda body -> Sexp_node sym (cons arg (cons body nil)) in - lambda (margs : List Sexp) -> case margs - | nil => Sexp_error - | cons fargs margstail - => case margstail - | nil => Sexp_error - | cons body bodytail - => case bodytail - | cons _ _ => Sexp_error - | nil => List_foldr mklambda - (Sexp_to_list fargs exceptions) - body; - -return_multiarg_lambda : String -> List Sexp -> IO Sexp; -return_multiarg_lambda = lambda name -> - lambda args -> IO_return (multiarg_lambda name args); - -lambda_->_ = macro (return_multiarg_lambda "##lambda_->_"); -lambda_=>_ = macro (return_multiarg_lambda "##lambda_=>_"); -lambda_≡>_ = macro (return_multiarg_lambda "##lambda_≡>_"); + lambda (margs : List Sexp) + -> IO_return + case margs + | nil => Sexp_error + | cons fargs margstail + => case margstail + | nil => Sexp_error + | cons body bodytail + => case bodytail + | cons _ _ => Sexp_error + | nil => List_foldr mklambda + (Sexp_to_list fargs exceptions) + body; + +lambda_->_ = macro (multiarg_lambda "##lambda_->_"); +lambda_=>_ = macro (multiarg_lambda "##lambda_=>_"); +lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_");
%%%% More list functions
@@ -331,14 +329,11 @@ type-impl = lambda (x : List Sexp) -> in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil)
%% return decls - in chain-decl3 type-decl % type as a function declaration - decl % inductive type declaration - ctors; % constructor declarations + in IO_return (chain-decl3 type-decl % type as a function declaration + decl % inductive type declaration + ctors); % constructor declarations
-return_type_impl : List Sexp -> IO Sexp; -return_type_impl = lambda args -> IO_return (type-impl args); - -type_ = macro return_type_impl; +type_ = macro type-impl;
%%%% Backward compatibility
@@ -388,12 +383,13 @@ __.__ = (cons o (cons branch nil))) nil) in macro (lambda args - -> case args - | cons o tail - => (case tail - | cons f _ => IO_return (mksel o f) - | nil => IO_return Sexp_error) - | nil => IO_return Sexp_error); + -> IO_return + case args + | cons o tail + => (case tail + | cons f _ => mksel o f + | nil => Sexp_error) + | nil => Sexp_error);
%%%% Logic
@@ -430,8 +426,8 @@ if_then_else_ e2 = List_nth 1 args Sexp_error; e3 = List_nth 2 args Sexp_error; in IO_return (quote (case uquote e1 - | true => uquote e2 - | false => uquote e3))); + | true => uquote e2 + | false => uquote e3)));
%%%% Test test1 : ?;
===================================== src/REPL.ml ===================================== @@ -1,6 +1,6 @@ (* REPL.ml --- Read Eval Print Loop (REPL)
-Copyright (C) 2016-2017 Free Software Foundation, Inc. +Copyright (C) 2016-2018 Free Software Foundation, Inc.
Author: Pierre Delaunay pierre.delaunay@hec.ca
@@ -142,25 +142,25 @@ let ieval lexps rctx = let vals = eval_all lexprs rctx false in vals, rctx
-let _ieval f str lctx rctx = +let _ieval f str ectx rctx = let pres = (f str) in let sxps = lex default_stt pres in (* FIXME: This is too eager: it prevents one declaration from changing * the grammar used in subsequent declarations. *) - let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in + let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in
(* Different from usual typer *) let pxps = ipexp_parse nods in - let lxps, lctx = ilexp_parse pxps lctx in + let lxps, ectx = ilexp_parse pxps ectx in let elxps = ierase_type lxps in let v, rctx = ieval elxps rctx in - v, lctx, rctx + v, ectx, rctx
-let _raw_eval f str lctx rctx = +let _raw_eval f str ectx rctx = let pres = (f str) in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in - let lxps, lctx = Elab.lexp_p_decls nods lctx in + let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in + let lxps, ectx = Elab.lexp_p_decls nods ectx in let elxps = List.map OL.clean_decls lxps in (* At this point, `elxps` is a `(vname * elexp) list list`, where: * - each `(vname * elexp)` is a definition @@ -170,7 +170,7 @@ let _raw_eval f str lctx rctx = * blocs of mutually-recursive definitions. *) let rctx = eval_decls_toplevel elxps rctx in (* This is for consistency with ieval *) - [], lctx, rctx + [], ectx, rctx
let ieval_string = _ieval prelex_string let ieval_file = _ieval prelex_file
===================================== src/debug_util.ml ===================================== @@ -193,7 +193,8 @@ let format_source () = let filename = List.hd (!arg_files) in let pretoks = prelex_file filename in let toks = lex default_stt pretoks in - let nodes = sexp_parse_all_to_list default_grammar toks (Some ";") in + let nodes = sexp_parse_all_to_list (ectx_to_grm Elab.default_ectx) + toks (Some ";") in let ctx = Elab.default_ectx in let lexps, _ = Elab.lexp_p_decls nodes ctx in
@@ -253,7 +254,8 @@ let main () =
(* get node sexp *) print_string yellow; - let nodes = sexp_parse_all_to_list default_grammar toks (Some ";") in + let nodes = sexp_parse_all_to_list (ectx_to_grm Elab.default_ectx) + toks (Some ";") in print_string reset;
(if (get_p_option "sexp") then(
===================================== src/elab.ml ===================================== @@ -479,10 +479,11 @@ and get_implicit_arg ctx loc oname t =
(* get the sexp returned by the macro *) let lsarg = match v with - | Vcommand cmd -> ( match (cmd ()) with - | Vsexp (sexp) -> sexp - | _ -> value_fatal loc v "default attribute should return a IO Sexp" ) - | _ -> value_fatal loc v "default attribute should return a IO Sexp" in + | Vcommand cmd + -> (match cmd () with + | Vsexp (sexp) -> sexp + | _ -> value_fatal loc v "default attribute should return a IO Sexp" ) + | _ -> value_fatal loc v "default attribute should return an IO" in
(* Elaborate the argument *) check lsarg t ctx @@ -746,12 +747,13 @@ and elab_macro_call ctx func args ot = | Some t -> t in let sxp = match lexp_expand_macro (lexp_location func) func args ctx (Some t) with - | Vcommand f -> (match (f ()) with - | Vsexp (sxp) -> sxp - | v -> value_fatal (lexp_location func) v - "Macros should return a IO Sexp") + | Vcommand cmd + -> (match cmd () with + | Vsexp (sxp) -> sxp + | v -> value_fatal (lexp_location func) v + "Macros should return a IO Sexp") | v -> value_fatal (lexp_location func) v - "Macros should return a IO Sexp" in + "Macros should return an IO" in elaborate ctx sxp ot
(* Identify Call Type and return processed call. *) @@ -922,29 +924,26 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) macro_expand args
(* Print each generated decls *) -and sexp_decls_macro_print sxp_decls = - match sxp_decls with - | Node (Symbol (_, "_;_"), decls) -> - List.iter (fun sxp -> sexp_decls_macro_print sxp) decls - | e -> sexp_print e; print_string "\n" +(* and sexp_decls_macro_print sxp_decls = + * match sxp_decls with + * | Node (Symbol (_, "_;_"), decls) -> + * List.iter (fun sxp -> sexp_decls_macro_print sxp) decls + * | e -> sexp_print e; print_string "\n" *)
and lexp_decls_macro (loc, mname) sargs ctx: sexp = - try let lxp, ltp = infer (Symbol (loc, mname)) ctx in + try let lxp, ltp = infer (Symbol (loc, mname)) ctx in
(* FIXME: Check that (conv_p ltp Macro)! *) let ret = lexp_expand_macro loc lxp sargs ctx None in match ret with - | Vcommand f -> (match (f ()) with - | Vsexp (sexp) -> sexp - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a IO sexp")) - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a IO sexp") - - with e -> - let relateds = get_related_name mname ctx in - let msg = if ((List.length relateds) > 0) then - ". Did you mean:" ^ (print_related relateds (ectx_to_lctx ctx)) - else "" in - fatal loc ("Macro `" ^ mname ^ "`not found" ^ msg) + | Vcommand cmd + -> (match (cmd ()) with + | Vsexp (sexp) -> sexp + | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a IO sexp")) + | _ -> fatal loc ("Macro `" ^ mname ^ "` should return an IO") + + with e -> + fatal loc ("Macro `" ^ mname ^ "` not found")
and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *)
===================================== src/sexp.ml ===================================== @@ -1,6 +1,6 @@ (* sexp.ml --- The Lisp-style Sexp abstract syntax tree.
-Copyright (C) 2011-2017 Free Software Foundation, Inc. +Copyright (C) 2011-2018 Free Software Foundation, Inc.
Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -209,7 +209,10 @@ let sexp_parse_all grm tokens limit : sexp * token list = | _ -> (internal_error "Didn't find a toplevel") in match rest with | [] -> (se,rest) - | Symbol (_,t) :: rest when Some t = limit -> (se,rest) + | Symbol (l,t) :: rest + -> if not (Some t = limit) + then sexp_error l ("Stray closing token: "" ^ t ^ """); + (se,rest) | _ -> (internal_error "Stopped parsing before the end!")
(* "sexp_p" is for "parsing" and "sexp_u" is for "unparsing". *)
===================================== tests/eval_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -56,16 +56,10 @@ let test_eval_eqv_named name decl run res = then success () else ( (* List.hd was throwing when run or res failed to compile *) - (if (List.length erun >= 1) - then - value_print (List.hd erun) - else - print_string ("no run expression\n")); - (if (List.length eres >= 1) - then - value_print (List.hd eres) - else - print_string ("no result expression\n")); + (match erun with x::_ -> value_print x + | _ -> print_string ("no run expression\n")); + (match eres with x::_ -> value_print x + | _ -> print_string ("no result expression\n")); failure ()))
let test_eval_eqv decl run res = test_eval_eqv_named run decl run res @@ -385,8 +379,10 @@ let _ = test_eval_eqv_named
PairTest = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b));
- ptest : PairTest Int String; - ptest = (##datacons PairTest cons) (x := 4) (y := "hello"); + Pair = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b)); + + ptest : Pair Int String; + ptest = (##datacons Pair cons) (x := 4) (y := "hello");
px = case ptest | (##datacons ? cons) (x := v) => v;
===================================== tests/macro_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -48,14 +48,11 @@ let _ = (add_test "MACROS" "macros base" (fun () -> my_fun = lambda (x : List Sexp) -> let hd = (case x | cons hd tl => hd - | nil => Sexp_symbol "x") : Sexp in - (Sexp_node (Sexp_symbol "_*_") - (cons hd (cons hd nil))); - - return_my_fun : List Sexp -> IO Sexp; - return_my_fun = (lambda args -> IO_return (my_fun args)); - - sqr = macro return_my_fun; + | nil => Sexp_symbol "x") : Sexp + in IO_return (Sexp_node (Sexp_symbol "_*_") + (cons hd (cons hd nil))); + + sqr = macro my_fun; " in
let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in @@ -81,12 +78,9 @@ let _ = (add_test "MACROS" "macros decls" (fun () ->
let d1 = make-decl "a" 1 in let d2 = make-decl "b" 2 in - chain-decl d1 d2; - - return_decls_impl : List Sexp -> IO Sexp; - return_decls_impl = (lambda args -> IO_return (decls-impl args)); + IO_return (chain-decl d1 d2);
- my-decls = macro return_decls_impl; + my-decls = macro decls-impl;
my-decls Nat;" in
View it on GitLab: https://gitlab.com/monnier/typer/compare/8182186174a37249b5f2671e09aead3e00d...
Afficher les réponses par date