{- |
Module      : App.Views
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 Miso t'View's of the application.
-}
module App.Views where

------------------------------------------------------------------------------------------
import App.Model
import Data.List qualified as L
import Data.Text qualified as T
import Fitch.Proof
import Miso (
  MisoString,
  Phase (BUBBLE),
  URI (..),
  View,
  defaultOptions,
  ms,
  onCreatedWith,
  onWithOptions,
  optionalAttrs,
  optionalChildren,
  prettyURI,
  preventDefault,
  stopPropagation,
  text,
  textProp,
  textRaw,
  valueDecoder,
 )
import Miso.Html.Element qualified as H
import Miso.Html.Event qualified as HE
import Miso.Html.Property qualified as HP
import Miso.Lens ((^.))
import Miso.Property (textProp)
import Miso.Router (URI (..), prettyURI)
import Relude.Extra (toPairs)
import Relude.Unsafe (fromJust)
import Specification.Types
import Util (interleave)

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

-- * Views

{- | Takes a t'Model' and returns the corresponding t'View'
containing a sidebar, the proof workspace and a header.
-}
viewModel :: Model -> View Model Action
viewModel :: Model -> View Model Action
viewModel Model
model =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"app-container"
    , -- This is needed to fix a bug, where on dragStart, we instantly get a random
      -- dragEnter fired in the middle of the screen.
      -- Possibly this bug only occurs on wayland.
      Action -> Attribute Action
forall action. action -> Attribute action
HE.onDragEnter Action
DragLeave
    ]
    [ Model -> View Model Action
viewHeader Model
model
    , [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
        [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"content-container"]
        [ Model -> View Model Action
viewSidebar Model
model
        , Model -> View Model Action
viewProof Model
model
        ]
    ]

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

-- ** Header

-- | Returns the header of the application.
viewHeader :: Model -> View Model Action
viewHeader :: Model -> View Model Action
viewHeader Model
model =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.header_
    [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"header"]
    [ Model -> View Model Action
viewLogoHeader Model
model
    , Item [View Model Action]
View Model Action
viewProofActionsHeader
    , Model -> View Model Action
viewHeaderRight Model
model
    ]

-- | Shows the logo in the 'viewHeader', together with a title and navigation buttons
viewLogoHeader :: Model -> View Model Action
viewLogoHeader :: Model -> View Model Action
viewLogoHeader Model
model =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"logo-header"]
    [ Item [View Model Action]
View Model Action
viewMenuButton
    , [Attribute Action] -> View Model Action
forall action model. [Attribute action] -> View model action
H.img_ [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.src_ MisoString
"icons/favicon.svg"]
    , [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.h1_ [] [Item [View Model Action]
View Model Action
"Finch"]
    ]

viewHeaderRight :: Model -> View Model Action
viewHeaderRight :: Model -> View Model Action
viewHeaderRight Model
model =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"header-right-container"]
    [ Model -> View Model Action
viewErrorNumber Model
model
    , Item [View Model Action]
View Model Action
viewNavigationButtons
    ]

viewErrorNumber :: Model -> View Model Action
viewErrorNumber :: Model -> View Model Action
viewErrorNumber Model
model =
  ([Attribute Action] -> [View Model Action] -> View Model Action)
-> [Attribute Action]
-> [View Model Action]
-> Bool
-> [View Model Action]
-> View Model Action
forall action model.
([Attribute action] -> [View model action] -> View model action)
-> [Attribute action]
-> [View model action]
-> Bool
-> [View model action]
-> View model action
optionalChildren
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-container"
    , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOver (MisoString -> Bool -> Action
OpenTooltip MisoString
"error-number" Bool
True)
    , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOut Action
CloseTooltip
    ]
    [ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.p_
        [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"error-number"
        , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-anchor"
        , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_
            [(MisoString
"success", Int
errors Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0), (MisoString
"failure", Int
errors Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0)]
        ]
        [ Item [View Model Action]
View Model Action
icon
        , MisoString -> View Model Action
forall model action. MisoString -> View model action
text (MisoString -> View Model Action)
-> MisoString -> View Model Action
forall a b. (a -> b) -> a -> b
$
            if Model
model Model -> Lens Model Bool -> Bool
forall record field. record -> Lens record field -> field
^. Lens Model Bool
onMobile
              then Int -> MisoString
forall b a. (Show a, IsString b) => a -> b
show Int
errors
              else MisoString
errorText
        ]
    ]
    (Model
model Model -> Lens Model Bool -> Bool
forall record field. record -> Lens record field -> field
^. Lens Model Bool
onMobile)
    [ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.p_
        [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ MisoString
"error-number", MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-bottom", MisoString -> MisoString -> Attribute Action
forall action. MisoString -> MisoString -> Attribute action
textProp MisoString
"popover" MisoString
"hint"]
        [MisoString -> View Model Action
forall model action. MisoString -> View model action
text MisoString
errorText]
    ]
 where
  icon :: View Model Action
icon =
    if Int
errors Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
      then MisoString -> View Model Action
viewMaterialIcon MisoString
"check_circle"
      else MisoString -> View Model Action
viewMaterialIcon MisoString
"warning"
  errors :: Int
errors = Proof -> Int
proofErrors (Model
model Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof)
  errorText :: MisoString
errorText = case Int
errors of
    Int
0 -> MisoString
"No errors found"
    Int
1 -> MisoString
"1 error found"
    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
" errors found"

-- | Adds navigation @<button>@s for accessing the browsers history API.
viewNavigationButtons :: View Model Action
viewNavigationButtons :: View Model Action
viewNavigationButtons =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"navigation-container"]
    [ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.button_
        [ Action -> Attribute Action
forall action. action -> Attribute action
HE.onClick Action
NavigateBackward
        , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"navigation-button"
        , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ MisoString
"back-button"
        ]
        [MisoString -> View Model Action
viewMaterialIcon MisoString
"arrow_left_alt"]
    , [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.button_
        [ Action -> Attribute Action
forall action. action -> Attribute action
HE.onClick Action
NavigateForward
        , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"navigation-button"
        , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ MisoString
"forward-button"
        ]
        [MisoString -> View Model Action
viewMaterialIcon MisoString
"arrow_right_alt"]
    ]

{- | For use in 'viewHeader',
returns buttons for spawning t'Assumption', t'Derivation', t'Proof' or a trash can.
-}
viewProofActionsHeader :: View Model Action
viewProofActionsHeader :: View Model Action
viewProofActionsHeader =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"proof-actions-header"]
    [ SpawnType -> MisoString -> MisoString -> View Model Action
viewSpawnNode SpawnType
SpawnLine MisoString
"Drag me into a proof to insert a new line" MisoString
"add"
    , Item [View Model Action]
View Model Action
viewBin
    , SpawnType -> MisoString -> MisoString -> View Model Action
viewSpawnNode SpawnType
SpawnProof MisoString
"Drag me into a proof to insert a new subproof" MisoString
"variable_add"
    ]

