@ -4,6 +4,9 @@
{- # LANGUAGE DerivingStrategies # -}
{- # LANGUAGE DeriveAnyClass # -}
{- # LANGUAGE ViewPatterns # -}
{- # LANGUAGE CPP # -}
{- # LANGUAGE ConstraintKinds # -}
{- # LANGUAGE KindSignatures # -}
module Elab.WiredIn where
import Control.Exception
@ -15,10 +18,13 @@ 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 )
@ -71,17 +77,17 @@ 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 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 = 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 -> VInc ( a @@ VI1 ) phi ( comp a phi u x )
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 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
@ -109,6 +115,11 @@ 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 )
@ -130,7 +141,6 @@ 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 )
@ -153,7 +163,7 @@ wiredInNames = Map.fromList
, ( " Glue " , WiGlue )
, ( " glue " , WiGlueElem )
, ( " unglue " , WiUnglue )
, ( " Eq_s " , WiSEq )
, ( " refl_s " , WiSRefl )
, ( " K_s " , WiSK )
@ -221,21 +231,26 @@ ielim line left right fn i =
_ -> error $ " can't ielim " ++ show ( prettyTm ( quote fn ) )
outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
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 ( 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 :: Has CallStack => NFLine -> NFEndp -> Value -> Value -> Value
comp :: Debug CallStack => NFLine -> NFEndp -> Value -> Value -> Value
comp _a VI1 u _a0 = u @@ VI1 @@ VReflStrict VI VI1
comp a psi @ phi u incA0 @ ( c ompO utS ( a @@ VI0 ) phi ( u @@ VI0 ) -> a0 ) =
comp a psi @ phi u incA0 @ ( outS ( a @@ VI0 ) phi ( u @@ VI0 ) -> a0 ) =
case force ( a @@ VVar name ) of
VPi { } ->
let
@ -243,20 +258,21 @@ comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
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
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 ) )
( VInc ( rng VI0 ( ybar VI0 arg ) ) phi ( vApp ( plic VI0 ) a0 ( ybar VI0 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 ) ) ( 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 ) )
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
@ -272,7 +288,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
( 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 ) )
( incS ( a' VI0 @@ VI0 @@ j ) phi ( ielim ( a' VI0 @@ VI0 ) ( u' VI0 ) ( v' VI0 ) a0 j ) )
VGlueTy _ thePhi theTypes theEquivs ->
let
@ -290,8 +306,8 @@ comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
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 )
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
@ -309,7 +325,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
( phi VI1 ` ior ` psi )
( system \ j _u -> mkVSystem ( Map . fromList [ ( phi VI1 , ielim ( base VI1 ) a1' ( vProj1 ( equivs VI1 @@ VReflStrict VI VI1 ) ) alpha j )
, ( psi , a VI1 ( VReflStrict VI VI1 ) ) ] ) )
( VInc ( base VI1 ) ( phi VI1 ` ior ` psi ) a1' )
( incS ( base VI1 ) ( phi VI1 ` ior ` psi ) a1' )
b1 = glueElem ( base VI1 ) ( phi VI1 ) ( types VI1 ) ( equivs VI1 ) ( fun ( const t1 ) ) a1
in b1
@ -321,14 +337,11 @@ comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
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 )
_ -> VComp a phi u ( incS ( 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 ) )
VSystem map -> mkVSystem ( fmap ( \ x -> comp x psi u incA0 ) map )
_ -> VComp a phi u ( VInc ( a @@ VI0 ) phi a0 )
_ -> VComp a phi u ( incS ( a @@ VI0 ) phi a0 )
where
{- # NOINLINE name # -}
name = unsafePerformIO newName
@ -350,12 +363,12 @@ compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value
compHIT name n a phi u a0 =
case force phi of
VI1 -> u @@ VI1 @@ VReflStrict VI VI1
VI0 | n == 0 -> c ompO utS ( a VI0 ) phi u a0
| otherwise -> transHit name a VI0 ( c ompO utS ( a VI0 ) phi u a0 )
VI0 | n == 0 -> outS ( a VI0 ) phi u 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 ( c ompO utS ( a VI1 ) phi ( u @@ VI1 @@ VReflStrict VI VI1 ) 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 ) )
compConArgs :: ( Name -> Int -> Value -> t1 -> t2 -> Value -> Value )
-> Int
@ -396,13 +409,6 @@ nthArg i (force -> VNe hd s) =
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
@ -414,18 +420,18 @@ fill a phi u a0 j =
, ( inot j , outS a phi ( u @@ VI0 ) a0 ) ] ) )
a0
hComp :: NFSort -> NFEndp -> Value -> Value -> Value
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 :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueType :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueType a phi tys eqvs = VGlueTy a phi tys eqvs
glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
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 vl = VGlue a phi tys eqvs t vl
unglue :: Has CallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
unglue :: Debug CallStack => 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 )
@ -462,18 +468,18 @@ equiv a b = GluedVl (HCon VType (Defined (T.pack "Equiv") (-1))) sp $ exists' "f
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 = ( 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
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 ) ) ( VInc ( tyA VI0 ) phi ( f VI0 @@ t0 ) )
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 ) ) ( VInc ( tyA VI0 ) phi a0 )
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 = ( VInc ty phi v , ty , fun \ u -> VPair ( t @@ u ) ( p @@ u ) ) where
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 ) )
@ -483,17 +489,17 @@ 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 ) )
( incS a phi ( vProj1 aC ) )
transp :: ( NFEndp -> Value ) -> Value -> Value
transp line a0 = comp ( fun line ) VI0 ( system \ _ _ -> VSystem mempty ) ( VInc ( line VI0 ) VI0 a0 )
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 ) ) ( VInc ( line VI0 ) VI0 a0 )
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 ( c ompO utS ( line VI0 ) phi u u0 ) )
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 ()
( _ , VNe hd ( length -> nargs ) ) = unPi con_type
@ -538,17 +544,17 @@ makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vP
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 )
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 ) ) ] ) ) ( VInc a ( ior j ( inot j ) ) ( g @@ y ) ) i
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 ) ] ) )
( VInc b ( ior j ( inot j ) ) ( ielim b y ( f @@ x ) beta y ) )
( 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 ) ) ) )
@ -556,7 +562,7 @@ makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vP
, ( 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 ) ) )
( 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 )
@ -571,7 +577,7 @@ idEquiv a = VPair idfun idisequiv where
id_fiber y = VPair y ( VLine a y y ( fun ( const y ) ) )
strictK :: Value -> Value -> Value -> Value -> Value -> Value
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
@ -579,7 +585,7 @@ strictK a x bigp pr (VCase env rng sc cases) = VCase env rng sc (map (projIntoCa
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 :: 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
@ -592,4 +598,4 @@ 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
go _ x = x