{-# OPTIONS -XTemplateHaskell -XMultiParamTypeClasses -XTypeOperators #-}
import UpdatableViewStub 
import Control.Arrow
import RIC

spec List a = Nil | Cons a (List a) deriving (Show,Eq) where
    index :: Int -> List a -> a 
    index 1 (Cons a Nil)  = a 
    index n (Cons _ x)    = index (n-1) x
    
    enrich :: [a] -> List a 
    enrich []    = Nil
    enrich (a:x) = Cons a (enrich x)

impl STree a = SEmp | SLeaf a | STree Int (STree a) (STree a) deriving (Show,Eq) where 
    index :: Int -> STree a -> a
    index 1 (SLeaf a) = a 
    index n (STree s lt rt) | n > ls    = index (n - ls) rt 
                            | otherwise = index n lt 
        where 
          ls = getSize lt 
          getSize (STree s _ _) = s
          getSize (SLeaf _)     = 1 

    enrich :: [a] -> STree a
    enrich x = f (length x) x 
       where 
         f 1 [x] = SLeaf x 
         f n x = let (a,b) = splitAt ls x 
                 in  STree n (f ls a) (f rs b)
             where ls = n `div` 2 
                   rs = n - ls 

abstractedBy
    view = $(foldT ''STree) ( nilB <||> wrapB <||> (ignoreFstB (getSize') >>>> appendB) ) >>>> foldListB (nilB' <||> consB')
           -- >>>> totalB myenrich myunenrich
           {- Clearly this fuunction is not written in RINV. 
              I failed to find how to write the function satisfying the joinly-surjective condition. -}
        where 
          nilB   = $(toC '[])
          wrapB  = introUnitRB >>>> (idB <**> nilB) >>>> $(toC '(:))
          nilB'  = $(toC 'Nil)
          consB' = $(toC 'Cons)
          getSize' (x,y) = length x + length y 




answerQueries is x = 
    let v = enrich x 
    in map (\i -> index i v) is