0c953a9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2323 from david-christiansen/wip/tactical

0c953a9David Christiansen11 years ago

libs/prelude/Language/Reflection/Elab.idr+18

compare with master

unifiedsplit

@@ -85,6 +85,8 @@ data Elab : Type -> Type where

85 prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))

86 prim__LookupDatatype : TTName -> Elab (List Datatype)

88+ prim__Check : Raw -> Elab (TT, TT)

89+

88 prim__SourceLocation : Elab SourceLocation

90 prim__SourceLocation : Elab SourceLocation

90 prim__Forget : TT -> Elab Raw

92 prim__Forget : TT -> Elab Raw

@@ -113,6 +115,7 @@ data Elab : Type -> Type where

113 prim__AddInstance : TTName -> TTName -> Elab ()

115 prim__AddInstance : TTName -> TTName -> Elab ()

114

116

115 prim__ResolveTC : TTName -> Elab ()

117 prim__ResolveTC : TTName -> Elab ()

118+ prim__Search : Int -> List TTName -> Elab ()

116 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

119 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

117

120

118 prim__Debug : {a : Type} -> Maybe String -> Elab a

121 prim__Debug : {a : Type} -> Maybe String -> Elab a

@@ -186,6 +189,10 @@ namespace Tactics

186 [] => fail [TextPart "No datatype named", NamePart n]

189 [] => fail [TextPart "No datatype named", NamePart n]

187 xs => fail [TextPart "More than one datatype named", NamePart n]

190 xs => fail [TextPart "More than one datatype named", NamePart n]

188

191

192+ ||| Attempt to type-check a term, getting back itself and its type

193+ check : (tm : Raw) -> Elab (TT, TT)

194+ check tm = prim__Check tm

195+

189 ||| Convert a type-annotated reflected term to its untyped

196 ||| Convert a type-annotated reflected term to its untyped

190 ||| equivalent

197 ||| equivalent

191 forgetTypes : TT -> Elab Raw

198 forgetTypes : TT -> Elab Raw

@@ -306,6 +313,17 @@ namespace Tactics

306 resolveTC : (fn : TTName) -> Elab ()

313 resolveTC : (fn : TTName) -> Elab ()

307 resolveTC fn = prim__ResolveTC fn

314 resolveTC fn = prim__ResolveTC fn

308

315

316+ ||| Use Idris's internal proof search.

317+ search : Elab ()

318+ search = prim__Search 100 []

319+

320+ ||| Use Idris's internal proof search, with more control.

321+ |||

322+ ||| @ depth the search depth

323+ ||| @ hints additional names to try

324+ search' : (depth : Int) -> (hints : List TTName) -> Elab ()

325+ search' depth hints = prim__Search depth hints

326+

309 ||| Halt elaboration, dumping the internal state for inspection.

327 ||| Halt elaboration, dumping the internal state for inspection.

310 |||

328 |||

311 ||| This is intended for elaboration script developers, not for

329 ||| This is intended for elaboration script developers, not for

src/Idris/Core/CaseTree.hs+2

@@ -269,6 +269,8 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo

269 fstT (x, _, _) = x

270 lstT (_, _, x) = x

271

272+ -- Check that all pattern variables are reachable by a case split

273+ -- Otherwise, they won't make sense on the RHS.

272 chkAccessible (avs, l, c)

274 chkAccessible (avs, l, c)

273 | phase == RunTime || reflect = return (l, c)

275 | phase == RunTime || reflect = return (l, c)

274 | otherwise = do mapM_ (acc l) avs

276 | otherwise = do mapM_ (acc l) avs

src/Idris/Core/Elaborate.hs+12−2

@@ -398,9 +398,10 @@ casetac tm = processTactic' (CaseTac tm)

398equiv :: Raw -> Elab' aux ()

399equiv tm = processTactic' (Equiv tm)

400

401−-- | Turn the current hole into a pattern variable with the provided name, made unique if MN

401+-- | Turn the current hole into a pattern variable with the provided

402+-- name, made unique if MN

402patvar :: Name -> Elab' aux ()

403patvar :: Name -> Elab' aux ()

403−patvar n@(SN _) = do apply (Var n) []; solve

404+patvar n@(SN _) = do apply (Var n) []; solve

