typed-irbuilder: try to make function pass typed args

This doesn't go as far as using singletons, currently we have to pass function
arguments with the TypeApplication. We need some massaging to make it look
nicer. Also it used unsafeCoerce under the hood.

But it let's you avoid coerce, function arguments in the body do-block have the
right type tags right away.

Example2 is changed to use new function, also added bigger Example3.

Author: yanok

Example2.hs

@@ -3,6 +3,8 @@
 {-# LANGUAGE RecursiveDo #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module Example2 where
 
@@ -20,15 +22,15 @@ import qualified LLVM.AST.Tagged as AST
 import LLVM.AST.Tagged.IRBuilder as TBuilder
 import qualified LLVM.IRBuilder as Builder
 
-import Data.Coerce
+import Data.HVect
 
 simple :: AST.Module
 simple = Builder.buildModule "exampleModule" $ do
     func
   where
   func :: Builder.ModuleBuilder (AST.Operand ::: IntegerType' 32)
   func =
-    TBuilder.function "add" [(AST.i32, "a"), (AST.i32, "b")] $ \[a, b] -> do
+    TBuilder.function @(IntegerType' 32) @'[ '(IntegerType' 32, 'ParameterName' "a"), '(IntegerType' 32, 'ParameterName' "b")] "add" $ \(a :&: b :&: HNil) -> do
       entry <- block `named` "entry"; do
-        c <- add (coerce a) (coerce b)
+        c <- add a b
         ret c

Example3.hs

@@ -0,0 +1,46 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE RecursiveDo #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Main where
+
+import GHC.TypeLits
+import LLVM.Prelude
+import LLVM.AST.Tagged.Operand
+import qualified LLVM.AST.Tagged.Constant as TC
+import LLVM.AST.Tagged.Global
+import LLVM.AST.Tagged.Tag
+import LLVM.AST.TypeLevel.Type
+import qualified LLVM.AST as AST
+import qualified LLVM.AST.Type as AST
+import qualified LLVM.AST.Float as F
+import qualified LLVM.AST.Constant as C
+import qualified LLVM.AST.IntegerPredicate as P
+
+import LLVM.AST.Tagged.IRBuilder as TBuilder
+import qualified LLVM.IRBuilder as Builder
+
+import Data.HVect
+
+simple :: AST.Module
+simple = Builder.buildModule "exampleModule" $ mdo
+  TBuilder.function @(IntegerType' 32) @'[ '(IntegerType' 32, 'ParameterName' "a")] "f" $ \(a :&: HNil)  -> mdo
+    entry <- block `named` "entry"
+    cond <- icmp P.EQ a (constantOperand (TC.int 0))
+    condBr cond ifThen ifElse
+    ifThen <- block
+    trVal <- add a (constantOperand (TC.int 0))
+    br ifExit
+    ifElse <- block `named` "if.else"
+    flVal <- add a (constantOperand (TC.int 0))
+    br ifExit
+    ifExit <- block `named` "if.exit"
+    r <- phi [(trVal, ifThen), (flVal, ifElse)]
+    ret r
+
+main :: IO ()
+main = print simple

llvm-hs-typed.cabal

@@ -57,6 +57,7 @@ library
     llvm-hs-pure    == 5.1.*,
     llvm-hs-pretty  >= 0.2,
     bytestring      >= 0.10 && < 0.11,
-    encode-string   == 0.1.*
+    encode-string   == 0.1.*,
+    hvect           == 0.4.*
   hs-source-dirs:      src
   default-language:    Haskell2010

src/LLVM/AST/Tagged/IRBuilder.hs

@@ -111,6 +111,8 @@ import qualified LLVM.AST.FloatingPointPredicate as FP
 import GHC.TypeLits
 import GHC.Exts (Constraint)
 import Data.Coerce
+import Unsafe.Coerce
+import Data.HVect hiding (Nat)
 import qualified LLVM.IRBuilder as IR
 
 -------------------------------------------------------------------------------
@@ -144,13 +146,20 @@ freshUnName = IR.freshUnName >>= pure . coerce
 named :: IR.MonadIRBuilder m => m (r ::: t) -> ShortByteString -> m (r ::: t)
 named m = IR.named m
 
+-- partially applied Map
+type family MapOp (as :: [(Type', ParameterName')]) where
+   MapOp '[] = '[]
+   MapOp ('(t, _) ': xs) = (Operand :::: t) ': MapOp xs
+
 function
-  :: forall (t :: Type') m. (Known t, IR.MonadModuleBuilder m)
+  :: forall (t :: Type') -- ^ Function return type
+            (as :: [(Type', ParameterName')]) -- ^ Function arguments
+            m.
+     (Known t, Known as, IR.MonadModuleBuilder m)
   => Name                              -- ^ Function name
-  -> [(Type, IR.ParameterName)]        -- ^ Parameter types and name suggestions
-  -> ([Operand] -> IR.IRBuilderT m ()) -- ^ Function body builder
+  -> (HVect (MapOp as) -> IR.IRBuilderT m ()) -- ^ Function body builder
   -> m (Operand ::: t)
-function nm params m = IR.function nm params (val @_ @t) m >>= pure . coerce
+function nm m = IR.function nm (val @_ @as) (val @_ @t) (unsafeCoerce m) >>= pure . coerce
 
 -------------------------------------------------------------------------------
 -- Types

src/LLVM/AST/TypeLevel/Type.hs

@@ -36,11 +36,14 @@ import qualified Data.ByteString.Short as BS
 import LLVM.AST.Type
 import LLVM.AST.AddrSpace
 import LLVM.AST.Name
+import qualified LLVM.IRBuilder as IR
 
 data Name' = Name' Symbol | UnName' Nat
 
 data AddrSpace' = AddrSpace' Nat
 
+data ParameterName' = ParameterName' Symbol
+
 -- | A copy of 'Type', suitable to be used on the type level
 data Type'
   = VoidType'
@@ -103,6 +106,8 @@ type instance Value FloatingPointType = FloatingPointType
 type instance Value Bool = Bool
 type instance Value Symbol = String
 type instance Value Nat = Integer
+type instance Value ParameterName' = IR.ParameterName
+type instance Value (a, b) = (Value a, Value b)
 
 word32Val :: forall (n::Nat). Known n => Word32
 word32Val = fromIntegral (val @_ @n)
@@ -153,6 +158,11 @@ instance Known s => Known ('Name' s) where
     val = Name (byteStringVal @s)
 instance Known n => Known (UnName' n) where
     val = UnName (wordVal @n)
+instance Known s => Known ('ParameterName' s) where
+    val = IR.ParameterName (byteStringVal @s)
+
+instance (Known a, Known b) => Known '(a, b) where
+    val = (val @_ @a, val @_ @b)
 
 instance Known HalfFP      where val = HalfFP
 instance Known FloatFP     where val = FloatFP