casetree prep

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 =>

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

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