Skip to content

Commit

Permalink
Working on fixing crashing on non-simple types
Browse files Browse the repository at this point in the history
  • Loading branch information
justingrubbs committed Jul 4, 2024
1 parent 0a5c26c commit 1be68a3
Show file tree
Hide file tree
Showing 3 changed files with 37 additions and 29 deletions.
19 changes: 14 additions & 5 deletions src/Disco/Compile.hs
Original file line number Diff line number Diff line change
Expand Up @@ -170,11 +170,9 @@ compileDTerm term@(DTAbs q _ _) = do
cbody <- compileDTerm body
case q of

Lam -> return $ abstractMemo xs cbody
-- Lam -> case _ of
-- _ -> return $ abstract xs cbody
-- _ -> return $ abstractMemo xs cbody

Lam -> case canMemo tys of
False -> return $ abstract xs cbody
True -> return $ abstractMemo xs cbody
Ex -> return $ quantify (OExists tys) (abstract xs cbody)
All -> return $ quantify (OForall tys) (abstract xs cbody)
where
Expand All @@ -195,6 +193,17 @@ compileDTerm term@(DTAbs q _ _) = do
quantify :: Op -> Core -> Core
quantify op = CApp (CConst op)

canMemo :: [Type] -> Bool
canMemo [] = True
canMemo (x : xs) = case x of
TyCon (CUser _) _ -> False
TyCon CGraph _ -> False
TyCon CMap _ -> False
-- TyCon CArr _ -> False
TyCon _ _ -> canMemo xs
TyAtom (ABase Gen) -> False
TyAtom _ -> canMemo xs

-- Special case for Cons, which compiles to a constructor application
-- rather than a function application.
compileDTerm (DTApp _ (DTPrim _ (PrimBOp Cons)) (DTPair _ t1 t2)) =
Expand Down
16 changes: 8 additions & 8 deletions src/Disco/Interpret/CESK.hs
Original file line number Diff line number Diff line change
Expand Up @@ -205,18 +205,18 @@ step cesk = case cesk of

(Out v (FMemo n sv : k)) -> memoSet n sv v *> (return $ Out v k)

(Out v2 (FApp (VClo mem mi e [x] b) : k)) -> case mi of
Nothing -> return $ In b (Ctx.insert (localName x) v2 e) k
(Out v (FApp (VClo mem mi e [x] b) : k)) -> case mi of
Nothing -> return $ In b (Ctx.insert (localName x) v e) k
Just n -> do
let sv = toSimpleValue $ foldr VPair VUnit (v2 : mem)
let sv = toSimpleValue $ foldr VPair VUnit (v : mem)
mv <- memoLookup n sv
case mv of
Nothing -> return $ In b (Ctx.insert (localName x) v2 e) (FMemo n sv : k)
Just v -> return $ Out v k
Nothing -> return $ In b (Ctx.insert (localName x) v e) (FMemo n sv : k)
Just v' -> return $ Out v' k

(Out v2 (FApp (VClo mem mi e (x : xs) b) : k)) -> case mi of
Just _ -> return $ Out (VClo (v2 : mem) mi (Ctx.insert (localName x) v2 e) xs b) k
Nothing -> return $ Out (VClo mem mi (Ctx.insert (localName x) v2 e) xs b) k
(Out v (FApp (VClo mem mi e (x : xs) b) : k)) -> case mi of
Just _ -> return $ Out (VClo (v : mem) mi (Ctx.insert (localName x) v e) xs b) k
Nothing -> return $ Out (VClo mem mi (Ctx.insert (localName x) v e) xs b) k



Expand Down
31 changes: 15 additions & 16 deletions src/Disco/Value.hs
Original file line number Diff line number Diff line change
Expand Up @@ -312,11 +312,11 @@ pattern SMExists :: SearchMotive
pattern SMExists = SearchMotive (True, True)

-- | A collection of variables that might need to be reported for
-- a test, along with their types and user-legible names.
-- a toMap, along with their types and user-legible names.
newtype TestVars = TestVars [(String, Type, Name Core)]
deriving newtype (Show, Semigroup, Monoid)

-- | A variable assignment found during a test.
-- | A variable assignment found during a toMap.
newtype TestEnv = TestEnv [(String, Type, Value)]
deriving newtype (Show, Semigroup, Monoid)

Expand All @@ -341,16 +341,16 @@ interpLOp LImpl = (==>)
True ==> False = False
_ ==> _ = True

-- | The possible outcomes of a property test, parametrized over
-- | The possible outcomes of a property toMap, parametrized over
-- the type of values. A @TestReason@ explains why a proposition
-- succeeded or failed.
data TestReason_ a
= -- | The prop evaluated to a boolean.
TestBool
| -- | The test was an equality test. Records the values being
| -- | The toMap was an equality toMap. Records the values being
-- compared and also their type (which is needed for printing).
TestEqual Type a a
| -- | The test was a less than test. Records the values being
| -- | The toMap was a less than toMap. Records the values being
-- compared and also their type (which is needed for printing).
TestLt Type a a
| -- | The search didn't find any examples/counterexamples.
Expand All @@ -370,16 +370,16 @@ type TestReason = TestReason_ Value
data TestResult = TestResult Bool TestReason TestEnv
deriving (Show)

-- | Whether the property test resulted in a runtime error.
-- | Whether the property toMap resulted in a runtime error.
testIsError :: TestResult -> Bool
testIsError (TestResult _ (TestRuntimeError _) _) = True
testIsError _ = False

-- | Whether the property test resulted in success.
-- | Whether the property toMap resulted in success.
testIsOk :: TestResult -> Bool
testIsOk (TestResult b _ _) = b

-- | The reason the property test had this result.
-- | The reason the property toMap had this result.
testReason :: TestResult -> TestReason
testReason (TestResult _ r _) = r

Expand Down Expand Up @@ -476,12 +476,15 @@ allocateRec e bs = do
lkup :: Members '[State Mem] r => Int -> Sem r (Maybe Cell)
lkup n = gets (IM.lookup n . mu)

-- | Set the cell at a given index.
set :: Members '[State Mem] r => Int -> Cell -> Sem r ()
set n c = modify $ \(Mem nxt m) -> Mem nxt (IM.insert n c m)

memoLookup :: Members '[State Mem] r => Int -> SimpleValue -> Sem r (Maybe Value)
memoLookup n sv = gets (M.lookup sv . test . IM.lookup n . mu)
memoLookup n sv = gets (M.lookup sv . toMap . IM.lookup n . mu)
where
test (Just (Disco.Value.V (VMap vmap))) = vmap
test (Just _) = M.empty
test Nothing = M.empty
toMap (Just (Disco.Value.V (VMap vmap))) = vmap
toMap _ = M.empty

memoSet :: Members '[State Mem] r => Int -> SimpleValue -> Value -> Sem r ()
memoSet n sv v = do
Expand All @@ -491,10 +494,6 @@ memoSet n sv v = do
Just (Disco.Value.V (VMap vmap)) -> set n (Disco.Value.V (VMap (M.insert sv v vmap)))
Just _ -> undefined

-- | Set the cell at a given index.
set :: Members '[State Mem] r => Int -> Cell -> Sem r ()
set n c = modify $ \(Mem nxt m) -> Mem nxt (IM.insert n c m)

------------------------------------------------------------
-- Pretty-printing values
------------------------------------------------------------
Expand Down

0 comments on commit 1be68a3

Please sign in to comment.