3 import Language.Pointwise.Syntax as Pointwise
4 import Language.Pointfree.Syntax as Pointfree hiding (Const)
8 path :: Ctx -> String -> Pointfree.Term
10 path (x:xs) y | x==y = SND
11 | otherwise = path xs y :.: FST
13 pwpf :: Ctx -> Pointwise.Term -> Pointfree.Term
14 pwpf e (Var x) = path e x
15 pwpf e (Lam x t) = Curry (pwpf (x:e) t)
16 pwpf e (l :@: r) = AP :.: (pwpf e l :/\: pwpf e r)
18 pwpf e (Const s) = Point s :.: BANG
19 pwpf e (l :&: r) = pwpf e l :/\: pwpf e r
20 pwpf e (Fst t) = FST :.: pwpf e t
21 pwpf e (Snd t) = SND :.: pwpf e t
23 AP :.: ((Macro "eithr" [] :.: (pwpf e l :/\: pwpf e r)) :/\: pwpf e t)
24 pwpf e (Inl t) = INL :.: pwpf e t
25 pwpf e (Inr t) = INR :.: pwpf e t
26 pwpf e (In t) = IN :.: pwpf e t
27 pwpf e (Out t) = OUT :.: pwpf e t
28 pwpf e (Pointwise.Fix t) = Macro "fix" [] :.: pwpf e t
30 unpoint :: Pointfree.Term -> Pointfree.Term
31 unpoint f = AP :.: ((f :.: BANG) :/\: ID)