packages feed

ivory (empty) → 0.1.0.0

raw patch · 41 files changed

+3931/−0 lines, 41 filesdep +basedep +containersdep +monadLibsetup-changed

Dependencies added: base, containers, monadLib, parsec, pretty, template-haskell, th-lift

Files

+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ivory.cabal view
@@ -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
+ src/Ivory/Language.hs view
@@ -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((>?),(>=?),(<?),(<=?))++    -- ** Boolean operators+  , iNot, (.&&), (.||)++    -- ** Bit operators+  , IvoryBits((.&),(.|),(.^),iComplement,iShiftL,iShiftR), extractByte+  , BitSplit(lbits, ubits), BitCast(bitCast)++    -- ** External memory areas+  , MemArea(), area, importArea+  , ConstMemArea(), constArea, importConstArea+  , IvoryAddrOf(addrOf)++    -- ** Procedures+  , Def()+  , ProcPtr(), procPtr+  , proc, externProc, importProc+  , Body(), body++    -- *** Pre/Post-Conditions+  , requires+  , checkStored+  , ensures++    -- ** Assumption/Assertion statements+  , assert+  , assume++    -- ** Structures+  , IvoryStruct(..), StructDef(), ivory, (~>), 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
+ src/Ivory/Language/Area.hs view
@@ -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)+
+ src/Ivory/Language/Array.hs view
@@ -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
+ src/Ivory/Language/Assert.hs view
@@ -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))+
+ src/Ivory/Language/Bits.hs view
@@ -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)
+ src/Ivory/Language/BoundedInteger.hs view
@@ -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))
+ src/Ivory/Language/CArray.hs view
@@ -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)))
+ src/Ivory/Language/Cast.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Ivory/Language/Cond.hs view
@@ -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
+ src/Ivory/Language/Const.hs view
@@ -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
+ src/Ivory/Language/Effects.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Ivory/Language/Float.hs view
@@ -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
+ src/Ivory/Language/IBool.hs view
@@ -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 -> a -> IBool+  (<?)   = boolOp (AST.ExpLt False)+  infix 4 <?++  (<=?) :: a -> 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 .||
+ src/Ivory/Language/IChar.hs view
@@ -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
+ src/Ivory/Language/IIntegral.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Ivory/Language/IString.hs view
@@ -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
+ src/Ivory/Language/Init.hs view
@@ -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))
+ src/Ivory/Language/Loop.hs view
@@ -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 <? maxSz .&& (-1::IxRep) <=? wrapExpr v)+  asst from+  asst to+  emit (AST.Loop ix (trans from) (incr $ trans to) (blockStmts block))++upTo :: SingI n+     => 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))
+ src/Ivory/Language/MemArea.hs view
@@ -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)+
+ src/Ivory/Language/Module.hs view
@@ -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
+ src/Ivory/Language/Monad.hs view
@@ -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))+
+ src/Ivory/Language/Proc.hs view
@@ -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
+ src/Ivory/Language/Proxy.hs view
@@ -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
+ src/Ivory/Language/Ptr.hs view
@@ -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
+ src/Ivory/Language/Ref.hs view
@@ -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
+ src/Ivory/Language/Scope.hs view
@@ -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
+ src/Ivory/Language/Sint.hs view
@@ -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)
+ src/Ivory/Language/SizeOf.hs view
@@ -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+
+ src/Ivory/Language/String.hs view
@@ -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)))+
+ src/Ivory/Language/Struct.hs view
@@ -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))
+ src/Ivory/Language/Struct/Parser.hs view
@@ -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 '"')
+ src/Ivory/Language/Struct/Quote.hs view
@@ -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)
+ src/Ivory/Language/Syntax.hs view
@@ -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
+ src/Ivory/Language/Syntax/AST.hs view
@@ -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
+ src/Ivory/Language/Syntax/Names.hs view
@@ -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 ]
+ src/Ivory/Language/Syntax/Type.hs view
@@ -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 ]
+ src/Ivory/Language/Type.hs view
@@ -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
+ src/Ivory/Language/Uint.hs view
@@ -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)