diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c)2013, Galois, Inc + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Galois, Inc nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ivory.cabal b/ivory.cabal new file mode 100644 --- /dev/null +++ b/ivory.cabal @@ -0,0 +1,71 @@ +-- Initial ivory.cabal generated by cabal init. For further documentation, +-- see http://haskell.org/cabal/users-guide/ + +name: ivory +version: 0.1.0.0 +author: Galois, Inc. +maintainer: trevor@galois.com +category: Language +synopsis: Safe embedded C programming. +description: Using GHC type-system extensions, enforces safe low-level programming, while maintaining expressiveness. +homepage: http://smaccmpilot.org/languages/ivory-introduction.html +build-type: Simple +cabal-version: >= 1.10 +license: BSD3 +license-file: LICENSE +source-repository this + type: git + location: https://github.com/GaloisInc/ivory + tag: hackage-0100 + +library + exposed-modules: Ivory.Language, + Ivory.Language.Effects, + Ivory.Language.Monad, + Ivory.Language.Area, + Ivory.Language.Array, + Ivory.Language.Assert, + Ivory.Language.Bits, + Ivory.Language.BoundedInteger, + Ivory.Language.CArray, + Ivory.Language.Cast, + Ivory.Language.Cond, + Ivory.Language.Const, + Ivory.Language.Float, + Ivory.Language.IBool, + Ivory.Language.IChar, + Ivory.Language.IIntegral, + Ivory.Language.Init, + Ivory.Language.IString, + Ivory.Language.Loop, + Ivory.Language.MemArea, + Ivory.Language.Module, + Ivory.Language.Proc, + Ivory.Language.Proxy, + Ivory.Language.Ptr, + Ivory.Language.Ref, + Ivory.Language.Scope, + Ivory.Language.Sint, + Ivory.Language.SizeOf, + Ivory.Language.String, + Ivory.Language.Struct, + Ivory.Language.Syntax, + Ivory.Language.Syntax.AST, + Ivory.Language.Syntax.Type, + Ivory.Language.Syntax.Names, + Ivory.Language.Type, + Ivory.Language.Uint + other-modules: Ivory.Language.Struct.Parser, + Ivory.Language.Struct.Quote + build-depends: base >= 4.6 && < 4.7, + pretty >= 1.1, + containers >= 0.5, + monadLib >= 3.7, + template-haskell >= 2.8, + parsec >= 3.1.3, + -- QuickCheck >= 2.5.1, + th-lift >= 0.5.5 + hs-source-dirs: src + default-language: Haskell2010 + + ghc-options: -Wall diff --git a/src/Ivory/Language.hs b/src/Ivory/Language.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language.hs @@ -0,0 +1,219 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE NoMonomorphismRestriction #-} + +module Ivory.Language ( + -- * Kinds + Area(..) + , Proc(..) + + -- * Types + , IvoryType(), IvoryArea() + , IvoryVar() + , IvoryExpr() + + , OpaqueType() + + -- ** Non-null References + , IvoryRef() + , ConstRef() + , IvoryStore() + , Ref(), refToPtr, constRef, deref, store, refCopy + + -- ** Stack Allocation + , IvoryInit(..), Init() + , IvoryZero(izero) + , iarray + , InitStruct(), (.=), istruct + , local + + -- ** SizeOf + , IvorySizeOf(..), sizeOf + + -- ** Nullable Pointers + , Ptr(), nullPtr + + -- ** Booleans + , IBool(), true, false + + -- ** Characters + , IChar(), char + + -- ** Strings + , IString() + + -- ** Signed Integers + , Sint8() + , Sint16() + , Sint32() + , Sint64() + + -- ** Unsigned Integers + , Uint8() + , Uint16() + , Uint32() + , Uint64() + + -- ** Floating-point Numbers + , IFloat() + , IDouble() + , isnan, isinf, roundF, ceilF, floorF + , ifloat, idouble + + -- * Effects + , Effects(..) + , BreakEff(..), GetBreaks(), AllowBreak(), ClearBreak(), noBreak + , ReturnEff(..), GetReturn(), ClearReturn(), noReturn + , AllocEff(..), GetAlloc(), ClearAlloc(), noAlloc + , AllocEffects, ProcEffects, NoEffects + + -- * Language + + -- ** Monadic Interface + , Ivory() + , RefScope(..) + + -- ** Subexpression naming + , assign + + -- ** Constants + , extern + + -- ** Arithmetic (operators from the 'Num' class are also provided). + , IvoryIntegral((.%), iDiv) + + -- ** Comparisons + , IvoryEq((==?),(/=?)) + , IvoryOrd((>?),(>=?),(), Label() + + -- ** Arrays + , (!) + , fromIx, toIx, Ix(), ixSize + , arrayLen + , SingI() + , toCArray + + -- ** Strings + , IvoryString(..) + + -- ** Looping + , for, times + , breakOut + , arrayMap + , forever + + -- ** Call + , call, indirect + , call_, indirect_ + + -- ** Conditional Branching + , ifte_, (?), withRef + + -- ** Return + , ret, retVoid + + -- ** Type-safe casting. + , SafeCast(), RuntimeCast(), Default() + , safeCast, castWith, castDefault + , SignCast(), signCast + + -- ** Module Definitions + , AST.Module(), moduleName, package + , ModuleDef, incl, depend, defStruct + , defStringType + , defMemArea, defConstMemArea + , inclHeader + , private, public + , sourceDep + + + -- * Utilities + , Proxy(..) + ) where + +import Ivory.Language.Area +import Ivory.Language.Array +import Ivory.Language.Assert +import Ivory.Language.Bits +import Ivory.Language.CArray +import Ivory.Language.Cast +import Ivory.Language.Cond +import Ivory.Language.Const +import Ivory.Language.Effects +import Ivory.Language.Float +import Ivory.Language.IBool +import Ivory.Language.IChar +import Ivory.Language.IIntegral +import Ivory.Language.IString +import Ivory.Language.Init +import Ivory.Language.Loop +import Ivory.Language.MemArea +import Ivory.Language.Module +import Ivory.Language.Monad +import Ivory.Language.Proc +import Ivory.Language.Proxy +import Ivory.Language.Ptr +import Ivory.Language.Ref +import Ivory.Language.Scope +import Ivory.Language.Sint +import Ivory.Language.SizeOf +import Ivory.Language.String +import Ivory.Language.Struct +import Ivory.Language.Struct.Quote (ivory) +import Ivory.Language.Type +import Ivory.Language.Uint +import qualified Ivory.Language.Syntax.AST as AST + +import GHC.TypeLits (SingI) + + +-- Language -------------------------------------------------------------------- + +-- | Unwrap a pointer, and use it as a reference. +withRef :: IvoryArea area + => Ptr as area + -> (Ref as area -> Ivory eff t) + -> Ivory eff f + -> Ivory eff () +withRef ptr t = ifte_ (nullPtr /=? ptr) (t (ptrToRef ptr)) + +-- | Primitive return from function. +ret :: (GetReturn eff ~ Returns r, IvoryVar r) => r -> Ivory eff () +ret r = emit (AST.Return (typedExpr r)) + +retVoid :: (GetReturn eff ~ Returns ()) => Ivory eff () +retVoid = emit AST.ReturnVoid diff --git a/src/Ivory/Language/Area.hs b/src/Ivory/Language/Area.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Area.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Ivory.Language.Area where + +import Ivory.Language.Proxy +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + +import GHC.TypeLits (Nat,Symbol,SingI,Sing,sing) + +-- Memory Areas ---------------------------------------------------------------- + +-- | Type proxies for @Area@s. +type AProxy a = Proxy (a :: Area *) + +-- | The kind of memory-area types. +data Area k + = Struct Symbol + | Array Nat (Area k) + | CArray (Area k) + | Stored k + -- ^ This is lifting for a *-kinded type + +-- | Guard the inhabitants of the Area type, as not all *s are Ivory *s. +class IvoryArea (a :: Area *) where + ivoryArea :: Proxy a -> I.Type + +instance (SingI len, IvoryArea area) => IvoryArea (Array len area) where + ivoryArea _ = I.TyArr len area + where + len = fromInteger (fromTypeNat (sing :: Sing len)) + area = ivoryArea (Proxy :: Proxy area) + +instance IvoryType a => IvoryArea (Stored a) where + ivoryArea _ = ivoryType (Proxy :: Proxy a) + diff --git a/src/Ivory/Language/Array.hs b/src/Ivory/Language/Array.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Array.hs @@ -0,0 +1,101 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Ivory.Language.Array where + +import Ivory.Language.IBool +import Ivory.Language.Area +import Ivory.Language.Proxy +import Ivory.Language.Ref +import Ivory.Language.Sint +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + +import GHC.TypeLits (SingI(..),Sing,Nat) + + +-- Arrays ---------------------------------------------------------------------- + +-- Note: it is assumed in ivory-opts and the ivory-backend that the associated +-- type is an Sint32, so this should not be changed in the front-end without +-- modifying the other packages. +type IxRep = Sint32 + +-- | Values in the range @0 .. n-1@. +newtype Ix (n :: Nat) = Ix { getIx :: I.Expr } + +instance (SingI n) => IvoryType (Ix n) where + ivoryType _ = ivoryType (Proxy :: Proxy IxRep) + +instance (SingI n) => IvoryVar (Ix n) where + wrapVar = wrapVarExpr + unwrapExpr = getIx + +instance (SingI n) => IvoryExpr (Ix n) where + wrapExpr = Ix + +instance (SingI n) => IvoryStore (Ix n) + +instance (SingI n) => Num (Ix n) where + (*) = ixBinop (*) + (-) = ixBinop (-) + (+) = ixBinop (+) + abs = ixUnary abs + signum = ixUnary signum + fromInteger = mkIx . fromInteger + +instance (SingI n) => IvoryEq (Ix n) +instance (SingI n) => IvoryOrd (Ix n) + +fromIx :: SingI n => Ix n -> IxRep +fromIx = wrapExpr . unwrapExpr + +-- | Casting from a bounded Ivory expression to an index. This is safe, +-- although the value may be truncated. Furthermore, indexes are always +-- positive. +toIx :: (IvoryExpr a, Bounded a, SingI n) => a -> Ix n +toIx = mkIx . unwrapExpr + +-- | The number of elements that an index covers. +ixSize :: forall n. (SingI n) => Ix n -> Integer +ixSize _ = fromTypeNat (sing :: Sing n) + +arrayLen :: forall s len area n ref. + (Num n, SingI len, IvoryArea area, IvoryRef ref) + => ref s (Array len area) -> n +arrayLen _ = fromInteger (fromTypeNat (sing :: Sing len)) + +-- | Array indexing. +(!) :: forall s len area ref. + ( SingI len, IvoryArea area, IvoryRef ref + , IvoryExpr (ref s (Array len area)), IvoryExpr (ref s area)) + => ref s (Array len area) -> Ix len -> ref s area +arr ! ix = wrapExpr (I.ExpIndex ty (unwrapExpr arr) ixRep (getIx ix)) + where + ty = ivoryArea (Proxy :: Proxy (Array len area)) + ixRep = ivoryType (Proxy :: Proxy IxRep) + +-- XXX don't export +mkIx :: forall n. (SingI n) => I.Expr -> Ix n +mkIx e = wrapExpr (I.ExpToIx e base) + where + base = ixSize (undefined :: Ix n) + +-- XXX don't export +ixBinop :: (SingI n) + => (I.Expr -> I.Expr -> I.Expr) + -> (Ix n -> Ix n -> Ix n) +ixBinop f x y = mkIx $ f (rawIxVal x) (rawIxVal y) + +-- XXX don't export +ixUnary :: (SingI n) => (I.Expr -> I.Expr) -> (Ix n -> Ix n) +ixUnary f = mkIx . f . rawIxVal + +-- XXX don't export +rawIxVal :: SingI n => Ix n -> I.Expr +rawIxVal n = case unwrapExpr n of + I.ExpToIx e _ -> e + e@(I.ExpVar _) -> e + e -> error $ "Front-end: can't unwrap ixVal: " + ++ show e diff --git a/src/Ivory/Language/Assert.hs b/src/Ivory/Language/Assert.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Assert.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +module Ivory.Language.Assert where + +import Ivory.Language.Monad +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as AST + +assert :: forall a eff. IvoryExpr a => a -> Ivory eff () +assert e = emit (AST.Assert (unwrapExpr e)) + +compilerAssert :: forall a eff. IvoryExpr a => a -> Ivory eff () +compilerAssert e = emit (AST.CompilerAssert (unwrapExpr e)) + +assume :: forall a eff. IvoryExpr a => a -> Ivory eff () +assume e = emit (AST.Assume (unwrapExpr e)) + diff --git a/src/Ivory/Language/Bits.hs b/src/Ivory/Language/Bits.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Bits.hs @@ -0,0 +1,114 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE FlexibleContexts #-} + +module Ivory.Language.Bits where + +import Ivory.Language.Type +import Ivory.Language.Uint +import Ivory.Language.Cast + +import qualified Ivory.Language.Syntax as AST + +-- XXX do not export +bitOp :: forall a. IvoryExpr a => AST.ExpOp -> a -> a -> a +bitOp op a b = wrapExpr (AST.ExpOp op [unwrapExpr a, unwrapExpr b]) + +class (Num a, IvoryExpr a) => IvoryBits a where + (.&) :: a -> a -> a + (.&) = bitOp AST.ExpBitAnd + + (.|) :: a -> a -> a + (.|) = bitOp AST.ExpBitOr + + (.^) :: a -> a -> a + (.^) = bitOp AST.ExpBitXor + + iComplement :: a -> a + iComplement a = wrapExpr (AST.ExpOp AST.ExpBitComplement [unwrapExpr a]) + + -- XXX what should the type of the shift count argument be? having + -- it be polymorphic is kind of a pain. for now, just have it be + -- the same type as the value being shifted. + iShiftL :: a -> a -> a + iShiftL = bitOp AST.ExpBitShiftL + + iShiftR :: a -> a -> a + iShiftR = bitOp AST.ExpBitShiftR + +instance IvoryBits Uint8 +instance IvoryBits Uint16 +instance IvoryBits Uint32 +instance IvoryBits Uint64 + +-- | Extraction of the upper or lower half of a bit type into the next +-- smallest bit type. +class (IvoryBits a, IvoryBits b) => BitSplit a b | a -> b where + ubits :: a -> b + lbits :: a -> b + +instance BitSplit Uint64 Uint32 where + ubits x = ivoryCast ((x `iShiftR` 32) .& 0xffffffff) + lbits x = ivoryCast (x .& 0xffffffff) + +instance BitSplit Uint32 Uint16 where + ubits x = ivoryCast ((x `iShiftR` 16) .& 0xffff) + lbits x = ivoryCast (x .& 0xffff) + +instance BitSplit Uint16 Uint8 where + ubits x = ivoryCast ((x `iShiftR` 8) .& 0xff) + lbits x = ivoryCast (x .& 0xff) + +-- | A narrowing cast from one bit type to another. This explicitly +-- discards the upper bits of the input value to return a smaller +-- type, and is only defined for unsigned integers. +class (IvoryBits a, IvoryBits b) => BitCast a b where + bitCast :: a -> b + +-- Uint64: +instance BitCast Uint64 Uint64 where + bitCast = id + +instance BitCast Uint64 Uint32 where + bitCast = lbits + +instance BitCast Uint64 Uint16 where + bitCast = lbits . lbits + +instance BitCast Uint64 Uint8 where + bitCast = lbits . lbits . lbits + +-- Uint32: +instance BitCast Uint32 Uint32 where + bitCast = id + +instance BitCast Uint32 Uint16 where + bitCast = lbits + +instance BitCast Uint32 Uint8 where + bitCast = lbits . lbits + +-- Uint16: +instance BitCast Uint16 Uint16 where + bitCast = id + +instance BitCast Uint16 Uint8 where + bitCast = lbits + +-- Uint8: +instance BitCast Uint8 Uint8 where + bitCast = id + +-- | Extract the least significant byte from an integer. This returns +-- the two values (x & 0xFF, x >> 8), with the first value safely +-- casted to an 8-bit integer. +-- +-- This is convenient to use with a state monad and "sets", such as: +-- +-- > fst $ runState x $ do +-- > a <- sets extractByte +-- > b <- sets extractByte +-- > return (a, b) +extractByte :: (BitCast a Uint8) => a -> (Uint8, a) +extractByte x = (bitCast x, x `iShiftR` 8) diff --git a/src/Ivory/Language/BoundedInteger.hs b/src/Ivory/Language/BoundedInteger.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/BoundedInteger.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +module Ivory.Language.BoundedInteger where + +import Text.Printf + +import Ivory.Language.Proxy +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + +-------------------------------------------------------------------------------- + +-- | It is an error if a constant implicitly underflows/overflows. +boundedFromInteger :: forall a b . (Num a, IvoryType a, Bounded b, Integral b) + => (I.Expr -> a) -> b -> Integer -> a +boundedFromInteger constr _ i = + if i > snd bounds + then error $ printf "The constant %d is too large to cast to type %s." i tyStr + else if i < fst bounds + then error $ printf "The constant %d is too small to cast to type %s." i tyStr + else constr (fromInteger i) + where + ty = ivoryType (Proxy :: Proxy a) + tyStr = show ty + bounds = (fromIntegral (minBound :: b), fromIntegral (maxBound :: b)) diff --git a/src/Ivory/Language/CArray.hs b/src/Ivory/Language/CArray.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/CArray.hs @@ -0,0 +1,42 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} + +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +module Ivory.Language.CArray where + +import Ivory.Language.Area +import Ivory.Language.Proxy +import Ivory.Language.Ref +import Ivory.Language.Struct +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + +import GHC.TypeLits (SingI) + + +instance IvoryArea a => IvoryArea (CArray a) where + ivoryArea _ = I.TyCArray (ivoryArea (Proxy :: Proxy a)) + + +-- | Guard invocations of toCArray. +class (IvoryArea area, IvoryArea rep) + => ToCArray (area :: Area *) (rep :: Area *) | area -> rep + +instance (SingI len, ToCArray area rep) + => ToCArray (Array len area) (CArray rep) +instance IvoryType a => ToCArray (Stored a) (Stored a) +instance IvoryStruct sym => ToCArray (Struct sym) (Struct sym) + +-- | Convert from a checked array to one that can be given to a c function. +toCArray :: forall s len area rep ref. + ( SingI len, ToCArray area rep, IvoryRef ref + , IvoryExpr (ref s (Array len area)) + , IvoryExpr (ref s (CArray rep))) + => ref s (Array len area) -> ref s (CArray rep) +toCArray ref = wrapExpr $ I.ExpSafeCast ty (unwrapExpr ref) + where ty = ivoryType (Proxy :: Proxy (ref s (CArray rep))) diff --git a/src/Ivory/Language/Cast.hs b/src/Ivory/Language/Cast.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Cast.hs @@ -0,0 +1,320 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverlappingInstances #-} + +-- Needed to check (SafeCast to from) in the instance constraints for +-- RuntimeCast. +{-# LANGUAGE UndecidableInstances #-} + +-- | Safe casting. We assume Floats have 32 bits and Doubles have 64. + +module Ivory.Language.Cast + ( safeCast + , ivoryCast -- do not export from "Ivory.Language" + , castWith + , castDefault + , signCast + , SafeCast(), RuntimeCast(), Default(), SignCast() + , toMaxSize + , toMinSize + ) where + +import Ivory.Language.Array +import Ivory.Language.Float +import Ivory.Language.IBool +import Ivory.Language.IChar +import Ivory.Language.IIntegral +import Ivory.Language.Proxy +import Ivory.Language.Sint +import Ivory.Language.Type +import Ivory.Language.Uint +import qualified Ivory.Language.Syntax as AST + +import GHC.TypeLits (SingI(..)) + +import Data.Word +import Data.Int + +-------------------------------------------------------------------------------- +-- Interface functions and methods. + +-- | Statically safe casts. +class (IvoryExpr from, IvoryExpr to) => SafeCast from to where + safeCast :: from -> to + safeCast = ivoryCast + +-- | Cast with a default value if the casted value is too large. +castWith :: RuntimeCast from to => to -> from -> to +castWith deflt from = inBounds deflt from ? (ivoryCast from, deflt) + +-- | `CastWith 0` for types for which 0 is defined. +castDefault :: (Default to, RuntimeCast from to) => from -> to +castDefault = castWith defaultVal + +-- | SignCast takes a unsigned number into its signed form iff safe, +-- otherwise 0, and same with signed into unsigned +class (IvoryExpr from, IvoryExpr to) => SignCast from to where + signCast :: from -> to + +-- | upperBoundCast implements signCast from unsigned to signed integers +upperBoundCast :: forall from to + . (IvoryOrd from, IvoryExpr from, IvoryExpr to, Num to, Bounded to) + => from -> to +upperBoundCast f = (f <=? bound) ? (ivoryCast f, 0) + where bound = ivoryCast (maxBound :: to) + +-- | lowerBoundCast implements signCast from signed to unsigned integers +lowerBoundCast :: forall from to + . (IvoryOrd from, IvoryExpr from, IvoryExpr to, Num to, Bounded to) + => from -> to +lowerBoundCast f = (f >? bound) ? (ivoryCast f, 0) + where bound = ivoryCast (minBound :: to) +-------------------------------------------------------------------------------- + +-- | Casts requiring runtime checks. +class (IvoryExpr from, IvoryExpr to, Default to) => RuntimeCast from to where + -- Does the from value fit within the to type? + inBounds :: to -> from -> IBool + +-------------------------------------------------------------------------------- +-- Statically safe instances. + +-- Booleans. +instance SafeCast IBool IBool where + safeCast = id +instance SafeCast IBool IChar +instance SafeCast IBool Uint8 +instance SafeCast IBool Uint16 +instance SafeCast IBool Uint32 +instance SafeCast IBool Uint64 +instance SafeCast IBool Sint8 +instance SafeCast IBool Sint16 +instance SafeCast IBool Sint32 +instance SafeCast IBool Sint64 +instance SafeCast IBool IFloat +instance SafeCast IBool IDouble + +-- Uint8. +instance SafeCast Uint8 Uint8 where + safeCast = id +instance SafeCast Uint8 Uint16 +instance SafeCast Uint8 Uint32 +instance SafeCast Uint8 Uint64 +instance SafeCast Uint8 Sint16 +instance SafeCast Uint8 Sint32 +instance SafeCast Uint8 Sint64 +instance SafeCast Uint8 IFloat +instance SafeCast Uint8 IDouble +instance SignCast Uint8 Sint8 where + signCast = upperBoundCast + +-- Uint16. +instance SafeCast Uint16 Uint16 where + safeCast = id +instance SafeCast Uint16 Uint32 +instance SafeCast Uint16 Uint64 +instance SafeCast Uint16 Sint32 +instance SafeCast Uint16 Sint64 +instance SafeCast Uint16 IFloat +instance SafeCast Uint16 IDouble +instance SignCast Uint16 Sint16 where + signCast = upperBoundCast + +-- Uint32. +instance SafeCast Uint32 Uint32 where + safeCast = id +instance SafeCast Uint32 Uint64 +instance SafeCast Uint32 Sint64 +instance SafeCast Uint32 IFloat +instance SafeCast Uint32 IDouble +instance SignCast Uint32 Sint32 where + signCast = upperBoundCast + +-- Uint64. +instance SafeCast Uint64 Uint64 where + safeCast = id +instance SafeCast Uint64 IDouble +instance SignCast Uint64 Sint64 where + signCast = upperBoundCast + +-- Sint8. +instance SafeCast Sint8 Sint8 where + safeCast = id +instance SafeCast Sint8 Sint16 +instance SafeCast Sint8 Sint32 +instance SafeCast Sint8 Sint64 +instance SafeCast Sint8 IFloat +instance SafeCast Sint8 IDouble +instance SignCast Sint8 Uint8 where + signCast = lowerBoundCast + +-- Sint16. +instance SafeCast Sint16 Sint16 where + safeCast = id +instance SafeCast Sint16 Sint32 +instance SafeCast Sint16 Sint64 +instance SafeCast Sint16 IFloat +instance SafeCast Sint16 IDouble +instance SignCast Sint16 Uint16 where + signCast = lowerBoundCast + +-- Sint32. +instance SafeCast Sint32 Sint32 where + safeCast = id +instance SafeCast Sint32 Sint64 +instance SafeCast Sint32 IFloat +instance SafeCast Sint32 IDouble +instance SignCast Sint32 Uint32 where + signCast = lowerBoundCast + +-- Sint64. +instance SafeCast Sint64 Sint64 where + safeCast = id +instance SafeCast Sint64 IDouble +instance SignCast Sint64 Uint64 where + signCast = lowerBoundCast + +-- IFloat. +instance SafeCast IFloat IFloat where + safeCast = id +instance SafeCast IFloat IDouble + +-- IDouble. +instance SafeCast IDouble IDouble where + safeCast = id + +-- IChar. +instance SafeCast IChar IChar where + safeCast = id + +-- By the C standard, we can't assume they're unsigned or how big they are (we +-- just know they're at least 8 bits). So this is the only cast for Char. + +-------------------------------------------------------------------------------- +-- Runtime check instances. + +-- All other casts, for going to a Num type. +instance ( Bounded from, Bounded to + , IvoryOrd from, IvoryOrd to + , IvoryExpr from, IvoryExpr to + , Default from, Default to + -- Important constraint! This means we can compare the values in the + -- `from` type, since it must be able to hold all the values of the + -- `to` type. Alas, it requires undeciable instances.... + , SafeCast to from + ) => RuntimeCast from to where + + -- We can assume that comparison in the `from` type is safe due to the above + -- constraint. + inBounds = boundPred + +-------------------------------------------------------------------------------- +-- | Default values for expression types. +class Default a where + defaultVal :: a + +instance Default Uint8 where defaultVal = 0 +instance Default Uint16 where defaultVal = 0 +instance Default Uint32 where defaultVal = 0 +instance Default Uint64 where defaultVal = 0 +instance Default Sint8 where defaultVal = 0 +instance Default Sint16 where defaultVal = 0 +instance Default Sint32 where defaultVal = 0 +instance Default Sint64 where defaultVal = 0 + +instance Default IFloat where defaultVal = 0 +instance Default IDouble where defaultVal = 0 + +-------------------------------------------------------------------------------- +-- Indexes. + +instance ( SingI n, IvoryIntegral to, Default to + ) => SafeCast (Ix n) to where + safeCast ix | Just s <- toMaxSize (ivoryType (Proxy :: Proxy to)) + , ixSize ix <= s + = ivoryCast (fromIx ix) + | otherwise + = error ixCastError + -- -- It doesn't make sense to case an index downwards dynamically. + -- inBounds _ _ = error ixCastError + +ixCastError :: String +ixCastError = "Idx cast : cannot cast index: result type is too small." + +-------------------------------------------------------------------------------- +-- Floating + +-- Have to define instances for Float and Double separately or you'll get +-- overlapping instances. + +-- | Casting from a floating to a `Integral` type always results in truncation. +instance ( Default to + , Bounded to + , IvoryIntegral to + -- Important constraint! This means we can compare the values in the + -- `from` type, since it must be able to hold all the values of the + -- `to` type. Alas, it requires undeciable instances.... + , SafeCast to IFloat + ) => RuntimeCast IFloat to where + inBounds to from = iNot (isnan from) .&& boundPred to from + +instance ( Default to + , Bounded to + , IvoryIntegral to + -- Important constraint! This means we can compare the values in the + -- `from` type, since it must be able to hold all the values of the + -- `to` type. Alas, it requires undeciable instances.... + , SafeCast to IDouble + ) => RuntimeCast IDouble to where + inBounds to from = iNot (isnan from) .&& boundPred to from + +-------------------------------------------------------------------------------- +-- Utils. + +boundPred :: forall from to . + ( IvoryExpr from + , IvoryExpr to + , Bounded to + , IvoryOrd from + ) => to -> from -> IBool +boundPred _ from = (from <=? ivoryCast (maxBound :: to)) + .&& (from >=? ivoryCast (minBound :: to)) + +-- XXX Don't export. +-- Type is what we're casting from. +ivoryCast :: forall a b. (IvoryExpr a, IvoryExpr b) => a -> b +ivoryCast x = wrapExpr (AST.ExpSafeCast ty (unwrapExpr x)) + where ty = ivoryType (Proxy :: Proxy a) + +toMaxSize :: AST.Type -> Maybe Integer +toMaxSize ty = + case ty of + AST.TyInt i -> Just $ case i of + AST.Int8 -> fromIntegral (maxBound :: Int8) + AST.Int16 -> fromIntegral (maxBound :: Int16) + AST.Int32 -> fromIntegral (maxBound :: Int32) + AST.Int64 -> fromIntegral (maxBound :: Int64) + AST.TyWord w -> Just $ case w of + AST.Word8 -> fromIntegral (maxBound :: Word8) + AST.Word16 -> fromIntegral (maxBound :: Word16) + AST.Word32 -> fromIntegral (maxBound :: Word32) + AST.Word64 -> fromIntegral (maxBound :: Word64) + _ -> Nothing + +toMinSize :: AST.Type -> Maybe Integer +toMinSize ty = + case ty of + AST.TyInt i -> Just $ case i of + AST.Int8 -> fromIntegral (minBound :: Int8) + AST.Int16 -> fromIntegral (minBound :: Int16) + AST.Int32 -> fromIntegral (minBound :: Int32) + AST.Int64 -> fromIntegral (minBound :: Int64) + AST.TyWord w -> Just $ case w of + AST.Word8 -> fromIntegral (minBound :: Word8) + AST.Word16 -> fromIntegral (minBound :: Word16) + AST.Word32 -> fromIntegral (minBound :: Word32) + AST.Word64 -> fromIntegral (minBound :: Word64) + _ -> Nothing + +-------------------------------------------------------------------------------- diff --git a/src/Ivory/Language/Cond.hs b/src/Ivory/Language/Cond.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Cond.hs @@ -0,0 +1,92 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} + +module Ivory.Language.Cond where + +import Ivory.Language.Area +import Ivory.Language.IBool +import Ivory.Language.Monad +import Ivory.Language.Proc +import Ivory.Language.Proxy +import Ivory.Language.Ref +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I +import Data.Monoid(Monoid(..)) + +-- Effects --------------------------------------------------------------------- + +-- | Emit a pre-condition. +-- +-- XXX do not export +emitPreCond :: I.Require -> Ivory eff () +emitPreCond r = emits mempty { blockRequires = [r] } + +-- | Emit a post-condition. +-- +-- XXX do not export +emitPostCond :: I.Ensure -> Ivory eff () +emitPostCond e = emits mempty { blockEnsures = [e] } + +-- Condition Notation ---------------------------------------------------------- + +newtype Cond = Cond + { runCond :: forall eff. Ivory eff I.Cond + -- ^ Use the naming environment from the Ivory monad. + } + +-- | Checkable a boolean expression. +check :: IBool -> Cond +check bool = Cond (return (I.CondBool (unwrapExpr bool))) + +checkStored :: forall ref s a. + (IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) + => ref s (Stored a) -> (a -> IBool) -> Cond +checkStored ref prop = Cond $ do + n <- freshVar "pre" + let ty = ivoryType (Proxy :: Proxy a) + b <- runCond $ check $ prop $ wrapVar n + return (I.CondDeref ty (unwrapExpr ref) n b) + +-- Pre-Conditions -------------------------------------------------------------- + +-- | Proc bodies that have pre-conditions. Multiple pre-conditions may be +-- provided, for which the conjunction must hold. +class Requires c where + requires :: IvoryType r => c -> Body r -> Body r + +-- XXX Do not export +requires' :: (Requires c, IvoryType r) => (c -> Cond) -> c -> Body r -> Body r +requires' chk prop b = Body $ do + req <- runCond $ chk $ prop + emitPreCond (I.Require req) + runBody b + +instance Requires IBool where + requires = requires' check + +instance Requires Cond where + requires = requires' id + +-- Post-Conditions ------------------------------------------------------------- + +-- | Proc bodies that have post-conditions. Multiple post-conditions may be +-- provided, for which the conjunction must hold. +class Ensures c where + ensures :: IvoryVar r => (r -> c) -> Body r -> Body r + +-- XXX Do not export +ensures' :: (Ensures c, IvoryVar r) + => (c -> Cond) -> (r -> c) -> Body r -> Body r +ensures' chk prop b = Body $ do + c <- runCond $ chk $ prop $ wrapVar I.retval + emitPostCond (I.Ensure c) + runBody b + +instance Ensures IBool where + ensures = ensures' check + +instance Ensures Cond where + ensures = ensures' id diff --git a/src/Ivory/Language/Const.hs b/src/Ivory/Language/Const.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Const.hs @@ -0,0 +1,10 @@ +module Ivory.Language.Const where + +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as AST + +-- Extern constants ------------------------------------------------------------ + +-- | Import and externally defined constant by providing a global name. +extern :: IvoryExpr t => AST.Sym -> t +extern = wrapExpr . AST.ExpSym diff --git a/src/Ivory/Language/Effects.hs b/src/Ivory/Language/Effects.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Effects.hs @@ -0,0 +1,88 @@ +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ExistentialQuantification #-} + +module Ivory.Language.Effects + ( Effects(..) + , AllocEffects + , ProcEffects + , NoEffects + + , ReturnEff(..) + , GetReturn() + , ClearReturn() + + , BreakEff(..) + , GetBreaks() + , AllowBreak() + , ClearBreak() + + , AllocEff(..) + , GetAlloc() + , ClearAlloc() + ) where + + +-------------------------------------------------------------------------------- +-- Effect Context + +-- | The effect context for 'Ivory' operations. +data Effects = Effects ReturnEff BreakEff AllocEff + +-- | Function return effect. +data ReturnEff = forall t. Returns t | NoReturn + +-- | Loop break effect. +data BreakEff = Break | NoBreak + +-- | Stack allocation effect. +data AllocEff = forall s. Scope s | NoAlloc + + +-------------------------------------------------------------------------------- +-- Returns + +-- | Retrieve any 'Return' effect present. +type family GetReturn (effs :: Effects) :: ReturnEff +type instance GetReturn ('Effects r b a) = r + +-- | Remove any 'Return' effects present. +type family ClearReturn (effs :: Effects) :: Effects +type instance ClearReturn ('Effects r b a) = 'Effects 'NoReturn b a + +-------------------------------------------------------------------------------- +-- Breaks + +-- | Retrieve any 'Breaks' effect present. +type family GetBreaks (effs :: Effects) :: BreakEff +type instance GetBreaks ('Effects r b a) = b + +-- | Add the 'Break' effect into an effect context. +type family AllowBreak (effs :: Effects) :: Effects +type instance AllowBreak ('Effects r b a) = 'Effects r 'Break a + +-- | Remove any 'Break' effect present. +type family ClearBreak (effs :: Effects) :: Effects +type instance ClearBreak ('Effects r b a) = 'Effects r 'NoBreak a + +-------------------------------------------------------------------------------- +-- Allocs + +-- | Retrieve the current allocation effect. +type family GetAlloc (effs :: Effects) :: AllocEff +type instance GetAlloc ('Effects r b a) = a + +-- | Remove any allocation effect currently present. +type family ClearAlloc (effs :: Effects) :: Effects +type instance ClearAlloc ('Effects r b a) = 'Effects r b 'NoAlloc + +-------------------------------------------------------------------------------- +-- Helpers + +type AllocEffects s = 'Effects 'NoReturn 'NoBreak (Scope s) +type ProcEffects s t = 'Effects (Returns t) 'NoBreak (Scope s) +type NoEffects = 'Effects 'NoReturn 'NoBreak 'NoAlloc + +-------------------------------------------------------------------------------- diff --git a/src/Ivory/Language/Float.hs b/src/Ivory/Language/Float.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Float.hs @@ -0,0 +1,169 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Ivory.Language.Float where + +import Ivory.Language.Area +import Ivory.Language.IBool +import Ivory.Language.Proxy +import Ivory.Language.Ref +import Ivory.Language.SizeOf +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + + +-- | NaN testing. +isnan :: forall a. (IvoryVar a, Floating a) => a -> IBool +isnan a = wrapExpr (I.ExpOp (I.ExpIsNan ty) [unwrapExpr a]) + where + ty = ivoryType (Proxy :: Proxy a) + +-- | Infinite testing. +isinf :: forall a. (IvoryVar a, Floating a) => a -> IBool +isinf a = wrapExpr (I.ExpOp (I.ExpIsInf ty) [unwrapExpr a]) + where + ty = ivoryType (Proxy :: Proxy a) + +-- Floating Point -------------------------------------------------------------- + +newtype IFloat = IFloat { getIFloat :: I.Expr } + +ifloat :: Float -> IFloat +ifloat = IFloat . I.ExpLit . I.LitFloat + +instance IvoryType IFloat where + ivoryType _ = I.TyFloat + +instance IvoryVar IFloat where + wrapVar = wrapVarExpr + unwrapExpr = getIFloat + +instance IvoryExpr IFloat where + wrapExpr = IFloat + +instance IvorySizeOf (Stored IFloat) where + sizeOfBytes _ = 4 + +instance IvoryEq IFloat + +instance IvoryOrd IFloat + +instance IvoryStore IFloat + +instance Num IFloat where + (*) = exprBinop (*) + (+) = exprBinop (+) + (-) = exprBinop (-) + abs = exprUnary abs + signum = exprUnary signum + negate = exprUnary negate + fromInteger = ifloat . fromInteger + +instance Fractional IFloat where + (/) = exprBinop (/) + recip = exprUnary recip + fromRational = ifloat . fromRational + +instance Floating IFloat where + pi = ifloat pi + exp = exprUnary exp + sqrt = exprUnary sqrt + log = exprUnary log + (**) = exprBinop (**) + logBase = exprBinop (logBase) + sin = exprUnary sin + tan = exprUnary tan + cos = exprUnary cos + asin = exprUnary asin + atan = exprUnary atan + acos = exprUnary acos + sinh = exprUnary sinh + tanh = exprUnary tanh + cosh = exprUnary cosh + asinh = exprUnary asinh + atanh = exprUnary atanh + acosh = exprUnary acosh + +-- Double Precision ------------------------------------------------------------ + +newtype IDouble = IDouble { getIDouble :: I.Expr } + +idouble :: Double -> IDouble +idouble = IDouble . I.ExpLit . I.LitDouble + +instance Fractional IDouble where + (/) = exprBinop (/) + recip = exprUnary recip + fromRational = idouble . fromRational + +instance IvoryType IDouble where + ivoryType _ = I.TyDouble + +instance IvoryVar IDouble where + wrapVar = wrapVarExpr + unwrapExpr = getIDouble + +instance IvoryExpr IDouble where + wrapExpr = IDouble + +instance IvorySizeOf (Stored IDouble) where + sizeOfBytes _ = 8 + +instance IvoryEq IDouble + +instance IvoryOrd IDouble + +instance IvoryStore IDouble + +instance Num IDouble where + (*) = exprBinop (*) + (+) = exprBinop (+) + (-) = exprBinop (-) + abs = exprUnary abs + signum = exprUnary signum + negate = exprUnary negate + fromInteger = idouble . fromInteger + +instance Floating IDouble where + pi = idouble pi + exp = exprUnary exp + sqrt = exprUnary sqrt + log = exprUnary log + (**) = exprBinop (**) + logBase = exprBinop (logBase) + sin = exprUnary sin + tan = exprUnary tan + cos = exprUnary cos + asin = exprUnary asin + atan = exprUnary atan + acos = exprUnary acos + sinh = exprUnary sinh + tanh = exprUnary tanh + cosh = exprUnary cosh + asinh = exprUnary asinh + atanh = exprUnary atanh + acosh = exprUnary acosh + + +-- Rounding -------------------------------------------------------------------- + +-- XXX do not export +primRound :: IvoryExpr a => I.ExpOp -> a -> a +primRound op a = wrapExpr (I.ExpOp op [unwrapExpr a]) + +class (Floating a, IvoryExpr a) => IvoryFloat a where + -- | Round a floating point number. + roundF :: a -> a + roundF = primRound I.ExpRoundF + + -- | Take the ceiling of a floating point number. + ceilF :: a -> a + ceilF = primRound I.ExpCeilF + + -- | Take the floor of a floating point number. + floorF :: a -> a + floorF = primRound I.ExpFloorF + +instance IvoryFloat IFloat +instance IvoryFloat IDouble diff --git a/src/Ivory/Language/IBool.hs b/src/Ivory/Language/IBool.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/IBool.hs @@ -0,0 +1,121 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +module Ivory.Language.IBool where + +import Ivory.Language.Monad +import Ivory.Language.Proxy +import Ivory.Language.Sint +import Ivory.Language.Type +import Ivory.Language.Uint +import qualified Ivory.Language.Syntax as AST + + +-- Booleans -------------------------------------------------------------------- + +newtype IBool = IBool { getIBool :: AST.Expr } + +instance IvoryType IBool where + ivoryType _ = AST.TyBool + +instance IvoryVar IBool where + wrapVar = wrapVarExpr + unwrapExpr = getIBool + +instance IvoryExpr IBool where + wrapExpr = IBool + +-- IfTE Support ---------------------------------------------------------------- + +-- | If-then-else. +ifte_ :: IBool -> Ivory eff a -> Ivory eff b -> Ivory eff () +ifte_ cmp t f = do + (_,tb) <- collect t + (_,fb) <- collect f + emit (AST.IfTE (unwrapExpr cmp) (blockStmts tb) (blockStmts fb)) + +-- | Conditional expressions. +(?) :: forall a. IvoryExpr a => IBool -> (a,a) -> a +cond ? (t,f) = wrapExpr + $ AST.ExpOp AST.ExpCond [unwrapExpr cond,unwrapExpr t,unwrapExpr f] + + +-- Constants ------------------------------------------------------------------- + +true :: IBool +true = wrapExpr (AST.ExpLit (AST.LitBool True)) + +false :: IBool +false = wrapExpr (AST.ExpLit (AST.LitBool False)) + + +-- Comparisons ----------------------------------------------------------------- + +-- XXX do not export +boolOp :: forall a. IvoryVar a => (AST.Type -> AST.ExpOp) -> a -> a -> IBool +boolOp op a b = wrapExpr (AST.ExpOp (op ty) [unwrapExpr a,unwrapExpr b]) + where + ty = ivoryType (Proxy :: Proxy a) + +class IvoryExpr a => IvoryEq a where + (==?) :: a -> a -> IBool + (==?) = boolOp AST.ExpEq + infix 4 ==? + + (/=?) :: a -> a -> IBool + (/=?) = boolOp AST.ExpNeq + infix 4 /=? + +class IvoryEq a => IvoryOrd a where + (>?) :: a -> a -> IBool + (>?) = boolOp (AST.ExpGt False) + infix 4 >? + + (>=?) :: a -> a -> IBool + (>=?) = boolOp (AST.ExpGt True) + infix 4 >=? + + ( a -> IBool + ( a -> IBool + (<=?) = boolOp (AST.ExpLt True) + infix 4 <=? + +instance IvoryEq IBool +instance IvoryOrd IBool + +instance IvoryEq Uint8 +instance IvoryOrd Uint8 +instance IvoryEq Uint16 +instance IvoryOrd Uint16 +instance IvoryEq Uint32 +instance IvoryOrd Uint32 +instance IvoryEq Uint64 +instance IvoryOrd Uint64 + +instance IvoryEq Sint8 +instance IvoryOrd Sint8 +instance IvoryEq Sint16 +instance IvoryOrd Sint16 +instance IvoryEq Sint32 +instance IvoryOrd Sint32 +instance IvoryEq Sint64 +instance IvoryOrd Sint64 + +-- Boolean logic --------------------------------------------------------------- + +iNot :: IBool -> IBool +iNot a = wrapExpr (AST.ExpOp AST.ExpNot [unwrapExpr a]) + +(.&&) :: IBool -> IBool -> IBool +l .&& r = wrapExpr (AST.ExpOp AST.ExpAnd [unwrapExpr l,unwrapExpr r]) +infixr 3 .&& + +(.||) :: IBool -> IBool -> IBool +l .|| r = wrapExpr (AST.ExpOp AST.ExpOr [unwrapExpr l,unwrapExpr r]) +infixr 2 .|| diff --git a/src/Ivory/Language/IChar.hs b/src/Ivory/Language/IChar.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/IChar.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} + +module Ivory.Language.IChar where + +import Ivory.Language.Area +import Ivory.Language.SizeOf +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + + +-- Characters ------------------------------------------------------------------ + +newtype IChar = IChar { getIChar :: I.Expr } + +char :: Char -> IChar +char = wrapExpr . I.ExpLit . I.LitChar + +instance IvoryType IChar where + ivoryType _ = I.TyChar + +instance IvoryVar IChar where + wrapVar = wrapVarExpr + unwrapExpr = getIChar + +instance IvoryExpr IChar where + wrapExpr = IChar + +instance IvorySizeOf (Stored IChar) where + sizeOfBytes _ = 1 diff --git a/src/Ivory/Language/IIntegral.hs b/src/Ivory/Language/IIntegral.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/IIntegral.hs @@ -0,0 +1,40 @@ +module Ivory.Language.IIntegral where + +import Ivory.Language.Sint +import Ivory.Language.Type +import Ivory.Language.Uint +import qualified Ivory.Language.Syntax.AST as I + +-------------------------------------------------------------------------------- + +-- | Integral, without the baggage from Haskell (i.e., supertypes of 'Real' and +-- 'Enum'). +class (IvoryExpr a, Num a) => IvoryIntegral a where + -- | Has C semantics: like Haskell's `quot` (truncate towards 0). + iDiv :: a -> a -> a + iDiv l r = wrapExpr (iDivE (unwrapExpr l) (unwrapExpr r)) + + -- | Has C semantics: like Haskell's `rem`. + (.%) :: a -> a -> a + l .% r = wrapExpr (iModE (unwrapExpr l) (unwrapExpr r)) + +-- | Has C semantics: like Haskell's `quot` (truncate towards 0). +iDivE :: I.Expr -> I.Expr -> I.Expr +iDivE l r = I.ExpOp I.ExpDiv [l,r] + +-- | Has C semantics: like Haskell's `rem`. +iModE :: I.Expr -> I.Expr -> I.Expr +iModE l r = I.ExpOp I.ExpMod [l,r] + +-------------------------------------------------------------------------------- + +instance IvoryIntegral Sint8 +instance IvoryIntegral Sint16 +instance IvoryIntegral Sint32 +instance IvoryIntegral Sint64 +instance IvoryIntegral Uint8 +instance IvoryIntegral Uint16 +instance IvoryIntegral Uint32 +instance IvoryIntegral Uint64 + +-------------------------------------------------------------------------------- diff --git a/src/Ivory/Language/IString.hs b/src/Ivory/Language/IString.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/IString.hs @@ -0,0 +1,22 @@ +module Ivory.Language.IString where + +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as AST + +import Data.String (IsString(..)) + + +newtype IString = IString { getIString :: AST.Expr } + +instance IvoryType IString where + ivoryType _ = AST.TyPtr AST.TyChar + +instance IvoryVar IString where + wrapVar = wrapVarExpr + unwrapExpr = getIString + +instance IvoryExpr IString where + wrapExpr = IString + +instance IsString IString where + fromString str = wrapExpr $ AST.ExpLit $ AST.LitString str diff --git a/src/Ivory/Language/Init.hs b/src/Ivory/Language/Init.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Init.hs @@ -0,0 +1,207 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE OverlappingInstances #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} + +module Ivory.Language.Init where + +import Ivory.Language.Area +import Ivory.Language.Array +import Ivory.Language.Float +import Ivory.Language.IBool +import Ivory.Language.IChar +import Ivory.Language.Monad +import Ivory.Language.Proc +import Ivory.Language.Proxy +import Ivory.Language.Ptr +import Ivory.Language.Ref +import Ivory.Language.Scope +import Ivory.Language.Struct +import Ivory.Language.Sint +import Ivory.Language.Type +import Ivory.Language.Uint +import qualified Ivory.Language.Syntax as I +import qualified Ivory.Language.Effects as E + +import Control.Monad (forM_) +import Data.Monoid (Monoid(..),mconcat) +import GHC.TypeLits + +-- Initializers ---------------------------------------------------------------- + +-- | Intermediate initializer type supporting compound initializers. +-- The "IFresh" nodes are flattened into multiple "I.Init" nodes +-- in a "FreshName" monad when the variable is allocated. +data XInit + = IVal I.Type I.Init + | IArray I.Type [XInit] + | IStruct I.Type [(String, XInit)] + | IFresh I.Type XInit (I.Var -> I.Init) + +-- | Return the type of the initializer. +initType :: XInit -> I.Type +initType (IVal ty _) = ty +initType (IArray ty _) = ty +initType (IStruct ty _) = ty +initType (IFresh ty _ _) = ty + +newtype Init (area :: Area *) = Init { getInit :: XInit } + +-- | Zero initializers. +class IvoryZero (area :: Area *) where + izero :: Init area + +-- Running Initializers -------------------------------------------------------- + +class Monad m => FreshName m where + freshName :: String -> m I.Var + +instance FreshName (Ivory eff) where + freshName = freshVar + +-- | A variable binding (on the stack or in a memory area). +data Binding = Binding + { bindingVar :: I.Var + , bindingType :: I.Type + , bindingInit :: I.Init + } deriving Show + +-- XXX do not export +bindingSym :: Binding -> I.Sym +bindingSym b = + case bindingVar b of + I.VarName s -> s + I.VarInternal s -> s + I.VarLitName s -> s + +-- | Return the initializer and auxillary bindings for an +-- initializer in a context that can allocate fresh names. +runInit :: FreshName m => XInit -> m (I.Init, [Binding]) +runInit ini = + case ini of + IVal _ i -> + return (i, []) + IArray _ is -> do + binds <- mapM runInit is + let inis = map fst binds + let aux = concatMap snd binds + return (I.InitArray inis, aux) + IStruct _ is -> do + binds <- mapM iniStruct is + let inis = map fst binds + let aux = concatMap snd binds + return (I.InitStruct inis, aux) + IFresh _ i f -> do + var <- freshName "init" + (i', aux) <- runInit i + let ty = initType i + let aux' = aux ++ [Binding var ty i'] + return (f var, aux') + where + iniStruct (s, i) = do + (i', binds) <- runInit i + return ((s, i'), binds) + +-- Stored Initializers --------------------------------------------------------- + +-- | Initializers for 'Stored' things. +class IvoryVar e => IvoryInit e where + ival :: e -> Init (Stored e) + ival e = Init (IVal ty (I.InitExpr ty (unwrapExpr e))) + where + ty = ivoryType (Proxy :: Proxy e) + +instance IvoryInit IBool +instance IvoryInit IChar +instance IvoryInit Uint8 +instance IvoryInit Uint16 +instance IvoryInit Uint32 +instance IvoryInit Uint64 +instance IvoryInit Sint8 +instance IvoryInit Sint16 +instance IvoryInit Sint32 +instance IvoryInit Sint64 +instance IvoryInit IFloat +instance IvoryInit IDouble +instance ProcType proc => IvoryInit (ProcPtr proc) +instance IvoryArea area => IvoryInit (Ptr Global area) +instance SingI len => IvoryInit (Ix len) + +instance IvoryZero (Stored IBool) where + izero = ival false + +instance IvoryZero (Stored IChar) where + izero = ival (char '\0') + +instance IvoryArea area => IvoryZero (Stored (Ptr Global area)) where + izero = ival nullPtr + +-- catch-all case for numeric things +instance (Num a, IvoryInit a) => IvoryZero (Stored a) where + izero = ival 0 + +-- Array Initializers ---------------------------------------------------------- + +instance (IvoryZero area, IvoryArea area, SingI len) => + IvoryZero (Array len area) where + izero = Init (IVal ty I.InitZero) + where + ty = ivoryArea (Proxy :: Proxy (Array len area)) + +iarray :: forall len area. (IvoryArea area, SingI len) + => [Init area] -> Init (Array len area) +iarray is = Init (IArray ty (take len (map getInit is))) + -- truncate to known length + where + len = fromInteger (fromTypeNat (sing :: Sing len)) + ty = ivoryArea (Proxy :: Proxy (Array len area)) + +-- Struct Initializers --------------------------------------------------------- + +instance IvoryStruct sym => IvoryZero (Struct sym) where + izero = Init (IVal ty I.InitZero) + where + ty = ivoryArea (Proxy :: Proxy (Struct sym)) + +newtype InitStruct (sym :: Symbol) = InitStruct + { getInitStruct :: [(String, XInit)] + } + +-- Much like the C initializers, the furthest right field initializer will take +-- precidence, and fields not mentioned will be left as zero. +instance IvoryStruct sym => Monoid (InitStruct sym) where + mempty = InitStruct [] + mappend l r = InitStruct (mappend (getInitStruct l) (getInitStruct r)) + +istruct :: forall sym. IvoryStruct sym => [InitStruct sym] -> Init (Struct sym) +istruct is = Init (IStruct ty fields) + where + fields = [ (l,i) | (l,i) <- getInitStruct (mconcat is) ] + ty = ivoryArea (Proxy :: Proxy (Struct sym)) + +(.=) :: Label sym area -> Init area -> InitStruct sym +l .= ini = InitStruct [(getLabel l, getInit ini)] + +-- | Stack allocation +local :: forall eff s area. (IvoryArea area, E.GetAlloc eff ~ E.Scope s) + => Init area + -> Ivory eff (Ref (Stack s) area) +local ini = do + (i, binds) <- runInit (getInit ini) + + forM_ binds $ \b -> do + emit (I.Local (bindingType b) (bindingVar b) (bindingInit b)) + + lname <- freshVar "local" + let ty = ivoryArea (Proxy :: Proxy area) + emit (I.Local ty lname i) + + rname <- freshVar "ref" + let areaTy = ivoryArea (Proxy :: Proxy area) + emit (I.AllocRef areaTy rname (I.NameVar lname)) + + return (wrapExpr (I.ExpVar rname)) diff --git a/src/Ivory/Language/Loop.hs b/src/Ivory/Language/Loop.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Loop.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} + +module Ivory.Language.Loop where + +import Ivory.Language.IIntegral +import Ivory.Language.IBool +import Ivory.Language.Assert +import Ivory.Language.Array +import Ivory.Language.Monad +import Ivory.Language.Proxy +import Ivory.Language.Type +import qualified Ivory.Language.Effects as E +import qualified Ivory.Language.Syntax as AST + +import GHC.TypeLits + +breakOut :: (E.GetBreaks eff ~ E.Break) => Ivory eff () +breakOut = emit AST.Break + +-- XXX don't export. +loop :: forall eff n a. (SingI n) + => (AST.Expr -> AST.LoopIncr) + -> Ix n + -> Ix n + -> (Ix n -> Ivory (E.AllowBreak eff) a) + -> Ivory eff () +loop incr fromIdx toIdx body = do + let maxSz :: IxRep + maxSz = fromInteger $ ixSize (undefined :: Ix n) + let trans v = unwrapExpr $ wrapExpr v .% maxSz + let from = rawIxVal fromIdx + let to = rawIxVal toIdx + ix <- freshVar "ix" + let ixVar = wrapExpr (AST.ExpVar ix) + (_,block) <- collect (body ixVar) + let asst v = compilerAssert (wrapExpr v Ix n -> Ix n -> (Ix n -> Ivory (E.AllowBreak eff) a) -> Ivory eff () +upTo = loop AST.IncrTo + +downTo :: SingI n + => Ix n -> Ix n -> (Ix n -> Ivory (E.AllowBreak eff) a) -> Ivory eff () +downTo = loop AST.DecrTo + +-- | Run the computation n times, where for +-- @ +-- n :: Ix m, 0 <= n < m. +-- @ +-- Indexes increment from 0 to n-1. +for :: forall eff n a. SingI n + => Ix n -> (Ix n -> Ivory (E.AllowBreak eff) a) -> Ivory eff () +for n f = upTo 0 (n-1) f + +-- | Run the computation n times, where for +-- @ +-- n :: Ix m, 0 <= n < m. +-- @ +-- Indexes decrement from n-1 to 0. +times :: forall eff n a. SingI n + => Ix n -> (Ix n -> Ivory (E.AllowBreak eff) a) -> Ivory eff () +times n f = downTo (n-1) 0 f + +arrayMap :: forall eff n a . SingI n + => (Ix n -> Ivory (E.AllowBreak eff) a) -> Ivory eff () +arrayMap = upTo 0 hi + where + hi = fromInteger ((fromTypeNat (sing :: Sing n)) - 1) + +forever :: Ivory (E.AllowBreak eff) () -> Ivory eff () +forever body = do + (_, block) <- collect (body) + emit (AST.Forever (blockStmts block)) diff --git a/src/Ivory/Language/MemArea.hs b/src/Ivory/Language/MemArea.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/MemArea.hs @@ -0,0 +1,147 @@ +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE FlexibleInstances #-} + +module Ivory.Language.MemArea where + +import Ivory.Language.Area +import Ivory.Language.Init +import Ivory.Language.Proxy +import Ivory.Language.Ref +import Ivory.Language.Scope +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + +import qualified MonadLib as M +import qualified MonadLib.Derive as M + +-- Running Initializers -------------------------------------------------------- + +-- | This is used to generate fresh names for compound initializers. +newtype AreaInitM a = AreaInitM + { unAreaInitM :: M.ReaderT String (M.StateT Int M.Id) a } + +areaInit_iso :: M.Iso (M.ReaderT String (M.StateT Int M.Id)) AreaInitM +areaInit_iso = M.Iso AreaInitM unAreaInitM + +instance Functor AreaInitM where + fmap = M.derive_fmap areaInit_iso + +instance Monad AreaInitM where + return = M.derive_return areaInit_iso + (>>=) = M.derive_bind areaInit_iso + +instance M.ReaderM AreaInitM String where + ask = M.derive_ask areaInit_iso + +instance M.StateM AreaInitM Int where + get = M.derive_get areaInit_iso + set = M.derive_set areaInit_iso + +instance FreshName AreaInitM where + freshName s = do + i <- M.get + M.set $! i + 1 + name <- M.ask + return (I.VarLitName ("_iv_" ++ name ++ "_" ++ s ++ show i)) + +runAreaInitM :: String -> AreaInitM a -> a +runAreaInitM s x = fst (M.runId (M.runStateT 0 (M.runReaderT s(unAreaInitM x)))) + +areaInit :: String -> Init area -> (I.Init, [Binding]) +areaInit s ini = runAreaInitM s (runInit (getInit ini)) + +-- Memory Areas ---------------------------------------------------------------- + +-- | Externally defined memory areas. +data MemArea (area :: Area *) + = MemImport I.AreaImport + | MemArea I.Area [I.Area] + +-- XXX do not export +memSym :: MemArea area -> I.Sym +memSym m = case m of + MemImport i -> I.aiSym i + MemArea a _ -> I.areaSym a + +-- | Create an area from an auxillary binding. +bindingArea :: Bool -> Binding -> I.Area +bindingArea isConst b = I.Area + { I.areaSym = bindingSym b + , I.areaConst = isConst + , I.areaType = bindingType b + , I.areaInit = bindingInit b + } + +makeArea :: I.Sym -> Bool -> I.Type -> I.Init -> I.Area +makeArea sym isConst ty ini = I.Area + { I.areaSym = sym + , I.areaConst = isConst + , I.areaType = ty + , I.areaInit = ini + } + +-- | Define a global constant. +area :: forall area. IvoryArea area + => I.Sym -> Maybe (Init area) -> MemArea area +area sym (Just ini) = MemArea a1 as + where + (ini', binds) = areaInit sym ini + ty = ivoryArea (Proxy :: Proxy area) + a1 = makeArea sym False ty ini' + as = map (bindingArea False) binds +area sym Nothing = MemArea a1 [] + where + ty = ivoryArea (Proxy :: Proxy area) + a1 = makeArea sym False ty I.zeroInit + +-- | Import an external symbol from a header. +importArea :: IvoryArea area => I.Sym -> String -> MemArea area +importArea name header = MemImport I.AreaImport + { I.aiSym = name + , I.aiConst = False + , I.aiFile = header + } + + +-- Constant Memory Areas ------------------------------------------------------- + +newtype ConstMemArea (area :: Area *) = ConstMemArea (MemArea area) + +-- | Constant memory area definition. +constArea :: forall area. IvoryArea area + => I.Sym -> Init area -> ConstMemArea area +constArea sym ini = ConstMemArea $ MemArea a1 as + where + (ini', binds) = areaInit sym ini + ty = ivoryArea (Proxy :: Proxy area) + a1 = makeArea sym True ty ini' + as = map (bindingArea True) binds + +-- | Import an external symbol from a header. +importConstArea :: IvoryArea area => I.Sym -> String -> ConstMemArea area +importConstArea name header = ConstMemArea $ MemImport I.AreaImport + { I.aiSym = name + , I.aiConst = False + , I.aiFile = header + } + +-- Area Usage ------------------------------------------------------------------ + +-- | Turn a memory area into a reference. +class IvoryAddrOf (mem :: Area * -> *) ref | mem -> ref, ref -> mem where + addrOf :: IvoryArea area => mem area -> ref Global area + +-- XXX do not export +primAddrOf :: IvoryArea area => MemArea area -> I.Expr +primAddrOf mem = I.ExpAddrOfGlobal (memSym mem) + +instance IvoryAddrOf MemArea Ref where + addrOf mem = wrapExpr (primAddrOf mem) + +instance IvoryAddrOf ConstMemArea ConstRef where + addrOf (ConstMemArea mem) = wrapExpr (primAddrOf mem) + diff --git a/src/Ivory/Language/Module.hs b/src/Ivory/Language/Module.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Module.hs @@ -0,0 +1,112 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +module Ivory.Language.Module where + +import Ivory.Language.Area (IvoryArea) +import Ivory.Language.MemArea (MemArea(..),ConstMemArea(..)) +import Ivory.Language.Proc (Def(..)) +import Ivory.Language.Proxy (Proxy(..)) +import Ivory.Language.String (IvoryString(..)) +import Ivory.Language.Struct (IvoryStruct(..),StructDef(..)) +import qualified Ivory.Language.Syntax as I + +import Control.Monad (forM_) +import Data.Monoid (mempty) +import GHC.TypeLits (SingI()) +import MonadLib (ReaderT,WriterT,ReaderM,WriterM,Id,runM,put,ask,local) +import MonadLib.Derive (Iso (..),derive_ask,derive_put) +import qualified Data.Set as Set + + +-- Modules --------------------------------------------------------------------- + +data Visible = Public | Private deriving (Show) + +newtype ModuleM a = Module + { unModule :: ReaderT Visible (WriterT I.Module Id) a + } deriving (Functor,Monad) + +instance ReaderM ModuleM Visible where + ask = derive_ask (Iso Module unModule) + +instance WriterM ModuleM I.Module where + put = derive_put (Iso Module unModule) + +type ModuleDef = ModuleM () + +-- | Add an element to the public/private list, depending on visibility +visAcc :: Visible -> a -> I.Visible a +visAcc vis e = case vis of + Public -> I.Visible { I.public = [e], I.private = [] } + Private -> I.Visible { I.public = [], I.private = [e] } + +-- | Include a defintion in the module. +incl :: Def a -> ModuleDef +incl (DefProc p) = do + visibility <- ask + put (mempty { I.modProcs = visAcc visibility p }) +incl (DefExtern e) = put (mempty { I.modExterns = [e] }) +incl (DefImport i) = put (mempty { I.modImports = [i] }) + +-- | Add a dependency on an external header. +inclHeader :: String -> ModuleDef +inclHeader inc = put (mempty { I.modHeaders = Set.singleton inc }) + +-- | Add a dependency on another module. +depend :: I.Module -> ModuleDef +depend m = + put (mempty { I.modDepends = Set.singleton (I.modName m) }) + +-- | Include the definition of a structure in the module. +defStruct :: forall sym. (IvoryStruct sym, SingI sym) => + Proxy sym -> ModuleDef +defStruct _ = do + visibility <- ask + put (mempty { I.modStructs = visAcc visibility (getStructDef def) }) + where + def :: StructDef sym + def = structDef + +-- | Include the definition of a string type's structure. +defStringType :: forall str. (IvoryString str) => Proxy str -> ModuleDef +defStringType _ = defStruct (Proxy :: Proxy (StructName str)) + +-- | Include the definition of a memory area. +defMemArea :: IvoryArea area => MemArea area -> ModuleDef +defMemArea m = case m of + MemImport ia -> put (mempty { I.modAreaImports = [ia] }) + MemArea a as -> do + visibility <- ask + put (mempty { I.modAreas = visAcc visibility a }) + forM_ as $ \aux -> do + put (mempty { I.modAreas = visAcc Private aux }) + +-- | Include the definition of a constant memory area. +defConstMemArea :: IvoryArea area => ConstMemArea area -> ModuleDef +defConstMemArea (ConstMemArea m) = defMemArea m + +-- | Depend on an existing (object language) source file which should be copied +-- to the user build tree as part of code generation +sourceDep :: FilePath -> ModuleDef +sourceDep d = + put (mempty { I.modSourceDeps = Set.singleton d }) + +-- | Package the module up. Default visibility is public. +package :: String -> ModuleDef -> I.Module +package name build = (snd (runM (unModule build) Public)) { I.modName = name } + +-- | Start a block of definitions that should not be put in the header. +private :: ModuleDef -> ModuleDef +private build = Module $ local Private (unModule build) + +-- | Start a block of definitions should be put in the header. This is the +-- default, and this function is just included to complement 'private'. +public :: ModuleDef -> ModuleDef +public build = Module $ local Public (unModule build) + +-- Accessors ------------------------------------------------------------------- + +moduleName :: I.Module -> String +moduleName = I.modName diff --git a/src/Ivory/Language/Monad.hs b/src/Ivory/Language/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Monad.hs @@ -0,0 +1,145 @@ +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE TypeOperators #-} + + +module Ivory.Language.Monad ( + -- * Ivory Monad + Ivory() + , retProxy + + -- ** Running Functions + , runIvory, primRunIvory + , collect + + -- ** Effects + , noBreak + , noReturn + , noAlloc + + -- ** Code Blocks + , CodeBlock(..) + , emits + , emit + + -- ** Name Generation + , freshVar + , result + , assign + ) where + +import qualified Ivory.Language.Effects as E +import Ivory.Language.Proxy +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as AST + +import Control.Applicative (Applicative(..)) +import Data.Monoid (Monoid(..)) +import MonadLib (StateT,WriterT,Id) +import qualified MonadLib + + +-- Monad ----------------------------------------------------------------------- + +newtype Ivory (eff :: E.Effects) a = Ivory + { unIvory :: WriterT CodeBlock (StateT Int Id) a + } deriving (Functor,Applicative,Monad) + +data CodeBlock = CodeBlock + { blockStmts :: AST.Block + , blockRequires :: [AST.Require] + , blockEnsures :: [AST.Ensure] + } deriving (Show) + +instance Monoid CodeBlock where + mempty = CodeBlock + { blockStmts = [] + , blockRequires = [] + , blockEnsures = [] + } + mappend l r = CodeBlock + { blockStmts = blockStmts l `mappend` blockStmts r + , blockRequires = blockRequires l `mappend` blockRequires r + , blockEnsures = blockEnsures l `mappend` blockEnsures r + } + + +-- | Run an Ivory block computation that could require any effect. +-- +-- XXX do not export +runIvory :: Ivory (E.ProcEffects s r) a -> (a,CodeBlock) +runIvory b = primRunIvory b + +primRunIvory :: Ivory (E.ProcEffects s r) a -> (a,CodeBlock) +primRunIvory m = fst (MonadLib.runM (unIvory m) 0) + +-- | Collect the 'CodeBlock' for an Ivory computation. +-- +-- XXX do not export +collect :: Ivory eff' a -> Ivory eff (a,CodeBlock) +collect (Ivory m) = Ivory (MonadLib.collect m) + +-- | Get a 'Proxy' to the return type of an Ivory block. +-- +-- XXX do not export +retProxy :: Ivory eff a -> Proxy r +retProxy _ = Proxy + +-- | Add some statements to the collected block. +-- +-- XXX do not export +emits :: CodeBlock -> Ivory eff () +emits = Ivory . MonadLib.put + +-- | Emit a single statement. +-- +-- XXX do not export +emit :: AST.Stmt -> Ivory eff () +emit s = emits mempty { blockStmts = [s] } + +-- | Generate a fresh variable name. +-- +-- XXX do not export +freshVar :: String -> Ivory eff AST.Var +freshVar pfx = Ivory $ do + s <- MonadLib.get + MonadLib.set $! s + 1 + return (AST.VarName (pfx ++ show s)) + +-- | Name the result of an expression. +-- +-- XXX do not export +result :: forall eff a. IvoryExpr a => a -> Ivory eff AST.Var +result a = do + res <- freshVar "r" + let ty = ivoryType (Proxy :: Proxy a) + emit (AST.Assign ty res (unwrapExpr a)) + return res + + +-- Public Functions ------------------------------------------------------------ + +noBreak :: Ivory (E.ClearBreak eff) a -> Ivory eff a +noBreak (Ivory body) = Ivory body + +noAlloc :: (innerEff ~ E.ClearAlloc outerEff) + => Ivory innerEff a -> Ivory outerEff a +noAlloc (Ivory body) = Ivory body + +noReturn :: Ivory (E.ClearReturn eff) a -> Ivory eff a +noReturn (Ivory body) = Ivory body + +-- | Sub-expression naming. +assign :: forall eff a. IvoryExpr a => a -> Ivory eff a +assign e = do + r <- freshVar "let" + emit (AST.Assign (ivoryType (Proxy :: Proxy a)) r (unwrapExpr e)) + return (wrapExpr (AST.ExpVar r)) + diff --git a/src/Ivory/Language/Proc.hs b/src/Ivory/Language/Proc.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Proc.hs @@ -0,0 +1,229 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ExistentialQuantification #-} + +module Ivory.Language.Proc where + +import Ivory.Language.Monad +import Ivory.Language.Proxy +import Ivory.Language.Type +import qualified Ivory.Language.Effects as E +import qualified Ivory.Language.Syntax as AST + + +-- Function Type --------------------------------------------------------------- + +-- | The kind of procedures. +data Proc k = [k] :-> k + +class ProcType (sig :: Proc *) where + procType :: Proxy sig -> (AST.Type,[AST.Type]) + +instance IvoryType r => ProcType ('[] :-> r) where + procType _ = (ivoryType (Proxy :: Proxy r),[]) + +instance (IvoryType a, ProcType (args :-> r)) + => ProcType ((a ': args) :-> r) where + procType _ = (r, ivoryType (Proxy :: Proxy a) : args) + where + (r,args) = procType (Proxy :: Proxy (args :-> r)) + + +-- Function Pointers ----------------------------------------------------------- + +-- | Procedure pointers +newtype ProcPtr (sig :: Proc *) = ProcPtr { getProcPtr :: AST.Name } + +instance ProcType proc => IvoryType (ProcPtr proc) where + ivoryType _ = AST.TyProc r args + where + (r,args) = procType (Proxy :: Proxy proc) + +instance ProcType proc => IvoryVar (ProcPtr proc) where + wrapVar = ProcPtr . AST.NameVar + unwrapExpr ptr = case getProcPtr ptr of + AST.NameSym sym -> AST.ExpSym sym + AST.NameVar var -> AST.ExpVar var + +procPtr :: ProcType sig => Def sig -> ProcPtr sig +procPtr = ProcPtr . defSymbol + + +-- Function Symbols ------------------------------------------------------------ + +-- | Procedure definitions. +data Def (proc :: Proc *) + = DefProc AST.Proc + | DefExtern AST.Extern + | DefImport AST.Import + deriving (Show, Eq, Ord) + +defSymbol :: Def proc -> AST.Name +defSymbol def = case def of + DefProc p -> AST.NameSym (AST.procSym p) + DefExtern e -> AST.NameSym (AST.externSym e) + DefImport i -> AST.NameSym (AST.importSym i) + +instance ProcType proc => IvoryType (Def proc) where + ivoryType _ = AST.TyProc r args + where + (r,args) = procType (Proxy :: Proxy proc) + + +-- Procedure Definition -------------------------------------------------------- + +-- | Procedure definition. +proc :: forall proc impl. IvoryProcDef proc impl => AST.Sym -> impl -> Def proc +proc name impl = DefProc AST.Proc + { AST.procSym = name + , AST.procRetTy = r + , AST.procArgs = zipWith AST.Typed args vars + , AST.procBody = blockStmts block + , AST.procRequires = blockRequires block + , AST.procEnsures = blockEnsures block + } + where + (r,args) = procType (Proxy :: Proxy proc) + (vars,block) = procDef initialClosure Proxy impl + + +newtype Body r = Body + { runBody :: forall s . Ivory (E.ProcEffects s r) () + } + +body :: IvoryType r + => (forall s . Ivory (E.ProcEffects s r) ()) + -> Body r +body m = Body m + +class ProcType proc => IvoryProcDef (proc :: Proc *) impl | impl -> proc where + procDef :: Closure -> Proxy proc -> impl -> ([AST.Var],CodeBlock) + +instance IvoryType ret => IvoryProcDef ('[] :-> ret) (Body ret) where + procDef env _ b = (getEnv env, snd (primRunIvory (runBody b))) + +instance (IvoryVar a, IvoryProcDef (args :-> ret) k) + => IvoryProcDef ((a ': args) :-> ret) (a -> k) where + procDef env _ k = procDef env' (Proxy :: Proxy (args :-> ret)) (k arg) + where + (var,env') = genVar env + arg = wrapVar var + + +-- | A variable name supply, and the typed values that have been generated. +data Closure = Closure + { closSupply :: [AST.Var] + , closEnv :: [AST.Var] + } + +-- | Initial closure, with no environment and a large supply of names. +initialClosure :: Closure +initialClosure = Closure + { closSupply = [ AST.VarName ("var" ++ show (n :: Int)) | n <- [0 ..] ] + , closEnv = [] + } + +-- | Given a type and a closure, generate a typed variable, and a new closure +-- with that typed variable in it's environment. +genVar :: Closure -> (AST.Var, Closure) +genVar clos = (var, clos') + where + var = head (closSupply clos) + clos' = Closure + { closSupply = tail (closSupply clos) + , closEnv = var : closEnv clos + } + +-- | Retrieve the environment from a closure. +getEnv :: Closure -> [AST.Var] +getEnv = reverse . closEnv + + +-- External Functions ---------------------------------------------------------- + +-- | External function reference. +externProc :: forall proc. ProcType proc => AST.Sym -> Def proc +externProc sym = DefExtern AST.Extern + { AST.externSym = sym + , AST.externRetType = r + , AST.externArgs = args + } + where + (r,args) = procType (Proxy :: Proxy proc) + + +-- Imported Functions ---------------------------------------------------------- + +-- | Import a function from a C header. +importProc :: forall proc. ProcType proc => AST.Sym -> String -> Def proc +importProc sym file = DefImport AST.Import + { AST.importSym = sym + , AST.importFile = file + } + + +-- Call ------------------------------------------------------------------------ + +-- | Direct calls. +call :: forall proc eff impl. IvoryCall proc eff impl => Def proc -> impl +call def = callAux (defSymbol def) (Proxy :: Proxy proc) [] + +-- | Indirect calls. +indirect :: forall proc eff impl. IvoryCall proc eff impl + => ProcPtr proc -> impl +indirect ptr = callAux (getProcPtr ptr) (Proxy :: Proxy proc) [] + +class IvoryCall (proc :: Proc *) (eff :: E.Effects) impl + | proc eff -> impl, impl -> eff where + callAux :: AST.Name -> Proxy proc -> [AST.Typed AST.Expr] -> impl + +instance IvoryVar r => IvoryCall ('[] :-> r) eff (Ivory eff r) where + callAux sym _ args = do + r <- freshVar "r" + emit (AST.Call (ivoryType (Proxy :: Proxy r)) (Just r) sym (reverse args)) + return (wrapVar r) + +instance (IvoryVar a, IvoryVar r, IvoryCall (args :-> r) eff impl) + => IvoryCall ((a ': args) :-> r) eff (a -> impl) where + callAux sym _ args a = callAux sym rest args' + where + rest = Proxy :: Proxy (args :-> r) + args' = typedExpr a : args + + +-- Call_ ----------------------------------------------------------------------- + +-- | Direct calls, ignoring the result. +call_ :: forall proc eff impl. IvoryCall_ proc eff impl => Def proc -> impl +call_ def = callAux_ (defSymbol def) (Proxy :: Proxy proc) [] + +-- | Indirect calls, ignoring the result. +indirect_ :: forall proc eff impl. IvoryCall_ proc eff impl + => ProcPtr proc -> impl +indirect_ ptr = callAux_ (getProcPtr ptr) (Proxy :: Proxy proc) [] + +class IvoryCall_ (proc :: Proc *) (eff :: E.Effects) impl + | proc eff -> impl, impl -> eff + where + callAux_ :: AST.Name -> Proxy proc -> [AST.Typed AST.Expr] -> impl + +instance IvoryType r => IvoryCall_ ('[] :-> r) eff (Ivory eff ()) where + callAux_ sym _ args = do + emit (AST.Call (ivoryType (Proxy :: Proxy r)) Nothing sym (reverse args)) + +instance (IvoryVar a, IvoryType r, IvoryCall_ (args :-> r) eff impl) + => IvoryCall_ ((a ': args) :-> r) eff (a -> impl) where + callAux_ sym _ args a = callAux_ sym rest args' + where + rest = Proxy :: Proxy (args :-> r) + args' = typedExpr a : args diff --git a/src/Ivory/Language/Proxy.hs b/src/Ivory/Language/Proxy.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Proxy.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE KindSignatures #-} + +module Ivory.Language.Proxy where + +import GHC.TypeLits (Sing,fromSing,Symbol,Nat) + + +data Proxy (a :: k) = Proxy + +-- | Type proxies for * types. +type SProxy a = Proxy (a :: *) + +-- | The string associated with a type-symbol. +fromTypeSym :: Sing (sym :: Symbol) -> String +fromTypeSym = fromSing + +-- | The integer associated with a type-nat. +fromTypeNat :: Sing (i :: Nat) -> Integer +fromTypeNat = fromSing diff --git a/src/Ivory/Language/Ptr.hs b/src/Ivory/Language/Ptr.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Ptr.hs @@ -0,0 +1,48 @@ +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +module Ivory.Language.Ptr where + +import Ivory.Language.IBool +import Ivory.Language.Area +import Ivory.Language.Proxy +import Ivory.Language.Ref +import Ivory.Language.Scope +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + + +-- Pointers -------------------------------------------------------------------- + +-- | Pointers (nullable references). +newtype Ptr (s :: RefScope) (a :: Area *) = Ptr { getPtr :: I.Expr } + +instance IvoryArea area => IvoryType (Ptr s area) where + ivoryType _ = I.TyPtr (ivoryArea (Proxy :: Proxy area)) + +instance IvoryArea area => IvoryVar (Ptr s area) where + wrapVar = wrapVarExpr + unwrapExpr = getPtr + +instance IvoryArea area => IvoryExpr (Ptr s area) where + wrapExpr = Ptr + +instance IvoryArea area => IvoryEq (Ptr s area) + +-- Only allow global pointers to be stored in structures. +instance IvoryArea a => IvoryStore (Ptr Global a) + +nullPtr :: IvoryArea area => Ptr s area +nullPtr = Ptr (I.ExpLit I.LitNull) + +-- | Convert a reference to a pointer. This direction is safe as we know that +-- the reference is a non-null pointer. +refToPtr :: IvoryArea area => Ref s area -> Ptr s area +refToPtr = wrapExpr . unwrapExpr + +-- XXX do not export +ptrToRef :: IvoryArea area => Ptr s area -> Ref s area +ptrToRef = wrapExpr . unwrapExpr diff --git a/src/Ivory/Language/Ref.hs b/src/Ivory/Language/Ref.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Ref.hs @@ -0,0 +1,111 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE InstanceSigs #-} + +module Ivory.Language.Ref where + +import Ivory.Language.IChar (IChar) +import Ivory.Language.Sint (Sint8,Sint16,Sint32,Sint64) +import Ivory.Language.Uint (Uint8,Uint16,Uint32,Uint64) + +import Ivory.Language.Area +import Ivory.Language.Monad +import Ivory.Language.Proxy +import Ivory.Language.Scope +import Ivory.Language.IBool +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + + +-- References ------------------------------------------------------------------ + +-- | A non-null pointer to a memory area. +newtype Ref (s :: RefScope) (a :: Area *) = Ref { getRef :: I.Expr } + +instance IvoryArea area => IvoryType (Ref s area) where + ivoryType _ = I.TyRef (ivoryArea (Proxy :: Proxy area)) + +instance IvoryArea area => IvoryVar (Ref s area) where + wrapVar = wrapVarExpr + unwrapExpr = getRef + +instance IvoryArea area => IvoryExpr (Ref s area) where + wrapExpr = Ref + + +-- Constant References --------------------------------------------------------- + +-- | Turn a reference into a constant reference. +constRef :: IvoryArea area => Ref s area -> ConstRef s area +constRef = wrapExpr . unwrapExpr + +newtype ConstRef (s :: RefScope) (a :: Area *) = ConstRef + { getConstRef :: I.Expr + } + +instance IvoryArea area => IvoryType (ConstRef s area) where + ivoryType _ = I.TyConstRef (ivoryArea (Proxy :: Proxy area)) + +instance IvoryArea area => IvoryVar (ConstRef s area) where + wrapVar = wrapVarExpr + unwrapExpr = getConstRef + +instance IvoryArea area => IvoryExpr (ConstRef s area) where + wrapExpr = ConstRef + + +-- Dereferencing --------------------------------------------------------------- + +class IvoryRef (ref :: RefScope -> Area * -> *) where + unwrapRef :: IvoryVar a => ref s (Stored a) -> I.Expr + +instance IvoryRef Ref where + unwrapRef = unwrapExpr + +instance IvoryRef ConstRef where + unwrapRef = unwrapExpr + +-- | Dereferenceing. +deref :: forall eff ref s a. + (IvoryVar a, IvoryVar (ref s (Stored a)), IvoryRef ref) + => ref s (Stored a) -> Ivory eff a +deref ref = do + r <- freshVar "deref" + emit (I.Deref (ivoryType (Proxy :: Proxy a)) r (unwrapRef ref)) + return (wrapVar r) + +-- Copying --------------------------------------------------------------------- + +-- | Memory copy. Emits an assertion that the two references are unequal. +refCopy :: forall eff sTo ref sFrom a. + ( IvoryRef ref, IvoryVar (Ref sTo a), IvoryVar (ref sFrom a), IvoryArea a) + => Ref sTo a -> ref sFrom a -> Ivory eff () +refCopy destRef srcRef = + emit (I.RefCopy (ivoryArea (Proxy :: Proxy a)) + (unwrapExpr destRef) (unwrapExpr srcRef)) + +-- Storing --------------------------------------------------------------------- + +store :: forall eff s a. IvoryStore a => Ref s (Stored a) -> a -> Ivory eff () +store ref a = emit (I.Store ty (unwrapExpr ref) (unwrapExpr a)) + where + ty = ivoryType (Proxy :: Proxy a) + +-- | Things that can be safely stored in references. +class IvoryVar a => IvoryStore a where + +-- simple types +instance IvoryStore IBool +instance IvoryStore IChar +instance IvoryStore Uint8 +instance IvoryStore Uint16 +instance IvoryStore Uint32 +instance IvoryStore Uint64 +instance IvoryStore Sint8 +instance IvoryStore Sint16 +instance IvoryStore Sint32 +instance IvoryStore Sint64 diff --git a/src/Ivory/Language/Scope.hs b/src/Ivory/Language/Scope.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Scope.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ExistentialQuantification #-} + +module Ivory.Language.Scope where + +-- | Definition scopes for values. +data RefScope + = Global -- ^ Globally allocated + | forall s. Stack s -- ^ Stack allocated diff --git a/src/Ivory/Language/Sint.hs b/src/Ivory/Language/Sint.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Sint.hs @@ -0,0 +1,130 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE DataKinds #-} + +module Ivory.Language.Sint where + +import Ivory.Language.Area +import Ivory.Language.BoundedInteger +import Ivory.Language.SizeOf +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + +import Data.Int (Int8,Int16,Int32,Int64) + +-- Signed Types ---------------------------------------------------------------- + +-- | 8-bit integers. +newtype Sint8 = Sint8 { getSint8 :: I.Expr } + +instance IvoryType Sint8 where + ivoryType _ = I.TyInt I.Int8 + +instance IvoryVar Sint8 where + wrapVar = wrapVarExpr + unwrapExpr = getSint8 + +instance IvoryExpr Sint8 where + wrapExpr = Sint8 + +instance IvorySizeOf (Stored Sint8) where + sizeOfBytes _ = 1 + +instance Num Sint8 where + (*) = exprBinop (*) + (+) = exprBinop (+) + (-) = exprBinop (-) + abs = exprUnary abs + signum = exprUnary signum + negate = exprUnary negate + fromInteger = boundedFromInteger Sint8 (0 :: Int8) + +instance Bounded Sint8 where + minBound = wrapExpr (I.ExpMaxMin False) + maxBound = wrapExpr (I.ExpMaxMin True) + +-- | 16-bit integers. +newtype Sint16 = Sint16 { getSint16 :: I.Expr } + +instance IvoryType Sint16 where + ivoryType _ = I.TyInt I.Int16 + +instance IvoryVar Sint16 where + wrapVar = wrapVarExpr + unwrapExpr = getSint16 + +instance IvoryExpr Sint16 where + wrapExpr = Sint16 + +instance IvorySizeOf (Stored Sint16) where + sizeOfBytes _ = 2 + +instance Num Sint16 where + (*) = exprBinop (*) + (+) = exprBinop (+) + (-) = exprBinop (-) + abs = exprUnary abs + signum = exprUnary signum + negate = exprUnary negate + fromInteger = boundedFromInteger Sint16 (0 :: Int16) + +instance Bounded Sint16 where + minBound = wrapExpr (I.ExpMaxMin False) + maxBound = wrapExpr (I.ExpMaxMin True) + +-- | 32-bit integers. +newtype Sint32 = Sint32 { getSint32 :: I.Expr } + +instance IvoryType Sint32 where + ivoryType _ = I.TyInt I.Int32 + +instance IvoryVar Sint32 where + wrapVar = wrapVarExpr + unwrapExpr = getSint32 + +instance IvoryExpr Sint32 where + wrapExpr = Sint32 + +instance IvorySizeOf (Stored Sint32) where + sizeOfBytes _ = 4 + +instance Num Sint32 where + (*) = exprBinop (*) + (+) = exprBinop (+) + (-) = exprBinop (-) + abs = exprUnary abs + signum = exprUnary signum + negate = exprUnary negate + fromInteger = boundedFromInteger Sint32 (0 :: Int32) + +instance Bounded Sint32 where + minBound = wrapExpr (I.ExpMaxMin False) + maxBound = wrapExpr (I.ExpMaxMin True) + +-- | 64-bit integers. +newtype Sint64 = Sint64 { getSint64 :: I.Expr } + +instance IvoryType Sint64 where + ivoryType _ = I.TyInt I.Int64 + +instance IvoryVar Sint64 where + wrapVar = wrapVarExpr + unwrapExpr = getSint64 + +instance IvoryExpr Sint64 where + wrapExpr = Sint64 + +instance IvorySizeOf (Stored Sint64) where + sizeOfBytes _ = 8 + +instance Num Sint64 where + (*) = exprBinop (*) + (+) = exprBinop (+) + (-) = exprBinop (-) + abs = exprUnary abs + signum = exprUnary signum + negate = exprUnary negate + fromInteger = boundedFromInteger Sint64 (0 :: Int64) + +instance Bounded Sint64 where + minBound = wrapExpr (I.ExpMaxMin False) + maxBound = wrapExpr (I.ExpMaxMin True) diff --git a/src/Ivory/Language/SizeOf.hs b/src/Ivory/Language/SizeOf.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/SizeOf.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE DataKinds #-} + +module Ivory.Language.SizeOf where + +import Ivory.Language.Area +import Ivory.Language.Proxy +import Ivory.Language.Type + +import GHC.TypeLits (SingI,Sing,sing) + + +class IvoryArea t => IvorySizeOf (t :: Area *) where + sizeOfBytes :: Proxy t -> Integer + +instance (SingI len, IvorySizeOf area) => IvorySizeOf (Array len area) where + sizeOfBytes _ = + fromTypeNat (sing :: Sing len) * sizeOfBytes (Proxy :: Proxy area) + + +-- | Get the size of an ivory type. +sizeOf :: (IvorySizeOf t, IvoryExpr a, Num a) => Proxy t -> a +sizeOf = fromInteger . sizeOfBytes + diff --git a/src/Ivory/Language/String.hs b/src/Ivory/Language/String.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/String.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleContexts #-} + +module Ivory.Language.String where + +import Ivory.Language.Area +import Ivory.Language.Array +import Ivory.Language.Struct +import Ivory.Language.Uint + +import GHC.TypeLits + +class ( SingI (Capacity a) + , IvoryStruct (StructName a) + , IvoryArea a + , a ~ Struct (StructName a) + ) => IvoryString a where + type Capacity a :: Nat + + stringDataL :: Label (StructName a) (Array (Capacity a) (Stored Uint8)) + stringLengthL :: Label (StructName a) (Stored (Ix (Capacity a))) + diff --git a/src/Ivory/Language/Struct.hs b/src/Ivory/Language/Struct.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Struct.hs @@ -0,0 +1,45 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} + +module Ivory.Language.Struct where + +import Ivory.Language.Area +import Ivory.Language.Proxy +import Ivory.Language.Ref +import Ivory.Language.Type(IvoryExpr(..), IvoryVar(..)) +import qualified Ivory.Language.Syntax as I + +import GHC.TypeLits (SingI,sing,Sing,Symbol) + + +-- Structs --------------------------------------------------------------------- + +instance (IvoryStruct sym, SingI sym) => IvoryArea (Struct sym) where + ivoryArea _ = I.TyStruct (fromTypeSym (sing :: Sing sym)) + +newtype StructDef (sym :: Symbol) = StructDef { getStructDef :: I.Struct } + +class (IvoryArea (Struct sym), SingI sym) => IvoryStruct (sym :: Symbol) where + type StructName (a :: Area *) :: Symbol + type StructName (Struct sym) = sym + + structDef :: StructDef sym + +-- | Struct field labels. +newtype Label (sym :: Symbol) (field :: Area *) = Label { getLabel :: String } + +instance Eq (Label (sym :: Symbol) (field :: Area *)) where + l0 == l1 = getLabel l0 == getLabel l1 + +-- | Label indexing in a structure. +(~>) :: forall ref s sym field. + ( IvoryStruct sym, IvoryRef ref + , IvoryExpr (ref s (Struct sym)), IvoryExpr (ref s field) ) + => ref s (Struct sym) -> Label sym field -> ref s field +s ~> l = wrapExpr (I.ExpLabel ty (unwrapExpr s) (getLabel l)) + where + ty = ivoryArea (Proxy :: Proxy (Struct sym)) diff --git a/src/Ivory/Language/Struct/Parser.hs b/src/Ivory/Language/Struct/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Struct/Parser.hs @@ -0,0 +1,109 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Ivory.Language.Struct.Parser ( + parseStructDefs + + , StructDef(..), Field(..), Type(..) + ) where + +import Control.Applicative ((<$>),(<$),(<*>),(*>),(<*),many,(<|>),some) +import Control.Monad (void) +import Data.Char (isLower,isAscii,isAlphaNum,isLetter) +import Text.Parsec.Char (char,satisfy,spaces,string,digit) +import Text.Parsec.Combinator (sepBy1) +import Text.Parsec.String (Parser) +import Text.Parsec.Prim (try) + + +data StructDef + = StructDef String [Field] + | AbstractDef String String + | StringDef String Integer + deriving (Show) + +data Field = Field + { fieldName :: String + , fieldType :: Type + } deriving (Show) + +data Type + = TApp Type Type + | TCon String + | TNat Integer + | TSym String + deriving (Show) + + +parseStructDefs :: Parser [StructDef] +parseStructDefs = comments *> some parseStructDef + +token' :: Parser a -> Parser a +token' body = try body <* comments + where + +comments :: Parser () +comments = spaces *> void (many comment) + where + comment = string "--" *> many (satisfy (not . newline)) *> spaces + newline = (== '\n') + + +token :: String -> Parser () +token str = void (token' (string str)) + +braces :: Parser a -> Parser a +braces body = token "{" *> body <* token "}" + +parens :: Parser a -> Parser a +parens body = token "(" *> body <* token ")" + +semi :: Parser () +semi = token ";" + +parseStructDef :: Parser StructDef +parseStructDef = structDef <|> abstractDef <|> stringDef + +structDef :: Parser StructDef +structDef = StructDef <$ token "struct" + <*> parseName + <*> braces (parseField `sepBy1` semi) + +abstractDef :: Parser StructDef +abstractDef = AbstractDef <$ token "abstract" + <* token "struct" + <*> parseName + <*> parseString + +stringDef :: Parser StructDef +stringDef = StringDef <$ token "string" + <*> parseName + <*> number + +parseName :: Parser String +parseName = token' ((:) <$> satisfy isLetter <*> following) + +parseIdent :: Parser String +parseIdent = token' ((:) <$> satisfy isLower <*> following) + +following :: Parser String +following = many (satisfy (\c -> isAscii c && (isAlphaNum c || c == '_'))) + +parseField :: Parser Field +parseField = Field <$> parseIdent + <* token "::" + <*> parseType + +parseType :: Parser Type +parseType = foldl1 TApp <$> some parseAType + +parseAType :: Parser Type +parseAType = (TNat <$> number) + <|> (TCon <$> parseName) + <|> (TSym <$> parseString) + <|> parens parseType + +number :: Parser Integer +number = read <$> token' (some digit) + +parseString :: Parser String +parseString = char '"' *> (many (satisfy (/= '"'))) <* token' (char '"') diff --git a/src/Ivory/Language/Struct/Quote.hs b/src/Ivory/Language/Struct/Quote.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Struct/Quote.hs @@ -0,0 +1,211 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} + +module Ivory.Language.Struct.Quote ( + ivory + ) where + +import Ivory.Language.Area +import Ivory.Language.Proxy +import Ivory.Language.Scope +import Ivory.Language.SizeOf +import Ivory.Language.String +import Ivory.Language.Struct +import qualified Ivory.Language.Struct.Parser as P +import qualified Ivory.Language.Syntax.AST as AST +import qualified Ivory.Language.Syntax.Type as AST + +import Data.Traversable (sequenceA) +import Language.Haskell.TH +import Language.Haskell.TH.Quote +import Text.Parsec.Prim (parse,setPosition,getPosition) +import Text.Parsec.Pos (setSourceLine,setSourceColumn) + + +ivory :: QuasiQuoter +ivory = QuasiQuoter + { quoteExp = const (fail "struct: unable to quote expressions") + , quotePat = const (fail "struct: unable to quote patterns") + , quoteType = const (fail "struct: unable to quote types") + , quoteDec = quoteStructDefs + } + +parseDefs :: String -> Q [P.StructDef] +parseDefs str = do + loc <- location + case parse (body loc) (loc_filename loc) str of + Right defs -> return defs + Left err -> fail (show err) + where + body loc = do + pos <- getPosition + let (line,col) = loc_start loc + setPosition (setSourceLine (setSourceColumn pos col) line) + P.parseStructDefs + +quoteStructDefs :: String -> Q [Dec] +quoteStructDefs str = concat `fmap` (mapM mkDef =<< parseDefs str) + +mkDef :: P.StructDef -> Q [Dec] +mkDef def = case def of + P.StructDef n fs -> do + let sym = mkSym n + sizeOfDefs <- mkIvorySizeOf sym fs + sequence (mkIvoryStruct sym def ++ sizeOfDefs ++ mkFields sym fs) + + P.AbstractDef n _hdr -> sequence (mkIvoryStruct (mkSym n) def) + + P.StringDef name len -> mkStringDef name len + where + mkSym n = litT (strTyLit n) + + +-- IvoryStruct ----------------------------------------------------------------- + +-- | Generate an @IvoryStruct@ instance. +mkIvoryStruct :: TypeQ -> P.StructDef -> [DecQ] +mkIvoryStruct sym def = + [ instanceD (cxt []) (appT (conT ''IvoryStruct) sym) [mkStructDef def] + ] + +mkStructDef :: P.StructDef -> DecQ +mkStructDef def = funD 'structDef + [ clause [] (normalB [| StructDef $astStruct |] ) [] + ] + where + astStruct = case def of + P.StructDef n fs -> [| AST.Struct $(stringE n) + $(listE (map mkField fs)) |] + P.AbstractDef n hdr -> [| AST.Abstract $(stringE n) $(stringE hdr) |] + P.StringDef _ _ -> error "unexpected string definition" + + mkField f = + [| AST.Typed + { AST.tType = $(mkTypeE (P.fieldType f)) + , AST.tValue = $(stringE (P.fieldName f)) + } + |] + + +-- IvorySizeOf ----------------------------------------------------------------- + +mkIvorySizeOf :: TypeQ -> [P.Field] -> Q [DecQ] +mkIvorySizeOf sym fields = do + mbs <- mapM fieldSizeOfBytes fields + case sequenceA mbs of + Just tys | not (null tys) -> return (mkIvorySizeOfInst sym tys) + _ -> return [] + +-- | Return a call to 'sizeOfBytes' if there's an instance for the type named in +-- the field. +fieldSizeOfBytes :: P.Field -> Q (Maybe Type) +fieldSizeOfBytes field = do + ty <- mkType (P.fieldType field) + hasInstance <- isInstance ''IvorySizeOf [ty] + if hasInstance + then return (Just ty) + else return Nothing + +mkIvorySizeOfInst :: TypeQ -> [Type] -> [DecQ] +mkIvorySizeOfInst sym tys = + [ instanceD (cxt []) (appT (conT ''IvorySizeOf) struct) [mkSizeOfBytes tys] + ] + where + struct = [t| Struct $sym |] + +mkSizeOfBytes :: [Type] -> DecQ +mkSizeOfBytes tys = funD 'sizeOfBytes + [ clause [wildP] (normalB (foldr1 add exprs)) [] + ] + where + exprs = [ [| sizeOfBytes (Proxy :: AProxy $(return ty)) |] | ty <- tys ] + add l r = [| $l + ($r :: Integer) |] + +-- Field Labels ---------------------------------------------------------------- + +mkFields :: TypeQ -> [P.Field] -> [DecQ] +mkFields sym = concatMap (mkLabel sym) + +mkLabel :: TypeQ -> P.Field -> [DecQ] +mkLabel sym f = + [ sigD field [t| Label $sym $(mkType (P.fieldType f)) |] + , funD field [clause [] (normalB [| Label $(stringE (P.fieldName f)) |]) []] + ] + where + field = mkName (P.fieldName f) + +mkType :: P.Type -> TypeQ +mkType ty = case ty of + P.TApp f x -> appT (mkType f) (mkType x) + + P.TCon "Stored" -> promotedT 'Stored + P.TCon "Array" -> promotedT 'Array + P.TCon "Struct" -> promotedT 'Struct + P.TCon "Global" -> promotedT 'Global + P.TCon "Stack" -> fail "struct: not sure what to do with Stack yet" + + P.TCon con -> do + mb <- lookupTypeName con + case mb of + Just n -> conT n + Nothing -> fail ("Unknown type: " ++ con) + + P.TNat n -> litT (numTyLit n) + + P.TSym s -> litT (strTyLit s) + +flattenTApp :: P.Type -> [P.Type] +flattenTApp ty = case ty of + P.TApp l r -> flattenTApp l ++ [r] + _ -> [ty] + +-- | Turn a parsed type into its AST representation. +mkTypeE :: P.Type -> ExpQ +mkTypeE ty = + appE (varE 'ivoryArea) + (sigE (conE 'Proxy) + (appT (conT ''Proxy) (mkType ty))) + +-- Note: The above is equivalent to: +-- +-- [| ivoryArea (Proxy :: Proxy $(mkType ty)) |] +-- +-- except I can't get TH to type-check that (maybe this will +-- work in GHC 7.8?) + +-- String Types --------------------------------------------------------------- + +-- | Create an Ivory type for a string with a fixed capacity. +mkStringDef :: String -> Integer -> Q [Dec] +mkStringDef ty_s len = do + let ty_n = mkName ty_s + let struct_s = "ivory_string_" ++ ty_s + let struct_n = mkName struct_s + let struct_t = [t| Struct $(litT (strTyLit struct_s)) |] + let data_s = struct_s ++ "_data" + let data_n = mkName data_s + let len_s = struct_s ++ "_len" + let len_n = mkName len_s + + let data_t = P.TApp (P.TApp (P.TCon "Array") (P.TNat len)) + (P.TApp (P.TCon "Stored") (P.TCon "Uint8")) + let data_f = P.Field data_s data_t + let len_t = P.TApp (P.TCon "Stored") + (P.TApp (P.TCon "Ix") (P.TNat len)) + let len_f = P.Field len_s len_t + let struct_def = P.StructDef struct_s [data_f, len_f] + + d1 <- mkDef struct_def + d2 <- sequence $ + [ tySynD ty_n [] struct_t + , instanceD (cxt []) (appT (conT ''IvoryString) struct_t) + [ tySynInstD ''Capacity [struct_t] (litT (numTyLit len)) + , valD (varP 'stringDataL) (normalB (varE data_n)) [] + , valD (varP 'stringLengthL) (normalB (varE len_n)) [] + ] + ] + + return (d1 ++ d2) diff --git a/src/Ivory/Language/Syntax.hs b/src/Ivory/Language/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Syntax.hs @@ -0,0 +1,7 @@ +module Ivory.Language.Syntax ( + module Exports + ) where + +import Ivory.Language.Syntax.AST as Exports +import Ivory.Language.Syntax.Names as Exports +import Ivory.Language.Syntax.Type as Exports diff --git a/src/Ivory/Language/Syntax/AST.hs b/src/Ivory/Language/Syntax/AST.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Syntax/AST.hs @@ -0,0 +1,436 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Ivory.Language.Syntax.AST where + +import Ivory.Language.Syntax.Names +import Ivory.Language.Syntax.Type + +import Data.Monoid (Monoid(..)) +import Language.Haskell.TH.Lift (deriveLiftMany) +import Language.Haskell.TH.Syntax (Lift(..)) +import qualified Data.Set as Set + + +-- Modules --------------------------------------------------------------------- + +-- | An external module that defines an imported resource. A header file in C +-- is an example of this. +type ModulePath = String + +data Visible a = Visible + { public :: [a] + , private :: [a] + } deriving (Show, Eq, Ord) + +instance Monoid (Visible a) where + mempty = Visible [] [] + mappend (Visible l0 l1) (Visible m0 m1) = Visible (l0 ++ m0) (l1 ++ m1) + +-- | The name of a module defined in Ivory. +type ModuleName = String + +data Module = Module + { modName :: ModuleName + -- ^ The name of this module + , modHeaders :: Set.Set FilePath + -- ^ Included headers + , modDepends :: Set.Set ModuleName + -- ^ Named module dependencies + , modExterns :: [Extern] + , modImports :: [Import] + , modProcs :: Visible Proc + , modStructs :: Visible Struct + , modAreas :: Visible Area + , modAreaImports :: [AreaImport] + , modSourceDeps :: Set.Set FilePath + } deriving (Show, Eq, Ord) + +instance Monoid Module where + mempty = Module + { modName = "" + , modHeaders = Set.empty + , modDepends = Set.empty + , modExterns = [] + , modImports = [] + , modProcs = mempty + , modStructs = mempty + , modAreas = mempty + , modAreaImports = [] + , modSourceDeps = Set.empty + } + + mappend l r = Module + { modName = modName (if null (modName l) then r else l) + , modHeaders = modHeaders l `mappend` modHeaders r + , modDepends = modDepends l `mappend` modDepends r + , modExterns = modExterns l `mappend` modExterns r + , modImports = modImports l `mappend` modImports r + , modProcs = modProcs l `mappend` modProcs r + , modStructs = modStructs l `mappend` modStructs r + , modAreas = modAreas l `mappend` modAreas r + , modAreaImports = modAreaImports l `mappend` modAreaImports r + , modSourceDeps = modSourceDeps l `mappend` modSourceDeps r + } + + +-- External Functions ---------------------------------------------------------- + +-- | Functions not defined in a header, but are available to the linker. +data Extern = Extern + { externSym :: Sym + , externRetType :: Type + , externArgs :: [Type] + } deriving (Show, Eq, Ord) + + +-- Imported Functions ---------------------------------------------------------- + +-- | Functions that are defined in a c header. +data Import = Import + { importSym :: Sym + , importFile :: ModulePath + } deriving (Show, Eq, Ord) + + +-- Procedures ------------------------------------------------------------------ + +-- | Functions defined in the language. +data Proc = Proc + { procSym :: Sym + , procRetTy :: Type + , procArgs :: [Typed Var] + , procBody :: Block + , procRequires :: [Require] + , procEnsures :: [Ensure] + } deriving (Show, Eq, Ord) + + +-- Structure Definitions ------------------------------------------------------- + +data Struct + = Struct String [Typed String] + | Abstract String ModulePath + deriving (Show, Eq, Ord) + +structName :: Struct -> String +structName def = case def of + Struct n _ -> n + Abstract n _ -> n + + +-- Global Memory Areas --------------------------------------------------------- + +data Area = Area + { areaSym :: Sym + , areaConst :: Bool + , areaType :: Type + , areaInit :: Init + } deriving (Show, Eq, Ord) + + +-- Imported Memory Areas ------------------------------------------------------- + +data AreaImport = AreaImport + { aiSym :: Sym + , aiConst :: Bool + , aiFile :: ModulePath + } deriving (Show, Eq, Ord) + + +-- Statements ------------------------------------------------------------------ + +type Block = [Stmt] + +data Stmt + = IfTE Expr Block Block + -- ^ If-then-else statement. The @Expr@ argument will be typed as an + -- @IBool@. + + | Assert Expr + -- ^ Boolean-valued assertions. The @Expr@ argument will be typed as an + -- @IBool@. + + | CompilerAssert Expr + -- ^ Compiler-inserted assertion (as opposed to user-level assertions). + -- These are expected to be correct (e.g., no overflow, etc). Not exported. + + | Assume Expr + -- ^ Boolean-valued assumptions. The @Expr@ argument will be typed as an + -- @IBool@. + + | Return (Typed Expr) + -- ^ Returning a value. + + | ReturnVoid + -- ^ Returning void. + + | Deref Type Var Expr + -- ^ Reference dereferencing. The type parameter refers to the type of the + -- referenced value, not the reference itself; the expression to be + -- dereferenced is assumed to always be a reference. + + | Store Type Expr Expr + -- ^ Storing to a reference. The type parameter refers to the type of the + -- referenced value, not the reference itself; the expression to be + -- dereferenced is assumed to always be a reference. + + | Assign Type Var Expr + -- ^ Simple assignment. + + | Call Type (Maybe Var) Name [Typed Expr] + -- ^ Function call. The optional variable is where to store the result. It + -- is expected that the @Expr@ passed for the function symbol will have the + -- same type as the combination of the types for the arguments, and the + -- return type. + + | Local Type Var Init + -- ^ Stack allocation. The type parameter is not a reference at this point; + -- references are allocated separately to the stack-allocated data. + + | RefCopy Type Expr Expr + -- ^ Ref copy. Copy the second variable reference to the fist (like + -- memcopy). The type is the dereferenced value of the variables. + + | AllocRef Type Var Name + -- ^ Reference allocation. The type parameter is not a reference, but the + -- referenced type. + + | Loop Var Expr LoopIncr Block + -- ^ Looping: arguments are the loop variable, start value, + -- break condition (for increment or decrement), and block. + + | Forever Block + -- ^ Nonterminting loop + + | Break + -- ^ Break out of a loop + + deriving (Show, Eq, Ord) + +data LoopIncr + = IncrTo Expr + | DecrTo Expr + deriving (Show, Eq, Ord) + +data Name + = NameSym Sym + | NameVar Var + deriving (Show, Eq, Ord) + + +-- Conditions ------------------------------------------------------------------ + +data Cond + = CondBool Expr + -- ^ Boolean Expressions + + | CondDeref Type Expr Var Cond + -- ^ Dereference introduction. The type is the type of the dereferenced + -- thing, not the reference itself. + deriving (Show, Eq, Ord) + + +-- Pre-conditions -------------------------------------------------------------- + +newtype Require = Require + { getRequire :: Cond + } deriving (Show, Eq, Ord) + + +-- Post-conditions ------------------------------------------------------------- + +-- | Ensure statements describe properties of the return value for the function +-- they annotate. The return value is referenced through the special internal +-- variable, "retval". +newtype Ensure = Ensure + { getEnsure :: Cond + } deriving (Show, Eq, Ord) + + +-- Expressions ----------------------------------------------------------------- + +data Expr + = ExpSym Sym + -- ^ Symbols + + | ExpVar Var + -- ^ Variables + + | ExpLit Literal + -- ^ Literals + + | ExpLabel Type Expr String + -- ^ Struct label indexing. + + | ExpIndex Type Expr Type Expr + -- ^ Array indexing. The type is the type of the array being indexed, it's + -- implied that the expression with the array in it is a reference. + + | ExpToIx Expr Integer + -- ^ Cast from an expression to an index (Ix) used in loops and array + -- indexing. The Integer is the maximum bound. + + | ExpSafeCast Type Expr + -- ^ Type-safe casting. The type is the type casted from. + + | ExpOp ExpOp [Expr] + -- ^ Primitive expression operators + + | ExpAddrOfGlobal Sym + -- ^ Take the address of a global memory area, introduced through a MemArea + -- *only*. + + | ExpMaxMin Bool + -- ^ True is max value, False is min value for the type. + + deriving (Show, Eq, Ord) + + +-- Expression Operators -------------------------------------------------------- + +data ExpOp + = ExpEq Type + | ExpNeq Type + | ExpCond + + | ExpGt Bool Type + -- ^ True is >=, False is > + | ExpLt Bool Type + -- ^ True is <=, False is < + + | ExpNot + | ExpAnd + | ExpOr + + | ExpMul + | ExpAdd + | ExpSub + | ExpNegate + | ExpAbs + | ExpSignum + + | ExpDiv + | ExpMod + | ExpRecip + + | ExpFExp + | ExpFSqrt + | ExpFLog + | ExpFPow + | ExpFLogBase + | ExpFSin + | ExpFTan + | ExpFCos + | ExpFAsin + | ExpFAtan + | ExpFAcos + | ExpFSinh + | ExpFTanh + | ExpFCosh + | ExpFAsinh + | ExpFAtanh + | ExpFAcosh + + | ExpIsNan Type + | ExpIsInf Type + | ExpRoundF + | ExpCeilF + | ExpFloorF + + | ExpToFloat Type + | ExpFromFloat Type -- ^ Truncate towards zero. + + | ExpBitAnd + | ExpBitOr + | ExpBitXor + | ExpBitComplement + | ExpBitShiftL + | ExpBitShiftR + + deriving (Show, Eq, Ord) + +instance Num Expr where + l * r = ExpOp ExpMul [l,r] + l + r = ExpOp ExpAdd [l,r] + l - r = ExpOp ExpSub [l,r] + abs e = ExpOp ExpAbs [e] + signum e = ExpOp ExpSignum [e] + negate e = ExpOp ExpNegate [e] + fromInteger i = ExpLit (LitInteger i) + +instance Bounded Expr where + minBound = ExpMaxMin False + maxBound = ExpMaxMin True + +instance Fractional Expr where + l / r = ExpOp ExpDiv [l,r] + recip a = ExpOp ExpRecip [a] + fromRational = error "fromRational not implemented for Expr" + +instance Floating Expr where + pi = error "pi not implemented for Expr" + exp e = ExpOp ExpFExp [e] + sqrt e = ExpOp ExpFSqrt [e] + log e = ExpOp ExpFLog [e] + a ** b = ExpOp ExpFPow [a,b] + logBase a b = ExpOp ExpFLogBase [a,b] + sin e = ExpOp ExpFSin [e] + tan e = ExpOp ExpFTan [e] + cos e = ExpOp ExpFCos [e] + asin e = ExpOp ExpFAsin [e] + atan e = ExpOp ExpFAtan [e] + acos e = ExpOp ExpFAcos [e] + sinh e = ExpOp ExpFSinh [e] + tanh e = ExpOp ExpFTanh [e] + cosh e = ExpOp ExpFCosh [e] + asinh e = ExpOp ExpFAsinh [e] + atanh e = ExpOp ExpFAtanh [e] + acosh e = ExpOp ExpFAcosh [e] + + +-- Literals -------------------------------------------------------------------- + +data Literal + = LitInteger Integer + | LitFloat Float + | LitDouble Double + | LitChar Char + | LitBool Bool + | LitNull + | LitString String + deriving (Show, Eq, Ord) + + +-- Initializers ---------------------------------------------------------------- + +-- | An initializer with no 'InitExpr' fields corresponds to @{0}@. +zeroInit :: Init +zeroInit = InitZero + +data Init + = InitZero -- ^ @ {} @ + | InitExpr Type Expr -- ^ @ expr @ + | InitStruct [(String,Init)] -- ^ @ { .f1 = i1, ..., .fn = in } @ + | InitArray [Init] -- ^ @ { i1, ..., in } @ + deriving (Show, Eq, Ord) + + +-- TH Lifting ------------------------------------------------------------------ + +deriveLiftMany + [ ''Module, ''Visible, ''AreaImport, ''Area, ''Struct + , ''Import + , ''Proc, ''Ensure, ''Require, ''Cond + , ''Extern, ''Set.Set + + , ''Name + , ''Stmt, ''LoopIncr + , ''Expr, ''ExpOp, ''Literal, ''Init + ] + +instance Lift Double where + lift = lift . toRational + +instance Lift Float where + lift = lift . toRational diff --git a/src/Ivory/Language/Syntax/Names.hs b/src/Ivory/Language/Syntax/Names.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Syntax/Names.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE TemplateHaskell #-} + +module Ivory.Language.Syntax.Names where + +import Language.Haskell.TH.Lift (deriveLiftMany) + + +-- Public Symbols -------------------------------------------------------------- + +-- | Symbol names. +type Sym = String + + +-- Names ----------------------------------------------------------------------- + +-- | Variable names. +data Var + = VarName String + -- ^ Names + | VarInternal String + -- ^ Internal names + | VarLitName String + -- ^ A literal name that should not be mangled + deriving (Show,Eq,Ord) + + +-- Special Names --------------------------------------------------------------- + +-- | The name for the return value named in an ensures statement. +retval :: Var +retval = VarInternal "retval" + + +-- TH Lifting ------------------------------------------------------------------ + +deriveLiftMany [ ''Var ] diff --git a/src/Ivory/Language/Syntax/Type.hs b/src/Ivory/Language/Syntax/Type.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Syntax/Type.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE TemplateHaskell #-} + +module Ivory.Language.Syntax.Type where + +import Language.Haskell.TH.Lift (deriveLiftMany) + + +-- Types ----------------------------------------------------------------------- + +data Type + = TyVoid -- ^ Unit type + | TyInt IntSize -- ^ Signed ints + | TyWord WordSize -- ^ Unsigned ints + | TyBool -- ^ Booleans + | TyChar -- ^ Characters + | TyFloat -- ^ Floats + | TyDouble -- ^ Doubles + | TyProc Type [Type] -- ^ Procedures + | TyRef Type -- ^ References + | TyConstRef Type -- ^ Constant References + | TyPtr Type -- ^ Pointers + | TyArr Int Type -- ^ Arrays + | TyStruct String -- ^ Structures + | TyCArray Type -- ^ C Arrays + | TyOpaque -- ^ Opaque type---not implementable. + deriving (Show, Eq, Ord) + + +data IntSize + = Int8 + | Int16 + | Int32 + | Int64 + deriving (Show,Eq,Ord) + + +data WordSize + = Word8 + | Word16 + | Word32 + | Word64 + deriving (Show,Eq,Ord) + + +data Typed a = Typed + { tType :: Type + , tValue :: a + } deriving (Show,Functor,Eq,Ord) + + +-- TH Lifting ------------------------------------------------------------------ + +deriveLiftMany [ ''Type, ''IntSize, ''WordSize, ''Typed ] diff --git a/src/Ivory/Language/Type.hs b/src/Ivory/Language/Type.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Type.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} + +module Ivory.Language.Type where + +import Ivory.Language.Proxy +import qualified Ivory.Language.Syntax as AST + +-- Ivory Types ----------------------------------------------------------------- + +-- | The connection between haskell and ivory types. +class IvoryType t where + ivoryType :: Proxy t -> AST.Type + +-- void +instance IvoryType () where + ivoryType _ = AST.TyVoid + +-- | Lifting a variable name. +class IvoryType t => IvoryVar t where + wrapVar :: AST.Var -> t + unwrapExpr :: t -> AST.Expr + +-- | Unwrapping for ivory expressions. +class IvoryVar t => IvoryExpr t where + wrapExpr :: AST.Expr -> t + +-- Utilities ------------------------------------------------------------------- + +-- XXX do not export +wrapVarExpr :: IvoryExpr t => AST.Var -> t +wrapVarExpr = wrapExpr . AST.ExpVar + +-- XXX do not export +typedExpr :: forall t. IvoryVar t => t -> AST.Typed AST.Expr +typedExpr t = AST.Typed + { AST.tType = ivoryType (Proxy :: Proxy t) + , AST.tValue = unwrapExpr t + } + +-- XXX do not export +exprBinop :: IvoryExpr a => (AST.Expr -> AST.Expr -> AST.Expr) -> (a -> a -> a) +exprBinop k x y = wrapExpr (k (unwrapExpr x) (unwrapExpr y)) + +-- XXX do not export +exprUnary :: IvoryExpr a => (AST.Expr -> AST.Expr) -> (a -> a) +exprUnary k x = wrapExpr (k (unwrapExpr x)) + +-- Proxy Type ------------------------------------------------------------------ + +-- | An opaque type that can never be implemented. +data OpaqueType = OpaqueType + +instance IvoryType OpaqueType where + ivoryType _ = AST.TyOpaque diff --git a/src/Ivory/Language/Uint.hs b/src/Ivory/Language/Uint.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Language/Uint.hs @@ -0,0 +1,134 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE DataKinds #-} + +module Ivory.Language.Uint where + +import Ivory.Language.Area +import Ivory.Language.BoundedInteger +import Ivory.Language.SizeOf +import Ivory.Language.Type +import qualified Ivory.Language.Syntax as I + +import Data.Word (Word8,Word16,Word32,Word64) + + +-- Unsigned Types -------------------------------------------------------------- + +-- | 8-bit words. +newtype Uint8 = Uint8 { getUint8 :: I.Expr } + +instance IvoryType Uint8 where + ivoryType _ = I.TyWord I.Word8 + +instance IvoryVar Uint8 where + wrapVar = wrapVarExpr + unwrapExpr = getUint8 + +instance IvoryExpr Uint8 where + wrapExpr = Uint8 + +instance IvorySizeOf (Stored Uint8) where + sizeOfBytes _ = 1 + +instance Num Uint8 where + (*) = exprBinop (*) + (+) = exprBinop (+) + (-) = exprBinop (-) + abs = id + signum = exprUnary signum + negate = exprUnary negate + fromInteger = boundedFromInteger Uint8 (0 :: Word8) + +instance Bounded Uint8 where + minBound = 0 + maxBound = wrapExpr (I.ExpMaxMin True) + + +-- | 16-bit words. +newtype Uint16 = Uint16 { getUint16 :: I.Expr } + +instance IvoryType Uint16 where + ivoryType _ = I.TyWord I.Word16 + +instance IvoryVar Uint16 where + wrapVar = wrapVarExpr + unwrapExpr = getUint16 + +instance IvoryExpr Uint16 where + wrapExpr = Uint16 + +instance IvorySizeOf (Stored Uint16) where + sizeOfBytes _ = 2 + +instance Num Uint16 where + (*) = exprBinop (*) + (+) = exprBinop (+) + (-) = exprBinop (-) + abs = id + signum = exprUnary signum + negate = exprUnary negate + fromInteger = boundedFromInteger Uint16 (0 :: Word16) + +instance Bounded Uint16 where + minBound = 0 + maxBound = wrapExpr (I.ExpMaxMin True) + + +-- | 32-bit words. +newtype Uint32 = Uint32 { getUint32 :: I.Expr } + +instance IvoryType Uint32 where + ivoryType _ = I.TyWord I.Word32 + +instance IvoryVar Uint32 where + wrapVar = wrapVarExpr + unwrapExpr = getUint32 + +instance IvoryExpr Uint32 where + wrapExpr = Uint32 + +instance IvorySizeOf (Stored Uint32) where + sizeOfBytes _ = 4 + +instance Num Uint32 where + (*) = exprBinop (*) + (+) = exprBinop (+) + (-) = exprBinop (-) + abs = id + signum = exprUnary signum + negate = exprUnary negate + fromInteger = boundedFromInteger Uint32 (0 :: Word32) + +instance Bounded Uint32 where + minBound = 0 + maxBound = wrapExpr (I.ExpMaxMin True) + + +-- | 64-bit words. +newtype Uint64 = Uint64 { getUint64 :: I.Expr } + +instance IvoryType Uint64 where + ivoryType _ = I.TyWord I.Word64 + +instance IvoryVar Uint64 where + wrapVar = wrapVarExpr + unwrapExpr = getUint64 + +instance IvoryExpr Uint64 where + wrapExpr = Uint64 + +instance IvorySizeOf (Stored Uint64) where + sizeOfBytes _ = 8 + +instance Num Uint64 where + (*) = exprBinop (*) + (+) = exprBinop (+) + (-) = exprBinop (-) + abs = id + signum = exprUnary signum + negate = exprUnary negate + fromInteger = boundedFromInteger Uint64 (0 :: Word64) + +instance Bounded Uint64 where + minBound = 0 + maxBound = wrapExpr (I.ExpMaxMin True)