{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ViewPatterns #-}
module Elab.WiredIn where

import Control.Exception

import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq
import qualified Data.Text as T
import Data.Map.Strict (Map)
import Data.Text (Text)
import Data.Typeable

import Elab.Eval

import GHC.Stack (HasCallStack)

import qualified Presyntax.Presyntax as P

import Syntax.Pretty (prettyTm, prettyVl)
import Syntax

import System.IO.Unsafe

wiType :: WiredIn -> NFType
wiType WiType     = VType
wiType WiPretype  = VTypeω

wiType WiInterval = VTypeω
wiType WiI0       = VI
wiType WiI1       = VI

wiType WiIAnd     = VI ~> VI ~> VI
wiType WiIOr      = VI ~> VI ~> VI
wiType WiINot     = VI ~> VI
wiType WiPathP    = dprod (VI ~> VType) \a -> a @@ VI0 ~> a @@ VI1 ~> VType

wiType WiIsOne    = VI ~> VTypeω
wiType WiItIsOne  = VIsOne VI1

wiType WiPartial  = VI ~> VType ~> VTypeω
wiType WiPartialP = dprod VI \x -> VPartial x VType ~> VTypeω

wiType WiSub      = dprod VType \a -> dprod VI \phi -> VPartial phi a ~> VTypeω
wiType WiInS      = forAll VType \a -> forAll VI \phi -> dprod a \u -> VSub a phi (fun (const u))
wiType WiOutS     = forAll VType \a -> forAll VI \phi -> forAll (VPartial phi a) \u -> VSub a phi u ~> a

wiType WiComp     = dprod' "A" (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> a @@ VI1
-- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
wiType WiGlue     = dprod' "A" VType \a -> forAll' "phi" VI \phi -> dprod' "T" (VPartial phi VType) \t -> VPartialP phi (fun \o -> equiv (t @@ o) a) ~> VType
-- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
wiType WiGlueElem = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \eqv ->
  dprod' "t" (VPartialP phi ty) \t -> VSub a phi (fun \o -> vProj1 (eqv @@ o) @@ (t @@ o)) ~> VGlueTy a phi ty eqv
-- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
wiType WiUnglue = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \e -> VGlueTy a phi ty e ~> a

wiType WiSEq   = forAll' "A" VTypeω \a -> a ~> a ~> VTypeω
wiType WiSRefl = forAll' "A" VTypeω \a -> forAll' "x" a \x -> VEqStrict a x x
wiType WiSK    = forAll' "A" VTypeω \a -> forAll' "x" a \x -> dprod' "P" (VEqStrict a x x ~> VTypeω) \bigp -> (bigp @@ VReflStrict a x) ~> dprod' "p" (VEqStrict a x x) \p -> bigp @@ p
wiType WiSJ    = forAll' "A" VTypeω \a -> forAll' "x" a \x -> dprod' "P" (dprod' "y" a \y -> VEqStrict a x y ~> VTypeω) \bigp -> bigp @@ x @@ VReflStrict a x ~> forAll' "y" a \y -> dprod' "p" (VEqStrict a x y) \p -> bigp @@ y @@ p

wiValue :: WiredIn -> Value
wiValue WiType     = VType
wiValue WiPretype  = VTypeω

wiValue WiInterval = VI
wiValue WiI0       = VI0
wiValue WiI1       = VI1

wiValue WiIAnd      = fun \x -> fun \y -> iand x y
wiValue WiIOr       = fun \x -> fun \y -> ior x y
wiValue WiINot      = fun inot
wiValue WiPathP     = fun \a -> fun \x -> fun \y -> VPath a x y

wiValue WiIsOne   = fun VIsOne
wiValue WiItIsOne = VItIsOne

wiValue WiPartial  = fun \phi -> fun \r -> VPartial phi r
wiValue WiPartialP = fun \phi -> fun \r -> VPartialP phi r
wiValue WiSub      = fun \a -> fun \phi -> fun \u -> VSub a phi u
wiValue WiInS      = forallI \a -> forallI \phi -> fun \u -> VInc a phi u
wiValue WiOutS     = forallI \a -> forallI \phi -> forallI \u -> fun \x -> outS a phi u x
wiValue WiComp     = fun \a -> forallI \phi -> fun \u -> fun \x -> comp a phi u x

