From 3cba2993e294f2470a3939278baf7ca5d63e3715 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Thu, 29 Aug 2024 21:59:54 -0700
Subject: [PATCH] casetree prep

---
 newt/Fix.newt      |  6 ++++--
 src/Lib/Syntax.idr |  7 ++++---
 src/Lib/Types.idr  | 10 ++++++++++
 3 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/newt/Fix.newt b/newt/Fix.newt
index b3ed612..6612c3f 100644
--- a/newt/Fix.newt
+++ b/newt/Fix.newt
@@ -18,15 +18,17 @@ data D : (A : Type) -> Type where
 
 unV : { A : U} -> D A -> A
 unV = \ v => case v of
-  V y => ?  -- y
+  V y => y
  --  F f => TRUSTME
 
+
+
 -- And here we have D A:4 and D A:1
 unF : {A : Type} -> D A -> D A -> D A
 unF = \ {A} v x =>
   case v of
     F {A} f => ? -- f x
-    -- V y => TRUSTME
+    V y => TRUSTME
 
 -- fix : {A : U} -> (A -> A) -> A
 -- fix = \ {A} g =>
diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr
index 050615c..1153ac9 100644
--- a/src/Lib/Syntax.idr
+++ b/src/Lib/Syntax.idr
@@ -15,9 +15,9 @@ data RigCount = Rig0 | RigW
 public export
 data Pattern
   = PatVar Name
-  | PatCon Name (List (Pattern, RigCount))
+  | PatCon Name (List Pattern)
   | PatWild
-  | PatLit Literal
+  -- | PatLit Literal
 
 -- %runElab deriveShow `{Pattern}
 
@@ -112,11 +112,12 @@ Show RigCount where
   show Rig0 = "Rig0"
   show RigW = "RigW"
 
+export
 Show Pattern where
   show (PatVar str) = foo ["PatVar", show str]
   show (PatCon str xs) = foo ["PatCon", show str, assert_total $ show xs]
   show PatWild = "PatWild"
-  show (PatLit x) = foo ["PatLit" , show x]
+  -- show (PatLit x) = foo ["PatLit" , show x]
 
 covering
 Show RCaseAlt where
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index 26741e9..4173f91 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -212,6 +212,16 @@ data Val : Type where
   VU : FC -> Val
   VLit : FC -> Literal -> Val
 
+public export
+getValFC : Val -> FC
+getValFC (VVar fc _ _) = fc
+getValFC (VRef fc _ _ _) = fc
+getValFC (VCase fc _ _) = fc
+getValFC (VMeta fc _ _) = fc
+getValFC (VLam fc _ _) = fc
+getValFC (VPi fc _ _ a b) = fc
+getValFC (VU fc) = fc
+getValFC (VLit fc _) = fc
 
 
 Show Closure