08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
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]
|