Merge branch 'develop' into example-fluid

spago.dhall

@@ -22,7 +22,6 @@ You can edit this file as you like.
   , "http-methods"
   , "identity"
   , "integers"
-  , "js-date"
   , "lists"
   , "maybe"
   , "newtype"

src/App/Fig.purs

@@ -26,19 +26,17 @@ import Effect.Console (log)
 import Effect.Exception (Error)
 import Eval (eval, eval_module)
 import EvalBwd (evalBwd)
-import EvalGraph (GraphConfig)
 import Expr (Expr)
 import Foreign.Object (lookup)
-import Graph.GraphImpl (GraphImpl)
 import Lattice (𝔹, bot, botOf, erase, neg, topOf)
-import Module (File(..), Folder(..), loadFile, open, openDatasetAs, openDefaultImports)
+import Module (File(..), Folder(..), initialConfig, datasetAs, defaultImports, loadFile, open)
 import Partial.Unsafe (unsafePartial)
 import Pretty (prettyP)
 import Primitive (matrixRep) as P
 import SExpr (Expr(..), Module(..), RecDefs, VarDefs) as S
 import SExpr (desugarModuleFwd)
 import Trace (Trace)
-import Util (MayFail, type (×), type (+), (×), absurd, error, orElse, successful)
+import Util (type (×), type (+), (×), absurd, error, orElse)
 import Val (class Ann, Env, Val(..), append_inv, (<+>))
 import Web.Event.EventTarget (eventListener)
 
@@ -74,7 +72,7 @@ type SplitDefs a =
    }
 
 -- Decompose as above.
-splitDefs :: forall a. Ann a => Env a -> S.Expr a -> MayFail (SplitDefs a)
+splitDefs :: forall a m. Ann a => MonadError Error m => Env a -> S.Expr a -> m (SplitDefs a)
 splitDefs γ0 s' = do
    let defs × s = unsafePartial $ unpack s'
    γ <- desugarModuleFwd (S.Module (singleton defs)) >>= flip (eval_module γ0) bot
@@ -111,8 +109,7 @@ type LinkFigSpec =
 
 type LinkFig =
    { spec :: LinkFigSpec
-   , γ0 :: Env 𝔹 -- ambient environment (default imports)
-   , γ :: Env 𝔹 -- local env (loaded dataset)
+   , γ :: Env 𝔹 -- prog context environment (modules + dataset)
    , s1 :: S.Expr 𝔹
    , s2 :: S.Expr 𝔹
    , e1 :: Expr 𝔹
@@ -131,18 +128,17 @@ type LinkResult =
    }
 
 drawLinkFig :: LinkFig -> EditorView -> EditorView -> EditorView -> Selector Val + Selector Val -> Effect Unit
-drawLinkFig fig@{ spec: { x, divId }, γ0, γ, s1, s2, e1, e2, t1, t2, v1, v2, dataFile } ed1 ed2 ed3 δv = do
+drawLinkFig fig@{ spec: { x, divId }, γ, s1, s2, e1, e2, t1, t2, v1, v2, dataFile } ed1 ed2 ed3 δv = do
    log $ "Redrawing " <> divId
-   let
-      v1' × v2' × δv1 × δv2 × v0 = successful case δv of
-         Left δv1 -> do
-            let v1' = δv1 v1
-            { v', v0' } <- linkResult x γ0 γ e1 e2 t1 t2 v1'
-            pure $ v1' × v' × const v1' × identity × v0'
-         Right δv2 -> do
-            let v2' = δv2 v2
-            { v', v0' } <- linkResult x γ0 γ e2 e1 t2 t1 v2'
-            pure $ v' × v2' × identity × const v2' × v0'
+   v1' × v2' × δv1 × δv2 × v0 <- case δv of
+      Left δv1 -> do
+         let v1' = δv1 v1
+         { v', v0' } <- linkResult x γ e1 e2 t1 t2 v1'
+         pure $ v1' × v' × const v1' × identity × v0'
+      Right δv2 -> do
+         let v2' = δv2 v2
+         { v', v0' } <- linkResult x γ e2 e1 t2 t1 v2'
+         pure $ v' × v2' × identity × const v2' × v0'
    drawView divId (\selector -> drawLinkFig fig ed1 ed2 ed3 (Left $ δv1 >>> selector)) 2 $ view "left view" v1'
    drawView divId (\selector -> drawLinkFig fig ed1 ed2 ed3 (Right $ δv2 >>> selector)) 0 $ view "right view" v2'
    drawView divId doNothing 1 $ view "common data" v0
