Predicate.Util_TH

Template Haskell methods for creating Refined* 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 OL (Between 100 125 Id) Int
Refined 123

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

interactive:8:4: error:
    * refinedTH: predicate failed with False (100 <= 99)
    * In the Template Haskell splice $$(refinedTH 99)
      In the expression:
          $$(refinedTH 99) :: Refined OL (Between 100 125 Id) Int

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

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

creates a Refined refinement type running in IO

Refined2

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

creates a Refined2 refinement type

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

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

interactive:127:4: error:
    * Step 2. False Boolean Check(op) | {100 <= 99}
*** Step 1. Success Initial Conversion(ip) (99) ***
P Id 99
*** Step 2. False Boolean Check(op) ***
Present False 100 <= 99
|
+- P Id 99
|
+- P '100
|
`- P '125

    * In the Template Haskell splice $$(refined2TH 99)
      In the expression:
          $$(refined2TH 99) :: Refined2 OAN Id (Between 100 125 Id) Int

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

creates a Refined2 refinement type using IO

Refined3

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

creates a Refined3 refinement type

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

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

interactive:127:4: error:
    * Step 2. False Boolean Check(op) | {100 <= 99}
*** Step 1. Success Initial Conversion(ip) (99) ***
P Id 99
*** Step 2. False Boolean Check(op) ***
Present False 100 <= 99
|
+- P Id 99
|
+- P '100
|
`- P '125

    * In the Template Haskell splice $$(refined3TH 99)
      In the expression:
          $$(refined3TH 99) :: Refined3 OAN Id (Between 100 125 Id) Id Int

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

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

creates a Refined3 refinement type using IO

Refined5

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

creates a Refined5 refinement type

>>> $$(refined5TH 100) :: Refined5 OAN Id (Between 100 125 Id) Int
Refined5 100

>$$(refined5TH 99) :: Refined5 OAN Id (Between 100 125 Id) Int

interactive:127:4: error:
    * Step 2. False Boolean Check(op) | {100 <= 99}
*** Step 1. Success Initial Conversion(ip) (99) ***
P Id 99
*** Step 2. False Boolean Check(op) ***
Present False 100 <= 99
|
+- P Id 99
|
+- P '100
|
`- P '125

    * In the Template Haskell splice $$(refined5TH 99)
      In the expression:
          $$(refined5TH 99) :: Refined5 OAN Id (Between 100 125 Id) Int

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

creates a Refined5 refinement type using IO