Skip to content

Commit

Permalink
various updates on generalising to functors
Browse files Browse the repository at this point in the history
  • Loading branch information
T-ab-F committed Sep 3, 2024
1 parent bb6e177 commit 86b5fa8
Show file tree
Hide file tree
Showing 5 changed files with 26 additions and 73 deletions.
39 changes: 9 additions & 30 deletions src/App/Fig.purs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module App.Fig where
import Prelude hiding (absurd, compare)

import App.CodeMirror (EditorView, addEditorView, dispatch, getContentsLength, update)
import App.Util (ReactState, 𝕊, as𝕊, getInert, getPersistent, getTransient, kindOfBot, reactState, to𝕊, vReact)
import App.Util (ReactState, 𝕊, as𝕊, getInert, getPersistent, getTransient, reactState, to𝕊)
import App.Util.Selector (envVal)
import App.View (view)
import App.View.Util (Direction(..), Fig, FigSpec, HTMLId, View, drawView)
Expand Down Expand Up @@ -39,7 +39,7 @@ str =
selectOutput :: Setter Fig (Val (ReactState 𝔹))
selectOutput δv fig@{ dir, γ, v } = fig
{ v = δv v
, γ = if dir == LinkedInputs then kindOfBot <$> γ else γ
, γ = if dir == LinkedInputs then botOf γ else γ
, dir = LinkedOutputs
}

Expand All @@ -51,7 +51,7 @@ setOutputView δvw fig = fig
selectInput :: Var -> Setter Fig (Val (ReactState 𝔹))
selectInput x δv fig@{ dir, γ, v } = fig
{ γ = envVal x δv γ
, v = if dir == LinkedOutputs then kindOfBot <$> v else v
, v = if dir == LinkedOutputs then botOf v else v
, dir = LinkedInputs
}

Expand All @@ -61,42 +61,23 @@ setInputView x δvw fig = fig
}

