Skip to content

Commit

Permalink
DeBruijn: add nameless de Bruijn names, use for serialization
Browse files Browse the repository at this point in the history
Convert back to named before evaluation, later we can just evaluate it
directly.
  • Loading branch information
michaelpj committed Sep 21, 2020
1 parent c129e09 commit 80dba72
Show file tree
Hide file tree
Showing 12 changed files with 215 additions and 39 deletions.
1 change: 1 addition & 0 deletions plutus-core/plutus-core.cabal
Expand Up @@ -200,6 +200,7 @@ library
Language.UntypedPlutusCore.Core.Instance.Pretty.Readable
Language.UntypedPlutusCore.Core.Instance.CBOR
Language.UntypedPlutusCore.Core.Type
Language.UntypedPlutusCore.Core.Plated
Language.UntypedPlutusCore.Size
Language.UntypedPlutusCore.Subst

Expand Down
4 changes: 2 additions & 2 deletions plutus-core/src/Language/PlutusCore/CBOR.hs
Expand Up @@ -273,8 +273,8 @@ instance Serialise Special
deriving newtype instance Serialise Index

instance Serialise DeBruijn where
encode (DeBruijn txt i) = encode txt <> encode i
decode = DeBruijn <$> decode <*> decode
encode (DeBruijn i) = encode i
decode = DeBruijn <$> decode

instance Serialise TyDeBruijn where
encode (TyDeBruijn n) = encode n
Expand Down
1 change: 1 addition & 0 deletions plutus-core/src/Language/PlutusCore/Core/Type.hs
Expand Up @@ -2,6 +2,7 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
Expand Down
34 changes: 18 additions & 16 deletions plutus-core/src/Language/PlutusCore/DeBruijn.hs
Expand Up @@ -15,6 +15,8 @@ module Language.PlutusCore.DeBruijn
, unDeBruijnTy
, unDeBruijnTerm
, unDeBruijnProgram
, unNameDeBruijn
, unNameTyDeBruijn
) where

import Language.PlutusCore.DeBruijn.Internal
Expand All @@ -28,22 +30,22 @@ import Control.Monad.Reader

import qualified Data.Bimap as BM

-- | Convert a 'Type' with 'TyName's into a 'Type' with 'TyDeBruijn's.
-- | Convert a 'Type' with 'TyName's into a 'Type' with 'NamedTyDeBruijn's.
deBruijnTy
:: MonadError FreeVariableError m
=> Type TyName uni ann -> m (Type TyDeBruijn uni ann)
=> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTy = flip runReaderT (Levels 0 BM.empty) . deBruijnTyM

-- | Convert a 'Term' with 'TyName's and 'Name's into a 'Term' with 'TyDeBruijn's and 'DeBruijn's.
-- | Convert a 'Term' with 'TyName's and 'Name's into a 'Term' with 'NamedTyDeBruijn's and 'NamedDeBruijn's.
deBruijnTerm
:: MonadError FreeVariableError m
=> Term TyName Name uni ann -> m (Term TyDeBruijn DeBruijn uni ann)
=> Term TyName Name uni ann -> m (Term NamedTyDeBruijn NamedDeBruijn uni ann)
deBruijnTerm = flip runReaderT (Levels 0 BM.empty) . deBruijnTermM

-- | Convert a 'Program' with 'TyName's and 'Name's into a 'Program' with 'TyDeBruijn's and 'DeBruijn's.
-- | Convert a 'Program' with 'TyName's and 'Name's into a 'Program' with 'NamedTyDeBruijn's and 'NamedDeBruijn's.
deBruijnProgram
:: MonadError FreeVariableError m
=> Program TyName Name uni ann -> m (Program TyDeBruijn DeBruijn uni ann)
=> Program TyName Name uni ann -> m (Program NamedTyDeBruijn NamedDeBruijn uni ann)
deBruijnProgram (Program ann ver term) = Program ann ver <$> deBruijnTerm term

