Initial

1 files changed, 65 insertions, 0 deletions

diff --git a/AST.hs b/AST.hs
new file mode 100644
index 0000000..a456b8e
--- /dev/null
+++ b/AST.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeOperators #-}
+module AST where
+
+
+data Idx env t where
+    Z :: Idx (t ': env) t
+    S :: Idx env t -> Idx (t' ': env) t
+
+data STy t where
+    TInt :: STy Int
+    TFloat :: STy Float
+
+data V s env t =
+    V (s t) (Idx env t)
+
+data Tup s t where
+    T0 :: Tup s ()
+    T1 :: s t -> Tup s t
+    T2 :: Tup s t1 -> Tup s t2 -> Tup s (t1, t2)
+
+data LHS s t env env' where
+    L0 :: Tup s t -> LHS s t env env
+    L1 :: s t -> LHS s t env (t ': env)
+    L2 :: LHS s t1 env env1 -> LHS s t2 env1 env2 -> LHS s (t1, t2) env env2
+
+data PExpr expr env t where
+    Const :: STy t -> t -> PExpr expr env t
+    Pair :: expr env t1 -> expr env t2 -> PExpr expr env (t1, t2)
+    Nil :: PExpr expr env ()
+    Prim :: Oper (t -> t') -> expr env t -> PExpr expr env t'
+    Var :: V STy env t -> PExpr expr env t
+    Let :: LHS STy t env env' -> expr env t -> expr env' t' -> PExpr expr env t'
+
+newtype Expr env t = Expr (PExpr Expr env t)
+
+data Oper t where
+    Add :: STy t -> Oper ((t, t) -> t)
+    Mul :: STy t -> Oper ((t, t) -> t)
+    Round :: Oper (Float -> Int)
+
+data PVal tenv env where  -- partial valuation
+    VZ :: PVal tenv tenv
+    VS :: PVal tenv env -> t -> PVal tenv (t ': env)
+
+type Val = PVal '[]
+
+data PTVal f tenv env where  -- partial tagged valuation
+    TVZ :: PTVal f tenv tenv
+    TVS :: PTVal f tenv env -> f t -> PTVal f tenv (t ': env)
+
+type TVal f = PTVal f '[]
+
+data NumDict t where
+    NumDict :: Num t => NumDict t
+
+data Exists f where
+    Exists :: f t -> Exists f
+
+data env :> env' =
+    Weaken { (>:>) :: forall t. Idx env t -> Idx env' t }