module Data.Term

import public Data.DPair
import public Data.Fin.Strong
import public Data.Vect
import Data.Vect.Properties.Map
import Syntax.PreorderReasoning

%prefix_record_projections off

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

public export
record Signature where
  constructor MkSignature
  Operator : Nat -> Type

%name Signature sig

public export
(.Op) : Signature -> Type
sig .Op = Exists sig.Operator

public export
interface DecOp (0 sig : Signature) where
  decOp : (op, op' : sig.Op) -> Dec (op = op')

public export
data Term : Signature -> Nat -> Type where
  Var : SFin (S n) -> Term sig (S n)
  Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n

%name Term t, u, v

export
Var' : SFin n -> Term sig n
Var' x = rewrite indexPred'Prf x in Var (replace {p = SFin} (indexPred'Prf x) x)

export
varIsVar : (x : SFin (S n)) -> Var' x = Var x
varIsVar x = Refl

export
Uninhabited (Op op ts = Var x) where uninhabited prf impossible

-- Substitution ----------------------------------------------------------------

export
pure : (SFin k -> SFin n) -> SFin k -> Term sig n
pure r = Var' . r

public export
(<$>) : (SFin k -> Term sig n) -> Term sig k -> Term sig n
f <$> Var i = f i
f <$> Op op ts = Op op (map (\t => f <$> assert_smaller ts t) ts)

-- Extensional Equality --------------------------------------------------------

public export
0 (.=.) : Rel (SFin k -> Term sig n)
f .=. g = (i : SFin k) -> f i = g i

export
subCong : {f, g : SFin k -> Term sig n} -> f .=. g -> (t : Term sig k) -> f <$> t = g <$> t
subCong prf (Var i) = prf i
subCong prf (Op op ts) =
  cong (Op op) $
  mapExtensional (f <$>) (g <$>) (\t => subCong prf (assert_smaller ts t)) ts

-- Substitution is Monadic -----------------------------------------------------

public export
(.) : (SFin k -> Term sig n) -> (SFin j -> Term sig k) -> SFin j -> Term sig n
f . g = (f <$>) . g

-- Properties

export
subUnit : (t : Term sig n) -> Var' <$> t = t
subUnit (Var i) = Refl
subUnit (Op op ts) = cong (Op op) $ Calc $
  |~ map (Var' <$>) ts
  ~~ map id ts         ...(mapExtensional (Var' <$>) id (\t => subUnit (assert_smaller ts t)) ts)
  ~~ ts                ...(mapId ts)

export
subAssoc :
  (f : SFin k -> Term sig n) ->
  (g : SFin j -> Term sig k) ->
  (t : Term sig j) ->
  (f . g) <$> t = f <$> g <$> t
subAssoc f g (Var i) = Refl
subAssoc f g (Op op ts) = cong (Op op) $ Calc $
  |~ map ((f . g) <$>) ts
  ~~ map ((f <$>) . (g <$>)) ts   ...(mapExtensional ((f . g) <$>) ((f <$>) . (g <$>)) (\t => subAssoc f g (assert_smaller ts t)) ts)
  ~~ map (f <$>) (map (g <$>) ts) ..<(mapFusion (f <$>) (g <$>) ts)

export
subComp :
  (f : SFin k -> Term sig n) ->
  (r : SFin j -> SFin k) ->
  f . pure r .=. f . r
subComp f r i = Refl

-- Injectivity -----------------------------------------------------------------

export
opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
opInjectiveLen Refl = Refl

export
opInjectiveOp :
  (prf : Op {sig, k} op ts = Op {sig, k = n} op' us) ->
  the sig.Op (Evidence k op) = Evidence n op'
opInjectiveOp Refl = Refl

export
opInjectiveTs' : {0 ts, us : Vect k (Term sig n)} -> (prf : Op op ts = Op op us) -> ts = us
opInjectiveTs' Refl = Refl

export
opInjectiveTs :
  {0 ts : Vect k (Term sig n)} ->
  {0 us : Vect j (Term sig n)} ->
  (prf : Op op ts = Op op' us) -> ts = (rewrite opInjectiveLen prf in us)
opInjectiveTs Refl = Refl