[Git][monnier/typer][master] * btl/types.typer (sexp_dispatch_): Generalize type
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...
Afficher les réponses par date
participants (1)
-
Stefan