a269492 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Disambiguate when printing totality information.

Fixes #592.

commita269492a42527f164e449bda43e8c806fba0f3df authorDavid Christiansen <david@davidchristiansen.dk> dateTue 19 Nov 2013, 13:01 (13 years ago) parent9449751

2 files changed+13−5

compare with master

unifiedsplit

src/Core/Evaluate.hs+5−1 src/Idris/REPL.hs+8−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+8−4

@@ -504,10 +504,13 @@ process h fn (Defn n)

504504 showImp (Just i) True c (delab i rhs))

505505process h fn (TotCheck n)

506506 = do i <- getIState

507− case lookupTotal n (tt_ctxt i) of

508− [t] -> iPrintResult (showTotal t i)

509− _ -> do iPrintError ""

510− return ()

507+ case lookupNameTotal n (tt_ctxt i) of

508+ [] -> ihPrintError h $ "Unknown operator " ++ show n

509+ ts -> ihPrintResult h . concat . intersperse "\n" .

510+ map (\(n, t) -> show n ++ " is " ++ showTotal t i) $

511+ ts

512+

513+

511514process h fn (DebugInfo n)

512515 = do i <- getIState

513516 let oi = lookupCtxtName n (idris_optimisation i)

@@ -885,6 +888,7 @@ dumpInstance n = do i <- getIState

885888 case lookupTy n ctxt of

886889 ts -> mapM_ (\t -> iputStrLn $ showImp Nothing imp False (delab i t)) ts

887890

891+showTotal :: Totality -> IState -> String

888892showTotal t@(Partial (Other ns)) i

889893 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)

890894showTotal t i = show t