From 5d1d3b4f251bf938648d7d21c6641a1a0cc0768b Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom.smeding@gmail.com>
Date: Sat, 26 Dec 2020 18:08:15 +0100
Subject: Initial

---
 Language.hs | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 Language.hs

(limited to 'Language.hs')

diff --git a/Language.hs b/Language.hs
new file mode 100644
index 0000000..7251161
--- /dev/null
+++ b/Language.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+module Language where
+
+import AST
+import ASTfunc
+
+
+class    IsSTy t     where magicSTy :: STy t
+instance IsSTy Int   where magicSTy = TInt
+instance IsSTy Float where magicSTy = TFloat
+
+class    IsTupTy t     where magicTupTy :: Tup STy t
+-- Need to list all the scalar types to avoid overlapping instances
+instance IsTupTy Int   where magicTupTy = T1 TInt
+instance IsTupTy Float where magicTupTy = T1 TFloat
+instance IsTupTy ()    where magicTupTy = T0
+instance (IsTupTy t1, IsTupTy t2) => IsTupTy (t1, t2) where
+    magicTupTy = T2 magicTupTy magicTupTy
+
+con :: IsSTy t => t -> Expr env t
+con = Expr . Const magicSTy
+
+pair :: Expr env t1 -> Expr env t2 -> Expr env (t1, t2)
+pair = (Expr .) . Pair
+
+nil :: Expr env ()
+nil = Expr Nil
+
+add :: IsSTy t => Expr env t -> Expr env t -> Expr env t
+add = ((Expr . Prim (Add magicSTy) . Expr) .) . Pair
+
+mul :: IsSTy t => Expr env t -> Expr env t -> Expr env t
+mul = ((Expr . Prim (Mul magicSTy) . Expr) .) . Pair
+
+let_ :: IsTupTy t
+     => Expr env t
+     -> (forall env'. (forall t2. Expr env t2 -> Expr env' t2)
+                   -> Expr env' t -> Expr env' t')
+     -> Expr env t'
+let_ rhs f
+  | LetBound lhs vs <- lhsCopy magicTupTy
+  = Expr (Let lhs rhs (f (weakenExpr (weakenWithLHS lhs)) (evars vs)))
+
+fst_ :: Expr env (t, t') -> Expr env t
+fst_ (Expr (Pair e1 _)) = e1
+fst_ _ = error "fst_: explicit let-binding necessary"
+
+snd_ :: Expr env (t, t') -> Expr env t'
+snd_ (Expr (Pair _ e2)) = e2
+snd_ _ = error "snd_: explicit let-binding necessary"
-- 
cgit v1.2.3-70-g09d2