Instance.hs

{-
SPDX-License-Identifier: AGPL-3.0-only

This file is part of `statebox/cql`, the categorical query language.

Copyright (C) 2019 Stichting Statebox <https://statebox.nl>

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Affero General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU Affero General Public License for more details.

You should have received a copy of the GNU Affero General Public License
along with this program.  If not, see <https://www.gnu.org/licenses/>.
-}
{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE ExplicitForAll        #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE LiberalTypeSynonyms   #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE DerivingStrategies #-}

module Language.CQL.Instance where

import           Control.DeepSeq
import           Control.Monad
import qualified Data.List             as List hiding (intercalate)
import           Data.Map.Strict       (Map, member, unionWith, (!))
import qualified Data.Map.Strict       as Map
import           Data.Kind
import           Data.Maybe
import           Data.Set              (Set)
import qualified Data.Set              as Set
import           Data.Typeable         hiding (typeOf)
import           Data.Void
import           Language.CQL.Collage  (Collage(..), assembleGens, attsFrom, fksFrom, typeOf)
import           Language.CQL.Common   (elem', fromListAccum, section, toMapSafely, Deps(..), Err, Kind(INSTANCE), MultiTyMap, TyMap, type (+))
import           Language.CQL.Instance.Algebra (Algebra(..), aAtt, Carrier, down1, evalSchTerm, evalSchTerm', nf, nf'', repr'', TalgGen(..))
import qualified Language.CQL.Instance.Algebra as A (simplify)
import           Language.CQL.Instance.Presentation (Presentation(..))
import qualified Language.CQL.Instance.Presentation as IP (toCollage, typecheck, Presentation(eqs))
import           Language.CQL.Mapping  as Mapping
import           Language.CQL.Options
import           Language.CQL.Prover
import           Language.CQL.Query
import           Language.CQL.Schema   as Schema
import           Language.CQL.Term     as Term
import           Language.CQL.Typeside as Typeside
import           Prelude               hiding (EQ)


-- | A database instance on a schema.  Contains a presentation, an algebra, and a decision procedure.
data Instance var ty sym en fk att gen sk x y
  = Instance
  { schema  :: Schema       var  ty sym en fk att
  , pres    :: Presentation var  ty sym en fk att gen sk
  , dp      :: EQ           Void ty sym en fk att gen sk     -> Bool
  , algebra :: Algebra      var  ty sym en fk att gen sk x y
  }

-- | True if the type algebra is empty, which approximates it being free,
-- which approximates it being conservative over the typeside.
freeTalg :: Instance var ty sym en fk att gen sk x y -> Bool
freeTalg (Instance _ _ _ (Algebra _ _ _ _ _ _ _ _ teqs)) = Prelude.null teqs

-- | Just syntactic equality of the theory for now.
instance TyMap Eq '[var, ty, sym, en, fk, att, gen, sk, x, y]
  => Eq (Instance var ty sym en fk att gen sk x y) where
  (==) (Instance schema'  (Presentation gens'  sks'  eqs' ) _ _)
       (Instance schema'' (Presentation gens'' sks'' eqs'') _ _)
    = (schema' == schema'') && (gens' == gens'') && (sks' == sks'') && (eqs' == eqs'')

instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk, x, y]
  => NFData (Instance var ty sym en fk att gen sk x y) where
  rnf (Instance s0 p0 dp0 a0) = deepseq s0 $ deepseq p0 $ deepseq dp0 $ rnf a0

-- | A dynamically typed instance.
data InstanceEx :: Type where
  InstanceEx
    :: forall var ty sym en fk att gen sk x y
    .  (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, gen, sk, x, y])
    => Instance var ty sym en fk att gen sk x y
    -> InstanceEx


-- | Converts an algebra into a presentation: adds one equation per fact in the algebra,
--   and one generator per element.  Presentations in this form are called saturated because
--   they are maximally large without being redundant.  @I(fk.x) = I(fk)(I(x))@
algebraToPresentation :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk], Ord y, Ord x)
  => Algebra var ty sym en fk att gen sk x y
  -> Presentation var ty sym en fk att x y
