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
|
{-# 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
|
