module Data.Term.Property

import Data.Term

import Data.Vect.Properties.Index
import Data.Vect.Quantifiers
import Data.Vect.Quantifiers.Extra

import Syntax.PreorderReasoning

-- Definition ------------------------------------------------------------------

public export
record Property (sig : Signature) (k : Nat) where
  constructor MkProp
  Prop : forall n. (Fin k -> Term sig n) -> Type
  cong : forall n. {f, g : Fin k -> Term sig n} -> f .=. g -> Prop f -> Prop g

%name Property p, q

-- Instances -------------------------------------------------------------------

public export
Unifies : Term sig k -> Term sig k -> Property sig k
Unifies t u = MkProp
  { Prop = \f => f <$> t = f <$> u
  , cong = \cong, prf => Calc $
    |~ _ <$> t
    ~~ _ <$> t ..<(subCong cong t)
    ~~ _ <$> u ...(prf)
    ~~ _ <$> u ...(subCong cong u)
  }

public export
All : Vect n (Property sig k) -> Property sig k
All ps = MkProp (\f => All (\p => p.Prop f) ps) (\cong => mapRel (\p => p.cong cong))

-- Equivalence -----------------------------------------------------------------

public export 0
(<=>) : Property sig k -> Property sig k -> Type
p <=> q = forall n. (f : Fin k -> Term sig n) -> p.Prop f <=> q.Prop f

-- Properties

export
unifiesSym : Unifies t u <=> Unifies u t
unifiesSym f = MkEquivalence (\prf => sym prf) (\prf => sym prf)

export
unifiesOp :
  {k : Nat} ->
  {0 op : sig.Operator k} ->
  {0 ts, us : Vect k (Term sig j)} ->
  Unifies (Op op ts) (Op op us) <=> All (tabulate (\i => Unifies (index i ts) (index i us)))
unifiesOp f = MkEquivalence
  { leftToRight = \prf => tabulate (\i => Unifies (index i ts) (index i us)) (leftToRight prf)
  , rightToLeft = \prf => irrelevantEq $ cong (Op op) $ rightToLeft prf
  }
  where
  leftToRight :
    (Unifies (Op op ts) (Op op us)).Prop f ->
    (i : _) ->
    f <$> index i ts = f <$> index i us
  leftToRight prf i =
    Calc $
      |~ f <$> index i ts
      ~~ index i (map (f <$>) ts) ...(sym $ indexNaturality i (f <$>) ts)
      ~~ index i (map (f <$>) us) ...(cong (index i) $ opInjectiveTs' prf)
      ~~ f <$> index i us         ...(indexNaturality i (f <$>) us)

  rightToLeft :
    {k : Nat} ->
    {ts, us : Vect k (Term sig j)} ->
    (All (tabulate (\i => Unifies (index i ts) (index i us)))).Prop f ->
    map (f <$>) ts = map (f <$>) us
  rightToLeft {ts = [], us = []} [] = Refl
  rightToLeft {ts = t :: ts, us = u :: us} (prf :: prfs) = cong2 (::) prf (rightToLeft prfs)

-- Nothing ---------------------------------------------------------------------

public export 0
Nothing : Property sig k -> Type
Nothing p = forall n. (f : Fin k -> Term sig n) -> Not (p.Prop f)

-- Properties

export
nothingEquiv : p <=> q -> Nothing p -> Nothing q
nothingEquiv eq absurd f x = absurd f ((eq f).rightToLeft x)

-- Extensions ------------------------------------------------------------------

public export
Extension : Property sig k -> (Fin k -> Term sig n) -> Property sig n
Extension p f = MkProp
  { Prop = \g => p.Prop (g . f)
  , cong = \prf => p.cong (\i => subCong prf (f i))
  }

-- Properties

export
nothingExtends : Nothing p -> Nothing (Extension p f)
nothingExtends absurd g x = void $ absurd (g . f) x

export
extendUnit : (p : Property sig k) -> p <=> Extension p Var
extendUnit p f = MkEquivalence id id

export
extendAssoc :
  (p : Property sig j) ->
  (f : Fin j -> Term sig k) ->
  (g : Fin k -> Term sig m) ->
  Extension (Extension p f) g <=> Extension p (g . f)
extendAssoc p f g h =
  MkEquivalence
    (p.cong (\i => subAssoc h g (f i)))
    (p.cong (\i => sym $ subAssoc h g (f i)))

export
extendUnify :
  (t, u : Term sig j) ->
  (f : Fin j -> Term sig k) ->
  (g : Fin k -> Term sig m) ->
  Extension (Unifies t u) (g . f) <=> Extension (Unifies (f <$> t) (f <$> u)) g
extendUnify t u f g h =
  MkEquivalence
    (\prf => Calc $
      |~ (h . g) <$> (f <$> t)
      ~~ ((h . g) . f) <$> t   ...(sym $ subAssoc (h . g) f t)
      ~~ (h . (g . f)) <$> t   ...(subCong (\i => subAssoc h g (f i)) t)
      ~~ (h . (g . f)) <$> u   ...(prf)
      ~~ ((h . g) . f) <$> u   ...(sym $ subCong (\i => subAssoc h g (f i)) u)
      ~~ (h . g) <$> (f <$> u) ...(subAssoc (h . g) f u))
    (\prf => Calc $
      |~ (h . (g . f)) <$> t
      ~~ ((h . g) . f) <$> t   ...(sym $ subCong (\i => subAssoc h g (f i)) t)
      ~~ (h . g) <$> (f <$> t) ...(subAssoc (h . g) f t)
      ~~ (h . g) <$> (f <$> u) ...(prf)
      ~~ ((h . g) . f) <$> u   ...(sym $ subAssoc (h . g) f u)
      ~~ (h . (g . f)) <$> u   ...(subCong (\i => subAssoc h g (f i)) u))