{- | For use in 'viewProofActionsHeader',
returns a trash can, where elements can be deleted.
-}
viewBin :: View Model Action
viewBin :: View Model Action
viewBin =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [ Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragOverWithOptions Options
preventDefault Action
Nop
    , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragLeaveWithOptions Options
preventDefault Action
Nop
    , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-container"
    , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-anchor"
    , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOver (MisoString -> Bool -> Action
OpenTooltip MisoString
"bin" Bool
True)
    , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOut Action
CloseTooltip
    , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDropWithOptions Options
defaultOptions (DropLocation -> Action
Drop DropLocation
LocationBin)
    , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"bin"
    ]
    [ MisoString -> View Model Action
viewMaterialIcon MisoString
"delete"
    , [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.p_
        [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-bottom"
        , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ MisoString
"bin"
        , MisoString -> MisoString -> Attribute Action
forall action. MisoString -> MisoString -> Attribute action
textProp MisoString
"popover" MisoString
"hint"
        , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False
        ]
        [MisoString -> View Model Action
forall model action. MisoString -> View model action
text MisoString
"Drag lines or subproofs here to delete them."]
    ]

{- | For use in 'viewProofActionsHeader',
returns a button for spawning a t'Assumption', t'Derivation' or t'Proof'.
-}
viewSpawnNode ::
  -- | Type of node to be spawned
  SpawnType ->
  -- | Tooltip of the button
  MisoString ->
  -- | The buttons icon.
  MisoString ->
  View Model Action
viewSpawnNode :: SpawnType -> MisoString -> MisoString -> View Model Action
viewSpawnNode SpawnType
tp MisoString
title MisoString
icon =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"spawn-button"
    , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"draggable"
    , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-container"
    , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-anchor"
    , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
True
    , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOver (MisoString -> Bool -> Action
OpenTooltip ([Char] -> MisoString
forall str. ToMisoString str => str -> MisoString
ms ([Char] -> MisoString) -> [Char] -> MisoString
forall a b. (a -> b) -> a -> b
$ SpawnType -> [Char]
forall b a. (Show a, IsString b) => a -> b
show SpawnType
tp) Bool
True)
    , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOut Action
CloseTooltip
    , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragStartWithOptions Options
stopPropagation (Action -> Attribute Action) -> Action -> Attribute Action
forall a b. (a -> b) -> a -> b
$ SpawnType -> Action
SpawnStart SpawnType
tp
    , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragEndWithOptions Options
defaultOptions Action
DragEnd
    ]
    [ MisoString -> View Model Action
viewMaterialIcon MisoString
icon
    , [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.p_
        [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-bottom"
        , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ (SpawnType -> MisoString
forall b a. (Show a, IsString b) => a -> b
show SpawnType
tp)
        , MisoString -> MisoString -> Attribute Action
forall action. MisoString -> MisoString -> Attribute action
textProp MisoString
"popover" MisoString
"hint"
        , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False
        ]
        [MisoString -> View Model Action
forall model action. MisoString -> View model action
text MisoString
title]
    ]

{- | For use in 'viewHeader'
returns a @<button>@ that opens and closes the sidebar.
-}
viewMenuButton :: View Model Action
viewMenuButton :: View Model Action
viewMenuButton =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.button_
    [Action -> Attribute Action
forall action. action -> Attribute action
HE.onClick Action
ToggleSidebar, MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"menu-button"]
    [MisoString -> View Model Action
viewMaterialIcon MisoString
"menu"]

{- | For use in 'viewHeader',
returns a @<button>@ for starting a new t'Proof'.
-}
viewNewProofButton :: Model -> View Model Action
viewNewProofButton :: Model -> View Model Action
viewNewProofButton Model
model =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.button_
    [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"new-proof-button"
    , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"sidebar-element"
    , Action -> Attribute Action
forall action. action -> Attribute action
HE.onClick (Proof -> Action
SetProof (Proof -> Action) -> Proof -> Action
forall a b. (a -> b) -> a -> b
$ [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [] [] (Model
model Model -> Lens Model Derivation -> Derivation
forall record field. record -> Lens record field -> field
^. Lens Model Derivation
emptyDerivation))
    ]
    [MisoString -> View Model Action
forall model action. MisoString -> View model action
text MisoString
"Start New Proof"]

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

-- ** Sidebar

-- | Returns the sidebar of the application.
viewSidebar :: Model -> View Model Action
viewSidebar :: Model -> View Model Action
viewSidebar Model
model =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"sidebar"
    , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_
        [ (MisoString
"sidebar-closed", Bool -> Bool
not (Model
model Model -> Lens Model Bool -> Bool
forall record field. record -> Lens record field -> field
^. Lens Model Bool
sidebarToggle))
        ]
    ]
    ([View Model Action] -> View Model Action)
-> [View Model Action] -> View Model Action
forall a b. (a -> b) -> a -> b
$ OneItem [View Model Action] -> [View Model Action]
forall x. One x => OneItem x -> x
one
    (OneItem [View Model Action] -> [View Model Action])
-> OneItem [View Model Action] -> [View Model Action]
forall a b. (a -> b) -> a -> b
$ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
      [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"sidebar-container"
      ]
      [ Model -> View Model Action
viewNewProofButton Model
model
      , Item [View Model Action]
View Model Action
viewUsage
      , Model -> View Model Action
viewGrammar Model
model
      , Model -> View Model Action
viewRules Model
model
      , Model -> View Model Action
viewExamples Model
model
      , Model -> View Model Action
viewLogics Model
model
      , Model -> View Model Action
viewSource Model
model
      ]

-- | Wrapper for creating @<details>@ elements in the sidebar.
viewDetails ::
  -- | Text of the <details> summary.
  MisoString ->
  -- | Icon of the <details> summary.
  MisoString ->
  -- | Content of the <details> element.
  View Model Action ->
  View Model Action
viewDetails :: MisoString -> MisoString -> View Model Action -> View Model Action
viewDetails MisoString
txt MisoString
icon View Model Action
content =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.details_
    [Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.open_ Bool
True, MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"sidebar-element"]
    [ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.summary_
        [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"sidebar-header"]
        [ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_ [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"icon-text"] [MisoString -> View Model Action
viewMaterialIcon MisoString
icon, [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.b_ [] [MisoString -> View Model Action
forall model action. MisoString -> View model action
text MisoString
txt]]
        , [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_ [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"summary-arrow"] [MisoString -> View Model Action
viewMaterialIcon MisoString
"keyboard_arrow_down"]
        ]
    , Item [View Model Action]
View Model Action
content
    ]

{- | For use in 'viewSidebar',
returns usage instructions.
-}
viewUsage :: View Model Action
viewUsage :: View Model Action
viewUsage =
  MisoString -> MisoString -> View Model Action -> View Model Action
viewDetails
    MisoString
"Usage Info"
    MisoString
"info"
    ( [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.ul_
        [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"column-sidebar-content", MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"usage-info"]
        [ MisoString -> MisoString -> View Model Action
mkLi MisoString
"Drag" MisoString
" the buttons at the top of the screen to insert lines and subproofs."
        , MisoString -> MisoString -> View Model Action
mkLi MisoString
"Drag" MisoString
" lines and subproofs to modify the proof."
        , MisoString -> MisoString -> View Model Action
mkLi MisoString
"Drag" MisoString
" lines and subproofs to the trash can at the top to delete them."
        , MisoString -> MisoString -> View Model Action
mkLi MisoString
"Click" MisoString
" lines to edit their contents."
        , MisoString -> MisoString -> View Model Action
mkLi MisoString
"Check" MisoString
" below to see how to write the symbols and how the rules are defined."
        , MisoString -> MisoString -> View Model Action
mkLi MisoString
"Share" MisoString
" proofs by copying the URL."
        , MisoString -> MisoString -> View Model Action
mkLi MisoString
"On mobile" MisoString
" long press to move subproofs."
        ]
    )
 where
  mkLi :: MisoString -> MisoString -> View Model Action
  mkLi :: MisoString -> MisoString -> View Model Action
mkLi MisoString
emph MisoString
content =
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.li_
      []
      [MisoString -> View Model Action
viewMaterialIcon MisoString
"keyboard_arrow_right", [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.p_ [] [[Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.b_ [] [MisoString -> View Model Action
forall model action. MisoString -> View model action
text MisoString
emph], MisoString -> View Model Action
forall model action. MisoString -> View model action
text MisoString
content]]

{- | For use in 'viewSidebar',
returns a list of symbols that can be used, and on hover shows their aliases.
-}
viewGrammar :: Model -> View Model Action
viewGrammar :: Model -> View Model Action
viewGrammar Model
model =
  MisoString -> MisoString -> View Model Action -> View Model Action
viewDetails
    MisoString
"Symbols"
    MisoString
"function"
    ( [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
        [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"row-sidebar-content"]
        ( ((MisoString, MisoString) -> View Model Action)
-> [(MisoString, MisoString)] -> [View Model Action]
forall a b. (a -> b) -> [a] -> [b]
map
            (MisoString, MisoString) -> View Model Action
viewSingleSymbol
            ( ((MisoString, MisoString, Int) -> (MisoString, MisoString))
-> [(MisoString, MisoString, Int)] -> [(MisoString, MisoString)]
forall a b. (a -> b) -> [a] -> [b]
map (\(MisoString
a, MisoString
b, Int
_) -> (MisoString
a, MisoString
b)) (Model
model Model
-> Lens Model [(MisoString, MisoString, Int)]
-> [(MisoString, MisoString, Int)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString, Int)]
operators)
                [(MisoString, MisoString)]
-> [(MisoString, MisoString)] -> [(MisoString, MisoString)]
forall a. Semigroup a => a -> a -> a
<> Model
model Model
-> Lens Model [(MisoString, MisoString)]
-> [(MisoString, MisoString)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString)]
quantifiers
                [(MisoString, MisoString)]
-> [(MisoString, MisoString)] -> [(MisoString, MisoString)]
forall a. Semigroup a => a -> a -> a
<> Model
model Model
-> Lens Model [(MisoString, MisoString)]
-> [(MisoString, MisoString)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, MisoString)]
infixPreds
            )
        )
    )
 where
  viewSingleSymbol :: (Name, Name) -> View Model Action
  viewSingleSymbol :: (MisoString, MisoString) -> View Model Action
viewSingleSymbol (MisoString
alias, MisoString
symbol) =
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
      [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-container"]
      [ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.button_
          [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-anchor"
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"symbol-button"
          , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOver (MisoString -> Bool -> Action
OpenTooltip MisoString
id Bool
True)
          , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOut Action
CloseTooltip
          ]
          [MisoString -> View Model Action
forall model action. MisoString -> View model action
text (MisoString -> View Model Action)
-> MisoString -> View Model Action
forall a b. (a -> b) -> a -> b
$ MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
symbol]
      , [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.p_
          [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-right"
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ MisoString
id
          , MisoString -> MisoString -> Attribute Action
forall action. MisoString -> MisoString -> Attribute action
textProp MisoString
"popover" MisoString
"hint"
          , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False
          ]
          [MisoString -> View Model Action
forall model action. MisoString -> View model action
text (MisoString -> View Model Action)
-> MisoString -> View Model Action
forall a b. (a -> b) -> a -> b
$ if MisoString
alias MisoString -> MisoString -> Bool
forall a. Eq a => a -> a -> Bool
== MisoString
"" then MisoString
"No alias." else MisoString
"Alias: " MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
alias]
      ]
   where
    id :: MisoString
id = MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms (MisoString -> MisoString) -> MisoString -> MisoString
forall a b. (a -> b) -> a -> b
$ if MisoString
alias MisoString -> MisoString -> Bool
forall a. Eq a => a -> a -> Bool
== MisoString
"" then MisoString
symbol else MisoString
alias

{- | For use in 'viewSidebar',
returns a list of the logic's rules, on hover shows the rule definition.
-}
viewRules :: Model -> View Model Action
viewRules :: Model -> View Model Action
viewRules Model
model =
  MisoString -> MisoString -> View Model Action -> View Model Action
viewDetails
    MisoString
"Rules"
    MisoString
"rule"
    ( [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
        [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"row-sidebar-content"]
        (((MisoString, RuleSpec) -> View Model Action)
-> [(MisoString, RuleSpec)] -> [View Model Action]
forall a b. (a -> b) -> [a] -> [b]
map (MisoString, RuleSpec) -> View Model Action
viewSingleRule ([(MisoString, RuleSpec)] -> [(MisoString, RuleSpec)]
forall t a b. (IsList t, Item t ~ (a, b)) => t -> [(a, b)]
toPairs ([(MisoString, RuleSpec)] -> [(MisoString, RuleSpec)])
-> [(MisoString, RuleSpec)] -> [(MisoString, RuleSpec)]
forall a b. (a -> b) -> a -> b
$ Model
model Model
-> Lens Model [(MisoString, RuleSpec)] -> [(MisoString, RuleSpec)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, RuleSpec)]
rules))
    )
 where
  viewSingleRule :: (Name, RuleSpec) -> View Model Action
  viewSingleRule :: (MisoString, RuleSpec) -> View Model Action
viewSingleRule (MisoString
name, RuleSpec
rs) =
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
      [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-container"]
      [ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.button_
          [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-anchor"
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"rule-button"
          , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOver (MisoString -> Bool -> Action
OpenTooltip (MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
name) Bool
True)
          , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOut Action
CloseTooltip
          ]
          [MisoString -> View Model Action
forall model action. MisoString -> View model action
text (MisoString -> View Model Action)
-> MisoString -> View Model Action
forall a b. (a -> b) -> a -> b
$ MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
name]
      , [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.p_
          [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-right"
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ (MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
name)
          , (DOMRef -> Action) -> Attribute Action
forall action. (DOMRef -> action) -> Attribute action
onCreatedWith DOMRef -> Action
InitMathJAX
          , MisoString -> MisoString -> Attribute Action
forall action. MisoString -> MisoString -> Attribute action
textProp MisoString
"popover" MisoString
"hint"
          , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False
          ]
          [MisoString -> Item [View Model Action]
MisoString -> View Model Action
forall model action. MisoString -> View model action
text (MisoString -> Item [View Model Action])
-> (MisoString -> MisoString)
-> MisoString
-> Item [View Model Action]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms (MisoString -> Item [View Model Action])
-> MisoString -> Item [View Model Action]
forall a b. (a -> b) -> a -> b
$ MisoString
"\\[(\\mathrm{" MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> MisoString
name MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> MisoString
"})" MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> RuleSpec -> MisoString
ruleSpecTex RuleSpec
rs MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> MisoString
"\\]"]
      ]

{- | For use in 'viewSidebar', returns a list of example t'Proof's,
on hover shows the t'Assumption's and conclusion of the t'Proof'.
-}
viewExamples :: Model -> View Model Action
viewExamples :: Model -> View Model Action
viewExamples Model
model =
  MisoString -> MisoString -> View Model Action -> View Model Action
viewDetails
    MisoString
"Examples"
    MisoString
"view_list"
    ([Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_ [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"column-sidebar-content"] (((MisoString, Proof) -> View Model Action)
-> [(MisoString, Proof)] -> [View Model Action]
forall a b. (a -> b) -> [a] -> [b]
map (MisoString, Proof) -> View Model Action
mkExample (Model
model Model -> Lens Model [(MisoString, Proof)] -> [(MisoString, Proof)]
forall record field. record -> Lens record field -> field
^. Lens Model [(MisoString, Proof)]
exampleProofs)))
 where
  mkExample :: (Text, Proof) -> View Model Action
  mkExample :: (MisoString, Proof) -> View Model Action
mkExample (MisoString
name, Proof
p) =
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
      [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-container"]
      [ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.button_
          [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-anchor"
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"example-button"
          , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOver (MisoString -> Bool -> Action
OpenTooltip (MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
name) Bool
True)
          , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOut Action
CloseTooltip
          , Action -> Attribute Action
forall action. action -> Attribute action
HE.onClick (Proof -> Action
SetProof Proof
p)
          ]
          [MisoString -> View Model Action
forall model action. MisoString -> View model action
text (MisoString -> View Model Action)
-> MisoString -> View Model Action
forall a b. (a -> b) -> a -> b
$ MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
name]
      , [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.p_
          [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-right"
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ (MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
name)
          , (DOMRef -> Action) -> Attribute Action
forall action. (DOMRef -> action) -> Attribute action
onCreatedWith DOMRef -> Action
InitMathJAX
          , MisoString -> MisoString -> Attribute Action
forall action. MisoString -> MisoString -> Attribute action
textProp MisoString
"popover" MisoString
"hint"
          , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False
          ]
          [MisoString -> Item [View Model Action]
MisoString -> View Model Action
forall model action. MisoString -> View model action
text (MisoString -> Item [View Model Action])
-> (MisoString -> MisoString)
-> MisoString
-> Item [View Model Action]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms (MisoString -> Item [View Model Action])
-> MisoString -> Item [View Model Action]
forall a b. (a -> b) -> a -> b
$ Proof -> MisoString
proofPreviewTex Proof
p]
      ]

{- | For use in 'viewSidebar', returns a list of buttons
that enable the user to change the underlying logic of the proof checker.
-}
viewLogics :: Model -> View Model Action
viewLogics :: Model -> View Model Action
viewLogics Model
model =
  MisoString -> MisoString -> View Model Action -> View Model Action
viewDetails
    MisoString
"Logics"
    MisoString
"schema"
    ( [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
        [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"column-sidebar-content"]
        (((MisoString, Logic) -> View Model Action)
-> [(MisoString, Logic)] -> [View Model Action]
forall a b. (a -> b) -> [a] -> [b]
map (MisoString, Logic) -> View Model Action
mkLogic [(MisoString
"First-order logic", Logic
FOL), (MisoString
"Propositional Logic", Logic
Prop)])
    )
 where
  mkLogic :: (MisoString, Logic) -> View Model Action
  mkLogic :: (MisoString, Logic) -> View Model Action
mkLogic (MisoString
description, Logic
l) =
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.a_
      [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"example-button"
      , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.target_ MisoString
"_blank"
      , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_ [(MisoString
"disabled", (Model
model Model -> Lens Model Logic -> Logic
forall record field. record -> Lens record field -> field
^. Lens Model Logic
logic) Logic -> Logic -> Bool
forall a. Eq a => a -> a -> Bool
== Logic
l)]
      , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.href_ (MisoString -> Attribute Action) -> MisoString -> Attribute Action
forall a b. (a -> b) -> a -> b
$
          URI -> MisoString
prettyURI (URI -> MisoString) -> URI -> MisoString
forall a b. (a -> b) -> a -> b
$
            URI
              { uriPath :: MisoString
uriPath = URI -> MisoString
uriPath (Model
model Model -> Lens Model URI -> URI
forall record field. record -> Lens record field -> field
^. Lens Model URI
uri)
              , uriFragment :: MisoString
uriFragment = MisoString
""
              , uriQueryString :: Map MisoString (Maybe MisoString)
uriQueryString = 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)
              }
      ]
      [MisoString -> View Model Action
forall model action. MisoString -> View model action
text MisoString
description]

{- | For use in 'viewSidebar', contains a link to the repository
and the documentation.
-}
viewSource :: Model -> View Model Action
viewSource :: Model -> View Model Action
viewSource Model
model =
  MisoString -> MisoString -> View Model Action -> View Model Action
viewDetails
    MisoString
"Source"
    MisoString
"code"
    ( [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
        [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"row-sidebar-content"]
        [ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.a_
            [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"source-button"
            , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.href_ MisoString
"https://github.com/Reijix/finch"
            , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.target_ MisoString
"_blank"
            ]
            [[Attribute Action] -> View Model Action
forall action model. [Attribute action] -> View model action
H.img_ [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.src_ MisoString
"icons/github.svg"], MisoString -> View Model Action
forall model action. MisoString -> View model action
text MisoString
" Repository"]
        , [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.a_
            [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"source-button"
            , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.target_ MisoString
"_blank"
            , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.href_
                ( URI -> MisoString
prettyURI (URI -> MisoString) -> URI -> MisoString
forall a b. (a -> b) -> a -> b
$
                    URI
                      { uriPath :: MisoString
uriPath = URI -> MisoString
uriPath (Model
model Model -> Lens Model URI -> URI
forall record field. record -> Lens record field -> field
^. Lens Model URI
uri) MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> MisoString
"docs"
                      , uriFragment :: MisoString
uriFragment = MisoString
""
                      , uriQueryString :: Map MisoString (Maybe MisoString)
uriQueryString = Map MisoString (Maybe MisoString)
forall a. Monoid a => a
mempty
                      }
                )
            ]
            [[Attribute Action] -> View Model Action
forall action model. [Attribute action] -> View model action
H.img_ [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.src_ MisoString
"icons/haskell.svg"], Item [View Model Action]
View Model Action
"Documentation"]
        ]
    )

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

-- ** Proof

{- | Shows the proof workspace of the application, containing a list of line numbers,
a list of formula inputs and a list of rule inputs.
-}
viewProof :: Model -> View Model Action
viewProof :: Model -> View Model Action
viewProof Model
model =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"proof-container-border"
    ]
    [ [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
        [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"proof-container"
        , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_
            [(MisoString
"dragging", Model
model Model -> Lens Model Bool -> Bool
forall record field. record -> Lens record field -> field
^. Lens Model Bool
dragging)]
        ]
        [Model -> View Model Action
viewLineNos Model
model, Item [View Model Action]
View Model Action
proofView, Model -> View Model Action
viewRuleApplications Model
model]
    ]
 where
  proofView :: View Model Action
proofView =
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
      [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"formulae-container"]
      [(ProofAddr -> ProofAddr)
-> (NodeAddr -> NodeAddr) -> Proof -> View Model Action
_viewProof ProofAddr -> ProofAddr
forall a. a -> a
id NodeAddr -> NodeAddr
forall a. a -> a
id (Model
model Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof)]
  _viewProof ::
    (ProofAddr -> ProofAddr) -> (NodeAddr -> NodeAddr) -> Proof -> View Model Action
  _viewProof :: (ProofAddr -> ProofAddr)
-> (NodeAddr -> NodeAddr) -> Proof -> View Model Action
_viewProof ProofAddr -> ProofAddr
pa NodeAddr -> NodeAddr
na (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
d) =
    ([Attribute Action] -> [View Model Action] -> View Model Action)
-> [Attribute Action]
-> Bool
-> [Attribute Action]
-> [View Model Action]
-> View Model Action
forall action model.
([Attribute action] -> [View model action] -> View model action)
-> [Attribute action]
-> Bool
-> [Attribute action]
-> [View model action]
-> View model action
optionalAttrs
      [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
      [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"subproof"
      , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ (MisoString -> Attribute Action) -> MisoString -> Attribute Action
forall a b. (a -> b) -> a -> b
$ MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms (MisoString -> MisoString) -> MisoString -> MisoString
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> MisoString -> MisoString
T.filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
' ') (ProofAddr -> MisoString
forall b a. (Show a, IsString b) => a -> b
show (ProofAddr -> MisoString) -> ProofAddr -> MisoString
forall a b. (a -> b) -> a -> b
$ ProofAddr -> ProofAddr
pa ProofAddr
PAProof)
      ]
      (ProofAddr -> ProofAddr
pa ProofAddr
PAProof ProofAddr -> ProofAddr -> Bool
forall a. Eq a => a -> a -> Bool
/= ProofAddr
PAProof)
      [ Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
True
      , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_
          [ (MisoString
"draggable", Bool -> Bool
not (Model
model Model -> Lens Model Bool -> Bool
forall record field. record -> Lens record field -> field
^. Lens Model Bool
dragging))
          , (MisoString
"drag-target", Either NodeAddr ProofAddr -> Maybe (Either NodeAddr ProofAddr)
forall a. a -> Maybe a
Just (ProofAddr -> Either NodeAddr ProofAddr
forall a b. b -> Either a b
Right (ProofAddr -> ProofAddr
pa ProofAddr
PAProof)) Maybe (Either NodeAddr ProofAddr)
-> Maybe (Either NodeAddr ProofAddr) -> Bool
forall a. Eq a => a -> a -> Bool
== Model
model Model
-> Lens Model (Maybe (Either NodeAddr ProofAddr))
-> Maybe (Either NodeAddr ProofAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr ProofAddr))
dragTarget)
          ]
      , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragStartWithOptions Options
stopPropagation (Action -> Item [Attribute Action])
-> (ProofAddr -> Action) -> ProofAddr -> Item [Attribute Action]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either NodeAddr ProofAddr -> Action
DragStart (Either NodeAddr ProofAddr -> Action)
-> (ProofAddr -> Either NodeAddr ProofAddr) -> ProofAddr -> Action
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofAddr -> Either NodeAddr ProofAddr
forall a b. b -> Either a b
Right (ProofAddr -> Item [Attribute Action])
-> ProofAddr -> Item [Attribute Action]
forall a b. (a -> b) -> a -> b
$ ProofAddr -> ProofAddr
pa ProofAddr
PAProof
      , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragEndWithOptions Options
defaultOptions Action
DragEnd
      ]
      ( Model
-> Maybe MisoString
-> Maybe NodeAddr
-> (Int -> NodeAddr)
-> [View Model Action]
-> [View Model Action]
interleaveWithDropZones
          Model
model
          (MisoString -> Maybe MisoString
forall a. a -> Maybe a
Just MisoString
"last-assumption")
          Maybe NodeAddr
forall a. Maybe a
Nothing
          (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr) -> (Int -> NodeAddr) -> Int -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr
NAAssumption)
          [View Model Action]
viewAssumptions
          [View Model Action] -> [View Model Action] -> [View Model Action]
forall a. Semigroup a => a -> a -> a
<> Model
-> Maybe MisoString
-> Maybe NodeAddr
-> (Int -> NodeAddr)
-> [View Model Action]
-> [View Model Action]
interleaveWithDropZones
            Model
model
            Maybe MisoString
forall a. Maybe a
Nothing
            (NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just (NodeAddr -> NodeAddr
na NodeAddr
NAConclusion))
            (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr) -> (Int -> NodeAddr) -> Int -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr
NALine)
            [View Model Action]
viewProofs
          [View Model Action] -> [View Model Action] -> [View Model Action]
forall a. Semigroup a => a -> a -> a
<> Int -> [View Model Action] -> [View Model Action]
forall a. Int -> [a] -> [a]
drop
            Int
1
            ( Model
-> Maybe MisoString
-> Maybe NodeAddr
-> (Int -> NodeAddr)
-> [View Model Action]
-> [View Model Action]
interleaveWithDropZones
                Model
model
                Maybe MisoString
forall a. Maybe a
Nothing
                (NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just (NodeAddr -> NodeAddr
na NodeAddr
NAAfterConclusion))
                (NodeAddr -> Int -> NodeAddr
forall a b. a -> b -> a
const (NodeAddr -> Int -> NodeAddr) -> NodeAddr -> Int -> NodeAddr
forall a b. (a -> b) -> a -> b
$ NodeAddr -> NodeAddr
na NodeAddr
NAAfterConclusion)
                (OneItem [View Model Action] -> [View Model Action]
forall x. One x => OneItem x -> x
one View Model Action
OneItem [View Model Action]
viewConclusion)
            )
      )
   where
    viewAssumptions :: [View Model Action]
viewAssumptions =
      (Int, [View Model Action]) -> [View Model Action]
forall a b. (a, b) -> b
snd ((Int, [View Model Action]) -> [View Model Action])
-> (Int, [View Model Action]) -> [View Model Action]
forall a b. (a -> b) -> a -> b
$
        (Int -> Assumption -> (Int, View Model Action))
-> Int -> [Assumption] -> (Int, [View Model Action])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
L.mapAccumL
          ( \Int
m Assumption
f ->
              ( Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
              , Model
-> NodeAddr -> Either Assumption Derivation -> View Model Action
viewLine
                  Model
model
                  (NodeAddr -> NodeAddr
na (Int -> NodeAddr
NAAssumption Int
m))
                  (Assumption -> Either Assumption Derivation
forall a b. a -> Either a b
Left Assumption
f)
              )
          )
          Int
0
          [Assumption]
fs
    viewProofs :: [View Model Action]
viewProofs =
      (Int, [View Model Action]) -> [View Model Action]
forall a b. (a, b) -> b
snd ((Int, [View Model Action]) -> [View Model Action])
-> (Int, [View Model Action]) -> [View Model Action]
forall a b. (a -> b) -> a -> b
$
        (Int -> Either Derivation Proof -> (Int, View Model Action))
-> Int -> [Either Derivation Proof] -> (Int, [View Model Action])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
L.mapAccumL
          ( \Int
m Either Derivation Proof
e ->
              ( Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
              , (Derivation -> View Model Action)
-> (Proof -> View Model Action)
-> Either Derivation Proof
-> View Model Action
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
                  (Model
-> NodeAddr -> Either Assumption Derivation -> View Model Action
viewLine Model
model (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall a b. (a -> b) -> a -> b
$ Int -> NodeAddr
NALine Int
m) (Either Assumption Derivation -> View Model Action)
-> (Derivation -> Either Assumption Derivation)
-> Derivation
-> View Model Action
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation -> Either Assumption Derivation
forall a b. b -> Either a b
Right)
                  ((ProofAddr -> ProofAddr)
-> (NodeAddr -> NodeAddr) -> Proof -> View Model Action
_viewProof (ProofAddr -> ProofAddr
pa (ProofAddr -> ProofAddr)
-> (ProofAddr -> ProofAddr) -> ProofAddr -> ProofAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ProofAddr -> ProofAddr
PANested Int
m) (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr)
-> (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr -> NodeAddr
NAProof Int
m))
                  Either Derivation Proof
e
              )
          )
          Int
0
          [Either Derivation Proof]
ps
    viewConclusion :: View Model Action
viewConclusion = Model
-> NodeAddr -> Either Assumption Derivation -> View Model Action
viewLine Model
model (NodeAddr -> NodeAddr
na NodeAddr
NAConclusion) (Derivation -> Either Assumption Derivation
forall a b. b -> Either a b
Right Derivation
d)

{- | For use in 'viewProof',
returns a list of line numbers that are shown to the left of the t'Proof'.
-}
viewLineNos :: Model -> View Model Action
viewLineNos :: Model -> View Model Action
viewLineNos Model
model =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_ [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"line-no-container"] ([View Model Action] -> View Model Action)
-> [View Model Action] -> View Model Action
forall a b. (a -> b) -> a -> b
$
    OneItem [View Model Action] -> [View Model Action]
forall x. One x => OneItem x -> x
one (OneItem [View Model Action] -> [View Model Action])
-> OneItem [View Model Action] -> [View Model Action]
forall a b. (a -> b) -> a -> b
$
      Int -> (NodeAddr -> NodeAddr) -> Proof -> View Model Action
goProof Int
1 NodeAddr -> NodeAddr
forall a. a -> a
id (Model
model Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof)
 where
  lineNoFor :: NodeAddr -> Int -> View Model Action
  lineNoFor :: NodeAddr -> Int -> View Model Action
lineNoFor NodeAddr
na =
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.p_
      [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"line-no"
      , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False
      , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_ [(MisoString
"dragged", Model
model Model
-> Lens Model (Maybe (Either NodeAddr ProofAddr))
-> Maybe (Either NodeAddr ProofAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr ProofAddr))
dragTarget Maybe (Either NodeAddr ProofAddr)
-> Maybe (Either NodeAddr ProofAddr) -> Bool
forall a. Eq a => a -> a -> Bool
== Either NodeAddr ProofAddr -> Maybe (Either NodeAddr ProofAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Either NodeAddr ProofAddr
forall a b. a -> Either a b
Left NodeAddr
na))]
      ]
      ([View Model Action] -> View Model Action)
-> (Int -> [View Model Action]) -> Int -> View Model Action
forall b c a. (b -> c) -> (a -> b) -> a -> c
. View Model Action -> [View Model Action]
OneItem [View Model Action] -> [View Model Action]
forall x. One x => OneItem x -> x
one
      (View Model Action -> [View Model Action])
-> (Int -> View Model Action) -> Int -> [View Model Action]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MisoString -> View Model Action
forall model action. MisoString -> View model action
text
      (MisoString -> View Model Action)
-> (Int -> MisoString) -> Int -> View Model Action
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> MisoString
forall str. ToMisoString str => str -> MisoString
ms
  goProof :: Int -> (NodeAddr -> NodeAddr) -> Proof -> View Model Action
  goProof :: Int -> (NodeAddr -> NodeAddr) -> Proof -> View Model Action
goProof Int
lineNo NodeAddr -> NodeAddr
na (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
      [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"line-no-wrapper", Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False]
      ( Model
-> Maybe MisoString
-> Maybe NodeAddr
-> (Int -> NodeAddr)
-> [View Model Action]
-> [View Model Action]
interleaveWithDropZones
          Model
model
          (MisoString -> Maybe MisoString
forall a. a -> Maybe a
Just MisoString
"empty-last-assumption")
          Maybe NodeAddr
forall a. Maybe a
Nothing
          (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr) -> (Int -> NodeAddr) -> Int -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr
NAAssumption)
          [View Model Action]
goFs
          [View Model Action] -> [View Model Action] -> [View Model Action]
forall a. Semigroup a => a -> a -> a
<> Model
-> Maybe MisoString
-> Maybe NodeAddr
-> (Int -> NodeAddr)
-> [View Model Action]
-> [View Model Action]
interleaveWithDropZones
            Model
model
            Maybe MisoString
forall a. Maybe a
Nothing
            (NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just (NodeAddr -> NodeAddr
na NodeAddr
NAConclusion))
            (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr) -> (Int -> NodeAddr) -> Int -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr
NALine)
            [View Model Action]
goPs
          [View Model Action] -> [View Model Action] -> [View Model Action]
forall a. Semigroup a => a -> a -> a
<> Int -> [View Model Action] -> [View Model Action]
forall a. Int -> [a] -> [a]
drop
            Int
1
            ( Model
-> Maybe MisoString
-> Maybe NodeAddr
-> (Int -> NodeAddr)
-> [View Model Action]
-> [View Model Action]
interleaveWithDropZones
                Model
model
                Maybe MisoString
forall a. Maybe a
Nothing
                (NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just (NodeAddr -> NodeAddr
na NodeAddr
NAAfterConclusion))
                (NodeAddr -> Int -> NodeAddr
forall a b. a -> b -> a
const (NodeAddr -> Int -> NodeAddr) -> NodeAddr -> Int -> NodeAddr
forall a b. (a -> b) -> a -> b
$ NodeAddr -> NodeAddr
na NodeAddr
NAAfterConclusion)
                (OneItem [View Model Action] -> [View Model Action]
forall x. One x => OneItem x -> x
one View Model Action
OneItem [View Model Action]
goC)
            )
      )
   where
    ((Int
lineNo', Int
_), [View Model Action]
goFs) =
      ((Int, Int) -> Assumption -> ((Int, Int), View Model Action))
-> (Int, Int) -> [Assumption] -> ((Int, Int), [View Model Action])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
        (\(Int
lineNo, Int
d) Assumption
f -> ((Int
lineNo Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1), NodeAddr -> Int -> View Model Action
lineNoFor (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall a b. (a -> b) -> a -> b
$ Int -> NodeAddr
NAAssumption Int
d) Int
lineNo))
        (Int
lineNo, Int
0)
        [Assumption]
fs
    ((Int
lineNo'', Int
_), [View Model Action]
goPs) =
      ((Int, Int)
 -> Either Derivation Proof -> ((Int, Int), View Model Action))
-> (Int, Int)
-> [Either Derivation Proof]
-> ((Int, Int), [View Model Action])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
        ( \(Int
lineNo, Int
n) Either Derivation Proof
e ->
            (Derivation -> ((Int, Int), View Model Action))
-> (Proof -> ((Int, Int), View Model Action))
-> Either Derivation Proof
-> ((Int, Int), View Model Action)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
              (\Derivation
d -> ((Int
lineNo Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1), Int -> NodeAddr -> Derivation -> View Model Action
goDerivation Int
lineNo (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall a b. (a -> b) -> a -> b
$ Int -> NodeAddr
NALine Int
n) Derivation
d))
              (\Proof
p -> ((Int
lineNo Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Proof -> Int
pLength Proof
p, Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1), Int -> (NodeAddr -> NodeAddr) -> Proof -> View Model Action
goProof Int
lineNo (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr)
-> (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr -> NodeAddr
NAProof Int
n) Proof
p))
              Either Derivation Proof
e
        )
        (Int
lineNo', Int
0)
        [Either Derivation Proof]
ps
    goC :: View Model Action
goC = Int -> NodeAddr -> Derivation -> View Model Action
goDerivation Int
lineNo'' (NodeAddr -> NodeAddr
na NodeAddr
NAConclusion) Derivation
c
  goDerivation :: Int -> NodeAddr -> Derivation -> View Model Action
  goDerivation :: Int -> NodeAddr -> Derivation -> View Model Action
goDerivation Int
lineNo NodeAddr
na Derivation
_ = NodeAddr -> Int -> View Model Action
lineNoFor NodeAddr
na Int
lineNo

{- | For use in 'viewProof',
returns a list of t'RuleApplication's (judgements),
that are shown to the right of the t'Proof'.
-}
viewRuleApplications :: Model -> View Model Action
viewRuleApplications :: Model -> View Model Action
viewRuleApplications Model
model =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_ [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"rules-container"] ([View Model Action] -> View Model Action)
-> [View Model Action] -> View Model Action
forall a b. (a -> b) -> a -> b
$
    OneItem [View Model Action] -> [View Model Action]
forall x. One x => OneItem x -> x
one (OneItem [View Model Action] -> [View Model Action])
-> OneItem [View Model Action] -> [View Model Action]
forall a b. (a -> b) -> a -> b
$
      (NodeAddr -> NodeAddr) -> Proof -> View Model Action
go NodeAddr -> NodeAddr
forall a. a -> a
id (Model
model Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof)
 where
  go :: (NodeAddr -> NodeAddr) -> Proof -> View Model Action
  go :: (NodeAddr -> NodeAddr) -> Proof -> View Model Action
go NodeAddr -> NodeAddr
na (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
      [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"rules-wrapper"]
      ( Model
-> Maybe MisoString
-> Maybe NodeAddr
-> (Int -> NodeAddr)
-> [View Model Action]
-> [View Model Action]
interleaveWithDropZones
          Model
model
          (MisoString -> Maybe MisoString
forall a. a -> Maybe a
Just MisoString
"empty-last-assumption")
          Maybe NodeAddr
forall a. Maybe a
Nothing
          (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr) -> (Int -> NodeAddr) -> Int -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr
NAAssumption)
          [View Model Action]
goFs
          [View Model Action] -> [View Model Action] -> [View Model Action]
forall a. Semigroup a => a -> a -> a
<> Model
-> Maybe MisoString
-> Maybe NodeAddr
-> (Int -> NodeAddr)
-> [View Model Action]
-> [View Model Action]
interleaveWithDropZones
            Model
model
            Maybe MisoString
forall a. Maybe a
Nothing
            (NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just (NodeAddr -> NodeAddr
na NodeAddr
NAConclusion))
            (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr) -> (Int -> NodeAddr) -> Int -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr
NALine)
            [View Model Action]
goPs
          [View Model Action] -> [View Model Action] -> [View Model Action]
forall a. Semigroup a => a -> a -> a
<> Int -> [View Model Action] -> [View Model Action]
forall a. Int -> [a] -> [a]
drop
            Int
1
            ( Model
-> Maybe MisoString
-> Maybe NodeAddr
-> (Int -> NodeAddr)
-> [View Model Action]
-> [View Model Action]
interleaveWithDropZones
                Model
model
                Maybe MisoString
forall a. Maybe a
Nothing
                (NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just (NodeAddr -> NodeAddr
na NodeAddr
NAAfterConclusion))
                (NodeAddr -> Int -> NodeAddr
forall a b. a -> b -> a
const (NodeAddr -> Int -> NodeAddr) -> NodeAddr -> Int -> NodeAddr
forall a b. (a -> b) -> a -> b
$ NodeAddr -> NodeAddr
na NodeAddr
NAAfterConclusion)
                (OneItem [View Model Action] -> [View Model Action]
forall x. One x => OneItem x -> x
one View Model Action
OneItem [View Model Action]
goC)
            )
      )
   where
    goFs :: [View Model Action]
goFs =
      (Assumption -> View Model Action)
-> [Assumption] -> [View Model Action]
forall a b. (a -> b) -> [a] -> [b]
map
        ( View Model Action -> Assumption -> View Model Action
forall a b. a -> b -> a
const (View Model Action -> Assumption -> View Model Action)
-> View Model Action -> Assumption -> View Model Action
forall a b. (a -> b) -> a -> b
$
            [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.p_
              [MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"empty-rule"]
              [MisoString -> View Model Action
forall model action. MisoString -> View model action
textRaw MisoString
"\160"]
        )
        [Assumption]
fs
    goPs :: [View Model Action]
goPs =
      (Int, [View Model Action]) -> [View Model Action]
forall a b. (a, b) -> b
snd ((Int, [View Model Action]) -> [View Model Action])
-> (Int, [View Model Action]) -> [View Model Action]
forall a b. (a -> b) -> a -> b
$
        (Int -> Either Derivation Proof -> (Int, View Model Action))
-> Int -> [Either Derivation Proof] -> (Int, [View Model Action])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
          (\Int
n Either Derivation Proof
e -> (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, (Derivation -> View Model Action)
-> (Proof -> View Model Action)
-> Either Derivation Proof
-> View Model Action
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (NodeAddr -> Derivation -> View Model Action
goDerivation (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall a b. (a -> b) -> a -> b
$ Int -> NodeAddr
NALine Int
n)) ((NodeAddr -> NodeAddr) -> Proof -> View Model Action
go (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr)
-> (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr -> NodeAddr
NAProof Int
n)) Either Derivation Proof
e))
          Int
0
          [Either Derivation Proof]
ps
    goC :: View Model Action
goC = NodeAddr -> Derivation -> View Model Action
goDerivation (NodeAddr -> NodeAddr
na NodeAddr
NAConclusion) Derivation
c
  goDerivation :: NodeAddr -> Derivation -> View Model Action
  goDerivation :: NodeAddr -> Derivation -> View Model Action
goDerivation NodeAddr
na (Derivation Formula
_ Wrapper RuleApplication
p) =
    let
      lineno :: Int
lineno = NodeAddr -> Proof -> Int
lineNoOr999 NodeAddr
na (Model
model Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof)
      inputId :: MisoString
inputId = NodeAddr -> Proof -> MisoString
mkRuleInputId NodeAddr
na (Model
model Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof)
      errorBoxId :: MisoString
errorBoxId = MisoString
"rule-error-" MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> Int -> MisoString
forall b a. (Show a, IsString b) => a -> b
show Int
lineno
     in
      [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
        [ Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOver (MisoString -> Bool -> Action
OpenTooltip MisoString
errorBoxId Bool
hasError)
        , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOut Action
CloseTooltip
        , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"rule-container"
        , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-container"
        , Action -> Attribute Action
forall action. action -> Attribute action
HE.onClick (Action -> Attribute Action) -> Action -> Attribute Action
forall a b. (a -> b) -> a -> b
$ Either NodeAddr NodeAddr -> Action
Focus (NodeAddr -> Either NodeAddr NodeAddr
forall a b. b -> Either a b
Right NodeAddr
na)
        , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_ [(MisoString
"dragged", Model
model Model
-> Lens Model (Maybe (Either NodeAddr ProofAddr))
-> Maybe (Either NodeAddr ProofAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr ProofAddr))
dragTarget Maybe (Either NodeAddr ProofAddr)
-> Maybe (Either NodeAddr ProofAddr) -> Bool
forall a. Eq a => a -> a -> Bool
== Either NodeAddr ProofAddr -> Maybe (Either NodeAddr ProofAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Either NodeAddr ProofAddr
forall a b. a -> Either a b
Left NodeAddr
na))]
        ]
        [ MisoString -> MisoString -> View Model Action
viewErrorBox MisoString
errorBoxId MisoString
err
        , [Attribute Action] -> View Model Action
forall action model. [Attribute action] -> View model action
H.input_
            [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"rule-input"
            , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.spellcheck_ Bool
False
            , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.placeholder_ MisoString
"    "
            , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ MisoString
inputId
            , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-anchor"
            , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_
                [ (MisoString
"has-error", Bool
hasError)
                , (MisoString
"focused", Either NodeAddr NodeAddr -> Maybe (Either NodeAddr NodeAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Either NodeAddr NodeAddr
forall a b. b -> Either a b
Right NodeAddr
na) Maybe (Either NodeAddr NodeAddr)
-> Maybe (Either NodeAddr NodeAddr) -> Bool
forall a. Eq a => a -> a -> Bool
== Model
model Model
-> Lens Model (Maybe (Either NodeAddr NodeAddr))
-> Maybe (Either NodeAddr NodeAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr NodeAddr))
focusedLine)
                ]
            , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.autocomplete_ Bool
False
            , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False
            , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.inert_ (Either NodeAddr NodeAddr -> Maybe (Either NodeAddr NodeAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Either NodeAddr NodeAddr
forall a b. b -> Either a b
Right NodeAddr
na) Maybe (Either NodeAddr NodeAddr)
-> Maybe (Either NodeAddr NodeAddr) -> Bool
forall a. Eq a => a -> a -> Bool
/= Model
model Model
-> Lens Model (Maybe (Either NodeAddr NodeAddr))
-> Maybe (Either NodeAddr NodeAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr NodeAddr))
focusedLine)
            , Action -> Attribute Action
forall action. action -> Attribute action
HE.onBlur (Either NodeAddr NodeAddr -> Action
Blur (NodeAddr -> Either NodeAddr NodeAddr
forall a b. b -> Either a b
Right NodeAddr
na))
            , Phase
-> Options
-> MisoString
-> Decoder MisoString
-> (MisoString -> DOMRef -> Action)
-> Attribute Action
forall r action.
Phase
-> Options
-> MisoString
-> Decoder r
-> (r -> DOMRef -> action)
-> Attribute action
onWithOptions Phase
BUBBLE Options
defaultOptions MisoString
"input" Decoder MisoString
valueDecoder MisoString -> DOMRef -> Action
Input
            , (MisoString -> Action) -> Attribute Action
forall action. (MisoString -> action) -> Attribute action
HE.onChange (Action -> MisoString -> Action
forall a b. a -> b -> a
const Action
Change)
            , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragStartWithOptions Options
preventDefault Action
Nop
            , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.value_ MisoString
ruleTxt
            ]
        ]
   where
    (Bool
hasError, MisoString
ruleTxt, MisoString
err) = case Wrapper RuleApplication
p of
      (ParsedValid MisoString
str RuleApplication
_) -> (Bool
False, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
str, MisoString
"")
      (ParsedInvalid MisoString
str MisoString
err RuleApplication
_) -> (Bool
True, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
str, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
err)
      (Unparsed MisoString
str MisoString
err) -> (Bool
True, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
str, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
err)

{- | Returns a errorbox that is shown on hover, containing errors
written in a @<code>@ element to get monospacing.
-}
viewErrorBox ::
  -- | @id@ of the errorbox.
  MisoString ->
  -- | Error message.
  MisoString ->
  View Model Action
viewErrorBox :: MisoString -> MisoString -> View Model Action
viewErrorBox MisoString
name MisoString
err =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.code_
    [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-bottom"
    , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ MisoString
name
    , MisoString -> MisoString -> Attribute Action
forall action. MisoString -> MisoString -> Attribute action
textProp MisoString
"popover" MisoString
"hint"
    , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False
    ]
    [MisoString -> View Model Action
forall model action. MisoString -> View model action
text MisoString
err]

-- | Helper for turning a t'NodeAddr' to a formula inputfield id.
mkFormulaInputId :: NodeAddr -> Proof -> MisoString
mkFormulaInputId :: NodeAddr -> Proof -> MisoString
mkFormulaInputId NodeAddr
na Proof
p = MisoString
"formula-input-" MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> Int -> MisoString
forall b a. (Show a, IsString b) => a -> b
show (NodeAddr -> Proof -> Int
lineNoOr999 NodeAddr
na Proof
p)

-- | Helper for turning a t'NodeAddr' to a rule inputfield id.
mkRuleInputId :: NodeAddr -> Proof -> MisoString
mkRuleInputId :: NodeAddr -> Proof -> MisoString
mkRuleInputId NodeAddr
na Proof
p = MisoString
"rule-input-" MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> Int -> MisoString
forall b a. (Show a, IsString b) => a -> b
show (NodeAddr -> Proof -> Int
lineNoOr999 NodeAddr
na Proof
p)

{- | For use in 'viewProof', shows a single line of the t'Proof',
specified by its t'NodeAddr'.
-}
viewLine :: Model -> NodeAddr -> Either Assumption Derivation -> View Model Action
viewLine :: Model
-> NodeAddr -> Either Assumption Derivation -> View Model Action
viewLine Model
model NodeAddr
na Either Assumption Derivation
e =
  let
    lineno :: Int
lineno = NodeAddr -> Proof -> Int
lineNoOr999 NodeAddr
na (Model
model Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof)
    errorBoxId :: MisoString
errorBoxId = MisoString
"formula-error-" MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> Int -> MisoString
forall b a. (Show a, IsString b) => a -> b
show Int
lineno
    inputId :: MisoString
inputId = NodeAddr -> Proof -> MisoString
mkFormulaInputId NodeAddr
na (Model
model Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof)
   in
    [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
      [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"formula-container"
      , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_
          [ (MisoString
"draggable", (Model
model Model
-> Lens Model (Maybe (Either NodeAddr NodeAddr))
-> Maybe (Either NodeAddr NodeAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr NodeAddr))
focusedLine Maybe (Either NodeAddr NodeAddr)
-> Maybe (Either NodeAddr NodeAddr) -> Bool
forall a. Eq a => a -> a -> Bool
/= Either NodeAddr NodeAddr -> Maybe (Either NodeAddr NodeAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Either NodeAddr NodeAddr
forall a b. a -> Either a b
Left NodeAddr
na)) Bool -> Bool -> Bool
&& Bool -> Bool
not (Model
model Model -> Lens Model Bool -> Bool
forall record field. record -> Lens record field -> field
^. Lens Model Bool
dragging))
          , (MisoString
"dragged", Model
model Model
-> Lens Model (Maybe (Either NodeAddr ProofAddr))
-> Maybe (Either NodeAddr ProofAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr ProofAddr))
dragTarget Maybe (Either NodeAddr ProofAddr)
-> Maybe (Either NodeAddr ProofAddr) -> Bool
forall a. Eq a => a -> a -> Bool
== Either NodeAddr ProofAddr -> Maybe (Either NodeAddr ProofAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Either NodeAddr ProofAddr
forall a b. a -> Either a b
Left NodeAddr
na))
          , (MisoString
"failed-drop", Model
model Model -> Lens Model (Maybe NodeAddr) -> Maybe NodeAddr
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe NodeAddr)
lastDragged Maybe NodeAddr -> Maybe NodeAddr -> Bool
forall a. Eq a => a -> a -> Bool
== NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just NodeAddr
na)
          ]
      , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-container"
      , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
True
      , if Model
model Model
-> Lens Model (Maybe (Either NodeAddr NodeAddr))
-> Maybe (Either NodeAddr NodeAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr NodeAddr))
focusedLine Maybe (Either NodeAddr NodeAddr)
-> Maybe (Either NodeAddr NodeAddr) -> Bool
forall a. Eq a => a -> a -> Bool
/= Either NodeAddr NodeAddr -> Maybe (Either NodeAddr NodeAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Either NodeAddr NodeAddr
forall a b. a -> Either a b
Left NodeAddr
na)
          then Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragStartWithOptions Options
stopPropagation (Action -> Attribute Action) -> Action -> Attribute Action
forall a b. (a -> b) -> a -> b
$ Either NodeAddr ProofAddr -> Action
DragStart (NodeAddr -> Either NodeAddr ProofAddr
forall a b. a -> Either a b
Left NodeAddr
na)
          else Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragStartWithOptions (Options
stopPropagation Options -> Options -> Options
forall a. Semigroup a => a -> a -> a
<> Options
preventDefault) Action
Nop
      , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragEnterWithOptions (Options
preventDefault Options -> Options -> Options
forall a. Semigroup a => a -> a -> a
<> Options
stopPropagation) Action
Nop
      , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragEndWithOptions Options
defaultOptions Action
DragEnd
      , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOver (MisoString -> Bool -> Action
OpenTooltip MisoString
errorBoxId Bool
hasError)
      , Action -> Attribute Action
forall action. action -> Attribute action
HE.onMouseOut Action
CloseTooltip
      , Action -> Attribute Action
forall action. action -> Attribute action
HE.onClick (Action -> Attribute Action) -> Action -> Attribute Action
forall a b. (a -> b) -> a -> b
$ Either NodeAddr NodeAddr -> Action
Focus (NodeAddr -> Either NodeAddr NodeAddr
forall a b. a -> Either a b
Left NodeAddr
na)
      ]
      [ [Attribute Action] -> View Model Action
forall action model. [Attribute action] -> View model action
H.input_
          [ Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.inert_ (Either NodeAddr NodeAddr -> Maybe (Either NodeAddr NodeAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Either NodeAddr NodeAddr
forall a b. a -> Either a b
Left NodeAddr
na) Maybe (Either NodeAddr NodeAddr)
-> Maybe (Either NodeAddr NodeAddr) -> Bool
forall a. Eq a => a -> a -> Bool
/= Model
model Model
-> Lens Model (Maybe (Either NodeAddr NodeAddr))
-> Maybe (Either NodeAddr NodeAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr NodeAddr))
focusedLine)
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ MisoString
inputId
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.placeholder_ MisoString
"    "
          , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.spellcheck_ Bool
False
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"formula-input"
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"tooltip-anchor"
          , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_
              [ (MisoString
"has-error", Bool
hasError)
              , (MisoString
"drag-target", Either NodeAddr ProofAddr -> Maybe (Either NodeAddr ProofAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Either NodeAddr ProofAddr
forall a b. a -> Either a b
Left NodeAddr
na) Maybe (Either NodeAddr ProofAddr)
-> Maybe (Either NodeAddr ProofAddr) -> Bool
forall a. Eq a => a -> a -> Bool
== Model
model Model
-> Lens Model (Maybe (Either NodeAddr ProofAddr))
-> Maybe (Either NodeAddr ProofAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr ProofAddr))
dragTarget)
              , (MisoString
"focused", Either NodeAddr NodeAddr -> Maybe (Either NodeAddr NodeAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Either NodeAddr NodeAddr
forall a b. a -> Either a b
Left NodeAddr
na) Maybe (Either NodeAddr NodeAddr)
-> Maybe (Either NodeAddr NodeAddr) -> Bool
forall a. Eq a => a -> a -> Bool
== Model
model Model
-> Lens Model (Maybe (Either NodeAddr NodeAddr))
-> Maybe (Either NodeAddr NodeAddr)
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe (Either NodeAddr NodeAddr))
focusedLine)
              ]
          , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.autocomplete_ Bool
False
          , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False
          , Action -> Attribute Action
forall action. action -> Attribute action
HE.onBlur (Either NodeAddr NodeAddr -> Action
Blur (NodeAddr -> Either NodeAddr NodeAddr
forall a b. a -> Either a b
Left NodeAddr
na))
          , (MisoString -> Action) -> Attribute Action
forall action. (MisoString -> action) -> Attribute action
HE.onChange (Action -> MisoString -> Action
forall a b. a -> b -> a
const Action
Change)
          , Phase
-> Options
-> MisoString
-> Decoder MisoString
-> (MisoString -> DOMRef -> Action)
-> Attribute Action
forall r action.
Phase
-> Options
-> MisoString
-> Decoder r
-> (r -> DOMRef -> action)
-> Attribute action
onWithOptions Phase
BUBBLE Options
defaultOptions MisoString
"input" Decoder MisoString
valueDecoder MisoString -> DOMRef -> Action
Input
          , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragStartWithOptions Options
preventDefault Action
Nop
          , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.value_ MisoString
txt
          ]
      , MisoString -> MisoString -> View Model Action
viewErrorBox MisoString
errorBoxId MisoString
err
      ]
 where
  (Bool
hasError, MisoString
txt, MisoString
err) = case Either Assumption Derivation
e of
    Left (Wrapper RawAssumption
a, Wrapper RuleApplication
_) -> case Wrapper RawAssumption
a of
      ParsedValid MisoString
