{- |
Module      : App.Update
Copyright   : (c) Leon Vatthauer, 2026
License     : GPL-3
Maintainer  : Leon Vatthauer <leon.vatthauer@fau.de>
Stability   : experimental
Portability : non-portable (ghc-wasm-meta)

The update loop of the application, basically all of its logic.
-}
module App.Update where

------------------------------------------------------------------------------------------

import App.Model
import App.URLDecoder
import App.Views
import Data.Text qualified as T
import Fitch.Proof
import Fitch.Verification
import Miso (
  Effect,
  MisoString,
  ROOT,
  URI (..),
  back,
  castJSVal,
  consoleLog,
  focus,
  forward,
  fromMisoString,
  getElementById,
  getProperty,
  getURI,
  io,
  io_,
  jsNull,
  ms,
  prettyURI,
  pushURI,
  setSelectionRange,
  setSessionStorage,
  (!),
  (#),
 )
import Miso.DSL (jsg, (#))
import Miso.Effect (Sub)
import Miso.FFI.QQ (js)
import Miso.Html.Element qualified as H
import Miso.Html.Property qualified as HP
import Miso.Lens (Lens, LensCore (_get), use, (%=), (.=), (<~), (^.))
import Miso.Subscription.Util (createSub)
import Parser.Formula (
  FormulaParserState (FormulaParserState),
  parseAssumption,
  parseFormula,
 )
import Parser.Proof (parseProof)
import Parser.Rule (parseRuleApplication)
import Relude.Extra.Map (insert, member, (!?))
import Util ((%=?))

------------------------------------------------------------------------------------------

-- * Update loop

-- | Main execution loop of the application.
updateModel :: Action -> Effect ROOT Model Action
------------------------------------
-- Setup events
updateModel :: Action -> Effect ROOT Model Action
updateModel Action
Setup = Effect ROOT Model Action
proofReparse Effect ROOT Model Action
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Effect ROOT Model Action
forall (m :: * -> *). MonadState Model m => m ()
checkProof Effect ROOT Model Action
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Effect ROOT Model Action
updateTitle Effect ROOT Model Action
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Effect ROOT Model Action
replaceInitialURI
updateModel (InitMathJAX JSVal
domRef) = IO () -> Effect ROOT Model Action
forall parent model action. IO () -> Effect parent model action
io_ [js| MathJax.typesetPromise([${domRef}]); |]
updateModel (SetProof Proof
p) =
  RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Bool
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
-> (Proof -> Bool)
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Proof -> Proof -> Bool
forall a. Eq a => a -> a -> Bool
/= Proof
p)) (Effect ROOT Model Action -> Effect ROOT Model Action)
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall a b. (a -> b) -> a -> b
$ do
    Lens Model Proof
proof Lens Model Proof -> Proof -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Proof
p
    Effect ROOT Model Action
proofReparse
    Effect ROOT Model Action
updateProof
    RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Bool
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Lens Model Bool
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Bool
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Bool
onMobile) Effect ROOT Model Action
toggleSidebar
updateModel (Resize Bool
b) = Lens Model Bool
onMobile Lens Model Bool -> Bool -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Bool
b
------------------------------------
-- t'URI' events
updateModel (PopState URI
uri) = do
  URI -> Effect ROOT Model Action
readURI URI
uri Effect ROOT Model Action
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Effect ROOT Model Action
proofReparse Effect ROOT Model Action
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Effect ROOT Model Action
forall (m :: * -> *). MonadState Model m => m ()
checkProof Effect ROOT Model Action
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Effect ROOT Model Action
updateTitle
updateModel Action
NavigateForward = IO () -> Effect ROOT Model Action
forall parent model action. IO () -> Effect parent model action
io_ IO ()
forward
updateModel Action
NavigateBackward = IO () -> Effect ROOT Model Action
forall parent model action. IO () -> Effect parent model action
io_ IO ()
back
------------------------------------
-- Events that toggle UI elements
updateModel (OpenTooltip MisoString
name Bool
True) =
  Lens Model Bool
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Bool
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Bool
dragging RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Bool
-> (Bool -> Effect ROOT Model Action) -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> (a
    -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b)
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Bool
True -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass
    Bool
False -> MisoString -> Effect ROOT Model Action
showTooltip MisoString
name
updateModel (OpenTooltip MisoString
_ Bool
False) = Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass
updateModel Action
CloseTooltip = Effect ROOT Model Action
hideTooltip
updateModel Action
ToggleSidebar = Effect ROOT Model Action
toggleSidebar
------------------------------------
-- Drag n Drop events
updateModel (Drop DropLocation
LocationBin) = do
  dt <- Lens Model (Maybe (Either NodeAddr ProofAddr))
-> RWST
     (ComponentInfo ROOT)
     [Schedule Action]
     Model
     Identity
     (Maybe (Either NodeAddr ProofAddr))
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model (Maybe (Either NodeAddr ProofAddr))
dragTarget
  case dt of
    Maybe (Either NodeAddr ProofAddr)
Nothing -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass
    Just (Left NodeAddr
na) -> Lens Model Proof
proof Lens Model Proof
-> (Proof -> Maybe Proof) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> (field -> Maybe field) -> m ()
%=? NodeAddr -> Proof -> Maybe Proof
naRemove NodeAddr
na
    Just (Right ProofAddr
pa) -> Lens Model Proof
proof Lens Model Proof
-> (Proof -> Maybe Proof) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> (field -> Maybe field) -> m ()
%=? ProofAddr -> Proof -> Maybe Proof
paRemove ProofAddr
pa
  clearDrag >> updateProof
