inductive Cvc.Symbols.Trace {Struct : Symbols.Repr} (State : Symbols Struct) (Repr : Nat → Type) (length : Nat) : Type

A trace of length indexed data.

Roughly equivalent to a list of indexed data with decreasing indices (length - 1 to 0). Note that this means the data of index 0 (if any) is always the very last element in the trace.

• empty {Struct : Symbols.Repr} {State : Symbols Struct} {Repr : Nat → Type} : State.Trace Repr 0

  The empty trace.

• cons {Struct : Symbols.Repr} {State : Symbols Struct} {Repr : Nat → Type} {n : Nat} (data : Repr n) (tail : State.Trace Repr n) : State.Trace Repr n.succ

  Some data with index n and the tail of the trace.

@[reducible, inline]

abbrev Cvc.Symbols.TermTrace {Struct : Symbols.Repr} (State : Symbols Struct) (length : Nat) : Type

A trace of terms.

Equations

• State.TermTrace length = State.Trace Cvc.Symbols.TermsAt length

@[reducible, inline]

abbrev Cvc.Symbols.ValueTrace {Struct : Symbols.Repr} (State : Symbols Struct) (length : Nat) : Type

A trace of values.

Equations

• State.ValueTrace length = State.Trace Cvc.Symbols.ValuesAt length

def Cvc.Symbols.Trace.mkOne {Struct : Symbols.Repr} [State : Symbols Struct] {Repr : Nat → Type} (data : Repr 0) : State.Trace Repr 1

Builds a trace of length 1.

Equations

• Cvc.Symbols.Trace.mkOne data = Cvc.Symbols.Trace.cons data Cvc.Symbols.Trace.empty

def Cvc.Symbols.Trace.get {Struct✝ : Symbols.Repr} {S : Symbols Struct✝} {R : Nat → Type} {k : Nat} : S.Trace R k → (idx : Nat) → (in_range : autoParam (idx < k) _auto✝) → R idx

Retrieves a state in a trace from its index.

Equations

• x_4.get x✝¹ x✝ = ⋯.elim
• (Cvc.Symbols.Trace.cons data tail).get x✝¹ x✝ = if i_eq_k : x✝¹ = k then ⋯ ▸ data else tail.get x✝¹ ⋯

def Cvc.Symbols.Trace.get? {Struct✝ : Symbols.Repr} {S : Symbols Struct✝} {R : Nat → Type} {k : Nat} (trace : S.Trace R k) (idx : Nat) : Option (R idx)

Retrieves a state in a trace from its index.

Equations

• trace.get? idx = if x : idx < k then some (trace.get idx x) else none

def Cvc.Symbols.Trace.decons {Struct✝ : Symbols.Repr} {S : Symbols Struct✝} {R : Nat → Type} {k : Nat} : S.Trace R (k + 1) → R k × S.Trace R k

Deconstructs a non-empty trace.

Equations

• (Cvc.Symbols.Trace.cons data tail).decons = (data, tail)

def Cvc.Symbols.Trace.getData {Struct✝ : Symbols.Repr} {S : Symbols Struct✝} {R : Nat → Type} {k : Nat} (trace : S.Trace R (k + 1)) : R k

Data at index k.

Equations

• trace.getData = trace.decons.fst

def Cvc.Symbols.Trace.getTail {Struct✝ : Symbols.Repr} {S : Symbols Struct✝} {R : Nat → Type} {k : Nat} (trace : S.Trace R (k + 1)) : S.Trace R k

Tail of a non-empty trace.

Equations

• trace.getTail = trace.decons.snd

@[reducible, inline]

abbrev Cvc.Symbols.Trace.Rev {Struct : Symbols.Repr} (State : Symbols Struct) (Repr : Nat → Type) (k : Nat) : Type

Alias for a reversed Trace, used to change the .

Actually a normal Trace, but Repr is manipulated so that the Repr-data at index idx is actually Repr (k - idx - 1). As a result Repr 0 is always the first element in the trace, as opposed to a regular Trace.

Rev traces should not be used in Trace.cons: the first data having index 0 we can only put data of index 0 in front of it, which does not make sense.

TODO

• make opaque or handle differently?

Equations

• Cvc.Symbols.Trace.Rev State Repr k = State.Trace (fun (idx : Nat) => Repr (k - idx - 1)) k

@[irreducible]

def Cvc.Symbols.Trace.reverse.loop {Struct : Symbols.Repr} {R : Nat → Type} [State : Symbols Struct] (k i : Nat) (trace : State.Trace R i) (acc : State.Trace (fun (idx : Nat) => R (k - idx - 1)) (k - i)) (h_i : i ≤ k := by (try simp [*]) <;> omega) : Trace.Rev State R k

Auxiliary function for reversing trace, tail-recursive.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Symbols.Trace.reverse {Struct : Symbols.Repr} {R : Nat → Type} {k : Nat} [State : Symbols Struct] (trace : State.Trace R k) : Trace.Rev State R k

