Copyright	(c) Leon Vatthauer 2026
License	GPL-3
Maintainer	Leon Vatthauer <leon.vatthauer@fau.de>
Stability	experimental
Portability	non-portable (ghc-wasm-meta)
Safe Haskell	None
Language	GHC2024

App.Model

Contents

Data Types
Model
Lenses

Description

This module defines the application Model.

Synopsis

data DropLocation where
- LineAddr :: NodeAddr -> DropLocation
- LocationBin :: DropLocation
data SpawnType where
- SpawnLine :: SpawnType
- SpawnProof :: SpawnType
data Logic
- = Prop
- | FOL
canSpawnBefore :: NodeAddr -> SpawnType -> Bool
data Action where
- InitMathJAX :: DOMRef -> Action
- OpenTooltip :: MisoString -> Bool -> Action
- CloseTooltip :: Action
- ToggleSidebar :: Action
- SetProof :: Proof -> Action
- PopState :: URI -> Action
- Setup :: Action
- Focus :: Either NodeAddr NodeAddr -> Action
- Blur :: Either NodeAddr NodeAddr -> Action
- Input :: MisoString -> DOMRef -> Action
- ProcessInput :: MisoString -> Int -> Int -> Either NodeAddr NodeAddr -> Action
- Change :: Action
- Drop :: DropLocation -> Action
- DragEnter :: NodeAddr -> Action
- DragLeave :: Action
- DragStart :: Either NodeAddr ProofAddr -> Action
- DragEnd :: Action
- SpawnStart :: SpawnType -> Action
- NavigateForward :: Action
- NavigateBackward :: Action
- Resize :: Bool -> Action
- Nop :: Action
type Pos = Int
data Model = Model {
- _focusedLine :: Maybe (Either NodeAddr NodeAddr)
- _exampleProofs :: [(Text, Proof)]
- _emptyDerivation :: Derivation
- _proof :: Proof
- _sidebarToggle :: Bool
- _dragTarget :: Maybe (Either NodeAddr ProofAddr)
- _lastDragged :: Maybe NodeAddr
- _spawnType :: Maybe SpawnType
- _currentHoverLine :: Maybe NodeAddr
- _dragging :: Bool
- _operators :: [(Text, Text, Int)]
- _infixPreds :: [(Text, Text)]
- _quantifiers :: [(Text, Text)]
- _functionSymbols :: Map Text (Int, Pos)
- _predicateSymbols :: Map Text (Int, Pos)
- _rules :: [(Name, RuleSpec)]
- _uri :: URI
- _logic :: Logic
- _currentTooltip :: Maybe MisoString
- _onMobile :: Bool
}
initialModel :: Derivation -> Proof -> [(Text, Proof)] -> [(Text, Text, Int)] -> [(Text, Text)] -> [(Text, Text)] -> [(Name, RuleSpec)] -> URI -> Logic -> Maybe Bool -> Bool -> Model
focusedLine :: Lens Model (Maybe (Either NodeAddr NodeAddr))
exampleProofs :: Lens Model [(Text, Proof)]
emptyDerivation :: Lens Model Derivation
proof :: Lens Model Proof
sidebarToggle :: Lens Model Bool
dragTarget :: Lens Model (Maybe (Either NodeAddr ProofAddr))
lastDragged :: Lens Model (Maybe NodeAddr)
spawnType :: Lens Model (Maybe SpawnType)
currentHoverLine :: Lens Model (Maybe NodeAddr)
dragging :: Lens Model Bool
operators :: Lens Model [(Text, Text, Int)]
infixPreds :: Lens Model [(Text, Text)]
quantifiers :: Lens Model [(Text, Text)]
functionSymbols :: Lens Model (Map Text (Int, Pos))
predicateSymbols :: Lens Model (Map Text (Int, Pos))
rules :: Lens Model [(Name, RuleSpec)]
uri :: Lens Model URI
logic :: Lens Model Logic
currentTooltip :: Lens Model (Maybe MisoString)
onMobile :: Lens Model Bool

Data Types

data DropLocation where Source #

Specifies the location where a Assumption, Derivation or tProof has been dropped.

Constructors

LineAddr :: NodeAddr -> DropLocation	Dropped before a `NodeAddr`.
LocationBin :: DropLocation	Dropped in the bin.

Instances

Instances details

Show DropLocation Source #
Instance details Defined in App.Model Methods showsPrec :: Int -> DropLocation -> ShowS # show :: DropLocation -> String # showList :: [DropLocation] -> ShowS #
Eq DropLocation Source #
Instance details Defined in App.Model Methods (==) :: DropLocation -> DropLocation -> Bool # (/=) :: DropLocation -> DropLocation -> Bool #

