diff --git a/cardano-api/cardano-api.cabal b/cardano-api/cardano-api.cabal index c6805f78b0..3c4def9527 100644 --- a/cardano-api/cardano-api.cabal +++ b/cardano-api/cardano-api.cabal @@ -205,7 +205,6 @@ library internal , typed-protocols ^>= 0.1 , unordered-containers >= 0.2.11 , vector - , world-peace , yaml library diff --git a/cardano-api/internal/Cardano/Api/Eon/Core.hs b/cardano-api/internal/Cardano/Api/Eon/Core.hs index fc648a5f42..c74b183524 100644 --- a/cardano-api/internal/Cardano/Api/Eon/Core.hs +++ b/cardano-api/internal/Cardano/Api/Eon/Core.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} @@ -7,17 +8,11 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} module Cardano.Api.Eon.Core where import Data.Kind -import Data.WorldPeace - -data Eon (eras :: [Type]) era where - Eon - :: IsMember era eras - => OpenUnion eras - -> Eon eras era data Byron = Byron deriving (Eq, Show) data Shelley = Shelley deriving (Eq, Show) @@ -27,13 +22,13 @@ data Alonzo = Alonzo deriving (Eq, Show) data Babbage = Babbage deriving (Eq, Show) data Conway = Conway deriving (Eq, Show) -type ByronEraOnly = '[Byron ] -type ShelleyEraOnly = '[ Shelley ] -type AllegraEraOnly = '[ Allegra ] -type MaryEraOnly = '[ Mary ] -type AlonzoEraOnly = '[ Alonzo ] -type BabbageEraOnly = '[ Babbage ] -type ConwayEraOnly = '[ Conway] +type ByronOnly = '[Byron ] +type ShelleyOnly = '[ Shelley ] +type AllegraOnly = '[ Allegra ] +type MaryOnly = '[ Mary ] +type AlonzoOnly = '[ Alonzo ] +type BabbageOnly = '[ Babbage ] +type ConwayOnly = '[ Conway] type ByronEraOnwards = '[Byron, Shelley, Allegra, Mary, Alonzo, Babbage, Conway] type ShelleyEraOnwards = '[ Shelley, Allegra, Mary, Alonzo, Babbage, Conway] @@ -43,21 +38,140 @@ type AlonzoEraOnwards = '[ Alonzo, Babbage, Conw type BabbageEraOnwards = '[ Babbage, Conway] type ConwayEraOnwards = '[ Conway] -relaxEon :: () - => Contains as bs - => IsMember a bs -- This constraing shouldn't be needed - => Eon as a - -> Eon bs a -relaxEon (Eon a) = Eon (relaxOpenUnion a) +type ByronToBabbage = '[Byron, Shelley, Allegra, Mary, Alonzo, Babbage] +type ShelleyToBabbage = '[ Shelley, Allegra, Mary, Alonzo, Babbage] +type AllegraToBabbage = '[ Allegra, Mary, Alonzo, Babbage] +type MaryToBabbage = '[ Mary, Alonzo, Babbage] +type AlonzoToBabbage = '[ Alonzo, Babbage] + +type ByronToAlonzo = '[Byron, Shelley, Allegra, Mary, Alonzo] +type ShelleyToAlonzo = '[ Shelley, Allegra, Mary, Alonzo] +type AllegraToAlonzo = '[ Allegra, Mary, Alonzo] +type MaryToAlonzo = '[ Mary, Alonzo] + +type ByronToMary = '[Byron, Shelley, Allegra, Mary] +type ShelleyToMary = '[ Shelley, Allegra, Mary] +type AllegraToMary = '[ Allegra, Mary] + +type ByronToAllegra = '[Byron, Shelley, Allegra] +type ShelleyToAllegra = '[ Shelley, Allegra] + +type ByronToShelley = '[Byron, Shelley] + +data Elem t where + Elem :: Elem t + +data (∈) (a :: Type) (as :: [Type]) where + MemberHead :: a ∈ (a ': as) + MemberTail :: a ∈ as -> a ∈ (b ': as) + +data (⊆) (as :: [Type]) (bs :: [Type]) where + SubsetCons + :: a ∈ bs + -> as ⊆ bs + -> (a:as) ⊆ bs + + SubsetNil + :: '[] ⊆ bs + +data Eon (eras :: [Type]) era where + Eon + :: era ∈ eras + -> era + -> Eon eras era + +-- relaxEon :: () +-- => as ⊆ bs +-- -> Eon as a +-- -> Eon bs a +-- relaxEon subsetProof (Eon membership era) = +-- case membership of +-- MemberHead -> +-- case subsetProof of +-- SubsetCons Elem subsetProofRest -> +-- Eon _u era example1 :: () - => IsMember era ByronEraOnwards -- These constraints are due to relaxEon. They shouldn't be needed. - => Eon ByronEraOnwards era - -> Eon ByronEraOnwards era -example1 = relaxEon + => Eon ConwayEraOnwards era + -> Eon ConwayEraOnwards era +example1 (Eon m era) = Eon m era example2 :: () - => IsMember era ByronEraOnwards -- These constraints are due to relaxEon. They shouldn't be needed. - => Eon ShelleyEraOnwards era - -> Eon ByronEraOnwards era -example2 = relaxEon + => Eon ConwayEraOnwards era + -> Eon BabbageEraOnwards era +example2 (Eon m era) = + case m of + MemberHead -> Eon (MemberTail MemberHead) era + MemberTail m' -> case m' of {} + +example3 :: () + => Eon ConwayEraOnwards era + -> Eon AlonzoEraOnwards era +example3 (Eon m era) = + case m of + MemberHead -> Eon (MemberTail (MemberTail MemberHead)) era + MemberTail m' -> case m' of {} + +example4 :: () + => Eon ByronOnly era + -> Eon ByronToShelley era +example4 (Eon m era) = + case m of + MemberHead -> Eon MemberHead era + MemberTail m' -> case m' of {} + +example5 :: () + => Eon ShelleyOnly era + -> Eon ByronToAllegra era +example5 (Eon m era) = + case m of + MemberHead -> Eon (MemberTail MemberHead) era + MemberTail m' -> case m' of {} + +example6 :: () + => Eon ShelleyToAllegra era + -> Eon ByronToAllegra era +example6 (Eon m era) = + case m of + MemberHead -> Eon (MemberTail MemberHead) era + MemberTail MemberHead -> Eon (MemberTail (MemberTail MemberHead)) era + MemberTail (MemberTail m') -> case m' of {} + +example7 :: () + => ShelleyToAllegra ⊆ ByronToAllegra + -> Eon ShelleyToAllegra era + -> Eon ByronToAllegra era +example7 _ (Eon m era) = + case m of + MemberHead -> Eon (MemberTail MemberHead) era + MemberTail MemberHead -> Eon (MemberTail (MemberTail MemberHead)) era + MemberTail (MemberTail m') -> case m' of {} + +moo :: ShelleyToAllegra ⊆ ByronToAllegra -> () +moo p = case p of + SubsetCons _pShelley p' -> case p' of + SubsetCons _pAllegra p'' -> case p'' of + SubsetNil -> () + +example8 :: () + => ShelleyToAllegra ⊆ ByronToAllegra + -> Eon ShelleyToAllegra era + -> Eon ByronToAllegra era +example8 p (Eon m era) = + case m of + MemberHead -> + case p of + SubsetCons pShelley _ -> + Eon pShelley era + MemberTail MemberHead -> + case p of + SubsetCons _ p' -> case p' of + SubsetCons pAllegra _ -> Eon pAllegra era + MemberTail (MemberTail m') -> + case m' of {} + +-- example2 :: () +-- => IsMember era ByronEraOnwards -- These constraints are due to relaxEon. They shouldn't be needed. +-- => Eon ShelleyEraOnwards era +-- -> Eon ByronEraOnwards era +-- example2 = relaxEon