diff --git a/newt/testcase.newt b/newt/testcase.newt index 6a0c939..52c3853 100644 --- a/newt/testcase.newt +++ b/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 diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 8df3c50..594f417 100644 --- a/src/Lib/Compile.idr +++ b/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 diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 32e7c5d..74cf643 100644 --- a/src/Lib/CompileExp.idr +++ b/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)