45bf2b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix ordering of run time case trees

45bf2b6Edwin Brady10 years ago

src/Idris/Core/CaseTree.hs+34−22

compare with master

unifiedsplit

@@ -251,7 +251,8 @@ data Phase = CompileTime | RunTime

251-- Work Right to Left

252

253simpleCase :: Bool -> SC -> Bool ->

254− Phase -> FC -> [Int] -> [Type] ->

254+ Phase -> FC -> [Int] ->

255+ [(Type, Bool)] -> -- ^ (Argument type, whether it's canonical)

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

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

256 ErasureInfo ->

257 ErasureInfo ->

257 TC CaseDef

258 TC CaseDef

@@ -273,7 +274,7 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo

273 OK pats ->

274 OK pats ->

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

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

275 ns = take numargs args

276 ns = take numargs args

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

277+ (ns', ps') = order phase [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats (map snd argtys)

277 (tree, st) = runCaseBuilder erInfo

278 (tree, st) = runCaseBuilder erInfo

278 (match ns' ps' defcase)

279 (match ns' ps' defcase)

279 ([], numargs, [])

280 ([], numargs, [])

@@ -431,28 +432,38 @@ partition xs = error $ "Partition " ++ show xs

431--

432--

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

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

433

434

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

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

436+-- do nothing at compile time: FIXME (EB): Put this in after checking

437+-- implications for Franck's reflection work... see issue 3233

438+-- order CompileTime ns cs _ = (map fst ns, cs)

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

439+order _ [] cs cans = ([], cs)

436−order ns' [] = (map fst ns', [])

440+order _ ns' [] cans = (map fst ns', [])

441+order phase ns' cs cans

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

442+ = let patnames = transpose (map (zip ns') (map (zip cans) (map fst cs)))

438− -- only sort the arguments where there is no clash in

443+ -- only sort the arguments where there is no clash in

444+ -- constructor tags between families, the argument type is canonical,

439− -- constructor tags between families, and no constructor/constant

445+ -- and no constructor/constant

440− -- clash, because otherwise we can't reliable make the

446+ -- clash, because otherwise we can't reliable make the

441− -- case distinction on evaluation

447+ -- case distinction on evaluation

442− (patnames_ord, patnames_rest)

448+ (patnames_ord, patnames_rest)

443− = Data.List.partition (noClash . map snd) patnames

449+ = Data.List.partition (noClash . map snd) patnames

444− -- note: sortBy . reverse is not nonsense because sortBy is stable

450+ patnames_ord' = case phase of

451+ CompileTime -> patnames_ord

452+ -- reversing tends to make better case trees

453+ -- and helps erasure

454+ RunTime -> reverse patnames_ord

445− pats' = transpose (sortBy moreDistinct (reverse patnames_ord)

455+ pats' = transpose (sortBy moreDistinct patnames_ord'

446− ++ patnames_rest) in

456+ ++ patnames_rest) in

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

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

448 where

458 where

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

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

450 getNOrder (c : _) = map (fst . fst) c

460 getNOrder (c : _) = map (fst . fst) c

451

461

452− rebuild patnames clause = (map snd patnames, snd clause)

462+ rebuild patnames clause = (map (snd . snd) patnames, snd clause)

453

463

454 noClash [] = True

464 noClash [] = True

455− noClash (p : ps) = not (any (clashPat p) ps) && noClash ps

465+ noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps))

466+ && noClash ps

456

467

457 clashPat (PCon _ _ _ _) (PConst _) = True

468 clashPat (PCon _ _ _ _) (PConst _) = True

458 clashPat (PConst _) (PCon _ _ _ _) = True

469 clashPat (PConst _) (PCon _ _ _ _) = True

@@ -462,12 +473,13 @@ order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

462 clashPat _ _ = False

473 clashPat _ _ = False

463

474

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

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

476+ moreDistinct xs ys

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

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

466− (snd . fst . head $ ys, numNames [] (map snd xs))

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

467

479

468− numNames xs (PCon _ n _ _ : ps)

480+ numNames xs ((_, PCon _ n _ _) : ps)

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

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

470− numNames xs (PConst c : ps)

482+ numNames xs ((_, PConst c) : ps)

471 | not (Right c `elem` xs) = numNames (Right c : xs) ps

483 | not (Right c `elem` xs) = numNames (Right c : xs) ps

472 numNames xs (_ : ps) = numNames xs ps

484 numNames xs (_ : ps) = numNames xs ps

473 numNames xs [] = length xs

485 numNames xs [] = length xs

src/Idris/Core/Evaluate.hs+13−3

