@@ -12,7 +12,7 @@ module CHR.Language.Examples.Term.AST
12
12
, S
13
13
, E
14
14
15
- , module CHR.Language.ATerm
15
+ , module CHR.Language.WithTerm
16
16
)
17
17
where
18
18
@@ -29,8 +29,8 @@ import CHR.Types.Core
29
29
import CHR.Utils
30
30
import CHR.Data.AssocL
31
31
import CHR.Data.Lens
32
- import CHR.Language.GTerm
33
- import CHR.Language.ATerm
32
+ import CHR.Language.Generic
33
+ import CHR.Language.WithTerm
34
34
import qualified CHR.Solve.MonoBacktrackPrio as MBP
35
35
36
36
import Data.Typeable
@@ -47,31 +47,6 @@ import GHC.Generics (Generic)
47
47
48
48
-- import UHC.Util.Debug
49
49
50
- {-
51
- type Var = -- IVar
52
- String
53
-
54
-
55
- data Key' op
56
- = Key_Int !Int
57
- | Key_Var !Var
58
- | Key_Str !String
59
- | Key_Lst
60
- | Key_Op !op
61
- | Key_Con !String
62
- deriving (Eq, Ord, Show)
63
-
64
- type Key = Key' POp
65
-
66
- instance PP op => PP (Key' op) where
67
- pp (Key_Int i) = pp i
68
- pp (Key_Var v) = pp v
69
- pp (Key_Str s) = pp s
70
- pp (Key_Lst ) = ppParens "kl"
71
- pp (Key_Op o) = pp o
72
- pp (Key_Con s) = pp s
73
- -}
74
-
75
50
-- | Terms
76
51
data Tm' op
77
52
= Tm_Var Var -- ^ variable (to be substituted)
@@ -101,47 +76,11 @@ instance PP op => PP (Tm' op) where
101
76
pp (Tm_Str s ) = pp $ show s
102
77
pp (Tm_Bool b ) = pp b
103
78
104
- {-
105
- -- | Constraint
106
- data C' tm
107
- = C_Con String [tm]
108
- | CB_Eq tm tm -- ^ builtin: unification
109
- | CB_Ne tm tm -- ^ builtin: non unification
110
- | CB_Fail -- ^ explicit fail
111
- deriving (Show, Eq, Ord, Typeable, Generic)
112
- -}
113
-
114
79
type C = C' Tm
115
80
116
- {-
117
- instance PP tm => PP (C' tm) where
118
- pp (C_Con c as) = c >#< ppSpaces as
119
- pp (CB_Eq x y ) = "unify" >#< ppSpaces [x,y]
120
- pp (CB_Ne x y ) = "not-unify" >#< ppSpaces [x,y]
121
- pp (CB_Fail ) = pp "fail"
122
-
123
- -- | Guard
124
- data G' tm
125
- = G_Eq tm tm -- ^ check for equality
126
- | G_Ne tm tm -- ^ check for inequality
127
- | G_Tm tm -- ^ determined by arithmetic evaluation
128
- deriving (Show, Typeable, Generic)
129
- -}
130
-
131
81
type G = G' Tm
132
82
133
- {-
134
- instance PP tm => PP (G' tm) where
135
- pp (G_Eq x y) = "is-eq" >#< ppParensCommas [x,y]
136
- pp (G_Ne x y) = "is-ne" >#< ppParensCommas [x,y]
137
- pp (G_Tm t ) = "eval" >#< ppParens t
138
-
139
- -- type instance TrTrKey (Tm' op) = Key' op
140
- -- type instance TrTrKey (C' (Tm' op)) = Key' op
141
- -}
142
-
143
83
type instance TT. TrTrKey (Tm' op ) = Key' op
144
- -- type instance TT.TrTrKey (C' (tm op)) = Key' op
145
84
146
85
instance TT. TreeTrieKeyable (Tm' op ) where
147
86
toTreeTriePreKey1 (Tm_Var v) = TT. prekey1Wild
@@ -152,13 +91,6 @@ instance TT.TreeTrieKeyable (Tm' op) where
152
91
toTreeTriePreKey1 (Tm_Op op as) = TT. prekey1WithChildren (Key_Op op) as
153
92
toTreeTriePreKey1 (Tm_Lst h _ ) = TT. prekey1WithChildren Key_Lst h
154
93
155
- {-
156
- instance (tm ~ Tm' op, TT.TrTrKey (C' tm) ~ TT.TrTrKey tm) => TT.TreeTrieKeyable (C' tm) where
157
- -- Only necessary for non-builtin constraints
158
- toTreeTriePreKey1 (C_Con c as) = TT.prekey1WithChildren (Key_Str {- $ "C_Con:" ++ -} c) as
159
- toTreeTriePreKey1 _ = TT.prekey1Nil
160
- -}
161
-
162
94
type E = E' Tm
163
95
164
96
-- | Binary operator
@@ -185,58 +117,11 @@ instance PP POp where
185
117
pp PBOp_Le = pp " <="
186
118
pp PUOp_Abs = pp " abs"
187
119
188
- {-
189
- newtype P' tm
190
- = P_Tm tm
191
- deriving (Eq, Ord, Show, Generic)
192
- -}
193
-
194
120
type P = P' Tm
195
121
196
- {-
197
- instance PP tm => PP (P' tm) where
198
- pp (P_Tm t) = pp t
199
-
200
- instance Bounded (P' (Tm' op)) where
201
- minBound = P_Tm $ Tm_Int $ fromIntegral $ unPrio $ minBound
202
- maxBound = P_Tm $ Tm_Int $ fromIntegral $ unPrio $ maxBound
203
- -}
204
-
205
- -- type S = IntMap.IntMap Tm
206
- -- type S' tm = Map.Map Var tm
207
122
type S = S' Tm
208
- -- type S = MapH.HashMap Var Tm
209
- -- type S = VAr.VecAlloc Tm
210
- -- type S = Lk.DefaultScpsLkup Var Tm
211
-
212
- {-
213
- type instance VarLookupKey (S' tm) = Var
214
- type instance VarLookupVal (S' tm) = tm
215
123
216
- instance PP tm => PP (S' tm) where
217
- pp = ppAssocLV . Lk.toList
218
- -}
219
-
220
- -- type instance ExtrValVarKey (G' tm) = Var
221
- -- type instance ExtrValVarKey (C' tm) = Var
222
124
type instance ExtrValVarKey (Tm' op ) = Var
223
- -- type instance ExtrValVarKey (P' tm) = Var
224
-
225
- -- type instance CHRMatchableKey (S' (tm op)) = Key' op
226
-
227
- {-
228
- instance VarLookup (S' tm) where
229
- varlookupWithMetaLev _ = Lk.lookup
230
- varlookupKeysSetWithMetaLev _ = Lk.keysSet
231
- varlookupSingletonWithMetaLev _ = Lk.singleton
232
- varlookupEmpty = Lk.empty
233
-
234
- instance Lk.LookupApply (S' tm) (S' tm) where
235
- apply = Lk.union
236
-
237
- instance VarUpdatable tm (S' tm) => VarUpdatable (S' tm) (S' tm) where
238
- varUpd s = {- Lk.apply s . -} Lk.map (s `varUpd`) -- (|+>)
239
- -}
240
125
241
126
instance VarUpdatable (Tm' op ) (S' (Tm' op )) where
242
127
s `varUpd` t = case fromMaybe t $ Lk. lookupResolveVal varTermMbKey t s of
@@ -245,76 +130,13 @@ instance VarUpdatable (Tm' op) (S' (Tm' op)) where
245
130
Tm_Op o as -> Tm_Op o $ s `varUpd` as
246
131
t -> t
247
132
248
- {-
249
- instance VarUpdatable tm (S' tm) => VarUpdatable (P' tm) (S' tm) where
250
- s `varUpd` p = case p of
251
- P_Tm t -> P_Tm (s `varUpd` t)
252
-
253
- instance VarUpdatable tm (S' tm) => VarUpdatable (G' tm) (S' tm) where
254
- s `varUpd` G_Eq x y = G_Eq (s `varUpd` x) (s `varUpd` y)
255
- s `varUpd` G_Ne x y = G_Ne (s `varUpd` x) (s `varUpd` y)
256
- s `varUpd` G_Tm x = G_Tm (s `varUpd` x)
257
-
258
- instance VarUpdatable tm (S' tm) => VarUpdatable (C' tm) (S' tm) where
259
- s `varUpd` c = case c of
260
- C_Con c as -> C_Con c $ map (s `varUpd`) as
261
- CB_Eq x y -> CB_Eq (s `varUpd` x) (s `varUpd` y)
262
- CB_Ne x y -> CB_Ne (s `varUpd` x) (s `varUpd` y)
263
- c -> c
264
- -}
265
-
266
133
instance VarExtractable (Tm' op ) where
267
134
varFreeSet (Tm_Var v) = Set. singleton v
268
135
varFreeSet (Tm_Con _ as) = Set. unions $ map varFreeSet as
269
136
varFreeSet (Tm_Lst h mt) = Set. unions $ map varFreeSet $ maybeToList mt ++ h
270
137
varFreeSet (Tm_Op _ as) = Set. unions $ map varFreeSet as
271
138
varFreeSet _ = Set. empty
272
139
273
- {-
274
- instance (VarExtractable tm, ExtrValVarKey (G' tm) ~ ExtrValVarKey tm) => VarExtractable (G' tm) where
275
- varFreeSet (G_Eq x y) = Set.unions [varFreeSet x, varFreeSet y]
276
- varFreeSet (G_Ne x y) = Set.unions [varFreeSet x, varFreeSet y]
277
- varFreeSet (G_Tm x ) = varFreeSet x
278
-
279
- instance (VarExtractable tm, ExtrValVarKey (C' tm) ~ ExtrValVarKey tm) => VarExtractable (C' tm) where
280
- varFreeSet (C_Con _ as) = Set.unions $ map varFreeSet as
281
- varFreeSet (CB_Eq x y ) = Set.unions [varFreeSet x, varFreeSet y]
282
- varFreeSet _ = Set.empty
283
-
284
- instance (VarExtractable tm, ExtrValVarKey (P' tm) ~ ExtrValVarKey tm) => VarExtractable (P' tm) where
285
- varFreeSet (P_Tm t) = varFreeSet t
286
-
287
- instance CHREmptySubstitution (S' tm) where
288
- chrEmptySubst = Lk.empty
289
- -}
290
-
291
- {-
292
- instance IsConstraint (C' tm) where
293
- cnstrSolvesVia (C_Con _ _) = ConstraintSolvesVia_Rule
294
- cnstrSolvesVia (CB_Eq _ _) = ConstraintSolvesVia_Solve
295
- cnstrSolvesVia (CB_Ne _ _) = ConstraintSolvesVia_Solve
296
- cnstrSolvesVia (CB_Fail ) = ConstraintSolvesVia_Fail
297
- -}
298
-
299
- {-
300
- instance (TmEvalOp Tm' op, Eq op) => CHRCheckable E (G' (Tm' op)) (S' (Tm' op)) where
301
- chrCheckM e g =
302
- case g of
303
- G_Eq t1 t2 -> chrUnifyM CHRMatchHow_Check e t1 t2
304
- G_Ne t1 t2 -> do
305
- menv <- getl chrmatcherstateEnv
306
- s <- getl chrmatcherstateVarLookup
307
- chrmatcherRun'
308
- (\e -> case e of {CHRMatcherFailure -> chrMatchSuccess; _ -> chrMatchFail})
309
- (\_ _ _ -> chrMatchFail)
310
- (chrCheckM e (G_Eq t1 t2)) menv s
311
- G_Tm t -> do
312
- e <- tmEval t
313
- case e of
314
- Tm_Bool True -> chrMatchSuccess
315
- _ -> chrMatchFail
316
- -}
317
-
318
140
instance (Eq op , TmEval (Tm' op )) => CHRMatchable E (Tm' op ) (S' (Tm' op )) where
319
141
chrUnifyM how e t1 t2 = case (t1, t2) of
320
142
(Tm_Con c1 as1, Tm_Con c2 as2) | c1 == c2 -> chrUnifyM how e as1 as2
@@ -353,47 +175,8 @@ instance TmEval Tm where
353
175
where ret x = return $ Tm_Int x
354
176
retb x = return $ Tm_Bool x
355
177
356
- {-
357
- instance (VarExtractable tm, CHRMatchable E tm (S' tm), ExtrValVarKey (C' tm) ~ ExtrValVarKey tm) => CHRMatchable E (C' tm) (S' tm) where
358
- chrUnifyM how e c1 c2 = do
359
- case (c1, c2) of
360
- (C_Con c1 as1, C_Con c2 as2) | c1 == c2 && length as1 == length as2
361
- -> sequence_ (zipWith (chrUnifyM how e) as1 as2)
362
- _ -> chrMatchFail
363
- chrBuiltinSolveM e b = case b of
364
- CB_Eq x y -> chrUnifyM CHRMatchHow_Unify e x y
365
- CB_Ne x y -> do
366
- menv <- getl chrmatcherstateEnv
367
- s <- getl chrmatcherstateVarLookup
368
- chrmatcherRun' (\_ -> chrMatchSuccess) (\_ _ _ -> chrMatchFail) (chrBuiltinSolveM e (CB_Eq x y)) menv s
369
-
370
- instance (VarExtractable tm, CHRMatchable E tm (S' tm), ExtrValVarKey (P' tm) ~ ExtrValVarKey tm) => CHRMatchable E (P' tm) (S' tm) where
371
- chrUnifyM how e p1 p2 = do
372
- case (p1, p2) of
373
- (P_Tm t1 , P_Tm t2 ) -> chrUnifyM how e t1 t2
374
-
375
- -}
376
-
377
178
type instance CHRPrioEvaluatableVal (Tm' op ) = Prio
378
179
379
- {-
380
- instance (TmEvalOp Tm' op) => CHRPrioEvaluatable E (Tm' op) (S' (Tm' op)) where
381
- chrPrioEval e s t = case chrmatcherRun' (\_ -> Tm_Int $ fromIntegral $ unPrio $ (minBound :: Prio)) (\_ _ x -> x) (tmEval t) emptyCHRMatchEnv (Lk.lifts s) of
382
- Tm_Int i -> fromIntegral i
383
- t -> minBound
384
- chrPrioLift = Tm_Int . fromIntegral
385
- -}
386
-
387
- -- type instance CHRPrioEvaluatableVal (P' tm) = Prio
388
-
389
- {-
390
- instance (CHRPrioEvaluatable E tm (S' tm), CHRPrioEvaluatableVal (P' tm) ~ CHRPrioEvaluatableVal tm
391
- ) => CHRPrioEvaluatable E (P' tm) (S' tm) where
392
- chrPrioEval e s p = case p of
393
- P_Tm t -> chrPrioEval e s t
394
- chrPrioLift = P_Tm . chrPrioLift
395
-
396
- -}
397
180
398
181
--------------------------------------------------------
399
182
@@ -423,38 +206,5 @@ instance TmIs Tm where
423
206
isTmBool (Tm_Bool v) = Just v
424
207
isTmBool _ = Nothing
425
208
426
- -- instance GTermAsTm Tm
427
-
428
- {-
429
- instance GTermAsTm tm => GTermAs (C' tm) (G' tm) (P' tm) (P' tm) where
430
- asHeadConstraint t = case t of
431
- GTm_Con c a -> forM a asTm >>= (return . C_Con c)
432
- t -> gtermasFail t "not a constraint"
433
-
434
- asBodyConstraint t = case t of
435
- GTm_Con "Fail" [] -> return CB_Fail
436
- GTm_Con o [a,b]
437
- | Just o' <- List.lookup o [("==", CB_Eq), ("/=", CB_Ne)] -> do
438
- a <- asTm a
439
- b <- asTm b
440
- return $ o' a b
441
- t -> asHeadConstraint t
442
-
443
- asGuard t = case t of
444
- GTm_Con o [a,b]
445
- | Just o' <- List.lookup o [("==", G_Eq), ("/=", G_Ne)] -> do
446
- a <- asTm a
447
- b <- asTm b
448
- return $ o' a b
449
- t -> fmap G_Tm $ asTm t
450
-
451
- asHeadBacktrackPrio = fmap P_Tm . asTm
452
209
453
- asAltBacktrackPrio = asHeadBacktrackPrio
454
- asRulePrio = asHeadBacktrackPrio
455
-
456
- -}
457
-
458
- --------------------------------------------------------
459
- -- leq example, backtrack prio specific
460
210
0 commit comments