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 {-# UNPACK #-} !MetaId
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)
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"
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
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