quox/lib/Quox/Thin/Term.idr

module Quox.Thin.Term

import public Quox.Thin.Base
import public Quox.Thin.Comp
import public Quox.Thin.List
import Quox.Thin.Eqv
import public Quox.Thin.Cover
import Quox.Name
import Quox.Loc
import Data.DPair
import public Data.List.Quantifiers
import Data.Vect
import Data.Singleton
import Decidable.Equality

%default total

public export
record Thinned f n where
  constructor Th
  {0 scope   : Nat}
  {scopeMask : Nat}
  0 ope : OPE scope n scopeMask
  term  : f scope
%name Thinned s, t, u

export
(forall n. Eq (f n)) => Eq (Thinned f n) where
  s == t = case decEq s.scopeMask t.scopeMask of
    Yes eq => s.term == (rewrite maskEqInner s.ope t.ope eq in t.term)
    No  _  => False

export
(forall n. Located (f n)) => Located (Thinned f n) where
  term.loc = term.term.loc

export
(forall n. Relocatable (f n)) => Relocatable (Thinned f n) where
  setLoc loc = {term $= setLoc loc}

namespace Thinned
  export
  pure : {n : Nat} -> f n -> Thinned f n
  pure term = Th id.snd term

  export
  join : {n : Nat} -> Thinned (Thinned f) n -> Thinned f n
  join (Th ope1 (Th ope2 term)) = Th (ope1 . ope2) term


public export
record ScopedN (s : Nat) (f : Nat -> Type) (n : Nat) where
  constructor S
  names : Vect s BindName
  {0 scope : Nat}
  {mask : Nat}
  0 ope : OPE scope s mask
  body : f (scope + n)

export
(forall n. Eq (f n)) => Eq (ScopedN s f n) where
  s1 == s2 = case decEq s1.mask s2.mask of
    Yes eq =>
      s1.names == s2.names &&
      s1.body == (rewrite maskEqInner s1.ope s2.ope eq in s2.body)
    No _ => False

export
{s : Nat} -> (forall n. Show (f n)) => Show (ScopedN s f n) where
  showPrec d (S ns ope body) = showCon d "S" $
    showArg ns ++ showArg (unVal $ maskToOpe ope) ++ showArg body

public export
Scoped : (Nat -> Type) -> Nat -> Type
Scoped d n = ScopedN 1 d n

(.name) : Scoped f n -> BindName
(S {names = [x], _}).name = x

export
(forall n. Located (f n)) => Located (ScopedN s f n) where
  s.loc = s.body.loc

export
(forall n. Relocatable (f n)) => Relocatable (ScopedN s f n) where
  setLoc loc = {body $= setLoc loc}


public export
record Thinned2 f d n where
  constructor Th2
  {0 dscope, tscope : Nat}
  {dmask, tmask : Nat}
  0 dope : OPE dscope d dmask
  0 tope : OPE tscope n tmask
  term : f dscope tscope
%name Thinned2 term

export
(forall d, n. Eq (f d n)) => Eq (Thinned2 f d n) where
  s == t = case (decEq s.dmask t.dmask, decEq s.tmask t.tmask) of
    (Yes deq, Yes teq) =>
      s.term == (rewrite maskEqInner s.dope t.dope deq in
                 rewrite maskEqInner s.tope t.tope teq in t.term)
    _ => False

export
(forall d, n. Located (f d n)) => Located (Thinned2 f d n) where
  term.loc = term.term.loc

export
(forall d, n. Relocatable (f d n)) => Relocatable (Thinned2 f d n) where
  setLoc loc = {term $= setLoc loc}

namespace Thinned2
  export
  pure : {d, n : Nat} -> f d n -> Thinned2 f d n
  pure term = Th2 id.snd id.snd term

  export
  join : {d, n : Nat} -> Thinned2 (Thinned2 f) d n -> Thinned2 f d n
  join (Th2 dope1 tope1 (Th2 dope2 tope2 term)) =
    Th2 (dope1 . dope2) (tope1 . tope2) term


namespace TermList
  public export
  data Element : (Nat -> Nat -> Type) ->
                 OPE dscope d dmask -> OPE tscope n tmask -> Type where
    T : f dscope tscope ->
        {dmask : Nat} -> (0 dope : OPE dscope d dmask) ->
        {tmask : Nat} -> (0 tope : OPE tscope n tmask) ->
        Element f dope tope
  %name TermList.Element s, t, u

  export
  elementEq : (forall d, n. Eq (f d n)) =>
              Element {d, n} f dope1 tope1 -> Element {d, n} f dope2 tope2 ->
              Bool
  elementEq (T s dope1 tope1 {dmask = dm1, tmask = tm1})
            (T t dope2 tope2 {dmask = dm2, tmask = tm2}) =
    case (decEq dm1 dm2, decEq tm1 tm2) of
      (Yes deq, Yes teq) =>
        s == (rewrite maskEqInner dope1 dope2 deq in
              rewrite maskEqInner tope1 tope2 teq in t)
      _ => False

  public export
  data TermList : List (Nat -> Nat -> Type) ->
                  OPEList d -> OPEList n -> Type where
    Nil  : TermList [] [] []
    (::) : Element f dope tope ->
           TermList fs dopes topes ->
           TermList (f :: fs) (dope :: dopes) (tope :: topes)
  %name TermList ss, ts, us

  export
  termListEq : All (\f => forall d, n. Eq (f d n)) fs =>
               TermList {d, n} fs dopes1 topes1 ->
               TermList {d, n} fs dopes2 topes2 ->
               Bool
  termListEq [] [] = True
  termListEq (s :: ss) (t :: ts) @{eq :: eqs} =
    elementEq s t && termListEq ss ts


public export
record Subterms (fs : List (Nat -> Nat -> Type)) d n where
  constructor Sub
  {0 dopes : OPEList d}
  {0 topes : OPEList n}
  terms : TermList fs dopes topes
  0 dcov : Cover dopes
  0 tcov : Cover topes
%name Subterms ss, ts, us

export
All (\f => forall d, n. Eq (f d n)) fs => Eq (Subterms fs d n) where
  ss == ts = ss.terms `termListEq` ts.terms