algebraToPresentation alg@(Algebra sch en' _ _ _ ty' _ _ _) =
  Presentation gens' sks' eqs'
  where
    gens'   = Map.fromList $ reify en' $ Schema.ens sch
    sks'    = Map.fromList $ reify ty' $ Typeside.tys $ Schema.typeside sch
    eqs1    = concatMap fksToEqs  reified
    eqs2    = concatMap attsToEqs reified
    eqs'    = Set.fromList $ eqs1 ++ eqs2
    reified = reify en' $ Schema.ens sch
    fksToEqs  (x, e) = (\(fk , _) -> fkToEq  x fk ) <$> fksFrom'  sch e
    attsToEqs (x, e) = (\(att, _) -> attToEq x att) <$> attsFrom' sch e
    fkToEq  x fk  = EQ (Fk fk   (Gen x), Gen $ aFk  alg fk  x)
    attToEq x att = EQ (Att att (Gen x), upp $ aAtt alg att x)

reify :: (Ord x, Ord en) => (en -> Set x) -> Set en -> [(x, en)]
reify f s = concat $ Set.toList $ Set.map (\en'-> Set.toList $ Set.map (, en') $ f en') s

-- | Checks that an 'Instance' satisfies its 'Schema'.
satisfiesSchema
  :: (MultiTyMap '[Show] '[var, ty, sym, en, fk, att, gen, sk, x, y], Eq x)
  => Instance var ty sym en fk att gen sk x y
  -> Err ()
