Skip to content

Commit

Permalink
CanFailWith
Browse files Browse the repository at this point in the history
  • Loading branch information
Ian Grant Jeffries committed Nov 11, 2019
1 parent e27ff19 commit 7d718cd
Show file tree
Hide file tree
Showing 5 changed files with 43 additions and 35 deletions.
14 changes: 8 additions & 6 deletions bowtie-visualize/src/Bowtie/Visualize.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,11 @@ module Bowtie.Visualize
, writeConstraints
) where

import Bowtie.Infer.Assumptions (Assumptions)
import Bowtie.Infer.Constraints
import Bowtie.Infer.Solve
import Bowtie.Infer.Solve (next, solveConstraint)
import Bowtie.Infer.Unify
import Bowtie.Lib.CanFailWith
import Bowtie.Lib.Environment
import Bowtie.Lib.Prelude
import Bowtie.Surface.AST (AST(astTerms, astTypes))
Expand Down Expand Up @@ -42,9 +44,9 @@ run libFiles appFile = do

let
f :: ( MonadState Int m
, CanSolveStuck m
, CanUnifyError m
, Infer.CanAssumptionsRemain m
, CanFailWith SolveStuck m
, CanFailWith UnifyError m
, CanFailWith Assumptions m
) => m [Constraints]
f = do
(constraints, _) <- Infer.gatherConstraints env dsg
Expand All @@ -67,7 +69,7 @@ writeConstraints cs =
BS.writeFile (Text.unpack (show n <> ".svg")) bts

solutionSteps
:: (MonadState Int m, CanSolveStuck m, CanUnifyError m)
:: (MonadState Int m, CanFailWith SolveStuck m, CanFailWith UnifyError m)
=> Constraints
-> m [Constraints]
solutionSteps cs = do
Expand All @@ -78,7 +80,7 @@ solutionSteps cs = do
pure mempty

else
failSolveStuck
failWith SolveStuckError

Just (c, rest) -> do
(_sub, rest2) <- solveConstraint c rest
Expand Down
3 changes: 2 additions & 1 deletion bowtie/bowtie.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ cabal-version: 1.18
--
-- see: https://github.com/sol/hpack
--
-- hash: 759169e0b3d720cfa7430eb1ab6d01ec5fdc06ddb6a89a10789f6bb437f0b38e
-- hash: 0b854e9d24f9bd96b6df9143a6958223d314d17aef63cf17d00ecf33561248fd

name: bowtie
version: 0.0.0
Expand All @@ -25,6 +25,7 @@ library
Bowtie.Infer.Unify
Bowtie.Interpret
Bowtie.Lib.Builtin
Bowtie.Lib.CanFailWith
Bowtie.Lib.Environment
Bowtie.Lib.FreeVars
Bowtie.Lib.OrderedMap
Expand Down
19 changes: 9 additions & 10 deletions bowtie/src/Bowtie/Infer/Solve.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,21 +4,20 @@ import Bowtie.Infer.Constraints
import Bowtie.Infer.Generalize (generalize, instantiate)
import Bowtie.Infer.Substitution
import Bowtie.Infer.Unify
import Bowtie.Lib.CanFailWith
import Bowtie.Lib.Prelude
import Control.Monad.State.Class

import qualified Bowtie.Infer.Constraints as Constraints
import qualified Data.List as List
import qualified Data.Set as Set

class CanSolveStuck m where
failSolveStuck :: m a

class CanUnifyError m where
failUnifyError :: UnifyError -> m a
data SolveStuck
= SolveStuckError
deriving (Eq, Show)

solve
:: (MonadState Int m, CanSolveStuck m, CanUnifyError m)
:: (MonadState Int m, CanFailWith SolveStuck m, CanFailWith UnifyError m)
=> Constraints
-> m Substitution
solve cs = do
Expand All @@ -29,23 +28,23 @@ solve cs = do
pure mempty

