-- Please, see the file LICENSE for copyright and license information.

module HFusion.Internal.HsSyn where

import Char(isDigit)
import List(union,(\\),nub)

-- | Abstract syntax tree for programs that "HFusion" can handle.
data Prog = Prog [Def]

-- | Representation for function definitions.
data Def = Defvalue Variable Term

getDefName :: Def -> Variable
getDefName (Defvalue v _) = v

getDefTerm :: Def -> Term
getDefTerm (Defvalue _ t) = t


-- | Representation of variables.
data Variable = Vuserdef String -- ^ Name found in the original program.
              | Vgen String Int -- ^ Generated identifier containing a prefix and an index.
  deriving Ord

instance Show Variable where
    show (Vuserdef name) = name
    show (Vgen p num) = p ++ show num

instance Eq Variable where
  Vuserdef v == Vuserdef v' = v==v'
  Vgen p i == Vgen p' i' = p==p' && i==i'
  v1 == v2 = show v1 == show v2


str2var [] = Vuserdef ""
str2var s | null ds = Vuserdef s
          | otherwise = Vgen (reverse p) ((read (reverse ds))::Int)
  where (ds,p) = break (not . isDigit) (reverse s)

varPrefix :: Variable -> String
varPrefix (Vgen p _) = p
varPrefix (Vuserdef s) = reverse . dropWhile isDigit . dropWhile (=='_'). reverse$ s

-- | Representation for Literals.
data Literal = Lstring String -- ^ String literals
               | Lint String  -- ^ Integer literals
               | Lchar Char   -- ^ Character literals
               | Lrat String  -- ^ Rational literals
    deriving (Eq)

-- | Representation for constructors.
type Constructor = String

-- | Representation for terms in programs handled by "HFusion".
data Term = Tvar Variable   -- ^ Variables
            | Tlit Literal  -- ^ Literals
            | Ttuple Bool [Term] -- ^ Tuples. The boolean argument tells if the tuple must be flattened
                                 --   when nested with others under an hylo application.
            | Tlamb Boundvar Term -- ^ Lambda expressions
            | Tlet Variable Term Term -- ^ Let expressions
            | Tcase Term [Pattern] [Term] -- ^ Case expressions
            | Tfapp Variable [Term] -- ^ Function application (saturated)
            | Tcapp Constructor [Term] -- ^ Constructor application
            | Tapp Term Term -- ^ General term application
            | Tbottom  -- ^ Undefined computation

            | Tif Term Term Term -- ^ If expressions, only used for pretty printing
            | Tpar Term -- Parenthesized expressions, to better handle associativity of infix operators
            | Thyloapp Variable Int [Term] (Maybe [Int]) Term -- ^ Hylo application, only used for inlining. In
                                                              -- @Thyloapp name recargsCount non-recargs recarg@ the argument
															  -- @recarg@ may be a tuple.
    deriving (Eq)


-- | Calculates arguments of a Thyloapp

thyloArgs :: Int -> [Term] -> Maybe [Int] -> Term -> [Term]
thyloArgs 1 ts pos t = insertElems (zip ts$ maybe [0..] id pos) [t]
thyloArgs 0 ts _   _ = insertElems (zip ts [0..]) []
thyloArgs _ ts pos t = insertElems (zip ts$ maybe [0..] id pos) (flatten t)
 where flatten (Ttuple True ts) = concat (map flatten ts)
       flatten t = [t]


insertElems :: [(a,Int)] -> [a] -> [a]
insertElems = insert 0
  where insert _ xs [] = map fst xs 
        insert _ [] as = as
        insert i xs@((x,ix):xss) as@(a:ass)
                 | ix<=i = x : insert (i+1) xss as
                 | otherwise = a : insert (i+1) xs ass

applyFst f (a,b) = (f a,b)


bv2pat (Bvar v)=Pvar v
bv2pat (Bvtuple _ vs)=Ptuple (map bv2pat vs)

