Agda Functions Index

This page lists all functions and operators defined in the Agda modules.

Operators

Background › BasicTypes

Background › InteractionTrees

_<?_$>_
_>>=_

Background › Objects

examples › RunnerUtilities

_>>_

Regular Functions

AVM › Context

AVM › Instruction

AVM › Interpreter

Background › BasicTypes

Background › InteractionTrees

Background › Objects

Background › StatelessObjects

examples › Battleship › Game

examples › Battleship › PlayerBoard

examples › Battleship › Runner

examples › Common › Display

examples › Common › Equality

examples › Common › InterpreterSetup

interpretAVMProgramRec

examples › Common › StateInit

examples › PingPong › Main

examples › PingPong › Runner

examples › RunnerUtilities

References to other modules

This page references the following modules:

AVM.Context
- Symbols: ObjError, IntrospectError, ReflectError, ReifyError, TxError, MachineError, ControllerError, PureError, FDError, NondetError, BaseError, TxLayerError, PureLayerError, AVMError, EventType, Result, ObjectMeta, Store, FunctionEntry, State, LogEntry, Success, mkMeta, mkStore, mkFunctionEntry, ErrObjectNotFound, ErrObjectAlreadyDestroyed, ErrObjectAlreadyExists, ErrInvalidInput, ErrObjectRejectedCall, ErrMetadataCorruption, ErrContextUnavailable, ErrMetadataNotFound, ErrMetadataInconsistent, ErrStoreCorruption, ErrScryPredicateFailed, ErrReflectionDenied, ErrReifyContextFailed, ErrNoTransactionToReify, ErrTxStateAccessDenied, ErrConstraintStoreUnavailable, ErrTxConflict, ErrTxNotFound, ErrTxAlreadyCommitted, ErrTxAlreadyAborted, ErrNoActiveTx, ErrInvalidDuringTx, ErrMachineUnreachable, ErrInvalidMachineTransfer, ErrTeleportDuringTx, ErrControllerUnreachable, ErrUnauthorizedTransfer, ErrCrossControllerTx, ErrObjectNotAvailable, ErrObjectNotConsistent, ErrFreezeFailed, ErrObjectHasNoController, ErrFunctionNotFound, ErrFunctionAlreadyRegistered, ErrVersionConflict, ErrNotImplemented, obj-error, introspect-error, reflect-error, reify-error, base-error, tx-error, tx-layer-error, pure-error, pure-layer-error, machine-error, controller-error, fd-error, nondet-error, err-object-not-found, err-object-destroyed, err-object-exists, err-invalid-input, err-object-rejected, err-metadata-corruption, err-context-unavailable, err-metadata-not-found, err-metadata-inconsistent, err-store-corruption, err-scry-predicate-failed, err-reflection-denied, err-reify-context-failed, err-no-transaction-to-reify, err-tx-state-access-denied, err-constraint-store-unavailable, err-tx-conflict, err-tx-not-found, err-tx-committed, err-tx-aborted, err-no-active-tx, err-invalid-during-tx, err-function-not-found, err-function-registered, err-version-conflict, err-machine-unreachable, err-invalid-machine-transfer, err-teleport-during-tx, err-controller-unreachable, err-unauthorized-transfer, err-cross-controller-tx, err-object-not-available, err-object-not-consistent, err-freeze-failed, err-object-has-no-controller, err-fd-not-implemented, err-nondet-not-implemented, ObjectCreated, ObjectDestroyed, ObjectCalled, MessageReceived, ObjectMoved, ExecutionMoved, ObjectFetched, ObjectTransferred, ObjectFrozen, FunctionUpdated, TransactionStarted, TransactionCommitted, TransactionAborted, ErrorOccurred, mkLogEntry, mkSuccess, success, failure, ObjectStore, MetaStore, StateStore, RuntimeObject, RuntimeObjectWithId, TxWrite, Hash, PureFunctions, Trace, BaseResult, TxResult, PureResult, AVMResult
AVM.Instruction
- Symbols: Safety, ObjInstruction, IntrospectInstruction, ReflectInstruction, ReifyInstruction, Instr₀, TxInstruction, Instr₁, PureInstruction, Instr₂, MachineInstruction, ControllerInstruction, Instr₃, Constraint, FDInstruction, NondetConstraint, NondetInstruction, Instruction, ReifiedContext, ReifiedTxState, ReifiedConstraints, VarId, Safe, Unsafe, createObj, destroyObj, call, self, input, getCurrentMachine, getState, setState, sender, reflect, scryMeta, scryDeep, mkReifiedContext, mkReifiedTxState, mkReifiedConstraints, reifyContext, reifyTxState, reifyConstraints, Obj, Introspect, Reflect, Reify, beginTx, commitTx, abortTx, Tx, callPure, registerPure, updatePure, Pure, getMachine, teleport, moveObject, fetch, getCurrentController, getController, transferObject, freeze, Machine, Controller, mkVarId, Eq, Neq, Leq, Lt, Geq, Gt, AllDiff, ValEq, ValLeq, ValLt, ValGeq, ValGt, newVar, narrow, post, label, Assert, choose, require, FD, Nondet, obj-create, obj-destroy, obj-call, obj-receive, get-self, get-input, get-current-machine, get-state, set-state, get-sender, obj-reflect, obj-scry-meta, obj-scry-deep, do-reify-context, do-reify-tx-state, do-reify-constraints, tx-begin, tx-commit, tx-abort, call-pure, register-pure, pure-update-pure, get-machine, do-teleport, move-object, fetch-object, get-current-controller, get-controller, transfer-object, freeze-object, ISA, Domain, AVMProgram
AVM.Interpreter
- Symbols: lookupObjectWithMeta, lookupPendingCreate, lookupPendingTransfer, updateMeta, lookupState, updateState, createWithMeta, initMeta, makeLogEntry, incrementEventCounter, pendingInputsFor, addPendingWrite, addPendingCreate, removePendingCreate, addPendingDestroy, addPendingTransfer, withTxBranch, withCreateTxBranch, mkSuccessNoTrace, mkSuccessWithLog, mkSuccessWithEvent, containsObserved, ensureObserved, inCreates, inDestroys, validateObserved, checkObject, checkOwnershipPure, resolveTxController, resolveAndCheckOwnership, applyCreates, applyWrite, applyWrites, applyDestroy, applyDestroys, applyTransfer, applyTransfers, applyStates, handleCall, handleCall-aux, callObjInTx, transferObjInTx, transferObjNoTx, destroyObjInTx, destroyObjNoTx, executeObj, executeIntrospect, executeReflect, matchMeta, matchDeep, executeReify, executeTx, executePure, executeMachine, executeController, executeInstr₀, executeInstr₁, executeInstr₂, executeInstruction, interpretAux, interpret, Interpreter, GenericInterpreter
Background.BasicTypes
- Symbols: ×, +, ⊥, Bool, ≡, Dec, Maybe, ℕ, List, ∈, Σ, ⊤, ↔, RawMonad, ,, ,Σ, inl, inr, tt, true, false, refl, yes, no, nothing, just, zero, suc, [], ∷, here, there, mk↔, fst, snd, ∃, ∃-syntax, ⊥-elim, ¬, not, sym, trans, cong, just≢nothing, just-injective, map-maybe, caseMaybe, length, ++-assoc, ++-right-id, map, foldr, null, head, filter, elem, concat, hasDuplicates, concatMap, all, any, find, lookup, filterMap, FinSet, Pred, case_of_, ∧, ∨, ||, if_then_else_, ≢, begin_, ≡⟨⟩, ≡⟨⟩_, _∎, >>=ᴹ, +ℕ, *ℕ, ∸, ≥, ≤, ≤?, <?, ≟ℕ, ==ℕ, ++, ∈Pred, ⊆, ∘, lsuc
Background.InteractionTrees
- Symbols: receive, Set₁, MessageEvent, ITreeF, ≈, ITree₁, ITree, send, create, destroy, retF, tauF, visF, ret-eq, tau-left, tau-right, vis-eq, EventSig, Interface, ret, tau, vis, trigger, bind-step, ITree-Monad, Handler, Impl, interp-step, >>=, <$>, _, first-definition
Background.Objects
- Symbols: InputSequence, →[]_, →*[]_, Object, WellFormedObjectType, SequentialObject, mkObjType, wfObjType, mkObj, transition, ε-trans, step-trans, ε, is-defined, output-of, ≈φ-refl, ≈φ-sym, ≈φ-trans, BehaviouralState, output, process-input, can-process, ≈ᵒ-refl, ≈ᵒ-sym, ≈ᵒ-trans, ≈ˢ-refl, ≈ˢ-sym, ≈ˢ-trans, behavioural-state-equiv, counter-type, counter-wf, counter-always-defined, prefix-def, echo-type, transition-preserves-type, reachable-from, create-object, initial-output, counter-object, process-preserves-wf, equiv-preserved, equiv-after-input, ·-++-assoc, execute-step, objecttype-to-behaviour, run-object-itree, ·, ≈φ[]_, ≈ᵒ, ≈ˢ
Background.StatelessObjects
- Symbols: CounterMsg, Key, KVMsg, KVEvent, AccountMsg, AccountOutput, VBool, VPair, VNil, inc, dec, key, put, del, get, put-event, del-event, depositMsg, withdrawMsg, balanceMsg, ok, error-insufficient, balance-val, withdraw, deposit, ok?, kudosTransfer, abortWithMsg, commitWithResult, handleDeposit, handleWithdraw, createCounter, counterExample, handleResult, updateBalance, invalidMsg, helper, handleUpdateResult, updateHelper, transferBatch, processTransfers, closeAccount, closeWithBalance, handleBalance, replay-counter, φ-counter, step-counter, KVStore, apply-kv-event, replay-kv, msg-to-event, φ-kv-aux, φ-kv, step-kv, replay-account, φ-account-aux, φ-account, step-account
examples.Battleship.Game
- Symbols: Player, Player1, Player2, GameState, setupGame, opponentBoard, attack, playerAttack, player1Attack, player2Attack, playFullGame, gameWithRollback, playGameWithPlayerType
examples.Battleship.PlayerBoard
- Symbols: VCoord, VShip, coordinateHitsShip, extractShip, checkHit, boardBehavior, handleInput
examples.Battleship.Runner
- Symbols: showMaybeVal, showGameState, testHit, testMiss
examples.Common.Display
- Symbols: showNat, showEventType, showLogEntry, showTrace, showError, showResult
examples.Common.Equality
- Symbols: eqString, eqNat, eqBool, isReachableController, isReachableMachine
examples.Common.InterpreterSetup
- Symbols: Set, interp, interpretAVMProgramRec, RunnerInterpreter
examples.Common.StateInit
- Symbols: emptyStore, noPureFunctions, mkInitialState
examples.PingPong.Main
- Symbols: Message, Input, Output, ObjectBehaviour, Val, VInt, VString, VList, NodeId, ObjectId, MachineId, ControllerId, TxId, MessageType, PingPongMsg, Ping, Pong, mkMsg, VPingPongMsg, createPing, createPong, startPingPong, pingPongExample
examples.PingPong.Runner
- Symbols: freshObjectId, freshTxId, initialState, showOid, showValAgda, eqObjectId, eqTxId, eqControllerId, mkControllerId, interpretBehaviorName, allObjectIds, getBehavior, runExample, main, ObjectBehaviourImpl, namedBehaviour, extractMsg, mkNextMsg, genericPingPongBehavior, pingBehaviorImpl, pongBehaviorImpl, testSimple, test, InterpreterImport
examples.RunnerUtilities
- Symbols: >>, RunnerState, Env, mkState, mkEnv, indent, freshId, showOID, eqOID, lookupObj

Symbol disambiguation log

The following references had multiple matches and were disambiguated:

_<: chose Background.BasicTypes._<?_ from ['Background.BasicTypes.<?', 'Background.InteractionTrees.<$>']
_≤: chose Background.BasicTypes._≤_ from ['Background.BasicTypes.≤', 'Background.BasicTypes.≤?']
_<: chose Background.BasicTypes._<?_ from ['Background.BasicTypes.<?', 'Background.InteractionTrees.<$>']

?>