else
failSolveStuck
failWith SolveStuckError

Just (c, rest) -> do
(sub, rest2) <- solveConstraint c rest
fmap (\a -> a <> sub) (solve rest2)

solveConstraint
:: (MonadState Int m, CanUnifyError m)
:: (MonadState Int m, CanFailWith UnifyError m)
=> Constraint
-> Constraints
-> m (Substitution, Constraints)
solveConstraint c rest = do
case c of
EqualityConstraint t1 t2 -> do
sub <- case unify t1 t2 of
Left e ->
failUnifyError e
Left unifyError ->
failWith unifyError

Right s ->
pure s
Expand Down
4 changes: 4 additions & 0 deletions bowtie/src/Bowtie/Lib/CanFailWith.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
module Bowtie.Lib.CanFailWith where

class CanFailWith e m where
failWith :: e -> m a
38 changes: 20 additions & 18 deletions bowtie/src/Bowtie/Surface/Infer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,10 @@ module Bowtie.Surface.Infer where
import Bowtie.Infer.Assumptions (Assumptions)
import Bowtie.Infer.BottomUp
import Bowtie.Infer.Constraints
import Bowtie.Infer.Unify
import Bowtie.Infer.Solve
import Bowtie.Infer.Substitution
import Bowtie.Infer.Unify
import Bowtie.Lib.CanFailWith
import Bowtie.Lib.Environment
import Bowtie.Lib.Prelude
import Bowtie.Surface.AST
Expand Down Expand Up @@ -39,7 +40,11 @@ elaborate env expr = do
pure (sub, typ, substExpr sub freshExpr)

inferType
:: (MonadState Int m, CanSolveStuck m, CanUnifyError m, CanAssumptionsRemain m)
:: ( MonadState Int m
, CanFailWith SolveStuck m
, CanFailWith UnifyError m
, CanFailWith Assumptions m
)
=> Environment
-> Expr
-> m (Substitution, Type)
Expand All @@ -49,11 +54,8 @@ inferType env expr = do
-- Heeren paper doesn't do the substType here:
pure (s, substType s typ)

class CanAssumptionsRemain m where
failAssumptionsRemain :: Assumptions -> m a

gatherConstraints
:: (MonadState Int m, CanAssumptionsRemain m)
:: (MonadState Int m, CanFailWith Assumptions m)
=> Environment
-> Expr
-> m (Constraints, Type)
Expand All @@ -70,7 +72,7 @@ gatherConstraints env expr = do
pure ()

else
failAssumptionsRemain a
failWith a

pure (c <> explicitConstraintOnSet env a, t)

Expand All @@ -90,26 +92,26 @@ newtype Infer a
= Infer (StateT Int (Either TypeError) a)
deriving newtype (Functor, Applicative, Monad, MonadError TypeError, MonadState Int)

instance CanSolveStuck Infer where
failSolveStuck :: Infer a
failSolveStuck =
instance CanFailWith SolveStuck Infer where
failWith :: SolveStuck -> Infer a
failWith SolveStuckError =
throwError SolveStuck

instance CanUnifyError Infer where
failUnifyError :: UnifyError -> Infer a
failUnifyError e =
instance CanFailWith UnifyError Infer where
failWith :: UnifyError -> Infer a
failWith e =
throwError (case e of
TypeMismatch t1 t2 ->
UnifyError t1 t2

IdOccursInType id t ->
OccursCheckFailed id t)

instance CanAssumptionsRemain Infer where
failAssumptionsRemain :: Assumptions -> Infer a
failAssumptionsRemain =
instance CanFailWith Assumptions Infer where
failWith :: Assumptions -> Infer a
failWith =
throwError . AssumptionsRemain

runInfer :: Infer a -> Either TypeError a
runInfer (Infer g) =
evalStateT g 0
runInfer (Infer f) =
evalStateT f 0

0 comments on commit 7d718cd

Please sign in to comment.