b1d2553 · Idris-dev · git.iko.soy

src/Idris/Core/CaseTree.hs+18−14

@@ -191,10 +191,10 @@ data Phase = CompileTime | RunTime

191191-- Work Right to Left

192192

193193simpleCase :: Bool -> Bool -> Bool ->

194− Phase -> FC -> [Type] ->

194+ Phase -> FC -> [Int] -> [Type] ->

195195 [([Name], Term, Term)] ->

196196 TC CaseDef

197−simpleCase tc cover reflect phase fc argtys cs

197+simpleCase tc cover reflect phase fc inacc argtys cs

198198 = sc' tc cover phase fc (filter (\(_, _, r) ->

199199 case r of

200200 Impossible -> False

@@ -212,7 +212,7 @@ simpleCase tc cover reflect phase fc argtys cs

212212 OK pats ->

213213 let numargs = length (fst (head pats))

214214 ns = take numargs args

215− (ns', ps') = order ns pats

215+ (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats

216216 (tree, st) = runState

217217 (match ns' ps' (defaultCase cover))

218218 ([], numargs, [])

@@ -381,21 +381,25 @@ partition xs = error $ "Partition " ++ show xs

381381-- reorder the patterns so that the one with most distinct names

382382-- comes next. Take rightmost first, otherwise (i.e. pick value rather

383383-- than dependency)

384−

385−order :: [Name] -> [Clause] -> ([Name], [Clause])

386−order [] cs = ([], cs)

387−order ns [] = (ns, [])

388−order ns cs = let patnames = transpose (map (zip ns) (map fst cs))

389− pats' = transpose (sortBy moreDistinct (reverse patnames)) in

390− (getNOrder pats', zipWith rebuild pats' cs)

384+--

385+-- The first argument means [(Name, IsInaccessible)].

386+

387+order :: [(Name, Bool)] -> [Clause] -> ([Name], [Clause])

388+order [] cs = ([], cs)

389+order ns' [] = (map fst ns', [])

390+order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

391+ -- note: sortBy . reverse is not nonsense because sortBy is stable

392+ pats' = transpose (sortBy moreDistinct (reverse patnames)) in

393+ (getNOrder pats', zipWith rebuild pats' cs)

391394 where

392− getNOrder [] = error $ "Failed order on " ++ show (ns, cs)

393− getNOrder (c : _) = map fst c

395+ getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)

396+ getNOrder (c : _) = map (fst . fst) c

394397

395398 rebuild patnames clause = (map snd patnames, snd clause)

396399

397− moreDistinct xs ys = compare (numNames [] (map snd ys))

398− (numNames [] (map snd xs))

400+ -- this compares (+isInaccessible, -numberOfCases)

401+ moreDistinct xs ys = compare (snd . fst . head $ xs, numNames [] (map snd ys))

402+ (snd . fst . head $ ys, numNames [] (map snd xs))

399403

400404 numNames xs (PCon n _ _ : ps)

401405 | not (Left n `elem` xs) = numNames (Left n : xs) ps

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

@@ -784,6 +784,7 @@ addDatatype (Data n tag ty cons) uctxt

784784-- FIXME: Too many arguments! Refactor all these Bools.

785785addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

786786 [Type] -> -- argument types

787+ [Int] -> -- inaccessible arguments

787788 [Either Term (Term, Term)] ->

788789 [([Name], Term, Term)] -> -- totality

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

@@ -791,16 +792,16 @@ addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

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

792793 Type -> Context -> Context

793794addCasedef n ci@(CaseInfo alwaysInline tcdict)

794− tcase covering reflect asserted argtys

795+ tcase covering reflect asserted argtys inacc

795796 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

796797 = let ctxt = definitions uctxt

797798 access = case lookupDefAcc n False uctxt of

798799 [(_, acc)] -> acc

799800 _ -> Public

800− ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC argtys ps_tot,

801− simpleCase tcase covering reflect CompileTime emptyFC argtys ps_ct,

802− simpleCase tcase covering reflect CompileTime emptyFC argtys ps_inl,

803− simpleCase tcase covering reflect RunTime emptyFC argtys ps_rt) of

801+ ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot,

802+ simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct,

803+ simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl,

804+ simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt) of

