Evaluation

partial def SynthLean.evalTp {_u : Lean.Level} {χ : Q(Type _u)} (env : Q(List (Val «$χ»))) (T' : Q(Expr «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ Δ : Ctx «$χ»} {σ : ℕ → Expr «$χ»} {l : ℕ}, EnvEqSb E Δ «$env» σ Γ → E ∣ Γ ⊢[l] «$T'» → ValEqTp E Δ l «$v» (Expr.subst σ «$T'»)))

Evaluate a type in an environment of values.

Note: we use as_aux_lemma pervasively to minimize the size of produced proof terms.

partial def SynthLean.evalTm {_u : Lean.Level} {χ : Q(Type _u)} (env : Q(List (Val «$χ»))) (t' : Q(Expr «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ Δ : Ctx «$χ»} {σ : ℕ → Expr «$χ»} {A : Expr «$χ»} {l : ℕ}, EnvEqSb E Δ «$env» σ Γ → E ∣ Γ ⊢[l] «$t'» : A → ValEqTm E Δ l «$v» (Expr.subst σ «$t'») (Expr.subst σ A)))

Evaluate a term in an environment of values.

partial def SynthLean.evalValTp {_u : Lean.Level} {χ : Q(Type _u)} (env : Q(List (Val «$χ»))) (vT' : Q(Val «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ Δ : Ctx «$χ»} {A : Expr «$χ»} {σ : ℕ → Expr «$χ»} {l : ℕ}, EnvEqSb E Δ «$env» σ Γ → ValEqTp E Γ l «$vT'» A → ValEqTp E Δ l «$v» (Expr.subst σ A)))

Evaluate a type value in a new environment.

This operation is not commonly implemented in NbE variants. We need it as an alternative to readback: when having to produce a type closure from a type value, instead of reading back and storing Clos.of_expr, we store Clos.of_val. However, that means we may later need to evaluate the stored value in a new environment, and evalValTp does that.

partial def SynthLean.evalValTm {_u : Lean.Level} {χ : Q(Type _u)} (env : Q(List (Val «$χ»))) (vt : Q(Val «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ Δ : Ctx «$χ»} {A t : Expr «$χ»} {σ : ℕ → Expr «$χ»} {l : ℕ}, EnvEqSb E Δ «$env» σ Γ → ValEqTm E Γ l «$vt» t A → ValEqTm E Δ l «$v» (Expr.subst σ t) (Expr.subst σ A)))

Evaluate a term value in a new environment.

partial def SynthLean.evalNeutTm {_u : Lean.Level} {χ : Q(Type _u)} (env : Q(List (Val «$χ»))) (nt : Q(Neut «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ Δ : Ctx «$χ»} {A t : Expr «$χ»} {σ : ℕ → Expr «$χ»} {l : ℕ}, EnvEqSb E Δ «$env» σ Γ → NeutEqTm E Γ l «$nt» t A → ValEqTm E Δ l «$v» (Expr.subst σ t) (Expr.subst σ A)))

Evaluate a neutral term in a new environment.

partial def SynthLean.evalClosTp {_u : Lean.Level} {χ : Q(Type _u)} (vB : Q(Clos «$χ»)) (vt : Q(Val «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ : Ctx «$χ»} {A B t : Expr «$χ»} {l l' : ℕ}, ClosEqTp E Γ l l' A «$vB» B → ValEqTm E Γ l «$vt» t A → ValEqTp E Γ l' «$v» (Expr.subst t.toSb B)))

Evaluate a type closure on an argument.

partial def SynthLean.forceClosTp {_u : Lean.Level} {χ : Q(Type _u)} (d : Q(ℕ)) (vA : Q(Val «$χ»)) (vB : Q(Clos «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ : Ctx «$χ»} {A B : Expr «$χ»} {l l' : ℕ}, «$d» = List.length Γ → ValEqTp E Γ l «$vA» A → ClosEqTp E Γ l l' A «$vB» B → ValEqTp E ((A, l) :: Γ) l' «$v» B))

Evaluate a type closure on a fresh variable.

partial def SynthLean.evalClos₂Tp {_u : Lean.Level} {χ : Q(Type _u)} (vC : Q(Clos «$χ»)) (vt vu : Q(Val «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ : Ctx «$χ»} {A B C t u : Expr «$χ»} {l l' l'' : ℕ}, Clos₂EqTp E Γ A l B l' l'' «$vC» C → ValEqTm E Γ l «$vt» t A → ValEqTm E Γ l' «$vu» u (Expr.subst t.toSb B) → ValEqTp E Γ l'' «$v» (Expr.subst (Expr.snoc t.toSb u) C)))

Evaluate a type closure on two arguments.

partial def SynthLean.forceClos₂Tp {_u : Lean.Level} {χ : Q(Type _u)} (d : Q(ℕ)) (vA vB : Q(Val «$χ»)) (vC : Q(Clos «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ : Ctx «$χ»} {A B C : Expr «$χ»} {l l' l'' : ℕ}, «$d» = List.length Γ → ValEqTp E Γ l «$vA» A → ValEqTp E ((A, l) :: Γ) l' «$vB» B → Clos₂EqTp E Γ A l B l' l'' «$vC» C → ValEqTp E ((B, l') :: (A, l) :: Γ) l'' «$v» C))

partial def SynthLean.evalClosTm {_u : Lean.Level} {χ : Q(Type _u)} (vb : Q(Clos «$χ»)) (vt : Q(Val «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ : Ctx «$χ»} {A B b t : Expr «$χ»} {l l' : ℕ}, ClosEqTm E Γ l l' A B «$vb» b → ValEqTm E Γ l «$vt» t A → ValEqTm E Γ l' «$v» (Expr.subst t.toSb b) (Expr.subst t.toSb B)))

Evaluate a term closure on an argument.

partial def SynthLean.forceClosTm {_u : Lean.Level} {χ : Q(Type _u)} (d : Q(ℕ)) (vA : Q(Val «$χ»)) (vb : Q(Clos «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ : Ctx «$χ»} {A B b : Expr «$χ»} {l l' : ℕ}, «$d» = List.length Γ → ValEqTp E Γ l «$vA» A → ClosEqTm E Γ l l' A B «$vb» b → ValEqTm E ((A, l) :: Γ) l' «$v» b B))

Evaluate a term closure on a fresh variable.

def SynthLean.evalEl {_u : Lean.Level} {χ : Q(Type _u)} (va : Q(Val «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Δ : Ctx «$χ»} {a : Expr «$χ»} {l : ℕ}, ValEqTm E Δ (l + 1) «$va» a (Expr.univ l) → ValEqTp E Δ l «$v» a.el))

Equations

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

partial def SynthLean.evalApp {_u : Lean.Level} {χ : Q(Type _u)} (vf va : Q(Val «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Δ : Ctx «$χ»} {A B f a : Expr «$χ»} {l l' : ℕ}, ValEqTm E Δ (max l l') «$vf» f (Expr.pi l l' A B) → ValEqTm E Δ l «$va» a A → ValEqTm E Δ l' «$v» (Expr.app l l' B f a) (Expr.subst a.toSb B)))

def SynthLean.evalFst {_u : Lean.Level} {χ : Q(Type _u)} (vp : Q(Val «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Δ : Ctx «$χ»} {A B p : Expr «$χ»} {l l' : ℕ}, ValEqTm E Δ (max l l') «$vp» p (Expr.sigma l l' A B) → ValEqTm E Δ l «$v» (Expr.fst l l' A B p) A))

Equations

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

partial def SynthLean.evalSnd {_u : Lean.Level} {χ : Q(Type _u)} (vp : Q(Val «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Δ : Ctx «$χ»} {A B p : Expr «$χ»} {l l' : ℕ}, ValEqTm E Δ (max l l') «$vp» p (Expr.sigma l l' A B) → ValEqTm E Δ l' «$v» (Expr.snd l l' A B p) (Expr.subst (Expr.fst l l' A B p).toSb B)))

partial def SynthLean.evalIdRec {_u : Lean.Level} {χ : Q(Type _u)} (l' : Q(ℕ)) (cM : Q(Clos «$χ»)) (vr vh : Q(Val «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Δ : Ctx «$χ»} {A M t r u h : Expr «$χ»} {l : ℕ}, Clos₂EqTp E Δ A l (Expr.Id l (Expr.subst Expr.wk A) (Expr.subst Expr.wk t) (Expr.bvar 0)) l «$l'» «$cM» M → ValEqTm E Δ «$l'» «$vr» r (Expr.subst (Expr.snoc t.toSb (Expr.refl l t)) M) → ValEqTm E Δ l «$vh» h (Expr.Id l A t u) → ValEqTm E Δ «$l'» «$v» (Expr.idRec l «$l'» t M r u h) (Expr.subst (Expr.snoc u.toSb h) M)))

def SynthLean.evalTpId {_u : Lean.Level} {χ : Q(Type _u)} (vΓ : Q(TpEnv «$χ»)) (T : Q(Expr «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ : Ctx «$χ»} {l : ℕ}, TpEnvEqCtx E «$vΓ» Γ → E ∣ Γ ⊢[l] «$T» → ValEqTp E Γ l «$v» «$T»))

Evaluate a type in the identity evaluation environment.

Equations

• SynthLean.evalTpId vΓ T = do let __discr ← SynthLean.evalTp q(«$vΓ».toEnv) q(«$T») match __discr with | ⟨vT, vTpost⟩ => pure ⟨vT, q(⋯)⟩

def SynthLean.evalTmId {_u : Lean.Level} {χ : Q(Type _u)} (vΓ : Q(TpEnv «$χ»)) (t : Q(Expr «$χ»)) : TypecheckerM ((v : Q(Val «$χ»)) × Q(∀ {E : Axioms «$χ»} {Γ : Ctx «$χ»} {A : Expr «$χ»} {l : ℕ}, TpEnvEqCtx E «$vΓ» Γ → E ∣ Γ ⊢[l] «$t» : A → ValEqTm E Γ l «$v» «$t» A))

Evaluate a term in the identity evaluation environment.

Equations

• SynthLean.evalTmId vΓ t = do let __discr ← SynthLean.evalTm q(«$vΓ».toEnv) q(«$t») match __discr with | ⟨vt, vtpost⟩ => pure ⟨vt, q(⋯)⟩