diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs index 9ef6993a8..dc85c23e7 100644 --- a/src/Kind/Check.hs +++ b/src/Kind/Check.hs @@ -33,7 +33,7 @@ infer src term dep = debug ("infer: " ++ termShower False term dep) $ go src ter envSusp (Check Nothing arg ftyp_inp dep) return $ ftyp_bod arg otherwise -> do - envLog (Error src (Ref "Function") ftyp (App fun arg) dep) + envLog (Error src (Ref "function") ftyp (App fun arg) dep) envFail go src (Ann chk val typ) dep = do @@ -69,7 +69,7 @@ infer src term dep = debug ("infer: " ++ termShower False term dep) $ go src ter case M.lookup nam book of Just val -> infer src val dep Nothing -> do - envLog (Error src (Ref "Term") (Ref "undefined") (Ref nam) dep) + envLog (Error src (Ref "expression") (Ref "undefined") (Ref nam) dep) envFail go src Set dep = do @@ -369,4 +369,4 @@ doCheckRef nam = do book <- envGetBook case M.lookup nam book of Just val -> doCheck val - Nothing -> envLog (Error Nothing (Ref "Term") (Ref "undefined") (Ref nam) 0) >> envFail + Nothing -> envLog (Error Nothing (Ref "expression") (Ref "undefined") (Ref nam) 0) >> envFail diff --git a/src/Kind/Show.hs b/src/Kind/Show.hs index 029618985..d1a607849 100644 --- a/src/Kind/Show.hs +++ b/src/Kind/Show.hs @@ -180,9 +180,9 @@ infoShow book fill info = case info of ctx' = contextShow book fill ctx dep in return $ concat ["\x1b[1mGOAL\x1b[0m ", nam', " : ", typ', "\n", ctx'] Error src exp det bad dep -> do - let exp' = concat ["- expected: \x1b[32m", termShower True exp dep, "\x1b[0m"] - det' = concat ["- detected: \x1b[31m", termShower True det dep, "\x1b[0m"] - bad' = concat ["- bad_term: \x1b[2m", termShower True bad dep, "\x1b[0m"] + let exp' = concat ["- expected : \x1b[32m", termShower True exp dep, "\x1b[0m"] + det' = concat ["- detected : \x1b[31m", termShower True det dep, "\x1b[0m"] + bad' = concat ["- origin : \x1b[2m", termShower True bad dep, "\x1b[0m"] (file, text) <- case src of Just (Cod (Loc fileName iniLine iniCol) (Loc _ endLine endCol)) -> do canonPath <- resolveToAbsolutePath fileName