class ScfFunctor.HasTy (d : Dialect) (DenotedTy : Type) [TyDenote d.Ty] [DialectSignature d] : Type

Describes that the dialect Op' has a type whose denotation is 'DenotedTy

• ty : d.Ty
• denote_eq : ⟦ScfFunctor.HasTy.ty DenotedTy⟧ = DenotedTy

theorem ScfFunctor.HasTy.denote_eq {d : Dialect} {DenotedTy : Type} : ∀ {inst : TyDenote d.Ty} {inst_1 : DialectSignature d} [self : ScfFunctor.HasTy d DenotedTy], ⟦ScfFunctor.HasTy.ty DenotedTy⟧ = DenotedTy

@[reducible, inline]

abbrev ScfFunctor.HasBool (d : Dialect) [TyDenote d.Ty] [DialectSignature d] : Type

Equations

• ScfFunctor.HasBool d = ScfFunctor.HasTy d Bool

@[reducible, inline]

abbrev ScfFunctor.HasInt (d : Dialect) [TyDenote d.Ty] [DialectSignature d] : Type

Equations

• ScfFunctor.HasInt d = ScfFunctor.HasTy d ℤ

@[reducible, inline]

abbrev ScfFunctor.HasNat (d : Dialect) [TyDenote d.Ty] [DialectSignature d] : Type

Equations

• ScfFunctor.HasNat d = ScfFunctor.HasTy d ℕ

inductive ScfFunctor.Scf.Op (Op' : Type) (Ty' : Type) (m' : Type → Type) [TyDenote Ty'] [DialectSignature { Op := Op', Ty := Ty', m := m' }] [DialectDenote { Op := Op', Ty := Ty', m := m' }] : Type

only flow operations, parametric over arithmetic from another dialect Op'

• coe: {Op' Ty' : Type} → {m' : Type → Type} → [inst : TyDenote Ty'] → [inst_1 : DialectSignature { Op := Op', Ty := Ty', m := m' }] → [inst_2 : DialectDenote { Op := Op', Ty := Ty', m := m' }] → Op' → ScfFunctor.Scf.Op Op' Ty' m'
• iterate: {Op' Ty' : Type} → {m' : Type → Type} → [inst : TyDenote Ty'] → [inst_1 : DialectSignature { Op := Op', Ty := Ty', m := m' }] → [inst_2 : DialectDenote { Op := Op', Ty := Ty', m := m' }] → ℕ → ScfFunctor.Scf.Op Op' Ty' m'
• run: {Op' Ty' : Type} → {m' : Type → Type} → [inst : TyDenote Ty'] → [inst_1 : DialectSignature { Op := Op', Ty := Ty', m := m' }] → [inst_2 : DialectDenote { Op := Op', Ty := Ty', m := m' }] → Ty' → ScfFunctor.Scf.Op Op' Ty' m'
• if: {Op' Ty' : Type} → {m' : Type → Type} → [inst : TyDenote Ty'] → [inst_1 : DialectSignature { Op := Op', Ty := Ty', m := m' }] → [inst_2 : DialectDenote { Op := Op', Ty := Ty', m := m' }] → Ty' → Ty' → ScfFunctor.Scf.Op Op' Ty' m'
• for: {Op' Ty' : Type} → {m' : Type → Type} → [inst : TyDenote Ty'] → [inst_1 : DialectSignature { Op := Op', Ty := Ty', m := m' }] → [inst_2 : DialectDenote { Op := Op', Ty := Ty', m := m' }] → Ty' → ScfFunctor.Scf.Op Op' Ty' m'

