ae4be75 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Well founded recursion check

ae4be75Edwin Brady15 years ago

src/Core/Evaluate.hs+50−22

compare with master

unifiedsplit

@@ -3,11 +3,12 @@

4module Core.Evaluate(normalise, normaliseC, normaliseAll,

5 simplify, specialise, hnf,

6− Def(..), Accessibility(..),

6+ Def(..), Accessibility(..), Totality(..), PReason(..),

7 Context, initContext, ctxtAlist, uconstraints, next_tvar,

8− addToCtxt, setAccess, addCtxtDef, addTyDecl, addDatatype,

8+ addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,

9 addCasedef, addOperator,

10− lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv, isConName,

10+ lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,

11+ lookupTyEnv, isConName,

11 Value(..)) where

12 Value(..)) where

13import Debug.Trace

14import Debug.Trace

@@ -470,42 +471,63 @@ instance Binary (a -> b) where

470

471

471data Accessibility = Public | Frozen | Hidden

472data Accessibility = Public | Frozen | Hidden

472 deriving (Show, Eq)

473 deriving (Show, Eq)

474+

475+data Totality = Total | Partial PReason

476+ deriving (Show, Eq)

477+

478+data PReason = Other [Name] | Itself | NotCovering | NotPositive

479+ deriving (Show, Eq)

480+

473{-!

481{-!

474deriving instance Binary Accessibility

482deriving instance Binary Accessibility

475!-}

483!-}

476

484

485+{-!

486+deriving instance Binary Totality

487+!-}

488+

489+{-!

490+deriving instance Binary PReason

491+!-}

492+

477data Context = MkContext { uconstraints :: [UConstraint],

493data Context = MkContext { uconstraints :: [UConstraint],

478 next_tvar :: Int,

494 next_tvar :: Int,

479− definitions :: Ctxt (Def, Accessibility) }

495+ definitions :: Ctxt (Def, Accessibility, Totality) }

480

496

481initContext = MkContext [] 0 emptyContext

497initContext = MkContext [] 0 emptyContext

482

498

483ctxtAlist :: Context -> [(Name, Def)]

499ctxtAlist :: Context -> [(Name, Def)]

484−ctxtAlist ctxt = map (\(n, (d, a)) -> (n, d)) $ toAlist (definitions ctxt)

500+ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)

485

501

486veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

502veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

487

503

488addToCtxt :: Name -> Term -> Type -> Context -> Context

504addToCtxt :: Name -> Term -> Type -> Context -> Context

489addToCtxt n tm ty uctxt

505addToCtxt n tm ty uctxt

490 = let ctxt = definitions uctxt

506 = let ctxt = definitions uctxt

491− ctxt' = addDef n (Function ty tm, Public) ctxt in

507+ ctxt' = addDef n (Function ty tm, Public, Total) ctxt in