@@ -158,71 +154,65 @@ drawCode ed s = do
 drawFig :: Fig -> EditorView -> Selector Val -> Effect Unit
 drawFig fig@{ spec: { divId }, s0 } ed δv = do
    log $ "Redrawing " <> divId
-   let v_view × views = successful $ figViews fig δv
+   v_view × views <- figViews fig δv
    sequence_ $
       uncurry (drawView divId doNothing) <$> zip (range 0 (length views - 1)) views
    drawView divId (\selector -> drawFig fig ed (δv >>> selector)) (length views) v_view
    drawCode ed $ prettyP s0
 
-varView :: Var -> Env 𝔹 -> MayFail View
+varView :: forall m. MonadError Error m => Var -> Env 𝔹 -> m View
 varView x γ = view x <$> (lookup x γ # orElse absurd)
 
-valViews :: Env 𝔹 -> Array Var -> MayFail (Array View)
+valViews :: forall m. MonadError Error m => Env 𝔹 -> Array Var -> m (Array View)
 valViews γ xs = sequence (flip varView γ <$> xs)
 
 -- For an output selection, views of corresponding input selections and output after round-trip.
-figViews :: Fig -> Selector Val -> MayFail (View × Array View)
+figViews :: forall m. MonadError Error m => Fig -> Selector Val -> m (View × Array View)
 figViews { spec: { xs }, γ0, γ, e, t, v } δv = do
    let
       γ0γ × e' × α = evalBwd (erase <$> (γ0 <+> γ)) (erase e) (δv v) t
    _ × v' <- eval γ0γ e' α
    views <- valViews γ0γ xs
    pure $ view "output" v' × views
 
-linkResult :: Var -> Env 𝔹 -> Env 𝔹 -> Expr 𝔹 -> Expr 𝔹 -> Trace -> Trace -> Val 𝔹 -> MayFail LinkResult
-linkResult x γ0 γ e1 e2 t1 _ v1 = do
+linkResult :: forall m. MonadError Error m => Var -> Env 𝔹 -> Expr 𝔹 -> Expr 𝔹 -> Trace -> Trace -> Val 𝔹 -> m LinkResult
+linkResult x γ0γ e1 e2 t1 _ v1 = do
    let
-      γ0γ × _ = evalBwd (erase <$> (γ0 <+> γ)) (erase e1) v1 t1
-      _ × γ' = append_inv (S.singleton x) γ0γ
+      γ0γ' × _ = evalBwd (erase <$> γ0γ) (erase e1) v1 t1
+      γ0' × γ' = append_inv (S.singleton x) γ0γ'
    v0' <- lookup x γ' # orElse absurd
    -- make γ0 and e2 fully available; γ0 was previously too big to operate on, so we use
    -- (topOf γ0) combined with negation of the dataset environment slice
-   _ × v2' <- eval (neg ((botOf <$> γ0) <+> γ')) (topOf e2) true
+   _ × v2' <- eval (neg ((botOf <$> γ0') <+> γ')) (topOf e2) true
    pure { v': neg v2', v0' }
 
 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 × _ <-
-      openDefaultImports >>= openDatasetAs (File "example/linking/renewables") "data"
-   let
-      γ0 = botOf <$> γα0
-      xv0 = botOf <$> xv
-   open file <#> \s' -> successful $ do
-      let s0 = botOf s'
-      { γ: γ1, s } <- splitDefs (γ0 <+> xv0) s0
-      e <- desug s
-      let γ0γ = γ0 <+> xv0 <+> γ1
-      t × v <- eval γ0γ e bot
-      pure { spec, γ0, γ: γ0 <+> γ1, s0, s, e, t, v }
+   { γ } <- defaultImports >>= initialConfig
+   let γ0 = botOf <$> γ
+   s' <- open file
+   let s0 = botOf s'
+   { γ: γ1, s } <- splitDefs γ0 s0
+   e <- desug s
+   let γ0γ = γ0 <+> γ1
+   t × v <- eval γ0γ e bot
+   pure { spec, γ0, γ: γ0 <+> γ1, s0, s, e, t, v }
 
 loadLinkFig :: forall m. MonadAff m => MonadError Error m => LinkFigSpec -> m LinkFig
 loadLinkFig spec@{ file1, file2, dataFile, x } = do
    let
       dir = File "linking/"
       name1 × name2 = (dir <> file1) × (dir <> file2)
-   -- the views share an ambient environment γ0 as well as dataset
-   { γα } × xv :: GraphConfig GraphImpl × _ <-
-      openDefaultImports >>= openDatasetAs (File "example/" <> dir <> dataFile) x
+   -- views share ambient environment γ
+   { γ } <- defaultImports >>= datasetAs (File "example/" <> dir <> dataFile) x >>= initialConfig
    s1' × s2' <- (×) <$> open name1 <*> open name2
    let
-      γ0 = botOf <$> γα
-      xv0 = botOf <$> xv
+      γ0 = botOf <$> γ
       s1 = botOf s1'
       s2 = botOf s2'
-   dataFile' <- loadFile (Folder "fluid/example/linking") (dataFile) -- use surface expression instead
+   dataFile' <- loadFile (Folder "fluid/example/linking") dataFile -- TODO: use surface expression instead
    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' }
+   t1 × v1 <- eval γ0 e1 bot
+   t2 × v2 <- eval γ0 e2 bot
+   let v0 = get x γ0
+   pure { spec, γ: γ0, s1, s2, e1, e2, t1, t2, v1, v2, v0, dataFile: dataFile' }

src/App/Util/Select.purs

@@ -32,7 +32,7 @@ constrArg :: Ctr -> Int -> Endo (Selector Val)
 constrArg c n δv = unsafePartial $ case _ of
    Constr α c' us | c == c' ->
       let
-         us' = definitely' $ do
+         us' = definitely' do
             u1 <- us !! n
             updateAt n (δv u1) us
       in

src/DataType.purs

@@ -68,7 +68,7 @@ instance DataTypeFor (Set Ctr) where
 
 -- Sets must be non-empty, but this is a more convenient signature.
 consistentWith :: forall m. MonadError Error m => Set Ctr -> Set Ctr -> m Unit
-consistentWith cs cs' = void $ do
+consistentWith cs cs' = void do
    d <- dataTypeFor cs'
    d' <- dataTypeFor cs'
    with ("constructors of " <> show d' <> " do not include " <> (show (S.map showCtr cs))) (d ≞ d')

src/Desug.purs

@@ -7,14 +7,14 @@ import Desugarable (desug, desugBwd)
 import Effect.Exception (Error)
 import Expr (Expr)
 import GaloisConnection (GaloisConnection(..))
-import Lattice (class BoundedJoinSemilattice, Raw)
+import Lattice (class BoundedLattice, Raw)
 import SExpr (Expr) as S
 import Util (successful)
 
 desugGC
    :: forall a m
     . MonadError Error m
-   => BoundedJoinSemilattice a
+   => BoundedLattice a
    => Raw S.Expr
    -> m (GaloisConnection (S.Expr a) (Expr a))
 desugGC s0 = do

src/Desugarable.purs

@@ -4,8 +4,8 @@ import Prelude
 
 import Control.Monad.Error.Class (class MonadError)
 import Effect.Exception (Error)
-import Lattice (Raw, class JoinSemilattice, class BoundedJoinSemilattice)
+import Lattice (class BoundedJoinSemilattice, class BoundedLattice, Raw)
 
 class (Functor s, Functor e) <= Desugarable s e | s -> e where
-   desug :: forall a m. MonadError Error m => JoinSemilattice a => s a -> m (e a)
+   desug :: forall a m. MonadError Error m => BoundedLattice a => s a -> m (e a)
    desugBwd :: forall a. BoundedJoinSemilattice a => e a -> Raw s -> s a

src/Eval.purs

@@ -129,9 +129,9 @@ eval γ (Matrix α e (x × y) e') α' = do
    let (i' × β) × (j' × β') = fst (intPair.match v)
    check (i' × j' >= 1 × 1) ("array must be at least (" <> show (1 × 1) <> "); got (" <> show (i' × j') <> ")")
    tss × vss <- unzipToArray <$> ((<$>) unzipToArray) <$>
-      ( sequence $ do
+      ( sequence do
            i <- range 1 i'
-           singleton $ sequence $ do
+           singleton $ sequence do
               j <- range 1 j'
               let γ' = D.singleton x (V.Int β i) `disjointUnion` (D.singleton y (V.Int β' j))
               singleton (eval (γ <+> γ') e α')
@@ -140,8 +140,8 @@ eval γ (Matrix α e (x × y) e') α' = do
    where
    unzipToArray :: forall b c. List (b × c) -> Array b × Array c
    unzipToArray = unzip >>> bimap A.fromFoldable A.fromFoldable
-eval γ (Lambda σ) α =
-   pure $ T.Const × V.Fun α (V.Closure (γ `restrict` fv σ) empty σ)
+eval γ (Lambda α σ) α' =
+   pure $ T.Const × V.Fun (α ∧ α') (V.Closure (γ `restrict` fv σ) empty σ)
 eval γ (Project e x) α = do
    t × v <- eval γ e α
    case v of
@@ -157,9 +157,9 @@ eval γ (Let (VarDef σ e) e') α = do
    γ' × _ × α' × w <- match v σ -- terminal meta-type of eliminator is meta-unit
    t' × v' <- eval (γ <+> γ') e' α' -- (α ∧ α') for consistency with functions? (similarly for module defs)
    pure $ T.Let (T.VarDef w t) t' × v'
-eval γ (LetRec ρ e) α = do
-   let γ' = closeDefs γ ρ α
-   t × v <- eval (γ <+> γ') e α
+eval γ (LetRec α ρ e) α' = do
+   let γ' = closeDefs γ ρ (α ∧ α')
+   t × v <- eval (γ <+> γ') e (α ∧ α')
    pure $ T.LetRec (erase <$> ρ) t × v
 
 eval_module :: forall a m. MonadError Error m => Ann a => Env a -> Module a -> a -> m (Env a)

src/EvalBwd.purs

@@ -118,7 +118,7 @@ evalBwd' v (T.Op op) = D.singleton op v × Op op × bot
 evalBwd' (V.Str α str) T.Const = empty × Str α str × α
 evalBwd' (V.Int α n) T.Const = empty × Int α n × α
 evalBwd' (V.Float α n) T.Const = empty × Float α n × α
-evalBwd' (V.Fun α (V.Closure γ _ σ)) T.Const = γ × Lambda σ × α
+evalBwd' (V.Fun α (V.Closure γ _ σ)) T.Const = γ × Lambda α σ × α
 evalBwd' (V.Record α xvs) (T.Record xts) =
    foldr (∨) empty (xγeαs <#> fst)
       × Record α (xγeαs <#> (fst <<< snd))
@@ -145,7 +145,7 @@ evalBwd' (V.Constr α _ vs) (T.Constr c ts) =
 evalBwd' (V.Matrix α (MatrixRep (vss × (_ × βi) × (_ × βj)))) (T.Matrix tss (x × y) (i' × j') t') =
    (γ ∨ γ') × Matrix α e (x × y) e' × (α ∨ α' ∨ α'')
    where
-   NonEmptyList ijs = nonEmpty $ do
+   NonEmptyList ijs = nonEmpty do
       i <- range 1 i'
       j <- range 1 j'
       L.singleton (i × j)
@@ -188,7 +188,7 @@ evalBwd' v (T.Let (T.VarDef w t1) t2) =
    v' × σ = matchBwd γ2 ContNone α2 w
    γ1' × e1 × α1 = evalBwd' v' t1
 evalBwd' v (T.LetRec ρ t) =
-   (γ1 ∨ γ1') × LetRec ρ' e × (α ∨ α')
+   (γ1 ∨ γ1') × LetRec (α ∨ α') ρ' e × (α ∨ α')
    where
    γ1γ2 × e × α = evalBwd' v t
    γ1 × γ2 = append_inv (S.fromFoldable $ keys ρ) γ1γ2