1 files changed, 35 insertions, 26 deletions

diff --git a/src/Language/AST.hs b/src/Language/AST.hs
index 1c53c8a..f31f249 100644
--- a/src/Language/AST.hs
+++ b/src/Language/AST.hs
@@ -7,17 +7,23 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
 module Language.AST where
 
+import Data.Proxy
+import Data.Type.Equality
+import GHC.OverloadedLabels
+import GHC.TypeLits (symbolVal, KnownSymbol)
+
 import AST
 import Data
-import Data.Type.Equality
-import Language.Tag
 
 
 data SExpr t where
   -- lambda calculus
-  SEVar :: Tag t -> SExpr t
+  SEVar :: Var t -> SExpr t
   SELet :: SExpr a -> Lambda a (SExpr t) -> SExpr t
 
   -- base types
@@ -47,27 +53,24 @@ data SExpr t where
   SEError :: STy a -> String -> SExpr a
 deriving instance Show (SExpr t)
 
-data Lambda a b = Lambda (Tag a) b
+data Var a = Var (STy a) String
   deriving (Show)
 
-mkLambda :: KnownTy a => handle -> (SExpr a -> f t) -> Lambda a (f t)
-mkLambda handle f = mkLambda' handle knownTy f
+data Lambda a b = Lambda (Var a) b
+  deriving (Show)
 
-mkLambda' :: handle -> STy a -> (SExpr a -> f t) -> Lambda a (f t)
-mkLambda' handle ty f =
-  let tag = genTag handle ty
-  in Lambda tag (f (SEVar tag))
+mkLambda :: KnownTy a => String -> (SExpr a -> f t) -> Lambda a (f t)
+mkLambda name f = mkLambda' (Var knownTy name) f
+
+mkLambda' :: Var a -> (SExpr a -> f t) -> Lambda a (f t)
+mkLambda' var f = Lambda var (f (SEVar var))
 
 mkLambda2 :: (KnownTy a, KnownTy b)
-          => handle -> (SExpr a -> SExpr b -> f t) -> Lambda a (Lambda b (f t))
-mkLambda2 handle f = mkLambda2' handle knownTy knownTy f
+          => String -> String -> (SExpr a -> SExpr b -> f t) -> Lambda a (Lambda b (f t))
+mkLambda2 name1 name2 f = mkLambda2' (Var knownTy name1) (Var knownTy name2) f
 
-mkLambda2' :: handle -> STy a -> STy b -> (SExpr a -> SExpr b -> f t) -> Lambda a (Lambda b (f t))
-mkLambda2' handle ty1 ty2 f =
-  let tag2 = genTag handle ty2
-      lam2 = Lambda tag2 (f (SEVar tag1) (SEVar tag2))
-      tag1 = genTag lam2 ty1
-  in Lambda tag1 lam2
+mkLambda2' :: Var a -> Var b -> (SExpr a -> SExpr b -> f t) -> Lambda a (Lambda b (f t))
+mkLambda2' var1 var2 f = Lambda var1 (Lambda var2 (f (SEVar var1) (SEVar var2)))
 
 instance (t ~ TScal st, KnownScalTy st, Num (ScalRep st)) => Num (SExpr t) where
   a + b = SEOp (OAdd knownScalTy) (SEPair a b)
@@ -80,14 +83,20 @@ instance (t ~ TScal st, KnownScalTy st, Num (ScalRep st)) => Num (SExpr t) where
     in case scalRepIsShow ty of
          Dict -> SEConst ty . fromInteger
 
-data SFun args t = SFun (SList Tag args) (SExpr t)
+instance (KnownTy t, KnownSymbol name) => IsLabel name (Var t) where
+  fromLabel = Var knownTy (symbolVal (Proxy @name))
+
+instance (KnownTy t, KnownSymbol name) => IsLabel name (SExpr t) where
+  fromLabel = SEVar (fromLabel @name)
+
+data SFun args t = SFun (SList Var args) (SExpr t)
 
 scopeCheck :: SFun env t -> Ex env t
 scopeCheck (SFun args e) = scopeCheckExpr args e
 
-scopeCheckExpr :: forall env t. SList Tag env -> SExpr t -> Ex env t
+scopeCheckExpr :: forall env t. SList Var env -> SExpr t -> Ex env t
 scopeCheckExpr val = \case
-  SEVar tag@(Tag ty _)
+  SEVar tag@(Var ty _)
     | Just idx <- find tag val -> EVar ext ty idx
     | otherwise -> error "Variable out of scope in conversion from surface \
                          \expression to De Bruijn expression"
@@ -118,17 +127,17 @@ scopeCheckExpr val = \case
     go :: SExpr t' -> Ex env t'
     go = scopeCheckExpr val
 
-    find :: Tag t' -> SList Tag env' -> Maybe (Idx env' t')
+    find :: Var t' -> SList Var env' -> Maybe (Idx env' t')
     find _ SNil = Nothing
-    find tag@(Tag ty i) (Tag ty' i' `SCons` val')
-      | i == i'
+    find tag@(Var ty s) (Var ty' s' `SCons` val')
+      | s == s'
       , Just Refl <- testEquality ty ty'
       = Just IZ
       | otherwise
       = IS <$> find tag val'
 
-    lambda :: SList Tag env' -> Lambda a (SExpr b) -> Ex (a : env') b
+    lambda :: SList Var env' -> Lambda a (SExpr b) -> Ex (a : env') b
     lambda val' (Lambda tag e) = scopeCheckExpr (tag `SCons` val') e
 
-    lambda2 :: SList Tag env' -> Lambda a (Lambda b (SExpr c)) -> Ex (a : b : env') c
+    lambda2 :: SList Var env' -> Lambda a (Lambda b (SExpr c)) -> Ex (a : b : env') c
     lambda2 val' (Lambda tag (Lambda tag' e)) = scopeCheckExpr (tag `SCons` tag' `SCons` val') e