remove zero-argument functions / applications in generated code

newt/testcase.newt

@@ -5,6 +5,8 @@ module Scratch
 
 -- There are indexes below, but we're got pulling constraints out of them yet.
 
+ptype Int
+
 data Nat : U where
   Z : Nat
   S : Nat -> Nat
@@ -79,4 +81,5 @@ nand = \ x y => not (case x of
 
 data Void : U where
 
-
+foo : Int
+foo = 42

src/Lib/Compile.idr

@@ -187,6 +187,7 @@ mkArgs Z acc = acc
 mkArgs (S k) acc = mkArgs k ("h\{show k}" :: acc)
 
 dcon : String -> Nat -> Doc
+dcon nm Z = stmtToDoc $ JConst nm $ LitObject [("tag", LitString nm)]
 dcon nm arity =
   let args := mkArgs arity []
       obj := ("tag", LitString nm) :: map (\x => (x, Var x)) args

src/Lib/CompileExp.idr

@@ -69,6 +69,7 @@ apply t (x :: xs) acc (S k) = apply t xs (acc :< x) k
 apply t ts acc 0 = go (CApp t (acc <>> [])) ts
   where
     go : CExp -> List CExp -> M CExp
+    go (CApp t []) [] = pure t
     go t [] = pure t
     go t (arg :: args) = go (CApp t [arg]) args
 
@@ -119,6 +120,7 @@ compileFun tm = go tm []
   where
     go : Tm -> List String -> M CExp
     go (Lam _ nm t) acc = go t (nm :: acc)
+    go tm [] = compileTerm tm
     go tm args = pure $ CFun (reverse args) !(compileTerm tm)