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

This module defines the application t'Model'.
-}
module App.Model where

import Fitch.Proof
import Miso (DOMRef, MisoString, URI)
import Miso.Lens (Lens, lens)
import Miso.Lens.TH (makeLenses)
import Specification.Types

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

-- * Data Types

{- | Specifies the location where a t'Assumption', t'Derivation' or
t'Proof' has been dropped.
-}
data DropLocation where
  -- | Dropped __before__ a t'NodeAddr'.
  LineAddr :: NodeAddr -> DropLocation
  -- | Dropped in the bin.
  LocationBin :: DropLocation
  deriving (Int -> DropLocation -> ShowS
[DropLocation] -> ShowS
DropLocation -> String
(Int -> DropLocation -> ShowS)
-> (DropLocation -> String)
-> ([DropLocation] -> ShowS)
-> Show DropLocation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DropLocation -> ShowS
showsPrec :: Int -> DropLocation -> ShowS
$cshow :: DropLocation -> String
show :: DropLocation -> String
$cshowList :: [DropLocation] -> ShowS
showList :: [DropLocation] -> ShowS
Show, DropLocation -> DropLocation -> Bool
(DropLocation -> DropLocation -> Bool)
-> (DropLocation -> DropLocation -> Bool) -> Eq DropLocation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DropLocation -> DropLocation -> Bool
== :: DropLocation -> DropLocation -> Bool
$c/= :: DropLocation -> DropLocation -> Bool
/= :: DropLocation -> DropLocation -> Bool
Eq)

-- | Specifies whether a t'Assumption', t'Derivation' or a t'Proof' should be spawned.
data SpawnType where
  -- | Spawn a t'Assumption' or t'Derivation'
  SpawnLine :: SpawnType
  -- | Spawn a t'Proof'
  SpawnProof :: SpawnType
  deriving (Int -> SpawnType -> ShowS
[SpawnType] -> ShowS
SpawnType -> String
(Int -> SpawnType -> ShowS)
-> (SpawnType -> String)
-> ([SpawnType] -> ShowS)
-> Show SpawnType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SpawnType -> ShowS
showsPrec :: Int -> SpawnType -> ShowS
$cshow :: SpawnType -> String
show :: SpawnType -> String
$cshowList :: [SpawnType] -> ShowS
showList :: [SpawnType] -> ShowS
Show, SpawnType -> SpawnType -> Bool
(SpawnType -> SpawnType -> Bool)
-> (SpawnType -> SpawnType -> Bool) -> Eq SpawnType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SpawnType -> SpawnType -> Bool
== :: SpawnType -> SpawnType -> Bool
$c/= :: SpawnType -> SpawnType -> Bool
/= :: SpawnType -> SpawnType -> Bool
Eq)

-- | Enumeration of Logics that the app supports.
data Logic = Prop | FOL deriving (Int -> Logic -> ShowS
[Logic] -> ShowS
Logic -> String
(Int -> Logic -> ShowS)
-> (Logic -> String) -> ([Logic] -> ShowS) -> Show Logic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Logic -> ShowS
showsPrec :: Int -> Logic -> ShowS
$cshow :: Logic -> String
show :: Logic -> String
$cshowList :: [Logic] -> ShowS
showList :: [Logic] -> ShowS
Show, Logic -> Logic -> Bool
(Logic -> Logic -> Bool) -> (Logic -> Logic -> Bool) -> Eq Logic
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Logic -> Logic -> Bool
== :: Logic -> Logic -> Bool
$c/= :: Logic -> Logic -> Bool
/= :: Logic -> Logic -> Bool
Eq)

{- | Returns whether a given t'SpawnType' can be spawned __before__ a t'NodeAddr'.
For example, a t'Proof' can be spawned before a 'NAConclusion',
but not before a 'NAAssumption'.
-}
canSpawnBefore :: NodeAddr -> SpawnType -> Bool
canSpawnBefore :: NodeAddr -> SpawnType -> Bool
canSpawnBefore (NAProof Int
n NodeAddr
na) SpawnType
st = NodeAddr -> SpawnType -> Bool
canSpawnBefore NodeAddr
na SpawnType
st
canSpawnBefore (NALine{}; NAAssumption{}; NodeAddr
NAConclusion; NodeAddr
NAAfterConclusion) SpawnType
SpawnLine =
  Bool
True
canSpawnBefore (NALine{}; NodeAddr
NAConclusion) SpawnType
SpawnProof = Bool
True
canSpawnBefore NodeAddr
_ SpawnType
_ = Bool
False

