From dfa6b835b0636f3c54bb5e60b0942a2b05272f80 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Thu, 22 Aug 2024 14:11:43 -0700
Subject: [PATCH] dce

---
 README.md          |  4 +++-
 src/Lib/Syntax.idr | 13 -------------
 src/Lib/Types.idr  | 11 +++++++++++
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/README.md b/README.md
index 07e3229..6791eeb 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,7 @@
 
-Need eval for case.
+- Support primitives
+- Make DCon/TCon separate from Ref? (Or add flavor to VRef/Ref? If processing is often the same. I think I want arity though. I don't think a checked DCon can be overapplied, but it could be underapplied without special form. And special form is possibly difficult if not collecting a stack on the way down...
+
 
 Need to typecheck case - learning stuff like `n = S k` is not happening and the final bit of the data constructor doesn't unify with the data type, because we're not handling `Bnd n =?= Val`. Cockx collects a list of constraints.  We might want flags on unification to enable that?
 
diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr
index 15e6b77..9d4700f 100644
--- a/src/Lib/Syntax.idr
+++ b/src/Lib/Syntax.idr
@@ -27,9 +27,6 @@ data Pattern
 public export
 data RCaseAlt = MkAlt Raw Raw
 
--- FC = MkPair Int Int
-
-
 data Raw : Type where
   RVar : FC -> (nm : Name) -> Raw
   RLam : FC -> (nm : String) -> (icit : Icit) -> (ty : Raw) -> Raw
@@ -67,11 +64,6 @@ getFC (RParseError fc str) = fc
 public export
 data Decl : Type where
 
-Telescope: Type
-Telescope = List Decl -- pi-forall, always typeSig?
-
-data ConstrDef = MkCDef Name Telescope
-
 data Decl
   = TypeSig FC Name Raw
   | Def FC Name Raw
@@ -102,11 +94,6 @@ implementation Show Raw
 export
 implementation Show Decl
 
-covering
-Show ConstrDef where
-  show (MkCDef str xs) = foo ["MkCDef", show str, show xs]
-
-
 covering
 Show Decl where
   show (TypeSig _ str x) = foo ["TypeSig", show str, show x]
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index 5c29199..422ad56 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -41,6 +41,17 @@ Show BD where
   show Bound = "bnd"
   show Defined = "def"
 
+
+-- do we just admit string names for these and let the prim functions
+-- sort it out?
+-- I'd like Int / String to have syntax
+
+data PrimType = StringType | IntType
+
+data PrimVal : Type where
+  PrimString : String -> PrimVal
+  PrimInt : Int -> PrimVal
+
 public export
 data Tm : Type