Describes that the dialect Op' has a type whose denotation is 'DenotedTy
- ty : d.Ty
- denote_eq : ⟦ScfFunctor.HasTy.ty DenotedTy⟧ = DenotedTy
Instances
Equations
Instances For
Equations
Instances For
Equations
Instances For
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'
Instances For
Equations
- ScfFunctor.Scf.instDecidableEqOp = ScfFunctor.Scf.decEqOp✝
Equations
- ScfFunctor.Scf.instReprOp = { reprPrec := ScfFunctor.Scf.reprOp✝ }
Equations
- ScfFunctor.Scf d = { Op := ScfFunctor.Scf.Op d.Op d.Ty d.m, Ty := d.Ty, m := d.m }
Instances For
Equations
- ScfFunctor.instMonadMScf = inferInstanceAs (Monad d.m)
Equations
- ScfFunctor.instTyDenoteTyScf = inferInstanceAs (TyDenote d.Ty)
Equations
- ScfFunctor.Scf.instCoeOp = { coe := fun (o : d.Op) => ScfFunctor.Scf.Op.coe o }
Equations
- One or more equations did not get rendered due to their size.
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)
Instances For
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)
Instances For
A loop body is invariant if it does not depend on the index.
Instances For
Evaluating a loop index invariant function is the same as evaluating it at 0
Loop invariant functions can be simulated by a simpler function
Equations
- f.atZero v = f 0 v
Instances For
If there exists a function g : t → t
which agrees with f
, then f
is
loop index invariant.
Evaluating a loop index invariant function is the same as evaluating it at atZero
iterating a loop invariant function gives a well understood answer: the iterates of the function.
the first component of iterating a loop invariant function
the second component of iterating a loop invariant function
iterated value of the fst of the tuple of counterDecorator (ie, the loop counter)
evaluating a function that does not access the index (const_index_fn)
iterating a function that does not access the index (const_index_fn)
counterDecorator on a constant function
Equations
- ScfFunctor.Scf.LoopBody.counterDecorator.to_loop_run δ f niters val = (ScfFunctor.Scf.LoopBody.counterDecorator δ f (↑niters, val)).2
Instances For
Equations
- One or more equations did not get rendered due to their size.
- int: ScfFunctor.Arith.Ty
- bool: ScfFunctor.Arith.Ty
- nat: ScfFunctor.Arith.Ty
Instances For
Equations
- ScfFunctor.Arith.instDecidableEqTy x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯
Equations
- ScfFunctor.Arith.instReprTy = { reprPrec := ScfFunctor.Arith.reprTy✝ }
Equations
- One or more equations did not get rendered due to their size.
- 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
Instances For
Equations
- ScfFunctor.Arith = { Op := ScfFunctor.Arith.Op, Ty := ScfFunctor.Arith.Ty, m := Id }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- ScfFunctor.Arith.instHasBoolArith = { ty := ScfFunctor.Arith.Ty.bool, denote_eq := ScfFunctor.Arith.instHasBoolArith.proof_1 }
Equations
- ScfFunctor.Arith.instHasNatArith = { ty := ScfFunctor.Arith.Ty.nat, denote_eq := ScfFunctor.Arith.instHasNatArith.proof_1 }
Equations
- ScfFunctor.Arith.instHasIntArith = { ty := ScfFunctor.Arith.Ty.int, denote_eq := ScfFunctor.Arith.instHasIntArith.proof_1 }
Compose Scf on top of Arith
Instances For
Equations
- ScfFunctor.cst n = Expr.mk (ScfFunctor.Scf.Op.coe (ScfFunctor.Arith.Op.const n)) ScfFunctor.cst.proof_1 ⋯ HVector.nil HVector.nil
Instances For
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
Instances For
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
Instances For
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
Instances For
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
Instances For
Equations
- ScfFunctor.neg a = Expr.mk (ScfFunctor.Scf.Op.coe ScfFunctor.Arith.Op.neg) ScfFunctor.neg.proof_1 ⋯ (a::ₕHVector.nil) HVector.nil
Instances For
Equations
- ScfFunctor.iterate k input body = Expr.mk (ScfFunctor.Scf.Op.iterate k) ScfFunctor.iterate.proof_1 ⋯ (input::ₕHVector.nil) (body::ₕHVector.nil)
Instances For
Equations
- ScfFunctor.if_ cond v then_ else_ = Expr.mk (ScfFunctor.Scf.Op.if t t') ⋯ ⋯ (cond::ₕ(v::ₕHVector.nil)) (then_::ₕ(else_::ₕHVector.nil))
Instances For
Equations
- ScfFunctor.run v body = Expr.mk (ScfFunctor.Scf.Op.run t) ⋯ ⋯ (v::ₕHVector.nil) (body::ₕHVector.nil)
Instances For
Equations
- ScfFunctor.for_ start step niter v body = Expr.mk (ScfFunctor.Scf.Op.for t) ⋯ ⋯ (start::ₕ(step::ₕ(niter::ₕ(v::ₕHVector.nil)))) (body::ₕHVector.nil)
Instances For
'if' condition of a true variable evaluates to the then region body.
'if' condition of a false variable evaluates to the else region body.
a region that returns the value immediately
Equations
- ScfFunctor.RegionRet t v = Com.ret v
Instances For
a for loop whose body immediately returns the loop variable is the same as just fetching the loop variable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ScfFunctor.ForAddToMul.instHadd = instHAdd
Instances For
Equations
- ScfFunctor.ForReversal.lhs rgn = Com.var (ScfFunctor.for_ ⟨0, ⋯⟩ ⟨1, ⋯⟩ ⟨2, ⋯⟩ ⟨3, ⋯⟩ rgn) (Com.ret ⟨0, ⋯⟩)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
running f(x) = x + x
0 times is the identity.
Equations
- One or more equations did not get rendered due to their size.