REType.idr

import Decidable.Equality

data RETree : (t : Type) -> Type where
  End : RETree t
  Item : t -> RETree t
  Sequence : RETree t -> RETree t -> RETree t
  OneOrTheOther : RETree t -> RETree t -> RETree t
  Repeated : RETree t -> RETree t -> RETree t

simpleItemAppliesToRE : (DecEq t) => t -> t -> Bool
simpleItemAppliesToRE x y with (decEq x y)
  simpleItemAppliesToRE x y | Yes prf = True
  simpleItemAppliesToRE x y | No contra = False

itemAppliesToRE : (DecEq t) => (r : RETree t) -> t -> Maybe (RETree t)
itemAppliesToRE End _ = Nothing
itemAppliesToRE (Item x) y =
  if simpleItemAppliesToRE x y then
    Just End
  else
    Nothing
itemAppliesToRE (Sequence a b) y with (itemAppliesToRE a y)
  itemAppliesToRE (Sequence a b) y | Nothing = Nothing
  itemAppliesToRE (Sequence a b) y | Just End = Just b
  itemAppliesToRE (Sequence a b) y | Just any = Just (Sequence any b)
itemAppliesToRE (OneOrTheOther a b) y with ((itemAppliesToRE a y),(itemAppliesToRE b y))
  itemAppliesToRE (OneOrTheOther a b) y | (Just aa, Just bb) = Just (OneOrTheOther aa bb)
  itemAppliesToRE (OneOrTheOther a b) y | (Just aa, _) = Just aa
  itemAppliesToRE (OneOrTheOther a b) y | (_, Just bb) = Just bb
  itemAppliesToRE (OneOrTheOther a b) y | (_, _) = Nothing
itemAppliesToRE (Repeated End End) _ = Nothing
itemAppliesToRE (Repeated a End) y = itemAppliesToRE (Repeated a a) y
itemAppliesToRE (Repeated a b) y with (itemAppliesToRE b y)
  itemAppliesToRE (Repeated a b) y | Just End = Just (Repeated a End)
  itemAppliesToRE (Repeated a b) y | Just v = Just (Repeated a v)
  itemAppliesToRE (Repeated a b) y | Nothing = Nothing

listAppliesToRE : (DecEq t) => List t -> RETree t -> Maybe (RETree t)
listAppliesToRE [] End = Just End
listAppliesToRE [] (Sequence a b) with ((listAppliesToRE [] a),(listAppliesToRE [] b))
  listAppliesToRE [] (Sequence a b) | (Just End, Just End) = Just End
  listAppliesToRE [] (Sequence a b) | _ = Nothing
listAppliesToRE [] (OneOrTheOther a b) with ((listAppliesToRE [] a),(listAppliesToRE [] b))
  listAppliesToRE [] (OneOrTheOther a b) | (Just End, _) = Just End
  listAppliesToRE [] (OneOrTheOther a b) | (_, Just End) = Just End
  listAppliesToRE [] (OneOrTheOther a b) | (_, _) = Nothing
listAppliesToRE [] (Repeated _ End) = Just End
listAppliesToRE [] _ = Nothing
listAppliesToRE (hd :: tl) re = itemAppliesToRE re hd >>= listAppliesToRE tl

reListType : (DecEq t) => List t -> RETree t -> Maybe (RETree t)
reListType l r = map (const r) (listAppliesToRE l r)

data REConformingList : (DecEq t) => Maybe (RETree t) -> Type -> Type where
  RETryList : (DecEq t) => (r : RETree t) -> (l : List t) -> REConformingList (reListType l r) t