module HFusion.Internal.HsSyn where
import Char(isDigit)
import List(union,(\\),nub)
data Prog = Prog [Def]
data Def = Defvalue Variable Term
getDefName :: Def -> Variable
getDefName (Defvalue v _) = v
getDefTerm :: Def -> Term
getDefTerm (Defvalue _ t) = t
data Variable = Vuserdef String
| Vgen String Int
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
data Literal = Lstring String
| Lint String
| Lchar Char
| Lrat String
deriving (Eq)
type Constructor = String
data Term = Tvar Variable
| Tlit Literal
| Ttuple Bool [Term]
| Tlamb Boundvar Term
| Tlet Variable Term Term
| Tcase Term [Pattern] [Term]
| Tfapp Variable [Term]
| Tcapp Constructor [Term]
| Tapp Term Term
| Tbottom
| Tif Term Term Term
| Tpar Term
| Thyloapp Variable Int [Term] (Maybe [Int]) Term
deriving (Eq)
thyloArgs :: Int -> [Term] -> Maybe [Int] -> Term -> [Term]
thyloArgs 1 ts pos t = insertElems (zip ts$ maybe [0..] id pos) [t]
thyloArgs 0 ts pos t = insertElems (zip ts [0..]) []
thyloArgs i 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 i xs [] = map fst xs
insert i [] 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
data Boundvar = Bvar Variable
| Bvtuple Bool [Boundvar]
deriving (Eq)
data Pattern = Pvar Variable
| Ptuple [Pattern]
| Pcons Constructor [Pattern]
| Plit Literal
| Pas Variable Pattern
deriving (Eq)
pany = Pvar (Vuserdef "_")
newtype Func = Fsum [Fprod]
deriving (Show,Eq)
type Fprod = (Int,Int)
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
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 i ts _ t) = nub (v:(vars ts++vars t))
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 _ i ts _ t) = varsB ts++varsB t
instance (VarsB a, VarsB b) => VarsB (Either a b) where
varsB = either varsB varsB
class AlphaConvertible a where
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 sc ss t@(Tlit _) = 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 sc ss t = 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 sc 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 sc lvars t@(Plit l) = t
alphaConvert sc lvars (Pas v p) = Pas (maybe v id$ lookup v lvars) (alphaConvert sc lvars p)
instance AlphaConvertible Boundvar where
alphaConvert sc lvars b@(Bvar v) = maybe b Bvar $ lookup v lvars
alphaConvert sc lvars (Bvtuple b vs) = Bvtuple b$ alphaConvert sc lvars vs