-- | The actions of the application.
data Action where
  -- | Start MathJAX on the given t'DOMRef'
  InitMathJAX :: DOMRef -> Action
  {- | Open the tooltip with given @id@. Takes a t'Bool',
  that turns the action into a Noop, when 'False'.
  -}
  OpenTooltip :: MisoString -> Bool -> Action
  -- | Close the currently opened tooltip element with given @id@.
  CloseTooltip :: Action
  -- | Toggle the sidebar.
  ToggleSidebar :: Action
  -- | Update the t'Proof'.
  SetProof :: Proof -> Action
  {- | Pop a state of the history,
  see <https://developer.mozilla.org/en-US/docs/Web/API/History_API>.
  -}
  PopState :: URI -> Action
  -- | Setup directly called after application is mounted.
  Setup :: Action
  -- | Focus a t'Formula' or t'RuleApplication' @<input>@ field.
  Focus :: Either NodeAddr NodeAddr -> Action
  -- | Blur a t'Formula' or t'RuleApplication' @<input>@ field.
  Blur :: Either NodeAddr NodeAddr -> Action
  -- | Handle input text to @<input>@ field.
  Input :: MisoString -> DOMRef -> Action
  -- | Same as v'Input' but with more information.
  ProcessInput :: MisoString -> Int -> Int -> Either NodeAddr NodeAddr -> Action
  -- | Handle changes to @<input>@ field, triggers only, after field loses focus.
  Change :: Action
  -- | Drop currently dragged element into t'DropLocation'
  Drop :: DropLocation -> Action
  -- | Called when the drop-zone at a t'NodeAddr' is entered.
  DragEnter :: NodeAddr -> Action
  -- | Called when a drop-zone is left.
  DragLeave :: Action
  -- | Called when dragging of a t'Assumption', t'Derivation' or t'Proof' begins.
  DragStart :: Either NodeAddr ProofAddr -> Action
  -- | Called when dragging ends.
  DragEnd :: Action
  -- | Called when spawning starts with given t'SpawnType'.
  SpawnStart :: SpawnType -> Action
  -- Navigate forward in the history
  NavigateForward :: Action
  -- | Navigate backward in the history
  NavigateBackward :: Action
  {- | Action fired when the window gets resized
  <https://developer.mozilla.org/en-US/docs/Web/API/Window/resize_event>
  -}
  Resize :: Bool -> Action
  -- | No op.
  Nop :: Action

-- | Type for position information.
type Pos = Int

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

-- * Model

-- | The t'Model' of the application.
data Model = Model
  { Model -> Maybe (Either NodeAddr NodeAddr)
_focusedLine :: Maybe (Either NodeAddr NodeAddr)
  -- ^ Currently focused line.
  , Model -> [(Text, Proof)]
_exampleProofs :: [(Text, Proof)]
  -- ^ List of example t'Proof's.
  , Model -> Derivation
_emptyDerivation :: Derivation
  -- ^ Empty t'Derivation' as a dummy for inserting.
  , Model -> Proof
_proof :: Proof
  -- ^ Current t'Proof' of the application.
  , Model -> Bool
_sidebarToggle :: Bool
  -- ^ v'True' if the sidebar is open.
  , Model -> Maybe (Either NodeAddr ProofAddr)
_dragTarget :: Maybe (Either NodeAddr ProofAddr)
  -- ^ t'Assumption', t'Derivation' or t'Proof' that is currently being dragged.
  , Model -> Maybe NodeAddr
_lastDragged :: Maybe NodeAddr
  -- ^ last node that was dragged
  , Model -> Maybe SpawnType
_spawnType :: Maybe SpawnType
  -- ^ Type of element to be spawned.
  , Model -> Maybe NodeAddr
_currentHoverLine :: Maybe NodeAddr
  -- ^ Line before which the user currently hovers.
  , Model -> Bool
_dragging :: Bool
  -- ^ v'True' if the user is currently dragging an element.
  , Model -> [(Text, Text, Int)]
_operators :: [(Text, Text, Int)]
  {- ^ List of operators, consisting of (alias, operator, arity),
  where alias is an alternative notation for the operator.
  -}
  , Model -> [(Text, Text)]
_infixPreds :: [(Text, Text)]
  {- ^ List of infix predicates, consisting of (alias, predicate),
  where alias is an alternative notation for the predicate.
  -}
  , Model -> [(Text, Text)]
_quantifiers :: [(Text, Text)]
  {- ^ List of quantifiers, consisting of (alias, quantifier),
  where alias is an alternative notation for the quantifier.
  -}
  , Model -> Map Text (Int, Int)
_functionSymbols :: Map Text (Int, Pos)
  {- ^ Collected function symbols consisting of

  * name :: Text
  * arity :: Int
  * first occurence :: Pos
  -}
  , Model -> Map Text (Int, Int)
_predicateSymbols :: Map Text (Int, Pos)
  {- ^ Collected predicate symbols consisting of

  * name :: Text
  * arity :: Int
  * first occurence :: Pos
  -}
  , Model -> [(Text, RuleSpec)]
_rules :: [(Name, RuleSpec)]
  -- ^ A map that contains all rules, mapping their t'Name' to their t'RuleSpec'.
  , Model -> URI
_uri :: URI
  -- ^ t'URI' of the application.
  , Model -> Logic
_logic :: Logic
  -- ^ t'Logic' that the app currently uses.
  , Model -> Maybe Text
_currentTooltip :: Maybe MisoString
  -- ^ @id@ of the currently opened tooltip
  , Model -> Bool
_onMobile :: Bool
  -- ^ Responds to the current viewport, v'True' if viewport is small (on mobile)
  }
  deriving (Model -> Model -> Bool
(Model -> Model -> Bool) -> (Model -> Model -> Bool) -> Eq Model
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Model -> Model -> Bool
== :: Model -> Model -> Bool
$c/= :: Model -> Model -> Bool
/= :: Model -> Model -> Bool
Eq)