str RawAssumption
a' -> (Bool
False, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
str, MisoString
"")
      ParsedInvalid MisoString
str MisoString
err RawAssumption
a' -> (Bool
True, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
str, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
err)
      Unparsed MisoString
str MisoString
err -> (Bool
True, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
str, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
err)
    Right (Derivation Formula
f Wrapper RuleApplication
r) -> case Formula
f of
      (ParsedValid MisoString
str RawFormula
f') -> (Bool
False, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
str, MisoString
"")
      (ParsedInvalid MisoString
str MisoString
err RawFormula
f') -> (Bool
True, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
str, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
err)
      (Unparsed MisoString
str MisoString
err) -> (Bool
True, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
str, MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms MisoString
err)

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

-- * Utilities

{- | Helper for viewing material icons based on their name,
see <https://fonts.google.com/icons>
-}
viewMaterialIcon :: MisoString -> View Model Action
viewMaterialIcon :: MisoString -> View Model Action
viewMaterialIcon MisoString
name = [Attribute Action] -> View Model Action
forall action model. [Attribute action] -> View model action
H.img_ [Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ Bool
False, MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.src_ (MisoString -> Attribute Action) -> MisoString -> Attribute Action
forall a b. (a -> b) -> a -> b
$ MisoString
"icons/" MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> MisoString
name MisoString -> MisoString -> MisoString
forall a. Semigroup a => a -> a -> a
<> MisoString
".svg"]

