pushforward (V :: newv) = (pushforward V) :: newv
Try to delete the variable from the argument list. Succeeds if variable does not occur in the argument list. Fails otherwise.
Equations
- One or more equations did not get rendered due to their size.
- DCE.arglistDeleteVar? DEL HVector.nil = some ⟨HVector.nil, ⋯⟩
Instances For
Equations
- DCE.Expr.deleteVar? DEL (Expr.mk op ty_eq eff_le args regArgs) = match DCE.arglistDeleteVar? DEL args with | none => none | some args' => some ⟨Expr.mk op ty_eq eff_le (↑args') regArgs, ⋯⟩
Instances For
Delete a variable from an Com.
Equations
- One or more equations did not get rendered due to their size.
- DCE.Com.deleteVar? DEL (Com.ret v) = match Var.tryDelete? DEL v with | none => none | some ⟨v_1, hv⟩ => some ⟨Com.ret v_1, ⋯⟩
Instances For
Declare the type of DCE up-front, so we can declare an Inhabited
instance.
This is necessary so that we can mark the DCE implementation as a partial def
and ensure that Lean does not freak out on us, since it's indeed unclear to Lean
that the output type of dce
is always inhabited.
Equations
- DCE.DCEType com = ((Γ' : Ctxt d.Ty) × (hom : Γ'.Hom Γ) × { com' : Com d Γ' EffectKind.pure t // ∀ (V : Γ.Valuation), com.denote V = com'.denote (V.comap hom) })
Instances For
Show that DCEType in inhabited.
Equations
- DCE.instInhabitedDCEType com = { default := ⟨Γ, ⟨Ctxt.Hom.id, ⟨com, ⋯⟩⟩⟩ }
walk the list of bindings, and for each let
, try to delete the variable
defined by the let
in the body/ Note that this is O(n^2)
, for an easy
proofs, as it is written as a forward pass. The fast O(n)
version is a
backward pass.
This is the real entrypoint to dce
which unfolds the type of dce_
, where
we play the DCEType
trick to convince Lean that the output type is in fact
inhabited.
Instances For
A version of DCE that returns an output program with the same context. It uses the context
morphism of dce
to adapt the result of DCE to work with the original context
Equations
Instances For
Equations
- DCE.Examples.instDecidableEqExTy x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯
Equations
- DCE.Examples.instReprExTy = { reprPrec := DCE.Examples.reprExTy✝ }
Equations
- DCE.Examples.instTyDenoteExTy = { toType := fun (x : DCE.Examples.ExTy) => match x with | DCE.Examples.ExTy.nat => ℕ | DCE.Examples.ExTy.bool => Bool }
- add: DCE.Examples.ExOp
- beq: DCE.Examples.ExOp
- cst: ℕ → DCE.Examples.ExOp
Instances For
Equations
- DCE.Examples.Ex = { Op := DCE.Examples.ExOp, Ty := DCE.Examples.ExTy, 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
- DCE.Examples.cst n = Expr.mk (DCE.Examples.ExOp.cst n) DCE.Examples.cst.proof_1 ⋯ HVector.nil HVector.nil
Instances For
Equations
- DCE.Examples.add e₁ e₂ = Expr.mk DCE.Examples.ExOp.add DCE.Examples.add.proof_1 ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil
Instances For
Equations
Instances For
TODO: how do we evaluate 'ex1_post_dce' within Lean? :D