804805 (OK (CaseDef args_tot sc_tot _),

805806 OK (CaseDef args_ct sc_ct _),

806807 OK (CaseDef args_inl sc_inl _),

@@ -827,7 +828,7 @@ simplifyCasedef n uctxt

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

828829 let ps_in' = map simpl ps_in

829830 pdef = map debind ps_in' in

830− case simpleCase False True False CompileTime emptyFC atys pdef of

831+ case simpleCase False True False CompileTime emptyFC [] atys pdef of

831832 OK (CaseDef args sc _) ->

832833 addDef n (CaseOp ci

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

src/Idris/ElabDecls.hs+8−2

@@ -944,6 +944,10 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

944944elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

945945elabClauses info fc opts n_in cs = let n = liftname info n_in in

946946 do ctxt <- getContext

947+ ist <- getIState

948+ let inacc = case lookupCtxt n (idris_optimisation ist) of

949+ [Optimise _ _ _ _ inacc] -> map fst inacc

950+ _ -> []

947951 -- Check n actually exists, with no definition yet

948952 let tys = lookupTy n ctxt

949953 let reflect = Reflection `elem` opts

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

10391043

10401044 let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats

10411045 tree@(CaseDef scargs sc _) <- tclift $

1042− simpleCase tcase False reflect CompileTime fc atys pdef

1046+ simpleCase tcase False reflect CompileTime fc inacc atys pdef

10431047 cov <- coverage

10441048 pmissing <-

10451049 if cov && not (hasDefault cs)

@@ -1088,11 +1092,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

10881092 let knowncovering = (pcover && cov) || AssertTotal `elem` opts

10891093

10901094 tree' <- tclift $ simpleCase tcase knowncovering reflect

1091− RunTime fc atys pdef'

1095+ RunTime fc inacc atys pdef'

10921096 logLvl 3 (show tree)

10931097 logLvl 3 $ "Optimised: " ++ show tree'

10941098 ctxt <- getContext

10951099 ist <- getIState

1100+ let opt = idris_optimisation ist

10961101 putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)

10971102 (idris_patdefs ist) })

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

@@ -1102,6 +1107,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

11021107 reflect

11031108 (AssertTotal `elem` opts)

11041109 atys

1110+ inacc

11051111 pats

11061112 pdef pdef pdef_inl pdef' ty)

11071113 addIBC (IBCDef n)

src/Idris/Erasure.hs+9−8

@@ -227,15 +227,16 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

227227 getDepsSC fn es vs (UnmatchedCase msg) = M.empty

228228 getDepsSC fn es vs (ProjCase t alt) = error "ProjCase not supported"

229229 getDepsSC fn es vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)

230− getDepsSC fn es vs (Case n alts)

231− -- we case-split on this variable, which necessarily marks it as used

232− -- hence we add a new dependency whose only preconditions are that the result

233− -- of this function is used at all

234− = M.insertWith S.union (S.singleton (fn, Result)) casedVar -- add this dep to all deps

235− $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree

230+ getDepsSC fn es vs (Case n alts)

231+ -- we case-split on this variable, which marks it as used

232+ -- (unless there is exactly one case branch)

233+ -- hence we add a new dependency, whose only precondition is

234+ -- that the result of this function is used at all

235+ = addTagDep $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree

236236 where

237− -- TODO: use effect instead of casedVar to mark the ctor tag

238− -- effect = S.insert (typeName, Result) casedVar -- mark the tag of the type name as used

237+ addTagDep = case alts of

238+ [_] -> id -- single branch, tag not used

239+ _ -> M.insertWith S.union (S.singleton (fn, Result)) casedVar -- more case branches

239240 casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)

240241

241242 getDepsAlt :: Name -> [Name] -> Vars -> Var -> CaseAlt -> Deps

src/Idris/Prover.hs+6−5

@@ -7,6 +7,7 @@ import Idris.Core.CaseTree

77import Idris.Core.Typecheck

88

99import Idris.AbsSyntax

10+import Idris.AbsSyntaxTree

1011import Idris.Delaborate

1112import Idris.ElabDecls

1213import Idris.ElabTerm

@@ -33,7 +34,7 @@ prover lit x =

3334 i <- getIState

3435 case lookupTy x ctxt of

3536 [t] -> if elem x (map fst (idris_metavars i))

36− then prove ctxt lit x t

37+ then prove (idris_optimisation i) ctxt lit x t

3738 else ifail $ show x ++ " is not a metavariable"

3839 _ -> fail "No such metavariable"

3940

@@ -56,8 +57,8 @@ assumptionNames e

5657 names ((MN _ _, _) : bs) = names bs

5758 names ((n, _) : bs) = show n : names bs

5859

59−prove :: Context -> Bool -> Name -> Type -> Idris ()

60−prove ctxt lit n ty

60+prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

61+prove opt ctxt lit n ty

6162 = do let ps = initElaborator n ctxt ty

6263 ideslavePutSExp "start-proof-mode" n

6364 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

@@ -67,7 +68,7 @@ prove ctxt lit n ty

6768 ideslavePutSExp "end-proof-mode" n

6869 let proofs = proof_list i

6970 putIState (i { proof_list = (n, prf) : proofs })

70− let tree = simpleCase False True False CompileTime (fileFC "proof") [] [([], P Ref n ty, tm)]

71+ let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

7172 logLvl 3 (show tree)

7273 (ptm, pty) <- recheckC (fileFC "proof") [] tm

7374 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

@@ -77,7 +78,7 @@ prove ctxt lit n ty

7778 Error e -> ierror (CantUnify False ty pty e [] 0)

7879 ptm' <- applyOpts ptm

7980 updateContext (addCasedef n (CaseInfo True False) False False True False

80− []

81+ [] [] -- argtys, inaccArgs

8182 [Right (P Ref n ty, ptm)]

8283 [([], P Ref n ty, ptm)]

8384 [([], P Ref n ty, ptm)]