tapp (Tvar v) t = Tfapp v [t]
tapp (Tfapp v []) t = Tfapp v [t]
tapp t1 t2 = Tapp t1 t2

ttuple [a] = a
ttuple as = Ttuple False as

ptuple [a] = a
ptuple as = Ptuple as

bvtuple [a] = a
bvtuple as = Bvtuple False as


-- | Representation of bound variables in lambda expressions.
data Boundvar = Bvar Variable -- Variables
              | Bvtuple Bool [Boundvar] -- ^ Bound variable tuples. Uses the boolean value like in 'Ttuple'.
                                        --   but when bounding input variables of hylomorphisms.
    deriving (Eq)

-- | Representation of patterns
data Pattern = Pvar Variable  -- ^ Variables
               | Ptuple [Pattern] -- ^ Tuple patterns
               | Pcons Constructor [Pattern] -- ^ Constructor application patterns
               | Plit Literal -- ^ Literals
               | Pas Variable Pattern -- ^ \@\-pattern
    deriving (Eq)

pany = Pvar (Vuserdef "_")


-- Representación de functores
-- Fue discutida, pero aún podría sufrir cambios.
newtype Func = Fsum [Fprod]
          deriving (Show,Eq)
type Fprod = (Int,Int)


-- | Operation for collecting free variables without repetitions.

class Vars a where
  vars :: a -> [Variable]

instance Vars Variable where
  vars a = [a]

instance Vars Boundvar where
  vars (Bvar v) = [v]
  vars (Bvtuple _ vs) = vars vs

instance Vars Pattern where
  vars p@(Pvar v) | p/=pany = [v]
                  | otherwise = []
  vars (Ptuple ps) = concat (map vars ps)
  vars (Pcons _ ps) = concat (map vars ps)
  vars (Plit _) = []
  vars (Pas v p) = v:vars p
 -- vars p = error "vars Pattern: not defined" -- ++ (not_Defined_For_Applied_Pattern p)

instance Vars a => Vars [a] where
  vars = concat.map vars

instance (Vars a, Vars b) => Vars (Either a b) where
  vars = either vars vars

instance Vars Term where
  vars (Tvar v) = [v]
  vars (Ttuple _ ps) = foldr union [] (map vars ps)
  vars (Tcapp _ ps) = foldr union [] (map vars ps)
  vars (Tlit _) = []
  vars (Tfapp fn ps) = foldr union [fn] (map vars ps)
  vars (Tapp t1 t2) = union (vars t1) (vars t2)
  vars (Tlamb bv t) = vars t \\ vars bv
  vars (Tlet v t0 t1) = union (vars t0) (vars t1 \\ [v])
  vars (Tpar t) = vars t
  vars (Tif t0 t1 t2) = union (vars t0) (union (vars t1) (vars t2))
  vars (Tcase t ps ts) = foldr union (vars t) (zipWith (\pi ti ->vars ti \\ vars pi) ps ts)
  vars Tbottom = []
  vars (Thyloapp v _ ts _ t) = nub (v:(vars ts++vars t))

instance Vars Def where
  vars (Defvalue v t) = filter (v/=)$ vars t

-- | Operations for obtaining bound variables.

class VarsB a where
  varsB :: a -> [Variable]

instance (VarsB a) => (VarsB [a]) where
 varsB x = concat$ map varsB x

instance VarsB Term where
  varsB (Tvar _) = []
  varsB (Ttuple _ ps) = concat (map varsB ps)
  varsB (Tcapp _ ps) = concat (map varsB ps)
  varsB (Tlit _) = []
  varsB (Tfapp _ ps) = concat (map varsB ps)
  varsB (Tapp t1 t2) = varsB t1 ++ varsB t2
  varsB (Tlamb bv t) = varsB t ++ vars bv
  varsB (Tlet v t0 t1) = v : (varsB t0 ++ varsB t1)
  varsB (Tif t0 t1 t2) = varsB t0 ++ varsB t1 ++ varsB t2
  varsB (Tpar t) = varsB t
  varsB (Tcase t ps ts) = varsB t ++ concat (zipWith (\pi ti ->varsB ti ++ vars pi) ps ts)
  varsB Tbottom = []
  varsB (Thyloapp _ _ ts _ t) = varsB ts++varsB t

