From de5e1e33b8b6797454a5d06596d3c28b9e9cdfa4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Sun, 14 Mar 2021 01:58:13 -0300 Subject: [PATCH] Fix recursive local lets --- intro.tt | 112 +++++++++++++++++++++++++++++++++++------- src/Elab.hs | 34 ++++++------- src/Elab/Eval.hs | 43 ++++++++++------ src/Elab/Monad.hs | 3 ++ src/Elab/WiredIn.hs | 1 + src/Main.hs | 34 ++++++++++--- src/Presyntax/Lexer.x | 5 +- src/Syntax.hs | 4 +- src/Syntax/Pretty.hs | 28 +++++------ 9 files changed, 184 insertions(+), 80 deletions(-) diff --git a/intro.tt b/intro.tt index 2971c27..3e4093c 100644 --- a/intro.tt +++ b/intro.tt @@ -529,21 +529,21 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where fill0 : I -> I -> A fill0 i j = comp (\i -> A) (\k [ (i = i0) -> t x0 (iand j k) - , (i = i1) -> g y - , (j = i0) -> g (p0 i) - ]) + , (i = i1) -> g y + , (j = i0) -> g (p0 i) + ]) (inS (g (p0 i))) fill1 : I -> I -> A fill1 i j = comp (\i -> A) (\k [ (i = i0) -> t x1 (iand j k) - , (i = i1) -> g y - , (j = i0) -> g (p1 i) ]) + , (i = i1) -> g y + , (j = i0) -> g (p1 i) ]) (inS (g (p1 i))) fill2 : I -> I -> A fill2 i j = comp (\i -> A) (\k [ (i = i0) -> rem0 (ior j (inot k)) - , (i = i1) -> rem1 (ior j (inot k)) - , (j = i1) -> g y ]) + , (i = i1) -> rem1 (ior j (inot k)) + , (j = i1) -> g y ]) (inS (g y)) sq : I -> I -> A @@ -555,10 +555,10 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where sq1 : I -> I -> B sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 j) k - , (i = i1) -> s (p1 j) k - , (j = i0) -> s (f (p i)) k - , (j = i1) -> s y k - ]) + , (i = i1) -> s (p1 j) k + , (j = i0) -> s (f (p i)) k + , (j = i1) -> s y k + ]) (inS (f (sq i j))) in \i -> (p i, \j -> sq1 i j) @@ -792,7 +792,8 @@ data Interval : Type where -- 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 : {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 @@ -842,6 +843,17 @@ windingSymLoop = refl windingBase : Path (winding (\i -> base)) (pos zero) windingBase = refl +goAround : Int -> Path base base +goAround = + \case + pos n -> goAround_nat n + neg n -> sym (goAround_nat (succ n)) + where + goAround_nat : Nat -> Path base base + goAround_nat = \case + zero -> refl + succ n -> trans (\i -> loop i) (goAround_nat n) + -- 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. @@ -913,7 +925,7 @@ torusToCircs = \case pathTwo i -> (base, loop i) square i j -> (loop i, loop j) -circsToTorus : ((x : S1) * S1) -> T2 +circsToTorus : (S1 * S1) -> T2 circsToTorus pair = go pair.1 pair.2 where baseCase : S1 -> T2 @@ -938,13 +950,77 @@ torusToCircsToTorus = \case pathTwo i -> refl square i j -> refl -postulate - exerciseForTomorrow : {A : Type} -> A - circsToTorusToCircs : (p : S1 * S1) -> Path (torusToCircs (circsToTorus p)) p -circsToTorusToCircs = exerciseForTomorrow +circsToTorusToCircs pair = go pair.1 pair.2 + where + baseCase : (y : S1) -> Path (torusToCircs (circsToTorus (base, y))) (base, y) + baseCase = \case + base -> refl + loop j -> refl + + loopCase : (i : I) (y : S1) -> Path (torusToCircs (circsToTorus (loop i, y))) (loop i, y ) + loopCase i = \case + base -> refl + loop j -> refl + + go : (x : S1) (y : S1) -> Path (torusToCircs (circsToTorus (x, y))) (x, y) + go = \case + base -> baseCase + loop i -> loopCase i TorusIsTwoCircles : Path T2 (S1 * S1) TorusIsTwoCircles = univalence (IsoToEquiv theIso) where theIso : Iso T2 (S1 * S1) - theIso = (torusToCircs, circsToTorus, circsToTorusToCircs, torusToCircsToTorus) \ No newline at end of file + theIso = (torusToCircs, circsToTorus, circsToTorusToCircs, torusToCircsToTorus) + +abs : Int -> Nat +abs = \case + pos n -> n + neg n -> succ n + +sign : Int -> Bool +sign = \case + pos n -> true + neg n -> false + +boolAnd : Bool -> Bool -> Bool +boolAnd = \case + true -> \case + true -> true + false -> false + false -> \case + true -> false + false -> false + +plusNat : Nat -> Nat -> Nat +plusNat = \case + zero -> \x -> x + succ n -> \x -> succ (plusNat n x) + +plusZero : (x : Nat) -> Path (plusNat zero x) x +plusZero = \case + zero -> refl + succ n -> \i -> succ (plusZero n i) + +multNat : Nat -> Nat -> Nat +multNat = \case + zero -> \x -> zero + succ n -> \x -> plusNat x (multNat n x) + +multInt : Int -> Int -> Int +multInt x y = signify (multNat (abs x) (abs y)) (boolAnd (sign x) (sign y)) where + signify : Nat -> Bool -> Int + signify = \case + zero -> \x -> pos zero + succ n -> \case + true -> pos (succ n) + false -> neg n + +two : Int +two = pos (succ (succ zero)) + +four : Int +four = multInt two two + +sixteen : Int +sixteen = multInt four four \ No newline at end of file diff --git a/src/Elab.hs b/src/Elab.hs index e780806..e8e74e7 100644 --- a/src/Elab.hs +++ b/src/Elab.hs @@ -205,7 +205,7 @@ check (P.LamCase pats) ty = 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 + checkPattern pat dom \pat wp boundary n_lams pat_nf -> do rhs <- check rhs (rng pat_nf) case boundary of -- If we're checking a higher constructor then we need to @@ -240,7 +240,7 @@ check (P.LamCase pats) ty = `withNote` (pretty "Mandated by the constructor" <+> prettyTm (quote pat_nf)) _ -> pure () - pure (pat, wp rhs) + pure (pat, n_lams, wp rhs) let x = wp (Lam P.Ex name (Case range (Ref name) cases)) pure x _ -> do @@ -253,8 +253,8 @@ check (P.LamCase pats) ty = 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 + (p, n, t) <- k (eval (Lam P.Ex n (Case rng (Ref n) acc))) x + checkPatterns rng ((p, n, t):acc) xs k appDummies (v:vl) (VPi p _ (Closure _ r)) x = appDummies vl (r v) (vApp p x v) appDummies [] _ x = x @@ -269,7 +269,7 @@ check exp ty = do wp <- isConvertibleTo has ty pure (wp tm) -checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> Maybe Boundary -> Value -> ElabM a) -> ElabM a +checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> Maybe Boundary -> Int -> Value -> ElabM a) -> ElabM a checkPattern (P.PCap var) dom cont = do name <- asks (Map.lookup var . nameMap) case name of @@ -278,9 +278,9 @@ checkPattern (P.PCap var) dom cont = do (ty, wp, _) <- instantiate =<< getNfType name unify ty dom wrap <- skipLams skip - cont (Con name) wrap Nothing =<< eval (wp (Con name)) + cont (Con name) wrap Nothing 0 =<< eval (wp (Con name)) Just name -> throwElab $ NotACon name - Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name) Nothing (VVar name) + Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name) Nothing 0 (VVar name) checkPattern (P.PCon var args) dom cont = do @@ -297,7 +297,7 @@ checkPattern (P.PCon var args) dom cont = con <- quote <$> getValue name bindNames args ty $ \names wrap -> - cont (Con name) (skip . wrap) (instBoundary xs <$> t) =<< eval (foldl (\x y -> App P.Ex x (Ref y)) (wp con) names) + cont (Con name) (skip . wrap) (instBoundary xs <$> t) (length names) =<< eval (foldl (\x y -> App P.Ex x (Ref y)) (wp con) names) Just name -> throwElab $ NotACon name _ -> throwElab $ NotInScope (Bound var 0) @@ -329,13 +329,13 @@ skipLams k = do n <- newName (Lam P.Im n . ) <$> skipLams (k - 1) -checkLetItems :: Map Text (Maybe NFType) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a +checkLetItems :: Map Text (Maybe (Name, NFType)) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a checkLetItems _ [] cont = cont [] checkLetItems map (P.LetDecl v t:xs) cont = do t <- check t VTypeω t_nf <- eval t - assume (Defined v 0) t_nf \_ -> - checkLetItems (Map.insert v (Just t_nf) map) xs cont + assume (Defined v 0) t_nf \name -> + checkLetItems (Map.insert v (Just (name, t_nf)) map) xs cont checkLetItems map (P.LetBind name rhs:xs) cont = do case Map.lookup name map of @@ -346,12 +346,12 @@ checkLetItems map (P.LetBind name rhs:xs) cont = do checkLetItems map xs \xs -> cont ((name', quote ty, tm):xs) Just Nothing -> throwElab $ Redefinition (Defined name 0) - Just (Just ty_nf) -> do + Just (Just (name, ty_nf)) -> do rhs <- check rhs ty_nf rhs_nf <- eval rhs - makeLetDef (Defined name 0) ty_nf rhs_nf \name' -> - checkLetItems (Map.insert name Nothing map) xs \xs -> - cont ((name', quote ty_nf, rhs):xs) + replaceLetDef name ty_nf rhs_nf $ + checkLetItems (Map.insert (getNameText name) Nothing map) xs \xs -> + cont ((name, quote ty_nf, rhs):xs) checkFormula :: P.Formula -> ElabM Value checkFormula P.FTop = pure VI1 @@ -598,10 +598,6 @@ checkStatement (P.Data name tele retk constrs) k = totalProp (x:xs) = ior (inot (VVar x)) (VVar x) `ior` totalProp xs totalProp [] = VI0 -evalFix :: Name -> NFType -> Term -> ElabM Value -evalFix name nft term = do - env <- ask - pure . fix $ \val -> eval' env{ getEnv = Map.insert name (nft, val) (getEnv env) } term checkProgram :: [P.Statement] -> ElabM a -> ElabM a checkProgram [] k = k diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs index 8702b0c..e2a2af9 100644 --- a/src/Elab/Eval.hs +++ b/src/Elab/Eval.hs @@ -38,8 +38,6 @@ import Syntax import System.IO.Unsafe import {-# SOURCE #-} Elab.WiredIn -import Control.Arrow (second) -import Debug.Trace eval :: HasCallStack => Term -> ElabM Value eval t = asks (flip eval' t) @@ -179,12 +177,16 @@ eval' e (GlueTy a phi tys f) = glueType (eval' e a) (eval' e phi) (eval' e tys) 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) eval' e (Unglue a phi tys f x) = unglue (eval' e a) (eval' e phi) (eval' e tys) (eval' e f) (eval' e x) 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 + let env' = foldl (\newe (n, ty, x) -> + let nft = eval' newe ty + in newe { getEnv = Map.insert n (nft, evalFix' newe n nft x) (getEnv newe) }) + e + ns in eval' env' x 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 :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Int, Term)] -> Value evalCase _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc)) evalCase env rng (VSystem fs) cases = VSystem (fmap (flip (evalCase env rng) cases) fs) @@ -195,18 +197,25 @@ evalCase env rng (VHComp a phi u a0) cases = where v = Elab.WiredIn.fill (fun (const a)) phi u a0 -evalCase env _ sc ((Ref _, k):_) = eval' env k @@ sc +evalCase env _ sc ((Ref _, _, k):_) = eval' env k @@ sc -evalCase env rng (val@(VNe (HCon _ x) sp)) ((Con x', k):xs) +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 env rng (val@(VNe (HPCon _ _ 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 rng val xs evalCase env rng sc xs = VCase (getEnv env) (fun rng) sc xs +evalFix' :: ElabEnv -> Name -> NFType -> Term -> Value +evalFix' env name nft term = fix $ \val -> eval' env{ getEnv = Map.insert name (nft, val) (getEnv env) } term + +evalFix :: Name -> NFType -> Term -> ElabM Value +evalFix name nft term = do + t <- ask + pure (evalFix' t name nft term) data NotEqual = NotEqual Value Value deriving (Show, Typeable, Exception) @@ -294,8 +303,8 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where 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') + let go (_, _, a) (_, _, b) = join $ unify' <$> eval a <*> eval b + zipWithM_ go (sortOn (\(x, _, _) -> x) b) (sortOn (\(x, _, _) -> x) b') go x y | x == y = pure () @@ -596,7 +605,7 @@ vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs) vApp p (VInc (VPi _ _ (Closure _ r)) phi f) arg = VInc (r (vApp p f arg)) phi (vApp p f arg) vApp p (VCase env rng sc branches) arg = VCase env (fun \x -> let VPi _ _ (Closure _ r) = rng @@ x in r arg) sc - (map (second (projIntoCase (flip (App p) (quote arg)))) branches) + (map (projIntoCase (flip (App p) (quote arg))) branches) vApp _ x _ = error $ "can't apply " ++ show (prettyTm (quote x)) (@@) :: HasCallStack => Value -> Value -> Value @@ -610,7 +619,7 @@ vProj1 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj1) (vProj1 vl) vProj1 (VSystem fs) = VSystem (fmap vProj1 fs) vProj1 (VInc (VSigma a _) b c) = VInc a b (vProj1 c) vProj1 (VCase env rng sc branches) = - VCase env (fun \x -> let VSigma a _ = rng @@ x in a) sc (map (second (projIntoCase Proj1)) branches) + VCase env rng sc (map (projIntoCase Proj1) branches) vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote x)) vProj2 :: HasCallStack => Value -> Value @@ -620,10 +629,12 @@ vProj2 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj2) (vProj2 vl) vProj2 (VSystem fs) = VSystem (fmap vProj2 fs) vProj2 (VInc (VSigma _ (Closure _ r)) b c) = VInc (r (vProj1 c)) b (vProj2 c) vProj2 (VCase env rng sc branches) = - VCase env (fun \x -> let VSigma _ (Closure _ r) = rng @@ x in r (vProj1 x)) sc (map (second (projIntoCase Proj2)) branches) + VCase env rng sc (map (projIntoCase Proj2) branches) vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x)) -projIntoCase :: (Term -> Term) -> Term -> Term -projIntoCase f (Lam p x r) = Lam p x (projIntoCase f r) -projIntoCase f (PathIntro l a b r) = PathIntro l a b (projIntoCase f r) -projIntoCase f x = f x \ No newline at end of file +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 \ No newline at end of file diff --git a/src/Elab/Monad.hs b/src/Elab/Monad.hs index 934a46f..68bfe62 100644 --- a/src/Elab/Monad.hs +++ b/src/Elab/Monad.hs @@ -58,6 +58,9 @@ define nm vty val = defineInternal nm vty (const val) makeLetDef :: Name -> Value -> Value -> (Name -> ElabM a) -> ElabM a makeLetDef nm vty val = defineInternal nm vty (\nm -> GluedVl (HVar nm) mempty val) +replaceLetDef :: Name -> Value -> Value -> ElabM a -> ElabM a +replaceLetDef nm vty val = redefine nm vty (GluedVl (HVar nm) mempty val) + assumes :: [Name] -> Value -> ([Name] -> ElabM a) -> ElabM a assumes nms ty k = do let diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs index 3193f4b..df561fb 100644 --- a/src/Elab/WiredIn.hs +++ b/src/Elab/WiredIn.hs @@ -191,6 +191,7 @@ ielim line left right (GluedVl h sp 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 diff --git a/src/Main.hs b/src/Main.hs index 37e2871..78737e8 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -47,17 +47,32 @@ main :: IO () main = do opts <- execParser parser case opts of - Load files -> do + Load files exp -> do env <- checkFiles files - enterReplIn env + case exp of + [] -> enterReplIn env + xs -> traverse_ (evalArgExpr env) xs Check files verbose -> do env <- checkFiles files when verbose $ dumpEnv env Repl -> enterReplIn =<< checkFiles ["./test.tt"] +evalArgExpr :: ElabEnv -> String -> IO () +evalArgExpr env str = + case runAlex (Bsl.fromStrict (T.encodeUtf8 inp)) parseExp of + Right e -> + flip runElab env (do + (e, _) <- infer e + liftIO . putStrLn . show . prettyTm . quote . zonk =<< Elab.Eval.eval e) + `catch` \e -> do + displayExceptions' inp (e :: SomeException) + Left e -> liftIO $ print e + where + inp = T.pack str + enterReplIn :: ElabEnv -> IO () enterReplIn env = runInputT defaultSettings (loop env') where - env' = env { commHook = T.putStrLn . render . prettyTm . quote . zonk } + env' = env { commHook = putStrLn . show . prettyTm . quote } loop :: ElabEnv -> InputT IO () loop env = do @@ -111,17 +126,20 @@ dumpEnv env = for_ (Map.toList (nameMap env)) $ \(_, name) -> parser :: ParserInfo Opts parser = info (subparser (load <> check) <|> pure Repl <**> helper) (header "cubical - a cubical programming language") where - load = command "load" $ info (fmap Load (some (argument str (metavar "file..."))) <**> helper) (progDesc "Check and load a list of files in the REPL") + load = command "load" $ + info ((Load <$> (some (argument str (metavar "file..."))) + <*> (many (strOption (long "eval" <> short 'e' <> help "Also evaluate this expression")))) + <**> helper) (progDesc "Check and load a list of files in the REPL") check = command "check" $ info ((Check <$> some (argument str (metavar "file...")) - <*> switch ( long "verbose" - <> short 'v' - <> help "Print the types of all declared/defined values")) + <*> switch ( long "verbose" + <> short 'v' + <> help "Print the types of all declared/defined values")) <**> helper) (progDesc "Check a list of files") data Opts - = Load { files :: [String] } + = Load { files :: [String], eval :: [String] } | Check { files :: [String], verbose :: Bool } | Repl deriving (Eq, Show, Ord) diff --git a/src/Presyntax/Lexer.x b/src/Presyntax/Lexer.x index 72123fd..4020f03 100644 --- a/src/Presyntax/Lexer.x +++ b/src/Presyntax/Lexer.x @@ -115,7 +115,7 @@ popStartCode = do alexSetStartCode x offsideRule :: AlexInput -> Int64 -> Alex Token -offsideRule (AlexPn _ line col, _, s, _) size +offsideRule (AlexPn _ line col, _, _, _) _ -- | Lbs.null s = pure (Token TokEof line col) | otherwise = do ~(col':ctx) <- layoutColumns <$> getUserState @@ -137,9 +137,8 @@ emptyLayout (AlexPn _ line col, _, _, _) _ = do pure (Token TokLEnd line col) startLayout :: AlexInput -> Int64 -> Alex Token -startLayout (AlexPn _ line col, _, s, _) size = do +startLayout (AlexPn _ line col, _, _, _) _ = do popStartCode - least <- leastColumn <$> getUserState ~(col':_) <- layoutColumns <$> getUserState if col' >= col then pushStartCode empty_layout diff --git a/src/Syntax.hs b/src/Syntax.hs index 1b8d56c..0839188 100644 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -98,7 +98,7 @@ data Term | Glue Term Term Term Term Term Term | Unglue Term Term Term Term Term - | Case Term Term [(Term, Term)] + | Case Term Term [(Term, Int, Term)] deriving (Eq, Show, Ord, Data) data MV = @@ -176,7 +176,7 @@ data Value | VGlue NFSort NFEndp NFPartial NFPartial NFPartial Value | VUnglue NFSort NFEndp NFPartial NFPartial Value - | VCase (Map.Map Name (NFType, Value)) Value Value [(Term, Term)] + | VCase (Map.Map Name (NFType, Value)) Value Value [(Term, Int, Term)] deriving (Eq, Show, Ord) pattern VVar :: Name -> Value diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs index 546b3cf..a304270 100644 --- a/src/Syntax/Pretty.hs +++ b/src/Syntax/Pretty.hs @@ -33,7 +33,7 @@ prettyTm = prettyTm . everywhere (mkT beautify) where prettyTm (PCon _ v) = keyword (pretty v) prettyTm (Data _ v) = operator (pretty v) - prettyTm (App Im f _) = prettyTm f + prettyTm (App Im f x) = parenFun f <+> braces (prettyTm x) prettyTm (App Ex f x) = parenFun f <+> parenArg x prettyTm (Pair x y) = parens $ prettyTm x <> operator comma <+> prettyTm y @@ -85,7 +85,7 @@ prettyTm = prettyTm . everywhere (mkT beautify) where prettyTm x = error (show x) prettyCase = vcat . map go where - go (x, xs) = prettyTm x <+> operator (pretty "=>") <+> prettyTm xs + go (x, _, xs) = prettyTm x <+> operator (pretty "=>") <+> prettyTm xs prettyLet = vcat . map go where go (x, t, y) = pretty x <+> align (colon <+> nest (- 1) (prettyTm t)) <> line <> pretty x <+> pretty "=" <+> prettyTm y @@ -106,18 +106,18 @@ prettyTm = prettyTm . everywhere (mkT beautify) where beautify (Comp a I0 (System (Map.null -> True)) a0) = toFun "transp" [a, a0] beautify (Lam _ _ (Lam _ _ (System (Map.null -> True)))) = System mempty - 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 (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 a phi u u0) = toFun "outS" [a, phi, u, u0] - - 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] + beautify (Sub a phi u) = toFun "Sub" [a, phi, u] + beautify (Inc _ _ u) = toFun "inS" [u] + beautify (Ouc a phi u u0) = toFun "outS" [a, phi, u, u0] + + beautify (GlueTy _ I1 (Lam _ _ a) _) = 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] beautify x = x toFun s a = foldl (App Ex) (Ref (Bound (T.pack ('.':s)) 0)) a @@ -207,4 +207,4 @@ 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 rng x y) = freeVars rng <> freeVars x <> foldMap (freeVars . snd) y +freeVars (Case rng x y) = freeVars rng <> freeVars x <> foldMap (\(_, _, y) -> freeVars y) y