mirror of
https://github.com/marcosh/crem.git
synced 2024-10-05 16:30:15 +03:00
use single-line Haddock comments
This commit is contained in:
parent
b9a99914cc
commit
7999a60a43
@ -0,0 +1,27 @@
|
||||
name: Use single line haddock comments
|
||||
date: 2023-01-12
|
||||
context: >
|
||||
We would like to document the project extensively, creating proper
|
||||
documentation for all datatypes and functions defined in the project.
|
||||
|
||||
Hence we would like to use as much as possible
|
||||
[Haddock](https://haskell-haddock.readthedocs.io)-style comments. Haddock
|
||||
supports two styles of comments:
|
||||
|
||||
- single-line: `-- |`
|
||||
|
||||
- multi-line: `{- |`
|
||||
|
||||
Moreover we would like to use `doctests` to properly check the examples
|
||||
included in the Haddock documentation. Such examples are defined using the
|
||||
`>>>` syntax inside Haddock comments.
|
||||
|
||||
The [Haskell Language Server](https://haskell-language-server.readthedocs.io)
|
||||
allows to execute directly examples defined with the `>>>` syntax inside any
|
||||
kind (i.e. not necessarily Haddock ones) on single-line comments.
|
||||
decision: >
|
||||
We will use single-line comments so that examples can be executed by HLS and
|
||||
recognised as doctests
|
||||
consequences: >
|
||||
We configure [Fourmolu](https://github.com/fourmolu/fourmolu) to use
|
||||
single-line comments and use it to enforce this style.
|
11
decision-log/README.md
Normal file
11
decision-log/README.md
Normal file
@ -0,0 +1,11 @@
|
||||
# Decision log
|
||||
|
||||
A [decision log](https://adr.github.io/) is a collection of records to document the decisions which were taken during the development of the project.
|
||||
|
||||
Every record is described in a `yaml` file with the `{year}-{month}-{day}-{name}` format inside this folder and will contain at least the following fields:
|
||||
|
||||
- name
|
||||
- date
|
||||
- context
|
||||
- decision
|
||||
- consequences
|
@ -5,8 +5,8 @@ import-export-style: leading
|
||||
indent-wheres: true
|
||||
record-brace-space: true
|
||||
newlines-between-decls: 1
|
||||
haddock-style: multi-line
|
||||
haddock-style-module: multi-line
|
||||
haddock-style: single-line
|
||||
haddock-style-module: single-line
|
||||
let-style: auto
|
||||
in-style: right-align
|
||||
unicode: never
|
||||
|
@ -8,12 +8,11 @@ import "profunctors" Data.Profunctor (Profunctor (..), Strong (..))
|
||||
|
||||
-- * Specifying state machines
|
||||
|
||||
{- | A `BaseMachine topology input output` describes a state machine with
|
||||
allowed transitions constrained by a given `topology`.
|
||||
A state machine is composed by an `initialState` and an `action`, which
|
||||
defines the `output` and the new `state` given the current `state` and an
|
||||
`input`
|
||||
-}
|
||||
-- | A `BaseMachine topology input output` describes a state machine with
|
||||
-- allowed transitions constrained by a given `topology`.
|
||||
-- A state machine is composed by an `initialState` and an `action`, which
|
||||
-- defines the `output` and the new `state` given the current `state` and an
|
||||
-- `input`
|
||||
data
|
||||
BaseMachine
|
||||
(topology :: Topology vertex)
|
||||
@ -58,17 +57,15 @@ instance Strong (BaseMachine topology) where
|
||||
, action = \state (c, a) -> (c,) <$> action state a
|
||||
}
|
||||
|
||||
{- | A value of type `InitialState state` describes the initial state of a
|
||||
state machine, describing the initial `vertex` in the `topology` and the
|
||||
actual initial data of type `state vertex`
|
||||
-}
|
||||
-- | A value of type `InitialState state` describes the initial state of a
|
||||
-- state machine, describing the initial `vertex` in the `topology` and the
|
||||
-- actual initial data of type `state vertex`
|
||||
data InitialState (state :: vertex -> Type) where
|
||||
InitialState :: state vertex -> InitialState state
|
||||
|
||||
{- | The result of an action of the state machine.
|
||||
An `ActionResult topology state initialVertex output` contains an `output` and a `state finalVertex`,
|
||||
where the transition from `initialVertex` to `finalVertex` is allowed by the machine `topology`
|
||||
-}
|
||||
-- | The result of an action of the state machine.
|
||||
-- An `ActionResult topology state initialVertex output` contains an `output` and a `state finalVertex`,
|
||||
-- where the transition from `initialVertex` to `finalVertex` is allowed by the machine `topology`
|
||||
data
|
||||
ActionResult
|
||||
(topology :: Topology vertex)
|
||||
|
@ -6,14 +6,13 @@ module CRM.Graph where
|
||||
newtype Graph a = Graph [(a, a)]
|
||||
deriving stock (Eq, Show)
|
||||
|
||||
{- | The product graph.
|
||||
It has as vertices the product of the set of vertices of the initial graph.
|
||||
It has as edge from `(a1, b1)` to `(a2, b2)` if and only if there is an edge
|
||||
from `a1` to `a2` and an edge from `b1` to `b2`
|
||||
|
||||
>>> productGraph (Graph [('a', 'b')]) (Graph [('c', 'd')])
|
||||
Graph [(('a','c'),('b','d'))]
|
||||
-}
|
||||
-- | The product graph.
|
||||
-- It has as vertices the product of the set of vertices of the initial graph.
|
||||
-- It has as edge from `(a1, b1)` to `(a2, b2)` if and only if there is an edge
|
||||
-- from `a1` to `a2` and an edge from `b1` to `b2`
|
||||
--
|
||||
-- >>> productGraph (Graph [('a', 'b')]) (Graph [('c', 'd')])
|
||||
-- Graph [(('a','c'),('b','d'))]
|
||||
productGraph :: Graph a -> Graph b -> Graph (a, b)
|
||||
productGraph (Graph edges1) (Graph edges2) =
|
||||
Graph $
|
||||
|
@ -24,9 +24,8 @@ topologyAsGraph (Topology edges) = Graph $ edges >>= edgify
|
||||
edgify :: (v, [v]) -> [(v, v)]
|
||||
edgify (v, vs) = (v,) <$> vs
|
||||
|
||||
{- | Interpret a `BaseMachine` as a `Graph` using the information contained in
|
||||
its topology
|
||||
-}
|
||||
-- | Interpret a `BaseMachine` as a `Graph` using the information contained in
|
||||
-- its topology
|
||||
baseMachineAsGraph
|
||||
:: forall vertex topology input output
|
||||
. (Demote (Topology vertex) ~ Topology vertex, SingKind vertex, SingI topology)
|
||||
@ -38,9 +37,8 @@ baseMachineAsGraph _ = topologyAsGraph (demote @topology)
|
||||
renderUntypedMermaid :: UntypedGraph -> Text
|
||||
renderUntypedMermaid (UntypedGraph graph) = renderMermaid graph
|
||||
|
||||
{- | Interpret a `StateMachine` as an `UntypedGraph` using the information
|
||||
contained in its structure and in the topology of its basic components
|
||||
-}
|
||||
-- | Interpret a `StateMachine` as an `UntypedGraph` using the information
|
||||
-- contained in its structure and in the topology of its basic components
|
||||
machineAsGraph :: StateMachine input output -> UntypedGraph
|
||||
machineAsGraph (Basic baseMachine) =
|
||||
UntypedGraph (baseMachineAsGraph baseMachine)
|
||||
|
@ -8,11 +8,8 @@ import CRM.Topology
|
||||
import "profunctors" Data.Profunctor (Profunctor (..), Strong (..))
|
||||
import "singletons-base" Data.Singletons (Demote, SingI, SingKind)
|
||||
|
||||
-- import "base" Control.Category (Category (..))
|
||||
|
||||
{- | A `StateMachine` is a [Mealy machine](https://en.wikipedia.org/wiki/Mealy_machine)
|
||||
with inputs of type `input` and outputs of type `output`
|
||||
-}
|
||||
-- | A `StateMachine` is a [Mealy machine](https://en.wikipedia.org/wiki/Mealy_machine)
|
||||
-- with inputs of type `input` and outputs of type `output`
|
||||
data StateMachine input output where
|
||||
Basic
|
||||
:: forall vertex (topology :: Topology vertex) input output
|
||||
|
@ -13,9 +13,8 @@ import "singletons-base" Data.Singletons.Base.TH (singletons)
|
||||
|
||||
-- * Topology
|
||||
|
||||
{- | A `Topology` is a description of the topology of a state machine
|
||||
It contains the collection of allowed transitions
|
||||
-}
|
||||
-- | A `Topology` is a description of the topology of a state machine
|
||||
-- It contains the collection of allowed transitions
|
||||
$( singletons
|
||||
[d|
|
||||
newtype Topology vertex = Topology {edges :: [(vertex, [vertex])]}
|
||||
@ -24,23 +23,19 @@ $( singletons
|
||||
|
||||
-- ** AllowedTransition
|
||||
|
||||
{- | We expose at the type level the information contained in the topology
|
||||
An instance of `AllowedTransition topology initial final` means that the
|
||||
`topology` allows transitions from the`initial` to the `final` state
|
||||
-}
|
||||
-- | We expose at the type level the information contained in the topology
|
||||
-- An instance of `AllowedTransition topology initial final` means that the
|
||||
-- `topology` allows transitions from the`initial` to the `final` state
|
||||
class AllowedTransition (topology :: Topology vertex) (initial :: vertex) (final :: vertex)
|
||||
|
||||
{- | If `a` is the start and `b` is the end of the first edge,
|
||||
then `map` contains an edge from `a` to `b`
|
||||
-}
|
||||
-- | If `a` is the start and `b` is the end of the first edge,
|
||||
-- then `map` contains an edge from `a` to `b`
|
||||
instance {-# OVERLAPPING #-} AllowedTransition ('Topology ('(a, b : l1) : l2)) a b
|
||||
|
||||
{- | If we know that we have an edge from `a` to `b` in `map`,
|
||||
then we also have an edge from `a` to `b` if we add another edge out of `a`
|
||||
-}
|
||||
-- | If we know that we have an edge from `a` to `b` in `map`,
|
||||
-- then we also have an edge from `a` to `b` if we add another edge out of `a`
|
||||
instance {-# OVERLAPPING #-} AllowedTransition ('Topology ('(a, l1) : l2)) a b => AllowedTransition ('Topology ('(a, x : l1) : l2)) a b
|
||||
|
||||
{- | If we know that we have an edge from `a` to `b` in `map`,
|
||||
then we also have an edge from `a` to `b` if we add another vertex
|
||||
-}
|
||||
-- | If we know that we have an edge from `a` to `b` in `map`,
|
||||
-- then we also have an edge from `a` to `b` if we add another vertex
|
||||
instance AllowedTransition ('Topology map) a b => AllowedTransition ('Topology (x : map)) a b
|
||||
|
Loading…
Reference in New Issue
Block a user