instance ScfFunctor.Scf.instDecidableEqOp : {Op' Ty' : Type} → {m' : Type → Type} → {inst : TyDenote Ty'} → {inst_1 : DialectSignature { Op := Op', Ty := Ty', m := m' }} → {inst_2 : DialectDenote { Op := Op', Ty := Ty', m := m' }} → [inst_3 : DecidableEq Op'] → [inst_4 : DecidableEq Ty'] → DecidableEq (ScfFunctor.Scf.Op Op' Ty' m')

Equations

• ScfFunctor.Scf.instDecidableEqOp = ScfFunctor.Scf.decEqOp✝

instance ScfFunctor.Scf.instReprOp : {Op' Ty' : Type} → {m' : Type → Type} → {inst : TyDenote Ty'} → {inst_1 : DialectSignature { Op := Op', Ty := Ty', m := m' }} → {inst_2 : DialectDenote { Op := Op', Ty := Ty', m := m' }} → [inst_3 : Repr Op'] → [inst_4 : Repr Ty'] → Repr (ScfFunctor.Scf.Op Op' Ty' m')

Equations

• ScfFunctor.Scf.instReprOp = { reprPrec := ScfFunctor.Scf.reprOp✝ }

def ScfFunctor.Scf (d : Dialect) [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] : Dialect

Equations

• ScfFunctor.Scf d = { Op := ScfFunctor.Scf.Op d.Op d.Ty d.m, Ty := d.Ty, m := d.m }

instance ScfFunctor.instMonadMScf {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] [Monad d.m] : Monad (ScfFunctor.Scf d).m

Equations

• ScfFunctor.instMonadMScf = inferInstanceAs (Monad d.m)

instance ScfFunctor.instTyDenoteTyScf {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] : TyDenote (ScfFunctor.Scf d).Ty

Equations

• ScfFunctor.instTyDenoteTyScf = inferInstanceAs (TyDenote d.Ty)

instance ScfFunctor.Scf.instCoeOp {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] : Coe d.Op (ScfFunctor.Scf d).Op

Equations

• ScfFunctor.Scf.instCoeOp = { coe := fun (o : d.Op) => ScfFunctor.Scf.Op.coe o }

@[reducible]

instance ScfFunctor.Scf.instDialectSignature {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] [B : ScfFunctor.HasBool d] [N : ScfFunctor.HasNat d] [I : ScfFunctor.HasInt d] : DialectSignature (ScfFunctor.Scf d)

Equations

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

@[reducible, inline]

abbrev ScfFunctor.Scf.LoopBody (t : Type) : Type

A loop body receives the current value of the loop induction variable, and the current loop carried value. The loop body produces the value of this loop iteration.

Consider the loop: for(int i = 0; i >= -10; i -= 2). In this case, the value i will be the sequence of values [0, -2, -4, -6, -8, -10]. The value i is the loop induction variable.

This value is distinct from the trip count, which is the number of times the loop body has been executed so far, which is [0, 1, 2, 3, 4].

The LoopBody does not provide access to the trip count, only to the loop induction variable.

Equations

• ScfFunctor.Scf.LoopBody t = (ℤ → t → t)

def ScfFunctor.Scf.LoopBody.counterDecorator {α : Type} (δ : ℤ) (f : ScfFunctor.Scf.LoopBody α) : ℤ × α → ℤ × α

Convert a function f which is a single loop iteration into a function that iterates and updates the loop counter.

Equations

• ScfFunctor.Scf.LoopBody.counterDecorator δ f (i, v) = (i + δ, f i v)

def ScfFunctor.Scf.LoopBody.IndexInvariant {t : Type} (f : ScfFunctor.Scf.LoopBody t) : Prop

A loop body is invariant if it does not depend on the index.

Equations

• f.IndexInvariant = ∀ (i j : ℤ) (v : t), f i v = f j v

theorem ScfFunctor.Scf.LoopBody.eval {t : Type} (f : ScfFunctor.Scf.LoopBody t) (hf : f.IndexInvariant) (i : ℤ) (v : t) : f i v = f 0 v

Evaluating a loop index invariant function is the same as evaluating it at 0

def ScfFunctor.Scf.LoopBody.atZero {t : Type} (f : ScfFunctor.Scf.LoopBody t) : t → t

Loop invariant functions can be simulated by a simpler function

Equations

• f.atZero v = f 0 v

theorem ScfFunctor.Scf.LoopBody.eq_invariant_fn {t : Type} (f : ScfFunctor.Scf.LoopBody t) (g : t → t) (hf : ∀ (i : ℤ) (v : t), f i v = g v) : f.IndexInvariant ∧ f.atZero = g

If there exists a function g : t → t which agrees with f, then f is loop index invariant.

@[simp]

theorem ScfFunctor.Scf.LoopBody.IndexInvariant.eval' {t : Type} {f : ScfFunctor.Scf.LoopBody t} (hf : f.IndexInvariant) (i : ℤ) (v : t) : f i v = f.atZero v

Evaluating a loop index invariant function is the same as evaluating it at atZero

@[simp]

theorem ScfFunctor.Scf.LoopBody.IndexInvariant.iterate {t : Type} {f : ScfFunctor.Scf.LoopBody t} (hf : f.IndexInvariant) (δ : ℤ) (i₀ : ℤ) (v₀ : t) (k : ℕ) : (ScfFunctor.Scf.LoopBody.counterDecorator δ f)^[k] (i₀, v₀) = (i₀ + δ * ↑k, f.atZero^[k] v₀)

iterating a loop invariant function gives a well understood answer: the iterates of the function.

@[simp]

theorem ScfFunctor.Scf.LoopBody.IndexInvariant.iterate_fst {t : Type} {f : ScfFunctor.Scf.LoopBody t} (δ : ℤ) (hf : f.IndexInvariant) (i₀ : ℤ) (v₀ : t) (k : ℕ) : ((ScfFunctor.Scf.LoopBody.counterDecorator δ f)^[k] (i₀, v₀)).1 = i₀ + δ * ↑k

the first component of iterating a loop invariant function

@[simp]

theorem ScfFunctor.Scf.LoopBody.IndexInvariant.iterate_snd {t : Type} {f : ScfFunctor.Scf.LoopBody t} (δ : ℤ) (hf : f.IndexInvariant) (i₀ : ℤ) (v₀ : t) (k : ℕ) : ((ScfFunctor.Scf.LoopBody.counterDecorator δ f)^[k] (i₀, v₀)).2 = f.atZero^[k] v₀

the second component of iterating a loop invariant function

@[simp]

theorem ScfFunctor.Scf.LoopBody.counterDecorator.iterate_fst_val {α : Type} (δ : ℤ) (f : ScfFunctor.Scf.LoopBody α) (i₀ : ℤ) (v₀ : α) (k : ℕ) : ((ScfFunctor.Scf.LoopBody.counterDecorator δ f)^[k] (i₀, v₀)).1 = i₀ + ↑k * δ

iterated value of the fst of the tuple of counterDecorator (ie, the loop counter)

theorem ScfFunctor.Scf.LoopBody.counterDecorator.const_index_fn_eval {α : Type} (δ : ℤ) (i : ℤ) (vstart : α) (f : ScfFunctor.Scf.LoopBody α) (f' : α → α) (hf : f = fun (x : ℤ) (a : α) => f' a) : ScfFunctor.Scf.LoopBody.counterDecorator δ f (i, vstart) = (i + δ, f' vstart)

evaluating a function that does not access the index (const_index_fn)

theorem ScfFunctor.Scf.LoopBody.counterDecorator.const_index_fn_iterate {α : Type} (δ : ℤ) (i : ℤ) (vstart : α) (f : ScfFunctor.Scf.LoopBody α) (f' : α → α) (hf : f = fun (x : ℤ) (a : α) => f' a) (k : ℕ) : (ScfFunctor.Scf.LoopBody.counterDecorator δ f)^[k] (i, vstart) = (i + ↑k * δ, f'^[k] vstart)

iterating a function that does not access the index (const_index_fn)

@[simp]

theorem ScfFunctor.Scf.LoopBody.counterDecorator.constant {α : Type} (δ : ℤ) (i : ℤ) (vstart : α) : ScfFunctor.Scf.LoopBody.counterDecorator δ (fun (_i : ℤ) (v : α) => v) (i, vstart) = (i + δ, vstart)

counterDecorator on a constant function

theorem ScfFunctor.Scf.LoopBody.counterDecorator.constant_iterate {α : Type} (k : ℕ) (δ : ℤ) : (ScfFunctor.Scf.LoopBody.counterDecorator δ fun (x : ℤ) (v : α) => v)^[k] = fun (args : ℤ × α) => (args.1 + ↑k * δ, args.2)

iterate the counterDecorator of a constant function.

def ScfFunctor.Scf.LoopBody.counterDecorator.to_loop_run {α : Type} (δ : ℤ) (f : ScfFunctor.Scf.LoopBody α) (niters : ℕ) (val : α) : α

Equations

• ScfFunctor.Scf.LoopBody.counterDecorator.to_loop_run δ f niters val = (ScfFunctor.Scf.LoopBody.counterDecorator δ f (↑niters, val)).2

@[reducible]

instance ScfFunctor.Scf.instDialectDenoteOfMonadM {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] [B : ScfFunctor.HasBool d] [N : ScfFunctor.HasNat d] [Z : ScfFunctor.HasInt d] [Monad d.m] : DialectDenote (ScfFunctor.Scf d)

Equations

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

inductive ScfFunctor.Arith.Ty : Type

• int: ScfFunctor.Arith.Ty
• bool: ScfFunctor.Arith.Ty
• nat: ScfFunctor.Arith.Ty

instance ScfFunctor.Arith.instDecidableEqTy : DecidableEq ScfFunctor.Arith.Ty

Equations

• ScfFunctor.Arith.instDecidableEqTy x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance ScfFunctor.Arith.instReprTy : Repr ScfFunctor.Arith.Ty

Equations

• ScfFunctor.Arith.instReprTy = { reprPrec := ScfFunctor.Arith.reprTy✝ }

instance ScfFunctor.Arith.instTyDenoteTy : TyDenote ScfFunctor.Arith.Ty

Equations

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

inductive ScfFunctor.Arith.Op : Type

• add: ScfFunctor.Arith.Op
• add_nat: ScfFunctor.Arith.Op

  a + b

• axpy: ScfFunctor.Arith.Op
• neg: ScfFunctor.Arith.Op
• const: ℤ → ScfFunctor.Arith.Op
• const_nat: ℕ → ScfFunctor.Arith.Op

@[reducible, inline]

abbrev ScfFunctor.Arith.Arith : Dialect

Equations

• ScfFunctor.Arith = { Op := ScfFunctor.Arith.Op, Ty := ScfFunctor.Arith.Ty, m := Id }

@[reducible]

instance ScfFunctor.Arith.instDialectSignatureArith : DialectSignature ScfFunctor.Arith

Equations

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

@[reducible]

instance ScfFunctor.Arith.instDialectDenoteArith : DialectDenote ScfFunctor.Arith

Equations

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

instance ScfFunctor.Arith.instHasBoolArith : ScfFunctor.HasBool ScfFunctor.Arith

Equations

• ScfFunctor.Arith.instHasBoolArith = { ty := ScfFunctor.Arith.Ty.bool, denote_eq := ScfFunctor.Arith.instHasBoolArith.proof_1 }

instance ScfFunctor.Arith.instHasNatArith : ScfFunctor.HasNat ScfFunctor.Arith

Equations

• ScfFunctor.Arith.instHasNatArith = { ty := ScfFunctor.Arith.Ty.nat, denote_eq := ScfFunctor.Arith.instHasNatArith.proof_1 }

instance ScfFunctor.Arith.instHasIntArith : ScfFunctor.HasInt ScfFunctor.Arith

Equations

• ScfFunctor.Arith.instHasIntArith = { ty := ScfFunctor.Arith.Ty.int, denote_eq := ScfFunctor.Arith.instHasIntArith.proof_1 }

@[reducible, inline]

abbrev ScfFunctor.ScfArith : Dialect

Compose Scf on top of Arith

Equations

• ScfFunctor.ScfArith = ScfFunctor.Scf ScfFunctor.Arith

def ScfFunctor.cst {Γ : Ctxt ScfFunctor.ScfArith.Ty} (n : ℤ) : Expr ScfFunctor.ScfArith Γ EffectKind.pure ScfFunctor.Arith.Ty.int

Equations

• ScfFunctor.cst n = Expr.mk (ScfFunctor.Scf.Op.coe (ScfFunctor.Arith.Op.const n)) ScfFunctor.cst.proof_1 ⋯ HVector.nil HVector.nil

def ScfFunctor.cst_nat {Γ : Ctxt ScfFunctor.ScfArith.Ty} (n : ℕ) : Expr ScfFunctor.ScfArith Γ EffectKind.pure ScfFunctor.Arith.Ty.nat

Equations

• ScfFunctor.cst_nat n = Expr.mk (ScfFunctor.Scf.Op.coe (ScfFunctor.Arith.Op.const_nat n)) ScfFunctor.cst_nat.proof_1 ⋯ HVector.nil HVector.nil

def ScfFunctor.add {Γ : Ctxt ScfFunctor.ScfArith.Ty} (e₁ : Γ.Var ScfFunctor.Arith.Ty.int) (e₂ : Γ.Var ScfFunctor.Arith.Ty.int) : Expr ScfFunctor.ScfArith Γ EffectKind.pure ScfFunctor.Arith.Ty.int

Equations

• ScfFunctor.add e₁ e₂ = Expr.mk (ScfFunctor.Scf.Op.coe ScfFunctor.Arith.Op.add) ScfFunctor.add.proof_1 ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil

def ScfFunctor.add_nat {Γ : Ctxt ScfFunctor.ScfArith.Ty} (e₁ : Γ.Var ScfFunctor.Arith.Ty.nat) (e₂ : Γ.Var ScfFunctor.Arith.Ty.nat) : Expr ScfFunctor.ScfArith Γ EffectKind.pure ScfFunctor.Arith.Ty.nat

Equations

• ScfFunctor.add_nat e₁ e₂ = Expr.mk (ScfFunctor.Scf.Op.coe ScfFunctor.Arith.Op.add_nat) ScfFunctor.add_nat.proof_1 ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil

def ScfFunctor.axpy {Γ : Ctxt ScfFunctor.ScfArith.Ty} (a : Γ.Var ScfFunctor.Arith.Ty.int) (x : Γ.Var ScfFunctor.Arith.Ty.nat) (b : Γ.Var ScfFunctor.Arith.Ty.int) : Expr ScfFunctor.ScfArith Γ EffectKind.pure ScfFunctor.Arith.Ty.int

Equations

• ScfFunctor.axpy a x b = Expr.mk (ScfFunctor.Scf.Op.coe ScfFunctor.Arith.Op.axpy) ScfFunctor.axpy.proof_1 ⋯ (a::ₕ(x::ₕ(b::ₕHVector.nil))) HVector.nil

def ScfFunctor.neg {Γ : Ctxt ScfFunctor.ScfArith.Ty} (a : Γ.Var ScfFunctor.Arith.Ty.int) : Expr ScfFunctor.ScfArith Γ EffectKind.pure ScfFunctor.Arith.Ty.int

Equations

• ScfFunctor.neg a = Expr.mk (ScfFunctor.Scf.Op.coe ScfFunctor.Arith.Op.neg) ScfFunctor.neg.proof_1 ⋯ (a::ₕHVector.nil) HVector.nil

def ScfFunctor.iterate {Γ : Ctxt ScfFunctor.Arith.Ty} (k : ℕ) (input : Γ.Var ScfFunctor.Arith.Ty.int) (body : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int] EffectKind.impure ScfFunctor.Arith.Ty.int) : Expr ScfFunctor.ScfArith Γ EffectKind.impure ScfFunctor.Arith.Ty.int

Equations

• ScfFunctor.iterate k input body = Expr.mk (ScfFunctor.Scf.Op.iterate k) ScfFunctor.iterate.proof_1 ⋯ (input::ₕHVector.nil) (body::ₕHVector.nil)

def ScfFunctor.if_ {Γ : Ctxt ScfFunctor.Arith.Ty} {t : ScfFunctor.Arith.Ty} {t' : ScfFunctor.Arith.Ty} (cond : Γ.Var ScfFunctor.Arith.Ty.bool) (v : Γ.Var t) (then_ : Com ScfFunctor.ScfArith [t] EffectKind.impure t') (else_ : Com ScfFunctor.ScfArith [t] EffectKind.impure t') : Expr ScfFunctor.ScfArith Γ EffectKind.impure t'

Equations

• ScfFunctor.if_ cond v then_ else_ = Expr.mk (ScfFunctor.Scf.Op.if t t') ⋯ ⋯ (cond::ₕ(v::ₕHVector.nil)) (then_::ₕ(else_::ₕHVector.nil))

def ScfFunctor.run {Γ : Ctxt ScfFunctor.Arith.Ty} {t : ScfFunctor.Arith.Ty} (v : Γ.Var t) (body : Com ScfFunctor.ScfArith [t] EffectKind.impure t) : Expr ScfFunctor.ScfArith Γ EffectKind.impure t

Equations

• ScfFunctor.run v body = Expr.mk (ScfFunctor.Scf.Op.run t) ⋯ ⋯ (v::ₕHVector.nil) (body::ₕHVector.nil)

def ScfFunctor.for_ {Γ : Ctxt ScfFunctor.Arith.Ty} {t : ScfFunctor.Arith.Ty} (start : Γ.Var ScfFunctor.Arith.Ty.int) (step : Γ.Var ScfFunctor.Arith.Ty.int) (niter : Γ.Var ScfFunctor.Arith.Ty.nat) (v : Γ.Var t) (body : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int, t] EffectKind.impure t) : Expr ScfFunctor.ScfArith Γ EffectKind.impure t

Equations

• ScfFunctor.for_ start step niter v body = Expr.mk (ScfFunctor.Scf.Op.for t) ⋯ ⋯ (start::ₕ(step::ₕ(niter::ₕ(v::ₕHVector.nil)))) (body::ₕHVector.nil)

theorem ScfFunctor.if_true' {Γ : Ctxt ScfFunctor.Arith.Ty} {Γv : Γ.Valuation} {t : ScfFunctor.Arith.Ty} (cond : Γ.Var ScfFunctor.Arith.Ty.bool) (hcond : Γv cond = true) (v : Γ.Var t) (then_ : Com ScfFunctor.ScfArith [t] EffectKind.impure t) (else_ : Com ScfFunctor.ScfArith [t] EffectKind.impure t) : (ScfFunctor.if_ cond v then_ else_).denote Γv = (ScfFunctor.run v then_).denote Γv

'if' condition of a true variable evaluates to the then region body.

theorem ScfFunctor.if_false' {Γ : Ctxt ScfFunctor.Arith.Ty} {Γv : Γ.Valuation} {t : ScfFunctor.Arith.Ty} (cond : Γ.Var ScfFunctor.Arith.Ty.bool) (hcond : Γv cond = false) (v : Γ.Var t) (then_ : Com ScfFunctor.ScfArith [t] EffectKind.impure t) (else_ : Com ScfFunctor.ScfArith [t] EffectKind.impure t) : (ScfFunctor.if_ cond v then_ else_).denote Γv = (ScfFunctor.run v else_).denote Γv

'if' condition of a false variable evaluates to the else region body.

@[reducible, inline]

abbrev ScfFunctor.RegionRet (t : ScfFunctor.Arith.Ty) {Γ : Ctxt ScfFunctor.Arith.Ty} (v : Γ.Var t) : Com ScfFunctor.ScfArith Γ EffectKind.impure t

a region that returns the value immediately

Equations

• ScfFunctor.RegionRet t v = Com.ret v

theorem ScfFunctor.for_return {Γ : Ctxt ScfFunctor.Arith.Ty} {Γv : Γ.Valuation} {t : ScfFunctor.Arith.Ty} (istart : Γ.Var ScfFunctor.Arith.Ty.int) (istep : Γ.Var ScfFunctor.Arith.Ty.int) (niters : Γ.Var ScfFunctor.Arith.Ty.nat) (v : Γ.Var t) : (ScfFunctor.for_ istart istep niters v (ScfFunctor.RegionRet t ⟨1, ⋯⟩)).denote Γv = Γv v

a for loop whose body immediately returns the loop variable is the same as just fetching the loop variable.

def ScfFunctor.ForAddToMul.lhs (vincrement : ℤ) : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.nat, ScfFunctor.Arith.Ty.int] EffectKind.impure ScfFunctor.Arith.Ty.int

Equations

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

def ScfFunctor.ForAddToMul.rhs (vincrement : ℤ) : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.nat, ScfFunctor.Arith.Ty.int] EffectKind.pure ScfFunctor.Arith.Ty.int

Equations

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

@[reducible, inline]

abbrev ScfFunctor.ForAddToMul.instHadd : HAdd ⟦ScfFunctor.Arith.Ty.int⟧ ⟦ScfFunctor.Arith.Ty.int⟧ ⟦ScfFunctor.Arith.Ty.int⟧

Equations

• ScfFunctor.ForAddToMul.instHadd = instHAdd

theorem ScfFunctor.ForAddToMul.correct {v0 : ℤ} {Γv : Ctxt.Valuation [ScfFunctor.Arith.Ty.nat, ScfFunctor.Arith.Ty.int]} : (ScfFunctor.ForAddToMul.lhs v0).denote Γv = (ScfFunctor.ForAddToMul.rhs v0).denote Γv

def ScfFunctor.ForReversal.lhs {t : ScfFunctor.Arith.Ty} (rgn : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int, t] EffectKind.impure t) : let Γ := [ScfFunctor.Arith.Ty.int, ScfFunctor.Arith.Ty.int, ScfFunctor.Arith.Ty.nat, t]; Com ScfFunctor.ScfArith Γ EffectKind.impure t

Equations

• ScfFunctor.ForReversal.lhs rgn = Com.var (ScfFunctor.for_ ⟨0, ⋯⟩ ⟨1, ⋯⟩ ⟨2, ⋯⟩ ⟨3, ⋯⟩ rgn) (Com.ret ⟨0, ⋯⟩)

def ScfFunctor.ForReversal.rhs {t : ScfFunctor.Arith.Ty} (rgn : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int, t] EffectKind.impure t) : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int, ScfFunctor.Arith.Ty.int, ScfFunctor.Arith.Ty.nat, t] EffectKind.impure t