@@ -21,7 +21,8 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

21 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

22 mapDefCtxt,

23 lookupTotal, lookupTotalExact, lookupInjectiveExact,

24− lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

24+ lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

25+ isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

25 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

26 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

26 isUniverse) where

27 isUniverse) where

@@ -697,7 +698,7 @@ data Def = Function !Type !Term

697 | Operator Type Int ([Value] -> Maybe Value)

698 | Operator Type Int ([Value] -> Maybe Value)

698 | CaseOp CaseInfo

699 | CaseOp CaseInfo

699 !Type

700 !Type

700− ![Type] -- argument types

701+ ![(Type, Bool)] -- argument types, whether canonical

701 ![Either Term (Term, Term)] -- original definition

702 ![Either Term (Term, Term)] -- original definition

702 ![([Name], Term, Term)] -- simplified for totality check definition

703 ![([Name], Term, Term)] -- simplified for totality check definition

703 !CaseDefs

704 !CaseDefs

@@ -915,7 +916,7 @@ addDatatype (Data n tag ty unique cons) uctxt

915addCasedef :: Name -> ErasureInfo -> CaseInfo ->

916addCasedef :: Name -> ErasureInfo -> CaseInfo ->

916 Bool -> SC -> -- default case

917 Bool -> SC -> -- default case

917 Bool -> Bool ->

918 Bool -> Bool ->

918− [Type] -> -- argument types

919+ [(Type, Bool)] -> -- argument types, whether canonical

919 [Int] -> -- inaccessible arguments

920 [Int] -> -- inaccessible arguments

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

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

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

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

@@ -1019,6 +1020,15 @@ lookupTy n ctxt = map snd (lookupTyName n ctxt)

1019lookupTyExact :: Name -> Context -> Maybe Type

1020lookupTyExact :: Name -> Context -> Maybe Type

1020lookupTyExact n ctxt = fmap snd (lookupTyNameExact n ctxt)

1021lookupTyExact n ctxt = fmap snd (lookupTyNameExact n ctxt)

1021

1022

1023+-- | Return true if the given type is a concrete type familyor primitive

1024+-- False it it's a function to compute a type or a variable

1025+isCanonical :: Type -> Context -> Bool

1026+isCanonical t ctxt

1027+ = case unApply t of

1028+ (P _ n _, _) -> isConName n ctxt

1029+ (Constant _, _) -> True

1030+ _ -> False

1031+

1022isConName :: Name -> Context -> Bool

1032isConName :: Name -> Context -> Bool

1023isConName n ctxt = isTConName n ctxt || isDConName n ctxt

1033isConName n ctxt = isTConName n ctxt || isDConName n ctxt

1024

1034

src/Idris/Elab/Clause.hs+2−1

@@ -84,7 +84,8 @@ elabClauses info' fc opts n_in cs =

84 -- question: CAFs in where blocks?

85 tclift $ tfail $ At fc (NoTypeDecl n)

86 [ty] -> return ty

87− let atys = map snd (getArgTys fty)

87+ let atys_in = map snd (getArgTys (normalise ctxt [] fty))

88+ let atys = map (\x -> (x, isCanonical x ctxt)) atys_in

88 cs_elab <- mapM (elabClause info opts)

89 cs_elab <- mapM (elabClause info opts)

89 (zip [0..] cs)

90 (zip [0..] cs)

90 ctxt <- getContext

91 ctxt <- getContext

src/Idris/Elab/Term.hs+3−1

@@ -1926,11 +1926,13 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

1926 in (ns, lhs', Impossible))

1927 clauses'

1928 let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''

1929+ let argtys = map (\x -> (x, isCanonical x ctxt))

1930+ (map snd (getArgTys (normalise ctxt [] ty)))

1929 ctxt'<- lift $

1931 ctxt'<- lift $

1930 addCasedef n (const [])

1932 addCasedef n (const [])

1931 info False (STerm Erased)

1933 info False (STerm Erased)

1932 True False -- TODO what are these?

1934 True False -- TODO what are these?

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

1935+ argtys [] -- TODO inaccessible types

1934 clauses'

1936 clauses'

1935 clauses'''

1937 clauses'''

1936 clauses'''

1938 clauses'''

src/Idris/IBC.hs+1−1

@@ -49,7 +49,7 @@ import Codec.Archive.Zip

49import Debug.Trace

51ibcVersion :: Word16

52−ibcVersion = 144

52+ibcVersion = 145

54-- | When IBC is being loaded - we'll load different things (and omit

55-- different structures/definitions) depending on which phase we're in.