From ada719349288bed1d067fd21538ee7e5b401871f Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 15 Nov 2023 11:46:15 +0000 Subject: [PATCH 1/4] Attempt to fix #21 --- Qq/Match.lean | 31 +++++++++---------------------- examples/matching.lean | 25 +++++++++++++++++++++++++ 2 files changed, 34 insertions(+), 22 deletions(-) diff --git a/Qq/Match.lean b/Qq/Match.lean index 8ae3267..46ad838 100644 --- a/Qq/Match.lean +++ b/Qq/Match.lean @@ -246,17 +246,6 @@ partial def isIrrefutablePattern : Term → Bool | `(true) => false | `(false) => false -- TODO properly | stx => stx.1.isIdent -scoped elab "_comefrom" n:ident "do" b:doSeq " in " body:term : term <= expectedType => do - let _ ← extractBind expectedType - (← elabTerm (← `(?m)).1.stripPos none).mvarId!.assign expectedType - elabTerm (← `(have $n:ident : ?m := (do $b:doSeq); $body)) expectedType - -scoped syntax "_comefrom" ident "do" doSeq : term -macro_rules | `(assert! (_comefrom $n do $b); $body) => `(_comefrom $n do $b in $body) - -scoped macro "comefrom" n:ident "do" b:doSeq : doElem => - `(doElem| assert! (_comefrom $n do $b)) - def mkLetDoSeqItem [Monad m] [MonadQuotation m] (pat : Term) (rhs : TSyntax `doElem) (alt : TSyntax ``doSeq) : m (List (TSyntax ``doSeqItem)) := do match pat with | `(_) => return [] @@ -356,11 +345,8 @@ macro_rules `(doElem| do $(lifts.push t):doSeqItem*) | _ => - let (pat', auxs) ← floatQMatch (← `(doSeq| alt)) pat [] - let items := - #[← `(doSeqItem| comefrom alt do $alt:doSeq)] ++ - (← mkLetDoSeqItem pat' rhs alt) ++ - auxs + let (pat', auxs) ← floatQMatch (← `(doSeq| $alt)) pat [] + let items := Array.mk <| (← mkLetDoSeqItem pat' rhs alt) ++ auxs `(doElem| do $items:doSeqItem*) | `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do @@ -373,14 +359,15 @@ macro_rules pure (← `(x), ← `(doSeqItem| let x := $d:term)) let mut items := discrs.map (·.2) let discrs := discrs.map (·.1) - items := items.push (← `(doSeqItem| comefrom alt do throwError "nonexhaustive match")) + let mut alt : TSyntax `doElem ← `(doElem| throwError "nonexhaustive match") for pats in patss.reverse, rhs in rhss.reverse do let mut subItems : Array (TSyntax ``doSeqItem) := #[] for discr in discrs, pat in pats do - subItems := subItems ++ (← mkLetDoSeqItem pat (← `(doElem| pure $discr:term)) (← `(doSeq| alt))) - subItems := subItems.push (← `(doSeqItem| do $rhs)) - items := items.push (← `(doSeqItem| comefrom alt do $subItems:doSeqItem*)) - items := items.push (← `(doSeqItem| alt)) - `(doElem| (do $items:doSeqItem*)) + subItems := + subItems ++ (← mkLetDoSeqItem pat (← `(doElem| pure $discr:term)) (←`(doSeq|$alt:doElem))) + subItems := subItems.push (←`(doSeqItem|do $rhs)) + alt ← `(doElem| do $subItems:doSeqItem*) + items := items.push (←`(doSeqItem|$alt:doElem)) + `(doElem| do $items:doSeqItem*) end diff --git a/examples/matching.lean b/examples/matching.lean index e05d754..0a2b767 100644 --- a/examples/matching.lean +++ b/examples/matching.lean @@ -27,6 +27,7 @@ abbrev square (a : Nat) := #eval summands q(inferInstance) q(k + square (square k)) #eval summands q(⟨(· * ·)⟩) q(k * square (square k)) +set_option pp.macroStack true in def matchProd (e : Nat × Q(Nat)) : MetaM Bool := do let (2, ~q(1)) := e | return false return true @@ -51,3 +52,27 @@ def getNatAdd (e : Expr) : MetaM (Option (Q(Nat) × Q(Nat))) := do #eval do guard <| (← getNatAdd q(1 + 2)) == some (q(1), q(2)) #eval do guard <| (← getNatAdd q((1 + 2 : Int))) == none + + + +section test_return + +def foo1 (T : Q(Type)) : MetaM Nat := do + let x : Nat ← match T with + | ~q(Prop) => return (2 : Nat) + | _ => pure (1 : Nat) + pure (3 + x) + +#eval do guard <| (←foo1 q(Prop)) == 2 +#eval do guard <| (←foo1 q(Nat)) == 3 + 1 + +def foo2 (T : Q(Type)) : MetaM Nat := do + let x : Nat ← match T with + | ~q(Prop) => pure (2 : Nat) + | _ => return (1 : Nat) + pure (3 + x) + +#eval do guard <| (←foo2 q(Prop)) == 3 + 2 +#eval do guard <| (←foo2 q(Nat)) == 1 + +end test_return From c8e607a810a07fd7669c5c0e080ddfe9b1600369 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 15 Nov 2023 11:59:41 +0000 Subject: [PATCH 2/4] add more testcases --- examples/matching.lean | 55 ++++++++++++++++++++++++++++++++++++------ examples/tyoe.lean | 53 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 101 insertions(+), 7 deletions(-) create mode 100644 examples/tyoe.lean diff --git a/examples/matching.lean b/examples/matching.lean index 0a2b767..794ab8b 100644 --- a/examples/matching.lean +++ b/examples/matching.lean @@ -54,25 +54,66 @@ def getNatAdd (e : Expr) : MetaM (Option (Q(Nat) × Q(Nat))) := do #eval do guard <| (← getNatAdd q((1 + 2 : Int))) == none - +-- tests for gh-21 section test_return -def foo1 (T : Q(Type)) : MetaM Nat := do +def foo_let1 (T : Q(Type)) : MetaM Nat := do + let x ← do + let ~q(Prop) := T | pure (1 : Nat) + return (2 : Nat) + pure (3 + x) + +#eval do guard <| (←foo_let1 q(Prop)) == 2 +#eval do guard <| (←foo_let1 q(Nat)) == 3 + 1 + +def foo_let2 (T : Q(Type)) : MetaM Nat := do + let x ← do + let ~q(Prop) := T | return (1 : Nat) + pure (2 : Nat) + pure (3 + x) + +#eval do guard <| (←foo_let2 q(Prop)) == 3 + 2 +#eval do guard <| (←foo_let2 q(Nat)) == 1 + + +def foo_match1 (T : Q(Type)) : MetaM Nat := do let x : Nat ← match T with | ~q(Prop) => return (2 : Nat) | _ => pure (1 : Nat) pure (3 + x) -#eval do guard <| (←foo1 q(Prop)) == 2 -#eval do guard <| (←foo1 q(Nat)) == 3 + 1 +#eval do guard <| (←foo_match1 q(Prop)) == 2 +#eval do guard <| (←foo_match1 q(Nat)) == 3 + 1 -def foo2 (T : Q(Type)) : MetaM Nat := do +def foo_match2 (T : Q(Type)) : MetaM Nat := do let x : Nat ← match T with | ~q(Prop) => pure (2 : Nat) | _ => return (1 : Nat) pure (3 + x) -#eval do guard <| (←foo2 q(Prop)) == 3 + 2 -#eval do guard <| (←foo2 q(Nat)) == 1 +#eval do guard <| (←foo_match2 q(Prop)) == 3 + 2 +#eval do guard <| (←foo_match2 q(Nat)) == 1 + +def foo_if_let1 (T : Q(Type)) : MetaM Nat := do + let x : Nat ← + if let ~q(Prop) := T then + return (2 : Nat) + else + pure (1 : Nat) + pure (3 + x) + +#eval do guard <| (←foo_if_let1 q(Prop)) == 2 +#eval do guard <| (←foo_if_let1 q(Nat)) == 3 + 1 + +def foo_if_let2 (T : Q(Type)) : MetaM Nat := do + let x : Nat ← + if let ~q(Prop) := T then + pure (2 : Nat) + else + return (1 : Nat) + pure (3 + x) + +#eval do guard <| (←foo_if_let2 q(Prop)) == 3 + 2 +#eval do guard <| (←foo_if_let2 q(Nat)) == 1 end test_return diff --git a/examples/tyoe.lean b/examples/tyoe.lean new file mode 100644 index 0000000..b85af43 --- /dev/null +++ b/examples/tyoe.lean @@ -0,0 +1,53 @@ + +import Lean +import Qq + +open Lean Meta +open Qq + +set_option pp.macroStack true in +def foo₁ (T : Q(Type)) : MetaM Bool := do + if let ~q(Prop) := T then + let x := Nat.zero.succ + return (Nat.zero, ()).2 + return true + + +set_option pp.macroStack true in +set_option pp.rawOnError true in +def foo₂ (T : Q(Type)) : MetaM Bool := do + let x : Unit ← match T with + | ~q(Prop) => return true || true + | ~q(Nat) => return true == true + | _ => return true && true + pure false + +#eval show MetaM Unit from do + let x := + pure () + pure Nat.zero + pure () + + +#eval foo₂ q(Prop) +#eval foo₂ q(Int) + + +#print foo₁ +#print foo₂ + + +set_option pp.macroStack true in +def afoo₁ (T : Q(Type)) : MetaM Bool := do + if let some (x : Nat) := none then + return false + return true + + +set_option pp.macroStack true in +def afoo₂ (T : Q(Type)) : MetaM Bool := do + let some (x : Nat) := none | return true + return false + +#print afoo₁ +#print afoo₂ From 17ab35ddedb6f441fdad4732c78cd2accf60ed1e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 15 Nov 2023 12:03:31 +0000 Subject: [PATCH 3/4] cleanup --- examples/tyoe.lean | 53 ---------------------------------------------- 1 file changed, 53 deletions(-) delete mode 100644 examples/tyoe.lean diff --git a/examples/tyoe.lean b/examples/tyoe.lean deleted file mode 100644 index b85af43..0000000 --- a/examples/tyoe.lean +++ /dev/null @@ -1,53 +0,0 @@ - -import Lean -import Qq - -open Lean Meta -open Qq - -set_option pp.macroStack true in -def foo₁ (T : Q(Type)) : MetaM Bool := do - if let ~q(Prop) := T then - let x := Nat.zero.succ - return (Nat.zero, ()).2 - return true - - -set_option pp.macroStack true in -set_option pp.rawOnError true in -def foo₂ (T : Q(Type)) : MetaM Bool := do - let x : Unit ← match T with - | ~q(Prop) => return true || true - | ~q(Nat) => return true == true - | _ => return true && true - pure false - -#eval show MetaM Unit from do - let x := - pure () - pure Nat.zero - pure () - - -#eval foo₂ q(Prop) -#eval foo₂ q(Int) - - -#print foo₁ -#print foo₂ - - -set_option pp.macroStack true in -def afoo₁ (T : Q(Type)) : MetaM Bool := do - if let some (x : Nat) := none then - return false - return true - - -set_option pp.macroStack true in -def afoo₂ (T : Q(Type)) : MetaM Bool := do - let some (x : Nat) := none | return true - return false - -#print afoo₁ -#print afoo₂ From 008fb1785aef314947823aefb1ef9ce978bd4ce7 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 5 Feb 2024 16:55:27 +0000 Subject: [PATCH 4/4] whitespace --- Qq/Match.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Qq/Match.lean b/Qq/Match.lean index 995540f..bbdf17d 100644 --- a/Qq/Match.lean +++ b/Qq/Match.lean @@ -353,10 +353,10 @@ macro_rules let mut subItems : Array (TSyntax ``doSeqItem) := #[] for discr in discrs, pat in pats do subItems := - subItems ++ (← mkLetDoSeqItem pat discr (←`(doSeq|$alt:doElem))) - subItems := subItems.push (←`(doSeqItem|do $rhs)) + subItems ++ (← mkLetDoSeqItem pat discr (← `(doSeq|$alt:doElem))) + subItems := subItems.push (← `(doSeqItem| do $rhs)) alt ← `(doElem| do $subItems:doSeqItem*) - items := items.push (←`(doSeqItem|$alt:doElem)) + items := items.push (← `(doSeqItem|$alt:doElem)) `(doElem| do $items:doSeqItem*) end