updateModel (Drop (LineAddr NodeAddr
targetAddr)) = NodeAddr -> Effect ROOT Model Action
dropBeforeLine NodeAddr
targetAddr
updateModel (DragEnter NodeAddr
na) = do
  p <- Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof
  use spawnType
    >>= \case
      Just (NodeAddr -> SpawnType -> Bool
canSpawnBefore NodeAddr
na -> Bool
True) ->
        Lens Model (Maybe NodeAddr)
currentHoverLine Lens Model (Maybe NodeAddr)
-> Maybe NodeAddr -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just NodeAddr
na
      Just (NodeAddr -> SpawnType -> Bool
canSpawnBefore NodeAddr
na -> Bool
False) ->
        Lens Model (Maybe NodeAddr)
currentHoverLine Lens Model (Maybe NodeAddr)
-> Maybe NodeAddr -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Maybe NodeAddr
forall a. Maybe a
Nothing
      Maybe SpawnType
Nothing ->
        Lens Model (Maybe (Either NodeAddr ProofAddr))
-> RWST
     (ComponentInfo ROOT)
     [Schedule Action]
     Model
     Identity
     (Maybe (Either NodeAddr ProofAddr))
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model (Maybe (Either NodeAddr ProofAddr))
dragTarget RWST
  (ComponentInfo ROOT)
  [Schedule Action]
  Model
  Identity
  (Maybe (Either NodeAddr ProofAddr))
-> (Maybe (Either NodeAddr ProofAddr) -> Effect ROOT Model Action)
-> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> (a
    -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b)
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Just (Left ((NodeAddr -> NodeAddr -> Bool) -> NodeAddr -> NodeAddr -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Proof -> NodeAddr -> NodeAddr -> Bool
naCanMoveBefore Proof
p) NodeAddr
na -> Bool
True)) -> Lens Model (Maybe NodeAddr)
currentHoverLine Lens Model (Maybe NodeAddr)
-> Maybe NodeAddr -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just NodeAddr
na
          Just (Right ProofAddr
sourcePA) -> case NodeAddr -> Proof -> Maybe ProofAddr
paFromNA NodeAddr
na Proof
p of
            Maybe ProofAddr
Nothing -> Lens Model (Maybe NodeAddr)
currentHoverLine Lens Model (Maybe NodeAddr)
-> Maybe NodeAddr -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Maybe NodeAddr
forall a. Maybe a
Nothing
            Just ProofAddr
targetPA ->
              Lens Model (Maybe NodeAddr)
currentHoverLine
                Lens Model (Maybe NodeAddr)
-> Maybe NodeAddr -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= if ProofAddr -> ProofAddr -> Bool
paCanMoveBefore ProofAddr
sourcePA ProofAddr
targetPA then NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just NodeAddr
na else Maybe NodeAddr
forall a. Maybe a
Nothing
          Maybe (Either NodeAddr ProofAddr)
_ -> Lens Model (Maybe NodeAddr)
currentHoverLine Lens Model (Maybe NodeAddr)
-> Maybe NodeAddr -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Maybe NodeAddr
forall a. Maybe a
Nothing
updateModel Action
DragLeave = Lens Model (Maybe NodeAddr)
currentHoverLine Lens Model (Maybe NodeAddr)
-> Maybe NodeAddr -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Maybe NodeAddr
forall a. Maybe a
Nothing
updateModel (SpawnStart SpawnType
st) = do
  Effect ROOT Model Action
hideTooltip
  Lens Model Bool
dragging Lens Model Bool -> Bool -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Bool
True
  Lens Model (Maybe SpawnType)
spawnType Lens Model (Maybe SpawnType)
-> Maybe SpawnType -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= SpawnType -> Maybe SpawnType
forall a. a -> Maybe a
Just SpawnType
st
updateModel (DragStart Either NodeAddr ProofAddr
dt) = do
  Effect ROOT Model Action
hideTooltip
  Lens Model Bool
dragging Lens Model Bool -> Bool -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Bool
True
  Lens Model (Maybe NodeAddr)
lastDragged Lens Model (Maybe NodeAddr)
-> Maybe NodeAddr -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Maybe NodeAddr
forall a. Maybe a
Nothing
  Lens Model (Maybe (Either NodeAddr ProofAddr))
dragTarget Lens Model (Maybe (Either NodeAddr ProofAddr))
-> Maybe (Either NodeAddr ProofAddr) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Either NodeAddr ProofAddr -> Maybe (Either NodeAddr ProofAddr)
forall a. a -> Maybe a
Just Either NodeAddr ProofAddr
dt
updateModel Action
DragEnd = do
  chl <- Lens Model (Maybe NodeAddr)
-> RWST
     (ComponentInfo ROOT)
     [Schedule Action]
     Model
     Identity
     (Maybe NodeAddr)
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model (Maybe NodeAddr)
currentHoverLine
  whenJust chl dropBeforeLine
  clearDrag
------------------------------------
-- Input related events
updateModel (Focus Either NodeAddr NodeAddr
ea) = do
  fline <- Lens Model (Maybe (Either NodeAddr NodeAddr))
-> RWST
     (ComponentInfo ROOT)
     [Schedule Action]
     Model
     Identity
     (Maybe (Either NodeAddr NodeAddr))
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model (Maybe (Either NodeAddr NodeAddr))
focusedLine
  if fline /= Just ea
    then
      setFocus ea
    else pass
updateModel (Blur Either NodeAddr NodeAddr
ea) = do
  fline <- Lens Model (Maybe (Either NodeAddr NodeAddr))
