module PGF.Tree 
         ( Tree(..),
           tree2expr, expr2tree,
           prTree
         ) where

import PGF.CId
import PGF.Expr hiding (Tree)

--import Data.Char
import Data.List as List
--import Control.Monad
--import qualified Text.PrettyPrint as PP
--import qualified Text.ParserCombinators.ReadP as RP

-- | The tree is an evaluated expression in the abstract syntax
-- of the grammar. The type is especially restricted to not
-- allow unapplied lambda abstractions. The tree is used directly 
-- from the linearizer and is produced directly from the parser.
data Tree = 
   Abs [(BindType,CId)] Tree        -- ^ lambda abstraction. The list of variables is non-empty
 | Var CId                          -- ^ variable
 | Fun CId [Tree]                   -- ^ function application
 | Lit Literal                      -- ^ literal
 | Meta {-# UNPACK #-} !MetaId      -- ^ meta variable
  deriving (Tree -> Tree -> Bool
(Tree -> Tree -> Bool) -> (Tree -> Tree -> Bool) -> Eq Tree
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Tree -> Tree -> Bool
$c/= :: Tree -> Tree -> Bool
== :: Tree -> Tree -> Bool
$c== :: Tree -> Tree -> Bool
Eq, Eq Tree
Eq Tree
-> (Tree -> Tree -> Ordering)
-> (Tree -> Tree -> Bool)
-> (Tree -> Tree -> Bool)
-> (Tree -> Tree -> Bool)
-> (Tree -> Tree -> Bool)
-> (Tree -> Tree -> Tree)
-> (Tree -> Tree -> Tree)
-> Ord Tree
Tree -> Tree -> Bool
Tree -> Tree -> Ordering
Tree -> Tree -> Tree
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Tree -> Tree -> Tree
$cmin :: Tree -> Tree -> Tree
max :: Tree -> Tree -> Tree
$cmax :: Tree -> Tree -> Tree
>= :: Tree -> Tree -> Bool
$c>= :: Tree -> Tree -> Bool
> :: Tree -> Tree -> Bool
$c> :: Tree -> Tree -> Bool
<= :: Tree -> Tree -> Bool
$c<= :: Tree -> Tree -> Bool
< :: Tree -> Tree -> Bool
$c< :: Tree -> Tree -> Bool
compare :: Tree -> Tree -> Ordering
$ccompare :: Tree -> Tree -> Ordering
$cp1Ord :: Eq Tree
Ord)

-----------------------------------------------------
-- Conversion Expr <-> Tree
-----------------------------------------------------

-- | Converts a tree to expression. The conversion
-- is always total, every tree is a valid expression.
tree2expr :: Tree -> Expr
tree2expr :: Tree -> Expr
tree2expr = [CId] -> Tree -> Expr
tree2expr []
  where
    tree2expr :: [CId] -> Tree -> Expr
tree2expr [CId]
ys (Fun CId
x [Tree]
ts) = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp (CId -> Expr
EFun CId
x) ((Tree -> Expr) -> [Tree] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
List.map ([CId] -> Tree -> Expr
tree2expr [CId]
ys) [Tree]
ts) 
    tree2expr [CId]
ys (Lit Literal
l)    = Literal -> Expr
ELit Literal
l
    tree2expr [CId]
ys (Meta MetaId
n)   = MetaId -> Expr
EMeta MetaId
n
    tree2expr [CId]
ys (Abs [(BindType, CId)]
xs Tree
t) = ((BindType, CId) -> Expr -> Expr)
-> Expr -> [(BindType, CId)] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(BindType
b,CId
x) Expr
e -> BindType -> CId -> Expr -> Expr
EAbs BindType
b CId
x Expr
e) ([CId] -> Tree -> Expr
tree2expr (((BindType, CId) -> CId) -> [(BindType, CId)] -> [CId]
forall a b. (a -> b) -> [a] -> [b]
List.map (BindType, CId) -> CId
forall a b. (a, b) -> b
snd ([(BindType, CId)] -> [(BindType, CId)]
forall a. [a] -> [a]
reverse [(BindType, CId)]
xs)[CId] -> [CId] -> [CId]
forall a. [a] -> [a] -> [a]
++[CId]
ys) Tree
t) [(BindType, CId)]
xs
    tree2expr [CId]
ys (Var CId
x)    = case CId -> [(CId, MetaId)] -> Maybe MetaId
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup CId
x ([CId] -> [MetaId] -> [(CId, MetaId)]
forall a b. [a] -> [b] -> [(a, b)]
zip [CId]
ys [MetaId
0..]) of
                                Just MetaId
i  -> MetaId -> Expr
EVar MetaId
i
                                Maybe MetaId
