Skip to content

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also .

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also .
...
  • 3 commits
  • 9 files changed
  • 0 commit comments
  • 1 contributor
View
3 README.md
@@ -4,8 +4,7 @@ Automated testing for Haskell programs. We take a program, simulate it against l
Roadmap
------
- - Compile .hs and interpret expressions.
- - Record reduction paths -- TODO
+ - Compile, interpret and test expressions.
- Find paths that were not run using an SMT solver -- TODO
- Simulate further -- TODO
View
2 examples/interpreter/Lists.hs
@@ -92,7 +92,7 @@ false1 = (takeTest2 :: [Int]) == (takeTest1 :: [Int])
-- | otherwise = MIN
first2 = take 2 [1,2,3,4]
-first0 = intListLength [1,2,3]
+first0 = [10,15]
first1 = intListLength [1..1] -- $ mytake 5 [5..10]
xs1 = [1..5]
View
42 src/DART/MkRandom.hs
@@ -18,22 +18,32 @@ import Language.Core.Interpreter
import System.Random
import Data.List((!!))
+-- newtype GenM a = GenM
+-- { unGenM :: ReaderT (Int,Int) (StateT Int (MaybeT (Rand StdGen))) a }
+-- deriving (Functor, Applicative, Monad, MonadPlus, MonadRandom,
+-- MonadState Int, MonadReader (Int,Int))
+
+-- -- | Run a generator to generate a data type of (approximately) size targetSize
+-- runGenM :: Int -> Double -> GenM a -> IM (Maybe a)
+-- runGenM targetSize eps m = do
+-- let wiggle = floor $ fromIntegral targetSize * eps
+-- minSize = targetSize - wiggle
+-- maxSize = targetSize + wiggle
+-- g <- newStdGen
+-- return . (evalRand ?? g) . runMaybeT . (evalStateT ?? 0)
+-- . (runReaderT ?? (minSize, maxSize)) . unGenM
+-- $ m
+
+-- -- | Checks whether the size has exceeded and fails in case the size of the structure is too big, it increases the size of the structure otherwise
+-- atom :: GenM ()
+-- atom = do
+-- (_, maxSize) <- ask
+-- curSize <- get
+-- when (curSize >= maxSize) mzero
+-- put (curSize + 1)
+
+
-- | Randomize on external core types. An environment might be needed in case there is a reference to the heap as an identifier in e.g. a data type
--- tyMkRandom :: Env -> Ty -> Maybe (IM Value)
--- tyMkRandom env ty = do
--- (_,val) <- runStateT mkRandomVal ty env
--- case val of
--- (Wrong _) -> Nothing
--- _ -> Just val
-
--- extractType ty >>= \et -> case et of
--- (CType ctype) -> Just $ mkRandomVal ctype env
--- --gtyp -> error $ "The impossible happened @tyMkRandom: It should not be called upon types that are not concrete (We are unpredicative), received " ++ show gtyp
--- _ -> Nothing
-
--- | A function that generates a random value given a type.
--- We could have type classes on RandomizableTypes but it would imply using template haskell
--- as there are Ty's in DataCons and they're not pattern match friendly (we have indeed an extractor)
mkRandomVal :: Env -> Ty -> IM Value
mkRandomVal env (Tcon qual_tcon) = case zDecodeQualified qual_tcon of
-- Make a random integer
@@ -55,8 +65,10 @@ fetchDataCons :: Id -> Env -> IM [DataCon]
fetchDataCons id env = do
-- look for the data type
msumtype <- lookupId id env
+ io $ putStrLn $ "fetchDataCons " ++ show msumtype
return $ case msumtype of
(Right (SumType datacons)) -> datacons
+ (Right (TypeConstructor datacons _)) -> [datacons]
_ -> []
-- | Given a list of data constructors (that form a sum type), make a random
View
4 src/DART/Util/StringUtils.hs
@@ -26,6 +26,8 @@ intercalateWith :: [String] -> String -> String
intercalateWith = flip intercalate
separateWithSpaces :: [String] -> String
-separateWithSpaces = intercalate space
+separateWithSpaces = intercalate space . filter (not . (==) empty_str)
+ where
+ empty_str = ""
separateWithNewLines = intercalate newLine
View
21 src/Language/Core/Interpreter/Evaluable.hs
@@ -181,13 +181,18 @@ instance Evaluable Exp where
res <- apply f id (heap_reference:env) -- Note1: the address is paassed
return res
- -- | A function application which has the type annotation which we will essentially ignore.
+ -- | A typed function (or data) application
eval e@(Appt exp ty) env = do
ti <- gets tab_indentation
let ?tab_indentation = ti
case exp of
(Var qvar) -> evalExpI exp env "Typed Var application "
- (Dcon qvar) -> evalExpI exp env $ "Typed Dcon application " ++ zDecodeQualified qvar
+ (Dcon qvar) -> do
+ v <- evalExpI exp env $ "Typed Dcon application " ++ zDecodeQualified qvar ++ ", to type " ++ show ty
+ case v of
+ tyconv@(TypeConstructor tycon@(MkDataCon id (t:ts)) tyname) -> return $ TypeConstructor (tycon { tyConExpectedTys = ts}) tyname
+ tyconapp@(TyConApp _ _) -> return tyconapp
+ otherwise -> return $ Wrong $ "The impossible happened: Typed application was expecting a type constructor or an applied type constructor, but got: " ++ show otherwise
_ -> evalExpI exp env "Typed application "
eval (Var ((Just (M (P ("base"),["GHC"],"Base"))),"zd")) env =
@@ -419,16 +424,18 @@ apply (Fun f d) id env = do
-- Applies a (possibly applied) type constructor that expects appliedValue of type ty.
-- The type constructor that we are applying has |vals| applied values
-apply (TyConApp tycon addresses) id env = do
+apply (TyConApp tycon@(MkDataCon _ (t:ts)) addresses) id env = do
addr <- getPointer id env
case addr of
- Pointer p -> return $ TyConApp tycon (addresses ++ [p])
+ Pointer p -> return $ TyConApp tycon { tyConExpectedTys = ts } (addresses ++ [p])
e@(Wrong s) -> return e
-
-apply (TypeConstructor tycon _) id env = do
+
+--apply tca@(TyConApp tycon@(MkDataCon _ ts) addresses) id env = return . Wrong $ "Applying " ++ (show . length) ts ++ " with argument " ++ show id
+
+apply (TypeConstructor tycon@(MkDataCon _ (t:ts)) _) id env = do
addr <- getPointer id env
case addr of
- Pointer p -> return $ TyConApp tycon ([p])
+ Pointer p -> return $ TyConApp (tycon { tyConExpectedTys = ts }) ([p])
e@(Wrong s) -> return e
apply w@(Wrong _) _ _ = return w
View
4 src/Language/Core/Interpreter/Libraries/GHC/Classes.hs
@@ -29,7 +29,7 @@ equals = (id, Right $ Fun (monomophy_2 "(==)" valEq) "polymorphic(==)") where
id = "ghc-prim:GHC.Classes.=="
valEq :: Value -> Value -> IM Value
valEq v@(Wrong _) _ = return v
- valEq _ w@(Wrong _) = return w
+ valEq _ w@(Wrong _) = return w
valEq (TyConApp dc1 ps) (TyConApp dc2 ps2) | dc1 == dc2 && length ps == length ps2 = do
-- get the value of every pointer
ps_vals <- mapM (flip eval []) ps
@@ -38,7 +38,7 @@ equals = (id, Right $ Fun (monomophy_2 "(==)" valEq) "polymorphic(==)") where
-- compare every corresponding pointer value, they must be all equal
mapM (uncurry valEq) (ps_vals `zip` ps2_vals) >>= return . Boolean . Data.List.all ((==) $ Boolean $ True)
| otherwise = return . Boolean $ False
- valEq v w = return . Boolean $ (==) v w
+ valEq v w = return . Boolean $ (==) v w
-- | (&&)
conjunction :: (Id, Either Thunk Value)
View
39 src/Language/Core/Interpreter/Libraries/GHC/Types.hs
@@ -7,38 +7,19 @@ import Language.Core.Interpreter(evalId)
-- | Evaluates definitions found in ghc-prim:GHC.Types
--- cons :: (Id,Either Thunk Value) -- (:) :: a -> [a] -> [a]
--- cons = (cons_name, Right $ TypeConstructor tycon ty_name) where
--- cons_name = "ghc-prim:GHC.Types.:"
--- ty_name = "ghc-prim:GHC.Types.[]"
--- tycon_args = [Tvar "a", Tvar "[a]"]
--- tycon = MkDataCon cons_name tycon_args
-
cons :: (Id,Either Thunk Value) -- (:) :: a -> [a] -> [a]
-cons = (id,Right val) where
- id = "ghc-prim:GHC.Types.:"
- -- type parameters
- typeArgs :: [Ty]
- typeArgs = [Tvar "a", Tvar "[a]"]
- typeConstructor :: DataCon
- typeConstructor = MkDataCon id typeArgs
- val = TyConApp typeConstructor []
+cons = (cons_name, Right $ TypeConstructor tycon ty_name) where
+ cons_name = "ghc-prim:GHC.Types.:"
+ ty_name = "ghc-prim:GHC.Types.[]"
+ tycon_args = [Tvar "aXX", Tvar "[a]YY", Tvar "XXXX"]
+ tycon = MkDataCon cons_name tycon_args
--- listConstructor :: (Id,Either Thunk Value) -- ([]) :: [a], kind * -> *
--- listConstructor = (cons_name, Right $ TypeConstructor tycon ty_name) where
--- cons_name = "ghc-prim:GHC.Types.[]"
--- ty_name = "ghc-prim:GHC.Types.[]"
--- tycon_args = [Tvar "a"]
--- tycon = MkDataCon cons_name tycon_args
-
listConstructor :: (Id,Either Thunk Value) -- ([]) :: [a], kind * -> *
-listConstructor = (id,Right $ TyConApp typeConstructor []) where
- id = "ghc-prim:GHC.Types.[]"
- -- type parameters
- typeArgs :: [Ty]
- typeArgs = [Tvar "a"]
- typeConstructor :: DataCon
- typeConstructor = MkDataCon id typeArgs
+listConstructor = (cons_name, Right $ TypeConstructor tycon ty_name) where
+ cons_name = "ghc-prim:GHC.Types.[]"
+ ty_name = "ghc-prim:GHC.Types.[]"
+ tycon_args = [Tvar "a"]
+ tycon = MkDataCon cons_name tycon_args
-- | An Int constructor, receives a literal and constructs an integer
intConstructor :: (Id, Either Thunk Value)
View
9 src/Language/Core/Interpreter/Structures.hs
@@ -119,7 +119,7 @@ data Value = Wrong String
| Fun (Id -> Env -> IM Value) Description
-- | List [Value]
| Pair Pointer Pointer --HERE, heap addresses
- | TyConApp DataCon [Pointer] -- a data constructor applicated to some values
+ | TyConApp DataCon [Pointer] -- a data constructor applicated to some values, possible expecting some more types
| Pointer Pointer
| FreeTypeVariable String -- useful when converting a to SomeClass a (we ignore parameters, and it's useful to save them)
| MkListOfValues [(String,Value)] -- When a value definition is recursive, depends on other values
@@ -144,8 +144,8 @@ data HaskellExpression = HaskellExpression String Module
-- | A data type constructor that has normally a qualified name and a list of
-- types that it expects.
data DataCon = MkDataCon {
- dataConId :: Id,
- dataConTys :: [Ty]
+ tyConId :: Id,
+ tyConExpectedTys :: [Ty]
} deriving Eq
type Description = String
@@ -262,7 +262,8 @@ instance Show Value where
| otherwise = "TypeConstructor " ++ show tycon ++ " of " ++ ty_name
instance Show DataCon where
- show (MkDataCon "ghc-prim:GHC.Types.[]" _) = "[]"
+ show (MkDataCon "ghc-prim:GHC.Types.[]" []) = "[]"
+ show (MkDataCon "ghc-prim:GHC.Types.[]" ty) = "[] expecting " ++ show ty
show (MkDataCon id []) = idName id
show (MkDataCon id types) = idName id ++ " :: " ++ types' where
types' :: String
View
6 src/Language/Core/Interpreter/Util.hs
@@ -54,14 +54,14 @@ showTyConApp tycon pointers = do
whnf_strings <- mapM showValue' vals -- [String]
return $ let
- tycon_name = (idName . dataConId) tycon
+ tycon_name = (idName . tyConId) tycon
arg_strings = separateWithSpaces whnf_strings
in tycon_name ++ " " ++ arg_strings
where
-- Should we wrap a value in parenthesis? Wrap the tycon apps! (iff they have applied vals)
showValue' :: Value -> IM String
- showValue' t@(TyConApp tycon []) = return . idName . dataConId $ tycon
+ showValue' t@(TyConApp tycon []) = return . idName . tyConId $ tycon
showValue' t@(TyConApp _ _) = showValue t >>= return . wrapInParenthesis
showValue' v = showValue v
@@ -83,7 +83,7 @@ showList ptrs = do
showValue' t@(TyConApp (MkDataCon "ghc-prim:GHC.Types.[]" _) []) = return ""
showValue' t@(TyConApp (MkDataCon "ghc-prim:GHC.Types.[]" _) ty) = return $ "[] to " ++ show ty
showValue' t@(TyConApp (MkDataCon "ghc-prim:GHC.Types.:" _) ptrs) = mapM showPtr ptrs >>= return . separateWithSpaces
- showValue' t@(TypeConstructor (MkDataCon "ghc-prim:GHC.Types.[]" [_]) "ghc-prim:GHC.Types.[]")= return ""
+ showValue' t@(TypeConstructor (MkDataCon "ghc-prim:GHC.Types.[]" []) "ghc-prim:GHC.Types.[]")= return ""
showValue' v = showValue v
wrapInParenthesis s = "(" ++ s ++ ")"

No commit comments for this range

Something went wrong with that request. Please try again.