git.iko.soy/Idris-dev
on master help sign in
Merge pull request #632 from david-christiansen/issue/592
76a3fdaEdwin Brady
src/Core/Evaluate.hs+5−1
compare with master
unifiedsplit
@@ -9,7 +9,7 @@ module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
9 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,
9 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,
10 addDatatype, addCasedef, simplifyCasedef, addOperator,
10 addDatatype, addCasedef, simplifyCasedef, addOperator,
11 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,
11 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,
12− lookupTotal, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
12+ lookupTotal, lookupNameTotal, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
13 Value(..), Quote(..), initEval) where
13 Value(..), Quote(..), initEval) where
14
14
15import Debug.Trace
15import Debug.Trace
@@ -883,6 +883,10 @@ lookupTotal :: Name -> Context -> [Totality]
883lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
883lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
884 where mkt (d, a, t) = t
884 where mkt (d, a, t) = t
885
885
886+lookupNameTotal :: Name -> Context -> [(Name, Totality)]
887+lookupNameTotal n = map (\(n, (_, _, t)) -> (n, t)) . lookupCtxtName n . definitions
888+
889+
886lookupVal :: Name -> Context -> [Value]
890lookupVal :: Name -> Context -> [Value]
887lookupVal n ctxt
891lookupVal n ctxt
888 = do def <- lookupCtxt n (definitions ctxt)
892 = do def <- lookupCtxt n (definitions ctxt)
src/Idris/REPL.hs+12−4
@@ -523,10 +523,17 @@ process h fn (Defn n)
523 showImp (Just i) True c (delab i rhs))
523 showImp (Just i) True c (delab i rhs))
524process h fn (TotCheck n)
524process h fn (TotCheck n)
525 = do i <- getIState
525 = do i <- getIState
526− case lookupTotal n (tt_ctxt i) of
526+ case lookupNameTotal n (tt_ctxt i) of
527− [t] -> iPrintResult (showTotal t i)
527+ [] -> ihPrintError h $ "Unknown operator " ++ show n
528− _ -> do iPrintError ""
528+ ts -> do ist <- getIState
529− return ()
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+
530process h fn (DebugInfo n)
537process h fn (DebugInfo n)
531 = do i <- getIState
538 = do i <- getIState
532 let oi = lookupCtxtName n (idris_optimisation i)
539 let oi = lookupCtxtName n (idris_optimisation i)
@@ -901,6 +908,7 @@ dumpInstance n = do i <- getIState
901 case lookupTy n ctxt of
908 case lookupTy n ctxt of
902 ts -> mapM_ (\t -> iputStrLn $ showImp Nothing imp False (delab i t)) ts
909 ts -> mapM_ (\t -> iputStrLn $ showImp Nothing imp False (delab i t)) ts
903
910
911+showTotal :: Totality -> IState -> String
904showTotal t@(Partial (Other ns)) i
912showTotal t@(Partial (Other ns)) i
905 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
913 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
906showTotal t i = show t
914showTotal t i = show t