Skip to content

Latest commit

 

History

History
189 lines (156 loc) · 4.54 KB

Refined.md

File metadata and controls

189 lines (156 loc) · 4.54 KB
Raw

Refined is the simplest refinement type which validates the input

(see documentation doctests)

:load Predicate

newtype Refined opts p a
  • opt display options see README
  • p predicate on a
  • a input type
  1. reads in a number and checks to see that it is greater than 99
>newRefined @OU @(ReadP Int Id > 99) "123"
Right (Refined "123")
  1. tries to read in a number but fails
>newRefined @OU @(ReadP Int Id > 99) "1x2y3"
Left Error ReadP Int (1x2y3) (>)
  1. reads in a hexadecimal string and checks to see that it is between 99 and 256
--  (>>) forward composition
>newRefined @OU @(ReadBase Int 16 >> Between 99 256 Id) "000fe"
Right (Refined "000fe")
  1. reads in a hexadecimal string but fails the predicate check
>newRefined @OU @(ReadBase Int 16 >> Between 99 253 Id) "000fe"
Left False ((>>) False | {254 <= 253})
  1. same as 4. above but now we get details of where it went wrong
>newRefined @OU @(ReadBase Int 16 >> Between 99 253 Id) "000fe"
  1. reads in a string as time and does simple validation
>newRefined @OU @(Resplit ":" >> Map (ReadP Int Id) >> Len == 3) "12:01:05"
Right (Refined "12:01:05")
  • Resplit ":" split using regex using a colon as a delimiter ["12","01","05"]
  • Map (ReadP Int Id) Read in the values as Ints [12,1,5]
  • Len == 3 Check to see that the length of the list of Ints is 3

Testing out predicates

When using Refined the expression in p must result in a True/False
pab does not have that restriction so you can run the whole thing or the individual pieces
for less detail use pl\

>pu @(Resplit ":" >> Map (ReadP Int Id) >> Len == 3) "12:01:05"

>pu @(Resplit ":") "12:01:05"

>pu @(Map (ReadP Int Id)) ["12","01","05"]

>pu @(Len == 3) [12,1,5]
ex1 :: Refined OU (ReadP Int Id > 99) String
ex1 = $$(refinedTH "123")
>$$(refinedTH @OU @(Lt 3 || Gt 55) 44)

<interactive>:36:4: error:
    * refinedTH: predicate failed with False (False || False | (44 < 3) || (44 > 55))
False False || False | (44 < 3) || (44 > 55)
|
+- False 44 < 3
|  |
|  +- P Id 44
|  |
|  `- P '3
|
`- False 44 > 55
   |
   +- P Id 44
   |
   `- P '55

    * In the Template Haskell splice
        $$(refinedTH @OU @(Lt 3 || Gt 55) 44)
      In the expression: $$(refinedTH @OU @(Lt 3 || Gt 55) 44)
>$$(refinedTH @OU @(Len > 7 || Elem 3 Id) [1..5])
Refined [1,2,3,4,5]
it :: Refined ((Len > 7) || Elem 3 Id) [Int]
>$$(refinedTH @OU @(Len > 7 || Elem 7 Id) [1..5])


<interactive>:31:4: error:
    * refinedTH: predicate failed with False (False || False | (5 > 7) || (7 `elem` [1,2,3,4,5]))
False False || False | (5 > 7) || (7 `elem` [1,2,3,4,5])
|
+- False 5 > 7
|  |
|  +- P Len 5
|  |
|  `- P '7
|
`- False 7 `elem` [1,2,3,4,5]
   |
   +- P '7
   |
   `- P Id [1,2,3,4,5]

    * In the Template Haskell splice
        $$(refinedTH @OU @(Len > 7 || Elem 7 Id) [1 .. 5])
      In the expression:
        $$(refinedTH @OU @(Len > 7 || Elem 7 Id) [1 .. 5])
>$$(refinedTH @OU @(Re "^[A-Z][a-z]+$") "smith")

<interactive>:32:4: error:
    * refinedTH: predicate failed with False (Re (^[A-Z][a-z]+$))
False Re (^[A-Z][a-z]+$)
|
+- P '"^[A-Z][a-z]+$"
|
`- P Id "smith"

    * In the Template Haskell splice
        $$(refinedTH @OU @(Re "^[A-Z][a-z]+$") "smith")
      In the expression:
        $$(refinedTH @OU @(Re "^[A-Z][a-z]+$") "smith")
>$$(refinedTH @OU @(Re "^[A-Z][a-z]+$") "Smith")
Refined "Smith"
>$$(refinedTH @OU @(Msg "expected title case" $ Re "^[A-Z][a-z]+$") "smith")

<interactive>:34:4: error:
    * refinedTH: predicate failed with False (expected title case Re (^[A-Z][a-z]+$))
False expected title case Re (^[A-Z][a-z]+$)
|
+- P '"^[A-Z][a-z]+$"
|
`- P Id "smith"

    * In the Template Haskell splice
        $$(refinedTH
             @OU @(Msg "expected title case" $ Re "^[A-Z][a-z]+$") "smith")
>$$(refinedTH @OU @(GuardBool "expected title case" (Re "^[A-Z][a-z]+$")) "smith")

<interactive>:22:4: error:
    * refinedTH: predicate failed with Error expected title case (GuardBool (Re (^[A-Z][a-z]+$)))
[Error expected title case] GuardBool (Re (^[A-Z][a-z]+$))
|
+- False Re (^[A-Z][a-z]+$)
|  |
|  +- P '"^[A-Z][a-z]+$"
|  |
|  `- P Id "smith"
|
`- P '"expected title case"

    * In the Template Haskell splice
        $$(refinedTH
             @OU @(GuardBool "expected title case" (Re "^[A-Z][a-z]+$"))
             "smith")