Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: 56e7649d by Jonathan Graveline at 2018-06-15T22:47:16Z New built-in gensym, changed macro signature to return IO Sexp

- - - - -

11 changed files:

- btl/builtins.typer - btl/pervasive.typer - samples/bool.typer - samples/case.typer - samples/do.typer - samples/error.typer - samples/list.typer - samples/myers.typer - src/elab.ml - src/eval.ml - tests/macro_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -155,7 +155,7 @@ String_sub = Built-in "String.sub" : String -> Int -> Int -> String;

Sexp_eq = Built-in "Sexp.=" : Sexp -> Sexp -> Bool;

-Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> Sexp; +Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp;

%% ----------------------------------------------------- %% List @@ -180,10 +180,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;

@@ -238,4 +238,8 @@ Ref_make = Built-in "Ref.make" : (a : Type) ≡> a -> IO (Ref a); Ref_read = Built-in "Ref.read" : (a : Type) ≡> Ref a -> IO a; Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit;

+%% gensym for macro + +gensym = Built-in "gensym" : Unit -> IO Sexp; + %%% builtins.typer ends here.

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -133,9 +133,13 @@ multiarg_lambda = (Sexp_to_list fargs exceptions) body;

-lambda_->_ = macro (multiarg_lambda "##lambda_->_"); -lambda_=>_ = macro (multiarg_lambda "##lambda_=>_"); -lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_"); +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_≡>_");

%%%% More list functions

@@ -196,7 +200,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

@@ -297,7 +301,10 @@ type-impl = lambda (x : List Sexp) -> ctors; % constructor declarations

-type_ = macro type-impl; +return_type_impl : List Sexp -> IO Sexp; +return_type_impl = lambda args -> IO_return (type-impl args); + +type_ = macro return_type_impl;

%%%% Backward compatibility

@@ -349,9 +356,9 @@ __.__ = -> case args | cons o tail => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error); + | cons f _ => IO_return (mksel o f) + | nil => IO_return Sexp_error) + | nil => IO_return Sexp_error);

%%%% Logic

@@ -387,9 +394,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 + in IO_return (quote (case uquote e1 | true => uquote e2 - | false => uquote e3)); + | false => uquote e3)));

%%%% Test test1 : ?;

===================================== samples/bool.typer ===================================== --- a/samples/bool.typer +++ b/samples/bool.typer @@ -19,9 +19,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 + in IO_return (quote (case uquote e1 | true => uquote e2 - | false => uquote e3)); + | false => uquote e3)));

%% FIXME: Type annotations should not be needed below. not : t -> t;

===================================== samples/case.typer ===================================== --- a/samples/case.typer +++ b/samples/case.typer @@ -53,10 +53,18 @@ mapi f i xs = case xs | nil => nil | cons x xs => cons (f x i) (mapi f (i + 1) xs);

-get_num_vars : List Sexp -> String -> List Sexp; -get_num_vars vars s = mapi - (lambda _ i -> Sexp_symbol (String_concat s (Int->String i))) - 0 vars; +io_list : List (IO ?a) -> IO (List ?a); +io_list l = IO_bind (List_foldl + (lambda o v -> IO_bind o + (lambda o -> IO_bind v + (lambda v -> IO_return (cons v o)))) + (IO_return nil) l) + (lambda l -> IO_return (List_reverse l nil)); + +get_num_vars : List Sexp -> IO (List Sexp); +get_num_vars vars = io_list (List_map + (lambda _ -> gensym ()) + vars);

%% %% Get pattern to match @@ -88,12 +96,11 @@ get_cases sexps = let in helper sexps;

%% -%% Rename nth constructor inside ctor to "s" -%% (I will need gensym here or from the calling function) +%% Rename nth constructor inside ctor to sym %%

-rename_nth : Int -> Sexp -> Sexp; -rename_nth n ctor = let +rename_nth : Int -> Sexp -> Sexp -> IO Sexp; +rename_nth n ctor sym = let

mapiif : (Sexp -> Int -> Sexp) -> (Sexp -> Bool) -> Int -> List Sexp -> List Sexp; mapiif f b i xs = case xs @@ -123,25 +130,26 @@ rename_nth n ctor = let sub_ctor : Sexp -> Int -> Sexp; sub_ctor ctor i = Sexp_dispatch ctor (lambda s ss -> if_then_else_ (Int_eq i n) - (Sexp_symbol "s") + (sym) (Sexp_symbol "_")) (lambda s -> Sexp_symbol s) err err err err ;

-in Sexp_dispatch ctor +in IO_return (Sexp_dispatch ctor (lambda s ss -> Sexp_node s (mapiif sub_ctor is_ctor 0 ss)) (lambda s -> Sexp_symbol s) - err err err err ; + err err err err);

%% %% Expand sub pattern into sub_test %%

