{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} -- I want to bring various type variables in scope using type annotations in -- patterns, but I don't want to have to mention all the other type parameters -- of the types in question as well then. Partial type signatures (with '_') are -- useful here. {-# LANGUAGE PartialTypeSignatures #-} {-# OPTIONS -Wno-partial-type-signatures #-} module AST.Bindings where import AST import Data import Lemmas -- binding lists: a let stack without a body. The stack lives in 'env' and defines 'binds'. data Bindings f env binds where BTop :: Bindings f env '[] BPush :: Bindings f env binds -> (STy t, f (Append binds env) t) -> Bindings f env (t : binds) deriving instance (forall e t. Show (f e t)) => Show (Bindings f env env') infixl `BPush` mapBindings :: (forall env' t'. f env' t' -> g env' t') -> Bindings f env binds -> Bindings g env binds mapBindings _ BTop = BTop mapBindings f (BPush b (t, e)) = BPush (mapBindings f b) (t, f e) weakenBindings :: (forall e1 e2 t. e1 :> e2 -> f e1 t -> f e2 t) -> env1 :> env2 -> Bindings f env1 binds -> (Bindings f env2 binds, Append binds env1 :> Append binds env2) weakenBindings _ w BTop = (BTop, w) weakenBindings wf w (BPush b (t, x)) = let (b', w') = weakenBindings wf w b in (BPush b' (t, wf w' x), WCopy w') weakenOver :: SList STy ts -> env :> env' -> Append ts env :> Append ts env' weakenOver SNil w = w weakenOver (SCons _ ts) w = WCopy (weakenOver ts w) sinkWithBindings :: Bindings f env binds -> env' :> Append binds env' sinkWithBindings BTop = WId sinkWithBindings (BPush b _) = WSink .> sinkWithBindings b bconcat :: forall f env binds1 binds2. Bindings f env binds1 -> Bindings f (Append binds1 env) binds2 -> Bindings f env (Append binds2 binds1) bconcat b1 BTop = b1 bconcat b1 (BPush (b2 :: Bindings _ (Append binds1 env) binds2C) (t, x)) | Refl <- lemAppendAssoc @binds2C @binds1 @env = BPush (bconcat b1 b2) (t, x) bindingsBinds :: Bindings f env binds -> SList STy binds bindingsBinds BTop = SNil bindingsBinds (BPush binds (t, _)) = SCons t (bindingsBinds binds) letBinds :: Bindings Ex env binds -> Ex (Append binds env) t -> Ex env t letBinds BTop = id letBinds (BPush b (_, rhs)) = letBinds b . ELet ext rhs