Add some more IRs for back ends to use

ANF, in which everything is applied to variables only, and VMCode, in
which everything is reduced to a list of assignments.
I don't plan to add a defunctionalisation step. I've tested with with a
quick hack C backend, though I don't intend to commit that (not here at
least) because even though it basically works, it's Very Slow.

idris2.ipkg

@@ -1,6 +1,7 @@
 package idris2
 
 modules =
+    Compiler.ANF,
     Compiler.Common,
     Compiler.CompileExpr,
     Compiler.Inline,
@@ -9,6 +10,7 @@ modules =
 --     Compiler.Scheme.Chicken,
     Compiler.Scheme.Racket,
     Compiler.Scheme.Common,
+    Compiler.VMCode,
 
     Control.Delayed,
 

src/Compiler/ANF.idr

@@ -0,0 +1,262 @@
+module Compiler.ANF
+
+import Compiler.LambdaLift
+
+import Core.CompileExpr
+import Core.Context
+import Core.Core
+import Core.TT
+
+import Data.Vect
+
+%default covering
+
+-- Convert the lambda lifted form to ANF, with variable names made explicit.
+-- i.e. turn intermediate expressions into let bindings. Every argument is
+-- a variable as a result.
+
+mutual
+  public export
+  data AVar : Type where
+       ALocal : Int -> AVar
+       ANull : AVar
+
+  public export
+  data ANF : Type where
+    AV : FC -> AVar -> ANF
+    AAppName : FC -> Name -> List AVar -> ANF
+    AUnderApp : FC -> Name -> (missing : Nat) -> (args : List AVar) -> ANF
+    AApp : FC -> (closure : AVar) -> (arg : AVar) -> ANF
+    ALet : FC -> (var : Int) -> ANF -> ANF -> ANF
+    ACon : FC -> Name -> (tag : Int) -> List AVar -> ANF
+    AOp : FC -> PrimFn arity -> Vect arity AVar -> ANF
+    AExtPrim : FC -> Name -> List AVar -> ANF
+    AConCase : FC -> AVar -> List AConAlt -> Maybe ANF -> ANF
+    AConstCase : FC -> AVar -> List AConstAlt -> Maybe ANF -> ANF
+    APrimVal : FC -> Constant -> ANF
+    AErased : FC -> ANF
+    ACrash : FC -> String -> ANF
+
+  public export
+  data AConAlt : Type where
+       MkAConAlt : Name -> (tag : Int) -> (args : List Int) ->
+                   ANF -> AConAlt
+
+  public export
+  data AConstAlt : Type where
+       MkAConstAlt : Constant -> ANF -> AConstAlt
+
+public export
+data ANFDef : Type where
+     MkAFun : (args : List Int) -> ANF -> ANFDef
+     MkACon : (tag : Int) -> (arity : Nat) -> ANFDef
+     MkAForeign : (ccs : List String) -> (fargs : List CFType) ->
+                  CFType -> ANFDef
+     MkAError : ANF -> ANFDef
+
+mutual
+  export
+  Show AVar where
+    show (ALocal i) = "v" ++ show i
+    show ANull = "[__]"
+
+  export
+  Show ANF where
+    show (AV _ v) = show v
+    show (AAppName fc n args)
+        = show n ++ "(" ++ showSep ", " (map show args) ++ ")"
+    show (AUnderApp fc n m args)
+        = "<" ++ show n ++ " underapp " ++ show m ++ ">(" ++ 
+          showSep ", " (map show args) ++ ")"
+    show (AApp fc c arg)
+        = show c ++ " @ (" ++ show arg ++ ")"
+    show (ALet fc x val sc)
+        = "%let v" ++ show x ++ " = " ++ show val ++ " in " ++ show sc
+    show (ACon fc n t args)
+        = "%con " ++ show n ++ "(" ++ showSep ", " (map show args) ++ ")"
+    show (AOp fc op args)
+        = "%op " ++ show op ++ "(" ++ showSep ", " (toList (map show args)) ++ ")"
+    show (AExtPrim fc p args)
+        = "%extprim " ++ show p ++ "(" ++ showSep ", " (map show args) ++ ")"
+    show (AConCase fc sc alts def)
+        = "%case " ++ show sc ++ " of { "
+             ++ showSep "| " (map show alts) ++ " " ++ show def
+    show (AConstCase fc sc alts def)
+        = "%case " ++ show sc ++ " of { "
+             ++ showSep "| " (map show alts) ++ " " ++ show def
+    show (APrimVal _ x) = show x
+    show (AErased _) = "___"
+    show (ACrash _ x) = "%CRASH(" ++ show x ++ ")"
+
+  export
+  Show AConAlt where
+    show (MkAConAlt n t args sc)
+        = "%conalt " ++ show n ++ 
+             "(" ++ showSep ", " (map showArg args) ++ ") => " ++ show sc
+      where
+        showArg : Int -> String
+        showArg i = "v" ++ show i
+
+  export
+  Show AConstAlt where
+    show (MkAConstAlt c sc)
+        = "%constalt(" ++ show c ++ ") => " ++ show sc
+
+export
+Show ANFDef where
+  show (MkAFun args exp) = show args ++ ": " ++ show exp
+  show (MkACon tag arity)
+      = "Constructor tag " ++ show tag ++ " arity " ++ show arity
+  show (MkAForeign ccs args ret)
+      = "Foreign call " ++ show ccs ++ " " ++
+        show args ++ " -> " ++ show ret
+  show (MkAError exp) = "Error: " ++ show exp
+
+data AVars : List Name -> Type where
+     Nil : AVars []
+     (::) : Int -> AVars xs -> AVars (x :: xs)
+
+data Next : Type where
+
+nextVar : {auto v : Ref Next Int} ->
+          Core Int
+nextVar
+    = do i <- get Next
+         put Next (i + 1)
+         pure i
+
+lookup : IsVar x idx vs -> AVars vs -> Int
+lookup First (x :: xs) = x
+lookup (Later p) (x :: xs) = lookup p xs
+
+bindArgs : {auto v : Ref Next Int} ->
+           List ANF -> Core (List (AVar, Maybe ANF))
+bindArgs [] = pure []
+bindArgs (AV fc var :: xs)
+    = do xs' <- bindArgs xs
+         pure $ (var, Nothing) :: xs'
+bindArgs (AErased fc :: xs)
+    = do xs' <- bindArgs xs
+         pure $ (ANull, Nothing) :: xs'
+bindArgs (x :: xs)
+    = do i <- nextVar
+         xs' <- bindArgs xs
+         pure $ (ALocal i, Just x) :: xs'
+
+letBind : {auto v : Ref Next Int} ->
+          FC -> List ANF -> (List AVar -> ANF) -> Core ANF
+letBind fc args f
+    = do bargs <- bindArgs args
+         pure $ doBind [] bargs
+  where
+    doBind : List AVar -> List (AVar, Maybe ANF) -> ANF
+    doBind vs [] = f (reverse vs)
+    doBind vs ((ALocal i, Just t) :: xs)
+        = ALet fc i t (doBind (ALocal i :: vs) xs)
+    doBind vs ((var, _) :: xs) = doBind (var :: vs) xs
+
+toVect : (n : Nat) -> List a -> Maybe (Vect n a)
+toVect Z [] = Just []
+toVect (S k) (x :: xs)
+    = do xs' <- toVect k xs
+         pure (x :: xs')
+toVect _ _ = Nothing
+
+mlet : {auto v : Ref Next Int} ->
+       FC -> ANF -> (AVar -> ANF) -> Core ANF
+mlet fc (AV _ var) sc = pure $ sc var
+mlet fc val sc
+    = do i <- nextVar
+         pure $ ALet fc i val (sc (ALocal i)) 
+
+mutual
+  anfArgs : {auto v : Ref Next Int} ->
+            FC -> AVars vars ->
+            List (Lifted vars) -> (List AVar -> ANF) -> Core ANF
+  anfArgs fc vs args f
+      = do args' <- traverse (anf vs) args
+           letBind fc args' f
+
+  anf : {auto v : Ref Next Int} ->
+        AVars vars -> Lifted vars -> Core ANF
+  anf vs (LLocal fc p) = pure $ AV fc (ALocal (lookup p vs))
+  anf vs (LAppName fc n args)
+      = anfArgs fc vs args (AAppName fc n)
+  anf vs (LUnderApp fc n m args)
+      = anfArgs fc vs args (AUnderApp fc n m)
+  anf vs (LApp fc f a)
+      = anfArgs fc vs [f, a]
+                (\args => case args of
+                               [fvar, avar] => AApp fc fvar avar
+                               _ => ACrash fc "Can't happen (AApp)")
+  anf vs (LLet fc x val sc)
+      = do i <- nextVar
+           let vs' = i :: vs
+           pure $ ALet fc i !(anf vs val) !(anf vs' sc)
+  anf vs (LCon fc n t args)
+      = anfArgs fc vs args (ACon fc n t)
+  anf vs (LOp {arity} fc op args)
+      = do args' <- traverse (anf vs) (toList args)
+           letBind fc args'
+                (\args => case toVect arity args of
+                               Nothing => ACrash fc "Can't happen (AOp)"
+                               Just argsv => AOp fc op argsv)
+  anf vs (LExtPrim fc p args)
+      = anfArgs fc vs args (AExtPrim fc p)
+  anf vs (LConCase fc scr alts def)
+      = do scr' <- anf vs scr
+           alts' <- traverse (anfConAlt vs) alts
+           def' <- traverseOpt (anf vs) def
+           mlet fc scr' (\x => AConCase fc x alts' def')
+  anf vs (LConstCase fc scr alts def)
+      = do scr' <- anf vs scr
+           alts' <- traverse (anfConstAlt vs) alts
+           def' <- traverseOpt (anf vs) def
+           mlet fc scr' (\x => AConstCase fc x alts' def')
+  anf vs (LPrimVal fc c) = pure $ APrimVal fc c
+  anf vs (LErased fc) = pure $ AErased fc
+  anf vs (LCrash fc err) = pure $ ACrash fc err
+
+  anfConAlt : {auto v : Ref Next Int} ->
+              AVars vars -> LiftedConAlt vars -> Core AConAlt
+  anfConAlt vs (MkLConAlt n t args sc)
+      = do (is, vs') <- bindArgs args vs
+           pure $ MkAConAlt n t is !(anf vs' sc)
+    where
+      bindArgs : {auto v : Ref Next Int} ->
+                 (args : List Name) -> AVars vars' ->
+                 Core (List Int, AVars (args ++ vars'))
+      bindArgs [] vs = pure ([], vs)
+      bindArgs (n :: ns) vs
+          = do i <- nextVar
+               (is, vs') <- bindArgs ns vs
+               pure (i :: is, i :: vs')
+
+  anfConstAlt : {auto v : Ref Next Int} ->
+                AVars vars -> LiftedConstAlt vars -> Core AConstAlt
+  anfConstAlt vs (MkLConstAlt c sc)
+      = pure $ MkAConstAlt c !(anf vs sc)
+
+export
+toANF : LiftedDef -> Core ANFDef
+toANF (MkLFun args scope sc)
+    = do v <- newRef Next (the Int 0)
+         (iargs, vsNil) <- bindArgs args []
+         let vs : AVars args = rewrite sym (appendNilRightNeutral args) in
+                                      vsNil
+         (iargs', vs) <- bindArgs scope vs
+         pure $ MkAFun (iargs ++ reverse iargs') !(anf vs sc)
+  where
+    bindArgs : {auto v : Ref Next Int} ->
+               (args : List Name) -> AVars vars' ->
+               Core (List Int, AVars (args ++ vars'))
+    bindArgs [] vs = pure ([], vs)
+    bindArgs (n :: ns) vs
+        = do i <- nextVar
+             (is, vs') <- bindArgs ns vs
+             pure (i :: is, i :: vs')
+toANF (MkLCon t a ns) = pure $ MkACon t a
+toANF (MkLForeign ccs fargs t) = pure $ MkAForeign ccs fargs t
+toANF (MkLError err)
+    = do v <- newRef Next (the Int 0)
+         pure $ MkAError !(anf [] err)

src/Compiler/Common.idr

@@ -1,8 +1,10 @@
 module Compiler.Common
 
+import Compiler.ANF
 import Compiler.CompileExpr
 import Compiler.Inline
 import Compiler.LambdaLift
+import Compiler.VMCode
 
 import Core.Context
 import Core.Directory
@@ -27,6 +29,24 @@ record Codegen where
   ||| Execute an Idris 2 expression directly.
   executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
 
+public export
+record CompileData where
+  constructor MkCompileData
+  allNames : List Name -- names which need to be compiled
+  nameTags : NameTags -- a mapping from type names to constructor tags
+  mainExpr : CExp [] -- main expression to execute. This also appears in
+                     -- the definitions below as MN "__mainExpression" 0
+  lambdaLifted : List (Name, LiftedDef)
+       -- ^ lambda lifted definitions, if required. Only the top level names
+       -- will be in the context, and (for the moment...) I don't expect to
+       -- need to look anything up, so it's just an alist.
+  anf : List (Name, ANFDef)
+       -- ^ lambda lifted and converted to ANF (all arguments to functions
+       -- and constructors transformed to either variables or Null if erased)
+  vmcode : List (Name, VMDef)
+       -- ^ A much simplified virtual machine code, suitable for passing
+       -- to a more low level target such as C
+
 ||| compile
 ||| Given a value of type Codegen, produce a standalone function
 ||| that executes the `compileExpr` method of the Codegen
@@ -102,6 +122,7 @@ fastAppend xs
     build b (x :: xs) = do addToStringBuffer b x
                            build b xs
 
+-- Hmm, these dump functions are all very similar aren't they...
 dumpCases : Defs -> String -> List Name ->
             Core ()
 dumpCases defs fn cns
@@ -137,16 +158,33 @@ dumpLifted fn lns
     dumpDef : (Name, LiftedDef) -> String
     dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n"
 
-public export
+dumpANF : String -> List (Name, ANFDef) -> Core ()
-record CompileData where
+dumpANF fn lns
-  constructor MkCompileData
+    = do let cstrs = map dumpDef lns
-  allNames : List Name -- names which need to be compiled
+         Right () <- coreLift $ writeFile fn (fastAppend cstrs)
-  nameTags : NameTags -- a mapping from type names to constructor tags
+               | Left err => throw (FileErr fn err)
-  mainExpr : CExp [] -- main expression to execute
+         pure ()
-  lambdaLifted : List (Name, LiftedDef)
+  where
-       -- ^ lambda lifted definitions, if required. Only the top level names
+    fullShow : Name -> String
-       -- will be in the context, and (for the moment...) I don't expect to
+    fullShow (DN _ n) = show n
-       -- need to look anything up, so it's just an alist.
+    fullShow n = show n
+
+    dumpDef : (Name, ANFDef) -> String
+    dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n"
+
+dumpVMCode : String -> List (Name, VMDef) -> Core ()
+dumpVMCode fn lns
+    = do let cstrs = map dumpDef lns
+         Right () <- coreLift $ writeFile fn (fastAppend cstrs)
+               | Left err => throw (FileErr fn err)
+         pure ()
+  where
+    fullShow : Name -> String
+    fullShow (DN _ n) = show n
+    fullShow n = show n
+
+    dumpDef : (Name, VMDef) -> String
+    dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n"
 
 -- Find all the names which need compiling, from a given expression, and compile
 -- them to CExp form (and update that in the Defs).
@@ -183,9 +221,17 @@ getCompileData tm
          logTime "Fix arity" $ traverse_ fixArityDef cns
          logTime "Forget names" $ traverse_ mkForgetDef cns
 
-         lifted <- logTime "Lambda lift" $ traverse lambdaLift cns
-
          compiledtm <- fixArityExp !(compileExp tycontags tm)
+         let mainname = MN "__mainExpression" 0
+         (liftedtm, ldefs) <- liftBody mainname compiledtm
+
+         lifted_in <- logTime "Lambda lift" $ traverse lambdaLift cns
+
+         let lifted = (mainname, MkLFun [] [] liftedtm) ::
+                      ldefs ++ concat lifted_in
+
+         anf <- logTime "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
+         vmcode <- logTime "Get VM Code" $ pure (allDefs anf)
 
          defs <- get Ctxt
          maybe (pure ())
@@ -194,9 +240,18 @@ getCompileData tm
                (dumpcases sopts)
          maybe (pure ())
                (\f => do coreLift $ putStrLn $ "Dumping lambda lifted defs to " ++ f
-                         dumpLifted f (concat lifted))
+                         dumpLifted f lifted)
                (dumplifted sopts)
-         pure (MkCompileData cns tycontags compiledtm (concat lifted))
+         maybe (pure ())
+               (\f => do coreLift $ putStrLn $ "Dumping ANF defs to " ++ f
+                         dumpANF f anf)
+               (dumpanf sopts)
+         maybe (pure ())
+               (\f => do coreLift $ putStrLn $ "Dumping VM defs to " ++ f
+                         dumpVMCode f vmcode)
+               (dumpvmcode sopts)
+         pure (MkCompileData cns tycontags compiledtm
+                             lifted anf vmcode)
   where
     primTags : Int -> NameTags -> List Constant -> NameTags
     primTags t tags [] = tags

src/Compiler/CompileExpr.idr

@@ -59,7 +59,7 @@ etaExpand i Z exp args = mkApp exp (map (mkLocal (getFC exp)) (reverse args))
     mkApp (CExtPrim fc p args) args' = CExtPrim fc p (args ++ args')
     mkApp tm args = CApp (getFC tm) tm args
 etaExpand i (S k) exp args
-    = CLam (getFC exp) (MN "x" i)
+    = CLam (getFC exp) (MN "eta" i)
              (etaExpand (i + 1) k (weaken exp)
                   (MkVar First :: map weakenVar args))
 

src/Compiler/LambdaLift.idr

@@ -54,7 +54,10 @@ data LiftedDef : Type where
      -- We take the outer scope and the function arguments separately so that
      -- we don't have to reshuffle de Bruijn indices, which is expensive.
      -- This should be compiled as a function which takes 'args' first,
-     -- then 'scope'.
+     -- then 'reverse scope'.
+     -- (Sorry for the awkward API - it's to do with how the indices are
+     -- arranged for the variables, and it oculd be expensive to reshuffle them!
+     -- See Compiler.ANF for an example of how they get resolved to names)
      MkLFun : (args : List Name) -> -- function arguments
               (scope : List Name) -> -- outer scope
               Lifted (scope ++ args) -> LiftedDef
@@ -107,7 +110,8 @@ mutual
 
 export
 Show LiftedDef where
-  show (MkLFun args scope exp) = show args ++ show scope ++ ": " ++ show exp
+  show (MkLFun args scope exp)
+      = show args ++ show (reverse scope) ++ ": " ++ show exp
   show (MkLCon tag arity pos)
       = "Constructor tag " ++ show tag ++ " arity " ++ show arity ++
         maybe "" (\n => " (newtype by " ++ show n ++ ")") pos
@@ -136,6 +140,7 @@ genName
     mkName : Name -> Int -> Name
     mkName (NS ns b) i = NS ns (mkName b i)
     mkName (UN n) i = MN n i
+    mkName (DN _ n) i = mkName n i
     mkName n i = MN (show n) i
 
 unload : FC -> Lifted vars -> List (Lifted vars) -> Core (Lifted vars)
@@ -188,7 +193,7 @@ mutual
       traverseArgs (a :: as) = pure $ !(liftExp a) :: !(traverseArgs as)
   liftExp (CExtPrim fc p args) = pure $ LExtPrim fc p !(traverse liftExp args)
   liftExp (CForce fc tm) = liftExp (CApp fc tm [CErased fc])
-  liftExp (CDelay fc tm) = liftExp (CLam fc (MN "x" 0) (weaken tm))
+  liftExp (CDelay fc tm) = liftExp (CLam fc (MN "act" 0) (weaken tm))
   liftExp (CConCase fc sc alts def)
       = pure $ LConCase fc !(liftExp sc) !(traverse liftConAlt alts)
                            !(traverseOpt liftExp def)
@@ -205,6 +210,7 @@ mutual
   liftExp (CErased fc) = pure $ LErased fc
   liftExp (CCrash fc str) = pure $ LCrash fc str
 
+export
 liftBody : Name -> CExp vars -> Core (Lifted vars, List (Name, LiftedDef))
 liftBody n tm
     = do l <- newRef Lifts (MkLDefs n [] 0)

src/Compiler/VMCode.idr

@@ -0,0 +1,196 @@
+module Compiler.VMCode
+
+import Compiler.ANF
+
+import Core.CompileExpr
+import Core.Context
+import Core.Core
+import Core.TT
+
+import Data.Vect
+
+import Debug.Trace
+
+%default covering
+
+public export
+data Reg : Type where
+     RVal : Reg
+     Loc : Int -> Reg
+     Discard : Reg
+
+-- VM instructions - first Reg is where the result goes, unless stated
+-- otherwise.
+
+-- As long as you have a representation of closures, and an 'apply' function
+-- which adds an argument and evaluates if it's fully applied, then you can
+-- translate this directly to a target language program.
+public export
+data VMInst : Type where
+     DECLARE : Reg -> VMInst
+     START : VMInst -- start of the main body of the function
+     ASSIGN : Reg -> Reg -> VMInst
+     MKCON : Reg -> (tag : Int) -> (args : List Reg) -> VMInst
+     MKCLOSURE : Reg -> Name -> (missing : Nat) -> (args : List Reg) -> VMInst
+     MKCONSTANT : Reg -> Constant -> VMInst
+     
+     APPLY : Reg -> (f : Reg) -> (a : Reg) -> VMInst
+     CALL : Reg -> (tailpos : Bool) -> Name -> (args : List Reg) -> VMInst
+     OP : Reg -> PrimFn arity -> Vect arity Reg -> VMInst
+     EXTPRIM : Reg -> Name -> List Reg -> VMInst
+
+     CASE : Reg -> -- scrutinee 
+            (alts : List (Int, List VMInst)) -> -- based on constructor tag
+            (def : Maybe (List VMInst)) ->
+            VMInst
+     CONSTCASE : Reg -> -- scrutinee 
+                 (alts : List (Constant, List VMInst)) ->
+                 (def : Maybe (List VMInst)) ->
+                 VMInst
+     PROJECT : Reg -> (value : Reg) -> (pos : Int) -> VMInst
+     NULL : Reg -> VMInst
+
+     ERROR : String -> VMInst
+
+public export
+data VMDef : Type where
+     MkVMFun : (args : List Int) -> List VMInst -> VMDef
+     MkVMError : List VMInst -> VMDef
+
+export
+Show Reg where
+  show RVal = "RVAL"
+  show (Loc i) = "v" ++ show i
+  show Discard = "DISCARD"
+
+export
+Show VMInst where
+  show (DECLARE r) = "DECLARE " ++ show r
+  show START = "START"
+  show (ASSIGN r v) = show r ++ " := " ++ show v
+  show (MKCON r t args)
+      = show r ++ " := MKCON " ++ show t ++ " (" ++
+                  showSep ", " (map show args) ++ ")"            
+  show (MKCLOSURE r n m args)
+      = show r ++ " := MKCLOSURE " ++ show n ++ " " ++ show m ++ " (" ++
+                  showSep ", " (map show args) ++ ")"
+  show (MKCONSTANT r c) = show r ++ " := MKCONSTANT " ++ show c
+  show (APPLY r f a) = show r ++ " := " ++ show f ++ " @ " ++ show a
+  show (CALL r t n args)
+      = show r ++ " := " ++ (if t then "TAILCALL " else "CALL ") ++
+        show n ++ "(" ++ showSep ", " (map show args) ++ ")"
+  show (OP r op args)
+      = show r ++ " := " ++ "OP " ++
+        show op ++ "(" ++ showSep ", " (map show (toList args)) ++ ")"
+  show (EXTPRIM r n args)
+      = show r ++ " := " ++ "EXTPRIM " ++
+        show n ++ "(" ++ showSep ", " (map show args) ++ ")"
+
+  show (CASE scr alts def)
+      = "CASE " ++ show scr ++ " " ++ show alts ++ " {default: " ++ show def ++ "}"
+  show (CONSTCASE scr alts def)
+      = "CASE " ++ show scr ++ " " ++ show alts ++ " {default: " ++ show def ++ "}"
+
+  show (PROJECT r val pos)
+      = show r ++ " := PROJECT(" ++ show val ++ ", " ++ show pos ++ ")"
+  show (NULL r) = show r ++ " := NULL"
+  show (ERROR str) = "ERROR " ++ show str
+
+export
+Show VMDef where
+  show (MkVMFun args body) = show args ++ ": " ++ show body
+  show (MkVMError err) = "Error: " ++ show err
+
+toReg : AVar -> Reg
+toReg (ALocal i) = Loc i
+toReg ANull = Discard
+
+toVM : (tailpos : Bool) -> (target : Reg) -> ANF -> List VMInst
+toVM t Discard _ = []
+toVM t res (AV fc (ALocal i))
+    = [ASSIGN res (Loc i)]
+toVM t res (AAppName fc n args)
+    = [CALL res t n (map toReg args)]
+toVM t res (AUnderApp fc n m args)
+    = [MKCLOSURE res n m (map toReg args)]
+toVM t res (AApp fc f a)
+    = [APPLY res (toReg f) (toReg a)]
+toVM t res (ALet fc var val body)
+    = toVM False (Loc var) val ++ toVM t res body
+toVM t res (ACon fc n tag args)
+    = [MKCON res tag (map toReg args)]
+toVM t res (AOp fc op args)
+    = [OP res op (map toReg args)]
+toVM t res (AExtPrim fc p args)
+    = [EXTPRIM res p (map toReg args)]
+toVM t res (AConCase fc (ALocal scr) alts def)
+    = [CASE (Loc scr) (map toVMConAlt alts) (map (toVM t res) def)]
+  where
+    projectArgs : Int -> List Int -> List VMInst
+    projectArgs i [] = []
+    projectArgs i (arg :: args)
+        = PROJECT (Loc arg) (Loc scr) i :: projectArgs (i + 1) args
+
+    toVMConAlt : AConAlt -> (Int, List VMInst)
+    toVMConAlt (MkAConAlt n tag args code)
+        = (tag, projectArgs 0 args ++ toVM t res code)
+toVM t res (AConstCase fc (ALocal scr) alts def)
+    = [CONSTCASE (Loc scr) (map toVMConstAlt alts) (map (toVM t res) def)]
+  where
+    toVMConstAlt : AConstAlt -> (Constant, List VMInst)
+    toVMConstAlt (MkAConstAlt c code)
+        = (c, toVM t res code)
+toVM t res (APrimVal fc c)
+    = [MKCONSTANT res c]
+toVM t res (AErased fc)
+    = [NULL res]
+toVM t res (ACrash fc err)
+    = [ERROR err]
+toVM t res _
+    = [NULL res]
+
+findVars : VMInst -> List Int
+findVars (ASSIGN (Loc r) _) = [r]
+findVars (MKCON (Loc r) _ _) = [r]
+findVars (MKCLOSURE (Loc r) _ _ _) = [r]
+findVars (MKCONSTANT (Loc r) _) = [r]
+findVars (APPLY (Loc r) _ _) = [r]
+findVars (CALL (Loc r) _ _ _) = [r]
+findVars (OP (Loc r) _ _) = [r]
+findVars (EXTPRIM (Loc r) _ _) = [r]
+findVars (CASE _ alts d)
+    = concatMap findVarAlt alts ++ fromMaybe [] (map (concatMap findVars) d)
+  where
+    findVarAlt : (Int, List VMInst) -> List Int
+    findVarAlt (t, code) = concatMap findVars code
+findVars (CONSTCASE _ alts d)
+    = concatMap findConstVarAlt alts ++ fromMaybe [] (map (concatMap findVars) d)
+  where
+    findConstVarAlt : (Constant, List VMInst) -> List Int
+    findConstVarAlt (t, code) = concatMap findVars code
+findVars (PROJECT (Loc r) _ _) = [r]
+findVars _ = []
+
+declareVars : List Int -> List VMInst -> List VMInst
+declareVars got code
+    = let vs = concatMap findVars code in
+          declareAll got vs
+  where
+    declareAll : List Int -> List Int -> List VMInst
+    declareAll got [] = START :: code
+    declareAll got (i :: is)
+        = if i `elem` got
+             then declareAll got is
+             else DECLARE (Loc i) :: declareAll (i :: got) is
+
+export
+toVMDef : ANFDef -> Maybe VMDef
+toVMDef (MkAFun args body)
+    = Just $ MkVMFun args (declareVars args (toVM True RVal body))
+toVMDef (MkAError body)
+    = Just $ MkVMError (declareVars [] (toVM True RVal body))
+toVMDef _ = Nothing
+
+export
+allDefs : List (Name, ANFDef) -> List (Name, VMDef)
+allDefs = mapMaybe (\ (n, d) => do d' <- toVMDef d; pure (n, d'))

src/Core/Options.idr

@@ -45,7 +45,10 @@ Eq CG where
 
 export
 availableCGs : List (String, CG)
-availableCGs = [("chez", Chez), ("chicken", Chicken), ("racket", Racket)]
+availableCGs
+    = [ ("chez", Chez),
+--        ("chicken", Chicken),
+       ("racket", Racket)]
 
 export
 getCG : String -> Maybe CG
@@ -101,6 +104,8 @@ record Session where
   debugElabCheck : Bool -- do conversion check to verify results of elaborator
   dumpcases : Maybe String -- file to output compiled case trees
   dumplifted : Maybe String -- file to output lambda lifted definitions
+  dumpanf : Maybe String -- file to output ANF definitions
+  dumpvmcode : Maybe String -- file to output VM code definitions
 
 public export
 record PPrinter where
@@ -146,7 +151,7 @@ defaultPPrint = MkPPOpts False True False
 
 defaultSession : Session
 defaultSession = MkSessionOpts False False False Chez 0 False False
-                               Nothing Nothing
+                               Nothing Nothing Nothing Nothing
 
 defaultElab : ElabDirectives
 defaultElab = MkElabDirectives True True PartialOK 3 True

src/Idris/CommandLine.idr

@@ -73,6 +73,10 @@ data CLOpt
   DumpCases String |
    ||| Dump lambda lifted defs before compiling
   DumpLifted String |
+   ||| Dump ANF defs before compiling
+  DumpANF String |
+   ||| Dump VM code defs before compiling
+  DumpVMCode String |
    ||| Run a REPL command then exit immediately
   RunREPL String |
   FindIPKG |
@@ -150,7 +154,11 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
            MkOpt ["--dumpcases"] ["output file"] (\f => [DumpCases f])
               Nothing, -- dump case trees to the given file
            MkOpt ["--dumplifted"] ["output file"] (\f => [DumpLifted f])
-              Nothing, -- dump case trees to the given file
+              Nothing, -- dump lambda lifted trees to the given file
+           MkOpt ["--dumpanf"] ["output file"] (\f => [DumpANF f])
+              Nothing, -- dump ANF to the given file
+           MkOpt ["--dumpvmcode"] ["output file"] (\f => [DumpVMCode f])
+              Nothing, -- dump VM Code to the given file
            MkOpt ["--debug-elab-check"] [] [DebugElabCheck]
               Nothing -- do more elaborator checks (currently conversion in LinearCheck)
            ]

src/Idris/SetOptions.idr

@@ -92,6 +92,12 @@ preOptions (DumpCases f :: opts)
 preOptions (DumpLifted f :: opts)
     = do setSession (record { dumplifted = Just f } !getSession)
          preOptions opts
+preOptions (DumpANF f :: opts)
+    = do setSession (record { dumpanf = Just f } !getSession)
+         preOptions opts
+preOptions (DumpVMCode f :: opts)
+    = do setSession (record { dumpvmcode = Just f } !getSession)
+         preOptions opts
 preOptions (_ :: opts) = preOptions opts
 
 -- Options to be processed after type checking. Returns whether execution