records.idr

module Records
import Data.String
import Data.Maybe
import Data.List
import Data.List.Elem
import Data.Vect
import Data.Morphisms
import Decidable.Equality
import Data.IOArray.Prims

infixr 10 :->
infixr 10 !!
infixr 3 <*~>
infixr 4 <$~>

data Any : Type where 
  MkAny : a -> Any

unsafeGetAny : Any -> a
unsafeGetAny (MkAny a) = believe_me a

public export
RecordSpec : Type -> Type
RecordSpec k = List (String, k)

public export
data RecordEntry : String -> Type -> Type where
  (:->) : (0 s:String) -> t -> RecordEntry s t

export
data RecordBuilder : (RecordSpec specType) -> (specType -> Type) -> Type where
  MkRecordBuilder : (ArrayData Any -> Int -> IO ()) -> RecordBuilder s f

export    
Nil : RecordBuilder Nil c
Nil = MkRecordBuilder $ \a, ix => pure ()

export
(::) : {s:String} -> 
       {0 f:k -> Type} ->
       {t: k} -> 
       RecordEntry s (f t) -> 
       RecordBuilder xs f -> 
       RecordBuilder ((s, t) :: xs) f
(_ :-> x) :: MkRecordBuilder builder = MkRecordBuilder $ \arr, ix => 
  do primIO $ prim__arraySet arr ix (MkAny x)
     builder arr (ix+1)

public export    
AllConstraints : (a -> Type) -> List a -> Type
AllConstraints f [] = ()
AllConstraints f (c::cs) = (f c, AllConstraints f cs)

public export
OverSpec : (k -> Type) -> (String, k) -> Type
OverSpec c (name, value) = c value

public export
AllSpecs : (k -> Type) -> RecordSpec k -> Type
AllSpecs c = AllConstraints (OverSpec c)

-- proof that the spec has some field with a given type.
public export
data HasField : (s:String) -> (t:k) -> RecordSpec k -> Type where
  [search s]
  FirstField : HasField s t ((s, t) :: _)
  NextField : (0 prf : (t == s) === False) => HasField s v xs -> HasField s v ((t, w) :: xs)
%builtin Natural HasField

public export
implementation Uninhabited (HasField s t []) where
  uninhabited FirstField impossible
  uninhabited NextField impossible

public export
HasField' : RecordSpec k -> (String, k) -> Type
HasField' r (s, t) = HasField s t r

