merge ivory : jal-master into master

ivory-backend-c/runtime/ivory_templates.h

@@ -16,7 +16,7 @@
 #define ABS_I                                       \
 static inline TYPE C(abs,EXT)(TYPE i) {             \
   if(i == MKMIN(M)) { return MKMAX(M); }            \
-  else { return i >= 0 ? i : -i; }                  \
+  else { return i >= 0 ? i : (TYPE) -i; }           \
 }
 
 // Unsigned signnum

ivory-backend-c/src/Ivory/Compile/C/Gen.hs

@@ -71,9 +71,10 @@ compileArea visibility area = do
       ty | I.areaConst area = [cty| const $ty:aty |]
          | otherwise        = aty
   case i of
-    I.InitZero -> putSrc [cedecl| $ty:(type' visibility ty) $id:(I.areaSym area) ; |]
-    _          -> putSrc [cedecl| $ty:(type' visibility ty)
-                                 $id:(I.areaSym area) = $init:(toInit i) ; |]
+    I.InitZero    -> putSrc [cedecl| $ty:(type' visibility ty) $id:(I.areaSym area) ; |]
+    I.InitNewType -> putSrc [cedecl| $ty:(type' visibility ty) $id:(I.areaSym area) ; |]
+    _             -> putSrc [cedecl| $ty:(type' visibility ty)
+                                     $id:(I.areaSym area) = $init:(toInit i) ; |]
   where
   type' Public ty' = [cty|$ty:ty'|]
   type' Private ty' = [cty|static $ty:ty'|]
@@ -184,6 +185,7 @@ toTypeCxt arrCase = convert
       [cty| $ty:(convert retTy) (*)
             ($params:(map (toParam . convert) argTys)) |]
     I.TyOpaque            -> error "Opaque type is not implementable."
+    I.TyNewType s         -> [cty| typename $id:s |] 
 
 intSize :: I.IntSize -> C.Type
 intSize I.Int8  = [cty| typename int8_t  |]
@@ -243,6 +245,8 @@ toBody ens stmt =
     I.Deref t var exp      -> [C.BlockDecl
       [cdecl| $ty:(toType t) $id:(toVar var) = $exp:(derefExp (toExpr (I.TyRef t) exp)); |]]
 
+    I.Local t var I.InitNewType   -> [C.BlockDecl
+      [cdecl| $ty:(toType t) $id:(toVar var); |]]
     I.Local t var inits    -> [C.BlockDecl
       [cdecl| $ty:(toType t) $id:(toVar var)
                 = $init:(toInit inits); |]]
@@ -328,6 +332,8 @@ toBody ens stmt =
       [cstm| $comment:("/* " ++ c ++ " */"); |]]
     I.Comment (I.SourcePos src)   -> [C.BlockStm
       [cstm| $comment:("/* " ++ prettyPrint (pretty src) ++ " */"); |]]
+
+
 -- | Return statement.
 typedRet :: I.Typed I.Expr -> C.Exp
 typedRet I.Typed { I.tType  = t
@@ -343,6 +349,7 @@ toInit i = case i of
   I.InitArray is  -> [cinit|{$inits:([ toInit j | j <- is ])}|]
   I.InitStruct fs ->
     C.CompoundInitializer [ (Just (fieldDes f), toInit j) | (f,j) <- fs ] noLoc
+  I.InitNewType   -> error "illegal use of newtype during toInit"
 
 fieldDes :: String -> C.Designation
 fieldDes n = C.Designation [ C.MemberDesignator (C.Id n noLoc) noLoc ] noLoc

ivory-eval/src/Ivory/Eval.hs

@@ -446,6 +446,7 @@ evalInit ty init = case init of
                         zstr inits
            return $ Struct str
          _ -> raise $ "evalInit: InitStruct: unexpected type: " ++ show ty
+  I.InitNewType -> error "illegal use of newtype"
 
 lookupTyped :: (Show a, Eq a) => a -> [I.Typed a] -> I.Type
 lookupTyped a [] = error $ "lookupTyped: couldn't find: " ++ show a

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

@@ -111,6 +111,7 @@ data Type = Void
           | Struct String
           | Array Type
           | Opaque
+          | NewType String
   deriving (Show, Read, Eq)
 
 instance Concrete Type where

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

@@ -208,6 +208,7 @@ toInit ty init =
           Nothing -> error $ "I don't know how to initialize field " ++ f
                           ++ " of struct " ++ s
       return tv
+    I.InitNewType -> error "illegal use of newtype"
   where
   lookupField f (I.Struct _ tfs) = listToMaybe [ t | I.Typed t f' <- tfs, f == f' ]
   lookupField f (I.Abstract _ _) = Nothing
@@ -485,6 +486,7 @@ toType t = case t of
   I.TyCArray t'    -> Array <$> toType t'
   I.TyOpaque       -> return Opaque
   I.TyStruct name  -> return $ Struct name
+  I.TyNewType s    -> return $ NewType s
 
 updateEnvRef :: I.Type -> I.Expr -> ModelCheck Var
 updateEnvRef t ref =

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

@@ -148,6 +148,7 @@ stmtFold ef stmt = case stmt of
   I.Forever blk                   -> do blk' <- runFreshStmts ef blk
                                         insert (I.Forever blk')
   I.Comment _                     -> insert stmt
+
   where
   efTyped (I.Typed ty e) = ef ty e
   efIncr incr = case incr of
@@ -159,6 +160,7 @@ stmtFold ef stmt = case stmt of
     I.InitExpr ty e     -> ef ty e
     I.InitStruct inits  -> mapM_ (efInit . snd) inits
     I.InitArray inits   -> mapM_ efInit inits
+    I.InitNewType       -> return ()
 
 --------------------------------------------------------------------------------
 

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

@@ -157,6 +157,7 @@ data InitF t
   | InitExpr AST.Type t
   | InitStruct [(String, InitF t)]
   | InitArray [InitF t]
+  | InitNewType
   deriving (Show, Eq, Ord, Functor)
 
 instance MuRef AST.Stmt where
@@ -183,6 +184,7 @@ instance MuRef AST.Stmt where
     AST.Comment{} -> pure $ StmtSimple stmt
     where
     mapInit AST.InitZero = pure InitZero
+    mapInit AST.InitNewType = pure InitNewType
     mapInit (AST.InitExpr ty ex) = InitExpr ty <$> child ex
     mapInit (AST.InitStruct fields) = InitStruct <$> traverse (\ (nm, i) -> (,) nm <$> mapInit i) fields
     mapInit (AST.InitArray elements) = InitArray <$> traverse mapInit elements
@@ -222,6 +224,7 @@ toBlock expr block b = case b of
   toInit (InitExpr ty ex) = AST.InitExpr ty <$> expr ex ty
   toInit (InitStruct fields) = AST.InitStruct <$> traverse (\ (nm, i) -> (,) nm <$> toInit i) fields
   toInit (InitArray elements) = AST.InitArray <$> traverse toInit elements
+  toInit InitNewType = pure AST.InitNewType
   toIncr (IncrTo ex) = AST.IncrTo <$> expr ex ixRep
   toIncr (DecrTo ex) = AST.DecrTo <$> expr ex ixRep
 

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

@@ -133,6 +133,7 @@ stmtFold cxt opt stmt =
       copies <- get
       return $ D.singleton $ I.Forever (newFold copies b)
     I.Comment{}          -> return $ D.singleton stmt
+
   where
   newFold copies = D.toList . blockFold cxt opt copies
 
@@ -141,6 +142,7 @@ constFoldInits _ I.InitZero = I.InitZero
 constFoldInits copies (I.InitExpr ty expr) = I.InitExpr ty $ cf copies ty expr
 constFoldInits copies (I.InitStruct i) = I.InitStruct $ map (second (constFoldInits copies)) i
 constFoldInits copies (I.InitArray i) = I.InitArray $ map (constFoldInits copies) i
+constFoldInits _ I.InitNewType = I.InitNewType
 
 --------------------------------------------------------------------------------
 -- Expressions

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

@@ -312,6 +312,8 @@ instance Pretty I.Type where
       -> text "CArray" <+> pretty t
     I.TyOpaque
       -> text "Opaque"
+    I.TyNewType s
+      -> text ("Newtype " ++ s)
 
 --------------------------------------------------------------------------------
 -- Unused for now.

ivory-quickcheck/src/Ivory/QuickCheck.hs

@@ -192,11 +192,12 @@ sampleType m t = case t of
     -> sampleArray m len ty
   I.TyStruct ty
     -> sampleStruct m ty
-  I.TyProc _ _ -> err 
-  I.TyVoid     -> err 
-  I.TyPtr _    -> err 
-  I.TyCArray _ -> err 
-  I.TyOpaque   -> err
+  I.TyProc _ _    -> err 
+  I.TyVoid        -> err 
+  I.TyPtr _       -> err 
+  I.TyCArray _    -> err 
+  I.TyOpaque      -> err
+  I.TyNewType _   -> err
   where
   err = error $ "I don't know how to make values of type '" ++ show t ++ "'!"
 

ivory/src/Ivory/Language.hs

@@ -29,7 +29,7 @@ module Ivory.Language (
   , IvoryZeroVal(izeroval)
   , IvoryZero(izero)
   , iarray
-  , InitStruct(), (.=), istruct
+  , InitStruct(), (.=), istruct, inewtype
   , local
 
     -- ** SizeOf

ivory/src/Ivory/Language/Coroutine.hs

@@ -524,6 +524,7 @@ updateInit (AST.InitStruct fields) =
 updateInit (AST.InitArray elems) =
   -- An 'AST.InitArray' is a list of 'AST.Init' which we must recurse over:
   AST.InitArray <$> mapM updateInit elems
+updateInit AST.InitNewType = return AST.InitNewType
 
 -- | Basically 'updateExpr', but on a typed expression.
 updateTypedExpr :: AST.Typed AST.Expr -> UpdateExpr (AST.Typed AST.Expr)

ivory/src/Ivory/Language/Init.hs

@@ -43,13 +43,15 @@ data XInit
   | IArray    I.Type [XInit]
   | IStruct   I.Type [(String, XInit)]
   | IFresh    I.Type XInit (I.Var -> I.Init)
+  | INewType
 
 -- | 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
+initType (INewType) = error "illegal use of inewtype"
 
 newtype Init (area :: Area *) = Init { getInit :: XInit }
 
@@ -110,6 +112,8 @@ runInit ini =
       let ty     = initType i
       let aux'   = aux ++ [Binding var ty i']
       return (f var, aux')
+    INewType -> do
+      return (I.InitNewType, [])
   where
     iniStruct (s, i) = do
       (i', binds) <- runInit i
@@ -161,6 +165,9 @@ instance IvoryZeroVal Sint64   where izeroval = ival 0
 instance IvoryZeroVal IFloat   where izeroval = ival 0
 instance IvoryZeroVal IDouble  where izeroval = ival 0
 
+inewtype :: (ASymbol sym) => Init ('Stored (NewType sym))
+inewtype = Init (INewType)
+
 instance (ANat n) => IvoryZeroVal (Ix n) where
   izeroval = ival 0
 

ivory/src/Ivory/Language/Monad.hs

@@ -83,10 +83,15 @@ instance Monoid CodeBlock where
 --
 -- XXX do not export
 runIvory :: Ivory (E.ProcEffects s r) a -> (a,CodeBlock)
-runIvory b = primRunIvory b
+runIvory b = fst $ primRunIvory 0 b
+
+-- | Run an Ivory block computation that could require any effect, and provide a fresh 
+--   variable supply. The function returns the fresh variable supply at the end of the computation.
+--
+-- XXX do not export
+primRunIvory :: Int -> Ivory (E.ProcEffects s r) a -> ((a,CodeBlock),Int)
+primRunIvory n m = (MonadLib.runM (unIvory m) n)
 
-primRunIvory :: Ivory (E.ProcEffects s r) a -> (a,CodeBlock)
-primRunIvory m = fst (MonadLib.runM (unIvory m) 0)
 
 -- | Collect the 'CodeBlock' for an Ivory computation.
 --

ivory/src/Ivory/Language/Proc.hs

@@ -161,7 +161,7 @@ class ProcType proc => IvoryProcDef (proc :: Proc *) impl | impl -> proc where
 
 -- Base case: No arguments in C signature
 instance IvoryType ret => IvoryProcDef ('[] ':-> ret) (Body ret) where
-  procDef env _ b = (getEnv env, Defined (snd (primRunIvory (runBody b))))
+  procDef env _ b = (getEnv env, Defined (snd (runIvory (runBody b))))
 
 -- Inductive case: Remove first argument from C signature, and
 -- parametrize 'impl' over another argument of the same type.
@@ -232,7 +232,7 @@ importFrom h = ImportFrom (return h)
 instance IvoryType ret => IvoryProcDef ('[] ':-> ret) (ImportFrom ret) where
   procDef env _ b = (getEnv env, Imported header reqs ens)
     where
-    (header, block) = primRunIvory (runImportFrom b)
+    (header, block) = runIvory (runImportFrom b)
     reqs            = blockRequires block
     ens             = blockEnsures block
 

ivory/src/Ivory/Language/Syntax/AST.hs

@@ -440,6 +440,7 @@ data Init
   | InitExpr Type Expr         -- ^ @ expr @
   | InitStruct [(String,Init)] -- ^ @ { .f1 = i1, ..., .fn = in } @
   | InitArray [Init]           -- ^ @ { i1, ..., in } @
+  | InitNewType                -- ^ @ Nothing @
     deriving (Show, Eq, Ord)
 
 

ivory/src/Ivory/Language/Syntax/Type.hs

@@ -9,22 +9,23 @@ import Language.Haskell.TH.Lift (deriveLiftMany)
 -- Types -----------------------------------------------------------------------
 
 data Type
-  = TyVoid             -- ^ Unit type
-  | TyInt IntSize      -- ^ Signed ints
-  | TyWord WordSize    -- ^ Unsigned ints
-  | TyIndex Integer    -- ^ Indices with an upper bound
-  | 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.
+  = TyVoid                -- ^ Unit type
+  | TyInt IntSize         -- ^ Signed ints
+  | TyWord WordSize       -- ^ Unsigned ints
+  | TyIndex Integer       -- ^ Indices with an upper bound
+  | 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.
+  | TyNewType String      -- ^ New type
     deriving (Show, Eq, Ord)
 
 data IntSize

ivory/src/Ivory/Language/Type.hs

@@ -6,6 +6,7 @@ module Ivory.Language.Type where
 
 import Ivory.Language.Proxy
 import qualified Ivory.Language.Syntax as AST
+import GHC.TypeLits (Symbol)
 
 -- Ivory Types -----------------------------------------------------------------
 
@@ -54,3 +55,10 @@ data OpaqueType = OpaqueType
 
 instance IvoryType OpaqueType where
   ivoryType _ = AST.TyOpaque
+
+-- New Types -------------------------------------------------------------------
+
+newtype NewType (sym :: Symbol) = NewType { getNewType :: AST.Expr }
+
+mkNewType :: (ASymbol sym) => Proxy (sym :: Symbol) -> AST.Type
+mkNewType p = AST.TyNewType (fromTypeSym p)