404patvar n = do env <- get_env

405patvar n = do env <- get_env

405 hs <- get_holes

406 hs <- get_holes

406 if (n `elem` map fst env) then do apply (Var n) []; solve

407 if (n `elem` map fst env) then do apply (Var n) []; solve

@@ -411,6 +412,15 @@ patvar n = do env <- get_env

411 x -> return $! n

412 x -> return $! n

412 processTactic' (PatVar n')

413 processTactic' (PatVar n')

413

414

415+-- | Turn the current hole into a pattern variable with the provided

416+-- name, but don't make MNs unique.

417+patvar' :: Name -> Elab' aux ()

418+patvar' n@(SN _) = do apply (Var n) [] ; solve

419+patvar' n = do env <- get_env

420+ hs <- get_holes

421+ if (n `elem` map fst env) then do apply (Var n) [] ; solve

422+ else processTactic' (PatVar n)

423+

414patbind :: Name -> Elab' aux ()

424patbind :: Name -> Elab' aux ()

415patbind n = processTactic' (PatBind n)

425patbind n = processTactic' (PatBind n)

416

426

src/Idris/Core/Evaluate.hs+36−32

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

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

2 PatternGuards #-}

3+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

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

5module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

5 rt_simplify, simplify, specialise, hnf, convEq, convEq',

6 rt_simplify, simplify, specialise, hnf, convEq, convEq',

@@ -157,6 +158,7 @@ bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)

157unbindEnv :: EnvTT n -> TT n -> TT n

158unbindEnv :: EnvTT n -> TT n -> TT n

158unbindEnv [] tm = tm

159unbindEnv [] tm = tm

159unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

160unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

161+unbindEnv env tm = error $ "Impossible case occurred: couldn't unbind env."

160

162

161usable :: Bool -- specialising

163usable :: Bool -- specialising

162 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])

164 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])

@@ -764,6 +766,7 @@ instance Show Totality where

764 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

766 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

765 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++

767 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++

766 showSep " --> " (map show ns)

768 showSep " --> " (map show ns)

769+ show (Partial (UseUndef n)) = "possibly not total because it uses the undefined name " ++ show n

767

770

