0 | module Data.Array.All
  1 |
  2 | import public Data.List
  3 | import public Data.List.Elem
  4 | import public Data.List.Quantifiers
  5 |
  6 | import Data.Array.Core
  7 | import Data.Array.Index
  8 | import Data.Linear
  9 | import Data.Linear.Token
 10 |
 11 | %default total
 12 |
 13 | public export
 14 | data El : List a -> List a -> Type where
 15 |   ZEl : El as as
 16 |   SEl : El as (v::bs) -> El as bs
 17 |
 18 | export
 19 | elToNat : El as bs -> Nat
 20 | elToNat ZEl     = 0
 21 | elToNat (SEl k) = S $ elToNat k
 22 |
 23 | export
 24 | 0 elLemma : (el : El as (v::bs)) -> LT (elToNat el) (length as)
 25 | elLemma ZEl     = LTESucc LTEZero
 26 | elLemma (SEl x) =
 27 |  let p := elLemma x
 28 |   in ?foo
 29 |
 30 | --------------------------------------------------------------------------------
 31 | -- Immutable heterogeneous arrays
 32 | --------------------------------------------------------------------------------
 33 |
 34 | ||| An immutable heterogeneous array of size `n`.
 35 | |||
 36 | ||| This has different performance characteristics than
 37 | ||| `Data.List.Quantifiers.All`: Lookup is `O(1)`, while
 38 | ||| prepending and appending is `O(n)`.
 39 | export
 40 | record ArrAll (f : a -> Type) (as : List a) where
 41 |   constructor AA
 42 |   arr : AnyPtr
 43 |
 44 | public export
 45 | 0 HArr : List Type -> Type
 46 | HArr = ArrAll Prelude.id
 47 |
 48 | public export
 49 | Index : (as : List a) -> Fin (length as) -> a
 50 | Index (x :: xs) FZ     = x
 51 | Index (x :: xs) (FS k) = Index xs k
 52 | Index [] _ impossible
 53 |
 54 | export
 55 | elemToFin : Elem a as -> Fin (length as)
 56 | elemToFin {as = _::_} Here      = FZ
 57 | elemToFin {as = _::_} (There x) = FS $ elemToFin x
 58 |
 59 | len : All f xs -> Nat
 60 | len []     = 0
 61 | len (_::t) = S $ len t
 62 |
 63 | export
 64 | 0 ElemLemma : (el : Elem a as) -> a === Index as (elemToFin el)
 65 | ElemLemma Here      = Refl
 66 | ElemLemma (There x) = ElemLemma x
 67 |
 68 | ||| Safely access a value in a heterogeneous array at the given position.
 69 | export %inline
 70 | at : ArrAll f as -> (x : Fin (length as)) -> f (Index as x)
 71 | at (AA ad) m = believe_me $ prim__arrayGet ad (cast $ finToNat m)
 72 |
 73 |
 74 | ||| Safely access a value in a heterogeneous array
 75 | ||| at the position of the given tag
 76 | export %inline
 77 | elem : ArrAll f as -> (0 a : _) -> (el : Elem a as) => f a
 78 | elem arr a = rewrite ElemLemma el in at arr (elemToFin el)
 79 |
 80 | --------------------------------------------------------------------------------
 81 | --          Immutable Heterogeneous Arrays
 82 | --------------------------------------------------------------------------------
 83 |
 84 | ||| A mutable array.
 85 | export
 86 | data MArrAll : (s : Type) -> (f : a -> Type) -> (as : List a) -> Type where
 87 |   MA : (arr : AnyPtr) -> MArrAll s f as
 88 |
 89 | public export
 90 | 0 MHArr : Type -> List Type -> Type
 91 | MHArr s = MArrAll s Prelude.id
 92 |
 93 | ||| Safely write a value to a mutable heterogeneous array.
 94 | export %inline
 95 | set : MArrAll s f as -> (x : Fin (length as)) -> f (Index as x) -> F1' s
 96 | set (MA arr) ix v = ffi (prim__arraySet arr (cast $ finToNat ix) (believe_me v))
 97 |
 98 | ||| Safely write a value to a mutable heterogeneous array.
 99 | export %inline
100 | setElem : MArrAll s f as -> f a -> (el : Elem a as) => F1' s
101 | setElem arr v = All.set arr (elemToFin el) (rewrite sym (ElemLemma el) in v)
102 |
103 | ||| Safely write a value to a mutable heterogeneous array.
104 | export
105 | setEls : MArrAll s f as -> All f bs -> (el : El as bs) -> F1' s
106 | setEls arr []             el t = () # t
107 | setEls ma@(MA arr) (v :: vs) el t =
108 |  let _ # t := ffi (prim__arraySet arr (cast $ elToNat el) (believe_me v)) t
109 |   in setEls ma vs %search t
110 |
111 | ||| Safely read a value from a mutable array.
112 | |||
113 | ||| This returns the values thus read with unrestricted quantity, paired
114 | ||| with a new linear token of quantity one to be further used in the
115 | ||| linear context.
116 | export %inline
117 | get : MArrAll s f as -> (x : Fin (length as)) -> F1 s (f $ Index as x)
118 | get (MA arr) ix t = believe_me (prim__arrayGet arr (cast $ finToNat ix)) # t
119 |
120 | export %inline
121 | getElem : MArrAll s f as -> (0 a : _) -> (el : Elem a as) => F1 s (f a)
122 | getElem arr ix = rewrite ElemLemma el in get arr (elemToFin el)
123 |
124 | export
125 | setElems : All f as -> All (`Elem` bs) as => MArrAll s f bs -> F1' s
126 | setElems []              _ t = () # t
127 | setElems (v::vs) @{_::_} x t = let _ # t := setElem x v t in setElems vs x t
128 |
129 | ||| Fills a new mutable heterogeneous array bound to linear computation `s`.
130 | export
131 | mall1 : All f as -> F1 s (MArrAll s f as)
132 | mall1 vs t =
133 |  let p # t := ffi (prim__emptyArray (cast $ len vs)) t
134 |      arr   := MA p
135 |      _ # t := setEls arr vs ZEl t
136 |   in arr # t
137 |
138 | export %inline
139 | unsafeFreeze : MArrAll s f as -> F1 s (ArrAll f as)
140 | unsafeFreeze (MA p) t = AA p # t
141 |
142 | ||| Fills a new mutable heterogeneous array
143 | export %inline
144 | mall : Lift1 s m => All f as -> m (MArrAll s f as)
145 | mall as = lift1 (mall1 as)
146 |
147 | --------------------------------------------------------------------------------
148 | -- Immutable Utilities
149 | --------------------------------------------------------------------------------
150 |
151 | ||| Creates a new immutable heterogeneous array
152 | export %inline
153 | all : All f as -> ArrAll f as
154 | all vs = run1 $ \t => let ma # t := mall1 vs t in unsafeFreeze ma t
155 |