1 files changed, 59 insertions, 62 deletions
diff --git a/src/Language.hs b/src/Language.hs
index f4719bf..58a7070 100644
--- a/src/Language.hs
+++ b/src/Language.hs
@@ -1,10 +1,11 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE TypeOperators #-}
 module Language (
-  scopeCheck,
-  SExpr,
+  fromNamed,
+  NExpr,
   module Language,
+  Lookup,
 ) where
 
 import AST
@@ -12,101 +13,97 @@ import Data
 import Language.AST
 
 
-lambda :: forall a args t. KnownTy a => Var a -> SFun args t -> SFun (Append args '[a]) t
-lambda var (SFun args e) = SFun (sappend args (var `SCons` SNil)) e
-
-body :: SExpr t -> SFun '[] t
-body e = SFun SNil e
-
-
 data a :-> b = a :-> b
   deriving (Show)
-infix 0 :->
+infixr 0 :->
+
+
+body :: NExpr env t -> NFun env env t
+body = NBody
 
+lambda :: Var name a -> NFun ('(name, a) : env) env' t -> NFun env env' t
+lambda = NLam
 
-TODO
--- TODO: should give SExpr an environment index of kind '[(Symbol, Ty)]. Then
--- the IsLabel instance for SExpr (but not the one for Var!) can check that the
--- type in the named environment matches the locally expected type.
 
-let_ :: KnownTy a => Var a -> SExpr a -> SExpr t -> SExpr t
-let_ var rhs e = SELet rhs (Lambda var e)
+let_ :: Var name a -> NExpr env a -> NExpr ('(name, a) : env) t -> NExpr env t
+let_ = NELet
 
-pair :: SExpr a -> SExpr b -> SExpr (TPair a b)
-pair = SEPair
+pair :: NExpr env a -> NExpr env b -> NExpr env (TPair a b)
+pair = NEPair
 
-fst_ :: SExpr (TPair a b) -> SExpr a
-fst_ = SEFst
+fst_ :: NExpr env (TPair a b) -> NExpr env a
+fst_ = NEFst
 
-snd_ :: SExpr (TPair a b) -> SExpr b
-snd_ = SESnd
+snd_ :: NExpr env (TPair a b) -> NExpr env b
+snd_ = NESnd
 
-nil :: SExpr TNil
-nil = SENil
+nil :: NExpr env TNil
+nil = NENil
 
-inl :: STy b -> SExpr a -> SExpr (TEither a b)
-inl = SEInl
+inl :: STy b -> NExpr env a -> NExpr env (TEither a b)
+inl = NEInl
 
-inr :: STy a -> SExpr b -> SExpr (TEither a b)
-inr = SEInr
+inr :: STy a -> NExpr env b -> NExpr env (TEither a b)
+inr = NEInr
 
-case_ :: (KnownTy a, KnownTy b)
-      => SExpr (TEither a b) -> (Var a :-> SExpr c) -> (Var b :-> SExpr c) -> SExpr c
-case_ e (v1 :-> e1) (v2 :-> e2) = SECase e (Lambda v1 e1) (Lambda v2 e2)
+case_ :: NExpr env (TEither a b) -> (Var name1 a :-> NExpr ('(name1, a) : env) c) -> (Var name2 b :-> NExpr ('(name2, b) : env) c) -> NExpr env c
+case_ e (v1 :-> e1) (v2 :-> e2) = NECase e v1 e1 v2 e2
 
-build1 :: SExpr TIx -> (Var TIx :-> SExpr t) -> SExpr (TArr (S Z) t)
-build1 a (v :-> b) = SEBuild1 a (Lambda v b)
+build1 :: NExpr env TIx -> (Var name TIx :-> NExpr ('(name, TIx) : env) t) -> NExpr env (TArr (S Z) t)
+build1 a (v :-> b) = NEBuild1 a v b
 
-build :: SNat n -> SExpr (Tup (Replicate n TIx)) -> (Var (Tup (Replicate n TIx)) :-> SExpr t) -> SExpr (TArr n t)
-build n a (v :-> b) = SEBuild n a (Lambda v b)
+build :: SNat n -> NExpr env (Tup (Replicate n TIx)) -> (Var name (Tup (Replicate n TIx)) :-> NExpr ('(name, Tup (Replicate n TIx)) : env) t) -> NExpr env (TArr n t)
+build n a (v :-> b) = NEBuild n a v b
 
-fold1 :: KnownTy t => (SExpr t -> SExpr t -> SExpr t) -> SExpr (TArr (S n) t) -> SExpr (TArr n t)
-fold1 f e = SEFold1 (mkLambda2 (f, e) f) e
+fold1 :: (Var name1 t :-> Var name2 t :-> NExpr ('(name2, t) : '(name1, t) : env) t) -> NExpr env (TArr (S n) t) -> NExpr env (TArr n t)
+fold1 (v1 :-> v2 :-> e1) e2 = NEFold1 v1 v2 e1 e2
 
-unit :: SExpr t -> SExpr (TArr Z t)
-unit = SEUnit
+unit :: NExpr env t -> NExpr env (TArr Z t)
+unit = NEUnit
 
-const_ :: KnownScalTy t => ScalRep t -> SExpr (TScal t)
+const_ :: KnownScalTy t => ScalRep t -> NExpr env (TScal t)
 const_ x =
   let ty = knownScalTy
   in case scalRepIsShow ty of
-       Dict -> SEConst ty x
+       Dict -> NEConst ty x
 
-idx0 :: SExpr (TArr Z t) -> SExpr t
-idx0 = SEIdx0
+idx0 :: NExpr env (TArr Z t) -> NExpr env t
+idx0 = NEIdx0
 
-(.!) :: SExpr (TArr (S n) t) -> SExpr TIx -> SExpr (TArr n t)
-(.!) = SEIdx1
+(.!) :: NExpr env (TArr (S n) t) -> NExpr env TIx -> NExpr env (TArr n t)
+(.!) = NEIdx1
 
-(!) :: SNat n -> SExpr (TArr n t) -> SExpr (Tup (Replicate n TIx)) -> SExpr t
-(!) = SEIdx
+(!) :: SNat n -> NExpr env (TArr n t) -> NExpr env (Tup (Replicate n TIx)) -> NExpr env t
+(!) = NEIdx
 
-shape :: SExpr (TArr n t) -> SExpr (Tup (Replicate n TIx))
-shape = SEShape
+shape :: NExpr env (TArr n t) -> NExpr env (Tup (Replicate n TIx))
+shape = NEShape
 
-oper :: SOp a t -> SExpr a -> SExpr t
-oper = SEOp
+oper :: SOp a t -> NExpr env a -> NExpr env t
+oper = NEOp
 
-error_ :: KnownTy t => String -> SExpr t
-error_ s = SEError knownTy s
+error_ :: KnownTy t => String -> NExpr env t
+error_ s = NEError knownTy s
 
-(.==) :: KnownScalTy st => SExpr (TScal st) -> SExpr (TScal st) -> SExpr (TScal TBool)
+(.==) :: KnownScalTy st => NExpr env (TScal st) -> NExpr env (TScal st) -> NExpr env (TScal TBool)
 a .== b = oper (OEq knownScalTy) (pair a b)
 
-(.<) :: KnownScalTy st => SExpr (TScal st) -> SExpr (TScal st) -> SExpr (TScal TBool)
+(.<) :: KnownScalTy st => NExpr env (TScal st) -> NExpr env (TScal st) -> NExpr env (TScal TBool)
 a .< b = oper (OLt knownScalTy) (pair a b)
 
-(.>) :: KnownScalTy st => SExpr (TScal st) -> SExpr (TScal st) -> SExpr (TScal TBool)
+(.>) :: KnownScalTy st => NExpr env (TScal st) -> NExpr env (TScal st) -> NExpr env (TScal TBool)
 (.>) = flip (.<)
 
-(.<=) :: KnownScalTy st => SExpr (TScal st) -> SExpr (TScal st) -> SExpr (TScal TBool)
+(.<=) :: KnownScalTy st => NExpr env (TScal st) -> NExpr env (TScal st) -> NExpr env (TScal TBool)
 a .<= b = oper (OLe knownScalTy) (pair a b)
 
-(.>=) :: KnownScalTy st => SExpr (TScal st) -> SExpr (TScal st) -> SExpr (TScal TBool)
+(.>=) :: KnownScalTy st => NExpr env (TScal st) -> NExpr env (TScal st) -> NExpr env (TScal TBool)
 (.>=) = flip (.<=)
 
-not_ :: SExpr (TScal TBool) -> SExpr (TScal TBool)
+not_ :: NExpr env (TScal TBool) -> NExpr env (TScal TBool)
 not_ = oper ONot
 
-if_ :: SExpr (TScal TBool) -> SExpr t -> SExpr t -> SExpr t
-if_ e a b = case_ (oper OIf e) (\_ -> a) (\_ -> b)
+-- | The "_" variables in scope are unusable and should be ignored. With a
+-- weakening function on NExprs they could be hidden.
+if_ :: NExpr env (TScal TBool) -> NExpr ('("_", TNil) : env) t -> NExpr ('("_", TNil) : env) t -> NExpr env t
+if_ e a b = case_ (oper OIf e) (#_ :-> a) (#_ :-> b)