git.iko.soy/Idris-dev
on master help sign in
Some refactoring in CaseOp

Separate case trees for totality checking, compile time and run time and lift into their own data structure, so that it's clear which one to use when. Needs a "make relib"

commita063bfa434ecea382c9b6f55dfecab4d051c4e01 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 4 Sep 2013, 16:55 (13 years ago) parent77f9051
7 files changed+79−48
compare with master
unifiedsplit
src/Core/Evaluate.hs+45−22 src/Core/Execute.hs+4−4 src/IRTS/Compiler.hs+3−2 src/Idris/Coverage.hs+3−2 src/Idris/ElabDecls.hs+3−1 src/Idris/IBC.hs+19−15 src/Idris/Providers.hs+2−2
src/Core/Evaluate.hs+45−22
@@ -3,7 +3,7 @@
33
44module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
55 simplify, specialise, hnf, convEq, convEq',
6− Def(..), CaseInfo(..),
6+ Def(..), CaseInfo(..), CaseDefs(..),
77 Accessibility(..), Totality(..), PReason(..),
88 Context, initContext, ctxtAlist, uconstraints, next_tvar,
99 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,
@@ -186,9 +186,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
186186 ev ntimes (n:stk) True env tm
187187 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
188188 return $ VP nt n vty
189− [(CaseOp ci _ _ _ [] tree _ _, acc)]
190− | acc == Public -> -- unoptimised version
191− if blockSimplify ci n stk
189+ [(CaseOp ci _ _ _ cd, acc)]
190+ | acc == Public &&
191+ null (fst (cases_totcheck cd)) -> -- unoptimised version
192+ let (_, tree) = if simpl then cases_totcheck cd
193+ else cases_compiletime cd in
194+ if blockSimplify ci n stk
192195 then liftM (VP Ref n) (ev ntimes stk top env ty)
193196 else do c <- evCase ntimes n (n:stk) top env [] [] tree
194197 case c of
@@ -256,9 +259,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
256259 if u then
257260 do let val = lookupDefAcc n atRepl ctxt
258261 case val of
259− [(CaseOp ci _ _ _ ns tree _ _, acc)]
262+ [(CaseOp ci _ _ _ cd, acc)]
260263 | acc == Public -> -- unoptimised version
261− if blockSimplify ci n stk
264+ let (ns, tree) = if simpl then cases_totcheck cd
265+ else cases_compiletime cd in
266+ if blockSimplify ci n stk
262267 then return $ unload env (VP Ref n ty) args
263268 else do c <- evCase ntimes n (n:stk) top env ns args tree
264269 case c of
@@ -488,9 +493,11 @@ convEq ctxt = ceq [] where
488493 sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of
489494 ([Function _ xdef], [Function _ ydef])
490495 -> ceq ((x,y):ps) xdef ydef
491− ([CaseOp _ _ _ _ _ xdef _ _],
492− [CaseOp _ _ _ _ _ ydef _ _])
493− -> caseeq ((x,y):ps) xdef ydef
496+ ([CaseOp _ _ _ _ xd],
497+ [CaseOp _ _ _ _ yd])
498+ -> let (_, xdef) = cases_compiletime xd
499+ (_, ydef) = cases_compiletime yd in
500+ caseeq ((x,y):ps) xdef ydef
494501 _ -> return False
495502
496503-- SPECIALISATION -----------------------------------------------------------
@@ -514,9 +521,16 @@ data Def = Function Type Term
514521 | CaseOp CaseInfo
515522 Type
516523 [Either Term (Term, Term)] -- original definition
517− [([Name], Term, Term)] -- simplified definition
518− [Name] SC -- Compile time case definition
519− [Name] SC -- Run time cae definitions
524+ [([Name], Term, Term)] -- simplified for totality check definition
525+ CaseDefs
526+-- [Name] SC -- Compile time case definition
527+-- [Name] SC -- Run time cae definitions
528+
529+data CaseDefs = CaseDefs {
530+ cases_totcheck :: ([Name], SC),
531+ cases_compiletime :: ([Name], SC),
532+ cases_runtime :: ([Name], SC)
533+ }
520534
521535data CaseInfo = CaseInfo {
522536 case_inlinable :: Bool,
@@ -526,13 +540,21 @@ data CaseInfo = CaseInfo {
526540{-!
527541deriving instance Binary Def
528542!-}
543+{-!
544+deriving instance Binary CaseInfo
545+!-}
546+{-!
547+deriving instance Binary CaseDefs
548+!-}
529549
530550instance Show Def where
531551 show (Function ty tm) = "Function: " ++ show (ty, tm)
532552 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
533553 show (Operator ty _ _) = "Operator: " ++ show ty
534− show (CaseOp (CaseInfo inlc inlr) ty ps_in ps ns sc ns' sc')
535− = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
554+ show (CaseOp (CaseInfo inlc inlr) ty ps_in ps cd)
555+ = let (ns, sc) = cases_compiletime cd
556+ (ns', sc') = cases_runtime cd in
557+ "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
536558 show ns ++ " " ++ show sc ++ "\n" ++
537559 show ns' ++ " " ++ show sc' ++ "\n" ++
538560 if inlc then "Inlinable\n" else "Not inlinable\n"
@@ -666,9 +688,10 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)
666688 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
667689 let inl = alwaysInline -- || tcdict
668690 inlc = (inl || small n args sc') && (not asserted)
669− inlr = inl || small n args sc' in
691+ inlr = inl || small n args sc'
692+ cdef = CaseDefs (args, sc) (args, sc) (args', sc') in
670693 addDef n (CaseOp (ci { case_inlinable = inlc })
671− ty ps_in ps args sc args' sc',
694+ ty ps_in ps cdef,
672695 access, Unchecked) ctxt in
673696 uctxt { definitions = ctxt' }
674697
@@ -676,15 +699,15 @@ simplifyCasedef :: Name -> Context -> Context
676699simplifyCasedef n uctxt
677700 = let ctxt = definitions uctxt
678701 ctxt' = case lookupCtxt n ctxt of
679− [(CaseOp ci ty [] ps args sc args' sc', acc, tot)] ->
702+ [(CaseOp ci ty [] ps _, acc, tot)] ->
680703 ctxt -- nothing to simplify (or already done...)
681− [(CaseOp ci ty ps_in ps args sc args' sc', acc, tot)] ->
704+ [(CaseOp ci ty ps_in ps cd, acc, tot)] ->
682705 let ps_in' = map simpl ps_in
683706 pdef = map debind ps_in' in
684707 case simpleCase False True False CompileTime (FC "" 0) pdef of
685708 OK (CaseDef args sc _) ->
686709 addDef n (CaseOp ci
687− ty ps_in' ps args sc args' sc',
710+ ty ps_in' ps (cd { cases_totcheck = (args, sc) }),
688711 acc, tot) ctxt
689712 Error err -> error (show err)
690713 _ -> ctxt in
@@ -722,7 +745,7 @@ lookupTy n ctxt
722745 (Function ty _) -> return ty
723746 (TyDecl _ ty) -> return ty
724747 (Operator ty _ _) -> return ty
725− (CaseOp _ ty _ _ _ _ _ _) -> return ty
748+ (CaseOp _ ty _ _ _) -> return ty
726749
727750isConName :: Name -> Context -> Bool
728751isConName n ctxt
@@ -738,7 +761,7 @@ isFnName n ctxt
738761 case tfst def of
739762 (Function _ _) -> return True
740763 (Operator _ _ _) -> return True
741− (CaseOp _ _ _ _ _ _ _ _) -> return True
764+ (CaseOp _ _ _ _ _) -> return True
742765 _ -> return False
743766
744767lookupP :: Name -> Context -> [Term]
@@ -747,7 +770,7 @@ lookupP n ctxt
747770 p <- case def of
748771 (Function ty tm, a, _) -> return (P Ref n ty, a)
749772 (TyDecl nt ty, a, _) -> return (P nt n ty, a)
750− (CaseOp _ ty _ _ _ _ _ _, a, _) -> return (P Ref n ty, a)
773+ (CaseOp _ ty _ _ _, a, _) -> return (P Ref n ty, a)
751774 (Operator ty _ _, a, _) -> return (P Ref n ty, a)
752775 case snd p of
753776 Hidden -> []
src/Core/Execute.hs+4−4
@@ -181,9 +181,9 @@ doExec env ctxt p@(P Ref n ty) =
181181 [Function _ tm] -> doExec env ctxt tm
182182 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
183183 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
184− [CaseOp _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
184+ [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _)] -> -- nullary fun
185185 doExec env ctxt tm
186− [CaseOp _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)
186+ [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _)] -> return (EP Ref n EErased)
187187 [] -> execFail $ "Could not find " ++ show n ++ " in definitions."
188188 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
189189doExec env ctxt p@(P Bound n ty) =
@@ -315,10 +315,10 @@ execApp' env ctxt f@(EP _ n _) args =
315315 execApp' env ctxt r (drop arity args)
316316 Nothing -> return (mkEApp f args)
317317 else return (mkEApp f args)
318− [CaseOp _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
318+ [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _)] -> -- nullary fun
319319 do rhs <- doExec env ctxt tm
320320 execApp' env ctxt rhs args
321− [CaseOp _ _ _ _ ns sc _ _] ->
321+ [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _)] ->
322322 do res <- execCase env ctxt ns sc args
323323 return $ fromMaybe (mkEApp f args) res
324324 thing -> return $ mkEApp f args
src/IRTS/Compiler.hs+3−2
@@ -159,8 +159,9 @@ declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
159159
160160mkLDecl n (Function tm _) = do e <- ir tm
161161 return (declArgs [] True n e)
162−mkLDecl n (CaseOp ci _ _ pats _ _ args sc)
163− = do e <- ir (args, sc)
162+mkLDecl n (CaseOp ci _ _ pats cd)
163+ = let (args, sc) = cases_runtime cd in
164+ do e <- ir (args, sc)
164165 return (declArgs [] (case_inlinable ci) n e)
165166mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
166167mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
src/Idris/Coverage.hs+3−2
@@ -303,7 +303,7 @@ checkTotality path fc n
303303 t' <- case t of
304304 Unchecked ->
305305 case lookupDef n ctxt of
306− [CaseOp _ _ _ pats _ _ _ _] ->
306+ [CaseOp _ _ _ pats _] ->
307307 do t' <- if AssertTotal `elem` opts
308308 then return $ Total []
309309 else calcTotality path fc n pats
@@ -367,7 +367,8 @@ buildSCG (_, n) = do
367367 ist <- getIState
368368 case lookupCtxt n (idris_callgraph ist) of
369369 [cg] -> case lookupDef n (tt_ctxt ist) of
370− [CaseOp _ _ pats _ args sc _ _] ->
370+ [CaseOp _ _ pats _ cd] ->
371+ let (args, sc) = cases_totcheck cd in
371372 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
372373 ++ show pats ++ "\n" ++ show sc
373374 let newscg = buildSCG' ist (rights pats) args
src/Idris/ElabDecls.hs+3−1
@@ -649,7 +649,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
649649 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
650650 i <- getIState
651651 case lookupDef n (tt_ctxt i) of
652− (CaseOp _ _ _ _ scargs sc scargs' sc' : _) ->
652+ (CaseOp _ _ _ _ cd : _) ->
653+ let (scargs, sc) = cases_compiletime cd
654+ (scargs', sc') = cases_runtime cd in
653655 do let calls = findCalls sc' scargs'
654656 let used = findUsedArgs sc' scargs'
655657 -- let scg = buildSCG i sc scargs
src/Idris/IBC.hs+19−15
@@ -23,7 +23,7 @@ import Debug.Trace
2323import Paths_idris
2424
2525ibcVersion :: Word8
26−ibcVersion = 35
26+ibcVersion = 36
2727
2828data IBCFile = IBCFile { ver :: Word8,
2929 sourcefile :: FilePath,
@@ -691,6 +691,17 @@ instance Binary CaseAlt where
691691 return (FnCase x1 x2 x3)
692692 _ -> error "Corrupted binary data for CaseAlt"
693693
694+instance Binary CaseDefs where
695+ put (CaseDefs x1 x2 x3)
696+ = do put x1
697+ put x2
698+ put x3
699+ get
700+ = do x1 <- get
701+ x2 <- get
702+ x3 <- get
703+ return (CaseDefs x1 x2 x3)
704+
694705instance Binary CaseInfo where
695706 put x@(CaseInfo x1 x2) = do put x1
696707 put x2
@@ -710,16 +721,12 @@ instance Binary Def where
710721 put x2
711722 -- all primitives just get added at the start, don't write
712723 Operator x1 x2 x3 -> do return ()
713− CaseOp x1 x2 x3 x3a x4 x5 x6 x7 ->
714− do putWord8 3
715− put x1
716− put x2
717− put x3
718− -- no x3a
719− put x4
720− put x5
721− put x6
722− put x7
724+ CaseOp x1 x2 x3 x3a x4 -> do putWord8 3
725+ put x1
726+ put x2
727+ put x3
728+ -- no x3a
729+ put x4
723730 get
724731 = do i <- getWord8
725732 case i of
@@ -738,10 +745,7 @@ instance Binary Def where
738745 x3 <- get
739746 -- x3 <- get always []
740747 x4 <- get
741− x5 <- get
742− x6 <- get
743− x7 <- get
744− return (CaseOp x1 x2 x3 [] x4 x5 x6 x7)
748+ return (CaseOp x1 x2 x3 [] x4)
745749 _ -> error "Corrupted binary data for Def"
746750
747751instance Binary Accessibility where
src/Idris/Providers.hs+2−2
@@ -15,12 +15,12 @@ providerTy fc tm = PApp fc (PRef fc $ UN "Provider") [PExp 0 False tm ""]
1515
1616-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.
1717getProvided :: TT Name -> Idris (TT Name)
18−getProvided tm | (P _ (UN "prim__IO") _, [tp, result]) <- unApply tm
18+getProvided tm | (P _ (UN "prim_io_return") _, [tp, result]) <- unApply tm
1919 , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply result =
2020 case err of
2121 Constant (Str msg) -> ierror . ProviderError $ msg
2222 _ -> fail "Internal error in type provider, non-normalised error"
23− | (P _ (UN "prim__IO") _, [tp, result]) <- unApply tm
23+ | (P _ (UN "prim_io_return") _, [tp, result]) <- unApply tm
2424 , (P _ (NS (UN "Provide") ["Providers"]) _, [_, res]) <- unApply result =
2525 return res
2626 | otherwise = fail $ "Internal type provider error: result was not " ++