orders

cfamily.Matching

record Matching

Pairing the blocks of two states: the first new block (blocks before it are the same in both), each block of the first state paired with the other’s (there) and back (back), the pairs not compared yet, and the budget left.

cfamily.Sameness

data Sameness

Whether two states are the same so far (the pairing so far), differ, or the budget ran out first.

cfamily.Matching.start

def Matching.start (base : Nat) (budget : Nat) : Matching

Nothing paired yet: blocks from base on are new, and budget steps are left.

cfamily.Matching.sameBool

def Matching.sameBool (a : Bool) (b : Bool) : Bool

Whether the truth values a and b are the same.

cfamily.Sameness.then

def Sameness.then (r : Sameness) (next : Matching -> Sameness) : Sameness

Going on with next from the comparison r when it is alike so far.

cfamily.Matching.provided

def Matching.provided (m : Matching) (b : Bool) : Sameness

Alike (with the pairing m) when the condition b holds.

cfamily.Matching.spend

def Matching.spend (m : Matching) : Sameness

One step of the budget of m spent.

cfamily.Matching.block

def Matching.block (m : Matching) (b : Nat) (c : Nat) : Sameness

The block b of the first state paired with the block c of the other, given the pairing m: a block before the start only with itself; a new one with the block it was paired with, or a new pair (to compare later) when neither was paired yet.

cfamily.Matching.lists

def Matching.lists {A : Type} (same : Matching -> A -> A -> Sameness) (m : Matching) (xs : List A) (ys : List A) : Sameness

The lists xs and ys alike element by element by same (the same length), given the pairing m.

cfamily.Matching.options

def Matching.options {A : Type} (same : Matching -> A -> A -> Sameness) (m : Matching) (x : Option A) (y : Option A) : Sameness

The options x and y alike by same, given the pairing m.

cfamily.Matching.sameNats

def Matching.sameNats (xs : List Nat) (ys : List Nat) : Bool

Whether the lists of numbers xs and ys are the same.

cfamily.Matching.sameFloat

def Matching.sameFloat (x : Float) (y : Float) : Bool

Whether the floating values x and y are the same (the same representation: NaN is NaN, -0 is not +0).

cfamily.Matching.pointer

def Matching.pointer (m : Matching) (p : Pointer) (q : Pointer) : Sameness

The pointers p and q alike, given the pairing m: the same place, in blocks paired.

cfamily.Matching.sameActive

def Matching.sameActive (a : Option Nat) (b : Option Nat) : Bool

Whether the active members a and b are the same (or both none).

cfamily.Matching.sameAllocation

def Matching.sameAllocation {L : Constructs} (a : Allocation L) (b : Allocation L) : Bool

Whether the blocks came to exist alike by a and b (a dialect’s way by its tag is the same: the statement that made it gave it).

cfamily.Matching.blocks

def Matching.blocks {L : Constructs} (fuel : Nat) (m : Matching) (x : Option (Block L)) (y : Option (Block L)) : Sameness

The blocks x and y alike, given the pairing m: both released, or both alive, made the same way, with objects alike (within fuel).

cfamily.Matching.drain

def Matching.drain {L : Constructs} (fuel : Nat) (one : Memory L) (other : Memory L) (m : Matching) : Sameness

The pairs of m not compared yet compared, between the memories one and other, within fuel (one pair each; the budget bounds it before the fuel does).

cfamily.Matching.binding

def Matching.binding (scope : Scope) (x : DeclId) : Option (DeclId * Nat)

The binding of scope (the other state’s) of the declaration x, if any.

cfamily.Matching.sameOrder

def Matching.sameOrder (a : Scope) (b : Scope) : Bool

Whether the scopes a and b have the same declarations in the same order.

cfamily.Matching.scopeBindings

def Matching.scopeBindings (m : Matching) (a : Scope) (b : Scope) : Sameness

Each declaration of the scope a bound alike in the scope b, given the pairing m (found by declaration: the two orders bind the temporaries of the calls in other orders).

cfamily.Matching.scope

def Matching.scope (m : Matching) (a : Scope) (b : Scope) : Sameness

The scopes a and b alike, given the pairing m: the same declarations, each bound to blocks paired.

cfamily.Matching.scopesInOrder

def Matching.scopesInOrder (a : List Scope) (b : List Scope) : Bool

Whether the scopes a and b (of the two states) bind their declarations in the same order.

cfamily.Matching.sameConsole

def Matching.sameConsole (a : Console) (b : Console) : Bool

Whether the consoles a and b are the same: what was written, what is left to read, and the flags.

cfamily.Matching.sameFile

def Matching.sameFile (a : String * List Nat) (b : String * List Nat) : Bool

Whether the files a and b are the same (name and bytes).

cfamily.Matching.sameStream

def Matching.sameStream (a : Stream) (b : Stream) : Bool

Whether the open streams a and b are the same.

cfamily.Matching.sameAll

def Matching.sameAll {A : Type} (same : A -> A -> Bool) (xs : List A) (ys : List A) : Bool

Whether the lists xs and ys are the same element by element by same.

cfamily.Matching.chosen

def Matching.chosen (m : Matching) (a : Chosen) (b : Chosen) : Sameness

The blocks left to a choice a and b alike, given the pairing m.

cfamily.Matching.sameRange

def Matching.sameRange (a : Option (Int * Int)) (b : Option (Int * Int)) : Bool

Whether the optional index ranges a and b are the same.

cfamily.Matching.held

def Matching.held (m : Matching) (a : Held) (b : Held) : Sameness

The arrays being sorted a and b alike, given the pairing m.

cfamily.Matching.callerBlocks

def Matching.callerBlocks (m : Matching) (scopes : List Scope) : Sameness

The blocks of the callers’ scopes alike, given the pairing m (named by both states alike: they are older than the start).

cfamily.State.sameAs

def State.sameAs {L : Constructs} (sameExtension : L.state -> L.state -> Bool) (base : Nat) (callers : List Scope) (budget : Nat) (a : State L) (b : State L) : Sameness

What the states a and b have in common to compare, given the blocks made from base on, the callers’ scopes and the budget, and sameExtension, the dialect’s comparison of its part: alike (with what is left of the budget), unlike, or undecided; and whether the scopes bind in another order (the temporaries end in another order). The notes, the calls the run is in and where comparing the orders stands are not compared.