summaryrefslogtreecommitdiff
path: root/tests/examples/SegFault2.hs
blob: 138e055b56cbd704d1274c0deabc89768762db0c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
{-# LANGUAGE CPP #-}

module UHC.Light.Compiler.CHR.Constraint
( Constraint (..)
, mkReduction
, cnstrReducablePart
, UnresolvedTrace (..)
, cnstrMpSingletonL, cnstrMpFromList
, ConstraintToInfoTraceMp
, cnstrTraceMpSingleton, cnstrTraceMpLiftTrace, cnstrTraceMpElimTrace, cnstrTraceMpFromList
, ConstraintToInfoMap
, emptyCnstrMp
, cnstrMpUnion, cnstrMpUnions
, cnstrRequiresSolve )
where
import UHC.Light.Compiler.Base.Common
import UHC.Light.Compiler.Ty
import UHC.Light.Compiler.CHR
import UHC.Light.Compiler.CHR.Key
import UHC.Light.Compiler.Base.TreeTrie
import UHC.Light.Compiler.Substitutable
import UHC.Util.Pretty as PP
import UHC.Util.Utils
import qualified Data.Set as Set
import qualified Data.Map as Map
import UHC.Light.Compiler.VarMp
import Control.Monad
import UHC.Util.Binary
import UHC.Util.Serialize
import Data.Typeable
import Data.Generics (Data)
import UHC.Light.Compiler.Opts.Base




{-# LINE 37 "src/ehc/CHR/Constraint.chs" #-}
-- | A Constraint is abstracted over the exact predicate, but differentiates on the role: to prove, can be assumed, and side effect of reduction
data Constraint p info
  = Prove           { cnstrPred :: !p }             -- proof obligation
  | Assume          { cnstrPred :: !p }             -- assumed constraint
  | Reduction                                       -- 'side effect', residual info used by (e.g.) codegeneration
                    { cnstrPred :: !p               -- the pred to which reduction was done
                    , cnstrInfo :: !info            -- additional reduction specific info w.r.t. codegeneration
                    , cnstrFromPreds :: ![p]        -- the preds from which reduction was done
                    , cnstrVarMp :: VarMp           -- additional bindings for type (etc.) variables, i.e. improving substitution
                    }
  deriving (Eq, Ord, Show)

{-# LINE 53 "src/ehc/CHR/Constraint.chs" #-}
mkReduction :: p -> info -> [p] -> Constraint p info
mkReduction p i ps
  = Reduction p i ps
              varlookupEmpty

{-# LINE 62 "src/ehc/CHR/Constraint.chs" #-}
#if __GLASGOW_HASKELL__ >= 708
deriving instance Typeable  Constraint
#else
deriving instance Typeable2 Constraint
#endif
deriving instance (Data x, Data y) => Data (Constraint x y)

{-# LINE 71 "src/ehc/CHR/Constraint.chs" #-}
-- | Dissection of Constraint, including reconstruction function
cnstrReducablePart :: Constraint p info -> Maybe (String,p,p->Constraint p info)
cnstrReducablePart (Prove  p) = Just ("Prf",p,Prove)
cnstrReducablePart (Assume p) = Just ("Ass",p,Assume)
cnstrReducablePart _          = Nothing

{-# LINE 84 "src/ehc/CHR/Constraint.chs" #-}
instance (CHRMatchable env p s) => CHRMatchable env (Constraint p info) s where
  chrMatchTo env s c1 c2
    = do { (_,p1,_) <- cnstrReducablePart c1
         ; (_,p2,_) <- cnstrReducablePart c2
         ; chrMatchTo env s p1 p2
         }

{-# LINE 93 "src/ehc/CHR/Constraint.chs" #-}
instance TTKeyable p => TTKeyable (Constraint p info) where
  toTTKey' o c -- = maybe [] (\(s,p,_) -> ttkAdd (TT1K_One $ Key_Str s) [toTTKey' o p]) $ cnstrReducablePart c
    = case cnstrReducablePart c of
        Just (s,p,_) -> ttkAdd' (TT1K_One $ Key_Str s) cs
                     where (_,cs) = toTTKeyParentChildren' o p
        _            -> panic "TTKeyable (Constraint p info).toTTKey'" -- ttkEmpty

{-# LINE 102 "src/ehc/CHR/Constraint.chs" #-}
instance (VarExtractable p v,VarExtractable info v) => VarExtractable (Constraint p info) v where
  varFreeSet c
    = case cnstrReducablePart c of
        Just (_,p,_) -> varFreeSet p
        _            -> Set.empty

instance (VarUpdatable p s,VarUpdatable info s) => VarUpdatable (Constraint p info) s where
  varUpd s      (Prove     p       ) = Prove      (varUpd s p)
  varUpd s      (Assume    p       ) = Assume     (varUpd s p)
  varUpd s      r@(Reduction {cnstrPred=p, cnstrInfo=i, cnstrFromPreds=ps})
                                     = r {cnstrPred=varUpd s p, cnstrInfo=varUpd s i, cnstrFromPreds=map (varUpd s) ps}

{-# LINE 120 "src/ehc/CHR/Constraint.chs" #-}
-- | The trace of an unresolved predicate
data UnresolvedTrace p info
  = UnresolvedTrace_None                                    -- no trace required when all is resolved
  | UnresolvedTrace_Red                                     -- ok reduction, with failure deeper down
      { utraceRedFrom       :: p
      , utraceInfoTo2From   :: info
      , utraceRedTo         :: [UnresolvedTrace p info]
      }
  | UnresolvedTrace_Fail                                    -- failed reduction
      { utraceRedFrom       :: p
      -- , utraceInfoTo2From    :: info
      , utraceRedTo         :: [UnresolvedTrace p info]
      }
  | UnresolvedTrace_Overlap                                 -- choice could not be made
      { utraceRedFrom       :: p
      , utraceRedChoices    :: [(info,[UnresolvedTrace p info])]
      }
  deriving Show

instance Eq p => Eq (UnresolvedTrace p info) where
  t1 == t2 = True -- utraceRedFrom t1 == utraceRedFrom t2

instance (PP p, PP info) => PP (UnresolvedTrace p info) where
  pp x = case x of
           UnresolvedTrace_None             -> PP.empty
           UnresolvedTrace_Red      p i us  -> p >|< ":" >#< i >-< indent 2 (vlist $ map pp us)
           UnresolvedTrace_Fail     p   us  -> p >|< ": FAIL" >-< indent 2 (vlist $ map pp us)
           UnresolvedTrace_Overlap  p uss   -> p >|< ": OVERLAP" >-< indent 2 (vlist $ map (\(i,u) -> i >-< indent 2 (vlist $ map pp u)) uss)

{-# LINE 155 "src/ehc/CHR/Constraint.chs" #-}
-- | Map from constraint to something
type ConstraintMp' p info x = Map.Map (Constraint p info) [x]

{-# LINE 160 "src/ehc/CHR/Constraint.chs" #-}
cnstrMpSingletonL :: Constraint p i -> [x] -> ConstraintMp' p i x
cnstrMpSingletonL c xs = Map.singleton c xs

cnstrMpSingleton :: Constraint p i -> x -> ConstraintMp' p i x
cnstrMpSingleton c x = cnstrMpSingletonL c [x]

cnstrMpFromList :: (Ord p, Ord i) => [(Constraint p i,x)] -> ConstraintMp' p i x
cnstrMpFromList l = Map.fromListWith (++) [ (c,[x]) | (c,x) <- l ]

cnstrMpMap :: (Ord p, Ord i) => (x -> y) -> ConstraintMp' p i x -> ConstraintMp' p i y
cnstrMpMap f = Map.map (map f)

{-# LINE 174 "src/ehc/CHR/Constraint.chs" #-}
-- | Map from constraint to info + trace
type ConstraintToInfoTraceMp p info = ConstraintMp' p info (info,[UnresolvedTrace p info])

{-# LINE 179 "src/ehc/CHR/Constraint.chs" #-}
cnstrTraceMpFromList :: (Ord p, Ord i) => [(Constraint p i,(i,[UnresolvedTrace p i]))] -> ConstraintToInfoTraceMp p i
cnstrTraceMpFromList = cnstrMpFromList

cnstrTraceMpSingleton :: Constraint p i -> i -> [UnresolvedTrace p i] -> ConstraintToInfoTraceMp p i
cnstrTraceMpSingleton c i ts = cnstrMpSingleton c (i,ts)

cnstrTraceMpElimTrace :: (Ord p, Ord i) => ConstraintToInfoTraceMp p i -> ConstraintToInfoMap p i
cnstrTraceMpElimTrace = cnstrMpMap fst

cnstrTraceMpLiftTrace :: (Ord p, Ord i) => ConstraintToInfoMap p i -> ConstraintToInfoTraceMp p i
cnstrTraceMpLiftTrace = cnstrMpMap (\x -> (x,[]))

{-# LINE 193 "src/ehc/CHR/Constraint.chs" #-}
-- | Map from constraint to info
type ConstraintToInfoMap     p info = ConstraintMp' p info info

{-# LINE 198 "src/ehc/CHR/Constraint.chs" #-}
emptyCnstrMp :: ConstraintMp' p info x
emptyCnstrMp = Map.empty

{-# LINE 208 "src/ehc/CHR/Constraint.chs" #-}
cnstrMpUnion :: (Ord p, Ord i) => ConstraintMp' p i x -> ConstraintMp' p i x -> ConstraintMp' p i x
cnstrMpUnion = Map.unionWith (++)

cnstrMpUnions :: (Ord p, Ord i) => [ConstraintMp' p i x] -> ConstraintMp' p i x
cnstrMpUnions = Map.unionsWith (++)

{-# LINE 220 "src/ehc/CHR/Constraint.chs" #-}
-- | Predicate for whether solving is required
cnstrRequiresSolve :: Constraint p info -> Bool
cnstrRequiresSolve (Reduction {}) = False
cnstrRequiresSolve _              = True

{-# LINE 231 "src/ehc/CHR/Constraint.chs" #-}
instance (PP p, PP info) => PP (Constraint p info) where
  pp (Prove     p     ) = "Prove"  >#< p
  pp (Assume    p     ) = "Assume" >#< p
  pp (Reduction {cnstrPred=p, cnstrInfo=i, cnstrFromPreds=ps})
                        = "Red"    >#< p >#< "<" >#< i >#< "<" >#< ppBracketsCommas ps

{-# LINE 243 "src/ehc/CHR/Constraint.chs" #-}
instance (Serialize p, Serialize i) => Serialize (Constraint p i) where
  sput (Prove     a      ) = sputWord8 0 >> sput a
  sput (Assume    a      ) = sputWord8 1 >> sput a
  sput (Reduction a b c d) = sputWord8 2 >> sput a >> sput b >> sput c >> sput d
  sget = do t <- sgetWord8
            case t of
              0 -> liftM  Prove     sget
              1 -> liftM  Assume    sget
              2 -> liftM4 Reduction sget sget sget sget