-      !"#$%&'()*+,-./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'*Application of the Pair type constructor. (*Application of the List type constructor. 55Check whether a witness is a capability constructor. 65Check whether an expression is the unit constructor. 7"Take a region handle from a type. 8)Take a region handle from an expression. 9Make 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. @2Take an integer literal from an data constructor. A,Take an integer literal from an expression. '()*+,-./0123456789:;<=>?@A'()*+,-./0123456789:;<=>?@A'()*+.,-/014235<6789:;=>?@A'()*+,-./0123456789:;<=>?@ANoneBData type definitions for:  Type Constructors  ---- ------------  Int 0 1 2 3 ...  Pair Pr  List Nil Cons C;Kind environment containing kinds of primitive data types. D#Take the kind of a primitive name. Returns  if the name isn't primitive. EIType 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#F#Take the type of a primitive name. Returns  if the name isn't primitive. G$Take the arity of a primitive name. BCDEFGBCDEFGBCDEFGBCDEFGNoneH7Core language fragment that can be directly evaluated. -Language features used by the eval fragment. HHHHNoneIStore binding. I These are naked objects that can be allocated directly into the heap. J#A thunk, used for lazy evaluation. L1Lambda abstraction, used for recursive bindings. P The flag indicates whether each binder is level-1 (True) or level-0 (False). OAn algebraic data constructor. T!Next store location to allocate. U Next region handle to allocate. V"Region handles already allocated. W/Regions that are marked as global, and are not ( deallocated with a stack discipline. X$Map of locations to store bindings,  their types, & and the handle for the regions they're in. Y@Initial store containing the preallocated regions and bindings. Z$Location of the static unit object. [6Check 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. a1Check whether a store contains the given region. bSet a region as being global. c9Add a store binding to the store, at the given location. d.Allocate a new binding into the given region,  returning the new location. e6Alloc some recursive bindings into the given region, " returning the new locations. f%Lookup a the binding for a location. g%Lookup the type of a store location. h;Lookup the region handle, type and binding for a location. "IJKLMNOPQRSTUVWXYZ[\]^_`abcdefgh$IJKLMNOPQRSTUVWXYZ[\]^_`abcdefgh$RSTUVWXIOLJPQMNKYZ[\]^_`abcdefghIOLJPQMNKRSTUVWXYZ[\]^_`abcdefghNoneiFStep a primitive constructor, which allocates an object in the store. jStep a primitive operator. kLike ^+ but return the region handle wrapped in a . lLike `) but accept a region handle wrapped in a . iData constructor to evaluate. Arguments to constructor. Current store. "New store and result expression, $ if the operator steps, otherwise . jName of operator to evaluate. Arguments to operator. Current store. "New store and result expression, $ if the operator steps, otherwise . klijklijklijklNone m(The result of stepping some expression. n,Expression is stuck, and we know for sure it' s mistyped. o3Expression cannot step, and is not a (weak) value. ) The original expression was mistyped, / or something is wrong with the interpreter. p.Expression cannot step and is a (weak) value.  We're done already. q&Expression progressed to a new state. r*Single step a core expression to a value. As opposed to s2, if the provided expression is the location of a ) Thunk, then the thunk will be forced. s/Single step a code expression to a weak value. As opposed to r3, 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. t#Check if an expression is a value.  Values can')t be progressed any further, with either r or s. u)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 r , but not s. (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. mnopqrCurrent store. Expression to force. Result of forcing it. sCurrent store. Expression to step. Result of stepping it. tu mnopqrstu mqponrstu mqponrstuNone v=Things that can go wrong with the capabilities in a program. w9A capability constructor applied to a non-region handle.  As with x* we only need to check for this because we're H using general witness application to represent capabilities, instead  of having an atomic form. x,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. z%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. vwxyz{|}  ~   vwxyz{|}~ ~vzxw{|}yyvzxw{|}yy  ~   NoneHmnopqrsHmqponrs     !!""#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~       !"#$%&'()*+ddc-core-eval-0.3.2.1DDC.Core.Eval.NameDDC.Core.Eval.CompoundsDDC.Core.Eval.EnvDDC.Core.Eval.ProfileDDC.Core.Eval.StoreDDC.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 lexExpStringtPairtListwGlobalwConstwMutablewLazy wManifest wDistinctwcGlobalwcConst wcMutablewcLazy wcManifest wcDistinct isCapConWisUnitX takeHandleT takeHandleXxLoctakeLocX stripLocX takeMutableXtInttcIntdcInt takeIntDCtakeIntX primDataDefs primKindEnvkindOfPrimName primTypeEnvtypeOfPrimName arityOfName evalProfileSBindSThunk sbindThunkExpSLams sbindLamBinds sbindLamBodySObj sbindDataTag sbindDataArgsStore storeNextLoc storeNextRgn storeRegions storeGlobal storeBindsinitiallocUnit isUnitOrLocXnewLocnewLocsnewRgnnewRgnsdelRgnhasRgn setGlobaladdBind allocBind allocBinds lookupBindlookupTypeOfLoclookupRegionTypeBind 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 $fNFDataNameddc-core-0.3.2.1DDC.Core.Compounds.AnnotxUnit takeXTypetakePrimWiConAppstakeWAppsAsList takeXWitnesswAppswApp bindsOfPattakeCtorNameOfAltvalwitBindsOfLetsspecBindsOfLets bindsOfLets splitXLets xLetsAnnotxLets takeXConApps takeXPrimAppstakeXAppsWithAnnotstakeXAppsAsList takeXApps1 takeXAppsmakeXAppsWithAnnotsxApps takeXLamFlags makeXLamFlags takeXLams takeXLAMsxLamsxLAMstakeAnnotOfExpDDC.Core.Exp.DaCon mkDaConSolid mkDaConAlgdcUnit typeOfDaContakeNameOfDaConDDC.Type.Compounds tConData1 tConData0 tManifest tHeadLazytLazy tDistinct tDeepMutabletMutable tDeepConsttConst tDeepGlobaltGlobaltEmptytPuretDeepUsetUse tDeepAlloctAlloc tDeepWritetWrite tDeepRead tHeadReadtReadkWitnesskClosurekEffectkRegionkDatasPropsComptSusptImpl arityOfTypetakeTFunAllArgResulttakeTFunWitArgResulttakeTFunArgResult takeTFunECtakeTFun tFunOfListPE tFunOfListtFunPEtFunECtFuntakeResultKind takeKFuns' takeKFunstakeKFunkFunskFuntUnittSum eraseTForalls takeTForalls tForalls'tForallstForall'tForalltakePrimeRegiontakeDataTyConAppstakePrimTyConApps takeTyConApps takeTAppstApps$:tApptBottIxreplaceTypeOfBoundtakeSubstBoundsOfBindstakeSubstBoundOfBindnamedBoundMatchesBindboundMatchesBindtakeNameOfBoundpartitionBindsByTypemakeBindFromBinder binderOfBindreplaceTypeOfBind typeOfBindtakeNameOfBindbase Data.MaybeNothing evalFeatures $fPrettySBind $fPrettyStoreDDC.Type.Exp.BaseBound tagMatchesAlt tagMatchesPat isSomeValueregionWitnessOfType unwrapCasts wrapCastsCapSetCheckM emptyCapSet mustInsertCapGHC.Errerror takeNameRgn checkCapSet checkCapsXM capsGlobal capsConst capsMutable capsDistinctcapsLazy capsManifest checkCapsCM checkCapsLM checkCapsAM checkCapsWM $fPrettyError