Combined-line mode checks bidirectionalizability
[darcs-mirror-sem_syn.git] / BUtil.hs
1 {-# OPTIONS -XRank2Types -XCPP -XScopedTypeVariables #-}
2 module BUtil where
3
4 import qualified Data.IntMap as IntMap 
5 import Control.Monad 
6
7 import System.IO.Unsafe
8
9 import Control.Exception
10
11 data Nat = S Nat | Z deriving (Eq)
12
13 instance Show Nat where
14   show = show . fromNat
15
16 instance Num Nat where
17   (+) = error "No operators defined for Nat"
18   (*) = error "No operators defined for Nat"
19   abs = error "No operators defined for Nat"
20   signum = error "No operators defined for Nat"
21   fromInteger n | n < 0  = error "Nat cannot be negative"
22                 | n >= 0 = toNat n
23
24 toNat x = if x == 0 then 
25               Z
26           else 
27               S (toNat $ x-1)
28
29 fromNat Z     = 0
30 fromNat (S x) = 1 + fromNat x
31
32 fromDistinctList = IntMap.fromList 
33
34 gen_put_bias :: Bias 
35                 -> (forall a. [a] -> [a]) 
36                 -> (Nat -> Nat -> Maybe Nat) 
37                 -> [a] -> [a] 
38                 -> Maybe [Maybe a]
39 gen_put_bias bias get sput s v =
40     do { let ls = length s  
41        ; let g = fromDistinctList (zip (bias ls) s)
42        ; l' <- maybe (fail "...")
43                      return
44                      (sput (toNat ls) (toNat (length v)))
45        ; let t = bias (fromNat l')
46        ; let h = fromDistinctList (zip (get t) v)
47        ; let h'= IntMap.union h g 
48        ; return (map (flip IntMap.lookup h') t) }
49
50 withDefaultBias put bias d s v =
51     do { s' <- put bias s v 
52        ; return (map (maybe d id) s') }
53
54 withDefault put d s v =
55     do { s' <- put s v 
56        ; return (map (maybe d id) s') }
57
58 gen_put_dbias :: Bias -> (forall a. [a] -> [a]) 
59                  -> (Nat -> Nat -> Maybe Nat)
60                  -> a -> [a] -> [a] -> Maybe [a]
61 gen_put_dbias bias get sput d s v =
62     do { s' <- gen_put_bias bias get sput s v
63        ; return (map (maybe d id) s') }
64
65 castError :: a -> Maybe a 
66 castError f = unsafePerformIO $ 
67     do { r <- try (evaluate f)
68        ; case r of
69 #if __GLASGOW_HASKELL__ >= 610 
70            Left (e::SomeException) -> return $ Nothing 
71 #else
72            Left  e -> return $ Nothing 
73 #endif
74            Right r -> return $ Just $ r }
75
76 type Bias = Int -> [ Int ]
77 rear l    = [ 0 .. l - 1 ]
78 front l   = reverse [ 0 .. l - 1 ]
79 middle l  = [1,3..l] ++ (reverse [2,4..l])
80 borders l = (reverse [1,3..l])++[2,4..l]