{- |
Shows a dropzone for the given t'NodeAddr',
i.e. a small empty div, where nodes can be dropped.

Expands, if a node can be dropped inside.
-}
viewDropZoneAt ::
  -- | The t'Model'.
  Model ->
  -- | Optional class for the dropzone.
  Maybe MisoString ->
  -- | The corresponding t'NodeAddr'.
  NodeAddr ->
  View Model Action
viewDropZoneAt :: Model -> Maybe MisoString -> NodeAddr -> View Model Action
viewDropZoneAt Model
model Maybe MisoString
mclass NodeAddr
na =
  [Attribute Action] -> [View Model Action] -> View Model Action
forall action model.
[Attribute action] -> [View model action] -> View model action
H.div_
    [ MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.class_ MisoString
"drop-zone"
    , MisoString -> Attribute Action
forall action. MisoString -> Attribute action
HP.id_ (MisoString -> Attribute Action) -> MisoString -> Attribute Action
forall a b. (a -> b) -> a -> b
$ MisoString -> MisoString
forall str. ToMisoString str => str -> MisoString
ms (MisoString -> MisoString) -> MisoString -> MisoString
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> MisoString -> MisoString
T.filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
' ') (NodeAddr -> MisoString
forall b a. (Show a, IsString b) => a -> b
show NodeAddr
na)
    , [(MisoString, Bool)] -> Attribute Action