768{-!

771{-!

769deriving instance Binary Accessibility

772deriving instance Binary Accessibility

@@ -866,22 +869,23 @@ addCasedef :: Name -> ErasureInfo -> CaseInfo ->

866 [([Name], Term, Term)] -> -- compile time

869 [([Name], Term, Term)] -> -- compile time

867 [([Name], Term, Term)] -> -- inlined

870 [([Name], Term, Term)] -> -- inlined

868 [([Name], Term, Term)] -> -- run time

871 [([Name], Term, Term)] -> -- run time

869− Type -> Context -> Context

872+ Type -> Context -> TC Context

870addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

873addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

871 tcase covering reflect asserted argtys inacc

874 tcase covering reflect asserted argtys inacc

872 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

875 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

873− = let ctxt = definitions uctxt

876+ = do let ctxt = definitions uctxt

874− access = case lookupDefAcc n False uctxt of

877+ access = case lookupDefAcc n False uctxt of

875− [(_, acc)] -> acc

878+ [(_, acc)] -> acc

876− _ -> Public

879+ _ -> Public

877− ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot ei,

880+ totalityTime <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot ei

878− simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct ei,

881+ compileTime <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct ei

879− simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl ei,

882+ inlined <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl ei

880− simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt ei) of

883+ runtime <- simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt ei

884+ ctxt' <- case (totalityTime, compileTime, inlined, runtime) of

881− (OK (CaseDef args_tot sc_tot _),

885+ (CaseDef args_tot sc_tot _,

882− OK (CaseDef args_ct sc_ct _),

886+ CaseDef args_ct sc_ct _,

883− OK (CaseDef args_inl sc_inl _),

887+ CaseDef args_inl sc_inl _,

884− OK (CaseDef args_rt sc_rt _)) ->

888+ CaseDef args_rt sc_rt _) ->

885 let inl = alwaysInline -- tcdict

889 let inl = alwaysInline -- tcdict

886 inlc = (inl || small n args_ct sc_ct) && (not asserted)

890 inlc = (inl || small n args_ct sc_ct) && (not asserted)

887 inlr = inl || small n args_rt sc_rt

891 inlr = inl || small n args_rt sc_rt

@@ -892,28 +896,27 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

892 op = (CaseOp (ci { case_inlinable = inlc })

896 op = (CaseOp (ci { case_inlinable = inlc })

893 ty argtys ps_in ps_tot cdef,

897 ty argtys ps_in ps_tot cdef,

894 access, Unchecked, EmptyMI)

898 access, Unchecked, EmptyMI)

895− in addDef n op ctxt

899+ in return $ addDef n op ctxt

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

900+-- other -> tfail (Msg $ "Error adding case def: " ++ show other)

897− in uctxt { definitions = ctxt' }

901+ return uctxt { definitions = ctxt' }

898

902

899-- simplify a definition for totality checking

903-- simplify a definition for totality checking

900−simplifyCasedef :: Name -> ErasureInfo -> Context -> Context

904+simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context

901simplifyCasedef n ei uctxt

905simplifyCasedef n ei uctxt

902− = let ctxt = definitions uctxt

906+ = do let ctxt = definitions uctxt

903− ctxt' = case lookupCtxt n ctxt of

907+ ctxt' <- case lookupCtxt n ctxt of

904− [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->

908+ [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->

905− ctxt -- nothing to simplify (or already done...)

909+ return ctxt -- nothing to simplify (or already done...)

906− [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->

910+ [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->

907− let ps_in' = map simpl ps_in

911+ do let ps_in' = map simpl ps_in

908− pdef = map debind ps_in' in

912+ pdef = map debind ps_in'

909− case simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei of

913+ CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei

910− OK (CaseDef args sc _) ->

911− addDef n (CaseOp ci

914+ return $ addDef n (CaseOp ci

912− ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

915+ ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

913− acc, tot, metainf) ctxt

916+ acc, tot, metainf) ctxt

914− Error err -> error (show err)

917+

915− _ -> ctxt in

918+ _ -> return ctxt

916− uctxt { definitions = ctxt' }

919+ return uctxt { definitions = ctxt' }

917 where

920 where

918 depat acc (Bind n (PVar t) sc)

921 depat acc (Bind n (PVar t) sc)

919 = depat (n : acc) (instantiate (P Bound n t) sc)

922 = depat (n : acc) (instantiate (P Bound n t) sc)

@@ -1068,6 +1071,7 @@ lookupVal n ctxt

1068 case tfst def of

1071 case tfst def of

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

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

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

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

1074+ _ -> []

1071

1075

1072lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

1076lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

1073lookupTyEnv n env = li n 0 env where

1077lookupTyEnv n env = li n 0 env where

src/Idris/Coverage.hs+3−1

@@ -423,7 +423,9 @@ checkTotality path fc n

423 | otherwise = do

424 t <- getTotality n

425 i <- getIState

426+ ctxt' <- do ctxt <- getContext

426− updateContext (simplifyCasedef n $ getErasureInfo i)

427+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt

428+ setContext ctxt'

427 ctxt <- getContext

429 ctxt <- getContext

428 i <- getIState

430 i <- getIState

429 let opts = case lookupCtxt n (idris_flags i) of

431 let opts = case lookupCtxt n (idris_flags i) of

src/Idris/Elab/Clause.hs+8−4

@@ -224,17 +224,21 @@ elabClauses info' fc opts n_in cs =

224 (idris_patdefs ist) })

225 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)

226 case lookupTy n ctxt of

227+ [ty] -> do ctxt' <- do ctxt <- getContext

228+ tclift $

227− [ty] -> do updateContext (addCasedef n erInfo caseInfo

229+ addCasedef n erInfo caseInfo

228 tcase defaultcase

230 tcase defaultcase

229 reflect

231 reflect

230 (AssertTotal `elem` opts)

232 (AssertTotal `elem` opts)

231 atys

233 atys

232 inacc

234 inacc

233 pats_pe

235 pats_pe

234− pdef

236+ pdef

235− pdef -- compile time

237+ pdef -- compile time

236 pdef_inl -- inlined

238 pdef_inl -- inlined

237− pdef' ty)

239+ pdef' ty

240+ ctxt

241+ setContext ctxt'

238 addIBC (IBCDef n)

242 addIBC (IBCDef n)

239 setTotality n tot

243 setTotality n tot

240 when (not reflect) $ do totcheck (fc, n)

244 when (not reflect) $ do totcheck (fc, n)

src/Idris/Elab/Term.hs+49−22

@@ -1730,21 +1730,27 @@ runTactical ist fc env tm = do tm' <- eval tm

1730 Left lhs -> let (ns, lhs') = patvars [] lhs'

1731 in (ns, lhs', Impossible))

1732 clauses'

1733− set_context $

1733+ ctxt'<- lift $

1734− addCasedef n (const [])

1734+ addCasedef n (const [])

1735− info False (STerm Erased)

1735+ info False (STerm Erased)

1736− True False -- TODO what are these?

1736+ True False -- TODO what are these?

1737− (map snd $ getArgTys ty) [] -- TODO inaccessible types

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

1738− clauses'

1738+ clauses'

1739− clauses''

1739+ clauses''

1740− clauses''

1740+ clauses''

1741− clauses''

1741+ clauses''

1742− clauses''

1742+ clauses''

1743− ty

1743+ ty

1744+ ctxt

1744− ctxt

1745+ set_context ctxt'

1745 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}

1746 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}

1746 return ()

1747 return ()

1747

1748

1749+ checkClosed :: Raw -> Elab' aux (Term, Type)

1750+ checkClosed tm = do ctxt <- get_context

1751+ (val, ty) <- lift $ check ctxt [] tm

1752+ return $! (finalise val, finalise ty)

1753+

1748 -- | Do a step in the reflected elaborator monad. The input is the

1754 -- | Do a step in the reflected elaborator monad. The input is the

1749 -- step, the output is the (reflected) term returned.

1755 -- step, the output is the (reflected) term returned.

1750 runTacTm :: Term -> ElabD Term

1756 runTacTm :: Term -> ElabD Term

@@ -1755,12 +1761,12 @@ runTactical ist fc env tm = do tm' <- eval tm

1755 | n == tacN "prim__Goal", [] <- args

1761 | n == tacN "prim__Goal", [] <- args

1756 = do (h:_) <- get_holes

1762 = do (h:_) <- get_holes

1757 t <- goal

1763 t <- goal

1758− fmap fst . get_type_val $

1764+ fmap fst . checkClosed $

1759 rawPair (Var (reflm "TTName"), Var (reflm "TT"))

1765 rawPair (Var (reflm "TTName"), Var (reflm "TT"))

1760 (reflectName h, reflect t)

1766 (reflectName h, reflect t)

1761 | n == tacN "prim__Holes", [] <- args

1767 | n == tacN "prim__Holes", [] <- args

1762 = do hs <- get_holes

1768 = do hs <- get_holes

1763− fmap fst . get_type_val $

1769+ fmap fst . checkClosed $

1764 mkList (Var $ reflm "TTName") (map reflectName hs)

1770 mkList (Var $ reflm "TTName") (map reflectName hs)

1765 | n == tacN "prim__Guess", [] <- args

1771 | n == tacN "prim__Guess", [] <- args

1766 = do ok <- is_guess

1772 = do ok <- is_guess

@@ -1770,7 +1776,7 @@ runTactical ist fc env tm = do tm' <- eval tm

1770 RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))

1776 RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))

1771 (Var (reflm "TT")))

1777 (Var (reflm "TT")))

1772 guess

1778 guess

1773− else fmap fst . get_type_val $

1779+ else fmap fst . checkClosed $

1774 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))

