Generic to row

Main.purs

module Main where

import Prelude

import Data.Foldable (fold)
import Effect (Effect)
import TryPureScript (h1, h2, p, text, list, indent, link, render, code)


import Data.Generic.Rep (class Generic, Argument(..), Constructor(..), Product(..), from)
import Data.Symbol (class IsSymbol)
import Data.Typelevel.Num (class Nat, class Succ, type (:*), D0, D1, D2, D3, D4, D5, D6, D7, D8, D9)
import Effect (Effect)
import Effect.Console (log)
import Prim.Row (class Cons, class Lacks)
import Prim.Symbol (class Append)
import Record as Record
import Type.Proxy (Proxy(..))

class Nat n <= NatToSym (n :: Type) (s :: Symbol) | n -> s
instance natToSymD0 :: NatToSym D0 "0"
instance natToSymD1 :: NatToSym D1 "1"
instance natToSymD2 :: NatToSym D2 "2"
instance natToSymD3 :: NatToSym D3 "3"
instance natToSymD4 :: NatToSym D4 "4"
instance natToSymD5 :: NatToSym D5 "5"
instance natToSymD6 :: NatToSym D6 "6"
instance natToSymD7 :: NatToSym D7 "7"
instance natToSymD8 :: NatToSym D8 "8"
instance natToSymD9 :: NatToSym D9 "9"
instance natToSymDCons :: (Nat (x :* y), NatToSym x sx, NatToSym y sy, Append sx "_" s0, Append s0 sy o) => NatToSym (x :* y) o

class Nat n <= GenericToRow n a r | n a -> r where
  genericToRow :: Proxy n -> a -> { | r }

instance genericToRowConstructor :: GenericToRow n rest r => GenericToRow n (Constructor sym rest) r where
  genericToRow px (Constructor rest) = genericToRow px rest

instance genericToRowProductCont :: (IsSymbol sym, NatToSym n sym', Append "_" sym' sym, Succ n nPlus1, GenericToRow nPlus1 (Product c d) r', Lacks sym r', Cons sym a r' r)=> GenericToRow n (Product (Argument a) (Product c d)) r where
  genericToRow _ (Product (Argument a) b) = Record.insert (Proxy :: _ sym) a (genericToRow (Proxy :: _ nPlus1) b)

instance genericToRowProductEnd :: (IsSymbol sym0, NatToSym n sym0', Append "_" sym0' sym0, Succ n nPlus1, Lacks sym0 (), Cons sym0 a () r', IsSymbol sym1, NatToSym nPlus1 sym1', Append "_" sym1' sym1, Lacks sym1 r', Cons sym1 b r' r)=> GenericToRow n (Product (Argument a) (Argument b)) r where
  genericToRow _ (Product (Argument a) (Argument b)) = Record.insert (Proxy :: _ sym1) b (Record.insert (Proxy :: _ sym0) a {})


asRow :: forall t rep r. Generic t rep => GenericToRow D0 rep r => t -> { | r }
asRow = genericToRow (Proxy :: _ D0) <<< from

data Foo a b c = Foo a b c

derive instance genericFoo :: Generic (Foo a b c) _


main :: Effect Unit
main =
  render $ fold
    [ h1 (text (show $ asRow (Foo 1 42.3 true)))]