satisfiesSchema (Instance sch pres' dp' alg) = do
  mapM_ (\(      EQ (l, r)) -> if hasTypeType l then report (show l) (show r) (instEqT l r) else report (show l) (show r) (instEqE l r)) $ Set.toList $ IP.eqs pres'
  mapM_ (\(en'', EQ (l, r)) -> report (show l) (show r) (schEqT l r en'')) $ Set.toList $ obs_eqs sch
  mapM_ (\(en'', EQ (l, r)) -> report (show l) (show r) (schEqE l r en'')) $ Set.toList $ path_eqs sch
  where
    -- Morally, we should create a new dp (decision procedure) for the talg, but that's computationally intractable, and this check still helps.
    instEqE l r = nf alg (down1 l) == nf alg (down1 r)
    instEqT l r = dp' $ EQ ((repr'' alg (nf'' alg l)), (repr'' alg (nf'' alg r)))

    report _ _ True  = return ()
    report l r False = Left $ "Not satisfied: " ++ l ++ " = " ++ r

    schEqE l r e = foldr (\x b -> (evalSchTerm' alg x l == evalSchTerm' alg x r) && b) True (en alg e)
    schEqT l r e = foldr (\x b -> dp' (EQ (repr'' alg (evalSchTerm alg x l), repr'' alg (evalSchTerm alg x r))) && b) True (en alg e)

-- | Constructs an algebra from a saturated theory with a free type algebra.
-- Needs to have satisfaction checked.
saturatedInstance
  :: forall var ty sym en fk att gen sk
  .  (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
  => Schema        var ty sym en fk att
  -> Presentation  var ty sym en fk att gen sk
  -> Err (Instance var ty sym en fk att gen sk gen (Either sk (gen, att)))
saturatedInstance sch (Presentation gens sks eqs) = do
  (fks, atts) <- foldM procEq (Map.empty, Map.empty) eqs
  checkTotality fks
  _ <- if Set.null (Typeside.eqs $ typeside sch) then return () else Left "Typeside must be free"
  let alg = Algebra sch (Set.fromList . gens') (nf1 fks) (nf2 fks) Gen (Set.fromList . sks' atts) (nf' atts) repr' Set.empty
  pure $ Instance sch (Presentation gens sks eqs) (\(EQ (l, r)) -> l == r) alg
  where
    checkTotality :: Map (gen, fk) gen -> Err ()
    checkTotality fks =
      mapM_ (\en -> if   List.null (fksMissing en fks)
                    then pure ()
                    else Left $ "Missing equation for " ++ show en) $ Schema.ens sch

    fksMissing  en fks  = [ gen | gen <- gens' en, (fk,  _) <- fksFrom'  sch en, not $ member (gen, fk ) fks  ]

    gens' en = [ gen | (gen, en') <- Map.toList gens, en == en' ]

    sks'  atts ty = [ Left sk  | (sk , ty') <- Map.toList sks , ty == ty' ] ++
      [ Right (gen, att) | enX :: en <- Set.toList (Schema.ens sch), gen <- gens' enX, (att, t) <- attsFrom' sch (enX :: en), not (member (gen, att) atts), t == ty ]

    --diff = sks'' en ty \\ atts
    repr' (Left g)         = Sk g
    repr' (Right (x, att)) = Att att $ Gen x

    procEq (fks, atts) (EQ (Fk fk (Gen gen), Gen gen')) = case Map.lookup (gen, fk) fks  of
      Nothing    -> pure (Map.insert (gen, fk) gen' fks, atts)
      Just gen'' -> Left $ "Duplicate binding: " ++ show gen ++ " and " ++ show gen''

    procEq (fks, atts) (EQ (Att att (Gen gen), w)) | isJust p  = case Map.lookup (gen, att) atts of
      Nothing    -> pure (fks, Map.insert (gen, att) (fromJust p) atts)
      Just gen'' -> Left $ "Duplicate binding: " ++ show gen ++ " and " ++ show gen''
      where
        p = case w of
          Sk s     -> Just $ Sk $ Left s
          Sym s [] -> Just $ Sym s []
          _        -> Nothing

    procEq _ (EQ (l, r)) = Left $ "Bad eq: " ++ show l ++ " = " ++ show r

    nf1 _ g = g
    nf2 fks f a = fks ! (a, f)

    nf' _    (Left  sk) = Sk $ Left sk
    nf' atts (Right x ) = Map.findWithDefault (Sk (Right x)) x atts


---------------------------------------------------------------------------------------------------------------
-- Initial algebras

-- | Computes an initial instance (minimal model of a presentation).
-- Actually, computes the cannonical term model, where the underlying elements
-- of the carriers are equivalence class of terms modulo provable equality
-- in the presentation (differs from CQL java, which uses fresh IDs).
-- The term model is constructed by repeatedly adding news terms to the empty model
-- until a fixedpoint is reached.
initialInstance
  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
  => Presentation var  ty  sym  en  fk  att  gen  sk
  -> (EQ    (() + var) ty  sym  en  fk  att  gen  sk -> Bool)
  -> Schema       var  ty  sym  en  fk  att
  -> Instance     var  ty  sym  en  fk  att  gen  sk (Carrier en fk gen) (TalgGen en fk att gen sk)
initialInstance p dp' sch = Instance sch p dp'' $ initialAlgebra
  where
    dp'' (EQ (lhs, rhs)) = dp' $ EQ (upp lhs, upp rhs)
    initialAlgebra = A.simplify this
    this  = Algebra sch en' nf''' nf'''2 id ty' nf'''' repr'''' teqs'
    col   = IP.toCollage sch p
    ens'  = assembleGens col (close col dp')
    en' k = ens' ! k

    nf'''    e = nf'''_old $ Gen e
    nf'''2 f e = nf'''_old $ Fk  f e
    nf'''_old e = let
      t = typeOf col e
      f []    = error "impossible, please report"
      f (a:b) = if dp' (EQ (upp a, upp e)) then a else f b
      in f $ Set.toList $ ens' ! t

    tys' = assembleSks col ens'
    ty' y =  tys' ! y

    nf'''' (Left g)          = Sk $ MkTalgGen $ Left   g
    nf'''' (Right (gt, att)) = Sk $ MkTalgGen $ Right (gt, att)

    repr'''' :: TalgGen en fk att gen sk -> Term Void ty sym en fk att gen sk
    repr'''' (MkTalgGen (Left g))         = Sk g
    repr'''' (MkTalgGen (Right (x, att))) = Att att $ upp x

    teqs'' = concatMap (\(e, EQ (lhs,rhs)) -> fmap (\x -> EQ (nf'' this $ subst' lhs x, nf'' this $ subst' rhs x)) (Set.toList $ en' e)) $ Set.toList $ obs_eqs sch
    teqs' = Set.union (Set.fromList teqs'') (Set.map (\(EQ (lhs,rhs)) -> EQ (nf'' this lhs, nf'' this rhs)) (Set.filter hasTypeType' $ IP.eqs p))

-- | Assemble Skolem terms (labeled nulls).
assembleSks
  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
  => Collage var ty sym en fk att gen sk
  -> Map en (Set (Carrier en fk gen))
  -> Map ty (Set (TalgGen en fk att gen sk))
assembleSks col ens' = unionWith Set.union sks' $ fromListAccum gens'
  where
    gens' = concatMap
      (\(en',set) -> concatMap (\term -> concatMap (\(att,ty') -> [(ty',(MkTalgGen . Right) (term,att))]) $ attsFrom col en') $ Set.toList set)
      (Map.toList ens')
    sks'  = foldr (\(sk,t) m -> Map.insert t (Set.insert (MkTalgGen . Left $ sk) (m ! t)) m) ret $ Map.toList $ csks col
    ret   = Map.fromSet (const Set.empty) $ ctys col

instance NFData InstanceEx where
  rnf (InstanceEx x) = rnf x

-- TODO move to Collage? Algebra?
-- TODO move to Collage? Algebra?
-- TODO move to Collage? Algebra?
close
  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
  => Collage var  ty   sym  en fk att  gen sk
  -> (EQ     var  ty   sym  en fk att  gen sk    -> Bool)
  -> [Carrier en fk gen]
close col dp' =
  y (close1m dp' col) $ fmap Gen $ Map.keys $ cgens col
  where
    y f x = let z = f x in if x == z then x else y f z

close1m
  :: (Foldable t, MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
  => (EQ var ty sym en fk att gen sk -> Bool)
  -> Collage var ty sym en fk att gen sk
  -> t (Term Void Void Void en fk Void gen Void)
  -> [Carrier en fk gen]
close1m dp' col = dedup dp' . concatMap (close1 col dp')

dedup
  :: (EQ var ty sym en fk att gen sk -> Bool)
  -> [Carrier en fk gen]
  -> [Carrier en fk gen]
dedup dp' = List.nubBy (\x y -> dp' (EQ (upp x, upp y)))

close1
  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
  => Collage var ty sym en fk att gen sk
  -> (EQ var ty sym en fk att gen sk -> Bool)
  -> Carrier en fk gen
  -> [Carrier en fk gen]
close1 col _ e = e:(fmap (\(x,_) -> Fk x e) l)
  where
    t = typeOf col e
    l = fksFrom col t


--------------------------------------------------------------------------------------------------------
-- Instance syntax

data InstanceExp where
  InstanceVar     :: String                                          -> InstanceExp
  InstanceInitial :: SchemaExp                                       -> InstanceExp

  InstanceDelta   :: MappingExp -> InstanceExp -> [(String, String)] -> InstanceExp
  InstanceSigma   :: MappingExp -> InstanceExp -> [(String, String)] -> InstanceExp
  InstancePi      :: MappingExp -> InstanceExp                       -> InstanceExp

  InstanceEval    :: QueryExp   -> InstanceExp                       -> InstanceExp
  InstanceCoEval  :: MappingExp -> InstanceExp                       -> InstanceExp

  InstanceRaw     :: InstExpRaw'                                     -> InstanceExp
  InstancePivot   :: InstanceExp                                     -> InstanceExp

  deriving stock (Eq, Show)

instance Deps InstanceExp where
  deps x = case x of
    InstanceVar v                       -> [(v, INSTANCE)]
    InstanceInitial  t                  ->  deps t
    InstancePivot    i                  ->  deps i
    InstanceDelta  f i _                -> (deps f) ++ (deps i)
    InstanceSigma  f i _                -> (deps f) ++ (deps i)
    InstancePi     f i                  -> (deps f) ++ (deps i)
    InstanceEval   q i                  -> (deps q) ++ (deps i)
    InstanceCoEval q i                  -> (deps q) ++ (deps i)
    InstanceRaw (InstExpRaw' s _ _ _ i) -> (deps s) ++ (concatMap deps i)

getOptionsInstance :: InstanceExp -> [(String, String)]
getOptionsInstance x = case x of
  InstanceVar _                       -> []
  InstanceInitial  _                  -> []
  InstancePivot    _                  -> []
  InstanceDelta  _ _ o                -> o
  InstanceSigma  _ _ o                -> o
  InstancePi     _ _                  -> undefined
  InstanceEval   _ _                  -> undefined
  InstanceCoEval _ _                  -> undefined
  InstanceRaw (InstExpRaw' _ _ _ o _) -> o


----------------------------------------------------------------------------------------------------------------------
-- Literal instances

data InstExpRaw' =
  InstExpRaw'
  { instraw_schema  :: SchemaExp
  , instraw_gens    :: [(String, String)]
--, instraw_sks     :: [(String, String)] this should maybe change in cql grammar
  , instraw_oeqs    :: [(RawTerm, RawTerm)]
  , instraw_options :: [(String, String)]
  , instraw_imports :: [InstanceExp]
} deriving stock (Eq, Show)

type Gen = String
type Sk  = String

conv' :: (Typeable ty,Show ty) => [(String, String)] -> Err [(String, ty)]
conv' [] = pure []
conv' ((att,ty'):tl) = case cast ty' of
   Just ty'' -> do
    x <- conv' tl
    return $ (att, ty''):x
   Nothing -> Left $ "Not in schema/typeside: " ++ show ty'


split'' :: (Typeable en, Typeable ty, Eq ty, Eq en) => [en] -> [ty] -> [(a, String)] -> Err ([(a, en)], [(a, ty)])
split'' _     _   []           = return ([], [])
split'' ens2 tys2 ((w, ei):tl) = do
  (a,b) <- split'' ens2 tys2 tl
  if elem' ei ens2
  then return ((w, fromJust $ cast ei):a, b)
  else if elem' ei tys2
    then return (a, (w, fromJust $ cast ei):b)
    else Left $ "Not an entity or type: " ++ show ei

evalInstanceRaw'
  :: forall var ty sym en fk att
   . (MultiTyMap '[Ord, Typeable] '[ty, sym, en, fk, att])
  => Schema var ty sym en fk att
  -> InstExpRaw'
  -> [Presentation var ty sym en fk att Gen Sk]
  -> Err (Presentation var ty sym en fk att Gen Sk)
evalInstanceRaw' sch (InstExpRaw' _ gens0 eqs' _ _) is = do
  (gens', sks') <- split'' (Set.toList $ Schema.ens sch) (Set.toList $ tys $ typeside sch) gens0
  gens''        <- toMapSafely gens'
  gens'''       <- return $ Map.toList gens''
  sks''         <- toMapSafely sks'
  sks'''        <- return $ Map.toList sks''
  let gensX = concatMap (Map.toList . gens) is ++ gens'''
      sksX  = concatMap (Map.toList . sks ) is ++ sks'''
  eqs'' <- transEq gensX sksX eqs'
  pure $ Presentation (Map.fromList gensX) (Map.fromList sksX) $ Set.fromList $ (concatMap (Set.toList . IP.eqs) is) ++ (Set.toList eqs'')
  where
    keys' = map fst

    transEq _ _ [] = pure Set.empty
    transEq gens' sks' ((lhs, rhs):eqs'') = do
      lhs' <- transTerm (keys' gens') (keys' sks') lhs
      rhs' <- transTerm (keys' gens') (keys' sks') rhs
      rest <- transEq gens' sks' eqs''
      pure $ Set.insert (EQ (lhs', rhs')) rest

    transPath :: forall var' ty' sym' en' att'. [String] -> RawTerm -> Err (Term var' ty' sym' en' fk att' String Sk)
    transPath gens' (RawApp x [])  | elem  x gens' = pure $ Gen x
    transPath gens' (RawApp x [a]) | elem' x (Map.keys $ sch_fks sch) = Fk (fromJust $ cast x) <$> transPath gens' a
    transPath _ x = Left $ "cannot type " ++ show x

    transTerm :: [String] -> [String] -> RawTerm -> Err (Term Void ty sym en fk att Gen Sk)
    transTerm gens' _    (RawApp x [])  | elem  x gens' = pure $ Gen x
    transTerm _     sks' (RawApp x [])  | elem  x sks'  = pure $ Sk  x
    transTerm gens' _    (RawApp x [a]) | elem' x (Map.keys $ sch_fks  sch) = Fk  (fromJust $ cast x) <$> transPath gens' a
    transTerm gens' _    (RawApp x [a]) | elem' x (Map.keys $ sch_atts sch) = Att (fromJust $ cast x) <$> transPath gens' a
    transTerm gens' sks' (RawApp v l) = case cast v :: Maybe sym of
        Just x  -> Sym x <$> mapM (transTerm gens' sks') l
        Nothing -> Left $ "Cannot type: " ++ v

evalInstanceRaw
  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att])
  => Options
  -> Schema var ty sym en fk att
  -> InstExpRaw'
  -> [InstanceEx]
  -> Err InstanceEx
evalInstanceRaw ops ty' t is = do
  (i :: [Presentation var ty sym en fk att Gen Sk]) <- doImports is
  r <- evalInstanceRaw' ty' t i
  _ <- IP.typecheck ty' r
  l <- toOptions ops $ instraw_options t
  if bOps l Interpret_As_Algebra
  then do
    j <- saturatedInstance ty' r
    pure $ InstanceEx j
  else do
    p <- createProver (IP.toCollage ty' r) l
    pure $ InstanceEx $ initialInstance r (prv p) ty'
  where
    prv p (EQ (l,r)) = prove p (Map.fromList []) (EQ (l,  r))
    doImports [] = return []
    doImports (InstanceEx ts : r) = case cast (pres ts) of
      Nothing  -> Left "Bad import"
      Just ts' -> do { r' <- doImports r ; return $ ts' : r' }

---------------------------------------------------------------------------------------------------------------
-- Basic instances

-- | The empty instance on a schema has no data, so the types of its generators and carriers are 'Void'.
emptyInstance :: Schema var ty sym en fk att -> Instance var ty sym en fk att Void Void Void Void
emptyInstance ts'' =
  Instance
    ts''
    (Presentation Map.empty Map.empty Set.empty)
    (const undefined)
    (Algebra ts''
      (const Set.empty) (const undefined) (const undefined) (const undefined)
      (const Set.empty) (const undefined) (const undefined)
      Set.empty)

-- | Pivot an instance. The returned schema will not have strings as fks etc, so it will be impossible to write a literal on it, at least for now.
--   (Java CQL hacks around this by landing on String.)
pivot
  :: forall var ty sym en fk att gen sk x y
   . (MultiTyMap '[Show, Ord, Typeable] '[var, ty, sym, en, fk, att, gen, sk, x, y])
  => Instance   var ty sym     en      fk      att                    gen  sk  x  y
  -> ( Schema   var ty sym (x, en) (x, fk) (x, att)
     , Instance var ty sym (x, en) (x, fk) (x, att)  (x, en) y  (x, en)           y
     , Mapping  var ty sym (x, en) (x, fk) (x, att)      en  fk att
     )
pivot (Instance sch _ idp (Algebra _ ens _ fk fn tys nnf rep2'' teqs)) =
  (sch', inst, mapp)
  where
    sch'_ens  = Set.fromList [  (x, en)                                | en <- Set.toList (Schema.ens sch), x <- Set.toList (ens en)]
    sch'_fks  = Map.fromList [ ((x, fk0 ), ((x, en), (fk fk0 x, en'))) | en <- Set.toList (Schema.ens sch), x <- Set.toList (ens en), (fk0,  en') <- fksFrom'  sch en ]
    sch'_atts = Map.fromList [ ((x, att0), ((x, en),  ty'           )) | en <- Set.toList (Schema.ens sch), x <- Set.toList (ens en), (att0, ty') <- attsFrom' sch en ]
    sch'_peqs = Set.empty
    sch'_oeqs = Set.empty

    dp' :: EQ Void ty sym (x, en) (x, fk) (x, att) (x, en) y -> Bool
    dp' (EQ (l, r)) = idp $ EQ (instToInst l, instToInst r)

    ens' = Set.singleton
    gen' = id
    fk' (x, f) (x', _) | x == x' = (fk f x', snd $ Schema.sch_fks sch ! f)
                       | otherwise = error "anomaly, please report"
    rep'  = Gen
    nnf' (Left sk) = Sk sk
    nnf' (Right ((x, _), (x', att))) | x == x' = nnf $ Right (x', att)
                                     | otherwise = error "anomaly, please report"
    rep2' = Sk
    gens' = Map.fromList [ ((x, en), (x, en)) | en <- Set.toList (Schema.ens sch),              x <- Set.toList (ens en) ]
    sks'  = Map.fromList [ ( y, ty)           | ty <- Set.toList (Typeside.tys $ typeside sch), y <- Set.toList (tys ty) ]
    eqs'  = Set.map (\(EQ (x, y)) -> EQ (repr'' alg' x, repr'' alg' y)) teqs
    es'   = teqs
    tys'  = tys
    em    = Map.fromList [ ((x, en)  , en)               | en <- Set.toList (Schema.ens sch), x <- Set.toList (ens en) ]
    fm    = Map.fromList [ ((x, fk ) , Fk  fk  $ Var ()) | (x, fk ) <- Map.keys sch'_fks  ]
    am    = Map.fromList [ ((x, att) , Att att $ Var ()) | (x, att) <- Map.keys sch'_atts ]

    dp2 :: (x, en) -> EQ () ty sym (x, en) (x, fk) (x, att) Void Void -> Bool
    dp2 (x, _) (EQ (l, r)) = idp $ EQ (schToInst' x l, schToInst' x r)

    sch'  = Schema (typeside sch) sch'_ens sch'_fks sch'_atts sch'_peqs sch'_oeqs dp2
    alg'  = Algebra sch' ens' gen' fk' rep' tys' nnf' rep2' es'
    inst  = Instance sch' (Presentation gens' sks' eqs') dp' alg'
    mapp  = Mapping sch' sch em fm am

    schToInst'
      :: x
      -> Term ()   ty sym (x, en) (x, fk) (x, att) Void Void
      -> Term Void ty sym     en      fk      att  gen  sk
    schToInst' x z = case z of
      Sym f as     -> Sym f $ fmap (schToInst' x) as
      Att (_, f) a -> Att f $ schToInst' x a
      Sk x0        -> absurd x0
      Var ()       -> upp $ fn x
      Fk (_, f) a  -> Fk f $ schToInst' x a
      Gen x0       -> absurd x0

    instToInst :: Term Void ty sym (x, en) (x, fk) (x, att) (x, en) y -> Term Void ty sym en fk att gen sk
    instToInst z = case z of
      Sym f as     -> Sym f $ fmap instToInst as
      Att (_, f) a -> Att f $ instToInst a
      Sk y         -> rep2'' y
      Var x        -> absurd x
      Fk (_, f) a  -> Fk f $ instToInst a
      Gen (x, _)   -> upp $ fn x


---------------------------------------------------------------------------------------------------------------
-- Functorial data migration

subs
  :: (MultiTyMap '[Ord] '[ty, sym, en, fk, att, en', fk', att', gen, sk])
  => Mapping var ty sym en fk att en' fk' att'
  -> Presentation var ty sym en  fk  att  gen sk
  -> Presentation var ty sym en' fk' att' gen sk
subs (Mapping _ _ ens' fks' atts') (Presentation gens' sks' eqs') = Presentation gens'' sks' eqs''
  where
    gens'' = Map.map (\k -> ens' ! k) gens'
    eqs''  = Set.map (\(EQ (l, r)) -> EQ (changeEn fks' atts' l, changeEn fks' atts' r)) eqs'

changeEn
  :: (Ord k1, Ord k2, Eq var)
  => Map k1 (Term () Void Void en1 fk Void Void Void)
  -> Map k2 (Term () ty1  sym  en1 fk att  Void Void)
  -> Term Void ty2 sym en2 k1 k2 gen sk
  -> Term var ty1 sym en1 fk att gen sk
changeEn fks' atts' t = case t of
  Var v    -> absurd v
  Sym h as -> Sym h $ changeEn fks' atts' <$> as
  Sk k     -> Sk k
  Gen g    -> Gen g
  Fk  h a  -> subst (upp $ fks'  ! h) $ changeEn fks' atts' a
  Att h a  -> subst (upp $ atts' ! h) $ changeEn fks' atts' a

changeEn'
  :: (Ord k, Eq var)
  => Map k (Term () Void Void en1 fk Void Void Void)
  -> t
  -> Term Void ty1 Void en2 k Void gen Void
  -> Term var ty2 sym en1 fk att gen sk
changeEn' fks' atts' t = case t of
  Var v   -> absurd v
  Sym h _ -> absurd h
  Sk k    -> absurd k
  Gen g   -> Gen g
  Fk h a  -> subst (upp $ fks' ! h) $ changeEn' fks' atts' a
  Att h _ -> absurd h

evalSigmaInst
  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, en', fk', att', gen, sk])
  => Mapping var ty sym en fk att en' fk' att'
  -> Instance var ty sym en fk att gen sk x y -> Options
  -> Err (Instance var ty sym en' fk' att' gen sk (Carrier en' fk' gen) (TalgGen en' fk' att' gen sk))
evalSigmaInst f i o = do
  d <- createProver (IP.toCollage s p) o
  return $ initialInstance p (\(EQ (l, r)) -> prove d Map.empty (EQ (l, r))) s
  where
    p = subs f $ pres i
    s = dst  f

mapGen :: (t1 -> t2) -> Term var ty sym en (t2 -> t2) att t1 sk -> t2
mapGen f (Gen g)   = f g
mapGen f (Fk fk a) = fk $ mapGen f a
mapGen _ _         = error "please report, error on mapGen"

evalDeltaAlgebra
  :: forall var ty sym en fk att gen sk x y en' fk' att'
   . (Ord en, Ord fk, Ord att, Ord x)
  => Mapping  var ty sym en  fk  att  en'       fk' att'
  -> Instance var ty sym en' fk' att' gen       sk  x       y
  -> Algebra  var ty sym en  fk  att  (en, x)   y   (en, x) y
evalDeltaAlgebra (Mapping src' _ ens' fks0 atts0)
  (Instance _ _ _ alg@(Algebra _ en' _ _ repr''' ty' _ _ teqs'))
  = Algebra src' en'' nf''x1 nf''x2 Gen ty' nf'''' Sk teqs'
 where
  en'' e = Set.map (\x -> (e,x)) $ en' $ ens' ! e

  nf''x1 g = g
  nf''x2 f a =  (snd $ Schema.fks src' ! f, nf alg $ subst (upp $ fks0 ! f) (repr''' $ snd a))
  nf'''' :: y + ((en,x), att) -> Term Void ty sym Void Void Void Void y
  nf'''' (Left y) = Sk y
  nf'''' (Right ((_, x), att)) = nf'' alg $ subst (upp $ atts0 ! att) (upp $ repr''' x)


