Agda Datatypes and Records Index

This page lists all datatypes and records defined in the Agda modules, organized by module.

AVM › Context

• AVMError
• BaseError
• ControllerError
• EventType
• FDError
• FunctionEntry (record)
• IntrospectError
• LogEntry (record)
• MachineError
• NondetError
• ObjectMeta (record)
• ObjError
• PureError
• PureLayerError
• ReflectError
• ReifyError
• Result
• State (record)
• Store (record)
• Success (record)
• TxError
• TxLayerError

AVM › Instruction

• Constraint
• ControllerInstruction
• FDInstruction
• Instruction
• Instr₀
• Instr₁
• Instr₂
• Instr₃
• IntrospectInstruction
• MachineInstruction
• NondetConstraint
• NondetInstruction
• ObjInstruction
• PureInstruction
• ReflectInstruction
• ReifiedConstraints (record)
• ReifiedContext (record)
• ReifiedTxState (record)
• ReifyInstruction
• Safety
• TxInstruction
• VarId (record)

Background › BasicTypes

• _+_
• _×_
• _↔_ (record)
• _∈_
• _≡_
• Bool
• Dec
• List
• Maybe
• RawMonad (record)
• Σ (record)
• ℕ
• ⊤ (record)
• ⊥

Background › InteractionTrees

• _≈_
• ITree (record)
• ITreeF
• ITree₁ (record)
• MessageEvent

Background › Objects

• _→*[_]_
• _→[_]_
• Object (record)
• SequentialObject (record)
• WellFormedObjectType (record)

Background › StatelessObjects

• AccountMsg
• AccountOutput
• CounterMsg
• Key
• KVEvent
• KVMsg

examples › Battleship › Game

• Player

examples › PingPong › Main

• MessageType
• PingPongMsg (record)
• Val

examples › PingPong › Runner

• ObjectBehaviourImpl

examples › RunnerUtilities

• Env (record)
• RunnerState (record)

---

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
• 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.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

?>