1 module Language.Pointwise.Matching where
3 import Language.Pointwise.Syntax
4 import Data.Generics hiding (Unit,Inl,Inr)
6 import Control.Monad.State
7 import Generics.Pointless.Combinators
10 -- Patterm matching elimination
12 -- Does not detect repeated variables in patterns
13 -- It can be improved in the pair case: does not detect equalities up to alpha
14 -- conversion, neither renanes variables appearing both at the pattern and the
15 -- term subject to matching
17 getVar :: String -> StateT Int Maybe String
18 getVar x = do seed <- get
20 return (x ++ show seed)
22 nomatch :: Term -> StateT Int Maybe Term
23 nomatch (Match e []) = fail "Should not hapen given the premises"
24 nomatch (Match e [(Var x, rhs)]) =
25 do rhs' <- nomatch rhs
26 return (subst [(x,e)] rhs')
27 nomatch (Match e [(Unit, rhs)]) =
30 | isPair (fst (head l)) =
31 do guard (all isPair (map fst l))
32 guard (all null (map (\(x :&: y, _) -> free x `intersect` free y) l))
33 guard (null (free e `intersect` concatMap (free . fst) l))
34 let aux = mygroup (\x y -> pwFst (fst x) == pwFst (fst y)) l
35 left = map (pwFst . fst . head) aux
36 rightmatch = map (nomatch . Match (Snd e) . map (pwSnd . fst /\ snd)) aux
37 right <- sequence rightmatch
38 nomatch (Match (Fst e) (zip left right))
40 | isInlr (fst (head l)) =
41 do guard (all isInlr (map fst l))
42 let left' = map (\ (Inl t, p) -> (t,p)) (filter (isInl . fst) l)
43 right' = map (\ (Inr t, p) -> (t,p)) (filter (isInr . fst) l)
45 left <- nomatch (Lam var (Match (Var var) left'))
46 right <- nomatch (Lam var (Match (Var var) right'))
47 return (Case e left right)
49 | isIn (fst (head l)) =
50 do guard (all isIn (map fst l))
51 let pats = map (\(In t,p) -> (t,p)) l
52 nomatch (Match (Out e) pats)
53 nomatch (Match t alts) =
54 fail "Not possible to eliminate pattern matching!"
55 nomatch e = gmapM (mkM nomatch) e
59 -- Auxiliary definitions
61 mygroup :: Eq a => (a -> a -> Bool) -> [a] -> [[a]]
63 mygroup f (h:t) = (h : filter (\x -> f x h) t) : mygroup f (filter (\x -> not (f x h)) t)