Skip to content
Merged
Show file tree
Hide file tree
Changes from 19 commits
Commits
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 covenant.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -133,6 +133,7 @@ library
bytestring >=0.12.1.0 && <0.13,
containers >=0.6.8 && <0.8,
enummapset ==0.7.3.0,
hex-text ==0.1.0.9,
mtl >=2.3.1 && <3,
nonempty-vector ==0.2.4,
optics-core ==0.4.1.1,
Expand Down
44 changes: 19 additions & 25 deletions src/Covenant/ASG.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ module Covenant.ASG
( -- * The ASG itself

-- ** Types
ASG,
ASGInternal (ASG),

-- ** Functions
topLevelId,
Expand Down Expand Up @@ -143,6 +143,7 @@ import Covenant.Internal.Term
( ASGNode (ACompNode, AValNode, AnError),
ASGNodeType (CompNodeType, ErrorNodeType, ValNodeType),
Arg (Arg),
BoundTyVar (BoundTyVar),
CompNodeInfo
( Builtin1Internal,
Builtin2Internal,
Expand Down Expand Up @@ -300,14 +301,19 @@ import Optics.Core
-- | A fully-assembled Covenant ASG.
--
-- @since 1.0.0
newtype ASG = ASG (Id, Map Id ASGNode)
newtype ASGInternal = ASGInternal (Id, Map Id ASGNode)
Comment thread
kozross marked this conversation as resolved.
Outdated
deriving stock
( -- | @since 1.0.0
Eq,
-- | @since 1.0.0
Show
)

{-# COMPLETE ASG #-}

pattern ASG :: Map Id ASGNode -> ASGInternal
pattern ASG m <- ASGInternal (_, m)

-- Note (Koz, 24/04/25): The `topLevelNode` and `nodeAt` functions use `fromJust`,
-- because we can guarantee it's impossible to miss. For an end user, the only
-- way to get hold of an `Id` is by inspecting a node, and since we control how
Expand All @@ -321,14 +327,14 @@ newtype ASG = ASG (Id, Map Id ASGNode)
-- | Retrieves the top-level 'Id' of an ASG.
--
-- @since 1.3.0
topLevelId :: ASG -> Id
topLevelId (ASG (i, _)) = i
topLevelId :: ASGInternal -> Id
topLevelId (ASGInternal (i, _)) = i

-- | Retrieves the top-level node of an ASG.
--
-- @since 1.0.0
topLevelNode :: ASG -> ASGNode
topLevelNode asg@(ASG (rootId, _)) = nodeAt rootId asg
topLevelNode :: ASGInternal -> ASGNode
topLevelNode asg@(ASGInternal (rootId, _)) = nodeAt rootId asg

-- | Given an 'Id' and an ASG, produces the node corresponding to that 'Id'.
--
Expand All @@ -340,8 +346,8 @@ topLevelNode asg@(ASG (rootId, _)) = nodeAt rootId asg
-- results, and at worst will crash. You have been warned.
--
-- @since 1.0.0
nodeAt :: Id -> ASG -> ASGNode
nodeAt i (ASG (_, mappings)) = fromJust . Map.lookup i $ mappings
nodeAt :: Id -> ASGInternal -> ASGNode
nodeAt i (ASG mappings) = fromJust . Map.lookup i $ mappings

-- | The environment used when \'building up\' an 'ASG'. This type is exposed
-- only for testing, or debugging, and should /not/ be used in general by those
Expand Down Expand Up @@ -453,8 +459,8 @@ pattern Lit c <- LitInternal c
-- 'Vector' field).
--
-- @since 1.0.0
pattern App :: Id -> Vector Ref -> ValNodeInfo
pattern App f args <- AppInternal f args
pattern App :: Id -> Vector Ref -> Vector (Wedge BoundTyVar (ValT Void)) -> ValNodeInfo
pattern App f args instTys <- AppInternal f args instTys

-- | Wrap a computation into a value (essentially delaying it).
--
Expand Down Expand Up @@ -552,7 +558,7 @@ runASGBuilder ::
forall (a :: Type).
Map TyName (DatatypeInfo AbstractTy) ->
ASGBuilder a ->
Either CovenantError ASG
Either CovenantError ASGInternal
runASGBuilder tyDict (ASGBuilder comp) =
case runIdentity . runHashConsT . runExceptT . runReaderT comp $ ASGEnv (ScopeInfo Vector.empty) tyDict of
(result, bm) -> case result of
Expand All @@ -563,7 +569,7 @@ runASGBuilder tyDict (ASGBuilder comp) =
let (i, rootNode') = Bimap.findMax bm
case rootNode' of
AnError -> Left TopLevelError
ACompNode _ _ -> pure . ASG $ (i, Bimap.toMap bm)
ACompNode _ _ -> pure . ASGInternal $ (i, Bimap.toMap bm)
AValNode t info -> Left . TopLevelValue bm t $ info

-- | Given a scope and a positional argument index, construct that argument.
Expand Down Expand Up @@ -754,7 +760,7 @@ app fId argRefs instTys = do
result <- either (throwError . UnificationError) pure $ checkApp tyDict instantiatedFT (Vector.toList renamedArgs)
restored <- undoRenameM result
checkEncodingWithInfo tyDict restored
refTo . AValNode restored . AppInternal fId $ argRefs
refTo . AValNode restored $ AppInternal fId argRefs instTys
ValNodeType t -> throwError . ApplyToValType $ t
ErrorNodeType -> throwError ApplyToError
where
Expand Down Expand Up @@ -1254,18 +1260,6 @@ tryApply algebraT argT =

-- Putting this here to reduce chance of annoying manual merge (will move later)

-- | Wrapper around an `Arg` that we know represents an in-scope type variable.
-- @since 1.2.0
data BoundTyVar = BoundTyVar DeBruijn (Index "tyvar")
deriving stock
( -- @since 1.2.0
Show,
-- @since 1.2.0
Eq,
-- @since 1.2.0
Ord
)

-- | Given a DeBruijn index (designating scope) and positional index (designating
-- which variable in that scope we are interested in), retrieve an in-scope type
-- variable.
Expand Down
26 changes: 24 additions & 2 deletions src/Covenant/Internal/Term.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ module Covenant.Internal.Term
ASGNode (..),
typeASGNode,
ASGNodeType (..),
BoundTyVar (..),
)
where

Expand All @@ -33,7 +34,10 @@ import Covenant.Prim (OneArgFunc, SixArgFunc, ThreeArgFunc, TwoArgFunc)
import Covenant.Type (ConstructorName, PlutusDataConstructor, Renamed)
import Data.Kind (Type)
import Data.Set qualified as Set
import Data.Text (Text)
import Data.Vector (Vector)
import Data.Void (Void)
import Data.Wedge (Wedge)
import Data.Word (Word64)

-- | An error that can arise during the construction of an ASG by programmatic
Expand Down Expand Up @@ -266,12 +270,15 @@ data CovenantTypeError
-- itself does not exist. It does not seem important to distinguish between the two failure cases.
-- @since 1.3.0
BaseFunctorDoesNotExistFor TyName
| -- 'app' was called with a number of instantiation arguments that does not match the number of
| -- | 'app' was called with a number of instantiation arguments that does not match the number of
-- type variables bound in Count the CompT of the function to which arguments are being applied.
-- The first Int is the number of bound tyvars in the function type, the second is the number of
-- instantiations supplied.
-- @since 1.3.0
WrongNumInstantiationsInApp (CompT Renamed) Int Int
| -- | A miscellaneous error, needed to catch various things that can go wrong during datatype preparation and
-- deserialization
OtherError Text
deriving stock
( -- | @since 1.0.0
Eq,
Expand Down Expand Up @@ -385,7 +392,8 @@ data CompNodeInfo
-- @since 1.0.0
data ValNodeInfo
= LitInternal AConstant
| AppInternal Id (Vector Ref)
| -- | @since 1.3.0
AppInternal Id (Vector Ref) (Vector (Wedge BoundTyVar (ValT Void)))
| ThunkInternal Id
| -- | @since 1.1.0
CataInternal Ref Ref
Expand Down Expand Up @@ -452,3 +460,17 @@ data ASGNodeType
-- | @since 1.0.0
Show
)

-- NOTE: Had to move this here

-- | Wrapper around an `Arg` that we know represents an in-scope type variable.
-- @since 1.2.0
data BoundTyVar = BoundTyVar DeBruijn (Index "tyvar")
deriving stock
( -- @since 1.2.0
Show,
-- @since 1.2.0
Eq,
-- @since 1.2.0
Ord
)
Loading
Loading