data SpawnType where Source #

Specifies whether a Assumption, Derivation or a Proof should be spawned.

Constructors

SpawnLine :: SpawnType	Spawn a `Assumption` or `Derivation`
SpawnProof :: SpawnType	Spawn a `Proof`

Instances

Instances details

Show SpawnType Source #
Instance details Defined in App.Model Methods showsPrec :: Int -> SpawnType -> ShowS # show :: SpawnType -> String # showList :: [SpawnType] -> ShowS #
Eq SpawnType Source #
Instance details Defined in App.Model Methods (==) :: SpawnType -> SpawnType -> Bool # (/=) :: SpawnType -> SpawnType -> Bool #

data Logic Source #

Enumeration of Logics that the app supports.

Constructors

Prop
FOL

Instances

Instances details

Show Logic Source #
Instance details Defined in App.Model Methods showsPrec :: Int -> Logic -> ShowS # show :: Logic -> String # showList :: [Logic] -> ShowS #
Eq Logic Source #
Instance details Defined in App.Model Methods (==) :: Logic -> Logic -> Bool # (/=) :: Logic -> Logic -> Bool #

canSpawnBefore :: NodeAddr -> SpawnType -> Bool Source #

Returns whether a given SpawnType can be spawned before a NodeAddr. For example, a Proof can be spawned before a NAConclusion, but not before a NAAssumption.

data Action where Source #

The actions of the application.

Constructors

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

type Pos = Int Source #

Type for position information.

Model

data Model Source #

The Model of the application.

Constructors

Model

Fields

_focusedLine :: Maybe (Either NodeAddr NodeAddr)
Currently focused line.
_exampleProofs :: [(Text, Proof)]
List of example Proofs.
_emptyDerivation :: Derivation
Empty Derivation as a dummy for inserting.
_proof :: Proof
Current Proof of the application.
_sidebarToggle :: Bool
True if the sidebar is open.
_dragTarget :: Maybe (Either NodeAddr ProofAddr)
Assumption, Derivation or Proof that is currently being dragged.
_lastDragged :: Maybe NodeAddr
last node that was dragged
_spawnType :: Maybe SpawnType
Type of element to be spawned.
_currentHoverLine :: Maybe NodeAddr
Line before which the user currently hovers.
_dragging :: Bool
True if the user is currently dragging an element.
_operators :: [(Text, Text, Int)]
List of operators, consisting of (alias, operator, arity), where alias is an alternative notation for the operator.
_infixPreds :: [(Text, Text)]
List of infix predicates, consisting of (alias, predicate), where alias is an alternative notation for the predicate.
_quantifiers :: [(Text, Text)]
List of quantifiers, consisting of (alias, quantifier), where alias is an alternative notation for the quantifier.
_functionSymbols :: Map Text (Int, Pos)
Collected function symbols consisting of
- name :: Text
- arity :: Int
- first occurence :: Pos
_predicateSymbols :: Map Text (Int, Pos)
Collected predicate symbols consisting of
- name :: Text
- arity :: Int
- first occurence :: Pos
_rules :: [(Name, RuleSpec)]
A map that contains all rules, mapping their Name to their RuleSpec.
_uri :: URI
URI of the application.
_logic :: Logic
Logic that the app currently uses.
_currentTooltip :: Maybe MisoString
id of the currently opened tooltip
_onMobile :: Bool
Responds to the current viewport, True if viewport is small (on mobile)

Instances

Instances details

Eq Model Source #
Instance details Defined in App.Model Methods (==) :: Model -> Model -> Bool # (/=) :: Model -> Model -> Bool #

initialModel Source #

Arguments

:: Derivation	Empty `Derivation`, used for inserting `Assumption`s, `Derivation`s and `Proof`s.
-> Proof	Initial `Proof`.
-> [(Text, Proof)]	Example `Proof`s.
-> [(Text, Text, Int)]	A list of operators (alias, operator, arity)
-> [(Text, Text)]	A list of quantifiers (alias, quantifier)
-> [(Text, Text)]	A list of infix predicates (alias, predicate)
-> [(Name, RuleSpec)]	The map of rules
-> URI	The current `URI`
-> Logic	Logic that the app uses.
-> Maybe Bool	Initial state of onMobile
-> Bool	Possibly a previous sidebarToggle state.
-> Model	Initial `Model` with sensible defaults