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.
81 lines
2 KiB
Text
81 lines
2 KiB
Text
universe u v
|
||
|
||
inductive myList (α : Type u)
|
||
| nil : myList α
|
||
| cons : α → myList α → myList α
|
||
|
||
inductive myPair (α : Type u) (β : Type v)
|
||
| mk : α → β → myPair α β
|
||
|
||
mutual
|
||
variable (α : Type u) (m : α → Type v)
|
||
inductive bla : Nat → Type (max u v)
|
||
| mk₁ (n : Nat) : α → boo n → bla (n+1)
|
||
| mk₂ (a : α) : m a → String → bla 0
|
||
inductive boo : Nat → Type (max u v)
|
||
| mk₃ (n : Nat) : bla n → bla (n+1) → boo (n+2)
|
||
end
|
||
|
||
#print bla
|
||
|
||
inductive Term (α : Type) (β : Type)
|
||
| var : α → bla (Term α β) (fun _ => Term α β) 10 → Term α β
|
||
| foo (p : Nat → myPair (Term α β) (myList $ Term α β)) (n : β) : myList (myList $ Term α β) → Term α β
|
||
|
||
#print Term
|
||
#print Term.below
|
||
#check @Term.casesOn
|
||
#print Term.noConfusionType
|
||
#print Term.noConfusion
|
||
|
||
inductive arrow (α β : Type)
|
||
| mk (s : Nat → myPair α β) : arrow α β
|
||
|
||
mutual
|
||
inductive tst1
|
||
| mk : (arrow (myPair tst2 Bool) tst2) → tst1
|
||
inductive tst2
|
||
| mk : tst1 → tst2
|
||
end
|
||
|
||
#check @tst1.casesOn
|
||
#check @tst2.casesOn
|
||
#check @tst1.recOn
|
||
|
||
namespace test
|
||
|
||
inductive Rbnode (α : Type u)
|
||
| leaf : Rbnode α
|
||
| redNode (lchild : Rbnode α) (val : α) (rchild : Rbnode α) : Rbnode α
|
||
| blackNode (lchild : Rbnode α) (val : α) (rchild : Rbnode α) : Rbnode α
|
||
|
||
#reduce sizeOf <| Rbnode.redNode Rbnode.leaf 10 Rbnode.leaf
|
||
|
||
#check @Rbnode.brecOn
|
||
|
||
namespace Rbnode
|
||
variable {α : Type u}
|
||
|
||
opaque insert (lt : α → α → Prop) [DecidableRel lt] (t : Rbnode α) (x : α) : Rbnode α := Rbnode.leaf
|
||
|
||
inductive WellFormed (lt : α → α → Prop) : Rbnode α → Prop
|
||
| leafWff : WellFormed lt leaf
|
||
| insertWff {n n' : Rbnode α} {x : α} (s : DecidableRel lt) : WellFormed lt n → n' = insert lt n x → WellFormed lt n'
|
||
|
||
end Rbnode
|
||
|
||
def Rbtree (α : Type u) (lt : α → α → Prop) : Type u :=
|
||
{t : Rbnode α // t.WellFormed lt }
|
||
|
||
inductive Trie
|
||
| Empty : Trie
|
||
| mk : Char → Rbnode (myPair Char Trie) → Trie
|
||
|
||
#print Trie.rec
|
||
#print Trie.noConfusion
|
||
end test
|
||
|
||
inductive Foo
|
||
| mk : List Foo → Foo
|
||
|
||
#check Foo
|