update demo
[coq-hetmet.git] / examples / GArrowSkeleton.hs
1 {-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies #-}
2 -----------------------------------------------------------------------------
3 -- |
4 -- Module      :  GArrowSkeleton
5 -- Copyright   :  none
6 -- License     :  public domain
7 --
8 -- Maintainer  :  Adam Megacz <megacz@acm.org>
9 -- Stability   :  experimental
10 --
11 -- | Sometimes it is convenient to be able to get your hands on the
12 -- explicit boxes-and-wires representation of a GArrow-polymorphic
13 -- term.  GArrowSkeleton lets you do that.
14 --
15 -- HOWEVER: technically this instance violates the laws (and RULEs)
16 -- for Control.Category; the compiler might choose to optimize (f >>>
17 -- id) into f, and this optimization would produce a change in
18 -- behavior below -- you'd get (GAS_comp f GAS_id) instead of f.  In
19 -- practice this means that the user must be prepared for the skeleton
20 -- TikZ diagram to be a nondeterministically-chosen boxes-and-wires
21 -- diagram which ks *equivalent to* the term, rather than structurally
22 -- exactly equal to it.
23 --
24 module GArrowSkeleton (GArrowSkeleton(..), optimize)
25 where
26 import Prelude hiding ( id, (.), lookup )
27 import Control.Category
28 import GHC.HetMet.GArrow
29 import Unify
30 import Control.Monad.State
31
32 data GArrowSkeleton m :: * -> * -> *
33  where
34   GAS_const     ::                                          Int -> GArrowSkeleton m () Int
35   GAS_id        ::                                                 GArrowSkeleton m x x
36   GAS_comp      :: GArrowSkeleton m x y -> GArrowSkeleton m y z -> GArrowSkeleton m x z
37   GAS_first     :: GArrowSkeleton m x y                         -> GArrowSkeleton m (x,z)  (y,z)
38   GAS_second    :: GArrowSkeleton m x y                         -> GArrowSkeleton m (z,x)  (z,y)
39   GAS_cancell   ::                                                 GArrowSkeleton m ((),x) x
40   GAS_cancelr   ::                                                 GArrowSkeleton m (x,()) x
41   GAS_uncancell ::                                                 GArrowSkeleton m x ((),x)
42   GAS_uncancelr ::                                                 GArrowSkeleton m x (x,())
43   GAS_assoc     ::                                                 GArrowSkeleton m ((x,y),z) (x,(y,z))
44   GAS_unassoc   ::                                                 GArrowSkeleton m (x,(y,z)) ((x,y),z)
45   GAS_drop      ::                                                 GArrowSkeleton m x         ()
46   GAS_copy      ::                                                 GArrowSkeleton m x         (x,x)
47   GAS_swap      ::                                                 GArrowSkeleton m (x,y)     (y,x)
48   GAS_merge     ::                                                 GArrowSkeleton m (x,y)     z
49   GAS_loopl     ::                 GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y
50   GAS_loopr     ::                 GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y
51   GAS_misc      ::                                        m x y -> GArrowSkeleton m x y
52
53 instance Category (GArrowSkeleton m) where
54   id           = GAS_id
55   g . f        = GAS_comp f g
56
57 instance GArrow (GArrowSkeleton m) (,) () where
58   ga_first     = GAS_first
59   ga_second    = GAS_second
60   ga_cancell   = GAS_cancell
61   ga_cancelr   = GAS_cancelr
62   ga_uncancell = GAS_uncancell
63   ga_uncancelr = GAS_uncancelr
64   ga_assoc     = GAS_assoc
65   ga_unassoc   = GAS_unassoc
66
67 instance GArrowDrop (GArrowSkeleton m) (,) () where
68   ga_drop      = GAS_drop
69
70 instance GArrowCopy (GArrowSkeleton m) (,) () where
71   ga_copy      = GAS_copy
72
73 instance GArrowSwap (GArrowSkeleton m) (,) () where
74   ga_swap      = GAS_swap
75
76 instance GArrowLoop (GArrowSkeleton m) (,) () where
77   ga_loopl     = GAS_loopl
78   ga_loopr     = GAS_loopr
79
80 type instance GArrowTensor      (GArrowSkeleton m) = (,)
81 type instance GArrowUnit        (GArrowSkeleton m) = ()
82 type instance GArrowExponent    (GArrowSkeleton m) = (->)
83
84 instance GArrowSTKC (GArrowSkeleton m)
85
86 --
87 -- | Simple structural equality on skeletons.  NOTE: two skeletons
88 --   with the same shape but different types will nonetheless be "equal";
89 --   there's no way around this since types are gone at runtime.
90 --
91 instance Eq ((GArrowSkeleton m) a b)
92  where
93   x == y = x === y
94    where
95     (===) :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) c d -> Bool
96     (GAS_id           ) === (GAS_id           ) = True
97     (GAS_comp      g f) === (GAS_comp    g' f') = f===f' && g===g'
98     (GAS_first       f) === (GAS_first  f')     = f===f'
99     (GAS_second      f) === (GAS_second f')     = f===f'
100     GAS_cancell         === GAS_cancell         = True
101     GAS_cancelr         === GAS_cancelr         = True
102     GAS_uncancell       === GAS_uncancell       = True
103     GAS_uncancelr       === GAS_uncancelr       = True
104     GAS_drop            === GAS_drop            = True
105     (GAS_const i)       === (GAS_const i')      = i==i'
106     GAS_copy            === GAS_copy            = True
107     GAS_merge           === GAS_merge           = True
108     GAS_swap            === GAS_swap            = True
109     GAS_assoc           === GAS_assoc           = True
110     GAS_unassoc         === GAS_unassoc         = True
111     (GAS_loopl f)       === (GAS_loopl f')      = f === f'
112     (GAS_loopr f)       === (GAS_loopr f')      = f === f'
113     _ === _                                     = False
114     -- FIXME: GAS_misc's are never equal!!!
115
116 --
117 -- | Performs some very simple-minded optimizations on a
118 --   boxes-and-wires diagram.  Preserves equivalence up to the GArrow
119 --   laws, but no guarantees about which optimizations actually happen.
120 --
121 optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
122 optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
123  where
124   optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
125
126   -- Some optimizations fail due to misparenthesization; we default to
127   -- left-associativity and hope for the best
128   optimize' (GAS_comp      f (GAS_comp g h)) = GAS_comp (GAS_comp f g) h
129   optimize' (GAS_comp    (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k
130   optimize' (GAS_comp    (GAS_comp f g) h) = case optimize_pair g h of
131                                                Nothing   -> GAS_comp (optimize' (GAS_comp f g)) h'
132                                                Just ret' -> GAS_comp f' ret'
133                                               where
134                                                 f' = optimize' f
135                                                 g' = optimize' g
136                                                 h' = optimize' h
137   optimize' (GAS_comp      f g     ) = case optimize_pair f g of
138                                          Nothing   -> GAS_comp f' g'
139                                          Just ret' -> ret'
140                                         where
141                                          f' = optimize' f
142                                          g' = optimize' g
143   optimize' (GAS_first     GAS_id  ) = GAS_id
144   optimize' (GAS_second    GAS_id  ) = GAS_id
145   optimize' (GAS_first     f       ) = GAS_first  $ optimize' f
146   optimize' (GAS_second    f       ) = GAS_second $ optimize' f
147   optimize' (GAS_loopl GAS_id)  = GAS_id
148   optimize' (GAS_loopr GAS_id)  = GAS_id
149   optimize' (GAS_loopl f      ) = GAS_loopl $ optimize' f
150   optimize' (GAS_loopr f      ) = GAS_loopr $ optimize' f
151   optimize' x                   = x
152
153   optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
154
155   optimize_pair f GAS_drop                    = Just $ GAS_drop
156   optimize_pair GAS_id f                      = Just $ f
157   optimize_pair f GAS_id                      = Just $ f
158   optimize_pair GAS_uncancell GAS_cancell     = Just $ GAS_id
159   optimize_pair GAS_uncancelr GAS_cancelr     = Just $ GAS_id
160   optimize_pair GAS_cancell GAS_uncancell     = Just $ GAS_id
161   optimize_pair GAS_cancelr GAS_uncancelr     = Just $ GAS_id
162   optimize_pair GAS_uncancelr GAS_cancell     = Just $ GAS_id
163   optimize_pair GAS_uncancell GAS_cancelr     = Just $ GAS_id
164
165   -- first priority: eliminate GAS_first                                                
166   optimize_pair (GAS_first f) GAS_cancelr     = Just $ GAS_comp   GAS_cancelr f
167   optimize_pair (GAS_second f) GAS_cancell    = Just $ GAS_comp   GAS_cancell f
168   optimize_pair GAS_uncancelr (GAS_first f)   = Just $ GAS_comp   f GAS_uncancelr
169   optimize_pair GAS_uncancell (GAS_second f)  = Just $ GAS_comp   f GAS_uncancell
170
171   -- second priority: push GAS_swap leftward... why isn't this working?
172   optimize_pair (GAS_second f) GAS_swap       = Just $ GAS_comp   GAS_swap (GAS_first  f)
173   optimize_pair (GAS_first f) GAS_swap        = Just $ GAS_comp   GAS_swap (GAS_second f)
174   optimize_pair GAS_swap GAS_swap             = Just $ GAS_id
175
176   optimize_pair (GAS_first f) (GAS_first g)   = Just $ GAS_first (GAS_comp f g)
177   optimize_pair (GAS_second f) (GAS_second g) = Just $ GAS_second (GAS_comp f g)
178
179   optimize_pair GAS_assoc   GAS_cancell       = Just $ GAS_first GAS_cancell
180   optimize_pair GAS_unassoc GAS_cancelr       = Just $ GAS_second GAS_cancelr
181
182   optimize_pair _ _                           = Nothing
183
184