From 2fdd17b847a3a796cb7bcb849b7efca7c18de965 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Tue, 2 Mar 2021 23:18:29 -0300 Subject: [PATCH] Report unsolved metas & composition for the universe --- intro.tt | 54 ++++++++++++++++++++++---------------------- src/Elab/Eval.hs | 37 +++++++++++++++++++----------- src/Elab/Monad.hs | 12 +++++++--- src/Elab/WiredIn.hs | 13 +++++------ src/Main.hs | 25 +++++++++++++++++--- src/Syntax.hs | 4 +++- src/Syntax/Pretty.hs | 2 +- 7 files changed, 92 insertions(+), 55 deletions(-) diff --git a/intro.tt b/intro.tt index c6bbb82..ca7b001 100644 --- a/intro.tt +++ b/intro.tt @@ -520,47 +520,47 @@ IsoToEquiv {A} {B} iso = lemIso y x0 x1 p0 p1 = let rem0 : Path x0 (g y) - rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i))) + rem0 i = hcomp {A} (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i))) rem1 : Path x1 (g y) - rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i))) + rem1 i = hcomp {A} (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i))) p : Path x0 x1 - p i = comp (\i -> A) (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y)) + p i = hcomp {A} (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y)) 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) - ]) - (inS (g (p0 i))) + fill0 i j = hcomp {A} (\k [ (i = i0) -> t x0 (iand j k) + , (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) ]) - (inS (g (p1 i))) + fill1 i j = hcomp {A} (\k [ (i = i0) -> t x1 (iand j k) + , (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 ]) - (inS (g y)) + fill2 i j = hcomp {A} (\k [ (i = i0) -> rem0 (ior j (inot k)) + , (i = i1) -> rem1 (ior j (inot k)) + , (j = i1) -> g y ]) + (inS (g y)) sq : I -> I -> A - sq i j = comp (\i -> A) (\k [ (i = i0) -> fill0 j (inot k) - , (i = i1) -> fill1 j (inot k) - , (j = i1) -> g y - , (j = i0) -> t (p i) (inot k) ]) - (inS (fill2 i j)) + sq i j = hcomp {A} (\k [ (i = i0) -> fill0 j (inot k) + , (i = i1) -> fill1 j (inot k) + , (j = i1) -> g y + , (j = i0) -> t (p i) (inot k) ]) + (inS (fill2 i j)) 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 - ]) - (inS (f (sq i j))) + sq1 i j = hcomp {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 + ]) + (inS (f (sq i j))) in \i -> (p i, \j -> sq1 i j) fCenter : (y : B) -> fiber f y diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs index bda55f5..7799b9f 100644 --- a/src/Elab/Eval.hs +++ b/src/Elab/Eval.hs @@ -1,7 +1,9 @@ +{-# LANGUAGE BlockArguments #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TupleSections #-} module Elab.Eval where import Control.Monad.Reader @@ -39,7 +41,7 @@ eval :: Term -> ElabM Value eval t = asks (flip eval' t) forceIO :: MonadIO m => Value -> m Value -forceIO mv@(VNe (HMeta (MV _ cell)) args) = do +forceIO mv@(VNe (HMeta (mvCell -> cell)) args) = do solved <- liftIO $ readIORef cell case solved of Just vl -> forceIO $ foldl applProj vl args @@ -66,7 +68,7 @@ zonkIO :: Value -> IO Value zonkIO (VNe hd sp) = do sp' <- traverse zonkSp sp case hd of - HMeta (MV _ cell) -> do + HMeta (mvCell -> cell) -> do solved <- liftIO $ readIORef cell case solved of Just vl -> zonkIO $ foldl applProj vl sp' @@ -366,10 +368,12 @@ isConvertibleTo a b = isConvertibleTo (force a) (force b) where pure id newMeta :: Value -> ElabM Value -newMeta _dom = do +newMeta dom = do + loc <- liftM2 (,) <$> asks currentFile <*> asks currentSpan n <- newName c <- liftIO $ newIORef Nothing - let m = MV (getNameText n) c + let m = MV (getNameText n) c dom (flatten <$> loc) + flatten (x, (y, z)) = (x, y, z) env <- asks getEnv @@ -390,16 +394,23 @@ _nameCounter = unsafePerformIO $ newIORef 0 {-# NOINLINE _nameCounter #-} solveMeta :: MV -> Seq Projection -> Value -> ElabM () -solveMeta m@(MV _ cell) sp rhs = do +solveMeta m@(mvCell -> cell) sp rhs = do env <- ask - names <- checkSpine Set.empty sp - checkScope (Set.fromList names) rhs - `withNote` hsep [prettyTm (quote (VNe (HMeta m) sp)), pretty '≡', prettyTm (quote rhs)] - let tm = quote rhs - lam = eval' env $ foldr (Lam Ex) tm names - liftIO . atomicModifyIORef' cell $ \case - Just _ -> error "filled cell in solvedMeta" - Nothing -> (Just lam, ()) + names <- tryElab $ checkSpine Set.empty sp + case names of + Right names -> do + checkScope (Set.fromList names) rhs + `withNote` hsep [prettyTm (quote (VNe (HMeta m) sp)), pretty '≡', prettyTm (quote rhs)] + let tm = quote rhs + lam = eval' env $ foldr (Lam Ex) tm names + liftIO . atomicModifyIORef' cell $ \case + Just _ -> error "filled cell in solvedMeta" + Nothing -> (Just lam, ()) + Left (_ :: SpineProjection) -> do + liftIO . atomicModifyIORef' (unsolvedMetas env) $ \x -> (, ()) $ + case Map.lookup m x of + Just qs -> Map.insert m ((sp, rhs):qs) x + Nothing -> Map.insert m [(sp, rhs)] x checkScope :: Set Name -> Value -> ElabM () checkScope scope (VNe h sp) = diff --git a/src/Elab/Monad.hs b/src/Elab/Monad.hs index 8e645da..69b635d 100644 --- a/src/Elab/Monad.hs +++ b/src/Elab/Monad.hs @@ -18,25 +18,31 @@ import Data.Typeable import qualified Presyntax.Presyntax as P import Syntax +import Data.IORef +import Data.Sequence (Seq) data ElabEnv = ElabEnv { getEnv :: Map Name (NFType, Value) , nameMap :: Map Text Name - , pingPong :: Int + , pingPong :: {-# UNPACK #-} !Int , commHook :: Value -> IO () , currentSpan :: Maybe (P.Posn, P.Posn) + , currentFile :: Maybe Text + , whereBound :: Map Name (P.Posn, P.Posn) , definedNames :: Set Name + + , unsolvedMetas :: {-# UNPACK #-} !(IORef (Map MV [(Seq Projection, Value)])) } newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a } deriving (Functor, Applicative, Monad, MonadReader ElabEnv, MonadIO) via ReaderT ElabEnv IO -emptyEnv :: ElabEnv -emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing mempty mempty +emptyEnv :: IO ElabEnv +emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing Nothing mempty mempty <$> newIORef mempty 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 5a76d90..a625312 100644 --- a/src/Elab/WiredIn.hs +++ b/src/Elab/WiredIn.hs @@ -228,11 +228,9 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = case force $ a @@ VVar (Bound (T.pack "neutral composition") 0) 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 = case force (a @@ i) of - VPi _ _ (Closure _ r) -> r - x -> error $ "not pi?? " ++ show x + plic i = let VPi p _ _ = force (a @@ i) in p + dom i = let VPi _ d _ = force (a @@ i) in d + rng i = let VPi _ _ (Closure _ r) = force (a @@ i) in r y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (dom VI0) phi y) i ybar i y = y' (inot i) y @@ -300,12 +298,13 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = (fun (const (base VI1 @@ VItIsOne))) (phi VI1 `ior` psi) (system \j _u -> mkVSystem (Map.fromList [ (phi VI1, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VItIsOne)) alpha j) - , (psi, a VI1)])) + , (psi, a VI1)])) a1' b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1 in b1 - VType -> VGlueTy a0 phi (system \_ _ -> u @@ VI1 @@ VItIsOne) (system \_ _ -> makeEquiv (\j -> (u @@ inot j))) + VType -> VGlueTy a0 phi (system \_ _ -> mkVSystem (Map.fromList [(phi, u @@ VI1 @@ VItIsOne)])) + (system \_ _ -> mkVSystem (Map.fromList [(phi, makeEquiv (\j -> (u @@ inot j)))])) -- fibrancy structure of the booleans is trivial VBool{} -> a0 diff --git a/src/Main.hs b/src/Main.hs index 3f97c60..f19a09b 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -39,6 +39,8 @@ import qualified Data.Set as Set import Data.Maybe import Presyntax.Tokens import Debug.Trace +import Data.IORef +import Data.Sequence (Seq) main :: IO () main = do @@ -50,7 +52,7 @@ main = do Check files verbose -> do env <- checkFiles files when verbose $ dumpEnv env - Repl -> enterReplIn emptyEnv + Repl -> enterReplIn =<< emptyEnv enterReplIn :: ElabEnv -> IO () enterReplIn env = runInputT defaultSettings (loop env') where @@ -75,7 +77,7 @@ enterReplIn env = runInputT defaultSettings (loop env') where loop env checkFiles :: [String] -> IO ElabEnv -checkFiles files = runElab (go files ask) emptyEnv where +checkFiles files = runElab (go files ask) =<< emptyEnv where go [] k = do env <- ask for_ (Map.toList (nameMap env)) \case @@ -86,13 +88,18 @@ checkFiles files = runElab (go files ask) emptyEnv where pos = fromJust (Map.lookup v (whereBound env)) in withSpan (fst pos) (snd pos) $ throwElab $ DeclaredUndefined v _ -> pure () + + metas <- liftIO $ readIORef (unsolvedMetas env) + unless (Map.null metas) $ do + liftIO $ reportUnsolved metas + k go (x:xs) k = do code <- liftIO $ Bsl.readFile x case runAlex (code <> Bsl.singleton 10) parseProg of Left e -> liftIO $ print e *> error (show e) Right prog -> - checkProgram prog (go xs k) + local (\e -> e { currentFile = Just (T.pack x) }) (checkProgram prog (go xs k)) `catchElab` \e -> liftIO $ displayAndDie (T.decodeUtf8 (Bsl.toStrict code)) (e :: SomeException) dumpEnv :: ElabEnv -> IO () @@ -160,6 +167,18 @@ displayExceptions lines = putStrLn $ "Name declared but not defined: " ++ show (pretty n) ] +reportUnsolved :: Foldable t => Map.Map MV (t (Seq Projection, Value)) -> IO () +reportUnsolved metas = do + for_ (Map.toList metas) \(m, p) -> do + case mvSpan m of + Just (f, s, e) -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f) + Nothing -> pure () + T.putStrLn . render $ + "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> prettyTm (quote (mvType m)) <+> "should satisfy:" + for_ p \p -> + T.putStrLn . render $ indent 2 $ prettyTm (quote (VNe (HMeta m) (fst p))) <+> pretty '≡' <+> prettyTm (quote (snd p)) + + displayExceptions' :: Exception e => Text -> e -> IO () displayExceptions' lines e = displayAndDie lines e `catch` \(_ :: ExitCode) -> pure () diff --git a/src/Syntax.hs b/src/Syntax.hs index b7c12e3..7905454 100644 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -14,7 +14,7 @@ import Data.Text (Text) import Data.Set (Set) import Data.Data -import Presyntax.Presyntax (Plicity(..)) +import Presyntax.Presyntax (Plicity(..), Posn) data WiredIn = WiType @@ -109,6 +109,8 @@ data Term data MV = MV { mvName :: Text , mvCell :: {-# UNPACK #-} !(IORef (Maybe Value)) + , mvType :: NFType + , mvSpan :: Maybe (Text, Posn, Posn) } instance Eq MV where diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs index b2e736e..cbad306 100644 --- a/src/Syntax/Pretty.hs +++ b/src/Syntax/Pretty.hs @@ -88,7 +88,7 @@ prettyTm = prettyTm . everywhere (mkT beautify) where beautify (Comp a phi u a0) = toFun "comp" [a, phi, u, a0] beautify (Sub a phi u) = toFun "Sub" [a, phi, u] beautify (Inc _ _ u) = toFun "inS" [u] - beautify (Ouc _ phi u0 u) = toFun "outS" [u] + beautify (Ouc _ _ _ u) = toFun "outS" [u] beautify (GlueTy a I1 _ _) = a beautify (GlueTy a b c d) = toFun "Glue" [a,b,c,d]