0 | ||| An ordered record is a record whose field names have to appear in
  1 | ||| a fixed order, but must otherwise be distinct.
  2 | module Data.Record
  3 |
  4 | import public Data.List.Fresh
  5 | import public Data.List.Fresh.Quantifiers
  6 | import Data.Fin
  7 | import Data.DPair
  8 | import public Decidable.Decidable.Extra1
  9 | import public Decidable.Equality
 10 |
 11 | %hide Builtin.infixr.(#)
 12 |
 13 | %default total
 14 |
 15 | public export
 16 | ArgList : Type
 17 | ArgList = FreshList String String.(##)
 18 |
 19 | public export
 20 | Field : (String -> Type) -> Type
 21 | Field a = (nm : String ** a nm)
 22 |
 23 | public export
 24 | Fields : (String -> Type) -> Type
 25 | Fields a = FreshList (Field a) ((##) `on` fst)
 26 |
 27 | public export
 28 | record Record {0 A : String -> Type}
 29 |               (0 F : Field A -> Type)
 30 |               (0 Flds : Fields A) where
 31 |   constructor MkRecord
 32 |   content : All F Flds
 33 |
 34 | namespace Record
 35 |
 36 |   public export
 37 |   map : {flds : Fields a} -> ((x : Field a) -> f x -> g x) ->
 38 |     Record f flds -> Record g flds
 39 |   map f (MkRecord rec) = MkRecord (All.map f rec)
 40 |
 41 | public export
 42 | IsField : (fldName : String) -> (flds : Fields a) -> Type
 43 | IsField fldName flds = Any (\ u => fldName === fst u) flds
 44 |
 45 | public export
 46 | isYesBecause : (d : Dec p) -> p -> IsYes d
 47 | isYesBecause (Yes prf) p = ItIsYes
 48 | isYesBecause (No nprf) p = absurd (nprf p)
 49 |
 50 | -- Todo: move to base
 51 | public export
 52 | soNotToEq : {b : Bool} -> So (not b) -> b = False
 53 | soNotToEq {b = False} Oh = Refl
 54 |
 55 | public export
 56 | stringEq : {x, y : String} -> x === y -> (x == y) === True
 57 | stringEq eq = go (decEq x y `isYesBecause` eq) where
 58 |
 59 |   go : IsYes (decEq x y) -> (x == y) === True
 60 |   go p with (x == y)
 61 |    go p | True = Refl
 62 |
 63 | public export
 64 | IsFieldStale : nm `IsField` flds -> fst nmv === nm ->
 65 |                (0 fresh : nmv # flds) -> Void
 66 | IsFieldStale (Here Refl) eq fresh
 67 |   = absurd $ trans (sym $ stringEq eq) (soNotToEq $ fst $ soAnd fresh)
 68 | IsFieldStale (There pos) eq fresh
 69 |   = IsFieldStale pos eq (snd $ soAnd fresh)
 70 |
 71 | public export
 72 | IsFieldIrrelevant : (p, q : nm `IsField` flds) -> p === q
 73 | IsFieldIrrelevant (Here Refl) (Here Refl) = Refl
 74 | IsFieldIrrelevant (Here Refl) (There {fresh} p)
 75 |   = void $ IsFieldStale p Refl fresh
 76 | IsFieldIrrelevant (There {fresh} p) (Here Refl)
 77 |   = void $ IsFieldStale p Refl fresh
 78 | IsFieldIrrelevant (There p) (There q)
 79 |   = cong There (IsFieldIrrelevant p q)
 80 |
 81 | public export
 82 | isField : (fldName : String) -> (flds : Fields a) ->
 83 |   Dec (fldName `IsField` flds)
 84 | isField fldName flds = any (\u => decEq fldName (fst u)) flds
 85 |
 86 | public export
 87 | field : {flds : Fields a} -> (pos : Any p flds) -> Field a
 88 | field pos = lookup pos
 89 |
 90 | public export
 91 | (.project) : {flds : Fields a} -> (rec : Record f flds) -> (name : String) ->
 92 |   {auto pos : IsYes $ name `isField` flds} -> f (field $ toWitness pos)
 93 | rec.project name = rec.content !! _
 94 |
 95 | public export
 96 | tabulate :
 97 |   (args : ArgList) ->
 98 |   (f : (arg : String) -> Any (arg ===) args -> a arg) ->
 99 |   Fields a
100 |
101 | public export
102 | 0 tabulateFreshness : {0 a : String -> Type} -> (args : ArgList) ->
103 |   (f : (arg : String) -> Any (arg ===) args -> a arg) ->
104 |   {0 y : String} -> {0 u : a y} ->
105 |   (y # args) -> (y ** u) # tabulate args f
106 |
107 | tabulate [] f = []
108 | tabulate ((x :: xs) {fresh}) f
109 |   = ((x ** f x (Here Refl)) :: tabulate xs (\u, pos => f u $ There pos))
110 |     {fresh = tabulateFreshness xs _ fresh}
111 |
112 | tabulateFreshness    []     f fresh = Oh
113 | tabulateFreshness (x :: xs) f fresh
114 |   = let (y_fresh_x, y_fresh_xs) = soAnd fresh in
115 |     andSo (y_fresh_x, tabulateFreshness xs _ y_fresh_xs)
116 |
117 | public export
118 | map : (f : (nm : String) -> a nm -> b nm) -> Fields a -> Fields b
119 | map f = Data.List.Fresh.map
120 |         (\ (nm ** a) => (nm ** f nm a))
121 |         (\(_**_), (_**_) => id)
122 |
123 | public export
124 | foldl : (f : b -> a -> b) -> b -> Record (const a) flds -> b
125 | foldl f x = foldl f x . content
126 |
127 | public export
128 | TypeFields : {flds : Fields a} ->
129 |              (rec : Record (const Type) flds ) -> Fields (const Type)
130 | TypeFields rec = Fresh.map (\ ((nm ** _) ** ty) => (nm ** ty))
131 |     (\((_**_) ** _),((_**_) ** _) => id)
132 |     (rec.content.toFreshList)
133 |
134 | public export
135 | PartialRecord : (f : Field a -> Type) -> Fields a -> Type
136 | PartialRecord f flds = Record (Maybe . f) flds
137 |
138 | public export
139 | traverse : {flds : Fields a} ->
140 |            Applicative m =>
141 |            ((x : Field a) -> f x -> m (g x)) ->
142 |            Record f flds  -> m (Record g flds)
143 | traverse f rec = MkRecord <$> (Quantifiers.traverse f rec.content)
144 |
145 | public export
146 | sequence : Applicative g =>
147 |            Record (g . f) flds  -> g (Record f flds)
148 | sequence rec = MkRecord <$> (Quantifiers.sequence rec.content)
149 |