Equations

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

theorem ScfFunctor.ForReversal.Ctxt.Var.toSnoc (ty : ScfFunctor.Arith.Ty) (snocty : ScfFunctor.Arith.Ty) (Γ : Ctxt ScfFunctor.Arith.Ty) (V : Γ.Valuation) {snocval : ⟦snocty⟧} {v : ℕ} {hvproof : Γ.get? v = some ty} {var : Γ.Var ty} (hvar : var = ⟨v, hvproof⟩) : V var = (V::ᵥsnocval) ⟨v + 1, ⋯⟩

rewrite a variable whose index is '> 0' to a new variable which is the 'snoc' of a smaller variable. this enables rewriting with Ctxt.Valuation.snoc_toSnoc.

theorem ScfFunctor.ForReversal.correct {t : ScfFunctor.Arith.Ty} (rgn : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int, t] EffectKind.impure t) {Γv : Ctxt.Valuation [ScfFunctor.Arith.Ty.int, ScfFunctor.Arith.Ty.int, ScfFunctor.Arith.Ty.nat, t]} : Com.denote (ScfFunctor.ForReversal.lhs rgn) Γv = (ScfFunctor.ForReversal.rhs rgn).denote Γv

def ScfFunctor.ForFusion.lhs {t : ScfFunctor.ScfArith.Ty} (rgn : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int, t] EffectKind.impure t) (niters1 : ℕ) (niters2 : ℕ) (start1 : ℤ) : Com ScfFunctor.ScfArith [t] EffectKind.impure t

