Stefan pushed to branch master at Stefan / Typer
Commits: 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.
- - - - -
7 changed files:
- btl/builtins.typer - btl/pervasive.typer - src/debruijn.ml - src/elab.ml - src/opslexp.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. @@ -149,10 +149,10 @@ Sexp_integer = Built-in "Sexp.integer" : Integer -> Sexp; Sexp_float = Built-in "Sexp.float" : Float -> Sexp;
Macro = typecons (Macro) - (macro (List Sexp -> Sexp)); + (macro (List Sexp -> IO Sexp)); macro = datacons Macro macro;
-Macro_expand : Macro -> List Sexp -> Sexp; +Macro_expand : Macro -> List Sexp -> IO Sexp; Macro_expand = lambda m -> lambda args -> case m | macro f => f args;
===================================== 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,17 +121,19 @@ 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; + 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_=>_"); @@ -196,7 +198,7 @@ quote1 x = let k = K x; in Sexp_dispatch x node symbol k k k k;
%% quote definition -quote = macro (lambda x -> quote1 (List_head Sexp_error x)); +quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x)));
%%%% The `type` declaration macro
@@ -293,8 +295,8 @@ type-impl = lambda (x : List Sexp) -> in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil)
%% return decls - in chain-decl decl % inductive type declaration - ctors; % constructor declarations + in IO_return (chain-decl decl % inductive type declaration + ctors); % constructor declarations
type_ = macro type-impl; @@ -346,12 +348,13 @@ __.__ = (cons o (cons branch nil))) nil) in macro (lambda args - -> case args - | cons o tail - => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error); + -> IO_return + case args + | cons o tail + => (case tail + | cons f _ => mksel o f + | nil => Sexp_error) + | nil => Sexp_error);
%%%% Logic
@@ -387,9 +390,9 @@ if_then_else_ let e1 = List_nth 0 args Sexp_error; e2 = List_nth 1 args Sexp_error; e3 = List_nth 2 args Sexp_error; - in quote (case uquote e1 - | true => uquote e2 - | false => uquote e3)); + in IO_return (quote (case uquote e1 + | true => uquote e2 + | false => uquote e3)));
%%%% Test test1 : ?;
===================================== src/debruijn.ml ===================================== @@ -147,7 +147,7 @@ let empty_elab_context : elab_context (0, 0, ref SMap.empty))
(* return its current DeBruijn index *) -let rec senv_lookup (name: string) (ctx: elab_context): int = +let senv_lookup (name: string) (ctx: elab_context): int = let (_, (n, map), _, _) = ctx in n - (SMap.find name map) - 1
===================================== src/elab.ml ===================================== @@ -466,8 +466,11 @@ and get_implicit_arg ctx loc oname t =
(* get the sexp returned by the macro *) let lsarg = match v with - | Vsexp (sexp) -> sexp - | _ -> value_fatal loc v "default attribute should return a 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 @@ -731,9 +734,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 - | Vsexp (sxp) -> sxp + | 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 Sexp" in + "Macros should return an IO" in elaborate ctx sxp ot
(* Identify Call Type and return processed call. *) @@ -904,23 +911,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 - | Vsexp (sexp) -> sexp - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a sexp") + | 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") + with e -> + fatal loc ("Macro `" ^ mname ^ "` not found")
and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) @@ -1500,7 +1510,7 @@ let sform_type ctx loc sargs ot = sform_dummy_ret ctx loc
(* Only print var info *) -and lexp_print_var_info ctx = +let lexp_print_var_info ctx = let ((m, _), env, _) = ctx in let n = Myers.length env in
===================================== src/opslexp.ml ===================================== @@ -954,8 +954,8 @@ let ctx2tup ctx nctx = types) SMap.empty), cons_label), - List.map (fun (name, t) - -> (P.Aimplicit, Var (name, offset))) + List.mapi (fun i (oname, t) + -> (P.Aimplicit, Var (oname, offset - i - 1))) types) | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) -> Let (loc, [(name, mkSusp e (S.shift 1), t)],
===================================== 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. @@ -55,8 +55,11 @@ let test_eval_eqv_named name decl run res = if value_eq_list erun eres then success () else ( - value_print (List.hd erun); - value_print (List.hd eres); + (* List.hd was throwing when run or res failed to compile *) + (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 @@ -343,7 +346,8 @@ let _ = test_eval_eqv_named "Implicit Arguments"
"default = new-attribute Macro; - default = add-attribute default Int (macro (lambda (lst : List Sexp) -> Sexp_integer (Int->Integer 1))); + default = add-attribute default Int (macro (lambda (lst : List Sexp) -> + (IO_return (Sexp_integer (Int->Integer 1)))));
fun = lambda (x : Int) => lambda (y : Int) -> @@ -373,6 +377,8 @@ let _ = test_eval_eqv_named tP : Decidable P; tP = (datacons Decidable true) (prop := P) (p := p);
+ Pair = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b)); + ptest : Pair Int String; ptest = (##datacons Pair cons) (x := 4) (y := "hello");
===================================== 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,9 +48,9 @@ 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))); + | nil => Sexp_symbol "x") : Sexp + in IO_return (Sexp_node (Sexp_symbol "_*_") + (cons hd (cons hd nil)));
sqr = macro my_fun; " in @@ -79,7 +79,7 @@ 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; + IO_return (chain-decl d1 d2);
my-decls = macro decls-impl;
View it on GitLab: https://gitlab.com/monnier/typer/commit/ec47c030cbe1410db12a3665a3d5521a9cb1...
Afficher les réponses par date