1780 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))

1775 (Var (reflm "TT"))

1781 (Var (reflm "TT"))

1776 | n == tacN "prim__LookupTy", [n] <- args

1782 | n == tacN "prim__LookupTy", [n] <- args

@@ -1790,7 +1796,7 @@ runTactical ist fc env tm = do tm' <- eval tm

1790 let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty)

1796 let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty)

1791 | (n, def) <- lookupNameDef n' ctxt

1797 | (n, def) <- lookupNameDef n' ctxt

1792 , let (nt, ty) = getNameTypeAndType def ]

1798 , let (nt, ty) = getNameTypeAndType def ]

1793− fmap fst . get_type_val $

1799+ fmap fst . checkClosed $

1794 rawList (raw_apply (Var pairTy) [ Var (reflm "TTName")

1800 rawList (raw_apply (Var pairTy) [ Var (reflm "TTName")

1795 , raw_apply (Var pairTy) [ Var (reflm "NameType")

1801 , raw_apply (Var pairTy) [ Var (reflm "NameType")

1796 , Var (reflm "TT")]])

1802 , Var (reflm "TT")]])

@@ -1799,15 +1805,15 @@ runTactical ist fc env tm = do tm' <- eval tm

1799 = do n' <- reifyTTName name

1805 = do n' <- reifyTTName name

