0 | module Literal
 1 |
 2 | import Data.DPair
 3 |
 4 | %default total
 5 |
 6 | public export
 7 | interface CharLit (0 a : Type) where
 8 |   constructor CL
 9 |   0 CharPred : Char -> Type
10 |   fromChar : (c : Char) -> (0 p : CharPred c) => a
11 |
12 | public export
13 | interface DoubleLit (0 a : Type) where
14 |   constructor DL
15 |   0 DoublePred : Double -> Type
16 |   fromDouble : (d : Double) -> (0 p : DoublePred d) => a
17 |
18 | public export
19 | interface IntegerLit (0 a : Type) where
20 |   constructor IL
21 |   0 IntegerPred : Integer -> Type
22 |   fromInteger : (i : Integer) -> (0 p : IntegerPred i) => a
23 |
24 | public export
25 | interface StringLit (0 a : Type) where
26 |   constructor SL
27 |   0 StringPred : String -> Type
28 |   fromString : (s : String) -> (0 p : StringPred s) => a
29 |
30 | public export %inline
31 | Cast Char a => CharLit (Subset a p) where
32 |   CharPred = p . cast
33 |   fromChar c = Element (cast c) %search
34 |
35 | public export %inline
36 | Cast Double a => DoubleLit (Subset a p) where
37 |   DoublePred = p . cast
38 |   fromDouble d = Element (cast d) %search
39 |
40 | public export %inline
41 | Cast Integer a => IntegerLit (Subset a p) where
42 |   IntegerPred = p . cast
43 |   fromInteger i = Element (cast i) %search
44 |
45 | public export %inline
46 | Cast String a => StringLit (Subset a p) where
47 |   StringPred = p . cast
48 |   fromString s = Element (cast s) %search
49 |
50 | --------------------------------------------------------------------------------
51 | -- Utility constructors for elab deriving
52 | --------------------------------------------------------------------------------
53 |
54 | public export %inline
55 | mkIL :
56 |      (p : Integer -> Type)
57 |   -> ((i : Integer) -> (0 prf : p i) -> a)
58 |   -> IntegerLit a
59 | mkIL p f = IL p (\v => f v %search)
60 |
61 | public export %inline
62 | mkSL :
63 |      (p : String -> Type)
64 |   -> ((i : String) -> (0 prf : p i) -> a)
65 |   -> StringLit a
66 | mkSL p f = SL p (\v => f v %search)
67 |
68 | public export %inline
69 | mkCL :
70 |      (p : Char -> Type)
71 |   -> ((i : Char) -> (0 prf : p i) -> a)
72 |   -> CharLit a
73 | mkCL p f = CL p (\v => f v %search)
74 |
75 | public export %inline
76 | mkDL :
77 |      (p : Double -> Type)
78 |   -> ((i : Double) -> (0 prf : p i) -> a)
79 |   -> DoubleLit a
80 | mkDL p f = DL p (\v => f v %search)
81 |
82 | public export %inline
83 | ilPlain : (Integer -> a) -> IntegerLit a
84 | ilPlain f = IL (const ()) (\v => f v)
85 |
86 | public export %inline
87 | clPlain : (Char -> a) -> CharLit a
88 | clPlain f = CL (const ()) (\v => f v)
89 |
90 | public export %inline
91 | slPlain : (String -> a) -> StringLit a
92 | slPlain f = SL (const ()) (\v => f v)
93 |
94 | public export %inline
95 | dlPlain : (Double -> a) -> DoubleLit a
96 | dlPlain f = DL (const ()) (\v => f v)
97 |