0 | ||| Selectively ported from agdARGS's Data.Recrod.SmartConstructors
 1 | |||
 2 | ||| Please port more if you want!
 3 | module Data.Record.SmartConstructors
 4 |
 5 | import Data.Record
 6 |
 7 | %hide Builtin.infixr.(#)
 8 |
 9 | %default total
10 |
11 | export infix 1 ::=
12 | namespace Check
13 |
14 |   public export
15 |   record Checkable
16 |     {a : String -> Type}
17 |     (f : Field a -> Type)
18 |     (flds : Fields a) where
19 |     constructor MkCheckable
20 |     mkCheckable : Record f flds
21 |
22 |   public export
23 |   record Entry
24 |     (a    : String -> Type)
25 |     (f    : Field a -> Type)
26 |     (flds : Fields a) where
27 |     constructor (::=)
28 |     name  : String
29 |     {auto 0 pos : IsYes (name `isField` flds)}
30 |     value : f (field (toWitness pos))
31 |
32 |   public export
33 |   Nil : Checkable f []
34 |   Nil = MkCheckable $ MkRecord []
35 |
36 |   public export
37 |   (::) : {flds : Fields a} ->
38 |          (entry : Entry a f flds) ->
39 |          Checkable f (remove (toWitness entry.pos)) ->
40 |          Checkable f flds
41 |   ((name ::= value) {pos}) :: rec
42 |     = MkCheckable
43 |     $ MkRecord
44 |     $ insertLookedup (toWitness pos) value rec.mkCheckable.content
45 |
46 |
47 | namespace Infer
48 |
49 |   public export
50 |   record Inferrable
51 |     {a : String -> Type}
52 |     (f : Field a -> Type)
53 |     (flds : Fields a) where
54 |     constructor MkInferrable
55 |     mkInferrable : Record f flds
56 |
57 |   public export
58 |   record Entry (a : String -> Type) (f : Field a -> Type) where
59 |     constructor (::=)
60 |     name  : String
61 |     {type : a name}
62 |     value : f (name ** type)
63 |
64 |   public export
65 |   Nil : Inferrable f []
66 |   Nil = MkInferrable $ MkRecord []
67 |
68 |   public export
69 |   (::) : {flds : Fields a} ->
70 |          (entry : Entry a f) ->
71 |          (rec : Inferrable f flds) ->
72 |     {auto 0 fresh : (entry.name ** entry.type) # flds} ->
73 |     Inferrable f ((entry.name ** entry.type) :: flds)
74 |   ((name ::= value) :: rec)
75 |     = MkInferrable
76 |     $ MkRecord
77 |     $ (value :: rec.mkInferrable.content)
78 |
79 | ||| A record where the notion of type for its fields is `Type` itself
80 | public export
81 | BasicRecord : (f : Type -> Type) -> Fields (const Type) -> Type
82 | BasicRecord f flds = Record (\ x => f (snd x)) flds
83 |
84 | ||| This acts as a type annotation ensuring the list passed as an
85 | ||| argument is a basic record.
86 | public export
87 | mkBasicRecord : BasicRecord f flds -> BasicRecord f flds
88 | mkBasicRecord rec = rec
89 |