amnn

/// BigVector is an arbitrary sized vector-like data structure,
/// implemented using an on-chain B+ Tree.
///
/// Elements in the vector are distributed between a fixed size
/// `tail`, stored in a `vector`, and an arbitrary size B+ Tree for
/// the rest of the data. Nodes in the B+ Tree are stored as
/// individual dynamic fields hanging off the `BigVector`.
///
/// This data structure supports:
///

amnn

[package]
name = "fermat-bench"
version = "0.1.0"
edition = "2021"

[dev-dependencies]
criterion = "0.5"

[[bench]]
name = "bench"

amnn

[package]
name = "Table Test"
version = "0.1.0"

[dependencies]
Sui = { ... }

[addresses]
std = "0x1"
sui = "0x2"

amnn

module p::example {
  use sui::coin::{Self, Coin};
  use sui::dynamic_field as field;
  use sui::object::UID;
  use sui::tx_context::TxContext;

  struct Manager has key { id: UID, /* ... */ }
  struct Label<phantom COIN> has copy, drop, store {}

  entry fun handle_coin<COIN>(m: &mut Manager, coin: Coin<COIN>, ctx: &mut TxContext) {

amnn

---
compiled_package_info:
  package_name: example
  address_alias_instantiation:
    example: "0000000000000000000000000000000000000000"
    std: "0000000000000000000000000000000000000001"
    sui: "0000000000000000000000000000000000000002"
  source_digest: E221B8FCD48A736A2DF75C6E39E806D621BE87E68D4049A99153D5986E77112A
  build_flags:
    dev_mode: false

amnn

module RBTree where

open import Agda.Primitive public
  using (Level; lzero; lsuc; _⊔_)

data Σ {l k} (A : Set l) (B : A → Set k) : Set (l ⊔ k) where
  _,_ : (a : A) → (b : B a) → Σ A B
infixr 10 _,_

fst : ∀ {l k} {A : Set l} {B : A → Set k} -> Σ A B -> A

amnn

module HList where

open import Agda.Primitive public
  using (Level; lzero; lsuc; _⊔_)

data Σ {l k} (A : Set l) (B : A -> Set k) : Set (l ⊔ k) where
  _,_ : (a : A) -> (B a) -> Σ A B

infixr 3 _,_

amnn

module Fact where

  fact :: Integer -> Integer
  fact 0 = 1
  fact n = n * fact (n-1)

  factk :: Integer -> (Integer -> r) -> r
  factk 0 k = k 1
  factk n k = factk (n-1) (k . (n*))

amnn

Based on Huet 1976, §5.7.2

Preliminaries

From earlier sections

• V is a countably infinite set of variables.
• C a finite set of constructors.
• a : C -> Nat an arity function.
• R : V -/-> Typ a partial environment function.

amnn

# A class to print arbitrary Sudoku-style grids, given a list of numbers
# Author: Ashok Menon, 01/09/2015

class Array
  def surround(delim)
    "#{delim}#{join delim}#{delim}"
  end
end

class Grid