-> RWST
     (ComponentInfo ROOT)
     [Schedule Action]
     Model
     Identity
     (Maybe (Either NodeAddr NodeAddr))
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model (Maybe (Either NodeAddr NodeAddr))
focusedLine
  focusedLine .= if fline == Just ea then Nothing else fline
updateModel Action
Change = Effect ROOT Model Action
updateProof
updateModel (Input MisoString
str JSVal
ref) = do
  m <- RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Model
forall s (m :: * -> *). MonadState s m => m s
get
  fline <- use focusedLine
  -- save selectionStart and selectionEnd
  case fline of
    Maybe (Either NodeAddr NodeAddr)
Nothing -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass
    Just Either NodeAddr NodeAddr
addr -> IO Action -> Effect ROOT Model Action
forall action parent model. IO action -> Effect parent model action
io (IO Action -> Effect ROOT Model Action)
-> IO Action -> Effect ROOT Model Action
forall a b. (a -> b) -> a -> b
$ do
      Just (start :: Int) <- JSVal -> IO (Maybe Int)
forall a. FromJSVal a => JSVal -> IO (Maybe a)
castJSVal (JSVal -> IO (Maybe Int)) -> IO JSVal -> IO (Maybe Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< JSVal -> MisoString -> IO JSVal
getProperty JSVal
ref MisoString
"selectionStart"
      Just (end :: Int) <- castJSVal =<< getProperty ref "selectionEnd"
      pure $ ProcessInput str start end addr
updateModel (ProcessInput MisoString
str Int
start Int
end Either NodeAddr NodeAddr
eaddr) = do
  m <- RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Model
forall s (m :: * -> *). MonadState s m => m s
get
  (identifier, len) <- case eaddr of
    Left NodeAddr
addr -> do
      if NodeAddr -> Bool
isNestedNAAssumption NodeAddr
addr
        then do
          let a :: Wrapper RawAssumption
a =
                Model -> Int -> MisoString -> Wrapper RawAssumption
forall a. FromText a => Model -> Int -> MisoString -> Wrapper a
tryParse
                  Model
m
                  (NodeAddr -> Proof -> Int
lineNoOr999 NodeAddr
addr (Model
m Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof))
                  (MisoString -> MisoString
forall a. FromMisoString a => MisoString -> a
fromMisoString MisoString
str) ::
                  Wrapper RawAssumption
          Lens Model Proof
proof Lens Model Proof
-> (Proof -> Maybe Proof) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> (field -> Maybe field) -> m ()
%=? Either (Assumption -> Assumption) (Formula -> Formula)
-> NodeAddr -> Proof -> Maybe Proof
naUpdateFormula ((Assumption -> Assumption)
-> Either (Assumption -> Assumption) (Formula -> Formula)
forall a b. a -> Either a b
Left (\(Wrapper RawAssumption
_, Wrapper RuleApplication
r) -> (Wrapper RawAssumption
a, Wrapper RuleApplication
r))) NodeAddr
addr
          (MisoString, Int)
-> RWST
     (ComponentInfo ROOT)
     [Schedule Action]
     Model
     Identity
     (MisoString, Int)
forall a.
a -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NodeAddr -> Proof -> MisoString
mkFormulaInputId NodeAddr
addr (Model
m Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof), MisoString -> Int
T.length (MisoString -> Int)
-> (Wrapper RawAssumption -> MisoString)
-> Wrapper RawAssumption
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapper RawAssumption -> MisoString
forall a. Wrapper a -> MisoString
getText (Wrapper RawAssumption -> Int) -> Wrapper RawAssumption -> Int
forall a b. (a -> b) -> a -> b
$ Wrapper RawAssumption
a)
        else do
          let f :: Formula
f =
                Model -> Int -> MisoString -> Formula
forall a. FromText a => Model -> Int -> MisoString -> Wrapper a
tryParse
                  Model
m
                  (NodeAddr -> Proof -> Int
lineNoOr999 NodeAddr
addr (Model
m Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof))
                  (MisoString -> MisoString
forall a. FromMisoString a => MisoString -> a
fromMisoString MisoString
str) ::
                  Formula
          Lens Model Proof
proof Lens Model Proof
-> (Proof -> Maybe Proof) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> (field -> Maybe field) -> m ()
%=? Either (Assumption -> Assumption) (Formula -> Formula)
-> NodeAddr -> Proof -> Maybe Proof
naUpdateFormula ((Formula -> Formula)
-> Either (Assumption -> Assumption) (Formula -> Formula)
forall a b. b -> Either a b
Right ((Formula -> Formula)
 -> Either (Assumption -> Assumption) (Formula -> Formula))
-> (Formula -> Formula)
-> Either (Assumption -> Assumption) (Formula -> Formula)
forall a b. (a -> b) -> a -> b
$ Formula -> Formula -> Formula
forall a b. a -> b -> a
const Formula
f) NodeAddr
addr
          (MisoString, Int)
-> RWST
     (ComponentInfo ROOT)
     [Schedule Action]
     Model
     Identity
     (MisoString, Int)
forall a.
a -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NodeAddr -> Proof -> MisoString
mkFormulaInputId NodeAddr
addr (Model
m Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof), MisoString -> Int
T.length (MisoString -> Int) -> (Formula -> MisoString) -> Formula -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> MisoString
forall a. Wrapper a -> MisoString
getText (Formula -> Int) -> Formula -> Int
forall a b. (a -> b) -> a -> b
$ Formula
f)
    Right NodeAddr
addr -> do
      let r :: Wrapper RuleApplication
