Predicate.Util_TH

Template Haskell methods for creating Refined, Refined2, and Refined3 refinement types

Refined

refinedTH :: forall opts p i. (Lift i, RefinedC opts p i) => i -> Q (TExp (Refined opts p i))

creates a Refined refinement type

>>> $$(refinedTH 123) :: Refined 'OZ (Between 100 125 Id) Int
Refined 123

>$$(refinedTH 99) :: Refined 'OZ (Between 100 125 Id) Int

interactive:8:4: error:
    * refinedTH: predicate failed with FalseP (100 <= 99)
    * In the Template Haskell splice $$(refinedTH 99)
      In the expression:
          $$(refinedTH 99) :: Refined (Between 100 125 Id) Int
      In an equation for 'it':
          it = $$(refinedTH 99) :: Refined (Between 100 125 Id) Int

>>> $$(refinedTH 123) :: Refined 'OAN (Between 100 125 Id) Int
Refined 123

>$$(refinedTH 99) :: Refined 'OAN (FailS "asdf" >> Between 100 125 Id) Int

interactive:116:4: error:
    *
[Error asdf] lhs failed >>
|
`- [Error asdf] Fail asdf
   |
   `- P 'asdf

refinedTH: predicate failed with FailP "asdf" ((>>) lhs failed)
    * In the Template Haskell splice $$(refinedTH 99)
      In the expression:
          $$(refinedTH 99) ::
            Refined (FailS "asdf" >> Between 100 125 Id) Int

refinedTHIO :: forall opts p i. (Lift i, RefinedC opts p i) => i -> Q (TExp (Refined opts p i))

Refined1

refined1TH :: forall opts ip op fmt i. (Show i, Show (PP ip i), Lift i, Lift (PP ip i), Refined1C opts ip op fmt i) => i -> Q (TExp (Refined1 opts ip op fmt i))

creates a Refined1 refinement type

>>> $$(refined1TH 100) :: Refined1 'OZ Id (Between 100 125 Id) Id Int
Refined1 100

>>> $$(refined1TH 100) :: Refined1 'OZ Id (Between 100 125 Id) Id Int
Refined1 100

>>> $$(refined1TH 100) :: Refined1 'OZ Id (Between 100 125 Id) Id Int
Refined1 100

>$$(refined1TH 99) :: Refined1 'OZ Id (Between 100 125 Id) Id Int

interactive:127:4: error:
    *
*** Step 1. Success Initial Conversion(ip) [99] ***

P Id 99

*** Step 2. False Boolean Check(op) ***

False 100 <= 99
|
+- P Id 99
|
+- P '100
|
`- P '125

refined1TH: predicate failed with Step 2. False Boolean Check(op) | {100 <= 99}
    * In the Template Haskell splice $$(refined1TH 99)
      In the expression:
          $$(refined1TH 99) :: Refined1 'OZ Id (Between 100 125 Id) Id Int
      In an equation for 'it':
          it = $$(refined1TH 99) :: Refined1 'OZ Id (Between 100 125 Id) Id Int

Refined2

refined2TH :: forall opts ip op i. (Show (PP ip i), Lift i, Lift (PP ip i), Refined2C opts ip op i) => i -> Q (TExp (Refined2 opts ip op i))

creates a Refined2 refinement type

>>> $$(refined2TH 100) :: Refined2 'OA Id (Between 100 125 Id) Int
Refined2 {r2In = 100, r2Out = 100}

>>> $$(refined2TH 100) :: Refined2 'OAN Id (Between 100 125 Id) Int
Refined2 {r2In = 100, r2Out = 100}

>$$(refined2TH 99) :: Refined2 'OAN Id (Between 100 125 Id) Int

interactive:127:4: error:
    *
*** Step 1. Success Initial Conversion(ip) [99] ***

P Id 99

*** Step 2. False Boolean Check(op) ***

False 100 <= 99
|
+- P Id 99
|
+- P '100
|
`- P '125

refined2TH: predicate failed with Step 2. False Boolean Check(op) | {100 <= 99}
    * In the Template Haskell splice $$(refined2TH 99)
      In the expression:
          $$(refined2TH 99) :: Refined2 'OZ Id (Between 100 125 Id) Id Int
      In an equation for 'it':
          it = $$(refined2TH 99) :: Refined2 'OZ Id (Between 100 125 Id) Id Int

refined2THIO :: forall opts ip op i. (Show (PP ip i), Lift i, Lift (PP ip i), Refined2C opts ip op i) => i -> Q (TExp (Refined2 opts ip op i))

Refined3

refined3TH :: forall opts ip op fmt i. (Show i, Show (PP ip i), Lift i, Lift (PP ip i), Refined3C opts ip op fmt i) => i -> Q (TExp (Refined3 opts ip op fmt i))

creates a Refined3 refinement type

>>> $$(refined3TH 100) :: Refined3 'OZ Id (Between 100 125 Id) Id Int
Refined3 {r3In = 100, r3Out = 100}

>>> $$(refined3TH 100) :: Refined3 'OAN Id (Between 100 125 Id) Id Int
Refined3 {r3In = 100, r3Out = 100}

>$$(refined3TH 99) :: Refined3 'OAN Id (Between 100 125 Id) Id Int

interactive:127:4: error:
    *
*** Step 1. Success Initial Conversion(ip) [99] ***

P Id 99

*** Step 2. False Boolean Check(op) ***

False 100 <= 99
|
+- P Id 99
|
+- P '100
|
`- P '125

refined3TH: predicate failed with Step 2. False Boolean Check(op) | {100 <= 99}
    * In the Template Haskell splice $$(refined3TH 99)
      In the expression:
          $$(refined3TH 99) :: Refined3 'OAN Id (Between 100 125 Id) Id Int
      In an equation for 'it':
          it = $$(refined3TH 99) :: Refined3 'OAN Id (Between 100 125 Id) Id Int

>>> $$(refined3TH @'OZ @(Resplit "\\." Id >> Map (ReadP Int Id) Id) @(All (0 <..> 0xff) Id && Len == 4) @(PrintL 4 "%03d.%03d.%03d.%03d" Id)  "200.2.3.4")
Refined3 {r3In = [200,2,3,4], r3Out = "200.002.003.004"}

refined3THIO :: forall opts ip op fmt i. (Show i, Show (PP ip i), Lift i, Lift (PP ip i), Refined3C opts ip op fmt i) => i -> Q (TExp (Refined3 opts ip op fmt i))