blob: a456b8eaa5684ca65566d32731e6ee68faee2e9f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
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 }
|
