Update to idris 1.2.0 and malfunction v0.2.1

.gitignore

@@ -0,0 +1,34 @@
+# haskell
+dist
+dist-*
+cabal-dev
+*.o
+*.out
+*.hi
+*.chi
+*.chs.h
+*.dyn_o
+*.dyn_hi
+.hpc
+.hsenv
+.cabal-sandbox/
+cabal.sandbox.config
+*.prof
+*.aux
+*.hp
+*.eventlog
+.stack-work/
+cabal.project.local
+cabal.project.local~
+.HTF/
+.ghc.environment.*
+
+# idris
+*.ibc
+*.lang
+
+# malfunction
+*.mlf
+
+# general
+*.log

.vscode/launch.json

@@ -0,0 +1,26 @@
+{
+    // Use IntelliSense to learn about possible attributes.
+    // Hover to view descriptions of existing attributes.
+    // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387
+    "version": "0.2.0",
+    "configurations": [
+        {
+            "type": "ghc",
+            "name": "haskell-debug-adapter",
+            "request": "launch",
+            "internalConsoleOptions": "openOnSessionStart",
+            "workspace": "${workspaceRoot}",
+            "startup": "${workspaceRoot}/src/Main.hs",
+            "startupFunc": "",
+            "startupArgs": "",
+            "stopOnEntry": true,
+            "mainArgs": "",
+            "ghciPrompt": "H>>= ",
+            "ghciInitialPrompt": "Prelude>",
+            "ghciCmd": "stack ghci --test --no-load --no-build --main-is TARGET --ghci-options -fprint-evld-with-show",
+            "ghciEnv": {},
+            "logFile": "${workspaceRoot}/.vscode/phoityne.log",
+            "logLevel": "WARNING"
+        }
+    ]
+}

.vscode/tasks.json

@@ -0,0 +1,68 @@
+{
+    // See https://go.microsoft.com/fwlink/?LinkId=733558
+    // for the documentation about the tasks.json format
+    "version": "2.0.0",
+    "tasks": [
+        {
+            "label": "stack install",
+            "type": "shell",
+            "command": "stack install",
+            "group": {
+                "kind": "build",
+                "isDefault": true
+            },
+            "presentation": {
+                "echo": true,
+                "reveal": "always",
+                "focus": true,
+            }
+        },
+        {
+            "label": "idrmlf compile",
+            "type": "shell",
+            "command": "idris ${relativeFile} --codegen malfunction -o test/${fileBasenameNoExtension}.o && test/${fileBasenameNoExtension}.o",
+            "presentation": {
+                "echo": true,
+                "reveal": "always",
+                "focus": true,
+            }
+        },{
+            "label": "idrmlf eval",
+            "type": "shell",
+            "command": "idris ${relativeFile} --codegen malfunction --interface -o test/${fileBasenameNoExtension}",
+            "presentation": {
+                "echo": true,
+                "reveal": "always",
+                "focus": true,
+            }
+        },
+        {
+            "label": "idrmlf run",
+            "type": "shell",
+            "command": "test/${fileBasenameNoExtension}.o",
+            "presentation": {
+                "echo": true,
+                "reveal": "always",
+                "focus": true,
+            }
+        },
+        {
+            "label": "malfunction compile",
+            "type": "shell",
+            "command": "malfunction compile ${relativeFile} -o test/${fileBasenameNoExtension}_1.o && test/${fileBasenameNoExtension}_1.o",
+            "presentation": {
+                "echo": true,
+                "reveal": "always",
+                "focus": true,
+            }
+        },
+        {
+            "label": "clean test",
+            "type": "shell",
+            "command": "rm test/*.ibc test/*.o test/*.lang test/*.mlf",
+            "presentation": {
+                "reveal": "never",
+            },
+        }
+    ]
+}

README.md

@@ -1,19 +1,28 @@
 # Idris backend for Malfunction
 
