{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances, 
NoMonomorphismRestriction, FlexibleContexts, ExistentialQuantification, 
FunctionalDependencies, ScopedTypeVariables, UndecidableInstances,
TypeOperators, OverlappingInstances #-}

module Struct 
               
       {- Arguments are represented as type classes.
              Struct:      main interface, parameterized by
              StructRepr:  datastructure representation (binary trees)
              StructPrim:  primitive data representation

          HOAS can use the (,) and L types to construct data
          structures that can be passed as function arguments. -}

       (Struct(..)
             
       ,StructRepr(..)  -- class (TL type)
       ,L(..)           -- types (TL constructors)
        
        -- Note: there's no separate Cons or Nil.  We use (,) and ()
        -- because the Arrow class uses (,) as a hard-coded binary
        -- product type, and we use () for lifting pure functions to
        -- stateful operations.
        
       ,StructVar(..)
       ) where

type VarName = String

{- Type parameter naming scheme:
   r s  representation of structure  (of type)
   sr   sturecture of representation (of type) -}   


-- The structure data type is abstract.
class (StructRepr r)
      => Struct r s sr | sr -> r s, 
                         r s -> sr, 
                         r sr -> s where

  -- Commute representation and structuring, 
  -- i.e. (r (L a), (r (L b), r (L c))) <-> r (L a, (L b, L c))
  repStruct   :: sr -> r s
  unrepStruct :: r s -> sr


-- While the Struct class is abstract, we only implement binary trees
-- in terms of the arity 0,1,2 structuring operations provided by
-- user. We reuse () and (,) but need to provide an explicit leaf type
-- to avoid instance ambiguities.

data L t = L {structL :: t}


-- Building blocks for binary trees: morphisms between commutation of
-- representation and structuring.

-- The real/phantom refers to how this is used in the Code
-- reprsentation.

class StructRepr r where
  --        real           phantom          
  rep0   :: ()          -> r ()
  rep1   :: L (r a)     -> r (L a)
  rep2   :: (r a, r b)  -> r (a, b)
  
  --        phantom        real
  unrep0  :: r ()       -> ()
  unrep1  :: r (L a)    -> L (r a)
  unrep2  :: r (a, b)   -> (r a, r b)


-- Use the StructRepr class to implement binary tree instances.

-- 2: pairs
instance (Struct r s1 sr1,
          Struct r s2 sr2)
         => Struct r (s1, s2) (sr1, sr2) where
                  
  repStruct (sr1, sr2) =
    rep2 $ (repStruct sr1, repStruct sr2)
  
  unrepStruct sr12 = 
    (unrepStruct sr1, unrepStruct sr2) where
      (sr1, sr2) = unrep2 sr12
  
-- 1: leafs
instance StructRepr r => Struct r (L t) (L (r t)) where  
  repStruct    = rep1
  unrepStruct  = unrep1

-- 0: null nodes
instance StructRepr r => Struct r () () where  
  repStruct    = rep0
  unrepStruct  = unrep0
  
  



{- Structured variable generation.  User provides atomic variable
generation for the L constructor while we implement binary product and
unit.  The Maybe argument is a template, i.e. if it already contains
variable references, those can be reused. -}

class StructVar sr where
  structVar :: String -> Int -> Maybe sr -> (Int, sr)
  structSize :: sr -> Int
  structSize _ = 1
  
instance (StructVar sr1,
          StructVar sr2) 
         => StructVar (sr1, sr2) where
  structVar = sv where
    sv p n0 Nothing = (n2, (sr1, sr2)) where
      (n1, sr1) = structVar p n0 Nothing
      (n2, sr2) = structVar p n1 Nothing
    sv p n0 (Just (sr1', sr2')) = (n2, (sr1, sr2)) where
      (n1, sr1) = structVar p n0 $ Just sr1'
      (n2, sr2) = structVar p n1 $ Just sr2'
  structSize _ = structSize (undefined :: sr1) +
                 structSize (undefined :: sr2)

instance StructVar () where
  structVar p n _ = (n, ())
  structSize _ = 0