instance (VarsB a, VarsB b) => VarsB (Either a b) where
  varsB = either varsB varsB


-- | Alpha conversion.

class AlphaConvertible a where
  -- The [Variable] is the list of variables in scope (i.e. which can be replaced).
  alphaConvert :: [Variable] -> [(Variable, Variable)] -> a -> a

instance AlphaConvertible Variable where
  alphaConvert sc lvars v = if elem v sc then maybe v id $ lookup v lvars else v

instance AlphaConvertible Term where
  alphaConvert sc ss t@(Tvar v) = if elem v sc then maybe t Tvar $ lookup v ss else t
  alphaConvert sc ss (Tlamb bv t) = Tlamb (alphaConvert sc ss bv) (alphaConvert (sc++vars bv) ss t)
  alphaConvert sc ss (Tlet v t0 t1) = case lookup v ss of
                                      Just valor -> Tlet valor (alphaConvert (v:sc) ss t0) (alphaConvert (v:sc) ss t1)
                                      Nothing ->  Tlet v (alphaConvert sc ss t0) (alphaConvert sc ss t1)
  alphaConvert sc ss (Tcase t0 ps ts) = Tcase (alphaConvert sc ss t0) (map (alphaConvert sc ss) ps) (zipWith alphaConvert' ps ts)
    where alphaConvert' p t = alphaConvert (sc++vars p) ss t
  alphaConvert _ _ t@(Tlit _) = t
  alphaConvert _ _ t@Tbottom = t
  alphaConvert sc ss (Ttuple b ts) = Ttuple b$ map (alphaConvert sc ss) ts
  alphaConvert sc ss (Tfapp v ts) = case lookup v ss of
             Just valor -> foldl Tapp (Tvar valor) (map (alphaConvert sc ss) ts)
             Nothing -> Tfapp v (map (alphaConvert sc ss) ts)
  alphaConvert sc ss (Tcapp cons ts) = Tcapp cons (map (alphaConvert sc ss) ts)
  alphaConvert sc ss (Tapp t0 t1) = Tapp (alphaConvert sc ss t0) (alphaConvert sc ss t1)
  alphaConvert sc ss (Thyloapp v i ts pos t) = case lookup v ss of
             Just valor -> foldl Tapp (Tvar valor) (map (alphaConvert sc ss) (thyloArgs i ts pos t))
             Nothing -> Thyloapp v i (map (alphaConvert sc ss) ts) pos (alphaConvert sc ss t)
  alphaConvert _ _ _ = error$ "alphaConvert: unexpected term"

instance (AlphaConvertible a, AlphaConvertible b) => AlphaConvertible (Either a b) where
  alphaConvert sc lvars = either (Left . alphaConvert sc lvars) (Right . alphaConvert sc lvars)

instance (AlphaConvertible a) => (AlphaConvertible [a]) where
 alphaConvert sc lvars x = map (alphaConvert sc lvars) x


instance AlphaConvertible Pattern where
  alphaConvert _ lvars t@(Pvar v) = maybe t Pvar $ lookup v lvars
  alphaConvert sc lvars (Ptuple ps) = Ptuple (map (alphaConvert sc lvars) ps)
  alphaConvert sc lvars (Pcons c ps) = Pcons c (map (alphaConvert sc lvars) ps)
  alphaConvert _ _ t@(Plit _) = t
  alphaConvert sc lvars (Pas v p) = Pas (maybe v id$ lookup v lvars) (alphaConvert sc lvars p)

instance AlphaConvertible Boundvar where
  alphaConvert _ lvars b@(Bvar v) = maybe b Bvar $ lookup v lvars
  alphaConvert sc lvars (Bvtuple b vs) = Bvtuple b$ alphaConvert sc lvars vs