{- Note [De Bruijn conversion and recursion schemes]
Expand All @@ -54,7 +56,7 @@ These are normally constant in a catamorphic application.
deBruijnTyM
:: (MonadReader Levels m, MonadError FreeVariableError m)
=> Type TyName uni ann
-> m (Type TyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
deBruijnTyM = \case
-- variable case
TyVar ann n -> TyVar ann <$> tyNameToDeBruijn n
Expand All @@ -75,7 +77,7 @@ deBruijnTyM = \case
deBruijnTermM
:: (MonadReader Levels m, MonadError FreeVariableError m)
=> Term TyName Name uni ann
-> m (Term TyDeBruijn DeBruijn uni ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni ann)
deBruijnTermM = \case
-- variable case
Var ann n -> Var ann <$> nameToDeBruijn n
Expand All @@ -96,27 +98,27 @@ deBruijnTermM = \case
Constant ann con -> pure $ Constant ann con
Builtin ann bn -> pure $ Builtin ann bn

-- | Convert a 'Type' with 'TyDeBruijn's into a 'Type' with 'TyName's.
-- | Convert a 'Type' with 'NamedTyDeBruijn's into a 'Type' with 'TyName's.
unDeBruijnTy
:: (MonadQuote m, MonadError FreeVariableError m)
=> Type TyDeBruijn uni ann -> m (Type TyName uni ann)
=> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTy = flip runReaderT (Levels 0 BM.empty) . unDeBruijnTyM

-- | Convert a 'Term' with 'TyDeBruijn's and 'DeBruijn's into a 'Term' with 'TyName's and 'Name's.
-- | Convert a 'Term' with 'NamedTyDeBruijn's and 'NamedDeBruijn's into a 'Term' with 'TyName's and 'Name's.
unDeBruijnTerm
:: (MonadQuote m, MonadError FreeVariableError m)
=> Term TyDeBruijn DeBruijn uni ann -> m (Term TyName Name uni ann)
=> Term NamedTyDeBruijn NamedDeBruijn uni ann -> m (Term TyName Name uni ann)
unDeBruijnTerm = flip runReaderT (Levels 0 BM.empty) . unDeBruijnTermM

-- | Convert a 'Program' with 'TyDeBruijn's and 'DeBruijn's into a 'Program' with 'TyName's and 'Name's.
-- | Convert a 'Program' with 'NamedTyDeBruijn's and 'NamedDeBruijn's into a 'Program' with 'TyName's and 'Name's.
unDeBruijnProgram
:: (MonadQuote m, MonadError FreeVariableError m)
=> Program TyDeBruijn DeBruijn uni ann -> m (Program TyName Name uni ann)
=> Program NamedTyDeBruijn NamedDeBruijn uni ann -> m (Program TyName Name uni ann)
unDeBruijnProgram (Program ann ver term) = Program ann ver <$> unDeBruijnTerm term

unDeBruijnTyM
:: (MonadReader Levels m, MonadQuote m, MonadError FreeVariableError m)
=> Type TyDeBruijn uni ann
=> Type NamedTyDeBruijn uni ann
-> m (Type TyName uni ann)
unDeBruijnTyM = \case
-- variable case
Expand All @@ -137,7 +139,7 @@ unDeBruijnTyM = \case

unDeBruijnTermM
:: (MonadReader Levels m, MonadQuote m, MonadError FreeVariableError m)
=> Term TyDeBruijn DeBruijn uni ann
=> Term NamedTyDeBruijn NamedDeBruijn uni ann
-> m (Term TyName Name uni ann)
unDeBruijnTermM = \case
-- variable case
Expand Down
60 changes: 49 additions & 11 deletions plutus-core/src/Language/PlutusCore/DeBruijn/Internal.hs
Expand Up @@ -8,7 +8,9 @@
module Language.PlutusCore.DeBruijn.Internal
( Index (..)
, DeBruijn (..)
, NamedDeBruijn (..)
, TyDeBruijn (..)
, NamedTyDeBruijn (..)
, FreeVariableError (..)
, Level (..)
, Levels (..)
Expand All @@ -19,6 +21,8 @@ module Language.PlutusCore.DeBruijn.Internal
, withScope
, getIndex
, getUnique
, unNameDeBruijn
, unNameTyDeBruijn
, nameToDeBruijn
, tyNameToDeBruijn
, deBruijnToName
Expand Down Expand Up @@ -50,31 +54,57 @@ newtype Index = Index Natural
deriving anyclass NFData

-- | A term name as a de Bruijn index.
data DeBruijn = DeBruijn { dbnString :: T.Text, dbnIndex :: Index }
data NamedDeBruijn = NamedDeBruijn { ndbnString :: T.Text, ndbnIndex :: Index }
deriving (Show, Generic)
deriving anyclass NFData

-- | A term name as a de Bruijn index, without the name string.
data DeBruijn = DeBruijn { dbnIndex :: Index }
deriving (Show, Generic)
deriving anyclass NFData

-- | A type name as a de Bruijn index.
newtype NamedTyDeBruijn = NamedTyDeBruijn NamedDeBruijn
deriving stock (Show, Generic)
deriving newtype (PrettyBy config)
deriving anyclass NFData
instance Wrapped NamedTyDeBruijn

-- | A type name as a de Bruijn index, without the name string.
newtype TyDeBruijn = TyDeBruijn DeBruijn
deriving stock (Show, Generic)
deriving newtype (PrettyBy config)
deriving anyclass NFData
instance Wrapped TyDeBruijn

instance HasPrettyConfigName config => PrettyBy config DeBruijn where
prettyBy config (DeBruijn txt (Index ix))
instance HasPrettyConfigName config => PrettyBy config NamedDeBruijn where
prettyBy config (NamedDeBruijn txt (Index ix))
| showsUnique = pretty txt <> "_i" <> pretty ix
| otherwise = pretty txt
where PrettyConfigName showsUnique = toPrettyConfigName config

instance HasPrettyConfigName config => PrettyBy config DeBruijn where
prettyBy config (DeBruijn (Index ix))
| showsUnique = "i" <> pretty ix
| otherwise = ""
where PrettyConfigName showsUnique = toPrettyConfigName config

class HasIndex a where
index :: Lens' a Index

instance HasIndex NamedDeBruijn where
index = lens g s where
g = ndbnIndex
s n i = n{ndbnIndex=i}

instance HasIndex DeBruijn where
index = lens g s where
g = dbnIndex
s n i = n{dbnIndex=i}

instance HasIndex NamedTyDeBruijn where
index = _Wrapped' . index

instance HasIndex TyDeBruijn where
index = _Wrapped' . index

Expand Down Expand Up @@ -150,22 +180,30 @@ getUnique ix = do
Just u -> pure u
Nothing -> throwError $ FreeIndex ix

unNameDeBruijn
:: NamedDeBruijn -> DeBruijn
unNameDeBruijn (NamedDeBruijn _ ix) = DeBruijn ix

unNameTyDeBruijn
:: NamedTyDeBruijn -> TyDeBruijn
unNameTyDeBruijn (NamedTyDeBruijn db) = TyDeBruijn $ unNameDeBruijn db

nameToDeBruijn
:: (MonadReader Levels m, MonadError FreeVariableError m)
=> Name -> m DeBruijn
nameToDeBruijn (Name str u) = DeBruijn str <$> getIndex u
=> Name -> m NamedDeBruijn
nameToDeBruijn (Name str u) = NamedDeBruijn str <$> getIndex u

tyNameToDeBruijn
:: (MonadReader Levels m, MonadError FreeVariableError m)
=> TyName -> m TyDeBruijn
tyNameToDeBruijn (TyName n) = TyDeBruijn <$> nameToDeBruijn n
=> TyName -> m NamedTyDeBruijn
tyNameToDeBruijn (TyName n) = NamedTyDeBruijn <$> nameToDeBruijn n

deBruijnToName
:: (MonadReader Levels m, MonadError FreeVariableError m)
=> DeBruijn -> m Name
deBruijnToName (DeBruijn str ix) = Name str <$> getUnique ix
=> NamedDeBruijn -> m Name
deBruijnToName (NamedDeBruijn str ix) = Name str <$> getUnique ix

deBruijnToTyName
:: (MonadReader Levels m, MonadError FreeVariableError m)
=> TyDeBruijn -> m TyName
deBruijnToTyName (TyDeBruijn n) = TyName <$> deBruijnToName n
=> NamedTyDeBruijn -> m TyName
deBruijnToTyName (NamedTyDeBruijn n) = TyName <$> deBruijnToName n
Expand Up @@ -5,6 +5,7 @@ module Language.UntypedPlutusCore

import Language.UntypedPlutusCore.Core as Export
import Language.UntypedPlutusCore.Size as Export
import Language.UntypedPlutusCore.Subst as Export
-- Also has some functions
import Language.UntypedPlutusCore.Core.Instance.CBOR as Export

Expand Down
Expand Up @@ -3,4 +3,5 @@ module Language.UntypedPlutusCore.Core
) where

import Language.UntypedPlutusCore.Core.Instance ()
import Language.UntypedPlutusCore.Core.Plated as Export
import Language.UntypedPlutusCore.Core.Type as Export
@@ -0,0 +1,57 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}

module Language.UntypedPlutusCore.Core.Plated
( termBinds
, termVars
, termUniques
, termSubterms
, termSubtermsDeep
, termUniquesDeep
) where

import Language.PlutusCore.Core (HasUniques)
import Language.PlutusCore.Name
import Language.UntypedPlutusCore.Core.Type

import Control.Lens

-- | Get all the direct child 'name a's of the given 'Term' from 'LamAbs'es.
termBinds :: Traversal' (Term name uni ann) name
termBinds f = \case
LamAbs ann n t -> f n <&> \n' -> LamAbs ann n' t
x -> pure x

-- | Get all the direct child 'name a's of the given 'Term' from 'Var's.
termVars :: Traversal' (Term name uni ann) name
termVars f = \case
Var ann n -> Var ann <$> f n
x -> pure x

-- | Get all the direct child 'Unique's of the given 'Term'.
termUniques :: HasUniques (Term name uni ann) => Traversal' (Term name uni ann) Unique
termUniques f = \case
LamAbs ann n t -> theUnique f n <&> \n' -> LamAbs ann n' t
Var ann n -> theUnique f n <&> Var ann
x -> pure x

{-# INLINE termSubterms #-}
-- | Get all the direct child 'Term's of the given 'Term'.
termSubterms :: Traversal' (Term name uni ann) (Term name uni ann)
termSubterms f = \case
LamAbs ann n t -> LamAbs ann n <$> f t
Apply ann t1 t2 -> Apply ann <$> f t1 <*> f t2
Delay ann t -> Delay ann <$> f t
Force ann t -> Force ann <$> f t
e@Error {} -> pure e
v@Var {} -> pure v
c@Constant {} -> pure c
b@Builtin {} -> pure b

-- | Get all the transitive child 'Term's of the given 'Term'.
termSubtermsDeep :: Fold (Term name uni ann) (Term name uni ann)
termSubtermsDeep = cosmosOf termSubterms

-- | Get all the transitive child 'Unique's of the given 'Term'.
termUniquesDeep :: HasUniques (Term name uni ann) => Fold (Term name uni ann) Unique
termUniquesDeep = termSubtermsDeep . termUniques
Expand Up @@ -23,6 +23,7 @@ import qualified Language.PlutusCore.Constant as TPLC
import qualified Language.PlutusCore.Core as TPLC
import Language.PlutusCore.Evaluation.Machine.ExBudgeting
import Language.PlutusCore.Evaluation.Machine.ExMemory
import qualified Language.PlutusCore.Name as TPLC
import Language.PlutusCore.Universe

-- | The type of Untyped Plutus Core terms. Mirrors the type of Typed Plutus Core terms except
Expand Down Expand Up @@ -64,6 +65,11 @@ instance TPLC.AsConstant (Term name uni ann) where
instance TPLC.FromConstant (Term name uni ()) where
fromConstant = Constant ()

type instance TPLC.HasUniques (Term name uni ann)
= TPLC.HasUnique name TPLC.TermUnique
type instance TPLC.HasUniques (Program name uni ann) = TPLC.HasUniques
(Term name uni ann)

instance ToExMemory (Term name uni ()) where
toExMemory _ = 0

Expand Down
Expand Up @@ -7,11 +7,13 @@
module Language.UntypedPlutusCore.DeBruijn
( Index (..)
, DeBruijn (..)
, NamedDeBruijn (..)
, FreeVariableError (..)
, deBruijnTerm
, deBruijnProgram
, unDeBruijnTerm
, unDeBruijnProgram
, unNameDeBruijn
) where

import Language.PlutusCore.DeBruijn.Internal
Expand All @@ -32,19 +34,19 @@ This module is just a boring port of the typed version.
-- | Convert a 'Term' with 'TyName's and 'Name's into a 'Term' with 'TyDeBruijn's and 'DeBruijn's.
deBruijnTerm
:: MonadError FreeVariableError m
=> Term Name uni ann -> m (Term DeBruijn uni ann)
=> Term Name uni ann -> m (Term NamedDeBruijn uni ann)
deBruijnTerm = flip runReaderT (Levels 0 BM.empty) . deBruijnTermM

-- | Convert a 'Program' with 'TyName's and 'Name's into a 'Program' with 'TyDeBruijn's and 'DeBruijn's.
deBruijnProgram
:: MonadError FreeVariableError m
=> Program Name uni ann -> m (Program DeBruijn uni ann)
=> Program Name uni ann -> m (Program NamedDeBruijn uni ann)
deBruijnProgram (Program ann ver term) = Program ann ver <$> deBruijnTerm term

deBruijnTermM
:: (MonadReader Levels m, MonadError FreeVariableError m)
=> Term Name uni ann
-> m (Term DeBruijn uni ann)
-> m (Term NamedDeBruijn uni ann)
deBruijnTermM = \case
-- variable case
Var ann n -> Var ann <$> nameToDeBruijn n
Expand All @@ -64,18 +66,18 @@ deBruijnTermM = \case
-- | Convert a 'Term' with 'TyDeBruijn's and 'DeBruijn's into a 'Term' with 'TyName's and 'Name's.
unDeBruijnTerm
:: (MonadQuote m, MonadError FreeVariableError m)
=> Term DeBruijn uni ann -> m (Term Name uni ann)
=> Term NamedDeBruijn uni ann -> m (Term Name uni ann)
unDeBruijnTerm = flip runReaderT (Levels 0 BM.empty) . unDeBruijnTermM

-- | Convert a 'Program' with 'TyDeBruijn's and 'DeBruijn's into a 'Program' with 'TyName's and 'Name's.
unDeBruijnProgram
:: (MonadQuote m, MonadError FreeVariableError m)
=> Program DeBruijn uni ann -> m (Program Name uni ann)
=> Program NamedDeBruijn uni ann -> m (Program Name uni ann)
unDeBruijnProgram (Program ann ver term) = Program ann ver <$> unDeBruijnTerm term

unDeBruijnTermM
:: (MonadReader Levels m, MonadQuote m, MonadError FreeVariableError m)
=> Term DeBruijn uni ann
=> Term NamedDeBruijn uni ann
-> m (Term Name uni ann)
unDeBruijnTermM = \case
-- variable case
Expand Down

0 comments on commit 80dba72

Please sign in to comment.