From 6db70f61afc878fcd80007cd9469752688f9f85a Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Thu, 21 Sep 2023 13:47:04 +0100 Subject: [PATCH 01/15] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Minor=20t?= =?UTF-8?q?idy=20up.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/EvalGraph.purs | 24 +++++++++++------------- src/GaloisConnection.purs | 2 +- test/Util.purs | 2 +- 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index e065f089f..de664bb6f 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -183,16 +183,14 @@ evalWithConfig { g, n, γα } e = pure (eα × vα) graphGC :: forall g. Graph g => GraphConfig g -> Raw Expr -> String + GaloisConnection (Set Vertex) (Set Vertex) -graphGC { g: g0, n, γα } e = - let - Identity q = (runWithGraphAllocT (g0 × n) :: _ -> Identity _) $ do - eα <- alloc e - vα <- eval γα eα S.empty - pure (vα × eα) - in - do - (g × _) × vα × eα <- q - pure $ - { fwd: \αs -> G.vertices (fwdSlice αs g) `intersection` vertices vα - , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- needs to include γα - } +graphGC { g: g0, n, γα } e = do + (g × _) × vα × eα <- q + pure $ + { fwd: \αs -> G.vertices (fwdSlice αs g) `intersection` vertices vα + , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- needs to include γα + } + where + Identity q = (runWithGraphAllocT (g0 × n) :: _ -> Identity _) $ do + eα <- alloc e + vα <- eval γα eα S.empty + pure (vα × eα) diff --git a/src/GaloisConnection.purs b/src/GaloisConnection.purs index 8229dd613..df981f5a7 100644 --- a/src/GaloisConnection.purs +++ b/src/GaloisConnection.purs @@ -12,7 +12,7 @@ type GaloisConnection a b = } deMorgan :: forall a b. BooleanLattice a => BooleanLattice b => Endo (a -> b) -deMorgan f = neg >>> f >>> neg +deMorgan = (neg >>> _) >>> (_ >>> neg) -- Could unify deMorgan and dual but would need to reify notion of opposite category. dual :: forall a b. BooleanLattice a => BooleanLattice b => GaloisConnection a b -> GaloisConnection b a diff --git a/test/Util.purs b/test/Util.purs index a5583790a..759df25ce 100644 --- a/test/Util.purs +++ b/test/Util.purs @@ -106,7 +106,7 @@ testGraph s gconf { δv, bwd_expect, fwd_expect } = do -- | Eval e <- desug s tEval1 <- preciseTime - (g × _) × (eα × vα) <- evalWithConfig gconf e >>= except + (g × _) × eα × vα <- evalWithConfig gconf e >>= except tEval2 <- preciseTime -- | Backward From 048885b59236c8a4f5fdafd9eaf2bb3f86478cf7 Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Thu, 21 Sep 2023 13:50:13 +0100 Subject: [PATCH 02/15] =?UTF-8?q?=F0=9F=A7=A9=20[layout]?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/EvalGraph.purs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index de664bb6f..c86bee74e 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -184,13 +184,13 @@ evalWithConfig { g, n, γα } e = graphGC :: forall g. Graph g => GraphConfig g -> Raw Expr -> String + GaloisConnection (Set Vertex) (Set Vertex) graphGC { g: g0, n, γα } e = do - (g × _) × vα × eα <- q + (g × _) × vα × eα <- m pure $ { fwd: \αs -> G.vertices (fwdSlice αs g) `intersection` vertices vα , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- needs to include γα } where - Identity q = (runWithGraphAllocT (g0 × n) :: _ -> Identity _) $ do + Identity m = (runWithGraphAllocT (g0 × n) :: _ -> Identity _) $ do eα <- alloc e vα <- eval γα eα S.empty pure (vα × eα) From 2db394db1736c00980f0c04c74d0d14b6f80ca26 Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Thu, 21 Sep 2023 14:17:49 +0100 Subject: [PATCH 03/15] =?UTF-8?q?=F0=9F=A7=A9=20[unconsolidate]:=20Might?= =?UTF-8?q?=20be=20better=20to=20separate=20ExceptT=20from=20WithGraphAllo?= =?UTF-8?q?cT.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/EvalGraph.purs | 10 ++++++++++ src/Graph/GraphWriter.purs | 14 +++++++++++--- 2 files changed, 21 insertions(+), 3 deletions(-) diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index c86bee74e..03fcc1865 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -194,3 +194,13 @@ graphGC { g: g0, n, γα } e = do eα <- alloc e vα <- eval γα eα S.empty pure (vα × eα) +{- +graphGC2 :: forall g m. Monad m => Graph g => GraphConfig g -> Raw Expr -> m (String + GaloisConnection (Set Vertex) (Set Vertex)) +graphGC2 { g: g0, n, γα } e = do + ?_ + where + m = (runWithGraphAllocT (g0 × n) :: _ -> m _) $ do + eα <- alloc e + vα <- eval γα eα S.empty + pure (vα × eα) +-} diff --git a/src/Graph/GraphWriter.purs b/src/Graph/GraphWriter.purs index e34ca359b..16205f611 100644 --- a/src/Graph/GraphWriter.purs +++ b/src/Graph/GraphWriter.purs @@ -16,6 +16,7 @@ module Graph.GraphWriter , runWithGraph , runWithGraphT , runWithGraphAllocT + , runWithGraphAlloc2T ) where import Prelude @@ -48,6 +49,8 @@ type AdjMapEntries = List (Vertex × Set Vertex) type WithAllocT m = StateT Int m type WithAlloc = WithAllocT Identity type WithGraphAllocT m = MayFailT (WithAllocT (WithGraphT m)) +-- May make sense to push MayFailT out of WithGraphAllocT. For now: +type WithGraphAlloc2T m = WithAllocT (WithGraphT m) type WithGraphT = StateT AdjMapEntries type WithGraph = WithGraphT Identity @@ -90,7 +93,12 @@ runWithGraphT c = runStateT c Nil <#> swap <#> first fromFoldable runWithGraph :: forall g a. Graph g => WithGraph a -> g × a runWithGraph = runWithGraphT >>> unwrap +runWithGraphAlloc2T :: forall g m a. Monad m => Graph g => g × Int -> WithGraphAlloc2T m a -> m ((g × Int) × a) +runWithGraphAlloc2T (g × n) m = do + (n' × a) × g_adds <- runStateT (runWithAllocT n m) Nil + pure $ ((g <> fromFoldable g_adds) × n') × a + runWithGraphAllocT :: forall g m a. Monad m => Graph g => g × Int -> WithGraphAllocT m a -> m (String + ((g × Int) × a)) -runWithGraphAllocT (g × n) c = do - (n' × maybe_a) × g_adds <- runStateT (runWithAllocT n (runExceptT c)) Nil - pure $ maybe_a <#> (((g <> fromFoldable g_adds) × n') × _) +runWithGraphAllocT (g × n) m = do + (g' × n') × maybe_a <- runWithGraphAlloc2T (g × n) (runExceptT m) + pure $ maybe_a <#> ((g' × n') × _) From ecdcc2b79bc5f473b24aba13e5028819870e3b1f Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Thu, 21 Sep 2023 16:15:45 +0100 Subject: [PATCH 04/15] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Abstract?= =?UTF-8?q?=20monads=20over=20concrete=20exception=20types=20to=20avoid=20?= =?UTF-8?q?endless=20cheesing=20packing=20and=20unpacking=20concrete=20mon?= =?UTF-8?q?ads.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/DataType.purs | 18 ++++++------ src/Eval.purs | 27 +++++++++--------- src/EvalGraph.purs | 61 +++++++++++++++++++++++++++++++---------- src/Primitive/Defs.purs | 47 +++++++++++++++---------------- src/Util.purs | 25 +++++++++-------- src/Val.purs | 13 +++++---- 6 files changed, 115 insertions(+), 76 deletions(-) diff --git a/src/DataType.purs b/src/DataType.purs index 3fb31ce79..3541777b3 100644 --- a/src/DataType.purs +++ b/src/DataType.purs @@ -1,20 +1,22 @@ module DataType where import Prelude hiding (absurd) + +import Bindings (Var) +import Control.Monad.Error.Class (class MonadError, class MonadThrow) import Data.CodePoint.Unicode (isUpper) import Data.Function (on) -import Data.List (fromFoldable) as L import Data.List (List, concat, (:)) +import Data.List (fromFoldable) as L import Data.Set (Set) import Data.Set (map, fromFoldable, toUnfoldable) as S import Data.String.CodePoints (codePointFromChar) import Data.String.CodeUnits (charAt) import Data.Tuple (uncurry) -import Partial.Unsafe (unsafePartial) import Dict (Dict, keys, lookup) import Dict (fromFoldable) as O -import Bindings (Var) -import Util (MayFailT, type (×), (×), (=<<<), (≞), absurd, error, definitely', with, orElse) +import Partial.Unsafe (unsafePartial) +import Util (type (×), absurd, definitely', error, orElse, with, (=<<<), (×), (≞)) type TypeName = String type FieldName = String @@ -55,7 +57,7 @@ ctrToDataType = dataTypes <#> (\d -> ctrs d # S.toUnfoldable <#> (_ × d)) # concat # O.fromFoldable class DataTypeFor a where - dataTypeFor :: forall m. Monad m => a -> MayFailT m DataType + dataTypeFor :: forall m. MonadThrow String m => a -> m DataType instance DataTypeFor Ctr where dataTypeFor c = lookup c ctrToDataType # orElse ("Unknown constructor " <> showCtr c) @@ -64,7 +66,7 @@ instance DataTypeFor (Set Ctr) where dataTypeFor cs = unsafePartial $ case S.toUnfoldable cs of c : _ -> dataTypeFor c -- Sets must be non-empty, but this is a more convenient signature. -consistentWith :: forall m. Monad m => Set Ctr -> Set Ctr -> MayFailT m Unit +consistentWith :: forall m. MonadError String m => Set Ctr -> Set Ctr -> m Unit consistentWith cs cs' = void $ do d <- dataTypeFor cs' d' <- dataTypeFor cs' @@ -73,12 +75,12 @@ consistentWith cs cs' = void $ do ctrs :: DataType -> Set Ctr ctrs (DataType _ sigs) = keys sigs # S.fromFoldable -arity :: forall m. Monad m => Ctr -> MayFailT m Int +arity :: forall m. MonadThrow String m => Ctr -> m Int arity c = do DataType _ sigs <- dataTypeFor c lookup c sigs # orElse absurd -checkArity :: forall m. Monad m => Ctr -> Int -> MayFailT m Unit +checkArity :: forall m. MonadError String m => Ctr -> Int -> m Unit checkArity c n = void $ with ("Checking arity of " <> showCtr c) (arity c `(=<<<) (≞)` pure n) diff --git a/src/Eval.purs b/src/Eval.purs index 2b0c4ab08..d83564cf7 100644 --- a/src/Eval.purs +++ b/src/Eval.purs @@ -3,6 +3,7 @@ module Eval where import Prelude hiding (absurd, apply, top) import Bindings (varAnon) +import Control.Monad.Error.Class (class MonadError, throwError) import Data.Array (fromFoldable) as A import Data.Bifunctor (bimap) import Data.Either (Either(..)) @@ -23,7 +24,7 @@ import Pretty (prettyP) import Primitive (intPair, string) import Trace (AppTrace(..), Trace(..), VarDef(..)) as T import Trace (AppTrace, ForeignTrace, ForeignTrace'(..), Match(..), Trace) -import Util (type (×), MayFailT, absurd, both, check, error, report, successful, orElse, with, (×)) +import Util (type (×), MayFailT, absurd, both, check, error, successful, orElse, with, (×)) import Util.Pair (unzip) as P import Val (Fun(..), Val(..)) as V import Val (class Ann, DictRep(..), Env, ForeignOp'(..), MatrixRep(..), (<+>), Val, for, lookup', restrict) @@ -31,7 +32,7 @@ import Val (class Ann, DictRep(..), Env, ForeignOp'(..), MatrixRep(..), (<+>), V patternMismatch :: String -> String -> String patternMismatch s s' = "Pattern mismatch: found " <> s <> ", expected " <> s' -match :: forall a m. Monad m => Ann a => Val a -> Elim a -> MayFailT m (Env a × Cont a × a × Match) +match :: forall a m. MonadError String m => Ann a => Val a -> Elim a -> m (Env a × Cont a × a × Match) match v (ElimVar x κ) | x == varAnon = pure (empty × κ × top × MatchVarAnon (erase v)) | otherwise = pure (D.singleton x v × κ × top × MatchVar x (erase v)) @@ -42,21 +43,21 @@ match (V.Constr α c vs) (ElimConstr m) = do pure (γ × κ' × (α ∧ α') × MatchConstr c ws) match v (ElimConstr m) = do d <- dataTypeFor $ keys m - report $ patternMismatch (prettyP v) (show d) + throwError $ patternMismatch (prettyP v) (show d) match (V.Record α xvs) (ElimRecord xs κ) = do check (subset xs (S.fromFoldable $ keys xvs)) $ patternMismatch (show (keys xvs)) (show xs) let xs' = xs # S.toUnfoldable γ × κ' × α' × ws <- matchMany (xs' <#> flip get xvs) κ pure (γ × κ' × (α ∧ α') × MatchRecord (D.fromFoldable (zip xs' ws))) -match v (ElimRecord xs _) = report (patternMismatch (prettyP v) (show xs)) +match v (ElimRecord xs _) = throwError $ patternMismatch (prettyP v) (show xs) -matchMany :: forall a m. Monad m => Ann a => List (Val a) -> Cont a -> MayFailT m (Env a × Cont a × a × List Match) +matchMany :: forall a m. MonadError String m => Ann a => List (Val a) -> Cont a -> m (Env a × Cont a × a × List Match) matchMany Nil κ = pure (empty × κ × top × Nil) matchMany (v : vs) (ContElim σ) = do γ × κ' × α × w <- match v σ γ' × κ'' × β × ws <- matchMany vs κ' pure $ γ `disjointUnion` γ' × κ'' × (α ∧ β) × (w : ws) -matchMany (_ : vs) (ContExpr _) = report $ +matchMany (_ : vs) (ContExpr _) = throwError $ show (length vs + 1) <> " extra argument(s) to constructor/record; did you forget parentheses in lambda pattern?" matchMany _ _ = error absurd @@ -64,12 +65,12 @@ closeDefs :: forall a. Env a -> RecDefs a -> a -> Env a closeDefs γ ρ α = ρ <#> \σ -> let ρ' = ρ `for` σ in V.Fun α $ V.Closure (γ `restrict` (fv ρ' `union` fv σ)) ρ' σ -checkArity :: forall m. Monad m => Ctr -> Int -> MayFailT m Unit +checkArity :: forall m. MonadError String m => Ctr -> Int -> m Unit checkArity c n = do n' <- arity c check (n' >= n) (showCtr c <> " got " <> show n <> " argument(s), expects at most " <> show n') -apply :: forall a m. Monad m => Ann a => Val a × Val a -> MayFailT m (AppTrace × Val a) +apply :: forall a m. MonadError String m => Ann a => Val a × Val a -> m (AppTrace × Val a) apply (V.Fun β (V.Closure γ1 ρ σ) × v) = do let γ2 = closeDefs γ1 ρ β γ3 × e'' × β' × w <- match v σ @@ -81,7 +82,7 @@ apply (V.Fun α (V.Foreign φ vs) × v) = do where vs' = vs <> singleton v - apply' :: forall t. ForeignOp' t -> MayFailT m (ForeignTrace × Val _) + apply' :: forall t. ForeignOp' t -> m (ForeignTrace × Val _) apply' (ForeignOp' φ') = do t × v'' <- do if φ'.arity > length vs' then pure $ Nothing × V.Fun α (V.Foreign φ vs') @@ -95,15 +96,15 @@ apply (V.Fun α (V.PartialConstr c vs) × v) = do v' = if length vs < n - 1 then V.Fun α $ V.PartialConstr c (vs <> singleton v) else V.Constr α c (vs <> singleton v) -apply (_ × v) = report $ "Found " <> prettyP v <> ", expected function" +apply (_ × v) = throwError $ "Found " <> prettyP v <> ", expected function" -apply2 :: forall a m. Monad m => Ann a => Val a × Val a × Val a -> MayFailT m ((AppTrace × AppTrace) × Val a) +apply2 :: forall a m. MonadError String m => Ann a => Val a × Val a × Val a -> m ((AppTrace × AppTrace) × Val a) apply2 (u1 × v1 × v2) = do t1 × u2 <- apply (u1 × v1) t2 × v <- apply (u2 × v2) pure $ (t1 × t2) × v -eval :: forall a m. Monad m => Ann a => Env a -> Expr a -> a -> MayFailT m (Trace × Val a) +eval :: forall a m. MonadError String m => Ann a => Env a -> Expr a -> a -> m (Trace × Val a) eval γ (Var x) _ = (T.Var x × _) <$> lookup' x γ eval γ (Op op) _ = (T.Op op × _) <$> lookup' op γ eval _ (Int α n) α' = pure (T.Const × V.Int (α ∧ α') n) @@ -144,7 +145,7 @@ eval γ (Project e x) α = do t × v <- eval γ e α case v of V.Record _ xvs -> (T.Project t x × _) <$> lookup' x xvs - _ -> report $ "Found " <> prettyP v <> ", expected record" + _ -> throwError $ "Found " <> prettyP v <> ", expected record" eval γ (App e e') α = do t × v <- eval γ e α t' × v' <- eval γ e' α diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index 03fcc1865..ce04a350b 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -12,6 +12,7 @@ module EvalGraph import Prelude hiding (apply, add) import Bindings (varAnon) +import Control.Monad.Error.Class (class MonadError, class MonadThrow, throwError) import Data.Array (range, singleton) as A import Data.Either (Either(..)) import Data.Exists (runExists) @@ -25,14 +26,14 @@ import DataType (checkArity, arity, consistentWith, dataTypeFor, showCtr) import Dict (disjointUnion, fromFoldable, empty, get, keys, lookup, singleton) as D import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, asExpr) import GaloisConnection (GaloisConnection) -import Graph (Vertex, class Graph) +import Graph (class Graph, Vertex) import Graph (vertices) as G -import Graph.GraphWriter (WithGraphAllocT, alloc, new, runWithGraphAllocT) +import Graph.GraphWriter (class MonadGraphAlloc, WithGraphAllocT, alloc, new, runWithGraphAllocT) import Graph.Slice (bwdSlice, fwdSlice, vertices) import Lattice (Raw) import Pretty (prettyP) import Primitive (string, intPair) -import Util (type (+), type (×), (×), MayFailT, check, error, report, successful, with, orElse) +import Util (type (+), type (×), (×), check, error, successful, with, orElse) import Util.Pair (unzip) as P import Val (DictRep(..), Env, ForeignOp'(..), MatrixRep(..), Val, for, lookup', restrict, (<+>)) import Val (Val(..), Fun(..)) as V @@ -47,7 +48,13 @@ type GraphConfig g = patternMismatch :: String -> String -> String patternMismatch s s' = "Pattern mismatch: found " <> s <> ", expected " <> s' -match :: forall m. Monad m => Val Vertex -> Elim Vertex -> MayFailT m (Env Vertex × Cont Vertex × Set Vertex) +match + :: forall m + . MonadGraphAlloc m + => MonadError String m + => Val Vertex + -> Elim Vertex + -> m (Env Vertex × Cont Vertex × Set Vertex) match v (ElimVar x κ) | x == varAnon = pure (D.empty × κ × empty) | otherwise = pure (D.singleton x v × κ × empty) @@ -58,26 +65,39 @@ match (V.Constr α c vs) (ElimConstr m) = do pure (γ × κ' × (insert α αs)) match v (ElimConstr m) = do d <- dataTypeFor $ D.keys m - report $ patternMismatch (prettyP v) (show d) + throwError $ patternMismatch (prettyP v) (show d) match (V.Record α xvs) (ElimRecord xs κ) = do check (S.subset xs (S.fromFoldable $ D.keys xvs)) $ patternMismatch (show (D.keys xvs)) (show xs) let xs' = xs # S.toUnfoldable γ × κ' × αs <- matchMany (flip D.get xvs <$> xs') κ pure $ γ × κ' × (insert α αs) -match v (ElimRecord xs _) = report (patternMismatch (prettyP v) (show xs)) +match v (ElimRecord xs _) = throwError (patternMismatch (prettyP v) (show xs)) -matchMany :: forall m. Monad m => List (Val Vertex) -> Cont Vertex -> MayFailT m (Env Vertex × Cont Vertex × Set Vertex) +matchMany + :: forall m + . MonadGraphAlloc m + => MonadError String m + => List (Val Vertex) + -> Cont Vertex + -> m (Env Vertex × Cont Vertex × Set Vertex) matchMany Nil κ = pure (D.empty × κ × empty) matchMany (v : vs) (ContElim σ) = do γ × κ × αs <- match v σ γ' × κ' × βs <- matchMany vs κ pure $ γ `D.disjointUnion` γ' × κ' × (αs `union` βs) -matchMany (_ : vs) (ContExpr _) = report $ +matchMany (_ : vs) (ContExpr _) = throwError $ show (length vs + 1) <> " extra argument(s) to constructor/record; did you forget parentheses in lambda pattern?" matchMany _ _ = error "absurd" -closeDefs :: forall m. Monad m => Env Vertex -> RecDefs Vertex -> Set Vertex -> WithGraphAllocT m (Env Vertex) +closeDefs + :: forall m + . MonadGraphAlloc m + => MonadThrow String m + => Env Vertex + -> RecDefs Vertex + -> Set Vertex + -> m (Env Vertex) closeDefs γ ρ αs = flip traverse ρ \σ -> let @@ -86,7 +106,13 @@ closeDefs γ ρ αs = V.Fun <$> new αs <@> V.Closure (γ `restrict` (fv ρ' `S.union` fv σ)) ρ' σ {-# Evaluation #-} -apply :: forall m. Monad m => Val Vertex -> Val Vertex -> WithGraphAllocT m (Val Vertex) +apply + :: forall m + . MonadGraphAlloc m + => MonadError String m + => Val Vertex + -> Val Vertex + -> m (Val Vertex) apply (V.Fun α (V.Closure γ1 ρ σ)) v = do γ2 <- closeDefs γ1 ρ (singleton α) γ3 × κ × αs <- match v σ @@ -96,7 +122,7 @@ apply (V.Fun α (V.Foreign φ vs)) v = where vs' = snoc vs v - apply' :: forall t. ForeignOp' t -> WithGraphAllocT m (Val Vertex) + apply' :: forall t. ForeignOp' t -> m (Val Vertex) apply' (ForeignOp' φ') = if φ'.arity > length vs' then V.Fun <$> new (singleton α) <@> V.Foreign φ vs' @@ -107,9 +133,16 @@ apply (V.Fun α (V.PartialConstr c vs)) v = do else pure $ V.Constr α c (snoc vs v) where n = successful (arity c) -apply _ v = report $ "Found " <> prettyP v <> ", expected function" +apply _ v = throwError $ "Found " <> prettyP v <> ", expected function" -eval :: forall m. Monad m => Env Vertex -> Expr Vertex -> Set Vertex -> WithGraphAllocT m (Val Vertex) +eval + :: forall m + . MonadGraphAlloc m + => MonadError String m + => Env Vertex + -> Expr Vertex + -> Set Vertex + -> m (Val Vertex) eval γ (Var x) _ = lookup' x γ eval γ (Op op) _ = lookup' op γ eval _ (Int α n) αs = V.Int <$> new (insert α αs) <@> n @@ -148,7 +181,7 @@ eval γ (Project e x) αs = do v <- eval γ e αs case v of V.Record _ xvs -> lookup' x xvs - _ -> report $ "Found " <> prettyP v <> ", expected record" + _ -> throwError $ "Found " <> prettyP v <> ", expected record" eval γ (App e e') αs = do v <- eval γ e αs v' <- eval γ e' αs diff --git a/src/Primitive/Defs.purs b/src/Primitive/Defs.purs index 1bb5e122e..18ccefffc 100644 --- a/src/Primitive/Defs.purs +++ b/src/Primitive/Defs.purs @@ -2,6 +2,7 @@ module Primitive.Defs where import Prelude hiding (absurd, apply, div, mod, top) +import Control.Monad.Error.Class (throwError) import Data.Exists (mkExists) import Data.Foldable (foldl, foldM) import Data.FoldableWithIndex (foldWithIndexM) @@ -26,7 +27,7 @@ import Partial.Unsafe (unsafePartial) import Prelude (div, mod) as P import Primitive (binary, binaryZero, boolean, int, intOrNumber, intOrNumberOrString, number, string, unary, union, union1, unionStr) import Trace (AppTrace) -import Util (type (+), type (×), Endo, error, orElse, report, unimplemented, (×)) +import Util (type (+), type (×), Endo, error, orElse, unimplemented, (×)) import Val (Array2, DictRep(..), Env, ForeignOp, ForeignOp'(..), Fun(..), MatrixRep(..), OpBwd, OpFwd, OpGraph, Val(..), matrixGet, matrixUpdate) extern :: forall a. BoundedJoinSemilattice a => ForeignOp -> Val a @@ -73,11 +74,11 @@ error_ = mkExists $ ForeignOp' { arity: 1, op': op', op: fwd, op_bwd: unsafePart where op' :: OpGraph op' (Str _ s : Nil) = pure $ error s - op' _ = report "String expected" + op' _ = throwError "String expected" fwd :: OpFwd Unit fwd (Str _ s : Nil) = error s - fwd _ = report "String expected" + fwd _ = throwError "String expected" bwd :: OpBwd Unit bwd _ = error unimplemented @@ -87,11 +88,11 @@ debugLog = mkExists $ ForeignOp' { arity: 1, op': op', op: fwd, op_bwd: unsafePa where op' :: OpGraph op' (x : Nil) = pure $ trace x (const x) - op' _ = report "Single value expected" + op' _ = throwError "Single value expected" fwd :: OpFwd Unit fwd (x : Nil) = pure $ unit × trace x (const x) - fwd _ = report "Single value expected" + fwd _ = throwError "Single value expected" bwd :: OpBwd Unit bwd _ = error unimplemented @@ -106,12 +107,12 @@ dims = mkExists $ ForeignOp' { arity: 1, op': op, op: fwd, op_bwd: unsafePartial v1 <- Int <$> new (singleton β1) <@> i v2 <- Int <$> new (singleton β2) <@> j Constr <$> new (singleton α) <@> cPair <@> (v1 : v2 : Nil) - op _ = report "Matrix expected" + op _ = throwError "Matrix expected" fwd :: OpFwd (Raw ArrayData) fwd (Matrix α (MatrixRep (vss × (i × β1) × (j × β2))) : Nil) = pure $ (map erase <$> vss) × Constr α cPair (Int β1 i : Int β2 j : Nil) - fwd _ = report "Matrix expected" + fwd _ = throwError "Matrix expected" bwd :: Partial => OpBwd (Raw ArrayData) bwd (vss × Constr α c (Int β1 i : Int β2 j : Nil)) | c == cPair = @@ -123,14 +124,14 @@ matrixLookup = mkExists $ ForeignOp' { arity: 2, op': op, op: fwd, op_bwd: bwd } op :: OpGraph op (Matrix _ r : Constr _ c (Int _ i : Int _ j : Nil) : Nil) | c == cPair = matrixGet i j r - op _ = report "Matrix and pair of integers expected" + op _ = throwError "Matrix and pair of integers expected" fwd :: OpFwd (Raw ArrayData × (Int × Int) × (Int × Int)) fwd (Matrix _ r@(MatrixRep (vss × (i' × _) × (j' × _))) : Constr _ c (Int _ i : Int _ j : Nil) : Nil) | c == cPair = do v <- matrixGet i j r pure $ ((map erase <$> vss) × (i' × j') × (i × j)) × v - fwd _ = report "Matrix and pair of integers expected" + fwd _ = throwError "Matrix and pair of integers expected" bwd :: OpBwd (Raw ArrayData × (Int × Int) × (Int × Int)) bwd ((vss × (i' × j') × (i × j)) × v) = @@ -144,12 +145,12 @@ dict_difference = mkExists $ ForeignOp' { arity: 2, op': op, op: fwd, op_bwd: un op :: OpGraph op (Dictionary α (DictRep d) : Dictionary β (DictRep d') : Nil) = Dictionary <$> new (singleton α # insert β) <@> DictRep (d \\ d') - op _ = report "Dictionaries expected." + op _ = throwError "Dictionaries expected." fwd :: OpFwd Unit fwd (Dictionary α (DictRep d) : Dictionary α' (DictRep d') : Nil) = pure $ unit × Dictionary (α ∧ α') (DictRep (d \\ d')) - fwd _ = report "Dictionaries expected." + fwd _ = throwError "Dictionaries expected." bwd :: Partial => OpBwd Unit bwd (_ × Dictionary α d) = @@ -162,12 +163,12 @@ dict_fromRecord = mkExists $ ForeignOp' { arity: 1, op': op, op: fwd, op_bwd: un op (Record α xvs : Nil) = do xvs' <- for xvs (\v -> new (singleton α) <#> (_ × v)) Dictionary <$> new (singleton α) <@> DictRep xvs' - op _ = report "Record expected." + op _ = throwError "Record expected." fwd :: OpFwd Unit fwd (Record α xvs : Nil) = pure $ unit × Dictionary α (DictRep $ xvs <#> (α × _)) - fwd _ = report "Record expected." + fwd _ = throwError "Record expected." bwd :: Partial => OpBwd Unit bwd (_ × Dictionary α (DictRep d)) = @@ -179,12 +180,12 @@ dict_disjointUnion = mkExists $ ForeignOp' { arity: 2, op': op, op: fwd, op_bwd: op :: OpGraph op (Dictionary α (DictRep d) : Dictionary β (DictRep d') : Nil) = do Dictionary <$> new (singleton α # insert β) <@> DictRep (D.disjointUnion d d') - op _ = report "Dictionaries expected" + op _ = throwError "Dictionaries expected" fwd :: OpFwd (Dict Unit × Dict Unit) fwd (Dictionary α (DictRep d) : Dictionary α' (DictRep d') : Nil) = pure $ ((const unit <$> d) × (const unit <$> d')) × Dictionary (α ∧ α') (DictRep $ D.disjointUnion d d') - fwd _ = report "Dictionaries expected" + fwd _ = throwError "Dictionaries expected" bwd :: Partial => OpBwd (Dict Unit × Dict Unit) bwd ((d × d') × Dictionary α (DictRep d'')) = @@ -196,7 +197,7 @@ dict_foldl = mkExists $ ForeignOp' { arity: 3, op': op, op: fwd, op_bwd: unsafeP op :: OpGraph op (v : u : Dictionary _ (DictRep d) : Nil) = foldM (\u1 (_ × u2) -> G.apply v u1 >>= flip G.apply u2) u d - op _ = report "Function, value and dictionary expected" + op _ = throwError "Function, value and dictionary expected" fwd :: OpFwd (Raw Val × List (String × AppTrace × AppTrace)) fwd (v : u : Dictionary _ (DictRep d) : Nil) = do @@ -207,7 +208,7 @@ dict_foldl = mkExists $ ForeignOp' { arity: 3, op': op, op: fwd, op_bwd: unsafeP d -- :: MayFail (List (String × AppTrace × AppTrace) × Val _) pure $ (erase v × ts) × u' - fwd _ = report "Function, value and dictionary expected" + fwd _ = throwError "Function, value and dictionary expected" bwd :: Partial => OpBwd (Raw Val × List (String × AppTrace × AppTrace)) bwd ((v × ts) × u) = v' : u' : Dictionary bot (DictRep d) : Nil @@ -225,12 +226,12 @@ dict_get = mkExists $ ForeignOp' { arity: 2, op': op, op: fwd, op_bwd: unsafePar op :: OpGraph op (Str _ s : Dictionary _ (DictRep d) : Nil) = snd <$> D.lookup s d # orElse ("Key \"" <> s <> "\" not found") - op _ = report "String and dictionary expected" + op _ = throwError "String and dictionary expected" fwd :: OpFwd String fwd (Str _ s : Dictionary _ (DictRep d) : Nil) = (s × _) <$> (snd <$> D.lookup s d # orElse ("Key \"" <> s <> "\" not found")) - fwd _ = report "String and dictionary expected" + fwd _ = throwError "String and dictionary expected" bwd :: Partial => OpBwd String bwd (s × v) = @@ -247,7 +248,7 @@ dict_intersectionWith = mkExists $ ForeignOp' { arity: 3, op': op, op: fwd, op_b apply' (β × u) (β' × u') = do β'' <- new (singleton β # insert β') (×) β'' <$> (G.apply v u >>= flip G.apply u') - op _ = report "Function and two dictionaries expected" + op _ = throwError "Function and two dictionaries expected" fwd :: OpFwd (Raw Val × Dict (AppTrace × AppTrace)) fwd (v : Dictionary α (DictRep d) : Dictionary α' (DictRep d') : Nil) = do @@ -256,7 +257,7 @@ dict_intersectionWith = mkExists $ ForeignOp' { arity: 3, op': op, op: fwd, op_b D.intersectionWith (\(β × u) (β' × u') -> (β ∧ β' × _) <$> apply2 (v × u × u')) d d' -- :: MayFailT m (Dict (_ × (AppTrace × AppTrace) × Val _)) pure $ (erase v × (d'' <#> snd >>> fst)) × Dictionary (α ∧ α') (DictRep (d'' <#> second snd)) - fwd _ = report "Function and two dictionaries expected" + fwd _ = throwError "Function and two dictionaries expected" bwd :: Partial => OpBwd (Raw Val × Dict (AppTrace × AppTrace)) bwd ((v × tts) × Dictionary α (DictRep βvs)) = @@ -277,13 +278,13 @@ dict_map = mkExists $ ForeignOp' { arity: 2, op': op, op: fwd, op_bwd: unsafePar op (v : Dictionary α (DictRep d) : Nil) = do d' <- traverse (\(β × u) -> (β × _) <$> G.apply v u) d Dictionary <$> new (singleton α) <@> DictRep d' - op _ = report "Function and dictionary expected" + op _ = throwError "Function and dictionary expected" fwd :: OpFwd (Raw Val × Dict AppTrace) fwd (v : Dictionary α (DictRep d) : Nil) = do ts × d' <- D.unzip <$> traverse (\(β × u) -> second (β × _) <$> apply (v × u)) d pure $ (erase v × ts) × Dictionary α (DictRep d') - fwd _ = report "Function and dictionary expected" + fwd _ = throwError "Function and dictionary expected" bwd :: Partial => OpBwd (Raw Val × Dict AppTrace) bwd ((v × ts) × Dictionary α (DictRep d')) = diff --git a/src/Util.purs b/src/Util.purs index 985ff5ef9..3456c2081 100644 --- a/src/Util.purs +++ b/src/Util.purs @@ -4,14 +4,14 @@ import Prelude hiding (absurd) import Control.Apply (lift2) import Control.Comonad (extract) -import Control.Monad.Except (Except, ExceptT(..), withExceptT, runExceptT, except) +import Control.Monad.Error.Class (class MonadError, class MonadThrow, catchError, throwError) +import Control.Monad.Except (Except, ExceptT(..), runExceptT, except) import Control.MonadPlus (class MonadPlus, empty) import Data.Array ((!!), updateAt) import Data.Either (Either(..)) -import Data.Either (note) as Either +import Data.Identity (Identity(..)) import Data.List (List(..), (:), intercalate) import Data.List.NonEmpty (NonEmptyList(..)) -import Data.Identity (Identity(..)) import Data.Map (Map) import Data.Map (lookup, unionWith) as M import Data.Maybe (Maybe(..)) @@ -58,10 +58,11 @@ onlyIf true = pure onlyIf false = const empty type MayFail a = Except String a -type MayFailT a = ExceptT String a +type MayFailT m = ExceptT String m -orElse :: forall a m. Monad m => String -> Maybe a -> MayFailT m a -orElse s = except <<< Either.note s +orElse :: forall a m. MonadThrow String m => String -> Maybe a -> m a +orElse s Nothing = throwError s +orElse _ (Just x) = pure x ignoreMessage :: forall a. MayFail a -> Maybe a ignoreMessage = runExceptT >>> extract >>> case _ of @@ -83,12 +84,12 @@ successfulWith :: String -> forall a. MayFail a -> a successfulWith msg = successful <<< with msg -- If the property fails, add an extra error message. -with :: forall a m. Functor m => String -> MayFailT m a -> MayFailT m a -with msg = withExceptT (\msg' -> msg' <> if msg == "" then "" else ("\n" <> msg)) +with :: forall a m. MonadError String m => String -> Endo (m a) +with msg m = catchError m (\msg' -> throwError $ msg' <> if msg == "" then "" else ("\n" <> msg)) -check :: forall m. Monad m => Boolean -> String -> MayFailT m Unit -check true _ = pure unit -check false msg = report msg +check :: forall m. MonadError String m => Boolean -> String -> m Unit +check true = const $ pure unit +check false = throwError mayEq :: forall a. Eq a => a -> a -> Maybe a mayEq x x' = whenever (x == x') x @@ -102,7 +103,7 @@ mustGeq x x' = definitely (show x <> " greater than " <> show x') (whenever (x > unionWithMaybe :: forall a b. Ord a => (b -> b -> Maybe b) -> Map a b -> Map a b -> Map a (Maybe b) unionWithMaybe f m m' = M.unionWith (\x -> lift2 f x >>> join) (Just <$> m) (Just <$> m') -mayFailEq :: forall a m. Monad m => Show a => Eq a => a -> a -> MayFailT m a +mayFailEq :: forall a m. MonadError String m => Show a => Eq a => a -> a -> m a mayFailEq x x' = x ≟ x' # orElse (show x <> " ≠ " <> show x') infixl 4 mayEq as ≟ diff --git a/src/Val.purs b/src/Val.purs index 880870f10..7aee90e56 100644 --- a/src/Val.purs +++ b/src/Val.purs @@ -4,6 +4,7 @@ import Prelude hiding (absurd, append) import Bindings (Var) import Control.Apply (lift2) +import Control.Monad.Error.Class (class MonadError, class MonadThrow) import Data.Array ((!!)) import Data.Array (zipWith) as A import Data.Bitraversable (bitraverse) @@ -19,9 +20,9 @@ import Expr (Elim, RecDefs, fv) import Foreign.Object (filterKeys, lookup, unionWith) import Foreign.Object (keys) as O import Graph (Vertex(..)) -import Graph.GraphWriter (WithGraphAllocT) +import Graph.GraphWriter (class MonadGraphAlloc) import Lattice (class BoundedJoinSemilattice, class BoundedLattice, class Expandable, class JoinSemilattice, class Neg, Raw, definedJoin, expand, maybeJoin, neg, (∨)) -import Util (Endo, MayFailT, type (×), (×), (≞), (≜), (!), error, orElse, report, unsafeUpdateAt) +import Util (type (×), Endo, error, orElse, report, unsafeUpdateAt, (!), (×), (≜), (≞)) import Util.Pretty (Doc, beside, text) data Val a @@ -50,9 +51,9 @@ instance Highlightable a => Highlightable (a × b) where instance (Ann a, BoundedLattice b) => Ann (a × b) -- similar to an isomorphism lens with complement t -type OpFwd t = forall a m. Ann a => Monad m => List (Val a) -> MayFailT m (t × Val a) +type OpFwd t = forall a m. Ann a => MonadError String m => List (Val a) -> m (t × Val a) type OpBwd t = forall a. Ann a => t × Val a -> List (Val a) -type OpGraph = forall m. Monad m => List (Val Vertex) -> WithGraphAllocT m (Val Vertex) +type OpGraph = forall m. MonadGraphAlloc m => MonadError String m => List (Val Vertex) -> m (Val Vertex) data ForeignOp' t = ForeignOp' { arity :: Int @@ -66,7 +67,7 @@ type ForeignOp = Exists ForeignOp' -- Environments. type Env a = Dict (Val a) -lookup' :: forall a m. Monad m => Var -> Dict a -> MayFailT m a +lookup' :: forall a m. MonadThrow String m => Var -> Dict a -> m a lookup' x γ = lookup x γ # orElse ("variable " <> x <> " not found") -- Want a monoid instance but needs a newtype @@ -104,7 +105,7 @@ newtype MatrixRep a = MatrixRep (Array2 (Val a) × (Int × a) × (Int × a)) type Array2 a = Array (Array a) -matrixGet :: forall a m. Monad m => Int -> Int -> MatrixRep a -> MayFailT m (Val a) +matrixGet :: forall a m. MonadThrow String m => Int -> Int -> MatrixRep a -> m (Val a) matrixGet i j (MatrixRep (vss × _ × _)) = orElse "Index out of bounds" $ do us <- vss !! (i - 1) From 67c75425d45dff1c9090593f76aea8241474c1ac Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Fri, 22 Sep 2023 07:26:11 +0100 Subject: [PATCH 05/15] =?UTF-8?q?=E2=9D=97=20[incomplete]:=20Some=20simpli?= =?UTF-8?q?fications.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/EvalGraph.purs | 42 +++++++++++++++++++++++++----------------- 1 file changed, 25 insertions(+), 17 deletions(-) diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index ce04a350b..400fd59dc 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -4,7 +4,6 @@ module EvalGraph , eval , evalWithConfig , eval_module - , graphGC , match , patternMismatch ) where @@ -28,7 +27,7 @@ import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, import GaloisConnection (GaloisConnection) import Graph (class Graph, Vertex) import Graph (vertices) as G -import Graph.GraphWriter (class MonadGraphAlloc, WithGraphAllocT, alloc, new, runWithGraphAllocT) +import Graph.GraphWriter (class MonadGraphAlloc, WithGraphAllocT, alloc, new, runWithGraphAlloc2T, runWithGraphAllocT) import Graph.Slice (bwdSlice, fwdSlice, vertices) import Lattice (Raw) import Pretty (prettyP) @@ -194,10 +193,17 @@ eval γ (LetRec ρ e) αs = do γ' <- closeDefs γ ρ αs eval (γ <+> γ') e αs -eval_module :: forall m. Monad m => Env Vertex -> Module Vertex -> Set Vertex -> WithGraphAllocT m (Env Vertex) +eval_module + :: forall m + . MonadGraphAlloc m + => MonadError String m + => Env Vertex + -> Module Vertex + -> Set Vertex + -> m (Env Vertex) eval_module γ = go D.empty where - go :: Env Vertex -> Module Vertex -> Set Vertex -> WithGraphAllocT m (Env Vertex) + go :: Env Vertex -> Module Vertex -> Set Vertex -> m (Env Vertex) go γ' (Module Nil) _ = pure γ' go y' (Module (Left (VarDef σ e) : ds)) αs = do v <- eval (γ <+> y') e αs @@ -208,14 +214,26 @@ eval_module γ = go D.empty go (γ' <+> γ'') (Module ds) αs -- TODO: Inline into graphGC -evalWithConfig :: forall g m a. Monad m => Graph g => GraphConfig g -> Expr a -> m (String + ((g × Int) × Expr Vertex × Val Vertex)) +evalWithConfig + :: forall g m a + . Monad m + => Graph g + => GraphConfig g + -> Expr a + -> m (String + ((g × Int) × Expr Vertex × Val Vertex)) evalWithConfig { g, n, γα } e = runWithGraphAllocT (g × n) $ do eα <- alloc e vα <- eval γα eα S.empty pure (eα × vα) -graphGC :: forall g. Graph g => GraphConfig g -> Raw Expr -> String + GaloisConnection (Set Vertex) (Set Vertex) +graphGC + :: forall g m + . Monad m + => Graph g + => GraphConfig g + -> Raw Expr + -> m (GaloisConnection (Set Vertex) (Set Vertex)) graphGC { g: g0, n, γα } e = do (g × _) × vα × eα <- m pure $ @@ -223,17 +241,7 @@ graphGC { g: g0, n, γα } e = do , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- needs to include γα } where - Identity m = (runWithGraphAllocT (g0 × n) :: _ -> Identity _) $ do - eα <- alloc e - vα <- eval γα eα S.empty - pure (vα × eα) -{- -graphGC2 :: forall g m. Monad m => Graph g => GraphConfig g -> Raw Expr -> m (String + GaloisConnection (Set Vertex) (Set Vertex)) -graphGC2 { g: g0, n, γα } e = do - ?_ - where - m = (runWithGraphAllocT (g0 × n) :: _ -> m _) $ do + m = runWithGraphAlloc2T (g0 × n) $ do eα <- alloc e vα <- eval γα eα S.empty pure (vα × eα) --} From 0b9c360c9171c56201c7fc0e4f64939a2ff57d13 Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Fri, 22 Sep 2023 08:04:40 +0100 Subject: [PATCH 06/15] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20More=20mo?= =?UTF-8?q?nad=20cleanup.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Desugarable.purs | 5 +++-- src/EvalGraph.purs | 19 ++++++++++--------- src/Expr.purs | 11 ++++++----- src/Graph/GraphWriter.purs | 7 ++++--- src/Lattice.purs | 14 ++++++++------ src/Module.purs | 26 ++++++++++++++------------ src/SExpr.purs | 33 +++++++++++++++++---------------- src/Val.purs | 8 ++++---- 8 files changed, 66 insertions(+), 57 deletions(-) diff --git a/src/Desugarable.purs b/src/Desugarable.purs index 115fb94c6..f83f84767 100644 --- a/src/Desugarable.purs +++ b/src/Desugarable.purs @@ -1,9 +1,10 @@ module Desugarable where import Prelude + +import Control.Monad.Error.Class (class MonadError) import Lattice (Raw, class JoinSemilattice, class BoundedJoinSemilattice) -import Util (MayFailT) class (Functor s, Functor e) <= Desugarable s e | s -> e where - desug :: forall a m. Monad m => JoinSemilattice a => s a -> MayFailT m (e a) + desug :: forall a m. MonadError String m => JoinSemilattice a => s a -> m (e a) desugBwd :: forall a. BoundedJoinSemilattice a => e a -> Raw s -> s a diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index 400fd59dc..6b8cecf88 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -15,21 +15,21 @@ import Control.Monad.Error.Class (class MonadError, class MonadThrow, throwError import Data.Array (range, singleton) as A import Data.Either (Either(..)) import Data.Exists (runExists) -import Data.Identity (Identity(..)) +--import Data.Identity (Identity(..)) import Data.List (List(..), (:), length, snoc, unzip, zip) -import Data.Set (Set, empty, insert, intersection, singleton, union) +import Data.Set (Set, empty, insert, {-intersection, -}singleton, union) import Data.Set as S import Data.Traversable (sequence, traverse) import Data.Tuple (fst) import DataType (checkArity, arity, consistentWith, dataTypeFor, showCtr) import Dict (disjointUnion, fromFoldable, empty, get, keys, lookup, singleton) as D import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, asExpr) -import GaloisConnection (GaloisConnection) +--import GaloisConnection (GaloisConnection) import Graph (class Graph, Vertex) -import Graph (vertices) as G -import Graph.GraphWriter (class MonadGraphAlloc, WithGraphAllocT, alloc, new, runWithGraphAlloc2T, runWithGraphAllocT) -import Graph.Slice (bwdSlice, fwdSlice, vertices) -import Lattice (Raw) +--import Graph (vertices) as G +import Graph.GraphWriter (class MonadGraphAlloc, {-WithGraphAllocT, -}alloc, new, {-runWithGraphAlloc2T, -}runWithGraphAllocT) +--import Graph.Slice (bwdSlice, fwdSlice, vertices) +--import Lattice (Raw) import Pretty (prettyP) import Primitive (string, intPair) import Util (type (+), type (×), (×), check, error, successful, with, orElse) @@ -226,7 +226,7 @@ evalWithConfig { g, n, γα } e = eα <- alloc e vα <- eval γα eα S.empty pure (eα × vα) - +{- graphGC :: forall g m . Monad m @@ -238,10 +238,11 @@ graphGC { g: g0, n, γα } e = do (g × _) × vα × eα <- m pure $ { fwd: \αs -> G.vertices (fwdSlice αs g) `intersection` vertices vα - , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- needs to include γα + , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- TODO: include γα } where m = runWithGraphAlloc2T (g0 × n) $ do eα <- alloc e vα <- eval γα eα S.empty pure (vα × eα) +-} \ No newline at end of file diff --git a/src/Expr.purs b/src/Expr.purs index a2041b453..eab3ccdf2 100644 --- a/src/Expr.purs +++ b/src/Expr.purs @@ -4,8 +4,9 @@ import Prelude hiding (absurd, top) import Bindings (Var) import Control.Apply (lift2) -import Data.Foldable (class Foldable) +import Control.Monad.Error.Class (throwError) import Data.Either (Either(..)) +import Data.Foldable (class Foldable) import Data.List (List(..), (:), zipWith) import Data.Set (Set, difference, empty, singleton, union, unions) import Data.Set (fromFoldable) as S @@ -15,7 +16,7 @@ import DataType (Ctr, consistentWith) import Dict (Dict, keys, asSingletonMap) import Dict (apply2) as D import Lattice (class BoundedJoinSemilattice, class Expandable, class JoinSemilattice, Raw, (∨), definedJoin, expand, maybeJoin) -import Util (type (+), type (×), both, error, report, (×), (≜), (≞)) +import Util (type (+), type (×), both, error, (×), (≜), (≞)) import Util.Pair (Pair, toTuple) data Expr a @@ -180,7 +181,7 @@ instance JoinSemilattice a => JoinSemilattice (Elim a) where maybeJoin (ElimConstr cκs) (ElimConstr cκs') = ElimConstr <$> ((keys cκs `consistentWith` keys cκs') *> maybeJoin cκs cκs') maybeJoin (ElimRecord xs κ) (ElimRecord ys κ') = ElimRecord <$> (xs ≞ ys) <*> maybeJoin κ κ' - maybeJoin _ _ = report "Incompatible eliminators" + maybeJoin _ _ = throwError "Incompatible eliminators" join σ = definedJoin σ @@ -194,7 +195,7 @@ instance JoinSemilattice a => JoinSemilattice (Cont a) where maybeJoin ContNone ContNone = pure ContNone maybeJoin (ContExpr e) (ContExpr e') = ContExpr <$> maybeJoin e e' maybeJoin (ContElim σ) (ContElim σ') = ContElim <$> maybeJoin σ σ' - maybeJoin _ _ = report "Incompatible continuations" + maybeJoin _ _ = throwError "Incompatible continuations" join κ = definedJoin κ @@ -227,7 +228,7 @@ instance JoinSemilattice a => JoinSemilattice (Expr a) where maybeJoin (App e1 e2) (App e1' e2') = App <$> maybeJoin e1 e1' <*> maybeJoin e2 e2' maybeJoin (Let def e) (Let def' e') = Let <$> maybeJoin def def' <*> maybeJoin e e' maybeJoin (LetRec ρ e) (LetRec ρ' e') = LetRec <$> maybeJoin ρ ρ' <*> maybeJoin e e' - maybeJoin _ _ = report "Incompatible expressions" + maybeJoin _ _ = throwError "Incompatible expressions" join e = definedJoin e diff --git a/src/Graph/GraphWriter.purs b/src/Graph/GraphWriter.purs index 16205f611..1dfd0d7d4 100644 --- a/src/Graph/GraphWriter.purs +++ b/src/Graph/GraphWriter.purs @@ -20,16 +20,17 @@ module Graph.GraphWriter ) where import Prelude -import Control.Monad.Except (runExceptT) + +import Control.Monad.Except (class MonadError, runExceptT) import Control.Monad.State (StateT, runState, runStateT, modify, modify_) import Control.Monad.Trans.Class (lift) import Data.Identity (Identity) import Data.List (List(..), (:)) import Data.Newtype (unwrap) import Data.Profunctor.Strong (first) +import Data.Set (Set) import Data.Traversable (class Traversable, traverse) import Data.Tuple (swap) -import Data.Set (Set) import Graph (Vertex(..), class Graph, fromFoldable) import Util (MayFailT, type (×), type (+), (×)) @@ -40,7 +41,7 @@ class Monad m <= MonadGraph m where class Monad m <= MonadAlloc m where fresh :: m Vertex -class (MonadAlloc m, MonadGraph m) <= MonadGraphAlloc m where +class (MonadAlloc m, MonadError String m, MonadGraph m) <= MonadGraphAlloc m where -- Extend with a freshly allocated vertex. new :: Set Vertex -> m Vertex diff --git a/src/Lattice.purs b/src/Lattice.purs index a76323661..43f24c33f 100644 --- a/src/Lattice.purs +++ b/src/Lattice.purs @@ -1,7 +1,10 @@ module Lattice where import Prelude hiding (absurd, join, top) + +import Bindings (Var) import Control.Apply (lift2) +import Control.Monad.Error.Class (class MonadError, throwError) import Data.Array (zipWith) as A import Data.Foldable (length, foldM) import Data.List (List, zipWith) @@ -10,15 +13,14 @@ import Data.Profunctor.Strong ((***)) import Data.Set (subset) import Data.Traversable (sequence) import Dict (Dict, difference, intersectionWith, lookup, insert, keys, toUnfoldable, union, unionWith, update) -import Bindings (Var) -import Util (Endo, MayFailT, type (×), (×), assert, report, successfulWith) +import Util (Endo, type (×), (×), assert, successfulWith) import Util.Pair (Pair(..)) -- join here is actually more general "weak join" operation of the formalism, which operates on maps using unionWith. class JoinSemilattice a where join :: a -> a -> a -- soft failure for joining incompatible eliminators, used to desugar function clauses - maybeJoin :: forall m. Monad m => a -> a -> MayFailT m a + maybeJoin :: forall m. MonadError String m => a -> a -> m a class MeetSemilattice a where meet :: a -> a -> a @@ -119,7 +121,7 @@ instance JoinSemilattice a => JoinSemilattice (List a) where join xs = definedJoin xs maybeJoin xs ys | (length xs :: Int) == length ys = sequence (zipWith maybeJoin xs ys) - | otherwise = report "Mismatched list lengths" + | otherwise = throwError "Mismatched list lengths" instance JoinSemilattice a => JoinSemilattice (Dict a) where join = unionWith (∨) -- faster than definedJoin @@ -128,7 +130,7 @@ instance JoinSemilattice a => JoinSemilattice (Dict a) where instance Neg a => Neg (Dict a) where neg = (<$>) neg -mayFailUpdate :: forall a m. Monad m => JoinSemilattice a => Dict a -> Var × a -> MayFailT m (Dict a) +mayFailUpdate :: forall a m. MonadError String m => JoinSemilattice a => Dict a -> Var × a -> m (Dict a) mayFailUpdate m (k × v) = case lookup k m of Nothing -> pure (insert k v m) @@ -138,7 +140,7 @@ instance JoinSemilattice a => JoinSemilattice (Array a) where join xs = definedJoin xs maybeJoin xs ys | length xs == (length ys :: Int) = sequence (A.zipWith maybeJoin xs ys) - | otherwise = report "Mismatched array lengths" + | otherwise = throwError "Mismatched array lengths" instance (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a diff --git a/src/Module.purs b/src/Module.purs index 79f856a1b..55f0f0a15 100644 --- a/src/Module.purs +++ b/src/Module.purs @@ -5,9 +5,8 @@ import Prelude import Affjax.ResponseFormat (string) import Affjax.Web (defaultRequest, printError, request) import Bindings (Var) -import Control.Monad.Except (except) -import Control.Monad.Trans.Class (lift) -import Data.Bifunctor (bimap) +import Control.Monad.Error.Class (throwError) +import Control.Monad.Except (class MonadError) import Data.Either (Either(..)) import Data.HTTP.Method (Method(..)) import Data.Newtype (class Newtype) @@ -16,18 +15,19 @@ import Data.Traversable (traverse) import Desugarable (desug) import Dict (singleton) as D import Effect.Aff (Aff) +import Effect.Aff.Class (class MonadAff, liftAff) import EvalGraph (GraphConfig, eval, eval_module) import Expr (traverseModule) import Graph (class Graph, Vertex) import Graph (empty) as G -import Graph.GraphWriter (WithGraphAllocT, runWithGraphAllocT, alloc, fresh) +import Graph.GraphWriter (class MonadGraphAlloc, alloc, fresh, runWithGraphAllocT) import Lattice (botOf) import Parse (module_, program) import Parsing (runParser) import Primitive.Defs (primitives) import SExpr (Expr) as S import SExpr (desugarModuleFwd) -import Util (MayFailT, type (×), (×), error, successful, fromRight) +import Util (type (×), (×), error, successful, fromRight) import Util.Parse (SParser) import Val (Env, (<+>)) @@ -48,8 +48,10 @@ loadFile (Folder folder) (File file) = do Left err -> error (printError err) Right response -> pure response.body -parse :: forall t m. Monad m => String -> SParser t -> MayFailT m t -parse src = runParser src >>> show `bimap` identity >>> except +parse :: forall a m. MonadError String m => String -> SParser a -> m a +parse src p = case runParser src p of + Left err -> throwError $ show err + Right x -> pure x parseProgram :: Folder -> File -> Aff (S.Expr Unit) parseProgram folder file = do @@ -59,24 +61,24 @@ parseProgram folder file = do open :: File -> Aff (S.Expr Unit) open = parseProgram (Folder "fluid/example") -loadModule :: File -> Env Vertex -> WithGraphAllocT Aff (Env Vertex) +loadModule :: forall m. MonadAff m => MonadGraphAlloc m => File -> Env Vertex -> m (Env Vertex) loadModule file γ = do - src <- lift $ lift $ lift $ loadFile (Folder "fluid/lib") file + src <- liftAff $ loadFile (Folder "fluid/lib") file mod <- parse src module_ >>= desugarModuleFwd >>= traverseModule (const fresh) eval_module γ mod empty <#> (γ <+> _) -defaultImports :: WithGraphAllocT Aff (Env Vertex) +defaultImports :: forall m. MonadAff m => MonadGraphAlloc m => m (Env Vertex) defaultImports = do γα <- traverse alloc primitives loadModule (File "prelude") γα >>= loadModule (File "graphics") >>= loadModule (File "convolution") --- | Evaluates the default imports from an empty initial graph config +-- | Evaluates default imports from empty initial graph config openDefaultImports :: forall g. Graph g => Aff (GraphConfig g) openDefaultImports = do (g × n) × γα <- fromRight <$> runWithGraphAllocT (G.empty × 0) defaultImports pure $ { g, n, γα } --- | Evaluates a dataset from an existing graph config (produced by openDefaultImports) +-- | Evaluate dataset in context of existing graph config openDatasetAs :: forall g. Graph g => File -> Var -> GraphConfig g -> Aff (GraphConfig g × Env Vertex) openDatasetAs file x { g, n, γα } = do s <- parseProgram (Folder "fluid") file diff --git a/src/SExpr.purs b/src/SExpr.purs index 22eb81ade..1e98d5f7d 100644 --- a/src/SExpr.purs +++ b/src/SExpr.purs @@ -3,6 +3,7 @@ module SExpr where import Prelude hiding (absurd, top) import Bindings (Bind, Var, varAnon, (↦), keys) +import Control.Monad.Error.Class (class MonadError) import Data.Either (Either(..)) import Data.Foldable (foldM, foldl) import Data.Function (applyN, on) @@ -26,7 +27,7 @@ import Expr (Cont(..), Elim(..), asElim, asExpr) import Expr (Expr(..), Module(..), RecDefs, VarDef(..)) as E import Lattice (class JoinSemilattice, (∨), bot, definedJoin, maybeJoin, class BoundedJoinSemilattice, Raw) import Partial.Unsafe (unsafePartial) -import Util (type (+), type (×), Endo, MayFailT, absurd, error, successful, unimplemented, (×)) +import Util (type (+), type (×), Endo, absurd, error, successful, unimplemented, (×)) import Util.Pair (Pair(..)) -- Surface language expressions. @@ -142,7 +143,7 @@ instance Desugarable Clauses Elim where desug = clausesFwd desugBwd = clausesBwd -desugarModuleFwd :: forall a m. Monad m => JoinSemilattice a => Module a -> MayFailT m (E.Module a) +desugarModuleFwd :: forall a m. MonadError String m => JoinSemilattice a => Module a -> m (E.Module a) desugarModuleFwd = moduleFwd -- helpers @@ -156,10 +157,10 @@ elimBool :: forall a. Cont a -> Cont a -> Elim a elimBool κ κ' = ElimConstr (D.fromFoldable [ cTrue × κ, cFalse × κ' ]) -- Module. Surface language supports "blocks" of variable declarations; core does not. Currently no backward. -moduleFwd :: forall a m. Monad m => JoinSemilattice a => Module a -> MayFailT m (E.Module a) +moduleFwd :: forall a m. MonadError String m => JoinSemilattice a => Module a -> m (E.Module a) moduleFwd (Module ds) = E.Module <$> traverse varDefOrRecDefsFwd (join (flatten <$> ds)) where - varDefOrRecDefsFwd :: VarDef a + RecDefs a -> MayFailT m (E.VarDef a + E.RecDefs a) + varDefOrRecDefsFwd :: VarDef a + RecDefs a -> m (E.VarDef a + E.RecDefs a) varDefOrRecDefsFwd (Left d) = Left <$> varDefFwd d varDefOrRecDefsFwd (Right xcs) = Right <$> recDefsFwd xcs @@ -167,11 +168,11 @@ moduleFwd (Module ds) = E.Module <$> traverse varDefOrRecDefsFwd (join (flatten flatten (Left ds') = Left <$> toList ds' flatten (Right δ) = pure (Right δ) -varDefFwd :: forall a m. Monad m => JoinSemilattice a => VarDef a -> MayFailT m (E.VarDef a) +varDefFwd :: forall a m. MonadError String m => JoinSemilattice a => VarDef a -> m (E.VarDef a) varDefFwd (VarDef π s) = E.VarDef <$> pattContFwd π (ContNone :: Cont a) <*> desug s -- VarDefs -varDefsFwd :: forall a m. Monad m => JoinSemilattice a => VarDefs a × Expr a -> MayFailT m (E.Expr a) +varDefsFwd :: forall a m. MonadError String m => JoinSemilattice a => VarDefs a × Expr a -> m (E.Expr a) varDefsFwd (NonEmptyList (d :| Nil) × s) = E.Let <$> varDefFwd d <*> desug s varDefsFwd (NonEmptyList (d :| d' : ds) × s) = @@ -189,7 +190,7 @@ varDefsBwd _ (NonEmptyList (_ :| _) × _) = error absurd -- RecDefs -- In the formalism, "group by name" is part of the syntax. -recDefsFwd :: forall a m. Monad m => JoinSemilattice a => RecDefs a -> MayFailT m (E.RecDefs a) +recDefsFwd :: forall a m. MonadError String m => JoinSemilattice a => RecDefs a -> m (E.RecDefs a) recDefsFwd xcs = D.fromFoldable <$> traverse recDefFwd xcss where xcss = map RecDef (groupBy (eq `on` fst) xcs) :: NonEmptyList (RecDef a) @@ -208,14 +209,14 @@ recDefsBwd ρ xcs = join (go (groupBy (eq `on` fst) xcs)) NonEmptyList (unwrap (recDefBwd (x ↦ get x ρ) (RecDef xcs1)) :| xcss') -- RecDef -recDefFwd :: forall a m. Monad m => JoinSemilattice a => RecDef a -> MayFailT m (Bind (Elim a)) +recDefFwd :: forall a m. MonadError String m => JoinSemilattice a => RecDef a -> m (Bind (Elim a)) recDefFwd xcs = (fst (head (unwrap xcs)) ↦ _) <$> clausesFwd (Clauses (snd <$> unwrap xcs)) recDefBwd :: forall a. BoundedJoinSemilattice a => Bind (Elim a) -> Raw RecDef -> RecDef a recDefBwd (x ↦ σ) (RecDef bs) = RecDef ((x × _) <$> unwrap (clausesBwd σ (Clauses (snd <$> bs)))) -- Expr -exprFwd :: forall a m. Monad m => JoinSemilattice a => Expr a -> MayFailT m (E.Expr a) +exprFwd :: forall a m. MonadError String m => JoinSemilattice a => Expr a -> m (E.Expr a) exprFwd (Var x) = pure (E.Var x) exprFwd (Op op) = pure (E.Op op) exprFwd (Int α n) = pure (E.Int α n) @@ -277,7 +278,7 @@ exprBwd (E.LetRec xσs e) (LetRec xcs s) = LetRec (recDefsBwd xσs xcs) (desugBw exprBwd _ _ = error absurd -- ListRest -listRestFwd :: forall a m. Monad m => JoinSemilattice a => ListRest a -> MayFailT m (E.Expr a) +listRestFwd :: forall a m. MonadError String m => JoinSemilattice a => ListRest a -> m (E.Expr a) listRestFwd (End α) = pure (enil α) listRestFwd (Next α s l) = econs α <$> desug s <*> desug l @@ -288,7 +289,7 @@ listRestBwd (E.Constr α _ (e1 : e2 : Nil)) (Next _ s l) = listRestBwd _ _ = error absurd -- List Qualifier × Expr -listCompFwd :: forall a m. Monad m => JoinSemilattice a => a × List (Qualifier a) × Expr a -> MayFailT m (E.Expr a) +listCompFwd :: forall a m. MonadError String m => JoinSemilattice a => a × List (Qualifier a) × Expr a -> m (E.Expr a) listCompFwd (α × Nil × s) = econs α <$> desug s <@> enil α listCompFwd (α × (Guard s : qs) × s') = do @@ -325,7 +326,7 @@ listCompBwd (E.App (E.App (E.Var "concatMap") (E.Lambda σ)) e) ((Generator p s0 listCompBwd _ _ = error absurd -- NonEmptyList Pattern × Expr -pattsExprFwd :: forall a m. Monad m => JoinSemilattice a => NonEmptyList Pattern × Expr a -> MayFailT m (Elim a) +pattsExprFwd :: forall a m. MonadError String m => JoinSemilattice a => NonEmptyList Pattern × Expr a -> m (Elim a) pattsExprFwd (NonEmptyList (p :| Nil) × s) = (ContExpr <$> desug s) >>= pattContFwd p pattsExprFwd (NonEmptyList (p :| p' : ps) × s) = pattContFwd p =<< ContExpr <$> E.Lambda <$> pattsExprFwd (NonEmptyList (p' :| ps) × s) @@ -338,7 +339,7 @@ pattsExprBwd (NonEmptyList (p :| p' : ps) × s) σ = next (asExpr (pattContBwd p next _ = error absurd -- Pattern × Cont -pattContFwd :: forall a m. Monad m => Pattern -> Cont a -> MayFailT m (Elim a) +pattContFwd :: forall a m. MonadError String m => Pattern -> Cont a -> m (Elim a) pattContFwd (PVar x) κ = pure (ElimVar x κ) pattContFwd (PConstr c ps) κ = checkArity c (length ps) *> (ElimConstr <$> D.singleton c <$> pattArgsFwd (Left <$> ps) κ) @@ -356,7 +357,7 @@ pattContBwd (PRecord xps) (ElimRecord _ κ) = pattArgsBwd ((snd >>> Left) <$> so pattContBwd _ _ = error absurd -- ListRestPattern × Cont -pattCont_ListRest_Fwd :: forall a m. Monad m => ListRestPattern -> Cont a -> MayFailT m (Elim a) +pattCont_ListRest_Fwd :: forall a m. MonadError String m => ListRestPattern -> Cont a -> m (Elim a) pattCont_ListRest_Fwd PEnd κ = pure (ElimConstr (D.singleton cNil κ)) pattCont_ListRest_Fwd (PNext p o) κ = ElimConstr <$> D.singleton cCons <$> pattArgsFwd (Left p : Right o : Nil) κ @@ -367,7 +368,7 @@ pattCont_ListRest_Bwd (ElimConstr m) PEnd = get cNil m pattCont_ListRest_Bwd (ElimConstr m) (PNext p o) = pattArgsBwd (Left p : Right o : Nil) (get cCons m) -- List (Pattern + ListRestPattern) × Cont -pattArgsFwd :: forall a m. Monad m => List (Pattern + ListRestPattern) -> Cont a -> MayFailT m (Cont a) +pattArgsFwd :: forall a m. MonadError String m => List (Pattern + ListRestPattern) -> Cont a -> m (Cont a) pattArgsFwd Nil κ = pure κ pattArgsFwd (Left p : πs) κ = ContElim <$> (pattArgsFwd πs κ >>= pattContFwd p) pattArgsFwd (Right o : πs) κ = ContElim <$> (pattArgsFwd πs κ >>= pattCont_ListRest_Fwd o) @@ -378,7 +379,7 @@ pattArgsBwd (Left p : πs) σ = pattArgsBwd πs (pattContBwd p (asElim σ)) pattArgsBwd (Right o : πs) σ = pattArgsBwd πs (pattCont_ListRest_Bwd (asElim σ) o) -- Clauses -clausesFwd :: forall a m. Monad m => JoinSemilattice a => Clauses a -> MayFailT m (Elim a) +clausesFwd :: forall a m. MonadError String m => JoinSemilattice a => Clauses a -> m (Elim a) clausesFwd (Clauses bs) = do NonEmptyList (σ :| σs) <- traverse pattsExprFwd (unwrap <$> bs) foldM maybeJoin σ σs diff --git a/src/Val.purs b/src/Val.purs index 7aee90e56..3271c37e5 100644 --- a/src/Val.purs +++ b/src/Val.purs @@ -4,7 +4,7 @@ import Prelude hiding (absurd, append) import Bindings (Var) import Control.Apply (lift2) -import Control.Monad.Error.Class (class MonadError, class MonadThrow) +import Control.Monad.Error.Class (class MonadError, class MonadThrow, throwError) import Data.Array ((!!)) import Data.Array (zipWith) as A import Data.Bitraversable (bitraverse) @@ -22,7 +22,7 @@ import Foreign.Object (keys) as O import Graph (Vertex(..)) import Graph.GraphWriter (class MonadGraphAlloc) import Lattice (class BoundedJoinSemilattice, class BoundedLattice, class Expandable, class JoinSemilattice, class Neg, Raw, definedJoin, expand, maybeJoin, neg, (∨)) -import Util (type (×), Endo, error, orElse, report, unsafeUpdateAt, (!), (×), (≜), (≞)) +import Util (type (×), Endo, error, orElse, unsafeUpdateAt, (!), (×), (≜), (≞)) import Util.Pretty (Doc, beside, text) data Val a @@ -209,7 +209,7 @@ instance JoinSemilattice a => JoinSemilattice (Val a) where maybeJoin (Constr α c vs) (Constr α' c' us) = Constr (α ∨ α') <$> (c ≞ c') <*> maybeJoin vs us maybeJoin (Matrix α m) (Matrix α' m') = Matrix (α ∨ α') <$> maybeJoin m m' maybeJoin (Fun α φ) (Fun α' φ') = Fun (α ∨ α') <$> maybeJoin φ φ' - maybeJoin _ _ = report "Incompatible values" + maybeJoin _ _ = throwError "Incompatible values" join v = definedJoin v @@ -220,7 +220,7 @@ instance JoinSemilattice a => JoinSemilattice (Fun a) where Foreign φ <$> maybeJoin vs vs' -- TODO: require φ == φ' maybeJoin (PartialConstr c vs) (PartialConstr c' us) = PartialConstr <$> (c ≞ c') <*> maybeJoin vs us - maybeJoin _ _ = report "Incompatible functions" + maybeJoin _ _ = throwError "Incompatible functions" join v = definedJoin v From 66c0b28fdeb4ed62d04b90b9b3fb9c220f4f928d Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Fri, 22 Sep 2023 15:50:36 +0100 Subject: [PATCH 07/15] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Mostly=20?= =?UTF-8?q?done=20with=20old=20WithGraphAllocT.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Eval.purs | 6 +-- src/EvalGraph.purs | 86 +++++++++----------------------------- src/Graph/GraphWriter.purs | 12 +++++- src/Primitive/Defs.purs | 1 - src/Util.purs | 5 +-- test/Util.purs | 4 +- 6 files changed, 37 insertions(+), 77 deletions(-) diff --git a/src/Eval.purs b/src/Eval.purs index d83564cf7..7877cd4cd 100644 --- a/src/Eval.purs +++ b/src/Eval.purs @@ -24,7 +24,7 @@ import Pretty (prettyP) import Primitive (intPair, string) import Trace (AppTrace(..), Trace(..), VarDef(..)) as T import Trace (AppTrace, ForeignTrace, ForeignTrace'(..), Match(..), Trace) -import Util (type (×), MayFailT, absurd, both, check, error, successful, orElse, with, (×)) +import Util (type (×), absurd, both, check, error, successful, orElse, with, (×)) import Util.Pair (unzip) as P import Val (Fun(..), Val(..)) as V import Val (class Ann, DictRep(..), Env, ForeignOp'(..), MatrixRep(..), (<+>), Val, for, lookup', restrict) @@ -161,10 +161,10 @@ eval γ (LetRec ρ e) α = do t × v <- eval (γ <+> γ') e α pure $ T.LetRec (erase <$> ρ) t × v -eval_module :: forall a m. Monad m => Ann a => Env a -> Module a -> a -> MayFailT m (Env a) +eval_module :: forall a m. MonadError String m => Ann a => Env a -> Module a -> a -> m (Env a) eval_module γ = go empty where - go :: Env a -> Module a -> a -> MayFailT m (Env a) + go :: Env a -> Module a -> a -> m (Env a) go γ' (Module Nil) _ = pure γ' go y' (Module (Left (VarDef σ e) : ds)) α = do _ × v <- eval (γ <+> y') e α diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index 6b8cecf88..f0c731053 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -4,6 +4,7 @@ module EvalGraph , eval , evalWithConfig , eval_module + , graphGC , match , patternMismatch ) where @@ -11,28 +12,27 @@ module EvalGraph import Prelude hiding (apply, add) import Bindings (varAnon) -import Control.Monad.Error.Class (class MonadError, class MonadThrow, throwError) +import Control.Monad.Error.Class (class MonadError, throwError) import Data.Array (range, singleton) as A import Data.Either (Either(..)) import Data.Exists (runExists) ---import Data.Identity (Identity(..)) import Data.List (List(..), (:), length, snoc, unzip, zip) -import Data.Set (Set, empty, insert, {-intersection, -}singleton, union) +import Data.Set (Set, empty, insert, intersection, singleton, union) import Data.Set as S import Data.Traversable (sequence, traverse) import Data.Tuple (fst) import DataType (checkArity, arity, consistentWith, dataTypeFor, showCtr) import Dict (disjointUnion, fromFoldable, empty, get, keys, lookup, singleton) as D import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, asExpr) ---import GaloisConnection (GaloisConnection) +import GaloisConnection (GaloisConnection) import Graph (class Graph, Vertex) ---import Graph (vertices) as G -import Graph.GraphWriter (class MonadGraphAlloc, {-WithGraphAllocT, -}alloc, new, {-runWithGraphAlloc2T, -}runWithGraphAllocT) ---import Graph.Slice (bwdSlice, fwdSlice, vertices) ---import Lattice (Raw) +import Graph (vertices) as G +import Graph.GraphWriter (class MonadGraphAlloc, alloc, new, runWithGraphAlloc2T) +import Graph.Slice (bwdSlice, fwdSlice, vertices) +import Lattice (Raw) import Pretty (prettyP) import Primitive (string, intPair) -import Util (type (+), type (×), (×), check, error, successful, with, orElse) +import Util (type (×), (×), check, error, successful, with, orElse) import Util.Pair (unzip) as P import Val (DictRep(..), Env, ForeignOp'(..), MatrixRep(..), Val, for, lookup', restrict, (<+>)) import Val (Val(..), Fun(..)) as V @@ -47,13 +47,7 @@ type GraphConfig g = patternMismatch :: String -> String -> String patternMismatch s s' = "Pattern mismatch: found " <> s <> ", expected " <> s' -match - :: forall m - . MonadGraphAlloc m - => MonadError String m - => Val Vertex - -> Elim Vertex - -> m (Env Vertex × Cont Vertex × Set Vertex) +match :: forall m. MonadGraphAlloc m => Val Vertex -> Elim Vertex -> m (Env Vertex × Cont Vertex × Set Vertex) match v (ElimVar x κ) | x == varAnon = pure (D.empty × κ × empty) | otherwise = pure (D.singleton x v × κ × empty) @@ -73,13 +67,7 @@ match (V.Record α xvs) (ElimRecord xs κ) = do pure $ γ × κ' × (insert α αs) match v (ElimRecord xs _) = throwError (patternMismatch (prettyP v) (show xs)) -matchMany - :: forall m - . MonadGraphAlloc m - => MonadError String m - => List (Val Vertex) - -> Cont Vertex - -> m (Env Vertex × Cont Vertex × Set Vertex) +matchMany :: forall m. MonadGraphAlloc m => List (Val Vertex) -> Cont Vertex -> m (Env Vertex × Cont Vertex × Set Vertex) matchMany Nil κ = pure (D.empty × κ × empty) matchMany (v : vs) (ContElim σ) = do γ × κ × αs <- match v σ @@ -89,29 +77,16 @@ matchMany (_ : vs) (ContExpr _) = throwError $ show (length vs + 1) <> " extra argument(s) to constructor/record; did you forget parentheses in lambda pattern?" matchMany _ _ = error "absurd" -closeDefs - :: forall m - . MonadGraphAlloc m - => MonadThrow String m - => Env Vertex - -> RecDefs Vertex - -> Set Vertex - -> m (Env Vertex) +closeDefs :: forall m. MonadGraphAlloc m => Env Vertex -> RecDefs Vertex -> Set Vertex -> m (Env Vertex) closeDefs γ ρ αs = flip traverse ρ \σ -> let ρ' = ρ `for` σ in - V.Fun <$> new αs <@> V.Closure (γ `restrict` (fv ρ' `S.union` fv σ)) ρ' σ + V.Fun <$> new αs <@> V.Closure (γ `restrict` (fv ρ' `union` fv σ)) ρ' σ {-# Evaluation #-} -apply - :: forall m - . MonadGraphAlloc m - => MonadError String m - => Val Vertex - -> Val Vertex - -> m (Val Vertex) +apply :: forall m. MonadGraphAlloc m => Val Vertex -> Val Vertex -> m (Val Vertex) apply (V.Fun α (V.Closure γ1 ρ σ)) v = do γ2 <- closeDefs γ1 ρ (singleton α) γ3 × κ × αs <- match v σ @@ -134,14 +109,7 @@ apply (V.Fun α (V.PartialConstr c vs)) v = do n = successful (arity c) apply _ v = throwError $ "Found " <> prettyP v <> ", expected function" -eval - :: forall m - . MonadGraphAlloc m - => MonadError String m - => Env Vertex - -> Expr Vertex - -> Set Vertex - -> m (Val Vertex) +eval :: forall m. MonadGraphAlloc m => Env Vertex -> Expr Vertex -> Set Vertex -> m (Val Vertex) eval γ (Var x) _ = lookup' x γ eval γ (Op op) _ = lookup' op γ eval _ (Int α n) αs = V.Int <$> new (insert α αs) <@> n @@ -193,14 +161,7 @@ eval γ (LetRec ρ e) αs = do γ' <- closeDefs γ ρ αs eval (γ <+> γ') e αs -eval_module - :: forall m - . MonadGraphAlloc m - => MonadError String m - => Env Vertex - -> Module Vertex - -> Set Vertex - -> m (Env Vertex) +eval_module :: forall m. MonadGraphAlloc m => Env Vertex -> Module Vertex -> Set Vertex -> m (Env Vertex) eval_module γ = go D.empty where go :: Env Vertex -> Module Vertex -> Set Vertex -> m (Env Vertex) @@ -214,22 +175,16 @@ eval_module γ = go D.empty go (γ' <+> γ'') (Module ds) αs -- TODO: Inline into graphGC -evalWithConfig - :: forall g m a - . Monad m - => Graph g - => GraphConfig g - -> Expr a - -> m (String + ((g × Int) × Expr Vertex × Val Vertex)) +evalWithConfig :: forall g m a. MonadError String m => Graph g => GraphConfig g -> Expr a -> m ((g × Int) × Expr Vertex × Val Vertex) evalWithConfig { g, n, γα } e = - runWithGraphAllocT (g × n) $ do + runWithGraphAlloc2T (g × n) $ do eα <- alloc e vα <- eval γα eα S.empty pure (eα × vα) -{- + graphGC :: forall g m - . Monad m + . MonadError String m => Graph g => GraphConfig g -> Raw Expr @@ -245,4 +200,3 @@ graphGC { g: g0, n, γα } e = do eα <- alloc e vα <- eval γα eα S.empty pure (vα × eα) --} \ No newline at end of file diff --git a/src/Graph/GraphWriter.purs b/src/Graph/GraphWriter.purs index 1dfd0d7d4..4c3832880 100644 --- a/src/Graph/GraphWriter.purs +++ b/src/Graph/GraphWriter.purs @@ -2,6 +2,7 @@ module Graph.GraphWriter ( AdjMapEntries , WithAllocT , WithGraphAllocT + , WithGraphAlloc2T , WithGraph , WithGraphT , class MonadAlloc @@ -63,7 +64,13 @@ instance Monad m => MonadAlloc (WithAllocT m) where instance Monad m => MonadAlloc (WithGraphAllocT m) where fresh = lift fresh -instance (Monad m, MonadAlloc (WithGraphAllocT m), MonadGraph (WithGraphAllocT m)) => MonadGraphAlloc (WithGraphAllocT m) where +instance MonadError String m => MonadGraphAlloc (WithGraphAlloc2T m) where + new αs = do + α <- fresh + extend α αs + pure α + +instance Monad m => MonadGraphAlloc (WithGraphAllocT m) where new αs = do α <- fresh extend α αs @@ -73,6 +80,9 @@ instance Monad m => MonadGraph (WithGraphT m) where extend α αs = void $ modify_ $ (:) (α × αs) +instance Monad m => MonadGraph (WithGraphAlloc2T m) where + extend α = lift <<< extend α + instance Monad m => MonadGraph (WithGraphAllocT m) where extend α = lift <<< lift <<< extend α diff --git a/src/Primitive/Defs.purs b/src/Primitive/Defs.purs index 18ccefffc..c3cb1cab4 100644 --- a/src/Primitive/Defs.purs +++ b/src/Primitive/Defs.purs @@ -255,7 +255,6 @@ dict_intersectionWith = mkExists $ ForeignOp' { arity: 3, op': op, op: fwd, op_b d'' <- sequence $ D.intersectionWith (\(β × u) (β' × u') -> (β ∧ β' × _) <$> apply2 (v × u × u')) d d' - -- :: MayFailT m (Dict (_ × (AppTrace × AppTrace) × Val _)) pure $ (erase v × (d'' <#> snd >>> fst)) × Dictionary (α ∧ α') (DictRep (d'' <#> second snd)) fwd _ = throwError "Function and two dictionaries expected" diff --git a/src/Util.purs b/src/Util.purs index 3456c2081..a7c1ff46d 100644 --- a/src/Util.purs +++ b/src/Util.purs @@ -5,7 +5,7 @@ import Prelude hiding (absurd) import Control.Apply (lift2) import Control.Comonad (extract) import Control.Monad.Error.Class (class MonadError, class MonadThrow, catchError, throwError) -import Control.Monad.Except (Except, ExceptT(..), runExceptT, except) +import Control.Monad.Except (Except, ExceptT(..), runExceptT) import Control.MonadPlus (class MonadPlus, empty) import Data.Array ((!!), updateAt) import Data.Either (Either(..)) @@ -69,9 +69,6 @@ ignoreMessage = runExceptT >>> extract >>> case _ of (Left _) -> Nothing (Right x) -> Just x -report :: String -> forall a m. Applicative m => MayFailT m a -report s = except $ Left s - fromRight :: forall a. Either String a -> a fromRight (Right x) = x fromRight (Left msg) = error msg diff --git a/test/Util.purs b/test/Util.purs index 759df25ce..24b1ac365 100644 --- a/test/Util.purs +++ b/test/Util.purs @@ -5,7 +5,7 @@ import App.Fig (LinkFigSpec) import App.Util (Selector) import Benchmark.Util (BenchRow(..), GraphRow, TraceRow, preciseTime, tdiff) import Control.Monad.Error.Class (class MonadThrow) -import Control.Monad.Except (except, runExceptT) +import Control.Monad.Except (runExceptT) import Control.Monad.Trans.Class (lift) import Data.Either (Either(..)) import Data.Foldable (foldl) @@ -106,7 +106,7 @@ testGraph s gconf { δv, bwd_expect, fwd_expect } = do -- | Eval e <- desug s tEval1 <- preciseTime - (g × _) × eα × vα <- evalWithConfig gconf e >>= except + (g × _) × eα × vα <- evalWithConfig gconf e tEval2 <- preciseTime -- | Backward From 6b2c4e3b79e74518a986e6e14e1dcffaa3cd12dd Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Fri, 22 Sep 2023 15:51:20 +0100 Subject: [PATCH 08/15] =?UTF-8?q?=F0=9F=A7=A9=20[layout]?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Module.purs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Module.purs b/src/Module.purs index 55f0f0a15..76721eb36 100644 --- a/src/Module.purs +++ b/src/Module.purs @@ -83,10 +83,9 @@ openDatasetAs :: forall g. Graph g => File -> Var -> GraphConfig g -> Aff (Graph openDatasetAs file x { g, n, γα } = do s <- parseProgram (Folder "fluid") file (g' × n') × (γα' × xv) <- fromRight <$> - ( runWithGraphAllocT (g × n) $ do + runWithGraphAllocT (g × n) do e <- desug s eα <- alloc e vα <- eval γα eα empty pure (γα × D.singleton x vα) - ) pure ({ g: g', n: n', γα: γα' } × xv) From 570516084e34bb698982063ac2953367c74bbc42 Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Fri, 22 Sep 2023 16:44:41 +0100 Subject: [PATCH 09/15] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Factor=20?= =?UTF-8?q?graphGC=20through=20evalWithConfig.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/EvalGraph.purs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index f0c731053..a112349f0 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -174,7 +174,6 @@ eval_module γ = go D.empty γ'' <- closeDefs (γ <+> γ') ρ αs go (γ' <+> γ'') (Module ds) αs --- TODO: Inline into graphGC evalWithConfig :: forall g m a. MonadError String m => Graph g => GraphConfig g -> Expr a -> m ((g × Int) × Expr Vertex × Val Vertex) evalWithConfig { g, n, γα } e = runWithGraphAlloc2T (g × n) $ do @@ -190,13 +189,8 @@ graphGC -> Raw Expr -> m (GaloisConnection (Set Vertex) (Set Vertex)) graphGC { g: g0, n, γα } e = do - (g × _) × vα × eα <- m + (g × _) × vα × eα <- evalWithConfig { g: g0, n, γα } e pure $ { fwd: \αs -> G.vertices (fwdSlice αs g) `intersection` vertices vα , bwd: \αs -> G.vertices (bwdSlice αs g) `intersection` vertices eα -- TODO: include γα } - where - m = runWithGraphAlloc2T (g0 × n) $ do - eα <- alloc e - vα <- eval γα eα S.empty - pure (vα × eα) From d56063329ba69348e0af584b8c8e1c29148939a5 Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Fri, 22 Sep 2023 17:01:26 +0100 Subject: [PATCH 10/15] =?UTF-8?q?=E2=9D=97=20[incomplete]:=20More=20monadi?= =?UTF-8?q?c=20shenanigans.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/App/Fig.purs | 18 +++++++++--------- src/Module.purs | 19 +++++++++---------- 2 files changed, 18 insertions(+), 19 deletions(-) diff --git a/src/App/Fig.purs b/src/App/Fig.purs index 98aa5ca74..6aeb0b46b 100644 --- a/src/App/Fig.purs +++ b/src/App/Fig.purs @@ -9,6 +9,7 @@ import App.MatrixView (MatrixView(..), drawMatrix, matrixViewHandler, matrixRep) import App.TableView (EnergyTable(..), drawTable, energyRecord, tableViewHandler) import App.Util (HTMLId, OnSel, Selector, doNothing, from, record) import Bindings (Var) +import Control.Monad.Error.Class (class MonadError, liftMaybe) import Data.Array (range, zip) import Data.Either (Either(..)) import Data.Foldable (length) @@ -19,7 +20,7 @@ import Data.Tuple (fst, uncurry) import DataType (cBarChart, cCons, cLineChart, cNil) import Desugarable (desug) import Effect (Effect) -import Effect.Aff (Aff) +import Effect.Aff.Class (class MonadAff) import Effect.Console (log) import Eval (eval, eval_module) import EvalBwd (evalBwd) @@ -187,7 +188,7 @@ linkResult x γ0 γ e1 e2 t1 _ v1 = do _ × v2' <- eval (neg ((botOf <$> γ0) <+> γ')) (topOf e2) true pure { v': neg v2', v0' } -loadFig :: FigSpec -> Aff Fig +loadFig :: forall m. MonadAff m => MonadError String m => FigSpec -> m Fig loadFig spec@{ file } = do -- TODO: not every example should run with this dataset. { γα: γα0 } × xv :: GraphConfig GraphImpl × _ <- @@ -203,7 +204,7 @@ loadFig spec@{ file } = do t × v <- eval γ0γ e bot pure { spec, γ0, γ: γ0 <+> γ1, s0, s, e, t, v } -loadLinkFig :: LinkFigSpec -> Aff LinkFig +loadLinkFig :: forall m. MonadAff m => MonadError String m => LinkFigSpec -> m LinkFig loadLinkFig spec@{ file1, file2, dataFile, x } = do let dir = File "linking/" @@ -218,9 +219,8 @@ loadLinkFig spec@{ file1, file2, dataFile, x } = do s1 = botOf s1' s2 = botOf s2' dataFile' <- loadFile (Folder "fluid/example/linking") (dataFile) -- use surface expression instead - pure $ successful do - e1 × e2 <- (×) <$> desug s1 <*> desug s2 - t1 × v1 <- eval (γ0 <+> xv0) e1 bot - t2 × v2 <- eval (γ0 <+> xv0) e2 bot - v0 <- lookup x xv0 # orElse absurd - pure { spec, γ0, γ: xv0, s1, s2, e1, e2, t1, t2, v1, v2, v0, dataFile: dataFile' } + e1 × e2 <- (×) <$> desug s1 <*> desug s2 + t1 × v1 <- eval (γ0 <+> xv0) e1 bot + t2 × v2 <- eval (γ0 <+> xv0) e2 bot + v0 <- lookup x xv0 # liftMaybe absurd + pure { spec, γ0, γ: xv0, s1, s2, e1, e2, t1, t2, v1, v2, v0, dataFile: dataFile' } diff --git a/src/Module.purs b/src/Module.purs index 76721eb36..c3a090072 100644 --- a/src/Module.purs +++ b/src/Module.purs @@ -14,13 +14,12 @@ import Data.Set (empty) import Data.Traversable (traverse) import Desugarable (desug) import Dict (singleton) as D -import Effect.Aff (Aff) import Effect.Aff.Class (class MonadAff, liftAff) import EvalGraph (GraphConfig, eval, eval_module) import Expr (traverseModule) import Graph (class Graph, Vertex) import Graph (empty) as G -import Graph.GraphWriter (class MonadGraphAlloc, alloc, fresh, runWithGraphAllocT) +import Graph.GraphWriter (class MonadGraphAlloc, alloc, fresh, runWithGraphAlloc2T, runWithGraphAllocT) import Lattice (botOf) import Parse (module_, program) import Parsing (runParser) @@ -40,10 +39,10 @@ derive newtype instance Show File derive newtype instance Semigroup File derive newtype instance Monoid File -loadFile :: Folder -> File -> Aff String +loadFile :: forall m. MonadAff m => MonadError String m => Folder -> File -> m String loadFile (Folder folder) (File file) = do let url = "./" <> folder <> "/" <> file <> ".fld" - result <- request (defaultRequest { url = url, method = Left GET, responseFormat = string }) + result <- liftAff $ request (defaultRequest { url = url, method = Left GET, responseFormat = string }) case result of Left err -> error (printError err) Right response -> pure response.body @@ -53,17 +52,17 @@ parse src p = case runParser src p of Left err -> throwError $ show err Right x -> pure x -parseProgram :: Folder -> File -> Aff (S.Expr Unit) +parseProgram :: forall m. MonadAff m => MonadError String m => Folder -> File -> m (S.Expr Unit) parseProgram folder file = do src <- loadFile folder file pure (successful $ flip parse (program <#> botOf) src) -open :: File -> Aff (S.Expr Unit) +open :: forall m. MonadAff m => MonadError String m => File -> m (S.Expr Unit) open = parseProgram (Folder "fluid/example") loadModule :: forall m. MonadAff m => MonadGraphAlloc m => File -> Env Vertex -> m (Env Vertex) loadModule file γ = do - src <- liftAff $ loadFile (Folder "fluid/lib") file + src <- loadFile (Folder "fluid/lib") file mod <- parse src module_ >>= desugarModuleFwd >>= traverseModule (const fresh) eval_module γ mod empty <#> (γ <+> _) @@ -73,13 +72,13 @@ defaultImports = do loadModule (File "prelude") γα >>= loadModule (File "graphics") >>= loadModule (File "convolution") -- | Evaluates default imports from empty initial graph config -openDefaultImports :: forall g. Graph g => Aff (GraphConfig g) +openDefaultImports :: forall m g. MonadAff m => MonadError String m => Graph g => m (GraphConfig g) openDefaultImports = do - (g × n) × γα <- fromRight <$> runWithGraphAllocT (G.empty × 0) defaultImports + (g × n) × γα <- runWithGraphAlloc2T (G.empty × 0) defaultImports pure $ { g, n, γα } -- | Evaluate dataset in context of existing graph config -openDatasetAs :: forall g. Graph g => File -> Var -> GraphConfig g -> Aff (GraphConfig g × Env Vertex) +openDatasetAs :: forall m g. MonadAff m => MonadError String m => Graph g => File -> Var -> GraphConfig g -> m (GraphConfig g × Env Vertex) openDatasetAs file x { g, n, γα } = do s <- parseProgram (Folder "fluid") file (g' × n') × (γα' × xv) <- fromRight <$> From 0b6100fac902451475f3c09cc639485c29215410 Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Sat, 23 Sep 2023 07:22:06 +0100 Subject: [PATCH 11/15] =?UTF-8?q?=E2=9D=97=20[incomplete]:=20Purge=20some?= =?UTF-8?q?=20'successful'.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/App/Main.purs | 15 ++++++++------- src/Module.purs | 17 +++++++---------- src/Util.purs | 6 +++++- 3 files changed, 20 insertions(+), 18 deletions(-) diff --git a/src/App/Main.purs b/src/App/Main.purs index f145a469f..e94e7d7e0 100644 --- a/src/App/Main.purs +++ b/src/App/Main.purs @@ -62,13 +62,14 @@ drawFigs loadFigs = drawFig fig ed botOf drawFiles :: Array (Folder × File) -> Effect Unit -drawFiles files = sequence_ $ files <#> \(folder × file) -> - flip runAff_ (loadFile folder file) - case _ of - Left err -> log $ show err - Right src -> do - ed <- addEditorView $ codeMirrorDiv $ unwrap file - drawCode ed src +drawFiles files = + sequence_ $ files <#> \(folder × file) -> + flip runAff_ ?_ --(loadFile folder file) + case _ of + Left err -> log $ show err + Right src -> do + ed <- addEditorView $ codeMirrorDiv $ unwrap file + drawCode ed src main :: Effect Unit main = do diff --git a/src/Module.purs b/src/Module.purs index c3a090072..2dad0be40 100644 --- a/src/Module.purs +++ b/src/Module.purs @@ -5,7 +5,7 @@ import Prelude import Affjax.ResponseFormat (string) import Affjax.Web (defaultRequest, printError, request) import Bindings (Var) -import Control.Monad.Error.Class (throwError) +import Control.Monad.Error.Class (liftEither, throwError) import Control.Monad.Except (class MonadError) import Data.Either (Either(..)) import Data.HTTP.Method (Method(..)) @@ -26,7 +26,7 @@ import Parsing (runParser) import Primitive.Defs (primitives) import SExpr (Expr) as S import SExpr (desugarModuleFwd) -import Util (type (×), (×), error, successful, fromRight) +import Util (type (×), fromRight, mapLeft, (×)) import Util.Parse (SParser) import Val (Env, (<+>)) @@ -44,18 +44,15 @@ loadFile (Folder folder) (File file) = do let url = "./" <> folder <> "/" <> file <> ".fld" result <- liftAff $ request (defaultRequest { url = url, method = Left GET, responseFormat = string }) case result of - Left err -> error (printError err) + Left err -> throwError $ printError err Right response -> pure response.body parse :: forall a m. MonadError String m => String -> SParser a -> m a -parse src p = case runParser src p of - Left err -> throwError $ show err - Right x -> pure x +parse src = liftEither <<< mapLeft show <<< runParser src parseProgram :: forall m. MonadAff m => MonadError String m => Folder -> File -> m (S.Expr Unit) -parseProgram folder file = do - src <- loadFile folder file - pure (successful $ flip parse (program <#> botOf) src) +parseProgram folder file = + loadFile folder file >>= flip parse (program <#> botOf) open :: forall m. MonadAff m => MonadError String m => File -> m (S.Expr Unit) open = parseProgram (Folder "fluid/example") @@ -75,7 +72,7 @@ defaultImports = do openDefaultImports :: forall m g. MonadAff m => MonadError String m => Graph g => m (GraphConfig g) openDefaultImports = do (g × n) × γα <- runWithGraphAlloc2T (G.empty × 0) defaultImports - pure $ { g, n, γα } + pure { g, n, γα } -- | Evaluate dataset in context of existing graph config openDatasetAs :: forall m g. MonadAff m => MonadError String m => Graph g => File -> Var -> GraphConfig g -> m (GraphConfig g × Env Vertex) diff --git a/src/Util.purs b/src/Util.purs index a7c1ff46d..d13758665 100644 --- a/src/Util.purs +++ b/src/Util.purs @@ -69,10 +69,14 @@ ignoreMessage = runExceptT >>> extract >>> case _ of (Left _) -> Nothing (Right x) -> Just x -fromRight :: forall a. Either String a -> a +fromRight :: forall a. String + a -> a fromRight (Right x) = x fromRight (Left msg) = error msg +mapLeft :: forall a b c. (a -> c) -> Either a b -> Either c b +mapLeft f (Left x) = Left (f x) +mapLeft _ (Right x) = Right x + successful :: forall a. MayFail a -> a successful (ExceptT (Identity (Right x))) = x successful (ExceptT (Identity (Left msg))) = error msg From 7c9c08a340616859f6b78fd1799dbf27ce5a58d1 Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Sun, 24 Sep 2023 08:02:20 +0100 Subject: [PATCH 12/15] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20Standardi?= =?UTF-8?q?se=20on=20Error=20rather=20than=20String=20for=20Aff=20compatib?= =?UTF-8?q?ility=20(can't=20figure=20out=20how=20to=20convert=20from=20one?= =?UTF-8?q?=20two=20other=20when=20in=20an=20abstract=20MonadError=20setti?= =?UTF-8?q?ng).?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/App/Fig.purs | 10 ++++---- src/App/Main.purs | 2 +- src/DataType.purs | 9 ++++---- src/Desugarable.purs | 3 ++- src/Dict.purs | 4 ++-- src/Eval.purs | 29 +++++++++++------------ src/EvalGraph.purs | 19 +++++++-------- src/Expr.purs | 9 ++++---- src/Graph/GraphWriter.purs | 9 +++++--- src/Lattice.purs | 13 ++++++----- src/Module.purs | 25 ++++++++++---------- src/Primitive/Defs.purs | 47 +++++++++++++++++++------------------- src/SExpr.purs | 29 +++++++++++------------ src/Util.purs | 31 ++++++++++++++----------- src/Val.purs | 17 +++++++------- test/Util.purs | 11 +++++---- 16 files changed, 142 insertions(+), 125 deletions(-) diff --git a/src/App/Fig.purs b/src/App/Fig.purs index 6aeb0b46b..ebeccaa78 100644 --- a/src/App/Fig.purs +++ b/src/App/Fig.purs @@ -9,7 +9,7 @@ import App.MatrixView (MatrixView(..), drawMatrix, matrixViewHandler, matrixRep) import App.TableView (EnergyTable(..), drawTable, energyRecord, tableViewHandler) import App.Util (HTMLId, OnSel, Selector, doNothing, from, record) import Bindings (Var) -import Control.Monad.Error.Class (class MonadError, liftMaybe) +import Control.Monad.Error.Class (class MonadError) import Data.Array (range, zip) import Data.Either (Either(..)) import Data.Foldable (length) @@ -19,9 +19,11 @@ import Data.Traversable (sequence, sequence_) import Data.Tuple (fst, uncurry) import DataType (cBarChart, cCons, cLineChart, cNil) import Desugarable (desug) +import Dict (get) import Effect (Effect) import Effect.Aff.Class (class MonadAff) import Effect.Console (log) +import Effect.Exception (Error) import Eval (eval, eval_module) import EvalBwd (evalBwd) import EvalGraph (GraphConfig) @@ -188,7 +190,7 @@ linkResult x γ0 γ e1 e2 t1 _ v1 = do _ × v2' <- eval (neg ((botOf <$> γ0) <+> γ')) (topOf e2) true pure { v': neg v2', v0' } -loadFig :: forall m. MonadAff m => MonadError String m => FigSpec -> m Fig +loadFig :: forall m. MonadAff m => MonadError Error m => FigSpec -> m Fig loadFig spec@{ file } = do -- TODO: not every example should run with this dataset. { γα: γα0 } × xv :: GraphConfig GraphImpl × _ <- @@ -204,7 +206,7 @@ loadFig spec@{ file } = do t × v <- eval γ0γ e bot pure { spec, γ0, γ: γ0 <+> γ1, s0, s, e, t, v } -loadLinkFig :: forall m. MonadAff m => MonadError String m => LinkFigSpec -> m LinkFig +loadLinkFig :: forall m. MonadAff m => MonadError Error m => LinkFigSpec -> m LinkFig loadLinkFig spec@{ file1, file2, dataFile, x } = do let dir = File "linking/" @@ -222,5 +224,5 @@ loadLinkFig spec@{ file1, file2, dataFile, x } = do e1 × e2 <- (×) <$> desug s1 <*> desug s2 t1 × v1 <- eval (γ0 <+> xv0) e1 bot t2 × v2 <- eval (γ0 <+> xv0) e2 bot - v0 <- lookup x xv0 # liftMaybe absurd + let v0 = get x xv0 pure { spec, γ0, γ: xv0, s1, s2, e1, e2, t1, t2, v1, v2, v0, dataFile: dataFile' } diff --git a/src/App/Main.purs b/src/App/Main.purs index e94e7d7e0..3bb3db750 100644 --- a/src/App/Main.purs +++ b/src/App/Main.purs @@ -64,7 +64,7 @@ drawFigs loadFigs = drawFiles :: Array (Folder × File) -> Effect Unit drawFiles files = sequence_ $ files <#> \(folder × file) -> - flip runAff_ ?_ --(loadFile folder file) + flip runAff_ (loadFile folder file) case _ of Left err -> log $ show err Right src -> do diff --git a/src/DataType.purs b/src/DataType.purs index 3541777b3..863b562cc 100644 --- a/src/DataType.purs +++ b/src/DataType.purs @@ -15,6 +15,7 @@ import Data.String.CodeUnits (charAt) import Data.Tuple (uncurry) import Dict (Dict, keys, lookup) import Dict (fromFoldable) as O +import Effect.Exception (Error) import Partial.Unsafe (unsafePartial) import Util (type (×), absurd, definitely', error, orElse, with, (=<<<), (×), (≞)) @@ -57,7 +58,7 @@ ctrToDataType = dataTypes <#> (\d -> ctrs d # S.toUnfoldable <#> (_ × d)) # concat # O.fromFoldable class DataTypeFor a where - dataTypeFor :: forall m. MonadThrow String m => a -> m DataType + dataTypeFor :: forall m. MonadThrow Error m => a -> m DataType instance DataTypeFor Ctr where dataTypeFor c = lookup c ctrToDataType # orElse ("Unknown constructor " <> showCtr c) @@ -66,7 +67,7 @@ instance DataTypeFor (Set Ctr) where dataTypeFor cs = unsafePartial $ case S.toUnfoldable cs of c : _ -> dataTypeFor c -- Sets must be non-empty, but this is a more convenient signature. -consistentWith :: forall m. MonadError String m => Set Ctr -> Set Ctr -> m Unit +consistentWith :: forall m. MonadError Error m => Set Ctr -> Set Ctr -> m Unit consistentWith cs cs' = void $ do d <- dataTypeFor cs' d' <- dataTypeFor cs' @@ -75,12 +76,12 @@ consistentWith cs cs' = void $ do ctrs :: DataType -> Set Ctr ctrs (DataType _ sigs) = keys sigs # S.fromFoldable -arity :: forall m. MonadThrow String m => Ctr -> m Int +arity :: forall m. MonadThrow Error m => Ctr -> m Int arity c = do DataType _ sigs <- dataTypeFor c lookup c sigs # orElse absurd -checkArity :: forall m. MonadError String m => Ctr -> Int -> m Unit +checkArity :: forall m. MonadError Error m => Ctr -> Int -> m Unit checkArity c n = void $ with ("Checking arity of " <> showCtr c) (arity c `(=<<<) (≞)` pure n) diff --git a/src/Desugarable.purs b/src/Desugarable.purs index f83f84767..0985db412 100644 --- a/src/Desugarable.purs +++ b/src/Desugarable.purs @@ -3,8 +3,9 @@ module Desugarable where import Prelude import Control.Monad.Error.Class (class MonadError) +import Effect.Exception (Error) import Lattice (Raw, class JoinSemilattice, class BoundedJoinSemilattice) class (Functor s, Functor e) <= Desugarable s e | s -> e where - desug :: forall a m. MonadError String m => JoinSemilattice a => s a -> m (e a) + desug :: forall a m. MonadError Error m => JoinSemilattice a => s a -> m (e a) desugBwd :: forall a. BoundedJoinSemilattice a => e a -> Raw s -> s a diff --git a/src/Dict.purs b/src/Dict.purs index 0385596ef..91c3fd70c 100644 --- a/src/Dict.purs +++ b/src/Dict.purs @@ -42,10 +42,10 @@ apply :: forall a b. Dict (a -> b) -> Dict a -> Dict b apply d ds = intersectionWith ($) d ds apply2 :: forall f a b. Apply f => Dict (f (a -> b)) -> Dict (f a) -> Dict (f b) -apply2 d ds = apply (map (<*>) d) ds +apply2 d ds = apply ((<*>) <$> d) ds lift2 :: forall f a b c. Apply f => (a -> b -> c) -> Dict (f a) -> Dict (f b) -> Dict (f c) -lift2 f d1 d2 = apply2 (map (map f) d1) d2 +lift2 f d1 d2 = apply2 ((f <$> _) <$> d1) d2 -- Unfortunately Foreign.Object doesn't define this; could implement using Foreign.Object.ST instead. foreign import intersectionWith :: forall a b c. (a -> b -> c) -> Dict a -> Dict b -> Dict c diff --git a/src/Eval.purs b/src/Eval.purs index 7877cd4cd..73a08089c 100644 --- a/src/Eval.purs +++ b/src/Eval.purs @@ -3,7 +3,7 @@ module Eval where import Prelude hiding (absurd, apply, top) import Bindings (varAnon) -import Control.Monad.Error.Class (class MonadError, throwError) +import Control.Monad.Error.Class (class MonadError) import Data.Array (fromFoldable) as A import Data.Bifunctor (bimap) import Data.Either (Either(..)) @@ -18,13 +18,14 @@ import Data.Tuple (fst, snd) import DataType (Ctr, arity, consistentWith, dataTypeFor, showCtr) import Dict (disjointUnion, get, empty, lookup, keys) import Dict (fromFoldable, singleton, unzip) as D +import Effect.Exception (Error) import Expr (Cont(..), Elim(..), Expr(..), Module(..), RecDefs, VarDef(..), asExpr, fv) import Lattice ((∧), erase, top) import Pretty (prettyP) import Primitive (intPair, string) import Trace (AppTrace(..), Trace(..), VarDef(..)) as T import Trace (AppTrace, ForeignTrace, ForeignTrace'(..), Match(..), Trace) -import Util (type (×), absurd, both, check, error, successful, orElse, with, (×)) +import Util (type (×), absurd, both, check, error, orElse, successful, throw, with, (×)) import Util.Pair (unzip) as P import Val (Fun(..), Val(..)) as V import Val (class Ann, DictRep(..), Env, ForeignOp'(..), MatrixRep(..), (<+>), Val, for, lookup', restrict) @@ -32,7 +33,7 @@ import Val (class Ann, DictRep(..), Env, ForeignOp'(..), MatrixRep(..), (<+>), V patternMismatch :: String -> String -> String patternMismatch s s' = "Pattern mismatch: found " <> s <> ", expected " <> s' -match :: forall a m. MonadError String m => Ann a => Val a -> Elim a -> m (Env a × Cont a × a × Match) +match :: forall a m. MonadError Error m => Ann a => Val a -> Elim a -> m (Env a × Cont a × a × Match) match v (ElimVar x κ) | x == varAnon = pure (empty × κ × top × MatchVarAnon (erase v)) | otherwise = pure (D.singleton x v × κ × top × MatchVar x (erase v)) @@ -43,21 +44,21 @@ match (V.Constr α c vs) (ElimConstr m) = do pure (γ × κ' × (α ∧ α') × MatchConstr c ws) match v (ElimConstr m) = do d <- dataTypeFor $ keys m - throwError $ patternMismatch (prettyP v) (show d) + throw $ patternMismatch (prettyP v) (show d) match (V.Record α xvs) (ElimRecord xs κ) = do check (subset xs (S.fromFoldable $ keys xvs)) $ patternMismatch (show (keys xvs)) (show xs) let xs' = xs # S.toUnfoldable γ × κ' × α' × ws <- matchMany (xs' <#> flip get xvs) κ pure (γ × κ' × (α ∧ α') × MatchRecord (D.fromFoldable (zip xs' ws))) -match v (ElimRecord xs _) = throwError $ patternMismatch (prettyP v) (show xs) +match v (ElimRecord xs _) = throw $ patternMismatch (prettyP v) (show xs) -matchMany :: forall a m. MonadError String m => Ann a => List (Val a) -> Cont a -> m (Env a × Cont a × a × List Match) +matchMany :: forall a m. MonadError Error m => Ann a => List (Val a) -> Cont a -> m (Env a × Cont a × a × List Match) matchMany Nil κ = pure (empty × κ × top × Nil) matchMany (v : vs) (ContElim σ) = do γ × κ' × α × w <- match v σ γ' × κ'' × β × ws <- matchMany vs κ' pure $ γ `disjointUnion` γ' × κ'' × (α ∧ β) × (w : ws) -matchMany (_ : vs) (ContExpr _) = throwError $ +matchMany (_ : vs) (ContExpr _) = throw $ show (length vs + 1) <> " extra argument(s) to constructor/record; did you forget parentheses in lambda pattern?" matchMany _ _ = error absurd @@ -65,12 +66,12 @@ closeDefs :: forall a. Env a -> RecDefs a -> a -> Env a closeDefs γ ρ α = ρ <#> \σ -> let ρ' = ρ `for` σ in V.Fun α $ V.Closure (γ `restrict` (fv ρ' `union` fv σ)) ρ' σ -checkArity :: forall m. MonadError String m => Ctr -> Int -> m Unit +checkArity :: forall m. MonadError Error m => Ctr -> Int -> m Unit checkArity c n = do n' <- arity c check (n' >= n) (showCtr c <> " got " <> show n <> " argument(s), expects at most " <> show n') -apply :: forall a m. MonadError String m => Ann a => Val a × Val a -> m (AppTrace × Val a) +apply :: forall a m. MonadError Error m => Ann a => Val a × Val a -> m (AppTrace × Val a) apply (V.Fun β (V.Closure γ1 ρ σ) × v) = do let γ2 = closeDefs γ1 ρ β γ3 × e'' × β' × w <- match v σ @@ -96,15 +97,15 @@ apply (V.Fun α (V.PartialConstr c vs) × v) = do v' = if length vs < n - 1 then V.Fun α $ V.PartialConstr c (vs <> singleton v) else V.Constr α c (vs <> singleton v) -apply (_ × v) = throwError $ "Found " <> prettyP v <> ", expected function" +apply (_ × v) = throw $ "Found " <> prettyP v <> ", expected function" -apply2 :: forall a m. MonadError String m => Ann a => Val a × Val a × Val a -> m ((AppTrace × AppTrace) × Val a) +apply2 :: forall a m. MonadError Error m => Ann a => Val a × Val a × Val a -> m ((AppTrace × AppTrace) × Val a) apply2 (u1 × v1 × v2) = do t1 × u2 <- apply (u1 × v1) t2 × v <- apply (u2 × v2) pure $ (t1 × t2) × v -eval :: forall a m. MonadError String m => Ann a => Env a -> Expr a -> a -> m (Trace × Val a) +eval :: forall a m. MonadError Error m => Ann a => Env a -> Expr a -> a -> m (Trace × Val a) eval γ (Var x) _ = (T.Var x × _) <$> lookup' x γ eval γ (Op op) _ = (T.Op op × _) <$> lookup' op γ eval _ (Int α n) α' = pure (T.Const × V.Int (α ∧ α') n) @@ -145,7 +146,7 @@ eval γ (Project e x) α = do t × v <- eval γ e α case v of V.Record _ xvs -> (T.Project t x × _) <$> lookup' x xvs - _ -> throwError $ "Found " <> prettyP v <> ", expected record" + _ -> throw $ "Found " <> prettyP v <> ", expected record" eval γ (App e e') α = do t × v <- eval γ e α t' × v' <- eval γ e' α @@ -161,7 +162,7 @@ eval γ (LetRec ρ e) α = do t × v <- eval (γ <+> γ') e α pure $ T.LetRec (erase <$> ρ) t × v -eval_module :: forall a m. MonadError String m => Ann a => Env a -> Module a -> a -> m (Env a) +eval_module :: forall a m. MonadError Error m => Ann a => Env a -> Module a -> a -> m (Env a) eval_module γ = go empty where go :: Env a -> Module a -> a -> m (Env a) diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index a112349f0..325b5352d 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -12,7 +12,7 @@ module EvalGraph import Prelude hiding (apply, add) import Bindings (varAnon) -import Control.Monad.Error.Class (class MonadError, throwError) +import Control.Monad.Error.Class (class MonadError) import Data.Array (range, singleton) as A import Data.Either (Either(..)) import Data.Exists (runExists) @@ -23,6 +23,7 @@ import Data.Traversable (sequence, traverse) import Data.Tuple (fst) import DataType (checkArity, arity, consistentWith, dataTypeFor, showCtr) import Dict (disjointUnion, fromFoldable, empty, get, keys, lookup, singleton) as D +import Effect.Exception (Error) import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, asExpr) import GaloisConnection (GaloisConnection) import Graph (class Graph, Vertex) @@ -32,7 +33,7 @@ import Graph.Slice (bwdSlice, fwdSlice, vertices) import Lattice (Raw) import Pretty (prettyP) import Primitive (string, intPair) -import Util (type (×), (×), check, error, successful, with, orElse) +import Util (type (×), check, error, orElse, successful, throw, with, (×)) import Util.Pair (unzip) as P import Val (DictRep(..), Env, ForeignOp'(..), MatrixRep(..), Val, for, lookup', restrict, (<+>)) import Val (Val(..), Fun(..)) as V @@ -58,14 +59,14 @@ match (V.Constr α c vs) (ElimConstr m) = do pure (γ × κ' × (insert α αs)) match v (ElimConstr m) = do d <- dataTypeFor $ D.keys m - throwError $ patternMismatch (prettyP v) (show d) + throw $ patternMismatch (prettyP v) (show d) match (V.Record α xvs) (ElimRecord xs κ) = do check (S.subset xs (S.fromFoldable $ D.keys xvs)) $ patternMismatch (show (D.keys xvs)) (show xs) let xs' = xs # S.toUnfoldable γ × κ' × αs <- matchMany (flip D.get xvs <$> xs') κ pure $ γ × κ' × (insert α αs) -match v (ElimRecord xs _) = throwError (patternMismatch (prettyP v) (show xs)) +match v (ElimRecord xs _) = throw (patternMismatch (prettyP v) (show xs)) matchMany :: forall m. MonadGraphAlloc m => List (Val Vertex) -> Cont Vertex -> m (Env Vertex × Cont Vertex × Set Vertex) matchMany Nil κ = pure (D.empty × κ × empty) @@ -73,7 +74,7 @@ matchMany (v : vs) (ContElim σ) = do γ × κ × αs <- match v σ γ' × κ' × βs <- matchMany vs κ pure $ γ `D.disjointUnion` γ' × κ' × (αs `union` βs) -matchMany (_ : vs) (ContExpr _) = throwError $ +matchMany (_ : vs) (ContExpr _) = throw $ show (length vs + 1) <> " extra argument(s) to constructor/record; did you forget parentheses in lambda pattern?" matchMany _ _ = error "absurd" @@ -107,7 +108,7 @@ apply (V.Fun α (V.PartialConstr c vs)) v = do else pure $ V.Constr α c (snoc vs v) where n = successful (arity c) -apply _ v = throwError $ "Found " <> prettyP v <> ", expected function" +apply _ v = throw $ "Found " <> prettyP v <> ", expected function" eval :: forall m. MonadGraphAlloc m => Env Vertex -> Expr Vertex -> Set Vertex -> m (Val Vertex) eval γ (Var x) _ = lookup' x γ @@ -148,7 +149,7 @@ eval γ (Project e x) αs = do v <- eval γ e αs case v of V.Record _ xvs -> lookup' x xvs - _ -> throwError $ "Found " <> prettyP v <> ", expected record" + _ -> throw $ "Found " <> prettyP v <> ", expected record" eval γ (App e e') αs = do v <- eval γ e αs v' <- eval γ e' αs @@ -174,7 +175,7 @@ eval_module γ = go D.empty γ'' <- closeDefs (γ <+> γ') ρ αs go (γ' <+> γ'') (Module ds) αs -evalWithConfig :: forall g m a. MonadError String m => Graph g => GraphConfig g -> Expr a -> m ((g × Int) × Expr Vertex × Val Vertex) +evalWithConfig :: forall g m a. MonadError Error m => Graph g => GraphConfig g -> Expr a -> m ((g × Int) × Expr Vertex × Val Vertex) evalWithConfig { g, n, γα } e = runWithGraphAlloc2T (g × n) $ do eα <- alloc e @@ -183,7 +184,7 @@ evalWithConfig { g, n, γα } e = graphGC :: forall g m - . MonadError String m + . MonadError Error m => Graph g => GraphConfig g -> Raw Expr diff --git a/src/Expr.purs b/src/Expr.purs index eab3ccdf2..0f66cffee 100644 --- a/src/Expr.purs +++ b/src/Expr.purs @@ -4,7 +4,6 @@ import Prelude hiding (absurd, top) import Bindings (Var) import Control.Apply (lift2) -import Control.Monad.Error.Class (throwError) import Data.Either (Either(..)) import Data.Foldable (class Foldable) import Data.List (List(..), (:), zipWith) @@ -16,7 +15,7 @@ import DataType (Ctr, consistentWith) import Dict (Dict, keys, asSingletonMap) import Dict (apply2) as D import Lattice (class BoundedJoinSemilattice, class Expandable, class JoinSemilattice, Raw, (∨), definedJoin, expand, maybeJoin) -import Util (type (+), type (×), both, error, (×), (≜), (≞)) +import Util (type (+), type (×), both, error, throw, (×), (≜), (≞)) import Util.Pair (Pair, toTuple) data Expr a @@ -181,7 +180,7 @@ instance JoinSemilattice a => JoinSemilattice (Elim a) where maybeJoin (ElimConstr cκs) (ElimConstr cκs') = ElimConstr <$> ((keys cκs `consistentWith` keys cκs') *> maybeJoin cκs cκs') maybeJoin (ElimRecord xs κ) (ElimRecord ys κ') = ElimRecord <$> (xs ≞ ys) <*> maybeJoin κ κ' - maybeJoin _ _ = throwError "Incompatible eliminators" + maybeJoin _ _ = throw "Incompatible eliminators" join σ = definedJoin σ @@ -195,7 +194,7 @@ instance JoinSemilattice a => JoinSemilattice (Cont a) where maybeJoin ContNone ContNone = pure ContNone maybeJoin (ContExpr e) (ContExpr e') = ContExpr <$> maybeJoin e e' maybeJoin (ContElim σ) (ContElim σ') = ContElim <$> maybeJoin σ σ' - maybeJoin _ _ = throwError "Incompatible continuations" + maybeJoin _ _ = throw "Incompatible continuations" join κ = definedJoin κ @@ -228,7 +227,7 @@ instance JoinSemilattice a => JoinSemilattice (Expr a) where maybeJoin (App e1 e2) (App e1' e2') = App <$> maybeJoin e1 e1' <*> maybeJoin e2 e2' maybeJoin (Let def e) (Let def' e') = Let <$> maybeJoin def def' <*> maybeJoin e e' maybeJoin (LetRec ρ e) (LetRec ρ' e') = LetRec <$> maybeJoin ρ ρ' <*> maybeJoin e e' - maybeJoin _ _ = throwError "Incompatible expressions" + maybeJoin _ _ = throw "Incompatible expressions" join e = definedJoin e diff --git a/src/Graph/GraphWriter.purs b/src/Graph/GraphWriter.purs index 4c3832880..6925cae35 100644 --- a/src/Graph/GraphWriter.purs +++ b/src/Graph/GraphWriter.purs @@ -32,6 +32,7 @@ import Data.Profunctor.Strong (first) import Data.Set (Set) import Data.Traversable (class Traversable, traverse) import Data.Tuple (swap) +import Effect.Exception (Error) import Graph (Vertex(..), class Graph, fromFoldable) import Util (MayFailT, type (×), type (+), (×)) @@ -42,7 +43,9 @@ class Monad m <= MonadGraph m where class Monad m <= MonadAlloc m where fresh :: m Vertex -class (MonadAlloc m, MonadError String m, MonadGraph m) <= MonadGraphAlloc m where +-- Fix exceptions at Error, the type of JavaScript exceptions, because Aff requires Error, and +-- I can't see a way to convert MonadError Error m (for example) to MonadError Error m. +class (MonadAlloc m, MonadError Error m, MonadGraph m) <= MonadGraphAlloc m where -- Extend with a freshly allocated vertex. new :: Set Vertex -> m Vertex @@ -64,7 +67,7 @@ instance Monad m => MonadAlloc (WithAllocT m) where instance Monad m => MonadAlloc (WithGraphAllocT m) where fresh = lift fresh -instance MonadError String m => MonadGraphAlloc (WithGraphAlloc2T m) where +instance MonadError Error m => MonadGraphAlloc (WithGraphAlloc2T m) where new αs = do α <- fresh extend α αs @@ -109,7 +112,7 @@ runWithGraphAlloc2T (g × n) m = do (n' × a) × g_adds <- runStateT (runWithAllocT n m) Nil pure $ ((g <> fromFoldable g_adds) × n') × a -runWithGraphAllocT :: forall g m a. Monad m => Graph g => g × Int -> WithGraphAllocT m a -> m (String + ((g × Int) × a)) +runWithGraphAllocT :: forall g m a. Monad m => Graph g => g × Int -> WithGraphAllocT m a -> m (Error + ((g × Int) × a)) runWithGraphAllocT (g × n) m = do (g' × n') × maybe_a <- runWithGraphAlloc2T (g × n) (runExceptT m) pure $ maybe_a <#> ((g' × n') × _) diff --git a/src/Lattice.purs b/src/Lattice.purs index 43f24c33f..a069d8e75 100644 --- a/src/Lattice.purs +++ b/src/Lattice.purs @@ -4,7 +4,7 @@ import Prelude hiding (absurd, join, top) import Bindings (Var) import Control.Apply (lift2) -import Control.Monad.Error.Class (class MonadError, throwError) +import Control.Monad.Error.Class (class MonadError) import Data.Array (zipWith) as A import Data.Foldable (length, foldM) import Data.List (List, zipWith) @@ -13,14 +13,15 @@ import Data.Profunctor.Strong ((***)) import Data.Set (subset) import Data.Traversable (sequence) import Dict (Dict, difference, intersectionWith, lookup, insert, keys, toUnfoldable, union, unionWith, update) -import Util (Endo, type (×), (×), assert, successfulWith) +import Effect.Exception (Error) +import Util (type (×), Endo, assert, successfulWith, throw, (×)) import Util.Pair (Pair(..)) -- join here is actually more general "weak join" operation of the formalism, which operates on maps using unionWith. class JoinSemilattice a where join :: a -> a -> a -- soft failure for joining incompatible eliminators, used to desugar function clauses - maybeJoin :: forall m. MonadError String m => a -> a -> m a + maybeJoin :: forall m. MonadError Error m => a -> a -> m a class MeetSemilattice a where meet :: a -> a -> a @@ -121,7 +122,7 @@ instance JoinSemilattice a => JoinSemilattice (List a) where join xs = definedJoin xs maybeJoin xs ys | (length xs :: Int) == length ys = sequence (zipWith maybeJoin xs ys) - | otherwise = throwError "Mismatched list lengths" + | otherwise = throw "Mismatched list lengths" instance JoinSemilattice a => JoinSemilattice (Dict a) where join = unionWith (∨) -- faster than definedJoin @@ -130,7 +131,7 @@ instance JoinSemilattice a => JoinSemilattice (Dict a) where instance Neg a => Neg (Dict a) where neg = (<$>) neg -mayFailUpdate :: forall a m. MonadError String m => JoinSemilattice a => Dict a -> Var × a -> m (Dict a) +mayFailUpdate :: forall a m. MonadError Error m => JoinSemilattice a => Dict a -> Var × a -> m (Dict a) mayFailUpdate m (k × v) = case lookup k m of Nothing -> pure (insert k v m) @@ -140,7 +141,7 @@ instance JoinSemilattice a => JoinSemilattice (Array a) where join xs = definedJoin xs maybeJoin xs ys | length xs == (length ys :: Int) = sequence (A.zipWith maybeJoin xs ys) - | otherwise = throwError "Mismatched array lengths" + | otherwise = throw "Mismatched array lengths" instance (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a diff --git a/src/Module.purs b/src/Module.purs index 2dad0be40..9eb993da5 100644 --- a/src/Module.purs +++ b/src/Module.purs @@ -15,6 +15,7 @@ import Data.Traversable (traverse) import Desugarable (desug) import Dict (singleton) as D import Effect.Aff.Class (class MonadAff, liftAff) +import Effect.Exception (Error, error) import EvalGraph (GraphConfig, eval, eval_module) import Expr (traverseModule) import Graph (class Graph, Vertex) @@ -39,22 +40,22 @@ derive newtype instance Show File derive newtype instance Semigroup File derive newtype instance Monoid File -loadFile :: forall m. MonadAff m => MonadError String m => Folder -> File -> m String +loadFile :: forall m. MonadAff m => MonadError Error m => Folder -> File -> m String loadFile (Folder folder) (File file) = do let url = "./" <> folder <> "/" <> file <> ".fld" result <- liftAff $ request (defaultRequest { url = url, method = Left GET, responseFormat = string }) case result of - Left err -> throwError $ printError err + Left err -> throwError $ error $ printError err Right response -> pure response.body -parse :: forall a m. MonadError String m => String -> SParser a -> m a -parse src = liftEither <<< mapLeft show <<< runParser src +parse :: forall a m. MonadError Error m => String -> SParser a -> m a +parse src = liftEither <<< mapLeft (error <<< show) <<< runParser src -parseProgram :: forall m. MonadAff m => MonadError String m => Folder -> File -> m (S.Expr Unit) +parseProgram :: forall m. MonadAff m => MonadError Error m => Folder -> File -> m (S.Expr Unit) parseProgram folder file = loadFile folder file >>= flip parse (program <#> botOf) -open :: forall m. MonadAff m => MonadError String m => File -> m (S.Expr Unit) +open :: forall m. MonadAff m => MonadError Error m => File -> m (S.Expr Unit) open = parseProgram (Folder "fluid/example") loadModule :: forall m. MonadAff m => MonadGraphAlloc m => File -> Env Vertex -> m (Env Vertex) @@ -69,19 +70,19 @@ defaultImports = do loadModule (File "prelude") γα >>= loadModule (File "graphics") >>= loadModule (File "convolution") -- | Evaluates default imports from empty initial graph config -openDefaultImports :: forall m g. MonadAff m => MonadError String m => Graph g => m (GraphConfig g) +openDefaultImports :: forall m g. MonadAff m => MonadError Error m => Graph g => m (GraphConfig g) openDefaultImports = do (g × n) × γα <- runWithGraphAlloc2T (G.empty × 0) defaultImports pure { g, n, γα } -- | Evaluate dataset in context of existing graph config -openDatasetAs :: forall m g. MonadAff m => MonadError String m => Graph g => File -> Var -> GraphConfig g -> m (GraphConfig g × Env Vertex) +openDatasetAs :: forall m g. MonadAff m => MonadError Error m => Graph g => File -> Var -> GraphConfig g -> m (GraphConfig g × Env Vertex) openDatasetAs file x { g, n, γα } = do s <- parseProgram (Folder "fluid") file (g' × n') × (γα' × xv) <- fromRight <$> runWithGraphAllocT (g × n) do - e <- desug s - eα <- alloc e - vα <- eval γα eα empty - pure (γα × D.singleton x vα) + e <- desug s + eα <- alloc e + vα <- eval γα eα empty + pure (γα × D.singleton x vα) pure ({ g: g', n: n', γα: γα' } × xv) diff --git a/src/Primitive/Defs.purs b/src/Primitive/Defs.purs index c3cb1cab4..a24e82463 100644 --- a/src/Primitive/Defs.purs +++ b/src/Primitive/Defs.purs @@ -2,7 +2,6 @@ module Primitive.Defs where import Prelude hiding (absurd, apply, div, mod, top) -import Control.Monad.Error.Class (throwError) import Data.Exists (mkExists) import Data.Foldable (foldl, foldM) import Data.FoldableWithIndex (foldWithIndexM) @@ -27,7 +26,7 @@ import Partial.Unsafe (unsafePartial) import Prelude (div, mod) as P import Primitive (binary, binaryZero, boolean, int, intOrNumber, intOrNumberOrString, number, string, unary, union, union1, unionStr) import Trace (AppTrace) -import Util (type (+), type (×), Endo, error, orElse, unimplemented, (×)) +import Util (type (+), type (×), Endo, error, orElse, throw, unimplemented, (×)) import Val (Array2, DictRep(..), Env, ForeignOp, ForeignOp'(..), Fun(..), MatrixRep(..), OpBwd, OpFwd, OpGraph, Val(..), matrixGet, matrixUpdate) extern :: forall a. BoundedJoinSemilattice a => ForeignOp -> Val a @@ -74,11 +73,11 @@ error_ = mkExists $ ForeignOp' { arity: 1, op': op', op: fwd, op_bwd: unsafePart where op' :: OpGraph op' (Str _ s : Nil) = pure $ error s - op' _ = throwError "String expected" + op' _ = throw "String expected" fwd :: OpFwd Unit fwd (Str _ s : Nil) = error s - fwd _ = throwError "String expected" + fwd _ = throw "String expected" bwd :: OpBwd Unit bwd _ = error unimplemented @@ -88,11 +87,11 @@ debugLog = mkExists $ ForeignOp' { arity: 1, op': op', op: fwd, op_bwd: unsafePa where op' :: OpGraph op' (x : Nil) = pure $ trace x (const x) - op' _ = throwError "Single value expected" + op' _ = throw "Single value expected" fwd :: OpFwd Unit fwd (x : Nil) = pure $ unit × trace x (const x) - fwd _ = throwError "Single value expected" + fwd _ = throw "Single value expected" bwd :: OpBwd Unit bwd _ = error unimplemented @@ -107,12 +106,12 @@ dims = mkExists $ ForeignOp' { arity: 1, op': op, op: fwd, op_bwd: unsafePartial v1 <- Int <$> new (singleton β1) <@> i v2 <- Int <$> new (singleton β2) <@> j Constr <$> new (singleton α) <@> cPair <@> (v1 : v2 : Nil) - op _ = throwError "Matrix expected" + op _ = throw "Matrix expected" fwd :: OpFwd (Raw ArrayData) fwd (Matrix α (MatrixRep (vss × (i × β1) × (j × β2))) : Nil) = pure $ (map erase <$> vss) × Constr α cPair (Int β1 i : Int β2 j : Nil) - fwd _ = throwError "Matrix expected" + fwd _ = throw "Matrix expected" bwd :: Partial => OpBwd (Raw ArrayData) bwd (vss × Constr α c (Int β1 i : Int β2 j : Nil)) | c == cPair = @@ -124,14 +123,14 @@ matrixLookup = mkExists $ ForeignOp' { arity: 2, op': op, op: fwd, op_bwd: bwd } op :: OpGraph op (Matrix _ r : Constr _ c (Int _ i : Int _ j : Nil) : Nil) | c == cPair = matrixGet i j r - op _ = throwError "Matrix and pair of integers expected" + op _ = throw "Matrix and pair of integers expected" fwd :: OpFwd (Raw ArrayData × (Int × Int) × (Int × Int)) fwd (Matrix _ r@(MatrixRep (vss × (i' × _) × (j' × _))) : Constr _ c (Int _ i : Int _ j : Nil) : Nil) | c == cPair = do v <- matrixGet i j r pure $ ((map erase <$> vss) × (i' × j') × (i × j)) × v - fwd _ = throwError "Matrix and pair of integers expected" + fwd _ = throw "Matrix and pair of integers expected" bwd :: OpBwd (Raw ArrayData × (Int × Int) × (Int × Int)) bwd ((vss × (i' × j') × (i × j)) × v) = @@ -145,12 +144,12 @@ dict_difference = mkExists $ ForeignOp' { arity: 2, op': op, op: fwd, op_bwd: un op :: OpGraph op (Dictionary α (DictRep d) : Dictionary β (DictRep d') : Nil) = Dictionary <$> new (singleton α # insert β) <@> DictRep (d \\ d') - op _ = throwError "Dictionaries expected." + op _ = throw "Dictionaries expected." fwd :: OpFwd Unit fwd (Dictionary α (DictRep d) : Dictionary α' (DictRep d') : Nil) = pure $ unit × Dictionary (α ∧ α') (DictRep (d \\ d')) - fwd _ = throwError "Dictionaries expected." + fwd _ = throw "Dictionaries expected." bwd :: Partial => OpBwd Unit bwd (_ × Dictionary α d) = @@ -163,12 +162,12 @@ dict_fromRecord = mkExists $ ForeignOp' { arity: 1, op': op, op: fwd, op_bwd: un op (Record α xvs : Nil) = do xvs' <- for xvs (\v -> new (singleton α) <#> (_ × v)) Dictionary <$> new (singleton α) <@> DictRep xvs' - op _ = throwError "Record expected." + op _ = throw "Record expected." fwd :: OpFwd Unit fwd (Record α xvs : Nil) = pure $ unit × Dictionary α (DictRep $ xvs <#> (α × _)) - fwd _ = throwError "Record expected." + fwd _ = throw "Record expected." bwd :: Partial => OpBwd Unit bwd (_ × Dictionary α (DictRep d)) = @@ -180,12 +179,12 @@ dict_disjointUnion = mkExists $ ForeignOp' { arity: 2, op': op, op: fwd, op_bwd: op :: OpGraph op (Dictionary α (DictRep d) : Dictionary β (DictRep d') : Nil) = do Dictionary <$> new (singleton α # insert β) <@> DictRep (D.disjointUnion d d') - op _ = throwError "Dictionaries expected" + op _ = throw "Dictionaries expected" fwd :: OpFwd (Dict Unit × Dict Unit) fwd (Dictionary α (DictRep d) : Dictionary α' (DictRep d') : Nil) = pure $ ((const unit <$> d) × (const unit <$> d')) × Dictionary (α ∧ α') (DictRep $ D.disjointUnion d d') - fwd _ = throwError "Dictionaries expected" + fwd _ = throw "Dictionaries expected" bwd :: Partial => OpBwd (Dict Unit × Dict Unit) bwd ((d × d') × Dictionary α (DictRep d'')) = @@ -197,7 +196,7 @@ dict_foldl = mkExists $ ForeignOp' { arity: 3, op': op, op: fwd, op_bwd: unsafeP op :: OpGraph op (v : u : Dictionary _ (DictRep d) : Nil) = foldM (\u1 (_ × u2) -> G.apply v u1 >>= flip G.apply u2) u d - op _ = throwError "Function, value and dictionary expected" + op _ = throw "Function, value and dictionary expected" fwd :: OpFwd (Raw Val × List (String × AppTrace × AppTrace)) fwd (v : u : Dictionary _ (DictRep d) : Nil) = do @@ -208,7 +207,7 @@ dict_foldl = mkExists $ ForeignOp' { arity: 3, op': op, op: fwd, op_bwd: unsafeP d -- :: MayFail (List (String × AppTrace × AppTrace) × Val _) pure $ (erase v × ts) × u' - fwd _ = throwError "Function, value and dictionary expected" + fwd _ = throw "Function, value and dictionary expected" bwd :: Partial => OpBwd (Raw Val × List (String × AppTrace × AppTrace)) bwd ((v × ts) × u) = v' : u' : Dictionary bot (DictRep d) : Nil @@ -226,12 +225,12 @@ dict_get = mkExists $ ForeignOp' { arity: 2, op': op, op: fwd, op_bwd: unsafePar op :: OpGraph op (Str _ s : Dictionary _ (DictRep d) : Nil) = snd <$> D.lookup s d # orElse ("Key \"" <> s <> "\" not found") - op _ = throwError "String and dictionary expected" + op _ = throw "String and dictionary expected" fwd :: OpFwd String fwd (Str _ s : Dictionary _ (DictRep d) : Nil) = (s × _) <$> (snd <$> D.lookup s d # orElse ("Key \"" <> s <> "\" not found")) - fwd _ = throwError "String and dictionary expected" + fwd _ = throw "String and dictionary expected" bwd :: Partial => OpBwd String bwd (s × v) = @@ -248,7 +247,7 @@ dict_intersectionWith = mkExists $ ForeignOp' { arity: 3, op': op, op: fwd, op_b apply' (β × u) (β' × u') = do β'' <- new (singleton β # insert β') (×) β'' <$> (G.apply v u >>= flip G.apply u') - op _ = throwError "Function and two dictionaries expected" + op _ = throw "Function and two dictionaries expected" fwd :: OpFwd (Raw Val × Dict (AppTrace × AppTrace)) fwd (v : Dictionary α (DictRep d) : Dictionary α' (DictRep d') : Nil) = do @@ -256,7 +255,7 @@ dict_intersectionWith = mkExists $ ForeignOp' { arity: 3, op': op, op: fwd, op_b sequence $ D.intersectionWith (\(β × u) (β' × u') -> (β ∧ β' × _) <$> apply2 (v × u × u')) d d' pure $ (erase v × (d'' <#> snd >>> fst)) × Dictionary (α ∧ α') (DictRep (d'' <#> second snd)) - fwd _ = throwError "Function and two dictionaries expected" + fwd _ = throw "Function and two dictionaries expected" bwd :: Partial => OpBwd (Raw Val × Dict (AppTrace × AppTrace)) bwd ((v × tts) × Dictionary α (DictRep βvs)) = @@ -277,13 +276,13 @@ dict_map = mkExists $ ForeignOp' { arity: 2, op': op, op: fwd, op_bwd: unsafePar op (v : Dictionary α (DictRep d) : Nil) = do d' <- traverse (\(β × u) -> (β × _) <$> G.apply v u) d Dictionary <$> new (singleton α) <@> DictRep d' - op _ = throwError "Function and dictionary expected" + op _ = throw "Function and dictionary expected" fwd :: OpFwd (Raw Val × Dict AppTrace) fwd (v : Dictionary α (DictRep d) : Nil) = do ts × d' <- D.unzip <$> traverse (\(β × u) -> second (β × _) <$> apply (v × u)) d pure $ (erase v × ts) × Dictionary α (DictRep d') - fwd _ = throwError "Function and dictionary expected" + fwd _ = throw "Function and dictionary expected" bwd :: Partial => OpBwd (Raw Val × Dict AppTrace) bwd ((v × ts) × Dictionary α (DictRep d')) = diff --git a/src/SExpr.purs b/src/SExpr.purs index 1e98d5f7d..47e9bf737 100644 --- a/src/SExpr.purs +++ b/src/SExpr.purs @@ -23,6 +23,7 @@ import DataType (Ctr, arity, checkArity, ctrs, cCons, cFalse, cNil, cTrue, dataT import Desugarable (class Desugarable, desugBwd, desug) import Dict (Dict, asSingletonMap, get) import Dict (fromFoldable, singleton) as D +import Effect.Exception (Error) import Expr (Cont(..), Elim(..), asElim, asExpr) import Expr (Expr(..), Module(..), RecDefs, VarDef(..)) as E import Lattice (class JoinSemilattice, (∨), bot, definedJoin, maybeJoin, class BoundedJoinSemilattice, Raw) @@ -143,7 +144,7 @@ instance Desugarable Clauses Elim where desug = clausesFwd desugBwd = clausesBwd -desugarModuleFwd :: forall a m. MonadError String m => JoinSemilattice a => Module a -> m (E.Module a) +desugarModuleFwd :: forall a m. MonadError Error m => JoinSemilattice a => Module a -> m (E.Module a) desugarModuleFwd = moduleFwd -- helpers @@ -157,7 +158,7 @@ elimBool :: forall a. Cont a -> Cont a -> Elim a elimBool κ κ' = ElimConstr (D.fromFoldable [ cTrue × κ, cFalse × κ' ]) -- Module. Surface language supports "blocks" of variable declarations; core does not. Currently no backward. -moduleFwd :: forall a m. MonadError String m => JoinSemilattice a => Module a -> m (E.Module a) +moduleFwd :: forall a m. MonadError Error m => JoinSemilattice a => Module a -> m (E.Module a) moduleFwd (Module ds) = E.Module <$> traverse varDefOrRecDefsFwd (join (flatten <$> ds)) where varDefOrRecDefsFwd :: VarDef a + RecDefs a -> m (E.VarDef a + E.RecDefs a) @@ -168,11 +169,11 @@ moduleFwd (Module ds) = E.Module <$> traverse varDefOrRecDefsFwd (join (flatten flatten (Left ds') = Left <$> toList ds' flatten (Right δ) = pure (Right δ) -varDefFwd :: forall a m. MonadError String m => JoinSemilattice a => VarDef a -> m (E.VarDef a) +varDefFwd :: forall a m. MonadError Error m => JoinSemilattice a => VarDef a -> m (E.VarDef a) varDefFwd (VarDef π s) = E.VarDef <$> pattContFwd π (ContNone :: Cont a) <*> desug s -- VarDefs -varDefsFwd :: forall a m. MonadError String m => JoinSemilattice a => VarDefs a × Expr a -> m (E.Expr a) +varDefsFwd :: forall a m. MonadError Error m => JoinSemilattice a => VarDefs a × Expr a -> m (E.Expr a) varDefsFwd (NonEmptyList (d :| Nil) × s) = E.Let <$> varDefFwd d <*> desug s varDefsFwd (NonEmptyList (d :| d' : ds) × s) = @@ -190,7 +191,7 @@ varDefsBwd _ (NonEmptyList (_ :| _) × _) = error absurd -- RecDefs -- In the formalism, "group by name" is part of the syntax. -recDefsFwd :: forall a m. MonadError String m => JoinSemilattice a => RecDefs a -> m (E.RecDefs a) +recDefsFwd :: forall a m. MonadError Error m => JoinSemilattice a => RecDefs a -> m (E.RecDefs a) recDefsFwd xcs = D.fromFoldable <$> traverse recDefFwd xcss where xcss = map RecDef (groupBy (eq `on` fst) xcs) :: NonEmptyList (RecDef a) @@ -209,14 +210,14 @@ recDefsBwd ρ xcs = join (go (groupBy (eq `on` fst) xcs)) NonEmptyList (unwrap (recDefBwd (x ↦ get x ρ) (RecDef xcs1)) :| xcss') -- RecDef -recDefFwd :: forall a m. MonadError String m => JoinSemilattice a => RecDef a -> m (Bind (Elim a)) +recDefFwd :: forall a m. MonadError Error m => JoinSemilattice a => RecDef a -> m (Bind (Elim a)) recDefFwd xcs = (fst (head (unwrap xcs)) ↦ _) <$> clausesFwd (Clauses (snd <$> unwrap xcs)) recDefBwd :: forall a. BoundedJoinSemilattice a => Bind (Elim a) -> Raw RecDef -> RecDef a recDefBwd (x ↦ σ) (RecDef bs) = RecDef ((x × _) <$> unwrap (clausesBwd σ (Clauses (snd <$> bs)))) -- Expr -exprFwd :: forall a m. MonadError String m => JoinSemilattice a => Expr a -> m (E.Expr a) +exprFwd :: forall a m. MonadError Error m => JoinSemilattice a => Expr a -> m (E.Expr a) exprFwd (Var x) = pure (E.Var x) exprFwd (Op op) = pure (E.Op op) exprFwd (Int α n) = pure (E.Int α n) @@ -278,7 +279,7 @@ exprBwd (E.LetRec xσs e) (LetRec xcs s) = LetRec (recDefsBwd xσs xcs) (desugBw exprBwd _ _ = error absurd -- ListRest -listRestFwd :: forall a m. MonadError String m => JoinSemilattice a => ListRest a -> m (E.Expr a) +listRestFwd :: forall a m. MonadError Error m => JoinSemilattice a => ListRest a -> m (E.Expr a) listRestFwd (End α) = pure (enil α) listRestFwd (Next α s l) = econs α <$> desug s <*> desug l @@ -289,7 +290,7 @@ listRestBwd (E.Constr α _ (e1 : e2 : Nil)) (Next _ s l) = listRestBwd _ _ = error absurd -- List Qualifier × Expr -listCompFwd :: forall a m. MonadError String m => JoinSemilattice a => a × List (Qualifier a) × Expr a -> m (E.Expr a) +listCompFwd :: forall a m. MonadError Error m => JoinSemilattice a => a × List (Qualifier a) × Expr a -> m (E.Expr a) listCompFwd (α × Nil × s) = econs α <$> desug s <@> enil α listCompFwd (α × (Guard s : qs) × s') = do @@ -326,7 +327,7 @@ listCompBwd (E.App (E.App (E.Var "concatMap") (E.Lambda σ)) e) ((Generator p s0 listCompBwd _ _ = error absurd -- NonEmptyList Pattern × Expr -pattsExprFwd :: forall a m. MonadError String m => JoinSemilattice a => NonEmptyList Pattern × Expr a -> m (Elim a) +pattsExprFwd :: forall a m. MonadError Error m => JoinSemilattice a => NonEmptyList Pattern × Expr a -> m (Elim a) pattsExprFwd (NonEmptyList (p :| Nil) × s) = (ContExpr <$> desug s) >>= pattContFwd p pattsExprFwd (NonEmptyList (p :| p' : ps) × s) = pattContFwd p =<< ContExpr <$> E.Lambda <$> pattsExprFwd (NonEmptyList (p' :| ps) × s) @@ -339,7 +340,7 @@ pattsExprBwd (NonEmptyList (p :| p' : ps) × s) σ = next (asExpr (pattContBwd p next _ = error absurd -- Pattern × Cont -pattContFwd :: forall a m. MonadError String m => Pattern -> Cont a -> m (Elim a) +pattContFwd :: forall a m. MonadError Error m => Pattern -> Cont a -> m (Elim a) pattContFwd (PVar x) κ = pure (ElimVar x κ) pattContFwd (PConstr c ps) κ = checkArity c (length ps) *> (ElimConstr <$> D.singleton c <$> pattArgsFwd (Left <$> ps) κ) @@ -357,7 +358,7 @@ pattContBwd (PRecord xps) (ElimRecord _ κ) = pattArgsBwd ((snd >>> Left) <$> so pattContBwd _ _ = error absurd -- ListRestPattern × Cont -pattCont_ListRest_Fwd :: forall a m. MonadError String m => ListRestPattern -> Cont a -> m (Elim a) +pattCont_ListRest_Fwd :: forall a m. MonadError Error m => ListRestPattern -> Cont a -> m (Elim a) pattCont_ListRest_Fwd PEnd κ = pure (ElimConstr (D.singleton cNil κ)) pattCont_ListRest_Fwd (PNext p o) κ = ElimConstr <$> D.singleton cCons <$> pattArgsFwd (Left p : Right o : Nil) κ @@ -368,7 +369,7 @@ pattCont_ListRest_Bwd (ElimConstr m) PEnd = get cNil m pattCont_ListRest_Bwd (ElimConstr m) (PNext p o) = pattArgsBwd (Left p : Right o : Nil) (get cCons m) -- List (Pattern + ListRestPattern) × Cont -pattArgsFwd :: forall a m. MonadError String m => List (Pattern + ListRestPattern) -> Cont a -> m (Cont a) +pattArgsFwd :: forall a m. MonadError Error m => List (Pattern + ListRestPattern) -> Cont a -> m (Cont a) pattArgsFwd Nil κ = pure κ pattArgsFwd (Left p : πs) κ = ContElim <$> (pattArgsFwd πs κ >>= pattContFwd p) pattArgsFwd (Right o : πs) κ = ContElim <$> (pattArgsFwd πs κ >>= pattCont_ListRest_Fwd o) @@ -379,7 +380,7 @@ pattArgsBwd (Left p : πs) σ = pattArgsBwd πs (pattContBwd p (asElim σ)) pattArgsBwd (Right o : πs) σ = pattArgsBwd πs (pattCont_ListRest_Bwd (asElim σ) o) -- Clauses -clausesFwd :: forall a m. MonadError String m => JoinSemilattice a => Clauses a -> m (Elim a) +clausesFwd :: forall a m. MonadError Error m => JoinSemilattice a => Clauses a -> m (Elim a) clausesFwd (Clauses bs) = do NonEmptyList (σ :| σs) <- traverse pattsExprFwd (unwrap <$> bs) foldM maybeJoin σ σs diff --git a/src/Util.purs b/src/Util.purs index d13758665..98626ea74 100644 --- a/src/Util.purs +++ b/src/Util.purs @@ -18,7 +18,8 @@ import Data.Maybe (Maybe(..)) import Data.NonEmpty ((:|)) import Data.Profunctor.Strong ((&&&), (***)) import Data.Tuple (Tuple(..), fst, snd) -import Effect.Exception (throw) +import Effect.Exception (Error, message) +import Effect.Exception (error) as E import Effect.Unsafe (unsafePerformEffect) infixr 6 type Tuple as × -- standard library has \/ @@ -29,6 +30,9 @@ infixr 6 type Either as + -- standard library has \/ error :: ∀ a. String -> a error msg = unsafePerformEffect (throw msg) +throw :: forall m a. MonadThrow Error m => String -> m a +throw = throwError <<< E.error + assert :: ∀ a. Boolean -> a -> a assert true = identity assert false = \_ -> error "Assertion failure" @@ -57,11 +61,11 @@ onlyIf :: Boolean -> forall m a. MonadPlus m => a -> m a onlyIf true = pure onlyIf false = const empty -type MayFail a = Except String a -type MayFailT m = ExceptT String m +type MayFail a = Except Error a +type MayFailT m = ExceptT Error m -orElse :: forall a m. MonadThrow String m => String -> Maybe a -> m a -orElse s Nothing = throwError s +orElse :: forall a m. MonadThrow Error m => String -> Maybe a -> m a +orElse s Nothing = throwError $ E.error s orElse _ (Just x) = pure x ignoreMessage :: forall a. MayFail a -> Maybe a @@ -69,9 +73,9 @@ ignoreMessage = runExceptT >>> extract >>> case _ of (Left _) -> Nothing (Right x) -> Just x -fromRight :: forall a. String + a -> a +fromRight :: forall a. Error + a -> a fromRight (Right x) = x -fromRight (Left msg) = error msg +fromRight (Left e) = error $ show e mapLeft :: forall a b c. (a -> c) -> Either a b -> Either c b mapLeft f (Left x) = Left (f x) @@ -79,18 +83,19 @@ mapLeft _ (Right x) = Right x successful :: forall a. MayFail a -> a successful (ExceptT (Identity (Right x))) = x -successful (ExceptT (Identity (Left msg))) = error msg +successful (ExceptT (Identity (Left e))) = error $ message e successfulWith :: String -> forall a. MayFail a -> a successfulWith msg = successful <<< with msg -- If the property fails, add an extra error message. -with :: forall a m. MonadError String m => String -> Endo (m a) -with msg m = catchError m (\msg' -> throwError $ msg' <> if msg == "" then "" else ("\n" <> msg)) +with :: forall a m. MonadError Error m => String -> Endo (m a) +with msg m = catchError m \e -> + let msg' = message e in throwError $ E.error $ msg' <> if msg == "" then "" else ("\n" <> msg) -check :: forall m. MonadError String m => Boolean -> String -> m Unit +check :: forall m. MonadError Error m => Boolean -> String -> m Unit check true = const $ pure unit -check false = throwError +check false = throwError <<< E.error mayEq :: forall a. Eq a => a -> a -> Maybe a mayEq x x' = whenever (x == x') x @@ -104,7 +109,7 @@ mustGeq x x' = definitely (show x <> " greater than " <> show x') (whenever (x > unionWithMaybe :: forall a b. Ord a => (b -> b -> Maybe b) -> Map a b -> Map a b -> Map a (Maybe b) unionWithMaybe f m m' = M.unionWith (\x -> lift2 f x >>> join) (Just <$> m) (Just <$> m') -mayFailEq :: forall a m. MonadError String m => Show a => Eq a => a -> a -> m a +mayFailEq :: forall a m. MonadError Error m => Show a => Eq a => a -> a -> m a mayFailEq x x' = x ≟ x' # orElse (show x <> " ≠ " <> show x') infixl 4 mayEq as ≟ diff --git a/src/Val.purs b/src/Val.purs index 3271c37e5..58ef59c05 100644 --- a/src/Val.purs +++ b/src/Val.purs @@ -4,7 +4,7 @@ import Prelude hiding (absurd, append) import Bindings (Var) import Control.Apply (lift2) -import Control.Monad.Error.Class (class MonadError, class MonadThrow, throwError) +import Control.Monad.Error.Class (class MonadError, class MonadThrow) import Data.Array ((!!)) import Data.Array (zipWith) as A import Data.Bitraversable (bitraverse) @@ -16,13 +16,14 @@ import Data.Traversable (class Traversable, sequenceDefault, traverse) import DataType (Ctr) import Dict (Dict, get) import Dict (apply2, intersectionWith) as D +import Effect.Exception (Error) import Expr (Elim, RecDefs, fv) import Foreign.Object (filterKeys, lookup, unionWith) import Foreign.Object (keys) as O import Graph (Vertex(..)) import Graph.GraphWriter (class MonadGraphAlloc) import Lattice (class BoundedJoinSemilattice, class BoundedLattice, class Expandable, class JoinSemilattice, class Neg, Raw, definedJoin, expand, maybeJoin, neg, (∨)) -import Util (type (×), Endo, error, orElse, unsafeUpdateAt, (!), (×), (≜), (≞)) +import Util (type (×), Endo, error, orElse, throw, unsafeUpdateAt, (!), (×), (≜), (≞)) import Util.Pretty (Doc, beside, text) data Val a @@ -51,9 +52,9 @@ instance Highlightable a => Highlightable (a × b) where instance (Ann a, BoundedLattice b) => Ann (a × b) -- similar to an isomorphism lens with complement t -type OpFwd t = forall a m. Ann a => MonadError String m => List (Val a) -> m (t × Val a) +type OpFwd t = forall a m. Ann a => MonadError Error m => List (Val a) -> m (t × Val a) type OpBwd t = forall a. Ann a => t × Val a -> List (Val a) -type OpGraph = forall m. MonadGraphAlloc m => MonadError String m => List (Val Vertex) -> m (Val Vertex) +type OpGraph = forall m. MonadGraphAlloc m => MonadError Error m => List (Val Vertex) -> m (Val Vertex) data ForeignOp' t = ForeignOp' { arity :: Int @@ -67,7 +68,7 @@ type ForeignOp = Exists ForeignOp' -- Environments. type Env a = Dict (Val a) -lookup' :: forall a m. MonadThrow String m => Var -> Dict a -> m a +lookup' :: forall a m. MonadThrow Error m => Var -> Dict a -> m a lookup' x γ = lookup x γ # orElse ("variable " <> x <> " not found") -- Want a monoid instance but needs a newtype @@ -105,7 +106,7 @@ newtype MatrixRep a = MatrixRep (Array2 (Val a) × (Int × a) × (Int × a)) type Array2 a = Array (Array a) -matrixGet :: forall a m. MonadThrow String m => Int -> Int -> MatrixRep a -> m (Val a) +matrixGet :: forall a m. MonadThrow Error m => Int -> Int -> MatrixRep a -> m (Val a) matrixGet i j (MatrixRep (vss × _ × _)) = orElse "Index out of bounds" $ do us <- vss !! (i - 1) @@ -209,7 +210,7 @@ instance JoinSemilattice a => JoinSemilattice (Val a) where maybeJoin (Constr α c vs) (Constr α' c' us) = Constr (α ∨ α') <$> (c ≞ c') <*> maybeJoin vs us maybeJoin (Matrix α m) (Matrix α' m') = Matrix (α ∨ α') <$> maybeJoin m m' maybeJoin (Fun α φ) (Fun α' φ') = Fun (α ∨ α') <$> maybeJoin φ φ' - maybeJoin _ _ = throwError "Incompatible values" + maybeJoin _ _ = throw "Incompatible values" join v = definedJoin v @@ -220,7 +221,7 @@ instance JoinSemilattice a => JoinSemilattice (Fun a) where Foreign φ <$> maybeJoin vs vs' -- TODO: require φ == φ' maybeJoin (PartialConstr c vs) (PartialConstr c' us) = PartialConstr <$> (c ≞ c') <*> maybeJoin vs us - maybeJoin _ _ = throwError "Incompatible functions" + maybeJoin _ _ = throw "Incompatible functions" join v = definedJoin v diff --git a/test/Util.purs b/test/Util.purs index 24b1ac365..364822aaa 100644 --- a/test/Util.purs +++ b/test/Util.purs @@ -1,10 +1,11 @@ module Test.Util where import Prelude hiding (absurd) + import App.Fig (LinkFigSpec) import App.Util (Selector) import Benchmark.Util (BenchRow(..), GraphRow, TraceRow, preciseTime, tdiff) -import Control.Monad.Error.Class (class MonadThrow) +import Control.Monad.Error.Class (class MonadThrow, throwError) import Control.Monad.Except (runExceptT) import Control.Monad.Trans.Class (lift) import Data.Either (Either(..)) @@ -34,7 +35,7 @@ import Parse (program) import Pretty (class Pretty, prettyP) import SExpr (Expr) as SE import Test.Spec.Assertions (fail) -import Util (MayFailT, (×), error, successful) +import Util (MayFailT, (×), successful) import Val (Val(..), class Ann) type TestConfig = @@ -47,13 +48,13 @@ type TestConfig = -- testWithSetup :: Boolean -> SE.Expr Unit -> GraphConfig (GraphImpl S.Set) -> TestConfig -> Aff BenchRow testWithSetup ∷ String -> SE.Expr Unit → GraphConfig GraphImpl → TestConfig → Aff BenchRow testWithSetup _name s gconfig tconfig = do - e <- runExceptT $ do + runExceptT $ do testParse s trRow <- testTrace s gconfig tconfig grRow <- testGraph s gconfig tconfig pure (BenchRow trRow grRow) - case e of - Left msg -> error msg + >>= case _ of + Left e -> throwError e Right x -> pure x testParse :: forall a. Ann a => SE.Expr a -> MayFailT Aff Unit From e8647e93da386560fa4703acb8e182bb293bde56 Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Sun, 24 Sep 2023 09:53:05 +0100 Subject: [PATCH 13/15] =?UTF-8?q?=F0=9F=A7=A9=20[consolidate]:=20liftEithe?= =?UTF-8?q?r.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- test/Util.purs | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/test/Util.purs b/test/Util.purs index 364822aaa..e60601de5 100644 --- a/test/Util.purs +++ b/test/Util.purs @@ -5,10 +5,9 @@ import Prelude hiding (absurd) import App.Fig (LinkFigSpec) import App.Util (Selector) import Benchmark.Util (BenchRow(..), GraphRow, TraceRow, preciseTime, tdiff) -import Control.Monad.Error.Class (class MonadThrow, throwError) +import Control.Monad.Error.Class (class MonadThrow, liftEither) import Control.Monad.Except (runExceptT) import Control.Monad.Trans.Class (lift) -import Data.Either (Either(..)) import Data.Foldable (foldl) import Data.Int (toNumber) import Data.List (elem) @@ -47,15 +46,12 @@ type TestConfig = -- fwd_expect: prettyprinted value after bwd then fwd round-trip -- testWithSetup :: Boolean -> SE.Expr Unit -> GraphConfig (GraphImpl S.Set) -> TestConfig -> Aff BenchRow testWithSetup ∷ String -> SE.Expr Unit → GraphConfig GraphImpl → TestConfig → Aff BenchRow -testWithSetup _name s gconfig tconfig = do - runExceptT $ do +testWithSetup _name s gconfig tconfig = + liftEither =<< (runExceptT $ do testParse s trRow <- testTrace s gconfig tconfig grRow <- testGraph s gconfig tconfig - pure (BenchRow trRow grRow) - >>= case _ of - Left e -> throwError e - Right x -> pure x + pure $ BenchRow trRow grRow) testParse :: forall a. Ann a => SE.Expr a -> MayFailT Aff Unit testParse s = do @@ -65,7 +61,7 @@ testParse s = do unless (eq (erase s) (erase s')) do log ("SRC\n" <> show (erase s)) log ("NEW\n" <> show (erase s')) - (lift $ fail "not equal") :: MayFailT Aff Unit + lift $ fail "not equal" testTrace :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff TraceRow testTrace s { γα: γ } { δv, bwd_expect, fwd_expect } = do @@ -178,14 +174,14 @@ isGraphical _ = false checkPretty :: forall a m. MonadThrow Error m => Pretty a => String -> String -> a -> m Unit checkPretty msg expect x = - unless (expect `eq` prettyP x) - $ fail (msg <> "\nExpected:\n" <> expect <> "\nReceived:\n" <> prettyP x) + unless (expect `eq` prettyP x) $ + fail (msg <> "\nExpected:\n" <> expect <> "\nReceived:\n" <> prettyP x) -- Like version in Test.Spec.Assertions but with error message. shouldSatisfy :: forall m t. MonadThrow Error m => Show t => String -> t -> (t -> Boolean) -> m Unit shouldSatisfy msg v pred = - unless (pred v) - $ fail (show v <> " doesn't satisfy predicate: " <> msg) + unless (pred v) $ + fail (show v <> " doesn't satisfy predicate: " <> msg) averageRows :: List BenchRow -> BenchRow averageRows rows = averagedTr From f792ebfccf400dbcf2130237da91b9185a7b0190 Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Mon, 25 Sep 2023 10:32:52 +0100 Subject: [PATCH 14/15] =?UTF-8?q?=F0=9F=A7=A9=20[remove-unused]:=20Old=20r?= =?UTF-8?q?unWithGraphAllocT.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/EvalBwd.purs | 7 ++++--- src/EvalGraph.purs | 4 ++-- src/GaloisConnection.purs | 3 ++- src/Graph/GraphWriter.purs | 22 +++++++--------------- src/Module.purs | 8 ++++---- test/Util.purs | 12 +++++++----- 6 files changed, 26 insertions(+), 30 deletions(-) diff --git a/src/EvalBwd.purs b/src/EvalBwd.purs index bcdf60688..1330ea262 100644 --- a/src/EvalBwd.purs +++ b/src/EvalBwd.purs @@ -3,7 +3,7 @@ module EvalBwd where import Prelude hiding (absurd) import Bindings (Var, varAnon) -import Control.Monad.Except (runExcept) +import Control.Monad.Except (class MonadError, runExcept) import Data.Exists (mkExists, runExists) import Data.Foldable (foldr) import Data.FoldableWithIndex (foldrWithIndex) @@ -18,6 +18,7 @@ import Data.Tuple (fst, snd, uncurry) import DataType (cPair) import Dict (disjointUnion, disjointUnion_inv, empty, get, insert, intersectionWith, isEmpty, keys) import Dict (fromFoldable, singleton, toUnfoldable) as D +import Effect.Exception (Error) import Eval (eval) import Expr (Cont(..), Elim(..), Expr(..), RecDefs, VarDef(..), bv) import GaloisConnection (GaloisConnection) @@ -200,8 +201,8 @@ evalBwd' v (T.LetRec ρ t) = γ1' × ρ' × α' = closeDefsBwd γ2 evalBwd' _ _ = error absurd -traceGC :: forall a. Ann a => Raw Env -> Raw Expr -> Trace -> GaloisConnection (EvalBwdResult a) (Val a) -traceGC γ e t = +traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> Trace -> m (GaloisConnection (EvalBwdResult a) (Val a)) +traceGC γ e t = pure $ { fwd: \{ γ: γ', e: e', α } -> snd $ fromRight $ runExcept $ eval γ' e' α , bwd: \v -> evalBwd γ e v t } diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs index 325b5352d..97ff05103 100644 --- a/src/EvalGraph.purs +++ b/src/EvalGraph.purs @@ -28,7 +28,7 @@ import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, import GaloisConnection (GaloisConnection) import Graph (class Graph, Vertex) import Graph (vertices) as G -import Graph.GraphWriter (class MonadGraphAlloc, alloc, new, runWithGraphAlloc2T) +import Graph.GraphWriter (class MonadGraphAlloc, alloc, new, runWithGraphAllocT) import Graph.Slice (bwdSlice, fwdSlice, vertices) import Lattice (Raw) import Pretty (prettyP) @@ -177,7 +177,7 @@ eval_module γ = go D.empty evalWithConfig :: forall g m a. MonadError Error m => Graph g => GraphConfig g -> Expr a -> m ((g × Int) × Expr Vertex × Val Vertex) evalWithConfig { g, n, γα } e = - runWithGraphAlloc2T (g × n) $ do + runWithGraphAllocT (g × n) $ do eα <- alloc e vα <- eval γα eα S.empty pure (eα × vα) diff --git a/src/GaloisConnection.purs b/src/GaloisConnection.purs index df981f5a7..41a4514a0 100644 --- a/src/GaloisConnection.purs +++ b/src/GaloisConnection.purs @@ -5,7 +5,8 @@ import Prelude import Lattice (class BooleanLattice, neg) import Util (Endo) --- a and b are posets, but we don't enforce that here. +-- a and b are posets, but we don't enforce that here. Maybe would make more sense as a type class, but +-- would have to add an explicit value-level representation of the "index" (e.g. graph or trace). type GaloisConnection a b = { fwd :: a -> b , bwd :: b -> a diff --git a/src/Graph/GraphWriter.purs b/src/Graph/GraphWriter.purs index 6925cae35..71ab8a26e 100644 --- a/src/Graph/GraphWriter.purs +++ b/src/Graph/GraphWriter.purs @@ -17,13 +17,12 @@ module Graph.GraphWriter , runWithGraph , runWithGraphT , runWithGraphAllocT - , runWithGraphAlloc2T ) where import Prelude -import Control.Monad.Except (class MonadError, runExceptT) -import Control.Monad.State (StateT, runState, runStateT, modify, modify_) +import Control.Monad.Except (class MonadError) +import Control.Monad.State (StateT, runStateT, modify, modify_) import Control.Monad.Trans.Class (lift) import Data.Identity (Identity) import Data.List (List(..), (:)) @@ -34,7 +33,7 @@ import Data.Traversable (class Traversable, traverse) import Data.Tuple (swap) import Effect.Exception (Error) import Graph (Vertex(..), class Graph, fromFoldable) -import Util (MayFailT, type (×), type (+), (×)) +import Util (MayFailT, type (×), (×)) class Monad m <= MonadGraph m where -- Extend graph with existing vertex pointing to set of existing vertices. @@ -94,12 +93,10 @@ alloc = traverse (const fresh) -- TODO: make synonymous with runStateT/runState? runWithAllocT :: forall m a. Monad m => Int -> WithAllocT m a -> m (Int × a) -runWithAllocT n c = do - a × n' <- runStateT c n - pure $ n' × a +runWithAllocT n c = runStateT c n <#> swap runWithAlloc :: forall a. Int -> WithAlloc a -> Int × a -runWithAlloc n c = runState c n # swap +runWithAlloc n = runWithAllocT n >>> unwrap runWithGraphT :: forall g m a. Monad m => Graph g => WithGraphT m a -> m (g × a) runWithGraphT c = runStateT c Nil <#> swap <#> first fromFoldable @@ -107,12 +104,7 @@ runWithGraphT c = runStateT c Nil <#> swap <#> first fromFoldable runWithGraph :: forall g a. Graph g => WithGraph a -> g × a runWithGraph = runWithGraphT >>> unwrap -runWithGraphAlloc2T :: forall g m a. Monad m => Graph g => g × Int -> WithGraphAlloc2T m a -> m ((g × Int) × a) -runWithGraphAlloc2T (g × n) m = do +runWithGraphAllocT :: forall g m a. Monad m => Graph g => g × Int -> WithGraphAlloc2T m a -> m ((g × Int) × a) +runWithGraphAllocT (g × n) m = do (n' × a) × g_adds <- runStateT (runWithAllocT n m) Nil pure $ ((g <> fromFoldable g_adds) × n') × a - -runWithGraphAllocT :: forall g m a. Monad m => Graph g => g × Int -> WithGraphAllocT m a -> m (Error + ((g × Int) × a)) -runWithGraphAllocT (g × n) m = do - (g' × n') × maybe_a <- runWithGraphAlloc2T (g × n) (runExceptT m) - pure $ maybe_a <#> ((g' × n') × _) diff --git a/src/Module.purs b/src/Module.purs index 9eb993da5..54c2e615f 100644 --- a/src/Module.purs +++ b/src/Module.purs @@ -20,14 +20,14 @@ import EvalGraph (GraphConfig, eval, eval_module) import Expr (traverseModule) import Graph (class Graph, Vertex) import Graph (empty) as G -import Graph.GraphWriter (class MonadGraphAlloc, alloc, fresh, runWithGraphAlloc2T, runWithGraphAllocT) +import Graph.GraphWriter (class MonadGraphAlloc, alloc, fresh, runWithGraphAllocT) import Lattice (botOf) import Parse (module_, program) import Parsing (runParser) import Primitive.Defs (primitives) import SExpr (Expr) as S import SExpr (desugarModuleFwd) -import Util (type (×), fromRight, mapLeft, (×)) +import Util (type (×), mapLeft, (×)) import Util.Parse (SParser) import Val (Env, (<+>)) @@ -72,14 +72,14 @@ defaultImports = do -- | Evaluates default imports from empty initial graph config openDefaultImports :: forall m g. MonadAff m => MonadError Error m => Graph g => m (GraphConfig g) openDefaultImports = do - (g × n) × γα <- runWithGraphAlloc2T (G.empty × 0) defaultImports + (g × n) × γα <- runWithGraphAllocT (G.empty × 0) defaultImports pure { g, n, γα } -- | Evaluate dataset in context of existing graph config openDatasetAs :: forall m g. MonadAff m => MonadError Error m => Graph g => File -> Var -> GraphConfig g -> m (GraphConfig g × Env Vertex) openDatasetAs file x { g, n, γα } = do s <- parseProgram (Folder "fluid") file - (g' × n') × (γα' × xv) <- fromRight <$> + (g' × n') × (γα' × xv) <- runWithGraphAllocT (g × n) do e <- desug s eα <- alloc e diff --git a/test/Util.purs b/test/Util.purs index e60601de5..f4dfd74a2 100644 --- a/test/Util.purs +++ b/test/Util.purs @@ -47,11 +47,13 @@ type TestConfig = -- testWithSetup :: Boolean -> SE.Expr Unit -> GraphConfig (GraphImpl S.Set) -> TestConfig -> Aff BenchRow testWithSetup ∷ String -> SE.Expr Unit → GraphConfig GraphImpl → TestConfig → Aff BenchRow testWithSetup _name s gconfig tconfig = - liftEither =<< (runExceptT $ do - testParse s - trRow <- testTrace s gconfig tconfig - grRow <- testGraph s gconfig tconfig - pure $ BenchRow trRow grRow) + liftEither =<< + ( runExceptT $ do + testParse s + trRow <- testTrace s gconfig tconfig + grRow <- testGraph s gconfig tconfig + pure $ BenchRow trRow grRow + ) testParse :: forall a. Ann a => SE.Expr a -> MayFailT Aff Unit testParse s = do From a54f0819a475d8b6163a1e0e364d56c9f0847deb Mon Sep 17 00:00:00 2001 From: Roly Perera Date: Mon, 25 Sep 2023 10:36:14 +0100 Subject: [PATCH 15/15] =?UTF-8?q?=F0=9F=A7=A9=20[remove-unused]:=20Old=20W?= =?UTF-8?q?ithGraphAllocT.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Graph/GraphWriter.purs | 25 +++++-------------------- 1 file changed, 5 insertions(+), 20 deletions(-) diff --git a/src/Graph/GraphWriter.purs b/src/Graph/GraphWriter.purs index 71ab8a26e..ed351750b 100644 --- a/src/Graph/GraphWriter.purs +++ b/src/Graph/GraphWriter.purs @@ -2,7 +2,6 @@ module Graph.GraphWriter ( AdjMapEntries , WithAllocT , WithGraphAllocT - , WithGraphAlloc2T , WithGraph , WithGraphT , class MonadAlloc @@ -33,7 +32,7 @@ import Data.Traversable (class Traversable, traverse) import Data.Tuple (swap) import Effect.Exception (Error) import Graph (Vertex(..), class Graph, fromFoldable) -import Util (MayFailT, type (×), (×)) +import Util (type (×), (×)) class Monad m <= MonadGraph m where -- Extend graph with existing vertex pointing to set of existing vertices. @@ -52,9 +51,7 @@ class (MonadAlloc m, MonadError Error m, MonadGraph m) <= MonadGraphAlloc m wher type AdjMapEntries = List (Vertex × Set Vertex) type WithAllocT m = StateT Int m type WithAlloc = WithAllocT Identity -type WithGraphAllocT m = MayFailT (WithAllocT (WithGraphT m)) --- May make sense to push MayFailT out of WithGraphAllocT. For now: -type WithGraphAlloc2T m = WithAllocT (WithGraphT m) +type WithGraphAllocT m = WithAllocT (WithGraphT m) type WithGraphT = StateT AdjMapEntries type WithGraph = WithGraphT Identity @@ -63,16 +60,7 @@ instance Monad m => MonadAlloc (WithAllocT m) where n <- modify $ (+) 1 pure (Vertex $ show n) -instance Monad m => MonadAlloc (WithGraphAllocT m) where - fresh = lift fresh - -instance MonadError Error m => MonadGraphAlloc (WithGraphAlloc2T m) where - new αs = do - α <- fresh - extend α αs - pure α - -instance Monad m => MonadGraphAlloc (WithGraphAllocT m) where +instance MonadError Error m => MonadGraphAlloc (WithGraphAllocT m) where new αs = do α <- fresh extend α αs @@ -82,11 +70,8 @@ instance Monad m => MonadGraph (WithGraphT m) where extend α αs = void $ modify_ $ (:) (α × αs) -instance Monad m => MonadGraph (WithGraphAlloc2T m) where - extend α = lift <<< extend α - instance Monad m => MonadGraph (WithGraphAllocT m) where - extend α = lift <<< lift <<< extend α + extend α = lift <<< extend α alloc :: forall m t a. MonadAlloc m => Traversable t => t a -> m (t Vertex) alloc = traverse (const fresh) @@ -104,7 +89,7 @@ runWithGraphT c = runStateT c Nil <#> swap <#> first fromFoldable runWithGraph :: forall g a. Graph g => WithGraph a -> g × a runWithGraph = runWithGraphT >>> unwrap -runWithGraphAllocT :: forall g m a. Monad m => Graph g => g × Int -> WithGraphAlloc2T m a -> m ((g × Int) × a) +runWithGraphAllocT :: forall g m a. Monad m => Graph g => g × Int -> WithGraphAllocT m a -> m ((g × Int) × a) runWithGraphAllocT (g × n) m = do (n' × a) × g_adds <- runStateT (runWithAllocT n m) Nil pure $ ((g <> fromFoldable g_adds) × n') × a