Equations

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

def ScfFunctor.ForFusion.rhs {t : ScfFunctor.ScfArith.Ty} (rgn : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int, t] EffectKind.impure t) (niters1 : ℕ) (niters2 : ℕ) (start1 : ℤ) : Com ScfFunctor.ScfArith [t] EffectKind.impure t

Equations

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

theorem ScfFunctor.ForFusion.correct {t : ScfFunctor.ScfArith.Ty} (rgn : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int, t] EffectKind.impure t) (niters1 : ℕ) (niters2 : ℕ) (start1 : ℤ) {Γv : Ctxt.Valuation [t]} : (ScfFunctor.ForFusion.lhs rgn niters1 niters2 start1).denote Γv = (ScfFunctor.ForFusion.rhs rgn niters1 niters2 start1).denote Γv

def ScfFunctor.IterateIdentity.lhs : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int] EffectKind.impure ScfFunctor.Arith.Ty.int

running f(x) = x + x 0 times is the identity.

Equations

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

def ScfFunctor.IterateIdentity.rhs : Com ScfFunctor.ScfArith [ScfFunctor.Arith.Ty.int] EffectKind.impure ScfFunctor.Arith.Ty.int

Equations

• ScfFunctor.IterateIdentity.rhs = Com.ret ⟨0, ScfFunctor.IterateIdentity.rhs.proof_1⟩