DrHylo-0.0.1: src/PwPf.hs

module PwPf where

import Language.Pointwise.Syntax as Pointwise
import Language.Pointfree.Syntax as Pointfree hiding (Const)

type Ctx = [String]

path :: Ctx -> String -> Pointfree.Term
path [] x = Point x
path (x:xs) y | x==y = SND
	      | otherwise = path xs y :.: FST

pwpf :: Ctx -> Pointwise.Term -> Pointfree.Term 
pwpf e (Var x)   = path e x
pwpf e (Lam x t) = Curry (pwpf (x:e) t)
pwpf e (l :@: r) = AP :.: (pwpf e l :/\: pwpf e r)
pwpf e Unit      = BANG
pwpf e (Const s) = Point s :.: BANG
pwpf e (l :&: r) = pwpf e l :/\: pwpf e r
pwpf e (Fst t)   = FST :.: pwpf e t
pwpf e (Snd t)   = SND :.: pwpf e t
pwpf e (Case t l r) = 
    AP :.: ((Macro "eithr" [] :.: (pwpf e l :/\: pwpf e r)) :/\: pwpf e t)
pwpf e (Inl t)   = INL :.: pwpf e t
pwpf e (Inr t)   = INR :.: pwpf e t
pwpf e (In t)    = IN :.: pwpf e t
pwpf e (Out t)   = OUT :.: pwpf e t
pwpf e (Pointwise.Fix t)   = Macro "fix" [] :.: pwpf e t

unpoint :: Pointfree.Term -> Pointfree.Term
unpoint f = AP :.: ((f :.: BANG) :/\: ID)