Skip to content

Commit

Permalink
Merge pull request #761 from explorable-viz/gc
Browse files Browse the repository at this point in the history
Monad transformer/error handling/graph building consolidation (WIP)
  • Loading branch information
rolyp authored Sep 25, 2023
2 parents 64cf7b1 + efddb7f commit a1de82e
Show file tree
Hide file tree
Showing 18 changed files with 251 additions and 231 deletions.
20 changes: 11 additions & 9 deletions src/App/Fig.purs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
import Data.Array (range, zip)
import Data.Either (Either(..))
import Data.Foldable (length)
Expand All @@ -18,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 (Aff)
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)
Expand Down Expand Up @@ -187,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 :: FigSpec -> Aff 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 × _ <-
Expand All @@ -203,7 +206,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 Error m => LinkFigSpec -> m LinkFig
loadLinkFig spec@{ file1, file2, dataFile, x } = do
let
dir = File "linking/"
Expand All @@ -218,9 +221,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
let v0 = get x xv0
pure { spec, γ0, γ: xv0, s1, s2, e1, e2, t1, t2, v1, v2, v0, dataFile: dataFile' }
15 changes: 8 additions & 7 deletions src/App/Main.purs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
19 changes: 11 additions & 8 deletions src/DataType.purs
Original file line number Diff line number Diff line change
@@ -1,20 +1,23 @@
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 Effect.Exception (Error)
import Partial.Unsafe (unsafePartial)
import Util (type (×), absurd, definitely', error, orElse, with, (=<<<), (×), (≞))

type TypeName = String
type FieldName = String
Expand Down Expand Up @@ -55,7 +58,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 Error m => a -> m DataType

instance DataTypeFor Ctr where
dataTypeFor c = lookup c ctrToDataType # orElse ("Unknown constructor " <> showCtr c)
Expand All @@ -64,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. Monad m => Set Ctr -> Set Ctr -> MayFailT 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'
Expand All @@ -73,12 +76,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 Error 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 Error m => Ctr -> Int -> m Unit
checkArity c n = void $
with ("Checking arity of " <> showCtr c) (arity c `(=<<<) (≞)` pure n)

Expand Down
6 changes: 4 additions & 2 deletions src/Desugarable.purs
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
module Desugarable where

import Prelude

import Control.Monad.Error.Class (class MonadError)
import Effect.Exception (Error)
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 Error m => JoinSemilattice a => s a -> m (e a)
desugBwd :: forall a. BoundedJoinSemilattice a => e a -> Raw s -> s a
4 changes: 2 additions & 2 deletions src/Dict.purs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
32 changes: 17 additions & 15 deletions src/Eval.purs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ module Eval where
import Prelude hiding (absurd, apply, top)

import Bindings (varAnon)
import Control.Monad.Error.Class (class MonadError)
import Data.Array (fromFoldable) as A
import Data.Bifunctor (bimap)
import Data.Either (Either(..))
Expand All @@ -17,21 +18,22 @@ 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 (×), MayFailT, absurd, both, check, error, report, 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)

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 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))
Expand All @@ -42,34 +44,34 @@ 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)
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 _) = report (patternMismatch (prettyP v) (show xs))
match v (ElimRecord xs _) = throw $ 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 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 _) = report $
matchMany (_ : vs) (ContExpr _) = throw $
show (length vs + 1) <> " extra argument(s) to constructor/record; did you forget parentheses in lambda pattern?"
matchMany _ _ = error absurd

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 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. Monad m => Ann a => Val a × Val a -> MayFailT 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 σ
Expand All @@ -81,7 +83,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')
Expand All @@ -95,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) = report $ "Found " <> prettyP v <> ", expected function"
apply (_ × v) = throw $ "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 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. Monad m => Ann a => Env a -> Expr a -> a -> MayFailT 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)
Expand Down Expand Up @@ -144,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
_ -> report $ "Found " <> prettyP v <> ", expected record"
_ -> throw $ "Found " <> prettyP v <> ", expected record"
eval γ (App e e') α = do
t × v <- eval γ e α
t' × v' <- eval γ e' α
Expand All @@ -160,10 +162,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 Error 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 α
Expand Down
7 changes: 4 additions & 3 deletions src/EvalBwd.purs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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
}
Loading

0 comments on commit a1de82e

Please sign in to comment.