wiValue WiGlue     = fun \a -> forallI \phi -> fun \t -> fun \e -> glueType a phi t e
wiValue WiGlueElem = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> fun \y -> glueElem a phi ty eqv x y
wiValue WiUnglue   = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> unglue a phi ty eqv x

wiValue WiSEq   = forallI \a -> fun \x -> fun \y -> VEqStrict a x y
wiValue WiSRefl = forallI \a -> forallI \x -> VReflStrict a x
wiValue WiSK    = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> fun \p -> strictK a x bigp pr p
wiValue WiSJ    = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> forallI \y -> fun \p -> strictJ a x bigp pr y p

(~>) :: Value -> Value -> Value
a ~> b = VPi P.Ex a (Closure (Bound "_" 0) (const b))
infixr 7 ~>

fun, line :: (Value -> Value) -> Value
fun k = VLam P.Ex $ Closure (Bound "x" 0) (k . force)
line k = VLam P.Ex $ Closure (Bound "i" 0) (k . force)

fun' :: String -> (Value -> Value) -> Value
fun' x k = VLam P.Ex $ Closure (Bound (T.pack x) 0) (k . force)

forallI :: (Value -> Value) -> Value
forallI k = VLam P.Im $ Closure (Bound "x" 0) (k . force)

dprod' :: String -> Value -> (Value -> Value) -> Value
dprod' t a b = VPi P.Ex a (Closure (Bound (T.pack t) 0) b)

dprod :: Value -> (Value -> Value) -> Value
dprod = dprod' "x"

exists' :: String -> Value -> (Value -> Value) -> Value
exists' s a b = VSigma a (Closure (Bound (T.pack s) 0) b)

exists :: Value -> (Value -> Value) -> Value
exists = exists' "x"

forAll' :: String -> Value -> (Value -> Value) -> Value
forAll' n a b = VPi P.Im a (Closure (Bound (T.pack n) 0) b)

forAll :: Value -> (Value -> Value) -> Value
forAll = forAll' "x"


wiredInNames :: Map Text WiredIn
wiredInNames = Map.fromList
  [ ("Pretype", WiPretype)
  , ("Type", WiType)
  , ("Interval", WiInterval)
  , ("i0", WiI0)
  , ("i1", WiI1)
  , ("iand", WiIAnd)
  , ("ior",  WiIOr)
  , ("inot", WiINot)
  , ("PathP", WiPathP)

  , ("IsOne", WiIsOne)
  , ("itIs1", WiItIsOne)

  , ("Partial", WiPartial)
  , ("PartialP", WiPartialP)
  , ("Sub", WiSub)
  , ("inS", WiInS)
  , ("outS", WiOutS)

  , ("comp", WiComp)
  , ("Glue", WiGlue)
  , ("glue", WiGlueElem)
  , ("unglue", WiUnglue)
  
  , ("Eq_s", WiSEq)
  , ("refl_s", WiSRefl)
  , ("K_s", WiSK)
  , ("J_s", WiSJ)
  ]

newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
  deriving (Show, Typeable)
  deriving anyclass (Exception)

-- Interval operations

iand, ior :: Value -> Value -> Value
iand x = case force x of
  VI1 -> id
  VI0 -> const VI0
  VIAnd x y -> \z -> case force z of
    VI0 -> VI0
    VI1 -> VI1
    z -> iand x (iand y z)
  x -> \y -> case force y of
    VI0 -> VI0
    VI1 -> x
    y -> VIAnd x y

ior x = case force x of
  VI0 -> id
  VI1 -> const VI1
  VIOr x y -> \z -> case force z of
    VI1 -> VI1
    VI0 -> VIOr x y
    _ -> ior x (ior y z)
  x -> \y -> case force y of
    VI1 -> VI1
    VI0 -> x
    y -> VIOr x y

