amelia
/
cubical


{-# LANGUAGE BlockArguments #-}

{-# LANGUAGE LambdaCase #-}

{-# LANGUAGE OverloadedStrings #-}

{-# LANGUAGE DerivingStrategies #-}

{-# LANGUAGE DeriveAnyClass #-}

{-# LANGUAGE ViewPatterns #-}

{-# LANGUAGE CPP #-}

{-# LANGUAGE ConstraintKinds #-}

{-# LANGUAGE KindSignatures #-}

{-# OPTIONS_GHC -fno-full-laziness #-}

module Elab.WiredIn

 ( wiType

 , wiValue

 , wiredInNames

 , NoSuchPrimitive(..)


 , iand

 , ior

 , inot

 , ielim

 , incS

 , outS

 , comp

 , fill

 , hComp

 , glueType

 , glueElem

 , unglue

 , fun

 , system

 , strictK

 , strictJ

 , projIntoCase

 )

 where


import Control.Exception ( assert, 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 Debug


import Elab.Eval


import GHC.Stack (HasCallStack)


import Presyntax.Presyntax (Plicity(Im, Ex))

import qualified Presyntax.Presyntax as P


import Syntax.Pretty (prettyTm, prettyVl)

import Syntax


import System.IO.Unsafe ( unsafePerformIO )


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 WiPartial = VI ~> VType ~> VTypeω

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

wiType WiPOr = forAll VType \a -> dprod VI \phi -> dprod VI \psi -> VPartial phi a ~> VPartial psi a ~> VPartial (ior phi psi) a


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) ~> VSub (a @@ VI1) phi (u @@ VI1)


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

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

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


wiType WiLineToEquiv = dprod' "P" (VI ~> VType) \a -> equiv (a @@ VI0) (a @@ VI1)


wiValue :: WiredIn -> Value

wiValue WiType = VType

wiValue WiPretype = VTypeω


wiValue WiInterval = VI

wiValue WiI0 = VI0

wiValue WiI1 = VI1


wiValue WiIAnd = functions [(Ex, "i"), (Ex, "j")] \[i, j] -> iand i j

wiValue WiIOr = functions [(Ex, "i"), (Ex, "j")] \[i, j] -> ior i j

wiValue WiINot = fun' "x" inot

wiValue WiPathP = functions [(Ex, "A"), (Ex, "x"), (Ex, "y")] \[a, x, y] -> VPath a x y


wiValue WiPartial = functions [(Ex, "phi"), (Ex, "A")] \[phi, a] -> VPartial phi a

wiValue WiPartialP = functions [(Ex, "phi"), (Ex, "A")] \[phi, a] -> VPartialP phi a

wiValue WiPOr = functions [(Im, "A"), (Ex, "phi"), (Ex, "psi"), (Ex, "a"), (Ex, "b")] \[_, phi, psi, a, b] -> mkVSystem (Map.fromList [(phi, a), (psi, b)])


wiValue WiSub = functions [(Ex, "A"), (Ex, "phi"), (Ex, "u")] \[a, phi, u] -> VSub a phi u

wiValue WiInS = functions [(Im, "A"), (Im, "phi"), (Ex, "u")] \[a, phi, u] -> incS a phi u

wiValue WiOutS = functions [(Im, "A"), (Im, "phi"), (Im, "u"), (Ex, "u0")] \[a, phi, u, x] -> outS a phi u x

wiValue WiComp = fun' "A" \a -> forallI \phi -> fun' "u" \u -> fun' "u0" \x -> incS (a @@ VI1) phi (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


wiValue WiLineToEquiv = fun \l ->

 GluedVl

 (HVar (Defined "lineToEquiv" (-1)))

 (Seq.fromList [(PApp P.Ex l)])

 (makeEquiv' ((l @@) . inot))


(~>) :: 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)


functions :: [(P.Plicity, String)] -> ([Value] -> Value) -> Value

functions args cont = go args [] where

 go [] acc = cont (reverse acc)

 go ((p, x):xs) acc = VLam p $ Closure (Bound (T.pack x) 0) \arg -> go xs (arg:acc)


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)


 , ("Partial", WiPartial)

 , ("PartialP", WiPartialP)

 , ("partialExt", WiPOr)

 , ("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)


 , ("lineToEquiv", WiLineToEquiv)

 ]


newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }

 deriving (Show, Typeable)

 deriving anyclass (Exception)


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 (projIntoCase (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)


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


incS :: DebugCallStack => NFSort -> NFEndp -> Value -> Value

incS _ _ (force -> VNe h (sp Seq.:|> POuc _ _ _))

 = VNe h sp

incS a phi u = VInc a phi u


outS :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value

outS _ (force -> VI1) u _ = u @@ VReflStrict VI VI1


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))


comp :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value

comp _a (force -> VI1) u _a0 = u @@ VI1 @@ VReflStrict VI VI1

comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> 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) (incS (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))

 (incS (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)) (incS (dom VI0) phi (vProj1 a0)) i

 c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (incS (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)]))

 (incS (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 @@ VReflStrict VI VI1

 equivs i = substitute (Map.singleton name i) theEquivs


 a i u = unglue (base i) (phi i) (types i) (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) (incS (base VI0) psi a0)

 t1' = comp (line (const (types VI0))) psi (line (b @@)) (incS (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 @@ VReflStrict VI VI1) (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)))

 (del `ior` psi)

 (system \j _u -> mkVSystem (Map.fromList [ (del, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VReflStrict VI VI1)) alpha j)

 , (psi, a psi _u)

 ]))

 (incS (base VI1) (phi VI1 `ior` psi) a1')

 b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) (incS (base VI1) (ior (del `ior` psi) (inot del `iand` inot psi)) a1)

 in b1


 VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1)

 (fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VReflStrict VI VI1))


 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 (incS (a @@ VI0) phi a0)


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


 _ -> VComp a phi u (incS (a @@ VI0) phi a0)

 where

 {-# NOINLINE name #-}

 name :: Name

 name = unsafePerformIO newName


 {-# NOINLINE equivVar #-}

 equivVar :: Name

 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 @@ VReflStrict VI VI1

 VI0 | n == 0 -> outS (a VI0) phi u a0

 | regular -> a0

 | otherwise -> transHit name a VI0 (outS (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 (outS (a VI0) phi (u @@ VI1 @@ VReflStrict VI VI1) a0))


 regular = a VI0 == a VI1


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))


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 :: DebugCallStack => 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 :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value

hComp _ (force -> VI1) u _ = u @@ VI1 @@ VReflStrict VI VI1

hComp a phi u a0 = VHComp a phi u a0


glueType :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value

glueType a phi tys eqvs = VGlueTy a phi tys eqvs


glueElem :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value

glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VReflStrict VI VI1

glueElem _a _phi _tys _eqvs _t (force -> VInc _ _ (force -> VUnglue _ _ _ _ vl)) = vl

glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl


unglue :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value

unglue _a (force -> VI1) _tys eqvs x = vProj1 (eqvs @@ VReflStrict VI VI1) @@ x

unglue _a _phi _tys _eqvs (force -> VGlue _ _ _ _ t vl) = outS _a _phi (t @@ VReflStrict VI VI1) 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


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)) y (f @@ x)


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 = GluedVl (HCon VType (Defined (T.pack "Equiv") (-1))) sp $ exists' "f" (a ~> b) \f -> isEquiv a b f where

 sp = Seq.fromList [ PApp P.Ex a, PApp P.Ex b ]


pres :: (NFEndp -> NFSort) -> (NFEndp -> NFSort) -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> Value -> (Value, NFSort, Value)

pres tyT tyA f phi t t0 = (incS 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)) (incS (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)) (incS (tyA VI0) phi a0)


opEquiv :: HasCallStack => Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)

opEquiv aT tT f phi t p a = (incS 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))

 (ior phi (inot phi))

 (system \i is1 -> mkVSystem $ Map.fromList [ (phi, ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)

 , (inot phi, vProj1 aC)

 ])

 (incS a phi (vProj1 aC))


transp :: (NFEndp -> Value) -> Value -> Value

transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (incS (line VI0) VI0 a0)


gtrans :: (NFEndp -> Value) -> NFEndp -> Value -> Value

gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (incS (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 (outS (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 ()

 (_, force -> 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

 (_, force -> 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 = makeEquiv' \x -> substitute (Map.singleton var x) vne


makeEquiv' :: (NFEndp -> Value) -> Value

makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)

 where

 line = fun \i -> line' (inot i)

 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) (incS a VI0 x) i

 v i = fun \x -> fill (fun ((line @@) . inot)) VI0 (system \_ _ -> mkVSystem mempty) (incS 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))])) (incS 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)]))

 (incS 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)]))

 (incS 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 :: DebugCallStack => 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 :: DebugCallStack => 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 = error $ show $ prettyTm x