darcs - DrHylo

1 module Hylos where

3 import Language.Pointwise.Syntax as Pointwise

4 import Language.Pointfree.Syntax as Pointfree hiding (Term)

5 import Data.List

6 import Control.Monad.State

9 -- Hylomorphism derivation a la Hu, Iwasaki, and Takeichi

11 derivable :: Term -> Bool

12 derivable (Pointwise.Fix (Lam f (Lam x l))) = branch l

13 where branch (Case m (Lam _ n) (Lam _ o)) =

14 (f `notElem` free m) && branch n && branch o

15 branch n = leaf n

16 leaf Unit = True

17 leaf (Pointwise.Const _) = True

18 leaf (Var y) = (y /= f)

19 leaf (Var g :@: n) | (g == f) = leaf n && (f `notElem` free n)

20 | otherwise = leaf n

21 leaf (n :@: m) = leaf n && leaf m

22 leaf (n :&: m) = leaf n && leaf m

23 leaf (Fst n) = leaf n

24 leaf (Snd n) = leaf n

25 leaf (Inl n) = leaf n

26 leaf (Inr n) = leaf n

27 leaf (In n) = leaf n

28 leaf (Out n) = leaf n

29 leaf _ = False

30 derivable _ = False

32 getVar :: String -> State Int String

33 getVar x = do seed <- get

34 modify (+1)

35 return (x ++ show seed)

37 fun :: Term -> String -> Funct

38 fun l r = evalState (aux l) 0

39 where aux (Case _ (Lam x m) (Lam y n)) =

40 do f <- aux m

41 g <- aux n

42 return (f :++: g)

43 aux Unit = return (Pointfree.Const One)

44 aux (Pointwise.Const _) = return (Pointfree.Const One)

45 aux (Var x) = liftM (Pointfree.Const . Base) (getVar "a")

46 aux (Var x :@: n) | x == r = return Id

47 aux (m :@: n) | null (free n) = aux m

48 | null (free m) = aux n

49 | otherwise = do f <- aux m

50 g <- aux n

51 return (f :**: g)

52 aux (m :&: n) | null (free n) = aux m

53 | null (free m) = aux n

54 | otherwise = do f <- aux m

55 g <- aux n

56 return (f :**: g)

57 aux (Fst n) = aux n

58 aux (Snd n) = aux n

59 aux (Inl n) = aux n

60 aux (Inr n) = aux n

61 aux (In n) = aux n

62 aux (Out n) = aux n

64 coa :: Term -> String -> Term

65 coa t r = aux t

66 where aux (Case l (Lam x m) (Lam y n)) =

67 let f = aux m

68 g = aux n

69 in Case l (Lam x (Inl f)) (Lam y (Inr g))

70 aux Unit = Unit

71 aux (Pointwise.Const _) = Unit

72 aux (Var x) = Var x

73 aux (Var x :@: n) | x == r = n

74 aux (m :@: n) | null (free n) = aux m

75 | null (free m) = aux n

76 | otherwise = let f = aux m

77 g = aux n

78 in f :&: g

79 aux (m :&: n) | null (free n) = aux m

80 | null (free m) = aux n

81 | otherwise = let f = aux m

82 g = aux n

83 in f :&: g

84 aux (Fst n) = aux n

85 aux (Snd n) = aux n

86 aux (Inl n) = aux n

87 aux (Inr n) = aux n

88 aux (In n) = aux n

89 aux (Out n) = aux n

91 alg :: Term -> String -> Term -> Term

92 alg t r p = aux t p

93 where aux (Case l (Lam x m) (Lam y n)) (Var p) =

94 let vl = p++"l"

95 vr = p++"r"

96 f = aux m (Var vl)

97 g = aux n (Var vr)

98 in Case (Var p) (Lam vl f) (Lam vr g)

99 aux Unit _ = Unit

100 aux (Pointwise.Const f) _ = Pointwise.Const f

101 aux (Var x) p = p

102 aux (Var x :@: n) p | x == r = p

103 aux (m :@: n) p | null (free n) = let f = aux m p

104 g = aux n p

105 in f :@: g

106 | null (free m) = let f = aux m p

107 g = aux n p

108 in f :@: g

109 | otherwise = let f = aux m (Fst p)

110 g = aux n (Snd p)

111 in f :@: g

112 aux (m :&: n) p | null (free n) = let f = aux m p

113 g = aux n p

114 in f :&: g

115 | null (free m) = let f = aux m p

116 g = aux n p

117 in f :&: g

118 | otherwise = let f = aux m (Fst p)

119 g = aux n (Snd p)

120 in f :&: g

121 aux (Fst n) p = Fst (aux n p)

122 aux (Snd n) p = Snd (aux n p)

123 aux (Inl n) p = Inl (aux n p)

124 aux (Inr n) p = Inr (aux n p)

125 aux (In n) p = In (aux n p)

126 aux (Out n) p = Out (aux n p)

127