From 058633c6c9cbea383f98d3505f422dd586d1a11c Mon Sep 17 00:00:00 2001
From: Victor Taelin <victor.taelin@gmail.com>
Date: Fri, 24 May 2024 23:40:13 -0300
Subject: [PATCH] desugar match with implicit args

---
 book/Equal/apply.kind2 | 10 ++++++----
 book/Equal/match.kind2 |  6 ++++++
 src/sugar/mod.rs       | 21 ++++++++++++---------
 3 files changed, 24 insertions(+), 13 deletions(-)
 create mode 100644 book/Equal/match.kind2

diff --git a/book/Equal/apply.kind2 b/book/Equal/apply.kind2
index a292e6cf..1131f27e 100644
--- a/book/Equal/apply.kind2
+++ b/book/Equal/apply.kind2
@@ -1,10 +1,12 @@
-//use Equal/{refl}
-
 apply <A: *> <B: *> <a: A> <b: B> (f: A -> B) (e: (Equal A a b)) : (Equal B (f a) (f b)) =
   match e {
-    Equal/refl: {=}
-  }
+    Equal/refl: ~λPλrefl(refl (f e.a))
+  }: (Equal B (f a) (f b))
 
+  //(Equal/match
+    //λaλbλe(Equal B (f a) (f b))
+    //λx ~λPλrefl(refl (f x))
+    //e)
 
 //Equal.apply
 //: ∀(A: *)
diff --git a/book/Equal/match.kind2 b/book/Equal/match.kind2
new file mode 100644
index 00000000..565cc699
--- /dev/null
+++ b/book/Equal/match.kind2
@@ -0,0 +1,6 @@
+match <T: *> <a: T> <b: T> 
+  (P: ∀(a:T) ∀(b:T) ∀(e: (Equal T a b)) *)
+  (refl: ∀(x: T) (P x x (Equal/refl/ T x)))
+  (e: (Equal T a b))
+: (P a b e) =
+  (~e P refl)
diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs
index 30b639c2..1e44f22c 100644
--- a/src/sugar/mod.rs
+++ b/src/sugar/mod.rs
@@ -919,17 +919,17 @@ impl Term {
       }
     }
 
-    // 3. Create `(Type/fold|match <param_holes> <motive>)`
+    // 3. Create `(Type/fold|match <motive>)`
     term = Term::Var {
-      nam: format!("{}/{}/", adt.name, if mat.fold { "fold" } else { "match" })
+      nam: format!("{}/{}", adt.name, if mat.fold { "fold" } else { "match" })
     };
-    for _par in &adt.pars {
-      term = Term::App {
-        era: true,
-        fun: Box::new(term),
-        arg: Box::new(Term::Met {}),
-      };
-    }
+    //for _par in &adt.pars {
+      //term = Term::App {
+        //era: true,
+        //fun: Box::new(term),
+        //arg: Box::new(Term::Met {}),
+      //};
+    //}
     term = Term::App {
       era: true,
       fun: Box::new(term),
@@ -995,6 +995,9 @@ impl Term {
       bod: Box::new(term)
     };
 
+    // Debug: Prints the generated term
+    //println!("{}", term.format().flatten(Some(800)));
+
     // 10. Return 'term'
     return term;
   }