diff options
Diffstat (limited to 'src/Language.hs')
| -rw-r--r-- | src/Language.hs | 32 |
1 files changed, 20 insertions, 12 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 |