!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ NoneA primitive operator. A primitive constructor. Cons data constructor. Nil data constructor. P data construct (pairs). List type constructor. Pair type constructor. Int type constructor. EThese are primitive witnesses that guarantee the associated property F of the program. Ostensibly, they are only introduced by the system E at runtime, but for testing purposes we can also inject them into  the source program. #Witness that a region is manifest. 3 This ensures there are no thunks in the region, & which prevents it from being Lazy. Witness that a region is lazy. 1 This lets is allocate thunks into the region, ( and prevents it from being Manifest. 'Witness that some regions are distinct 6 This lets us perform aliasing based optimisations. "Witness that a region is mutable. / This lets us update objects in the region, ( and prevents it from being Constant. #Witness that a region is constant. : This lets us purify read and allocation effects on it, ' and prevents it from being Mutable. !Witness that a region is global. C Global regions live for the duration of the program and are not D deallocated in a stack like manner. This lets us hide the use of B such regions, and rely on the garbage collector to reclaim the  space. A region handle. These are pretty printed like R5#. A store location. These are pretty printed like L4#. -Names of things recognised by the evaluator. Store capabilities. Region handles. Store locations. Primitive operators (eg addInt, subInt). Primitive constructors (eg  List, Nil). !,Integer literals (which data constructors). "User constructors. #User variables. $Read a primitive name. %/Lex a string to tokens, using primitive names. :The first argument gives the starting source line number. &/Lex a string to tokens, using primitive names. :The first argument gives the starting source line number. 3  !"#$%&'  !"#$%&'#"!   $%&  #"! $%&None'Store binding. I These are naked objects that can be allocated directly into the heap. (#A thunk, used for lazy evaluation. *1Lambda abstraction, used for recursive bindings. P The flag indicates whether each binder is level-1 (True) or level-0 (False). -An algebraic data constructor. 2!Next store location to allocate. 3 Next region handle to allocate. 4"Region handles already allocated. 5/Regions that are marked as global, and are not ( deallocated with a stack discipline. 6$Map of locations to store bindings,  their types, & and the handle for the regions they're in. 7@Initial store containing the preallocated regions and bindings. 8$Location of the static unit object. 96Check whether an expression is the unit constructor,  or its static heap location. :$Create a new location in the store. ;+Create several new locations in the store. <"Create a new region in the store. =(Create several new regions in the store >,Delete a region, removing all its bindings. ?1Check whether a store contains the given region. @Set a region as being global. A9Add a store binding to the store, at the given location. B.Allocate a new binding into the given region,  returning the new location. C6Alloc some recursive bindings into the given region, " returning the new locations. D%Lookup a the binding for a location. E%Lookup the type of a store location. F;Lookup the region handle, type and binding for a location. "'()*+,-./0123456789:;<=>?@ABCDEF$'()*+,-./0123456789:;<=>?@ABCDEF$0123456'-*(./+,)789:;<=>?@ABCDEF'-*(./+,)0123456789:;<=>?@ABCDEFNoneG*Application of the Pair type constructor. H*Application of the List type constructor. U5Check whether a witness is a capability constructor. VMake a unit literal. W5Check whether an expression is the unit constructor. X"Take a region handle from a type. Y)Take a region handle from an expression. ZMake a location expression. [*Take a store location from an expression.  We strip off forget casts along the way \=Take a store location from an expression, reaching under any forget casts. ]1Take a witness of mutability from an expression. ^)Application of the Int type constructor. _The integer type constructor `"Make an integer data constructor. a2Take an integer literal from an data constructor. b,Take an integer literal from an expression. GHIJKLMNOPQRSTUVWXYZ[\]^_`abGHIJKLMNOPQRSTUVWXYZ[\]^_`abGHIJKNLMOPQTRSU]VWXYZ[\^_`abGHIJKLMNOPQRSTUVWXYZ[\]^_`abNonecData type definitions for:  Type Constructors  ---- ------------  Int 0 1 2 3 ...  Pair Pr  List Nil Cons d;Kind environment containing kinds of primitive data types. e#Take the kind of a primitive name. Returns  if the name isn't primitive. fIType environment containing types of primitive data constructors as well ) as the following primitive operators:  8negInt, addInt, subInt, mulInt, divInt, eqInt, updateIntBIt also contains types for the primitive capability constructors: Global#, Const# , Mutable#, Lazy# , Manifest#g#Take the type of a primitive name. Returns  if the name isn't primitive. h$Take the arity of a primitive name. cdefghcdefghcdefghcdefghNonei7Core language fragment that can be directly evaluated. -Language features used by the eval fragment. iiiiNonejFStep a primitive constructor, which allocates an object in the store. kStep a primitive operator. lLike <+ but return the region handle wrapped in a . mLike >) but accept a region handle wrapped in a . jData constructor to evaluate. Arguments to constructor. Current store. "New store and result expression, $ if the operator steps, otherwise . kName of operator to evaluate. Arguments to operator. Current store. "New store and result expression, $ if the operator steps, otherwise . lmjklmjklmjklmNone n(The result of stepping some expression. o,Expression is stuck, and we know for sure it' s mistyped. p3Expression cannot step, and is not a (weak) value. ) The original expression was mistyped, / or something is wrong with the interpreter. q.Expression cannot step and is a (weak) value.  We're done already. r&Expression progressed to a new state. s*Single step a core expression to a value. As opposed to t2, if the provided expression is the location of a ) Thunk, then the thunk will be forced. t/Single step a code expression to a weak value. As opposed to s3, if the provided expression is the location of a ( Thunk, then the thunk is not forced. 5See if a constructor tag matches a case alternative. ,See if a constructor tag matches a pattern. u#Check if an expression is a value.  Values can')t be progressed any further, with either s or t. v)Check if an expression is a weak values. A These are all the values, and locations that point to thunks. #Weak values can be progressed with s , but not t. (Check if an expression is a weak value. JGet the region witness corresponding to one of the witness types that are  permitted in a letregion. nopqrsCurrent store. Expression to force. Result of forcing it. tCurrent store. Expression to step. Result of stepping it. uv nopqrstuv nrqpostuv nrqpostuvNone w=Things that can go wrong with the capabilities in a program. x9A capability constructor applied to a non-region handle.  As with y* we only need to check for this because we're H using general witness application to represent capabilities, instead  of having an atomic form. y,A partially applied capability constructor. @ In the formal semantics, capabilities are atomic, so this isn't  a problem. However, as we'*re representing them with general witness 5 appliction we need to ensure the constructors aren' t partially  applied. {%Conflicting capabilities in program. Set of used capabilities. Capability Checking monad. 6Check for conflicting store capabilities in a module. ;Check for conflicting store capabilities in an expression. An empty capability set Insert a capability, or  if this isn't one. ,Take a region name from a witness argument. ?Check a capability set for conflicts between the capabilities. 4Collect the list of capabilities in an expression, ( and check that they are well-formed. wxyz{|}~ wxyz{|}~ w{yx|}~zzw{yx|}~zz Noneinopqrstinrqpost     !!""#$%&'()*+,-./01234567889:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ddc-core-eval-0.3.1.1DDC.Core.Eval.NameDDC.Core.Eval.StoreDDC.Core.Eval.CompoundsDDC.Core.Eval.EnvDDC.Core.Eval.ProfileDDC.Core.Eval.PrimDDC.Core.Eval.StepDDC.Core.Eval.Check DDC.Core.EvalPrimOp PrimOpCopyIntPrimOpUpdateInt PrimOpEqInt PrimOpDivInt PrimOpMulInt PrimOpSubInt PrimOpAddInt PrimOpNegIntPrimCon PrimDaConCons PrimDaConNil PrimDaConPr PrimTyConList PrimTyConPair PrimTyConIntCap CapManifestCapLazy CapDistinct CapMutableCapConst CapGlobalRgnLocNameNameCapNameRgnNameLoc NamePrimOp NamePrimConNameIntNameConNameVarreadNamelexModuleString lexExpStringSBindSThunk sbindThunkExpSLams sbindLamBinds sbindLamBodySObj sbindDataTag sbindDataArgsStore storeNextLoc storeNextRgn storeRegions storeGlobal storeBindsinitiallocUnit isUnitOrLocXnewLocnewLocsnewRgnnewRgnsdelRgnhasRgn setGlobaladdBind allocBind allocBinds lookupBindlookupTypeOfLoclookupRegionTypeBindtPairtListwGlobalwConstwMutablewLazy wManifest wDistinctwcGlobalwcConst wcMutablewcLazy wcManifest wcDistinct isCapConWxUnitisUnitX takeHandleT takeHandleXxLoctakeLocX stripLocX takeMutableXtInttcIntdcInt takeIntDCtakeIntX primDataDefs primKindEnvkindOfPrimName primTypeEnvtypeOfPrimName arityOfName evalProfile stepPrimCon stepPrimOp primNewRegion primDelRegion StepResult StepMistyped StepStuckStepDone StepProgressforcestepisValue isWeakValueErrorErrorNonHandle ErrorPartial errorWitness ErrorConflict errorRegions errorCap1 errorCap2checkCapsModule checkCapsX$fPrettyPrimOp$fNFDataPrimOp$fPrettyPrimCon$fNFDataPrimCon $fPrettyCap $fNFDataCap $fPrettyRgn $fNFDataRgn $fPrettyLoc $fNFDataLoc $fPrettyName $fNFDataName $fPrettySBind $fPrettyStorebase Data.MaybeNothing evalFeaturesddc-core-0.3.1.1DDC.Type.Exp.BaseBound tagMatchesAlt tagMatchesPat isSomeValueregionWitnessOfType unwrapCasts wrapCastsCapSetCheckM emptyCapSet mustInsertCapGHC.Errerror takeNameRgn checkCapSet checkCapsXM capsGlobal capsConst capsMutable capsDistinctcapsLazy capsManifest checkCapsCM checkCapsLM checkCapsMM checkCapsAM checkCapsWM $fPrettyError