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

git.iko.soy/Idris-dev

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

Updates from Elab reflection

commit0c953a9c2d4e2f1fb11b5022055b60af4ee45f19 authorDavid Christiansen <david@davidchristiansen.dk> dateThu 28 May 2015, 12:59 (11 years ago) parent6a6d0d6 d312a57

10 files changed+145−70

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Elab.idr+18 src/Idris/Core/CaseTree.hs+2 src/Idris/Core/Elaborate.hs+12−2 src/Idris/Core/Evaluate.hs+36−32 src/Idris/Coverage.hs+3−1 src/Idris/Elab/Clause.hs+8−4 src/Idris/Elab/Term.hs+49−22 src/Idris/ElabDecls.hs+3−1 src/Idris/Parser.hs+4−1 src/Idris/Prover.hs+10−7

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

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

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

8686 prim__LookupDatatype : TTName -> Elab (List Datatype)

8787

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

89+

8890 prim__SourceLocation : Elab SourceLocation

8991

9092 prim__Forget : TT -> Elab Raw

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

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

114116

115117 prim__ResolveTC : TTName -> Elab ()

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

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

117120

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

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

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

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

188191

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+

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

190197 ||| equivalent

191198 forgetTypes : TT -> Elab Raw

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

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

307314 resolveTC fn = prim__ResolveTC fn

308315

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+

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

310328 |||

311329 ||| 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

269269 fstT (x, _, _) = x

270270 lstT (_, _, x) = x

271271

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

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

272274 chkAccessible (avs, l, c)

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

274276 | otherwise = do mapM_ (acc l) avs

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

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

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

399399equiv tm = processTactic' (Equiv tm)

400400

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

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

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

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

404405patvar n = do env <- get_env

405406 hs <- get_holes

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

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

411412 x -> return $! n

412413 processTactic' (PatVar n')

413414

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+

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

415425patbind n = processTactic' (PatBind n)

416426

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

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

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

22 PatternGuards #-}

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

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

56 rt_simplify, simplify, specialise, hnf, convEq, convEq',

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

157158unbindEnv :: EnvTT n -> TT n -> TT n

158159unbindEnv [] tm = tm

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

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

160162

161163usable :: Bool -- specialising

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

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

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

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

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

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

767770