r =
            Model -> Int -> MisoString -> Wrapper RuleApplication
forall a. FromText a => Model -> Int -> MisoString -> Wrapper a
tryParse
              Model
m
              (NodeAddr -> Proof -> Int
lineNoOr999 NodeAddr
addr (Model
m Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof))
              (MisoString -> MisoString
forall a. FromMisoString a => MisoString -> a
fromMisoString MisoString
str) ::
              Wrapper RuleApplication
      Lens Model Proof
proof Lens Model Proof
-> (Proof -> Maybe Proof) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> (field -> Maybe field) -> m ()
%=? (Wrapper RuleApplication -> Wrapper RuleApplication)
-> NodeAddr -> Proof -> Maybe Proof
naUpdateRule (Wrapper RuleApplication
-> Wrapper RuleApplication -> Wrapper RuleApplication
forall a b. a -> b -> a
const Wrapper RuleApplication
r) NodeAddr
addr
      (MisoString, Int)
-> RWST
     (ComponentInfo ROOT)
     [Schedule Action]
     Model
     Identity
     (MisoString, Int)
forall a.
a -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NodeAddr -> Proof -> MisoString
mkRuleInputId NodeAddr
addr (Model
m Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof), MisoString -> Int
T.length (MisoString -> Int)
-> (Wrapper RuleApplication -> MisoString)
-> Wrapper RuleApplication
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapper RuleApplication -> MisoString
forall a. Wrapper a -> MisoString
getText (Wrapper RuleApplication -> Int) -> Wrapper RuleApplication -> Int
forall a b. (a -> b) -> a -> b
$ Wrapper RuleApplication
r)

  checkProof
  let delta = MisoString -> Int
T.length (MisoString -> MisoString
forall a. FromMisoString a => MisoString -> a
fromMisoString MisoString
str) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
len
  -- restore selectionStart and selectionEnd (delta-adjusted)
  when (delta /= 0) $
    io_ $
      setSelectionRange
        identifier
        (start - delta)
        (end - delta)
------------------------------------
updateModel Action
Nop = Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass

------------------------------------------------------------------------------------------

-- * Effects

{- | Re-checks a t'Proof', i.e. runs the verifier, updates the t'URI' and document title.

Should be called after every change to the t'Proof'.
-}
updateProof :: Effect ROOT Model Action
updateProof :: Effect ROOT Model Action
updateProof = Effect ROOT Model Action
forall (m :: * -> *). MonadState Model m => m ()
checkProof Effect ROOT Model Action
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Effect ROOT Model Action
pushProofURI Effect ROOT Model Action
-> Effect ROOT Model Action -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Effect ROOT Model Action
updateTitle

{- | Updates the @document.title@ to show how many errors there are and
what the conclusion of the t'Proof' is.
-}
updateTitle :: Effect ROOT Model Action
updateTitle :: Effect ROOT Model Action
updateTitle = do
  p@(SubProof _ _ (Derivation f _)) <- Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof
  let title =
        ( case Proof -> Int
proofErrors Proof
p of
            Int
0 -> MisoString
forall a. Monoid a => a
mempty
            Int
n -> Int -> MisoString
forall b a. (Show a, IsString b) => a -> b
show Int
n MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> MisoString
" ✖ | "
        )
          MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> Formula -> MisoString
forall a. PrettyPrint a => a -> MisoString
prettyPrint Formula
f
  io_ [js| document.title = ${title} |]

