@@ -11,14 +11,14 @@ public export
11data Resource : Type where
11data Resource : Type where
12 MkRes : label -> Type -> Resource
12 MkRes : label -> Type -> Resource
15+data Var = MkVar -- Phantom, just for labelling purposes
14%error_reverse
17%error_reverse
15public export
18public export
16−(:::) : label -> Type -> Resource
19+(:::) : Var -> Type -> Resource
17(:::) = MkRes
20(:::) = MkRes
20−data Var = MkVar -- Phantom, just for labelling purposes
22{- Contexts for holding current resources states -}
22{- Contexts for holding current resources states -}
23namespace Resources
23namespace Resources
24 public export
24 public export
@@ -33,7 +33,7 @@ namespace Resources
34{- Proof that a label has a particular type in a given context -}
34{- Proof that a label has a particular type in a given context -}
35public export
35public export
36−data InState : lbl -> Type -> Resources -> Type where
36+data InState : Var -> Type -> Resources -> Type where
37 Here : InState lbl st (MkRes lbl st :: rs)
37 Here : InState lbl st (MkRes lbl st :: rs)
38 There : InState lbl st rs -> InState lbl st (r :: rs)
38 There : InState lbl st rs -> InState lbl st (r :: rs)
@@ -221,14 +221,14 @@ infix 6 :->
222public export
222public export
223data Action : Type -> Type where
223data Action : Type -> Type where
224− Stable : lbl -> Type -> Action ty
224+ Stable : Var -> Type -> Action ty
225− Trans : lbl -> Type -> (ty -> Type) -> Action ty
225+ Trans : Var -> Type -> (ty -> Type) -> Action ty
226− Remove : lbl -> Type -> Action ty
226+ Remove : Var -> Type -> Action ty
227 Add : (ty -> Resources) -> Action ty
227 Add : (ty -> Resources) -> Action ty
229namespace Stable
229namespace Stable
230 public export %error_reduce
230 public export %error_reduce
231− (:::) : lbl -> Type -> Action ty
231+ (:::) : Var -> Type -> Action ty
232 (:::) = Stable
232 (:::) = Stable
234namespace Trans
234namespace Trans
@@ -236,7 +236,7 @@ namespace Trans
236 data Trans ty = (:->) Type Type
236 data Trans ty = (:->) Type Type
238 public export %error_reduce
238 public export %error_reduce
239− (:::) : lbl -> Trans ty -> Action ty
239+ (:::) : Var -> Trans ty -> Action ty
240 (:::) lbl (st :-> st') = Trans lbl st (const st')
240 (:::) lbl (st :-> st') = Trans lbl st (const st')
242namespace DepTrans
242namespace DepTrans
@@ -244,7 +244,7 @@ namespace DepTrans
244 data DepTrans ty = (:->) Type (ty -> Type)
244 data DepTrans ty = (:->) Type (ty -> Type)
246 public export %error_reduce
246 public export %error_reduce
247− (:::) : lbl -> DepTrans ty -> Action ty
247+ (:::) : Var -> DepTrans ty -> Action ty
248 (:::) lbl (st :-> st') = Trans lbl st st'
248 (:::) lbl (st :-> st') = Trans lbl st st'
250public export
250public export
@@ -252,19 +252,19 @@ or : a -> a -> Either b c -> a
252or x y = either (const x) (const y)
252or x y = either (const x) (const y)
254public export %error_reduce
254public export %error_reduce
255−add : Type -> Action a
255+add : Type -> Action Var
256add ty = Add (\var => [var ::: ty])
256add ty = Add (\var => [var ::: ty])
258public export %error_reduce
258public export %error_reduce
259−remove : lbl -> Type -> Action ty
259+remove : Var -> Type -> Action ty
260remove = Remove
260remove = Remove
262public export %error_reduce
262public export %error_reduce
263−addIfRight : Type -> Action (Either a b)
263+addIfRight : Type -> Action (Either a Var)
264addIfRight ty = Add (either (const []) (\var => [var ::: ty]))
264addIfRight ty = Add (either (const []) (\var => [var ::: ty]))
266public export %error_reduce
266public export %error_reduce
267−addIfJust : Type -> Action (Maybe a)
267+addIfJust : Type -> Action (Maybe Var)
268addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
268addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
270public export
270public export