e32e899 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Totality checking for functions defined in Elab scripts

e32e899David Raymond Christiansen12 years ago

src/Idris/Core/CaseTree.hs+3−4

compare with master

unifiedsplit

@@ -136,10 +136,9 @@ namesUsed sc = nub $ nu' [] sc where

136 nut ps (Bind n b sc) = nut (n:ps) sc

137 nut ps _ = []

138

139−-- Return all called functions, and which arguments are used in each argument position

139+-- | Return all called functions, and which arguments are used

140+-- in each argument position for the call, in order to help reduce

140−-- for the call, in order to help reduce compilation time, and trace all unused

141+-- compilation time, and trace all unused arguments

141−-- arguments

142−

143findCalls :: SC -> [Name] -> [(Name, [[Name]])]

142findCalls :: SC -> [Name] -> [(Name, [[Name]])]

144findCalls sc topargs = nub $ nu' topargs sc where

143findCalls sc topargs = nub $ nu' topargs sc where

145 nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)

144 nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)

src/Idris/Core/Evaluate.hs+7−5

@@ -887,11 +887,13 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

887 cdef = CaseDefs (args_tot, sc_tot)

888 (args_ct, sc_ct)

889 (args_inl, sc_inl)

890− (args_rt, sc_rt) in

890+ (args_rt, sc_rt)

891− addDef n (CaseOp (ci { case_inlinable = inlc })

891+ op = (CaseOp (ci { case_inlinable = inlc })

892− ty argtys ps_in ps_tot cdef,

892+ ty argtys ps_in ps_tot cdef,

893− access, Unchecked, EmptyMI) ctxt in

893+ access, Unchecked, EmptyMI)

894+ in addDef n op ctxt

895+ other -> error ("Error adding case def: " ++ show other)

894− uctxt { definitions = ctxt' }

896+ in uctxt { definitions = ctxt' }

895

897

896-- simplify a definition for totality checking

898-- simplify a definition for totality checking

897simplifyCasedef :: Name -> ErasureInfo -> Context -> Context

899simplifyCasedef :: Name -> ErasureInfo -> Context -> Context

src/Idris/Coverage.hs+52−7

@@ -1,5 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

2−

2+{-| The coverage and totality checkers for Idris are in this module.

3+-}

3module Idris.Coverage where

4module Idris.Coverage where

5import Idris.Core.TT

6import Idris.Core.TT

@@ -120,6 +121,52 @@ genClauses fc n xs given

120 as' <- mkArg as

121 as' <- mkArg as

121 return (a':as')

122 return (a':as')

122

123

124+-- | Does this error result rule out a case as valid when coverage checking?

125+validCoverageCase :: Context -> Err -> Bool

126+validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)

127+ = let topx' = normalise ctxt [] topx

128+ topy' = normalise ctxt [] topy in

129+ not (sameFam topx' topy' || not (validCoverageCase ctxt e))

130+ where sameFam topx topy

131+ = case (unApply topx, unApply topy) of

132+ ((P _ x _, _), (P _ y _, _)) -> x == y

133+ _ -> False

134+validCoverageCase ctxt (CantConvert _ _ _) = False

135+validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e

136+validCoverageCase ctxt (Elaborating _ _ e) = validCoverageCase ctxt e

137+validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e

138+validCoverageCase ctxt _ = True

139+

140+-- | Check whether an error is recoverable in the sense needed for

141+-- coverage checking.

142+recoverableCoverage :: Context -> Err -> Bool

143+recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)

144+ = let topx' = normalise ctxt [] topx

145+ topy' = normalise ctxt [] topy in

146+ checkRec topx' topy'

147+ where -- different notion of recoverable than in unification, since we

148+ -- have no metavars -- just looking to see if a constructor is failing

149+ -- to unify with a function that may be reduced later

150+ checkRec (App f a) p@(P _ _ _) = checkRec f p

151+ checkRec p@(P _ _ _) (App f a) = checkRec p f

152+ checkRec fa@(App _ _) fa'@(App _ _)

153+ | (f, as) <- unApply fa,

154+ (f', as') <- unApply fa'

155+ = if (length as /= length as')

156+ then checkRec f f'

157+ else checkRec f f' && and (zipWith checkRec as as')

158+ checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt

159+ checkRec _ _ = False

160+

161+ ntRec x y | Ref <- x = True

162+ | Ref <- y = True

163+ | (Bound, Bound) <- (x, y) = True

