b1d2553 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Respect accessibility in case tree elaboration.

b1d2553Matus Tejiscak13 years ago

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

compare with master

unifiedsplit

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

191-- Work Right to Left

192

193simpleCase :: Bool -> Bool -> Bool ->

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

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

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

196 TC CaseDef

197−simpleCase tc cover reflect phase fc argtys cs

197+simpleCase tc cover reflect phase fc inacc argtys cs

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

199 case r of

200 Impossible -> False

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

212 OK pats ->

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

214 ns = take numargs args

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

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

216 (tree, st) = runState

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

218 ([], numargs, [])

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

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

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

383-- than dependency)

384−

384+--

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

386+

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

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

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

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

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

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

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

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

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

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

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

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

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

391 where

394 where

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

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

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

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

394

397

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

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

396

399

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

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

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

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

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

399

403

400 numNames xs (PCon n _ _ : ps)

404 numNames xs (PCon n _ _ : ps)

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

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

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

785addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

786 [Type] -> -- argument types

787+ [Int] -> -- inaccessible arguments

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

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

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

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

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

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

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

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

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

792 Type -> Context -> Context

793 Type -> Context -> Context

793addCasedef n ci@(CaseInfo alwaysInline tcdict)

794addCasedef n ci@(CaseInfo alwaysInline tcdict)

794− tcase covering reflect asserted argtys

795+ tcase covering reflect asserted argtys inacc

795 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

796 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

796 = let ctxt = definitions uctxt

797 = let ctxt = definitions uctxt

797 access = case lookupDefAcc n False uctxt of

798 access = case lookupDefAcc n False uctxt of

798 [(_, acc)] -> acc

799 [(_, acc)] -> acc

799 _ -> Public

800 _ -> Public

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

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

801− simpleCase tcase covering reflect CompileTime emptyFC argtys ps_ct,

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

802− simpleCase tcase covering reflect CompileTime emptyFC argtys ps_inl,

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

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

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

804 (OK (CaseDef args_tot sc_tot _),

805 (OK (CaseDef args_tot sc_tot _),

805 OK (CaseDef args_ct sc_ct _),

806 OK (CaseDef args_ct sc_ct _),

806 OK (CaseDef args_inl sc_inl _),

807 OK (CaseDef args_inl sc_inl _),

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

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

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

828 let ps_in' = map simpl ps_in

829 let ps_in' = map simpl ps_in

829 pdef = map debind ps_in' in

830 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

831 OK (CaseDef args sc _) ->

832 OK (CaseDef args sc _) ->

832 addDef n (CaseOp ci

833 addDef n (CaseOp ci

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

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

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

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

946 do ctxt <- getContext

947+ ist <- getIState

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

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

950+ _ -> []

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

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

948 let tys = lookupTy n ctxt

952 let tys = lookupTy n ctxt

949 let reflect = Reflection `elem` opts

953 let reflect = Reflection `elem` opts

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

1039

1043

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

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

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

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

1042− simpleCase tcase False reflect CompileTime fc atys pdef

1046+ simpleCase tcase False reflect CompileTime fc inacc atys pdef

1043 cov <- coverage

1047 cov <- coverage

1044 pmissing <-

1048 pmissing <-

1045 if cov && not (hasDefault cs)

1049 if cov && not (hasDefault cs)

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

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

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

1089

1093

1090 tree' <- tclift $ simpleCase tcase knowncovering reflect

1094 tree' <- tclift $ simpleCase tcase knowncovering reflect

1091− RunTime fc atys pdef'

1095+ RunTime fc inacc atys pdef'

1092 logLvl 3 (show tree)

1096 logLvl 3 (show tree)

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

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

1094 ctxt <- getContext

1098 ctxt <- getContext

1095 ist <- getIState

1099 ist <- getIState

1100+ let opt = idris_optimisation ist

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

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

1097 (idris_patdefs ist) })

1102 (idris_patdefs ist) })

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

1103 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

1102 reflect

1107 reflect

1103 (AssertTotal `elem` opts)

1108 (AssertTotal `elem` opts)

1104 atys

1109 atys

1110+ inacc

1105 pats

1111 pats

1106 pdef pdef pdef_inl pdef' ty)

1112 pdef pdef pdef_inl pdef' ty)

1107 addIBC (IBCDef n)

1113 addIBC (IBCDef n)

src/Idris/Erasure.hs+9−8

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

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

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

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

230− getDepsSC fn es vs (Case n alts)

230+ getDepsSC fn es vs (Case n alts)

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

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

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

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

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

233− -- of this function is used at all

234+ -- that the result 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

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

236 where

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

237+ addTagDep = case alts of

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

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

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

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

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

240

241

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

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

src/Idris/Prover.hs+6−5

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

7import Idris.Core.Typecheck

9import Idris.AbsSyntax

10+import Idris.AbsSyntaxTree

10import Idris.Delaborate

11import Idris.Delaborate

11import Idris.ElabDecls

12import Idris.ElabDecls

12import Idris.ElabTerm

13import Idris.ElabTerm

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

33 i <- getIState

34 i <- getIState

34 case lookupTy x ctxt of

35 case lookupTy x ctxt of

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

36 [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

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

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

38 _ -> fail "No such metavariable"

39 _ -> fail "No such metavariable"

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

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

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

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

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

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

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

60−prove ctxt lit n ty

61+prove opt ctxt lit n ty

61 = do let ps = initElaborator n ctxt ty

62 = do let ps = initElaborator n ctxt ty

62 ideslavePutSExp "start-proof-mode" n

63 ideslavePutSExp "start-proof-mode" n

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

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

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

67 ideslavePutSExp "end-proof-mode" n

68 ideslavePutSExp "end-proof-mode" n

68 let proofs = proof_list i

69 let proofs = proof_list i

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

70 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)]

71 logLvl 3 (show tree)

72 logLvl 3 (show tree)

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

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

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

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

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

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

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

78 ptm' <- applyOpts ptm

79 ptm' <- applyOpts ptm

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

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

80− []

81+ [] [] -- argtys, inaccArgs

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

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

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

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

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