{- | Runs the t'Proof' verification algorithm, i.e.

1. Checks that symbols only occur with the same arity
2. Checks freshness t'Assumption's
3. Verifies all t'RuleApplication's.
-}
checkProof :: forall m. (MonadState Model m) => m ()
checkProof :: forall (m :: * -> *). MonadState Model m => m ()
checkProof = do
  p <- Lens Model Proof -> m Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof
  ruleMap <- use rules
  let (fsymbs, psymbs, p') = regenerateSymbols p
      p'' = Proof -> Proof
checkFreshness Proof
p'
      p''' = [(MisoString, RuleSpec)] -> Proof -> Proof
verifyProof [(MisoString, RuleSpec)]
ruleMap Proof
p''
  functionSymbols .= fsymbs
  predicateSymbols .= psymbs
  proof .= p'''

-- | To be called after dragging ends, resets all drag parameters.
clearDrag :: Effect ROOT Model Action
clearDrag :: Effect ROOT Model Action
clearDrag = do
  Lens Model (Maybe NodeAddr)
currentHoverLine Lens Model (Maybe NodeAddr)
-> Maybe NodeAddr -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Maybe NodeAddr
forall a. Maybe a
Nothing
  Lens Model Bool
dragging Lens Model Bool -> Bool -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Bool
False
  Lens Model (Maybe (Either NodeAddr ProofAddr))
dragTarget Lens Model (Maybe (Either NodeAddr ProofAddr))
-> Maybe (Either NodeAddr ProofAddr) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Maybe (Either NodeAddr ProofAddr)
forall a. Maybe a
Nothing
  Lens Model (Maybe SpawnType)
spawnType Lens Model (Maybe SpawnType)
-> Maybe SpawnType -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Maybe SpawnType
forall a. Maybe a
Nothing

-- | Takes a t'URI' and reads in a proof if it contains one.
readURI :: URI -> Effect ROOT Model Action
readURI :: URI -> Effect ROOT Model Action
readURI URI
uri = do
  case URI -> Map MisoString (Maybe MisoString)
uriQueryString URI
uri Map MisoString (Maybe MisoString)
-> Key (Map MisoString (Maybe MisoString))
-> Maybe (Val (Map MisoString (Maybe MisoString)))
forall t. StaticMap t => t -> Key t -> Maybe (Val t)
!? MisoString
Key (Map MisoString (Maybe MisoString))
"proof" of
    Just (Just MisoString
str) -> case MisoString -> Maybe Proof
decodeFromUrl (MisoString -> MisoString
forall a. FromMisoString a => MisoString -> a
fromMisoString MisoString
str :: Text) of
      Maybe Proof
Nothing -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass
      Just (Proof
p :: Proof) -> Lens Model Proof
proof Lens Model Proof -> Proof -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Proof
p
    Maybe (Val (Map MisoString (Maybe MisoString)))
_ -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass

{- | Pushes a new t'URI' that has the t'Proof' encoded to the history stack.

See @static/Navigation.js@ for the used @pushStateHistory@ function.
-}
pushProofURI :: Effect ROOT Model Action
pushProofURI :: Effect ROOT Model Action
pushProofURI = do
  p <- Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof
  io_ $ do
    uri <- getURI
    let newURI =
          URI
uri
            { uriQueryString =
                insert "proof" (Just . ms $ encodeForUrl p) (uriQueryString uri)
            }
    if uri /= newURI
      then void $ jsg "window" # "pushStateHistory" $ prettyURI newURI
      else pass

{- | To be called in the v'Setup' t'Action'.
Replaces the initial URI that possible does not contain the queryParameters,
with a URI that does. Also initializes the tracking of the HTML5 historu API.

See @static/Navigation.js@ for the used @initHistory@ function.
-}
replaceInitialURI :: Effect ROOT Model Action
replaceInitialURI :: Effect ROOT Model Action
replaceInitialURI = do
  p <- Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof
  l <- use logic
  io_ $ do
    uri <- getURI
    let newURI =
          URI
            { uriPath :: MisoString
uriPath = URI -> MisoString
uriPath URI
uri
            , uriQueryString :: Map MisoString (Maybe MisoString)
uriQueryString =
                OneItem (Map MisoString (Maybe MisoString))
-> Map MisoString (Maybe MisoString)
forall x. One x => OneItem x -> x
one (MisoString
"proof", MisoString -> Maybe MisoString
forall a. a -> Maybe a
Just (MisoString -> Maybe MisoString)
-> (MisoString -> MisoString) -> MisoString -> Maybe MisoString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms (MisoString -> Maybe MisoString) -> MisoString -> Maybe MisoString
forall a b. (a -> b) -> a -> b
$ Proof -> MisoString
encodeForUrl Proof
p)
                  Map MisoString (Maybe MisoString)
-> Map MisoString (Maybe MisoString)
-> Map MisoString (Maybe MisoString)
forall a. Semigroup a => a -> a -> a
<> OneItem (Map MisoString (Maybe MisoString))
-> Map MisoString (Maybe MisoString)
forall x. One x => OneItem x -> x
one (MisoString
"logic", MisoString -> Maybe MisoString
forall a. a -> Maybe a
Just (MisoString -> Maybe MisoString) -> MisoString -> Maybe MisoString
forall a b. (a -> b) -> a -> b
$ Logic -> MisoString
forall b a. (Show a, IsString b) => a -> b
show Logic
l)
            , uriFragment :: MisoString
uriFragment = MisoString
""
            }
    void $ jsg "window" # "initHistory" $ prettyURI newURI

-- | Re-parses every line of the current t'Proof'
proofReparse :: Effect ROOT Model Action
proofReparse :: Effect ROOT Model Action
proofReparse = RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Model
forall s (m :: * -> *). MonadState s m => m s
get RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Model
-> (Model -> Effect ROOT Model Action) -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> (a
    -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b)
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Model
m -> Lens Model Proof
proof Lens Model Proof -> (Proof -> Proof) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> (field -> field) -> m ()
%= Model -> Proof -> Proof
reparseProof Model
m

-- | Re-parses a single t'Derivation' or t'Assumption'.
naReparseLine :: NodeAddr -> Effect ROOT Model Action
naReparseLine :: NodeAddr -> Effect ROOT Model Action
naReparseLine NodeAddr
na =
  RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Model
forall s (m :: * -> *). MonadState s m => m s
get RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Model
-> (Model -> Effect ROOT Model Action) -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> (a
    -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b)
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Model
m ->
    Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
-> (Proof -> Effect ROOT Model Action) -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> (a
    -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b)
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Proof
p -> case (NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup NodeAddr
na Proof
p, NodeAddr -> Proof -> Maybe Int
fromNodeAddr NodeAddr
na Proof
p) of
      (Just (Left (Wrapper RawAssumption
a, Wrapper RuleApplication
r)), Just Int
lineNo) ->
        Lens Model Proof
proof Lens Model Proof
-> (Proof -> Maybe Proof) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> (field -> Maybe field) -> m ()
%=? Either (Assumption -> Assumption) (Formula -> Formula)
-> NodeAddr -> Proof -> Maybe Proof
naUpdateFormula ((Assumption -> Assumption)
-> Either (Assumption -> Assumption) (Formula -> Formula)
forall a b. a -> Either a b
Left ((Assumption -> Assumption)
 -> Either (Assumption -> Assumption) (Formula -> Formula))
-> (Assumption -> Assumption)
-> Either (Assumption -> Assumption) (Formula -> Formula)
forall a b. (a -> b) -> a -> b
$ Assumption -> Assumption -> Assumption
forall a b. a -> b -> a
const (Model -> Int -> Wrapper RawAssumption -> Wrapper RawAssumption
forall a. FromText a => Model -> Int -> Wrapper a -> Wrapper a
reparse Model
m Int
lineNo Wrapper RawAssumption
a, Wrapper RuleApplication
r)) NodeAddr
na
      (Just (Right (Derivation Formula
f Wrapper RuleApplication
_)), Just Int
lineNo) ->
        Lens Model Proof
proof Lens Model Proof
-> (Proof -> Maybe Proof) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> (field -> Maybe field) -> m ()
%=? Either (Assumption -> Assumption) (Formula -> Formula)
-> NodeAddr -> Proof -> Maybe Proof
naUpdateFormula ((Formula -> Formula)
-> Either (Assumption -> Assumption) (Formula -> Formula)
forall a b. b -> Either a b
Right ((Formula -> Formula)
 -> Either (Assumption -> Assumption) (Formula -> Formula))
-> (Formula -> Formula)
-> Either (Assumption -> Assumption) (Formula -> Formula)
forall a b. (a -> b) -> a -> b
$ Formula -> Formula -> Formula
forall a b. a -> b -> a
const (Model -> Int -> Formula -> Formula
forall a. FromText a => Model -> Int -> Wrapper a -> Wrapper a
reparse Model
m Int
lineNo Formula
f)) NodeAddr
na
      (Maybe (Either Assumption Derivation), Maybe Int)
_ -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass

-- | Move or create a t'Assumption', t'Derivation' or t'Proof' before a given t'NodeAddr'.
dropBeforeLine :: NodeAddr -> Effect ROOT Model Action
dropBeforeLine :: NodeAddr -> Effect ROOT Model Action
dropBeforeLine NodeAddr
targetAddr = do
  m <- RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Model
forall s (m :: * -> *). MonadState s m => m s
get
  p <- use proof
  use dragTarget >>= \case
    Maybe (Either NodeAddr ProofAddr)
Nothing -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass
    Just (Left NodeAddr
na) -> do
      Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
-> (Proof -> Effect ROOT Model Action) -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> (a
    -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b)
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Proof
p -> case NodeAddr -> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naMoveBefore NodeAddr
targetAddr NodeAddr
na Proof
p of
        Maybe (NodeAddr, Proof)
Nothing -> Lens Model (Maybe NodeAddr)
lastDragged Lens Model (Maybe NodeAddr)
-> Maybe NodeAddr -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just NodeAddr
na
        Just (NodeAddr
ta, Proof
p) -> do
          Lens Model Proof
proof Lens Model Proof -> (Proof -> Proof) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> (field -> field) -> m ()
%= Proof -> Proof -> Proof
forall a b. a -> b -> a
const Proof
p
          NodeAddr -> Effect ROOT Model Action
naReparseLine NodeAddr
ta
    Just (Right ProofAddr
pa) -> do
      p <- Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof
      proof %=? \Proof
p -> do
        paTarget <- NodeAddr -> Proof -> Maybe ProofAddr
paFromNA NodeAddr
targetAddr Proof
p
        snd <$> paMoveBefore paTarget pa p
  use spawnType >>= \case
    Maybe SpawnType
Nothing -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass
    Just SpawnType
SpawnLine -> do
      Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof
        RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
-> (Proof -> Effect ROOT Model Action) -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> (a
    -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b)
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Proof
p ->
          case Either Assumption Derivation
-> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naInsertBefore
            (Derivation -> Either Assumption Derivation
forall a b. b -> Either a b
Right (Derivation -> Either Assumption Derivation)
-> Derivation -> Either Assumption Derivation
forall a b. (a -> b) -> a -> b
$ LensCore Derivation Model -> Model -> Derivation
forall field record. LensCore field record -> record -> field
_get LensCore Derivation Model
emptyDerivation Model
m)
            NodeAddr
targetAddr
            Proof
p of
            Just (NodeAddr
na, Proof
p) -> Lens Model Proof
proof Lens Model Proof -> Proof -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Proof
p
            Maybe (NodeAddr, Proof)
_ -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass
    Just SpawnType
SpawnProof ->
      Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof
        RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
-> (Proof -> Effect ROOT Model Action) -> Effect ROOT Model Action
forall a b.
RWST (ComponentInfo ROOT) [Schedule Action] Model Identity a
-> (a
    -> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b)
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Proof
p -> case Maybe (Maybe (ProofAddr, Proof)) -> Maybe (ProofAddr, Proof)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (ProofAddr, Proof)) -> Maybe (ProofAddr, Proof))
-> Maybe (Maybe (ProofAddr, Proof)) -> Maybe (ProofAddr, Proof)
forall a b. (a -> b) -> a -> b
$
          (Proof -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof))