1800 datatypes <- get_datatypes

1806 datatypes <- get_datatypes

1801 ctxt <- get_context

1807 ctxt <- get_context

1802− fmap fst . get_type_val $

1808+ fmap fst . checkClosed $

1803 rawList (Var (tacN "Datatype"))

1809 rawList (Var (tacN "Datatype"))

1804 (map reflectDatatype (buildDatatypes ctxt datatypes n'))

1810 (map reflectDatatype (buildDatatypes ctxt datatypes n'))

1805 | n == tacN "prim__SourceLocation", [] <- args

1811 | n == tacN "prim__SourceLocation", [] <- args

1806− = fmap fst . get_type_val $

1812+ = fmap fst . checkClosed $

1807 reflectFC fc

1813 reflectFC fc

1808 | n == tacN "prim__Env", [] <- args

1814 | n == tacN "prim__Env", [] <- args

1809 = do env <- get_env

1815 = do env <- get_env

1810− fmap fst . get_type_val $ reflectEnv env

1816+ fmap fst . checkClosed $ reflectEnv env

1811 | n == tacN "prim__Fail", [_a, errs] <- args

1817 | n == tacN "prim__Fail", [_a, errs] <- args

1812 = do errs' <- eval errs

1818 = do errs' <- eval errs

1813 parts <- reifyReportParts errs'

1819 parts <- reifyReportParts errs'

@@ -1843,9 +1849,17 @@ runTactical ist fc env tm = do tm' <- eval tm

1843 ty' <- reifyRaw ty

1849 ty' <- reifyRaw ty

1844 claim n' ty'

1850 claim n' ty'

1845 returnUnit

1851 returnUnit

1852+ | n == tacN "prim__Check", [raw] <- args

1853+ = do raw' <- reifyRaw =<< eval raw

1854+ ctxt <- get_context

1855+ env <- get_env

1856+ (tm, ty) <- lift $ check ctxt env raw'

1857+ fmap fst . checkClosed $

1858+ rawPair (Var (reflm "TT"), Var (reflm "TT"))

1859+ (reflect tm, reflect ty)

1846 | n == tacN "prim__Forget", [tt] <- args

1860 | n == tacN "prim__Forget", [tt] <- args

1847 = do tt' <- reifyTT tt

1861 = do tt' <- reifyTT tt

1848− fmap fst . get_type_val . reflectRaw $ forget tt'

1862+ fmap fst . checkClosed . reflectRaw $ forget tt'

1849 | n == tacN "prim__Attack", [] <- args

1863 | n == tacN "prim__Attack", [] <- args

1850 = do attack

1864 = do attack

1851 returnUnit

1865 returnUnit

@@ -1874,7 +1888,7 @@ runTactical ist fc env tm = do tm' <- eval tm

1874 returnUnit

1888 returnUnit

1875 | n == tacN "prim__PatVar", [n] <- args

1889 | n == tacN "prim__PatVar", [n] <- args

1876 = do n' <- reifyTTName n

1890 = do n' <- reifyTTName n

1877− patvar n'

1891+ patvar' n'

1878 returnUnit

1892 returnUnit

1879 | n == tacN "prim__PatBind", [n] <- args

1893 | n == tacN "prim__PatBind", [n] <- args

1880 = do n' <- reifyTTName n

1894 = do n' <- reifyTTName n

@@ -1921,6 +1935,19 @@ runTactical ist fc env tm = do tm' <- eval tm

1921 fn <- reifyTTName fn

1935 fn <- reifyTTName fn

1922 resolveTC False True 100 g fn ist

1936 resolveTC False True 100 g fn ist

1923 returnUnit

1937 returnUnit

1938+ | n == tacN "prim__Search", [depth, hints] <- args

1939+ = do d <- eval depth

1940+ hints' <- eval hints

1941+ case (d, unList hints') of

1942+ (Constant (I i), Just hs) ->

1943+ do actualHints <- mapM reifyTTName hs

1944+ unifyProblems

1945+ let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")

1946+ proofSearch True True False False i psElab Nothing (sMN 0 "search ") actualHints ist

1947+ returnUnit

1948+ (Constant (I _), Nothing ) ->

1949+ lift . tfail . InternalMsg $ "Not a list: " ++ show hints'

1950+ (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d

1924 | n == tacN "prim__RecursiveElab", [goal, script] <- args

1951 | n == tacN "prim__RecursiveElab", [goal, script] <- args

1925 = do goal' <- reifyRaw goal

1952 = do goal' <- reifyRaw goal

1926 ctxt <- get_context

1953 ctxt <- get_context

@@ -1939,7 +1966,7 @@ runTactical ist fc env tm = do tm' <- eval tm

1939 env' <- get_env

1966 env' <- get_env

1940 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out

1967 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out

1941 let (tm', ty') = (reflect tm, reflect ty)

1968 let (tm', ty') = (reflect tm, reflect ty)

1942− fmap fst . get_type_val $

1969+ fmap fst . checkClosed $

1943 rawPair (Var $ reflm "TT", Var $ reflm "TT")

1970 rawPair (Var $ reflm "TT", Var $ reflm "TT")

1944 (tm', ty')

1971 (tm', ty')

1945 | n == tacN "prim__Debug", [ty, msg] <- args

1972 | n == tacN "prim__Debug", [ty, msg] <- args

src/Idris/ElabDecls.hs+3−1

@@ -195,7 +195,9 @@ elabDecl' what info (PMutual f ps)

195 -- Do totality checking after entire mutual block

196 i <- get

197 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

198+ ctxt' <- do ctxt <- getContext

198− updateContext (simplifyCasedef n $ getErasureInfo i))

199+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt

200+ setContext ctxt')

199 (map snd (idris_totcheck i))

201 (map snd (idris_totcheck i))

200 mapM_ buildSCG (idris_totcheck i)

202 mapM_ buildSCG (idris_totcheck i)

201 mapM_ checkDeclTotality (idris_totcheck i)

203 mapM_ checkDeclTotality (idris_totcheck i)

src/Idris/Parser.hs+4−1

@@ -1474,7 +1474,10 @@ loadSource lidr f toline

1474 -- simplify every definition do give the totality checker

1475 -- a better chance

1476 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

1477+ ctxt' <-

1478+ do ctxt <- getContext

1477− updateContext (simplifyCasedef n $ getErasureInfo i))

1479+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt

1480+ setContext ctxt')

1478 (map snd (idris_totcheck i))

1481 (map snd (idris_totcheck i))

1479 -- build size change graph from simplified definitions

1482 -- build size change graph from simplified definitions

1480 iLOG "Totality checking"

1483 iLOG "Totality checking"

src/Idris/Prover.hs+10−7

@@ -86,13 +86,16 @@ prove opt ctxt lit n ty

86 Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0)

87 ptm' <- applyOpts ptm

88 ei <- getErasureInfo `fmap` getIState

89+ ctxt' <- do ctxt <- getContext

89− updateContext (addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False

90+ tclift $ addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False

90− [] [] -- argtys, inaccArgs

91+ [] [] -- argtys, inaccArgs

91− [Right (P Ref n ty, ptm)]

92+ [Right (P Ref n ty, ptm)]

92− [([], P Ref n ty, ptm)]

93+ [([], P Ref n ty, ptm)]

93− [([], P Ref n ty, ptm)]

94+ [([], P Ref n ty, ptm)]

94− [([], P Ref n ty, ptm)]

95+ [([], P Ref n ty, ptm)]

95− [([], P Ref n ty, ptm')] ty)

96+ [([], P Ref n ty, ptm')] ty

97+ ctxt

98+ setContext ctxt'

96 solveDeferred n

99 solveDeferred n

97 case idris_outputmode i of

100 case idris_outputmode i of

98 IdeMode n h ->

101 IdeMode n h ->