module Data.Term

import public Data.Vect
import Data.Vect.Properties.Map
import Syntax.PreorderReasoning

%prefix_record_projections off

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

public export
record Signature where
  Operator : Nat -> Type

%name Signature sig

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

%name Term t, u, v

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

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

export
(<$>) : (Fin 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 (Fin k -> Term sig n)
f .=. g = (i : Fin k) -> f i = g i

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

export
(.) : (Fin k -> Term sig n) -> (Fin j -> Term sig k) -> Fin 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 : Fin k -> Term sig n) ->
  (g : Fin 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 : Fin k -> Term sig n) ->
  (r : Fin j -> Fin 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
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