{-|
    Module      :  Functional.Language
    Copyright   :  (c) Miguel Vilaça 2007

    Maintainer  :  jmvilaca@di.uminho.pt
    Stability   :  experimental
    Portability :  portable


    Small Functional Language

-}
module Functional.Language where

import Data.List

import Common


type Variable = String

data CallBy = Value | Name | Need deriving (Eq, Show)

data FuncLang = Var Variable  -- 1 (precedences)
	      | Abst Variable FuncLang -- 7
	      | Appl FuncLang FuncLang -- 10
	      | TT -- 1
	      | FF -- 1
	      | IterBool FuncLang FuncLang FuncLang -- 5
	      | Zero -- 1
	      | Succ FuncLang -- 3
	      | IterNat Variable FuncLang FuncLang FuncLang -- 5
	      | Nil -- 1
	      | Cons FuncLang FuncLang -- 3
	      | IterList Variable Variable FuncLang FuncLang FuncLang -- 5
	      deriving (Eq)

-- | Default names and expressions for 'FuncLang' terms.
listLangConstructors :: [(String, FuncLang)]
listLangConstructors =
	[ ("Abstraction"  , Abst "x" (Var "t"))
	, ("Application"  , Appl (Var "t") (Var "u"))
	, ("True"	  , TT)
	, ("False"	  , FF)
	, ("If then else" , IterBool (Var "V") (Var "F") (Var "b"))
	, ("0"		  , Zero)
	, ("successor"	  , Succ (Var "t"))
	, ("Nat iterator" , IterNat "x" (Var "S") (Var "Z") (Var "t"))
	, ("[]"		  , Nil)
	, (":"		  , Cons (Var "H") (Var "T"))
	, ("List iterator", IterList "x" "y" (Var "C") (Var "N") (Var "t"))
	]

instance Show FuncLang where
 -- precedence 9 is a special one; means that it is inside an abstraction
 showsPrec 9 (Abst v t) =
		showChar ','
		. showString v
		. showsPrec 9 t
 showsPrec 9 x = showChar ']' . showsPrec 0 x
 showsPrec d (Abst v t) =
		showParen (d > 7) $
		showChar '['
		. showString v
		. showsPrec 9 t
 -- elements of precedence 1; those never surrounded by parenthesis
 showsPrec _ (Var x) = showString x
 showsPrec _ TT      = showString "tt"
 showsPrec _ FF      = showString "ff"
 showsPrec _ Zero    = showString "0"
 showsPrec _ Nil     = showString "nil"
 -- elements of precedence 3
 showsPrec _ (Succ n) =
		showString "suc("
		. showsPrec 0 n
		. showChar ')'
 showsPrec _ (Cons h t) =
		showString "cons("
		. showsPrec 0 h
		. showChar ','
		. showsPrec 0 t
		. showChar ')'
 -- elements of precedence 5
 showsPrec _ (IterBool v f b) =
		showString "iterbool("
		. showsPrec 0 v
		. showChar ','
		. showsPrec 0 f
		. showChar ','
		. showsPrec 0 b
		. showChar ')'
 showsPrec _ (IterNat x s z n) =
		showString "iternat("
		. showsPrec 0 (Abst x s)
		. showChar ','
		. showsPrec 0 z
		. showChar ','
		. showsPrec 0 n
		. showChar ')'
 showsPrec _ (IterList h t c n l) =
		showString "iterlist("
		. showsPrec 0 (Abst h $ Abst t c)
		. showChar ','
		. showsPrec 0 n
		. showChar ','
		. showsPrec 0 l
		. showChar ')'
 -- elements of precedence 10
 showsPrec d (Appl u v) =
		showParen (d > 10) $
		showsPrec 11 u
		. showChar ' '
		. showsPrec 11 v

-- | Show iter_TYPE symbols.
showAgent :: FuncLang -> String
showAgent t@(IterBool v f (Var ""))     = show t
showAgent t@(IterNat x s z (Var ""))    = show t
showAgent t@(IterList h r c n (Var "")) = show t
showAgent _ = error "unexpected functional term here"

