Compile if_then_else_ expressions

Author: omelkonian

Main.hs

@@ -110,12 +110,25 @@ isOp (Hs.UnQual _ Hs.Symbol{}) = True
 isOp (Hs.Special _ Hs.Cons{})  = True
 isOp _                         = False
 
+freshString :: String -> TCM String
+freshString s = do
+  ctx <- getContextNames
+  -- prettyShow <$> freshName_ s
+  -- ^ this returns 'x' even when context contains 'x'??
+  return $ freshWrt (show <$> ctx) s
+  where
+    freshWrt :: [String] -> String -> String
+    freshWrt xs s
+      | s `elem` xs = freshWrt xs (s ++ "'")
+      | otherwise   = s
+
 -- Builtins ---------------------------------------------------------------
 
 data Prim = Unit
           | Nat | Float | Word64
           | Char
           | List | Cons | Nil
+          | Bool | True_ | False_
   deriving (Show, Eq)
 
 type Builtins = Map QName Prim
@@ -125,6 +138,7 @@ getBuiltins = Map.fromList . concat <$> mapM getB
   [ builtinUnit |-> Unit
   , builtinNat |-> Nat, builtinFloat |-> Float
   , builtinWord64 |-> Word64
+  , builtinBool |-> Bool, builtinTrue |-> True_, builtinFalse |-> False_
   , builtinChar |-> Char
   , builtinList |-> List , builtinCons |-> Cons , builtinNil |-> Nil
   ]
@@ -142,6 +156,9 @@ compilePrim = \case
   Nat    -> unqual "Integer"
   Float  -> unqual "Double"
   Word64 -> unqual "Word64"
+  Bool   -> unqual "Bool"
+  True_  -> unqual "True"
+  False_ -> unqual "False"
   Char   -> unqual "Char"
   List   -> special Hs.ListCon
   Cons   -> special Hs.Cons
@@ -241,7 +258,11 @@ compileTerm :: Builtins -> Term -> TCM (Hs.Exp ())
 compileTerm builtins v =
   case unSpine v of
     Var x es   -> (`app` es) . Hs.Var () . Hs.UnQual () . hsName =<< showTCM (Var x [])
-    Def f es   -> (`app` es) . Hs.Var () =<< hsQName builtins f
+    Def f es
+      | show (qnameName f) == "if_then_else_"
+      -> ite es
+      | otherwise
+      -> (`app` es) . Hs.Var () =<< hsQName builtins f
     Con h i es -> (`app` es) . Hs.Con () =<< hsQName builtins (conName h)
     Lit (LitNat _ n) -> return $ Hs.intE n
     Lit (LitFloat _ d) -> return $ Hs.Lit () $ Hs.Frac () (toRational d) (show d)
@@ -251,11 +272,23 @@ compileTerm builtins v =
     Lam _ b -> underAbstraction_ b (compileTerm builtins)
     t -> genericDocError =<< text "bad term:" <?> prettyTCM t
   where
-    app :: Hs.Exp () -> Elims -> TCM (Hs.Exp ())
-    app hd es = do
+    compileArgs :: Elims -> TCM [Hs.Exp ()]
+    compileArgs es = do
       let Just args = allApplyElims es