-- generalise Env, Val to f,g?
lift :: GaloisConnection (Env 𝔹) (Val 𝔹) -> GaloisConnection (Env (ReactState 𝔹)) (Val (ReactState 𝔹))
lift :: forall f g. Apply f => Apply g => GaloisConnection (f 𝔹) (g 𝔹) -> GaloisConnection (f (ReactState 𝔹)) (g (ReactState 𝔹))
lift (GC gc) = (GC { bwd: bwd1, fwd: fwd1 })
where
fwd1 :: Env (ReactState 𝔹) -> Val (ReactState 𝔹)
fwd1 :: f (ReactState 𝔹) -> g (ReactState 𝔹)
fwd1 γ = reactState <$> v0 <*> v1 <*> v2
where
v0 = gc.fwd (γ <#> getInert)
v1 = gc.fwd (γ <#> getPersistent)
v2 = gc.fwd (γ <#> getTransient)

bwd1 :: Val (ReactState 𝔹) -> Env (ReactState 𝔹)
bwd1 :: g (ReactState 𝔹) -> f (ReactState 𝔹)
bwd1 v = reactState <$> v0 <*> v1 <*> v2
where
v0 = gc.bwd (v <#> getInert)
v1 = gc.bwd (v <#> getPersistent)
v2 = gc.bwd (v <#> getTransient)

liftdual :: GaloisConnection (Val 𝔹) (Env 𝔹) -> GaloisConnection (Val (ReactState 𝔹)) (Env (ReactState 𝔹))
liftdual (GC gc) = (GC { bwd: bwd1, fwd: fwd1 })
where
fwd1 :: Val (ReactState 𝔹) -> Env (ReactState 𝔹)
fwd1 γ = reactState <$> v0 <*> v1 <*> v2
where
v0 = gc.fwd (γ <#> getInert)
v1 = gc.fwd (γ <#> getPersistent)
v2 = gc.fwd (getTransient <$> γ)

bwd1 :: Env (ReactState 𝔹) -> Val (ReactState 𝔹)
bwd1 v = reactState <$> v0 <*> v1 <*> v2
where
v0 = gc.bwd (v <#> getInert) -- or botOf v
v1 = gc.bwd (v <#> getPersistent)
v2 = gc.bwd (v <#> getTransient)

--bwd1 v = gc.bwd <$> (v)

selectionResult :: Fig -> Val (ReactState 𝕊) × Env (ReactState 𝕊)
selectionResult fig@{ v, dir: LinkedOutputs } =
(as𝕊 <$> v <*> v1) × (to𝕊 <$> report γ1)
Expand Down Expand Up @@ -148,12 +129,10 @@ loadFig spec@{ inputs, imports, file, datasets } = do

γ0 = neg (unwrap gc1).bwd (topOf outα)
v0 = neg (unwrap gc1_dual).bwd (topOf γα)
gc_dual = ((lift gc1) `GC.(***)` identity) >>> meet >>> (liftdual gc1_dual)
gc = ((liftdual gc1_dual) `GC.(***)` identity) >>> meet >>> (lift gc1)
{-v: botOf outα
γ: botOf γα-}
gc_dual = ((lift gc1) `GC.(***)` identity) >>> meet >>> (lift gc1_dual)
gc = ((lift gc1_dual) `GC.(***)` identity) >>> meet >>> (lift gc1)

pure { spec, s, γ: vReact <$> γ0 <*> {-Reactive <$> -} botOf γα, v: vReact <$> v0 {-} Reactive <$>-} <*> botOf outα, gc, gc_dual, dir: LinkedOutputs, in_views, out_view: Nothing }
pure { spec, s, γ: reactState <$> γ0 <*> botOf γα <*> botOf γα, v: reactState <$> v0 <*> botOf outα <*> botOf outα, gc, gc_dual, dir: LinkedOutputs, in_views, out_view: Nothing }

codeMirrorDiv :: Endo String
codeMirrorDiv = ("codemirror-" <> _)
Expand Down
44 changes: 8 additions & 36 deletions src/App/Util.purs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@ import Data.String.CodeUnits (drop, take)
import Data.Traversable (sequence, sequence_)
import Data.Tuple (snd)
import DataType (cCons, cNil)
import Debug (spy)
import Dict (Dict)
import Effect (Effect)
import Effect.Aff (Aff, runAff_)
Expand All @@ -29,7 +28,7 @@ import Lattice (class BoundedJoinSemilattice, class JoinSemilattice, 𝔹, bot,
import Primitive (as, intOrNumber, unpack)
import Primitive as P
import Unsafe.Coerce (unsafeCoerce)
import Util (type (×), Endo, Setter, absurd, definitely', error)
import Util (type (×), Endo, Setter, absurd, definitely', error, shapeMismatch)
import Util.Map (get)
import Val (class Highlightable, BaseVal(..), DictRep(..), Val(..), highlightIf)
import Web.Event.Event (Event, EventType(..), target, type_)
Expand Down Expand Up @@ -60,31 +59,6 @@ persist δα = \sel ->
Reactive (SelState s) -> Reactive (SelState { persistent: δα s.persistent, transient: s.transient })
Inert -> Inert

checkREq :: ReactState 𝔹 -> ReactState 𝔹 -> 𝔹
checkREq Inert Inert = true
checkREq (Reactive a) (Reactive b) = eq a b
checkREq _ _ = false

nullify :: ReactState 𝔹 -> ReactState 𝔹
nullify (Inert) = Inert
nullify (Reactive (SelState _)) = Inert

compress :: ReactState 𝔹 -> ReactState 𝔹
compress Inert = (Reactive (SelState { persistent: false, transient: false }))
compress (Reactive a) = (Reactive a)

kindOfBot :: ReactState 𝔹 -> ReactState 𝔹
kindOfBot (Inert) = Inert
kindOfBot (Reactive (SelState _)) = Reactive (SelState { persistent: false, transient: false })

kindOfBotS :: ReactState 𝕊 -> ReactState 𝕊
kindOfBotS (Inert) = Inert
kindOfBotS (Reactive (SelState _)) = Reactive (SelState { persistent: None, transient: None })

--vReact applies the inert set to the reactState (should try to incorporate into ReactState def)
vReact :: 𝔹 -> SelState 𝔹 -> ReactState 𝔹
vReact b a = if b then Inert else (Reactive a)

reactState :: 𝔹 -> 𝔹 -> 𝔹 -> ReactState 𝔹
reactState true _ _ = Inert
reactState false b1 b2 = Reactive (SelState { persistent: b1, transient: b2 })
Expand Down Expand Up @@ -172,7 +146,7 @@ cheatToSel :: ReactState 𝔹 -> SelState 𝔹
cheatToSel Inert = (SelState { persistent: false, transient: false })
cheatToSel (Reactive sel) = sel

-- methods for obtaining the ReactStates
-- methods for obtaining the ReactState, designed to accept varying type inputs for redundancy
as𝕊 :: ReactState 𝔹 -> ReactState 𝔹 -> ReactState 𝕊
as𝕊 Inert _ = Inert
as𝕊 _ Inert = Inert
Expand Down Expand Up @@ -335,7 +309,7 @@ instance Apply ReactState where
apply Inert Inert = Inert
apply (Reactive (SelState fs)) (Reactive (SelState s)) =
Reactive (SelState { persistent: fs.persistent s.persistent, transient: fs.transient s.transient })
apply _ _ = error absurd
apply _ _ = shapeMismatch unit

derive instance Ord a => Ord (SelState a)
derive instance Eq a => Eq (SelState a)
Expand All @@ -348,18 +322,16 @@ instance JoinSemilattice a => JoinSemilattice (SelState a) where
instance BoundedJoinSemilattice a => BoundedJoinSemilattice (SelState a) where
bot = SelState { persistent: bot, transient: bot }

instance BoundedJoinSemilattice a => BoundedJoinSemilattice (ReactState a) where
bot = Inert

instance Eq a => Eq (ReactState a) where
derive instance Eq a => Eq (ReactState a) {-} where
eq (Reactive (SelState { persistent: a1, transient: b1 })) (Reactive (SelState { persistent: a2, transient: b2 })) = spy "reactive comparison" (eq a1 a2) && (eq b1 b2)
eq Inert Inert = spy "inert comparison" true
eq Inert _ = spy "inert-reactive" error absurd
eq _ Inert = spy "reactive-inert" error absurd
eq Inert _ = spy "inert-reactive" false
eq _ Inert = spy "reactive-inert" false-}

{-}
instance BoundedJoinSemilattice 𝕊 where
bot = None

-}
{-
yarn tidy
yarn build
Expand Down
4 changes: 2 additions & 2 deletions src/Lattice.purs
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ instance Neg Unit where

instance (Functor f, BoundedJoinSemilattice a) => BotOf (Unit × Raw f) (a × f a) where
botOf = const bot *** botOf -- for dictionary selections
else instance BotOf (f a) (f a') => BotOf (Dict (f a)) (Dict (f a')) where
else instance (Functor g, BotOf (f a) (f a')) => BotOf (g (f a)) (g (f a')) where
botOf = (<$>) botOf
else instance (Functor f, BoundedJoinSemilattice a') => BotOf (f a) (f a') where
botOf = (<$>) (const bot)
Expand All @@ -88,7 +88,7 @@ else instance (BotOf a b, BotOf c d) => BotOf (a × c) (b × d) where

instance (Functor f, BoundedMeetSemilattice a) => TopOf (Unit × Raw f) (a × f a) where
topOf = const top *** ((<$>) (const top)) -- for dictionary selections
else instance TopOf (f a) (f a') => TopOf (Dict (f a)) (Dict (f a')) where
else instance (Functor g, TopOf (f a) (f a')) => TopOf (g (f a)) (g (f a')) where
topOf = (<$>) topOf
else instance (Functor f, BoundedMeetSemilattice a') => TopOf (f a) (f a') where
topOf = (<$>) (const top)
Expand Down
9 changes: 5 additions & 4 deletions test/Test.purs
Original file line number Diff line number Diff line change
Expand Up @@ -8,19 +8,20 @@ import Effect (Effect)
import Effect.Aff (Aff)
import Test.Benchmark (benchmarks)
import Test.Specs.LinkedInputs (linkedInputs_cases)
import Test.Specs.LinkedOutputs (linkedOutputs_cases, linkedOutputs_spec3)
import Test.Specs.LinkedOutputs (linkedOutputs_cases)
import Test.Util.Mocha (run)
import Test.Util.Suite (BenchSuite, linkedInputsSuite, linkedOutputsSuite)
import Util (type (×), (×))

main :: Effect Unit
main = run tests
--main = run tests

--main = run $ asTestSuite $ suite desugar_cases
--main = run scratchpad
main = run scratchpad

scratchpad :: TestSuite
scratchpad = linkedOutputsSuite [ linkedOutputs_spec3 ]
scratchpad = linkedOutputsSuite linkedOutputs_cases
<> linkedInputsSuite linkedInputs_cases

type TestSuite = Array (String × Aff Unit)

Expand Down
3 changes: 2 additions & 1 deletion test/Util/Suite.purs
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,7 @@ linkedOutputsTest { spec, δ_out, out_expect } = do
v <- logTimeWhen timing.selectionResult (unwrap spec.file) \_ ->
pure (fst (selectionResult fig))
checkEq "selected" "expected" (toR𝔹 <$> v) (out_expect (botOf <$> v))
{- checkEq "selected" "expected" (cheatToSel <<< toR𝔹 <$> v) (cheatToSel <$> (out_expect (toR𝔹 <$> (kindOfBotS <$> v))))-}
pure fig

linkedOutputsSuite :: Array TestLinkedOutputsSpec -> Array (String × Aff Unit)
Expand All @@ -99,7 +100,7 @@ linkedInputsTest { spec, δ_in, in_expect } = do
fig <- loadFig (spec { file = spec.file }) <#> uncurry selectInput δ_in
γ <- logTimeWhen timing.selectionResult (unwrap spec.file) \_ ->
pure (snd (selectionResult fig))
checkEq "selected" "expected" (toR𝔹 <$> γ) ((in_expect (botOf <$> γ)))
checkEq "selected" "expected" (toR𝔹 <$> γ) (in_expect (botOf <$> γ))
pure fig

linkedInputsSuite :: Array TestLinkedInputsSpec -> Array (String × Aff Unit)
Expand Down

0 comments on commit 86b5fa8

Please sign in to comment.