Skip to content
Permalink
Browse files

Removed 'Visibility' and the associated machinery

  • Loading branch information...
effectfully committed Nov 8, 2019
1 parent 95b021a commit e1d7e86d747d0a2b6c25cfdd4d63c81ee3737965
@@ -73,7 +73,7 @@ library
Language.PlutusCore.Generators.Interesting
Language.PlutusCore.Generators.Test
Language.PlutusCore.Lexer
-- Language.PlutusCore.Parser
Language.PlutusCore.Parser
PlutusPrelude
Control.Monad.Trans.Inner
Common
@@ -2,12 +2,12 @@
module Language.PlutusCore
(
-- * Parser
parse
, parseST
, parseTermST
, parseTypeST
, parseScoped
, parseProgram
-- parse
-- , parseST
-- , parseTermST
-- , parseTypeST
-- , parseScoped
parseProgram
, parseTerm
, parseType
-- * AST
@@ -143,7 +143,7 @@ makeConstAppResult = pure . makeKnown
-- | Convert a PLC constant (unwrapped from 'Value') into the corresponding Haskell value.
-- Checks that the constant is of a given built-in type.
extractBuiltin
:: forall m uni a. (Monad m, InternalKnownType a uni)
:: forall m uni a. (Monad m, KnownType a uni)
=> Value TyName Name uni () -> EvaluateConstApp uni m a
extractBuiltin value =
thoist (InnerT . fmap nat . runReflectT) $ readKnownM value where
@@ -1,6 +1,8 @@
-- | A dynamic built-in name that allows to call arbitrary 'IO' actions over
-- PLC values of a built-in types (including dynamic built-in types).

{-# LANGUAGE DataKinds #-}

module Language.PlutusCore.Constant.Dynamic.Call
( dynamicCallTypeScheme
, dynamicCallAssign
@@ -16,17 +18,17 @@ import Language.PlutusCore.Type
import Data.Proxy
import System.IO.Unsafe

dynamicCallTypeScheme :: (KnownType a uni, Evaluable uni) => TypeScheme uni (a -> ()) ()
dynamicCallTypeScheme :: (KnownType a uni, Evaluable uni) => TypeScheme uni '[a] ()
dynamicCallTypeScheme = Proxy `TypeSchemeArrow` TypeSchemeResult Proxy

dynamicCallAssign
:: (KnownType a uni, Evaluable uni)
=> DynamicBuiltinName
-> (a -> IO ())
-> DynamicBuiltinNameDefinition uni
-> NameDefinition uni
dynamicCallAssign name f =
DynamicBuiltinNameDefinition name $
DynamicBuiltinNameMeaning dynamicCallTypeScheme (unsafePerformIO . f)
NameDefinition name $
NameMeaning dynamicCallTypeScheme (unsafePerformIO . f)

dynamicCall :: DynamicBuiltinName -> Term tyname name uni ()
dynamicCall = dynamicBuiltinNameAsTerm
@@ -64,8 +64,6 @@ instance PrettyKnown Integer where
prettyKnown = undefined

instance KnownType a uni => KnownType (EvaluationResult a) uni where
type VisibilityOf (EvaluationResult a) = VisibilityOf a

toTypeAst _ = toTypeAst @a Proxy

makeKnown EvaluationFailure = Error () $ toTypeAst @a Proxy
@@ -103,8 +101,6 @@ instance Pretty a => Pretty (Shallow a) where
pretty = pretty . unShallow

instance (Evaluable uni, uni `Includes` a, PrettyKnown a) => KnownType (Shallow a) uni where
type VisibilityOf (Shallow a) = 'Internal

toTypeAst _ = constantType @a Proxy ()

makeKnown (Shallow x) = constantTerm () x
@@ -117,21 +113,6 @@ instance (Evaluable uni, uni `Includes` a, PrettyKnown a) => KnownType (Shallow
instance PrettyKnown a => PrettyKnown (Shallow a) where
prettyKnown = prettyKnown . unShallow

newtype Deep a = Deep
{ unDeep :: a
} deriving (Show, Generic, Typeable)

instance Pretty a => Pretty (Deep a) where
pretty = pretty . unDeep

instance ExternalKnownType a uni => KnownType (Deep a) uni where
type VisibilityOf (Deep a) = 'Internal
toTypeAst = undefined -- toTypeAst
makeKnown = makeKnown . unDeep
readKnown eval = fmap Deep . readKnown eval
instance PrettyKnown a => PrettyKnown (Deep a) where
prettyKnown = prettyKnown . unDeep

instance Evaluable uni => KnownType Bool uni where
toTypeAst _ = bool

@@ -187,8 +168,6 @@ newtype AsExtension (uni :: * -> *) a = AsExtension

instance (Evaluable uni, euni ~ Extend a uni, Typeable a, Pretty a) =>
KnownType (AsExtension uni a) euni where
type VisibilityOf (AsExtension uni a) = 'Internal

toTypeAst _ = extensionType ()

makeKnown = extensionTerm () . unAsExtension
@@ -64,19 +64,19 @@ withTypedBuiltinName GtByteString k = k typedGtByteString
-- make is just one @args@ by induction on the list type argument.

oneArg
:: (InternalKnownType a uni, InternalKnownType b uni)
:: (KnownType a uni, KnownType b uni)
=> TypeScheme uni '[a] b
oneArg =
Proxy `TypeSchemeArrow` TypeSchemeResult Proxy

twoArgs
:: (InternalKnownType a uni, InternalKnownType b uni, InternalKnownType c uni)
:: (KnownType a uni, KnownType b uni, KnownType c uni)
=> TypeScheme uni '[a, b] c
twoArgs =
Proxy `TypeSchemeArrow` Proxy `TypeSchemeArrow` TypeSchemeResult Proxy

threeArgs
:: (InternalKnownType a uni, InternalKnownType b uni, InternalKnownType c uni, InternalKnownType d uni)
:: (KnownType a uni, KnownType b uni, KnownType c uni, KnownType d uni)
=> TypeScheme uni '[a, b, c] d
threeArgs =
Proxy `TypeSchemeArrow` Proxy `TypeSchemeArrow` Proxy `TypeSchemeArrow` TypeSchemeResult Proxy
@@ -118,27 +118,27 @@ typedModInteger = TypedBuiltinName ModInteger twoArgs

-- | Typed 'LessThanInteger'.
typedLessThanInteger
:: Evaluable uni => TypedBuiltinName uni '[Shallow Integer, Shallow Integer] (Deep Bool)
:: Evaluable uni => TypedBuiltinName uni '[Shallow Integer, Shallow Integer] Bool
typedLessThanInteger = TypedBuiltinName LessThanInteger twoArgs

-- | Typed 'LessThanEqInteger'.
typedLessThanEqInteger
:: Evaluable uni => TypedBuiltinName uni '[Shallow Integer, Shallow Integer] (Deep Bool)
:: Evaluable uni => TypedBuiltinName uni '[Shallow Integer, Shallow Integer] Bool
typedLessThanEqInteger = TypedBuiltinName LessThanEqInteger twoArgs

-- | Typed 'GreaterThanInteger'.
typedGreaterThanInteger
:: Evaluable uni => TypedBuiltinName uni '[Shallow Integer, Shallow Integer] (Deep Bool)
:: Evaluable uni => TypedBuiltinName uni '[Shallow Integer, Shallow Integer] Bool
typedGreaterThanInteger = TypedBuiltinName GreaterThanInteger twoArgs

-- | Typed 'GreaterThanEqInteger'.
typedGreaterThanEqInteger
:: Evaluable uni => TypedBuiltinName uni '[Shallow Integer, Shallow Integer] (Deep Bool)
:: Evaluable uni => TypedBuiltinName uni '[Shallow Integer, Shallow Integer] Bool
typedGreaterThanEqInteger = TypedBuiltinName GreaterThanEqInteger twoArgs

-- | Typed 'EqInteger'.
typedEqInteger
:: Evaluable uni => TypedBuiltinName uni '[Shallow Integer, Shallow Integer] (Deep Bool)
:: Evaluable uni => TypedBuiltinName uni '[Shallow Integer, Shallow Integer] Bool
typedEqInteger = TypedBuiltinName EqInteger twoArgs

-- | Typed 'Concatenate'.
@@ -168,20 +168,20 @@ typedSHA3 = TypedBuiltinName SHA3 oneArg

-- | Typed 'VerifySignature'.
typedVerifySignature
:: Evaluable uni => TypedBuiltinName uni '[Shallow BSL.ByteString, Shallow BSL.ByteString, Shallow BSL.ByteString] (EvaluationResult (Deep Bool))
:: Evaluable uni => TypedBuiltinName uni '[Shallow BSL.ByteString, Shallow BSL.ByteString, Shallow BSL.ByteString] (EvaluationResult Bool)
typedVerifySignature = TypedBuiltinName VerifySignature threeArgs

-- | Typed 'EqByteString'.
typedEqByteString
:: Evaluable uni => TypedBuiltinName uni '[Shallow BSL.ByteString, Shallow BSL.ByteString] (Deep Bool)
:: Evaluable uni => TypedBuiltinName uni '[Shallow BSL.ByteString, Shallow BSL.ByteString] Bool
typedEqByteString = TypedBuiltinName EqByteString twoArgs

-- | Typed 'LtByteString'.
typedLtByteString
:: Evaluable uni => TypedBuiltinName uni '[Shallow BSL.ByteString, Shallow BSL.ByteString] (Deep Bool)
:: Evaluable uni => TypedBuiltinName uni '[Shallow BSL.ByteString, Shallow BSL.ByteString] Bool
typedLtByteString = TypedBuiltinName LtByteString twoArgs

-- | Typed 'GtByteString'.
typedGtByteString
:: Evaluable uni => TypedBuiltinName uni '[Shallow BSL.ByteString, Shallow BSL.ByteString] (Deep Bool)
:: Evaluable uni => TypedBuiltinName uni '[Shallow BSL.ByteString, Shallow BSL.ByteString] Bool
typedGtByteString = TypedBuiltinName GtByteString twoArgs
@@ -29,10 +29,7 @@ module Language.PlutusCore.Constant.Typed
, Evaluator (..)
, EvaluateT (..)
, ReflectT (..)
, Visibility (..)
, KnownType (..)
, InternalKnownType
, ExternalKnownType
, PrettyKnown (..)
, KnownTypeValue (..)
, OpaqueTerm (..)
@@ -82,18 +79,15 @@ import GHC.TypeLits

infixr 9 `TypeSchemeArrow`

type InternalKnownType a uni = (KnownType a uni, VisibilityOf a ~ 'Internal)
type ExternalKnownType a uni = (KnownType a uni, VisibilityOf a ~ 'External)

-- | Type schemes of primitive operations.
-- @a@ is the Haskell denotation of a PLC type represented as a 'TypeScheme'.
-- @r@ is the resulting type in @a@, e.g. the resulting type in
-- @ByteString -> Size -> Integer@ is @Integer@.
data TypeScheme uni as r where
TypeSchemeResult
:: InternalKnownType a uni => Proxy a -> TypeScheme uni '[] a
:: KnownType a uni => Proxy a -> TypeScheme uni '[] a
TypeSchemeArrow
:: InternalKnownType a uni => Proxy a -> TypeScheme uni as r -> TypeScheme uni (a ': as) r
:: KnownType a uni => Proxy a -> TypeScheme uni as r -> TypeScheme uni (a ': as) r
TypeSchemeAllType
:: (KnownSymbol text, KnownNat uniq)
-- Here we require the user to manually provide the unique of a type variable.
@@ -341,17 +335,10 @@ makeReflectT = ReflectT . ExceptT . InnerT
makeRightReflectT :: Monad m => m (EvaluationResult a) -> ReflectT m a
makeRightReflectT = ReflectT . lift . InnerT

data Visibility
= Internal
| External

-- See Note [Semantics of dynamic built-in types].
-- See Note [Converting PLC values to Haskell values].
-- | Haskell types known to exist on the PLC side.
class PrettyKnown a => KnownType a uni where
type VisibilityOf a :: Visibility
type VisibilityOf a = 'External

-- | The type representing @a@ used on the PLC side.
toTypeAst :: proxy a -> Type TyName uni ()

@@ -575,8 +562,6 @@ newtype InExtended (b :: *) (uni :: * -> *) a = InExtended
-- A type known in a universe is known in an extended version of that universe.
instance (Evaluable uni, KnownType a uni, euni ~ Extend b uni, Typeable b) =>
KnownType (InExtended b uni a) euni where
type VisibilityOf (InExtended b uni a) = 'Internal

toTypeAst _ = shiftConstantsType $ toTypeAst @a Proxy

makeKnown (InExtended x) = shiftConstantsTerm $ makeKnown @a x
@@ -593,8 +578,6 @@ newtype InUnextended (euni :: * -> *) a = InUnextended

instance (Evaluable uni, KnownType a euni, euni ~ Extend b uni, Typeable b) =>
KnownType (InUnextended euni a) uni where
type VisibilityOf (InUnextended euni a) = 'Internal

toTypeAst _ = unshiftConstantsType $ toTypeAst @a @euni Proxy

makeKnown (InUnextended x) = unshiftConstantsTerm $ makeKnown @a @euni x
@@ -1,8 +1,13 @@
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}

-- | The CK machine.

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE OverloadedStrings #-}

module Language.PlutusCore.Evaluation.CkMachine
( CkMachineException
@@ -48,7 +53,6 @@ test = readKnownCk @_ @DefaultUni $ makeKnown ((Shallow (5 :: Integer), ()), ('a
test2 :: EvaluationResult (Either Text ())
test2 = readKnownCk @() @DefaultUni unitval


infix 4 |>, <|

-- | The CK machine-specific 'MachineException'.
@@ -0,0 +1,24 @@
module Language.PlutusCore.Parser where

import Control.Monad.Except
import qualified Data.ByteString.Lazy as BSL
import Language.PlutusCore.Error
import Language.PlutusCore.Lexer
import Language.PlutusCore.Name
import Language.PlutusCore.Quote
import Language.PlutusCore.Type

-- | Parse a PLC program. The resulting program will have fresh names. The underlying monad must be capable
-- of handling any parse errors.
parseProgram :: (AsParseError e AlexPosn, MonadError e m, MonadQuote m) => BSL.ByteString -> m (Program TyName Name uni AlexPosn)
parseProgram str = undefined -- mapParseRun (parseST str)

-- | Parse a PLC term. The resulting program will have fresh names. The underlying monad must be capable
-- of handling any parse errors.
parseTerm :: (AsParseError e AlexPosn, MonadError e m, MonadQuote m) => BSL.ByteString -> m (Term TyName Name uni AlexPosn)
parseTerm str = undefined -- mapParseRun (parseTermST str)

-- | Parse a PLC type. The resulting program will have fresh names. The underlying monad must be capable
-- of handling any parse errors.
parseType :: (AsParseError e AlexPosn, MonadError e m, MonadQuote m) => BSL.ByteString -> m (Type TyName uni AlexPosn)
parseType str = undefined -- mapParseRun (parseTypeST str)

0 comments on commit e1d7e86

Please sign in to comment.
You can’t perform that action at this time.