cata :: (Variable -> r) -- ^ Var
     -> (Variable -> r -> r) -- ^ Abstraction
     -> (r -> r -> r) -- ^ Application
     -> r -- ^ True
     -> r -- ^ False
     -> (r -> r -> r -> r) -- ^ IterBool
     -> r -- ^ Zero
     -> (r -> r) -- ^ Succ
     -> (Variable -> r -> r -> r -> r) -- ^ IterNat
     -> r -- ^ Nil
     -> (r -> r -> r) -- ^ Cons
     -> (Variable -> Variable -> r -> r -> r -> r) -- ^ IterList
     -> FuncLang -- ^ term
     -> r -- ^ result
cata fVar fAbst fAppl fTT fFF fIB fZ fS fIN fN fC fIL = cata'
 where cata' term =
	    case term of
	Var var 		    -> fVar var
	Abst var t 		    -> fAbst var (cata' t)
	Appl t1 t2 		    -> fAppl (cata' t1) (cata' t2)
	TT 			    -> fTT
	FF 			    -> fFF
	IterBool t1 t2 t3 	    -> fIB (cata' t1) (cata' t2) (cata' t3)
	Zero 			    -> fZ
	Succ t 			    -> fS (cata' t)
	IterNat var t1 t2 t3 	    -> fIN var (cata' t1) (cata' t2) (cata' t3)
	Nil 			    -> fN
	Cons t1 t2 		    -> fC (cata' t1) (cata' t2)
	IterList var1 var2 t1 t2 t3 -> fIL var1 var2 (cata' t1) (cata' t2) (cata' t3)

-- | Dummy variable
eVar = Var ""

-- | Collect all the symbols in a term.
-- The possible symbols are:
--   *  @ IterBool t1 t2 (Var \"\") @
--   *  @ IterNat v t1 t2 (Var \"\") @
--   *  @ IterList v1 v2 t1 t2 (Var \"\") @
listIteratorSymbols,listSymbs :: FuncLang -> [FuncLang]
listIteratorSymbols = listSymbs

listSymbs term =
    case term of
	Var _var 		    -> []
	Abst _var t 		    -> listSymbs t
	Appl t1 t2 		    -> (listSymbs t1) `join` (listSymbs t2)
	TT 			    -> []
	FF 			    -> []
	IterBool t1 t2 t3 	    -> [IterBool t1 t2 eVar] `join` (listSymbs t1) `join` (listSymbs t2) `join` (listSymbs t3)
	Zero 			    -> []
	Succ t 			    -> listSymbs t
	IterNat var t1 t2 t3 	    -> [IterNat var t1 t2 eVar] `join` (listSymbs t1) `join` (listSymbs t2) `join` (listSymbs t3)
	Nil 			    -> []
	Cons t1 t2 		    -> (listSymbs t1) `join` (listSymbs t2)
	IterList var1 var2 t1 t2 t3 -> [IterList var1 var2 t1 t2 eVar] `join` (listSymbs t1) `join` (listSymbs t2) `join` (listSymbs t3)
  where join = union

-- | Give some sequential names to symbols.
giveNames :: [FuncLang] -> [(FuncLang, String)]
giveNames = snd . mapAccumL f 1
  where f acc x = (acc+1,(x,"Iter_" ++ show acc))


-- | List the free variables of a term; the result is a set.
freeVars :: FuncLang -> [String]
freeVars = cata singleton delete union [] [] fIB [] id fIN [] union fIL
  where
	fIB r1 r2 r3 = r1 `union` r2 `union` r3
	fIN v r1 r2 r3 = (delete v r1) `union` r2 `union` r3
	fIL x y r1 r2 r3 = ( r1\\[x,y] ) `union` r2 `union` r3

-- | Special lookup function for iterators with an equality.
lookupIterName :: FuncLang -> [(FuncLang, String)] -> Maybe String
lookupIterName term [] = Nothing
lookupIterName term ((term2,str):xs) | term `equal` term2 = Just str
				     | otherwise = lookupIterName term xs
  where
	equal :: FuncLang -> FuncLang -> Bool
	equal (IterBool v1 f1 _) (IterBool v2 f2 _) = v1==v2 && f1==f2
	equal (IterNat x1 s1 z1 _) (IterNat x2 s2 z2 _) = x1==x2 && s1==s2 && z1==z2
	equal (IterList x1 y1 c1 n1 _) (IterList x2 y2 c2 n2 _) = x1==x2 && y1==y2 && c1==c2 && n1==n2
	equal _ _ = False