Safe Haskell | None |
---|---|
Language | Haskell2010 |
Template Haskell methods for creating Refined* refinement types
Synopsis
- refinedTH :: forall opts p i. (Lift i, RefinedC opts p i) => i -> Q (TExp (Refined opts p i))
- refinedTHIO :: forall opts p i. (Lift i, RefinedC opts p i) => i -> Q (TExp (Refined opts p i))
- 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))
- 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))
- 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))
- 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))
- 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))
- 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))
Refined
refinedTH :: forall opts p i. (Lift i, RefinedC opts p i) => i -> Q (TExp (Refined opts p i)) Source #
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)) Source #
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)) Source #
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)) Source #
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)) Source #
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)) Source #
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)) Source #
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