summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Language.hs32
-rw-r--r--src/Language/AST.hs61
2 files changed, 55 insertions, 38 deletions
diff --git a/src/Language.hs b/src/Language.hs
index b76e07f..f4719bf 100644
--- a/src/Language.hs
+++ b/src/Language.hs
@@ -12,17 +12,25 @@ import Data
import Language.AST
-lambda :: forall a args t. KnownTy a => (SExpr a -> SFun args t) -> SFun (Append args '[a]) t
-lambda f = case mkLambda f f of
- Lambda tag (SFun args e) ->
- SFun (sappend args (tag `SCons` SNil)) e
+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
-let_ :: KnownTy a => SExpr a -> (SExpr a -> SExpr t) -> SExpr t
-let_ rhs f = SELet rhs (mkLambda (rhs, f) f)
+data a :-> b = a :-> b
+ deriving (Show)
+infix 0 :->
+
+
+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)
pair :: SExpr a -> SExpr b -> SExpr (TPair a b)
pair = SEPair
@@ -43,14 +51,14 @@ inr :: STy a -> SExpr b -> SExpr (TEither a b)
inr = SEInr
case_ :: (KnownTy a, KnownTy b)
- => SExpr (TEither a b) -> (SExpr a -> SExpr c) -> (SExpr b -> SExpr c) -> SExpr c
-case_ e f g = SECase e (mkLambda (e, f) f) (mkLambda (e, g) g)
+ => 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)
-build1 :: SExpr TIx -> (SExpr TIx -> SExpr t) -> SExpr (TArr (S Z) t)
-build1 e f = SEBuild1 e (mkLambda (e, f) f)
+build1 :: SExpr TIx -> (Var TIx :-> SExpr t) -> SExpr (TArr (S Z) t)
+build1 a (v :-> b) = SEBuild1 a (Lambda v b)
-build :: SNat n -> SExpr (Tup (Replicate n TIx)) -> (SExpr (Tup (Replicate n TIx)) -> SExpr t) -> SExpr (TArr n t)
-build n e f = SEBuild n e (mkLambda' (e, f) (tTup (sreplicate n tIx)) f)
+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)
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
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
generated by cgit v1.2.3-70-g09d2 (git 2.48.1) at 2025-03-31 23:27:01 +0200