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.Update

Contents

Update loop
Effects
Parsing

Description

The update loop of the application, basically all of its logic.

Synopsis

updateModel :: Action -> Effect ROOT Model Action
updateProof :: Effect ROOT Model Action
updateTitle :: Effect ROOT Model Action
checkProof :: MonadState Model m => m ()
clearDrag :: Effect ROOT Model Action
readURI :: URI -> Effect ROOT Model Action
pushProofURI :: Effect ROOT Model Action
replaceInitialURI :: Effect ROOT Model Action
proofReparse :: Effect ROOT Model Action
naReparseLine :: NodeAddr -> Effect ROOT Model Action
dropBeforeLine :: NodeAddr -> Effect ROOT Model Action
setFocus :: Either NodeAddr NodeAddr -> Effect ROOT Model Action
showTooltip :: MisoString -> Effect ROOT Model Action
hideTooltip :: Effect ROOT Model Action
toggleSidebar :: Effect ROOT Model Action
class FromText a where
- fromText :: Model -> Int -> Text -> Either Text a
tryParse :: FromText a => Model -> Int -> Text -> Wrapper a
reparse :: FromText a => Model -> Int -> Wrapper a -> Wrapper a
reparseProof :: Model -> Proof -> Proof

Update loop

updateModel :: Action -> Effect ROOT Model Action Source #

Main execution loop of the application.

Effects

updateProof :: Effect ROOT Model Action Source #

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

Should be called after every change to the Proof.

updateTitle :: Effect ROOT Model Action Source #

Updates the document.title to show how many errors there are and what the conclusion of the Proof is.

checkProof :: MonadState Model m => m () Source #

Runs the Proof verification algorithm, i.e.

Checks that symbols only occur with the same arity
Checks freshness Assumptions
Verifies all RuleApplications.

clearDrag :: Effect ROOT Model Action Source #

To be called after dragging ends, resets all drag parameters.

readURI :: URI -> Effect ROOT Model Action Source #

Takes a URI and reads in a proof if it contains one.

pushProofURI :: Effect ROOT Model Action Source #

Pushes a new URI that has the Proof encoded to the history stack.

See static/Navigation.js for the used pushStateHistory function.

replaceInitialURI :: Effect ROOT Model Action Source #

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

See static/Navigation.js for the used initHistory function.

proofReparse :: Effect ROOT Model Action Source #

Re-parses every line of the current Proof

naReparseLine :: NodeAddr -> Effect ROOT Model Action Source #

Re-parses a single Derivation or Assumption.

dropBeforeLine :: NodeAddr -> Effect ROOT Model Action Source #

Move or create a Assumption, Derivation or Proof before a given NodeAddr.

setFocus :: Either NodeAddr NodeAddr -> Effect ROOT Model Action Source #

Set focus to a input field specified by a NodeAddr (either the Formula or the RuleApplication).

showTooltip :: MisoString -> Effect ROOT Model Action Source #

Show the popover with the given id.

hideTooltip :: Effect ROOT Model Action Source #

Hide the popover with the given id.

toggleSidebar :: Effect ROOT Model Action Source #

Flip the sidebar state and save it in sessionStorage

Parsing

class FromText a where Source #

Class for parsing Text

Methods

fromText :: Model -> Int -> Text -> Either Text a Source #

Takes a Model and some Text and tries to parse it to the desired type. On failure returns an error message.

Instances

Instances details

FromText RawAssumption Source #
Instance details Defined in App.Update Methods fromText :: Model -> Int -> Text -> Either Text RawAssumption Source #
FromText RawFormula Source #
Instance details Defined in App.Update Methods fromText :: Model -> Int -> Text -> Either Text RawFormula Source #
FromText RuleApplication Source #
Instance details Defined in App.Update Methods fromText :: Model -> Int -> Text -> Either Text RuleApplication Source #

tryParse Source #

Arguments

:: FromText a
=> Model	The `Model`.
-> Int	Line number.
-> Text	Text to parse.
-> Wrapper a	Parse result.

Wrapper for fromText that also takes a list of aliases and tries to replace these aliases in the Text

reparse Source #

Arguments

:: FromText a
=> Model	The `Model`.
-> Int	The line number.
-> Wrapper a	The `Wrapper` to re-parse.
-> Wrapper a	Parse result.

Takes some Wrapper and re-parses it.

reparseProof :: Model -> Proof -> Proof Source #

Uses reparse to re-parse the whole Proof.