From: Anders Mörtberg Date: Fri, 4 Dec 2015 03:52:19 +0000 (-0500) Subject: add a shrink function that can be used to not print all of the output X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0cb4ee67261146536261823e39598ce437b720eb;p=cubicaltt.git add a shrink function that can be used to not print all of the output --- diff --git a/Main.hs b/Main.hs index d448264..166802b 100644 --- a/Main.hs +++ b/Main.hs @@ -82,6 +82,9 @@ main = do (_,_,errs) -> putStrLn $ "Input error: " ++ concat errs ++ "\n" ++ usageInfo usage options +shrink :: String -> String +shrink s = s -- if length s > 1000 then take 1000 s ++ "..." else s + -- Initialize the main loop initLoop :: [Flag] -> FilePath -> History -> IO () initLoop flags f hist = do @@ -94,9 +97,10 @@ initLoop flags f hist = do putStrLn $ "Resolver failed: " ++ err runInputT (settings []) (putHistory hist >> loop flags f [] TC.verboseEnv) Right (adefs,names) -> do - (merr,tenv) <- TC.runDeclss TC.verboseEnv adefs + (merr,tenv) <- + TC.runDeclss TC.verboseEnv (takeWhile (\x -> fst (head x) /= "stop") adefs) case merr of - Just err -> putStrLn $ "Type checking failed: " ++ err + Just err -> putStrLn $ "Type checking failed: " ++ shrink err Nothing -> putStrLn "File loaded." -- Compute names for auto completion runInputT (settings [n | (n,_) <- names]) (putHistory hist >> loop flags f names tenv) @@ -137,7 +141,7 @@ loop flags f names tenv = do let e = mod $ E.eval (TC.env tenv) body -- Let's not crash if the evaluation raises an error: - liftIO $ catch (putStrLn (msg ++ show e)) + liftIO $ catch (putStrLn (msg ++ shrink (show e))) (\e -> putStrLn ("Exception: " ++ show (e :: SomeException))) stop <- liftIO getCurrentTime diff --git a/examples/shortsetquot.ctt b/examples/shortsetquot.ctt index 52b504e..d514a2c 100644 --- a/examples/shortsetquot.ctt +++ b/examples/shortsetquot.ctt @@ -194,9 +194,6 @@ ntrue' : setquot bool R.1 = (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\( - - - -- This is not true: -- test' : Id (P' true').1 (K' true') -- (hdisj_in1 (Id (setquot bool R.1) true' true') (Id (setquot bool R.1) true' false') (<_> true')) =