evalDeltaInst
  :: forall var ty sym en fk att gen sk x y en' fk' att'
   . (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, x, y])
  => Mapping var ty sym en fk att en' fk' att'
  -> Instance var ty sym en' fk' att' gen sk x y -> Options
  -> Err (Instance var ty sym en fk att (en,x) y (en,x) y)
evalDeltaInst m i _ = pure $ Instance (src m) (algebraToPresentation alg) eq' alg
  where
    alg = evalDeltaAlgebra m i
    eq' (EQ (l, r)) = dp i $ EQ (translateTerm l, translateTerm r)

    translateTerm :: Term Void ty sym en  fk  att (en, x) y -> Term Void ty sym en' fk' att' gen    sk
    translateTerm t = case t of
      Var v      -> absurd v
      Sym s'  as -> Sym s' $ translateTerm <$> as
      Fk  fk  a  -> subst (upp $ Mapping.fks  m ! fk ) $ translateTerm a
      Att att a  -> subst (upp $ Mapping.atts m ! att) $ translateTerm a
      Gen (_, x) -> upp  $ repr  (algebra i) x
      Sk  y      ->        repr' (algebra i) y


-------------------------------------------------------------------------------------------------------------------
-- Printing

-- InstanceEx is an implementation detail, so hide its presence
instance (Show InstanceEx) where
  show (InstanceEx i) = show i

instance (TyMap Show '[var, ty, sym, en, fk, att, gen, sk, x, y], Eq en, Eq fk, Eq att)
  => Show (Instance var ty sym en fk att gen sk x y) where
  show (Instance _ p _ alg) =
    section "instance" $ unlines
      [ section "presentation" $ show p
      , section "algebra"      $ show alg
      ]