From fb87b16429fdd54f7e71b653ffaed115015066cc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Sat, 6 Mar 2021 23:36:47 -0300 Subject: [PATCH] some initial work on HITs --- intro.tt | 152 ++++++++++++++++++++++++++++++++++- src/Elab.hs | 158 ++++++++++++++++++++++++++++++------- src/Elab/Eval.hs | 56 ++++++++++--- src/Elab/Monad.hs | 7 +- src/Elab/WiredIn.hs | 68 +++++++++++----- src/Elab/WiredIn.hs-boot | 10 ++- src/Main.hs | 2 +- src/Presyntax/Parser.y | 17 +++- src/Presyntax/Presyntax.hs | 7 +- src/Syntax.hs | 68 ++++++++-------- src/Syntax/Pretty.hs | 21 +++-- 11 files changed, 458 insertions(+), 108 deletions(-) diff --git a/intro.tt b/intro.tt index 8b09eb6..69a934f 100644 --- a/intro.tt +++ b/intro.tt @@ -682,14 +682,35 @@ pathIsHom {A} {B} {f} {g} = theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g}) in univalence (IsoToEquiv theIso) +-- Inductive types +------------------- +-- +-- An inductive type is a type freely generated by a finite set of +-- constructors. For instance, the type of natural numbers is generated +-- by the constructors for "zero" and "successor". + data Nat : Type where zero : Nat succ : Nat -> Nat +-- Pattern matching allows us to prove that these initial types are +-- initial algebras for their corresponding functors. + +Nat_elim : (P : Nat -> Type) -> P zero -> ((x : Nat) -> P x -> P (succ x)) -> (x : Nat) -> P x +Nat_elim P pz ps = \case + zero -> pz + succ x -> ps x (Nat_elim P pz ps x) + +-- The type of integers can be defined as A + B, where "pos n" means +n +-- and "neg n" means -(n + 1). + data Int : Type where pos : Nat -> Int neg : Nat -> Int +-- On this representation we can define the successor and predecessor +-- functions by (nested) induction. + sucZ : Int -> Int sucZ = \case pos n -> pos (succ n) @@ -710,6 +731,9 @@ predZ = \case in pred_pos n neg n -> neg (succ n) +-- And prove that the successor function is an isomorphism, and thus, an +-- equivalence. + sucEquiv : isIso sucZ sucEquiv = let @@ -733,5 +757,131 @@ sucEquiv = in k n in (predZ, sucPredZ, predSucZ) +-- Univalence gives us a path between integers such that transp intPath +-- x = suc x, transp (sym intPath) x = pred x + intPath : Path Int Int -intPath = univalence (IsoToEquiv (sucZ, sucEquiv)) \ No newline at end of file +intPath = univalence (IsoToEquiv (sucZ, sucEquiv)) + +-- Higher inductive types +------------------------- +-- +-- While inductive types let us generate discrete spaces like the +-- naturals or integers, they do not support defining higher-dimensional +-- structures given by spaces with points and paths. + +-- A very simple higher inductive type is the interval, given by + +data Interval : Type where + ii0 : Interval + ii1 : Interval + seg i : Interval [ (i = i0) -> ii0, (i = i1) -> ii1 ] + +-- This expresses that we have two points ii0 and ii1 and a path (\i -> +-- seg i) with endpoints ii0 and ii1. + +-- With this type we can reproduce the proof of Lemma 6.3.2 from the +-- HoTT book: + +iFunext : {A : Type} {B : A -> Type} (f : (x : A) -> B x) (g : (x : A) -> B x) -> ((x : A) -> Path (f x) (g x)) -> Path f g +iFunext f g p i = h' (seg i) where + h : (x : A) -> Interval -> B x + h x = \case + ii0 -> f x + ii1 -> g x + seg i -> p x i + + h' : Interval -> (x : A) -> B x + h' i x = h x i + +-- Of course, Cubical Type Theory also has an interval (pre)type, but +-- that, unlike the Interval here, is not Kan: it has no composition +-- structure. + +-- Another simple higher-inductive type is the circle, with a point and +-- a non-trivial loop, (\i -> loop i). + +data S1 : Type where + base : S1 + loop i : S1 [ (i = i1) -> base, (i = i0) -> base ] + +-- By writing a function from the circle to the universe of types Type, +-- we can calculate winding numbers along the circle. + +helix : S1 -> Type +helix = \case + base -> Int + loop i -> intPath i + +winding : Path base base -> Int +winding p = transp (\i -> helix (p i)) (pos zero) + +-- For instance, going around the loop once has a winding number of +1, + +windingLoop : Path (winding (\i -> loop i)) (pos (succ zero)) +windingLoop = refl + +-- Going backwards has a winding number of -1 (remember the +-- representation of integers), + +windingSymLoop : Path (winding (\i -> loop (inot i))) (neg zero) +windingSymLoop = refl + +-- And going around the trivial loop (\i -> base) goes around the the +-- non-trivial loop (\i -> loop) zero times. + +windingBase : Path (winding (\i -> base)) (pos zero) +windingBase = refl + +-- One particularly general higher inductive type is the homotopy pushout, +-- which can be seen as a kind of sum B + C with the extra condition that +-- whenever x and y are in the image of f (resp. g), inl x ≡ inr y. + +data Pushout {A : Type} {B : Type} {C : Type} (f : A -> B) (g : A -> C) : Type where + inl : (x : B) -> Pushout f g + inr : (y : C) -> Pushout f g + push i : (a : A) -> Pushout f g [ (i = i0) -> inl (f a), (i = i1) -> inr (g a) ] + +-- The name is due to the category-theoretical notion of pushout. +-- TODO: finish writing this tomorrow lol + +data Susp (A : Type) : Type where + north : Susp A + south : Susp A + merid i : A -> Susp A [ (i = i0) -> north, (i = i1) -> south ] + +data Unit : Type where + tt : Unit + +poSusp : Type -> Type +poSusp A = Pushout {A} {Unit} {Unit} (\x -> tt) (\x -> tt) + +poSusp_to_Susp : {A : Type} -> poSusp A -> Susp A +poSusp_to_Susp = \case + inl x -> north + inr x -> south + push x i -> merid x i + +Susp_to_poSusp : {A : Type} -> Susp A -> poSusp A +Susp_to_poSusp = \case + north -> inl tt + south -> inr tt + merid x i -> push x i + +Susp_to_poSusp_to_Susp : {A : Type} -> (x : Susp A) -> Path (poSusp_to_Susp (Susp_to_poSusp x)) x +Susp_to_poSusp_to_Susp = \case + north -> refl + south -> refl + merid x i -> refl + +unitEta : (x : Unit) -> Path x tt +unitEta = \case tt -> refl + +poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x +poSusp_to_Susp_to_poSusp {A} = \case + inl x -> cong inl (sym (unitEta x)) + inr x -> cong inr (sym (unitEta x)) + push x i -> refl + +Susp_is_poSusp : {A : Type} -> Path (Susp A) (poSusp A) +Susp_is_poSusp {A} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A})) \ No newline at end of file diff --git a/src/Elab.hs b/src/Elab.hs index 57c501a..a1408b7 100644 --- a/src/Elab.hs +++ b/src/Elab.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE DeriveAnyClass #-} @@ -30,6 +31,7 @@ import Prettyprinter import Syntax.Pretty import Syntax +import Debug.Trace infer :: P.Expr -> ElabM (Term, NFType) infer (P.Span ex a b) = withSpan a b $ infer ex @@ -194,52 +196,108 @@ check (P.LamSystem bs) ty = do mkB _ (Nothing, b) = b pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, mkB name y)) eqns)))) -check (P.LamCase pats) ty = do - porp <- isPiType P.Ex ty - case porp of - It'sProd dom rng wp -> do - name <- newName - cases <- for pats $ \(pat, rhs) -> do - checkPattern pat dom \pat wp pat_nf -> do - rhs <- check rhs (rng pat_nf) - pure (pat, wp rhs) - let x = wp (Lam P.Ex name (Case (Ref name) cases)) - pure x - _ -> do - dom <- newMeta VTypeω - n <- newName' (Bound (T.singleton 'x') 0) - assume n dom \_ -> do - rng <- newMeta VTypeω - throwElab $ NotEqual (VPi P.Ex dom (Closure n (const rng))) ty +check (P.LamCase pats) ty = + do + porp <- isPiType P.Ex ty + case porp of + It'sProd dom rng wp -> do + name <- newName + let range = Lam P.Ex name (quote (rng (VVar name))) + + cases <- checkPatterns range [] pats \partialPats (pat, rhs) -> do + checkPattern pat dom \pat wp boundary pat_nf -> do + rhs <- check rhs (rng pat_nf) + case boundary of + -- If we're checking a higher constructor then we need to + -- compute what the case expression computed so far does + -- with all the faces + + -- and make sure that the current case agrees with that + -- boundary + Just boundary -> do + rhs_nf <- eval (wp rhs) + cases <- partialPats + + let + (ty, a, b) = case pat_nf of + VNe (HCon ty (ConName _ _ a b)) _ -> (ty, a, b) + VNe (HPCon _ ty (ConName _ _ a b)) _ -> (ty, a, b) + _ -> undefined + dummies <- replicateM ((a + b) - length (getBoundaryNames boundary)) newName + let + base = appDummies (VVar <$> dummies) ty rhs_nf + sys = boundaryFormulas (drop a dummies ++ getBoundaryNames boundary) (getBoundaryMap boundary) + + for_ (Map.toList sys) \(formula, side) -> do + let rhs = cases @@ side + for_ (truthAssignments formula mempty) $ \i -> do + let vl = foldl (\v n -> vApp P.Ex v (snd (i Map.! n))) base (getBoundaryNames boundary) + unify vl rhs + `withNote` vcat [ pretty "These must be the same because of the face" + , indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm (quote (zonk side)) + ] + `withNote` (pretty "Mandated by the constructor" <+> prettyTm (quote pat_nf)) + _ -> pure () + + pure (pat, wp rhs) + let x = wp (Lam P.Ex name (Case range (Ref name) cases)) + pure x + _ -> do + dom <- newMeta VTypeω + n <- newName' (Bound (T.singleton 'x') 0) + assume n dom \_ -> do + rng <- newMeta VTypeω + throwElab $ NotEqual (VPi P.Ex dom (Closure n (const rng))) ty + where + checkPatterns _ acc [] _ = pure (reverse acc) + checkPatterns rng acc (x:xs) k = do + n <- newName + (p, t) <- k (eval (Lam P.Ex n (Case rng (Ref n) acc))) x + checkPatterns rng ((p, t):acc) xs k + + appDummies (v:vl) (VPi p _ (Closure _ r)) x = appDummies vl (r v) (vApp p x v) + appDummies [] _ x = x + appDummies vs t _ = error (show (vs, t)) + + boundaryFormulas [] (VSystem fs) = fs + boundaryFormulas (x:xs) k = boundaryFormulas xs $ k @@ VVar x + boundaryFormulas a b = error (show (a, b)) check exp ty = do (tm, has) <- switch $ infer exp wp <- isConvertibleTo has ty pure (wp tm) -checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> Value -> ElabM a) -> ElabM a +checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> Maybe Boundary -> Value -> ElabM a) -> ElabM a checkPattern (P.PCap var) dom cont = do name <- asks (Map.lookup var . nameMap) case name of Just name@(ConName _ _ skip arity) -> do unless (arity == 0) $ throwElab $ UnsaturatedCon name - (ty, wp) <- instantiate =<< getNfType name + (ty, wp, _) <- instantiate =<< getNfType name unify ty dom wrap <- skipLams skip - cont (Con name) wrap =<< eval (wp (Con name)) + cont (Con name) wrap Nothing =<< eval (wp (Con name)) Just name -> throwElab $ NotACon name - Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name) (VVar name) + Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name) Nothing (VVar name) + checkPattern (P.PCon var args) dom cont = do name <- asks (Map.lookup var . nameMap) case name of Just name@(ConName _ _ nskip arity) -> do unless (arity == length args) $ throwElab $ UnsaturatedCon name - (ty, wp) <- instantiate =<< getNfType name + (ty, wp, xs) <- instantiate =<< getNfType name _ <- isConvertibleTo (skipBinders arity ty) dom + skip <- skipLams nskip + t <- asks (Map.lookup name . boundaries) + + con <- quote <$> getValue name + bindNames args ty $ \names wrap -> - cont (Con name) (skip . wrap) =<< eval (foldl (\x y -> App P.Ex x (Ref y)) (wp (Con name)) names) + cont (Con name) (skip . wrap) (instBoundary xs <$> t) =<< eval (foldl (\x y -> App P.Ex x (Ref y)) (wp con) names) + Just name -> throwElab $ NotACon name _ -> throwElab $ NotInScope (Bound var 0) where @@ -254,12 +312,15 @@ checkPattern (P.PCon var args) dom cont = bindNames [] _ k = k [] id bindNames xs t _ = error $ show (xs, t) -instantiate :: NFType -> ElabM (NFType, Term -> Term) +instBoundary :: [Value] -> Boundary -> Boundary +instBoundary metas (Boundary x y) = Boundary x (foldl (vApp P.Ex) y metas) + +instantiate :: NFType -> ElabM (NFType, Term -> Term, [Value]) instantiate (VPi P.Im d (Closure _ k)) = do t <- newMeta d - (ty, w) <- instantiate (k t) - pure (ty, \inner -> App P.Im (w inner) (quote t)) -instantiate x = pure (x, id) + (ty, w, xs) <- instantiate (k t) + pure (ty, \inner -> w (App P.Im inner (quote t)), t:xs) +instantiate x = pure (x, id, []) skipLams :: Int -> ElabM (Term -> Term) skipLams 0 = pure id @@ -447,13 +508,17 @@ checkStatement (P.Data name tele retk constrs) k = do checkTeleRetk True tele retk \kind tele undef -> do kind_nf <- eval kind - defineInternal (Defined name 0) kind_nf (\name' -> VNe (HData name') mempty) \name' -> - checkCons tele (VNe (HData name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k) + defineInternal (Defined name 0) kind_nf (\name' -> VNe (mkHead name') mempty) \name' -> + checkCons tele (VNe (mkHead name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k) where makeProj (x, p, _) = PApp p (VVar x) markAsDef x e = e { definedNames = Set.insert x (definedNames e) } + mkHead name + | any (\case { P.Path{} -> True; _ -> False}) constrs = HData True name + | otherwise = HData False name + checkTeleRetk allKan [] retk cont = do t <- check retk VTypeω t_nf <- eval t @@ -472,7 +537,7 @@ checkStatement (P.Data name tele retk constrs) k = checkCons _ _et [] k = k - checkCons n ret ((x, ty):xs) k = do + checkCons n ret (P.Point x ty:xs) k = do t <- check ty VTypeω ty_nf <- eval t let @@ -482,6 +547,34 @@ checkStatement (P.Data name tele retk constrs) k = unify ret' ret closed_nf <- eval closed defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons n ret xs k + + checkCons n ret (P.Path name indices return faces:xs) k = do + (con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do + t <- check return VTypeω + ty_nf <- eval t + let + (args, ret') = splitPi ty_nf + closed = close n (addArgs args (addInterval indices (quote ret'))) + n' = map (\(x, _, y) -> (x, P.Im, y)) n + + addArgs = flip $ foldr (\(x, p, t) -> Pi p x (quote t)) + addInterval = flip $ foldr (\n -> Pi P.Ex n I) + + envArgs ((x, _, y):xs) = assume x y . const . envArgs xs + envArgs [] = id + + closed_nf <- eval closed + unify ret' ret + + faces <- envArgs args $ for faces \(f, t) -> do + phi <- checkFormula f + t <- check t ret + pure (quote phi, t) + + system <- eval $ foldr (\x -> Lam P.Ex x) (System (Map.fromList faces)) (map (\(x, _, _) -> x) n' ++ map (\(x, _, _) -> x) args ++ indices) + + pure (ConName name 0 (length n') (length args + length indices), closed_nf, makePCon closed_nf mempty n' args indices system, Boundary indices system) + defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons n ret xs k close [] t = t close ((x, _, y):xs) t = Pi P.Im x (quote y) (close xs t) @@ -493,6 +586,11 @@ checkStatement (P.Data name tele retk constrs) k = makeCon cty sp ((nm, p, _):xs) ys con = VLam p $ Closure nm \a -> makeCon cty (sp Seq.:|> PApp p a) xs ys con makeCon cty sp [] ((nm, p, _):ys) con = VLam p $ Closure nm \a -> makeCon cty (sp Seq.:|> PApp p a) [] ys con + makePCon cty sp [] [] [] sys con = VNe (HPCon sys cty con) sp + makePCon cty sp ((nm, p, _):xs) ys zs sys con = VLam p $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp p a) xs ys zs (sys @@ a) con + makePCon cty sp [] ((nm, p, _):ys) zs sys con = VLam p $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp p a) [] ys zs (sys @@ a) con + makePCon cty sp [] [] (nm:zs) sys con = VLam P.Ex $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp P.Ex a) [] [] zs (sys @@ a) con + evalFix :: Name -> NFType -> Term -> ElabM Value evalFix name nft term = do env <- ask diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs index 1402aa3..841d715 100644 --- a/src/Elab/Eval.hs +++ b/src/Elab/Eval.hs @@ -36,6 +36,8 @@ import Syntax import System.IO.Unsafe import {-# SOURCE #-} Elab.WiredIn +import Debug.Trace +import Data.List (sortOn) eval :: Term -> ElabM Value eval t = asks (flip eval' t) @@ -109,11 +111,12 @@ zonkIO (VSystem fs) = do zonkIO (VSub a b c) = VSub <$> zonkIO a <*> zonkIO b <*> zonkIO c zonkIO (VInc a b c) = VInc <$> zonkIO a <*> zonkIO b <*> zonkIO c zonkIO (VComp a b c d) = comp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d +zonkIO (VHComp a b c d) = hComp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d zonkIO (VGlueTy a phi ty e) = glueType <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e zonkIO (VGlue a phi ty e t x) = glueElem <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO t <*> zonkIO x zonkIO (VUnglue a phi ty e x) = unglue <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO x -zonkIO (VCase x xs) = VCase <$> zonkIO x <*> pure xs +zonkIO (VCase t x xs) = VCase <$> zonkIO t <*> zonkIO x <*> pure xs zonkSp :: Projection -> IO Projection zonkSp (PApp p x) = PApp p <$> zonkIO x @@ -143,7 +146,13 @@ eval' env (Con x) = Just (ty, _) -> VNe (HCon ty x) mempty Nothing -> error $ "constructor " ++ show x ++ " has no type in scope" -eval' _ (Data x) = VNe (HData x) mempty +eval' env (PCon sys x) = + case Map.lookup x (getEnv env) of + Just (ty, _) -> VNe (HPCon (eval' env sys) ty x) mempty + Nothing -> error $ "constructor " ++ show x ++ " has no type in scope" + + +eval' _ (Data n x) = VNe (HData n x) mempty eval' env (App p f x) = vApp p (eval' env f) (eval' env x) eval' env (Lam p s t) = @@ -191,6 +200,7 @@ eval' e (Inc a phi u) = VInc (eval' e a) (eval' e phi) (eval' e u) eval' e (Ouc a phi u x) = outS (eval' e a) (eval' e phi) (eval' e u) (eval' e x) eval' e (Comp a phi u a0) = comp (eval' e a) (eval' e phi) (eval' e u) (eval' e a0) +eval' e (HComp a phi u a0) = hComp (eval' e a) (eval' e phi) (eval' e u) (eval' e a0) eval' e (GlueTy a phi tys f) = glueType (eval' e a) (eval' e phi) (eval' e tys) (eval' e f) eval' e (Glue a phi tys eqvs t x) = glueElem (eval' e a) (eval' e phi) (eval' e tys) (eval' e eqvs) (eval' e t) (eval' e x) @@ -199,15 +209,28 @@ eval' e (Let ns x) = let env' = foldl (\newe (n, ty, x) -> newe { getEnv = Map.insert n (eval' newe ty, eval' newe x) (getEnv newe) }) e ns in eval' env' x -eval' e (Case sc xs) = evalCase e (eval' e sc) xs +eval' e (Case range sc xs) = evalCase e (eval' e range @@) (force (eval' e sc)) xs + +evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Term)] -> Value +evalCase _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc)) + +evalCase env rng (VHComp a phi u a0) cases = + comp (fun \i -> rng (v i)) phi (system \i is1 -> evalCase env rng (u @@ i @@ is1) cases) + (VInc (rng a) phi (evalCase env rng (outS a0 phi (u @@ VI0) a0) cases)) + where + v = Elab.WiredIn.fill a phi u a0 + +evalCase env _ sc ((Ref _, k):_) = eval' env k @@ sc + +evalCase env rng (val@(VNe (HCon _ x) sp)) ((Con x', k):xs) + | x == x' = foldl applProj (eval' env k) sp + | otherwise = evalCase env rng val xs -evalCase :: ElabEnv -> Value -> [(Term, Term)] -> Value -evalCase _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc)) -evalCase env sc ((Ref _, k):_) = eval' env k @@ sc -evalCase env (force -> val@(VNe (HCon _ x) sp)) ((Con x', k):xs) +evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', k):xs) | x == x' = foldl applProj (eval' env k) sp - | otherwise = evalCase env val xs -evalCase _ sc xs = VCase sc xs + | otherwise = evalCase env rng val xs + +evalCase _ rng sc xs = VCase (fun rng) sc xs vApp :: HasCallStack => Plicity -> Value -> Value -> Value vApp p (VLam p' k) arg @@ -247,6 +270,12 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs + go (VNe (HPCon s _ _) _) rhs + | VSystem _ <- s = go (force s) rhs + + go lhs (VNe (HPCon s _ _) _) + | VSystem _ <- s = go lhs (force s) + go (VNe x a) (VNe x' a') | x == x', length a == length a' = traverse_ (uncurry unify'Spine) (Seq.zip a a') @@ -317,6 +346,11 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where go (VSystem sys) rhs = goSystem unify' sys rhs go rhs (VSystem sys) = goSystem (flip unify') sys rhs + go (VCase _ a b) (VCase _ a' b') = do + unify' a a' + let go a b = join $ unify' <$> eval (snd a) <*> eval (snd b) + zipWithM_ go (sortOn fst b) (sortOn fst b') + go x y | x == y = pure () | otherwise = @@ -433,6 +467,7 @@ checkScope scope (VNe h sp) = NotInScope v HVar{} -> pure () HCon{} -> pure () + HPCon{} -> pure () HMeta{} -> pure () HData{} -> pure () traverse_ checkProj sp @@ -483,12 +518,13 @@ checkScope s (VSystem fs) = checkScope s (VSub a b c) = traverse_ (checkScope s) [a, b, c] checkScope s (VInc a b c) = traverse_ (checkScope s) [a, b, c] checkScope s (VComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0] +checkScope s (VHComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0] checkScope s (VGlueTy a phi ty eq) = traverse_ (checkScope s) [a, phi, ty, eq] checkScope s (VGlue a phi ty eq inv x) = traverse_ (checkScope s) [a, phi, ty, eq, inv, x] checkScope s (VUnglue a phi ty eq vl) = traverse_ (checkScope s) [a, phi, ty, eq, vl] -checkScope s (VCase v _) = checkScope s v +checkScope s (VCase _ v _) = checkScope s v checkSpine :: Set Name -> Seq Projection -> ElabM [Name] checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs) diff --git a/src/Elab/Monad.hs b/src/Elab/Monad.hs index f621006..934a46f 100644 --- a/src/Elab/Monad.hs +++ b/src/Elab/Monad.hs @@ -34,6 +34,8 @@ data ElabEnv = , whereBound :: Map Name (P.Posn, P.Posn) , definedNames :: Set Name + , boundaries :: Map Name Boundary + , unsolvedMetas :: {-# UNPACK #-} !(IORef (Map MV [(Seq Projection, Value)])) } @@ -42,7 +44,10 @@ newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a } via ReaderT ElabEnv IO emptyEnv :: IO ElabEnv -emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing Nothing mempty mempty <$> newIORef mempty +emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing Nothing mempty mempty mempty <$> newIORef mempty + +addBoundary :: Name -> Boundary -> ElabM a -> ElabM a +addBoundary nm boundary = local (\e -> e { boundaries = Map.insert nm boundary (boundaries e)} ) assume :: Name -> Value -> (Name -> ElabM a) -> ElabM a assume nm ty k = defineInternal nm ty VVar k diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs index 341043e..e3dfa83 100644 --- a/src/Elab/WiredIn.hs +++ b/src/Elab/WiredIn.hs @@ -25,6 +25,7 @@ import Syntax.Pretty (prettyTm) import Syntax import System.IO.Unsafe +import Debug.Trace (traceShowId, traceShow) wiType :: WiredIn -> NFType wiType WiType = VType @@ -195,10 +196,10 @@ ielim line left right fn i = 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 x xs -> VCase x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs) + VCase r x xs -> VCase r x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs) _ -> error $ "can't ielim " ++ show (prettyTm (quote fn)) -outS :: NFSort -> NFEndp -> Value -> Value -> Value +outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value outS _ (force -> VI1) u _ = u @@ VItIsOne outS _ _phi _ (VInc _ _ x) = x @@ -210,8 +211,15 @@ outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v)) -- Composition comp :: NFLine -> NFEndp -> Value -> Value -> Value -comp _ VI1 u _ = u @@ VI1 @@ VItIsOne -comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = +comp a VI1 u _ + | not (isTyFam a) = u @@ VI1 @@ VItIsOne + where + isTyFam a = + case force (a @@ VI0) of + VType -> True + _ -> False + +comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = case force $ a @@ VVar (Bound (T.pack "i") 0) of VPi{} -> let @@ -258,17 +266,17 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = fam = a in let - base i = let VGlueTy base _ _ _ = force (fam @@ i) in base - phi i = let VGlueTy _ phi _ _ = force (fam @@ i) in phi - types i = let VGlueTy _ _ types _ = force (fam @@ i) in types - equivs i = let VGlueTy _ _ _ equivs = force (fam @@ i) in equivs + base i = let VGlueTy base _ _ _ = forceAndGlue (fam @@ i) in base + phi i = let VGlueTy _ phi _ _ = forceAndGlue (fam @@ i) in phi + types i = let VGlueTy _ _ types _ = forceAndGlue (fam @@ i) in types + equivs i = let VGlueTy _ _ _ equivs = forceAndGlue (fam @@ i) in equivs a i = fun \u -> unglue (base i) (phi i) (types i @@ u) (equivs i @@ u) (b @@ i @@ u) a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0 del = faceForall phi - a1' = comp (line base) psi (line a) (VInc undefined undefined a0) - t1' = comp (line types) psi (line (b @@)) (VInc undefined undefined b0) + a1' = comp (line base) psi (line a) (VInc (base VI0) (phi VI0) a0) + t1' = comp (line types) psi (line (b @@)) (VInc (base VI0) (phi VI0) b0) (omega_st, omega_t, omega_rep) = pres types base equivs psi (b @@) b0 omega = outS omega_t psi omega_rep omega_st @@ -290,17 +298,35 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1 in b1 - VType -> VGlueTy a0 phi (system \_ _ -> mkVSystem (Map.fromList [(phi, u @@ VI1 @@ VItIsOne)])) - (system \_ _ -> mkVSystem (Map.fromList [(phi, makeEquiv (\j -> (u @@ inot j)))])) + VType -> VGlueTy a0 phi (fun \is1 -> u @@ VI1 @@ is1) + (fun \i -> mkVSystem (Map.fromList [(phi, makeEquiv (\i -> u @@ inot i @@ VItIsOne))])) - VNe HData{} args -> + VNe (HData False _) args -> case force a0 of VNe (HCon con_type con_name) con_args -> VNe (HCon con_type con_name) $ compConArgs (length args) (a @@) con_type con_args phi u _ -> VComp a phi u (VInc (a @@ VI0) phi a0) + + VNe (HData True _) args -> compHIT (length args) (a @@) phi u incA0 _ -> VComp a phi u (VInc (a @@ VI0) phi a0) +forceAndGlue :: Value -> Value +forceAndGlue v = + case force v of + v@VGlueTy{} -> v + y -> VGlueTy y VI1 (fun (const y)) (fun (const (idEquiv y))) + +compHIT :: Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value +compHIT _ a phi u a0 = error $ unlines + [ "*** TODO: composition for HIT: " + , "domain = " ++ show (prettyTm (quote (zonk (fun a)))) + , "phi = " ++ show (prettyTm (quote (zonk phi))) + , "u = " ++ show (prettyTm (quote (zonk u))) + , "a0 = " ++ show (prettyTm (quote (zonk a0))) + ] + + compConArgs :: Int -> (NFEndp -> Value) -> Value -> Seq.Seq Projection -> NFEndp -> Value -> Seq.Seq Projection compConArgs total_args fam = go total_args where go _ _ Seq.Empty _ _ = Seq.Empty @@ -318,14 +344,14 @@ compConArgs total_args fam = go total_args where nthArg i (VSystem vs) = VSystem (fmap (nthArg i) vs) nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs)) - makeFiller nth (VNe (HData (Bound _ (negate -> 10))) args) phi u a0 = + makeFiller nth (VNe (HData _ (Bound _ (negate -> 10))) args) phi u a0 = fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0 makeFiller _ _ _ _ a0 = fun (const a0) makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs makeDomain _ = error "somebody smuggled something that smells" - smuggle x = VNe (HData (Bound "__comp_con_tyarg" (negate 10))) (Seq.singleton (PApp P.Ex x)) + smuggle x = VNe (HData False (Bound "__comp_con_tyarg" (negate 10))) (Seq.singleton (PApp P.Ex x)) compOutS :: NFSort -> NFEndp -> Value -> Value -> Value compOutS a b c d = compOutS a b c (force d) where @@ -344,6 +370,10 @@ fill a phi u a0 j = , (inot j, 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 @@ -411,14 +441,16 @@ contr a aC phi u = (vProj1 aC) makeEquiv :: (NFEndp -> Value) -> Value -makeEquiv line = comp (fun \i -> equiv a (line i)) VI0 (system \_ _ -> VSystem mempty) (VPair idfun idisequiv) where +makeEquiv line = comp (fun \i -> equiv a (line i)) VI0 (system \_ _ -> VSystem mempty) (idEquiv a) where a = line VI0 + +idEquiv :: NFSort -> Value +idEquiv a = VPair idfun idisequiv where idfun = fun id --- idEquiv y = ((y, \i -> y), \u i -> (u.2 (inot i), \j -> u.2 (ior (inot i) j))) 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))) + id_fiber y = VPair y (VLine a y y (fun (const y))) \ No newline at end of file diff --git a/src/Elab/WiredIn.hs-boot b/src/Elab/WiredIn.hs-boot index b3b6545..9b20dad 100644 --- a/src/Elab/WiredIn.hs-boot +++ b/src/Elab/WiredIn.hs-boot @@ -1,6 +1,7 @@ module Elab.WiredIn where import Syntax +import GHC.Stack.Types wiType :: WiredIn -> NFType wiValue :: WiredIn -> NFType @@ -9,9 +10,14 @@ iand, ior :: NFEndp -> NFEndp -> NFEndp inot :: NFEndp -> NFEndp ielim :: NFSort -> Value -> Value -> Value -> NFEndp -> Value -outS :: NFSort -> NFEndp -> Value -> Value -> Value +outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value comp :: NFLine -> NFEndp -> Value -> Value -> Value +fill :: NFLine -> NFEndp -> Value -> Value -> Value -> Value +hComp :: NFSort -> NFEndp -> Value -> Value -> Value glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value -unglue :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value \ No newline at end of file +unglue :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value + +fun :: (Value -> Value) -> Value +system :: (Value -> Value -> Value) -> Value \ No newline at end of file diff --git a/src/Main.hs b/src/Main.hs index 9eec467..26ef83d 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -53,7 +53,7 @@ main = do Check files verbose -> do env <- checkFiles files when verbose $ dumpEnv env - Repl -> enterReplIn =<< emptyEnv + Repl -> enterReplIn =<< checkFiles ["./intro.tt"] enterReplIn :: ElabEnv -> IO () enterReplIn env = runInputT defaultSettings (loop env') where diff --git a/src/Presyntax/Parser.y b/src/Presyntax/Parser.y index 7932c43..d77ccce 100644 --- a/src/Presyntax/Parser.y +++ b/src/Presyntax/Parser.y @@ -164,9 +164,16 @@ Statement :: { Statement } | var LhsList '=' Rhs { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) } | '{-#' Pragma '#-}' { spanSt $1 $3 $ $2 } | 'postulate' START Postulates END { spanSt $1 $4 $ Postulate $3 } - | 'data' var Parameters ':' Exp 'where' START Postulates END + | 'data' var Parameters ':' Exp 'where' START Constructors END { spanSt $1 $9 $ Data (getVar $2) $3 $5 $8 } +Constructors :: { [Constructor] } + : var ':' Exp { [Point (getVar $1) $3] } + | var PatVarList ':' Exp '[' Faces ']' { [Path (getVar $1) (thd $2) $4 $6] } + | var ':' Exp Semis Constructors { Point (getVar $1) $3:$5 } + | var PatVarList ':' Exp '[' Faces ']' Semis Constructors + { Path (getVar $1) (thd $2) $4 $6:$9 } + Parameters :: { [(Text, Plicity, Expr)] } : {- empty -} { [] } | '(' var ':' Exp ')' Parameters { (getVar $2, Ex, $4):$6 } @@ -218,6 +225,14 @@ SystemLhs :: { Condition } : Formula 'as' var { Condition $1 (Just (getVar $3)) } | Formula { Condition $1 Nothing } +Faces :: { [(Formula, Expr)] } + : {- empty system -} { [] } + | NeFaces { $1 } + +NeFaces :: { [(Formula, Expr) ]} + : Formula '->' Exp { [($1, $3)] } + | Formula '->' Exp ',' NeFaces { ($1, $3):$5 } + Formula :: { Formula } : Disjn { $1 } | Disjn '&&' Disjn { $1 `FAnd` $3 } diff --git a/src/Presyntax/Presyntax.hs b/src/Presyntax/Presyntax.hs index 0e98e0c..e5cd810 100644 --- a/src/Presyntax/Presyntax.hs +++ b/src/Presyntax/Presyntax.hs @@ -60,11 +60,16 @@ data Statement | ReplNf Expr -- REPL eval | ReplTy Expr -- REPL :t - | Data Text [(Text, Plicity, Expr)] Expr [(Text, Expr)] + | Data Text [(Text, Plicity, Expr)] Expr [Constructor] | SpanSt Statement Posn Posn deriving (Eq, Show, Ord) +data Constructor + = Point Text Expr + | Path Text [Text] Expr [(Formula, Expr)] + deriving (Eq, Show, Ord) + data Posn = Posn { posnLine :: {-# UNPACK #-} !Int , posnColm :: {-# UNPACK #-} !Int diff --git a/src/Syntax.hs b/src/Syntax.hs index 9430c89..2cb7af7 100644 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -50,7 +50,8 @@ data WiredIn data Term = Ref Name | Con Name - | Data Name + | PCon Term Name + | Data Bool Name | App Plicity Term Term | Lam Plicity Name Term | Pi Plicity Name Term Term @@ -91,12 +92,13 @@ data Term | Ouc Term Term Term Term | Comp Term Term Term Term + | HComp Term Term Term Term | GlueTy Term Term Term Term | Glue Term Term Term Term Term Term | Unglue Term Term Term Term Term - | Case Term [(Term, Term)] + | Case Term Term [(Term, Term)] deriving (Eq, Show, Ord, Data) data MV = @@ -167,13 +169,14 @@ data Value | VSub NFSort NFEndp Value | VInc NFSort NFEndp Value - | VComp NFSort NFEndp Value Value + | VComp NFLine NFEndp Value Value + | VHComp NFSort NFEndp Value Value | VGlueTy NFSort NFEndp NFPartial NFPartial | VGlue NFSort NFEndp NFPartial NFPartial NFPartial Value | VUnglue NFSort NFEndp NFPartial NFPartial Value - | VCase Value [(Term, Term)] + | VCase Value Value [(Term, Term)] deriving (Eq, Show, Ord) pattern VVar :: Name -> Value @@ -181,10 +184,17 @@ pattern VVar x = VNe (HVar x) Seq.Empty quoteWith :: Set Name -> Value -> Term quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where - goHead (HVar v) = Ref v - goHead (HMeta m) = Meta m - goHead (HCon _ v) = Con v - goHead (HData v) = Data v + goHead (HVar v) = Ref v + goHead (HMeta m) = Meta m + goHead (HCon _ v) = Con v + goHead (HPCon sys _ v) = + case sys of + VSystem f -> + case Map.lookup VI1 f of + Just vl -> constantly (length sp) vl + _ -> PCon (quote sys) v + _ -> PCon (quote sys) v + goHead (HData x v) = Data x v goSpine t (PApp p v) = App p t (quoteWith names v) goSpine t (PIElim l x y i) = IElim (quote l) (quote x) (quote y) t (quote i) @@ -192,12 +202,16 @@ quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where goSpine t PProj2 = Proj2 t goSpine t (POuc a phi u) = Ouc (quote a) (quote phi) (quote u) t + constantly 0 n = quoteWith names n + constantly k x = Lam Ex (Bound (T.pack "x") (negate 1)) $ constantly (k - 1) x + +quoteWith names (GluedVl _ Seq.Empty x) = quoteWith names x + quoteWith names (GluedVl h sp (VLam p (Closure n k))) = quoteWith names (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PApp p a) (k a)))) quoteWith names (GluedVl h sp vl) | GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner) - | Seq.Empty <- sp = quoteWith names vl | alwaysShort vl = quoteWith names vl | otherwise = quoteWith names (VNe h sp) @@ -236,12 +250,13 @@ quoteWith names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith quoteWith names (VSub a b c) = Sub (quoteWith names a) (quoteWith names b) (quoteWith names c) quoteWith names (VInc a b c) = Inc (quoteWith names a) (quoteWith names b) (quoteWith names c) quoteWith names (VComp a phi u a0) = Comp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0) +quoteWith names (VHComp a phi u a0) = HComp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0) quoteWith names (VGlueTy a phi t e) = GlueTy (quoteWith names a) (quoteWith names phi) (quoteWith names t) (quoteWith names e) quoteWith names (VGlue a phi ty e t x) = Glue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names t) (quoteWith names x) quoteWith names (VUnglue a phi ty e x) = Unglue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names x) -quoteWith names (VCase v xs) = Case (quoteWith names v) xs +quoteWith names (VCase rng v xs) = Case (quoteWith names rng) (quoteWith names v) xs alwaysShort :: Value -> Bool alwaysShort (VNe HCon{} _) = True @@ -278,34 +293,10 @@ instance Ord Closure where data Head = HVar Name | HCon Value Name + | HPCon Value Value Name | HMeta MV - | HData Name - deriving (Show) - -instance Eq Head where - HVar x == HVar y = x == y - HCon _ x == HCon _ y = x == y - HMeta x == HMeta y = x == y - HData x == HData y = x == y - _ == _ = False - -instance Ord Head where - compare x y = - case x of - HVar n -> case y of - HVar n' -> compare n n' - _ -> LT - HCon _ n -> case y of - HVar _ -> GT - HCon _ n' -> compare n n' - _ -> LT - HMeta n -> case y of - HMeta n' -> compare n n' - HData _ -> LT - _ -> GT - HData n -> case y of - HData n' -> compare n n' - _ -> GT + | HData Bool Name + deriving (Eq, Ord, Show) data Projection = PApp Plicity Value @@ -314,3 +305,6 @@ data Projection | PProj2 | POuc NFSort NFEndp Value deriving (Eq, Show, Ord) + +data Boundary = Boundary { getBoundaryNames :: [Name], getBoundaryMap :: Value } + deriving (Eq, Show, Ord) \ No newline at end of file diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs index bea9123..3812da2 100644 --- a/src/Syntax/Pretty.hs +++ b/src/Syntax/Pretty.hs @@ -30,9 +30,10 @@ prettyTm = prettyTm . everywhere (mkT beautify) where Just ('.', w) -> keyword (pretty w) _ -> pretty v prettyTm (Con v) = keyword (pretty v) - prettyTm (Data v) = operator (pretty v) + prettyTm (PCon _ v) = keyword (pretty v) + prettyTm (Data _ v) = operator (pretty v) - prettyTm (App Im f x) = parenFun f <+> braces (prettyTm x) + prettyTm (App Im f _) = prettyTm f prettyTm (App Ex f x) = parenFun f <+> parenArg x prettyTm (Pair x y) = parens $ prettyTm x <> operator comma <+> prettyTm y @@ -76,7 +77,7 @@ prettyTm = prettyTm . everywhere (mkT beautify) where prettyTm (System xs) = braces (line <> indent 2 (vcat (punctuate comma (map go (Map.toList xs)))) <> line) where go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t - prettyTm (Case x xs) = keyword (pretty "case") <+> prettyTm x <+> keyword (pretty "of") <+> braces (line <> indent 2 (prettyCase xs) <> line) + prettyTm (Case _ x xs) = keyword (pretty "case") <+> prettyTm x <+> keyword (pretty "of") <+> braces (line <> indent 2 (prettyCase xs) <> line) prettyTm (Let xs e) = align $ keyword (pretty "let") <+> braces (line <> indent 2 (prettyLet xs) <> line) <+> keyword (pretty "in") <+> prettyTm e prettyTm x = error (show x) @@ -91,6 +92,9 @@ prettyTm = prettyTm . everywhere (mkT beautify) where beautify (IElim _ _ _ f i) = App Ex f i beautify (PathIntro _ _ _ f) = f + beautify (App p (Lam p' v b) _) + | v `Set.notMember` freeVars b = beautify b + beautify (IsOne phi) = toFun "IsOne" [phi] beautify ItIsOne = Ref (Bound (T.pack ".1=1") 0) @@ -100,11 +104,12 @@ prettyTm = prettyTm . everywhere (mkT beautify) where beautify (Partial phi a) = toFun "Partial" [phi, a] beautify (PartialP phi a) = toFun "PartialP" [phi, a] beautify (Comp a phi u a0) = toFun "comp" [a, phi, u, a0] + beautify (HComp a phi u a0) = toFun "hcomp" [a, phi, u, a0] beautify (Sub a phi u) = toFun "Sub" [a, phi, u] beautify (Inc _ _ u) = toFun "inS" [u] - beautify (Ouc _ _ _ u) = toFun "outS" [u] + beautify (Ouc a phi u u0) = toFun "outS" [a, phi, u, u0] - beautify (GlueTy a I1 _ _) = a + -- beautify (GlueTy a I1 _ _) = a beautify (GlueTy a b c d) = toFun "Glue" [a,b,c,d] beautify (Glue a b c d e f) = toFun "glue" [a,b,c,d,e,f] beautify (Unglue a b c d e) = toFun "unglue" [a,b,c,d,e] @@ -164,6 +169,7 @@ freeVars (Let ns x) = Set.union (freeVars x `Set.difference` bound) freed where freed = foldr (\(_, x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty ns freeVars Meta{} = mempty freeVars Con{} = mempty +freeVars PCon{} = mempty freeVars Data{} = mempty freeVars Type{} = mempty freeVars Typeω{} = mempty @@ -189,8 +195,11 @@ freeVars (System fs) = foldr (\(x, y) -> Set.union (Set.union (freeVars x) (free freeVars (Sub x y z) = Set.unions $ map freeVars [x, y, z] freeVars (Inc x y z) = Set.unions $ map freeVars [x, y, z] freeVars (Ouc x y z a) = Set.unions $ map freeVars [x, y, z, a] + freeVars (Comp x y z a) = Set.unions $ map freeVars [x, y, z, a] +freeVars (HComp x y z a) = Set.unions $ map freeVars [x, y, z, a] + freeVars (GlueTy x y z a) = Set.unions $ map freeVars [x, y, z, a] freeVars (Glue x y z a b c) = Set.unions $ map freeVars [x, y, z, a, b, c] freeVars (Unglue x y z a c) = Set.unions $ map freeVars [x, y, z, a, c] -freeVars (Case x y) = freeVars x <> foldMap (freeVars . snd) y +freeVars (Case rng x y) = freeVars rng <> freeVars x <> foldMap (freeVars . snd) y