Tupled.idr

module Tupled

import Data.Vect
import Data.Fin

%default total

namespace Types

  public export
  data Ty = TyInt
          | TyTuple (Vect (S n) Ty)

namespace Terms

  mutual
    ||| Fields in a Tuple.
    public export
    data Fields : (types : Vect (S n) Ty)
               -> Type
      where
        Singleton : {ty    : Ty}
                 -> (field : Tupled ty)
                          -> Fields (ty::Nil)

        Extend : {ty    : Ty}
              -> {tys   : Vect (S n) Ty}
              -> (field : Tupled ty)
              -> (rest  : Fields      tys)
                       -> Fields (ty::tys)

    public export
    data Tupled : Ty -> Type where
          -- Base Values
          I : Int  -> Tupled TyInt

          -- Tuples & Accessors
          MkTuple : {types : Vect (S n) Ty}
                 -> (values : Fields          types)
                           -> Tupled (TyTuple types)

          Proj : {types : Vect (S n) Ty}
              -> (tuple : Tupled (TyTuple types))
              -> (idx   : Fin (S n))
                       -> Tupled (index idx types)

  public export
  index : {types  : Vect (S n) Ty}
       -> (idx    : Fin (S n))
       -> (fields : Fields types)
                 -> Tupled (index idx types)
  index FZ (Singleton first) = first
  index FZ (Extend next rest) = next
  index (FS x) (Extend next rest) = index _ rest

namespace Values
  mutual
    namespace Fields
      public export
      data Value : (fields : Fields types) -> Type
        where
          SingletonV : (field : Value v) -> Value (Singleton v)
          ExtendV : {field  : Tupled type}
                 -> {fields : Fields types}
                 -> (next : Value field)
                 -> (rest : Value fields)
                         -> Value (Extend field fields)

    public export
    data Value : Tupled type -> Type where
    
      IV : Value (I i)

      -- Tuples
      MkTupleV : Value fields
              -> Value (MkTuple fields)

namespace Reduction

  mutual
    namespace Fields
      public export
      data Redux : (this, that : Fields types) -> Type where
          SimplifySingleton : (prf : Redux this that)
                                  -> Redux (Singleton this) (Singleton that)

          SimplifyExtend : {this, that : Tupled type}
                        -> {rest : Fields types}
                        -> (prf : Redux this that)
                        -> Redux (Extend this rest) (Extend that rest)

          SimplifyExtendV : {this, that : Fields types}
                         -> (value      : Values.Value v)
                         -> (rest       : Fields.Redux this that)
                                       -> Redux (Extend v this) (Extend v that)


    public export
    data Redux : (this, that : Tupled type) -> Type where


      SimplifyTupleR : Redux this that
                    -> Redux (MkTuple this) (MkTuple that)


      -- Accessors
      SimplifyProj : {labels : Vect (S n) Ty}
                  -> {this, that : Tupled (TyTuple labels)}
                  -> {idx        : Fin (S n)}
                  -> Redux this that
                  -> Redux (Proj this idx) (Proj that idx)

      ReduceProj : {types  : Vect (S n) Ty}
                -> {fields : Fields types}
                -> {idx    : Fin (S n)}
                -> (values : Value fields)
                    -> Redux (Proj (MkTuple fields) idx)
                             (index idx fields)

namespace Progress


  public export
  data Progress : (term : Tupled type) -> Type where
      Done : Value term -> Progress term
      Step : {this,that : Tupled type} -> (step : Redux this that) -> Progress this

  namespace Fields
    public export
    data Progress : (fields : Fields types) -> Type where
      Done : (value : Value fields) -> Progress fields
      Step : {this,that : Fields types} -> (step  : Redux this that) -> Progress this

  mutual
    namespace Fields
      public export
      progress : (fields : Fields types) -> Progress fields
      progress (Singleton first) with (progress first)
        progress (Singleton first) | (Done x) = Done (SingletonV x)
        progress (Singleton first) | (Step prf) = Step (SimplifySingleton prf)


      progress (Extend next rest) with (progress next)
        progress (Extend next rest) | (Done x) with (progress rest)
          progress (Extend next rest) | (Done x) | (Done xs)  = Done (ExtendV x xs)
          progress (Extend next rest) | (Done x) | (Step prf) = Step (SimplifyExtendV x prf)

        progress (Extend next rest) | (Step prf) = Step (SimplifyExtend prf)

    public export
    progress : (term : Tupled type) -> Progress term

    progress (I x) = Done IV

    progress (MkTuple values) with (progress values)
      progress (MkTuple values) | (Done value)
        = Done (MkTupleV value)
      progress (MkTuple values) | (Step step)
        = Step (SimplifyTupleR step)

    progress (Proj tuple idx) with (progress tuple)
      progress (Proj (MkTuple fields) idx) | (Done (MkTupleV x)) = ?progress_rhs_6_rhs__1 -- Compiler Not Happy
--      progress (Proj tuple idx) | (Done term) = ?progress_rhs_6_rhs_ -- Compiler Happy when this is inserted as well
--      progress (Proj (MkTuple fields) idx) | (Done (MkTupleV x)) = Step (ReduceProj x) -- this is what it used to be
      progress (Proj tuple idx) | (Step step) = Step (SimplifyProj step)