From 8e81db0d2b2b71cd54b89df64229eec1b288d860 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 27 Sep 2020 06:58:10 -0700 Subject: [PATCH] chore: add temporary workaround to tests We will remove it after we implement `doMatch` --- src/Lean/Elab/Do.lean | 4 ++-- tests/lean/PPRoundtrip.lean | 4 ++-- tests/lean/run/28.lean | 6 +++--- tests/lean/run/catchThe.lean | 4 ++-- tests/lean/run/depElim1.lean | 12 ++++++------ tests/lean/run/elabCmd.lean | 10 +++++----- tests/lean/run/finally.lean | 4 ++-- tests/lean/run/instuniv.lean | 2 +- tests/lean/run/meta2.lean | 12 ++++++------ tests/lean/run/meta3.lean | 4 ++-- tests/lean/run/structInst2.lean | 8 ++++---- tests/lean/run/termparsertest1.lean | 4 ++-- tests/lean/run/toExpr.lean | 6 +++--- 13 files changed, 40 insertions(+), 40 deletions(-) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 98c78e1cec..d8ce57b2f1 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -127,10 +127,10 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → MacroM Syn rest ← mkRest (); newBody ← if optElse.isNone then do - `(do let x ← $discr; match x with | $pat => $rest) + `(do let x ← $discr; (match x with | $pat => $rest)) else let elseBody := optElse.getArg 1; - `(do let x ← $discr; match x with | $pat => $rest | _ => $elseBody); + `(do let x ← $discr; (match x with | $pat => $rest | _ => $elseBody)); addPrefix newBody else if i < doElems.size - 1 && doElem.getKind == `Lean.Parser.Term.doExpr then do -- def doExpr := parser! termParser diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 56d2ac2a96..be235dbd22 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -17,12 +17,12 @@ let stx' ← liftCoreM $ PrettyPrinter.parenthesizeTerm stx'; let f' ← liftCoreM $ PrettyPrinter.formatTerm stx'; IO.println $ f'.pretty opts; let env ← getEnv; -match Parser.runParserCategory env `term (toString f') "" with +(match Parser.runParserCategory env `term (toString f') "" with | Except.error e => throwErrorAt stx e | Except.ok stx'' => do let e' ← elabTermAndSynthesize stx'' none <* throwErrorIfErrors; unlessM (isDefEq e e') $ - throwErrorAt stx (fmt "failed to round-trip" ++ line ++ fmt e ++ line ++ fmt e') + throwErrorAt stx (fmt "failed to round-trip" ++ line ++ fmt e ++ line ++ fmt e')) -- set_option trace.PrettyPrinter.parenthesize true set_option format.width 20 diff --git a/tests/lean/run/28.lean b/tests/lean/run/28.lean index 9755771dea..897ad3d5e6 100644 --- a/tests/lean/run/28.lean +++ b/tests/lean/run/28.lean @@ -39,6 +39,6 @@ def evalInstr : instr → sim (Option val) | instr.store _ _ _ => do let pv <- f; g; - match pv with - | val.bv 27 _ => throw (IO.userError "asdf") - | _ => throw (IO.userError "expected pointer value in store" ) + (match pv with + | val.bv 27 _ => throw (IO.userError "asdf") + | _ => throw (IO.userError "expected pointer value in store" )) diff --git a/tests/lean/run/catchThe.lean b/tests/lean/run/catchThe.lean index 843999190f..9efa9d7411 100644 --- a/tests/lean/run/catchThe.lean +++ b/tests/lean/run/catchThe.lean @@ -9,9 +9,9 @@ abbrev M := ExceptT String $ MetaM def testM {α} [HasBeq α] [HasToString α] (x : M α) (expected : α) : MetaM Unit := do let r ← x; -match r with +(match r with | Except.ok a => unless (a == expected) $ throwError ("unexpected result " ++ toString a) -| Except.error e => throwError ("FAILED: " ++ e) +| Except.error e => throwError ("FAILED: " ++ e)) @[noinline] def act1 : M Nat := throwThe Exception $ Exception.error Syntax.missing "Error at act1" diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean index 4541c9e469..a3925b45ea 100644 --- a/tests/lean/run/depElim1.lean +++ b/tests/lean/run/depElim1.lean @@ -26,20 +26,20 @@ inductive ArrayLit4 {α : Sort u} (a b c d : α) : Type u | mk : ArrayLit4 a b c private def getConstructorVal (ctorName : Name) (fn : Expr) (args : Array Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do let env ← getEnv; -match env.find? ctorName with +(match env.find? ctorName with | some (ConstantInfo.ctorInfo v) => if args.size == v.nparams + v.nfields then pure $ some (v, fn, args) else pure none -| _ => pure none +| _ => pure none) private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do let env ← getEnv; -match e with +(match e with | Expr.lit (Literal.natVal n) _ => if n == 0 then getConstructorVal `Nat.zero (mkConst `Nat.zero) #[] else getConstructorVal `Nat.succ (mkConst `Nat.succ) #[mkNatLit (n-1)] | _ => let fn := e.getAppFn; match fn with | Expr.const n _ _ => getConstructorVal n fn e.getAppArgs - | _ => pure none + | _ => pure none) /- Convert expression using auxiliary hints `inaccessible` and `val` into a pattern -/ partial def mkPattern : Expr → MetaM Pattern @@ -75,13 +75,13 @@ partial def mkPattern : Expr → MetaM Pattern | none => do let e ← whnfD e; let r? ← constructorApp? e; - match r? with + (match r? with | none => throwError "unexpected pattern" | some (cval, fn, args) => do let params := args.extract 0 cval.nparams; let fields := args.extract cval.nparams args.size; let pats ← fields.toList.mapM mkPattern; - pure $ Pattern.ctor cval.name fn.constLevels! params.toList pats + pure $ Pattern.ctor cval.name fn.constLevels! params.toList pats) partial def decodePats : Expr → MetaM (List Pattern) | e => diff --git a/tests/lean/run/elabCmd.lean b/tests/lean/run/elabCmd.lean index db66134b0c..06c4a7e093 100644 --- a/tests/lean/run/elabCmd.lean +++ b/tests/lean/run/elabCmd.lean @@ -7,21 +7,21 @@ open Lean.Elab.Term def getCtors (c : Name) : TermElabM (List Name) := do let env ← getEnv; -match env.find? c with +(match env.find? c with | some (ConstantInfo.inductInfo val) => pure val.ctors -| _ => pure [] +| _ => pure []) -def elabAnonCtor (args : Syntax) (τ : Expr) : TermElabM Expr := do +def elabAnonCtor (args : Syntax) (τ : Expr) : TermElabM Expr := match τ.getAppFn with | Expr.const C _ _ => do let ctors ← getCtors C; - match ctors with + (match ctors with | [c] => do let stx ← `($(Lean.mkIdent c) $(Array.getSepElems args.getArgs)*); elabTerm stx τ -- error handling - | _ => unreachable! + | _ => unreachable!) | _ => unreachable! elab "foo⟨" args:(sepBy term ", ") "⟩" : term <= τ => do diff --git a/tests/lean/run/finally.lean b/tests/lean/run/finally.lean index 5853e2731c..cf48e9099b 100644 --- a/tests/lean/run/finally.lean +++ b/tests/lean/run/finally.lean @@ -18,9 +18,9 @@ catch def checkE {α ε : Type} [HasBeq α] (x : IO (Except ε α)) (expected : α) : IO Unit := do let r ← x; -match r with +(match r with | Except.ok a => unless (a == expected) $ throw $ IO.userError "unexpected result" -| Except.error _ => throw $ IO.userError "unexpected error" +| Except.error _ => throw $ IO.userError "unexpected error") #eval (tst1.run).run' 0 diff --git a/tests/lean/run/instuniv.lean b/tests/lean/run/instuniv.lean index d266b7472b..9dc9189b39 100644 --- a/tests/lean/run/instuniv.lean +++ b/tests/lean/run/instuniv.lean @@ -3,7 +3,7 @@ new_frontend open Lean unsafe def tst : IO Unit := -withImportModules [{module := `Init.Data.Array}] 0 fun env => do +withImportModules [{module := `Init.Data.Array}] 0 fun env => match env.find? `Array.foldl with | some info => do IO.println (info.instantiateTypeLevelParams [levelZero, levelZero]); diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean index 2fc2b6e5cd..1c8826e54b 100644 --- a/tests/lean/run/meta2.lean +++ b/tests/lean/run/meta2.lean @@ -16,9 +16,9 @@ unlessM x $ throwError "check failed" def getAssignment (m : Expr) : MetaM Expr := do let v? ← getExprMVarAssignment? m.mvarId!; - match v? with + (match v? with | some v => pure v - | none => throwError "metavariable is not assigned" + | none => throwError "metavariable is not assigned") def nat := mkConst `Nat def boolE := mkConst `Bool @@ -734,12 +734,12 @@ check t; let t <- mkArrayLit nat [mkNatLit 1, mkNatLit 2]; print t; check t; -match t.arrayLit? with +(match t.arrayLit? with | some (_, xs) => do check $ pure $ xs.length == 2; - match (xs.get! 0).natLit?, (xs.get! 1).natLit? with + (match (xs.get! 0).natLit?, (xs.get! 1).natLit? with | some 1, some 2 => pure () - | _, _ => throwError "nat lits expected" -| none => throwError "array lit expected" + | _, _ => throwError "nat lits expected") +| none => throwError "array lit expected") #eval tst42 diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean index afadbbec01..d36a03fe0e 100644 --- a/tests/lean/run/meta3.lean +++ b/tests/lean/run/meta3.lean @@ -17,9 +17,9 @@ unlessM x $ throwError "check failed" def getAssignment (m : Expr) : MetaM Expr := do let v? ← getExprMVarAssignment? m.mvarId!; - match v? with + (match v? with | some v => pure v - | none => throwError "metavariable is not assigned" + | none => throwError "metavariable is not assigned") unsafe def run (mods : List Name) (x : MetaM Unit) (opts : Options := dbgOpt) : IO Unit := withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do diff --git a/tests/lean/run/structInst2.lean b/tests/lean/run/structInst2.lean index e7229ac955..85f009b56e 100644 --- a/tests/lean/run/structInst2.lean +++ b/tests/lean/run/structInst2.lean @@ -12,9 +12,9 @@ variables {m : Type u → Type v} [Monad m] {α β : Type u} @[inline] protected def bind (ma : OptionT2 m α) (f : α → OptionT2 m β) : OptionT2 m β := (do { let a? ← ma; - match a? with + (match a? with | some a => f a - | none => pure none + | none => pure none) } : m (Option β)) @[inline] protected def pure (a : α) : OptionT2 m α := @@ -22,9 +22,9 @@ variables {m : Type u → Type v} [Monad m] {α β : Type u} @[inline] protected def orelse (ma : OptionT2 m α) (mb : OptionT2 m α) : OptionT2 m α := (do { let a? ← ma; - match a? with + (match a? with | some a => pure (some a) - | _ => mb } : m (Option α)) + | _ => mb) } : m (Option α)) @[inline] protected def fail : OptionT2 m α := (pure none : m (Option α)) diff --git a/tests/lean/run/termparsertest1.lean b/tests/lean/run/termparsertest1.lean index 643cf057b2..a36f803753 100644 --- a/tests/lean/run/termparsertest1.lean +++ b/tests/lean/run/termparsertest1.lean @@ -17,9 +17,9 @@ is.forM $ fun input => do def testParserFailure (input : String) : IO Unit := do let env ← mkEmptyEnvironment; -match runParserCategory env `term input "" with +(match runParserCategory env `term input "" with | Except.ok stx => throw (IO.userError ("unexpected success\n" ++ toString stx)) -| Except.error msg => IO.println ("failed as expected, error: " ++ msg) +| Except.error msg => IO.println ("failed as expected, error: " ++ msg)) def testFailures (is : List String) : IO Unit := is.forM $ fun input => do diff --git a/tests/lean/run/toExpr.lean b/tests/lean/run/toExpr.lean index c141b34058..219fff463f 100644 --- a/tests/lean/run/toExpr.lean +++ b/tests/lean/run/toExpr.lean @@ -14,16 +14,16 @@ let decl := Declaration.defnDecl { isUnsafe := false }; IO.println (toExpr a); -match env.addAndCompile {} decl with +(match env.addAndCompile {} decl with | Except.error _ => throwError "addDecl failed" -| Except.ok env => do +| Except.ok env => match env.evalConst α auxName with | Except.error ex => throwError ex | Except.ok b => do IO.println b; unless (a == b) $ throwError "toExpr failed"; - pure () + pure ()) #eval test #[(1, 2), (3, 4)] #eval test ['a', 'b', 'c']