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

This is the entry point of the Finch application. It reads the @?logic=@
and @?proof=@ URL query parameters to select the initial logic (propositional
or first-order) and to optionally restore a t'Proof' encoded in the URL,
then starts the Miso application with the appropriate t'Model'.
-}
module App.Entry where

import App.Model
import App.URLDecoder
import App.Update
import App.Views
import Data.Text qualified as T
import Fitch.Proof
import Miso
import Miso.FFI.QQ (js)
import Miso.Subscription.Util (createSub)
import Relude.Extra.Map
import Specification.FOL
import Specification.Prop

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

-- * Running the App

{- | Starts the Miso application for the given @window@ t'DOMRef' and
initial t'Model'.

Registers the browser event listeners (drag, keyboard, mouse,
touch and default events), mounts the application with the 'Setup' action,
and adds the 'PopState' URI subscription together with the keyboard
subscription 'onKeyDownSub'.
-}
startAppWrapper :: DOMRef -> Model -> IO ()
startAppWrapper :: JSVal -> Model -> IO ()
startAppWrapper JSVal
window Model
model =
  Events -> App Model Action -> IO ()
forall model action.
Eq model =>
Events -> App model action -> IO ()
startApp
    ( Events
dragEvents
        Events -> Events -> Events
forall a. Semigroup a => a -> a -> a
<> [Item Events] -> Events
forall l. IsList l => [Item l] -> l
fromList [(MisoString
"dblclick", Phase
BUBBLE)]
        Events -> Events -> Events
forall a. Semigroup a => a -> a -> a
<> Events
keyboardEvents
        Events -> Events -> Events
forall a. Semigroup a => a -> a -> a
<> Events
defaultEvents
        Events -> Events -> Events
forall a. Semigroup a => a -> a -> a
<> Events
mouseEvents
        Events -> Events -> Events
forall a. Semigroup a => a -> a -> a
<> Events
touchEvents
    )
    (App Model Action -> IO ()) -> App Model Action -> IO ()
forall a b. (a -> b) -> a -> b
$ (Model
-> (Action -> Effect ROOT Model Action)
-> (Model -> View Model Action)
-> App Model Action
forall model action parent.
model
-> (action -> Effect parent model action)
-> (model -> View model action)
-> Component parent model action
component Model
model Action -> Effect ROOT Model Action
updateModel Model -> View Model Action
viewModel)
      { mount = Just Setup
      , subs =
          [ uriSub PopState
          , onKeyDownSub window
          , resizeSub window
          ]
      }

{- | Application entry point.

1. Reads the current t'URI'.
2. Inspects the @?logic=@ query parameter:

   * @prop@ — initializes propositional logic via 'initialModelProp'.
   * @fol@ — initializes first-order logic via 'initialModelFOL'.
   * defaults to @fol@.
3. If a @?proof=@ query parameter is present, decodes it with
   'decodeFromUrl' and uses it as the initial t'Proof'; otherwise the
   default example proof for the selected logic is shown.
4. Then starts the Miso application using 'startAppWrapper'.
-}
runApp :: IO ()
runApp :: IO ()
runApp = IO () -> IO ()
forall a. IO a -> IO a
withJS (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  window <- MisoString -> IO JSVal
jsg MisoString
"window"
  uri <- getURI

  _sidebarToggle :: Maybe MisoString <- getSessionStorage "sidebarToggle"

  -- if storage could be found, take it, otherwise use a @media query
  -- to determine if sidebar should be initially open (on desktop) or closed (mobile).
  let sidebarToggle = case Maybe MisoString
_sidebarToggle of
        Just MisoString
"True" -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
        Just MisoString
"False" -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
        Maybe MisoString
_ -> Maybe Bool
forall a. Maybe a
Nothing

  onMobile :: Bool <-
    [js| return window.matchMedia("only screen and (max-width: 1200px)").matches; |]

  -- set the initial model by checking if ?logic= and ?proof= are specified.
  model <- case join (uriQueryString uri !? "logic") of
    Just ((MisoString -> MisoString -> Bool
forall a. Eq a => a -> a -> Bool
== Logic -> MisoString
forall b a. (Show a, IsString b) => a -> b
show Logic
Prop) -> Bool
True) ->
      (Maybe Bool -> Bool -> Model) -> IO (Maybe Bool -> Bool -> Model)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Maybe Bool -> Bool -> Model) -> IO (Maybe Bool -> Bool -> Model))
-> (Maybe Bool -> Bool -> Model)
-> IO (Maybe Bool -> Bool -> Model)
forall a b. (a -> b) -> a -> b
$
        URI -> Maybe Proof -> Maybe Bool -> Bool -> Model
initialModelProp URI
uri (Maybe Proof -> Maybe Bool -> Bool -> Model)
-> Maybe Proof -> Maybe Bool -> Bool -> Model
forall a b. (a -> b) -> a -> b
$
          MisoString -> Maybe Proof
decodeFromUrl (MisoString -> Maybe Proof)
-> (MisoString -> MisoString) -> MisoString -> Maybe Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MisoString -> MisoString
forall b a. (Show a, IsString b) => a -> b
show (MisoString -> Maybe Proof) -> Maybe MisoString -> Maybe Proof
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe (Maybe MisoString) -> Maybe MisoString
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (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")
    (Just ((MisoString -> MisoString -> Bool
forall a. Eq a => a -> a -> Bool
== Logic -> MisoString
forall b a. (Show a, IsString b) => a -> b
show Logic
FOL) -> Bool
True); Maybe MisoString
Nothing) ->
      (Maybe Bool -> Bool -> Model) -> IO (Maybe Bool -> Bool -> Model)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Maybe Bool -> Bool -> Model) -> IO (Maybe Bool -> Bool -> Model))
