Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Builtins] Unfold 'geq' for the default universe #4463

Closed
wants to merge 1 commit into from
Closed

[Builtins] Unfold 'geq' for the default universe #4463

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
102 changes: 82 additions & 20 deletions plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,22 +2,26 @@

{-# OPTIONS -fno-warn-missing-pattern-synonym-signatures #-}

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- effectfully: to the best of my experimentation, -O2 here improves performance, however by
-- inspecting GHC Core I was only able to see a difference in how the 'KnownTypeIn' instance for
Expand All @@ -40,9 +44,11 @@ import Control.Applicative
import Data.ByteString qualified as BS
import Data.Int
import Data.IntCast (intCastEq)
import Data.Kind
import Data.Proxy
import Data.Text qualified as Text
import GHC.Exts (inline, oneShot)
import GHC.TypeNats
import Universe as Export

{- Note [PLC types and universes]
Expand Down Expand Up @@ -99,12 +105,68 @@ pattern DefaultUniList uniA =
pattern DefaultUniPair uniA uniB =
DefaultUniProtoPair `DefaultUniApply` uniA `DefaultUniApply` uniB

deriveGEq ''DefaultUni
deriveGCompare ''DefaultUni

-- | For pleasing the coverage checker.
noMoreTypeFunctions :: DefaultUni (Esc (f :: a -> b -> c -> d)) -> any
noMoreTypeFunctions (f `DefaultUniApply` _) = noMoreTypeFunctions f
data Peano = Z | S Peano

type family Pred (n :: Peano) :: Peano where
Pred 'Z = 'Z
Pred ('S n) = n

type family NatToPeano (n :: Nat) where
NatToPeano 0 = 'Z
NatToPeano n = 'S (NatToPeano (n - 1))

class UnfoldGEq (n :: Peano) f where
unfoldGeq :: f a -> f b -> Maybe (a :~: b)

instance UnfoldGEq 'Z DefaultUni where
unfoldGeq = unfoldGeq @('S 'Z)
{-# NOINLINE unfoldGeq #-}

type family Min n m where
Min ('S n) ('S m) = 'S (Min n m)
Min _ _ = 'Z

instance (UnfoldGEq n DefaultUni, UnfoldGEq (Min ('S 'Z) n) DefaultUni) =>
UnfoldGEq ('S n) DefaultUni where
DefaultUniInteger `unfoldGeq` DefaultUniInteger = Just Refl
DefaultUniByteString `unfoldGeq` DefaultUniByteString = Just Refl
DefaultUniString `unfoldGeq` DefaultUniString = Just Refl
DefaultUniUnit `unfoldGeq` DefaultUniUnit = Just Refl
DefaultUniBool `unfoldGeq` DefaultUniBool = Just Refl
DefaultUniProtoList `unfoldGeq` DefaultUniProtoList = Just Refl
DefaultUniProtoPair `unfoldGeq` DefaultUniProtoPair = Just Refl
DefaultUniApply f1 a1 `unfoldGeq` DefaultUniApply f2 a2 = do
Refl <- unfoldGeq @n f1 f2
Refl <- unfoldGeq @(Min ('S 'Z) n) a1 a2
Just Refl
DefaultUniData `unfoldGeq` DefaultUniData = Just Refl
_ `unfoldGeq` _ = Nothing
{-# INLINE unfoldGeq #-}

type MaxApplyDepth = NatToPeano 3

instance GEq DefaultUni where
geq = unfoldGeq @MaxApplyDepth
{-# INLINE geq #-}

type GreaterThanOrEqualTo :: Peano -> Peano -> Constraint
type family m `GreaterThanOrEqualTo` n where
'S m `GreaterThanOrEqualTo` 'S n = m `GreaterThanOrEqualTo` n
_ `GreaterThanOrEqualTo` 'Z = ()

type CountArgs :: forall k. k -> Peano
type family CountArgs a where
CountArgs (a -> b) = 'S (CountArgs b)
CountArgs _ = 'Z

class CountArgs k `GreaterThanOrEqualTo` MaxApplyDepth => NoMoreTypeFunctions (f :: k) where
-- | For pleasing the coverage checker.
noMoreTypeFunctions :: DefaultUni (Esc f) -> any

instance NoMoreTypeFunctions (f :: a -> b -> c -> d) where
noMoreTypeFunctions (f `DefaultUniApply` _) = noMoreTypeFunctions f

instance ToKind DefaultUni where
toSingKind DefaultUniInteger = knownKind
Expand Down