{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances, 
NoMonomorphismRestriction, FlexibleContexts, 
FunctionalDependencies, ScopedTypeVariables, 
TypeOperators,

OverlappingInstances,
IncoherentInstances #-}


module Control (Control(..), TypeOf(..)
               ,app1,app2,app3,app4
               ,lam1,lam2,lam3,lam4

               ) where

import Data
import Struct
import Type

type VarName = String

{- Control.
First order language with lexical scope and tail calls, no recursion.

a,b,... values
t       value, global return type
f,g,... functions

This turns out to be an embedding of the simply typed lambda calculus
with constraints on reference and return types.

Control uses the Struct class, which abstracts data structures.

-}

class Data m r => Control m r | r -> m,
                                m -> r
                                where
  
  -- Conditional branching
  ifte  :: DataWord t
           => r Tbool
           -> m (r t) 
           -> m (r t)
           -> m (r t)
           
  -- Recursive function definitions (loops)
  letrec :: (r f -> m (r f)) -- body with open recursion
            -> (r f -> m (r t)) -- scope with functions defined
            -> m (r t)
          
  -- Function abstraction and application.  The language is first
  -- order so we need a way to compose multiple arguments into one.
  -- We don't care about the return type of functions since we only
  -- use CPS / tail calls.
  
  -- StructVar is for variable name generation in Code.  FIXME: can it
  -- be moved elsewhere?
  
  lam :: (DataWord s,
          StructVar sr,
          Struct r s sr) 
         => (sr -> m (r t))
         -> m (r (s -> m t))
  
  app    :: (DataWord s,
             Struct r s sr) 
            => r (s -> m t)
            -> sr -> m (r t)
             
  -- Application exit.  I.e. for embedding in C we need a single
  -- return value to pass to the parent continuation.
  ret :: r a -> m (r a)
  
  -- Toplevel definition.  FIXME: This probably shouldn't be part of
  -- Control.  Maybe use a separate Toplevel class?
  def :: TypeOf (r t) => String -> m (r t) -> m (r ())




-- TODO: For now these will work, but try to abstract these in a class.

app1 f a1          = app f (L a1)
app2 f a1 a2       = app f ((,) (L a1) (L a2))
app3 f a1 a2 a3    = app f ((,) (L a1) ((,) (L a2) (L a3)))
app4 f a1 a2 a3 a4 = app f ((,) (L a1) ((,) (L a2) ((,) (L a3) (L a4))))

lam1 f = lam $ \(L a1) -> f a1
lam2 f = lam $ \((,) (L a1) (L a2)) -> f a1 a2
lam3 f = lam $ \((,) (L a1) ((,) (L a2) (L a3))) -> f a1 a2 a3
lam4 f = lam $ \((,) (L a1) ((,) (L a2) ((,) (L a3) (L a4)))) -> f a1 a2 a3 a4




-- Compilation requires a standard way to convert a term to a run-time
-- representation of its type.  The main point of this class is to
-- handle the representation (r) wrapping of DataWord, and provide a
-- way to get the return type of Control functions (_lambda).

-- These are overlapping instances, but that seems to work OK (for now).

class TypeOf t where typeOf :: t -> Type

instance DataWord t => TypeOf (r t) where
  typeOf _ = primType (undefined :: t)

instance (Data m r, TypeOf (r o)) => TypeOf (r (i -> m o)) where 
  typeOf _ = typeOf (undefined :: (r o))