forall action. [(MisoString, Bool)] -> Attribute action
HP.classList_
        [ (MisoString
"expanded-drop-zone", Model
model Model -> Lens Model (Maybe NodeAddr) -> Maybe NodeAddr
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe NodeAddr)
currentHoverLine Maybe NodeAddr -> Maybe NodeAddr -> Bool
forall a. Eq a => a -> a -> Bool
== NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just NodeAddr
na)
        , (MisoString -> Maybe MisoString -> MisoString
forall a. a -> Maybe a -> a
fromMaybe MisoString
"" Maybe MisoString
mclass, Maybe MisoString -> Bool
forall a. Maybe a -> Bool
isJust Maybe MisoString
mclass)
        , (MisoString
"draggable", Maybe MisoString -> Bool
forall a. Maybe a -> Bool
isJust Maybe MisoString
mclass Bool -> Bool -> Bool
&& Bool -> Bool
not (NodeAddr -> Bool
isNAAssumption NodeAddr
na))
        , (MisoString
"failed-drop", Model
model Model -> Lens Model (Maybe NodeAddr) -> Maybe NodeAddr
forall record field. record -> Lens record field -> field
^. Lens Model (Maybe NodeAddr)
lastDragged Maybe NodeAddr -> Maybe NodeAddr -> Bool
forall a. Eq a => a -> a -> Bool
== NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just NodeAddr
na)
        ]
    , Bool -> Attribute Action