-> Maybe Proof
-> Maybe ProofAddr
-> Maybe Proof
-> Maybe (Maybe (ProofAddr, Proof))
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3
            Proof -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paInsertBefore
            (Proof -> Maybe Proof
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof) -> Proof -> Maybe Proof
forall a b. (a -> b) -> a -> b
$ [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [] [] (LensCore Derivation Model -> Model -> Derivation
forall field record. LensCore field record -> record -> field
_get LensCore Derivation Model
emptyDerivation Model
m))
            (NodeAddr -> Proof -> Maybe ProofAddr
paFromNA NodeAddr
targetAddr Proof
p)
            (Proof -> Maybe Proof
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Proof
p) of
          Just (ProofAddr
pa, Proof
p) -> Lens Model Proof
proof Lens Model Proof -> Proof -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Proof
p
          Maybe (ProofAddr, Proof)
_ -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass
  clearDrag >> updateProof

{- | Set focus to a @<input>@ field specified by a t'NodeAddr'
(either the t'Formula' or the t'RuleApplication').
-}
setFocus :: Either NodeAddr NodeAddr -> Effect ROOT Model Action
setFocus :: Either NodeAddr NodeAddr -> Effect ROOT Model Action
setFocus Either NodeAddr NodeAddr
ea = do
  Lens Model (Maybe (Either NodeAddr NodeAddr))
