git.iko.soy/Idris-dev
on master help sign in
Merge pull request #632 from david-christiansen/issue/592

Show totality info for overloaded definitions, in amazing color!

commit76a3fda8ff74320c9552154a20685b780e52f95c authorEdwin Brady <edwin.brady@gmail.com> dateTue 19 Nov 2013, 05:38 (13 years ago) parent81089511c0b43f
2 files changed+17−5
compare with master
unifiedsplit
src/Core/Evaluate.hs+5−1 src/Idris/REPL.hs+12−4
src/Core/Evaluate.hs+5−1
@@ -9,7 +9,7 @@ module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
99 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,
1010 addDatatype, addCasedef, simplifyCasedef, addOperator,
1111 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,
12− lookupTotal, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
12+ lookupTotal, lookupNameTotal, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
1313 Value(..), Quote(..), initEval) where
1414
1515import Debug.Trace
@@ -883,6 +883,10 @@ lookupTotal :: Name -> Context -> [Totality]
883883lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
884884 where mkt (d, a, t) = t
885885
886+lookupNameTotal :: Name -> Context -> [(Name, Totality)]
887+lookupNameTotal n = map (\(n, (_, _, t)) -> (n, t)) . lookupCtxtName n . definitions
888+
889+
886890lookupVal :: Name -> Context -> [Value]
887891lookupVal n ctxt
888892 = do def <- lookupCtxt n (definitions ctxt)
src/Idris/REPL.hs+12−4
@@ -523,10 +523,17 @@ process h fn (Defn n)
523523 showImp (Just i) True c (delab i rhs))
524524process h fn (TotCheck n)
525525 = do i <- getIState
526− case lookupTotal n (tt_ctxt i) of
527− [t] -> iPrintResult (showTotal t i)
528− _ -> do iPrintError ""
529− return ()
526+ case lookupNameTotal n (tt_ctxt i) of
527+ [] -> ihPrintError h $ "Unknown operator " ++ show n
528+ ts -> do ist <- getIState
529+ c <- colourise
530+ imp <- impShow
531+ let showN = showName (Just ist) [] imp c
532+ ihPrintResult h . concat . intersperse "\n" .
533+ map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
534+ ts
535+
536+
530537process h fn (DebugInfo n)
531538 = do i <- getIState
532539 let oi = lookupCtxtName n (idris_optimisation i)
@@ -901,6 +908,7 @@ dumpInstance n = do i <- getIState
901908 case lookupTy n ctxt of
902909 ts -> mapM_ (\t -> iputStrLn $ showImp Nothing imp False (delab i t)) ts
903910
911+showTotal :: Totality -> IState -> String
904912showTotal t@(Partial (Other ns)) i
905913 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
906914showTotal t i = show t