mirror of
https://github.com/simplex-chat/simplex-chat.git
synced 2026-08-29 07:38:54 +00:00
move extensions to code
This commit is contained in:
@@ -19,45 +19,11 @@ ghc-options:
|
||||
- -Wincomplete-uni-patterns
|
||||
|
||||
default-extensions:
|
||||
- TemplateHaskell
|
||||
- NoImplicitPrelude
|
||||
# numbers, strings, lists
|
||||
- NegativeLiterals
|
||||
- NumericUnderscores
|
||||
- OverloadedStrings
|
||||
# function syntax
|
||||
- BlockArguments
|
||||
- EmptyCase
|
||||
- LambdaCase
|
||||
# Records
|
||||
- DuplicateRecordFields
|
||||
- NamedFieldPuns
|
||||
- NoImplicitPrelude
|
||||
- OverloadedStrings
|
||||
- RecordWildCards
|
||||
# deriving
|
||||
- DeriveAnyClass
|
||||
- DeriveFunctor
|
||||
- DeriveGeneric
|
||||
- StandaloneDeriving
|
||||
# type classes
|
||||
- FunctionalDependencies
|
||||
- FlexibleContexts
|
||||
- FlexibleInstances
|
||||
- InstanceSigs
|
||||
- TypeSynonymInstances
|
||||
- UndecidableInstances
|
||||
# types
|
||||
- DataKinds
|
||||
- ConstraintKinds
|
||||
- GADTs
|
||||
- KindSignatures
|
||||
- LiberalTypeSynonyms
|
||||
- NoStarIsType
|
||||
- PolyKinds
|
||||
- RankNTypes
|
||||
- ScopedTypeVariables
|
||||
- TypeApplications
|
||||
- TypeFamilies
|
||||
- TypeOperators
|
||||
|
||||
dependencies:
|
||||
- aeson
|
||||
|
||||
@@ -1,4 +1,15 @@
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE NoStarIsType #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
module Simplex.Messaging.Protocol where
|
||||
|
||||
@@ -30,11 +41,11 @@ data BrokerCS :: ConnectionState -> Type where
|
||||
BrkDrained :: BrokerCS 'Drained
|
||||
BrkNone :: BrokerCS 'None
|
||||
|
||||
instance Auto (TyPred BrokerCS) 'New where auto = BrkNew
|
||||
instance Auto (TyPred BrokerCS) 'Secured where auto = BrkSecured
|
||||
instance Auto (TyPred BrokerCS) 'Disabled where auto = BrkDisabled
|
||||
instance Auto (TyPred BrokerCS) 'Drained where auto = BrkDrained
|
||||
instance Auto (TyPred BrokerCS) 'None where auto = BrkNone
|
||||
instance Auto (TyPred BrokerCS) 'New where auto = autoTC
|
||||
instance Auto (TyPred BrokerCS) 'Secured where auto = autoTC
|
||||
instance Auto (TyPred BrokerCS) 'Disabled where auto = autoTC
|
||||
instance Auto (TyPred BrokerCS) 'Drained where auto = autoTC
|
||||
instance Auto (TyPred BrokerCS) 'None where auto = autoTC
|
||||
|
||||
-- sender connection states
|
||||
data SenderCS :: ConnectionState -> Type where
|
||||
@@ -43,10 +54,10 @@ data SenderCS :: ConnectionState -> Type where
|
||||
SndSecured :: SenderCS 'Secured
|
||||
SndNone :: SenderCS 'None
|
||||
|
||||
instance Auto (TyPred SenderCS) 'New where auto = SndNew
|
||||
instance Auto (TyPred SenderCS) 'Confirmed where auto = SndConfirmed
|
||||
instance Auto (TyPred SenderCS) 'Secured where auto = SndSecured
|
||||
instance Auto (TyPred SenderCS) 'None where auto = SndNone
|
||||
instance Auto (TyPred SenderCS) 'New where auto = autoTC
|
||||
instance Auto (TyPred SenderCS) 'Confirmed where auto = autoTC
|
||||
instance Auto (TyPred SenderCS) 'Secured where auto = autoTC
|
||||
instance Auto (TyPred SenderCS) 'None where auto = autoTC
|
||||
|
||||
-- allowed participant connection states
|
||||
data HasState (p :: Participant) (s :: ConnectionState) :: Type where
|
||||
@@ -54,7 +65,7 @@ data HasState (p :: Participant) (s :: ConnectionState) :: Type where
|
||||
BrkHasState :: Prf1 BrokerCS s => HasState 'Broker s
|
||||
SndHasState :: Prf1 SenderCS s => HasState 'Sender s
|
||||
|
||||
class Prf p a s where auto' :: p a s
|
||||
class Prf t p s where auto' :: t p s
|
||||
instance Prf HasState 'Recipient s
|
||||
where auto' = RcpHasState
|
||||
instance Prf1 BrokerCS s => Prf HasState 'Broker s
|
||||
|
||||
@@ -1,4 +1,7 @@
|
||||
{-# OPTIONS_GHC -fno-warn-orphans #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
|
||||
module Simplex.Messaging.ServerAPI
|
||||
( ServerAPI
|
||||
|
||||
@@ -0,0 +1,63 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE EmptyCase #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE InstanceSigs #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
{-# OPTIONS_GHC -Wall #-}
|
||||
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
|
||||
|
||||
module Simplex.Messaging.Test where
|
||||
|
||||
import ClassyPrelude
|
||||
|
||||
import Data.Kind
|
||||
import Data.Singletons()
|
||||
import Data.Singletons.TH
|
||||
import Data.Type.Predicate
|
||||
import Data.Type.Predicate.Auto
|
||||
|
||||
$(singletons [d|
|
||||
data Participant = Recipient | Broker | Sender
|
||||
|
||||
data ConnectionState = New -- (participants: all) connection created (or received from sender)
|
||||
| Pending -- (recipient) sent to sender out-of-band
|
||||
| Confirmed -- (recipient) confirmed by sender with the broker
|
||||
| Secured -- (all) secured with the broker
|
||||
|])
|
||||
|
||||
-- broker connection states
|
||||
data BrokerCS :: ConnectionState -> Type where
|
||||
BrkNew :: BrokerCS 'New
|
||||
BrkSecured :: BrokerCS 'Secured
|
||||
|
||||
instance Auto (TyPred BrokerCS) 'New where auto = autoTC
|
||||
instance Auto (TyPred BrokerCS) 'Secured where auto = autoTC
|
||||
|
||||
data RBState (rs :: ConnectionState) (bs :: ConnectionState) :: Type where
|
||||
RBState :: Auto (TyPred BrokerCS) bs
|
||||
=> Sing rs -> Sing bs -> RBState rs bs
|
||||
|
||||
data Box a = Num a => Box a
|
||||
|
||||
goodBoxSample :: Box Int
|
||||
goodBoxSample = Box 1
|
||||
|
||||
-- badBoxSample :: Box String
|
||||
-- badBox = Box "foo"
|
||||
|
||||
goodSt :: RBState 'New 'New
|
||||
goodSt = RBState SNew SNew
|
||||
|
||||
-- badSt :: RBState 'Pending 'Pending
|
||||
-- badSt = RBState SPending SPending
|
||||
@@ -1,3 +1,6 @@
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
|
||||
module Simplex.Messaging.Types where
|
||||
|
||||
import ClassyPrelude
|
||||
|
||||
Reference in New Issue
Block a user