521b8bf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove unused case tree code

521b8bfEdwin Brady10 years ago

src/Idris/AbsSyntax.hs+2−2

compare with master

unifiedsplit

@@ -669,9 +669,9 @@ clearPTypes = do i <- get

669 where pErase (CaseOp c t tys orig tot cds)

670 = CaseOp c t tys orig [] (pErase' cds)

671 pErase x = x

672− pErase' (CaseDefs _ (cs, c) _ rs)

672+ pErase' (CaseDefs (cs, c) rs)

673 = let c' = (cs, fmap pEraseType c) in

674− CaseDefs c' c' c' rs

674+ CaseDefs c' rs

675

676checkUndefined :: FC -> Name -> Idris ()

677checkUndefined fc n

src/Idris/Core/Evaluate.hs+12−23

@@ -271,7 +271,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

271 || (n == sUN "prim__syntactic_eq")

272 | otherwise = False

273

274− getCases cd | simpl = cases_totcheck cd

274+ getCases cd | simpl = cases_compiletime cd

275 | runtime = cases_runtime cd

276 | otherwise = cases_compiletime cd

277

@@ -293,7 +293,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

293 [(CaseOp ci _ _ _ _ cd, acc)]

294 | (acc == Public || acc == Hidden) &&

295-- || sUN "assert_total" `elem` stk) &&

296− null (fst (cases_totcheck cd)) -> -- unoptimised version

296+ null (fst (cases_compiletime cd)) -> -- unoptimised version

297 let (ns, tree) = getCases cd in

298 if blockSimplify ci n stk

299 then liftM (VP Ref n) (ev ntimes stk top env ty)

@@ -755,9 +755,7 @@ data Def = Function !Type !Term

755-- [Name] SC -- Run time cae definitions

756

757data CaseDefs = CaseDefs {

758− cases_totcheck :: !([Name], SC),

759 cases_compiletime :: !([Name], SC),

758 cases_compiletime :: !([Name], SC),

760− cases_inlined :: !([Name], SC),

761 cases_runtime :: !([Name], SC)

759 cases_runtime :: !([Name], SC)

762 }

760 }

763 deriving Generic

761 deriving Generic

@@ -785,11 +783,8 @@ instance Show Def where

785 show (Operator ty _ _) = "Operator: " ++ show ty

783 show (Operator ty _ _) = "Operator: " ++ show ty

786 show (CaseOp (CaseInfo inlc inla inlr) ty atys ps_in ps cd)

784 show (CaseOp (CaseInfo inlc inla inlr) ty atys ps_in ps cd)

787 = let (ns, sc) = cases_compiletime cd

785 = let (ns, sc) = cases_compiletime cd

788− (ns_t, sc_t) = cases_totcheck cd

789 (ns', sc') = cases_runtime cd in

786 (ns', sc') = cases_runtime cd in

790 "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

787 "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

791− "TOTALITY CHECK TIME:\n\n" ++

792− show ns_t ++ " " ++ show sc_t ++ "\n\n" ++

793 "COMPILE TIME:\n\n" ++

788 "COMPILE TIME:\n\n" ++

794 show ns ++ " " ++ show sc ++ "\n\n" ++

789 show ns ++ " " ++ show sc ++ "\n\n" ++

795 "RUN TIME:\n\n" ++

790 "RUN TIME:\n\n" ++

@@ -949,42 +944,37 @@ addCasedef :: Name -> ErasureInfo -> CaseInfo ->

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

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

950 [Int] -> -- inaccessible arguments

945 [Int] -> -- inaccessible arguments

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

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

952− [([Name], Term, Term)] -> -- totality

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

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

954− [([Name], Term, Term)] -> -- inlined

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

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

956 Type -> Context -> TC Context

949 Type -> Context -> TC Context

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

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

958 tcase covering reflect asserted argtys inacc

951 tcase covering reflect asserted argtys inacc

959− ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

952+ ps_in ps_ct ps_rt ty uctxt

960 = do let ctxt = definitions uctxt

953 = do let ctxt = definitions uctxt

961 access = case lookupDefAcc n False uctxt of

954 access = case lookupDefAcc n False uctxt of

962 [(_, acc)] -> acc

955 [(_, acc)] -> acc

963 _ -> Public

956 _ -> Public

964− totalityTime <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot ei

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

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

966− inlined <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl ei

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

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

968− ctxt' <- case (totalityTime, compileTime, inlined, runtime) of

959+ ctxt' <- case (compileTime, runtime) of

969− (CaseDef args_tot sc_tot _,

970− CaseDef args_ct sc_ct _,

960+ ( CaseDef args_ct sc_ct _,

971− CaseDef args_inl sc_inl _,

972 CaseDef args_rt sc_rt _) ->

961 CaseDef args_rt sc_rt _) ->

973 let inl = alwaysInline -- tcdict

962 let inl = alwaysInline -- tcdict

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

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

975 inlr = inl || small n args_rt sc_rt

964 inlr = inl || small n args_rt sc_rt

976− cdef = CaseDefs (args_tot, sc_tot)

977− (args_ct, sc_ct)

965+ cdef = CaseDefs (args_ct, sc_ct)

978− (args_inl, sc_inl)

979 (args_rt, sc_rt)

966 (args_rt, sc_rt)

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

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

981− ty argtys ps_in ps_tot cdef,

968+ ty argtys ps_in ps_ct cdef,

982 False, access, Unchecked, EmptyMI)

969 False, access, Unchecked, EmptyMI)

983 in return $ addDef n op ctxt

970 in return $ addDef n op ctxt

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

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