focusedLine Lens Model (Maybe (Either NodeAddr NodeAddr))
-> Maybe (Either NodeAddr NodeAddr) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Either NodeAddr NodeAddr -> Maybe (Either NodeAddr NodeAddr)
forall a. a -> Maybe a
Just Either NodeAddr NodeAddr
ea
  p <- Lens Model Proof
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Proof
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Proof
proof
  case ea of
    Left NodeAddr
na -> IO () -> Effect ROOT Model Action
forall parent model action. IO () -> Effect parent model action
io_ (IO () -> Effect ROOT Model Action)
-> IO () -> Effect ROOT Model Action
forall a b. (a -> b) -> a -> b
$ MisoString -> IO ()
focus (NodeAddr -> Proof -> MisoString
mkFormulaInputId NodeAddr
na Proof
p)
    Right NodeAddr
na -> IO () -> Effect ROOT Model Action
forall parent model action. IO () -> Effect parent model action
io_ (IO () -> Effect ROOT Model Action)
-> IO () -> Effect ROOT Model Action
forall a b. (a -> b) -> a -> b
$ MisoString -> IO ()
focus (NodeAddr -> Proof -> MisoString
mkRuleInputId NodeAddr
na Proof
p)

-- | Show the @<popover>@ with the given @id@.
showTooltip :: MisoString -> Effect ROOT Model Action
showTooltip :: MisoString -> Effect ROOT Model Action
showTooltip MisoString
name = do
  tt <- Lens Model (Maybe MisoString)
-> RWST
     (ComponentInfo ROOT)
     [Schedule Action]
     Model
     Identity
     (Maybe MisoString)
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model (Maybe MisoString)
currentTooltip
  if tt == Just name
    then pass
    else do
      io_ [js| let ref = document.getElementById(${name}); if (ref) { ref.showPopover() } |]
      currentTooltip .= Just name

-- | Hide the @<popover>@ with the given @id@.
hideTooltip :: Effect ROOT Model Action
hideTooltip :: Effect ROOT Model Action
hideTooltip = do
  tt <- Lens Model (Maybe MisoString)
-> RWST
     (ComponentInfo ROOT)
     [Schedule Action]
     Model
     Identity
     (Maybe MisoString)
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model (Maybe MisoString)
currentTooltip
  case tt of
    Maybe MisoString
Nothing -> Effect ROOT Model Action
forall (f :: * -> *). Applicative f => f ()
pass
    Just MisoString
name -> do
      IO () -> Effect ROOT Model Action
forall parent model action. IO () -> Effect parent model action
io_ [js| let ref = document.getElementById(${name}); if (ref) { ref.hidePopover() } |]
      Lens Model (Maybe MisoString)
currentTooltip Lens Model (Maybe MisoString)
-> Maybe MisoString -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> field -> m ()
.= Maybe MisoString
forall a. Maybe a
Nothing

-- | Flip the sidebar state and save it in sessionStorage
toggleSidebar :: Effect ROOT Model Action
toggleSidebar :: Effect ROOT Model Action
toggleSidebar = do
  Lens Model Bool
sidebarToggle Lens Model Bool -> (Bool -> Bool) -> Effect ROOT Model Action
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> (field -> field) -> m ()
%= Bool -> Bool
not
  st <- Lens Model Bool
-> RWST (ComponentInfo ROOT) [Schedule Action] Model Identity Bool
forall record (m :: * -> *) field.
MonadState record m =>
Lens record field -> m field
use Lens Model Bool
sidebarToggle
  io_ $ setSessionStorage "sidebarToggle" (ms $ show st)

-- * Parsing

-- | Class for parsing t`Text`
class FromText a where
  {- | Takes a t`Model` and some t`Text` and tries to parse it to the desired type.
  On failure returns an error message.
  -}
  fromText :: Model -> Int -> Text -> Either Text a

instance FromText RawFormula where
  fromText :: Model -> Int -> Text -> Either Text RawFormula
  fromText :: Model -> Int -> MisoString -> Either MisoString RawFormula
fromText Model
m =
    FormulaParserState
-> Int -> MisoString -> Either MisoString RawFormula
parseFormula
      ( [(MisoString, MisoString, Int)]
-> [(MisoString, MisoString)]
-> [(MisoString, MisoString)]
-> FormulaParserState
FormulaParserState
          (Model
m Model
-> Lens Model [(MisoString, MisoString, Int)]
-> [(MisoString, MisoString, Int)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString, Int)]
operators)
          (Model
m Model
-> Lens Model [(MisoString, MisoString)]
-> [(MisoString, MisoString)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString)]
infixPreds)
          (Model
m Model
-> Lens Model [(MisoString, MisoString)]
-> [(MisoString, MisoString)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString)]
quantifiers)
      )

instance FromText RawAssumption where
  fromText :: Model -> Int -> Text -> Either Text RawAssumption
  fromText :: Model -> Int -> MisoString -> Either MisoString RawAssumption
fromText Model
m =
    FormulaParserState
