feat: match-expressions showing signs of life

src/Lean/Elab/Match.lean

@@ -500,7 +500,6 @@ private def elabPatterns (patternVarDecls : Array PatternVarDecl) (patternStxs :
 (patterns, matchType) ← withSynthesize $ elabPatternsAux patternStxs 0 matchType #[];
 localDecls ← finalizePatternDecls patternVarDecls;
 patterns ← patterns.mapM instantiateMVars;
-trace `Elab.match fun _ => MessageData.ofArray $ localDecls.map fun (d : LocalDecl) => (d.userName ++ " : " ++ d.type : MessageData);
 patterns.forM $ fun pattern => when pattern.hasExprMVar $ throwError ("pattern contains metavariables " ++ indentExpr pattern);
 patterns ← patterns.mapM $ toDepElimPattern localDecls;
 trace `Elab.match fun _ => "patterns: " ++ MessageData.ofArray (patterns.map fun (p : Meta.DepElim.Pattern) => p.toMessageData);
@@ -518,6 +517,14 @@ withPatternVars patternVars fun patternVarDecls => do
   trace `Elab.match fun _ => "rhs: " ++ rhs;
   pure (altLHS, rhs)
 
+def mkMotiveType (matchType : Expr) (expectedType : Expr) : TermElabM Expr := do
+liftMetaM $ Meta.forallTelescopeReducing matchType fun xs matchType => do
+  u ← Meta.getLevel matchType;
+  Meta.mkForall xs (mkSort u)
+
+def mkElim (elimName : Name) (motiveType : Expr) (lhss : List Meta.DepElim.AltLHS) : TermElabM Meta.DepElim.ElimResult :=
+liftMetaM $ Meta.DepElim.mkElim elimName motiveType lhss
+
 /-
 ```
 parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
@@ -534,7 +541,18 @@ matchType ← elabMatchOptType stx discrStxs.size;
 matchAlts ← expandMacrosInPatterns $ getMatchAlts stx;
 discrs ← elabDiscrs discrStxs matchType expectedType;
 alts ← matchAlts.mapM $ fun alt => elabMatchAltView alt matchType;
-throwError ("WIP type: " ++ matchType ++ "\n" ++ discrs ++ "\n" ++ toString (matchAlts.map fun alt => toString alt.patterns))
+let rhss := alts.map Prod.snd;
+let altLHSS := alts.map Prod.fst;
+motiveType ← mkMotiveType matchType expectedType;
+motive ← liftMetaM $ Meta.forallTelescopeReducing matchType fun xs matchType => Meta.mkLambda xs matchType;
+elimName ← mkAuxName `elim;
+elimResult ← mkElim elimName motiveType altLHSS.toList;
+-- TODO: report `eliminator errors`.
+let r := mkApp elimResult.elim motive;
+let r := mkAppN r discrs;
+let r := mkAppN r rhss;
+trace `Elab.match fun _ => "result: " ++ r;
+pure r
 
 /- Auxiliary method for `expandMatchDiscr?` -/
 private partial def mkMatchType (discrs : Array Syntax) : Nat → MacroM Syntax

tests/lean/match1.lean

@@ -0,0 +1,48 @@
+new_frontend
+
+#print "---- h1"
+
+def h1 (b : Bool) : Nat :=
+match b with
+| true  => 0
+| false => 10
+
+#eval h1 false
+
+#print "---- h2"
+
+def h2 (x : List Nat) : Nat :=
+match x with
+| [x1, x2] => x1 + x2
+| x::xs    => x
+| _        => 0
+
+#eval h2 [1, 2]
+#eval h2 [10, 4, 5]
+#eval h2 []
+
+#print "---- h3"
+
+def h3 (x : Array Nat) : Nat :=
+match x with
+| #[x]    => x
+| #[x, y] => x + y
+| xs      => xs.size
+
+#eval h3 #[10]
+#eval h3 #[10, 20]
+#eval h3 #[10, 20, 30, 40]
+
+#print "---- inv"
+
+inductive Image {α β : Type} (f : α → β) : β → Type
+| mk (a : α) : Image (f a)
+
+def mkImage {α β : Type} (f : α → β) (a : α) : Image f (f a) :=
+Image.mk a
+
+def inv {α β : Type} {f : α → β} {b : β} (t : Image f b) : α :=
+match b, t with
+| _, Image.mk a => a
+
+#eval inv (mkImage Nat.succ 10)

tests/lean/match1.lean.expected.out

@@ -0,0 +1,12 @@
+---- h1
+10
+---- h2
+3
+10
+0
+---- h3
+10
+30
+4
+---- inv
+10