Idris 2 implementation

Makefile

@@ -91,7 +91,7 @@ DOCKERIZE =
 
 IMPLS = ada ada.2 awk bash basic bbc-basic c chuck clojure coffee common-lisp cpp crystal cs d dart \
 	elisp elixir elm erlang es6 factor fantom forth fsharp go groovy gnu-smalltalk \
-	guile haskell haxe hy io java js jq julia kotlin livescript logo lua make mal \
+	guile haskell haxe hy idris2 io java js jq julia kotlin livescript logo lua make mal \
 	matlab miniMAL nasm nim objc objpascal ocaml perl perl6 php picolisp pike plpgsql \
 	plsql powershell ps python python.2 r racket rexx rpython ruby rust scala scheme skew \
 	swift swift3 swift4 swift5 tcl ts vala vb vhdl vimscript wasm wren yorick xslt zig
@@ -217,6 +217,7 @@ guile_STEP_TO_PROG =         impls/guile/$($(1)).scm
 haskell_STEP_TO_PROG =       impls/haskell/$($(1))
 haxe_STEP_TO_PROG =          $(haxe_STEP_TO_PROG_$(haxe_MODE))
 hy_STEP_TO_PROG =            impls/hy/$($(1)).hy
+idris2_STEP_TO_PROG =        impls/idris2/build/exec/$($(1))
 io_STEP_TO_PROG =            impls/io/$($(1)).io
 java_STEP_TO_PROG =          impls/java/target/classes/mal/$($(1)).class
 js_STEP_TO_PROG =            impls/js/$($(1)).js

impls/idris2/.gitignore

@@ -0,0 +1 @@
+build

impls/idris2/Class.idr

@@ -0,0 +1,88 @@
+||| Typeclasses that describe types that correspond to Mal data
+module Class
+
+import Eval
+import Types
+
+export
+interface MalType a where
+  toMalAst : a -> AST
+  fromMalAst : AST -> Maybe a
+
+export
+implementation MalType AST where
+  toMalAst = id
+  fromMalAst = Just
+
+export
+implementation MalType () where
+  toMalAst () = Symbol "nil"
+  fromMalAst (Symbol "nil") = Just ()
+  fromMalAst _ = Nothing
+
+export
+implementation MalType Integer where
+  toMalAst = Number
+  fromMalAst (Number x) = Just x
+  fromMalAst _ = Nothing
+
+export
+implementation MalType String where
+  toMalAst = Str
+  fromMalAst (Str s) = Just s
+  fromMalAst _ = Nothing
+
+export
+implementation MalType Bool where
+  toMalAst True = Symbol "true"
+  toMalAst False = Symbol "false"
+  fromMalAst (Symbol "true") = Just True
+  fromMalAst (Symbol "false") = Just False
+  -- fromMalAst (Symbol "nil") = Just False -- Maybe?
+  fromMalAst _ = Nothing
+
+export
+implementation MalType (IORef AST) where
+  toMalAst = Atom
+  fromMalAst (Atom a) = Just a
+  fromMalAst _ = Nothing
+
+export
+implementation MalType a => MalType (List a) where
+  toMalAst = List False . map toMalAst
+  fromMalAst (List _ xs) = traverse fromMalAst xs
+  fromMalAst (Symbol "nil") = Just []
+  fromMalAst _ = Nothing
+
+export
+implementation MalType (SortedMap String AST) where
+  toMalAst = Map
+  fromMalAst (Map m) = Just m
+  fromMalAst (Symbol "nil") = Just empty
+  fromMalAst _ = Nothing
+
+export
+interface MalFunction a where
+  toMalFunc : a -> List AST -> MalM AST
+
+export
+implementation MalType a => MalFunction a where
+  toMalFunc x [] = pure $ toMalAst x
+  toMalFunc _ xs = do
+    traverse eval xs -- (+ 1 2 (println "hi")) should print hi
+    throwError $ Str "Too many arguments"
+
+export
+implementation MalType a => MalFunction (MalM a) where
+  toMalFunc x [] = map toMalAst x
+  toMalFunc _ xs = do
+    traverse eval xs
+    throwError $ Str "Too many arguments"
+
+export
+implementation (MalType a, MalFunction b) => MalFunction (a -> b) where
+  toMalFunc _ [] = throwError $ Str "Too few arguments"
+  toMalFunc f (x::xs) = do
+    Just x' <- map fromMalAst $ eval x
+      | Nothing => traverse_ eval xs *> throwError (Str "Wrong argument type")
+    toMalFunc (f x') xs