From 41e574d6cc45543d182576fedab8c11cfb97c05f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 Nov 2019 14:44:05 -0800 Subject: [PATCH] chore: fix tests --- tests/compiler/float_cases_bug.lean | 4 +- tests/compiler/lazylist.lean | 2 +- tests/lean/run/34.lean | 2 +- tests/lean/run/backtrackable_estate.lean | 4 +- tests/lean/run/fun.lean | 10 +-- tests/lean/run/rc_tests.lean | 4 +- tests/lean/run/trace.lean | 6 +- tests/lean/typeclass_context.lean | 80 ++++++++++++------------ tests/lean/zipper.lean | 2 +- 9 files changed, 57 insertions(+), 57 deletions(-) diff --git a/tests/compiler/float_cases_bug.lean b/tests/compiler/float_cases_bug.lean index 304a43d527..af8e76fbe8 100644 --- a/tests/compiler/float_cases_bug.lean +++ b/tests/compiler/float_cases_bug.lean @@ -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 () diff --git a/tests/compiler/lazylist.lean b/tests/compiler/lazylist.lean index 84afc0c941..8366517044 100644 --- a/tests/compiler/lazylist.lean +++ b/tests/compiler/lazylist.lean @@ -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 diff --git a/tests/lean/run/34.lean b/tests/lean/run/34.lean index c900d0a004..d6e82e6b04 100644 --- a/tests/lean/run/34.lean +++ b/tests/lean/run/34.lean @@ -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 diff --git a/tests/lean/run/backtrackable_estate.lean b/tests/lean/run/backtrackable_estate.lean index 1e151d28bb..b5a078807a 100644 --- a/tests/lean/run/backtrackable_estate.lean +++ b/tests/lean/run/backtrackable_estate.lean @@ -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 } diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean index 17b0179197..7810d098c4 100644 --- a/tests/lean/run/fun.lean +++ b/tests/lean/run/fun.lean @@ -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 _ diff --git a/tests/lean/run/rc_tests.lean b/tests/lean/run/rc_tests.lean index 0cedad2f06..27390e9596 100644 --- a/tests/lean/run/rc_tests.lean +++ b/tests/lean/run/rc_tests.lean @@ -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 diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean index 5930491fe7..9f95e81066 100644 --- a/tests/lean/run/trace.lean +++ b/tests/lean/run/trace.lean @@ -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 "----"; diff --git a/tests/lean/typeclass_context.lean b/tests/lean/typeclass_context.lean index 179d015ed5..6087f12f0d 100644 --- a/tests/lean/typeclass_context.lean +++ b/tests/lean/typeclass_context.lean @@ -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 {} diff --git a/tests/lean/zipper.lean b/tests/lean/zipper.lean index a5209e64ea..c150919baf 100644 --- a/tests/lean/zipper.lean +++ b/tests/lean/zipper.lean @@ -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 α