0 | module Core.Name.Scoped
  1 |
  2 | import public Core.Name
  3 |
  4 | import Libraries.Data.List.SizeOf
  5 |
  6 | import public Libraries.Data.List.Thin
  7 |
  8 | %default total
  9 |
 10 | ------------------------------------------------------------------------
 11 | -- Basic type definitions
 12 |
 13 | ||| Something which is having similar order as Scope itself
 14 | public export
 15 | Scopeable : (a: Type) -> Type
 16 | Scopeable = List
 17 |
 18 | ||| A scope is represented by a list of names. E.g. in the following
 19 | ||| rule, the scope Γ is extended with x when going under the λx.
 20 | ||| binder:
 21 | |||
 22 | |||    Γ, x ⊢ t : B
 23 | |||  -----------------------------
 24 | |||    Γ    ⊢ λx. t : A → B
 25 | public export
 26 | Scope : Type
 27 | Scope = Scopeable Name
 28 |
 29 | namespace Scope
 30 |   public export
 31 |   empty : Scopeable a
 32 |   empty = []
 33 |
 34 |   {-
 35 |   public export
 36 |   ext : Scopeable a -> List a -> Scopeable a
 37 |   ext vars ns = ns ++ vars
 38 |   --- TODO replace by `vars <>< ns`
 39 |   -}
 40 |
 41 |   public export
 42 |   addInner : Scopeable a -> Scopeable a -> Scopeable a
 43 |   addInner vars inner = inner ++ vars
 44 |   --- TODO replace by `vars ++ inner`
 45 |
 46 |   public export
 47 |   bind : Scopeable a -> a -> Scopeable a
 48 |   bind vars n = n :: vars
 49 |   --- TODO replace with `<:`
 50 |
 51 |   public export
 52 |   single : a -> Scopeable a
 53 |   single n = [n]
 54 |
 55 | ||| A scoped definition is one indexed by a scope
 56 | public export
 57 | Scoped : Type
 58 | Scoped = Scope -> Type
 59 |
 60 | ------------------------------------------------------------------------
 61 | -- Semi-decidable equality
 62 |
 63 | export
 64 | scopeEq : (xs, ys : Scope) -> Maybe (xs = ys)
 65 | scopeEq [] [] = Just Refl
 66 | scopeEq (x :: xs) (y :: ys)
 67 |     = do Refl <- nameEq x y
 68 |          Refl <- scopeEq xs ys
 69 |          Just Refl
 70 | scopeEq _ _ = Nothing
 71 |
 72 | ------------------------------------------------------------------------
 73 | -- Generate a fresh name (for a given scope)
 74 |
 75 | export
 76 | mkFresh : Scope -> Name -> Name
 77 | mkFresh vs n
 78 |   = if n `elem` vs
 79 |     then assert_total $ mkFresh vs (next n)
 80 |     else n
 81 |
 82 |
 83 | ------------------------------------------------------------------------
 84 | -- Compatible variables
 85 |
 86 | public export
 87 | data CompatibleVars : (xs, ys : List a) -> Type where
 88 |    Pre : CompatibleVars xs xs
 89 |    Ext : CompatibleVars xs ys -> CompatibleVars (n :: xs) (m :: ys)
 90 |
 91 | export
 92 | invertExt : CompatibleVars (n :: xs) (m :: ys) -> CompatibleVars xs ys
 93 | invertExt Pre = Pre
 94 | invertExt (Ext p) = p
 95 |
 96 | export
 97 | extendCompats : (args : List a) ->
 98 |                 CompatibleVars xs ys ->
 99 |                 CompatibleVars (args ++ xs) (args ++ ys)
