gallais

module Instrumented where

import Control.Monad.State

data Counters = Counters
  { swaps       :: !Int
  , comparisons :: !Int
  }

type Instrumented = State Counters

gallais

Require Import ZArith.

Local Open Scope Z_scope.

Section FF.

Parameter A : Type.
Parameter (a b c d : A).

Definition FF := Z -> Z -> A.

gallais

Inductive T :=
  | Var : nat -> T
  | App : T -> T -> T.

Inductive S e : Prop := 
| def: forall R, (forall i, R i -> S i) ->
       (forall e', R e' -> S (App e e')) -> S e.

Definition def' :
  forall e, (forall e', S e' -> S (App e e')) -> S e.

gallais

open import Data.String.Base
open import Data.Nat.Base
open import Data.List.Base
open import Relation.Binary.PropositionalEquality

infix 5 _at_
record Variable : Set where
  constructor _at_
  field name   : String

gallais

open import Data.Nat

module atleastn (n : ℕ) {a} (A : Set a) where

open import Data.List using (List; length)
open import Data.Vec

record SizedList : Set a where
  field list : List A
        size : length list ≥ n

gallais

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality
open import Data.Maybe
open import Function

cong⁻¹ : ∀ {A B : Set} {a a'} (f : A → Maybe B) →
         (eq : a ≡ a') →
         from-just (f a) ≅ from-just (f a')
cong⁻¹ {a = a} f refl = refl

gallais

module bins where

open import Size
open import Codata.Stream
open import Codata.Thunk
open import Data.List.Base as List using (List; _∷_; [])
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; [_])
open import Function
open import Relation.Unary

gallais

open import Relation.Binary

module Reasoning {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
  {_≈_ : Rel A ℓ₁} (≈-trans : Transitive _≈_) (≈-sym   : Symmetric _≈_) (≈-refl : Reflexive _≈_)
  {_≤_ : Rel A ℓ₂} (≤-trans : Transitive _≤_) (≤-respˡ-≈ : _≤_ Respectsˡ _≈_) (≤-respʳ-≈ : _≤_ Respectsʳ _≈_) (≤-refl  : Reflexive _≤_)
  {_<_ : Rel A ℓ₃} (<-trans : Transitive _<_) (<-respˡ-≈ : _<_ Respectsˡ _≈_) (<-respʳ-≈ : _<_ Respectsʳ _≈_) (<⇒≤ : _<_ ⇒ _≤_)
  (<-≤-trans : ∀ {x y z} → x < y → y ≤ z → x < z)
  (≤-<-trans : ∀ {x y z} → x ≤ y → y < z → x < z)
  where

gallais

module Container

%default total

record Container where
  constructor MkContainer
  shape : Type
  position : shape -> Type

container : Container -> Type -> Type

gallais

open import Relation.Nullary
open import Agda.Builtin.Equality

data X : Set where
  a b c : X

firstA : (x y z : X) → X
firstA a y z = a
firstA x a z = a
firstA x y a = a