From aeac85dadb9cc67e2c35db3ccd354cd0b840a971 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Oct 2020 09:07:46 -0700 Subject: [PATCH] chore: cleanup --- src/Lean/Meta/Match/Match.lean | 63 +++++++++++++---------------- tests/lean/match1.lean.expected.out | 2 +- 2 files changed, 28 insertions(+), 37 deletions(-) diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index cfbf7e2f2f..74c1f23b3a 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -29,13 +29,13 @@ namespace Pattern instance : Inhabited Pattern := ⟨Pattern.inaccessible (arbitrary _)⟩ partial def toMessageData : Pattern → MessageData -| inaccessible e => ".(" ++ e ++ ")" +| inaccessible e => msg!".({e})" | var varId => mkFVar varId | ctor ctorName _ _ [] => ctorName -| ctor ctorName _ _ pats => "(" ++ ctorName ++ pats.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil ++ ")" +| ctor ctorName _ _ pats => msg!"({ctorName}{pats.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil})" | val e => e -| arrayLit _ pats => "#[" ++ MessageData.joinSep (pats.map toMessageData) ", " ++ "]" -| as varId p => mkFVar varId ++ "@" ++toMessageData p +| arrayLit _ pats => msg!"#[{MessageData.joinSep (pats.map toMessageData) ", "}]" +| as varId p => msg!"{mkFVar varId}@{toMessageData p}" partial def toExpr : Pattern → MetaM Expr | inaccessible e => pure e @@ -151,10 +151,10 @@ match alt.fvarDecls.find? fun (fvarDecl : LocalDecl) => fvarDecl.fvarId == fvarI | none => throwErrorAt alt.ref "unknown free pattern variable" | some fvarDecl => do let vType ← inferType v - unlessM (isDefEqGuarded fvarDecl.type vType) $ - withExistingLocalDecls alt.fvarDecls $ throwErrorAt alt.ref $ - "type mismatch during dependent match-elimination at pattern variable '" ++ mkFVar fvarDecl.fvarId ++ "' with type" ++ indentExpr fvarDecl.type ++ - Format.line ++ "expected type" ++ indentExpr vType + unless (← isDefEqGuarded fvarDecl.type vType) do + withExistingLocalDecls alt.fvarDecls do + throwErrorAt alt.ref $ + msg!"type mismatch during dependent match-elimination at pattern variable '{mkFVar fvarDecl.fvarId}' with type{indentExpr fvarDecl.type}\nexpected type{indentExpr vType}" pure $ replaceFVarId fvarId v alt end Alt @@ -239,9 +239,9 @@ structure MatcherResult := (unusedAltIdxs : List Nat) /- The number of patterns in each AltLHS must be equal to majors.length -/ -private def checkNumPatterns (majors : Array Expr) (lhss : List AltLHS) : MetaM Unit := +private def checkNumPatterns (majors : Array Expr) (lhss : List AltLHS) : MetaM Unit := do let num := majors.size -when (lhss.any (fun lhs => lhs.patterns.length != num)) $ +if lhss.any fun lhs => lhs.patterns.length != num then throwError "incorrect number of patterns" private partial def withAltsAux {α} (motive : Expr) : List AltLHS → List Alt → Array (Expr × Nat) → (List Alt → Array (Expr × Nat) → MetaM α) → MetaM α @@ -390,7 +390,7 @@ match p.vars with private def throwInductiveTypeExpected {α} (e : Expr) : MetaM α := do let t ← inferType e -throwError ("failed to compile pattern matching, inductive type expected" ++ indentExpr e ++ Format.line ++ "has type" ++ indentExpr t) +throwError! "failed to compile pattern matching, inductive type expected{indentExpr e}\nhas type{indentExpr t}" private def inLocalDecls (localDecls : List LocalDecl) (fvarId : FVarId) : Bool := localDecls.any fun d => d.fvarId == fvarId @@ -525,9 +525,7 @@ match alt.patterns with pure $ some { alt with patterns := fields ++ ps } else pure none - | _ => throwErrorAt alt.ref $ - "dependent match elimination failed, inaccessible pattern found " ++ indentD p.toMessageData ++ - Format.line ++ "constructor expected" + | _ => throwErrorAt! alt.ref "dependent match elimination failed, inaccessible pattern found{indentD p.toMessageData}\nconstructor expected" | _ => unreachable! private def processConstructor (p : Problem) : MetaM (Array Problem) := do @@ -591,20 +589,17 @@ match p.vars with else pure $ some { alt with patterns := fields ++ ps } | Pattern.inaccessible _ :: _ => processInaccessibleAsCtor alt ctorVal.name - | p :: _ => throwError ("failed to compile pattern matching, inaccessible pattern or constructor expected" ++ indentD p.toMessageData) + | p :: _ => throwError! "failed to compile pattern matching, inaccessible pattern or constructor expected{indentD p.toMessageData}" | _ => unreachable! let xFields := xArgs.extract ctorVal.nparams xArgs.size pure { p with alts := alts, vars := xFields.toList ++ xs } - | none => - throwError ("failed to compile pattern matching, constructor expected" ++ indentExpr x) + | none => throwError! "failed to compile pattern matching, constructor expected{indentExpr x}" private def collectValues (p : Problem) : Array Expr := -p.alts.foldl - (fun (values : Array Expr) alt => - match alt.patterns with - | Pattern.val v :: _ => if values.contains v then values else values.push v - | _ => values) - #[] +p.alts.foldl (init := #[]) fun values alt => + match alt.patterns with + | Pattern.val v :: _ => if values.contains v then values else values.push v + | _ => values private def isFirstPatternVar (alt : Alt) : Bool := match alt.patterns with @@ -612,7 +607,7 @@ match alt.patterns with | _ => false private def processValue (p : Problem) : MetaM (Array Problem) := do -trace! `Meta.Match.match ("value step") +trace[Meta.Match.match]! "value step" match p.vars with | [] => unreachable! | x :: xs => do @@ -644,12 +639,10 @@ match p.vars with pure { p with mvarId := subgoal.mvarId, alts := newAlts, vars := x::xs } private def collectArraySizes (p : Problem) : Array Nat := -p.alts.foldl - (fun (sizes : Array Nat) alt => - match alt.patterns with - | Pattern.arrayLit _ ps :: _ => let sz := ps.length; if sizes.contains sz then sizes else sizes.push sz - | _ => sizes) - #[] +p.alts.foldl (init := #[]) fun sizes alt => + match alt.patterns with + | Pattern.arrayLit _ ps :: _ => let sz := ps.length; if sizes.contains sz then sizes else sizes.push sz + | _ => sizes private def expandVarIntoArrayLit (alt : Alt) (fvarId : FVarId) (arrayElemType : Expr) (arraySize : Nat) : MetaM Alt := withExistingLocalDecls alt.fvarDecls do @@ -715,7 +708,7 @@ withGoalOf p (traceM `Meta.Match.match p.toMessageData) private def throwNonSupported (p : Problem) : MetaM Unit := withGoalOf p do let msg ← p.toMessageData - throwError ("failed to compile pattern matching, stuck at" ++ (indentD msg)) + throwError! "failed to compile pattern matching, stuck at{indentD msg}" def isCurrVarInductive (p : Problem) : MetaM Bool := do match p.vars with @@ -942,7 +935,7 @@ def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp := lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do unless motiveArgs.size == matcherApp.discrs.size do -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. - throwError ("unexpected matcher application, motive must be lambda expression with #" ++ toString matcherApp.discrs.size ++ " arguments") + throwError! "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" let eType ← inferType e let eTypeAbst ← matcherApp.discrs.size.foldRevM (fun i eTypeAbst => do @@ -965,7 +958,7 @@ lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do let aux := mkAppN aux matcherApp.discrs trace! `Meta.debug aux check aux - unlessM (isTypeCorrect aux) $ + unless (← isTypeCorrect aux) do throwError "failed to add argument to matcher application, type error when constructing the new motive" let auxType ← inferType aux let (altNumParams, alts) ← updateAlts auxType matcherApp.altNumParams matcherApp.alts 0 @@ -981,6 +974,4 @@ initialize registerTraceClass `Meta.Match.debug registerTraceClass `Meta.Match.unify - -end Meta -end Lean +end Lean.Meta diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out index d405485535..a3edb36f7b 100644 --- a/tests/lean/match1.lean.expected.out +++ b/tests/lean/match1.lean.expected.out @@ -15,7 +15,7 @@ match1.lean:82:0: error: type mismatch during dependent match-elimination at pat expected type VecPred P tail✝ [false, true, true] -match1.lean:113:0: error: dependent match elimination failed, inaccessible pattern found +match1.lean:113:0: error: dependent match elimination failed, inaccessible pattern found .(j + j) constructor expected [false, true, true]