Merge pull request #5 from distrap/cleanupAndCi

Cleanup and CI updates

.github/workflows/ci.yaml

@@ -37,9 +37,10 @@ jobs:
     strategy:
       matrix:
         cabal:
-          - '3.4'
+          - '3.6'
         ghc:
           - '8.10.7'
+          - '9.0.2'
 name: Haskell CI
 on:
   - push

ci.dhall

@@ -8,8 +8,8 @@ in    haskellCi.generalCi
           # haskellCi.matrixSteps
         )
         ( Some
-            { ghc = [ haskellCi.GHC.GHC8107 ]
-            , cabal = [ haskellCi.Cabal.Cabal34 ]
+            { ghc = [ haskellCi.GHC.GHC8107, haskellCi.GHC.GHC902 ]
+            , cabal = [ haskellCi.Cabal.Cabal36 ]
             }
         )
     : haskellCi.CI.Type

ivory-model-check/src/Ivory/ModelCheck/Ivory2CVC4.hs

@@ -59,8 +59,8 @@ modelCheckProc mods p = do
 toArea :: I.Area -> ModelCheck ()
 toArea I.Area { I.areaSym   = sym
               , I.areaType  = ty
-              , I.areaInit  = init
-              , I.areaAttrs = []
+              , I.areaInit  = _init
+              , I.areaAttrs = _attrs
               }
   = void $ addEnvVar ty sym
 

ivory-opts/src/Ivory/Opts/CFG.hs

@@ -242,7 +242,6 @@ cfg m = G.insEdges (concatMap go nodes) $ G.insNodes nodes G.empty
                 | ((i,p):_) <- ls
                 , procSym p == sym = Just i
                 | (_:ls') <- ls    = lookup ls' sym
-                | otherwise        = error "Unreachable in cfg" -- To make GHC happy.
 
 -- | Just label the nodes with the function names.
 procSymGraph :: CFG -> G.Gr CallNm ()

ivory/src/Ivory/Language/Area.hs

@@ -10,12 +10,13 @@ import Ivory.Language.Proxy
 import Ivory.Language.Type
 import qualified Ivory.Language.Syntax as I
 
+import Data.Kind (Type)
 import GHC.TypeLits (Nat, Symbol)
 
 -- Memory Areas ----------------------------------------------------------------
 
 -- | Type proxies for @Area@s.
-type AProxy a = Proxy (a :: Area *)
+type AProxy a = Proxy (a :: Area Type)
 
 -- | The kind of memory-area types.
 data Area k
@@ -26,7 +27,7 @@ data Area 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
+class IvoryArea (a :: Area Type) where
   ivoryArea :: Proxy a -> I.Type
 
 instance (ANat len, IvoryArea area)

ivory/src/Ivory/Language/BitData/Array.hs

@@ -14,13 +14,15 @@
 
 module Ivory.Language.BitData.Array where
 
+import Data.Kind (Type)
+import GHC.TypeLits(Nat)
+
 import Ivory.Language.Bits
 import Ivory.Language.Proxy
 
 import Ivory.Language.BitData.Bits
 import Ivory.Language.BitData.BitData
 
-import GHC.TypeLits(Nat)
 
 -- NOTE: This type family is used to calculate the total size of a bit
 -- array by multiplying "n" by the size of "a" in bits.  Once we have
@@ -29,7 +31,7 @@ import GHC.TypeLits(Nat)
 -- The quasiquoter may generate multiple instances of "ArraySize" with
 -- the same "n", "a" and result, which is allowed by the type family
 -- overlapping rules.  It does seem like a bit of a hack though.
-type family ArraySize (n :: Nat) (a :: *) :: Nat
+type family ArraySize (n :: Nat) (a :: Type) :: Nat
 
 -- | An array of "n" bit data elements of type "a".
 data BitArray (n :: Nat) a = BitArray { unArray :: Bits (ArraySize n a) }

ivory/src/Ivory/Language/BitData/BitData.hs

@@ -14,6 +14,7 @@
 
 module Ivory.Language.BitData.BitData where
 
+import Data.Kind (Type)
 import Ivory.Language.Bits
 import Ivory.Language.Proxy
 import Ivory.Language.Cast
@@ -27,7 +28,7 @@ class (ANat (BitSize (BitType a)),
        BitType a ~ Bits (BitSize (BitType a))) => BitData a where
   -- | Return the base "(Bits n)" type as defined in the "bitdata"
   -- quasiquoter.
-  type BitType a :: *
+  type BitType a :: Type
 
   -- | Convert a bit data type to its raw bit value.  This is always
   -- well defined and should be exported.

ivory/src/Ivory/Language/BitData/Bits.hs

@@ -18,6 +18,7 @@
 
 module Ivory.Language.BitData.Bits where
 
+import Data.Kind (Type)
 import GHC.TypeLits
 import Ivory.Language.Uint
 import Ivory.Language.Bits
@@ -35,7 +36,7 @@ import Ivory.Language.BitData.DefBitRep
 -- | Type function: "BitRep (n :: Nat)" returns an Ivory type given a
 -- bit size as a type-level natural.  Instances of this type family
 -- for bits [1..64] are generated using Template Haskell.
-type family BitRep (n :: Nat) :: *
+type family BitRep (n :: Nat) :: Type
 
 defBitRep ''BitRep ''Uint8  [1..8]
 defBitRep ''BitRep ''Uint16 [9..16]

ivory/src/Ivory/Language/CArray.hs

@@ -9,6 +9,7 @@
 
 module Ivory.Language.CArray where
 
+import Data.Kind (Type)
 import Ivory.Language.Area
 import Ivory.Language.Proxy
 import Ivory.Language.Ref
@@ -24,7 +25,7 @@ instance IvoryArea a => IvoryArea ('CArray a) where
 
 -- | Guard invocations of toCArray.
 class (IvoryArea area, IvoryArea rep)
-  => ToCArray (area :: Area *) (rep :: Area *) | area -> rep
+  => ToCArray (area :: Area Type) (rep :: Area Type) | area -> rep
 
 instance (ANat len, ToCArray area rep)
     => ToCArray ('Array len area) ('CArray rep)

ivory/src/Ivory/Language/Init.hs

@@ -28,7 +28,7 @@ import           Ivory.Language.Type
 import           Ivory.Language.Uint
 
 import           Control.Monad          (forM_)
-
+import           Data.Kind              (Type)
 import           GHC.TypeLits           (Symbol)
 
 -- Initializers ----------------------------------------------------------------
@@ -49,11 +49,11 @@ initType (IArray  ty _ _) = ty
 initType (IStruct ty _)   = ty
 initType (IFresh  ty _ _) = ty
 
-newtype Init (area :: Area *) = Init { getInit :: XInit }
+newtype Init (area :: Area Type) = Init { getInit :: XInit }
 
 -- | Zero initializers. The semantics of Ivory is that initializers must be
 -- compatible with C semantics of initializing to 0 for globals in .bss.
-class IvoryZero (area :: Area *) where
+class IvoryZero (area :: Area Type) where
   izero :: Init area
 
 -- | Zero the memory pointed to by this reference, as long as it could have been

ivory/src/Ivory/Language/MemArea.hs

@@ -7,6 +7,8 @@
 
 module Ivory.Language.MemArea where
 
+import Data.Kind (Type)
+
 import Ivory.Language.Area
 import Ivory.Language.Init
 import Ivory.Language.Proxy
@@ -69,7 +71,7 @@ areaInit s ini = runAreaInitM s (runInit (getInit ini))
 -- Memory Areas ----------------------------------------------------------------
 
 -- | Externally defined memory areas.
-data MemArea (area :: Area *)
+data MemArea (area :: Area Type)
   = MemImport I.AreaImport
   | MemArea I.Area [I.Area]
   deriving (Eq, Show)
@@ -100,10 +102,11 @@ makeArea sym isConst ty ini = I.Area
   }
 
 setAreaAttributes :: [I.AreaAttribute] -> I.Area -> I.Area
-setAreaAttributes attrs area = area { I.areaAttrs = attrs }
+setAreaAttributes attrs area' = area' { I.areaAttrs = attrs }
 
 setMemAreaAttributes :: [I.AreaAttribute] -> MemArea area -> MemArea area
 setMemAreaAttributes attrs (MemArea a1 as) = MemArea (setAreaAttributes attrs a1) as
+setMemAreaAttributes _ memImport = memImport
 
 -- | Define a global constant. Requires an IvoryZero constraint to ensure the
 -- area has an initializers, but does not explicilty initialize to 0 so that the
@@ -132,7 +135,7 @@ importArea name header = MemImport I.AreaImport
 
 -- Constant Memory Areas -------------------------------------------------------
 
-newtype ConstMemArea (area :: Area *) = ConstMemArea (MemArea area)
+newtype ConstMemArea (area :: Area Type) = ConstMemArea (MemArea area)
 
 -- | Constant memory area definition.
 constArea :: forall area. IvoryArea area
@@ -155,7 +158,7 @@ importConstArea name header = ConstMemArea $ MemImport I.AreaImport
 -- Area Usage ------------------------------------------------------------------
 
 -- | Turn a memory area into a reference.
-class IvoryAddrOf (mem :: Area * -> *) ref | mem -> ref, ref -> mem  where
+class IvoryAddrOf (mem :: Area Type -> Type) ref | mem -> ref, ref -> mem  where
   addrOf :: IvoryArea area => mem area -> ref 'Global area
 
 -- XXX do not export

ivory/src/Ivory/Language/Pointer.hs

@@ -31,6 +31,8 @@ import           Ivory.Language.Type
                  (IvoryExpr, IvoryType, IvoryVar, ivoryType, unwrapExpr,
                   wrapExpr, wrapVar, wrapVarExpr)
 
+import qualified Data.Kind
+
 -- * Nullability
 data Nullability
   = Nullable -- ^ may be NULL
@@ -60,7 +62,7 @@ instance KnownConstancy 'Mutable where
   demoteConstancy _ = Mutable
 
 -- * Generic Pointer
-data Pointer (n :: Nullability) (c :: Constancy) (s :: RefScope) (a :: Area *) = Pointer
+data Pointer (n :: Nullability) (c :: Constancy) (s :: RefScope) (a :: Area Data.Kind.Type) = Pointer
   { getPointer :: Expr
   }
 
@@ -99,7 +101,7 @@ nullPtr = Pointer (ExpLit LitNull)
 -- | Safe pointer casting. Only defined if conversion is safe.
 class PointerCast n1 c1 n2 c2 where
   pointerCast
-    :: forall (s :: RefScope) (a :: Area *).
+    :: forall (s :: RefScope) (a :: Area Data.Kind.Type).
        IvoryArea a
     => Pointer n1 c1 s a -> Pointer n2 c2 s a
 

ivory/src/Ivory/Language/Proc.hs

@@ -14,22 +14,23 @@
 
 module Ivory.Language.Proc where
 
+import Data.Kind (Type)
+
 import Ivory.Language.Monad
 import Ivory.Language.Proxy
 import Ivory.Language.Type
 import Ivory.Language.Effects
 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
 
 -- | Typeclass for procedure types, parametrized over the C procedure's
 -- signature, to produce a value representing their signature.
-class ProcType (sig :: Proc *) where
+class ProcType (sig :: Proc Type) where
 
   -- | Turn a type-level description of the signature into a (return
   -- type, [argument types]) value.
@@ -52,7 +53,7 @@ instance (IvoryType a, ProcType (args ':-> r))
 -- Function Pointers -----------------------------------------------------------
 
 -- | Procedure pointers
-newtype ProcPtr (sig :: Proc *) = ProcPtr { getProcPtr :: AST.Name }
+newtype ProcPtr (sig :: Proc Type) = ProcPtr { getProcPtr :: AST.Name }
 
 instance ProcType proc => IvoryType (ProcPtr proc) where
   ivoryType _ = AST.TyProc r args
@@ -72,7 +73,7 @@ procPtr  = ProcPtr . defSymbol
 -- Function Symbols ------------------------------------------------------------
 
 -- | Procedure definitions.
-data Def (proc :: Proc *)
+data Def (proc :: Proc Type)
   = DefProc AST.Proc
   | DefImport AST.Import
     deriving (Show, Eq, Ord)
@@ -156,7 +157,7 @@ data Definition = Defined CodeBlock
 --   value, or else a Haskell function type whose arguments correspond
 --   to the C arguments and whose return type is @Body r@ on the return
 --   type @r@.
-class ProcType proc => IvoryProcDef (proc :: Proc *) impl | impl -> proc where
+class ProcType proc => IvoryProcDef (proc :: Proc Type) impl | impl -> proc where
   procDef :: Closure -> Proxy proc -> impl -> ([AST.Var], Definition)
 
 -- Base case: No arguments in C signature
@@ -253,7 +254,7 @@ indirect ptr = callAux (getProcPtr ptr) (Proxy :: Proxy proc) []
 -- 'IvoryProcDef'), parameter 'eff' is the effect context (which
 -- remains unchanged through the calls here), and parameter 'impl', as
 -- in 'IvoryProcDef', is the implementation type.
-class IvoryCall (proc :: Proc *) (eff :: E.Effects) impl
+class IvoryCall (proc :: Proc Type) (eff :: E.Effects) impl
     | proc eff -> impl, impl -> eff where
 
   -- | Recursive helper call.  'proc' encodes a C procedure type, and
@@ -302,7 +303,7 @@ indirect_ ptr = callAux_ (getProcPtr ptr) (Proxy :: Proxy proc) []
 
 -- | Typeclass for something callable in Ivory without a return value
 -- needed.  This is otherwise identical to 'IvoryCall'.
-class IvoryCall_ (proc :: Proc *) (eff :: E.Effects) impl
+class IvoryCall_ (proc :: Proc Type) (eff :: E.Effects) impl
     | proc eff -> impl, impl -> eff
   where
   callAux_ :: AST.Name -> Proxy proc -> [AST.Typed AST.Expr] -> impl

ivory/src/Ivory/Language/Proxy.hs

@@ -20,11 +20,12 @@ module Ivory.Language.Proxy
   , fromTypeSym
   ) where
 
+import Data.Kind    (Type)
 import Data.Proxy   (Proxy (..))
 import GHC.TypeLits (KnownNat, KnownSymbol, Nat, Symbol, natVal, symbolVal)
 
 -- | Type proxies for * types.
-type SProxy a = Proxy (a :: *)
+type SProxy a = Proxy (a :: Type)
 
 type ANat    n = KnownNat n
 type NatType n = Proxy n

ivory/src/Ivory/Language/Ref.hs

@@ -37,6 +37,7 @@ import Ivory.Language.Scope
 import qualified Ivory.Language.Syntax as I
 import Ivory.Language.Type
 
+import Data.Kind (Type)
 
 -- References ------------------------------------------------------------------
 
@@ -55,7 +56,7 @@ type ConstRef = Pointer 'Valid 'Const
 -- Dereferencing ---------------------------------------------------------------
 
 -- | TODO remove class, leave function only
-class IvoryRef (ref :: RefScope -> Area * -> *) where
+class IvoryRef (ref :: RefScope -> Area Type -> Type) where
   unwrapRef
     :: IvoryVar a
     => ref s ('Stored a) -> I.Expr

ivory/src/Ivory/Language/SizeOf.hs

@@ -3,12 +3,14 @@
 
 module Ivory.Language.SizeOf where
 
+import Data.Kind (Type)
+
 import Ivory.Language.Area
 import Ivory.Language.Proxy
 import qualified Ivory.Language.Syntax as AST
 import Ivory.Language.Type
 
-class IvorySizeOf (t :: Area *) where
+class IvorySizeOf (t :: Area Type) where
 
 instance IvorySizeOf ('Struct sym) where
 instance (ANat len, IvorySizeOf area) => IvorySizeOf ('Array len area) where

ivory/src/Ivory/Language/Struct.hs

@@ -14,6 +14,7 @@ import Ivory.Language.Ref
 import Ivory.Language.Type(IvoryExpr(..), IvoryVar(..))
 import qualified Ivory.Language.Syntax as I
 
+import Data.Kind(Type)
 import GHC.TypeLits(Symbol)
 
 -- Structs ---------------------------------------------------------------------
@@ -23,16 +24,16 @@ instance (IvoryStruct sym, ASymbol sym) => IvoryArea ('Struct sym) where
 
 newtype StructDef (sym :: Symbol) = StructDef { getStructDef :: I.Struct }
 
-type family StructName (a :: Area *) :: Symbol
+type family StructName (a :: Area Type) :: Symbol
 type instance StructName ('Struct sym) = sym
 
 class (IvoryArea ('Struct sym), ASymbol sym) => IvoryStruct (sym :: Symbol) where
   structDef :: StructDef sym
 
 -- | Struct field labels.
-newtype Label (sym :: Symbol) (field :: Area *) = Label { getLabel :: String }
+newtype Label (sym :: Symbol) (field :: Area Type) = Label { getLabel :: String }
 
-instance Eq (Label (sym :: Symbol) (field :: Area *)) where
+instance Eq (Label (sym :: Symbol) (field :: Area Type)) where
   l0 == l1 = getLabel l0 == getLabel l1
 
 -- | Label indexing in a structure.