forall action. Bool -> Attribute action
HP.draggable_ (Maybe MisoString -> Bool
forall a. Maybe a -> Bool
isNothing Maybe MisoString
mclass) -- true to overshadow the draggable of subproof
    , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragStartWithOptions (Options
preventDefault Options -> Options -> Options
forall a. Semigroup a => a -> a -> a
<> Options
stopPropagation) Action
Nop
    , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragOverWithOptions Options
preventDefault Action
Nop
    , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDragEnterWithOptions (Options
preventDefault Options -> Options -> Options
forall a. Semigroup a => a -> a -> a
<> Options
stopPropagation) (NodeAddr -> Action
DragEnter NodeAddr
na)
    , Options -> Action -> Attribute Action
forall action. Options -> action -> Attribute action
HE.onDropWithOptions Options
defaultOptions (DropLocation -> Action
Drop (NodeAddr -> DropLocation
LineAddr NodeAddr
na))
    ]
    []

-- | Interleaves the list @views@ with dropzones of the corresponding t'NodeAddr'.
interleaveWithDropZones ::
  -- | The t'Model'.
  Model ->
  -- | Optionally a class for the last dropzone.
  Maybe MisoString ->
  -- | Optionally a differing t'NodeAddr' for the last dropzone.
  Maybe NodeAddr ->
  {- | A function for generating t'NodeAddr' from a number
  (e.g. turn @n@ into @v'NAAssumption' n@).
  -}
  (Int -> NodeAddr) ->
  -- | The list of views to be interleaved.
  [View Model Action] ->
  [View Model Action]
