
  0 | module Core.Name.CompatibleVars
  1 | 
  2 | public export
  3 | data CompatibleVars : (xs, ys : SnocList a) -> Type where
  4 |    Pre : CompatibleVars xs xs
  5 |    Ext : CompatibleVars xs ys -> CompatibleVars (xs :< n) (ys :< m)
  6 | 
  7 | export
  8 | invertExt : CompatibleVars (xs :< n) (ys :< m) -> CompatibleVars xs ys
  9 | invertExt Pre = Pre
 10 | invertExt (Ext p) = p
 11 | 
 12 | export
 13 | extendCompats : (args : SnocList a) ->
 14 |                 CompatibleVars xs ys ->
 15 |                 CompatibleVars (xs ++ args) (ys ++ args)
 16 | extendCompats args Pre = Pre
 17 | extendCompats args prf = go args prf where
 18 | 
 19 |   go : (args : SnocList a) ->
 20 |        CompatibleVars xs ys ->
 21 |        CompatibleVars (xs ++ args) (ys ++ args)
 22 |   go [<] prf = prf
 23 |   go (xs :< x) prf = Ext (go xs prf)
 24 | 
 25 | export
 26 | decCompatibleVars : (xs, ys : SnocList a) -> Dec (CompatibleVars xs ys)
 27 | decCompatibleVars [<] [<] = Yes Pre
 28 | decCompatibleVars [<] (xs :< x) = No (\case p impossible)
 29 | decCompatibleVars (xs :< x) [<] = No (\case p impossible)
 30 | decCompatibleVars (xs :< x) (ys :< y) = case decCompatibleVars xs ys of
 31 |   Yes prf => Yes (Ext prf)
 32 |   No nprf => No (nprf . invertExt)
 33 | 
 34 | export
 35 | areCompatibleVars : (xs, ys : SnocList a) ->
 36 |                     Maybe (CompatibleVars xs ys)
 37 | areCompatibleVars [<] [<] = pure Pre
 38 | areCompatibleVars (xs :< x) (ys :< y)
 39 |     = do compat <- areCompatibleVars xs ys
 40 |          pure (Ext compat)
 41 | areCompatibleVars _ _ = Nothing
 42 |