768771{-!

769772deriving instance Binary Accessibility

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

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

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

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

869− Type -> Context -> Context

872+ Type -> Context -> TC Context

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

871874 tcase covering reflect asserted argtys inacc

872875 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

873− = let ctxt = definitions uctxt

874− access = case lookupDefAcc n False uctxt of

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

876− _ -> Public

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

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

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

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

881− (OK (CaseDef args_tot sc_tot _),

882− OK (CaseDef args_ct sc_ct _),

883− OK (CaseDef args_inl sc_inl _),

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

876+ = do let ctxt = definitions uctxt

877+ access = case lookupDefAcc n False uctxt of

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

879+ _ -> Public

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

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

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

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

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

885+ (CaseDef args_tot sc_tot _,

886+ CaseDef args_ct sc_ct _,

887+ CaseDef args_inl sc_inl _,

888+ CaseDef args_rt sc_rt _) ->

885889 let inl = alwaysInline -- tcdict

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

887891 inlr = inl || small n args_rt sc_rt

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

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

893897 ty argtys ps_in ps_tot cdef,

894898 access, Unchecked, EmptyMI)

895− in addDef n op ctxt

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

897− in uctxt { definitions = ctxt' }

899+ in return $ addDef n op ctxt

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

901+ return uctxt { definitions = ctxt' }

898902

899903-- simplify a definition for totality checking

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

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

901905simplifyCasedef n ei uctxt

902− = let ctxt = definitions uctxt

903− ctxt' = case lookupCtxt n ctxt of

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

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

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

907− let ps_in' = map simpl ps_in

908− pdef = map debind ps_in' in

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

910− OK (CaseDef args sc _) ->

911− addDef n (CaseOp ci

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

913− acc, tot, metainf) ctxt

914− Error err -> error (show err)

915− _ -> ctxt in

916− uctxt { definitions = ctxt' }

906+ = do let ctxt = definitions uctxt

907+ ctxt' <- case lookupCtxt n ctxt of

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

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

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

911+ do let ps_in' = map simpl ps_in

912+ pdef = map debind ps_in'

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

914+ return $ addDef n (CaseOp ci

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

916+ acc, tot, metainf) ctxt

917+

918+ _ -> return ctxt

919+ return uctxt { definitions = ctxt' }

917920 where

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

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

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

10681071 case tfst def of

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

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

1074+ _ -> []

10711075

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

10731077lookupTyEnv n env = li n 0 env where

src/Idris/Coverage.hs+3−1

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

423423 | otherwise = do

424424 t <- getTotality n

425425 i <- getIState

426− updateContext (simplifyCasedef n $ getErasureInfo i)

426+ ctxt' <- do ctxt <- getContext

427+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt

428+ setContext ctxt'

427429 ctxt <- getContext

428430 i <- getIState

429431 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 =

224224 (idris_patdefs ist) })

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

226226 case lookupTy n ctxt of

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

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

228+ tclift $

229+ addCasedef n erInfo caseInfo

228230 tcase defaultcase

229231 reflect

230232 (AssertTotal `elem` opts)

231233 atys

232234 inacc

233235 pats_pe

234− pdef

235− pdef -- compile time

236+ pdef

237+ pdef -- compile time

236238 pdef_inl -- inlined

237− pdef' ty)

239+ pdef' ty

240+ ctxt

241+ setContext ctxt'

238242 addIBC (IBCDef n)

239243 setTotality n tot

240244 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

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

17311731 in (ns, lhs', Impossible))

17321732 clauses'

1733− set_context $

1734− addCasedef n (const [])

1735− info False (STerm Erased)

1736− True False -- TODO what are these?

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

1738− clauses'

1739− clauses''

1740− clauses''

1741− clauses''

1742− clauses''

1743− ty

1744− ctxt

1733+ ctxt'<- lift $

1734+ addCasedef n (const [])

1735+ info False (STerm Erased)

1736+ True False -- TODO what are these?

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

1738+ clauses'

1739+ clauses''

1740+ clauses''

1741+ clauses''

1742+ clauses''

1743+ ty

1744+ ctxt

1745+ set_context ctxt'

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

17461747 return ()

17471748

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+

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

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

17501756 runTacTm :: Term -> ElabD Term

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

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

17561762 = do (h:_) <- get_holes

17571763 t <- goal

1758− fmap fst . get_type_val $

1764+ fmap fst . checkClosed $

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

17601766 (reflectName h, reflect t)

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

17621768 = do hs <- get_holes

1763− fmap fst . get_type_val $

1769+ fmap fst . checkClosed $

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

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

17661772 = do ok <- is_guess

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

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

17711777 (Var (reflm "TT")))

17721778 guess

1773− else fmap fst . get_type_val $

1779+ else fmap fst . checkClosed $

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

17751781 (Var (reflm "TT"))

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

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

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

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

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

1793− fmap fst . get_type_val $

1799+ fmap fst . checkClosed $

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

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

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

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

17991805 = do n' <- reifyTTName name

18001806 datatypes <- get_datatypes

18011807 ctxt <- get_context

1802− fmap fst . get_type_val $

1808+ fmap fst . checkClosed $

18031809 rawList (Var (tacN "Datatype"))

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

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

1806− = fmap fst . get_type_val $

1812+ = fmap fst . checkClosed $

18071813 reflectFC fc

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

18091815 = do env <- get_env

1810− fmap fst . get_type_val $ reflectEnv env

1816+ fmap fst . checkClosed $ reflectEnv env

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

18121818 = do errs' <- eval errs

18131819 parts <- reifyReportParts errs'

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

18431849 ty' <- reifyRaw ty

18441850 claim n' ty'

18451851 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)

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

18471861 = do tt' <- reifyTT tt

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

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

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

18501864 = do attack

18511865 returnUnit

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

18741888 returnUnit

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

18761890 = do n' <- reifyTTName n

1877− patvar n'

1891+ patvar' n'

18781892 returnUnit

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

18801894 = do n' <- reifyTTName n

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

19211935 fn <- reifyTTName fn

19221936 resolveTC False True 100 g fn ist

19231937 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

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

19251952 = do goal' <- reifyRaw goal

19261953 ctxt <- get_context

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

19391966 env' <- get_env

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

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

1942− fmap fst . get_type_val $

1969+ fmap fst . checkClosed $

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

19441971 (tm', ty')

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

src/Idris/ElabDecls.hs+3−1

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

195195 -- Do totality checking after entire mutual block

196196 i <- get

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

198− updateContext (simplifyCasedef n $ getErasureInfo i))

198+ ctxt' <- do ctxt <- getContext

199+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt

200+ setContext ctxt')

199201 (map snd (idris_totcheck i))

200202 mapM_ buildSCG (idris_totcheck i)

201203 mapM_ checkDeclTotality (idris_totcheck i)

src/Idris/Parser.hs+4−1

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

14741474 -- simplify every definition do give the totality checker

14751475 -- a better chance

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

1477− updateContext (simplifyCasedef n $ getErasureInfo i))

1477+ ctxt' <-

1478+ do ctxt <- getContext

1479+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt

1480+ setContext ctxt')

14781481 (map snd (idris_totcheck i))

14791482 -- build size change graph from simplified definitions

14801483 iLOG "Totality checking"

src/Idris/Prover.hs+10−7

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

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

8787 ptm' <- applyOpts ptm

8888 ei <- getErasureInfo `fmap` getIState

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

90− [] [] -- argtys, inaccArgs

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

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

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

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

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

89+ ctxt' <- do ctxt <- getContext

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

91+ [] [] -- argtys, inaccArgs

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

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

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

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

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

97+ ctxt

98+ setContext ctxt'

9699 solveDeferred n

97100 case idris_outputmode i of

98101 IdeMode n h ->