985 return uctxt { definitions = ctxt' }

972 return uctxt { definitions = ctxt' }

986

973

987−-- simplify a definition for totality checking

974+-- simplify a definition by inlining

975+-- (Note: This used to be for totality checking, and now it's actually a

976+-- no-op, but I'm keeping it here because I'll be putting it back with some

977+-- more carefully controlled inlining at some stage. --- EB)

988simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context

978simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context

989simplifyCasedef n ei uctxt

979simplifyCasedef n ei uctxt

990 = do let ctxt = definitions uctxt

980 = do let ctxt = definitions uctxt

@@ -996,8 +986,7 @@ simplifyCasedef n ei uctxt

996 pdef = map debind ps_in'

986 pdef = map debind ps_in'

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

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

998 return $ addDef n (CaseOp ci

988 return $ addDef n (CaseOp ci

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

1000− cases_compiletime = (args, sc) }),

989+ ty atys ps_in' ps (cd { cases_compiletime = (args, sc) }),

1001 inj, acc, tot, metainf) ctxt

990 inj, acc, tot, metainf) ctxt

1002

991

1003 _ -> return ctxt

992 _ -> return ctxt

src/Idris/Core/Execute.hs+4−4

@@ -175,9 +175,9 @@ doExec env ctxt p@(P Ref n ty) =

175 [Function _ tm] -> doExec env ctxt tm

176 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def

177 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later

178− [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

178+ [CaseOp _ _ _ _ _ (CaseDefs ([], STerm tm) _)] -> -- nullary fun

179 doExec env ctxt tm

180− [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)

180+ [CaseOp _ _ _ _ _ (CaseDefs (ns, sc) _)] -> return (EP Ref n EErased)

181 [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."

182 other | length other > 1 -> execFail . Msg $ "Multiple definitions found for " ++ show n

183 | otherwise -> execFail . Msg . take 500 $ "got to " ++ show other ++ " lookup up " ++ show n

@@ -270,10 +270,10 @@ execApp env ctxt f@(EP _ n _) args =

270 execApp env ctxt r (drop arity args)

271 _ -> return (mkEApp f args)

272 else return (mkEApp f args)

273− [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

273+ [CaseOp _ _ _ _ _ (CaseDefs ([], STerm tm) _)] -> -- nullary fun

274 do rhs <- doExec env ctxt tm

275 execApp env ctxt rhs args

276− [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->

276+ [CaseOp _ _ _ _ _ (CaseDefs (ns, sc) _)] ->

277 do res <- execCase env ctxt ns sc args

278 return $ fromMaybe (mkEApp f args) res

279 thing -> return $ mkEApp f args

src/Idris/Coverage.hs+1−1

@@ -604,7 +604,7 @@ buildSCG (_, n) = do

604 case lookupCtxt n (idris_callgraph ist) of

605 [cg] -> case lookupDefExact n (tt_ctxt ist) of

606 Just (CaseOp _ _ _ pats _ cd) ->

607− let (args, sc) = cases_totcheck cd in

607+ let (args, sc) = cases_compiletime cd in

608 do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"

609 ++ show pats ++ "\n" ++ show sc

610 let newscg = buildSCG' ist n (rights pats) args

src/Idris/Elab/Clause.hs−2

@@ -240,8 +240,6 @@ elabClauses info' fc opts n_in cs =

240 inacc

241 pats_pe

242 pdef

243− pdef -- compile time

244− pdef_inl -- inlined

245 pdef' ty

243 pdef' ty

246 ctxt

244 ctxt

247 setContext ctxt'

245 setContext ctxt'

src/Idris/Elab/Term.hs−2

@@ -1941,8 +1941,6 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

1941 clauses'

1942 clauses'''

1943 clauses'''

1944− clauses'''

1945− clauses'''

1946 ty

1944 ty

1947 ctxt

1945 ctxt

1948 set_context ctxt'

1946 set_context ctxt'

src/Idris/IBC.hs+8−9

@@ -47,7 +47,7 @@ import System.Directory

47import System.FilePath

49ibcVersion :: Word16

50−ibcVersion = 152

50+ibcVersion = 153

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

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

@@ -660,10 +660,10 @@ processDefs ar = do

660 r' <- update r

661 return $ Right (l', r')

662

663− updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r)) = do

663+ updateCD (CaseDefs (cs, c) (rs, r)) = do

664 c' <- updateSC c

665 r' <- updateSC r

666− return $ CaseDefs (cs, c') (cs, c') (cs, c') (rs, r')

666+ return $ CaseDefs (cs, c') (rs, r')

667

668 updateSC (Case t n alts) = do

669 alts' <- mapM updateAlt alts

@@ -1039,14 +1039,13 @@ instance Binary CaseAlt where

1039 _ -> error "Corrupted binary data for CaseAlt"

1040

1041instance Binary CaseDefs where

1042− put (CaseDefs x1 x2 x3 x4)

1042+ put (CaseDefs x1 x2)

1043− = do -- don't need totality checked or inlined versions

1043+ = do put x1

1044 put x2

1045− put x4

1046 get

1045 get

1047− = do x2 <- get

1046+ = do x1 <- get

1048− x4 <- get

1047+ x2 <- get

1049− return (CaseDefs x2 x2 x2 x4)

1048+ return (CaseDefs x1 x2)

1050

1049

1051instance Binary CaseInfo where

1050instance Binary CaseInfo where

1052 put x@(CaseInfo x1 x2 x3) = do put x1

1051 put x@(CaseInfo x1 x2 x3) = do put x1

src/Idris/Prover.hs−2

@@ -121,8 +121,6 @@ prove mode info opt ctxt lit n ty

121 [] [] -- argtys, inaccArgs

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

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

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

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

126 [([], P Ref n ty, ptm')] ty

124 [([], P Ref n ty, ptm')] ty

127 ctxt

125 ctxt

128 setContext ctxt'

126 setContext ctxt'