inot :: Value -> Value
inot x = case force x of
  VI0 -> VI1
  VI1 -> VI0
  VIOr x y -> VIAnd (inot x) (inot y)
  VIAnd x y -> VIOr (inot x) (inot y)
  VINot x -> x
  x -> VINot x

ielim :: Value -> Value -> Value -> Value -> NFEndp -> Value
ielim line left right (GluedVl h sp vl) i =
  GluedVl h (sp Seq.:|> PIElim line left right i) (ielim line left right vl i)
ielim line left right fn i =
  case force fn of
    VLine _ _ _ fun -> fun @@ i
    VLam _ (Closure _ k) -> k i
    x -> case force i of
      VI1 -> right
      VI0 -> left
      _ -> case x of
        VNe n sp -> VNe n (sp Seq.:|> PIElim line left right i)
        VSystem map -> VSystem (fmap (flip (ielim line left right) i) map)
        VInc (VPath _ _ _) _ u -> ielim line left right u i

        VCase env r x xs -> VCase env r x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)

        _ -> error $ "can't ielim " ++ show (prettyTm (quote fn))

outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
outS _ (force -> VI1) u _  = u @@ VItIsOne

outS _ _phi _ (VInc _ _ x) = x
outS _ VI0 _  x            = x

outS a phi u  (GluedVl x sp vl) = GluedVl x (sp Seq.:|> POuc a phi u) (outS a phi u vl)
outS a phi u  (VNe x sp) = VNe x (sp Seq.:|> POuc a phi u)
outS a phi u (VSystem fs) = mkVSystem (fmap (outS a phi u) fs)
outS _ _ _ v             = error $ "can't outS " ++ show (prettyTm (quote v))

