module Quox.Equal

import public Quox.Syntax
import Control.Monad.Either
import Generics.Derive

%default total
%language ElabReflection


public export
data Mode = Equal | Sub
%runElab derive "Mode" [Generic, Meta, Eq, Ord, DecEq, Show]

public export
data Error
= ClashT Mode (Term d n) (Term d n)
| ClashU Mode Universe Universe
| ClashQ      Qty      Qty

private %inline
ClashE : Mode -> Elim d n -> Elim d n -> Error
ClashE mode = ClashT mode `on` E

parameters {auto _ : MonadError Error m}
  private %inline
  clashT : Mode -> Term d n -> Term d n -> m a
  clashT mode = throwError .: ClashT mode

  private %inline
  clashE : Mode -> Elim d n -> Elim d n -> m a
  clashE mode = throwError .: ClashE mode

  mutual
    private covering
    compareTN' : Mode ->
                 (s, t : Term 0 n) ->
                 (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()

    compareTN' mode (TYPE k) (TYPE l) _ _ =
      case mode of
           Equal => unless (k == l) $ throwError $ ClashU Equal k l
           Sub   => unless (k <= l) $ throwError $ ClashU Sub   k l
    compareTN' mode s@(TYPE _) t _ _ = clashT mode s t

    compareTN' mode (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
      -- [todo] this should probably always be ==, right..?
      unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
      compareT0  mode arg2 arg1 -- reversed for contravariant Sub
      compareTS0 mode res1 res2
    compareTN' mode s@(Pi {}) t _ _ = clashT mode s t

    -- [todo] eta
    compareTN' _ (Lam _ body1) (Lam _ body2) _ _ =
      compareTS0 Equal body1 body2
    compareTN' mode s@(Lam {}) t _ _ = clashT mode s t

    compareTN' mode (E e) (E f) ps pt = compareE0 mode e f
    compareTN' mode s@(E _) t _ _ = clashT mode s t

    compareTN' _ (CloT  {}) _ ps _ = void $ ps IsCloT
    compareTN' _ (DCloT {}) _ ps _ = void $ ps IsDCloT

    private covering
    compareEN' : Mode ->
                 (e, f : Elim 0 n) ->
                 (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()

    compareEN' mode e@(F x) f@(F y) _ _ =
      unless (x == y) $ clashE mode e f
    compareEN' mode e@(F _) f _ _ = clashE mode e f

    compareEN' mode e@(B i) f@(B j) _ _ =
      unless (i == j) $ clashE mode e f
    compareEN' mode e@(B _) f _ _ = clashE mode e f

    -- [todo] tracking variance of functions? maybe???
    -- probably not
    compareEN' _ (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do
      compareE0 Equal fun1 fun2
      compareT0 Equal arg1 arg2
    compareEN' mode e@(_ :@ _) f _ _ = clashE mode e f

    -- [todo] is always checking the types are equal correct?
    compareEN' mode (tm1 :# ty1) (tm2 :# ty2) _ _ = do
      compareT0 mode tm1 tm2
      compareT0 Equal ty1 ty2
    compareEN' mode e@(_ :# _) f _ _ = clashE mode e f

    compareEN' _ (CloE  {}) _ pe _ = void $ pe IsCloE
    compareEN' _ (DCloE {}) _ pe _ = void $ pe IsDCloE


    private covering %inline
    compareTN : Mode -> NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
    compareTN mode s t = compareTN' mode s.fst t.fst s.snd t.snd

    private covering %inline
    compareEN : Mode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
    compareEN mode e f = compareEN' mode e.fst f.fst e.snd f.snd


    export covering %inline
    compareT : Mode -> DimEq d -> Term d n -> Term d n -> m ()
    compareT mode eqs s t =
      for_ (splits eqs) $ \th => compareT0 mode (s /// th) (t /// th)

    export covering %inline
    compareE : Mode -> DimEq d -> Elim d n -> Elim d n -> m ()
    compareE mode eqs e f =
      for_ (splits eqs) $ \th => compareE0 mode (e /// th) (f /// th)


    export covering %inline
    compareT0 : Mode -> Term 0 n -> Term 0 n -> m ()
    compareT0 mode s t = compareTN mode (whnfT s) (whnfT t)

    export covering %inline
    compareE0 : Mode -> Elim 0 n -> Elim 0 n -> m ()
    compareE0 mode e f = compareEN mode (whnfE e) (whnfE f)

    export covering %inline
    compareTS0 : Mode -> ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
    compareTS0 mode (TUnused body1) (TUnused body2) =
      compareT0 mode body1 body2
    compareTS0 mode body1 body2 =
      compareT0 mode (fromScopeTerm body1) (fromScopeTerm body2)


    export covering %inline
    equalTWith : DimEq d -> Term d n -> Term d n -> m ()
    equalTWith = compareT Equal

    export covering %inline
    equalEWith : DimEq d -> Elim d n -> Elim d n -> m ()
    equalEWith = compareE Equal

    export covering %inline
    subTWith : DimEq d -> Term d n -> Term d n -> m ()
    subTWith = compareT Sub

    export covering %inline
    subEWith : DimEq d -> Elim d n -> Elim d n -> m ()
    subEWith = compareE Sub


    export covering %inline
    equalT : {d : Nat} -> Term d n -> Term d n -> m ()
    equalT = equalTWith DimEq.new

    export covering %inline
    equalE : {d : Nat} -> Elim d n -> Elim d n -> m ()
    equalE = equalEWith DimEq.new

    export covering %inline
    subT : {d : Nat} -> Term d n -> Term d n -> m ()
    subT = subTWith DimEq.new

    export covering %inline
    subE : {d : Nat} -> Elim d n -> Elim d n -> m ()
    subE = subEWith DimEq.new