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

git.iko.soy/Idris-dev

Remove unused case tree code

We now only need case trees for compile time and run time versions of a definition

commit521b8bf64b39163eb3b3ee8e8eee6be170ebe3a1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 17 Nov 2016, 14:56 (10 years ago) parentff01a4c

8 files changed+27−45

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−2 src/Idris/Core/Evaluate.hs+12−23 src/Idris/Core/Execute.hs+4−4 src/Idris/Coverage.hs+1−1 src/Idris/Elab/Clause.hs−2 src/Idris/Elab/Term.hs−2 src/Idris/IBC.hs+8−9 src/Idris/Prover.hs−2

src/Idris/AbsSyntax.hs+2−2

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

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

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

671671 pErase x = x

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

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

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

674− CaseDefs c' c' c' rs

674+ CaseDefs c' rs

675675

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

677677checkUndefined 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

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

272272 | otherwise = False

273273

274− getCases cd | simpl = cases_totcheck cd

274+ getCases cd | simpl = cases_compiletime cd

275275 | runtime = cases_runtime cd

276276 | otherwise = cases_compiletime cd

277277

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

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

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

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

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

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

297297 let (ns, tree) = getCases cd in

298298 if blockSimplify ci n stk

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

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

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

756756

757757data CaseDefs = CaseDefs {

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

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

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

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

762760 }

763761 deriving Generic

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

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

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

787785 = let (ns, sc) = cases_compiletime cd

788− (ns_t, sc_t) = cases_totcheck cd

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

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

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

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

793788 "COMPILE TIME:\n\n" ++

794789 show ns ++ " " ++ show sc ++ "\n\n" ++

795790 "RUN TIME:\n\n" ++

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

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

950945 [Int] -> -- inaccessible arguments

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

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

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

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

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

956949 Type -> Context -> TC Context

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

958951 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

960953 = do let ctxt = definitions uctxt

961954 access = case lookupDefAcc n False uctxt of

962955 [(_, acc)] -> acc

963956 _ -> Public

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

965957 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

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

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

969− (CaseDef args_tot sc_tot _,

970− CaseDef args_ct sc_ct _,

971− CaseDef args_inl sc_inl _,

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

960+ ( CaseDef args_ct sc_ct _,

972961 CaseDef args_rt sc_rt _) ->

973962 let inl = alwaysInline -- tcdict

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

975964 inlr = inl || small n args_rt sc_rt

976− cdef = CaseDefs (args_tot, sc_tot)

977− (args_ct, sc_ct)

978− (args_inl, sc_inl)

965+ cdef = CaseDefs (args_ct, sc_ct)

979966 (args_rt, sc_rt)

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

981− ty argtys ps_in ps_tot cdef,

968+ ty argtys ps_in ps_ct cdef,

982969 False, access, Unchecked, EmptyMI)

983970 in return $ addDef n op ctxt

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

985972 return uctxt { definitions = ctxt' }

986973

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)

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

989979simplifyCasedef n ei uctxt

990980 = do let ctxt = definitions uctxt

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

996986 pdef = map debind ps_in'

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

998988 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) }),

1001990 inj, acc, tot, metainf) ctxt

1002991

1003992 _ -> return ctxt

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

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

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

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

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

179179 doExec env ctxt tm

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

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

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

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

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

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

270270 execApp env ctxt r (drop arity args)

271271 _ -> return (mkEApp f args)

272272 else return (mkEApp f args)

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

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

274274 do rhs <- doExec env ctxt tm

275275 execApp env ctxt rhs args

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

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

277277 do res <- execCase env ctxt ns sc args

278278 return $ fromMaybe (mkEApp f args) res

279279 thing -> return $ mkEApp f args

src/Idris/Coverage.hs+1−1

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

604604 case lookupCtxt n (idris_callgraph ist) of

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

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

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

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

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

609609 ++ show pats ++ "\n" ++ show sc

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

240240 inacc

241241 pats_pe

242242 pdef

243− pdef -- compile time

244− pdef_inl -- inlined

245243 pdef' ty

246244 ctxt

247245 setContext ctxt'

src/Idris/Elab/Term.hs−2

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

19411941 clauses'

19421942 clauses'''

19431943 clauses'''

1944− clauses'''

1945− clauses'''

19461944 ty

19471945 ctxt

19481946 set_context ctxt'

src/Idris/IBC.hs+8−9

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

4747import System.FilePath

4848

4949ibcVersion :: Word16

50−ibcVersion = 152

50+ibcVersion = 153

5151

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

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

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

660660 r' <- update r

661661 return $ Right (l', r')

662662

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

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

664664 c' <- updateSC c

665665 r' <- updateSC r

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

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

667667

668668 updateSC (Case t n alts) = do

669669 alts' <- mapM updateAlt alts

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

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

10401040

10411041instance Binary CaseDefs where

1042− put (CaseDefs x1 x2 x3 x4)

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

1042+ put (CaseDefs x1 x2)

1043+ = do put x1

10441044 put x2

1045− put x4

10461045 get

1047− = do x2 <- get

1048− x4 <- get

1049− return (CaseDefs x2 x2 x2 x4)

1046+ = do x1 <- get

1047+ x2 <- get

1048+ return (CaseDefs x1 x2)

10501049

10511050instance Binary CaseInfo where

10521051 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

121121 [] [] -- argtys, inaccArgs

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

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

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

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

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

127125 ctxt

128126 setContext ctxt'