diff options
| author | Gabriel Kerneis | 2013-11-12 16:01:52 +0000 |
|---|---|---|
| committer | Gabriel Kerneis | 2013-11-12 16:09:41 +0000 |
| commit | f2717777c8c1159511c6af70c22338d243ea6d68 (patch) | |
| tree | 34d959c5c2313060a811a702d945261c6072d657 /src | |
| parent | 4e005a7065f88fb2ba4888c51dc8c0508d867e3f (diff) | |
Define and test addition in library
Notice the need for double parentheses in test/test3.sail, because the
interpreter does not perform curryfication automatically (only the first
parameter in kept with List_extra.head):
add ((1, 3)) (* works *)
add (1, 3) (* fails, equivalent to: add (1) *)
Fortunately enough, infix functions work correctly by default. A dirty
quickfix would be easy, but I'm not sure at which level this should be
addressed properly (interpreter? typing? etc.).
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 7 | ||||
| -rw-r--r-- | src/test/test3.sail | 6 |
2 files changed, 7 insertions, 6 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 192cd641..4873149e 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -1,8 +1,9 @@ -open import Interp ;; +open import Interp +open import Interp_ast import Maybe_extra +open import Num -let add v = v ;; - +let add (V_tuple [V_lit(L_num x); V_lit(L_num y)]) = V_lit(L_num (x+y)) ;; let function_map = [ ("add", add); diff --git a/src/test/test3.sail b/src/test/test3.sail index 3127db28..8d0d9056 100644 --- a/src/test/test3.sail +++ b/src/test/test3.sail @@ -7,8 +7,8 @@ val ( nat -> nat effect { wmem , rmem } ) MEM_GPU val ( ( nat * nat ) -> nat effect { wmem , rmem } ) MEM_SIZE (* extern functions *) -val extern ( nat -> nat pure ) add = "add" -val extern ( nat -> nat pure ) (: + ) = "add_infix" (* infix plus *) +val extern ( ( nat * nat ) -> nat pure ) add = "add" +val extern ( ( nat * nat ) -> nat pure ) (: + ) = "add_infix" (* infix plus *) function nat (: * ) ( < nat > x, < nat > y ) = 42 @@ -36,5 +36,5 @@ function nat main _ = { (* extern calls *) 3 + 39; - add(5); + add((5, 37)); } |