{-# OPTIONS -fglasgow-exts #-}

module Haskell where

-- A module for providing Haskell syntax for the lifting operation.

import Lift
import List(intersperse)
import Maybe(fromJust)

class Haskell a where
    haskell :: a -> String
instance Haskell Type where
    haskell (x `TypeArrow` y) = 
        "("++(haskell x)++" -> "++(haskell y)++")"
    haskell (x `TypeApply` y) = 
        "("++(haskell x)++" "++(haskell y)++")"
    haskell (Forall v k t) = 
        "(forall ("++(haskell v)++" :: "++(haskell k)++") . "++(haskell t)++")"
    {- The below is not valid Haskell; lambda lifting must be done to make it 
       so. However, when transforming valid Haskell data types, type lambdas
       only occur at universally quantified types, which are rare.
     -}
    haskell (Lambda v k t) = 
        "(/\\ ("++(haskell v)++" :: "++(haskell k)++") . "++(haskell t)++")"
    haskell (Name d) = haskell d
    haskell (Var v) = haskell v
instance Haskell Variable where
    haskell (Variable v) = v
instance Haskell Data where
    haskell (Data s) = s
    haskell (LiftData d) = (haskell d)++"Lift"
    haskell (Tag c) = (haskell c)++"Tag"
instance Haskell Constructor where
    haskell (Constructor s) = s
    haskell (LiftConstructor c) = (haskell c)++"Lift"
instance Haskell ConstructorType where
    haskell (ConstructorType vsks ts d rs) = 
        {- Type variables in constructor signatures are implicitly universally
           quantified in Haskell, so we don't need this line, though it would
           be harmless to leave in.
         -}
        -- (concatMap (\x -> "forall "++(haskell x)++" . ") (fst $ unzip vsks)) ++
        (concat $ intersperse " -> " 
                    ((map haskell ts) 
                     ++ [(haskell d)++" "++(concat $ intersperse " " (map haskell rs))]))
instance Haskell RestrictedConstructorType where
    haskell (RestrictedConstructorType vsks ts s rs) = 
        {- Type variables in constructor signatures are implicitly universally
           quantified in Haskell, so we don't need this line, though it would
           be harmless to leave in.
         -}
        -- (concatMap (\x -> "forall "++(haskell x)++" . ") (fst $ unzip vsks)) ++
        (concat $ intersperse " -> " 
                    ((map haskell ts) 
                     ++ [s++" "++(concat $ intersperse " " (map haskell rs))]))
instance Haskell Context where
    haskell c = haskell' c c 
        {- We keep two copies of the context so we can traverse through one 
           and save the other for looking up names, which may appear in any 
           order.
         -}
        where haskell' c Empty = ""
              haskell' c (Typed _ _ r) = haskell' c r
              haskell' c (Kinded s k r) = 
                  let ns = restrictedConstructorsOf s c
                  in "data "++s++(
                     if null ns 
                     {- If there are no constructors, GHC does not allow GADT-style syntax.
                        We simply list the parameters and expect kind inference to get the
                        kinds right.
                      -}
                     then " "++(concat $ intersperse " " $ take (arity k) (map (('v':).show) [0..]))
                     else " :: "++(haskell k)++" where \n    "
                          ++(concat $ intersperse "\n    " (map (\x -> (fst x)++" :: "++(haskell (snd x))) ns)))
                     -- Check if the datatype admits equality before lifting it
                     ++(if singleton c [] (Name (Data s)) 
                        then "\ndata "++(haskell (LiftData (Data s)))++
                             (if null ns
                              then " "++(concat $ intersperse " " $ take (arity (liftKind k)) (map (('v':).show) [0..]))
                              else " :: "++(haskell (liftKind k))++" where \n    "
                                   ++(concat $ intersperse "\n    " 
                                       (map (\x -> (haskell (fst x))++" :: "++(haskell (snd x))) 
                                            {- This fromJust is a shame: It might be better if the
                                               test for whether a datatype admits equality returned
                                               Maybe [(Constructor, ConstructorType)], but that would
                                               make the code look different than the formalism in 
                                               the paper.
                                             -}
                                            (fromJust $ constructorsOf (LiftData (Data s)) c)))++"\n"
                                   ++(concat $ intersperse "\n" (map (\x -> "data "++(haskell (Tag (Constructor (fst x))))
                                   ++" "++((concat $ intersperse " " $ take (length $ arguments $ snd x) (map (('v':).show) [0..])))) ns)))
                       else "")
                     ++"\n"++(haskell' c r)

instance Haskell Kind where
    haskell Star = "*"
    haskell (k1 `KindArrow` k2) = "("++(haskell k1)++" -> "++(haskell k2)++")"