164+ | otherwise = False -- name is different, unrecoverable

165+recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e

166+recoverableCoverage ctxt (Elaborating _ _ e) = recoverableCoverage ctxt e

167+recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e

168+recoverableCoverage _ _ = False

169+

123-- FIXME: Just look for which one is the deepest, then generate all

170-- FIXME: Just look for which one is the deepest, then generate all

124-- possibilities up to that depth.

171-- possibilities up to that depth.

125-- This and below issues for this function are tracked as Issue #1741 on the issue tracker.

172-- This and below issues for this function are tracked as Issue #1741 on the issue tracker.

@@ -350,10 +397,9 @@ calcProd i fc topn pats

350 _ -> False

397 _ -> False

351 cotype nt n ty = False

398 cotype nt n ty = False

352

399

353−-- Calculate the totality of a function from its patterns.

400+-- | Calculate the totality of a function from its patterns.

354-- Either follow the size change graph (if inductive) or check for

401-- Either follow the size change graph (if inductive) or check for

355-- productivity (if coinductive)

402-- productivity (if coinductive)

356−

357calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

403calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

358calcTotality fc n pats

404calcTotality fc n pats

359 = do i <- getIState

405 = do i <- getIState

@@ -450,17 +496,16 @@ checkDeclTotality (fc, n)

450 return t

496 return t

451

497

452

498

453−-- Calculate the size change graph for this definition

499+-- | Calculate the size change graph for this definition

454−

500+--

455-- SCG for a function f consists of a list of:

501-- SCG for a function f consists of a list of:

456-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])

502-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])

457−

503+--

458-- where g is a function called

504-- where g is a function called

459-- a1 ... an are the arguments of f in positions 1..n of g

505-- a1 ... an are the arguments of f in positions 1..n of g

460-- sizechange1 ... sizechange2 is how their size has changed wrt the input

506-- sizechange1 ... sizechange2 is how their size has changed wrt the input

461-- to f

507-- to f

462-- Nothing, if the argument is unrelated to the input

508-- Nothing, if the argument is unrelated to the input

463−

464buildSCG :: (FC, Name) -> Idris ()

509buildSCG :: (FC, Name) -> Idris ()

465buildSCG (_, n) = do

510buildSCG (_, n) = do

466 ist <- getIState

511 ist <- getIState

src/Idris/Elab/Clause.hs+9−52

@@ -455,58 +455,15 @@ checkPossible info fc tcgen fname lhs_in

455 (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of

456 OK (ElabResult lhs' _ _ ctxt' newDecls, _) ->

457 do setContext ctxt'

458− processTacticDecls newDecls

458+ processTacticDecls info newDecls

459 let lhs_tm = orderPats (getInferTerm lhs')

460 case recheck ctxt [] (forget lhs_tm) lhs_tm of

461 OK _ -> return True

462 err -> return False

463 -- if it's a recoverable error, the case may become possible

464− Error err -> if tcgen then return (recoverable ctxt err)

464+ Error err -> if tcgen then return (recoverableCoverage ctxt err)

465− else return (validCase ctxt err ||

465+ else return (validCoverageCase ctxt err ||

466− recoverable ctxt err)

466+ recoverableCoverage ctxt err)

467− where validCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)

468− = let topx' = normalise ctxt [] topx

469− topy' = normalise ctxt [] topy in

470− not (sameFam topx' topy' || not (validCase ctxt e))

471− validCase ctxt (CantConvert _ _ _) = False

472− validCase ctxt (At _ e) = validCase ctxt e

473− validCase ctxt (Elaborating _ _ e) = validCase ctxt e

474− validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e

475− validCase ctxt _ = True

476−

477− recoverable ctxt (CantUnify r (topx, _) (topy, _) e _ _)

478− = let topx' = normalise ctxt [] topx

479− topy' = normalise ctxt [] topy in

480− checkRec topx' topy'

481− recoverable ctxt (At _ e) = recoverable ctxt e

482− recoverable ctxt (Elaborating _ _ e) = recoverable ctxt e

483− recoverable ctxt (ElaboratingArg _ _ _ e) = recoverable ctxt e

484− recoverable _ _ = False

485−

486− sameFam topx topy

487− = case (unApply topx, unApply topy) of

488− ((P _ x _, _), (P _ y _, _)) -> x == y

489− _ -> False

490−

491− -- different notion of recoverable than in unification, since we

492− -- have no metavars -- just looking to see if a constructor is failing

493− -- to unify with a function that may be reduced later

494−

495− checkRec (App f a) p@(P _ _ _) = checkRec f p

496− checkRec p@(P _ _ _) (App f a) = checkRec p f

497− checkRec fa@(App _ _) fa'@(App _ _)

498− | (f, as) <- unApply fa,

499− (f', as') <- unApply fa'

500− = if (length as /= length as')

501− then checkRec f f'

502− else checkRec f f' && and (zipWith checkRec as as')

503− checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt

504− checkRec _ _ = False

505−

506− ntRec x y | Ref <- x = True

507− | Ref <- y = True

508− | (Bound, Bound) <- (x, y) = True

509− | otherwise = False -- name is different, unrecoverable

510

467

511propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

468propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

512propagateParams i ps t tm@(PApp _ (PRef fc n) args)

469propagateParams i ps t tm@(PApp _ (PRef fc n) args)

@@ -587,7 +544,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

587 inj <- get_inj

544 inj <- get_inj

588 return (res, probs, inj))