100 | extendCompats args Pre = Pre
101 | extendCompats args prf = go args prf where
102 |
103 |   go : (args : List a) ->
104 |        CompatibleVars xs ys ->
105 |        CompatibleVars (args ++ xs) (args ++ ys)
106 |   go [] prf = prf
107 |   go (x :: xs) prf = Ext (go xs prf)
108 |
109 | export
110 | decCompatibleVars : (xs, ys : List a) -> Dec (CompatibleVars xs ys)
111 | decCompatibleVars [] [] = Yes Pre
112 | decCompatibleVars [] (x :: xs) = No (\case p impossible)
113 | decCompatibleVars (x :: xs) [] = No (\case p impossible)
114 | decCompatibleVars (x :: xs) (y :: ys) = case decCompatibleVars xs ys of
115 |   Yes prf => Yes (Ext prf)
116 |   No nprf => No (nprf . invertExt)
117 |
118 | export
119 | areCompatibleVars : (xs, ys : List a) ->
120 |                     Maybe (CompatibleVars xs ys)
121 | areCompatibleVars [] [] = pure Pre
122 | areCompatibleVars (x :: xs) (y :: ys)
123 |     = do compat <- areCompatibleVars xs ys
124 |          pure (Ext compat)
125 | areCompatibleVars _ _ = Nothing
126 |
127 | ------------------------------------------------------------------------
128 | -- Concepts
129 |
130 | public export
131 | 0 Weakenable : Scoped -> Type
132 | Weakenable tm = {0 vars, ns : Scope} ->
133 |   SizeOf ns -> tm vars -> tm (ns ++ vars)
134 |
135 | public export
136 | 0 Strengthenable : Scoped -> Type
137 | Strengthenable tm = {0 vars, ns : Scope} ->
138 |   SizeOf ns -> tm (ns ++ vars) -> Maybe (tm vars)
139 |
140 | public export
141 | 0 GenWeakenable : Scoped -> Type
142 | GenWeakenable tm = {0 outer, ns, local : Scope} ->
143 |   SizeOf local -> SizeOf ns -> tm (local ++ outer) -> tm (local ++ (ns ++ outer))
144 |
145 | public export
146 | 0 Thinnable : Scoped -> Type
147 | Thinnable tm = {0 xs, ys : Scope} -> tm xs -> Thin xs ys -> tm ys
148 |
149 | public export
150 | 0 Shrinkable : Scoped -> Type
151 | Shrinkable tm = {0 xs, ys : Scope} -> tm xs -> Thin ys xs -> Maybe (tm ys)
152 |
153 | public export
154 | 0 Embeddable : Scoped -> Type
155 | Embeddable tm = {0 outer, vars : Scope} -> tm vars -> tm (vars ++ outer)
156 |
157 | ------------------------------------------------------------------------
158 | -- IsScoped interface
159 |
160 | public export
161 | interface Weaken (0 tm : Scoped) where
162 |   constructor MkWeaken
163 |   -- methods
164 |   weaken : tm vars -> tm (nm :: vars)
165 |   weakenNs : Weakenable tm
166 |   -- default implementations
167 |   weaken = weakenNs (suc zero)
168 |
169 | -- This cannot be merged with Weaken because of WkCExp
170 | public export
171 | interface GenWeaken (0 tm : Scoped) where
172 |   constructor MkGenWeaken
173 |   genWeakenNs : GenWeakenable tm
174 |
175 | export
176 | genWeaken : GenWeaken tm =>
177 |   SizeOf local -> tm (local ++ outer) -> tm (local ++ n :: outer)
178 | genWeaken l = genWeakenNs l (suc zero)
179 |
180 | public export
181 | interface Strengthen (0 tm : Scoped) where
182 |   constructor MkStrengthen
183 |   -- methods
184 |   strengthenNs : Strengthenable tm
185 |
186 | export
187 | strengthen : Strengthen tm => tm (nm :: vars) -> Maybe (tm vars)
188 | strengthen = strengthenNs (suc zero)
189 |
190 | public export
191 | interface FreelyEmbeddable (0 tm : Scoped) where
192 |   constructor MkFreelyEmbeddable
193 |   -- this is free for nameless representations
194 |   embed : Embeddable tm
195 |   embed = believe_me
196 |
197 | export
198 | FunctorFreelyEmbeddable : Functor f => FreelyEmbeddable tm => FreelyEmbeddable (f . tm)
199 | FunctorFreelyEmbeddable = MkFreelyEmbeddable believe_me
200 |
201 | export
202 | ListFreelyEmbeddable : FreelyEmbeddable tm => FreelyEmbeddable (List . tm)
203 | ListFreelyEmbeddable = FunctorFreelyEmbeddable
204 |
205 | export
206 | MaybeFreelyEmbeddable : FreelyEmbeddable tm => FreelyEmbeddable (Maybe . tm)
207 | MaybeFreelyEmbeddable = FunctorFreelyEmbeddable
208 |
209 | export
210 | GenWeakenWeakens : GenWeaken tm => Weaken tm
211 | GenWeakenWeakens = MkWeaken (genWeakenNs zero (suc zero)) (genWeakenNs zero)
212 |
213 | export
214 | FunctorGenWeaken : Functor f => GenWeaken tm => GenWeaken (f . tm)
215 | FunctorGenWeaken = MkGenWeaken (\ l, s => map (genWeakenNs l s))
216 |
217 | export
218 | FunctorWeaken : Functor f => Weaken tm => Weaken (f . tm)
219 | FunctorWeaken = MkWeaken (go (suc zero)) go where
220 |
221 |   go : Weakenable (f . tm)
222 |   go s = map (weakenNs s)
223 |
224 | export
225 | ListWeaken : Weaken tm => Weaken (List . tm)
226 | ListWeaken = FunctorWeaken
227 |
228 | export
229 | MaybeWeaken : Weaken tm => Weaken (Maybe . tm)
230 | MaybeWeaken = FunctorWeaken
231 |
232 | public export
233 | interface Weaken tm => IsScoped (0 tm : Scoped) where
234 |   -- methods
235 |   compatNs : CompatibleVars xs ys -> tm xs -> tm ys
236 |
237 |   thin : Thinnable tm
238 |   shrink : Shrinkable tm
239 |
240 | export
241 | compat : IsScoped tm => tm (m :: xs) -> tm (n :: xs)
242 | compat = compatNs (Ext Pre)
243 |