-- Composition
comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
comp _a VI1 u _a0 =  u @@ VI1 @@ VItIsOne
comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
  case force (a @@ VVar name) of
    VPi{} ->
      let
        plic i = let VPi p _ _ = force (a @@ i)              in p
        dom  i = let VPi _ d _ = force (a @@ i)              in d
        rng  i = let VPi _ _ (Closure _ r) =  force (a @@ i) in r

        y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (dom VI0) phi y) i
        ybar i y = y' (inot i) y
       in VLam (plic VI1) . Closure (Bound "x" 0) $ \arg ->
              comp (line \i -> rng i (ybar i arg))
                   phi
                   (system \i isone -> vApp (plic i) (u @@ i @@ isone) (ybar i arg))
                   (VInc (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg)))
    VSigma{} ->
      let
        dom i = let VSigma d _             = force (a @@ i) in d
        rng i = let VSigma _ (Closure _ r) = force (a @@ i) in r

        w i = fill (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) i
        c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (VInc (rng VI0 (w VI0)) phi (vProj2 a0))
       in
         VPair (w VI1) c2

    VPath{} ->
      let
        a' i = let VPath thea _ _ = force (a @@ i) in thea
        u' i = let VPath _ theu _ = force (a @@ i) in theu
        v' i = let VPath _ _ thev = force (a @@ i) in thev
      in
        VLine (a' VI1 @@ VI1) (u' VI1) (v' VI1) $ fun \j ->
          comp (fun \x -> a' x @@ x)
            (phi `ior` j `ior` inot j)
            (system \i isone -> mkVSystem (Map.fromList [ (phi, ielim (a' VI0) (u' VI0) (v' VI0) (u @@ i @@ isone) j)
                                                        , (j, v' i)
                                                        , (inot j, u' i)]))
            (VInc (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))

    VGlueTy _ thePhi theTypes theEquivs ->
      let
        b = u
        b0 = a0
        fam = a
      in
      let
        base i   = let VGlueTy b _ _ _ = forceAndGlue (fam @@ i) in b
        phi i    = substitute (Map.singleton name i) thePhi
        types i  = substitute (Map.singleton name i) theTypes @@ VItIsOne
        equivs i = substitute (Map.singleton name i) theEquivs

        a i u = unglue (base i) (phi i) (types i @@ u) (equivs i) (b @@ i @@ u)
        a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0

        del = faceForall phi
        a1' = comp (line base)  psi (system a) (VInc (base VI0) psi a0)
        t1' = comp (line (const (types VI0))) psi (line (b @@)) (VInc (base VI0) psi b0)

        (omega_st, omega_t, omega_rep) = pres types base equivs psi (b @@) b0
        omega = outS omega_t psi omega_rep omega_st

        (t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1) (equivs VI1 @@ VItIsOne) (del `ior` psi) (fun ts) (fun ps) a1'
        t1alpha = outS t1a_t (del `ior` psi) t1a_rep t1alpha_st

        (t1, alpha) = (vProj1 t1alpha, vProj2 t1alpha)

        ts isone = mkVSystem . Map.fromList $ [(del, t1'), (psi, (b @@ VI1 @@ isone))]
        ps _isone = mkVSystem . Map.fromList $ [(del, omega), (psi, VLine (line (const (base VI1))) a1' a1' (fun (const a1')))]

        a1 = comp
          (fun (const (base VI1)))
          (phi VI1 `ior` psi)
          (system \j _u -> mkVSystem (Map.fromList [ (phi VI1, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VItIsOne)) alpha j)
                                                   , (psi, a VI1 VItIsOne)]))
          (VInc (base VI1) (phi VI1 `ior` psi) a1')
        b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1
       in b1

    VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1)
                            (fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VItIsOne))

    VNe (HData False _) Seq.Empty -> a0
    VNe (HData False _) args ->
      case force a0 of
        VNe (HCon con_type con_name) con_args ->
          VNe (HCon con_type con_name) $ compConArgs makeSetFiller (length args) (a @@) con_type con_args phi u
        _ -> VComp a phi u (VInc (a @@ VI0) phi a0)

    VNe (HData True name) args -> compHIT name (length args) (a @@) phi u incA0

    VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a))
    sys@VSystem{} -> error $ "comp VSystem: " ++ show (prettyTm (quote sys))

    _ -> VComp a phi u (VInc (a @@ VI0) phi a0)
  where
    {-# NOINLINE name #-}
    name = unsafePerformIO newName

    {-# NOINLINE equivVar #-}
    equivVar = unsafePerformIO newName

mapVSystem :: (Value -> Value) -> Value -> Value
mapVSystem f (VSystem fs) = VSystem (fmap f fs)
mapVSystem f x = f x

forceAndGlue :: Value -> Value
forceAndGlue v =
  case force v of
    v@VGlueTy{} -> v
    y -> VGlueTy y VI1 (fun (const y)) (fun (const (idEquiv y)))

compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
compHIT name n a phi u a0 =
  case force phi of
    VI1 -> u @@ VI1 @@ VItIsOne
    VI0 | n == 0 -> compOutS (a VI0) phi u a0
        | otherwise -> transHit name a VI0 (compOutS (a VI0) phi u a0)
    x -> go n a x u a0
  where
    go 0 a phi u a0 = VHComp (a VI0) phi u a0
    go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> transSqueeze name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (compOutS (a VI1) phi (u @@ VI1 @@ VItIsOne) a0))

compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value)
            -> Int
            -> (Value -> Value)
            -> Value
            -> Seq.Seq Projection
            -> t1 -> t2
            -> Seq.Seq Projection
compConArgs makeFiller total_args fam = go total_args where
  go _ _ Seq.Empty _ _ = Seq.Empty
  go nargs (VPi p dom (Closure _ rng)) (PApp p' y Seq.:<| xs) phi u
    | nargs > 0 = assert (p == p') $
        PApp p' (nthArg (total_args - nargs) (fam VI1)) Seq.:<| go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u
    | otherwise = assert (p == p') $
      let fill = makeFiller typeArgument nargs dom phi u y
       in PApp p' (fill @@ VI1) Seq.:<| go (nargs - 1) (rng fill) xs phi u
  go _ _ _ _ _ = error $ "invalid constructor"

  smuggle x = VNe (HData False typeArgument) (Seq.singleton (PApp P.Ex x))

  typeArgument = unsafePerformIO newName
  {-# NOINLINE typeArgument #-}

makeSetFiller :: Name -> Int -> Value -> NFEndp -> Value -> Value -> Value
makeSetFiller typeArgument nth (VNe (HData _ n') args) phi u a0
  | n' == typeArgument =
    fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0
  where
    makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
    makeDomain _ = error "somebody smuggled something that smells"
makeSetFiller _ _ _ _ _ a0 = fun (const a0)

nthArg :: Int -> Value -> Value
nthArg i (force -> VNe hd s) =
  case s Seq.!? i of
    Just (PApp _ t) -> t
    _ -> error $ "invalid " ++ show i ++ "th argument to data type " ++ show hd
nthArg i (force -> VSystem vs) = VSystem (fmap (nthArg i) vs)
nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs))

compOutS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
compOutS a b c d = compOutS a b c (force d) where
  compOutS _ _hi _0 vl@VComp{}   = error $ "unwrapped composition given as input to composition operation is fuckign illegal " ++ show (prettyTm (quote (zonk vl)))
  compOutS _ _hi _0 vl@VHComp{}  = error $ "unwrapped composition (gay) given as input to composition operation is fuckign illegal " ++ show (prettyTm (quote (zonk vl)))
  compOutS _ _hi _0 (VInc _ _ x) = x
  compOutS a phi a0 v = outS a phi a0 v

system :: (Value -> Value -> Value) -> Value
system k = VLam P.Ex $ Closure (Bound "i" 0) \i -> VLam P.Ex $ Closure (Bound "[i]" 0) \isone -> k i isone

fill :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
fill a phi u a0 j =
  comp (line \i -> a @@ (i `iand` j))
       (phi `ior` inot j)
       (system \i isone -> mkVSystem (Map.fromList [ (phi, u @@ (i `iand` j) @@ isone)
                                                   , (inot j, outS a phi (u @@ VI0) a0)]))
       a0

hComp :: NFSort -> NFEndp -> Value -> Value -> Value
hComp _ (force -> VI1) u _ = u @@ VI1 @@ VItIsOne
hComp a phi u a0 = VHComp a phi u a0

glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueType a phi tys eqvs = VGlueTy a phi tys eqvs

glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VItIsOne
glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl

unglue   :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
unglue _a (force -> VI1) _tys eqvs x = vProj1 (eqvs @@ VItIsOne) @@ x
unglue _a _phi _tys _eqvs (force -> VGlue _ _ _ _ _ vl) = vl
unglue a phi tys eqvs (force -> VSystem fs) = VSystem (fmap (unglue a phi tys eqvs) fs)
unglue a phi tys eqvs vl = VUnglue a phi tys eqvs vl
-- Definition of equivalences

faceForall :: (NFEndp -> NFEndp) -> Value
faceForall phi = T.length (getNameText name) `seq` go (phi (VVar name)) where
  {-# NOINLINE name #-}
  name = unsafePerformIO newName

  go x@(VVar n)
    | n == name = VI0
    | otherwise = x
  go x@(VINot (VVar n))
    | n == name = VI0
    | otherwise = x
  go (VIAnd x y) = iand (go x) (go y)
  go (VIOr x y) = ior (go x) (go y)
  go (VINot x) = inot (go x)
  go vl = vl

isContr :: Value -> Value
isContr a = exists' "x" a \x -> dprod' "y" a \y -> VPath (line (const a)) x y

fiber :: NFSort -> NFSort -> Value -> Value -> Value
fiber a b f y = exists' "x" a \x -> VPath (line (const b)) (f @@ x) y

isEquiv :: NFSort -> NFSort -> Value -> Value
isEquiv a b f = dprod' "y" b \y -> isContr (fiber a b f y)

equiv :: NFSort -> NFSort -> Value
equiv a b = exists' "f" (a ~> b) \f -> isEquiv a b f

pres :: (NFEndp -> NFSort) -> (NFEndp -> NFSort) -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> Value -> (Value, NFSort, Value)
pres tyT tyA f phi t t0 = (VInc pathT phi (VLine (tyA VI1) c1 c2 (line path)), pathT, fun $ \u -> VLine (fun (const (tyA VI1))) c1 c2 (fun (const (f VI1 @@ (t VI1 @@ u))))) where
  pathT = VPath (fun (const (tyA VI1))) c1 c2
  c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (VInc (tyA VI0) phi (f VI0 @@ t0))
  c2 = f VI1 @@ comp (line tyT) phi (system \i u -> t i @@ u) t0

  a0 = f VI0 @@ t0
  v = fill (fun tyT) phi (system \i u -> t i @@ u) t0

  path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) a0

opEquiv :: HasCallStack => Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)
opEquiv aT tT f phi t p a = (VInc ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
  fn = vProj1 f
  ty  = exists' "f" tT \x -> VPath (line (const aT)) a (fn @@ x)
  v   = contr ty (vProj2 f @@ a) phi (\u -> VPair (t @@ u) (p @@ u))

contr :: HasCallStack => Value -> Value -> NFEndp -> (Value -> Value) -> Value
contr a aC phi u =
  comp (line (const a))
    phi
    (system \i is1 -> ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
    (VInc a phi (vProj1 aC))

transp :: (NFEndp -> Value) -> Value -> Value
transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0)

gtrans :: (NFEndp -> Value) -> NFEndp -> Value -> Value
gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (VInc (line VI0) VI0 a0)

transHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> Value
transHit name line phi x = transHit name line phi (force x) where
  transHit name line phi (VHComp _ psi u u0) = VHComp (line VI1) psi (system \i j -> transHit name line phi (u @@ i @@ j)) (transHit name line phi (compOutS (line VI0) phi u u0))
  transHit name line phi (VNe (HCon con_type con_name) spine) | ourType = x' where
    x' = VNe (HCon con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
    (_, VNe hd (length -> nargs)) = unPi con_type
    ourType = case hd of
      HData True n' -> n' == name
      _ -> False

  transHit name line phi (VNe (HPCon sys con_type con_name) spine) | ourType = x' where
    x' = VNe (HPCon (mapVSystem rec sys) con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
    rec = transHit name line phi
    (_, VNe hd (length -> nargs)) = unPi con_type
    ourType = case hd of
      HData True n' -> n' == name
      _ -> False

  transHit name line phi (VSystem xs) = mkVSystem (fmap (transHit name line phi) xs)
  transHit _ line phi a0 = gtrans line phi a0

transFill :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> NFEndp -> Value
transFill name a phi a0 i = transHit name (\j -> a (iand i j)) (phi `ior` inot i) a0 where

transSqueeze :: Name -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> NFEndp -> Value
transSqueeze name a phi x i = transHit name (\j -> a (ior i j)) (phi `ior` i) (x i)

makeTransFiller :: Name -> Name -> p -> Value -> NFEndp -> () -> Value -> Value
makeTransFiller thedata typeArgument _ (VNe (HData _ n') args) phi () a0
  | n' == typeArgument = fun (transFill thedata (makeDomain args) phi a0)
  where
    makeDomain (PApp _ x Seq.:<| xs) = \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
    makeDomain _ = error "somebody smuggled something that smells"
makeTransFiller _ _ _ _ _ _ a0 = fun (const a0)

makeEquiv :: Name -> Value -> Value
makeEquiv var vne = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
  where
    line = fun \i -> substitute (Map.singleton var (inot i)) vne
    a = line @@ VI0
    b = line @@ VI1

    f = fun \x -> transp (line @@) x
    g = fun \x -> transp ((line @@) . inot) x
    u i = fun \x -> fill line VI0 (system \_ _ -> mkVSystem mempty) (VInc a VI0 x) i
    v i = fun \x -> fill (fun ((line @@) . inot)) VI0 (system \_ _ -> mkVSystem mempty) (VInc a VI1 x) (inot i)

    fib y = VPair (g @@ y) (VLine b y (f @@ (g @@ y)) (fun (theta0 y VI1)))
    theta0 y i j = fill line (ior j (inot j)) (system \i _ -> mkVSystem (Map.fromList [(j, v i @@ y), (inot j, u i @@ (g @@ y))])) (VInc a (ior j (inot j)) (g @@ y)) i
    theta1 x beta y i j =
      fill (fun ((line @@) . inot))
           (ior j (inot j))
           (system \i _ -> mkVSystem (Map.fromList [ (inot j, v (inot i) @@ y)
                                                   , (j, u (inot i) @@ x)]))
           (VInc b (ior j (inot j)) (ielim b y (f @@ x) beta y))
           (inot i)
    omega x beta y = theta1 x beta y VI0
    delta x beta y j k = comp line (ior k (ior (inot k) (ior j (inot j))))
                                   (system \i _ -> mkVSystem (Map.fromList [ (inot k, theta0 y i j)
                                                                           , (k, theta1 x beta y i j)
                                                                           , (inot j, v i @@ y)
                                                                           , (j, u i @@ omega x beta y k)]))
                                   (VInc a (ior k (ior (inot k) (ior j (inot j)))) (omega x beta y (iand j k)))
    p x beta y = VLine (exists a \x -> VPath b y (f @@ x)) (fib y) (VPair x beta) $ fun \k ->
      VPair (omega x beta y k) (VLine (VPath b y (f @@ x)) (vProj2 (fib y)) beta $ fun \j -> delta x beta y j k)

idEquiv :: NFSort -> Value
idEquiv a = VPair idfun idisequiv where
  idfun = fun id
  u_ty = exists' "y" a \x -> VPath (fun (const a)) x x
  idisequiv = fun \y -> VPair (id_fiber y) $ fun \u ->
    VLine u_ty (id_fiber y) u $ fun \i -> VPair (ielim (fun (const a)) y y (vProj2 u) i) $
      VLine (fun (const a)) y (vProj1 u) $ fun \j ->
        ielim (fun (const a)) y y (vProj2 u) (iand i j)

  id_fiber y = VPair y (VLine a y y (fun (const y)))

strictK :: Value -> Value -> Value -> Value -> Value -> Value
strictK _ _ _ pr (VReflStrict _ _) = pr
strictK a x bigp pr (VNe h sp) = VNe h (sp Seq.:|> PK a x bigp pr)
strictK a x bigp pr (VCase env rng sc cases) = VCase env rng sc (map (projIntoCase func) cases) where
  func = AxK (quote a) (quote x) (quote bigp) (quote pr)
strictK a x bigp pr (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PK a x bigp pr) (strictK a x bigp pr vl)
strictK _ _ _ _r eq = error $ "can't K " ++ show (prettyVl eq)

strictJ :: Value -> Value -> Value -> Value -> Value -> Value -> Value
strictJ _a _x _bigp pr _ (VReflStrict _ _) = pr
strictJ a x bigp pr y (VNe h sp) = VNe h (sp Seq.:|> PJ a x bigp pr y)
strictJ a x bigp pr y (VCase env rng sc cases) = VCase env rng sc (map (projIntoCase func) cases) where
  func = AxJ (quote a) (quote x) (quote bigp) (quote pr) (quote y)
strictJ a x bigp pr y (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PJ a x bigp pr y) (strictJ a x bigp pr y vl)
strictJ _ _ _ _r _ eq = error $ "can't J " ++ show eq

projIntoCase :: (Term -> Term) -> (Term, Int, Term) -> (Term, Int, Term)
projIntoCase fun (pat, nLams, term) = (pat, nLams, go nLams term) where
  go 0 x = fun x
  go n (Lam p x r) = Lam p x (go (n - 1) r)
  go n (PathIntro l a b r) = PathIntro l a b (go (n - 1) r)
  go _ x = x