Nothing -> [Char] -> Expr
forall a. HasCallStack => [Char] -> a
error [Char]
"unknown variable"

-- | Converts an expression to tree. The conversion is only partial.
-- Variables and meta variables of function type and beta redexes are not allowed.
expr2tree :: Expr -> Tree
expr2tree :: Expr -> Tree
expr2tree Expr
e = [CId] -> [(BindType, CId)] -> Expr -> Tree
abs [] [] Expr
e
  where
    abs :: [CId] -> [(BindType, CId)] -> Expr -> Tree
abs [CId]
ys [(BindType, CId)]
xs (EAbs BindType
b CId
x Expr
e)    = [CId] -> [(BindType, CId)] -> Expr -> Tree
abs [CId]
ys ((BindType
b,CId
x)(BindType, CId) -> [(BindType, CId)] -> [(BindType, CId)]
forall a. a -> [a] -> [a]
:[(BindType, CId)]
xs) Expr
e
    abs [CId]
ys [(BindType, CId)]
xs (ETyped Expr
e Type
_)    = [CId] -> [(BindType, CId)] -> Expr -> Tree
abs [CId]
ys [(BindType, CId)]
xs Expr
e
    abs [CId]
ys [(BindType, CId)]
xs Expr
e               = case [(BindType, CId)]
xs of
                                  [] -> [CId] -> [Tree] -> Expr -> Tree
app [CId]
ys [] Expr
e
                                  [(BindType, CId)]
xs -> [(BindType, CId)] -> Tree -> Tree
Abs ([(BindType, CId)] -> [(BindType, CId)]
forall a. [a] -> [a]
reverse [(BindType, CId)]
xs) ([CId] -> [Tree] -> Expr -> Tree
app (((BindType, CId) -> CId) -> [(BindType, CId)] -> [CId]
forall a b. (a -> b) -> [a] -> [b]
map (BindType, CId) -> CId
forall a b. (a, b) -> b
snd [(BindType, CId)]
xs[CId] -> [CId] -> [CId]
forall a. [a] -> [a] -> [a]
++[CId]
ys) [] Expr
e)

    app :: [CId] -> [Tree] -> Expr -> Tree
app [CId]
xs [Tree]
as (EApp Expr
e1 Expr
e2)    = [CId] -> [Tree] -> Expr -> Tree
app [CId]
xs (([CId] -> [(BindType, CId)] -> Expr -> Tree
abs [CId]
xs [] Expr
e2) Tree -> [Tree] -> [Tree]
forall a. a -> [a] -> [a]
: [Tree]
as) Expr
e1
    app [CId]
xs [Tree]
as (ELit Literal
l)
               | [Tree] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
List.null [Tree]
as = Literal -> Tree
Lit Literal
l
               | Bool
otherwise    = [Char] -> Tree
forall a. HasCallStack => [Char] -> a
error [Char]
"literal of function type encountered"
    app [CId]
xs [Tree]
as (EMeta MetaId
n)
               | [Tree] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
List.null [Tree]
as = MetaId -> Tree
Meta MetaId
n
               | Bool
otherwise    = [Char] -> Tree
forall a. HasCallStack => [Char] -> a
error [Char]
"meta variables of function type are not allowed in trees"
    app [CId]
xs [Tree]
as (EAbs BindType
_ CId
x Expr
e)    = [Char] -> Tree
forall a. HasCallStack => [Char] -> a
error [Char]
"beta redexes are not allowed in trees"
    app [CId]
xs [Tree]
as (EVar MetaId
i)        = if [CId] -> MetaId
forall (t :: * -> *) a. Foldable t => t a -> MetaId
length [CId]
xs MetaId -> MetaId -> Bool
forall a. Ord a => a -> a -> Bool
> MetaId
i then CId -> Tree
Var ([CId]
xs [CId] -> MetaId -> CId
forall a. [a] -> MetaId -> a
!! MetaId
i) else MetaId -> Tree
Meta MetaId
i
                         ---- AR 14/12/2010: work-around needed in PGF.Paraphrase.fromDef
    app [CId]
xs [Tree]
as (EFun CId
f)        = CId -> [Tree] -> Tree
Fun CId
f [Tree]
as
    app [CId]
xs [Tree]
as (ETyped Expr
e Type
_)    = [CId] -> [Tree] -> Expr -> Tree
app [CId]
xs [Tree]
as Expr
e


prTree :: Tree -> String
prTree :: Tree -> [Char]
prTree = [CId] -> Expr -> [Char]
showExpr [] (Expr -> [Char]) -> (Tree -> Expr) -> Tree -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree -> Expr
tree2expr