Reverses a trace, tail-recursive.

Equations

• trace.reverse = Cvc.Symbols.Trace.reverse.loop k k trace (⋯.mpr Cvc.Symbols.Trace.empty) ⋯

@[reducible, inline]

abbrev Cvc.Symbols.Trace.rev {Struct : Symbols.Repr} {R : Nat → Type} {k : Nat} [State : Symbols Struct] (trace : State.Trace R k) : Trace.Rev State R k

Reverses a trace, tail-recursive.

Equations

• @Cvc.Symbols.Trace.rev = @Cvc.Symbols.Trace.reverse

@[irreducible]

def Cvc.Symbols.Trace.mapM.loop {m : Type → Type u_1} [Monad m] {k : Nat} {R R' : Nat → Type} {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {Struct✝¹ : Symbols.Repr} {S : Symbols Struct✝¹} (f : (i : Fin k) → R ↑i → m (R' ↑i)) (i : Fin k) (data : R ↑i) (tail : State.Trace R ↑i) : m (S.Trace R' ↑i.succ)

Auxiliary function for Trace.mapM.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Symbols.Trace.mapM.loop f ⟨0, h⟩ data Cvc.Symbols.Trace.empty = do let data ← f ⟨0, h⟩ data pure (Cvc.Symbols.Trace.cons data Cvc.Symbols.Trace.empty)

def Cvc.Symbols.Trace.mapM {m : Type → Type u_1} [Monad m] {Struct✝ : Symbols.Repr} {S : Symbols Struct✝} {R : Nat → Type} {k : Nat} {R' : Nat → Type} (trace : S.Trace R k) (f : (i : Fin k) → R ↑i → m (R' ↑i)) : m (S.Trace R' k)

Monadic map over trace data.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Symbols.Trace.map {Struct✝ : Symbols.Repr} {S : Symbols Struct✝} {R : Nat → Type} {k : Nat} {R' : Nat → Type} (trace : S.Trace R k) (f : (i : Fin k) → R ↑i → R' ↑i) : S.Trace R' k

Map over trace data.

Equations

• trace.map f = trace.mapM f

@[irreducible]

def Cvc.Symbols.Trace.forIn.loop {m : Type u_1 → Type u_2} [Monad m] {k : Nat} {R : Nat → Type} {β : Type u_1} {Struct✝ : Symbols.Repr} {S : Symbols Struct✝} (f : (i : Fin k) × R ↑i → β → m (ForInStep β)) (acc : β) (i : Fin k) (data : R ↑i) (tail : S.Trace R ↑i) : m β

Auxiliary function for Trace.forIn.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Symbols.Trace.forIn {m : Type u_1 → Type u_2} [Monad m] {Struct✝ : Symbols.Repr} {S : Symbols Struct✝} {R : Nat → Type} {k : Nat} {β : Type u_1} (trace : S.Trace R k) (init : β) (f : (i : Fin k) × R ↑i → β → m (ForInStep β)) : m β

Used to instantiate ForIn.

Equations

• One or more equations did not get rendered due to their size.

instance Cvc.Symbols.Trace.instForInSigmaFinVal {m : Type u_1 → Type u_2} {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {R : Nat → Type} {k : Nat} : ForIn m (State.Trace R k) ((i : Fin k) × R ↑i)

Equations

• Cvc.Symbols.Trace.instForInSigmaFinVal = { forIn := fun {β : Type ?u.52} [Monad m] => Cvc.Symbols.Trace.forIn }

def Cvc.Symbols.Trace.foldDecM {m : Type u_1 → Type u_2} {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {R : Nat → Type} {k : Nat} {β : Type u_1} [Monad m] (trace : State.Trace R k) (f : β → (i : Fin k) → R ↑i → m β) (init : β) : m β

Monadic fold over trace elements with decreasing indices.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Symbols.Trace.foldIncM {m : Type u_1 → Type u_2} {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {R : Nat → Type} {k : Nat} {β : Type u_1} [Monad m] (trace : State.Trace R k) (f : β → (i : Fin k) → R ↑i → m β) (init : β) : m β

Monadic fold over trace elements with increasing indices.

Equations

• trace.foldIncM f init = Cvc.Symbols.Trace.foldDecM trace.reverse (fun (acc : β) (i : Fin k) => f acc ⟨k - ↑i - 1, ⋯⟩) init

def Cvc.Symbols.Trace.foldDec {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {R : Nat → Type} {k : Nat} {β : Type u_1} (trace : State.Trace R k) (f : β → (i : Fin k) → R ↑i → β) (init : β) : β

Fold over trace elements with decreasing indices.

Equations

• trace.foldDec f init = trace.foldDecM f init

def Cvc.Symbols.Trace.foldInc {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {R : Nat → Type} {k : Nat} {β : Type u_1} (trace : State.Trace R k) (f : β → (i : Fin k) → R ↑i → β) (init : β) : β

Fold over trace elements with increasing indices.

Equations

• trace.foldInc f init = trace.foldIncM f init