module Core.Experiments.Discrimination where

{-

Experiments on discrimination trees (dtree)

We probably want them for level values, where a level is basically "Map (Maybe Val) Integer",
representing N₀ ⊔ (t₁ + N₁) ⊔ (t₂ + N₂) ⊔ ... ⊔ (tₙ + Nₙ) where Nᵢ are naturals and tᵢ are values.

There are several approaches to representing discrimination trees.
1 There's a classic FP flavor that uses nested types. It's fine for many purposes, but
  it has some performance disadvantage, because some operations need to either allocate
  closures on every nesting, or use consecutive lookup/insert instead of in-place update.
2 There's a version where we represent Map nesting explicitly as Mapᴺ for
  a runtime N integer. This is part of a known reduction of nested ADT-s to inductive
  families: https://gallais.github.io/blog/non-regular-parameters.html
  In Haskell it can be approximated either with Any and unsafe coercions, or
  with a "weakly typed tagged" representation, where we don't have type nesting
  but allow a bunch of illegal trees to be representable.
  The version with unsafe coercions is the most efficient, because we learn possible
  constructors at runtime from a plain Int and don't need extra layers of Haskell
  constructors.
-}
import Prelude hiding (lookup)
import Common hiding (empty)

--------------------------------------------------------------------------------
-- Version with nested types and closure-free insertion.
-- I try to make the generic implementation apparent.

data Tree = Leaf | Node2 Tree Tree | Node3 Tree Tree Tree
  deriving Show

data Map v = Map {
    mapLeaf  :: Maybe v
  , mapNode2 :: Maybe (Map (Map v))
  , mapNode3 :: Maybe (Map (Map (Map v)))
  }
  deriving (Show,Foldable)

makeFields ''Map

empty = Map Nothing Nothing Nothing

singleLeaf v = Just v
singleNode2 a b v = Just $ single a $ single b v
singleNode3 a b c v = Just $ single a $ single b $ single c v

single :: forall v. Tree -> v -> Map v
single Leaf          v = empty & leaf  .~ singleLeaf v
single (Node2 a b)   v = empty & node2 .~ singleNode2 a b v
single (Node3 a b c) v = empty & node3 .~ singleNode3 a b c v

lookup :: Tree -> Map v -> Maybe v
lookup Leaf          map = map^.leaf
lookup (Node2 a b)   map = map^.node2 >>= lookup a >>= lookup b
lookup (Node3 a b c) map = map^.node3 >>= lookup a >>= lookup b >>= lookup c

update :: Tree -> v -> (v -> v) -> Map v -> Map v
update = \t v f m -> case lookup t m of
  Nothing -> insert t v m
  Just v  -> insert t (f v) m

-- Maybe a can be viewed as a partial (Map () a)
updateMaybe :: a -> (a -> a) -> Maybe a -> Maybe a
updateMaybe = \a f -> \case
  Nothing -> Just a
  Just a' -> Just $ f a'

insert :: Tree -> v -> Map v -> Map v
insert Leaf v map =
  map & leaf %~ (
    updateMaybe v $
    id
  )
insert (Node2 a b) v map =
  map & node2 %~ (
    updateMaybe (single a $ single b v) $
    update a (single b v) $
    id
  )
insert (Node3 a b c) v map =
  map & node3 %~ (
    updateMaybe (single a $ single b $ single c v) $
    update a (single b $ single c v) $
    update b (single c v) $
    update c v $
    id
  )

mapToList :: Map v -> [(Tree, v)]
mapToList m =
     do {v <- toList (m^.leaf);
         pure (Leaf, v)}
  ++ do {m <- toList (m^.node2);
         (a, m) <- mapToList m;
         (b, v) <- mapToList m;
         pure (Node2 a b, v)}
  ++ do {m <- toList (m^.node3);
         (a, m) <- mapToList m;
         (b, m) <- mapToList m;
         (c, v) <- mapToList m;
         pure (Node3 a b c, v)}


--------------------------------------------------------------------------------