Stefan pushed to branch master at Stefan / Typer

Commits: b2c05da9 by Stefan Monnier at 2017-03-10T21:33:38-05:00 * btl/pervasive.typer: Redefine lambda as a macro

* btl/pervasive.typer (List_foldr, List_find): New functions. (Sexp_error): Move. (Sexp_to_list, multiarg_lambda): New functions. (lambda_->_, lambda_=>_, lambda_≡>_): Redefine to add multiarg support via macros. (List_head, List_map, List_foldl): * btl/builtins.typer (Eq_comm, Macro_expand): Don't use multi-arg lambdas (yet).

- - - - -

2 changed files:

- btl/builtins.typer - btl/pervasive.typer

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -54,7 +54,7 @@ Eq_cast = Built-in "Eq.cast" %% Commutativity of equality! Eq_comm : (l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) ≡> (y : t) ≡> (p : Eq (t := t) x y) -> Eq (t := t) y x; -Eq_comm = lambda l t x y ≡> lambda p -> +Eq_comm = lambda l ≡> lambda t ≡> lambda x ≡> lambda y ≡> lambda p -> Eq_cast (f := lambda xy -> Eq (t := t) xy x) (p := p) Eq_refl; @@ -133,12 +133,12 @@ Sexp_node = Built-in "Sexp.node" (Sexp -> List Sexp -> Sexp); Sexp_integer = Built-in "Sexp.integer" (Int -> Sexp); Sexp_float = Built-in "Sexp.float" (Float -> Sexp);

-Macro = typecons (Macro) - (macro (List Sexp -> Sexp)); +Macro = typecons (Macro) + (macro (List Sexp -> Sexp)); macro = datacons Macro macro;

Macro_expand : Macro -> List Sexp -> Sexp; -Macro_expand m args = case m +Macro_expand = lambda m -> lambda args -> case m | macro f => f args;

Sexp_dispatch = Built-in "Sexp.dispatch" (

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -72,7 +72,7 @@ List_head1 = lambda a ≡> lambda xs -> case xs | cons hd tl => some hd;

List_head : (a : Type) ≡> a -> List a -> a; -List_head = lambda a ≡> lambda x xs -> case xs +List_head = lambda a ≡> lambda x -> lambda xs -> case xs | cons x _ => x | nil => x;

@@ -82,15 +82,96 @@ List_tail = lambda a ≡> lambda xs -> case xs | cons hd tl => tl;

List_map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; -List_map = lambda a b ≡> lambda f xs -> case xs +List_map = lambda a ≡> lambda b ≡> lambda f -> lambda xs -> case xs | nil => nil | cons x xs => cons (f x) (List_map f xs);

List_foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; -List_foldl = lambda a b ≡> lambda f i xs -> case xs +List_foldl = lambda a ≡> lambda b ≡> lambda f -> lambda i -> lambda xs -> case xs | nil => i | cons x xs => List_foldl f (f i x) xs;

+List_foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; +List_foldr = lambda a ≡> lambda b ≡> lambda f -> lambda xs -> lambda i -> case xs + | nil => i + | cons x xs => f x (List_foldr f xs i); + +List_find : (a : Type) ≡> (a -> Bool) -> List a -> Option a; +List_find = lambda a ≡> lambda f -> lambda xs -> case xs + | nil => none + | cons x xs => case f x | true => some x | false => List_find f xs; + +%%%% A more flexible `lambda`. + +%% An Sexp which we use to represents an error. +Sexp_error = Sexp_symbol "<error>"; + +Sexp_to_list : Sexp -> List Sexp -> List Sexp; +Sexp_to_list = lambda s -> lambda exceptions + -> let singleton = lambda (a : Type) ≡> lambda (_ : a) -> cons s nil in + Sexp_dispatch + s + (node := lambda head -> lambda tail + -> case List_find (Sexp_eq head) exceptions + | some _ => singleton () + | none => cons head tail) + (symbol := lambda s + -> case String_eq "" s + | true => nil + | false => singleton ()) + singleton singleton singleton singleton; + +multiarg_lambda = + %% let bodytail = cons body nil; + %% mklam = lambda (a : Type) ≡> lambda (_ : a) + %% -> Sexp_node (Sexp_symbol "##lambda_->_") + %% (cons arg bodytail) in + %% Sexp_dispatch + %% arg + %% (node := (lambda head -> lambda tail -> + %% Sexp_dispatch + %% head + %% (symbol := (lambda s -> case String_eq s "_:_" + %% | true -> mklam () + %% | false -> case String_eq s "_::_" + %% | true + %% -> Sexp_node (Sexp_symbol "##lambda_=>_") + %% (cons (Sexp_node + %% (Sexp_symbol "_:_") + %% tail) + %% bodytail) + %% | false -> case String_eq s "_:::_" + %% | true + %% -> Sexp_node (Sexp_symbol "##lambda_≡>_") + %% (cons (Sexp_node + %% (Sexp_symbol "_:_") + %% tail) + %% bodytail) + %% | false -> mklam ())) + %% mklam mklam mklam mklam mklam)) + %% mklam mklam mklam mklam mklam + let exceptions = List_map Sexp_symbol + (cons "_:_" (cons "_::_" (cons "_:::_" nil))) in + lambda name -> + 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_->_ = macro (multiarg_lambda "##lambda_->_"); +lambda_=>_ = macro (multiarg_lambda "##lambda_=>_"); +lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_"); + %%%% Quasi-Quote macro

%% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) @@ -99,9 +180,6 @@ List_foldl = lambda a b ≡> lambda f i xs -> case xs %% %% => x

-%% An Sexp which we use to represents an error. -Sexp_error = Sexp_symbol "<error>"; - quote1 : Sexp -> Sexp; quote1 x = let k = K x; node op y = case (Sexp_eq op (Sexp_symbol "uquote"))

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