max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-05 14:44:05 -08:00
parent c3e9ac73e2
commit 41e574d6cc
9 changed files with 57 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/compiler/float_cases_bug.lean
View file

@ -11,11 +11,11 @@ end Term
open Term
structure MyState : Type := (ts : List Term)
def emit (t : Term) : State MyState Unit := modify (λ ms => ⟨t::ms.ts⟩)
def emit (t : Term) : StateM MyState Unit := modify (λ ms => ⟨t::ms.ts⟩)
partial def foo : MyState -> Term -> Term -> List Term
| ms₀, t, u =>
let stateT : State MyState Unit := do {
let stateT : StateM MyState Unit := do {
match t with
| const _ => pure ()

2
tests/compiler/lazylist.lean
View file

@ -35,7 +35,7 @@ partial def toList : LazyList α → List α
| delayed as => toList as.get
partial def head [Inhabited α] : LazyList α → α
| nil => default α
| nil => arbitrary α
| cons a as => a
| delayed as => head as.get

2
tests/lean/run/34.lean
View file

@ -1,4 +1,4 @@
partial def foo : ∀ (n : Nat), State Unit Unit
partial def foo : ∀ (n : Nat), StateM Unit Unit
| n =>
if n == 0 then pure () else
match n with

4
tests/lean/run/backtrackable_estate.lean
View file

@ -7,11 +7,11 @@ structure MyState :=
instance : HasRepr MyState :=
⟨fun s => repr (s.bs, s.ps)⟩
instance : EState.Backtrackable Nat MyState :=
instance : EStateM.Backtrackable Nat MyState :=
{ save := fun s => s.bs,
restore := fun s d => { bs := d, .. s } }
abbrev M := EState String MyState
abbrev M := EStateM String MyState
def bInc : M Unit := -- increment backtrackble counter
modify $ fun s => { bs := s.bs + 1, .. s }

10
tests/lean/run/fun.lean
View file

@ -1,19 +1,19 @@
open Function Bool
constant f : Nat → Bool := default _
constant g : Nat → Nat := default _
constant f : Nat → Bool := arbitrary _
constant g : Nat → Nat := arbitrary _
#check f ∘ g ∘ g
#check (id : Nat → Nat)
constant h : Nat → Bool → Nat := default _
constant h : Nat → Bool → Nat := arbitrary _
#check swap h
#check swap h false Nat.zero
#check (swap h false Nat.zero : Nat)
constant f1 : Nat → Nat → Bool := default _
constant f2 : Bool → Nat := default _
constant f1 : Nat → Nat → Bool := arbitrary _
constant f2 : Bool → Nat := arbitrary _

4
tests/lean/run/rc_tests.lean
View file

@ -58,10 +58,10 @@ end x5
namespace x6
@[noinline] def act : State Nat Unit :=
@[noinline] def act : StateM Nat Unit :=
modify (fun a => a + 1)
def f : State Nat Unit :=
def f : StateM Nat Unit :=
act *> act
end x6

6
tests/lean/run/trace.lean
View file

@ -5,7 +5,7 @@ structure MyState :=
(traceState : TraceState := {})
(s : Nat := 0)
abbrev M := ReaderT Options (EState String MyState)
abbrev M := ReaderT Options (EStateM String MyState)
/- We can enable tracing for a monad M by adding an instance of `SimpleMonadTracerAdapter M` -/
instance : SimpleMonadTracerAdapter M :=
@ -52,8 +52,8 @@ let opts := opts.setBool `trace.module true;
let opts := opts.setBool `trace.bughunt true;
-- let opts := opts.setBool `trace.slow true;
match x.run opts {} with
| EState.Result.ok _ s => IO.println s.traceState
| EState.Result.error _ s => do IO.println "Error"; IO.println s.traceState
| EStateM.Result.ok _ s => IO.println s.traceState
| EStateM.Result.error _ s => do IO.println "Error"; IO.println s.traceState
def main : IO Unit :=
do IO.println "----";

80
tests/lean/typeclass_context.lean
View file

@ -13,91 +13,91 @@ open Lean
open Lean.TypeClass
open Lean.TypeClass.Context
def testEUnify1 : EState String Context Expr := do
t ← EState.fromState $ eNewMeta (mkConst "Term");
def testEUnify1 : EStateM String Context Expr := do
t ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
eUnify (mkApp (mkConst "f") #[mkConst "a"]) t;
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t
def testEUnify2 : EState String Context Expr := do
t ← EState.fromState $ eNewMeta (mkConst "Term");
def testEUnify2 : EStateM String Context Expr := do
t ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
eUnify (mkApp (mkConst "f") #[mkConst "a"]) (mkApp (mkConst "f") #[t]);
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t
def testEUnify3 : EState String Context Expr := do
t ← EState.fromState $ eNewMeta (mkConst "Term");
def testEUnify3 : EStateM String Context Expr := do
t ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
eUnify t t;
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t
def testEUnify4 : EState String Context Expr := do
t₁ ← EState.fromState $ eNewMeta (mkConst "Term");
t₂ ← EState.fromState $ eNewMeta (mkConst "Term");
def testEUnify4 : EStateM String Context Expr := do
t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
eUnify (Expr.forallE "foo" BinderInfo.default t₂ t₁) (Expr.forallE "foo" BinderInfo.default t₁ t₂);
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
def testEUnify5 : EState String Context Expr := do
t₁ ← EState.fromState $ eNewMeta (mkConst "Term");
t₂ ← EState.fromState $ eNewMeta (mkConst "Term");
def testEUnify5 : EStateM String Context Expr := do
t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
eUnify (Expr.forallE "foo" BinderInfo.default t₁ t₂) (Expr.forallE "foo" BinderInfo.default t₂ t₁);
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
def testEUnify6 : EState String Context Expr := do
u ← EState.fromState Context.uNewMeta;
def testEUnify6 : EStateM String Context Expr := do
u ← EStateM.fromStateM Context.uNewMeta;
let t₁ := Expr.const "foo" [Level.zero];
let t₂ := Expr.const "foo" [u];
eUnify t₁ t₂;
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
def testEUnify7 : EState String Context Expr := do
e ← EState.fromState $ Context.eNewMeta $ Expr.sort Level.zero;
def testEUnify7 : EStateM String Context Expr := do
e ← EStateM.fromStateM $ Context.eNewMeta $ Expr.sort Level.zero;
let t₁ := Expr.fvar "foo";
let t₂ := e;
eUnify t₁ t₂;
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
def testEAssign1 : EState String Context Expr := do
t ← EState.fromState $ eNewMeta (mkConst "Term");
EState.fromState $ eAssign t $ mkApp (mkConst "f") #[mkConst "a"];
def testEAssign1 : EStateM String Context Expr := do
t ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
EStateM.fromStateM $ eAssign t $ mkApp (mkConst "f") #[mkConst "a"];
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t
def testClash1 : EState String Context Expr := do
def testClash1 : EStateM String Context Expr := do
eUnify (mkConst "f") (mkConst "g");
pure $ default _
pure $ arbitrary _
def testClash2 : EState String Context Expr := do
def testClash2 : EStateM String Context Expr := do
eUnify (mkApp (mkConst "f") #[mkConst "a"]) (mkApp (mkConst "g") #[mkConst "a"]);
pure $ default _
pure $ arbitrary _
def testClash3 : EState String Context Expr := do
def testClash3 : EStateM String Context Expr := do
eUnify (mkApp (mkConst "f") #[mkConst "a"]) (mkApp (mkConst "f") #[mkConst "b"]);
pure $ default _
pure $ arbitrary _
def testClash4 : EState String Context Expr := do
def testClash4 : EStateM String Context Expr := do
eUnify (mkApp (mkConst "f") #[mkConst "a"]) (mkApp (mkConst "f") #[]);
pure $ default _
pure $ arbitrary _
def testChain1 : EState String Context Expr := do
t₁ ← EState.fromState $ eNewMeta (mkConst "Term");
t₂ ← EState.fromState $ eNewMeta (mkConst "Term");
def testChain1 : EStateM String Context Expr := do
t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
eUnify t₁ t₂;
eUnify t₂ $ mkConst "foo";
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₁
def testAlphaNorm1 : EState String Context Expr := do
t₁ ← EState.fromState $ eNewMeta (mkConst "Term");
t₂ ← EState.fromState $ eNewMeta (mkConst "Term");
def testAlphaNorm1 : EStateM String Context Expr := do
t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
pure $ αNorm $ mkApp (mkConst "f") #[t₁, t₂]
def testAlphaNorm2 : EState String Context Expr := do
t₁ ← EState.fromState $ eNewMeta (mkConst "Term");
t₂ ← EState.fromState $ eNewMeta (mkConst "Term");
def testAlphaNorm2 : EStateM String Context Expr := do
t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
pure $ αNorm $ mkApp (mkConst "f") #[t₂, t₁]
def testAlphaNorm3 : EState String Context Expr := do
def testAlphaNorm3 : EStateM String Context Expr := do
pure $ αNorm (mkConst "f")
def testAlphaNorm4 : EState String Context Expr := do
t₁ ← EState.fromState $ eNewMeta (mkConst "Term");
t₂ ← EState.fromState $ eNewMeta (mkConst "Term");
def testAlphaNorm4 : EStateM String Context Expr := do
t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term");
pure $ αNorm $ Expr.forallE "foo" BinderInfo.default (mkApp (mkConst "f") #[t₂]) (mkApp (mkConst "g") #[t₁])
#eval testEUnify1.run {}

2
tests/lean/zipper.lean
View file

@ -23,7 +23,7 @@ def erase : ListZipper α → ListZipper α
| ⟨x::xs, bs⟩ => ⟨xs, bs⟩
def curr [Inhabited α] : ListZipper α → α
| ⟨[], bs⟩ => default _
| ⟨[], bs⟩ => arbitrary _
| ⟨x::xs, bs⟩ => x
def currOpt : ListZipper α → Option α