diff --git a/default.nix b/default.nix index 353bd00..cee7e30 100644 --- a/default.nix +++ b/default.nix @@ -11,6 +11,7 @@ compiler.developPackage { modifier = drv: pkgs.haskell.lib.compose.addBuildTools [ pkgs.haskellPackages.cabal-install + pkgs.haskell-language-server # LLVM CLI tools for local testing purposes. pkgs.llvm_9 # For viewing heap profiles (mainly ps2pdf). diff --git a/elemental.cabal b/elemental.cabal index 72b015a..8778027 100644 --- a/elemental.cabal +++ b/elemental.cabal @@ -33,8 +33,10 @@ common shared , bytestring ^>= 0.10 , containers ^>= 0.6 , data-fix ^>= 0.3 + , dlist ^>= 1.0 , fused-effects ^>= 1.1 , integer-logarithms ^>= 1.0 + , lens ^>= 4.19 , llvm-hs == 9.0.1 , llvm-hs-pure ^>= 9.0 , megaparsec ^>= 9.0 @@ -42,6 +44,7 @@ common shared , tagged ^>= 0.8 , text ^>= 1.2 , text-short ^>= 0.1 + , transformers ^>= 0.5 default-language: Haskell2010 ghc-options: -Wall @@ -70,9 +73,12 @@ library , Language.Elemental.AST.Program , Language.Elemental.AST.Type , Language.Elemental.AST.Unchecked + , Language.Elemental.Backend + , Language.Elemental.Backend.LLVM , Language.Elemental.Diagnostic , Language.Elemental.Emit , Language.Elemental.Location + , Language.Elemental.InteractionNet , Language.Elemental.Parser , Language.Elemental.Pretty , Language.Elemental.Primitive @@ -116,5 +122,6 @@ test-suite test , tasty ^>= 1.4 , tasty-golden ^>= 2.3 , tasty-hedgehog ^>= 1.1 + , tasty-hunit ^>= 0.10 ghc-options: -threaded diff --git a/src/Control/Effect/ModuleBuilder.hs b/src/Control/Effect/ModuleBuilder.hs index b9173c4..355e12e 100644 --- a/src/Control/Effect/ModuleBuilder.hs +++ b/src/Control/Effect/ModuleBuilder.hs @@ -57,10 +57,12 @@ function -- ^ The types of the function arguments. -> Type -- ^ The return type of the function. + -> Linkage + -- ^ The linkage of the function. -> ([Operand] -> IRBuilderC m ()) -- ^ A function that builds the function's basic blocks from its arguments. -> m Operand -function nm argTys retTy body = do +function nm argTys retTy link body = do (blocks, paramNames) <- runIRBuilder emptyIRBuilder $ do paramNames <- traverse (const fresh) argTys body $ zipWith LocalReference argTys paramNames @@ -71,6 +73,7 @@ function nm argTys retTy body = do = (($ []) <$> zipWith Parameter argTys paramNames, False) , returnType = retTy , basicBlocks = blocks + , linkage = link } funTy = ptr $ FunctionType retTy argTys False ConstantOperand (GlobalReference funTy nm) <$ emitDefn def diff --git a/src/Language/Elemental.hs b/src/Language/Elemental.hs index b46f3b2..8a543b7 100644 --- a/src/Language/Elemental.hs +++ b/src/Language/Elemental.hs @@ -33,6 +33,7 @@ module Language.Elemental -- * Emitting -- $emitting , module Language.Elemental.Emit + , module Language.Elemental.InteractionNet ) where import Data.Version (Version) @@ -45,6 +46,7 @@ import Language.Elemental.AST.Type import Language.Elemental.AST.Unchecked import Language.Elemental.Diagnostic import Language.Elemental.Emit +import Language.Elemental.InteractionNet import Language.Elemental.Location import Language.Elemental.Parser import Language.Elemental.Pretty @@ -116,7 +118,11 @@ version = Paths.version -} {- $emitting - Programs can be emitted as LLVM using 'emitProgram'. + Programs can be emitted as interaction nets using 'emitProgram'. These can + then be compiled with 'compileINet'. This will output a generic backend + representation, which can finally be converted into LLVM using + "Language.Elemental.Backend.LLVM" or into some other target language by + manually folding the representation. The compiler also exposes its other emitting functions, however their interface may be more volatile as there's no clear use case for them. diff --git a/src/Language/Elemental/AST/Expr.hs b/src/Language/Elemental/AST/Expr.hs index 1b6cfb8..882c0c5 100644 --- a/src/Language/Elemental/AST/Expr.hs +++ b/src/Language/Elemental/AST/Expr.hs @@ -33,13 +33,14 @@ module Language.Elemental.AST.Expr , pattern (:@) , pattern (:\) -- * Marshalling - , LlvmOperandType + , BackendOperandType , IsOpType , sIsOpType , AllIsOpType , sAllIsOpType , HasForeignType(..) , ForeignType + , sForeignType , BuildForeignType , sBuildForeignType , MarshallableType(..) @@ -53,6 +54,7 @@ module Language.Elemental.AST.Expr , exprType , IncrementAll , sIncrementAll + , sIncrementAll' , SubstituteAll , sSubstituteAll , incrementExpr @@ -76,15 +78,13 @@ module Language.Elemental.AST.Expr import Data.Data import Data.Kind qualified as Kind import Data.Void (absurd) -import LLVM.AST qualified as LLVM -import LLVM.AST.Constant qualified as LLVM.Constant import Numeric (showHex) import Numeric.Natural (Natural) import Prettyprinter import Unsafe.Coerce qualified as Unsafe -import Control.Effect.IRBuilder import Language.Elemental.AST.Type +import Language.Elemental.Backend qualified as Backend import Language.Elemental.Singleton @@ -119,15 +119,21 @@ data Expr tscope scope t where :: (MarshallableType tx, IsOpType (Marshall tx) ~ 'True) => Address -> SPointerKind pk -> SType tscope tx -> Expr tscope scope ('PointerType pk tx) - -- | A pure LLVM operand. This is an internal expression. - LlvmOperand - :: SLlvmType lt -> LlvmOperandType lt - -> Expr tscope scope ('LlvmType lt) - -- | An LLVM operand in @IO@. This is an internal expression. - LlvmIO - :: SLlvmType lt - -> (forall sig m. Has IRBuilder sig m => m (LlvmOperandType lt)) - -> Expr tscope scope ('IOType ('LlvmType lt)) + -- | A pure backend operand. This is an internal expression. + BackendOperand + :: SBackendType lt -> Backend.Operand + -> Expr tscope scope ('BackendType lt) + -- | An backend operand in @IO@. This is an internal expression. + BackendIO + :: SBackendType lt + -- -> (forall sig m. Has IRBuilder sig m => m (BackendOperandType lt)) + -> Backend.Instruction + -> Expr tscope scope ('IOType ('BackendType lt)) + -- TODO: Merge with v'Call'. + BackendPIO + :: SBackendType lta -> SBackendType lt + -> (Backend.Operand -> Backend.Instruction) + -> Expr tscope scope ('BackendType lta :-> 'IOType ('BackendType lt)) -- | The @pureIO@ primitive. This is an internal expression. PureIO :: Expr tscope scope PureIOType -- | The @bindIO@ primitive. This is an internal expression. @@ -138,21 +144,24 @@ data Expr tscope scope t where StorePointer :: Expr tscope scope StorePointerType -- | A call of a foreign function. This is an internal expression. Call - :: AllIsOpType ltargs ~ 'True => LLVM.CallableOperand -> [LLVM.Operand] - -> SList SLlvmType ltargs -> SLlvmType ltret + :: AllIsOpType ltargs ~ 'True => Backend.ForeignName + -> SList SBackendType ltargs -> SBackendType ltret -> Expr tscope scope (BuildForeignType ltargs ltret) -- | Extracts a single bit from an integer. This is an internal expression. IsolateBit :: CmpNat idx size ~ 'LT => SNat idx -> SNat size -> Expr tscope scope - ('LlvmType ('LlvmInt size) :-> 'LlvmType ('LlvmInt ('Succ 'Zero))) + ( 'BackendType ('BackendInt size) + :-> 'BackendType ('BackendInt ('Succ 'Zero)) + ) -- | Inserts a bit as the MSB of an integer. This is an internal expression. InsertBit :: SNat size -> Expr tscope scope - ('LlvmType ('LlvmInt ('Succ 'Zero)) :-> 'LlvmType ('LlvmInt size) - :-> 'LlvmType ('LlvmInt ('Succ size))) - -- | Converts an LLVM @i1@ into a 'BitType'. This is an internal expression. - TestBit - :: Expr tscope scope ('LlvmType ('LlvmInt ('Succ 'Zero))) - -> Expr tscope scope BitType + ( 'BackendType ('BackendInt ('Succ 'Zero)) + :-> 'BackendType ('BackendInt size) + :-> 'BackendType ('BackendInt ('Succ size)) + ) + -- | Converts an @i1@ into a 'BitType'. This is an internal expression. + TestBit :: Expr tscope scope + ('BackendType ('BackendInt ('Succ 'Zero)) :-> 'IOType BitType) -- | Pointer addresses in the AST. newtype Address = Address { getAddress :: Natural } @@ -198,58 +207,81 @@ pattern (:\) pattern tx :\ ey = Lam tx ey infixr 0 :\ --- | Type synonym to convert any t'LlvmType' into its compiler representation. -type LlvmOperandType :: LlvmType -> Kind.Type -type LlvmOperandType lt = If (IsOpType lt) LLVM.Operand () +-- | Type synonym to convert a t'BackendType' into its compiler representation. +type BackendOperandType :: BackendType -> Kind.Type +type BackendOperandType lt = If (IsOpType lt) Backend.Operand () --- | Is the t'LlvmType' a legal LLVM operand type? Notably, @void@ is not. -type IsOpType :: LlvmType -> Bool +-- | Is the t'BackendType' a legal backend operand type? Notably, @i0@ is not. +type IsOpType :: BackendType -> Bool type family IsOpType lt where - IsOpType ('LlvmInt size) = SwitchOrd (CmpNat size 'Zero) Stuck 'False 'True + IsOpType ('BackendInt size) + = SwitchOrd (CmpNat size 'Zero) Stuck 'False 'True -- | Singleton version of 'IsOpType'. -sIsOpType :: SLlvmType lt -> SBool (IsOpType lt) -sIsOpType (SLlvmInt size) = case sCmpNat size SZero of +sIsOpType :: SBackendType lt -> SBool (IsOpType lt) +sIsOpType (SBackendInt size) = case sCmpNat size SZero of SLT -> absurd $ zeroNoLT size Refl SEQ -> SFalse SGT -> STrue --- | Is every t'LlvmType' in a list a legal LLVM operand type? -type AllIsOpType :: [LlvmType] -> Bool +-- | Is every t'BackendType' in a list a legal backend operand type? +type AllIsOpType :: [BackendType] -> Bool type family AllIsOpType lts where AllIsOpType '[] = 'True AllIsOpType (lt ': lts) = IsOpType lt && AllIsOpType lts -- | Singleton version of 'AllIsOpType'. -sAllIsOpType :: SList SLlvmType lts -> SBool (AllIsOpType lts) +sAllIsOpType :: SList SBackendType lts -> SBool (AllIsOpType lts) sAllIsOpType SNil = STrue sAllIsOpType (lt :^ lts) = sIsOpType lt &&^ sAllIsOpType lts -- | The type has an isomorphic foreign type. type HasForeignType :: Type -> Kind.Constraint class AllIsOpType (ForeignArgs t) ~ 'True => HasForeignType t where - -- | The argument t'LlvmType' of the foreign type. - type ForeignArgs t :: [LlvmType] + -- | The argument t'BackendType' of the foreign type. + type ForeignArgs t :: [BackendType] -- | Singleton version of 'ForeignArgs'. - sForeignArgs :: SType tscope t -> SList SLlvmType (ForeignArgs t) + sForeignArgs :: SType tscope t -> SList SBackendType (ForeignArgs t) - -- | The return t'LlvmType' of the foreign type. - type ForeignRet t :: LlvmType + -- | The return t'BackendType' of the foreign type. + type ForeignRet t :: BackendType -- | Singleton version of 'ForeignRet'. - sForeignRet :: SType tscope t -> SLlvmType (ForeignRet t) + sForeignRet :: SType tscope t -> SBackendType (ForeignRet t) + + -- | The return t'Type' of the Elemental type. + type InternalRet t :: Type + + -- | Singleton version of 'InternalRet'. + sInternalRet :: SType tscope t -> SType tscope (InternalRet t) -- | Wraps the foreign type into the native type. wrapImport - :: SNat tscope -> SList (SType tscope) scope - -> SType tscope t -> Expr tscope scope (ForeignType t) - -> Expr tscope scope t - + :: SNat tscope -> SList (SType tscope) scope -> SType tscope t + -> Expr tscope scope (ForeignType t) -> Expr tscope scope t + -- | Wraps the native type into the foreign type. wrapExport - :: SNat tscope -> SList (SType tscope) scope - -> SType tscope t -> Expr tscope scope t + :: SNat tscope -> SList (SType tscope) scope -> SType tscope t + -> Expr tscope scope t -> Expr tscope scope (ForeignType t) + + -- | Lifts an IO bind into the foreign type. + bindImport + :: SNat tscope -> SList (SType tscope) scope -> SType tscope t + -> Expr tscope scope ('IOType tx) + -> (forall scope'. SList (SType tscope) scope' + -> (forall tr. Expr tscope scope tr -> Expr tscope scope' tr) + -> Expr tscope scope' tx -> Expr tscope scope' t) + -> Expr tscope scope t + + -- | Lifts an IO bind into the foreign type. + bindExport + :: SNat tscope -> SList (SType tscope) scope -> SType tscope t + -> Expr tscope scope ('IOType tx) + -> (forall scope'. SList (SType tscope) scope' + -> (forall tr. Expr tscope scope tr -> Expr tscope scope' tr) + -> Expr tscope scope' tx -> Expr tscope scope' (ForeignType t)) -> Expr tscope scope (ForeignType t) instance MarshallableType t => HasForeignType ('IOType t) where @@ -259,19 +291,41 @@ instance MarshallableType t => HasForeignType ('IOType t) where type ForeignRet ('IOType t) = Marshall t sForeignRet (SIOType t) = sMarshall t - wrapImport tscope scope (SIOType t) x = BindIO :@ t' :$ x :@ t :$ (t' - :\ PureIO :@ t - :$ marshallIn tscope (t' :^ scope) t (Var SZero)) + type InternalRet ('IOType t) = t + sInternalRet (SIOType t) = t + + wrapImport tscope scope (SIOType t) x = BindIO + :@ bt :$ x + :@ t :$ (bt :\ marshallIn tscope (bt :^ scope) t (Var SZero)) where - t' = SLlvmType $ sMarshall t + bt = SBackendType $ sMarshall t wrapExport tscope scope (SIOType (t :: SType tscope tx)) x = withProof (subIncElim tscope SZero t' t Refl) $ BindIO :@ t :$ x :@ t' :$ (t :\ PureIO :@ t' :$ marshallOut tscope (t :^ scope) t (Var SZero)) where - t' :: SType tscope ('LlvmType (Marshall tx)) - t' = SLlvmType $ sMarshall t + t' :: SType tscope ('BackendType (Marshall tx)) + t' = SBackendType $ sMarshall t + + bindImport tscope scope (SIOType t) ex cont + = withProof (subIncElim tscope SZero t (SIOType tx) Refl) + $ withProof (insZeroP tx scope) + $ BindIO :@ tx :$ ex :@ t :$ (tx :\ cont (tx :^ scope) + (incrementExpr tscope scope SZero tx) (Var SZero)) + where + SIOType tx = exprType tscope scope ex + + bindExport tscope scope (SIOType (t :: SType tscope t)) ex cont + = withProof (subIncElim tscope SZero t' (SIOType tx) Refl) + $ withProof (insZeroP tx scope) + $ BindIO :@ tx :$ ex :@ t' :$ (tx :\ cont (tx :^ scope) + (incrementExpr tscope scope SZero tx) (Var SZero)) + where + SIOType tx = exprType tscope scope ex + + t' :: SType tscope ('BackendType (Marshall t)) + t' = SBackendType $ sMarshall t instance (MarshallableType tx, IsOpType (Marshall tx) ~ 'True , HasForeignType ty) => HasForeignType (tx :-> ty) @@ -282,60 +336,89 @@ instance (MarshallableType tx, IsOpType (Marshall tx) ~ 'True type ForeignRet (_ :-> ty) = ForeignRet ty sForeignRet (SArrow _ ty) = sForeignRet ty + type InternalRet (_ :-> ty) = InternalRet ty + sInternalRet (SArrow _ ty) = sInternalRet ty + wrapImport tscope scope (SArrow tx ty) x = tx :\ wrapImport tscope (tx :^ scope) ty ( withProof (insZeroP tx scope) $ incrementExpr tscope scope SZero tx x :$ marshallOut tscope (tx :^ scope) tx (Var SZero) ) - - wrapExport tscope scope (SArrow tx ty) x = tx' - :\ wrapExport tscope (tx' :^ scope) ty - (withProof (insZeroP tx' scope) - $ incrementExpr tscope scope SZero tx' x - :$ marshallIn tscope (tx' :^ scope) tx (Var SZero) - ) + + wrapExport tscope scope (SArrow tx ty) ex = withProof (insZeroP tx' scope) + $ tx' :\ bindExport tscope scope' ty + (marshallIn tscope scope' tx $ Var SZero) + (\sc inc ey -> wrapExport tscope sc ty + $ inc (incrementExpr tscope scope SZero tx' ex) :$ ey) where - tx' = SLlvmType $ sMarshall tx + tx' = SBackendType $ sMarshall tx + scope' = tx' :^ scope + + bindImport tscope scope (SArrow tx ty) ex ef = withProof (insZeroP tx scope) + $ tx :\ bindImport tscope (tx :^ scope) ty + (incrementExpr tscope scope SZero tx ex) + (\scope' inc' ey + -> ef scope' (inc' . incrementExpr tscope scope SZero tx) ey + :$ inc' (Var SZero)) + + bindExport tscope scope (SArrow (tx :: SType tscope tx) ty) ex ef + = withProof (insZeroP tx' scope) + $ tx' :\ bindExport tscope (tx' :^ scope) ty + (incrementExpr tscope scope SZero tx' ex) + (\scope' inc' ey + -> ef scope' (inc' . incrementExpr tscope scope SZero tx') ey + :$ inc' (Var SZero)) + where + tx' :: SType tscope ('BackendType (Marshall tx)) + tx' = SBackendType $ sMarshall tx -- | The foreign type corresponding to a native type. type ForeignType t = BuildForeignType (ForeignArgs t) (ForeignRet t) --- | Builds a type from a list of argument t'LlvmType' and a return t'LlvmType'. -type BuildForeignType :: [LlvmType] -> LlvmType -> Type +-- | Singleton version of 'ForeignType'. +sForeignType + :: HasForeignType t => SType tscope t -> SType tscope (ForeignType t) +sForeignType t = sBuildForeignType (sForeignArgs t) (sForeignRet t) + +{-| + Builds a type from a list of argument t'BackendType' and a return + t'BackendType'. +-} +type BuildForeignType :: [BackendType] -> BackendType -> Type type family BuildForeignType ltargs ltret where - BuildForeignType '[] ltret = 'IOType ('LlvmType ltret) + BuildForeignType '[] ltret = 'IOType ('BackendType ltret) BuildForeignType (ltarg ': ltargs) ltret - = 'LlvmType ltarg :-> BuildForeignType ltargs ltret + = 'BackendType ltarg :-> BuildForeignType ltargs ltret -- | Singleton version of 'BuildForeignType'. sBuildForeignType - :: SList SLlvmType ltargs -> SLlvmType ltret + :: SList SBackendType ltargs -> SBackendType ltret -> SType tscope (BuildForeignType ltargs ltret) -sBuildForeignType SNil ltret = SIOType $ SLlvmType ltret +sBuildForeignType SNil ltret = SIOType $ SBackendType ltret sBuildForeignType (ltarg :^ ltargs) ltret - = SLlvmType ltarg :-> sBuildForeignType ltargs ltret + = SBackendType ltarg :-> sBuildForeignType ltargs ltret --- | The type is isomorphic to and can be marshalled to and from an t'LlvmType'. +-- | The type is isomorphic to a t'BackendType'. type MarshallableType :: Type -> Kind.Constraint class t ~ Unmarshall (Marshall t) => MarshallableType t where - -- | The t'LlvmType' corresponding to a native type. - type Marshall t :: LlvmType + -- | The t'BackendType' corresponding to a native type. + type Marshall t :: BackendType -- | Singleton version of 'Marshall'. - sMarshall :: SType scope t -> SLlvmType (Marshall t) + sMarshall :: SType scope t -> SBackendType (Marshall t) - -- | Marshalls an expression from the t'LlvmType' to the native type. + -- | Marshalls an expression from the t'BackendType' to the native type. marshallIn :: SNat tscope -> SList (SType tscope) scope -> SType tscope t - -> Expr tscope scope ('LlvmType (Marshall t)) - -> Expr tscope scope t + -> Expr tscope scope ('BackendType (Marshall t)) + -> Expr tscope scope ('IOType t) - -- | Marshalls an expression from the native type to the t'LlvmType'. + -- | Marshalls an expression from the native type to the t'BackendType'. marshallOut :: SNat tscope -> SList (SType tscope) scope -> SType tscope t -> Expr tscope scope t - -> Expr tscope scope ('LlvmType (Marshall t)) + -> Expr tscope scope ('BackendType (Marshall t)) -- | Proof that 'Increment' is a no-op, i.e. the type is closed. incMarshall @@ -348,28 +431,30 @@ class t ~ Unmarshall (Marshall t) => MarshallableType t where -> t :~: Substitute idx tsub t instance MarshallableType UnitType where - type Marshall UnitType = 'LlvmInt 'Zero - sMarshall _ = SLlvmInt SZero + type Marshall UnitType = 'BackendInt 'Zero + sMarshall _ = SBackendInt SZero - marshallIn _ _ _ _ = TypeLam $ STypeVar SZero :\ Var SZero + marshallIn _ _ _ _ + = PureIO :@ SUnitType :$ TypeLam (STypeVar SZero :\ Var SZero) - marshallOut _ _ _ _ = LlvmOperand (SLlvmInt SZero) () + marshallOut _ _ _ = (:$ BackendOperand (SBackendInt SZero) Backend.Empty) + . (:@ SBackendType (SBackendInt SZero)) incMarshall _ _ = Refl subMarshall _ _ _ = Refl instance MarshallableType BitType where - type Marshall BitType = 'LlvmInt ('Succ 'Zero) - sMarshall _ = SLlvmInt $ SSucc SZero + type Marshall BitType = 'BackendInt ('Succ 'Zero) + sMarshall _ = SBackendInt $ SSucc SZero - marshallIn _ _ _ = TestBit + marshallIn _ _ _ = (TestBit :$) - marshallOut _ _ _ x = x :@ SLlvmType lt - :$ LlvmOperand lt (LLVM.ConstantOperand $ LLVM.Constant.Int 1 1) - :$ LlvmOperand lt (LLVM.ConstantOperand $ LLVM.Constant.Int 1 0) + marshallOut _ _ _ x = x :@ SBackendType lt + :$ BackendOperand lt (Backend.Constant Backend.B1) + :$ BackendOperand lt (Backend.Constant Backend.B0) where - lt = SLlvmInt $ SSucc SZero + lt = SBackendInt $ SSucc SZero incMarshall _ _ = Refl @@ -379,37 +464,52 @@ instance (t ~ BitTuple (ArgCount t), ArgCount t ~ 'Succ _n) => MarshallableType ('Forall ((BitType :-> t) :-> 'TypeVar 'Zero)) where type Marshall ('Forall ((BitType :-> t) :-> 'TypeVar 'Zero)) - = 'LlvmInt ('Succ (ArgCount t)) - sMarshall (SForall (SArrow t _)) = SLlvmInt $ sArgCount t - - marshallIn tscope scope t x = TypeLam $ tx :\ withProof (ltSucc size) - ( withProof (insZeroP tx scope') - $ marshallTuple (SSucc tscope) (tx :^ scope') size size - ( withProof (insZeroP tx scope') - $ incrementExpr (SSucc tscope) scope' SZero tx - $ incrementExprType tscope scope SZero x - ) - $ Var SZero - ) + = 'BackendInt ('Succ (ArgCount t)) + sMarshall (SForall (SArrow t _)) = SBackendInt $ sArgCount t + + marshallIn tscope scope t x = withProof (ltSucc size) + $ marshallTuple tscope scope size size t x $ \_ _ cont + -> PureIO :@ t :$ TypeLam (tx :\ cont (Var SZero)) where size = sArgCount tx SForall (SArrow tx _) = t - scope' = sIncrementAll tscope SZero scope marshallTuple - :: forall tscope scope n size. (CmpNat n ('Succ size) ~ 'LT) - => SNat ('Succ tscope) -> SList (SType ('Succ tscope)) scope - -> SNat n -> SNat size - -> Expr ('Succ tscope) scope ('LlvmType ('LlvmInt size)) - -> Expr ('Succ tscope) scope (BitTuple n) - -> Expr ('Succ tscope) scope ('TypeVar 'Zero) - marshallTuple _ _ SZero _ _ er = er - marshallTuple tsc sc (SSucc idx) size' ex er - = withProof (ltSuccLToLT idx (SSucc size') Refl) - $ marshallTuple tsc sc idx size' ex - $ er :$ marshallIn tsc sc SBitType (IsolateBit idx size' :$ ex) - - marshallOut tscope scope t x = x :@ SLlvmType (sMarshall t) + :: forall tscope scope n size tr. (CmpNat n ('Succ size) ~ 'LT) + => SNat tscope -> SList (SType tscope) scope + -> SNat n -> SNat size -> SType tscope tr + -> Expr tscope scope ('BackendType ('BackendInt size)) + -> (forall scope'. SList (SType tscope) scope' + -> (forall tx. Expr ('Succ tscope) (IncrementAll 'Zero scope) tx + -> Expr ('Succ tscope) + (BitTuple size ': IncrementAll 'Zero scope') tx) + -> (Expr ('Succ tscope) + (BitTuple size ': IncrementAll 'Zero scope') (BitTuple n) + -> Expr ('Succ tscope) + (BitTuple size ': IncrementAll 'Zero scope') + ('TypeVar 'Zero)) + -> Expr tscope scope' ('IOType tr)) + -> Expr tscope scope ('IOType tr) + marshallTuple tsc sc SZero size' _ _ cont + = withProof (insZeroP (sBitTuple size') + $ sIncrementAll tsc SZero sc) + $ cont sc (incrementExpr (SSucc tsc) (sIncrementAll tsc SZero sc) + SZero $ sBitTuple size') id + marshallTuple tsc sc (SSucc idx) size' tr ex cont = BindIO + :@ SBitType :$ marshallIn tsc sc SBitType + (IsolateBit idx size' :$ ex) + :@ tr :$ withProof (ltSuccLToLT idx (SSucc size') Refl) (withProof + (insZeroP SBitType $ sIncrementAll tsc SZero sc) + $ withProof (insZeroP SBitType sc) + $ SBitType + :\ marshallTuple tsc (SBitType :^ sc) idx size' tr + (incrementExpr tsc sc SZero SBitType ex) + (\sc' inc cont' -> cont sc' + (inc . incrementExpr (SSucc tsc) + (sIncrementAll tsc SZero sc) SZero SBitType) + $ \er -> cont' $ er :$ inc (Var SZero))) + + marshallOut tscope scope t x = x :@ SBackendType (sMarshall t) :$ marshallTuple tscope scope size (const $ const id) where size = sArgCount tx @@ -420,10 +520,11 @@ instance (t ~ BitTuple (ArgCount t), ArgCount t ~ 'Succ _n) -> SNat size -> (forall scope'. SList (SType tscope) scope' -> (forall t2. Expr tscope scope t2 -> Expr tscope scope' t2) - -> Expr tscope scope' ('LlvmType ('LlvmInt size)) + -> Expr tscope scope' ('BackendType ('BackendInt size)) -> Expr tscope scope' tr) -> Expr tscope scope (Substitute 'Zero tr (BitTuple size)) - marshallTuple _ sc SZero f = f sc id $ LlvmOperand (SLlvmInt SZero) () + marshallTuple _ sc SZero f + = f sc id $ BackendOperand (SBackendInt SZero) Backend.Empty marshallTuple tsc sc (SSucc size') f = SBitType :\ marshallTuple tsc (SBitType :^ sc) size' (\sc' inc ex -> f sc' (withProof (insZero @BitType sc) @@ -478,23 +579,24 @@ sArgCount (SArrow _ tr) = SSucc $ sArgCount tr sArgCount (SForall _) = SZero sArgCount (SIOType _) = SZero sArgCount (SPointerType _ _) = SZero -sArgCount (SLlvmType _) = SZero +sArgCount (SBackendType _) = SZero {-| - Converts an t'LlvmType' to an isomorphic native type. Inverse of 'Marshall'. + Converts a t'BackendType' to an isomorphic native type. Inverse of + 'Marshall'. -} -type Unmarshall :: LlvmType -> Type +type Unmarshall :: BackendType -> Type type family Unmarshall lt where - Unmarshall ('LlvmInt 'Zero) = 'Forall ('TypeVar 'Zero :-> 'TypeVar 'Zero) - Unmarshall ('LlvmInt ('Succ 'Zero)) = BitType - Unmarshall ('LlvmInt size) = 'Forall (BitTuple size :-> 'TypeVar 'Zero) + Unmarshall ('BackendInt 'Zero) = 'Forall ('TypeVar 'Zero :-> 'TypeVar 'Zero) + Unmarshall ('BackendInt ('Succ 'Zero)) = BitType + Unmarshall ('BackendInt size) = 'Forall (BitTuple size :-> 'TypeVar 'Zero) -- | Singleton version of 'Unmarshall'. -sUnmarshall :: SLlvmType lt -> SType tscope (Unmarshall lt) -sUnmarshall (SLlvmInt SZero) = SForall $ STypeVar SZero :-> STypeVar SZero -sUnmarshall (SLlvmInt (SSucc SZero)) +sUnmarshall :: SBackendType lt -> SType tscope (Unmarshall lt) +sUnmarshall (SBackendInt SZero) = SForall $ STypeVar SZero :-> STypeVar SZero +sUnmarshall (SBackendInt (SSucc SZero)) = SForall $ STypeVar SZero :-> STypeVar SZero :-> STypeVar SZero -sUnmarshall (SLlvmInt size@(SSucc (SSucc _))) +sUnmarshall (SBackendInt size@(SSucc (SSucc _))) = SForall $ sBitTuple size :-> STypeVar SZero -- | Gets the type of an expression. @@ -511,8 +613,9 @@ exprType tscope scope = \case TypeLam ex -> SForall $ exprType (SSucc tscope) (sIncrementAll tscope SZero scope) ex Addr _ pk tx -> SPointerType pk tx - LlvmOperand lt _ -> SLlvmType lt - LlvmIO lt _ -> SIOType $ SLlvmType lt + BackendOperand lt _ -> SBackendType lt + BackendIO lt _ -> SIOType $ SBackendType lt + BackendPIO lta lt _ -> SBackendType lta :-> SIOType (SBackendType lt) PureIO -> SForall $ STypeVar SZero :-> SIOType (STypeVar SZero) BindIO -> SForall $ SIOType (STypeVar SZero) :-> SForall ((STypeVar (SSucc SZero) :-> SIOType (STypeVar SZero)) @@ -521,13 +624,13 @@ exprType tscope scope = \case :-> SIOType (STypeVar SZero) StorePointer -> SForall $ SPointerType SWritePointer (STypeVar SZero) :-> STypeVar SZero :-> SIOType SUnitType - Call _ _ ltargs ltret -> sBuildForeignType ltargs ltret - IsolateBit _ size - -> SLlvmType (SLlvmInt size) :-> SLlvmType (SLlvmInt $ SSucc SZero) - InsertBit size -> SLlvmType (SLlvmInt $ SSucc SZero) - :-> SLlvmType (SLlvmInt size) - :-> SLlvmType (SLlvmInt (SSucc size)) - TestBit _ -> SBitType + Call _ ltargs ltret -> sBuildForeignType ltargs ltret + IsolateBit _ size -> SBackendType (SBackendInt size) + :-> SBackendType (SBackendInt $ SSucc SZero) + InsertBit size -> SBackendType (SBackendInt $ SSucc SZero) + :-> SBackendType (SBackendInt size) + :-> SBackendType (SBackendInt (SSucc size)) + TestBit -> SBackendType (SBackendInt $ SSucc SZero) :-> SIOType SBitType -- | Increments every type in a list. type IncrementAll :: Nat -> [Type] -> [Type] @@ -539,9 +642,14 @@ type family IncrementAll idx ts where sIncrementAll :: SNat scope -> SNat idx -> SList (SType scope) ts -> SList (SType ('Succ scope)) (IncrementAll idx ts) -sIncrementAll _ _ SNil = SNil -sIncrementAll scope idx (t :^ ts) - = sIncrement scope idx t :^ sIncrementAll scope idx ts +sIncrementAll scope idx = sIncrementAll' (sIncrement scope idx) idx + +-- | Generalised version of 'sIncrementAll'. +sIncrementAll' + :: (forall t. proxy t -> proxy' (Increment idx t)) + -> SNat idx -> SList proxy ts -> SList proxy' (IncrementAll idx ts) +sIncrementAll' _ _ SNil = SNil +sIncrementAll' inc idx (t :^ ts) = inc t :^ sIncrementAll' inc idx ts -- | Substitutes every type in a list. type SubstituteAll :: Nat -> Type -> [Type] -> [Type] @@ -584,16 +692,17 @@ incrementExpr tscope scope idx tnew = \case $ incrementExpr (SSucc tscope) (sIncrementAll tscope SZero scope) idx (Proxy @(Increment 'Zero tnew)) ex Addr addr pk tx -> Addr addr pk tx - LlvmOperand lt op -> LlvmOperand lt op - LlvmIO lt op -> LlvmIO lt op + BackendOperand lt op -> BackendOperand lt op + BackendIO lt op -> BackendIO lt op + BackendPIO lta lt pio -> BackendPIO lta lt pio PureIO -> PureIO BindIO -> BindIO LoadPointer -> LoadPointer StorePointer -> StorePointer - Call fop aops ltargs ltret -> Call fop aops ltargs ltret + Call fop ltargs ltret -> Call fop ltargs ltret IsolateBit bidx size -> IsolateBit bidx size InsertBit size -> InsertBit size - TestBit ex -> TestBit $ incrementExpr tscope scope idx tnew ex + TestBit -> TestBit -- | Substitutes a variable at the given index. substituteExpr @@ -632,16 +741,17 @@ substituteExpr tscope scope idx sub = \case $ substituteExpr (SSucc tscope) (sIncrementAll tscope SZero scope) idx (incrementExprType tscope (sRemove idx scope) SZero sub) ex Addr addr pk tx -> Addr addr pk tx - LlvmOperand lt op -> LlvmOperand lt op - LlvmIO lt op -> LlvmIO lt op + BackendOperand lt op -> BackendOperand lt op + BackendIO lt op -> BackendIO lt op + BackendPIO lta lt pio -> BackendPIO lta lt pio PureIO -> PureIO BindIO -> BindIO LoadPointer -> LoadPointer StorePointer -> StorePointer - Call fop aops ltargs ltret -> Call fop aops ltargs ltret + Call fop ltargs ltret -> Call fop ltargs ltret IsolateBit bidx size -> IsolateBit bidx size InsertBit size -> InsertBit size - TestBit ex -> TestBit $ substituteExpr tscope scope idx sub ex + TestBit -> TestBit -- | Introduces a type variable at the given type index. incrementExprType @@ -669,17 +779,18 @@ incrementExprType tscope scope idx = \case (SSucc idx) ex Addr addr pk tx -> withProof (incMarshall idx tx) $ Addr addr pk $ sIncrement tscope idx tx - LlvmOperand lt op -> LlvmOperand lt op - LlvmIO lt op -> LlvmIO lt op + BackendOperand lt op -> BackendOperand lt op + BackendIO lt op -> BackendIO lt op + BackendPIO lta lt pio -> BackendPIO lta lt pio PureIO -> PureIO BindIO -> BindIO LoadPointer -> LoadPointer StorePointer -> StorePointer - Call fop aops ltargs ltret -> withProof (incForeign idx ltargs ltret) - $ Call fop aops ltargs ltret + Call fop ltargs ltret -> withProof (incForeign idx ltargs ltret) + $ Call fop ltargs ltret IsolateBit bidx size -> IsolateBit bidx size InsertBit size -> InsertBit size - TestBit ex -> TestBit $ incrementExprType tscope scope idx ex + TestBit -> TestBit -- | Substitutes a type variable at the given type index. substituteExprType @@ -707,17 +818,18 @@ substituteExprType tscope scope idx tsub = withProofs $ \case (sIncrement tscope SZero tsub) ex Addr addr pk tx -> withProof (subMarshall idx tsub tx) $ Addr addr pk $ sSubstitute tscope idx tsub tx - LlvmOperand lt op -> LlvmOperand lt op - LlvmIO lt op -> LlvmIO lt op + BackendOperand lt op -> BackendOperand lt op + BackendIO lt op -> BackendIO lt op + BackendPIO lta lt pio -> BackendPIO lta lt pio PureIO -> PureIO BindIO -> BindIO LoadPointer -> LoadPointer StorePointer -> StorePointer - Call fop aops ltargs ltret -> withProof (subForeign idx tsub ltargs ltret) - $ Call fop aops ltargs ltret + Call fop ltargs ltret -> withProof (subForeign idx tsub ltargs ltret) + $ Call fop ltargs ltret IsolateBit bidx size -> IsolateBit bidx size InsertBit size -> InsertBit size - TestBit ex -> TestBit $ substituteExprType tscope scope idx tsub ex + TestBit -> TestBit where {- Adding @@ -880,3 +992,4 @@ countBitTuple (SSucc size) = withProof (countBitTuple size) Refl {-# RULES "Proof/countBitTuple" countBitTuple = \_ -> Unsafe.unsafeCoerce Refl #-} {-# INLINE [1] countBitTuple #-} + diff --git a/src/Language/Elemental/AST/Type.hs b/src/Language/Elemental/AST/Type.hs index 7423ff0..68b3025 100644 --- a/src/Language/Elemental/AST/Type.hs +++ b/src/Language/Elemental/AST/Type.hs @@ -18,8 +18,8 @@ module Language.Elemental.AST.Type , SType(..) , PointerKind(..) , SPointerKind(..) - , LlvmType(..) - , SLlvmType(..) + , BackendType(..) + , SBackendType(..) -- * Synonyms , UnitType , pattern SUnitType @@ -62,8 +62,8 @@ data Type | IOType Type -- | A pointer to data of the contained type. | PointerType PointerKind Type - -- | An LLVM operand of the given type. This is an internal type. - | LlvmType LlvmType + -- | A backend operand of the given type. This is an internal type. + | BackendType BackendType {-| Singleton for 'Type'. Used to witness an Elemental type at runtime. @@ -83,8 +83,8 @@ data SType scope t where -- | Singleton constructor for 'PointerType'. SPointerType :: SPointerKind pk -> SType scope tx -> SType scope ('PointerType pk tx) - -- | Singleton constructor for v'LlvmType'. - SLlvmType :: SLlvmType lt -> SType scope ('LlvmType lt) + -- | Singleton constructor for v'BackendType'. + SBackendType :: SBackendType lt -> SType scope ('BackendType lt) {-| The kind of pointer kinds in the AST. Used to annotate pointers with @@ -105,16 +105,16 @@ data SPointerKind pk where -- | Singleton constructor for 'WritePointer'. SWritePointer :: SPointerKind 'WritePointer --- | The subset of LLVM types used internally when emitting LLVM. -newtype LlvmType - -- | An LLVM integer of the given size. A size of 0 is used for @void@. - = LlvmInt Nat +-- | The subset of Backend types used internally when emitting. +newtype BackendType + -- | A backend integer of the given size. + = BackendInt Nat --- | Singleton for t'LlvmType'. Used to witness an LLVM type at runtime. -type SLlvmType :: LlvmType -> Kind.Type -data SLlvmType lt where - -- | Singleton constructor for 'LlvmInt'. - SLlvmInt :: SNat size -> SLlvmType ('LlvmInt size) +-- | Singleton for t'BackendType'. Used to witness a backend type at runtime. +type SBackendType :: BackendType -> Kind.Type +data SBackendType lt where + -- | Singleton constructor for 'BackendInt'. + SBackendInt :: SNat size -> SBackendType ('BackendInt size) -- | The Elemental unit type. Used to encode a @void@ return in the FFI. type UnitType = 'Forall ('TypeVar 'Zero :-> 'TypeVar 'Zero) @@ -159,7 +159,7 @@ type family Increment idx t where Increment idx ('Forall tx) = 'Forall (Increment ('Succ idx) tx) Increment idx ('IOType tx) = 'IOType (Increment idx tx) Increment idx ('PointerType pk tx) = 'PointerType pk (Increment idx tx) - Increment _ ('LlvmType lt) = 'LlvmType lt + Increment _ ('BackendType lt) = 'BackendType lt -- | Singleton version of 'Increment'. sIncrement @@ -176,7 +176,7 @@ sIncrement scope idx = \case SForall tx -> SForall $ sIncrement (SSucc scope) (SSucc idx) tx SIOType tx -> SIOType $ sIncrement scope idx tx SPointerType pk tx -> SPointerType pk $ sIncrement scope idx tx - SLlvmType lt -> SLlvmType lt + SBackendType lt -> SBackendType lt {-| Substitutes a type at the given index. The first type is the substituted @@ -193,7 +193,7 @@ type family Substitute idx tsub t where Substitute idx tsub ('IOType tx) = 'IOType (Substitute idx tsub tx) Substitute idx tsub ('PointerType pk tx) = 'PointerType pk (Substitute idx tsub tx) - Substitute idx tsub ('LlvmType lt) = 'LlvmType lt + Substitute idx tsub ('BackendType lt) = 'BackendType lt -- | Singleton version of 'Substitute'. sSubstitute @@ -217,7 +217,7 @@ sSubstitute scope idx tsub = \case $ sSubstitute (SSucc scope) (SSucc idx) (sIncrement scope SZero tsub) tx SIOType tx -> SIOType $ sSubstitute scope idx tsub tx SPointerType pk tx -> SPointerType pk $ sSubstitute scope idx tsub tx - SLlvmType lt -> SLlvmType lt + SBackendType lt -> SBackendType lt -- | Proof for transposing two increments. incInc @@ -252,7 +252,7 @@ incInc scope idx1 idx2 t lt@Refl = case t of -> withProof (incInc (SSucc scope) (SSucc idx1) (SSucc idx2) tx lt) Refl SIOType tx -> withProof (incInc scope idx1 idx2 tx lt) Refl SPointerType _ tx -> withProof (incInc scope idx1 idx2 tx lt) Refl - SLlvmType _ -> Refl + SBackendType _ -> Refl {-# RULES "Proof/incInc" incInc = \_ _ _ _ -> Unsafe.unsafeCoerce #-} {-# INLINE [1] incInc #-} @@ -286,7 +286,7 @@ incSub scope sidx iidx tsub t slt@Refl ilt = case t of $ withProof (incInc scope iidx SZero tsub Refl) Refl SIOType tx -> withProof (incSub scope sidx iidx tsub tx slt ilt) Refl SPointerType _ tx -> withProof (incSub scope sidx iidx tsub tx slt ilt) Refl - SLlvmType _ -> Refl + SBackendType _ -> Refl {-# RULES "Proof/incSub" incSub = \_ _ _ _ _ _ -> Unsafe.unsafeCoerce #-} {-# INLINE [1] incSub #-} @@ -325,7 +325,7 @@ subInc scope idx1 idx2 tsub t lt1@Refl lt2@Refl = case t of (sIncrement scope SZero tsub) tx lt1 lt2) Refl SIOType tx -> withProof (subInc scope idx1 idx2 tsub tx lt1 lt2) Refl SPointerType _ tx -> withProof (subInc scope idx1 idx2 tsub tx lt1 lt2) Refl - SLlvmType _ -> Refl + SBackendType _ -> Refl {-# RULES "Proof/subInc" subInc = \_ _ _ _ _ _ -> Unsafe.unsafeCoerce #-} {-# INLINE [1] subInc #-} @@ -368,7 +368,7 @@ subSub scope idx1 idx2 tsub1 tsub2 t lt1@Refl lt2@Refl = case t of SIOType tx -> withProof (subSub scope idx1 idx2 tsub1 tsub2 tx lt1 lt2) Refl SPointerType _ tx -> withProof (subSub scope idx1 idx2 tsub1 tsub2 tx lt1 lt2) Refl - SLlvmType _ -> Refl + SBackendType _ -> Refl {-# RULES "Proof/subSub" subSub = \_ _ _ _ _ _ _ -> Unsafe.unsafeCoerce #-} {-# INLINE [1] subSub #-} @@ -391,7 +391,7 @@ subIncElim scope idx tsub t lt = case t of (Proxy @(Increment 'Zero tsub)) tx lt) Refl SIOType tx -> withProof (subIncElim scope idx tsub tx lt) Refl SPointerType _ tx -> withProof (subIncElim scope idx tsub tx lt) Refl - SLlvmType _ -> Refl + SBackendType _ -> Refl {-# RULES "Proof/subIncElim" subIncElim = \_ _ _ _ -> Unsafe.unsafeCoerce #-} {-# INLINE [1] subIncElim #-} diff --git a/src/Language/Elemental/Backend.hs b/src/Language/Elemental/Backend.hs new file mode 100644 index 0000000..80879b3 --- /dev/null +++ b/src/Language/Elemental/Backend.hs @@ -0,0 +1,467 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Language.Elemental.Backend + ( Name(..) + , Named + , FunctionName(..) + , NamedFunction + , ForeignName(..) + , ForeignNamed + , Named'(..) + , Label(..) + , Type(..) + , Bit(..) + , Operand(..) + , Instruction(..) + , Terminator(..) + , _Return + , _TailCall + , Block(..) + , _entryBlock + , _namedBlocks + , IBlock(..) + , _IBlock + , BlockList(..) + , _blockInstrs + , _blockTerm + , NamedBlockList(..) + , Function(..) + , _functionArgs + , _functionRet + , ImplicitFunction(..) + , _ifunctionBlocks + , External(..) + , Program(..) + , opType + , instrType + -- * Partial + , Partial(..) + , FoldArrow + , addOperand + -- * Traversals + , opRefs + , instrOps + , termOps + , blockOps + , blockBoundNames + , blockFreeRefs + , blockListBlocks + , blockListBoundNames + , blockListFreeRefs + ) where + +import Control.Lens + ( Bifunctor, Iso', Lens', Prism', Traversal' + , anyOf, bimap, filtered, iso, lens, noneOf, prism + ) +import Data.ByteString.Short (ShortByteString) +import Data.DList (DList, snoc, toList) +import Data.Foldable (foldl') +import Data.IntMap qualified as IM +import Data.Kind qualified as Kind +import Data.String (IsString(fromString)) +import Numeric.Natural (Natural) +import Prettyprinter + ( Doc, Pretty(pretty) + , concatWith, encloseSep, flatAlt, group + , hardline, indent, line, nest, parens, tupled + , (<+>) + ) + +import Language.Elemental.Singleton + +-- | Names for the operand namespace. +newtype Name = Name Int + deriving stock (Eq, Ord, Read, Show) + deriving newtype (Pretty) + +-- | Names for the function namespace. +data FunctionName = PrivateName Name | ExternalName ForeignName + deriving stock (Eq, Ord, Read, Show) + +instance Pretty FunctionName where + pretty (PrivateName n) = pretty n + pretty (ExternalName n) = pretty n + +newtype ForeignName = ForeignName { unForeignName :: ShortByteString } + deriving stock (Eq, Ord, Read, Show) + +instance IsString ForeignName where + fromString = ForeignName . fromString + +instance Pretty ForeignName where + pretty = pretty . show . unForeignName + +newtype Label = Label { unLabel :: Int } + deriving newtype (Eq, Ord, Read, Show) + +instance Pretty Label where + pretty (Label idx) = "@" <> pretty idx + +data Type = IntType Int | TupleType [Type] + deriving stock (Eq, Read, Show) + +instance Pretty Type where + pretty (IntType size) = "i" <> pretty size + pretty (TupleType ts) = braced $ pretty <$> ts + +data Bit = B0 | B1 + deriving stock (Enum, Eq, Read, Show) + +instance Pretty Bit where + pretty B0 = "0" + pretty B1 = "1" + +data Operand + = Reference Type Name + | Address Type Natural + | Empty + | Constant Bit + -- | Extracts the nth LSB. + | IsolateBit Int Int Operand + -- | Inserts a new MSB. + | InsertBit Int Operand Operand + {-| + The first operand is the condition. The second operand is the result + when the condition's value is @True@. + -} + | Select Operand Operand Operand + | Tuple [Operand] + | GetElement Int Operand + deriving stock (Eq, Read, Show) + +instance Pretty Operand where + pretty (Reference _ name) = "%" <> pretty name + pretty (Address _ addr) = "@" <> pretty addr + pretty Empty = "[]" + pretty (Constant b) = "#" <> pretty b + pretty (IsolateBit _ idx op) = parens $ pretty op <+> "!!" <+> pretty idx + pretty (InsertBit _ b op) = parens $ pretty b <+> ":" <+> pretty op + pretty (Select op opt opf) = parens $ "if" <+> pretty op + <+> "then" <+> pretty opt <+> "else" <+> pretty opf + pretty (Tuple ops) = braced $ pretty <$> ops + pretty (GetElement idx op) = parens $ pretty op <+> "!" <+> pretty idx + +opType :: Operand -> Type +opType = \case + Reference t _ -> t + Address t _ -> t + Empty -> IntType 0 + Constant _ -> IntType 1 + IsolateBit {} -> IntType 1 + InsertBit size _ _ -> IntType $ succ size + Select _ opt _ -> opType opt + Tuple ops -> TupleType $ opType <$> ops + GetElement idx op -> case opType op of + TupleType ts | length ts > idx -> ts !! idx + _ -> error "illegal GetElement" + +data Instruction + -- | Allows setting a = b. + = Pure Operand + -- | Calls the function with the given arguments. + | Call Type FunctionName [Operand] + -- | Loads the value of a pointer. + | Load Operand + -- | Stores the second value into the first pointer. + | Store Operand Operand + deriving stock (Eq, Read, Show) + +instance Pretty Instruction where + pretty (Pure op) = "Pure" <+> pretty op + pretty (Call _ name args) + = foldl' (<+>) ("Call" <+> pretty name) (pretty <$> args) + pretty (Load op) = "Load" <+> pretty op + pretty (Store op1 op2) = "Store" <+> pretty op1 <+> pretty op2 + +instrType :: Instruction -> Type +instrType = \case + Pure op -> opType op + Call t _ _ -> t + Load ptr -> opType ptr + Store _ _ -> IntType 0 + +data Terminator + = Jump Label + {-| + Jumps to the first label if the value of the operand is @True@. + Otherwise, it jumps to the second label. + -} + | Branch Operand Label Label + | Return Operand + -- | Calls the function and returns its return value. + | TailCall Name Operand + -- | Indicates that this block is unreachable. + | Unreachable + deriving stock (Eq, Read, Show) + +instance Pretty Terminator where + pretty (Jump lbl) = "Jump" <+> pretty lbl + pretty (Branch op lblt lblf) + = "Branch" <+> pretty op <+> pretty lblt <+> pretty lblf + pretty (Return op) = "Return" <+> pretty op + pretty (TailCall name parg) = "TailCall" <+> pretty name <+> pretty parg + pretty Unreachable = "Unreachable" + +_Return :: Prism' Terminator Operand +_Return = prism Return $ \case + Return op -> Right op + term -> Left term +{-# INLINE _Return #-} + +_TailCall :: Prism' Terminator (Name, Operand) +_TailCall = prism (uncurry TailCall) $ \case + TailCall name parg -> Right (name, parg) + term -> Left term +{-# INLINE _TailCall #-} + +data Partial a where + Partial :: SNat ('Succ n) -> FoldArrow ('Succ n) Operand a -> Partial a + +-- Doesn't check equality of the arrows; for testing. +instance Eq (Partial a) where + Partial a _ == Partial b _ = go a b + where + go :: SNat a -> SNat b -> Bool + go SZero SZero = True + go (SSucc _) SZero = False + go SZero (SSucc _) = False + go (SSucc a') (SSucc b') = go a' b' + +instance Functor Partial where + fmap f' (Partial arity g') = Partial arity $ foldNat f' arity g' + where + foldNat + :: (a -> b) -> SNat n + -> FoldArrow n Operand a -> FoldArrow n Operand b + foldNat f SZero g = f g + foldNat f (SSucc n) g = foldNat f n . g + +instance Pretty (Partial a) where + pretty (Partial n _) = "p" <> pretty (toNatural n) + +type FoldArrow :: Nat -> Kind.Type -> Kind.Type -> Kind.Type +type family FoldArrow n a b where + FoldArrow 'Zero _ b = b + FoldArrow ('Succ n) a b = a -> FoldArrow n a b + +data Named' a b = a := b + deriving stock (Eq, Read, Show, Foldable, Functor, Traversable) + +instance (Pretty a, Pretty b) => Pretty (Named' a b) where + pretty (name := a) = pretty name <+> "=" <+> pretty a + +instance Bifunctor Named' where + bimap f g (name := a) = f name := g a + +type Named = Named' Name +type ForeignNamed = Named' ForeignName +type NamedFunction + = Either (Named ImplicitFunction) (Named' FunctionName Function) + +data Block = Block + { blockInstrs :: DList (Named Instruction) + , blockTerm :: Terminator + } deriving stock (Eq, Read, Show) + +instance Pretty Block where + pretty b = concatWith (>>>) . toList + $ snoc (pretty <$> blockInstrs b) (pretty $ blockTerm b) + +_blockInstrs :: Lens' Block (DList (Named Instruction)) +_blockInstrs = lens blockInstrs $ \b instrs -> b { blockInstrs = instrs } +{-# INLINE _blockInstrs #-} + +_blockTerm :: Lens' Block Terminator +_blockTerm = lens blockTerm $ \b term -> b { blockTerm = term } +{-# INLINE _blockTerm #-} + +newtype IBlock = IBlock { unIBlock :: DList (Named Instruction) } + deriving stock (Eq, Read, Show) + deriving newtype (Monoid, Semigroup) + +instance Pretty IBlock where + pretty (IBlock instrs) = concatWith (>>>) . toList $ pretty <$> instrs + +_IBlock :: Iso' IBlock (DList (Named Instruction)) +_IBlock = iso unIBlock IBlock +{-# INLINE _IBlock #-} + +data BlockList = BlockList + { entryBlock :: Block + , namedBlocks :: NamedBlockList + } deriving stock (Eq, Read, Show) + +instance Pretty BlockList where + pretty bs = concatWith (>>>) + $ indent 4 (pretty $ entryBlock bs) : prettyNamedBlocks (namedBlocks bs) + +_entryBlock :: Lens' BlockList Block +_entryBlock = lens entryBlock $ \bs b -> bs { entryBlock = b } +{-# INLINE _entryBlock #-} + +_namedBlocks :: Lens' BlockList NamedBlockList +_namedBlocks = lens namedBlocks $ \bs nbs -> bs { namedBlocks = nbs } +{-# INLINE _namedBlocks #-} + +newtype NamedBlockList = NamedBlockList { unNamedBlockList :: IM.IntMap Block } + deriving stock (Eq, Read, Show) + deriving newtype (Monoid, Semigroup) + +instance Pretty NamedBlockList where + pretty nbs = concatWith (>>>) $ prettyNamedBlocks nbs + +prettyNamedBlocks :: NamedBlockList -> [Doc ann] +prettyNamedBlocks nbs = prettyLabel <$> IM.assocs (unNamedBlockList nbs) + where + prettyLabel (lbl, b) = nest 4 $ pretty lbl <> ":" <> line <> pretty b + +data Function = Function + { functionArgs :: [Named Type] + , functionRet :: Type + , functionBlocks :: BlockList + } deriving stock (Eq, Read, Show) + +instance Pretty Function where + pretty f = "Function" <+> pretty (functionRet f) + <+> tupled (pretty <$> functionArgs f) + >>> pretty (functionBlocks f) + >>> "End" + +_functionArgs :: Lens' Function [Named Type] +_functionArgs = lens functionArgs $ \f args -> f { functionArgs = args } +{-# INLINE _functionArgs #-} + +_functionRet :: Lens' Function Type +_functionRet = lens functionRet $ \f t -> f { functionRet = t } +{-# INLINE _functionRet #-} + +data ImplicitFunction = ImplicitFunction + { ifunctionArgs :: [Named Type] + , ifunctionBlocks :: BlockList + } + deriving stock (Eq, Read, Show) + +instance Pretty ImplicitFunction where + pretty f = "Implicit Function" <+> tupled (pretty <$> ifunctionArgs f) + >>> pretty (ifunctionBlocks f) >>> "End" + +_ifunctionBlocks :: Lens' ImplicitFunction BlockList +_ifunctionBlocks = lens ifunctionBlocks $ \f bs -> f { ifunctionBlocks = bs } +{-# INLINE _ifunctionBlocks #-} + +data External = External + { externalArgs :: [Type] + , externalRet :: Type + } deriving stock (Eq, Read, Show) + +instance Pretty External where + pretty (External args ret) = pretty ret <+> tupled (pretty <$> args) + +data Program = Program + { programImports :: [ForeignNamed External] + , programFunctions :: [NamedFunction] + } + deriving stock (Eq, Read, Show) + +instance Pretty Program where + pretty (Program exts funcs) + = concatWith f $ (pretty <$> exts) <> (either pretty pretty <$> funcs) + where + f a b = a <> line <> line <> b + +addOperand :: Operand -> Partial a -> Either (Partial a) a +addOperand op (Partial (SSucc n) f) = case n of + SZero -> Right $ f op + SSucc _ -> Left $ Partial n $ f op + +opRefs :: Traversal' Operand (Type, Name) +opRefs f op = case op of + Reference t name -> uncurry Reference <$> f (t, name) + Address _ _ -> pure op + Empty -> pure op + Constant _ -> pure op + IsolateBit size idx op' -> IsolateBit size idx <$> opRefs f op' + InsertBit size oph opt -> InsertBit size <$> opRefs f oph <*> opRefs f opt + Select opc opt opf + -> Select <$> opRefs f opc <*> opRefs f opt <*> opRefs f opf + Tuple ops -> Tuple <$> traverse (opRefs f) ops + GetElement idx opt -> GetElement idx <$> opRefs f opt +{-# INLINABLE opRefs #-} + +instrOps :: Traversal' Instruction Operand +instrOps f instr = case instr of + Pure op -> Pure <$> f op + Call t name args -> Call t name <$> traverse f args + Load ptr -> Load <$> f ptr + Store ptr op -> Store <$> f ptr <*> f op + +termOps :: Traversal' Terminator Operand +termOps f = \case + Jump lbl -> pure $ Jump lbl + Branch opc lblt lblf -> (\opc' -> Branch opc' lblt lblf) <$> f opc + Return op -> Return <$> f op + TailCall name parg -> TailCall name <$> f parg + Unreachable -> pure Unreachable +{-# INLINABLE termOps #-} + +blockOps :: Traversal' Block Operand +blockOps f (Block instrs term) = Block <$> go instrs <*> termOps f term + where + go = traverse . traverse $ instrOps f +{-# INLINABLE blockOps #-} + +blockBoundNames :: Traversal' Block Name +blockBoundNames f (Block instrs term) = Block <$> go instrs <*> pure term + where + go = traverse $ \(name := instr) -> (:=) <$> f name <*> pure instr +{-# INLINABLE blockBoundNames #-} + +blockFreeRefs :: Traversal' Block (Type, Name) +blockFreeRefs f b@(Block instrs term) = Block <$> go instrs <*> termNames g term + where + go = traverse . traverse $ instrNames g + g ref + | anyOf blockBoundNames (== snd ref) b = pure ref + | otherwise = f ref + + instrNames :: Traversal' Instruction (Type, Name) + instrNames = instrOps . opRefs + + termNames :: Traversal' Terminator (Type, Name) + termNames = termOps . opRefs +{-# INLINABLE blockFreeRefs #-} + +blockListBlocks :: Traversal' BlockList Block +blockListBlocks f (BlockList eb (NamedBlockList nbs)) + = BlockList <$> f eb <*> (NamedBlockList <$> traverse f nbs) +{-# INLINABLE blockListBlocks #-} + +blockListBoundNames :: Traversal' BlockList Name +blockListBoundNames = blockListBlocks . blockBoundNames +{-# INLINABLE blockListBoundNames #-} + +blockListFreeRefs :: Traversal' BlockList (Type, Name) +blockListFreeRefs f bs = (blockListBlocks . blockFreeRefs . filtered g) f bs + where + g :: (Type, Name) -> Bool + g (_, name) = noneOf blockListBoundNames (name ==) bs +{-# INLINABLE blockListFreeRefs #-} + +(>>>) :: Doc ann -> Doc ann -> Doc ann +a >>> b = a <> flatAlt hardline "; " <> b +infixr 6 >>> + +braced :: [Doc ann] -> Doc ann +braced = group . encloseSep (flatAlt "{ " "{") (flatAlt " }" "}") ", " + diff --git a/src/Language/Elemental/Backend/LLVM.hs b/src/Language/Elemental/Backend/LLVM.hs new file mode 100644 index 0000000..971352d --- /dev/null +++ b/src/Language/Elemental/Backend/LLVM.hs @@ -0,0 +1,363 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +module Language.Elemental.Backend.LLVM + ( compileProgram + , compileExternal + , compileFunction + , compileBlockList + , compileBlock + , compileInstruction + , compileTerminator + , compileOperand + , toLlvmName + , toLlvmType + , toLlvmInt + , toLlvmNat + , LlvmOp + , orUndef + , Scope + ) where + +import Control.Algebra ((:+:)) +import Control.Carrier.Reader (Reader, asks, local, runReader) +import Control.Carrier.State.Church (State, evalState, get, modify) +import Control.Lens hiding (Empty, op) +import Data.Foldable (fold, foldl', foldrM) +import Data.Functor (void) +import Data.Graph (SCC(AcyclicSCC, CyclicSCC), stronglyConnComp) +import Data.IntMap qualified as IM +import Data.List (elemIndex, nub) +import Data.Map qualified as M +import Data.Maybe (fromMaybe) +import Data.String (fromString) +import LLVM.AST qualified as LLVM +import LLVM.AST.CallingConvention qualified as LLVM.CConv +import LLVM.AST.Constant qualified as LLVM.Constant +import LLVM.AST.Linkage qualified as LLVM.Linkage +import LLVM.AST.Type qualified as LLVM.Type +import Math.NumberTheory.Logarithms (naturalLog2) +import Numeric.Natural (Natural) +import Prettyprinter (pretty, (<+>)) + +import Control.Carrier.IRBuilder +import Control.Carrier.ModuleBuilder +import Language.Elemental.Backend + +type LlvmOp = (LLVM.Type, Maybe LLVM.Operand) + +type Scope + = Reader (M.Map FunctionName LLVM.Operand) + :+: Reader (M.Map Name Function) + :+: Reader (IM.IntMap LLVM.Name) + +-- | Assumes that functions are defined before the functions that use them. +compileProgram :: Program -> [LLVM.Definition] +compileProgram (Program exts funcs) = run + $ runModuleBuilder (const . pure) emptyModuleBuilder + $ runReader initScope $ runReader pfuncs $ runReader (IM.empty @LLVM.Name) + $ foldr compileExternal (foldr compileFunction (pure ()) efuncs) exts + where + extMap = M.fromList $ (\(name := ext) -> (name, ext)) <$> exts + + initScope :: M.Map FunctionName LLVM.Operand + efuncs :: [ForeignNamed (LLVM.Linkage.Linkage, Function)] + pfuncs :: M.Map Name Function + (initScope, efuncs, pfuncs) = run $ evalState @Int 0 + $ fmap fold $ traverse nameFunction $ M.assocs + $ foldl' (flip toExplicit) M.empty $ stronglyConnComp $ toConn <$> funcs + + nameFunction + :: forall sig m. Has (State Int) sig m + => (FunctionName, Function) + -> m (M.Map FunctionName LLVM.Operand + , [ForeignNamed (LLVM.Linkage.Linkage, Function)] + , M.Map Name Function) + nameFunction (funcName@(PrivateName name), func) = go + where + go :: m (M.Map FunctionName LLVM.Operand + , [ForeignNamed (LLVM.Linkage.Linkage, Function)] + , M.Map Name Function) + go = do + idx <- get @Int <* modify @Int succ + let namef = ForeignName . ("__elem_" <>) . fromString $ show idx + opf = LLVM.ConstantOperand $ LLVM.Constant.GlobalReference t + $ toLlvmName namef + t = LLVM.Type.ptr $ LLVM.FunctionType tret targs False + targs = toLlvmType . (\(_ := t') -> t') <$> functionArgs func + tret = toLlvmType $ functionRet func + lf = (LLVM.Linkage.Private, func) + pf = M.singleton name func + if M.member namef extMap + then go + else pure (M.singleton funcName opf, [namef := lf], pf) + nameFunction (ExternalName name, func) + = pure (mempty, [name := (LLVM.Linkage.External, func)], mempty) + + toExplicit + :: SCC NamedFunction + -> M.Map FunctionName Function -> M.Map FunctionName Function + toExplicit scc fs = fs <> case scc of + AcyclicSCC nf -> either go sing nf + CyclicSCC nfs -> foldMap (either go sing) nfs + where + iargs = scc ^.. traverse . implicitArgs + trets = scc ^.. traverse . retTypes + + go :: Named ImplicitFunction -> M.Map FunctionName Function + go (name := ImplicitFunction args' bs) + = M.singleton (PrivateName name) (Function (nub args) ret bs) + where + args = args' <> iargs + ret = case nub trets of + [] -> IntType 0 + [t] -> t + ts -> TupleType ts + + sing (name := func) = M.singleton name func + + implicitArgs :: Monoid a => Getting a NamedFunction (Named Type) + implicitArgs = _Left . traverse . _ifunctionBlocks . (blockListBlocks + . _blockTerm . _TailCall . _1 . to ((fs M.!?) . PrivateName) + . traverse . _functionArgs . dropping 1 traverse + <> blockListFreeRefs . to (uncurry $ flip (:=))) + + retTypes :: Monoid a => Getting a NamedFunction Type + retTypes = _Left . traverse . _ifunctionBlocks . (blRets <> blTails) + + blRets :: Fold BlockList Type + blRets = blockListBlocks . _blockTerm . _Return . to opType + + blTails :: Fold BlockList Type + blTails = blockListBlocks . _blockTerm . _TailCall . _1 + . to ((fs M.!?) . PrivateName) . traverse . _functionRet + + toConn :: NamedFunction -> (NamedFunction, FunctionName, [FunctionName]) + toConn nf = (nf, name, nf ^.. refs) + where + name = case nf of + Left (name' := _) -> PrivateName name' + Right (name' := _) -> name' + + refs :: Fold NamedFunction FunctionName + refs = _Left . traverse . _ifunctionBlocks . blockListBlocks + . _blockTerm . _TailCall . _1 . to PrivateName + +compileExternal + :: (Has ModuleBuilder sig m, Has Scope sig m) + => ForeignNamed External -> m r -> m r +compileExternal (name := External targs tret) cont = do + let lname = toLlvmName name + lopf <- extern lname (toLlvmType <$> targs) (toLlvmType tret) + local (M.insert (ExternalName name) lopf) cont + +compileFunction + :: forall sig m r. (Has ModuleBuilder sig m, Has Scope sig m) + => ForeignNamed (LLVM.Linkage.Linkage, Function) -> m r -> m r +compileFunction (name := (linkage, Function args ret bs)) cont = do + let tret = toLlvmType ret + lname = toLlvmName name + _ <- function lname (toLlvmType . namedValue <$> args) tret linkage + $ \lops -> do + foldr bindOp (compileBlockList ret bs) $ zip args lops + void block + cont + where + namedValue :: Named a -> a + namedValue (_ := a) = a + + bindOp :: (Named Type, LLVM.Operand) -> IRBuilderC m r' -> IRBuilderC m r' + bindOp (name' := _, lop) = local (M.insert (PrivateName name') lop) + +compileBlockList + :: (Has IRBuilder sig m, Has Scope sig m) => Type -> BlockList -> m () +compileBlockList tret (BlockList be (NamedBlockList bs)) = do + labels <- traverse (const fresh) bs + local (labels <>) $ compileBlock tret be $ foldr go (pure ()) (IM.assocs bs) + where + go (idx, b) cont = do + llbl <- asks $ fromMaybe abort . (IM.!? idx) + emitBlockStart llbl + compileBlock tret b cont + where + abort = error . show $ "compileBlockList: label not in scope:" + <+> pretty (Label idx) + +compileBlock + :: forall sig m. (Has IRBuilder sig m, Has Scope sig m) + => Type -> Block -> m () -> m () +compileBlock tret (Block instrs term) cont + = foldr go (compileTerminator tret term *> cont) instrs + where + go :: Named Instruction -> m r -> m r + go (name := instr) cont' = do + lop <- compileInstruction instr + local (M.insert (PrivateName name) $ orUndef lop) cont' + +compileInstruction + :: (Has IRBuilder sig m, Has Scope sig m) => Instruction -> m LlvmOp +compileInstruction = \case + Pure op -> compileOperand op + Call t name args -> do + lopf <- fromMaybe (error $ "function not in scope: " <> show name) + <$> asks (M.!? name) + largs <- traverse ((mkParam . orUndef <$>) . compileOperand) args + let call = LLVM.Call Nothing LLVM.CConv.C [] (Right lopf) largs [] [] + ltret = toLlvmType t + (,) ltret <$> case t of + IntType 0 -> Nothing <$ emitInstrVoid call + _ -> Just <$> emitInstr ltret call + Load ptr -> do + (lt, mlptr) <- compileOperand ptr + let lptr = fromMaybe (undef $ LLVM.Type.ptr lt) mlptr + ((,) lt . Just <$>) $ emitInstr lt $ LLVM.Load True lptr Nothing 1 [] + Store ptr op -> do + (ltp, mlptr) <- compileOperand ptr + (lt, mlop) <- compileOperand op + let lptr = fromMaybe (undef $ LLVM.Type.ptr ltp) mlptr + lop = fromMaybe (undef lt) mlop + emitInstrVoid $ LLVM.Store True lptr lop Nothing 1 [] + pure (LLVM.VoidType, Nothing) + where + mkParam a = (a, []) + +compileTerminator + :: (Has IRBuilder sig m, Has Scope sig m) => Type -> Terminator -> m () +compileTerminator tret = \case + Jump lbl -> do + llbl <- getLabel lbl + emitTerm $ LLVM.Br llbl [] + Branch opc lblt lblf -> do + lopc <- orUndef <$> compileOperand opc + llblt <- getLabel lblt + llblf <- getLabel lblf + emitTerm $ LLVM.CondBr lopc llblt llblf [] + Return op + | opType op == tret -> do + (_, lop) <- compileOperand op + emitTerm $ LLVM.Ret lop [] + | otherwise -> do + let opt = Tuple $ ix idx .~ op $ (`Reference` Name 0) <$> ts + idx = fromMaybe abortRetType $ elemIndex (opType op) ts + ts = case tret of + TupleType ts' -> ts' + _ -> abortRetType + (_, lop) <- compileOperand opt + emitTerm $ LLVM.Ret lop [] + TailCall name parg -> do + let abort = error . show + $ "compileTerminator: function not in scope:" <+> pretty name + mkArg (name' := t) = Reference t name' + Function args ret _ <- asks $ fromMaybe abort . (M.!? name) + let args' = zipWith (fromMaybe . mkArg) args + $ Just parg : repeat Nothing + (_, lop) <- compileInstruction $ Call ret (PrivateName name) args' + if ret == tret then emitTerm $ LLVM.Ret lop [] else do + let idx = fromMaybe abortRetType $ elemIndex tret ts + ts = case ret of + TupleType ts' -> ts' + _ -> abortRetType + op = fromMaybe abortRetType lop + tmp = Name $ -2 + (_, lop') <- local (M.insert (PrivateName tmp) op) + $ compileOperand $ GetElement idx $ Reference ret tmp + emitTerm $ LLVM.Ret lop' [] + Unreachable -> emitTerm $ LLVM.Unreachable [] + where + abortRetType = error . show + $ "compileTerminator: incompatible return type" <+> pretty tret + getLabel lbl = asks $ fromMaybe abort . (IM.!? unLabel lbl) + where + abort = error . show + $ "compileTerminator: label not in scope:" <+> pretty lbl + +compileOperand :: (Has IRBuilder sig m, Has Scope sig m) => Operand -> m LlvmOp +compileOperand = skipVoid $ \case + Reference t name -> asks $ (,) (toLlvmType t) . (M.!? PrivateName name) + Address t addr -> pure $ (,) (toLlvmType t) $ Just $ LLVM.ConstantOperand + $ LLVM.Constant.IntToPtr (toLlvmNat addr) $ LLVM.Type.ptr $ toLlvmType t + Empty -> pure (LLVM.VoidType, Nothing) + Constant bit -> pure $ (,) LLVM.Type.i1 $ Just + $ LLVM.ConstantOperand $ LLVM.Constant.Int 1 $ toInteger $ fromEnum bit + IsolateBit size idx op -> do + lop <- orUndef <$> compileOperand op + lops <- emitInstr (LLVM.IntegerType $ succ $ fromIntegral size) + $ LLVM.LShr False lop (toLlvmInt size $ toInteger idx) [] + ((,) LLVM.Type.i1 . Just <$>) $ emitInstr LLVM.Type.i1 + $ LLVM.Trunc lops LLVM.Type.i1 [] + InsertBit size op1 op2 -> case size of + 0 -> compileOperand op1 + _ -> do + lop1 <- orUndef <$> compileOperand op1 + lop2 <- orUndef <$> compileOperand op2 + let lt = LLVM.IntegerType $ succ $ fromIntegral size + sh = toInteger size + lopz1 <- emitInstr lt $ LLVM.ZExt lop1 lt [] + lopz2 <- emitInstr lt $ LLVM.ZExt lop2 lt [] + lops1 <- emitInstr lt + $ LLVM.Shl False True lopz1 (toLlvmInt (succ size) sh) [] + ((,) lt . Just <$>) $ emitInstr lt $ LLVM.Or lops1 lopz2 [] + Select opc opt opf -> do + (ltc, mlopc) <- compileOperand opc + (ltt, mlopt) <- compileOperand opt + (ltf, mlopf) <- compileOperand opf + let lopc = fromMaybe (undef ltc) mlopc + lopt = fromMaybe (undef ltt) mlopt + lopf = fromMaybe (undef ltf) mlopf + ((,) ltt . Just <$>) $ emitInstr ltt $ LLVM.Select lopc lopt lopf [] + Tuple ops -> do + lops <- traverse (fmap orUndef . compileOperand) ops + let lt = toLlvmType $ TupleType $ opType <$> ops + lopz = LLVM.ConstantOperand $ LLVM.Constant.AggregateZero lt + ((,) lt . Just <$>) $ foldrM (insertStruct lt) lopz $ zip [0..] lops + opSelf@(GetElement idx op) -> do + lop <- orUndef <$> compileOperand op + let lt = toLlvmType $ opType opSelf + ((,) lt . Just <$>) $ emitInstr lt + $ LLVM.ExtractValue lop [fromIntegral idx] [] + where + insertStruct + :: Has IRBuilder sig m + => LLVM.Type -> (Int, LLVM.Operand) -> LLVM.Operand -> m LLVM.Operand + insertStruct lt (idx, lop1) lops = emitInstr lt + $ LLVM.InsertValue lops lop1 [fromIntegral idx] [] + + skipVoid + :: Has IRBuilder sig m => (Operand -> m LlvmOp) -> Operand -> m LlvmOp + skipVoid cont op = case opType op of + IntType 0 -> pure (LLVM.VoidType, Nothing) + _ -> cont op + +undef :: LLVM.Type -> LLVM.Operand +undef = LLVM.ConstantOperand . LLVM.Constant.Undef + +orUndef :: LlvmOp -> LLVM.Operand +orUndef (lt, mlop) = fromMaybe (undef lt) mlop + +toLlvmName :: ForeignName -> LLVM.Name +toLlvmName (ForeignName s) = LLVM.Name s + +toLlvmType :: Type -> LLVM.Type +toLlvmType = \case + IntType 0 -> LLVM.VoidType + IntType size -> LLVM.IntegerType $ fromIntegral size + TupleType ts -> LLVM.StructureType False $ toLlvmType <$> ts + +toLlvmInt :: Integral n => n -> Integer -> LLVM.Operand +toLlvmInt size n + = LLVM.ConstantOperand $ LLVM.Constant.Int (fromIntegral size) n + +toLlvmNat :: Natural -> LLVM.Constant.Constant +toLlvmNat n = LLVM.Constant.Int size $ toInteger n + where + size :: Num n => n + size + | n == 0 = 1 + | otherwise = fromIntegral $ naturalLog2 n + 1 + diff --git a/src/Language/Elemental/Emit.hs b/src/Language/Elemental/Emit.hs index 9996e68..590269a 100644 --- a/src/Language/Elemental/Emit.hs +++ b/src/Language/Elemental/Emit.hs @@ -1,5 +1,4 @@ {-# LANGUAGE DataKinds #-} -{-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} @@ -9,598 +8,298 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} --- | Functions to convert an Elemental program into an LLVM module. +-- | Functions to convert an Elemental program into an interaction net. module Language.Elemental.Emit ( emitProgram , emitDeclScope , emitDecl , emitExpr - , emitExprIO - , emitExprOp - , foldArrow - , foldForall - , foldIO - , foldPointer - , llvmType - , llvmForeignName - , llvmAddress + , backendType + , backendForeignName ) where -import Control.Monad (void) +import Control.Algebra ((:+:)) +import Control.Carrier.State.Church (State, get, put, runState) +import Control.Monad.Trans.Class (lift) +import Data.DList (DList, toList) +import Data.Functor.Const (Const(..), getConst) import Data.Text.Short (toShortByteString) -import Data.Type.Equality ((:~:)(Refl)) -import Data.Void (absurd) -import LLVM.AST qualified as LLVM -import LLVM.AST.CallingConvention qualified as LLVM.CallConv -import LLVM.AST.Constant qualified as LLVM.Constant -import LLVM.AST.Type qualified as LLVM.Type -import Math.NumberTheory.Logarithms (naturalLog2) import Control.Carrier.ModuleBuilder -import Control.Effect.IRBuilder import Language.Elemental.AST.Decl import Language.Elemental.AST.Expr import Language.Elemental.AST.Program import Language.Elemental.AST.Type +import Language.Elemental.Backend qualified as Backend +import Language.Elemental.InteractionNet import Language.Elemental.Primitive import Language.Elemental.Singleton - --- | Emits a program as a list of LLVM definitions. -emitProgram :: Program -> [LLVM.Definition] -emitProgram (Program decls) - = runModuleBuilder const emptyModuleBuilder $ emitDeclScope decls +-- | Emits a program as an interaction net. +emitProgram + :: HasRewriter sig m + => Program -> m [Backend.ForeignNamed Backend.External] +emitProgram (Program decls) = toList <$> emitDeclScope SNil SNil decls -- | Emits a list of declarations. -emitDeclScope :: Has ModuleBuilder sig m => DeclScope '[] rest -> m () -emitDeclScope = \case - DeclNil -> pure () - DeclCons decl decls -> do - expr <- emitDecl decl - case declType SNil decl of - SNothing -> emitDeclScope decls - SJust t -> emitDeclScope - $ substituteDeclScope (t :^ SNil) SZero expr decls +emitDeclScope + :: (HasRewriter sig m) + => SList (SType 'Zero) scope -> SList (Const (Ref -> m ())) scope + -> DeclScope scope rest + -> m (DList (Backend.ForeignNamed Backend.External)) +emitDeclScope scopeTypes scope = \case + DeclNil -> pure mempty + DeclCons decl decls -> case declType scopeTypes decl of + SNothing -> do + exts <- emitDecl scopeTypes scope () decl + (exts <>) <$> emitDeclScope scopeTypes scope decls + SJust t -> do + rn0 <- newNode $ AppNode () () () + rn1 <- newNode $ LamNode () () () + linkNodes (Ref rn0 0) (Ref rn1 0) + propagate2 (Ref rn0 2) (Ref rn1 2) DeadNode + exts <- emitDecl scopeTypes scope (Const $ Ref rn0 1) decl + Ref rn1 1 >=^ scope + $ \scope' -> (exts <>) + <$> emitDeclScope (t :^ scopeTypes) scope' decls {-| Emits a declaration, returning the expression to add to the scope if the declaration adds anything to the scope. -} emitDecl - :: Has ModuleBuilder sig m - => Decl '[] mt -> m (FoldMaybe () (Expr 'Zero '[]) mt) -emitDecl = \case - Binding expr -> pure expr + :: (HasRewriter sig m) + => SList (SType 'Zero) scope -> SList (Const (Ref -> m ())) scope + -> FoldMaybe () (Const Ref) mt -> Decl scope mt + -> m (DList (Backend.ForeignNamed Backend.External)) +emitDecl scopeTypes scope rr = \case + Binding expr -> mempty <$ emitExpr scope (getConst rr) expr ForeignImport fname t -> do let ltargs = sForeignArgs t - ltargs' = llvmArgs ltargs ltret = sForeignRet t - ltret' = llvmType ltret - op <- extern (llvmForeignName fname) ltargs' ltret' - pure $ wrapImport SZero SNil t $ Call (Right op) [] ltargs ltret + name = backendForeignName fname + ext = Backend.External (backendArgs ltargs) (backendType ltret) + emitExpr scope (getConst rr) + $ wrapImport SZero scopeTypes t $ Call name ltargs ltret + pure $ pure $ name Backend.:= ext ForeignExport fname expr -> do - let t = exprType SZero SNil expr + let t = exprType SZero scopeTypes expr ltargs = sForeignArgs t - ltargs' = llvmArgs ltargs ltret = sForeignRet t - ltret' = llvmType ltret - export ops = applyArgs ltret ltargs ops - $ wrapExport SZero SNil t expr - _ <- function (llvmForeignName fname) ltargs' ltret' $ emitExpr . export - pure () - ForeignPrimitive pfin -> pure $ primitiveExprs !!^ pfin - ForeignAddress addr pk t -> pure $ Addr addr pk t + names <- traverseSList newName ltargs + let ops = zipWith Backend.Reference (backendArgs ltargs) names + bargs = zipWith (Backend.:=) names (backendArgs ltargs) + bret = backendType ltret + bname = backendForeignName fname + rn1 <- newNode $ ExternalRootNode bname bargs bret () + rn2 <- newNode $ AccumIONode mempty () () + rn3 <- newNode $ Bind0CNode () () () + rn4 <- newNode $ LamNode () () () + rn5 <- newNode $ ReturnCNode () () + linkNodes (Ref rn1 0) (Ref rn2 1) + linkNodes (Ref rn2 0) (Ref rn3 2) + linkNodes (Ref rn3 1) (Ref rn4 0) + linkNodes (Ref rn4 1) (Ref rn5 1) + linkNodes (Ref rn4 2) (Ref rn5 0) + emitExpr scope (Ref rn3 0) $ applyArgs ltret ltargs ops + $ wrapExport SZero scopeTypes t expr + pure mempty + ForeignPrimitive pfin + -> (mempty <$) $ emitExpr scope (getConst rr) $ primitiveExprs !!^ pfin + ForeignAddress addr pk (t :: SType 'Zero t) -> let + lt :: SType 'Zero ('BackendType (Marshall t)) + lt = SBackendType $ sMarshall t + baddr = Backend.Address (backendType $ sMarshall t) $ getAddress addr + li0 = SBackendInt SZero + i0 = SBackendType li0 + in case pk of + SReadPointer -> (mempty <$) $ emitExpr scope (getConst rr) $ BindIO + :@ lt :$ BackendIO (sMarshall t) (Backend.Load baddr) + :@ t :$ (lt + :\ marshallIn SZero (lt :^ scopeTypes) t (Var SZero)) + SWritePointer -> (mempty <$) $ emitExpr scope (getConst rr) + $ Lam t $ BindIO + :@ i0 :$ (BackendPIO (sMarshall t) li0 (Backend.Store baddr) + :$ marshallOut SZero (t :^ scopeTypes) t (Var SZero)) + :@ SUnitType :$ (i0 :\ marshallIn SZero (i0 :^ t :^ scopeTypes) + SUnitType (Var SZero)) where - llvmArgs :: SList SLlvmType lts -> [LLVM.Type] - llvmArgs SNil = [] - llvmArgs (lt :^ lts) = llvmType lt : llvmArgs lts + traverseSList :: Applicative f => f a -> SList sing as -> f [a] + traverseSList _ SNil = pure [] + traverseSList f (_ :^ xs) = (:) <$> f <*> traverseSList f xs + backendArgs :: SList SBackendType lts -> [Backend.Type] + backendArgs SNil = [] + backendArgs (lt :^ lts) = backendType lt : backendArgs lts + applyArgs :: AllIsOpType ltargs ~ 'True - => proxy ltret -> SList SLlvmType ltargs -> [LLVM.Operand] - -> Expr 'Zero '[] (BuildForeignType ltargs ltret) - -> Expr 'Zero '[] ('IOType ('LlvmType ltret)) + => proxy ltret -> SList SBackendType ltargs -> [Backend.Operand] + -> Expr 'Zero scope (BuildForeignType ltargs ltret) + -> Expr 'Zero scope ('IOType ('BackendType ltret)) applyArgs _ SNil [] expr = expr applyArgs t (ltarg :^ ltargs) (op : ops) expr = withAllIsOpTypeProof ltarg ltargs $ applyArgs t ltargs ops - $ expr :$ LlvmOperand ltarg op + $ expr :$ BackendOperand ltarg op applyArgs _ SNil ops _ = error $ "emitDecl: " <> show (length ops) <> " excess operands" applyArgs _ ltargs [] _ = error $ "emitDecl: " <> show (toNatural $ sLength ltargs) <> " missing operands" --- | Emits an expression. This emits a @ret@ instruction. emitExpr - :: Has IRBuilder sig m => Expr 'Zero '[] ('IOType ('LlvmType lt)) -> m () -emitExpr expr = do - let SIOType (SLlvmType lt) = exprType SZero SNil expr - mop <- toMaybeOp lt <$> emitExprIO expr - emitTerm $ LLVM.Ret mop [] - void block + :: forall tscope scope tx sig m. HasRewriter sig m + => SList (Const (Ref -> m ())) scope -> Ref -> Expr tscope scope tx -> m () +emitExpr scope rr = \case + Var vidx -> mkBox vidx >>= getConst (scope !!^ vidx) + App ef ex -> do + rn1 <- newNode $ AppNode () () () + emitExpr scope (Ref rn1 0) ef + emitExpr scope (Ref rn1 1) ex + linkNodes rr $ Ref rn1 2 + TypeApp ef _ -> emitExpr scope rr ef + Lam _ ey -> do + rn1 <- newNode $ LamNode () () () + Ref rn1 1 >=^ scope $ \scope' -> emitExpr scope' (Ref rn1 2) ey + linkNodes rr $ Ref rn1 0 + TypeLam ex -> emitExpr (coerceScope scope) rr ex + Addr addr _ tx -> do + rn1 <- newNode $ OperandNode (Backend.Address + (backendType $ sMarshall tx) $ getAddress addr) () + linkNodes rr $ Ref rn1 0 + BackendOperand _ op -> do + rn1 <- newNode $ OperandNode op () + linkNodes rr $ Ref rn1 0 + BackendIO _ instr -> propagate1 rr $ IOContNode instr + BackendPIO _ tret pio -> propagate1 rr + $ IOANode (backendType tret) (Backend.Partial (SSucc SZero) pio) + PureIO -> do + rn1 <- newNode $ LamNode () () () + rn2 <- newNode $ IOPureNode () () + rn3 <- newNode $ LamNode () () () + rn4 <- newNode $ AppNode () () () + rn5 <- newNode $ BoxNode 0 () () + linkNodes (Ref rn1 1) (Ref rn5 0) + linkNodes (Ref rn1 2) (Ref rn2 0) + linkNodes (Ref rn2 1) (Ref rn3 0) + linkNodes (Ref rn3 1) (Ref rn4 0) + linkNodes (Ref rn3 2) (Ref rn4 2) + linkNodes (Ref rn4 1) (Ref rn5 1) + linkNodes rr $ Ref rn1 0 + BindIO -> mkLambda rr Bind0BNode + LoadPointer -> do + rn1 <- newNode $ LamNode () () () + linkNodes (Ref rn1 1) (Ref rn1 2) + linkNodes rr $ Ref rn1 0 + StorePointer -> do + rn1 <- newNode $ LamNode () () () + linkNodes (Ref rn1 1) (Ref rn1 2) + linkNodes rr $ Ref rn1 0 + Call fname SNil tret -> propagate1 rr $ IOContNode + $ Backend.Call (backendType tret) (Backend.ExternalName fname) [] + Call fname ltargs@(_ :^ _) tret -> do + let callp = Backend.Partial len $ withVarargs len + $ Backend.Call (backendType tret) (Backend.ExternalName fname) + len = sLength ltargs + propagate1 rr $ IOANode (backendType tret) callp + IsolateBit bidx ssize -> do + let opp = Backend.Partial (SSucc SZero) $ mkIsolateBit size bidx' + size = fromIntegral $ toNatural ssize + bidx' = fromIntegral $ toNatural bidx + propagate1 rr $ OperandANode opp + InsertBit ssize -> do + let opp = Backend.Partial (SSucc $ SSucc SZero) $ Backend.InsertBit size + size = fromIntegral $ toNatural ssize + propagate1 rr $ OperandANode opp + TestBit -> do + rn1 <- newNode $ LamNode () () () + rn2 <- newNode $ IOPureNode () () + rn3 <- newNode $ LamNode () () () + rn4 <- newNode $ DupIONode 0 () () () + rn5 <- newNode $ AppNode () () () + rn6 <- newNode $ DupNode 0 () () () + r7 <- mkChurchBool const + r8 <- mkChurchBool $ const id + rn9 <- newNode $ BoxNode 0 () () + linkNodes (Ref rn1 1) (Ref rn9 0) + linkNodes (Ref rn1 2) (Ref rn2 0) + linkNodes (Ref rn2 1) (Ref rn3 0) + linkNodes (Ref rn3 1) (Ref rn5 0) + linkNodes (Ref rn3 2) (Ref rn4 2) + linkNodes (Ref rn4 0) (Ref rn5 2) + linkNodes (Ref rn4 1) (Ref rn9 1) + linkNodes (Ref rn5 1) (Ref rn6 0) + linkNodes r7 $ Ref rn6 1 + linkNodes r8 $ Ref rn6 2 + linkNodes rr $ Ref rn1 0 where - toMaybeOp :: SLlvmType lt -> LlvmOperandType lt -> Maybe LLVM.Operand - toMaybeOp lt op = case sIsOpType lt of - SFalse -> Nothing - STrue -> Just op + coerceScope :: SList (Const a) as -> SList (Const a) (IncrementAll 'Zero as) + coerceScope SNil = SNil + coerceScope (Const a :^ as) = Const a :^ coerceScope as -{-| - Emits an expression. Unlike 'emitExpr', this does not emit a @ret@ - instruction but instead returns the final operand for the caller to use. --} -emitExprIO - :: forall lt sig m. Has IRBuilder sig m - => Expr 'Zero '[] ('IOType ('LlvmType lt)) -> m (LlvmOperandType lt) -emitExprIO = \case - Var vidx -> absurd $ zeroNoLT vidx Refl - App ef ex -> foldArrow - (\tx -> emitExprIO . substituteExpr SZero (tx :^ SNil) SZero ex) - (\Refl -> emitExprOp ex) - (\_ -> \case {}) - (\Refl Refl tx ey ty -> foldIO - (\Refl lt -> do - op <- emitExprIO ey - emitExprIO $ ex :$ LlvmOperand lt op) - (\ez -> emitExprIO $ ex :$ ez) - (\op et ef' -> withProof (subIncElim SZero SZero ty tx Refl) - $ emitCondBr op - (BindIO :@ tx :$ et :@ ty :$ ex) - (BindIO :@ tx :$ ef' :@ ty :$ ex)) - ey) - (\Refl Refl _ -> foldPointer - (\tx pop -> do - let lt = sMarshall tx - op <- emitInstr (llvmType lt) $ LLVM.Load True pop Nothing 1 [] - emitExprOp $ marshallIn SZero SNil tx $ LlvmOperand lt op) - ex) - (\_ -> \case {}) - (\case {}) - (\Refl Refl fop aops (ltarg :^ SNil) ltret -> do - aop <- withAllIsOpTypeProof ltarg SNil $ emitExprOp ex - emitCall fop (aop : aops) ltret) - (\_ -> \case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\case {}) - (\Refl op ey -> emitCondBr op ey ex) - (\op ey ez -> emitCondBr op (ey :$ ex) (ez :$ ex)) - ef - TypeApp ef tx -> foldForall - (emitExprIO . substituteExprType SZero SNil SZero tx) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\op ey ez -> emitCondBr op (ey :@ tx) (ez :@ tx)) - ef - LlvmIO _ mop -> mop - Call fop aops SNil ltret -> emitCall fop aops ltret - where - emitCall - :: LLVM.CallableOperand -> [LLVM.Operand] - -> SLlvmType ltret -> m (LlvmOperandType ltret) - emitCall fop aops ltret = case sIsOpType ltret of - SFalse -> emitInstrVoid instr - STrue -> emitInstr (llvmType ltret) instr - where - instr = LLVM.Call Nothing LLVM.CallConv.C [] fop - ((, []) <$> reverse aops) [] [] + withVarargs :: SNat n -> ([a] -> b) -> Backend.FoldArrow n a b + withVarargs SZero f = f [] + withVarargs (SSucc n) f = \x -> withVarargs n $ f . (x :) - emitCondBr - :: LLVM.Operand - -> Expr 'Zero '[] ('IOType ('LlvmType lt)) - -> Expr 'Zero '[] ('IOType ('LlvmType lt)) - -> m (LlvmOperandType lt) - emitCondBr opc et ef = do - bt <- fresh - bf <- fresh - br <- fresh - emitTerm $ LLVM.CondBr opc bt bf [] - emitBlockStart bt - opt <- emitExprIO et - bt' <- currentBlock - emitTerm $ LLVM.Br br [] - emitBlockStart bf - opf <- emitExprIO ef - bf' <- currentBlock - emitTerm $ LLVM.Br br [] - emitBlockStart br - case sIsOpType lt of - SFalse -> pure () - STrue -> emitInstr (llvmType lt) - $ LLVM.Phi (llvmType lt) [(opt, bt'), (opf, bf')] [] - where - SIOType (SLlvmType lt) = exprType SZero SNil et + mkBox :: SNat n -> m Ref + mkBox SZero = pure rr + mkBox (SSucc n) = do + r1 <- mkBox n + rn2 <- newNode $ BoxNode 0 () () + linkNodes r1 $ Ref rn2 1 + pure $ Ref rn2 0 -{-| - Emits a pure LLVM operand. + mkIsolateBit :: Int -> Int -> Backend.Operand -> Backend.Operand + mkIsolateBit size bidx (Backend.InsertBit _ oph opt) + | bidx == 0 = oph + | otherwise = mkIsolateBit size (pred bidx) opt + mkIsolateBit size bidx op = Backend.IsolateBit size bidx op - This still needs an 'IRBuilder' effect because it may need to emit - instructions for operand conversion. All instructions emitted by this - function do not have any side effects; they may be eliminated by the LLVM - optimiser if their result is unused. --} -emitExprOp - :: forall lt sig m. Has IRBuilder sig m - => Expr 'Zero '[] ('LlvmType lt) -> m (LlvmOperandType lt) -emitExprOp = \case - Var vidx -> absurd $ zeroNoLT vidx Refl - App ef ex -> foldArrow - (\tx -> emitExprOp . substituteExpr SZero (tx :^ SNil) SZero ex) - (\case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\case {}) - (\Refl Refl _ _ (_ :^ ltargs) _ -> case ltargs of {}) - (\Refl Refl bidx size -> do - let SLlvmType lt = exprType SZero SNil ex - li1 = llvmType $ SLlvmInt $ SSucc SZero - op <- withProof (ltRightPredSucc bidx size Refl) - $ emitExprOp ex - shifted <- emitInstr (llvmType lt) $ LLVM.LShr False op - (LLVM.ConstantOperand $ LLVM.Constant.Int - (fromIntegral $ toNatural size) - (fromIntegral $ toNatural bidx)) [] - emitInstr li1 $ LLVM.Trunc shifted li1 []) - (\_ -> \case {}) - (\Refl Refl size bop -> case sCmpNat size SZero of - SLT -> absurd $ zeroNoLT size Refl - SEQ -> pure bop - SGT -> do - iop <- emitExprOp ex - let lt = SLlvmInt $ SSucc size - ft = llvmType lt - usize :: Integral n => n - usize = fromIntegral $ toNatural size - bext <- emitInstr ft $ LLVM.ZExt bop ft [] - iext <- emitInstr ft $ LLVM.ZExt iop ft [] - bsh <- emitInstr ft $ LLVM.Shl False True bext - (LLVM.ConstantOperand $ LLVM.Constant.Int - (usize + 1) usize) [] - emitInstr ft $ LLVM.Or bsh iext []) - (\case {}) - (\Refl op ey -> emitSelect op ey ex) - (\op ey ez -> emitSelect op (ey :$ ex) (ez :$ ex)) - ef - TypeApp ef tx -> foldForall - (emitExprOp . substituteExprType SZero SNil SZero tx) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\op ey ez -> emitSelect op (ey :@ tx) (ez :@ tx)) - ef - LlvmOperand _ op -> pure op - Call _ _ ltargs _ -> case ltargs of {} +(>=^) + :: HasRewriter sig m + => Ref -> SList (Const (Ref -> m ())) scope + -> (forall n. Algebra (State (Ref, Maybe Ref) :+: sig) n + => SList (Const (Ref -> n ())) (tx ': scope) -> n r) + -> m r +(r0 >=^ sc) f = runState @(Ref, Maybe Ref) finish (r0, Nothing) $ f + $ Const dup :^ sMap (Const . (.) lift . getConst) sc where - emitSelect - :: LLVM.Operand - -> Expr 'Zero '[] ('LlvmType lt) -> Expr 'Zero '[] ('LlvmType lt) - -> m (LlvmOperandType lt) - emitSelect opc et ef = case sIsOpType lt of - SFalse -> pure () - STrue -> do - opt <- emitExprOp et - opf <- emitExprOp ef - emitInstr (llvmType lt) $ LLVM.Select opc opt opf [] - where - SLlvmType lt = exprType SZero SNil et - --- | Folds an arrow using the given continuations for each possible value. -foldArrow - :: forall ta tb sig r m. Has IRBuilder sig m - => (SType 'Zero ta -> Expr 'Zero '[ta] tb -> m r) - -- ^ Lam - -> (tb :~: 'IOType ta -> m r) - -- ^ PureIO :@ ta - -> (forall tx. ta :~: 'IOType tx -> tb :~: 'Forall ((Increment 'Zero tx - :-> 'IOType ('TypeVar 'Zero)) :-> 'IOType ('TypeVar 'Zero)) - -> SType 'Zero tx -> m r) - -- ^ BindIO :@ _ - -> (forall tx ty. ta :~: 'Arrow tx ('IOType ty) -> tb :~: 'IOType ty - -> SType 'Zero tx -> Expr 'Zero '[] ('IOType tx) - -> SType 'Zero ty -> m r) - -- ^ BindIO :@ _ :$ _ :@ _ - -> (forall tx. ta :~: 'PointerType 'ReadPointer tx -> tb :~: 'IOType tx - -> SType 'Zero tx -> m r) - -- ^ LoadPointer :@ _ - -> (forall tx. ta :~: 'PointerType 'WritePointer tx - -> tb :~: (tx :-> 'IOType UnitType) -> SType 'Zero tx -> m r) - -- ^ StorePointer :@ _ - -> (tb :~: 'IOType UnitType - -> Expr 'Zero '[] ('PointerType 'WritePointer ta) -> m r) - -- ^ StorePointer :@ ta :$ _ - -> (forall ltarg ltargs ltret. AllIsOpType (ltarg ': ltargs) ~ 'True - => ta :~: 'LlvmType ltarg - -> tb :~: BuildForeignType ltargs ltret - -> LLVM.CallableOperand -> [LLVM.Operand] - -> SList SLlvmType (ltarg ': ltargs) -> SLlvmType ltret -> m r) - -- ^ Call _ _ _ _ - -> (forall bidx size. CmpNat bidx size ~ 'LT - => ta :~: 'LlvmType ('LlvmInt size) - -> tb :~: 'LlvmType ('LlvmInt ('Succ 'Zero)) - -> SNat bidx -> SNat size -> m r) - -- ^ IsolateBit _ - -> (forall size. ta :~: 'LlvmType ('LlvmInt ('Succ 'Zero)) - -> tb :~: ('LlvmType ('LlvmInt size) - :-> 'LlvmType ('LlvmInt ('Succ size))) - -> SNat size -> m r) - -- ^ InsertBit _ - -> (forall size. ta :~: 'LlvmType ('LlvmInt size) - -> tb :~: 'LlvmType ('LlvmInt ('Succ size)) - -> SNat size -> LLVM.Operand -> m r) - -- ^ InsertBit _ :$ _ - -> (tb :~: 'Arrow ta ta -> LLVM.Operand -> m r) - -- ^ TestBit _ :@ ta - -> (tb :~: ta -> LLVM.Operand -> Expr 'Zero '[] ta -> m r) - -- ^ TestBit _ :@ ta :$ _ - -> (LLVM.Operand -> Expr 'Zero '[] (ta :-> tb) - -> Expr 'Zero '[] (ta :-> tb) -> m r) - -- ^ TestBit _ :@ ta :-> tb :$ _ :$ _ - -> Expr 'Zero '[] (ta :-> tb) -> m r -foldArrow lam pureIO1 bindIO1 bindIO3 loadPointer1 storePointer1 storePointer2 - call isolateBit insertBit insertBit1 testBit1 testBit2 testBit3 = \case - Var vidx -> absurd $ zeroNoLT vidx Refl - App ef ex -> foldArrow - (\tx -> foldArrow lam pureIO1 bindIO1 bindIO3 loadPointer1 storePointer1 - storePointer2 call isolateBit insertBit insertBit1 testBit1 - testBit2 testBit3 - . substituteExpr SZero (tx :^ SNil) SZero ex) - (\case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\Refl Refl _ -> storePointer2 Refl ex) - (\case {}) - (\Refl Refl fop aops (ltarg :^ ltargs) ltret -> case ltargs of - _ :^ _ -> withAllIsOpTypeProof ltarg ltargs $ do - aop <- emitExprOp ex - call Refl Refl fop (aop : aops) ltargs ltret) - (\_ -> \case {}) - (\Refl Refl size -> emitExprOp ex >>= insertBit1 Refl Refl size) - (\_ -> \case {}) - (\Refl op -> testBit2 Refl op ex) - (\Refl op ey -> testBit3 op ey ex) - (\op ey ez -> testBit3 op (ey :$ ex) (ez :$ ex)) - ef - TypeApp ef tx -> foldForall - (foldArrow lam pureIO1 bindIO1 bindIO3 loadPointer1 storePointer1 - storePointer2 call isolateBit insertBit insertBit1 testBit1 - testBit2 testBit3 - . substituteExprType SZero SNil SZero tx) - (\Refl -> pureIO1 Refl) - (\Refl -> bindIO1 Refl Refl tx) - (\Refl ty ex -> withProof (subIncElim SZero SZero tx ty Refl) - $ bindIO3 Refl Refl ty ex tx) - (\Refl -> loadPointer1 Refl Refl tx) - (\Refl -> storePointer1 Refl Refl tx) - (\Refl -> testBit1 Refl) - (\op ey ez -> testBit3 op (ey :@ tx) (ez :@ tx)) - ef - Lam tx ex -> lam tx ex - Call fop aops ltargs@(_ :^ _) ltret -> call Refl Refl fop aops ltargs ltret - IsolateBit bidx size -> isolateBit Refl Refl bidx size - InsertBit size -> insertBit Refl Refl size + sMap :: (forall a. f a -> g a) -> SList f as -> SList g as + sMap _ SNil = SNil + sMap nt (a :^ as) = nt a :^ sMap nt as --- | Folds a forall using the given continuations for each possible value. -foldForall - :: forall t sig r m. Has IRBuilder sig m - => (Expr ('Succ 'Zero) '[] t -> m r) - -- ^ TypeLam - -> (t :~: ('TypeVar 'Zero :-> 'IOType ('TypeVar 'Zero)) -> m r) - -- ^ PureIO - -> (t :~: ('IOType ('TypeVar 'Zero) :-> 'Forall (('TypeVar ('Succ 'Zero) - :-> 'IOType ('TypeVar 'Zero)) :-> 'IOType ('TypeVar 'Zero))) -> m r) - -- ^ BindIO - -> (forall tx. t :~: ((Increment 'Zero tx :-> 'IOType ('TypeVar 'Zero)) - :-> 'IOType ('TypeVar 'Zero)) - -> SType 'Zero tx -> Expr 'Zero '[] ('IOType tx) -> m r) - -- ^ BindIO :@ _ :$ _ - -> (t :~: ('PointerType 'ReadPointer ('TypeVar 'Zero) - :-> 'IOType ('TypeVar 'Zero)) -> m r) - -- ^ LoadPointer - -> (t :~: ('PointerType 'WritePointer ('TypeVar 'Zero) :-> 'TypeVar 'Zero - :-> 'IOType UnitType) -> m r) - -- ^ StorePointer - -> (t :~: ('TypeVar 'Zero :-> 'TypeVar 'Zero :-> 'TypeVar 'Zero) - -> LLVM.Operand -> m r) - -- ^ TestBit - -> (LLVM.Operand -> Expr 'Zero '[] ('Forall t) - -> Expr 'Zero '[] ('Forall t) -> m r) - -- ^ TestBit _ :@ Forall t :$ _ :$ _ - -> Expr 'Zero '[] ('Forall t) -> m r -foldForall typeLam pureIO bindIO bindIO2 loadPointer storePointer testBit - testBit3 = \case - Var vidx -> absurd $ zeroNoLT vidx Refl - App ef ex -> foldArrow - (\tx -> foldForall typeLam pureIO bindIO bindIO2 loadPointer - storePointer testBit testBit3 - . substituteExpr SZero (tx :^ SNil) SZero ex) - (\case {}) - (\Refl Refl tx -> bindIO2 Refl tx ex) - (\_ -> \case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\case {}) - (\Refl Refl _ _ (_ :^ ltargs) _ -> case ltargs of {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\case {}) - (\Refl op ey -> testBit3 op ey ex) - (\op ey ez -> testBit3 op (ey :$ ex) (ez :$ ex)) - ef - TypeApp ef tx -> foldForall - (foldForall typeLam pureIO bindIO bindIO2 loadPointer storePointer - testBit testBit3 . substituteExprType SZero SNil SZero tx) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\op ey ez -> testBit3 op (ey :@ tx) (ez :@ tx)) - ef - TypeLam ex -> typeLam ex - PureIO -> pureIO Refl - BindIO -> bindIO Refl - LoadPointer -> loadPointer Refl - StorePointer -> storePointer Refl - Call _ _ ltargs _ -> case ltargs of {} - TestBit ex -> emitExprOp ex >>= testBit Refl + dup :: (HasRewriter sig m, Has (State (Ref, Maybe Ref)) sig m) + => Ref -> m () + dup r1 = do + (r2, mr3) <- get @(Ref, Maybe Ref) + case mr3 of + Nothing -> put (r2, Just r1) + Just r3 -> do + rn4 <- newNode $ DupNode 0 () () () + linkNodes r2 $ Ref rn4 0 + linkNodes r3 $ Ref rn4 1 + put (Ref rn4 2, Just r1) --- | Folds an @IO@ value using the given continuations for each possible value. -foldIO - :: forall t sig r m. Has IRBuilder sig m - => (forall lt. t :~: 'LlvmType lt -> SLlvmType lt -> m r) - -- ^ LLVM-typed expressions - -> (Expr 'Zero '[] t -> m r) - -- ^ Pure expressions - -> (LLVM.Operand -> Expr 'Zero '[] ('IOType t) - -> Expr 'Zero '[] ('IOType t) -> m r) - -- ^ TestBit _ :@ IOType t :$ _ :$ _ - -> Expr 'Zero '[] ('IOType t) -> m r -foldIO llvmIO pureIO testBit3 = \case - Var vidx -> absurd $ zeroNoLT vidx Refl - App ef ex -> foldArrow - (\tx -> foldIO llvmIO pureIO testBit3 - . substituteExpr SZero (tx :^ SNil) SZero ex) - (\Refl -> pureIO ex) - (\_ -> \case {}) - (\Refl Refl tx ey ty -> foldIO - (\Refl lt -> do - op <- emitExprIO ey - foldIO llvmIO pureIO testBit3 $ ex :$ LlvmOperand lt op) - (\ez -> foldIO llvmIO pureIO testBit3 $ ex :$ ez) - (\op et ef' -> foldIO llvmIO pureIO testBit3 - $ withProof (subIncElim SZero SZero ty tx Refl) - $ TestBit (LlvmOperand (SLlvmInt $ SSucc SZero) op) - :@ SIOType ty - :$ (BindIO :@ tx :$ et :@ ty :$ ex) - :$ (BindIO :@ tx :$ ef' :@ ty :$ ex)) - ey) - (\Refl Refl _ -> foldPointer - (\tx pop -> do - let lt = sMarshall tx - op <- emitInstr (llvmType lt) $ LLVM.Load True pop Nothing 1 [] - pureIO $ marshallIn SZero SNil tx $ LlvmOperand lt op) - ex) - (\_ -> \case {}) - (\Refl ey -> foldPointer - (\tx pop -> do - op <- emitExprOp $ marshallOut SZero SNil tx ex - emitInstrVoid $ LLVM.Store True pop op Nothing 1 [] - pureIO $ TypeLam $ STypeVar SZero :\ Var SZero) - ey) - (\Refl Refl _ _ (_ :^ SNil) ltret -> llvmIO Refl ltret) - (\_ -> \case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\case {}) - (\Refl op ey -> testBit3 op ey ex) - (\op ey ez -> testBit3 op (ey :$ ex) (ez :$ ex)) - ef - TypeApp ef tx -> foldForall - (foldIO llvmIO pureIO testBit3 . substituteExprType SZero SNil SZero tx) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\op ey ez -> testBit3 op (ey :@ tx) (ez :@ tx)) - ef - LlvmIO lt _ -> llvmIO Refl lt - Call _ _ SNil ltret -> llvmIO Refl ltret + finish :: HasRewriter sig m => (Ref, Maybe Ref) -> r -> m r + finish (r1, mr2) r = r <$ maybe (propagate1 r1 DeadNode) (linkNodes r1) mr2 --- | Folds a pointer using the given continuations for each possible value. -foldPointer - :: forall pk tx sig r m. Has IRBuilder sig m - => ((MarshallableType tx, IsOpType (Marshall tx) ~ 'True) - => SType 'Zero tx -> LLVM.Operand -> m r) - -> Expr 'Zero '[] ('PointerType pk tx) -> m r -foldPointer addr = \case - Var vidx -> absurd $ zeroNoLT vidx Refl - App ef ex -> foldArrow - (\tx -> foldPointer addr . substituteExpr SZero (tx :^ SNil) SZero ex) - (\case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\case {}) - (\Refl Refl _ _ (_ :^ ltargs) _ -> case ltargs of {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\_ -> \case {}) - (\case {}) - (\Refl op ey -> emitSelect' op ey ex) - (\op ey ez -> emitSelect' op (ey :$ ex) (ez :$ ex)) - ef - TypeApp ef tx -> foldForall - (foldPointer addr . substituteExprType SZero SNil SZero tx) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\case {}) - (\op ey ez -> emitSelect' op (ey :@ tx) (ez :@ tx)) - ef - Addr addr' _ tx -> addr tx $ llvmAddress (sMarshall tx) addr' - Call _ _ ltargs _ -> case ltargs of {} - where - emitSelect' - :: LLVM.Operand - -> Expr 'Zero '[] ('PointerType pk tx) - -> Expr 'Zero '[] ('PointerType pk tx) - -> m r - emitSelect' opc et ef = foldPointer (\_ opt -> foldPointer (\_ opf -> do - opr <- emitInstr (llvmType $ sMarshall tx) - $ LLVM.Select opc opt opf [] - addr tx opr - ) ef) et - where - SPointerType _ tx = exprType SZero SNil et - --- | Converts an t'LlvmType' into an LLVM type in the LLVM AST. -llvmType :: SLlvmType t -> LLVM.Type -llvmType = \case - SLlvmInt size -> case sCmpNat size SZero of - SLT -> absurd $ zeroNoLT size Refl - SEQ -> LLVM.VoidType - SGT -> LLVM.IntegerType $ fromIntegral $ toNatural size +-- | Converts a t'BackendType' into a backend type in the backend AST. +backendType :: SBackendType t -> Backend.Type +backendType (SBackendInt size) = Backend.IntType $ fromIntegral $ toNatural size --- | Converts a foreign name to a name in the LLVM AST. -llvmForeignName :: ForeignName -> LLVM.Name -llvmForeignName (ForeignName t) = LLVM.Name $ toShortByteString t - -{-| - Converts an address to an LLVM operand representing that address. The given - t'LlvmType' is used to determine the type of the operand. --} -llvmAddress :: SLlvmType lt -> Address -> LLVM.Operand -llvmAddress lt (Address addr) = LLVM.ConstantOperand - $ LLVM.Constant.IntToPtr (LLVM.Constant.Int (log2 addr) $ fromIntegral addr) - $ LLVM.Type.ptr $ llvmType lt - where - log2 0 = error "Address is 0" - log2 n = fromIntegral $ naturalLog2 n + 1 +-- | Converts a foreign name to a name in the backend AST. +backendForeignName :: ForeignName -> Backend.ForeignName +backendForeignName (ForeignName t) = Backend.ForeignName $ toShortByteString t -- GHC gives a nonexhaustive pattern warning if this is inlined. :/ -- | Calls a continuation with a proof relating 'AllIsOpType' and 'IsOpType'. withAllIsOpTypeProof - :: AllIsOpType (lt ': lts) ~ 'True => SLlvmType lt -> proxy lts + :: AllIsOpType (lt ': lts) ~ 'True => SBackendType lt -> proxy lts -> ((IsOpType lt ~ 'True, AllIsOpType lts ~ 'True) => r') -> r' withAllIsOpTypeProof lt _ x = case sIsOpType lt of STrue -> x + diff --git a/src/Language/Elemental/InteractionNet.hs b/src/Language/Elemental/InteractionNet.hs new file mode 100644 index 0000000..3f1431e --- /dev/null +++ b/src/Language/Elemental/InteractionNet.hs @@ -0,0 +1,1660 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralisedNewtypeDeriving #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} + +{-| + Interaction net based evaluator for compiling Elemental. + + This evaluator makes the following assumptions about the input: + - The program is total. + - There are no edges between ports whose types don't unify. + + The easiest way of using the evaluator is to use 'reduce'. + + Should you choose to manually generate an interaction net instead of using + existing functions, be careful not to violate these assumptions, else your + net may fail to evaluate. + + For better performance, the evaluator tracks redundant data about the net: + interacting nodes are stored in 'INetPairs'. The evaluator assumes that the + data stored there is correct and complete, and it will neither verify that a + pair is interacting nor look elsewhere for missing interacting pairs. Hence, + it is highly recommended to only use the exported helper functions, never + manually change 'INet' or 'INetPairs', and always keep an 'INet' and its + 'INetPairs' together. +-} +module Language.Elemental.InteractionNet + ( INet(..) + , _INet + , INetPairs(..) + , _INetPairs + , INetSize(..) + , _INetSize + , INetF(..) + , Ref(..) + , Level(..) + , BuildType(..) + , HasRewriter + , compileINet + , reduce + , propagate1 + , propagate2 + , mkLambda + , mkChurchBool + , newNode + , newName + , newLabel + , linkNodes + -- * Debugging + , TraceRewrite(..) + , traceRewrite + , deleteBoxes + ) where + +import Control.Algebra (Has, send) +import Control.Carrier.Writer.Church (Writer, execWriter, tell) +import Control.Effect.State (State, get, gets, modify) +import Control.Lens.At (At(at), Index, Ixed(ix), IxValue) +import Control.Lens.Cons (_head) +import Control.Lens.Fold (IndexedFold, filtered, folded, imapMOf_, (^?)) +import Control.Lens.Getter (to) +import Control.Lens.Indexed (Indexed(Indexed), indexing) +import Control.Lens.Iso (Iso', iso) +import Control.Lens.Setter ((.~), (%~), (?~)) +import Control.Lens.Traversal (traversed) +import Control.Lens.Wrapped (_Wrapped) +import Data.DList (snoc) +import Data.Foldable (find) +import Data.IntMap.Strict qualified as IM +import Data.IntSet qualified as IS +import Data.Maybe (fromMaybe) +import Prettyprinter + +import Language.Elemental.Backend qualified as B +import Language.Elemental.Singleton + +newtype INet = INet { unINet :: IM.IntMap (INetF Ref) } + deriving newtype (Semigroup, Monoid) + +instance Pretty INet where + pretty = concatWith mkLine . fmap go . IM.assocs . unINet + where + go (idx, v) = pretty idx <+> "=" <+> pretty v + mkLine a b = a <> line <> b + +instance Ixed INet where + ix idx = _INet . ix idx + {-# INLINE ix #-} + +instance At INet where + at idx = _INet . at idx + {-# INLINE at #-} + +type instance Index INet = Int +type instance IxValue INet = INetF Ref + +_INet :: Iso' INet (IM.IntMap (INetF Ref)) +_INet = iso unINet INet +{-# INLINE _INet #-} + +{-| + A set of interacting nodes in an interaction net. + + This data structure must be kept in sync with its 'INet', else weird things + will happen. +-} +newtype INetPairs = INetPairs { unINetPairs :: IS.IntSet } + deriving newtype (Semigroup, Monoid) + +_INetPairs :: Iso' INetPairs IS.IntSet +_INetPairs = iso unINetPairs INetPairs +{-# INLINE _INetPairs #-} + +-- | A reference to a port in an interaction net. +data Ref = Ref + { refNode :: {-# UNPACK #-} !Int + -- ^ The index of the port's node. + , refPort :: {-# UNPACK #-} !Int + -- ^ The index of the port within the node's port list. + } deriving stock (Eq, Ord, Show) + +instance Pretty Ref where + pretty r0 = pretty (refNode r0) <> ":" <> pretty (refPort r0) + +{-| + The "level" of a node. + + 'DupNode'-related interactions use this to determine whether two nodes + annihilate (same level) or commute (different levels). +-} +newtype Level = Level { unLevel :: Int } + deriving newtype (Enum, Eq, Ord, Num, Pretty) + +{-| + A node in the interaction net. + + The documentation for each constructor indicates the intended type for the + node's ports. + + +----------+--------------------------------------------------------+ + | Type | Description | + +==========+========================================================+ + | @a -> b@ | A function taking an @a@ as input and returning a @b@. | + +----------+--------------------------------------------------------+ + | @i{n}@ | An operand of the specified type (e.g. @i8@). | + +----------+--------------------------------------------------------+ + | @IO a@ | An IO action returning a value of type @a@. | + +----------+--------------------------------------------------------+ + | @B@ | A list of blocks. | + +----------+--------------------------------------------------------+ + | @CB@ | A fully-reduced (i.e. completed) list of blocks. | + +----------+--------------------------------------------------------+ + | @NB@ | A list of named blocks. | + +----------+--------------------------------------------------------+ + | @T@ | A tunnel for pairing 'DupNode' when sharing blocks. | + +----------+--------------------------------------------------------+ +-} +data INetF a + -- | (a -> b, a, b) + = AppNode a a a + -- | (a -> b, a, b) + | LamNode a a a + -- | (a, a, a) + | DupNode !Level a a a + -- | a + | DeadNode a + -- | (a, a) and the non-principal node is in a new box. + | BoxNode !Level a a + -- FFI + -- | CB + | ExternalRootNode B.ForeignName [B.Named B.Type] B.Type a + -- | CB + | PrivateRootNode B.Name B.Name a + -- | (CB, B) + | AccumIONode B.IBlock a a + -- | (NB, CB) + | AccumNBNode B.BlockList a a + -- | i{n} + | OperandNode B.Operand a + -- | {... ->} i{n} + | OperandANode (B.Partial B.Operand) a + -- | (i{m}, {... ->} i{n}) + | OperandPNode (B.Partial B.Operand) a a + -- | B + | IONode B.BlockList a + -- | {... ->} IO i{n} + | IOANode B.Type (B.Partial B.Instruction) a + -- | (i{m}, {... ->} IO i{n}) + | IOPNode (B.Partial B.Instruction) a a + -- | (IO a, (a -> B) -> B) + | IOPureNode a a + -- | IO a + | IOContNode B.Instruction a + -- | (B, i{n}) + | ReturnCNode a a + -- | (i{n}, B) + | ReturnFNode a a + -- | (i{n}, B) + | TailCallNode B.Name a a + -- | (IO a, (a -> IO b) -> IO b) + | Bind0BNode a a + -- | (IO a, a -> B, B) + | Bind0CNode a a a + -- | (IO a, B, B) + | Bind0FNode B.Name a a a + -- | (B, IO a, (a -> B) -> B) + | Bind1CNode B.Name a a a + -- | (B, B) + | Bind1FNode (B.Named B.Instruction) a a + -- | (B, i{n}, B, B) + | Branch0CNode a a a a + -- | (i{n}, B, B, B) + | Branch0FNode a a a a + -- | (CB, NB) + | LabelNode B.Label a a + -- | NB + | NamedBlockNode B.NamedBlockList a + -- | (NB, NB, NB) + | Merge0Node a a a + -- | (NB, NB) + | Merge1Node B.NamedBlockList a a + -- | (a, T, a) + | TBuild1Node !Level BuildType B.Operand a a a + -- | (a, T, T, a) + | TBuild2Node !Level BuildType B.Operand a a a a + -- | (T, T) + | TCross1Node !Level B.Operand a a + -- | (T, T, T) + | TCross2Node !Level B.Operand a a a + -- | (B, T, B) + | TEntryNode a a a + -- | (T, T, T) + | TSplitNode a a a + -- | T + | TCloseNode a + -- | (T, a, a) + | TLeaveNode BuildType a a a + -- | (T, T, T, i1) + | TMatchNode !Level a a a a + -- | (a, i{n} -> a, i{n}) + | PArgumentNode (Maybe B.Type) a a a + -- | (a, a) + | PReduceNode a a + -- | (B, i{n}, B) + | DupIONode !Level a a a + deriving stock (Foldable, Functor, Traversable) + +instance Pretty a => Pretty (INetF a) where + pretty (AppNode r0 r1 r2) = "App" <+> pretty r0 <+> pretty r1 <+> pretty r2 + pretty (LamNode r0 r1 r2) = "Lam" <+> pretty r0 <+> pretty r1 <+> pretty r2 + pretty (DupNode lvl r0 r1 r2) + = "Dup" <+> pretty lvl <+> pretty r0 <+> pretty r1 <+> pretty r2 + pretty (DeadNode r0) = "Dead" <+> pretty r0 + pretty (BoxNode lvl r0 r1) + = "Box" <+> pretty lvl <+> pretty r0 <+> pretty r1 + pretty (ExternalRootNode fname args ret r0) + = "ExternalRoot" <+> pretty r0 + <+> pretty fname <+> tupled (pretty <$> args) <+> pretty ret + pretty (PrivateRootNode fname namep r0) + = "PrivateRoot" <+> pretty r0 <+> pretty fname <+> pretty namep + pretty (AccumIONode ib r0 r1) + = "AccumIO" <+> pretty r0 <+> pretty r1 <> nest 4 (line <> pretty ib) + pretty (AccumNBNode bs r0 r1) + = "AccumNB" <+> pretty r0 <+> pretty r1 <> nest 4 (line <> pretty bs) + <> nest 4 (line <> pretty bs) + pretty (OperandNode op r0) = "Operand" <+> pretty r0 <+> pretty op + pretty (OperandANode opp r0) = "OperandA" <+> pretty r0 <+> pretty opp + pretty (OperandPNode opp r0 r1) + = "OperandP" <+> pretty r0 <+> pretty r1 <+> pretty opp + pretty (IONode bs r0) = "IO" <+> pretty r0 <> nest 4 (line <> pretty bs) + pretty (IOANode t iop r0) = "IOA" <+> pretty r0 <+> pretty t <+> pretty iop + pretty (IOPNode iop r0 r1) + = "IOP" <+> pretty r0 <+> pretty r1 <+> pretty iop + pretty (IOPureNode r0 r1) = "IOPure" <+> pretty r0 <+> pretty r1 + pretty (IOContNode instr r0) + = "IOCont" <+> pretty r0 <> nest 4 (line <> pretty instr) + pretty (ReturnCNode r0 r1) = "ReturnC" <+> pretty r0 <+> pretty r1 + pretty (ReturnFNode r0 r1) = "ReturnF" <+> pretty r0 <+> pretty r1 + pretty (TailCallNode name r0 r1) + = "TailCall" <+> pretty r0 <+> pretty r1 <+> pretty name + pretty (Bind0BNode r0 r1) = "Bind0B" <+> pretty r0 <+> pretty r1 + pretty (Bind0CNode r0 r1 r2) + = "Bind0C" <+> pretty r0 <+> pretty r1 <+> pretty r2 + pretty (Bind0FNode name r0 r1 r2) + = "Bind0F" <+> pretty r0 <+> pretty r1 <+> pretty r2 <+> pretty name + pretty (Bind1CNode name r0 r1 r2) + = "Bind1C" <+> pretty r0 <+> pretty r1 <+> pretty r2 <+> pretty name + pretty (Bind1FNode instr r0 r1) + = "Bind1F" <+> pretty r0 <+> pretty r1 <> nest 4 (line <> pretty instr) + pretty (Branch0CNode r0 r1 r2 r3) + = "Branch0C" <+> pretty r0 <+> pretty r1 <+> pretty r2 <+> pretty r3 + pretty (Branch0FNode r0 r1 r2 r3) + = "Branch0F" <+> pretty r0 <+> pretty r1 <+> pretty r2 <+> pretty r3 + pretty (LabelNode lbl r0 r1) + = "Label" <+> pretty r0 <+> pretty r1 <+> pretty lbl + pretty (NamedBlockNode nbs r0) + = "NamedBlock" <+> pretty r0 <> nest 4 (line <> pretty nbs) + pretty (Merge0Node r0 r1 r2) + = "Merge0" <+> pretty r0 <+> pretty r1 <+> pretty r2 + pretty (Merge1Node nbs r0 r1) + = "Merge1" <+> pretty r0 <+> pretty r1 <> nest 4 (line <> pretty nbs) + pretty (TBuild1Node lvl t namep r0 r1 r2) = "TBuild1" + <+> pretty lvl <+> pretty r0 <+> pretty r1 <+> pretty r2 + <+> pretty t <+> pretty namep + pretty (TBuild2Node lvl t namep r0 r1 r2 r3) = "TBuild2" + <+> pretty lvl <+> pretty r0 <+> pretty r1 <+> pretty r2 <+> pretty r3 + <+> pretty t <+> pretty namep + pretty (TCross1Node lvl namep r0 r1) + = "TCross1" <+> pretty lvl <+> pretty r0 <+> pretty r1 <+> pretty namep + pretty (TCross2Node lvl namep r0 r1 r2) + = "TCross2" <+> pretty lvl <+> pretty r0 <+> pretty r1 <+> pretty r2 + <+> pretty namep + pretty (TEntryNode r0 r1 r2) + = "TEntry" <+> pretty r0 <+> pretty r1 <+> pretty r2 + pretty (TSplitNode r0 r1 r2) + = "TSplit" <+> pretty r0 <+> pretty r1 <+> pretty r2 + pretty (TCloseNode r0) = "TClose" <+> pretty r0 + pretty (TLeaveNode t r0 r1 r2) + = "TLeave" <+> pretty r0 <+> pretty r1 <+> pretty r2 <+> pretty t + pretty (TMatchNode lvl r0 r1 r2 r3) = "TMatch" + <+> pretty lvl <+> pretty r0 <+> pretty r1 <+> pretty r2 <+> pretty r3 + pretty (PArgumentNode t r0 r1 r2) + = "PArgument" <+> pretty r0 <+> pretty r1 <+> pretty r2 <+> pretty t + pretty (PReduceNode r0 r1) = "PReduce" <+> pretty r0 <+> pretty r1 + pretty (DupIONode lvl r0 r1 r2) + = "DupIO" <+> pretty lvl <+> pretty r0 <+> pretty r1 <+> pretty r2 + +instance Ixed (INetF a) where + ix idx f = indexing traverse $ Indexed go + where + go idx' x + | idx == idx' = f x + | otherwise = pure x + {-# INLINE ix #-} + +type instance Index (INetF a) = Int +type instance IxValue (INetF a) = a + +data BuildType = BuildOperand | BuildIO + deriving stock (Eq, Ord, Show, Read) + +instance Pretty BuildType where + pretty BuildOperand = "Operand" + pretty BuildIO = "IO" + +-- | Compiles an interaction net and a list of externals into a backend program. +compileINet + :: (HasRewriter sig m, Has TraceRewrite sig m) + => [B.ForeignNamed B.External] -> m B.Program +compileINet exts = B.Program exts <$> reduce +{-# INLINABLE compileINet #-} + +-- | Reduces the interaction net into a list of functions. +reduce :: (HasRewriter sig m, Has TraceRewrite sig m) => m [B.NamedFunction] +reduce = execWriter $ try *> lintFinal + where + go r0 = do + net <- get + let r1 = derefPort n0 0 + n1 = derefNode net $ refNode r1 + n0 = derefNode net $ refNode r0 + traceRewrite r0 r1 n0 n1 $ do + reduceNode n0 n1 + safeDelete r0 n0 + safeDelete r1 n1 + try + + try :: (HasRewriter sig m, Has TraceRewrite sig m + , Has (Writer [B.NamedFunction]) sig m) + => m () + try = do + net <- get + case net ^? _INetPairs . _Wrapped . _head of + Nothing -> pure () + Just rn0 -> go $ Ref rn0 0 + + isRoot :: INetF Ref -> Bool + isRoot ExternalRootNode {} = True + isRoot PrivateRootNode {} = True + isRoot TEntryNode {} = True + isRoot _ = False + + derefNode :: INet -> Int -> INetF Ref + derefNode net rn0 = fromMaybe (error "reduce: missing node") + $ net ^? ix rn0 + + derefPort :: INetF Ref -> Int -> Ref + derefPort n0 r1 = fromMaybe (error "reduce: missing port") + $ n0 ^? ix r1 + + -- Handling self-reference during reduction is far more tedious. + safeDelete :: HasRewriter sig m => Ref -> INetF Ref -> m () + safeDelete (Ref rn0 _) n0 = do + imapMOf_ targets relink n0 + modify $ _INet . at rn0 .~ Nothing + modify $ _INetPairs %~ IS.delete rn0 + where + targets :: IndexedFold Int (INetF Ref) Int + targets = traversed . filtered ((== rn0) . refNode) . to refPort + + relink :: HasRewriter sig m => Int -> Int -> m () + relink rp1 rp2 = do + net <- get + let n3 = derefNode net rn0 + linkNodes (derefPort n3 rp1) (derefPort n3 rp2) + + lintFinal :: HasRewriter sig m => m () + lintFinal = do + net <- get + case find isRoot $ unINet net of + Nothing -> pure () + Just _ -> do + deleteBoxes + net' <- get @INet + error . show $ "lint: failed to reduce root" + <> line <> pretty net' +{-# INLINABLE reduce #-} + +reduceNode + :: (HasRewriter sig m, Has (Writer [B.NamedFunction]) sig m) + => INetF Ref -> INetF Ref -> m () +reduceNode (AppNode _ r0 r1) (LamNode _ r2 r3) = do + rn4 <- newNode $ BoxNode 0 () () + rn5 <- newNode $ BoxNode 0 () () + linkNodes r0 $ Ref rn4 0 + linkNodes r1 $ Ref rn5 0 + linkNodes r2 $ Ref rn4 1 + linkNodes r3 $ Ref rn5 1 +reduceNode n0@LamNode {} n1@AppNode {} = reduceNode n1 n0 +reduceNode (AppNode _ r0 r1) (DupNode lvl _ r2 r3) + = commute2 AppNode (DupNode lvl) r0 r1 r2 r3 +reduceNode n0@DupNode {} n1@AppNode {} = reduceNode n1 n0 +reduceNode (LamNode _ r0 r1) (DupNode lvl _ r2 r3) + = commute2 LamNode (DupNode $ succ lvl) r0 r1 r2 r3 +reduceNode n0@DupNode {} n1@LamNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl1 _ r0 r1) (DupNode lvl2 _ r2 r3) + | lvl1 == lvl2 = linkNodes r0 r2 *> linkNodes r1 r3 + | otherwise = commute2 (DupNode lvl1) (DupNode lvl2) r0 r1 r2 r3 +reduceNode (AppNode _ r0 r1) (DeadNode _) = propagate2 r0 r1 DeadNode +reduceNode n0@DeadNode {} n1@AppNode {} = reduceNode n1 n0 +reduceNode (LamNode _ r0 r1) (DeadNode _) = propagate2 r0 r1 DeadNode +reduceNode n0@DeadNode {} n1@LamNode {} = reduceNode n1 n0 +reduceNode (DupNode _ _ r0 r1) (DeadNode _) = propagate2 r0 r1 DeadNode +reduceNode n0@DeadNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DeadNode _) (DeadNode _) = pure () +-- Book-keeping +reduceNode (AppNode _ r0 r1) (BoxNode lvl _ r2) + = commute1 AppNode (BoxNode lvl) r0 r1 r2 +reduceNode n0@BoxNode {} n1@AppNode {} = reduceNode n1 n0 +reduceNode (LamNode _ r0 r1) (BoxNode lvl _ r2) + = commute1 LamNode (BoxNode $ succ lvl) r0 r1 r2 +reduceNode n0@BoxNode {} n1@LamNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl0 _ r0 r1) (BoxNode lvl1 _ r2) = commute1 + (DupNode $ if lvl0 < lvl1 then lvl0 else succ lvl0) + (BoxNode lvl1) + r0 r1 r2 +reduceNode n0@BoxNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (BoxNode _ _ r0) (DeadNode _) = propagate1 r0 DeadNode +reduceNode n0@DeadNode {} n1@BoxNode {} = reduceNode n1 n0 +reduceNode (BoxNode lvl0 _ r0) (BoxNode lvl1 _ r1) + | lvl0 == lvl1 = linkNodes r0 r1 + | otherwise = commute0 + (BoxNode $ if lvl0 < lvl1 then lvl0 else succ lvl0) + (BoxNode $ if lvl1 < lvl0 then lvl1 else succ lvl1) + r0 r1 +-- FFI +reduceNode (ExternalRootNode fname args ret _) (IONode b _) + = tell @[B.NamedFunction] $ pure $ Right + $ B.ExternalName fname B.:= B.Function args ret b +reduceNode n0@IONode {} n1@ExternalRootNode {} = reduceNode n1 n0 +reduceNode (PrivateRootNode name namep _) (IONode bs _) + = tell @[B.NamedFunction] $ pure $ Left + $ name B.:= B.ImplicitFunction [namep B.:= B.IntType 1] bs +reduceNode n0@IONode {} n1@PrivateRootNode {} = reduceNode n1 n0 +reduceNode (AccumIONode ib _ r0) (IONode bs _) = propagate1 r0 + $ IONode $ B._entryBlock . B._blockInstrs %~ (B.unIBlock ib <>) $ bs +reduceNode n0@IONode {} n1@AccumIONode {} = reduceNode n1 n0 +reduceNode (AccumIONode ib _ r0) (ReturnCNode _ r1) = do + rn2 <- newNode $ AccumIONode ib () () + rn3 <- newNode $ ReturnFNode () () + rn4 <- newNode $ PReduceNode () () + linkNodes (Ref rn2 0) (Ref rn3 1) + linkNodes (Ref rn3 0) (Ref rn4 1) + linkNodes r0 $ Ref rn2 1 + linkNodes r1 $ Ref rn4 0 +reduceNode n0@ReturnCNode {} n1@AccumIONode {} = reduceNode n1 n0 +reduceNode (AccumIONode ib _ r0) (Bind1CNode name _ r1 r2) = do + rn3 <- newNode $ AccumIONode ib () () + rn4 <- newNode $ Bind0FNode name () () () + rn5 <- newNode $ PReduceNode () () + linkNodes (Ref rn3 0) (Ref rn4 2) + linkNodes (Ref rn4 0) (Ref rn5 1) + linkNodes r0 $ Ref rn3 1 + linkNodes r1 $ Ref rn5 0 + linkNodes r2 $ Ref rn4 1 +reduceNode n0@Bind1CNode {} n1@AccumIONode {} = reduceNode n1 n0 +reduceNode (AccumIONode ib _ r0) (Bind1FNode instr _ r1) = do + let ib' = B._IBlock %~ (`snoc` instr) $ ib + rn2 <- newNode $ AccumIONode ib' () () + linkNodes r0 $ Ref rn2 1 + linkNodes r1 $ Ref rn2 0 +reduceNode n0@Bind1FNode {} n1@AccumIONode {} = reduceNode n1 n0 +reduceNode (AccumIONode ib _ r0) (Branch0CNode _ r1 r2 r3) = do + rn4 <- newNode $ AccumIONode ib () () + rn5 <- newNode $ Branch0FNode () () () () + rn6 <- newNode $ PReduceNode () () + linkNodes (Ref rn4 0) (Ref rn5 3) + linkNodes (Ref rn5 0) (Ref rn6 1) + linkNodes r0 $ Ref rn4 1 + linkNodes r1 $ Ref rn6 0 + linkNodes r2 $ Ref rn5 1 + linkNodes r3 $ Ref rn5 2 +reduceNode n0@Branch0CNode {} n1@AccumIONode {} = reduceNode n1 n0 +reduceNode (AccumNBNode bs _ r0) (NamedBlockNode nbs _) + = propagate1 r0 $ IONode $ B._namedBlocks %~ (<>) nbs $ bs +reduceNode n0@NamedBlockNode {} n1@AccumNBNode {} = reduceNode n1 n0 +reduceNode (OperandANode opp _) (AppNode _ r0 r1) = do + rn2 <- newNode $ PArgumentNode Nothing () () () + propagate1 (Ref rn2 1) $ OperandANode opp + linkNodes r0 $ Ref rn2 2 + linkNodes r1 $ Ref rn2 0 +reduceNode n0@AppNode {} n1@OperandANode {} = reduceNode n1 n0 +reduceNode (OperandPNode opp _ r0) (OperandNode op _) + = case B.addOperand op opp of + Left opp' -> mkLambda r0 $ OperandPNode opp' + Right op' -> propagate1 r0 $ OperandNode op' +reduceNode n0@OperandNode {} n1@OperandPNode {} = reduceNode n1 n0 +reduceNode (IOANode t iop _) (AppNode _ r0 r1) = do + rn2 <- newNode $ PArgumentNode (Just t) () () () + propagate1 (Ref rn2 1) $ IOANode t iop + linkNodes r0 $ Ref rn2 2 + linkNodes r1 $ Ref rn2 0 +reduceNode n0@AppNode {} n1@IOANode {} = reduceNode n1 n0 +reduceNode (IOPNode iop _ r0) (OperandNode op _) + = case B.addOperand op iop of + Left iop' -> mkLambda r0 $ IOPNode iop' + Right instr -> propagate1 r0 $ IOContNode instr +reduceNode n0@OperandNode {} n1@IOPNode {} = reduceNode n1 n0 +reduceNode (ReturnFNode _ r0) (OperandNode op _) + = propagate1 r0 $ IONode $ B.BlockList (B.Block mempty $ B.Return op) mempty +reduceNode n0@OperandNode {} n1@ReturnFNode {} = reduceNode n1 n0 +reduceNode (TailCallNode name _ r0) (OperandNode op _) = propagate1 r0 + $ IONode $ B.BlockList (B.Block mempty $ B.TailCall name op) mempty +reduceNode (Bind0BNode _ r0) (IOPureNode _ r1) = reassocPure r0 r1 +reduceNode n0@IOPureNode {} n1@Bind0BNode {} = reduceNode n1 n0 +reduceNode (Bind0BNode _ r0) (IOContNode instr _) = do + rn1 <- newNode $ IOContNode instr () + reassocCont (B.instrType instr) r0 $ Ref rn1 0 +reduceNode n0@IOContNode {} n1@Bind0BNode {} = reduceNode n1 n0 +reduceNode (Bind0BNode _ r0) (PArgumentNode (Just t) _ r1 r2) = do + rn3 <- newNode $ PArgumentNode (Just t) () () () + linkNodes r1 $ Ref rn3 1 + linkNodes r2 $ Ref rn3 2 + reassocCont t r0 $ Ref rn3 0 +reduceNode n0@PArgumentNode {} n1@Bind0BNode {} = reduceNode n1 n0 +reduceNode (Bind0CNode _ r0 r1) (IOPureNode _ r2) = do + rn3 <- newNode $ AppNode () () () + linkNodes r0 $ Ref rn3 1 + linkNodes r1 $ Ref rn3 2 + linkNodes r2 $ Ref rn3 0 +reduceNode n0@IOPureNode {} n1@Bind0CNode {} = reduceNode n1 n0 +reduceNode (Bind0FNode name _ r0 r1) (IOContNode instr _) = do + rn2 <- newNode $ Bind1FNode (name B.:= instr) () () + linkNodes r0 $ Ref rn2 1 + linkNodes r1 $ Ref rn2 0 +reduceNode n0@IOContNode {} n1@Bind0FNode {} = reduceNode n1 n0 +reduceNode (Branch0FNode _ r0 r1 r2) (OperandNode op _) = mkBranch1 op r0 r1 r2 +reduceNode n0@OperandNode {} n1@Branch0FNode {} = reduceNode n1 n0 +reduceNode (LabelNode lbl _ r0) (IONode bs _) = propagate1 r0 $ NamedBlockNode + $ B.NamedBlockList $ IM.insert (B.unLabel lbl) (B.entryBlock bs) + $ B.unNamedBlockList $ B.namedBlocks bs +reduceNode n0@IONode {} n1@LabelNode {} = reduceNode n1 n0 +reduceNode (Merge0Node _ r0 r1) (NamedBlockNode nbs _) = do + rn2 <- newNode $ Merge1Node nbs () () + linkNodes r0 $ Ref rn2 0 + linkNodes r1 $ Ref rn2 1 +reduceNode n0@NamedBlockNode {} n1@Merge0Node {} = reduceNode n1 n0 +reduceNode (Merge1Node nbs0 _ r0) (NamedBlockNode nbs1 _) + = propagate1 r0 $ NamedBlockNode $ nbs0 <> nbs1 +reduceNode n0@NamedBlockNode {} n1@Merge1Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node lvl t namep _ r0 r1) (LamNode _ r2 r3) = do + rn4 <- newNode $ TBuild1Node lvl t namep () () () + rn5 <- newNode $ LamNode () () () + linkNodes (Ref rn4 2) (Ref rn5 2) + linkNodes r0 $ Ref rn4 1 + linkNodes r1 $ Ref rn5 0 + linkNodes r2 $ Ref rn5 1 + linkNodes r3 $ Ref rn4 0 +reduceNode n0@LamNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node lvl t namep _ r0 r1 r2) (LamNode _ r3 r4) = do + rn5 <- newNode $ TBuild2Node lvl t namep () () () () + rn6 <- newNode $ LamNode () () () + linkNodes (Ref rn5 3) (Ref rn6 2) + linkNodes r0 $ Ref rn5 1 + linkNodes r1 $ Ref rn5 2 + linkNodes r2 $ Ref rn6 0 + linkNodes r3 $ Ref rn6 1 + linkNodes r4 $ Ref rn5 0 +reduceNode n0@LamNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node _ _ _ _ r0 r1) (OperandNode op _) + = propagate1 r0 TCloseNode *> propagate1 r1 (OperandNode op) +reduceNode n0@OperandNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node _ _ _ _ r0 r1 r2) (OperandNode op _) + = propagate2 r0 r1 TCloseNode *> propagate1 r2 (OperandNode op) +reduceNode n0@OperandNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node _ _ _ _ r0 r1) (OperandANode opp _) + = propagate1 r0 TCloseNode *> propagate1 r1 (OperandANode opp) +reduceNode n0@OperandANode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node _ _ _ _ r0 r1 r2) (OperandANode opp _) + = propagate2 r0 r1 TCloseNode *> propagate1 r2 (OperandANode opp) +reduceNode n0@OperandANode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node _ _ _ _ r0 r1) (IONode bs _) + = propagate1 r0 TCloseNode *> propagate1 r1 (IONode bs) +reduceNode n0@IONode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node _ _ _ _ r0 r1 r2) (IONode bs _) + = propagate2 r0 r1 TCloseNode *> propagate1 r2 (IONode bs) +reduceNode n0@IONode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node _ _ _ _ r0 r1) (IOANode t iop _) + = propagate1 r0 TCloseNode *> propagate1 r1 (IOANode t iop) +reduceNode n0@IOANode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node _ _ _ _ r0 r1 r2) (IOANode t iop _) + = propagate2 r0 r1 TCloseNode *> propagate1 r2 (IOANode t iop) +reduceNode n0@IOANode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node _ _ _ _ r0 r1) (IOContNode instr _) + = propagate1 r0 TCloseNode *> propagate1 r1 (IOContNode instr) +reduceNode n0@IOContNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node _ _ _ _ r0 r1 r2) (IOContNode instr _) + = propagate2 r0 r1 TCloseNode *> propagate1 r2 (IOContNode instr) +reduceNode n0@IOContNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node lvl _ namep _ r0 r1) (ReturnCNode _ r2) = do + rn3 <- newNode $ TBuild1Node lvl BuildOperand namep () () () + rn4 <- newNode $ ReturnFNode () () + rn5 <- newNode $ PReduceNode () () + linkNodes (Ref rn3 2) (Ref rn5 0) + linkNodes (Ref rn4 0) (Ref rn5 1) + linkNodes r0 $ Ref rn3 1 + linkNodes r1 $ Ref rn4 1 + linkNodes r2 $ Ref rn3 0 +reduceNode n0@ReturnCNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node lvl _ namep _ r0 r1 r2) (ReturnCNode _ r3) = do + rn4 <- newNode $ TBuild2Node lvl BuildOperand namep () () () () + rn5 <- newNode $ ReturnFNode () () + rn6 <- newNode $ PReduceNode () () + linkNodes (Ref rn4 3) (Ref rn6 0) + linkNodes (Ref rn5 0) (Ref rn6 1) + linkNodes r0 $ Ref rn4 1 + linkNodes r1 $ Ref rn4 2 + linkNodes r2 $ Ref rn5 1 + linkNodes r3 $ Ref rn4 0 +reduceNode n0@ReturnCNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node lvl _ namep _ r0 r1) (Bind1CNode name _ r2 r3) = do + rn4 <- newNode $ TBuild1Node lvl BuildOperand namep () () () + rn5 <- newNode $ TBuild1Node lvl BuildIO namep () () () + rn6 <- newNode $ Bind0FNode name () () () + rn7 <- newNode $ TSplitNode () () () + rn8 <- newNode $ PReduceNode () () + linkNodes (Ref rn4 1) (Ref rn7 1) + linkNodes (Ref rn4 2) (Ref rn8 0) + linkNodes (Ref rn5 1) (Ref rn7 2) + linkNodes (Ref rn5 2) (Ref rn6 1) + linkNodes (Ref rn6 0) (Ref rn8 1) + linkNodes r0 $ Ref rn7 0 + linkNodes r1 $ Ref rn6 2 + linkNodes r2 $ Ref rn4 0 + linkNodes r3 $ Ref rn5 0 +reduceNode n0@Bind1CNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node lvl _ namep _ r0 r1 r2) (Bind1CNode name _ r3 r4) = do + rn5 <- newNode $ TBuild2Node lvl BuildOperand namep () () () () + rn6 <- newNode $ TBuild2Node lvl BuildIO namep () () () () + rn7 <- newNode $ Bind0FNode name () () () + rn8 <- newNode $ TSplitNode () () () + rn9 <- newNode $ TSplitNode () () () + rn10 <- newNode $ PReduceNode () () + linkNodes (Ref rn5 1) (Ref rn8 1) + linkNodes (Ref rn5 2) (Ref rn9 1) + linkNodes (Ref rn5 3) (Ref rn10 0) + linkNodes (Ref rn6 1) (Ref rn8 2) + linkNodes (Ref rn6 2) (Ref rn9 2) + linkNodes (Ref rn6 3) (Ref rn7 1) + linkNodes (Ref rn7 0) (Ref rn10 1) + linkNodes r0 $ Ref rn8 0 + linkNodes r1 $ Ref rn9 0 + linkNodes r2 $ Ref rn7 2 + linkNodes r3 $ Ref rn5 0 + linkNodes r4 $ Ref rn6 0 +reduceNode n0@Bind1CNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node lvl _ namep _ r0 r1) (Bind1FNode instr _ r2) = do + rn3 <- newNode $ TBuild1Node lvl BuildIO namep () () () + rn4 <- newNode $ Bind1FNode instr () () + linkNodes (Ref rn3 2) (Ref rn4 1) + linkNodes r0 $ Ref rn3 1 + linkNodes r1 $ Ref rn4 0 + linkNodes r2 $ Ref rn3 0 +reduceNode n0@Bind1FNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node lvl _ namep _ r0 r1 r2) (Bind1FNode instr _ r3) = do + rn4 <- newNode $ TBuild2Node lvl BuildIO namep () () () () + rn5 <- newNode $ Bind1FNode instr () () + linkNodes (Ref rn4 3) (Ref rn5 1) + linkNodes r0 $ Ref rn4 1 + linkNodes r1 $ Ref rn4 2 + linkNodes r2 $ Ref rn5 0 + linkNodes r3 $ Ref rn4 0 +reduceNode n0@Bind1FNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node lvl _ namep _ r0 r1) (Branch0CNode _ r2 r3 r4) = do + rn5 <- newNode $ TBuild1Node lvl BuildOperand namep () () () + rn6 <- newNode $ TBuild1Node lvl BuildIO namep () () () + rn7 <- newNode $ TBuild1Node lvl BuildIO namep () () () + rn8 <- newNode $ Branch0CNode () () () () + rn9 <- newNode $ TSplitNode () () () + rn10 <- newNode $ TSplitNode () () () + linkNodes (Ref rn5 1) (Ref rn9 1) + linkNodes (Ref rn5 2) (Ref rn8 1) + linkNodes (Ref rn6 1) (Ref rn10 1) + linkNodes (Ref rn6 2) (Ref rn8 2) + linkNodes (Ref rn7 1) (Ref rn10 2) + linkNodes (Ref rn7 2) (Ref rn8 3) + linkNodes (Ref rn9 2) (Ref rn10 0) + linkNodes r0 $ Ref rn9 0 + linkNodes r1 $ Ref rn8 0 + linkNodes r2 $ Ref rn5 0 + linkNodes r3 $ Ref rn6 0 + linkNodes r4 $ Ref rn7 0 +reduceNode n0@Branch0CNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node lvl _ namep _ r0 r1 r2) (Branch0CNode _ r3 r4 r5) = do + rn6 <- newNode $ TBuild2Node lvl BuildOperand namep () () () () + rn7 <- newNode $ TBuild2Node lvl BuildIO namep () () () () + rn8 <- newNode $ TBuild2Node lvl BuildIO namep () () () () + rn9 <- newNode $ Branch0CNode () () () () + rn10 <- newNode $ TSplitNode () () () + rn11 <- newNode $ TSplitNode () () () + rn12 <- newNode $ TSplitNode () () () + rn13 <- newNode $ TSplitNode () () () + linkNodes (Ref rn6 1) (Ref rn10 1) + linkNodes (Ref rn6 2) (Ref rn11 1) + linkNodes (Ref rn6 3) (Ref rn9 1) + linkNodes (Ref rn7 1) (Ref rn12 1) + linkNodes (Ref rn7 2) (Ref rn13 1) + linkNodes (Ref rn7 3) (Ref rn9 2) + linkNodes (Ref rn8 1) (Ref rn12 2) + linkNodes (Ref rn8 2) (Ref rn13 2) + linkNodes (Ref rn8 3) (Ref rn9 3) + linkNodes (Ref rn10 2) (Ref rn12 0) + linkNodes (Ref rn11 2) (Ref rn13 0) + linkNodes r0 $ Ref rn10 0 + linkNodes r1 $ Ref rn11 0 + linkNodes r2 $ Ref rn9 0 + linkNodes r3 $ Ref rn6 0 + linkNodes r4 $ Ref rn7 0 + linkNodes r5 $ Ref rn8 0 +reduceNode n0@Branch0CNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TBuild1Node lvl _ namep _ r0 r1) (PArgumentNode t _ r2 r3) = do + rn4 <- newNode $ TBuild1Node lvl BuildOperand namep () () () + rn5 <- newNode $ TBuild1Node lvl BuildOperand namep () () () + rn6 <- newNode $ PArgumentNode t () () () + rn7 <- newNode $ TSplitNode () () () + linkNodes (Ref rn4 1) (Ref rn7 1) + linkNodes (Ref rn4 2) (Ref rn6 1) + linkNodes (Ref rn5 1) (Ref rn7 2) + linkNodes (Ref rn5 2) (Ref rn6 2) + linkNodes r0 $ Ref rn7 0 + linkNodes r1 $ Ref rn6 0 + linkNodes r2 $ Ref rn4 0 + linkNodes r3 $ Ref rn5 0 +reduceNode n0@PArgumentNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node lvl _ namep _ r0 r1 r2) (PArgumentNode t _ r3 r4) = do + rn5 <- newNode $ TBuild2Node lvl BuildOperand namep () () () () + rn6 <- newNode $ TBuild2Node lvl BuildOperand namep () () () () + rn7 <- newNode $ PArgumentNode t () () () + rn8 <- newNode $ TSplitNode () () () + rn9 <- newNode $ TSplitNode () () () + linkNodes (Ref rn5 1) (Ref rn8 1) + linkNodes (Ref rn5 2) (Ref rn9 1) + linkNodes (Ref rn5 3) (Ref rn7 1) + linkNodes (Ref rn6 1) (Ref rn8 2) + linkNodes (Ref rn6 2) (Ref rn9 2) + linkNodes (Ref rn6 3) (Ref rn7 2) + linkNodes r0 $ Ref rn8 0 + linkNodes r1 $ Ref rn9 0 + linkNodes r2 $ Ref rn7 0 + linkNodes r3 $ Ref rn5 0 + linkNodes r4 $ Ref rn6 0 +reduceNode n0@PArgumentNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (AccumIONode ib _ r0) (TEntryNode _ r1 r2) = do + rn3 <- newNode $ AccumIONode ib () () + linkNodes r0 $ Ref rn3 1 + propagate1 r1 TCloseNode + linkNodes r2 $ Ref rn3 0 +reduceNode n0@TEntryNode {} n1@AccumIONode {} = reduceNode n1 n0 +reduceNode (TBuild1Node lvl _ namep _ r0 r1) (TEntryNode _ r2 r3) = do + rn4 <- newNode $ TCross1Node lvl namep () () + linkNodes r0 $ Ref rn4 1 + linkNodes r1 r3 + linkNodes r2 $ Ref rn4 0 +reduceNode n0@TEntryNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node lvl _ namep _ r0 r1 r2) (TEntryNode _ r3 r4) = do + rn5 <- newNode $ TCross2Node lvl namep () () () + linkNodes r0 $ Ref rn5 1 + linkNodes r1 $ Ref rn5 2 + linkNodes r2 r4 + linkNodes r3 $ Ref rn5 0 +reduceNode n0@TEntryNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TSplitNode _ r0 r1) (TCross1Node lvl namep _ r2) + = commute1 TSplitNode (TCross1Node lvl namep) r0 r1 r2 +reduceNode n0@TCross1Node {} n1@TSplitNode {} = reduceNode n1 n0 +reduceNode (TCross2Node lvl namep _ r0 r1) (TSplitNode _ r2 r3) + = commute2 (TCross2Node lvl namep) TSplitNode r0 r1 r2 r3 +reduceNode n0@TSplitNode {} n1@TCross2Node {} = reduceNode n1 n0 +reduceNode (TCross1Node _ _ _ r0) (TCloseNode _) = propagate1 r0 TCloseNode +reduceNode n0@TCloseNode {} n1@TCross1Node {} = reduceNode n1 n0 +reduceNode (TCross2Node _ _ _ r0 r1) (TCloseNode _) + = propagate2 r0 r1 TCloseNode +reduceNode n0@TCloseNode {} n1@TCross2Node {} = reduceNode n1 n0 +reduceNode (TSplitNode _ r0 r1) (TCloseNode _) = propagate2 r0 r1 TCloseNode +reduceNode n0@TCloseNode {} n1@TSplitNode {} = reduceNode n1 n0 +reduceNode (TCloseNode _) (TCloseNode _) = pure () +reduceNode (TCross1Node lvl namep _ r0) (TLeaveNode t _ r1 r2) = do + rn3 <- newNode $ TBuild1Node lvl t namep () () () + linkNodes r0 $ Ref rn3 1 + linkNodes r1 $ Ref rn3 0 + linkNodes r2 $ Ref rn3 2 +reduceNode n0@TLeaveNode {} n1@TCross1Node {} = reduceNode n1 n0 +reduceNode (TCross2Node lvl namep _ r0 r1) (TLeaveNode t _ r2 r3) = do + rn4 <- newNode $ TBuild2Node lvl t namep () () () () + linkNodes r0 $ Ref rn4 1 + linkNodes r1 $ Ref rn4 2 + linkNodes r2 $ Ref rn4 0 + linkNodes r3 $ Ref rn4 3 +reduceNode n0@TLeaveNode {} n1@TCross2Node {} = reduceNode n1 n0 +reduceNode (TLeaveNode _ _ r0 r1) (TCloseNode _) = linkNodes r0 r1 +reduceNode n0@TCloseNode {} n1@TLeaveNode {} = reduceNode n1 n0 +reduceNode (TCross1Node lvl0 namep _ r0) (TMatchNode lvl1 _ r1 r2 r3) + | lvl0 == lvl1 = do + rn4 <- newNode $ TSplitNode () () () + linkNodes r0 $ Ref rn4 0 + linkNodes r1 $ Ref rn4 1 + linkNodes r2 $ Ref rn4 2 + propagate1 r3 $ OperandNode namep + | otherwise = do + rn4 <- newNode $ TCross1Node lvl0 namep () () + rn5 <- newNode $ TCross1Node lvl0 namep () () + rn6 <- newNode $ TMatchNode lvl1 () () () () + linkNodes (Ref rn4 1) (Ref rn6 1) + linkNodes (Ref rn5 1) (Ref rn6 2) + linkNodes r0 $ Ref rn6 0 + linkNodes r1 $ Ref rn4 0 + linkNodes r2 $ Ref rn5 0 + linkNodes r3 $ Ref rn6 3 +reduceNode n0@TMatchNode {} n1@TCross1Node {} = reduceNode n1 n0 +reduceNode (TCross2Node lvl0 namep _ r0 r1) (TMatchNode lvl1 _ r2 r3 r4) + | lvl0 == lvl1 = do + linkNodes r0 r2 + linkNodes r1 r3 + propagate1 r4 $ OperandNode namep + | otherwise = do + let opp = B.Partial (SSucc $ SSucc SZero) $ mkSelect namep + rn5 <- newNode $ TCross2Node lvl0 namep () () () + rn6 <- newNode $ TCross2Node lvl0 namep () () () + rn7 <- newNode $ TMatchNode lvl1 () () () () + rn8 <- newNode $ TMatchNode lvl1 () () () () + rn9 <- newNode $ OperandPNode opp () () + rn10 <- newNode $ AppNode () () () + linkNodes (Ref rn5 1) (Ref rn7 1) + linkNodes (Ref rn5 2) (Ref rn8 1) + linkNodes (Ref rn6 1) (Ref rn7 2) + linkNodes (Ref rn6 2) (Ref rn8 2) + linkNodes (Ref rn7 3) (Ref rn9 0) + linkNodes (Ref rn8 3) (Ref rn10 1) + linkNodes (Ref rn9 1) (Ref rn10 0) + linkNodes r0 $ Ref rn7 0 + linkNodes r1 $ Ref rn8 0 + linkNodes r2 $ Ref rn5 0 + linkNodes r3 $ Ref rn6 0 + linkNodes r4 $ Ref rn10 2 +reduceNode n0@TMatchNode {} n1@TCross2Node {} = reduceNode n1 n0 +reduceNode (TCloseNode _) (TMatchNode _ _ r0 r1 r2) + = propagate2 r0 r1 TCloseNode *> propagate1 r2 (OperandNode opUndef) + where + opUndef = B.Reference (B.IntType 1) $ B.Name $ -1 +reduceNode n0@TMatchNode {} n1@TCloseNode {} = reduceNode n1 n0 +reduceNode (PArgumentNode t _ r0 r1) (AppNode _ r2 r3) = do + rn4 <- newNode $ PArgumentNode t () () () + rn5 <- newNode $ PArgumentNode t () () () + linkNodes (Ref rn4 0) (Ref rn5 1) + linkNodes r0 $ Ref rn4 1 + linkNodes r1 $ Ref rn4 2 + linkNodes r2 $ Ref rn5 2 + linkNodes r3 $ Ref rn5 0 +reduceNode n0@AppNode {} n1@PArgumentNode {} = reduceNode n1 n0 +reduceNode (PArgumentNode _ _ r0 r1) (OperandPNode opp _ r2) = do + rn3 <- newNode $ AppNode () () () + rn4 <- newNode $ PReduceNode () () + rn5 <- newNode $ PReduceNode () () + rn6 <- newNode $ OperandPNode opp () () + linkNodes (Ref rn3 0) (Ref rn4 1) + linkNodes (Ref rn3 1) (Ref rn5 1) + linkNodes (Ref rn3 2) (Ref rn6 0) + linkNodes r0 $ Ref rn4 0 + linkNodes r1 $ Ref rn5 0 + linkNodes r2 $ Ref rn6 1 +reduceNode n0@OperandPNode {} n1@PArgumentNode {} = reduceNode n1 n0 +reduceNode (PArgumentNode _ _ r0 r1) (IOPNode iop _ r2) = do + rn3 <- newNode $ AppNode () () () + rn4 <- newNode $ PReduceNode () () + rn5 <- newNode $ PReduceNode () () + rn6 <- newNode $ IOPNode iop () () + linkNodes (Ref rn3 0) (Ref rn4 1) + linkNodes (Ref rn3 1) (Ref rn5 1) + linkNodes (Ref rn3 2) (Ref rn6 0) + linkNodes r0 $ Ref rn4 0 + linkNodes r1 $ Ref rn5 0 + linkNodes r2 $ Ref rn6 1 +reduceNode n0@IOPNode {} n1@PArgumentNode {} = reduceNode n1 n0 +reduceNode (PArgumentNode _ _ r0 r1) (PReduceNode _ r2) = do + rn3 <- newNode $ AppNode () () () + rn4 <- newNode $ PReduceNode () () + rn5 <- newNode $ PReduceNode () () + linkNodes (Ref rn3 0) (Ref rn4 1) + linkNodes (Ref rn3 1) (Ref rn5 1) + linkNodes r0 $ Ref rn4 0 + linkNodes r1 $ Ref rn5 0 + linkNodes r2 $ Ref rn3 2 +reduceNode n0@PReduceNode {} n1@PArgumentNode {} = reduceNode n1 n0 +reduceNode (PReduceNode _ r0) (OperandNode op _) + = propagate1 r0 $ OperandNode op +reduceNode n0@OperandNode {} n1@PReduceNode {} = reduceNode n1 n0 +reduceNode (PReduceNode _ r0) (OperandANode opp _) + = mkLambda r0 $ OperandPNode opp +reduceNode n0@OperandANode {} n1@PReduceNode {} = reduceNode n1 n0 +reduceNode (PReduceNode _ r0) (IOANode _ iop _) = mkLambda r0 $ IOPNode iop +reduceNode n0@IOANode {} n1@PReduceNode {} = reduceNode n1 n0 +reduceNode (PReduceNode _ r0) (IOContNode instr _) + = propagate1 r0 $ IOContNode instr +reduceNode n0@IOContNode {} n1@PReduceNode {} = reduceNode n1 n0 +-- FFI Duplication +reduceNode (DupNode _ _ r0 r1) (OperandNode op _) + = propagate2 r0 r1 $ OperandNode op +reduceNode n0@OperandNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode _ _ r0 r1) (OperandANode opp _) + = propagate2 r0 r1 $ OperandANode opp +reduceNode n0@OperandANode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (OperandPNode opp _ r2) + = commute1 (DupNode lvl) (OperandPNode opp) r0 r1 r2 +reduceNode n0@OperandPNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (IONode bs _) = do + rn2 <- newNode $ IONode bs () + dedupIO lvl r0 r1 $ Ref rn2 0 +reduceNode n0@IONode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode _ _ r0 r1) (IOANode t iop _) + = propagate2 r0 r1 $ IOANode t iop +reduceNode n0@IOANode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (IOPNode iop _ r2) + = commute1 (DupNode lvl) (IOPNode iop) r0 r1 r2 +reduceNode n0@IOPNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (IOPureNode _ r2) + = commute1 (DupNode lvl) IOPureNode r0 r1 r2 +reduceNode n0@IOPureNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode _ _ r0 r1) (IOContNode instr _) + = propagate2 r0 r1 $ IOContNode instr +reduceNode n0@IOContNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (ReturnCNode _ r2) = do + rn3 <- newNode $ ReturnCNode () () + linkNodes r2 $ Ref rn3 1 + dedupIO lvl r0 r1 $ Ref rn3 0 +reduceNode n0@ReturnCNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupIONode lvl _ r0 r1) (ReturnCNode _ r2) = do + rn3 <- newNode $ ReturnCNode () () + linkNodes r2 $ Ref rn3 1 + dedupIO' lvl r0 r1 $ Ref rn3 0 +reduceNode n0@ReturnCNode {} n1@DupIONode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (Bind0BNode _ r2) + = commute1 (DupNode lvl) Bind0BNode r0 r1 r2 +reduceNode n0@Bind0BNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (Bind0CNode _ r2 r3) + = commute2 (DupNode lvl) Bind0CNode r0 r1 r2 r3 +reduceNode n0@Bind0CNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (Bind1CNode name _ r2 r3) = do + rn4 <- newNode $ Bind1CNode name () () () + linkNodes r2 $ Ref rn4 1 + linkNodes r3 $ Ref rn4 2 + dedupIO lvl r0 r1 $ Ref rn4 0 +reduceNode n0@Bind1CNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupIONode lvl _ r0 r1) (Bind1CNode name _ r2 r3) = do + rn4 <- newNode $ Bind1CNode name () () () + linkNodes r2 $ Ref rn4 1 + linkNodes r3 $ Ref rn4 2 + dedupIO' lvl r0 r1 $ Ref rn4 0 +reduceNode n0@Bind1CNode {} n1@DupIONode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (Branch0CNode _ r2 r3 r4) = do + rn5 <- newNode $ Branch0CNode () () () () + linkNodes r2 $ Ref rn5 1 + linkNodes r3 $ Ref rn5 2 + linkNodes r4 $ Ref rn5 3 + dedupIO lvl r0 r1 $ Ref rn5 0 +reduceNode n0@Branch0CNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl0 _ r0 r1) (TBuild1Node lvl1 t opp _ r2 r3) + | lvl0 == lvl1 = do + rn4 <- newNode $ TSplitNode () () () + rn5 <- newNode $ TLeaveNode t () () () + rn6 <- newNode $ TLeaveNode t () () () + linkNodes (Ref rn4 1) (Ref rn5 0) + linkNodes (Ref rn4 2) (Ref rn6 0) + linkNodes r0 $ Ref rn5 1 + linkNodes r1 $ Ref rn6 1 + linkNodes r2 $ Ref rn4 0 + case t of + BuildOperand -> do + let opp' = B.Partial (SSucc $ SSucc SZero) $ mkSelect opp + rn7 <- newNode $ OperandPNode opp' () () + rn8 <- newNode $ AppNode () () () + linkNodes (Ref rn5 2) (Ref rn7 0) + linkNodes (Ref rn6 2) (Ref rn8 1) + linkNodes (Ref rn7 1) (Ref rn8 0) + linkNodes r3 $ Ref rn8 2 + BuildIO -> mkBranch1 opp (Ref rn5 2) (Ref rn6 2) r3 + | otherwise = do + rn4 <- newNode $ TMatchNode lvl0 () () () () + rn5 <- newNode $ TBuild1Node lvl1 t opp () () () + rn6 <- newNode $ TBuild1Node lvl1 t opp () () () + linkNodes (Ref rn4 1) (Ref rn5 1) + linkNodes (Ref rn4 2) (Ref rn6 1) + linkNodes r0 $ Ref rn5 0 + linkNodes r1 $ Ref rn6 0 + linkNodes r2 $ Ref rn4 0 + case t of + BuildOperand -> do + let opp' = B.Partial (SSucc $ SSucc $ SSucc SZero) mkSelect + rn7 <- newNode $ OperandPNode opp' () () + rn8 <- newNode $ AppNode () () () + rn9 <- newNode $ AppNode () () () + linkNodes (Ref rn7 0) (Ref rn4 3) + linkNodes (Ref rn7 1) (Ref rn8 0) + linkNodes (Ref rn8 1) (Ref rn5 2) + linkNodes (Ref rn8 2) (Ref rn9 0) + linkNodes (Ref rn9 1) (Ref rn6 2) + linkNodes r3 $ Ref rn9 2 + BuildIO -> do + rn7 <- newNode $ Branch0CNode () () () () + linkNodes (Ref rn4 3) (Ref rn7 1) + linkNodes (Ref rn5 2) (Ref rn7 2) + linkNodes (Ref rn6 2) (Ref rn7 3) + linkNodes r3 $ Ref rn7 0 +reduceNode n0@TBuild1Node {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl0 _ r0 r1) (TBuild2Node lvl1 t opp _ r2 r3 r4) + | lvl0 == lvl1 = do + rn5 <- newNode $ TLeaveNode t () () () + rn6 <- newNode $ TLeaveNode t () () () + linkNodes r0 $ Ref rn5 1 + linkNodes r1 $ Ref rn6 1 + linkNodes r2 $ Ref rn5 0 + linkNodes r3 $ Ref rn6 0 + case t of + BuildOperand -> do + let opp' = B.Partial (SSucc $ SSucc SZero) $ mkSelect opp + rn7 <- newNode $ OperandPNode opp' () () + rn8 <- newNode $ AppNode () () () + linkNodes (Ref rn5 2) (Ref rn7 0) + linkNodes (Ref rn6 2) (Ref rn8 1) + linkNodes (Ref rn7 1) (Ref rn8 0) + linkNodes r4 $ Ref rn8 2 + BuildIO -> mkBranch1 opp (Ref rn5 2) (Ref rn6 2) r4 + | otherwise = do + let opp' = B.Partial (SSucc $ SSucc SZero) $ mkSelect opp + rn3 <- newNode $ OperandPNode opp' () () + rn4 <- newNode $ AppNode () () () + rn5 <- newNode $ TMatchNode lvl0 () () () () + rn6 <- newNode $ TMatchNode lvl0 () () () () + rn7 <- newNode $ TBuild2Node lvl1 t opp () () () () + rn8 <- newNode $ TBuild2Node lvl1 t opp () () () () + linkNodes (Ref rn3 0) (Ref rn5 3) + linkNodes (Ref rn3 1) (Ref rn4 0) + linkNodes (Ref rn4 1) (Ref rn6 3) + linkNodes (Ref rn5 1) (Ref rn7 1) + linkNodes (Ref rn5 2) (Ref rn8 1) + linkNodes (Ref rn6 1) (Ref rn7 2) + linkNodes (Ref rn6 2) (Ref rn8 2) + linkNodes r0 $ Ref rn7 0 + linkNodes r1 $ Ref rn8 0 + linkNodes r2 $ Ref rn5 0 + linkNodes r3 $ Ref rn6 0 + case t of + BuildOperand -> do + let opp'' = B.Partial (SSucc $ SSucc $ SSucc SZero) mkSelect + rn2 <- newNode $ OperandPNode opp'' () () + rn9 <- newNode $ AppNode () () () + rn10 <- newNode $ AppNode () () () + linkNodes (Ref rn2 0) (Ref rn4 2) + linkNodes (Ref rn2 1) (Ref rn9 0) + linkNodes (Ref rn7 3) (Ref rn9 1) + linkNodes (Ref rn8 3) (Ref rn10 1) + linkNodes (Ref rn9 2) (Ref rn10 0) + linkNodes r4 $ Ref rn10 2 + BuildIO -> do + rn2 <- newNode $ Branch0CNode () () () () + linkNodes (Ref rn2 1) (Ref rn4 2) + linkNodes (Ref rn2 2) (Ref rn7 3) + linkNodes (Ref rn2 3) (Ref rn8 3) + linkNodes r4 $ Ref rn2 0 +reduceNode n0@TBuild2Node {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (TEntryNode _ r2 r3) = do + rn4 <- newNode $ TEntryNode () () () + linkNodes r2 $ Ref rn4 1 + linkNodes r3 $ Ref rn4 2 + dedupIO lvl r0 r1 $ Ref rn4 0 +reduceNode n0@TEntryNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupIONode lvl _ r0 r1) (TEntryNode _ r2 r3) = do + rn4 <- newNode $ TEntryNode () () () + linkNodes r2 $ Ref rn4 1 + linkNodes r3 $ Ref rn4 2 + dedupIO' lvl r0 r1 $ Ref rn4 0 +reduceNode n0@TEntryNode {} n1@DupIONode {} = reduceNode n1 n0 +reduceNode (DupNode lvl _ r0 r1) (PArgumentNode t _ r2 r3) + = commute2 (DupNode lvl) (PArgumentNode t) r0 r1 r2 r3 +reduceNode n0@PArgumentNode {} n1@DupNode {} = reduceNode n1 n0 +reduceNode (DupNode lvl0 _ r0 r1) (DupIONode lvl1 _ r2 r3) + | lvl0 == lvl1 = do + rn4 <- newNode $ DupNode lvl0 () () () + linkNodes r0 $ Ref rn4 1 + linkNodes r1 $ Ref rn4 2 + dedupIO' lvl1 r2 r3 $ Ref rn4 0 + | otherwise = commute2 (DupNode lvl0) (DupIONode lvl1) r0 r1 r2 r3 +reduceNode n0@DupIONode {} n1@DupNode {} = reduceNode n1 n0 +-- FFI Dead +reduceNode (AccumIONode ib _ r0) (DeadNode _) = propagate1 r0 + $ IONode $ B.BlockList (B.Block (B.unIBlock ib) B.Unreachable) mempty +reduceNode n0@DeadNode {} n1@AccumIONode {} = reduceNode n1 n0 +reduceNode (OperandNode _ _) (DeadNode _) = pure () +reduceNode n0@DeadNode {} n1@OperandNode {} = reduceNode n1 n0 +reduceNode (OperandANode _ _) (DeadNode _) = pure () +reduceNode n0@DeadNode {} n1@OperandANode {} = reduceNode n1 n0 +reduceNode (OperandPNode _ _ r0) (DeadNode _) = propagate1 r0 DeadNode +reduceNode n0@DeadNode {} n1@OperandPNode {} = reduceNode n1 n0 +reduceNode (IONode _ _) (DeadNode _) = pure () +reduceNode n0@DeadNode {} n1@IONode {} = reduceNode n1 n0 +reduceNode (IOANode _ _ _) (DeadNode _) = pure () +reduceNode n0@DeadNode {} n1@IOANode {} = reduceNode n1 n0 +reduceNode (IOPNode _ _ r0) (DeadNode _) = propagate1 r0 DeadNode +reduceNode n0@DeadNode {} n1@IOPNode {} = reduceNode n1 n0 +reduceNode (IOPureNode _ r0) (DeadNode _) = propagate1 r0 DeadNode +reduceNode n0@DeadNode {} n1@IOPureNode {} = reduceNode n1 n0 +reduceNode (IOContNode _ _) (DeadNode _) = pure () +reduceNode n0@DeadNode {} n1@IOContNode {} = reduceNode n1 n0 +reduceNode (TailCallNode _ _ r0) (DeadNode _) = propagate1 r0 DeadNode +reduceNode n0@DeadNode {} n1@TailCallNode {} = reduceNode n1 n0 +reduceNode (Bind0BNode _ r0) (DeadNode _) = propagate1 r0 DeadNode +reduceNode n0@DeadNode {} n1@Bind0BNode {} = reduceNode n1 n0 +reduceNode (Bind0CNode _ r0 r1) (DeadNode _) = propagate2 r0 r1 DeadNode +reduceNode n0@DeadNode {} n1@Bind0CNode {} = reduceNode n1 n0 +reduceNode (Bind0FNode _ _ r0 r1) (DeadNode _) = propagate2 r0 r1 DeadNode +reduceNode n0@DeadNode {} n1@Bind0FNode {} = reduceNode n1 n0 +reduceNode (Bind1CNode _ _ r0 r1) (DeadNode _) = propagate2 r0 r1 DeadNode +reduceNode n0@DeadNode {} n1@Bind1CNode {} = reduceNode n1 n0 +reduceNode (Bind1FNode _ _ r0) (DeadNode _) = propagate1 r0 DeadNode +reduceNode n0@DeadNode {} n1@Bind1FNode {} = reduceNode n1 n0 +reduceNode (LabelNode lbl _ r0) (DeadNode _) + = propagate1 r0 $ NamedBlockNode $ B.NamedBlockList + $ IM.singleton (B.unLabel lbl) $ B.Block mempty B.Unreachable +reduceNode n0@DeadNode {} n1@LabelNode {} = reduceNode n1 n0 +reduceNode (NamedBlockNode _ _) (DeadNode _) = pure () +reduceNode n0@DeadNode {} n1@NamedBlockNode {} = reduceNode n1 n0 +reduceNode (TBuild1Node _ _ _ _ r0 r1) (DeadNode _) + = propagate1 r0 TCloseNode *> propagate1 r1 DeadNode +reduceNode n0@DeadNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node _ _ _ _ r0 r1 r2) (DeadNode _) + = propagate2 r0 r1 TCloseNode *> propagate1 r2 DeadNode +reduceNode n0@DeadNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TEntryNode _ r0 r1) (DeadNode _) + = propagate1 r0 TCloseNode *> propagate1 r1 DeadNode +reduceNode n0@DeadNode {} n1@TEntryNode {} = reduceNode n1 n0 +reduceNode (PArgumentNode _ _ r0 r1) (DeadNode _) = propagate2 r0 r1 DeadNode +reduceNode n0@DeadNode {} n1@PArgumentNode {} = reduceNode n1 n0 +reduceNode (PReduceNode _ r0) (DeadNode _) = propagate1 r0 DeadNode +reduceNode n0@DeadNode {} n1@PReduceNode {} = reduceNode n1 n0 +reduceNode (DupIONode _ _ r0 r1) (DeadNode _) = propagate2 r0 r1 DeadNode +reduceNode n0@DeadNode {} n1@DupIONode {} = reduceNode n1 n0 +-- FFI Book-keeping +reduceNode (AccumIONode ib _ r0) (BoxNode _ _ r1) = do + rn2 <- newNode $ AccumIONode ib () () + linkNodes r0 $ Ref rn2 1 + linkNodes r1 $ Ref rn2 0 +reduceNode n0@BoxNode {} n1@AccumIONode {} = reduceNode n1 n0 +reduceNode (OperandNode op _) (BoxNode _ _ r0) = propagate1 r0 $ OperandNode op +reduceNode n0@BoxNode {} n1@OperandNode {} = reduceNode n1 n0 +reduceNode (OperandANode opp _) (BoxNode _ _ r0) + = propagate1 r0 $ OperandANode opp +reduceNode n0@BoxNode {} n1@OperandANode {} = reduceNode n1 n0 +reduceNode (OperandPNode opp _ r0) (BoxNode lvl _ r1) + = commute0 (OperandPNode opp) (BoxNode lvl) r0 r1 +reduceNode n0@BoxNode {} n1@OperandPNode {} = reduceNode n1 n0 +reduceNode (IONode b _) (BoxNode _ _ r0) = propagate1 r0 $ IONode b +reduceNode n0@BoxNode {} n1@IONode {} = reduceNode n1 n0 +reduceNode (IOANode t iop _) (BoxNode _ _ r0) = propagate1 r0 $ IOANode t iop +reduceNode n0@BoxNode {} n1@IOANode {} = reduceNode n1 n0 +reduceNode (IOPNode iop _ r0) (BoxNode lvl _ r1) + = commute0 (IOPNode iop) (BoxNode lvl) r0 r1 +reduceNode n0@BoxNode {} n1@IOPNode {} = reduceNode n1 n0 +reduceNode (IOPureNode _ r0) (BoxNode lvl _ r1) + = commute0 IOPureNode (BoxNode lvl) r0 r1 +reduceNode n0@BoxNode {} n1@IOPureNode {} = reduceNode n1 n0 +reduceNode (IOContNode instr _) (BoxNode _ _ r0) + = propagate1 r0 $ IOContNode instr +reduceNode n0@BoxNode {} n1@IOContNode {} = reduceNode n1 n0 +reduceNode (ReturnCNode _ r0) (BoxNode lvl _ r1) + = commute0 ReturnCNode (BoxNode lvl) r0 r1 +reduceNode n0@BoxNode {} n1@ReturnCNode {} = reduceNode n1 n0 +reduceNode (ReturnFNode _ r0) (BoxNode lvl _ r1) + = commute0 ReturnFNode (BoxNode lvl) r0 r1 +reduceNode n0@BoxNode {} n1@ReturnFNode {} = reduceNode n1 n0 +reduceNode (TailCallNode name _ r0) (BoxNode lvl _ r1) + = commute0 (TailCallNode name) (BoxNode lvl) r0 r1 +reduceNode n0@BoxNode {} n1@TailCallNode {} = reduceNode n1 n0 +reduceNode (Bind0BNode _ r0) (BoxNode lvl _ r1) + = commute0 Bind0BNode (BoxNode lvl) r0 r1 +reduceNode n0@BoxNode {} n1@Bind0BNode {} = reduceNode n1 n0 +reduceNode (Bind0CNode _ r0 r1) (BoxNode lvl _ r2) + = commute1 Bind0CNode (BoxNode lvl) r0 r1 r2 +reduceNode n0@BoxNode {} n1@Bind0CNode {} = reduceNode n1 n0 +reduceNode (Bind0FNode name _ r0 r1) (BoxNode lvl _ r2) + = commute1 (Bind0FNode name) (BoxNode lvl) r0 r1 r2 +reduceNode n0@BoxNode {} n1@Bind0FNode {} = reduceNode n1 n0 +reduceNode (Bind1CNode name _ r0 r1) (BoxNode lvl _ r2) + = commute1 (Bind1CNode name) (BoxNode lvl) r0 r1 r2 +reduceNode n0@BoxNode {} n1@Bind1CNode {} = reduceNode n1 n0 +reduceNode (Bind1FNode nbs _ r0) (BoxNode lvl _ r1) + = commute0 (Bind1FNode nbs) (BoxNode lvl) r0 r1 +reduceNode n0@BoxNode {} n1@Bind1FNode {} = reduceNode n1 n0 +reduceNode (Branch0CNode _ r0 r1 r2) (BoxNode lvl _ r3) + = commute2b Branch0CNode (BoxNode lvl) r0 r1 r2 r3 +reduceNode n0@BoxNode {} n1@Branch0CNode {} = reduceNode n1 n0 +reduceNode (Branch0FNode _ r0 r1 r2) (BoxNode lvl _ r3) + = commute2b Branch0FNode (BoxNode lvl) r0 r1 r2 r3 +reduceNode n0@BoxNode {} n1@Branch0FNode {} = reduceNode n1 n0 +reduceNode (LabelNode lbl _ r0) (BoxNode _ _ r1) + = do + rn2 <- newNode $ LabelNode lbl () () + linkNodes r0 $ Ref rn2 1 + linkNodes r1 $ Ref rn2 0 +reduceNode n0@BoxNode {} n1@LabelNode {} = reduceNode n1 n0 +reduceNode (TBuild1Node lvl0 t namep _ r0 r1) (BoxNode lvl1 _ r2) = do + let lvl0' = if lvl0 < lvl1 then lvl0 else succ lvl0 + rn3 <- newNode $ TBuild1Node lvl0' t namep () () () + rn4 <- newNode $ BoxNode lvl1 () () + linkNodes (Ref rn3 1) (Ref rn4 1) + linkNodes r0 $ Ref rn4 0 + linkNodes r1 $ Ref rn3 2 + linkNodes r2 $ Ref rn3 0 +reduceNode n0@BoxNode {} n1@TBuild1Node {} = reduceNode n1 n0 +reduceNode (TBuild2Node lvl0 t namep _ r0 r1 r2) (BoxNode lvl1 _ r3) = do + let lvl0' = if lvl0 < lvl1 then lvl0 else succ lvl0 + rn4 <- newNode $ TBuild2Node lvl0' t namep () () () () + rn5 <- newNode $ BoxNode lvl1 () () + rn6 <- newNode $ BoxNode lvl1 () () + linkNodes (Ref rn4 1) (Ref rn5 1) + linkNodes (Ref rn4 2) (Ref rn6 1) + linkNodes r0 $ Ref rn5 0 + linkNodes r1 $ Ref rn6 0 + linkNodes r2 $ Ref rn4 3 + linkNodes r3 $ Ref rn4 0 +reduceNode n0@BoxNode {} n1@TBuild2Node {} = reduceNode n1 n0 +reduceNode (TCross1Node lvl0 namep _ r0) (BoxNode lvl1 _ r1) = commute0 + (TCross1Node (if lvl0 < lvl1 then lvl0 else succ lvl0) namep) + (BoxNode lvl1) + r0 r1 +reduceNode n0@BoxNode {} n1@TCross1Node {} = reduceNode n1 n0 +reduceNode (TCross2Node lvl0 namep _ r0 r1) (BoxNode lvl1 _ r2) = commute1 + (TCross2Node (if lvl0 < lvl1 then lvl0 else succ lvl0) namep) + (BoxNode lvl1) + r0 r1 r2 +reduceNode n0@BoxNode {} n1@TCross2Node {} = reduceNode n1 n0 +reduceNode (TEntryNode _ r0 r1) (BoxNode lvl _ r2) + = commute1 TEntryNode (BoxNode lvl) r0 r1 r2 +reduceNode n0@BoxNode {} n1@TEntryNode {} = reduceNode n1 n0 +reduceNode (TSplitNode _ r0 r1) (BoxNode lvl _ r2) + = commute1 TSplitNode (BoxNode lvl) r0 r1 r2 +reduceNode n0@BoxNode {} n1@TSplitNode {} = reduceNode n1 n0 +reduceNode (TCloseNode _) (BoxNode _ _ r0) = propagate1 r0 TCloseNode +reduceNode n0@BoxNode {} n1@TCloseNode {} = reduceNode n1 n0 +reduceNode (TLeaveNode t _ r0 r1) (BoxNode lvl _ r2) = do + rn3 <- newNode $ TLeaveNode t () () () + rn4 <- newNode $ BoxNode lvl () () + linkNodes (Ref rn3 1) (Ref rn4 1) + linkNodes r0 $ Ref rn4 0 + linkNodes r1 $ Ref rn3 2 + linkNodes r2 $ Ref rn3 0 +reduceNode n0@BoxNode {} n1@TLeaveNode {} = reduceNode n1 n0 +reduceNode (TMatchNode lvl0 _ r0 r1 r2) (BoxNode lvl1 _ r3) = commute2b + (TMatchNode $ if lvl0 < lvl1 then lvl0 else succ lvl0) + (BoxNode lvl1) + r0 r1 r2 r3 +reduceNode n0@BoxNode {} n1@TMatchNode {} = reduceNode n1 n0 +reduceNode (PArgumentNode t _ r0 r1) (BoxNode lvl _ r2) + = commute1 (PArgumentNode t) (BoxNode lvl) r0 r1 r2 +reduceNode n0@BoxNode {} n1@PArgumentNode {} = reduceNode n1 n0 +reduceNode (PReduceNode _ r0) (BoxNode _ _ r1) = do + rn2 <- newNode $ PReduceNode () () + linkNodes r0 $ Ref rn2 1 + linkNodes r1 $ Ref rn2 0 +reduceNode n0@BoxNode {} n1@PReduceNode {} = reduceNode n1 n0 +reduceNode (DupIONode lvl0 _ r0 r1) (BoxNode lvl1 _ r2) = commute1 + (DupIONode $ if lvl0 < lvl1 then lvl0 else succ lvl0) + (BoxNode lvl1) + r0 r1 r2 +reduceNode n0@BoxNode {} n1@DupIONode {} = reduceNode n1 n0 +reduceNode n0 n1 = error . show + $ "unexpected node pairing" <> line <> pretty n0 <> line <> pretty n1 +{-# INLINABLE reduceNode #-} + +commute0 + :: HasRewriter sig m + => (() -> () -> INetF ()) -> (() -> () -> INetF ()) + -> Ref -> Ref -> m () +commute0 mk1 mk2 r0 r1 = do + rn3 <- newNode $ mk2 () () + rn4 <- newNode $ mk1 () () + linkNodes (Ref rn3 1) (Ref rn4 1) + linkNodes r0 $ Ref rn3 0 + linkNodes r1 $ Ref rn4 0 +{-# INLINABLE commute0 #-} + +commute1 + :: HasRewriter sig m + => (() -> () -> () -> INetF ()) -> (() -> () -> INetF ()) + -> Ref -> Ref -> Ref -> m () +commute1 mk1 mk2 = commute1' mk1 mk2 mk2 +{-# INLINABLE commute1 #-} + +commute1' + :: HasRewriter sig m + => (() -> () -> () -> INetF ()) + -> (() -> () -> INetF ()) -> (() -> () -> INetF ()) + -> Ref -> Ref -> Ref -> m () +commute1' mk1 mk2a mk2b r0 r1 r2 = do + rn3 <- newNode $ mk2a () () + rn4 <- newNode $ mk2b () () + rn5 <- newNode $ mk1 () () () + linkNodes (Ref rn3 1) (Ref rn5 1) + linkNodes (Ref rn4 1) (Ref rn5 2) + linkNodes r0 $ Ref rn3 0 + linkNodes r1 $ Ref rn4 0 + linkNodes r2 $ Ref rn5 0 +{-# INLINABLE commute1' #-} + +commute2 + :: HasRewriter sig m + => (() -> () -> () -> INetF ()) + -> (() -> () -> () -> INetF ()) + -> Ref -> Ref -> Ref -> Ref -> m () +commute2 mk1 mk2 = commute2' mk1 mk1 mk2 mk2 +{-# INLINABLE commute2 #-} + +commute2' + :: HasRewriter sig m + => (() -> () -> () -> INetF ()) + -> (() -> () -> () -> INetF ()) + -> (() -> () -> () -> INetF ()) + -> (() -> () -> () -> INetF ()) + -> Ref -> Ref -> Ref -> Ref -> m () +commute2' mk1a mk1b mk2a mk2b r0 r1 r2 r3 = do + rn4 <- newNode $ mk1a () () () + rn5 <- newNode $ mk1b () () () + rn6 <- newNode $ mk2a () () () + rn7 <- newNode $ mk2b () () () + linkNodes (Ref rn4 1) (Ref rn6 1) + linkNodes (Ref rn4 2) (Ref rn7 1) + linkNodes (Ref rn5 1) (Ref rn6 2) + linkNodes (Ref rn5 2) (Ref rn7 2) + linkNodes r0 $ Ref rn6 0 + linkNodes r1 $ Ref rn7 0 + linkNodes r2 $ Ref rn4 0 + linkNodes r3 $ Ref rn5 0 +{-# INLINABLE commute2' #-} + +commute2b + :: HasRewriter sig m + => (() -> () -> () -> () -> INetF ()) + -> (() -> () -> INetF ()) + -> Ref -> Ref -> Ref -> Ref -> m () +commute2b mk1 mk2 r0 r1 r2 r3 = do + rn4 <- newNode $ mk1 () () () () + rn5 <- newNode $ mk2 () () + rn6 <- newNode $ mk2 () () + rn7 <- newNode $ mk2 () () + linkNodes (Ref rn4 1) (Ref rn5 1) + linkNodes (Ref rn4 2) (Ref rn6 1) + linkNodes (Ref rn4 3) (Ref rn7 1) + linkNodes r0 $ Ref rn5 0 + linkNodes r1 $ Ref rn6 0 + linkNodes r2 $ Ref rn7 0 + linkNodes r3 $ Ref rn4 0 +{-# INLINABLE commute2b #-} + +propagate1 :: HasRewriter sig m => Ref -> (() -> INetF ()) -> m () +propagate1 r0 mk1 = do + rn1 <- newNode $ mk1 () + linkNodes r0 $ Ref rn1 0 +{-# INLINABLE propagate1 #-} + +propagate2 :: HasRewriter sig m => Ref -> Ref -> (() -> INetF ()) -> m () +propagate2 r0 r1 mk1 = propagate1 r0 mk1 *> propagate1 r1 mk1 +{-# INLINABLE propagate2 #-} + +dedupIO :: HasRewriter sig m => Level -> Ref -> Ref -> Ref -> m () +dedupIO lvl r0 r1 r2 = do + name <- newName + namep <- newName + let opp = B.Reference (B.IntType 1) namep + mk = B.Block mempty . B.TailCall name . B.Constant + rn3 <- newNode $ TEntryNode () () () + rn4 <- newNode $ TEntryNode () () () + rn5 <- newNode $ TBuild2Node lvl BuildIO opp () () () () + rn6 <- newNode $ AccumIONode mempty () () + linkNodes (Ref rn3 1) (Ref rn5 1) + linkNodes (Ref rn4 1) (Ref rn5 2) + linkNodes (Ref rn5 3) (Ref rn6 0) + propagate1 (Ref rn3 2) $ IONode $ B.BlockList (mk B.B1) mempty + propagate1 (Ref rn4 2) $ IONode $ B.BlockList (mk B.B0) mempty + propagate1 (Ref rn6 1) $ PrivateRootNode name namep + linkNodes r0 $ Ref rn3 0 + linkNodes r1 $ Ref rn4 0 + linkNodes r2 $ Ref rn5 0 +{-# INLINABLE dedupIO #-} + +dedupIO' :: HasRewriter sig m => Level -> Ref -> Ref -> Ref -> m () +dedupIO' lvl r0 r1 r2 = do + name <- newName + namep <- newName + let opp = B.Reference (B.IntType 1) namep + rn2 <- newNode $ TEntryNode () () () + rn3 <- newNode $ TBuild1Node lvl BuildIO opp () () () + rn4 <- newNode $ AccumIONode mempty () () + rn5 <- newNode $ TailCallNode name () () + rn6 <- newNode $ PReduceNode () () + linkNodes (Ref rn2 1) (Ref rn3 1) + linkNodes (Ref rn2 2) (Ref rn5 1) + linkNodes (Ref rn3 2) (Ref rn4 0) + linkNodes (Ref rn5 0) (Ref rn6 1) + propagate1 (Ref rn4 1) $ PrivateRootNode name namep + linkNodes r0 $ Ref rn6 0 + linkNodes r1 $ Ref rn2 0 + linkNodes r2 $ Ref rn3 0 +{-# INLINABLE dedupIO' #-} + +reassocPure :: HasRewriter sig m => Ref -> Ref -> m () +reassocPure r0 r1 = do + rn2 <- newNode $ LamNode () () () + rn3 <- newNode $ IOPureNode () () + rn4 <- newNode $ LamNode () () () + rn5 <- newNode $ AppNode () () () + rn6 <- newNode $ LamNode () () () + rn7 <- newNode $ Bind0CNode () () () + rn8 <- newNode $ AppNode () () () + rn9 <- newNode $ BoxNode 0 () () + rn10 <- newNode $ BoxNode 0 () () + rn11 <- newNode $ BoxNode 0 () () + rn12 <- newNode $ BoxNode 0 () () + rn13 <- newNode $ BoxNode 0 () () + linkNodes (Ref rn2 1) (Ref rn12 0) + linkNodes (Ref rn2 2) (Ref rn3 0) + linkNodes (Ref rn3 1) (Ref rn4 0) + linkNodes (Ref rn4 1) (Ref rn9 0) + linkNodes (Ref rn4 2) (Ref rn5 2) + linkNodes (Ref rn5 0) (Ref rn11 1) + linkNodes (Ref rn5 1) (Ref rn6 0) + linkNodes (Ref rn6 1) (Ref rn8 1) + linkNodes (Ref rn6 2) (Ref rn7 2) + linkNodes (Ref rn7 0) (Ref rn8 2) + linkNodes (Ref rn7 1) (Ref rn9 1) + linkNodes (Ref rn8 0) (Ref rn13 1) + linkNodes (Ref rn10 1) (Ref rn11 0) + linkNodes (Ref rn12 1) (Ref rn13 0) + linkNodes r0 $ Ref rn2 0 + linkNodes r1 $ Ref rn10 0 +{-# INLINABLE reassocPure #-} + +-- | @r0 = \a -> IOPure (\b -> Bind1C r1 (\c -> Bind0C (a c) b))@ +reassocCont :: HasRewriter sig m => B.Type -> Ref -> Ref -> m () +reassocCont t r0 r1 = do + name <- newName + rn2 <- newNode $ LamNode () () () + rn3 <- newNode $ IOPureNode () () + rn4 <- newNode $ LamNode () () () + rn5 <- newNode $ Bind1CNode name () () () + rn6 <- newNode $ BoxNode 0 () () + rn7 <- newNode $ BoxNode 0 () () + rn8 <- newNode $ LamNode () () () + rn9 <- newNode $ Bind0CNode () () () + rn10 <- newNode $ AppNode () () () + rn11 <- newNode $ BoxNode 0 () () + rn12 <- newNode $ BoxNode 0 () () + rn13 <- newNode $ BoxNode 0 () () + rn14 <- newNode $ AppNode () () () + linkNodes (Ref rn2 1) (Ref rn11 0) + linkNodes (Ref rn2 2) (Ref rn3 0) + linkNodes (Ref rn3 1) (Ref rn4 0) + linkNodes (Ref rn4 1) (Ref rn13 0) + linkNodes (Ref rn4 2) (Ref rn5 0) + linkNodes (Ref rn5 1) (Ref rn7 1) + linkNodes (Ref rn5 2) (Ref rn14 2) + linkNodes (Ref rn6 1) (Ref rn7 0) + linkNodes (Ref rn8 0) (Ref rn14 0) + linkNodes (Ref rn8 1) (Ref rn10 1) + linkNodes (Ref rn8 2) (Ref rn9 2) + linkNodes (Ref rn9 0) (Ref rn10 2) + linkNodes (Ref rn9 1) (Ref rn13 1) + linkNodes (Ref rn10 0) (Ref rn12 1) + linkNodes (Ref rn11 1) (Ref rn12 0) + propagate1 (Ref rn14 1) $ OperandNode $ B.Reference t name + linkNodes r0 $ Ref rn2 0 + linkNodes r1 $ Ref rn6 0 +{-# INLINABLE reassocCont #-} + +mkBranch1 :: HasRewriter sig m => B.Operand -> Ref -> Ref -> Ref -> m () +mkBranch1 opc r0 r1 r2 = do + lblt <- newLabel + lblf <- newLabel + let b = B.Block mempty $ B.Branch opc lblt lblf + rn3 <- newNode $ AccumNBNode (B.BlockList b mempty) () () + rn4 <- newNode $ Merge0Node () () () + rn5 <- newNode $ LabelNode lblt () () + rn6 <- newNode $ LabelNode lblf () () + rn7 <- newNode $ AccumIONode mempty () () + rn8 <- newNode $ AccumIONode mempty () () + linkNodes (Ref rn3 0) (Ref rn4 2) + linkNodes (Ref rn4 0) (Ref rn5 1) + linkNodes (Ref rn4 1) (Ref rn6 1) + linkNodes (Ref rn5 0) (Ref rn7 1) + linkNodes (Ref rn6 0) (Ref rn8 1) + linkNodes r0 $ Ref rn7 0 + linkNodes r1 $ Ref rn8 0 + linkNodes r2 $ Ref rn3 1 +{-# INLINABLE mkBranch1 #-} + +mkLambda :: HasRewriter sig m => Ref -> (() -> () -> INetF ()) -> m () +mkLambda r0 mk1 = do + rn1 <- newNode $ mk1 () () + rn2 <- newNode $ LamNode () () () + linkNodes (Ref rn1 0) (Ref rn2 1) + linkNodes (Ref rn1 1) (Ref rn2 2) + linkNodes r0 $ Ref rn2 0 +{-# INLINE mkLambda #-} + +mkSelect :: B.Operand -> B.Operand -> B.Operand -> B.Operand +mkSelect (B.Constant bitc) opt opf = case bitc of + B.B0 -> opf + B.B1 -> opt +mkSelect opc (B.Constant B.B1) (B.Constant B.B0) = opc +mkSelect opc opt opf + | opt == opf = opt + | otherwise = B.Select opc opt opf +{-# INLINABLE mkSelect #-} + +mkChurchBool :: HasRewriter sig m => (m () -> m () -> m ()) -> m Ref +mkChurchBool sel = do + rn1 <- newNode $ LamNode () () () + rn2 <- newNode $ LamNode () () () + rn3 <- newNode $ DeadNode () + linkNodes (Ref rn1 2) (Ref rn2 0) + sel (mkTrue rn1 rn2 rn3) (mkFalse rn1 rn2 rn3) + pure $ Ref rn1 0 + where + mkTrue rn1 rn2 rn3 = do + rn4 <- newNode $ BoxNode 0 () () + linkNodes (Ref rn2 1) (Ref rn3 0) + linkNodes (Ref rn1 1) (Ref rn4 0) + linkNodes (Ref rn2 2) (Ref rn4 1) + + mkFalse rn1 rn2 rn3 = do + linkNodes (Ref rn1 1) (Ref rn3 0) + linkNodes (Ref rn2 1) (Ref rn2 2) +{-# INLINABLE mkChurchBool #-} + +type HasRewriter sig m = (Has (State INet) sig m, Has (State INetPairs) sig m + , Has (State INetSize) sig m) + +newtype INetSize = INetSize { unINetSize :: Int } + deriving newtype (Enum, Eq, Num, Ord) + +_INetSize :: Iso' INetSize Int +_INetSize = iso unINetSize INetSize +{-# INLINE _INetSize #-} + +newNode :: HasRewriter sig m => INetF () -> m Int +newNode mk = do + idx <- newNodeIndex + modify $ _INet . at idx ?~ (unsetRef <$ mk) + pure idx + where + unsetRef = Ref (-1) (-1) +{-# INLINE newNode #-} + +newName :: HasRewriter sig m => m B.Name +newName = B.Name <$> newNodeIndex +{-# INLINE newName #-} + +newLabel :: HasRewriter sig m => m B.Label +newLabel = B.Label <$> newNodeIndex +{-# INLINE newLabel #-} + +newNodeIndex :: Has (State INetSize) sig m => m Int +newNodeIndex = gets unINetSize <* modify @INetSize succ +{-# INLINE newNodeIndex #-} + +linkNodes :: HasRewriter sig m => Ref -> Ref -> m () +linkNodes r0 r1 = do + net <- get + modify @INet $ ix (refNode r0) . ix (refPort r0) .~ r1 + modify @INet $ ix (refNode r1) . ix (refPort r1) .~ r0 + modify $ _INetPairs %~ updatePairs net + where + updatePairs net + | refPort r0 == 0 && refPort r1 == 0 + = IS.insert (refNode r0) . IS.insert (refNode r1) + | refPort r0 == 0 = IS.delete (refNode r0) . IS.delete (deref r0) + | refPort r1 == 0 = IS.delete (refNode r1) . IS.delete (deref r1) + | otherwise = id + where + deref r2 = fromMaybe (-1) $ unINet net IM.!? refNode r2 + >>= (^? folded . to refNode) +{-# INLINE linkNodes #-} + +-- | Deletes all 'BoxNode' from the graph. Helps unclutter debugging output. +deleteBoxes :: HasRewriter sig m => m () +deleteBoxes = do + size <- gets unINetSize + go size 0 + where + go size rn0 + | rn0 < size = do + net <- gets unINet + case net IM.!? rn0 of + Just (BoxNode _ r1 r2) -> do + linkNodes r1 r2 + modify $ _INet . at rn0 .~ Nothing + _ -> pure () + go size $ succ rn0 + | otherwise = pure () +{-# INLINABLE deleteBoxes #-} + +-- | Effect for tracing rewrites. +data TraceRewrite m a where + {-| + The @m r@ continuation performs a rewrite on the @'INetF' 'Ref'@ nodes. + The 'Ref's refer to the principal ports of the nodes. + -} + TraceRewrite + :: Ref -> Ref -> INetF Ref -> INetF Ref -> m r -> TraceRewrite m r + +traceRewrite + :: Has TraceRewrite sig m + => Ref -> Ref -> INetF Ref -> INetF Ref -> m r -> m r +traceRewrite r0 r1 n0 n1 cont = send $ TraceRewrite r0 r1 n0 n1 cont +{-# INLINE traceRewrite #-} + diff --git a/src/Language/Elemental/Parser.hs b/src/Language/Elemental/Parser.hs index a32fc21..7f5c50d 100644 --- a/src/Language/Elemental/Parser.hs +++ b/src/Language/Elemental/Parser.hs @@ -367,6 +367,9 @@ isIdentifierChar = \case '@' -> False '(' -> False ')' -> False + ';' -> False + '{' -> False + '}' -> False c -> isLetter c || isMark c || isNumber c || isPunctuation c || isSymbol c -- MTL boilerplate diff --git a/src/Language/Elemental/Pretty.hs b/src/Language/Elemental/Pretty.hs index bcf9bca..37ce25f 100644 --- a/src/Language/Elemental/Pretty.hs +++ b/src/Language/Elemental/Pretty.hs @@ -10,7 +10,7 @@ module Language.Elemental.Pretty ( prettyDecl , prettyExpr , prettyType - , prettyLlvmType + , prettyBackendType , prettyNat -- * Unchecked , prettyUProgramF @@ -73,20 +73,27 @@ prettyExpr = flip $ \case Lam tx ey -> withPrec 0 $ "λ" <> prettyType 2 tx <+> prettyExpr 0 ey TypeLam ex -> withPrec 0 $ "Λ" <+> prettyExpr 0 ex Addr addr _ _ -> withPrec 3 $ braces $ "addr" <+> pretty addr - LlvmOperand lt _ -> withPrec 3 $ braces $ "op" <+> prettyLlvmType lt - LlvmIO lt _ -> withPrec 3 $ braces $ "io op" <+> prettyLlvmType lt + BackendOperand lt op + -> withPrec 3 $ braces $ "op" <+> prettyBackendType lt <+> pretty op + BackendIO lt b + -> withPrec 3 $ braces $ "io op" <+> prettyBackendType lt <+> pretty b + BackendPIO lt _ _ -> withPrec 3 $ braces $ "iop op" <+> prettyBackendType lt + -- ContIO t cont -> withPrec 3 $ braces $ "contIO" <+> prettyType 2 t + -- -- This might not be the correct type, but seeing into 'ContIO' helps. + -- <+> prettyExpr 2 (cont $ SBackendInt SZero) PureIO -> withPrec 3 $ braces "pureIO" BindIO -> withPrec 3 $ braces "bindIO" LoadPointer -> withPrec 3 $ braces "loadPointer" StorePointer -> withPrec 3 $ braces "storePointer" - Call _ _ ltargs ltret -> withPrec 3 $ braces $ "call" - <+> prettyLlvmType ltret <> parens (concatWith (surround ", ") - $ demoteList prettyLlvmType ltargs) + Call _ ltargs ltret -> withPrec 3 $ braces $ "call" + <+> prettyBackendType ltret <> parens (concatWith (surround ", ") + $ demoteList prettyBackendType ltargs) IsolateBit bidx size -> withPrec 3 $ braces $ "isolate" - <+> prettyNat bidx <+> prettyLlvmType (SLlvmInt size) + <+> prettyNat bidx <+> prettyBackendType (SBackendInt size) InsertBit size -> withPrec 3 $ braces - $ "insert" <+> prettyLlvmType (SLlvmInt size) - TestBit ex -> withPrec 3 $ braces $ "testBit" <+> prettyExpr 0 ex + $ "insert" <+> prettyBackendType (SBackendInt size) + TestBit -> withPrec 3 $ braces "testBit" + -- TestBit _ -> withPrec 3 $ braces "testBit" -- | Prettyprints a type with the given precedence. prettyType :: Int -> SType tscope t -> Doc ann @@ -98,12 +105,12 @@ prettyType = flip $ \case SPointerType pk tx -> withPrec 1 $ case pk of SReadPointer -> "ReadPointer" <+> prettyType 2 tx SWritePointer -> "WritePointer" <+> prettyType 2 tx - SLlvmType lt -> withPrec 3 $ prettyLlvmType lt + SBackendType lt -> withPrec 3 $ prettyBackendType lt --- | Prettyprints an t'LlvmType'. -prettyLlvmType :: SLlvmType lt -> Doc ann -prettyLlvmType = \case - SLlvmInt size -> "i" <> prettyNat size +-- | Prettyprints a t'BackendType'. +prettyBackendType :: SBackendType lt -> Doc ann +prettyBackendType = \case + SBackendInt size -> "i" <> prettyNat size -- | Prettyprints a 'Nat'. prettyNat :: SNat nat -> Doc ann diff --git a/src/Language/Elemental/TypeCheck.hs b/src/Language/Elemental/TypeCheck.hs index eb5ee46..23e9fdf 100644 --- a/src/Language/Elemental/TypeCheck.hs +++ b/src/Language/Elemental/TypeCheck.hs @@ -18,7 +18,7 @@ module Language.Elemental.TypeCheck , unify , unify' , unifyPtrKind - , unifyLlvmType + , unifyBackendType , unifyNat , checkScope , checkForeignType @@ -212,22 +212,23 @@ unify' mismatch ta tb cont = case (ta, tb) of (SPointerType tapk tax, SPointerType tbpk tbx) -> unifyPtrKind (mismatch ta tb) tapk tbpk $ unify' mismatch tax tbx cont - (SLlvmType lta, SLlvmType ltb) - -> unifyLlvmType (mismatch ta tb) lta ltb cont + (SBackendType lta, SBackendType ltb) + -> unifyBackendType (mismatch ta tb) lta ltb cont _ -> mismatch ta tb -- | Attempts to unify two pointer kinds, producing a proof if they're equal. unifyPtrKind :: r -> SPointerKind exp -> SPointerKind act -> (exp ~ act => r) -> r unifyPtrKind mismatch apk bpk cont = case (apk, bpk) of - (SReadPointer, SReadPointer) -> cont - (SWritePointer, SWritePointer) -> cont - _ -> mismatch + (SReadPointer, SReadPointer) -> cont + (SWritePointer, SWritePointer) -> cont + _ -> mismatch --- | Attempts to unify two t'LlvmType', producing a proof if they're equal. -unifyLlvmType :: r -> SLlvmType exp -> SLlvmType act -> (exp ~ act => r) -> r -unifyLlvmType mismatch lta ltb cont = case (lta, ltb) of - (SLlvmInt sizea, SLlvmInt sizeb) -> unifyNat mismatch sizea sizeb cont +-- | Attempts to unify two t'BackendType', producing a proof if they're equal. +unifyBackendType + :: r -> SBackendType exp -> SBackendType act -> (exp ~ act => r) -> r +unifyBackendType mismatch lta ltb cont = case (lta, ltb) of + (SBackendInt sizea, SBackendInt sizeb) -> unifyNat mismatch sizea sizeb cont -- | Attempts to unify two natural numbers, producing a proof if they're equal. unifyNat :: r -> SNat exp -> SNat act -> (exp ~ act => r) -> r diff --git a/test/Gen.hs b/test/Gen.hs index 1d7ce8e..fd09f1c 100644 --- a/test/Gen.hs +++ b/test/Gen.hs @@ -77,7 +77,8 @@ instance Eq SomeType where (SIOType tax, SIOType tbx) -> SomeType tax == SomeType tbx (SPointerType pka tax, SPointerType pkb tbx) -> unifyPtrKind False pka pkb $ SomeType tax == SomeType tbx - (SLlvmType lta, SLlvmType ltb) -> unifyLlvmType False lta ltb True + (SBackendType lta, SBackendType ltb) + -> unifyBackendType False lta ltb True _ -> False genPSubexpr :: MonadGen m => PExpr -> m PExpr @@ -169,7 +170,7 @@ genTypedExpr tscope scope t = orVar $ case t of <$> genTypedExpr (SSucc tscope) (sIncrementAll tscope SZero scope) tx SIOType _ -> Gen.discard SPointerType _ _ -> Gen.discard - SLlvmType _ -> Gen.discard + SBackendType _ -> Gen.discard where orVar :: m (Expr tscope scope t) -> m (Expr tscope scope t) orVar m = Gen.choice [m, findVar scope $ pure . Var] @@ -250,8 +251,9 @@ genMarshallableRetType cont = Gen.choice , genMarshallableType cont ] -genLlvmType :: forall m r. MonadGen m => (forall lt. SLlvmType lt -> m r) -> m r -genLlvmType cont = genNat sup $ cont . SLlvmInt +genBackendType + :: forall m r. MonadGen m => (forall lt. SBackendType lt -> m r) -> m r +genBackendType cont = genNat sup $ cont . SBackendInt where sup = SSucc $ SSucc $ SSucc $ SSucc $ SSucc $ SSucc $ SSucc $ SSucc SZero diff --git a/test/Golden.hs b/test/Golden.hs index 33c1d67..fb0e371 100644 --- a/test/Golden.hs +++ b/test/Golden.hs @@ -1,12 +1,30 @@ +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralisedNewtypeDeriving #-} {-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module Golden where -import Control.Algebra (run) +import Control.Algebra (Algebra(alg), Has, (:+:)(L, R), run) +import Control.Carrier.Reader (ReaderC(ReaderC), runReader) +import Control.Carrier.State.Church + (State, evalState, get, gets, modify, runState) +import Control.Lens (Fold, Iso', at, iso, ix, to, (^?), (%~), (^..)) +import Control.Monad (when) +import Control.Monad.IO.Class (MonadIO, liftIO) import Data.ByteString qualified as BS import Data.ByteString.Lazy qualified as BSL +import Data.Foldable (traverse_) import Data.Functor.Identity (Identity) +import Data.IntMap qualified as IM +import Data.IntSet qualified as IS +import Data.Map.Strict qualified as M import Data.Text qualified as T import Data.Text.Encoding qualified as TE import Data.Text.Short qualified as TS @@ -17,14 +35,24 @@ import LLVM.Module (File(File), moduleLLVMAssembly, withModuleFromAST, writeLLVMAssemblyToFile) import LLVM.PassManager (runPassManager, withPassManager) import LLVM.PassManager qualified as LLVM.Pass -import Prettyprinter (pretty, (<+>)) +import LLVM.Transforms qualified as LLVM.Opt +import Prettyprinter + ( Doc, PageWidth(Unbounded), Pretty + , defaultLayoutOptions, layoutPageWidth, layoutPretty + , line, nest, pretty, vcat, (<+>) + ) +import Prettyprinter.Render.Text (renderIO) import System.FilePath (replaceExtension, takeBaseName) -import System.IO (IOMode(WriteMode), withFile) +import System.IO + ( BufferMode(NoBuffering), Handle, IOMode(WriteMode) + , hPrint, hPutStrLn, hSetBuffering, withFile + ) import Test.Tasty (TestTree, testGroup) import Test.Tasty.Golden (findByExtension, goldenVsString) import Text.Megaparsec (MonadParsec(eof), errorBundlePretty, runParser) -import Language.Elemental +import Language.Elemental hiding (L, R) +import Language.Elemental.Backend.LLVM goldenTests :: IO TestTree @@ -37,38 +65,68 @@ goldenTests = do ] compileFile :: FilePath -> IO BSL.ByteString -compileFile file = do - src <- TE.decodeUtf8 <$> BS.readFile file - uprog <- parseSource src +compileFile file = runGolden $ \lh -> do + uprog <- liftIO $ do + hSetBuffering lh NoBuffering + src <- TE.decodeUtf8 <$> BS.readFile file + parseSource src let prog = printDiags $ tcProgram uprog - llvmDefs = emitProgram prog + liftIO $ hPutStrLn lh "Emitting" + exts <- emitProgram prog + graph <- get @INet + liftIO $ withFile (replaceExtension file ".inet") WriteMode + $ \h -> hPutDoc h $ pretty graph + liftIO $ hPutStrLn lh "Interpreting" + bprog <- compileINet exts + graph' <- get @INet + liftIO $ hPutStrLn lh "Translating" + let llvmDefs = compileProgram bprog llvm = defaultModule { moduleSourceFileName = TS.toShortByteString $ TS.fromString file , moduleDefinitions = llvmDefs } - withContext $ \ctx -> withModuleFromAST ctx llvm - $ \m -> withPassManager passes $ \pm -> do - -- writeLLVMAssemblyToFile doesn't truncate the file if it exists. - () <- withFile (replaceExtension file ".ll") WriteMode mempty - writeLLVMAssemblyToFile (File $ replaceExtension file ".ll") m - verify m - {- - Run -O3 multiple times because llvm-hs doesn't allow us to build - our own custom pipeline with all the passes we need and once - isn't enough. - -} - _ <- runPassManager pm m - _ <- runPassManager pm m - _ <- runPassManager pm m - _ <- runPassManager pm m - _ <- runPassManager pm m - BSL.fromStrict <$> moduleLLVMAssembly m + liftIO $ do + withFile (replaceExtension file ".opt.inet") WriteMode + $ \h -> hPutDoc h $ pretty graph' + withFile (replaceExtension file ".hl") WriteMode + $ \h -> hPutDoc h $ pretty bprog + withContext $ \ctx -> withModuleFromAST ctx llvm + $ \m -> withPassManager passes $ \pm + -> withPassManager passes' $ \pm' -> do + -- writeLLVMAssemblyToFile doesn't truncate the file. + () <- withFile (replaceExtension file ".ll") WriteMode mempty + writeLLVMAssemblyToFile (File $ replaceExtension file ".ll") m + verify m + {- + Run -O3 multiple times because llvm-hs doesn't allow us to + build our own custom pipeline with all the passes we need + and once isn't enough. + -} + _ <- runPassManager pm m + _ <- runPassManager pm' m + _ <- runPassManager pm m + _ <- runPassManager pm m + _ <- runPassManager pm' m + _ <- runPassManager pm m + _ <- runPassManager pm m + _ <- runPassManager pm' m + BSL.fromStrict <$> moduleLLVMAssembly m where parseSource :: T.Text -> IO PProgram parseSource src = case runParser (mkParser $ pProgram <* eof) file src of Left errors -> error $ errorBundlePretty errors Right uprog -> pure uprog + runGolden m = withFile (replaceExtension file ".log") WriteMode $ \lh + -> evalState @INet mempty + $ evalState @INetPairs mempty + $ evalState @INetSize 0 + $ runState @Count (flip (<$) . liftIO . hPrint lh . (<+>) "Total" + . pretty . unCount) 0 + $ runState @Stats (flip (<$) . liftIO . hPrint lh . pretty) mempty + $ runReader @Level 0 + $ runTraceRewrite <*> m $ lh + printDiags :: DiagnosisC Diagnostic Identity a -> a printDiags = run . runDiagnosis pure (printDiag "Error") (printDiag "Warning") @@ -81,10 +139,239 @@ passes = LLVM.Pass.CuratedPassSetSpec , LLVM.Pass.sizeLevel = Nothing , LLVM.Pass.unitAtATime = Nothing , LLVM.Pass.simplifyLibCalls = Nothing - , LLVM.Pass.loopVectorize = Nothing - , LLVM.Pass.superwordLevelParallelismVectorize = Nothing - , LLVM.Pass.useInlinerWithThreshold = Nothing + , LLVM.Pass.loopVectorize = Just True + , LLVM.Pass.superwordLevelParallelismVectorize = Just True + , LLVM.Pass.useInlinerWithThreshold = Just 65536 + , LLVM.Pass.dataLayout = Nothing + , LLVM.Pass.targetLibraryInfo = Nothing + , LLVM.Pass.targetMachine = Nothing + } + +-- CuratedPassSetSpec O3 doesn't apply -inline even though opt -O3 does. +passes' :: LLVM.Pass.PassSetSpec +passes' = LLVM.Pass.PassSetSpec + { LLVM.Pass.transforms = + [ LLVM.Opt.PartialInlining + , LLVM.Opt.FunctionInlining 225 + ] , LLVM.Pass.dataLayout = Nothing , LLVM.Pass.targetLibraryInfo = Nothing , LLVM.Pass.targetMachine = Nothing } + +newtype TraceRewriteC m a = TraceRewriteC (Handle -> m a) + deriving (Functor, Applicative, Monad, MonadIO) via ReaderC Handle m + +runTraceRewrite :: Handle -> TraceRewriteC m a -> m a +runTraceRewrite h (TraceRewriteC f) = f h +{-# INLINE runTraceRewrite #-} + +instance (MonadIO m, Has (State Count) sig m, Has (State INet) sig m + , Has (State INetPairs) sig m, Has (State INetSize) sig m + , Has (State Stats) sig m) + => Algebra (TraceRewrite :+: sig) (TraceRewriteC m) + where + alg hdl sig ctx = TraceRewriteC $ \h -> case sig of + L (TraceRewrite _ _ n0 n1 cont) -> do + size0 <- gets unINetSize + r <- runTraceRewrite h . hdl $ cont <$ ctx + lint size0 n0 n1 + let nh0 = nodeHead n0 + nh1 = nodeHead n1 + statKey = if nh0 < nh1 then (nh0, nh1) else (nh1, nh0) + modify $ _Count %~ succ + modify $ _Stats . at statKey %~ Just . maybe 1 succ + count <- gets unCount + netSize <- gets (IM.size . unINet) + pairsSize <- gets (IS.size . unINetPairs) + case (n0, n1) of + -- These nodes are extremely abundant and usually uninteresting. + (LamNode {}, _) -> pure () + (_, LamNode {}) -> pure () + (AppNode {}, DupNode {}) -> pure () + (DupNode {}, AppNode {}) -> pure () + (DupNode {}, DupNode {}) -> pure () + (DeadNode {}, _) -> pure () + (_, DeadNode {}) -> pure () + (BoxNode {}, _) -> pure () + (_, BoxNode {}) -> pure () + (TCrossNode {}, TSplitNode {}) -> pure () + (TSplitNode {}, TCrossNode {}) -> pure () + (TCloseNode {}, _) -> pure () + (_, TCloseNode {}) -> pure () + _ -> liftIO $ hPrint h + $ pretty count + <+> pretty netSize + <+> pretty pairsSize + <+> pretty size0 + <> nest 4 (line <> pretty n0 <> line <> pretty n1) + when (count > 1000000) $ do + stats <- get @Stats + liftIO $ hPrint h $ pretty stats + error "too much work, giving up" + pure r + R other -> alg (runTraceRewrite h . hdl) other ctx + where + lint :: HasRewriter sig m => Int -> INetF Ref -> INetF Ref -> m () + lint size n0 n1 = do + net <- gets unINet + (traverse_ . traverse) lintRef . snd $ IM.split (pred size) net + let f :: Fold (INetF Ref) Ref + f = traverse . to ((net IM.!?) . refNode) . traverse . traverse + traverse_ lintRef $ n0 ^.. f + traverse_ lintRef $ n1 ^.. f + where + lintRef :: HasRewriter sig m => Ref -> m () + lintRef (Ref (-1) (-1)) = abort "uninitialised ref" + lintRef r3 = do + net <- get @INet + case net ^? ix (refNode r3) of + Nothing -> abort $ "missing node:" <+> pretty r3 + Just n4 -> case n4 ^? ix (refPort r3) of + Nothing -> abort $ "missing port:" <+> pretty r3 + Just _ -> pure () + + abort :: HasRewriter sig m => Doc ann -> m a + abort msg = do + deleteBoxes + net <- get @INet + error . show $ "lint:" <+> msg + <> line <> "Size before reduction was" <+> pretty size + <> line <> "Node 1: " <> pretty n0 + <> line <> "Node 2: " <> pretty n1 + <> line <> pretty net + {-# INLINE alg #-} + +newtype Count = Count { unCount :: Int } + deriving newtype (Eq, Num, Ord) + +_Count :: Iso' Count Int +_Count = iso unCount Count +{-# INLINE _Count #-} + +newtype Stats = Stats { unStats :: M.Map (NodeHead, NodeHead) Int } + deriving newtype (Eq, Ord, Monoid, Semigroup) + +instance Pretty Stats where + pretty + = vcat . (uncurry ((. pretty) . (<+>) + . uncurry ((. pretty) . (<+>) . pretty)) <$>) + . M.assocs . unStats + +_Stats :: Iso' Stats (M.Map (NodeHead, NodeHead) Int) +_Stats = iso unStats Stats +{-# INLINE _Stats #-} + +data NodeHead + = AppHead | LamHead | DupHead | DeadHead | BoxHead + | ExternalRootHead | PrivateRootHead | AccumIOHead | AccumNBHead + | OperandHead | OperandAHead | OperandPHead + | IOHead | IOAHead | IOPHead | IOPureHead | IOContHead + | ReturnCHead | ReturnFHead | TailCallHead + | Bind0BHead | Bind0CHead | Bind0FHead | Bind1CHead | Bind1FHead + | Branch0CHead | Branch0FHead + | LabelHead | NamedBlockHead | Merge0Head | Merge1Head + | TBuild1Head | TBuild2Head | TCross1Head | TCross2Head + | TEntryHead | TSplitHead | TCloseHead | TLeaveHead | TMatchHead + | PArgumentHead | PReduceHead + | DupIOHead + deriving stock (Eq, Ord) + +instance Pretty NodeHead where + pretty AppHead = "App" + pretty LamHead = "Lam" + pretty DupHead = "Dup" + pretty DeadHead = "Dead" + pretty ExternalRootHead = "ExternalRoot" + pretty PrivateRootHead = "PrivateRoot" + pretty AccumIOHead = "AccumIO" + pretty AccumNBHead = "AccumNB" + pretty BoxHead = "Box" + pretty OperandHead = "Operand" + pretty OperandAHead = "OperandA" + pretty OperandPHead = "OperandP" + pretty IOHead = "IO" + pretty IOAHead = "IOA" + pretty IOPHead = "IOP" + pretty IOPureHead = "IOPure" + pretty IOContHead = "IOCont" + pretty ReturnCHead = "ReturnC" + pretty ReturnFHead = "ReturnF" + pretty TailCallHead = "TailCall" + pretty Bind0BHead = "Bind0B" + pretty Bind0CHead = "Bind0C" + pretty Bind0FHead = "Bind0F" + pretty Bind1CHead = "Bind1C" + pretty Bind1FHead = "Bind1F" + pretty Branch0CHead = "Branch0C" + pretty Branch0FHead = "Branch0F" + pretty LabelHead = "Label" + pretty NamedBlockHead = "NamedBlock" + pretty Merge0Head = "Merge0" + pretty Merge1Head = "Merge1" + pretty TBuild1Head = "TBuild1" + pretty TBuild2Head = "TBuild2" + pretty TCross1Head = "TCross1" + pretty TCross2Head = "TCross2" + pretty TEntryHead = "TEntry" + pretty TSplitHead = "TSplit" + pretty TCloseHead = "TClose" + pretty TLeaveHead = "TLeave" + pretty TMatchHead = "TMatch" + pretty PArgumentHead = "PArgument" + pretty PReduceHead = "PReduce" + pretty DupIOHead = "DupIO" + +nodeHead :: INetF a -> NodeHead +nodeHead x = case x of + AppNode {} -> AppHead + LamNode {} -> LamHead + DupNode {} -> DupHead + DeadNode {} -> DeadHead + BoxNode {} -> BoxHead + ExternalRootNode {} -> ExternalRootHead + PrivateRootNode {} -> PrivateRootHead + AccumIONode {} -> AccumIOHead + AccumNBNode {} -> AccumNBHead + OperandNode {} -> OperandHead + OperandANode {} -> OperandAHead + OperandPNode {} -> OperandPHead + IONode {} -> IOHead + IOANode {} -> IOAHead + IOPNode {} -> IOPHead + IOPureNode {} -> IOPureHead + IOContNode {} -> IOContHead + ReturnCNode {} -> ReturnCHead + ReturnFNode {} -> ReturnFHead + TailCallNode {} -> TailCallHead + Bind0BNode {} -> Bind0BHead + Bind0CNode {} -> Bind0CHead + Bind0FNode {} -> Bind0FHead + Bind1CNode {} -> Bind1CHead + Bind1FNode {} -> Bind1FHead + Branch0CNode {} -> Branch0CHead + Branch0FNode {} -> Branch0FHead + LabelNode {} -> LabelHead + NamedBlockNode {} -> NamedBlockHead + Merge0Node {} -> Merge0Head + Merge1Node {} -> Merge1Head + TBuild1Node {} -> TBuild1Head + TBuild2Node {} -> TBuild2Head + TCross1Node {} -> TCross1Head + TCross2Node {} -> TCross2Head + TEntryNode {} -> TEntryHead + TSplitNode {} -> TSplitHead + TCloseNode {} -> TCloseHead + TLeaveNode {} -> TLeaveHead + TMatchNode {} -> TMatchHead + PArgumentNode {} -> PArgumentHead + PReduceNode {} -> PReduceHead + DupIONode {} -> DupIOHead + +hPutDoc :: Handle -> Doc ann -> IO () +hPutDoc h doc = renderIO h $ layoutPretty opts doc + where + opts = defaultLayoutOptions + { layoutPageWidth = Unbounded + } + diff --git a/test/Golden/.gitignore b/test/Golden/.gitignore index 5210c4e..5363b53 100644 --- a/test/Golden/.gitignore +++ b/test/Golden/.gitignore @@ -1,4 +1,6 @@ *.log +*.inet +*.hl *.ll # Don't ignore optimised outputs; we need them for golden tests !*.opt.ll diff --git a/test/Golden/Arithmetic.elem b/test/Golden/Arithmetic.elem new file mode 100644 index 0000000..68c4d46 --- /dev/null +++ b/test/Golden/Arithmetic.elem @@ -0,0 +1,97 @@ +foreign export "expsign" c_expsign + : (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + → (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + → IO (∀ 0 → 0 → 0) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +zero = Λ λ((∀ 0 → (1 → 0) → 0) → 0) 0 (nothing @0) +succ = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) Λ λ((∀ 0 → (1 → 0) → 0) → 0) 0 (just @0 (1 @0 0)) + +nothing = Λ Λ λ0 λ(1 → 0) 1 +just = Λ λ0 Λ λ0 λ(1 → 0) 0 2 + +f = Λ λ0 λ0 0 +t = Λ λ0 λ0 1 + +add = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 1 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) 1 succ) + +mul = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 1 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) zero (add 1)) + +exp = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (succ zero) (mul 2)) + +isOdd = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 0 @(∀ 0 → 0 → 0) (λ(∀ 0 → ((∀ 0 → 0 → 0) → 0) → 0) + 0 @(∀ 0 → 0 → 0) f not) + +not = λ(∀ 0 → 0 → 0) Λ λ0 λ0 2 @0 0 1 + +from2 = λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + (λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) + add (from1 0) (mul (succ (succ zero)) (from1 1))) + +from1 = λ(∀ 0 → 0 → 0) 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (succ zero) zero + +c_expsign = λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + pureIO @(∀ 0 → 0 → 0) (isOdd (exp (from2 1) (from2 0))) + -- pureIO @(∀ 0 → 0 → 0) (isOdd (add (from2 1) (from2 0))) + +{- +to8 = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) _ + +c_exp = λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + pureIO @(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + (to8 (exp (from8 1) (from8 0))) + +pred = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 0 @(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + (λ(∀ 0 → ((∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) → 0) → 0) + 0 @(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + (nothing @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0)) + (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + 0 @(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + (just @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) zero) + (λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + just @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (succ 0)))) + +sub = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 0 @(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + (λ(∀ 0 → ((∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) → 0) → 0) + 0 @(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + (just @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) 2) + (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + 0 @(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + (nothing @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0)) + pred)) +-} + +{- +mod = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 1 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) zero (succMod 1)) + +-- succMod a b = "(succ b) mod a" if b = "b mod a" +succMod = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + eq (succ 0) 1 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) zero (succ 0) + +eq = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) isZero isSucc) + +isZero = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 0 @(∀ 0 → 0 → 0) t (λ(∀ 0 → 0 → 0) f) + +isSucc = λ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → ∀ 0 → 0 → 0) λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 0 @(∀ 0 → 0 → 0) f (λ(∀ 0 → 0 → 0) _) +-} + diff --git a/test/Golden/Arithmetic.opt.ll b/test/Golden/Arithmetic.opt.ll new file mode 100644 index 0000000..2f10210 --- /dev/null +++ b/test/Golden/Arithmetic.opt.ll @@ -0,0 +1,13 @@ +; ModuleID = '' +source_filename = "test/Golden/Arithmetic.elem" + +; Function Attrs: norecurse nounwind readnone +define i1 @expsign(i2, i2) local_unnamed_addr #0 { + %3 = and i2 %0, 1 + %4 = icmp ne i2 %3, 0 + %5 = icmp eq i2 %1, 0 + %6 = or i1 %5, %4 + ret i1 %6 +} + +attributes #0 = { norecurse nounwind readnone } diff --git a/test/Golden/BranchIO.elem b/test/Golden/BranchIO.elem new file mode 100644 index 0000000..b768e85 --- /dev/null +++ b/test/Golden/BranchIO.elem @@ -0,0 +1,7 @@ +foreign import c_t "t" : IO (∀ 0 → 0) +foreign import c_f "f" : IO (∀ 0 → 0) + +foreign export "main" main : (∀ 0 → 0 → 0) → IO (∀ 0 → 0) + +main = λ(∀ 0 → 0 → 0) 0 @(IO (∀ 0 → 0)) c_t c_f + diff --git a/test/Golden/BranchIO.opt.ll b/test/Golden/BranchIO.opt.ll new file mode 100644 index 0000000..ddc5256 --- /dev/null +++ b/test/Golden/BranchIO.opt.ll @@ -0,0 +1,21 @@ +; ModuleID = '' +source_filename = "test/Golden/BranchIO.elem" + +declare void @t() local_unnamed_addr + +declare void @f() local_unnamed_addr + +define void @main(i1) local_unnamed_addr { + br i1 %0, label %2, label %3 + +2: ; preds = %1 + tail call void @t() + br label %__elem_0.exit + +3: ; preds = %1 + tail call void @f() + br label %__elem_0.exit + +__elem_0.exit: ; preds = %3, %2 + ret void +} diff --git a/test/Golden/CataDynamic.opt.ll b/test/Golden/CataDynamic.opt.ll index b30b758..3fbb1bc 100644 --- a/test/Golden/CataDynamic.opt.ll +++ b/test/Golden/CataDynamic.opt.ll @@ -6,13 +6,13 @@ declare void @dothing() local_unnamed_addr define void @main(i1) local_unnamed_addr { tail call void @dothing() tail call void @dothing() - br i1 %0, label %3, label %2 + br i1 %0, label %__elem_0.exit, label %2 2: ; preds = %1 tail call void @dothing() tail call void @dothing() - br label %3 + br label %__elem_0.exit -3: ; preds = %1, %2 +__elem_0.exit: ; preds = %1, %2 ret void } diff --git a/test/Golden/CataStaticAccum.elem b/test/Golden/CataStaticAccum.elem new file mode 100644 index 0000000..f1c6e27 --- /dev/null +++ b/test/Golden/CataStaticAccum.elem @@ -0,0 +1,27 @@ +foreign export "main" main : IO (∀ 0 → 0 → 0) + +main = count @(IO (∀ 0 → 0 → 0)) (λ(∀ 0 → (IO (∀ 0 → 0 → 0) → 0) → 0) + 0 @(IO (∀ 0 → 0 → 0)) + (pureIO @(∀ 0 → 0 → 0) f) + (λ(IO (∀ 0 → 0 → 0)) bindIO + @(∀ 0 → 0 → 0) 0 + @(∀ 0 → 0 → 0) (λ(∀ 0 → 0 → 0) bindIO + @(∀ 0 → 0 → 0) c_dothing + @(∀ 0 → 0 → 0) (λ(∀ 0 → 0 → 0) pureIO @(∀ 0 → 0 → 0) (xor 1 0)))) + ) + +xor = λ(∀ 0 → 0 → 0) 0 @((∀ 0 → 0 → 0) → ∀ 0 → 0 → 0) not (λ(∀ 0 → 0 → 0) 0) +not = λ(∀ 0 → 0 → 0) Λ λ0 λ0 2 @0 0 1 + +f = Λ λ0 λ0 0 +t = Λ λ0 λ0 1 + +count = succ (succ (succ zero)) + +zero = Λ λ((∀ 0 → (1 → 0) → 0) → 0) 0 (Λ λ0 λ(1 → 0) 1) +succ = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) Λ λ((∀ 0 → (1 → 0) → 0) → 0) 0 (Λ λ0 λ(1 → 0) 0 (3 @1 2)) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +foreign import c_dothing "dothing" : IO (∀ 0 → 0 → 0) diff --git a/test/Golden/CataStaticAccum.opt.ll b/test/Golden/CataStaticAccum.opt.ll new file mode 100644 index 0000000..305e6cd --- /dev/null +++ b/test/Golden/CataStaticAccum.opt.ll @@ -0,0 +1,13 @@ +; ModuleID = '' +source_filename = "test/Golden/CataStaticAccum.elem" + +declare i1 @dothing() local_unnamed_addr + +define i1 @main() local_unnamed_addr { + %1 = tail call i1 @dothing() + %2 = tail call i1 @dothing() + %3 = tail call i1 @dothing() + %.v.i.i.i.i.i.i.i = xor i1 %1, %2 + %4 = xor i1 %.v.i.i.i.i.i.i.i, %3 + ret i1 %4 +} diff --git a/test/Golden/CataStaticDouble.elem b/test/Golden/CataStaticDouble.elem new file mode 100644 index 0000000..f360087 --- /dev/null +++ b/test/Golden/CataStaticDouble.elem @@ -0,0 +1,23 @@ +-- CataStatic but using a doubling function instead of repeating succ. + +foreign export "main" main : IO (∀ 0 → 0) + +main = count @(IO (∀ 0 → 0)) (λ(∀ 0 → (IO (∀ 0 → 0) → 0) → 0) + 0 @(IO (∀ 0 → 0)) + (pureIO @(∀ 0 → 0) (Λ λ0 0)) + (λ(IO (∀ 0 → 0)) bindIO @(∀ 0 → 0) 0 @(∀ 0 → 0) (λ(∀ 0 → 0) c_dothing)) + ) + +count = double (double (succ zero)) + +double = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0) + 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) 1 succ) + +zero = Λ λ((∀ 0 → (1 → 0) → 0) → 0) 0 (Λ λ0 λ(1 → 0) 1) +succ = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) Λ λ((∀ 0 → (1 → 0) → 0) → 0) 0 (Λ λ0 λ(1 → 0) 0 (3 @1 2)) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +foreign import c_dothing "dothing" : IO (∀ 0 → 0) diff --git a/test/Golden/CataStaticDouble.opt.ll b/test/Golden/CataStaticDouble.opt.ll new file mode 100644 index 0000000..00dcf4c --- /dev/null +++ b/test/Golden/CataStaticDouble.opt.ll @@ -0,0 +1,12 @@ +; ModuleID = '' +source_filename = "test/Golden/CataStaticDouble.elem" + +declare void @dothing() local_unnamed_addr + +define void @main() local_unnamed_addr { + tail call void @dothing() + tail call void @dothing() + tail call void @dothing() + tail call void @dothing() + ret void +} diff --git a/test/Golden/CataStaticTwice.elem b/test/Golden/CataStaticTwice.elem new file mode 100644 index 0000000..4ed27a8 --- /dev/null +++ b/test/Golden/CataStaticTwice.elem @@ -0,0 +1,22 @@ +-- CataStatic but using repeated composition instead of repeating succ. + +foreign export "main" main : IO (∀ 0 → 0) + +main = count @(IO (∀ 0 → 0)) (λ(∀ 0 → (IO (∀ 0 → 0) → 0) → 0) + 0 @(IO (∀ 0 → 0)) + (pureIO @(∀ 0 → 0) (Λ λ0 0)) + (λ(IO (∀ 0 → 0)) bindIO @(∀ 0 → 0) 0 @(∀ 0 → 0) (λ(∀ 0 → 0) c_dothing)) + ) + +count = twice (twice (twice succ)) zero + +twice = λ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → ∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) + λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) 1 (1 0) + +zero = Λ λ((∀ 0 → (1 → 0) → 0) → 0) 0 (Λ λ0 λ(1 → 0) 1) +succ = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) Λ λ((∀ 0 → (1 → 0) → 0) → 0) 0 (Λ λ0 λ(1 → 0) 0 (3 @1 2)) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +foreign import c_dothing "dothing" : IO (∀ 0 → 0) diff --git a/test/Golden/CataStaticTwice.opt.ll b/test/Golden/CataStaticTwice.opt.ll new file mode 100644 index 0000000..3d4c16c --- /dev/null +++ b/test/Golden/CataStaticTwice.opt.ll @@ -0,0 +1,16 @@ +; ModuleID = '' +source_filename = "test/Golden/CataStaticTwice.elem" + +declare void @dothing() local_unnamed_addr + +define void @main() local_unnamed_addr { + tail call void @dothing() + tail call void @dothing() + tail call void @dothing() + tail call void @dothing() + tail call void @dothing() + tail call void @dothing() + tail call void @dothing() + tail call void @dothing() + ret void +} diff --git a/test/Golden/ForeignNames.opt.ll b/test/Golden/ForeignNames.opt.ll index 21d579c..dcf24ed 100644 --- a/test/Golden/ForeignNames.opt.ll +++ b/test/Golden/ForeignNames.opt.ll @@ -2,12 +2,12 @@ source_filename = "test/Golden/ForeignNames.elem" ; Function Attrs: norecurse nounwind readnone -define void @"\5C"() local_unnamed_addr #0 { +define void @"\09"() local_unnamed_addr #0 { ret void } ; Function Attrs: norecurse nounwind readnone -define void @"\22"() local_unnamed_addr #0 { +define void @"\0A"() local_unnamed_addr #0 { ret void } @@ -17,12 +17,12 @@ define void @"\0D"() local_unnamed_addr #0 { } ; Function Attrs: norecurse nounwind readnone -define void @"\0A"() local_unnamed_addr #0 { +define void @"\22"() local_unnamed_addr #0 { ret void } ; Function Attrs: norecurse nounwind readnone -define void @"\09"() local_unnamed_addr #0 { +define void @"\5C"() local_unnamed_addr #0 { ret void } diff --git a/test/Golden/FunctionInIO.opt.ll b/test/Golden/FunctionInIO.opt.ll index af3a468..ecf8b76 100644 --- a/test/Golden/FunctionInIO.opt.ll +++ b/test/Golden/FunctionInIO.opt.ll @@ -3,6 +3,12 @@ source_filename = "test/Golden/FunctionInIO.elem" declare i1 @getbit() local_unnamed_addr +; Function Attrs: norecurse nounwind readnone +define i1 @main(i1) local_unnamed_addr #0 { + %not..i = xor i1 %0, true + ret i1 %not..i +} + define i1 @main2() local_unnamed_addr { %1 = tail call i1 @getbit() %2 = tail call i1 @getbit() @@ -10,10 +16,4 @@ define i1 @main2() local_unnamed_addr { ret i1 %3 } -; Function Attrs: norecurse nounwind readnone -define i1 @main(i1) local_unnamed_addr #0 { - %not. = xor i1 %0, true - ret i1 %not. -} - attributes #0 = { norecurse nounwind readnone } diff --git a/test/Golden/IOInIO.elem b/test/Golden/IOInIO.elem new file mode 100644 index 0000000..916ff0d --- /dev/null +++ b/test/Golden/IOInIO.elem @@ -0,0 +1,11 @@ +foreign export "main" main : IO (∀ 0 → 0 → 0) + +foreign import c_getbit "getbit" : IO (∀ 0 → 0 → 0) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +main = bindIO + @(IO (∀ 0 → 0 → 0)) (pureIO @(IO (∀ 0 → 0 → 0)) c_getbit) + @(∀ 0 → 0 → 0) (λ(IO (∀ 0 → 0 → 0)) 0) + diff --git a/test/Golden/IOInIO.opt.ll b/test/Golden/IOInIO.opt.ll new file mode 100644 index 0000000..0d6ad95 --- /dev/null +++ b/test/Golden/IOInIO.opt.ll @@ -0,0 +1,9 @@ +; ModuleID = '' +source_filename = "test/Golden/IOInIO.elem" + +declare i1 @getbit() local_unnamed_addr + +define i1 @main() local_unnamed_addr { + %1 = tail call i1 @getbit() + ret i1 %1 +} diff --git a/test/Golden/MemoryBit.opt.ll b/test/Golden/MemoryBit.opt.ll index 16b845f..63592fb 100644 --- a/test/Golden/MemoryBit.opt.ll +++ b/test/Golden/MemoryBit.opt.ll @@ -4,8 +4,8 @@ source_filename = "test/Golden/MemoryBit.elem" ; Function Attrs: nofree norecurse nounwind define void @main() local_unnamed_addr #0 { %1 = load volatile i1, i1* inttoptr (i14 -8192 to i1*), align 8192 - %not. = xor i1 %1, true - store volatile i1 %not., i1* inttoptr (i14 -8192 to i1*), align 8192 + %not..i = xor i1 %1, true + store volatile i1 %not..i, i1* inttoptr (i14 -8192 to i1*), align 8192 ret void } diff --git a/test/Golden/NestedBranch.elem b/test/Golden/NestedBranch.elem new file mode 100644 index 0000000..31493a9 --- /dev/null +++ b/test/Golden/NestedBranch.elem @@ -0,0 +1,21 @@ +foreign export "main" main + : (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + → IO (∀ 0 → 0) + +foreign import c_dothing "dothing" : IO (∀ 0 → 0) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +main = abort_if_nonzero c_dothing + +abort_if_nonzero = λ(IO (∀ 0 → 0)) λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + 0 @(∀ 0 → 0 → 0) (λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) + λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) + or 0 (or 1 (or 2 (or 3 (or 4 (or 5 (or 6 7)))))) + ) @(IO (∀ 0 → 0)) (pureIO @(∀ 0 → 0) (Λ λ0 0)) 1 + +or = λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) 1 @(∀ 0 → 0 → 0) t 0 + +t = Λ λ0 λ0 1 + diff --git a/test/Golden/NestedBranch.opt.ll b/test/Golden/NestedBranch.opt.ll new file mode 100644 index 0000000..0eb1584 --- /dev/null +++ b/test/Golden/NestedBranch.opt.ll @@ -0,0 +1,16 @@ +; ModuleID = '' +source_filename = "test/Golden/NestedBranch.elem" + +declare void @dothing() local_unnamed_addr + +define void @main(i8) local_unnamed_addr { + %2 = icmp eq i8 %0, 0 + br i1 %2, label %3, label %__elem_14.exit + +3: ; preds = %1 + tail call void @dothing() + br label %__elem_14.exit + +__elem_14.exit: ; preds = %1, %3 + ret void +} diff --git a/test/Golden/NestedBranch2.elem b/test/Golden/NestedBranch2.elem new file mode 100644 index 0000000..a2d1932 --- /dev/null +++ b/test/Golden/NestedBranch2.elem @@ -0,0 +1,36 @@ +foreign export "main" main + -- : (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + -- : (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + : (∀ 0 → 0 → 0) + → IO (∀ 0 → 0) + +foreign import c_dothing "dothing" + -- : (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + -- : (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + : (∀ 0 → 0 → 0) + → IO (∀ 0 → 0) + +foreign primitive pureIO : ∀ 0 → IO 0 +-- foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +{- +main = abort_if_null (λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) bindIO + @(∀ 0 → 0) (c_dothing 0) + @(∀ 0 → 0) (λ(∀ 0 → 0) (c_dothing 1))) +-} +main = abort_if_null c_dothing + +-- abort_if_null = λ((∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) {- → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) -} → 0) → 0) → IO (∀ 0 → 0)) +-- λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) {- → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) -} → 0) → 0) +-- 0 @(∀ 0 → 0 → 0) (λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) -- λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) +-- -- or 0 (or 1 (or 2 3)) +-- or 0 1 +-- ) @(IO (∀ 0 → 0)) (1 0) (pureIO @(∀ 0 → 0) (Λ λ0 0)) +-- +-- or = λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) 1 @(∀ 0 → 0 → 0) t 0 +-- +-- t = Λ λ0 λ0 1 + +abort_if_null = λ((∀ 0 → 0 → 0) → IO (∀ 0 → 0)) λ(∀ 0 → 0 → 0) 0 @(IO (∀ 0 → 0)) (1 0) (pureIO @(∀ 0 → 0) (Λ λ0 0)) + + diff --git a/test/Golden/NestedBranch2.opt.ll b/test/Golden/NestedBranch2.opt.ll new file mode 100644 index 0000000..5595cb1 --- /dev/null +++ b/test/Golden/NestedBranch2.opt.ll @@ -0,0 +1,15 @@ +; ModuleID = '' +source_filename = "test/Golden/NestedBranch2.elem" + +declare void @dothing(i1) local_unnamed_addr + +define void @main(i1) local_unnamed_addr { + br i1 %0, label %2, label %__elem_0.exit + +2: ; preds = %1 + tail call void @dothing(i1 true) + br label %__elem_0.exit + +__elem_0.exit: ; preds = %1, %2 + ret void +} diff --git a/test/Golden/NestedBranch3.elem b/test/Golden/NestedBranch3.elem new file mode 100644 index 0000000..0368fa8 --- /dev/null +++ b/test/Golden/NestedBranch3.elem @@ -0,0 +1,25 @@ +foreign export "main" main : IO (∀ 0 → 0 → 0) + +foreign import c_dothing "dothing" + : IO (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +main = bindIO + @(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) c_dothing + @(∀ 0 → 0 → 0) (abort_if_null (λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) bindIO + @(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) c_dothing + @(∀ 0 → 0 → 0) (abort_if_null (λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) pureIO @(∀ 0 → 0 → 0) t)))) + +abort_if_null = λ((∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) → IO (∀ 0 → 0 → 0)) + λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + 0 @(∀ 0 → 0 → 0) (λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) + or 0 1 + ) @(IO (∀ 0 → 0 → 0)) (1 0) (pureIO @(∀ 0 → 0 → 0) f) + +or = λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) 1 @(∀ 0 → 0 → 0) t 0 + +f = Λ λ0 λ0 0 +t = Λ λ0 λ0 1 + diff --git a/test/Golden/NestedBranch3.opt.ll b/test/Golden/NestedBranch3.opt.ll new file mode 100644 index 0000000..ebcfc6f --- /dev/null +++ b/test/Golden/NestedBranch3.opt.ll @@ -0,0 +1,19 @@ +; ModuleID = '' +source_filename = "test/Golden/NestedBranch3.elem" + +declare i2 @dothing() local_unnamed_addr + +define i1 @main() local_unnamed_addr { + %1 = tail call i2 @dothing() + %2 = icmp eq i2 %1, 0 + br i1 %2, label %__elem_2.exit, label %__elem_2.exit.sink.split + +__elem_2.exit.sink.split: ; preds = %0 + %3 = tail call i2 @dothing() + %4 = icmp ne i2 %3, 0 + br label %__elem_2.exit + +__elem_2.exit: ; preds = %0, %__elem_2.exit.sink.split + %5 = phi i1 [ %4, %__elem_2.exit.sink.split ], [ false, %0 ] + ret i1 %5 +} diff --git a/test/Golden/SelfReference.elem b/test/Golden/SelfReference.elem new file mode 100644 index 0000000..6294070 --- /dev/null +++ b/test/Golden/SelfReference.elem @@ -0,0 +1,15 @@ +-- Minimal program that can't be optimally evaluated without any book-keeping. + +foreign export "main" main : IO (∀ 0 → 0) + +foreign primitive pureIO : ∀ 0 → IO 0 + +main = pureIO @(∀ 0 → 0) (id @(∀ 0 → 0) id) + +-- Both t and f cause problems here. +id = Λ λ0 t @0 0 0 +-- id = Λ λ0 f @0 0 0 + +t = Λ λ0 λ0 1 +-- f = Λ λ0 λ0 0 + diff --git a/test/Golden/SelfReference.opt.ll b/test/Golden/SelfReference.opt.ll new file mode 100644 index 0000000..1cd9fdd --- /dev/null +++ b/test/Golden/SelfReference.opt.ll @@ -0,0 +1,9 @@ +; ModuleID = '' +source_filename = "test/Golden/SelfReference.elem" + +; Function Attrs: norecurse nounwind readnone +define void @main() local_unnamed_addr #0 { + ret void +} + +attributes #0 = { norecurse nounwind readnone } diff --git a/test/Golden/ShareBindCont.elem b/test/Golden/ShareBindCont.elem new file mode 100644 index 0000000..3f1bd60 --- /dev/null +++ b/test/Golden/ShareBindCont.elem @@ -0,0 +1,17 @@ +foreign export "main1" main1 : IO (∀ 0 → 0 → 0) +foreign export "main2" main2 : IO (∀ 0 → 0 → 0) + +foreign import c_getbit "getbit" : IO (∀ 0 → 0 → 0) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +main1 = shared (pureIO @(∀ 0 → 0 → 0)) +main2 = shared (λ(∀ 0 → 0 → 0) pureIO @(∀ 0 → 0 → 0) (not 0)) + +shared = λ((∀ 0 → 0 → 0) → IO (∀ 0 → 0 → 0)) bindIO + @(∀ 0 → 0 → 0) c_getbit + @(∀ 0 → 0 → 0) 0 + +not = λ(∀ 0 → 0 → 0) Λ λ0 λ0 2 @0 0 1 + diff --git a/test/Golden/ShareBindCont.opt.ll b/test/Golden/ShareBindCont.opt.ll new file mode 100644 index 0000000..6920904 --- /dev/null +++ b/test/Golden/ShareBindCont.opt.ll @@ -0,0 +1,15 @@ +; ModuleID = '' +source_filename = "test/Golden/ShareBindCont.elem" + +declare i1 @getbit() local_unnamed_addr + +define i1 @main1() local_unnamed_addr { + %1 = tail call i1 @getbit() + ret i1 %1 +} + +define i1 @main2() local_unnamed_addr { + %1 = tail call i1 @getbit() + %not..i.i = xor i1 %1, true + ret i1 %not..i.i +} diff --git a/test/Golden/ShareFunction.elem b/test/Golden/ShareFunction.elem new file mode 100644 index 0000000..fb135d9 --- /dev/null +++ b/test/Golden/ShareFunction.elem @@ -0,0 +1,13 @@ +foreign export "value" pureValue : IO (∀ 0 → 0) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +pureValue = bindIO @(∀ 0 → 0) (pureIO @(∀ 0 → 0) value) + @(∀ 0 → 0) (λ(∀ 0 → 0) pureIO @(∀ 0 → 0) 0) + +value = Λ λ0 0 + +-- This assignment causes duplication, which can break the rewriting. +break = value + diff --git a/test/Golden/ShareFunction.opt.ll b/test/Golden/ShareFunction.opt.ll new file mode 100644 index 0000000..10b3b20 --- /dev/null +++ b/test/Golden/ShareFunction.opt.ll @@ -0,0 +1,9 @@ +; ModuleID = '' +source_filename = "test/Golden/ShareFunction.elem" + +; Function Attrs: norecurse nounwind readnone +define void @value() local_unnamed_addr #0 { + ret void +} + +attributes #0 = { norecurse nounwind readnone } diff --git a/test/Golden/ShareFunction2.elem b/test/Golden/ShareFunction2.elem new file mode 100644 index 0000000..fbc14dd --- /dev/null +++ b/test/Golden/ShareFunction2.elem @@ -0,0 +1,10 @@ +-- Minimal test case that breaks when there are no duplication tags. + +foreign primitive pureIO : ∀ 0 → IO 0 + +foreign export "value" pureValue : IO (∀ 0 → 0) + +pureValue = pureIO @(∀ 0 → 0) (Λ λ0 0) + +break = pureValue + diff --git a/test/Golden/ShareFunction2.opt.ll b/test/Golden/ShareFunction2.opt.ll new file mode 100644 index 0000000..885283b --- /dev/null +++ b/test/Golden/ShareFunction2.opt.ll @@ -0,0 +1,9 @@ +; ModuleID = '' +source_filename = "test/Golden/ShareFunction2.elem" + +; Function Attrs: norecurse nounwind readnone +define void @value() local_unnamed_addr #0 { + ret void +} + +attributes #0 = { norecurse nounwind readnone } diff --git a/test/Golden/ShareIO.elem b/test/Golden/ShareIO.elem new file mode 100644 index 0000000..f6eaffb --- /dev/null +++ b/test/Golden/ShareIO.elem @@ -0,0 +1,30 @@ +foreign export "main1" main1 : IO (∀ 0 → 0) +foreign export "main2" main2 : IO (∀ 0 → 0) + +foreign import c_getbit "getbit" : IO (∀ 0 → 0 → 0) +foreign import c_putbit "putbit" : (∀ 0 → 0 → 0) → IO (∀ 0 → 0) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +main1 = bindIO + @(∀ 0 → 0 → 0) getValue + @(∀ 0 → 0) c_putbit + +-- main2 = main1 +main2 = bindIO + @(∀ 0 → 0 → 0) getValue + @(∀ 0 → 0) c_putbit + +-- This is a fairly tricky sequence of binds to duplicate. +getValue = bindIO + @(∀ 0 → 0 → 0) c_getbit + @(∀ 0 → 0 → 0) (λ(∀ 0 → 0 → 0) + bindIO + @(∀ 0 → 0 → 0) c_getbit + @(∀ 0 → 0 → 0) (λ(∀ 0 → 0 → 0) pureIO @(∀ 0 → 0 → 0) (xor 0 1))) + +not = λ(∀ 0 → 0 → 0) Λ λ0 λ0 2 @0 0 1 + +xor = λ(∀ 0 → 0 → 0) 0 @((∀ 0 → 0 → 0) → ∀ 0 → 0 → 0) not (λ(∀ 0 → 0 → 0) 0) + diff --git a/test/Golden/ShareIO.opt.ll b/test/Golden/ShareIO.opt.ll new file mode 100644 index 0000000..df885d2 --- /dev/null +++ b/test/Golden/ShareIO.opt.ll @@ -0,0 +1,22 @@ +; ModuleID = '' +source_filename = "test/Golden/ShareIO.elem" + +declare void @putbit(i1) local_unnamed_addr + +declare i1 @getbit() local_unnamed_addr + +define void @main1() local_unnamed_addr { + %1 = tail call i1 @getbit() + %2 = tail call i1 @getbit() + %3 = xor i1 %1, %2 + tail call void @putbit(i1 %3) + ret void +} + +define void @main2() local_unnamed_addr { + %1 = tail call i1 @getbit() + %2 = tail call i1 @getbit() + %3 = xor i1 %1, %2 + tail call void @putbit(i1 %3) + ret void +} diff --git a/test/Golden/ShareIOPoly.elem b/test/Golden/ShareIOPoly.elem new file mode 100644 index 0000000..b54ce80 --- /dev/null +++ b/test/Golden/ShareIOPoly.elem @@ -0,0 +1,17 @@ +-- Verifies that polymorphic functions are shared correctly. + +foreign export "main1" main1 : (∀ 0 → 0 → 0) → IO (∀ 0 → 0 → 0) +foreign export "main2" main2 : (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) → IO (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + +foreign import c_dothing "dothing" : IO (∀ 0 → 0) + +foreign primitive pureIO : ∀ 0 → IO 0 +foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0 + +main1 = shared @(∀ 0 → 0 → 0) +main2 = shared @(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0) + +shared = Λ λ0 bindIO + @(∀ 0 → 0) c_dothing + @0 (λ(∀ 0 → 0) pureIO @0 1) + diff --git a/test/Golden/ShareIOPoly.opt.ll b/test/Golden/ShareIOPoly.opt.ll new file mode 100644 index 0000000..21305c1 --- /dev/null +++ b/test/Golden/ShareIOPoly.opt.ll @@ -0,0 +1,14 @@ +; ModuleID = '' +source_filename = "test/Golden/ShareIOPoly.elem" + +declare void @dothing() local_unnamed_addr + +define i1 @main1(i1 returned) local_unnamed_addr { + tail call void @dothing() + ret i1 %0 +} + +define i2 @main2(i2 returned) local_unnamed_addr { + tail call void @dothing() + ret i2 %0 +} diff --git a/test/Golden/SimpleArgs.opt.ll b/test/Golden/SimpleArgs.opt.ll index d884c87..00ecb3a 100644 --- a/test/Golden/SimpleArgs.opt.ll +++ b/test/Golden/SimpleArgs.opt.ll @@ -2,13 +2,13 @@ source_filename = "test/Golden/SimpleArgs.elem" ; Function Attrs: norecurse nounwind readnone -define i1 @snd(i1, i1 returned) local_unnamed_addr #0 { - ret i1 %1 +define i1 @main(i1 returned) local_unnamed_addr #0 { + ret i1 %0 } ; Function Attrs: norecurse nounwind readnone -define i1 @main(i1 returned) local_unnamed_addr #0 { - ret i1 %0 +define i1 @snd(i1, i1 returned) local_unnamed_addr #0 { + ret i1 %1 } attributes #0 = { norecurse nounwind readnone } diff --git a/test/Main.hs b/test/Main.hs index dcea660..adf62f6 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -27,4 +27,5 @@ tests = do ] where timeout :: Timeout - timeout = mkTimeout 1000000 -- 1s + timeout = mkTimeout $ 3600 * 1000000 -- 1 hour + diff --git a/test/Pretty.hs b/test/Pretty.hs index 23f7878..6fc8f66 100644 --- a/test/Pretty.hs +++ b/test/Pretty.hs @@ -46,8 +46,11 @@ propParseDecl = property $ do propParseUProgram :: Property propParseUProgram = property $ do program <- forAllWith (show . prettyUProgram) $ genUProgram 5 5 - tripping' program enc dec + tripping' show1 T.unpack show3 program enc dec where + show1 = show . prettyUProgram + show3 = either id show1 + enc :: UProgram -> T.Text enc = renderStrict . layoutPretty defaultLayoutOptions . prettyUProgram diff --git a/test/Util.hs b/test/Util.hs index 2e70ae8..279dcf7 100644 --- a/test/Util.hs +++ b/test/Util.hs @@ -7,6 +7,7 @@ import Control.Monad (unless) import Data.Bifunctor (Bifunctor, first) import Data.Fix (Fix(Fix), foldFix, unFix) import Hedgehog +import Hedgehog.Internal.Property (failWith) import Language.Elemental @@ -26,10 +27,20 @@ stripType = foldFix $ Fix . sndP1 (===) :: (Eq a, MonadTest m) => a -> a -> m () x === y = unless (x == y) failure +-- Hedgehog's tripping requires 'Show' instances. tripping' :: (Eq (f a), Applicative f, MonadTest m) - => a -> (a -> b) -> (b -> f a) -> m () -tripping' x enc dec = if pure x == my then pure () else failure + => (a -> String) -> (b -> String) -> (f a -> String) + -> a -> (a -> b) -> (b -> f a) -> m () +tripping' show1 show2 show3 x enc dec + = if pure x == my then pure () else failWith Nothing $ unlines + [ "━━━ Original ━━━" + , show1 x + , "━━━ Intermediate ━━━" + , show2 i + , "━━━ Roundtrip ━━━" + , show3 my + ] where i = enc x my = dec i