-> Int -> MisoString -> Either MisoString RawAssumption
parseAssumption
      ( [(MisoString, MisoString, Int)]
-> [(MisoString, MisoString)]
-> [(MisoString, MisoString)]
-> FormulaParserState
FormulaParserState
          (Model
m Model
-> Lens Model [(MisoString, MisoString, Int)]
-> [(MisoString, MisoString, Int)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString, Int)]
operators)
          (Model
m Model
-> Lens Model [(MisoString, MisoString)]
-> [(MisoString, MisoString)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString)]
infixPreds)
          (Model
m Model
-> Lens Model [(MisoString, MisoString)]
-> [(MisoString, MisoString)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString)]
quantifiers)
      )

instance FromText RuleApplication where
  fromText :: Model -> Int -> Text -> Either Text RuleApplication
  fromText :: Model -> Int -> MisoString -> Either MisoString RuleApplication
fromText Model
_ = Int -> MisoString -> Either MisoString RuleApplication
parseRuleApplication

{- | Wrapper for `fromText` that also takes a list of aliases and
tries to replace these aliases in the t`Text`
-}
tryParse ::
  forall a.
  (FromText a) =>
  -- | The t'Model'.
  Model ->
  -- | Line number.
  Int ->
  -- | Text to parse.
  Text ->
  -- | Parse result.
  Wrapper a
tryParse :: forall a. FromText a => Model -> Int -> MisoString -> Wrapper a
tryParse Model
m Int
n MisoString
txt = case Model -> Int -> MisoString -> Either MisoString a
forall a.
FromText a =>
Model -> Int -> MisoString -> Either MisoString a
fromText Model
m Int
n MisoString
replacedTxt :: Either Text a of
  Left MisoString
err -> MisoString -> MisoString -> Wrapper a
forall a. MisoString -> MisoString -> Wrapper a
Unparsed MisoString
replacedTxt MisoString
err
  Right a
result -> MisoString -> a -> Wrapper a
forall a. MisoString -> a -> Wrapper a
ParsedValid MisoString
replacedTxt a
result
 where
  replacedTxt :: MisoString
replacedTxt =
    ((MisoString, MisoString) -> MisoString -> MisoString)
-> MisoString -> [(MisoString, MisoString)] -> MisoString
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
      (\(MisoString
alias, MisoString
name) MisoString
t -> HasCallStack =>
MisoString -> MisoString -> MisoString -> MisoString
MisoString -> MisoString -> MisoString -> MisoString
T.replace MisoString
alias MisoString
name MisoString
t)
      (((MisoString, MisoString, Int) -> MisoString -> MisoString)
-> MisoString -> [(MisoString, MisoString, Int)] -> MisoString
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(MisoString
alias, MisoString
name, Int
_) MisoString
t -> HasCallStack =>
MisoString -> MisoString -> MisoString -> MisoString
MisoString -> MisoString -> MisoString -> MisoString
T.replace MisoString
alias MisoString
name MisoString
t) MisoString
txt (Model
m Model
-> Lens Model [(MisoString, MisoString, Int)]
-> [(MisoString, MisoString, Int)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString, Int)]
operators))
      (Model
m Model
-> Lens Model [(MisoString, MisoString)]
-> [(MisoString, MisoString)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString)]
quantifiers)

-- | Takes some t'Wrapper' and re-parses it.
reparse ::
  forall a.
  (FromText a) =>
  -- | The t'Model'.
  Model ->
  -- | The line number.
  Int ->
  -- | The t'Wrapper' to re-parse.
  Wrapper a ->
  -- | Parse result.
  Wrapper a
reparse :: forall a. FromText a => Model -> Int -> Wrapper a -> Wrapper a
reparse Model
m Int
n Wrapper a
w = Model -> Int -> MisoString -> Wrapper a
forall a. FromText a => Model -> Int -> MisoString -> Wrapper a
tryParse Model
m Int
n (Wrapper a -> MisoString
forall a. Wrapper a -> MisoString
getText Wrapper a
w)

-- | Uses 'reparse' to re-parse the whole t'Proof'.
reparseProof :: Model -> Proof -> Proof
reparseProof :: Model -> Proof -> Proof
reparseProof Model
model = (Int -> Assumption -> Assumption)
-> (Int -> Derivation -> Derivation) -> Proof -> Proof
pMapLinesWithLineNo Int -> Assumption -> Assumption
reparseAssumption Int -> Derivation -> Derivation
reparseDerivation
 where
  reparseDerivation :: Int -> Derivation -> Derivation
reparseDerivation Int
line (Derivation Formula
f Wrapper RuleApplication
r) =
    Formula -> Wrapper RuleApplication -> Derivation
Derivation
      (Model -> Int -> Formula -> Formula
forall a. FromText a => Model -> Int -> Wrapper a -> Wrapper a
reparse Model
model Int
line Formula
f)
      (Model -> Int -> Wrapper RuleApplication -> Wrapper RuleApplication
forall a. FromText a => Model -> Int -> Wrapper a -> Wrapper a
reparse Model
model Int
line Wrapper RuleApplication
r)
  reparseAssumption :: Int -> Assumption -> Assumption
reparseAssumption Int
line (Wrapper RawAssumption
a, Wrapper RuleApplication
r) =
    (Model -> Int -> Wrapper RawAssumption -> Wrapper RawAssumption
forall a. FromText a => Model -> Int -> Wrapper a -> Wrapper a
reparse Model
model Int
line Wrapper RawAssumption
a, Model -> Int -> Wrapper RuleApplication -> Wrapper RuleApplication
forall a. FromText a => Model -> Int -> Wrapper a -> Wrapper a
reparse Model
model Int
line Wrapper RuleApplication
r)