-      args <- mapM (compileTerm builtins . unArg) $ filter visible args
-      return $ eApp hd args
+      mapM (compileTerm builtins . unArg) $ filter visible args
+
+    app :: Hs.Exp () -> Elims -> TCM (Hs.Exp ())
+    app hd es = eApp <$> pure hd <*> compileArgs es
+
+    ite :: Elims -> TCM (Hs.Exp ())
+    ite es = compileArgs es >>= \case
+      -- fully applied
+      (b : t : f : es') -> return $ Hs.If () b t f `eApp` es'
+      -- partially applied -> eta-expand
+      es' -> do
+        xs <- fmap Hs.name . drop (length es') <$> mapM freshString ["b", "t", "f"]
+        let [b, t, f] = es' ++ (Hs.var <$> xs)
+        return $ Hs.lamE (Hs.pvar <$> xs) $ Hs.If () b t f
 
 compilePats :: Builtins -> NAPs -> TCM [Hs.Pat ()]
 compilePats builtins ps = mapM (compilePat builtins . namedArg) $ filter visible ps

Prelude.agda

@@ -0,0 +1,17 @@
+module Prelude where
+
+open import Agda.Builtin.List public
+open import Agda.Builtin.Nat public
+open import Agda.Builtin.Bool public
+open import Agda.Builtin.Float public
+open import Agda.Builtin.Word public
+open import Agda.Builtin.Char public
+open import Agda.Builtin.Equality public
+
+variable
+  a b c d e f g h i j k l m n o p q r s t u v w x y z : Set
+
+infix 0 if_then_else_
+if_then_else_ : Bool → a → a → a
+if true  then t else f = t
+if false then t else f = f

README.md

@@ -6,7 +6,6 @@ See test/Test.agda for an example.
 
 ### Future work
 
-- Compile if/then/else
 - Literals in patterns
 - Map instance arguments to Haskell type classes (definitions and use) [#3](https://github.com/agda/agda2hs/pull/3)
 - `where` clauses

test/Prelude.agda

@@ -0,0 +1,17 @@
+module Prelude where
+
+open import Agda.Builtin.List public
+open import Agda.Builtin.Nat public
+open import Agda.Builtin.Bool public
+open import Agda.Builtin.Float public
+open import Agda.Builtin.Word public
+open import Agda.Builtin.Char public
+open import Agda.Builtin.Equality public
+
+variable
+  a b c d e f g h i j k l m n o p q r s t u v w x y z : Set
+
+infix 0 if_then_else_
+if_then_else_ : Bool → a → a → a
+if true  then t else f = t
+if false then t else f = f

test/Test.agda

@@ -1,14 +1,6 @@
 module _ where
 
-open import Agda.Builtin.List
-open import Agda.Builtin.Nat
-open import Agda.Builtin.Float
-open import Agda.Builtin.Word
-open import Agda.Builtin.Char
-open import Agda.Builtin.Equality
-
-variable
-  a b : Set
+open import Prelude
 
 -- ** Foreign HS code
 
@@ -78,9 +70,9 @@ ex_char = 'a'
 postulate
   toEnum : Nat → Char
 
-d : Char
-d = toEnum 100
-{-# COMPILE AGDA2HS d #-}
+char_d : Char
+char_d = toEnum 100
+{-# COMPILE AGDA2HS char_d #-}
 
 -- ** Polymorphic functions
 
@@ -113,3 +105,37 @@ assoc (suc a) b c rewrite assoc a b c = refl
 thm : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
 thm []       ys = refl
 thm (x ∷ xs) ys rewrite thm xs ys | assoc x (sum xs) (sum ys) = refl
+
+-- ** Booleans
+
+ex_bool : Bool
+ex_bool = true
+{-# COMPILE AGDA2HS ex_bool #-}
+
+ex_if : Nat
+ex_if = if true then 1 else 0
+{-# COMPILE AGDA2HS ex_if #-}
+
+if_over : Nat
+if_over = (if true then (λ x → x) else (λ x → x + 1)) 0
+{-# COMPILE AGDA2HS if_over #-}
+
+if_partial₁ : List Nat → List Nat
+if_partial₁ = map (if true then 1 else_)
+{-# COMPILE AGDA2HS if_partial₁ #-}
+
+if_partial₂ : List Nat → List (Nat → Nat)
+if_partial₂ = map (if true then_else_)
+{-# COMPILE AGDA2HS if_partial₂ #-}
+
+if_partial₃ : List Bool → List (Nat → Nat → Nat)
+if_partial₃ = map if_then_else_
+{-# COMPILE AGDA2HS if_partial₃ #-}
+
+if_partial₄ : List Bool → List (Nat → Nat)
+if_partial₄ = map (if_then 1 else_)
+{-# COMPILE AGDA2HS if_partial₄ #-}
+
+if_partial₅ : Bool → Nat → List Nat → List Nat
+if_partial₅ b f = map (if b then f else_)
+{-# COMPILE AGDA2HS if_partial₅ #-}

test/golden/Test.hs

@@ -38,8 +38,8 @@ ex_word = fromInteger 0
 ex_char :: Char
 ex_char = 'a'
 
-d :: Char
-d = toEnum 100
+char_d :: Char
+char_d = toEnum 100
 
 (++) :: [a] -> [a] -> [a]
 [] ++ ys = ys
@@ -55,3 +55,27 @@ plus3 = map (\ n -> n + 3)
 doubleLambda :: Integer -> Integer -> Integer
 doubleLambda = \ a b -> a + 2 * b
 
+ex_bool :: Bool
+ex_bool = True
+
+ex_if :: Integer
+ex_if = if True then 1 else 0
+
+if_over :: Integer
+if_over = (if True then \ x -> x else \ x -> x + 1) 0
+
+if_partial₁ :: [Integer] -> [Integer]
+if_partial₁ = map (\ f -> if True then 1 else f)
+
+if_partial₂ :: [Integer] -> [Integer -> Integer]
+if_partial₂ = map (\ t f -> if True then t else f)
+
+if_partial₃ :: [Bool] -> [Integer -> Integer -> Integer]
+if_partial₃ = map (\ b t f -> if b then t else f)
+
+if_partial₄ :: [Bool] -> [Integer -> Integer]
+if_partial₄ = map (\ section f -> if section then 1 else f)
+
+if_partial₅ :: Bool -> Integer -> [Integer] -> [Integer]
+if_partial₅ b f = map (\ f' -> if b then f else f')
+