public export
HasFields : (l:RecordSpec k) -> RecordSpec k -> Type
HasFields l r = AllConstraints (HasField' r)  l

data IsNothing : Maybe a -> Type where
  ItIsNothing : IsNothing Nothing

-- proof that an optional field with the given type exists.
-- present.  This is written in terms of HasField, so it is  be
-- isomorphic to Maybe Natural, and can use efficient indexing.
public export
data HasOptionalField : (s:String) -> (t:k) -> RecordSpec k -> Type where
  NoSuchField : IsNothing (lookup s specs) => HasOptionalField s t specs
  FieldExists : HasField s t specs => HasOptionalField  s t specs

public export
HasOptionalField' : RecordSpec k -> (String, k) -> Type
HasOptionalField' r (s, t) = HasOptionalField s t r

public export
HasOptionalFields : (l:RecordSpec k) -> RecordSpec k -> Type
HasOptionalFields l r = AllConstraints (HasOptionalField' r)  l

public export
remField : RecordSpec k -> (String, k) -> RecordSpec k
remField [] _ = []
remField ((s, k) :: specs) (t, l) = 
  if (s == t) then specs else (s, k) :: remField specs (t, l)

public export
remFields :  (l:RecordSpec k)
          -> RecordSpec k 
          -> RecordSpec k
remFields spec [] = spec
remFields spec (x :: xs) = remFields (remField spec x) xs

public export
data NubFields : RecordSpec k -> RecordSpec k -> RecordSpec k ->Type where
  MkNubFields : {spec:RecordSpec k} -> {fields: RecordSpec k} -> NubFields spec fields (remFields spec fields)

public export
data WithRecordFields :  RecordSpec k
                      -> RecordSpec k 
                      -> RecordSpec k
                      -> RecordSpec k 
                      -> Type where
  MkWithRecordFields :  {spec:RecordSpec k} 
                     -> {mandatory: RecordSpec k}
                     -> {optional: RecordSpec k}
                     -> {other: RecordSpec k}
                     -> HasFields spec mandatory
                     => NubFields spec (optional ++ mandatory) other
                     => WithRecordFields spec mandatory optional other

export
data Record : RecordSpec specType -> (specType -> Type) -> Type where
  MkRecord : Int -> ArrayData Any -> Record s f

public export
SimpleRecord : RecordSpec Type -> Type
SimpleRecord s = Record s Prelude.id

export
recordHead : Record ((l, x) :: rs) f -> f x
recordHead (MkRecord ix arr) = 
  unsafeGetAny $ unsafePerformIO $ primIO $ prim__arrayGet arr ix

export
recordTail : Record (_ :: rs) f -> Record rs f
recordTail (MkRecord ix arr) = MkRecord (ix+1) arr

namespace RecordView
  public export
  data RecordView : (sp : RecordSpec k) -> (f : k -> Type) -> Type where
    Nil : RecordView [] f
    (::) : {0 f : k -> Type} -> RecordEntry s (f t) -> Record xs f -> RecordView ((s, t) :: xs) f

export
recordView : {spec:RecordSpec k} -> 
             Record spec f -> 
             RecordView spec f
recordView {spec=[]} _ = []
recordView {spec=(lbl,t)::xs} r = (lbl :-> recordHead r) :: recordTail r

public export
RecordEntryType : (l:RecordSpec k) -> (s:String) -> (k -> Type) -> HasField s t l  => Type
RecordEntryType ((s, t) :: _) s f @{FirstField} = f t
RecordEntryType (_ :: xs) s f @{NextField x} = RecordEntryType xs s f

export
buildRecord : {s: RecordSpec specType} -> RecordBuilder s f -> Record s f
buildRecord {s} (MkRecordBuilder builder) = unsafePerformIO $
  do newArr <- primIO $ prim__newArray (cast $ length s) (MkAny ())
     builder newArr 0
     pure $ MkRecord 0 newArr

export  
hasFieldToIndex : HasField s t r -> Integer
hasFieldToIndex FirstField = 0
hasFieldToIndex (NextField prevField) = 1 + hasFieldToIndex prevField
%builtin NaturalToInteger hasFieldToIndex

export
get : (0 s:String) -> HasField s t r => Record r f -> (f t)
get @{fld} s (MkRecord ix arr) = 
  unsafeGetAny $ unsafePerformIO $  primIO $ prim__arrayGet arr $
  (cast $ hasFieldToIndex fld) + ix

export
getMaybe : (0 s:String) -> HasOptionalField s t r => Record r f -> Maybe (f t)
getMaybe _ @{NoSuchField} _ = Nothing
getMaybe s @{FieldExists} rl = Just $ get s rl

export
getOpt : (0 s:String) -> HasOptionalField s t r => Lazy (f t) -> Record r f -> f t
getOpt s def r = fromMaybe def $ getMaybe s r

mapRecordBuilder : {specs:RecordSpec k} ->
                   ({a : k} -> f a -> g a) -> 
                   Record specs f ->
                   RecordBuilder specs g
mapRecordBuilder f r with (recordView r)
  _ | [] = []
  _ | ((lbl :-> v) :: y) = (lbl :-> f v) :: mapRecordBuilder f y
  
export  
mapRecord : {specs: RecordSpec k} -> 
            ({a : k} -> f a -> g a) ->
             Record specs f ->
             Record specs g
mapRecord f r = buildRecord $ mapRecordBuilder f r

fillRecordBuilder : (s:RecordSpec k) -> (forall a. f a) -> RecordBuilder s f
fillRecordBuilder [] v = []
fillRecordBuilder ((s, x) :: xs) v = (s :-> v) :: fillRecordBuilder xs v

export
fillRecord  : (s:RecordSpec k) -> (forall a. f a) -> Record s f
fillRecord r v = buildRecord $ fillRecordBuilder r v

zipWithRecordBuilder :  ({a : k} -> f a -> g a -> h a) ->
                     {s: RecordSpec k} ->
                     Record s f ->
                     Record s g ->
                     RecordBuilder s h
zipWithRecordBuilder f r1 r2 with ((recordView r1, recordView r2))
  _ | ([], []) = []
  _ | (lbl :-> x :: z, lbl :-> y :: w) = 
         lbl :-> f x y :: zipWithRecordBuilder f z w

export
zipWithRecord : ({a : k} -> f a -> g a -> h a) ->
                {s: RecordSpec k} ->
                Record s f ->
                Record s g ->
                Record s h
zipWithRecord f r1 r2 = buildRecord $ zipWithRecordBuilder f r1 r2 

namespace Hkd
  public export
  data HkdList : (k -> Type) -> List k -> Type where
    Nil : HkdList f []
    (::) : {f:k -> Type} -> f a -> HkdList f b -> HkdList f (a :: b)

export
mapHkd : {g : k -> Type} -> (forall a . f a -> g a) -> HkdList f s -> HkdList g s
mapHkd f [] = []
mapHkd f (x :: y) = f x :: mapHkd f y

splitRow : {fs : List (k -> Type)} ->
           {as : RecordSpec k} ->
           HkdList (Record ((s, a) :: as)) fs -> 
           ( HkdList ($ a) fs
           , HkdList (Record as) fs)
splitRow [] = ([], [])
splitRow (r :: y) with (recordView r) 
  _ | ((lbl :-> x) :: z) =
        let (ls, zs) = splitRow y
        in (x :: ls, z :: zs)

zipWithManyRB : {fs : List (k -> Type)} ->
                {s : RecordSpec k} ->
                ({a : k} -> Hkd.HkdList ($ a) fs -> g a) ->
                Hkd.HkdList (Record s) fs -> 
                RecordBuilder s g
zipWithManyRB f l with (s)
  _ | [] = []
  _ | ((s1, a1) :: ss) = 
      let (l1, ls) = splitRow l 
      in s1 :-> f l1 :: zipWithManyRB f ls

export
zipWithManyRecord : {fs : List (k -> Type)} ->
                    {s : RecordSpec k} ->
                    ({a : k} -> Hkd.HkdList ($ a) fs -> g a) ->
                    Hkd.HkdList (\f => Record s f) fs -> 
                    Record s g
zipWithManyRecord f l = buildRecord $ zipWithManyRB f l 

export
foldMapRecord : Monoid m => 
                {spec:RecordSpec k} ->
                ({a : k} -> f a -> m) ->
                Record spec f -> m
foldMapRecord f r with (recordView r) 
  _ | [] = neutral
  _ | ((lbl :-> x) :: y) = f x <+> foldMapRecord f y

export
foldrRecord : {spec:RecordSpec k} ->
              ({a : k} -> f a -> acc -> acc) -> 
              acc -> 
              Record spec f -> 
              acc
foldrRecord f acc r with (recordView r)
  _ | [] = acc
  _ | ((_ :-> x) :: y) = f x $ foldrRecord f acc y

export
foldlRecord : {s : RecordSpec k} -> 
              ({a : k} -> acc -> f a -> acc) -> 
              acc -> 
              Record s f -> 
              acc
foldlRecord f acc r with (recordView r)
  _ | [] = acc
  _ | ((_ :-> x) :: y) = foldlRecord f (f acc x) y

export
recordToList : {s : RecordSpec k} -> 
               {a : Type} ->
               Record s (const a) -> 
               List a
recordToList = foldrRecord (::) []

recordBuilderLabels : (s : RecordSpec k) -> RecordBuilder s (const String)
recordBuilderLabels [] = []
recordBuilderLabels ((lbl, x) :: xs) = (lbl :-> lbl) :: recordBuilderLabels {s = xs}

export
recordLabels : (s : RecordSpec k) -> Record s (const String)
recordLabels s = buildRecord $ recordBuilderLabels s

recordBuilderDicts : (0 c : k -> Type) -> (s : RecordSpec k) -> (cs : AllSpecs c s) => RecordBuilder s c
recordBuilderDicts _ [] = []
recordBuilderDicts c ((s, x) :: xs) {cs=(c1,_)} = (s :-> c1) :: recordBuilderDicts c xs

export
recordDicts : (0 c : k -> Type) -> (l : RecordSpec k) -> (cs : AllSpecs c l) => Record l c
recordDicts c l {cs} = buildRecord $ recordBuilderDicts c l {cs=cs}

recordBuilderSpecs : (l : RecordSpec k) -> RecordBuilder l (const k)
recordBuilderSpecs [] = []
recordBuilderSpecs ((s, spec) :: xs) = s :-> spec :: recordBuilderSpecs xs

export
recordSpecs : (l : RecordSpec k) -> Record l (const k)
recordSpecs l = buildRecord $ recordBuilderSpecs l

export
{spec : RecordSpec k} -> 
  {f : k -> Type} -> 
  AllSpecs (\k => Show (f k)) spec =>
  Show (Record spec f) where
    show r = "[" <+>
             ( joinBy ", " $
               recordToList $ 
               zipWithManyRecord 
               (\ [showDict, lbl, x] => 
                 "(lbl" <+> " :-> " <+> show @{showDict} x <+> ")")
               [ recordDicts (\k => Show (f k)) spec
               , recordLabels spec
               , r]
             ) <+> "]"
        


testShow : {l:List (String, Type)} -> AllSpecs Show l => SimpleRecord l -> Record l (const String)
testShow x = zipWithManyRecord (\[d, x] => show @{d} x)
             [recordDicts Show l, x]

testx : Record [("anint", Int), ("astring", String)] Prelude.id
testx = buildRecord ["anint" :-> 3, "astring" :-> "foo"]