darcs - DrHylo

1 module Language.Pointwise.Syntax where

3 import Data.Generics hiding (Unit,Inl,Inr)

4 import Data.List

5 import Data.Maybe

6 import Generics.Pointless.Combinators

8 data Term = Var String

9 | Unit

10 | Const String -- Is this really necessary?

11 | Term :&: Term

12 | Fst Term

13 | Snd Term

14 | Case Term Term Term

15 | Match Term [(Term,Term)]

16 | Inl Term

17 | Inr Term

18 | Lam String Term

19 | Term :@: Term

20 | In Term

21 | Out Term

22 | Fix Term

23 deriving (Eq,Show,Data,Typeable)

25 isPair :: Term -> Bool

26 isPair (_ :&: _) = True

27 isPair _ = False

29 pwFst :: Term -> Term

30 pwFst (l :&: r) = l

32 pwSnd :: Term -> Term

33 pwSnd (l :&: r) = r

35 isInl :: Term -> Bool

36 isInl (Inl _) = True

37 isInl _ = False

39 isInr :: Term -> Bool

40 isInr (Inr _) = True

41 isInr _ = False

43 isInlr :: Term -> Bool

44 isInlr t = isInl t || isInr t

46 isIn :: Term -> Bool

47 isIn (In _) = True

48 isIn _ = False

51 -- Free variables

52 -- only works correctly when there are no Match constructors in Term

54 free :: Term -> [String]

55 free (Var v) = [v]

56 free (Lam v x) = delete v (free x)

57 free e = nub (concat (gmapQ (mkQ [] free) e))

59 -- Substitution

60 -- only works correctly when there are no Match constructors in Term

62 subst :: [(String, Term)] -> Term -> Term

63 subst s (Var y) =

64 case lookup y s

65 of Nothing -> Var y

66 Just t -> t

67 subst s (Lam y e) =

68 let x = concat (concatMap free (e : map snd s))

69 in Lam x (subst ((y, Var x) : s) e)

70 subst s t =

71 gmapT (mkT (subst s)) t

73 -- single traversal (bottom-up) beta reduction

75 step :: Term -> Term

76 step = everywhere (mkT aux)

77 where aux ((Lam v t) :@: m) = subst [(v,m)] t

78 aux t = t

80 -- Replacing constant by definition

82 replace :: [(String, Term)] -> Term -> Term

83 replace defs = everywhere (mkT aux)

84 where aux (Const x) = fromMaybe (Const x) (lookup x defs)

85 aux t = t

87 -- Examples

89 distr :: Term

90 distr = Lam "x" (Match (Var "x") [(Var "y" :&: Inl (Var "z"),Inl (Var "y" :&: Var "z")),(Var "y" :&: Inr (Var "z"),Inr (Var "y" :&: Var "z"))])

92 swap :: Term

93 swap = Lam "x" (Match (Var "x") [(Var "w" :&: Var "y", Var "y" :&: Var "w")])

95 coswap :: Term

96 coswap = Lam "x" (Match (Var "x") [(Inl (Var "y"), Inr (Var "y")),(Inr (Var "y"), Inl (Var "y"))])

98 assocr :: Term

99 assocr = Lam "w" (Match (Var "w") [((Var "x" :&: Var "y") :&: Var "z", Var "x" :&: (Var "y" :&: Var "z"))])

100

101 coassocr :: Term

102 coassocr = Lam "w" (Match (Var "w") [(Inl (Inl (Var "x")), Inl (Var "x")),(Inl (Inr (Var "x")), Inr (Inl (Var "x"))),(Inr (Var "x"), Inr (Inr (Var "x")))])

103

104 test :: Term

105 test = Lam "x" (Match (Var "x") [(Var "y", Var "y")])