fir-0.1.0.0: src/FIR/Validation/Bindings.hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-|
Module: FIR.Validation.Bindings
Validation module providing checks for stateful operations
such as 'FIR.Syntax.Program.get' and 'FIR.Syntax.Program.put',
using type families with custom type errors.
These are used, for instance, to prevent any name from being bound twice,
or accessing a binding that does not exist.
-}
module FIR.Validation.Bindings where
-- base
import Prelude
hiding ( Integral, Floating )
import Data.Kind
( Type, Constraint )
import Data.Type.Bool
( If, type (||), type (&&) )
import Data.Type.Equality
( type (==) )
import GHC.TypeLits
( Symbol
, TypeError
, ErrorMessage(..)
)
import GHC.TypeNats
( Nat )
-- fir
import Data.Type.Known
( Known )
import Data.Type.List
( Elem )
import Data.Type.Map
( Map, (:->)((:->))
, Insert, Remove
, Lookup, Union
, Keys
)
import Data.Type.POrd
( POrd(Compare) )
import FIR.Binding
( Binding, BindingsMap, FunctionType
, Permission(Read,Write)
, Var, Fun
)
import FIR.Builtin
( ModelBuiltins )
import FIR.Prim.Types
( HasOpaqueType )
import FIR.ProgramState
( FunctionContext(..)
, ProgramState(ProgramState)
, Definedness(..), FunctionInfo(..)
, EntryPointInfo(..), TLInterface
, Bindings
)
import FIR.Validation.Interface
( ValidInterface )
import qualified SPIRV.Stage as SPIRV
( ExecutionModel, NamedExecutionModel
, ExecutionInfo
, Backend, OtherBackend, BackendOf
)
-------------------------------------------------
-- * Lookup whether a binding exists in the monadic state.
-- | Compute the type of a variable bound by a given name.
--
-- Throws a type error if no variable by that name exists.
type family Has (k :: Symbol) (i :: ProgramState) :: Type where
Has k ('ProgramState bds _ _ _ _ _ _ _) = HasBinding k (Lookup k bds)
type family HasBinding (k :: Symbol) (mbd :: Maybe Binding) :: Type where
HasBinding k 'Nothing
= TypeError
( Text "No binding named " :<>: ShowType k :<>: Text " is in scope." )
HasBinding k ('Just (Var _ a))
= a
HasBinding _ ('Just (Fun as b)) = FunctionType as b
-------------------------------------------------
-- * Constraints for 'FIR.Syntax.Program.get' and 'FIR.Syntax.Program.use'
-- | Check whether we can 'get' a binding.
type family CanGet (k :: Symbol) (i :: ProgramState) :: Constraint where
CanGet k ('ProgramState bds _ _ _ _ _ _ _) = GetBinding k (Lookup k bds)
type family GetBinding (k :: Symbol) (mbd :: Maybe Binding) :: Constraint where
GetBinding k 'Nothing
= TypeError
( Text "'get'/'use': no binding named " :<>: ShowType k :<>: Text " is in scope." )
GetBinding k ('Just (Var perms _))
= If
( Elem 'Read perms )
( () :: Constraint )
( TypeError
( Text "'get'/'use': variable named " :<>: ShowType k :<>: Text " is not readable." )
)
GetBinding _ ('Just (Fun as b)) = ()
-------------------------------------------------
-- * Constraints for 'FIR.Syntax.Program.put' and 'FIR.Syntax.Program.assign'
-- | Check whether we can write to a binding.
type family CanPut (k :: Symbol) (i :: ProgramState) :: Constraint where
CanPut k ('ProgramState bds _ _ _ _ _ _ _) = PutBinding k (Lookup k bds)
type family PutBinding (k :: Symbol) (lookup :: Maybe Binding) :: Constraint where
PutBinding k 'Nothing = TypeError
( Text "'put'/'assign': no binding named " :<>: ShowType k :<>: Text " is in scope."
:$$: Text "To bind a new variable, use 'def'."
)
PutBinding k ('Just (Fun as b)) = TypeError
( Text "'put'/'assign': function bound at name "
:<>: ShowType k :<>: Text ": "
:<>: ShowType (Fun as b) :<>: Text "."
:$$: Text "Use 'fundef' to define a function."
)
PutBinding k ('Just (Var perms _))
= If
( Elem 'Write perms )
( () :: Constraint )
( TypeError
( Text "'put'/'assign': variable " :<>: ShowType k :<>: Text " is not writable." )
)
-------------------------------------------------
-- * Constraints for 'FIR.Syntax.Program.def'
-- | Add a new binding to the indexed state.
type family AddBinding
( k :: Symbol )
( bd :: Binding )
( s :: ProgramState )
:: ProgramState where
AddBinding k bd ('ProgramState bds ctx cfg funs eps iface rayQueries bkend)
= 'ProgramState (Insert k bd bds) ctx cfg funs eps iface rayQueries bkend
-- | Check that it is valid to define a new variable with given name.
--
-- Throws a type error if a binding by this name already exists.
type family ValidDef (k :: Symbol) (i :: ProgramState) (a :: Type) :: Constraint where
ValidDef k ('ProgramState bds _ _ _ _ _ _ _) a =
( NotAlreadyDefined k (Lookup k bds)
, NotOpaqueType (HasOpaqueType a) k a
)
type family NotAlreadyDefined (k :: Symbol) (lookup :: Maybe Binding) :: Constraint where
NotAlreadyDefined _ 'Nothing = ()
NotAlreadyDefined k ('Just _) = TypeError
( Text "'def': a binding by the name " :<>: ShowType k :<>: Text " already exists." )
type family NotOpaqueType (hasOpaque :: Bool) (k :: Symbol) (a :: Type) :: Constraint where
NotOpaqueType True k a =
TypeError
( Text "'def': cannot define new binding named " :<>: ShowType k :<>: Text ":"
:$$: ShowType a :<>: Text " is an opaque type (or it contains an opaque type)."
)
NotOpaqueType False _ _ = ()
-------------------------------------------------
-- * Constraints for 'FIR.Syntax.Program.fundef'
-- | Indexed monadic state at start of function body.
--
-- Adds the required function variables to the map of in-scope bindings.
type family FunctionDefinitionStartState
( k :: Symbol )
( as :: BindingsMap )
( s :: ProgramState )
= ( j :: ProgramState )
| j -> k as
where
FunctionDefinitionStartState k as ('ProgramState i ctx cfg funs eps iface rayQueries bkend)
= 'ProgramState (Union i as) ('InFunction k as) cfg funs eps iface rayQueries bkend
type family FunctionDefinitionEndState
( k :: Symbol )
( as :: BindingsMap )
( bds :: BindingsMap )
( i :: ProgramState )
= ( j :: ProgramState )
| j -> k as bds
where
FunctionDefinitionEndState k as bds ('ProgramState _ _ cfg funs eps iface rayQueries bkend)
= 'ProgramState
bds
( 'InFunction k as)
cfg
funs
eps
iface
rayQueries
bkend
type family GetFunctionInfo
( k :: Symbol )
( i :: ProgramState )
:: FunctionInfo
where
GetFunctionInfo k ('ProgramState _ _ _ funs _ _ _ _)
= GetFunctionInfoFromLookup k (Lookup k funs)
type family FunctionTypes
( k :: Symbol )
( i :: ProgramState )
:: ( BindingsMap, Type )
where
FunctionTypes k i = FunctionTypesFromInfo (GetFunctionInfo k i)
type family FunctionTypesFromInfo
( info :: FunctionInfo )
:: ( BindingsMap, Type )
where
FunctionTypesFromInfo ('FunctionInfo as b _ _) = '( as, b )
type family GetFunctionInfoFromLookup
( k :: Symbol )
( mbFun :: Maybe FunctionInfo )
:: FunctionInfo
where
GetFunctionInfoFromLookup _ (Just info) = info
GetFunctionInfoFromLookup k 'Nothing
= TypeError
( Text "'fundef': function named " :<>: ShowType k
:<>: Text " has not been declared (no function info)."
)
-- | Adds a function binding to the indexed monadic state.
type family AddFunBinding (k :: Symbol) (as :: BindingsMap) (b :: Type) (s :: ProgramState) :: ProgramState where
AddFunBinding k as b ('ProgramState bds ctx cfg funs eps iface rayQueries bkend)
-- 'ValidFunDef' should have already checked that name 'k' is not already in use
= 'ProgramState (Insert k (Fun as b) bds) ctx cfg (SetFunctionDefined k funs) eps iface rayQueries bkend
type family SetFunctionDefined
( k :: Symbol )
( funs :: Map Symbol FunctionInfo )
:: Map Symbol FunctionInfo
where
SetFunctionDefined k '[]
= TypeError
( Text "'fundef': function named " :<>: ShowType k
:<>: Text " has not been declared."
)
SetFunctionDefined k ( ( k ':-> 'FunctionInfo as b fc Declared ) ': funs )
= ( k ':-> 'FunctionInfo as b fc Defined ) ': funs
SetFunctionDefined k ( ( k ':-> 'FunctionInfo _ _ _ Defined ) ': _ )
= TypeError
( Text "'fundef': function named " :<>: ShowType k
:<>: Text " has already been defined."
)
SetFunctionDefined k ( fun ': funs )
= fun ': SetFunctionDefined k funs
-- | Set the monadic context: within a function body.
type family SetFunctionContext
( k :: Symbol )
( as :: BindingsMap )
( s :: ProgramState )
:: ProgramState where
SetFunctionContext k as ('ProgramState bds TopLevel cfg funs eps iface rayQueries bkend)
= 'ProgramState bds ('InFunction k as) cfg funs eps iface rayQueries bkend
SetFunctionContext k _ ('ProgramState _ ('InFunction l _) _ _ _ _ _ _)
= TypeError
( Text "'fundef': unexpected nested function definition."
:$$: Text "Function " :<>: ShowType k
:<>: Text " declared inside the body of function " :<>: ShowType l :<>: Text "."
)
SetFunctionContext k _
( 'ProgramState _ ('InEntryPoint stageName ( _ :: SPIRV.ExecutionInfo Nat em) _) _ _ _ _ _ _ )
= TypeError
( Text "'fundef': unexpected function definition inside entry point."
:$$: Text "Function " :<>: ShowType k
:<>: Text " declared inside " :<>: Text (SPIRV.NamedExecutionModel stageName em)
:<>: Text "."
)
-- | Check that a function definition is valid.
--
-- Throws a type error if:
--
-- * function is not declared at the top level,
-- * function name is already in use,
-- * one of the function's arguments is itself a function,
-- * another function is defined inside the function,
type family ValidFunDef
( k :: Symbol ) -- name of function to be defined
( as :: BindingsMap ) -- function arguments
( s :: ProgramState ) -- indexed state at the point the function is definition
( l :: BindingsMap ) -- total bindings at the end of the function definition
:: Constraint
where
ValidFunDef k _ ('ProgramState _ ('InFunction l _) _ _ _ _ _ _ ) _
= TypeError
( Text "'fundef': unexpected nested function definition."
:$$: Text "Function " :<>: ShowType k
:<>: Text " declared inside the body of function " :<>: ShowType l :<>: Text "."
)
ValidFunDef k _
( 'ProgramState _ ('InEntryPoint stageName ( _ :: SPIRV.ExecutionInfo Nat em) _) _ _ _ _ _ _)
_
= TypeError
( Text "'fundef': unexpected function definition inside entry point."
:$$: Text "Function " :<>: ShowType k
:<>: Text " declared inside " :<>: Text (SPIRV.NamedExecutionModel stageName em)
:<>: Text "."
)
ValidFunDef k as ('ProgramState i 'TopLevel _ _ _ _ _ _) l
= ( NoFunctionNameConflict k ( Lookup k i ) -- check that function name is not already in use
, ValidArguments k as (Remove i (Remove as l)) )
-- │ └━━━━━━┬━━━━━┘
-- │ │
-- │ │
-- │ local variables ├━━━━━━━━┘
-- │
-- └━━┤ check that none of the function arguments or local variables are themselves functions or images
type ValidArguments (k :: Symbol) (as :: BindingsMap) (l :: BindingsMap)
= ( ValidArguments' k as l as l :: Constraint )
type family ValidArguments'
( k :: Symbol )
( as :: BindingsMap )
( l :: BindingsMap )
( as_rec :: BindingsMap )
( l_rec :: BindingsMap )
:: Constraint where
ValidArguments' _ _ _ '[] '[] = ()
ValidArguments' k as _ ((v ':-> Fun _ _) ': _ ) _ = TypeError
( Text "'fundef': forbidden higher order argument " :<>: ShowType v :<>: Text ","
:$$: Text "in function definition for " :<>: ShowType k :<>: Text ","
:$$: Text "when trying to abstract over:"
:$$: ShowType as
:$$: Text "Function definitions can only abstract over variables, not over functions."
)
ValidArguments' k as l (_ ': as_rec) l_rec = ValidArguments' k as l as_rec l_rec
ValidArguments' k _ l _ ((v ':-> Fun _ _) ': _ ) = TypeError
( Text "'fundef': unexpected nested function definition inside function " :<>: ShowType k :<>: Text ":"
:$$: Text "local name " :<>: ShowType v :<>: Text " binds a function."
:$$: Text "Local bindings for " :<>: ShowType k :<>: Text " are:"
:$$: ShowType l
)
ValidArguments' k as l as_rec (_ ': l_rec) = ValidArguments' k as l as_rec l_rec
type family NoFunctionNameConflict
( k :: Symbol )
( mb_bd :: Maybe Binding ) -- conflict with in-scope variables?
:: Constraint where
NoFunctionNameConflict k ('Just _) = TypeError
( Text "'fundef': cannot define a new function with name " :<>: ShowType k :<>: Text "."
:$$: Text "that name is already in scope."
)
NoFunctionNameConflict _ 'Nothing = ()
-------------------------------------------------
-- * Constraints for 'FIR.Syntax.Program.entryPoint'
-- | Check that an entry point definition is valid.
--
-- Throws a type error if:
--
-- * a function is defined within the entry point,
-- * the name of a builtin for this entry point is already in use.
type family ValidEntryPoint
( k :: Symbol )
( nfo :: SPIRV.ExecutionInfo Nat s )
( i :: ProgramState )
( l :: BindingsMap )
:: Constraint where
ValidEntryPoint k (nfo :: SPIRV.ExecutionInfo Nat s) ('ProgramState i _ _ _ eps _ _ bkend) l
= ( ValidInterface k ( LookupEntryPointInfo k s eps )
, NoEntryPointNameConflict k (Lookup k i)
, ValidLocalBehaviour s (Remove i l)
, BuiltinsDoNotAppearBefore s (ModelBuiltins nfo) i
)
type family EntryPointsBackend
( eps :: [ Symbol :-> ( SPIRV.ExecutionModel, modes ) ] )
:: SPIRV.Backend
where
EntryPointsBackend '[]
= TypeError
( Text "SPIR-V module must specify at least one entry point."
:$$: Text "Entry points are specified as part of a type signature containing module definitions."
:$$: Text "For instance, a fragment shader can be specified as follows:"
:$$: Text " \"main\" ':-> EntryPoint '[ OriginUpperLeft ] Fragment "
)
EntryPointsBackend ( ( k ':-> '( s, _ ) ) ': eps )
= CompatibleWithBackend k s (SPIRV.BackendOf s) eps
type family CompatibleWithBackend
( k :: Symbol )
( s :: SPIRV.ExecutionModel )
( bkend :: SPIRV.Backend )
( eps :: [ Symbol :-> ( SPIRV.ExecutionModel, modes ) ] )
:: SPIRV.Backend
where
CompatibleWithBackend _ _ bk '[] = bk
CompatibleWithBackend k s bk ( ( k' ':-> '( s', _ ) ) ': eps )
= If ( SPIRV.BackendOf s' == bk )
( CompatibleWithBackend k s bk eps )
( TypeError
( Text "Incompatible backends."
:$$: Text ( SPIRV.NamedExecutionModel k s )
:<>: Text " uses " :<>: ShowType bk :<>: Text ","
:$$: Text "while " :<>: Text ( SPIRV.NamedExecutionModel k' s' )
:<>: Text " uses " :<>: ShowType ( SPIRV.OtherBackend bk ) :<>: Text "."
)
)
-- | Indexed monadic state at start of entry point body.
type family EntryPointStartState
( k :: Symbol )
( nfo :: SPIRV.ExecutionInfo Nat s )
( i :: ProgramState )
= ( j :: ProgramState )
| j -> k nfo
where
EntryPointStartState k nfo ('ProgramState bds _ cfg funs eps g_iface _ bkend)
= 'ProgramState
( Union bds (ModelBuiltins nfo) ) -- bindings at the beginning
( 'InEntryPoint -- context: now within an entry point
k
nfo
( 'Just '[] ) -- initial empty interface
)
cfg
funs
eps
g_iface
'[] -- no ray queries to start off with
bkend
-- | Indexed monadic state at end of entry point body.
type family EntryPointEndState
( k :: Symbol )
( nfo :: SPIRV.ExecutionInfo Nat s )
( bds :: BindingsMap )
( iface :: TLInterface )
( i :: ProgramState )
= ( j :: ProgramState )
| j -> k nfo bds iface
where
EntryPointEndState k nfo bds iface ('ProgramState _ _ cfg funs eps g_iface rayQueries bkend)
= 'ProgramState
bds
( InEntryPoint k nfo ('Just iface) )
cfg
funs
eps
g_iface
rayQueries
bkend
type family GetExecutionInfo
( k :: Symbol )
( em :: SPIRV.ExecutionModel )
( i :: ProgramState )
:: SPIRV.ExecutionInfo Nat em
where
GetExecutionInfo k em ('ProgramState _ _ _ _ eps _ _ _)
= GetExecutionInfoOf k em eps
type family GetExecutionInfoOf
( k :: Symbol )
( em :: SPIRV.ExecutionModel )
( i :: [ Symbol :-> EntryPointInfo ] )
:: SPIRV.ExecutionInfo Nat em
where
GetExecutionInfoOf k em '[]
= TypeError
( Text "'GetExecutionInfo': cannot find "
:<>: Text (SPIRV.NamedExecutionModel k em)
:<>: Text "."
)
GetExecutionInfoOf k em
( ( k ':-> 'EntryPointInfo (nfo :: SPIRV.ExecutionInfo Nat em) _ _ ) ': _ )
= nfo
GetExecutionInfoOf k em (_ ': eps)
= GetExecutionInfoOf k em eps
type family SetInterface
( k :: Symbol )
( nfo :: SPIRV.ExecutionInfo Nat s )
( iface :: TLInterface )
( i :: ProgramState )
:: ProgramState
where
SetInterface k (nfo :: SPIRV.ExecutionInfo Nat s) iface ('ProgramState i fc cfg funs eps globalIface rayQueries bkend)
= 'ProgramState i fc cfg funs (SetInterfaceOf k s iface eps) globalIface rayQueries bkend
type family SetInterfaceOf
( k :: Symbol )
( em :: SPIRV.ExecutionModel )
( iface :: TLInterface )
( eps :: [ Symbol :-> EntryPointInfo ] )
:: [ Symbol :-> EntryPointInfo ]
where
SetInterfaceOf k em _ '[]
= TypeError
( Text "'SetInterface': cannot find "
:<>: Text (SPIRV.NamedExecutionModel k em)
:<>: Text "."
)
SetInterfaceOf k em iface
( ( k ':-> 'EntryPointInfo (nfo :: SPIRV.ExecutionInfo Nat em) _ Declared ) ': eps )
= ( k ':-> 'EntryPointInfo nfo iface Defined ) ': eps
SetInterfaceOf k em iface
( (k ':-> 'EntryPointInfo (nfo :: SPIRV.ExecutionInfo Nat em) _ Defined ) ': _ )
= TypeError
( Text "'entryPoint': entry point "
:<>: Text (SPIRV.NamedExecutionModel k em)
:<>: Text " has already been defined."
)
SetInterfaceOf k em iface (ep ': eps)
= ep ': SetInterfaceOf k em iface eps
type family InsertEntryPointInfo
( k :: Symbol )
( nfo :: EntryPointInfo )
( eps :: [ Symbol :-> EntryPointInfo ] )
:: [ Symbol :-> EntryPointInfo ]
where
InsertEntryPointInfo k nfo '[]
= '[ k ':-> nfo ]
InsertEntryPointInfo k
( 'EntryPointInfo (nfo :: SPIRV.ExecutionInfo Nat s1) iface def)
( ( l ':-> 'EntryPointInfo (nfo2 :: SPIRV.ExecutionInfo Nat s2) iface2 def2 ) ': eps )
= InsertEntryPointInfoWithComparison
( k `Compare` l )
( s1 `Compare` s2 )
k ( 'EntryPointInfo nfo iface def )
l ( 'EntryPointInfo nfo2 iface2 def2 )
eps
type family InsertEntryPointInfoWithComparison
( cmpName :: Ordering )
( cmpStage :: Ordering )
( name1 :: Symbol )
( nfo1 :: EntryPointInfo )
( name2 :: Symbol )
( nfo2 :: EntryPointInfo )
( nfos :: [ Symbol :-> EntryPointInfo ] )
:: [ Symbol :-> EntryPointInfo ]
where
-- NB: duplicate declarations are reported by 'FIR.Validation.Definitions.ValidDefinitions'.
InsertEntryPointInfoWithComparison EQ EQ
_ _
name2 nfo2
nfos
= ( name2 ':-> nfo2 ) ': nfos
InsertEntryPointInfoWithComparison cmpName cmpStage name1 nfo1 name2 nfo2 nfos
= If ( cmpName == LT || ( cmpName == EQ && cmpStage == LT ) )
( ( name1 ':-> nfo1 ) ': ( name2 ':-> nfo2 ) ': nfos )
( ( name2 ':-> nfo2 ) ': InsertEntryPointInfo name1 nfo1 nfos )
type family LookupEntryPointInfo
( name :: Symbol )
( em :: SPIRV.ExecutionModel )
( eps :: [ Symbol :-> EntryPointInfo ] )
:: EntryPointInfo
where
LookupEntryPointInfo name em
( ( name ':-> 'EntryPointInfo ( nfo :: SPIRV.ExecutionInfo Nat em ) iface defi ) ': _ )
= 'EntryPointInfo nfo iface defi
LookupEntryPointInfo name em ( _ ': eps ) = LookupEntryPointInfo name em eps
LookupEntryPointInfo name em '[]
= TypeError
( Text "'entryPoint': cannot define "
:<>: Text (SPIRV.NamedExecutionModel name em) :<>: Text "."
:$$: Text "No such entry point has been declared in the top-level definitions of the program."
)
type family NoEntryPointNameConflict
( k :: Symbol )
( mb_bd :: Maybe Binding )
:: Constraint where
NoEntryPointNameConflict k ('Just _) = TypeError
( Text "'entryPoint': cannot define a new entry point with name " :<>: ShowType k :<>: Text "."
:$$: Text "That name is already in scope."
)
NoEntryPointNameConflict _ 'Nothing = ()
type ValidLocalBehaviour (s :: SPIRV.ExecutionModel) (l :: BindingsMap)
= ( ValidLocalBehaviour' s l l :: Constraint )
type family ValidLocalBehaviour'
( s :: SPIRV.ExecutionModel )
( l :: BindingsMap )
( l_rec :: BindingsMap )
:: Constraint where
ValidLocalBehaviour' _ _ '[] = ()
ValidLocalBehaviour' s l ((_ ':-> Var _ _) ': l_rec) = ValidLocalBehaviour' s l l_rec
ValidLocalBehaviour' s l ((v ':-> Fun _ _) ': _ ) = TypeError
( Text "'entryPoint': unexpected nested function definition inside " :<>: ShowType s :<>: Text " entry point:"
:$$: Text "local name " :<>: ShowType v :<>: Text "binds a function."
:$$: Text "Local bindings for " :<>: ShowType s :<>: Text " entry point are:"
:$$: ShowType l
)
type family BuiltinsDoNotAppearBefore
( s :: SPIRV.ExecutionModel )
( builtins :: BindingsMap )
( i :: BindingsMap )
:: Constraint where
BuiltinsDoNotAppearBefore _ '[] _ = ()
BuiltinsDoNotAppearBefore s ((b ':-> _) ': bs) i
= BuiltinDoesNotAppearBefore s b bs i (Lookup b i)
type family BuiltinDoesNotAppearBefore
( s :: SPIRV.ExecutionModel )
( b :: Symbol )
( bs :: BindingsMap )
( i :: BindingsMap )
( lkp :: Maybe Binding )
:: Constraint where
BuiltinDoesNotAppearBefore s _ bs i 'Nothing = BuiltinsDoNotAppearBefore s bs i
BuiltinDoesNotAppearBefore s b _ i ('Just _)
= TypeError ( Text "'entryPoint': conflict with built-in variable for " :<>: ShowType s :<>: Text " stage."
:$$: Text "Variable with name " :<>: ShowType b :<>: Text " is a built-in, yet is already bound."
:$$: Text "Variables in scope at site of entry point definition are:"
:$$: ShowType i
)
-------------------------------------------------
-- * Constraints for 'FIR.Syntax.Program.embed'.
class Known [Symbol] (Keys (Bindings i)) => Embeddable (i :: ProgramState) (j :: ProgramState) where
instance ( Known [Symbol] (Keys (Bindings i)), CanEmbed i j ) => Embeddable i j where
type family CanEmbed (i :: ProgramState) (j :: ProgramState) :: Constraint where
CanEmbed ('ProgramState '[] 'TopLevel _ '[] _ _ _ _) _ = ()
CanEmbed ('ProgramState i_bds i_ctx _ i_funs _ _ _ _) ('ProgramState j_bds i_ctx _ j_funs _ _ _ _)
= ( SubsetBindings i_bds j_bds
, SubsetFunctions i_funs j_funs
)
CanEmbed ('ProgramState _ i_ctx _ _ _ _ _ _) ('ProgramState _ j_ctx _ _ _ _ _ _)
= TypeError
( Text "'embed': cannot embed computation with function context "
:<>: ShowType i_ctx
:<>: Text " into computation with function context "
:<>: ShowType j_ctx
:<>: Text "."
)
type family SubsetBindings (is :: BindingsMap) (js :: BindingsMap) :: Constraint where
SubsetBindings '[] _ = ()
SubsetBindings (i ': is) js
= If (i `Elem` js)
( SubsetBindings is js )
( TypeError
( Text "'embed': cannot embed computation."
:$$: Text "Binding " :<>: ShowType i
:<>: Text " is missing in larger context "
:<>: ShowType js
:<>: Text "."
)
)
type family SubsetFunctions
( fs :: Map Symbol FunctionInfo )
( gs :: Map Symbol FunctionInfo )
:: Constraint where
SubsetFunctions '[] _ = ()
SubsetFunctions ( (k ':-> f) ': fs) gs
= SubsetFunctionsRec k f (Lookup k gs) fs gs
type family SubsetFunctionsRec
( k :: Symbol )
( f :: FunctionInfo )
( g :: Maybe FunctionInfo )
( fs :: Map Symbol FunctionInfo )
( gs :: Map Symbol FunctionInfo )
:: Constraint where
SubsetFunctionsRec k _ Nothing _ _
= TypeError
( Text "'embed': cannot embed computation."
:$$: Text "Function named " :<>: ShowType k
:<>: Text " is missing in larger context."
)
SubsetFunctionsRec _ f (Just f) fs gs
= SubsetFunctions fs gs
SubsetFunctionsRec k f (Just f') _ _
= TypeError
( Text "'embed': cannot embed computation."
:$$: Text "Mismatch between functions of name " :<>: ShowType k
:<>: Text "."
:$$: Text " - Smaller context function info: " :<>: ShowType f :<>: Text ","
:$$: Text " - Larger context function info: " :<>: ShowType f' :<>: Text "."
)