interleaveWithDropZones :: Model
-> Maybe MisoString
-> Maybe NodeAddr
-> (Int -> NodeAddr)
-> [View Model Action]
-> [View Model Action]
interleaveWithDropZones Model
model Maybe MisoString
mclass Maybe NodeAddr
lastNA Int -> NodeAddr
na [View Model Action]
views = [View Model Action] -> [View Model Action] -> [View Model Action]
forall a. [a] -> [a] -> [a]
interleave [View Model Action]
dropzones [View Model Action]
views
 where
  dropzones :: [View Model Action]
  dropzones :: [View Model Action]
dropzones =
    (Int -> View Model Action) -> [Int] -> [View Model Action]
forall a b. (a -> b) -> [a] -> [b]
map
      ( \Int
n ->
          Model -> Maybe MisoString -> NodeAddr -> View Model Action
viewDropZoneAt
            Model
model
            (if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [View Model Action] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [View Model Action]
views then Maybe MisoString
mclass else Maybe MisoString
forall a. Maybe a
Nothing)
            (if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [View Model Action] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [View Model Action]
views then NodeAddr -> Maybe NodeAddr -> NodeAddr
forall a. a -> Maybe a -> a
fromMaybe (Int -> NodeAddr
na Int
n) Maybe NodeAddr
lastNA else Int -> NodeAddr
na Int
n)
      )
      [Int
Item [Int]
0 .. [View Model Action] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [View Model Action]
views]

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