a269492 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Disambiguate when printing totality information.

a269492David Christiansen13 years ago

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,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

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

15import Debug.Trace

@@ -883,6 +883,10 @@ lookupTotal :: Name -> Context -> [Totality]

883lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

884 where mkt (d, a, t) = t

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+8−4

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

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

505process h fn (TotCheck n)

506 = do i <- getIState

507− case lookupTotal n (tt_ctxt i) of

507+ case lookupNameTotal n (tt_ctxt i) of

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

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

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

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

509− _ -> do iPrintError ""

511+ ts

510− return ()

512+

513+

511process h fn (DebugInfo n)

514process h fn (DebugInfo n)

512 = do i <- getIState

515 = do i <- getIState

513 let oi = lookupCtxtName n (idris_optimisation i)

516 let oi = lookupCtxtName n (idris_optimisation i)

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

885 case lookupTy n ctxt of

888 case lookupTy n ctxt of

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

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

887

890

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

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

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

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

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

890showTotal t i = show t

894showTotal t i = show t