492 uctxt { definitions = ctxt' }

508 uctxt { definitions = ctxt' }

493

509

494setAccess :: Name -> Accessibility -> Context -> Context

510setAccess :: Name -> Accessibility -> Context -> Context

495setAccess n a uctxt

511setAccess n a uctxt

496 = let ctxt = definitions uctxt

512 = let ctxt = definitions uctxt

497− ctxt' = updateDef n (\ (d, _) -> (d, a)) ctxt in

513+ ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in

514+ uctxt { definitions = ctxt' }

515+

516+setTotal :: Name -> Totality -> Context -> Context

517+setTotal n t uctxt

518+ = let ctxt = definitions uctxt

519+ ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in

498 uctxt { definitions = ctxt' }

520 uctxt { definitions = ctxt' }

499

521

500addCtxtDef :: Name -> Def -> Context -> Context

522addCtxtDef :: Name -> Def -> Context -> Context

501addCtxtDef n d c = let ctxt = definitions c

523addCtxtDef n d c = let ctxt = definitions c

502− ctxt' = addDef n (d, Public) ctxt in

524+ ctxt' = addDef n (d, Public, Total) ctxt in

503 c { definitions = ctxt' }

525 c { definitions = ctxt' }

504

526

505addTyDecl :: Name -> Type -> Context -> Context

527addTyDecl :: Name -> Type -> Context -> Context

506addTyDecl n ty uctxt

528addTyDecl n ty uctxt

507 = let ctxt = definitions uctxt

529 = let ctxt = definitions uctxt

508− ctxt' = addDef n (TyDecl Ref ty, Public) ctxt in

530+ ctxt' = addDef n (TyDecl Ref ty, Public, Total) ctxt in

509 uctxt { definitions = ctxt' }

531 uctxt { definitions = ctxt' }

510

532

511addDatatype :: Datatype Name -> Context -> Context

533addDatatype :: Datatype Name -> Context -> Context

@@ -513,14 +535,14 @@ addDatatype (Data n tag ty cons) uctxt

513 = let ctxt = definitions uctxt

535 = let ctxt = definitions uctxt

514 ty' = normalise uctxt [] ty

536 ty' = normalise uctxt [] ty

515 ctxt' = addCons 0 cons (addDef n

537 ctxt' = addCons 0 cons (addDef n

516− (TyDecl (TCon tag (arity ty')) ty, Public) ctxt) in

538+ (TyDecl (TCon tag (arity ty')) ty, Public, Total) ctxt) in

517 uctxt { definitions = ctxt' }

539 uctxt { definitions = ctxt' }

518 where

540 where

519 addCons tag [] ctxt = ctxt

541 addCons tag [] ctxt = ctxt

520 addCons tag ((n, ty) : cons) ctxt

542 addCons tag ((n, ty) : cons) ctxt

521 = let ty' = normalise uctxt [] ty in

543 = let ty' = normalise uctxt [] ty in

522 addCons (tag+1) cons (addDef n

544 addCons (tag+1) cons (addDef n

523− (TyDecl (DCon tag (arity ty')) ty, Public) ctxt)

545+ (TyDecl (DCon tag (arity ty')) ty, Public, Total) ctxt)

524

546

525addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->

547addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->

526 Type -> Context -> Context

548 Type -> Context -> Context

@@ -532,7 +554,7 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt

532 (CaseDef args sc _, CaseDef args' sc' _) ->

554 (CaseDef args sc _, CaseDef args' sc' _) ->

533 let inl = alwaysInline in

555 let inl = alwaysInline in

534 addDef n (CaseOp inl ty ps args sc args' sc',

556 addDef n (CaseOp inl ty ps args sc args' sc',

535− Public) ctxt in

557+ Public, Total) ctxt in

536 uctxt { definitions = ctxt' }

558 uctxt { definitions = ctxt' }

537 where simpl [] = []

559 where simpl [] = []

538 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

560 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

@@ -540,13 +562,15 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt

540addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

562addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

541addOperator n ty a op uctxt

563addOperator n ty a op uctxt

542 = let ctxt = definitions uctxt

564 = let ctxt = definitions uctxt

543− ctxt' = addDef n (Operator ty a op, Public) ctxt in

565+ ctxt' = addDef n (Operator ty a op, Public, Total) ctxt in

544 uctxt { definitions = ctxt' }

566 uctxt { definitions = ctxt' }

545

567

568+tfst (a, _, _) = a

569+

546lookupTy :: Maybe [String] -> Name -> Context -> [Type]

570lookupTy :: Maybe [String] -> Name -> Context -> [Type]

547lookupTy root n ctxt

571lookupTy root n ctxt

548 = do def <- lookupCtxt root n (definitions ctxt)

572 = do def <- lookupCtxt root n (definitions ctxt)

549− case fst def of

573+ case tfst def of

550 (Function ty _) -> return ty

574 (Function ty _) -> return ty

551 (TyDecl _ ty) -> return ty

575 (TyDecl _ ty) -> return ty

552 (Operator ty _ _) -> return ty

576 (Operator ty _ _) -> return ty

@@ -555,7 +579,7 @@ lookupTy root n ctxt

555isConName :: Maybe [String] -> Name -> Context -> Bool

579isConName :: Maybe [String] -> Name -> Context -> Bool

556isConName root n ctxt

580isConName root n ctxt

557 = or $ do def <- lookupCtxt root n (definitions ctxt)

581 = or $ do def <- lookupCtxt root n (definitions ctxt)

558− case fst def of

582+ case tfst def of

559 (TyDecl (DCon _ _) _) -> return True

583 (TyDecl (DCon _ _) _) -> return True

560 (TyDecl (TCon _ _) _) -> return True

584 (TyDecl (TCon _ _) _) -> return True

561 _ -> return False

585 _ -> return False

@@ -564,26 +588,30 @@ lookupP :: Maybe [String] -> Name -> Context -> [Term]

564lookupP root n ctxt

588lookupP root n ctxt

565 = do def <- lookupCtxt root n (definitions ctxt)

589 = do def <- lookupCtxt root n (definitions ctxt)

566 p <- case def of

590 p <- case def of

567− (Function ty tm, a) -> return (P Ref n ty, a)

591+ (Function ty tm, a, _) -> return (P Ref n ty, a)

568− (TyDecl nt ty, a) -> return (P nt n ty, a)

592+ (TyDecl nt ty, a, _) -> return (P nt n ty, a)

569− (CaseOp _ ty _ _ _ _ _, a) -> return (P Ref n ty, a)

593+ (CaseOp _ ty _ _ _ _ _, a, _) -> return (P Ref n ty, a)

570− (Operator ty _ _, a) -> return (P Ref n ty, a)

594+ (Operator ty _ _, a, _) -> return (P Ref n ty, a)

571 case snd p of

595 case snd p of

572 Hidden -> []

596 Hidden -> []

573 _ -> return (fst p)

597 _ -> return (fst p)

574

598

575lookupDef :: Maybe [String] -> Name -> Context -> [Def]

599lookupDef :: Maybe [String] -> Name -> Context -> [Def]

576−lookupDef root n ctxt = map fst $ lookupCtxt root n (definitions ctxt)

600+lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt)

577

601

578lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context -> [(Def, Accessibility)]

602lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context -> [(Def, Accessibility)]

579lookupDefAcc root n mkpublic ctxt

603lookupDefAcc root n mkpublic ctxt

580 = map mkp $ lookupCtxt root n (definitions ctxt)

604 = map mkp $ lookupCtxt root n (definitions ctxt)

581− where mkp (d, a) = if mkpublic then (d, Public) else (d, a)

605+ where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)

606+

607+lookupTotal :: Name -> Context -> [Totality]

608+lookupTotal n ctxt = map mkt $ lookupCtxt Nothing n (definitions ctxt)

609+ where mkt (d, a, t) = t

582

610

583lookupVal :: Maybe [String] -> Name -> Context -> [Value]

611lookupVal :: Maybe [String] -> Name -> Context -> [Value]

584lookupVal root n ctxt

612lookupVal root n ctxt

585 = do def <- lookupCtxt root n (definitions ctxt)

613 = do def <- lookupCtxt root n (definitions ctxt)

586− case fst def of

614+ case tfst def of

587 (Function _ htm) -> return (veval ctxt [] htm)

615 (Function _ htm) -> return (veval ctxt [] htm)

588 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

616 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

589

617

src/Idris/AbsSyntax.hs+8−1

@@ -81,6 +81,7 @@ data IBCWrite = IBCFix FixDecl

81 | IBCLib String

82 | IBCHeader String

83 | IBCAccess Name Accessibility

84+ | IBCTotal Name Totality

84 | IBCDef Name -- i.e. main context

85 | IBCDef Name -- i.e. main context

85 deriving Show

86 deriving Show

@@ -117,6 +118,12 @@ setAccessibility n a

117 let ctxt = setAccess n a (tt_ctxt i)

118 let ctxt = setAccess n a (tt_ctxt i)

118 put (i { tt_ctxt = ctxt })

119 put (i { tt_ctxt = ctxt })

119

120

121+setTotality :: Name -> Totality -> Idris ()

122+setTotality n a

123+ = do i <- get

124+ let ctxt = setTotal n a (tt_ctxt i)

125+ put (i { tt_ctxt = ctxt })

126+

120addIBC :: IBCWrite -> Idris ()

127addIBC :: IBCWrite -> Idris ()

121addIBC ibc@(IBCDef n)

128addIBC ibc@(IBCDef n)

122 = do i <- get

129 = do i <- get

@@ -349,7 +356,7 @@ impl = Imp False Dynamic

349expl = Exp False Dynamic

356expl = Exp False Dynamic

350constraint = Constraint False Static

357constraint = Constraint False Static

351

358

352−data FnOpt = Inlinable | Partial | Abstract | Private | TCGen

359+data FnOpt = Inlinable | Abstract | Private | TCGen

353 deriving (Show, Eq)

360 deriving (Show, Eq)

354

361

355type FnOpts = [FnOpt]

362type FnOpts = [FnOpt]

src/Idris/Coverage.hs+54

@@ -4,6 +4,8 @@ module Idris.Coverage where

5import Core.TT

6import Core.Evaluate

7+import Core.CaseTree

7import Idris.AbsSyntax

9import Idris.AbsSyntax

8import Idris.Delaborate

10import Idris.Delaborate

@@ -95,3 +97,55 @@ genAll i args = concatMap otherPats (nub args)

96upd p' p = p { getTm = p' }

98upd p' p = p { getTm = p' }

100+-- recursive calls are well-founded if one of their argument positions is

101+-- always decreasing.

102+

103+-- If we encounter a non-total name, we'll fail

104+

105+wellFounded :: IState -> Name -> SC -> Either [Name] Bool

106+wellFounded i n sc = case wff [] sc of

107+ RightOK smaller_args ->

108+ -- is there a number in every list?

109+ -- trace (show (n, smaller_args)) $

110+ case smaller_args of

111+ [] -> Right True

112+ (x : xs) -> let args = foldl intersect x xs in

113+ Right $ not (null args)

114+ LeftErr x -> Left x

115+ where

116+ wff :: [Name] -> SC -> EitherErr [Name] [[Int]]

117+ wff ns (Case n as) = do is <- mapM (wffC ns) as

118+ return $ concat is

119+ where wffC ns (ConCase _ i ns' sc) = wff (ns ++ ns') sc

120+ wffC ns (ConstCase _ sc) = wff ns sc

121+ wffC ns (DefaultCase sc) = wff ns sc

122+ wff ns (STerm t) = argPos ns t

123+ wff ns _ = return []

124+

125+ checkOK n' = case lookupTotal n' (tt_ctxt i) of

126+ [Partial _] -> LeftErr [n']

127+ [Total] -> RightOK ()

128+ x -> RightOK ()

129+-- checkOK n = RightOK ()

130+

131+ argPos ns ap@(App f' a')

132+ | (P _ f _, args) <- unApply ap

133+ = if f == n then

134+ do aa <- argPos ns a'

135+ return $ chkArgs 0 ns args : aa

136+ else do checkOK f

137+ argPos ns a'

138+ argPos ns (App f a) = do f' <- argPos ns f

139+ a' <- argPos ns a

140+ return (f' ++ a')

141+ argPos ns (Bind n (Let t v) sc) = do v' <- argPos ns v

142+ sc' <- argPos ns sc

143+ return (v' ++ sc')

144+ argPos ns (Bind n _ sc) = argPos ns sc

145+ argPos ns _ = return []

146+

147+ chkArgs i ns [] = []

148+ chkArgs i ns (P _ n _ : xs) | n `elem` ns = i : chkArgs (i + 1) ns xs

149+ chkArgs i ns (_ : xs) = chkArgs (i+1) ns xs

150+

151+

src/Idris/ElabDecls.hs+16−1

@@ -128,7 +128,20 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

128 return False)

129 else return False

130 pdef' <- applyOpts pdef

131− let tree = simpleCase tcase pcover pdef

131+ let tree@(CaseDef _ sc _) = simpleCase tcase pcover pdef

132+ ist <- get

133+ let wf = wellFounded ist n sc

134+ tot <- if pcover

135+ then case wf of

136+ Left ns -> do logLvl 2 $ show n ++ " not well founded due to "

137+ ++ show ns

138+ return $ Partial (Other ns)

139+ Right False -> do logLvl 2 $ show n ++ " not well founded"

140+ return $ Partial Itself

141+ Right True -> do logLvl 2 $ show n ++ " well founded"

142+ return Total

143+ else do logLvl 2 $ show n ++ " does not cover all cases"

144+ return $ Partial NotCovering

132 case tree of

145 case tree of

133 CaseDef _ _ [] -> return ()

146 CaseDef _ _ [] -> return ()

134 CaseDef _ _ xs -> mapM_ (\x ->

147 CaseDef _ _ xs -> mapM_ (\x ->

@@ -146,6 +159,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

146 [ty] -> do updateContext (addCasedef n (inlinable opts)

159 [ty] -> do updateContext (addCasedef n (inlinable opts)

147 tcase pcover pdef pdef' ty)

160 tcase pcover pdef pdef' ty)

148 addIBC (IBCDef n)

161 addIBC (IBCDef n)

162+ setTotality n tot

163+ addIBC (IBCTotal n tot)

149 [] -> return ()

164 [] -> return ()

150 where

165 where

151 debind (x, y) = (depat x, depat y)

166 debind (x, y) = (depat x, depat y)

src/Idris/IBC.hs+47−4

@@ -22,7 +22,7 @@ import System.Directory

22import Paths_idris

24ibcVersion :: Word8

25−ibcVersion = 10

25+ibcVersion = 14

27data IBCFile = IBCFile { ver :: Word8,

28 sourcefile :: FilePath,

@@ -40,13 +40,14 @@ data IBCFile = IBCFile { ver :: Word8,

40 ibc_libs :: [String],

41 ibc_hdrs :: [String],

42 ibc_access :: [(Name, Accessibility)],

43+ ibc_total :: [(Name, Totality)],

43 ibc_defs :: [(Name, Def)] }

44 ibc_defs :: [(Name, Def)] }

44{-!

45{-!

45deriving instance Binary IBCFile

46deriving instance Binary IBCFile

46!-}

47!-}

48initIBC :: IBCFile

49initIBC :: IBCFile

49−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

50+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

51loadIBC :: FilePath -> Idris ()

52loadIBC :: FilePath -> Idris ()

52loadIBC fp = do iLOG $ "Loading ibc " ++ fp

53loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -106,6 +107,7 @@ ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

106 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

107 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

107 _ -> fail "IBC write failed"

108 _ -> fail "IBC write failed"

108ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

109ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

110+ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

109

111

110process :: IBCFile -> FilePath -> Idris ()

112process :: IBCFile -> FilePath -> Idris ()

111process i fn

113process i fn

@@ -131,6 +133,7 @@ process i fn

131 pHdrs (ibc_hdrs i)

133 pHdrs (ibc_hdrs i)

132 pDefs (ibc_defs i)

134 pDefs (ibc_defs i)

133 pAccess (ibc_access i)

135 pAccess (ibc_access i)

136+ pTotal (ibc_total i)

134

137

135timestampOlder :: FilePath -> FilePath -> IO ()

138timestampOlder :: FilePath -> FilePath -> IO ()

136timestampOlder src ibc = do srct <- getModificationTime src

139timestampOlder src ibc = do srct <- getModificationTime src

@@ -231,6 +234,12 @@ pAccess ds = mapM_ (\ (n, a) ->

231 putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))

234 putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))

232 ds

235 ds

233

236

237+pTotal :: [(Name, Totality)] -> Idris ()

238+pTotal ds = mapM_ (\ (n, a) ->

239+ do i <- getIState

240+ putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) }))

241+ ds

242+

234----- Generated by 'derive'

243----- Generated by 'derive'

235

244

236

245

@@ -580,8 +589,40 @@ instance Binary Accessibility where

580 2 -> return Hidden

589 2 -> return Hidden

581 _ -> error "Corrupted binary data for Accessibility"

590 _ -> error "Corrupted binary data for Accessibility"

582

591

592+instance Binary PReason where

593+ put x

594+ = case x of

595+ Other x1 -> do putWord8 0

596+ put x1

597+ Itself -> putWord8 1

598+ NotCovering -> putWord8 2

599+ NotPositive -> putWord8 3

600+ get

601+ = do i <- getWord8

602+ case i of

603+ 0 -> do x1 <- get

604+ return (Other x1)

605+ 1 -> return Itself

606+ 2 -> return NotCovering

607+ 3 -> return NotPositive

608+ _ -> error "Corrupted binary data for PReason"

609+

610+instance Binary Totality where

611+ put x

612+ = case x of

613+ Total -> putWord8 0

614+ Partial x1 -> do putWord8 1

615+ put x1

616+ get

617+ = do i <- getWord8

618+ case i of

619+ 0 -> return Total

620+ 1 -> do x1 <- get

621+ return (Partial x1)

622+ _ -> error "Corrupted binary data for Totality"

623+

583instance Binary IBCFile where

624instance Binary IBCFile where

584− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17)

625+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18)

585 = do put x1

626 = do put x1

586 put x2

627 put x2

587 put x3

628 put x3

@@ -599,6 +640,7 @@ instance Binary IBCFile where

599 put x15

640 put x15

600 put x16

641 put x16

601 put x17

642 put x17

643+ put x18

602 get

644 get

603 = do x1 <- get

645 = do x1 <- get

604 if x1 == ibcVersion then

646 if x1 == ibcVersion then

@@ -618,7 +660,8 @@ instance Binary IBCFile where

618 x15 <- get

660 x15 <- get

619 x16 <- get

661 x16 <- get

620 x17 <- get

662 x17 <- get

663+ x18 <- get

621− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17)

664+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18)

622 else return (initIBC { ver = x1 })

665 else return (initIBC { ver = x1 })

623

666

624instance Binary Fixity where

667instance Binary Fixity where

src/Idris/REPL.hs+3

@@ -176,6 +176,9 @@ process fn (Defn n) = do i <- get

176 [] -> return ()

177 [d] -> do iputStrLn "Original definiton:\n"

178 mapM_ (printCase i) d

179+ case lookupTotal n (tt_ctxt i) of

180+ [t] -> iputStrLn (show t)

181+ _ -> return ()

179 where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)

182 where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)

180 liftIO $ putStr " = "

183 liftIO $ putStr " = "

181 liftIO $ putStrLn $ showImp True (delab i rhs)

184 liftIO $ putStrLn $ showImp True (delab i rhs)