Stefan pushed to branch master at Stefan / Typer

Commits: 89b8df07 by Stefan Monnier at 2016-08-28T22:58:52-04:00 * btl/types.typer (sexp_dispatch_): Generalize type

- - - - -

2 changed files:

- btl/types.typer - samples/quote.typer

Changes:

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -96,25 +96,28 @@ tail = lambda a ≡> % Macro % -----------------------------------------------------

-block_ = Built-in "block_" ((List Sexp) -> Sexp); -symbol_ = Built-in "symbol_" (String -> Sexp); -string_ = Built-in "string_" (String -> Sexp); -node_ = Built-in "node_" (Sexp -> (List Sexp) -> Sexp); -integer_ = Built-in "integer_" (Int -> Sexp); -float_ = Built-in "float_" (Float -> Sexp); +block_ = Built-in "block_" (List Sexp -> Sexp); +symbol_ = Built-in "symbol_" (String -> Sexp); +string_ = Built-in "string_" (String -> Sexp); +node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp); +integer_ = Built-in "integer_" (Int -> Sexp); +float_ = Built-in "float_" (Float -> Sexp);

% Macro : Type; -Macro = inductive_ (dMacro) (Macro_ ((List Sexp) -> Sexp)); +Macro = inductive_ (dMacro) (Macro_ (List Sexp -> Sexp)); Macro_ = inductive-cons Macro Macro_ ;

-sexp_dispatch_ = Built-in "sexp_dispatch_" (Sexp - -> (Sexp -> List Sexp -> Sexp) - -> (String -> Sexp) - -> (String -> Sexp) - -> (Int -> Sexp) - -> (Float -> Sexp) - -> (List Sexp -> Sexp) - -> Sexp); +sexp_dispatch_ = Built-in "sexp_dispatch_" ( + (a : Type) ≡> + Sexp + -> (Sexp -> List Sexp -> a) + -> (String -> a) + -> (String -> a) + -> (Int -> a) + -> (Float -> a) + -> (List Sexp -> a) + -> a + );

% ----------------------------------------------------- % Monads

===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -44,7 +44,7 @@ quote' = lambda (x : List Sexp) -> let target = head Sexp x; tl = tail Sexp x;

- rhd = sexp_dispatch_ target + rhd = sexp_dispatch_ (a := Sexp) target node symbol string integer float block;

rtl = case tl

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