-> (Maybe Bool -> Bool -> Model)
-> IO (Maybe Bool -> Bool -> Model)
forall a b. (a -> b) -> a -> b
$
        URI -> Maybe Proof -> Maybe Bool -> Bool -> Model
initialModelFOL URI
uri (Maybe Proof -> Maybe Bool -> Bool -> Model)
-> Maybe Proof -> Maybe Bool -> Bool -> Model
forall a b. (a -> b) -> a -> b
$
          MisoString -> Maybe Proof
decodeFromUrl (MisoString -> Maybe Proof)
-> (MisoString -> MisoString) -> MisoString -> Maybe Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MisoString -> MisoString
forall b a. (Show a, IsString b) => a -> b
show
            (MisoString -> Maybe Proof) -> Maybe MisoString -> Maybe Proof
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe (Maybe MisoString) -> Maybe MisoString
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join
              (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")
  startAppWrapper window (model sidebarToggle onMobile)

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

-- * Subscriptions

{- | Subscription for the @onkeydown@ event.

Used for detecting presses of @(@ and @Enter@.

* On @Enter@ fires the `Blur` event,
* On @(@ inserts the closing parenthesis at the end of selection.
-}
onKeyDownSub :: DOMRef -> Sub Action
onKeyDownSub :: JSVal -> Sub Action
onKeyDownSub JSVal
window = IO Function -> (Function -> IO ()) -> Sub Action
forall a b action. IO a -> (a -> IO b) -> Sub action
createSub IO Function
acquire (JSVal -> MisoString -> Function -> IO ()
removeEventListener JSVal
window MisoString
"keydown")
 where
  acquire :: IO Function
acquire =
    JSVal -> MisoString -> (JSVal -> IO ()) -> IO Function
addEventListener JSVal
window MisoString
"keydown" ((JSVal -> IO ()) -> IO Function)
-> (JSVal -> IO ()) -> IO Function
forall a b. (a -> b) -> a -> b
$ \JSVal
evt -> do
      domRef <- MisoString -> IO JSVal
jsg MisoString
"document" IO JSVal -> MisoString -> MisoString -> IO JSVal
forall object args.
(ToObject object, ToArgs args) =>
object -> MisoString -> args -> IO JSVal
# MisoString
"querySelector" (MisoString -> IO JSVal) -> MisoString -> IO JSVal
forall a b. (a -> b) -> a -> b
$ (MisoString
".focused" :: MisoString)
      isNull domRef >>= \case
        Bool
True -> IO ()
forall (f :: * -> *). Applicative f => f ()
pass
        Bool
False -> do
          Just (keyCode :: 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
evt MisoString
"keyCode"
          Just (shiftKey :: Bool) <- castJSVal =<< getProperty evt "shiftKey"
          Just (start :: Int) <- castJSVal =<< getProperty domRef "selectionStart"
          Just (end :: Int) <- castJSVal =<< getProperty domRef "selectionEnd"

          -- when '(' is pressed, insert closing parenthesis as well
          when (keyCode == 57 && shiftKey && start < end) $ void $ do
            -- prevent call of the `input` event.
            eventPreventDefault evt
            -- split current value into parts, to insert the parentheses
            Just (value :: Text) <- castJSVal =<< getProperty domRef "value"
            let (firstPart, rest) = T.splitAt start value
                (secondPart, third) = T.splitAt (end - start) rest
                newTxt = [MisoString] -> MisoString
T.concat [Item [MisoString]
MisoString
firstPart, Item [MisoString]
MisoString
"(", Item [MisoString]
MisoString
secondPart, Item [MisoString]
MisoString
")", Item [MisoString]
MisoString
third]
            -- select all text, replace it with the new text, and adjust cursor position
            doc <- jsg "document"
            _ <- domRef # "select" $ ()
            -- NOTE: execCommand is deprecated, however its use is still recommended
            --       for inserting text to <input> while keeping the history intact.
            _ <- doc # "execCommand" $ ("insertText" :: String, False, newTxt)
            domRef # "setSelectionRange" $ (end + 2, end + 2, "none" :: String)

          -- when 'Enter' is pressed, call blur on the element, to lose focus
          when (keyCode == 13) $ void $ callFunction domRef "blur" ()

{- | Subscription for the resize event
<https://developer.mozilla.org/en-US/docs/Web/API/VisualViewport/resize_event>

Dynamically adjusts the '_onMobile' field of the t'Model'
-}
resizeSub :: DOMRef -> Sub Action
resizeSub :: JSVal -> Sub Action
resizeSub JSVal
window Sink Action
sink = IO Function -> (Function -> IO ()) -> Sub Action
forall a b action. IO a -> (a -> IO b) -> Sub action
createSub IO Function
acquire (JSVal -> MisoString -> Function -> IO ()
removeEventListener JSVal
window MisoString
"resize") Sink Action
sink
 where
  acquire :: IO Function
acquire = do
    JSVal -> MisoString -> (JSVal -> IO ()) -> IO Function
addEventListener JSVal
window MisoString
"resize" ((JSVal -> IO ()) -> IO Function)
-> (IO () -> JSVal -> IO ()) -> IO () -> IO Function
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO () -> JSVal -> IO ()
forall a b. a -> b -> a
const (IO () -> IO Function) -> IO () -> IO Function
forall a b. (a -> b) -> a -> b
$ do
      onMobile :: Bool <-
        [js| return window.matchMedia("only screen and (max-width: 1200px)").matches; |]
      sink (Resize onMobile)

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