Skip to content

Commit c6e272d

Browse files
ttuegelttuegel
committed
Pattern: add From instances
1 parent 6497673 commit c6e272d

File tree

1 file changed

+191
-4
lines changed

1 file changed

+191
-4
lines changed

‎kore/src/Kore/Syntax/Pattern.hs

Lines changed: 191 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -54,11 +54,33 @@ import qualified GHC.Generics as GHC
5454

5555
import qualified Kore.Attribute.Null as Attribute
5656
import Kore.Debug
57+
import Kore.Sort
58+
import Kore.Syntax.And
59+
import Kore.Syntax.Application
60+
import Kore.Syntax.Bottom
61+
import Kore.Syntax.Ceil
62+
import Kore.Syntax.DomainValue
63+
import Kore.Syntax.Equals
64+
import Kore.Syntax.Exists
65+
import Kore.Syntax.Floor
66+
import Kore.Syntax.Forall
67+
import Kore.Syntax.Iff
68+
import Kore.Syntax.Implies
69+
import Kore.Syntax.In
70+
import Kore.Syntax.Inhabitant
71+
import Kore.Syntax.Mu
72+
import Kore.Syntax.Next
73+
import Kore.Syntax.Not
74+
import Kore.Syntax.Nu
75+
import Kore.Syntax.Or
5776
import Kore.Syntax.PatternF
5877
( Const (..)
5978
, PatternF (..)
6079
)
6180
import qualified Kore.Syntax.PatternF as PatternF
81+
import Kore.Syntax.Rewrites
82+
import Kore.Syntax.StringLiteral
83+
import Kore.Syntax.Top
6284
import Kore.Syntax.Variable
6385
import Kore.TopBottom
6486
( TopBottom (..)
@@ -238,13 +260,178 @@ instance TopBottom (Pattern variable annotation) where
238260
isBottom (Recursive.project -> _ :< BottomF _) = True
239261
isBottom _ = False
240262

241-
instance
242-
(Unparse variable)
243-
=> SQL.Column (Pattern variable annotation)
244-
where
263+
instance Unparse variable => SQL.Column (Pattern variable annotation) where
245264
defineColumn tableName _ = SQL.defineColumn tableName (SQL.Proxy @Text)
246265
toColumn = SQL.toColumn . Pretty.renderText . Pretty.layoutOneLine . unparse
247266

267+
instance
268+
From
269+
(And Sort (Pattern variable Attribute.Null))
270+
(Pattern variable Attribute.Null)
271+
where
272+
from = Recursive.embed . (:<) Attribute.Null . from
273+
{-# INLINE CONLIKE from #-}
274+
275+
instance
276+
From
277+
(Application SymbolOrAlias (Pattern variable Attribute.Null))
278+
(Pattern variable Attribute.Null)
279+
where
280+
from = Recursive.embed . (:<) Attribute.Null . from
281+
{-# INLINE CONLIKE from #-}
282+
283+
instance
284+
From
285+
(Bottom Sort (Pattern variable Attribute.Null))
286+
(Pattern variable Attribute.Null)
287+
where
288+
from = Recursive.embed . (:<) Attribute.Null . from
289+
{-# INLINE CONLIKE from #-}
290+
291+
instance
292+
From
293+
(Ceil Sort (Pattern variable Attribute.Null))
294+
(Pattern variable Attribute.Null)
295+
where
296+
from = Recursive.embed . (:<) Attribute.Null . from
297+
{-# INLINE CONLIKE from #-}
298+
299+
instance
300+
From
301+
(DomainValue Sort (Pattern variable Attribute.Null))
302+
(Pattern variable Attribute.Null)
303+
where
304+
from = Recursive.embed . (:<) Attribute.Null . from
305+
{-# INLINE CONLIKE from #-}
306+
307+
instance
308+
From
309+
(Equals Sort (Pattern variable Attribute.Null))
310+
(Pattern variable Attribute.Null)
311+
where
312+
from = Recursive.embed . (:<) Attribute.Null . from
313+
{-# INLINE CONLIKE from #-}
314+
315+
instance
316+
From
317+
(Exists Sort variable (Pattern variable Attribute.Null))
318+
(Pattern variable Attribute.Null)
319+
where
320+
from = Recursive.embed . (:<) Attribute.Null . from
321+
{-# INLINE CONLIKE from #-}
322+
323+
instance
324+
From
325+
(Floor Sort (Pattern variable Attribute.Null))
326+
(Pattern variable Attribute.Null)
327+
where
328+
from = Recursive.embed . (:<) Attribute.Null . from
329+
{-# INLINE CONLIKE from #-}
330+
331+
instance
332+
From
333+
(Forall Sort variable (Pattern variable Attribute.Null))
334+
(Pattern variable Attribute.Null)
335+
where
336+
from = Recursive.embed . (:<) Attribute.Null . from
337+
{-# INLINE CONLIKE from #-}
338+
339+
instance
340+
From
341+
(Iff Sort (Pattern variable Attribute.Null))
342+
(Pattern variable Attribute.Null)
343+
where
344+
from = Recursive.embed . (:<) Attribute.Null . from
345+
{-# INLINE CONLIKE from #-}
346+
347+
instance
348+
From
349+
(Implies Sort (Pattern variable Attribute.Null))
350+
(Pattern variable Attribute.Null)
351+
where
352+
from = Recursive.embed . (:<) Attribute.Null . from
353+
{-# INLINE CONLIKE from #-}
354+
355+
instance
356+
From
357+
(In Sort (Pattern variable Attribute.Null))
358+
(Pattern variable Attribute.Null)
359+
where
360+
from = Recursive.embed . (:<) Attribute.Null . from
361+
{-# INLINE CONLIKE from #-}
362+
363+
instance
364+
From
365+
(Mu variable (Pattern variable Attribute.Null))
366+
(Pattern variable Attribute.Null)
367+
where
368+
from = Recursive.embed . (:<) Attribute.Null . from
369+
{-# INLINE CONLIKE from #-}
370+
371+
instance
372+
From
373+
(Next Sort (Pattern variable Attribute.Null))
374+
(Pattern variable Attribute.Null)
375+
where
376+
from = Recursive.embed . (:<) Attribute.Null . from
377+
{-# INLINE CONLIKE from #-}
378+
379+
instance
380+
From
381+
(Not Sort (Pattern variable Attribute.Null))
382+
(Pattern variable Attribute.Null)
383+
where
384+
from = Recursive.embed . (:<) Attribute.Null . from
385+
{-# INLINE CONLIKE from #-}
386+
387+
instance
388+
From
389+
(Nu variable (Pattern variable Attribute.Null))
390+
(Pattern variable Attribute.Null)
391+
where
392+
from = Recursive.embed . (:<) Attribute.Null . from
393+
{-# INLINE CONLIKE from #-}
394+
395+
instance
396+
From
397+
(Or Sort (Pattern variable Attribute.Null))
398+
(Pattern variable Attribute.Null)
399+
where
400+
from = Recursive.embed . (:<) Attribute.Null . from
401+
{-# INLINE CONLIKE from #-}
402+
403+
instance
404+
From
405+
(Rewrites Sort (Pattern variable Attribute.Null))
406+
(Pattern variable Attribute.Null)
407+
where
408+
from = Recursive.embed . (:<) Attribute.Null . from
409+
{-# INLINE CONLIKE from #-}
410+
411+
instance
412+
From
413+
(Top Sort (Pattern variable Attribute.Null))
414+
(Pattern variable Attribute.Null)
415+
where
416+
from = Recursive.embed . (:<) Attribute.Null . from
417+
{-# INLINE CONLIKE from #-}
418+
419+
instance
420+
From
421+
(Inhabitant (Pattern variable Attribute.Null))
422+
(Pattern variable Attribute.Null)
423+
where
424+
from = Recursive.embed . (:<) Attribute.Null . from
425+
{-# INLINE CONLIKE from #-}
426+
427+
instance From StringLiteral (Pattern variable Attribute.Null) where
428+
from = Recursive.embed . (:<) Attribute.Null . from
429+
{-# INLINE CONLIKE from #-}
430+
431+
instance From (SomeVariable variable) (Pattern variable Attribute.Null) where
432+
from = Recursive.embed . (:<) Attribute.Null . from
433+
{-# INLINE CONLIKE from #-}
434+
248435
fromPattern
249436
:: Pattern variable annotation
250437
-> Base

0 commit comments

Comments
 (0)