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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module AST.Weaken.Auto (
autoWeak,
GivenSegment(..),
($..),
Layout(..),
) where
import Data.Functor.Const
import GHC.OverloadedLabels
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
import AST.Weaken
import Data
import Lemmas
type family Lookup name list where
Lookup name ('(name, x) : _) = x
Lookup name (_ : list) = Lookup name list
data Layout (segments :: [(Symbol, [t])]) (env :: [t]) where
LSeg :: forall name segments. KnownSymbol name => Layout segments (Lookup name segments)
(:++:) :: Layout segments env1 -> Layout segments env2 -> Layout segments (Append env1 env2)
infixr :++:
instance (KnownSymbol name, seg ~ Lookup name segments) => IsLabel name (Layout segments seg) where
fromLabel = LSeg @name @segments
data SSegments (segments :: [(Symbol, [t])]) where
SSegNil :: SSegments '[]
SSegCons :: SSymbol name -> SList (Const ()) ts -> SSegments list -> SSegments ('(name, ts) : list)
class ToSegments k a | a -> k where
type SegmentsOf k a :: [(Symbol, [k])]
toSegments :: a -> SSegments (SegmentsOf k a)
instance ToSegments k (SSegments (segments :: [(Symbol, [k])])) where
type SegmentsOf k (SSegments segments) = segments
toSegments = id
data GivenSegment name ts = forall f. KnownSymbol name => Seg (SList f ts)
| (KnownSymbol name, KnownListSpine ts) => Seg'
instance ToSegments k (GivenSegment name (ts :: [k])) where
type SegmentsOf k (GivenSegment name (ts :: [k])) = '[ '(name, ts)]
toSegments (Seg list) = SSegCons symbolSing (slistMap (\_ -> Const ()) list) SSegNil
toSegments Seg' = SSegCons symbolSing knownListSpine SSegNil
infixr $..
($..) :: (ToSegments k a, ToSegments k b) => a -> b -> SSegments (Append (SegmentsOf k a) (SegmentsOf k b))
x $.. y = ssegmentsAppend (toSegments x) (toSegments y)
where
ssegmentsAppend :: SSegments a -> SSegments b -> SSegments (Append a b)
ssegmentsAppend SSegNil l2 = l2
ssegmentsAppend (SSegCons name list l1) l2 = SSegCons name list (ssegmentsAppend l1 l2)
-- | If the found segment is a TopSeg, returns Nothing.
segmentLookup :: forall segments name. SSegments segments -> SSymbol name -> SList (Const ()) (Lookup name segments)
segmentLookup = \segs name -> case go segs name of
Just ts -> ts
Nothing -> error $ "Segment not found: " ++ fromSSymbol name
where
go :: forall segs'. SSegments segs' -> SSymbol name -> Maybe (SList (Const ()) (Lookup name segs'))
go SSegNil _ = Nothing
go (SSegCons n@(SSymbol @n) (ts :: SList _ ts) (sseg :: SSegments rest)) name@SSymbol =
case sameSymbol n name of
Just Refl ->
case go sseg name of
Nothing -> Just ts
Just _ -> error $ "Duplicate segment with name " ++ fromSSymbol name
Nothing ->
case unsafeCoerce Refl :: (Lookup name ('(n, ts) : rest) :~: Lookup name rest) of
Refl -> go sseg name
data LinLayout (segments :: [(Symbol, [t])]) (env :: [t]) where
LinEnd :: LinLayout segments '[]
LinApp :: SSymbol name -> LinLayout segments env -> LinLayout segments (Append (Lookup name segments) env)
linLayoutAppend :: LinLayout segments env1 -> LinLayout segments env2 -> LinLayout segments (Append env1 env2)
linLayoutAppend LinEnd lin = lin
linLayoutAppend (LinApp (name :: SSymbol name) (lin1 :: LinLayout segments env1')) (lin2 :: LinLayout _ env2)
| Refl <- lemAppendAssoc @(Lookup name segments) @env1' @env2
= LinApp name (linLayoutAppend lin1 lin2)
lineariseLayout :: Layout segments env -> LinLayout segments env
lineariseLayout (LSeg @name :: Layout _ seg)
| Refl <- lemAppendNil @seg
= LinApp (symbolSing @name) LinEnd
lineariseLayout (ly1 :++: ly2) = lineariseLayout ly1 `linLayoutAppend` lineariseLayout ly2
linLayoutEnv :: SSegments segments -> LinLayout segments env -> SList (Const ()) env
linLayoutEnv _ LinEnd = SNil
linLayoutEnv segs (LinApp name lin) = sappend (segmentLookup segs name) (linLayoutEnv segs lin)
pullDown :: SSegments segments -> SSymbol name -> LinLayout segments env
-> r -- Name was not found in source
-> (forall env'. LinLayout segments env' -> env :> Append (Lookup name segments) env' -> r)
-> r
pullDown segs name@SSymbol linlayout kNotFound k =
case linlayout of
LinEnd -> kNotFound
LinApp n'@SSymbol lin
| Just Refl <- sameSymbol name n' -> k lin WId
| otherwise ->
pullDown segs name lin kNotFound $ \(lin' :: LinLayout _ env') w ->
k (LinApp n' lin') (WSwap (segmentLookup segs n') (segmentLookup segs name) (linLayoutEnv segs lin')
.> wCopies (segmentLookup segs n') w)
sortLinLayouts :: forall segments env1 env2.
SSegments segments
-> LinLayout segments env1 -> LinLayout segments env2 -> env1 :> env2
sortLinLayouts _ LinEnd LinEnd = WId
sortLinLayouts segs lin1@(LinApp name1@SSymbol tail1) (LinApp name2@SSymbol tail2)
| Just Refl <- sameSymbol name1 name2 = wCopies (segmentLookup segs name1) (sortLinLayouts segs tail1 tail2)
| otherwise =
pullDown segs name2 lin1
(wSinks (segmentLookup segs name2) .> sortLinLayouts segs lin1 tail2)
(\tail1' w ->
-- We've pulled down name2 in lin1 so that it's at the head; the
-- resulting modified tail is tail1'. Thus now we have (name2 : tail1')
-- vs (name2 : tail2). Thus we continue sorting tail1' vs tail2, and
-- wCopies the name2 on top of that.
wCopies (segmentLookup segs name2) (sortLinLayouts segs tail1' tail2) .> w)
sortLinLayouts _ LinEnd LinApp{} = error "Unequal number of segments: more in target than in source"
sortLinLayouts _ LinApp{} LinEnd = error "Unequal number of segments: more in source than in target"
autoWeak :: forall segments env1 env2.
SSegments segments -> Layout segments env1 -> Layout segments env2 -> env1 :> env2
autoWeak segs ly1 ly2 = sortLinLayouts segs (lineariseLayout ly1) (lineariseLayout ly2)
|