-expand_cases : List Pattern -> List Pattern; +expand_cases : List Pattern -> IO (List Pattern); expand_cases pats = let

- foldi : (Sexp -> Int -> List VarTest -> List VarTest) -> Int -> List VarTest -> List Sexp -> List VarTest; + foldi : (Sexp -> Int -> ?a -> ?a) + -> Int -> ?a -> List Sexp -> ?a; foldi f i o xs = case xs | nil => o | cons x xs => foldi f (i + 1) (f x i o) xs; @@ -171,27 +179,34 @@ expand_cases pats = let

in Sexp_dispatch ctor (lambda s ss -> helper ss) - (no_pattern nil) (no_pattern nil) (no_pattern nil) (no_pattern nil) (no_pattern nil); + (no_pattern nil) (no_pattern nil) + (no_pattern nil) (no_pattern nil) (no_pattern nil);

- expand_one : List VarTest -> VarTest -> List VarTest; + expand_one : IO (List VarTest) -> VarTest -> IO (List VarTest); expand_one all test = case test - | push_var n => (List_concat all (cons (push_var n) nil)) + | push_var n => IO_bind all (lambda all -> + IO_return (List_concat all (cons (push_var n) nil))) | _ => (let

- expand : VarTest -> List VarTest; + expand : VarTest -> IO (List VarTest); expand test = let

+ not_unique_sym : Sexp; + not_unique_sym = Sexp_symbol " %not gensym% "; + t : Sexp; t = case test | (var_test t) => t | (sub_test _ t) => t | _ => Sexp_error;

- renamed : Int -> VarTest; + renamed : Int -> IO VarTest; renamed i = case test - | (var_test t) => (var_test (rename_nth i t)) - | (sub_test v t) => (sub_test v (rename_nth i t)) - | _ => (var_test Sexp_error); + | (var_test t) => IO_bind (rename_nth i t not_unique_sym) + (lambda t -> IO_return (var_test t)) + | (sub_test v t) => IO_bind (rename_nth i t not_unique_sym) + (lambda t -> IO_return (sub_test v t)) + | _ => IO_return (var_test Sexp_error);

sub_pattern : List Sexp; sub_pattern = List_reverse (get_sub_pattern t) nil; @@ -199,35 +214,43 @@ expand_cases pats = let nb_pattern : Int; nb_pattern = List_length sub_pattern;

- sub_case : List VarTest; - sub_case = (cons (push_var nb_pattern) - (foldi - (lambda c i o -> - (List_concat o - (cons (renamed i) (cons (sub_test (Sexp_symbol "s") c) nil)))) - 0 nil sub_pattern)); + sub_case : IO (List VarTest); + sub_case = let + + helper : Sexp -> VarTest -> List VarTest -> IO (List VarTest); + helper c r o = IO_return (List_concat o + (cons r (cons (sub_test not_unique_sym c) nil))); + + in IO_bind (foldi + (lambda c i o -> IO_bind o (lambda o -> (IO_bind (renamed i) + (lambda r -> (helper c r o))))) + 0 (IO_return nil) sub_pattern) + (lambda l -> IO_return (cons (push_var nb_pattern) l));

in if_then_else_ (Int_eq nb_pattern 0) - (List_concat all (cons test nil)) - (List_concat all sub_case) + (IO_bind all (lambda all -> + IO_return (List_concat all (cons test nil)))) + (IO_bind sub_case (lambda l -> IO_bind all + (lambda all -> IO_return (List_concat all l))))

in expand test); % (List_concat all (cons test nil));

- expand_all : Pattern -> Pattern; + expand_all : Pattern -> IO Pattern; expand_all p = case p - | (dflt_branch _) => p + | (dflt_branch _) => IO_return p | (branch cs f) => (let

- ctors : List VarTest; - ctors = (List_foldl expand_one nil cs); + ctors : IO (List VarTest); + ctors = (List_foldl expand_one (IO_return nil) cs);

- in if_then_else_ (Int_eq (List_length cs) (List_length ctors)) - (branch ctors f) - (expand_all (branch ctors f))); + in IO_bind ctors (lambda ctors -> + if_then_else_ (Int_eq (List_length cs) (List_length ctors)) + (IO_return (branch ctors f)) + (expand_all (branch ctors f))));

-in List_map expand_all pats; +in io_list (List_map expand_all pats);

-pattern_to_sexp : List Sexp -> List Pattern -> Sexp; +pattern_to_sexp : List Sexp -> List Pattern -> IO Sexp; pattern_to_sexp vars pats = let

vars_wrap : List Sexp -> Sexp -> List Sexp -> Sexp; @@ -307,17 +330,23 @@ pattern_to_sexp vars pats = let last_test_fun vars pat = (quote (lambda (_ : Unit) -> (uquote (last_to_sexp vars pat))));