-- | Generates an initial t'Model' for pre-filling some fields (mostly with v'Nothing').
initialModel ::
  {- | Empty t'Derivation', used for inserting t'Assumption's, t'Derivation's and
  t'Proof's.
  -}
  Derivation ->
  -- | Initial t'Proof'.
  Proof ->
  -- | Example t'Proof's.
  [(Text, Proof)] ->
  -- | A list of operators (alias, operator, arity)
  [(Text, Text, Int)] ->
  -- | A list of quantifiers (alias, quantifier)
  [(Text, Text)] ->
  -- | A list of infix predicates (alias, predicate)
  [(Text, Text)] ->
  -- | The map of rules
  [(Name, RuleSpec)] ->
  -- | The current t'URI'
  URI ->
  -- | Logic that the app uses.
  Logic ->
  -- | Initial state of onMobile
  Maybe Bool ->
  -- | Possibly a previous sidebarToggle state.
  Bool ->
  -- | Initial t'Model' with sensible defaults
  Model
initialModel :: Derivation
-> Proof
-> [(Text, Proof)]
-> [(Text, Text, Int)]
-> [(Text, Text)]
-> [(Text, Text)]
-> [(Text, RuleSpec)]
-> URI
-> Logic
-> Maybe Bool
-> Bool
-> Model
initialModel
  Derivation
emptyD
  Proof
initialP
  [(Text, Proof)]
ps
  [(Text, Text, Int)]
operators
  [(Text, Text)]
infixPreds
  [(Text, Text)]
quantifiers
  [(Text, RuleSpec)]
rules
  URI
uri
  Logic
logic
  Maybe Bool
sidebarToggle
  Bool
onMobile =
    Model
      { _focusedLine :: Maybe (Either NodeAddr NodeAddr)
_focusedLine = Maybe (Either NodeAddr NodeAddr)
forall a. Maybe a
Nothing
      , _exampleProofs :: [(Text, Proof)]
_exampleProofs = [(Text, Proof)]
ps
      , _emptyDerivation :: Derivation
_emptyDerivation = Derivation
emptyD
      , _proof :: Proof
_proof = Proof
initialP
      , _sidebarToggle :: Bool
_sidebarToggle = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe (Bool -> Bool
not Bool
onMobile) Maybe Bool
sidebarToggle
      , _dragTarget :: Maybe (Either NodeAddr ProofAddr)
_dragTarget = Maybe (Either NodeAddr ProofAddr)
forall a. Maybe a
Nothing
      , _lastDragged :: Maybe NodeAddr
_lastDragged = Maybe NodeAddr
forall a. Maybe a
Nothing
      , _spawnType :: Maybe SpawnType
_spawnType = Maybe SpawnType
forall a. Maybe a
Nothing
      , _currentHoverLine :: Maybe NodeAddr
_currentHoverLine = Maybe NodeAddr
forall a. Maybe a
Nothing
      , _dragging :: Bool
_dragging = Bool
False
      , _operators :: [(Text, Text, Int)]
_operators = [(Text, Text, Int)]
operators
      , _infixPreds :: [(Text, Text)]
_infixPreds = [(Text, Text)]
infixPreds
      , _quantifiers :: [(Text, Text)]
_quantifiers = [(Text, Text)]
quantifiers
      , _functionSymbols :: Map Text (Int, Int)
_functionSymbols = Map Text (Int, Int)
forall a. Monoid a => a
mempty
      , _predicateSymbols :: Map Text (Int, Int)
_predicateSymbols = Map Text (Int, Int)
forall a. Monoid a => a
mempty
      , _rules :: [(Text, RuleSpec)]
_rules = [(Text, RuleSpec)]
rules
      , _uri :: URI
_uri = URI
uri
      , _logic :: Logic
_logic = Logic
logic
      , _currentTooltip :: Maybe Text
_currentTooltip = Maybe Text
forall a. Maybe a
Nothing
      , _onMobile :: Bool
_onMobile = Bool
onMobile
      }

-- * Lenses

{- $makeLensesParagraph
Generated using 'makeLenses'.
-}

$(makeLenses ''Model)