module PGF.Tree
( Tree(..),
tree2expr, expr2tree,
prTree
) where
import PGF.CId
import PGF.Expr hiding (Tree)
import Data.List as List
data Tree =
Abs [(BindType,CId)] Tree
| Var CId
| Fun CId [Tree]
| Lit Literal
| Meta !MetaId
deriving (Eq, Ord)
tree2expr :: Tree -> Expr
tree2expr = tree2expr []
where
tree2expr ys (Fun x ts) = foldl EApp (EFun x) (List.map (tree2expr ys) ts)
tree2expr ys (Lit l) = ELit l
tree2expr ys (Meta n) = EMeta n
tree2expr ys (Abs xs t) = foldr (\(b,x) e -> EAbs b x e) (tree2expr (List.map snd (reverse xs)++ys) t) xs
tree2expr ys (Var x) = case List.lookup x (zip ys [0..]) of
Just i -> EVar i
Nothing -> error "unknown variable"
expr2tree :: Expr -> Tree
expr2tree e = abs [] [] e
where
abs ys xs (EAbs b x e) = abs ys ((b,x):xs) e
abs ys xs (ETyped e _) = abs ys xs e
abs ys xs e = case xs of
[] -> app ys [] e
xs -> Abs (reverse xs) (app (map snd xs++ys) [] e)
app xs as (EApp e1 e2) = app xs ((abs xs [] e2) : as) e1
app xs as (ELit l)
| List.null as = Lit l
| otherwise = error "literal of function type encountered"
app xs as (EMeta n)
| List.null as = Meta n
| otherwise = error "meta variables of function type are not allowed in trees"
app xs as (EAbs _ x e) = error "beta redexes are not allowed in trees"
app xs as (EVar i) = if length xs > i then Var (xs !! i) else Meta i
app xs as (EFun f) = Fun f as
app xs as (ETyped e _) = app xs as e
prTree :: Tree -> String
prTree = showExpr [] . tree2expr