545 return (res, probs, inj))

589 setContext ctxt'

546 setContext ctxt'

590− processTacticDecls newDecls

547+ processTacticDecls info newDecls

591 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

548 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

592

549

593 let lhs_tm = orderPats (getInferTerm lhs')

550 let lhs_tm = orderPats (getInferTerm lhs')

@@ -672,7 +629,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

672 probs <- get_probs

629 probs <- get_probs

673 return (tm, ds, is, probs, ctxt', newDecls))

630 return (tm, ds, is, probs, ctxt', newDecls))

674 setContext ctxt'

631 setContext ctxt'

675− processTacticDecls newDecls

632+ processTacticDecls info newDecls

676 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

633 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

677

634

678 logLvl 5 "DONE CHECK"

635 logLvl 5 "DONE CHECK"

@@ -820,7 +777,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

820 (errAt "left hand side of with in " fname

777 (errAt "left hand side of with in " fname

821 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

778 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

822 setContext ctxt'

779 setContext ctxt'

823− processTacticDecls newDecls

780+ processTacticDecls info newDecls

824 let lhs_tm = orderPats (getInferTerm lhs')

781 let lhs_tm = orderPats (getInferTerm lhs')

825 let lhs_ty = getInferType lhs'

782 let lhs_ty = getInferType lhs'

826 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

783 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

@@ -844,7 +801,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

844 tt <- get_term

801 tt <- get_term

845 return (tt, d, is, ctxt', newDecls))

802 return (tt, d, is, ctxt', newDecls))

846 setContext ctxt'

803 setContext ctxt'

847− processTacticDecls newDecls

804+ processTacticDecls info newDecls

848 def' <- checkDef fc iderr defer

805 def' <- checkDef fc iderr defer

849 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

806 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

850 addDeferred def''

807 addDeferred def''

@@ -939,7 +896,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

939 tt <- get_term

896 tt <- get_term

940 return (tt, d, is, ctxt', newDecls))

897 return (tt, d, is, ctxt', newDecls))

941 setContext ctxt'

898 setContext ctxt'

942− processTacticDecls newDecls

899+ processTacticDecls info newDecls

943

900

944 def' <- checkDef fc iderr defer

901 def' <- checkDef fc iderr defer

945 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

902 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

src/Idris/Elab/Instance.hs+1−1

@@ -180,7 +180,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

180 tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

181 (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

182 setContext ctxt'

183− processTacticDecls newDecls

183+ processTacticDecls info newDecls

184 ctxt <- getContext

185 (cty, _) <- recheckC fc id [] tyT

186 let nty = normalise ctxt [] cty

src/Idris/Elab/Transform.hs+2−2

@@ -58,7 +58,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

58 (erun fc (buildTC i info ELHS [] (sUN "transform")

59 (infTerm lhs)))

60 setContext ctxt'

61− processTacticDecls newDecls

61+ processTacticDecls info newDecls

62 let lhs_tm = orderPats (getInferTerm lhs')

63 let lhs_ty = getInferType lhs'

64 let newargs = pvars i lhs_tm

@@ -78,7 +78,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

78 let (rhs', defer) = runState (collectDeferred Nothing tt) []

79 return (rhs', defer, ctxt', newDecls))

80 setContext ctxt'

81− processTacticDecls newDecls

81+ processTacticDecls info newDecls

83 (crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'

84 let crhs_tm = renamepats pnames crhs_tm_in

src/Idris/Elab/Type.hs+1−1

@@ -70,7 +70,7 @@ buildType info syn fc opts n ty' = do

70 tclift $ elaborate ctxt n (TType (UVal 0)) initEState

71 (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

72 setContext ctxt'

73− processTacticDecls newDecls

73+ processTacticDecls info newDecls

75 let tyT = patToImp tyT'

src/Idris/Elab/Value.hs+1−1

@@ -69,7 +69,7 @@ elabValBind info aspat norm tm_in

70 -- Extend the context with new definitions created

71 setContext ctxt'

72− processTacticDecls newDecls

72+ processTacticDecls info newDecls

74 let vtm = orderPats (getInferTerm tm')

src/Idris/ElabTerm.hs+107−20

@@ -10,12 +10,13 @@ import Idris.Error

10import Idris.ProofSearch

11import Idris.Output (pshow)

13−import Idris.Core.CaseTree (SC, SC'(STerm))

13+import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)

14import Idris.Core.Elaborate hiding (Tactic(..))

15import Idris.Core.TT

16import Idris.Core.Evaluate

17import Idris.Core.Unify

18import Idris.Core.Typecheck (check, recheck)

19+import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)

19import Idris.ErrReverse (errReverse)

20import Idris.ErrReverse (errReverse)

20import Idris.ElabQuasiquote (extractUnquotes)

21import Idris.ElabQuasiquote (extractUnquotes)

21import Idris.Elab.Utils

22import Idris.Elab.Utils

@@ -49,24 +50,6 @@ data ElabResult =

49 -- ^ Meta-info about the new type declarations

50 -- ^ Meta-info about the new type declarations

50 }

51 }

52−processTacticDecls :: [RDeclInstructions] -> Idris ()

53−processTacticDecls info =

54− forM_ info $ \case

55− RTyDeclInstrs n fc impls ty ->

56− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

57− logLvl 3 $ " It has impls " ++ show impls

58− updateIState $ \i -> i { idris_implicits =

59− addDef n impls (idris_implicits i) }

60− addIBC (IBCImp n)

61− ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]

62− addIBC (IBCDef n)

63− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

64− addDeferred ds'

65− RClausesInstrs n cs ->

66− do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n

67− solveDeferred n

68− updateIState $ \i -> i { idris_patdefs = addDef n (cs, []) $ idris_patdefs i } -- TODO: missing clauses

69− addIBC (IBCDef n)

71-- Using the elaborator, convert a term in raw syntax to a fully

54-- Using the elaborator, convert a term in raw syntax to a fully

72-- elaborated, typechecked term.

55-- elaborated, typechecked term.

@@ -1628,7 +1611,7 @@ runTactical fc env tm = do tm' <- eval tm

1628 addCasedef n (const [])

1611 addCasedef n (const [])

1629 info False (STerm Erased)

1612 info False (STerm Erased)

1630 True False -- TODO what are these?

1613 True False -- TODO what are these?

1631− [] [] -- TODO argument types, inaccessible types

1614+ (map snd $ getArgTys ty) [] -- TODO inaccessible types

1632 clauses'

1615 clauses'

1633 clauses''

1616 clauses''

1634 clauses''

1617 clauses''

@@ -2088,3 +2071,107 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2088 parts -> ReflectionError errorparts e

2071 parts -> ReflectionError errorparts e

2089

2072

2090solveAll = try (do solve; solveAll) (return ())

2073solveAll = try (do solve; solveAll) (return ())

2074+

2075+-- | Do the left-over work after creating declarations in reflected

2076+-- elaborator scripts

2077+processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()

2078+processTacticDecls info steps =

2079+ -- The order of steps is important: type declarations might

2080+ -- establish metavars that later function bodies resolve.

2081+ forM_ (reverse steps) $ \case

2082+ RTyDeclInstrs n fc impls ty ->

2083+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

2084+ logLvl 3 $ " It has impls " ++ show impls

2085+ updateIState $ \i -> i { idris_implicits =

2086+ addDef n impls (idris_implicits i) }

2087+ addIBC (IBCImp n)

2088+ ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]

2089+ addIBC (IBCDef n)

2090+ ctxt <- getContext

2091+ case lookupDef n ctxt of

2092+ (TyDecl _ _ : _) ->

2093+ -- If the function isn't defined at the end of the elab script,

2094+ -- then it must be added as a metavariable. This needs guarding

2095+ -- to prevent overwriting case defs with a metavar, if the case

2096+ -- defs come after the type decl in the same script!

2097+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

2098+ in addDeferred ds'

2099+ _ -> return ()

2100+ RClausesInstrs n cs ->

2101+ do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n

2102+ solveDeferred n

2103+ let lhss = map (\(_, lhs, _) -> lhs) cs

2104+ let fc = fileFC "elab_reflected"

2105+ pmissing <-

2106+ do ist <- getIState

2107+ possible <- genClauses fc n lhss

2108+ (map (\lhs ->

2109+ delab' ist lhs True True) lhss)

2110+ missing <- filterM (checkPossible n) possible

2111+ return (filter (noMatch ist lhss) missing)

2112+ let tot = if null pmissing

2113+ then Unchecked -- still need to check recursive calls

2114+ else Partial NotCovering -- missing cases implies not total

2115+ setTotality n tot

2116+ updateIState $ \i -> i { idris_patdefs =

2117+ addDef n (cs, pmissing) $ idris_patdefs i }

2118+ addIBC (IBCDef n)

2119+

2120+ ctxt <- getContext

2121+ case lookupDefExact n ctxt of

2122+ Just (CaseOp _ _ _ _ _ cd) ->

2123+ -- Here, we populate the call graph with a list of things

2124+ -- we refer to, so that if they aren't total, the whole

2125+ -- thing won't be.

2126+ let (scargs, sc) = cases_compiletime cd

2127+ (scargs', sc') = cases_runtime cd

2128+ calls = findCalls sc' scargs

2129+ used = findUsedArgs sc' scargs'

2130+ cg = CGInfo scargs' calls [] used []

2131+ in do logLvl 2 $ "Called names in reflected elab: " ++ show cg

2132+ addToCG n cg

2133+ addToCalledG n (nub (map fst calls))

2134+ addIBC $ IBCCG n

2135+ Just _ -> return () -- TODO throw internal error

2136+ Nothing -> return ()

2137+

2138+ -- checkDeclTotality requires that the call graph be present

2139+ -- before calling it.

2140+ -- TODO: reduce code duplication with Idris.Elab.Clause

2141+ buildSCG (fc, n)

2142+

2143+ -- Actually run the totality checker. In the main clause

2144+ -- elaborator, this is deferred until after. Here, we run it

2145+ -- now to get totality information as early as possible.

2146+ tot' <- checkDeclTotality (fc, n)

2147+ setTotality n tot'

2148+ when (tot' /= Unchecked) $ addIBC (IBCTotal n tot')

2149+ where

2150+ -- TODO: see if the code duplication with Idris.Elab.Clause can be

2151+ -- reduced or eliminated.

2152+ checkPossible :: Name -> PTerm -> Idris Bool

2153+ checkPossible fname lhs_in =

2154+ do ctxt <- getContext

2155+ ist <- getIState

2156+ let lhs = addImplPat ist lhs_in

2157+ let fc = fileFC "elab_reflected_totality"

2158+ let tcgen = False -- TODO: later we may support dictionary generation

2159+ case elaborate ctxt (sMN 0 "refPatLHS") infP initEState

2160+ (erun fc (buildTC ist info ELHS [] fname (infTerm lhs))) of

2161+ OK (ElabResult lhs' _ _ _ _, _) ->

2162+ do -- not recursively calling here, because we don't

2163+ -- want to run infinitely many times

2164+ let lhs_tm = orderPats (getInferTerm lhs')

2165+ case recheck ctxt [] (forget lhs_tm) lhs_tm of

2166+ OK _ -> return True

2167+ err -> return False

2168+ -- if it's a recoverable error, the case may become possible

2169+ Error err -> if tcgen then return (recoverableCoverage ctxt err)

2170+ else return (validCoverageCase ctxt err ||

2171+ recoverableCoverage ctxt err)

2172+

2173+

2174+ -- TODO: Attempt to reduce/eliminate code duplication with Idris.Elab.Clause

2175+ noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of

2176+ Right _ -> False

2177+ Left _ -> True) cs

src/Idris/Reflection.hs+1−1

@@ -2,7 +2,7 @@

2quoters and unquoters along with some supporting datatypes.

3-}

4{-# LANGUAGE PatternGuards #-}

5−{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

5+{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}

6module Idris.Reflection where

8import Control.Monad (liftM, liftM2)