-Compiles Idris to [Malfunction](https://github.com/stedolan/malfunction)
+Compiles Idris to [Malfunction](https://github.com/stedolan/malfunction).
 
 It seems to go pretty fast:
-
+    
     $ idris pythag.idr -o pythag-idris
     $ idris pythag.idr --codegen malfunction -o pythag-malfunction
+
     $ time ./pythag-idris  > /dev/null
+
+    real    0m4.548s
+    user    0m4.528s
+    sys     0m0.016s
 
-    real    0m13.102s
-    user    0m13.084s
-    sys     0m0.004s
     $ time ./pythag-malfunction  > /dev/null
 
-    real    0m1.096s
-    user    0m1.092s
+    real    0m0.654s
+    user    0m0.652s
     sys     0m0.000s
-    $ 
+
+Tested on:
+* Ubuntu `16.04.4 LTS 64-bit`
+* Intel® Core™ i5-2500 CPU @ 3.30GHz × 4 
+* 8 GB RAM
+* Idris `1.2.0`
+* Malfunction `v0.2.1`
+* OCaml `4.05.0+flambda`

benchmark/BinaryTrees.idr

@@ -0,0 +1,74 @@
+--
+-- The Computer Language Benchmarks Game
+-- https://salsa.debian.org/benchmarksgame-team/benchmarksgame/
+--
+-- Contributed by Don Stewart
+-- *reset*
+--
+-- import System.Environment
+import Data.Bits
+-- import Text.Printf
+
+--
+-- an artificially strict tree. 
+--
+-- normally you would ensure the branches are lazy, but this benchmark
+-- requires strict allocation.
+--
+data Tree = Nil | Node Int Tree Tree
+
+minN : Int
+minN = 4
+
+-- io s n t = printf "%s of depth %d\t check: %d\n" s n t
+-- io : String -> Int -> Int -> IO ()
+-- io s n t = putStrLn (s ++ " of depth " ++ (show d) ++ "\t check: " ++ (show t))
+
+-- traverse the tree, counting up the nodes
+ccheck : Tree -> Int
+ccheck Nil          = 0
+ccheck (Node i l r) = 1 + ccheck l + ccheck r
+
+-- build a tree
+make : Int -> Int -> Tree
+make i 0 = Node i Nil Nil
+make i d = Node i (make d d2) (make d2 d2)
+  where d2 = d-1
+
+-- allocate and check lots of trees
+sumT : Int -> Int -> Int -> Int
+sumT d 0 t = t
+sumT d i t = sumT d (i-1) (t + a)
+  where a = ccheck (make 0 d)
+
+-- generate many trees
+depth : Int -> Int -> List (Int, Int, Int)
+depth d m = 
+    if d <= m then (n, d, (sumT d n 0)) :: depth (d+2) m
+    else []
+    where n = 2 * (m - d + minN)
+
+
+main : IO ()
+main = do
+    -- n <- getArgs >>= readIO . head
+    let n = 25
+    let maxN     = max (minN + 2) n
+    let stretchN = maxN + 1
+
+    -- stretch memory tree
+    let c = ccheck (make 0 stretchN)
+    -- io "stretch tree" stretchN c
+
+    -- allocate a long lived tree
+    let long    = make 0 maxN
+
+    -- allocate, walk, and deallocate many bottom-up binary trees
+    let vs = depth minN maxN
+    -- traverse (\ (m,d,i) => io (show m ++ "\t trees") d i) vs
+    traverse_ (putStrLn . show) vs
+
+    -- confirm the the long-lived binary tree still exists
+    -- io "long lived tree" maxN (ccheck long)
+
+

benchmark/Fib.idr

@@ -0,0 +1,7 @@
+myfib : Integer -> Integer
+myfib 0 = 1
+myfib 1 = 1
+myfib n = myfib (n - 1) + myfib (n - 2)
+
+main : IO ()
+main = putStrLn $ show $ myfib 40

docs/notes.md

@@ -0,0 +1,22 @@
+# Notes on what I've been doing
+
+## Idris and TDD with dep types
+
+## OCaml runtime
+
+## Malfunction 
+
+### Why lang?
+
+## Compilers
+
+## VSCode + other dev tools
+
+## Haskell
+
+## IRC
+
+## Extras (Academia, SPLS, other talks)
+
+## Future work
+### FFI

idris-malfunction.cabal

@@ -3,26 +3,21 @@
 
 name:                idris-malfunction
 version:             0.1.0.0
--- synopsis:            
--- description:         
 license:             MIT
 license-file:        LICENSE
 author:              Stephen Dolan
 maintainer:          [email protected]
--- copyright:           
--- category:            
 build-type:          Simple
--- extra-source-files:  
 cabal-version:       >=1.10
 
 executable idris-codegen-malfunction
   main-is:             Main.hs
-  -- other-modules:       
-  -- other-extensions:    
+  other-modules:       IRTS.CodegenMalfunction
   build-depends:       base
   hs-source-dirs:      src
   default-language:    Haskell2010
   build-depends:       containers
   build-depends:       idris
   build-depends:       process
   build-depends:       directory
+  build-depends:       filepath