Merge branch 'master' into ari/optics

Examples/DataKinds.hs

@@ -1,10 +1,8 @@
 module Examples.DataKinds where
 
 import Data.Kind (Type)
-import GHC.Generics (Generic)
-import Plutarch.Core
-import Plutarch.EType
-import Plutarch.Experimental
+import Plutarch.Experimental (EEq)
+import Plutarch.Prelude
 
 data Nat = N | S Nat
 data SNat :: Nat -> Type where
@@ -13,8 +11,10 @@ data SNat :: Nat -> Type where
 
 data EBool ef = EFalse | ETrue
   deriving stock (Generic)
-  deriving anyclass (EIsNewtype)
+instance EHasRepr EBool where type EReprSort _ = EReprSOP
 
 data ESBool (b :: EHs EBool) ef
   = ESFalse (ef /$ EEq b EFalse)
   | ESTrue (ef /$ EEq b ETrue)
+  deriving stock (Generic)
+instance EHasRepr (ESBool b) where type EReprSort _ = EReprSOP

Examples/DataKinds2.hs

@@ -0,0 +1,31 @@
+module Examples.DataKinds2 (F' (..)) where
+
+import Plutarch.Prelude
+
+data EProxy (x :: EHs a) ef = EProxy
+  deriving stock (Generic)
+instance EHasRepr (EProxy x) where type EReprSort _ = EReprSOP
+
+newtype EIdentity a ef = EIdentity (ef /$ a)
+  deriving stock (Generic)
+instance EHasRepr (EIdentity a) where type EReprSort _ = EReprSOP
+
+newtype F' a x ef = F' (ef /$ EProxy x #-> EUnit)
+
+{-
+newtype F (a :: EType) ef = F (ef /$ EForall (F' a))
+
+f :: EForall F
+f = econ $ EForall $$ F $$ EForall $$ F' $ elam \_ -> econ EUnit
+
+--g :: Proxy x -> ()
+--g (Proxy @x) = f (Proxy @(Identity x))
+
+g :: EForall F
+g = econ $ EForall $$ F $$ EForall $$ F' $ elam \(x :: Term edsl (EProxy x)) ->
+  ematch f \EForall f ->
+  ematch f \F f ->
+  ematch f \EForall f ->
+  ematch f \F' f ->
+  f # (econ EProxy :: Term edsl (EProxy ('EIdentity x)))
+-}

Examples/Simple.hs

@@ -1,57 +1,39 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module Examples.Simple where
+module Examples.Simple (eid_alt, eid, efalse) where
 
-import Data.Proxy (Proxy (Proxy))
-import GHC.Generics (Generic)
-import Plutarch.Core
-import Plutarch.EType
+import Plutarch.Core (ELC, EPolymorphic, ESOP)
+import Plutarch.Prelude
 
 type ESystemF edsl = (ELC edsl, EPolymorphic edsl, ESOP edsl)
 
 data EBool ef = ETrue | EFalse
   deriving stock (Generic)
-  deriving anyclass (EIsNewtype)
+instance EHasRepr EBool where type EReprSort _ = EReprSOP
 
-newtype EForall1 (f :: EType -> EType) ef = EForall1 (Ef ef (EForall (IsEType (UnEf ef)) f))
+newtype EId' a ef = EId' (ef /$ (a #-> a))
   deriving stock (Generic)
-  deriving anyclass (EIsNewtype)
+instance EHasRepr (EId' a) where type EReprSort _ = EReprSOP
 
-newtype EId' a ef = EId' (Ef ef (a #-> a))
-newtype EId ef = EId (Ef ef (EForall1 EId'))
-
-type U0 = EUnit
-type U1 = EEither U0 U0
-type U2 = EEither U1 U1
-type U3 = EEither U2 U2
-type U4 = EEither U3 U3
-type U5 = EEither U4 U4
-type U6 = EEither U5 U5
-type U7 = EEither U6 U6
-type U8 = EEither U7 U7
-
-type Word = U8
-
-f :: ESOP edsl => Term edsl U1 -> Term edsl U0
-f x = ematch x \case
-  ERight EUnit -> econ EUnit
-  ELeft EUnit -> econ EUnit
-
-{-
+newtype EId ef = EId (ef /$ EForall EId')
+  deriving stock (Generic)
+instance EHasRepr EId where type EReprSort _ = EReprSOP
 
-f :: Functor f => f Bool -> f Bool
-f x = not <$> x
+efalse :: ESystemF edsl => Term edsl EBool
+efalse = econ EFalse
 
---newtype EMap f a b ef = EMap (Ef ef (f a #-> f b))
+eid''' :: (ESystemF edsl, IsEType edsl a) => Term edsl $ a #-> a
+eid''' = elam \x -> x
 
---newtype EMap' a b ef = EMap (EForall (IsEType2 edsl) )
+eid'' :: (ESystemF edsl, IsEType edsl a) => Term edsl $ EId' a
+eid'' = econ $ EId' eid'''
 
-class EFunctor edsl f where
-  --emap :: Term edsl (EMap f)
+eid' :: ESystemF edsl => Term edsl (EForall EId')
+eid' = econ $ EForall eid''
 
-newtype A a f = A (Ef f (a EBool #-> a EBool))
+eid :: ESystemF edsl => Term edsl EId
+eid = econ $ EId eid'
 
---f' :: EFunctor f => Term edsl
---
--}
+eid_alt :: ESystemF edsl => Term edsl EId
+eid_alt = econ $ EId $$ EForall $ econ $ EId' $ elam \x -> x