dce

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?
 

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]

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