From 9c090b515eb68193da2037076f2fc720948c6cd3 Mon Sep 17 00:00:00 2001 From: Tilde Rose Date: Tue, 18 Jan 2022 18:27:46 +0000 Subject: [PATCH] bind fields, most of the way to full field API --- Plutarch/DataRepr.hs | 4 ++ Plutarch/Field.hs | 165 +++++++++++++++++++++++++++++++++++++------ 2 files changed, 149 insertions(+), 20 deletions(-) diff --git a/Plutarch/DataRepr.hs b/Plutarch/DataRepr.hs index 8d863064d..3bfbfdc70 100644 --- a/Plutarch/DataRepr.hs +++ b/Plutarch/DataRepr.hs @@ -52,6 +52,7 @@ punDataRepr = phoistAcyclic $ plet (pasConstr #$ pasData t) $ \d -> (punsafeCoerce $ psndBuiltin # d :: Term _ (PDataList def)) + pindexDataRepr :: (KnownNat n) => Proxy n -> Term s (PDataRepr (def : defs) :--> PDataList (IndexList n (def : defs))) pindexDataRepr n = phoistAcyclic $ plam $ \t -> @@ -128,6 +129,9 @@ class (PMatch a, PIsData a) => PIsDataRepr (a :: PType) where type PIsDataReprRepr a :: [[PType]] pmatchRepr :: forall s b. Term s (PDataRepr (PIsDataReprRepr a)) -> (a s -> Term s b) -> Term s b +pasDataRepr :: (PIsDataRepr a) => Term s a -> Term s (PDataRepr (PIsDataReprRepr a)) +pasDataRepr = punsafeCoerce + instance PIsDataRepr a => PIsData (PIsDataReprInstances a h) where pdata = punsafeCoerce pfromData = punsafeCoerce diff --git a/Plutarch/Field.hs b/Plutarch/Field.hs index 5adfa315a..dc58181a4 100644 --- a/Plutarch/Field.hs +++ b/Plutarch/Field.hs @@ -1,50 +1,68 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FunctionalDependencies #-} -module Plutarch.Field (HList (..), indexHList, Elem (..), NatElem (..), getField) where +module Plutarch.Field + (HList (..), indexHList, Elem (..), NatElem (..), getField, BindFields (..), xssum) where -import Data.Kind (Type) +--import Data.Kind (Type) --import Data.Proxy (Proxy (..)) import GHC.TypeLits (type (-), type (+), Nat) +import Plutarch.DataRepr + (PDataList, pdhead, pdtail) +import Plutarch.Internal (TermCont (..), punsafeCoerce) +--import Plutarch (PType) +import Plutarch.Builtin (PAsData, PData, PBuiltinList, PIsData (..)) +import Plutarch.Prelude + +import qualified PlutusTx +import Plutarch.Integer +import Plutarch.Lift + -------------------------------------------------------------------------------- +-- | Usual GADT Heterogenous List encoding data HList (xs :: [Type]) where HNil :: HList '[] HCons :: x -> HList xs -> HList (x ': xs) +-- | GADT proof-witness of HList membership, usable as an index data Elem (x :: k) (xs :: [k]) where Here :: Elem x (x ': xs) There :: Elem x xs -> Elem x (y ': xs) -type family IndexList (n :: Nat) (l :: [k]) :: k where - IndexList 0 (x ': _) = x - IndexList n (x : xs) = IndexList (n - 1) xs - +-- | Index HList using Elem indexHList :: HList xs -> (forall x. Elem x xs -> x) indexHList (HCons x _) Here = x indexHList (HCons _ xs) (There i) = indexHList xs i indexHList HNil impossible = case impossible of {} -getField - :: forall f fs x xs n. - ( (IndexOf f fs ~ n) - , (IndexList n xs) ~ x - , NatElem n x xs - ) => - HList xs -> x -getField xs = indexHList xs (natElem @_ @n) +-- | Indexing type-level lists +type family IndexList (n :: Nat) (l :: [k]) :: k where + IndexList 0 (x ': _) = x + IndexList n (x : xs) = IndexList (n - 1) xs -type family IndexOf (x :: k) (xs :: [k]) :: Nat where - IndexOf x (x ': _) = 0 - IndexOf x (y ': xs) = (IndexOf x xs + 1) +{- | + Construct an `Elem` via Nat. ---type family Field (f :: l) (fs :: [l]) (xs :: [k]) :: k where --- Field f fs xs = IndexList (IndexOf f fs) xs + This class could instead be a more direct version of 'indexHList', + but perhaps the `Elem` encoding will be useful. +-} class (IndexList n xs ~ x) => NatElem (n :: Nat) (x :: k) (xs :: [k]) | xs n -> x where + {- | Construct the `Elem` corresponding to a Nat index. + + Example: + + >>> natElem @_ @0 + Here + + >>> natElem @_ @3 + There (There (There Here)) + -} + natElem :: Elem x xs instance {-# OVERLAPS #-} NatElem 0 x (x ': xs) where @@ -57,4 +75,111 @@ instance {-# OVERLAPPABLE #-} ) => NatElem n x (y ': xs) where natElem :: Elem x (y ': xs) - natElem = There (natElem @_ @(n-1) @x @xs) \ No newline at end of file + natElem = There (natElem @_ @(n-1) @x @xs) + +-- | Get the Index of a type in a list +type family IndexOf (x :: k) (xs :: [k]) :: Nat where + IndexOf x (x ': _) = 0 + IndexOf x (y ': xs) = (IndexOf x xs + 1) + +{- | + Construct an Elem via the position of a given type + in a type-level list. + + The intended use is to 'lookup' the index of a + field name: + + >>> fieldElem @"z" @["x", "y", "z", "w"] + >>> There (There Here)) + +-} +fieldElem :: + forall f fs x xs n. + ( (IndexOf f fs ~ n) + , (IndexList n xs) ~ x + , NatElem n x xs + ) => + Elem x xs +fieldElem = natElem @_ @n + +{- | + Index a HList with a field in a provided list of fields. + + >>> xs = HCons 1 (HCons 2 (HCons 3 HNil)) + >>> getField @"y" @["x", "y", "z"] xs + >>> 2 + +-} +getField + :: forall f fs x xs n. + ( (IndexOf f fs ~ n) + , (IndexList n xs) ~ x + , NatElem n x xs + ) => + HList xs -> x +getField xs = indexHList xs $ fieldElem @f @fs + +-------------------------------------------------------------------------------- + +type family TermsOf (s :: S) (as :: [PType]) :: [Type] where + TermsOf _ '[] = '[] + TermsOf s (x ': xs) = Term s (PAsData x) ': TermsOf s xs + +class BindFields as where + {- | + Bind all the fields in a 'PDataList' term to a corresponding + HList of Terms. + + A continuation is returned to enable sharing of + the generated bound-variables. + + -} + bindFields' :: Term s (PDataList as) -> TermCont s (HList (TermsOf s as)) + +instance {-# OVERLAPS #-} + BindFields (a ': '[]) where + bindFields' t = + pure $ HCons (pdhead # t) HNil + +instance {-# OVERLAPPABLE #-} + (BindFields as) => BindFields (a ': as) where + bindFields' t = do + t' <- TermCont $ plet t + --tail <- TermCont $ plet $ pdtail # t + xs <- bindFields @as (pdtail # t') + pure $ HCons (pdhead # t') xs + +xs :: Term s (PDataList '[PInteger, PInteger, PInteger]) +xs = + punsafeCoerce $ + pconstant @(PBuiltinList PData) $ fmap (PlutusTx.toData @Integer) [1,2,3] + +xssum :: Term s PInteger +xssum = + runTermCont (bindFields' xs) $ \case + (HCons x (HCons y (HCons z HNil))) -> + pfromData x + pfromData y + pfromData z + +-------------------------------------------------------------------------------- + +{- | + Heterogenous Record, using a list of symbols as a + set of corresponding indices by position. + +-} +newtype HRec (fs :: [Symbol]) (as :: [Type]) = + HRec { hrecList :: HList as } + +class PDataFields (a :: PType) where + type PFieldNames a :: [Symbol] + type PFieldTypes a :: [PType] + ptoFields :: Term s a -> Term s (PDataList (PFieldTypes a)) + +letFields :: + ( PDataFields a + , BindFields (PFieldTypes a) + ) => + Term s a -> (HRec (PFieldNames a) (PFieldTypes a) -> Term s b) -> Term s b +letFields t = + bindFields @as +