diff options
Diffstat (limited to 'ASTfunc.hs')
-rw-r--r-- | ASTfunc.hs | 148 |
1 files changed, 148 insertions, 0 deletions
diff --git a/ASTfunc.hs b/ASTfunc.hs new file mode 100644 index 0000000..59fddbb --- /dev/null +++ b/ASTfunc.hs @@ -0,0 +1,148 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +module ASTfunc where + +import AST + + +idxToInt :: Idx env t -> Int +idxToInt Z = 0 +idxToInt (S i) = succ (idxToInt i) + +data LetBound s env t t' = + forall env'. LetBound (LHS s t env env') (Tup (V s env') t) + +lhsCopy :: Tup s t -> LetBound s env t t +lhsCopy T0 = LetBound (L0 T0) T0 +lhsCopy (T1 t) = LetBound (L1 t) (T1 (V t Z)) +lhsCopy (T2 t1 t2) + | LetBound l1 vs1 <- lhsCopy t1 + , LetBound l2 vs2 <- lhsCopy t2 + = LetBound (L2 l1 l2) (T2 (fmapTup (weakenVar (weakenWithLHS l2)) vs1) vs2) + +lhstypeOf :: LHS s t env env' -> Tup s t +lhstypeOf (L0 t) = t +lhstypeOf (L1 t) = T1 t +lhstypeOf (L2 l1 l2) = T2 (lhstypeOf l1) (lhstypeOf l2) + +rebuildLHS :: LHS s t env env' -> Exists (LHS s t env1) +rebuildLHS (L0 t) = Exists (L0 t) +rebuildLHS (L1 t) = Exists (L1 t) +rebuildLHS (L2 l1 l2) + | Exists l1' <- rebuildLHS l1 + , Exists l2' <- rebuildLHS l2 + = Exists (L2 l1' l2') + +fmapTup :: (forall t'. s t' -> s' t') -> Tup s t -> Tup s' t +fmapTup _ T0 = T0 +fmapTup f (T1 x) = T1 (f x) +fmapTup f (T2 t1 t2) = T2 (fmapTup f t1) (fmapTup f t2) + +prj :: PVal tenv env -> Idx env t -> Maybe t +prj VZ _ = Nothing +prj (VS _ x) Z = Just x +prj (VS v _) (S i) = prj v i + +prjV :: Val env -> Idx env t -> t +prjV v Z = case v of VS _ x -> x +prjV v (S i) = case v of VS v' _ -> prjV v' i + +vpush :: LHS s t env env' -> t -> Val env -> Val env' +vpush (L0 _) _ v = v +vpush (L1 _) x v = VS v x +vpush (L2 l1 l2) (x, y) v = vpush l2 y (vpush l1 x v) + +reifyNum :: STy t -> NumDict t +reifyNum TInt = NumDict +reifyNum TFloat = NumDict + +(>.) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3 +Weaken f >. Weaken g = Weaken (f . g) + +weakenId :: env :> env +weakenId = Weaken id + +weakenSucc :: env :> (t ': env) +weakenSucc = Weaken S + +weakenSucc' :: (t ': env) :> env +weakenSucc' = Weaken (\case S i -> i + Z -> error "weakenSucc': reference to skipped item") + +weakenWithLHS :: LHS s t env env' -> env :> env' +weakenWithLHS (L0 _) = Weaken id +weakenWithLHS (L1 _) = Weaken S +weakenWithLHS (L2 l1 l2) = weakenWithLHS l2 >. weakenWithLHS l1 + +weakenSkip :: LHS s t env env' -> env :> env2 -> env' :> env2 +weakenSkip (L0 _) = id +weakenSkip (L1 _) = (>. weakenSucc') +weakenSkip (L2 l1 l2) = weakenSkip l2 . weakenSkip l1 + +weakenVar :: env :> env' -> V s env t -> V s env' t +weakenVar w (V t i) = V t (w >:> i) + +weakenExpr :: env :> env' -> Expr env t -> Expr env' t +weakenExpr w (Expr e) = Expr (weakenPExpr weakenExpr w e) + +weakenPExpr :: (forall env1 env1' t'. env1 :> env1' -> expr env1 t' -> expr env1' t') + -> env :> env' -> PExpr expr env t -> PExpr expr env' t +weakenPExpr _ _ (Const t x) = Const t x +weakenPExpr f w (Pair e1 e2) = Pair (f w e1) (f w e2) +weakenPExpr _ _ Nil = Nil +weakenPExpr f w (Prim op e) = Prim op (f w e) +weakenPExpr _ w (Var var) = Var (weakenVar w var) +weakenPExpr f w (Let lhs rhs e) + | Exists lhs' <- rebuildLHS lhs + = Let lhs' (f w rhs) (f (sinkWithLHS lhs lhs' w) e) + +sinkWithLHS :: LHS s t env1 env1' -> LHS s t env2 env2' -> env1 :> env2 -> env1' :> env2' +sinkWithLHS (L0 _) (L0 _) w = w +sinkWithLHS (L1 _) (L1 _) w = Weaken (\case Z -> Z ; S i -> S (w >:> i)) +sinkWithLHS (L2 l1 l2) (L2 l1' l2') w = sinkWithLHS l2 l2' (sinkWithLHS l1 l1' w) +sinkWithLHS _ _ _ = error "sinkWithLHS: unequal LHSs" + +untupleE :: Tup (Expr env) t -> Expr env t +untupleE = untupleE' Expr + +untupleE' :: (forall t'. PExpr expr env t' -> expr env t') + -> Tup (expr env) t -> expr env t +untupleE' f T0 = f Nil +untupleE' _ (T1 e) = e +untupleE' f (T2 t1 t2) = f (Pair (untupleE' f t1) (untupleE' f t2)) + +evars :: Tup (V STy env) t -> Expr env t +evars = evars' Expr + +evars' :: (forall env' t'. PExpr expr env' t' -> expr env' t') + -> Tup (V STy env) t -> expr env t +evars' f = untupleE' f . fmapTup (f . Var) + +etypeOf :: Expr env t -> Tup STy t +etypeOf (Expr e) = eptypeOf etypeOf e + +eptypeOf :: (forall env' t'. expr env' t' -> Tup STy t') + -> PExpr expr env t -> Tup STy t +eptypeOf _ (Const t _) = T1 t +eptypeOf f (Pair e1 e2) = T2 (f e1) (f e2) +eptypeOf _ Nil = T0 +eptypeOf _ (Prim op _) = T1 (opertypeOf op) +eptypeOf _ (Var (V t _)) = T1 t +eptypeOf f (Let _ _ e) = f e + +opertypeOf :: Oper (t -> t') -> STy t' +opertypeOf (Add t) = t +opertypeOf (Mul t) = t +opertypeOf Round = TInt + +eInto :: (forall env' t'. expr env' t' -> expr' env' t') + -> PExpr expr env t -> PExpr expr' env t +eInto _ (Const t x) = Const t x +eInto f (Pair e1 e2) = Pair (f e1) (f e2) +eInto _ Nil = Nil +eInto f (Prim op e) = Prim op (f e) +eInto _ (Var v) = Var v +eInto f (Let lhs rhs e) = Let lhs (f rhs) (f e) |