55 lines
1.8 KiB
Text
55 lines
1.8 KiB
Text
inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
|
||
| nil : HList β []
|
||
| cons : β i → HList β is → HList β (i::is)
|
||
|
||
infix:67 " :: " => HList.cons
|
||
|
||
inductive Member : α → List α → Type _
|
||
| head : Member a (a::as)
|
||
| tail : Member a bs → Member a (b::bs)
|
||
|
||
def HList.get : HList β is → Member i is → β i
|
||
| a::as, .head => a
|
||
| a::as, .tail h => as.get h
|
||
|
||
inductive Ty where
|
||
| nat
|
||
| fn : Ty → Ty → Ty
|
||
|
||
abbrev Ty.denote : Ty → Type
|
||
| nat => Nat
|
||
| fn a b => a.denote → b.denote
|
||
|
||
inductive Term : List Ty → Ty → Type
|
||
| var : Member ty ctx → Term ctx ty
|
||
| const : Nat → Term ctx .nat
|
||
| plus : Term ctx .nat → Term ctx .nat → Term ctx .nat
|
||
| app : Term ctx (.fn dom ran) → Term ctx dom → Term ctx ran
|
||
| lam : Term (dom :: ctx) ran → Term ctx (.fn dom ran)
|
||
| «let» : Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
|
||
|
||
@[simp] def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote
|
||
| var h, env => env.get h
|
||
| const n, _ => n
|
||
| plus a b, env => a.denote env + b.denote env
|
||
| app f a, env => f.denote env (a.denote env)
|
||
| lam b, env => fun x => b.denote (x :: env)
|
||
| «let» a b, env => b.denote (a.denote env :: env)
|
||
|
||
@[simp] def Term.constFold : Term ctx ty → Term ctx ty
|
||
| const n => const n
|
||
| var h => var h
|
||
| app f a => app f.constFold a.constFold
|
||
| lam b => lam b.constFold
|
||
| «let» a b => «let» a.constFold b.constFold
|
||
| plus a b =>
|
||
match a.constFold, b.constFold with
|
||
| const n, const m => const (n+m)
|
||
| a', b' => plus a' b'
|
||
|
||
theorem Term.constFold_sound (e : Term ctx ty) : e.constFold.denote env = e.denote env := by
|
||
induction e with simp [*]
|
||
| plus a b iha ihb =>
|
||
split
|
||
next he₁ he₂ => simp [← iha, ← ihb, he₁, he₂]
|
||
next => simp [iha, ihb]
|