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

Jump to bottom

Added UPLC for untyped Plutus core, and smaller changes #16

Closed
wants to merge 1 commit into from
Closed

Added UPLC for untyped Plutus core, and smaller changes #16

Show file tree
Hide file tree
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
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
/dist-newstyle
cabal.project.local
46 changes: 30 additions & 16 deletions Plutarch/Core.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module Plutarch.Core (
EIfNewtype,
IsEType,
EConcrete,
EConcreteRepr,
EConstructable' (econImpl, ematchImpl),
EConstructable,
econ,
Expand All @@ -31,6 +32,7 @@ module Plutarch.Core (
EForall (EForall),
ESome (ESome),
EFix (EFix),
ELet (ELet),
EAny (EAny),
EPolymorphic,
ESOP,
Expand All @@ -40,6 +42,7 @@ module Plutarch.Core (
ELC,
unTerm,
elam,
elam2,
(#),
elet,
eunsafeCoerce,
Expand Down Expand Up @@ -87,16 +90,25 @@ import Plutarch.Reduce (NoReduce)
class EDSL (edsl :: EDSLKind) where
type IsEType' edsl :: ETypeRepr -> Constraint

type role Term nominal nominal
data Term (edsl :: EDSLKind) (a :: EType) where
Term :: {unTerm :: (EDSL edsl, IsEType' edsl (ERepr a)) => edsl (ERepr a)} -> Term edsl a
class (IsEType' edsl (ERepr a)) => IsEType (edsl :: EDSLKind) (a :: EType)
instance (IsEType' edsl (ERepr a)) => IsEType edsl a

type ClosedTerm (c :: EDSLKind -> Constraint) (a :: EType) = forall edsl. c edsl => Term edsl a
class (forall a. IsEType edsl a => IsEType edsl (f a)) => IsEType2 (edsl :: EDSLKind) (f :: EType -> EType)
instance (forall a. IsEType edsl a => IsEType edsl (f a)) => IsEType2 (edsl :: EDSLKind) (f :: EType -> EType)

type family Helper (edsl :: EDSLKind) :: ETypeF where
Helper edsl = MkETypeF (IsEType edsl) (Compose NoReduce (Term edsl))
type role Term representational nominal
type Term :: EDSLKind -> EType -> Type
newtype Term edsl a where
Term :: { unTerm :: edsl (ERepr a) } -> Term edsl a

type EConcrete (edsl :: EDSLKind) (a :: EType) = a (Helper edsl)
type ClosedTerm :: (EDSLKind -> Constraint) -> EType -> Type
type ClosedTerm c a = forall edsl. c edsl => Term edsl a

type Helper :: EDSLKind -> ETypeF
type Helper edsl = MkETypeF (IsEType edsl) (Compose NoReduce (Term edsl))

type EConcrete :: EDSLKind -> EType -> Type
type EConcrete edsl a = a (Helper edsl)

type EConcreteRepr (edsl :: EDSLKind) (a :: ETypeRepr) = EConcrete edsl (EReprAp a)

Expand All @@ -105,12 +117,6 @@ toERepr x = coerceERepr (Proxy @a) $ coerce x
fromERepr :: forall a edsl. EIsNewtype a => EConcreteRepr edsl (ERepr a) -> EConcrete edsl a
fromERepr x = coerceERepr (Proxy @a) $ coerce x

class (IsEType' edsl (ERepr a)) => IsEType (edsl :: EDSLKind) (a :: EType)
instance (IsEType' edsl (ERepr a)) => IsEType edsl a

class (forall a. IsEType edsl a => IsEType edsl (f a)) => IsEType2 (edsl :: EDSLKind) (f :: EType -> EType)
instance (forall a. IsEType edsl a => IsEType edsl (f a)) => IsEType2 (edsl :: EDSLKind) (f :: EType -> EType)

class (EDSL edsl, IsEType' edsl a) => EConstructable' edsl (a :: ETypeRepr) where
econImpl :: HasCallStack => EConcreteRepr edsl a -> edsl a

Expand All @@ -137,7 +143,8 @@ data EVoid ef
instance EIsNewtype EVoid where type EIsNewtype' _ = False

-- | Effects of `econ` are effects of the argument.
data ELet a ef = ELet (Ef ef a)
type ELet :: EType -> EType
newtype ELet a ef = ELet (Ef ef a)

instance EIsNewtype (ELet a) where type EIsNewtype' _ = False

Expand Down Expand Up @@ -166,7 +173,8 @@ instance EIsNewtype EAny where type EIsNewtype' _ = False
newtype EForall (constraint :: a -> Constraint) (b :: a -> EType) ef = EForall (forall (x :: a). constraint x => ef /$ b x)
instance EIsNewtype (EForall c ef) where type EIsNewtype' _ = False

data ESome (constraint :: a -> Constraint) (b :: a -> EType) ef = forall (x :: a). ESome (constraint x => ef /$ b x)
data ESome (constraint :: a -> Constraint) (b :: a -> EType) ef where
ESome :: (constraint x => ef /$ b x) -> ESome constraint b ef
instance EIsNewtype (ESome c ef) where type EIsNewtype' _ = False

newtype EFix f ef = EFix (ef /$ f (EFix f))
Expand All @@ -185,7 +193,13 @@ type ELC :: EDSLKind -> Constraint
type ELC edsl = forall a b. (IsEType edsl a, IsEType edsl b) => EConstructable edsl (a #-> b)

elam :: forall edsl a b. (HasCallStack, EConstructable edsl (a #-> b)) => (Term edsl a -> Term edsl b) -> Term edsl (a #-> b)
elam f = econ $ (ELam f :: EConcrete edsl (a #-> b))
elam body = econ $ (ELam body :: EConcrete edsl (a #-> b))

elam2 :: EConstructable edsl (a #-> b #-> c)
=> EConstructable edsl (b #-> c)
=> (Term edsl a -> Term edsl b -> Term edsl c)
-> Term edsl (a #-> (b #-> c))
elam2 body = elam \a -> elam \b -> body a b

(#) :: (HasCallStack, ELC edsl, IsEType edsl a, IsEType edsl b) => Term edsl (a #-> b) -> Term edsl a -> Term edsl b
(#) f x = ematch f (\(ELam f') -> f' x)
Expand Down
18 changes: 8 additions & 10 deletions Plutarch/EType.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ module Plutarch.EType (
import Data.Coerce (Coercible)
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy)
import Data.Type.Coercion (Coercion(..))
import Generics.SOP (Top)
import Plutarch.Reduce (NoReduce, Reduce)

Expand All @@ -44,8 +45,6 @@ data ETypeF = MkETypeF
-- | Higher HKD
type EType = ETypeF -> Type

type EDSLKind = ETypeRepr -> Type

type family Ef (f :: ETypeF) (x :: EType) :: Type where
Ef (MkETypeF _constraint concretise) x = Reduce (concretise x)

Expand All @@ -66,6 +65,8 @@ type EIfNewtype a = (EIsNewtype a, EIsNewtype' a ~ True)

newtype ETypeRepr = MkETypeRepr EType

type EDSLKind = ETypeRepr -> Type

type family EReprHelper (b :: Bool) (a :: EType) where
EReprHelper True a = ENewtype a
EReprHelper False a = a
Expand All @@ -76,9 +77,6 @@ type family EReprAp (a :: ETypeRepr) :: EType where
type ERepr :: EType -> ETypeRepr
type ERepr a = MkETypeRepr (EReprHelper (EIsNewtype' a) a)

data Dict :: Constraint -> Type where
Dict :: c => Dict c

-- FIXME replace with generic-singletons
data SBool :: Bool -> Type where
STrue :: SBool 'True
Expand All @@ -93,17 +91,17 @@ instance KnownBool 'True where
instance KnownBool 'False where
knownBool = SFalse

h :: Proxy a -> SBool b -> Dict (Coercible (EReprHelper b a) a)
h _ STrue = Dict
h _ SFalse = Dict
h :: Proxy a -> SBool b -> Coercion (EReprHelper b a) a
h _ STrue = Coercion
h _ SFalse = Coercion

g :: forall a. EIsNewtype a => Proxy a -> Dict (Coercible (EReprAp (ERepr a)) a)
g :: forall a. EIsNewtype a => Proxy a -> Coercion (EReprAp (ERepr a)) a
g p =
let _ = EHs' -- FIXME: Remove, -Wunused-top-binds is broken
in h p (knownBool :: SBool (EIsNewtype' a))

coerceERepr :: forall a b. EIsNewtype a => Proxy a -> (Coercible (EReprAp (ERepr a)) a => b) -> b
coerceERepr p f = case g p of Dict -> f
coerceERepr p f = case g p of Coercion -> f

type EHs' :: EType -> Type
type EHs (a :: EType) = a (MkETypeF Top EHs')
Expand Down
6 changes: 4 additions & 2 deletions Plutarch/Reduce.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@ import GHC.Generics

newtype NoReduce a = NoReduce a

type family GReduce (def :: Type) (rep :: Type -> Type) :: Type where
type GReduce :: Type -> (Type -> Type) -> Type
type family GReduce def rep where
-- newtype
GReduce _def (D1 ( 'MetaData _ _ _ 'True) (C1 _ (S1 _ (Rec0 (x :: Type))))) = Reduce x
-- data
Expand All @@ -26,7 +27,8 @@ type family GReduce (def :: Type) (rep :: Type -> Type) :: Type where
@
It is then true that @forall a. Reduce (F' a) ~ F a@.
-}
type family Reduce (x :: Type) :: Type where
type Reduce :: Type -> Type
type family Reduce x where
Reduce (NoReduce a) = a
Reduce (a -> b) = a -> b
Reduce x = GReduce x (Rep x)
Expand Down
Loading