+ fail_sym : Sexp; + fail_sym = Sexp_symbol " %fail sym% "; + helper : List Sexp -> List Pattern -> Sexp; helper vars pats = case pats | (cons p pats) => (case pats - | (cons _ _) => (quote (let - (uquote (Sexp_symbol " fail sym ")) - = (uquote (helper vars pats)); - in (uquote (test_fun vars p (Sexp_symbol " fail sym "))))) + | (cons _ _) => Sexp_node (Sexp_symbol "let_in_") + (cons (Sexp_node (Sexp_symbol "_;_") + (cons (Sexp_node (Sexp_symbol "_=_") (cons fail_sym + (cons (helper vars pats) nil))) nil)) + (cons (test_fun vars p fail_sym) nil)) + %(quote (let_in_ (_;_ (_=_ (uquote fail_sym) (uquote (helper vars pats)))) + %(uquote (test_fun vars p fail_sym)))) | nil => (last_test_fun vars p)) | nil => Sexp_error;

-in (quote ((uquote (helper vars pats)) ())); +in IO_return (quote ((uquote (helper vars pats)) ()));

%% %% The macro we want. @@ -325,12 +354,12 @@ in (quote ((uquote (helper vars pats)) ()));

case_ = macro (lambda args -> let

- foldi : (Sexp -> Int -> Sexp -> Sexp) -> Int -> Sexp -> List Sexp -> Sexp; + foldi : (?a -> Int -> ?b -> ?b) -> Int -> ?b -> List ?a -> ?b; foldi f i o xs = case xs | nil => o | cons x xs => foldi f (i + 1) (f x i o) xs;

- case0_ : List Sexp -> Sexp; + case0_ : List Sexp -> IO Sexp; case0_ args = let

vars : List Sexp; @@ -343,29 +372,47 @@ case_ = macro (lambda args -> let | (cons s ss) => get_cases ss | nil => nil;

- num_vars : List Sexp; - num_vars = get_num_vars vars " sym no "; + num_vars : IO (List Sexp); + num_vars = get_num_vars vars; + + free_vars : IO (List Sexp); + free_vars = get_num_vars vars;

- vars_wrap : Sexp -> Sexp; - vars_wrap fun = (Sexp_node (foldi - (lambda v i fun -> (quote (lambda_->_ - ((uquote (List_nth i num_vars Sexp_error)) : (decltype (uquote v))) - (uquote fun)))) - 0 fun ( vars ) - ) (List_reverse vars nil)); + vars_wrap : List Sexp -> List Sexp -> Sexp -> IO Sexp; + vars_wrap fvars nvars fun = let + + rvars : List Sexp; + rvars = List_reverse vars nil; + + nfun : Sexp; + nfun = (Sexp_node (foldi + (lambda v i fun -> (quote (lambda_->_ + ((uquote (List_nth i nvars Sexp_error)) : (decltype (uquote v))) + (uquote fun)))) + 0 fun fvars) (List_reverse fvars nil)); + + in IO_return ( (foldi + (lambda v i fun -> (quote ( + let (uquote (List_nth i fvars Sexp_error)) = (uquote v); in (uquote fun)))) + 0 nfun vars)); + % in IO_return nfun;

- in vars_wrap (pattern_to_sexp num_vars (expand_cases pats)); + in IO_bind (expand_cases pats) (lambda pats -> + (IO_bind num_vars (lambda num_vars -> + IO_bind free_vars (lambda free_vars -> + IO_bind (pattern_to_sexp num_vars pats) (lambda f -> + vars_wrap free_vars num_vars f)))));

% Only the Sexp after "_|_" are interesting

- case1_ : List Sexp -> Sexp; + case1_ : List Sexp -> IO Sexp; case1_ args = case args | (cons s ss) => if_then_else_ (Sexp_eq (Sexp_symbol "_|_") s) (case0_ ss) - (Sexp_error) - | nil => Sexp_error; + (IO_return Sexp_error) + | nil => IO_return Sexp_error;

- err = (lambda _ -> Sexp_error); + err = (lambda _ -> IO_return Sexp_error);

% Expecting only one Sexp_node containing a case with arguments

===================================== samples/do.typer ===================================== --- a/samples/do.typer +++ b/samples/do.typer @@ -100,7 +100,7 @@ in helper (Sexp_symbol "") args; % return Unit if no command given %% Serie of command

action = macro (lambda args -> - (set-fun (get-decl args)) + (IO_return (set-fun (get-decl args))) );

%% Next are example command

===================================== samples/error.typer ===================================== --- a/samples/error.typer +++ b/samples/error.typer @@ -73,7 +73,7 @@ fun2 n = case n

% h = fun2 1 2;

-% [X] Fatal [Ln 6, cl 6] LPARSE macro expects `(List Sexp) -> Sexp` +% [X] Fatal [Ln 6, cl 6] LPARSE macro expects `(List Sexp) -> IO Sexp` % > Vcons: (cons 2 (nil)) % > Root: n

===================================== samples/list.typer ===================================== --- a/samples/list.typer +++ b/samples/list.typer @@ -44,6 +44,22 @@ map f = lambda xs -> case xs | nil => nil | cons x xs => cons (f x) (map f xs);

+mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> t a -> t b; +mapi f xs = let + helper : (a -> Int -> b) -> Int -> t a -> t b; + helper f i xs = case xs + | nil => nil + | cons x xs => cons (f x i) (helper f (i + 1) xs); +in helper f 0 xs; + +foldli : (a : Type) ≡> (b : Type) ≡> (a -> b -> Int -> a) -> a -> t b -> a; +foldli f o xs = let + helper : (a -> b -> Int -> a) -> Int -> a -> t b -> a; + helper f i o xs = case xs + | nil => o + | cons x xs => helper f (i + 1) (f o x i) xs; +in helper f 0 o xs; + foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> t b -> a -> a; foldr f = lambda xs -> lambda i -> case xs | nil => i

===================================== samples/myers.typer ===================================== --- a/samples/myers.typer +++ b/samples/myers.typer @@ -1,8 +1,8 @@ -% -% Adaptation of Myers list from ocaml file `myers.ml` -% -% since 2018-05-14 -% +%%% +%%% Adaptation of Myers list from ocaml file `myers.ml` +%%% +%%% since 2018-05-14 +%%%

%% We could replace mnil and mcons by nil and cons %% when load and list.typer are ready @@ -65,6 +65,8 @@ nth n l = car (nthcdr n l); set_nth : (a : Type) ≡> Int -> a -> t a -> t a; set_nth n v l = let

+ % I should use the new case_ macro here! + type Helper (a : Type) | pat1 (idx : Int) (data : a) (link1 : t a) (i : Int) (link2 : t a) | pat2 (idx : Int);

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -748,9 +748,12 @@ 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 f -> (match (f ()) 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 a IO Sexp" in elaborate ctx sxp ot

(* Identify Call Type and return processed call. *) @@ -937,8 +940,10 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = (* 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 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 -> fatal loc ("Macro `" ^ mname ^ "`not found")

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -317,7 +317,8 @@ let sexp_debug_print loc depth args_val = match args_val with | Float _ -> "Float" | Node _ -> "Node" ) - in print_string ("\n\t"^tstr^" : ["^(sexp_string s1)^"]\n\n"); Vsexp (s1)) + in (print_string ("\n\t"^tstr^" : ["^(sexp_string s1)^"]\n\n") + ; Vcommand (fun () -> Vsexp (s1)))) | _ -> error loc "Sexp.debug_print expects 1 sexps"

let file_open loc depth args_val = match args_val with @@ -704,7 +705,7 @@ let nop_fun loc _ vs = match vs with | _ -> error loc "Wrong number of argument to nop"

let ref_make loc depth args_val = match args_val with - | [v] -> Vcommand (fun () -> Vref (ref v)) + | [v] -> Vcommand (fun () -> print_string "\n\tIN REF_MAKE\n\n"; Vref (ref v)) | _ -> error loc "Ref.make takes a single value as argument"

let ref_read loc depth args_val = match args_val with @@ -716,6 +717,13 @@ let ref_write loc depth args_val = match args_val with Vcommand (fun () -> actual := value; Vcons ((dloc,"()"),[])) | _ -> error loc "Ref.write takes a value and a Ref as argument"

+let gensym = let count = ref 0 in + (fun loc depth args_val -> match args_val with + | [v] -> Vcommand (fun () -> ( + count := ((!count) + 1); + Vsexp (Symbol (dloc,(" %gensym% no "^(string_of_int (!count))^" "))))) + | _ -> error loc "gensym takes a Unit as argument") + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -747,6 +755,7 @@ let register_builtin_functions () = ("Ref.make" , ref_make, 1); ("Ref.read" , ref_read, 1); ("Ref.write" , ref_write, 2); + ("gensym" , gensym, 1); ] let _ = register_builtin_functions ()

===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -51,8 +51,11 @@ let _ = (add_test "MACROS" "macros base" (fun () -> | 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 my_fun; + sqr = macro return_my_fun; " in

let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in @@ -66,7 +69,6 @@ let _ = (add_test "MACROS" "macros base" (fun () -> | _ -> failure ()) )

- let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " decls-impl = lambda (x : List Sexp) -> @@ -80,8 +82,11 @@ 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));

- my-decls = macro decls-impl; + my-decls = macro return_decls_impl;

my-decls Nat;" in

View it on GitLab: https://gitlab.com/monnier/typer/commit/56e7649d252fa1205c848d22f48761f20f99...