a063bfa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some refactoring in CaseOp

a063bfaEdwin Brady13 years ago

src/Core/Evaluate.hs+45−22

compare with master

unifiedsplit

@@ -3,7 +3,7 @@

4module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

5 simplify, specialise, hnf, convEq, convEq',

6− Def(..), CaseInfo(..),

6+ Def(..), CaseInfo(..), CaseDefs(..),

7 Accessibility(..), Totality(..), PReason(..),

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,

@@ -186,9 +186,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

186 ev ntimes (n:stk) True env tm

187 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

188 return $ VP nt n vty

189− [(CaseOp ci _ _ _ [] tree _ _, acc)]

189+ [(CaseOp ci _ _ _ cd, acc)]

190+ | acc == Public &&

190− | acc == Public -> -- unoptimised version

191+ null (fst (cases_totcheck cd)) -> -- unoptimised version

192+ let (_, tree) = if simpl then cases_totcheck cd

193+ else cases_compiletime cd in

191− if blockSimplify ci n stk

194+ if blockSimplify ci n stk

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

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

193 else do c <- evCase ntimes n (n:stk) top env [] [] tree

196 else do c <- evCase ntimes n (n:stk) top env [] [] tree

194 case c of

197 case c of

@@ -256,9 +259,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

256 if u then

259 if u then

257 do let val = lookupDefAcc n atRepl ctxt

260 do let val = lookupDefAcc n atRepl ctxt

258 case val of

261 case val of

259− [(CaseOp ci _ _ _ ns tree _ _, acc)]

262+ [(CaseOp ci _ _ _ cd, acc)]

260 | acc == Public -> -- unoptimised version

263 | acc == Public -> -- unoptimised version

264+ let (ns, tree) = if simpl then cases_totcheck cd

265+ else cases_compiletime cd in

261− if blockSimplify ci n stk

266+ if blockSimplify ci n stk

262 then return $ unload env (VP Ref n ty) args

267 then return $ unload env (VP Ref n ty) args

263 else do c <- evCase ntimes n (n:stk) top env ns args tree

268 else do c <- evCase ntimes n (n:stk) top env ns args tree

264 case c of

269 case c of

@@ -488,9 +493,11 @@ convEq ctxt = ceq [] where

488 sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of

493 sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of

489 ([Function _ xdef], [Function _ ydef])

494 ([Function _ xdef], [Function _ ydef])

490 -> ceq ((x,y):ps) xdef ydef

495 -> ceq ((x,y):ps) xdef ydef

491− ([CaseOp _ _ _ _ _ xdef _ _],

496+ ([CaseOp _ _ _ _ xd],

492− [CaseOp _ _ _ _ _ ydef _ _])

497+ [CaseOp _ _ _ _ yd])

498+ -> let (_, xdef) = cases_compiletime xd

499+ (_, ydef) = cases_compiletime yd in

493− -> caseeq ((x,y):ps) xdef ydef

500+ caseeq ((x,y):ps) xdef ydef

494 _ -> return False

501 _ -> return False

495

502

496-- SPECIALISATION -----------------------------------------------------------

503-- SPECIALISATION -----------------------------------------------------------

@@ -514,9 +521,16 @@ data Def = Function Type Term

514 | CaseOp CaseInfo

521 | CaseOp CaseInfo

515 Type

522 Type

516 [Either Term (Term, Term)] -- original definition

523 [Either Term (Term, Term)] -- original definition

517− [([Name], Term, Term)] -- simplified definition

524+ [([Name], Term, Term)] -- simplified for totality check definition

525+ CaseDefs

518− [Name] SC -- Compile time case definition

526+-- [Name] SC -- Compile time case definition

519− [Name] SC -- Run time cae definitions

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+ }

520

534

521data CaseInfo = CaseInfo {

535data CaseInfo = CaseInfo {

522 case_inlinable :: Bool,

536 case_inlinable :: Bool,

@@ -526,13 +540,21 @@ data CaseInfo = CaseInfo {

526{-!

540{-!

527deriving instance Binary Def

541deriving instance Binary Def

528!-}

542!-}

543+{-!

544+deriving instance Binary CaseInfo

545+!-}

546+{-!

547+deriving instance Binary CaseDefs

548+!-}

529

549

530instance Show Def where

550instance Show Def where

531 show (Function ty tm) = "Function: " ++ show (ty, tm)

551 show (Function ty tm) = "Function: " ++ show (ty, tm)

532 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

552 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

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

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

534− show (CaseOp (CaseInfo inlc inlr) ty ps_in ps ns sc ns' sc')

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

535− = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

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

536 show ns ++ " " ++ show sc ++ "\n" ++

558 show ns ++ " " ++ show sc ++ "\n" ++

537 show ns' ++ " " ++ show sc' ++ "\n" ++

559 show ns' ++ " " ++ show sc' ++ "\n" ++

538 if inlc then "Inlinable\n" else "Not inlinable\n"

560 if inlc then "Inlinable\n" else "Not inlinable\n"

@@ -666,9 +688,10 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)

666 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

688 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

667 let inl = alwaysInline -- || tcdict

689 let inl = alwaysInline -- || tcdict

668 inlc = (inl || small n args sc') && (not asserted)

690 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

670 addDef n (CaseOp (ci { case_inlinable = inlc })

693 addDef n (CaseOp (ci { case_inlinable = inlc })

671− ty ps_in ps args sc args' sc',

694+ ty ps_in ps cdef,

672 access, Unchecked) ctxt in

695 access, Unchecked) ctxt in

673 uctxt { definitions = ctxt' }

696 uctxt { definitions = ctxt' }

674

697

@@ -676,15 +699,15 @@ simplifyCasedef :: Name -> Context -> Context

676simplifyCasedef n uctxt

699simplifyCasedef n uctxt

677 = let ctxt = definitions uctxt

700 = let ctxt = definitions uctxt

678 ctxt' = case lookupCtxt n ctxt of

701 ctxt' = case lookupCtxt n ctxt of

679− [(CaseOp ci ty [] ps args sc args' sc', acc, tot)] ->

702+ [(CaseOp ci ty [] ps _, acc, tot)] ->

680 ctxt -- nothing to simplify (or already done...)

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

682 let ps_in' = map simpl ps_in

705 let ps_in' = map simpl ps_in

683 pdef = map debind ps_in' in

706 pdef = map debind ps_in' in

684 case simpleCase False True False CompileTime (FC "" 0) pdef of

707 case simpleCase False True False CompileTime (FC "" 0) pdef of

685 OK (CaseDef args sc _) ->

708 OK (CaseDef args sc _) ->

686 addDef n (CaseOp ci

709 addDef n (CaseOp ci

687− ty ps_in' ps args sc args' sc',

710+ ty ps_in' ps (cd { cases_totcheck = (args, sc) }),

688 acc, tot) ctxt

711 acc, tot) ctxt

689 Error err -> error (show err)

712 Error err -> error (show err)

690 _ -> ctxt in

713 _ -> ctxt in

@@ -722,7 +745,7 @@ lookupTy n ctxt

722 (Function ty _) -> return ty

745 (Function ty _) -> return ty

723 (TyDecl _ ty) -> return ty

746 (TyDecl _ ty) -> return ty

724 (Operator ty _ _) -> return ty

747 (Operator ty _ _) -> return ty

725− (CaseOp _ ty _ _ _ _ _ _) -> return ty

748+ (CaseOp _ ty _ _ _) -> return ty

726

749

727isConName :: Name -> Context -> Bool

750isConName :: Name -> Context -> Bool

728isConName n ctxt

751isConName n ctxt

@@ -738,7 +761,7 @@ isFnName n ctxt

738 case tfst def of

761 case tfst def of

739 (Function _ _) -> return True

762 (Function _ _) -> return True

740 (Operator _ _ _) -> return True

763 (Operator _ _ _) -> return True

741− (CaseOp _ _ _ _ _ _ _ _) -> return True

764+ (CaseOp _ _ _ _ _) -> return True

742 _ -> return False

765 _ -> return False

743

766

744lookupP :: Name -> Context -> [Term]

767lookupP :: Name -> Context -> [Term]

@@ -747,7 +770,7 @@ lookupP n ctxt

747 p <- case def of

770 p <- case def of

748 (Function ty tm, a, _) -> return (P Ref n ty, a)

771 (Function ty tm, a, _) -> return (P Ref n ty, a)

749 (TyDecl nt ty, a, _) -> return (P nt n ty, a)

772 (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)

751 (Operator ty _ _, a, _) -> return (P Ref n ty, a)

774 (Operator ty _ _, a, _) -> return (P Ref n ty, a)

752 case snd p of

775 case snd p of

753 Hidden -> []

776 Hidden -> []

src/Core/Execute.hs+4−4

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

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

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

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

185 doExec env ctxt tm

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

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

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

188 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

189doExec env ctxt p@(P Bound n ty) =

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

315 execApp' env ctxt r (drop arity args)

316 Nothing -> return (mkEApp f args)

317 else return (mkEApp f args)

318− [CaseOp _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

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

319 do rhs <- doExec env ctxt tm

320 execApp' env ctxt rhs args

321− [CaseOp _ _ _ _ ns sc _ _] ->

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

322 do res <- execCase env ctxt ns sc args

323 return $ fromMaybe (mkEApp f args) res

324 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

159

160mkLDecl n (Function tm _) = do e <- ir tm

161 return (declArgs [] True n e)

162−mkLDecl n (CaseOp ci _ _ pats _ _ args sc)

162+mkLDecl n (CaseOp ci _ _ pats cd)

163+ = let (args, sc) = cases_runtime cd in

163− = do e <- ir (args, sc)

164+ do e <- ir (args, sc)

164 return (declArgs [] (case_inlinable ci) n e)

165 return (declArgs [] (case_inlinable ci) n e)

165mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a

166mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a

166mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

167mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

src/Idris/Coverage.hs+3−2

@@ -303,7 +303,7 @@ checkTotality path fc n

303 t' <- case t of

304 Unchecked ->

305 case lookupDef n ctxt of

306− [CaseOp _ _ _ pats _ _ _ _] ->

306+ [CaseOp _ _ _ pats _] ->

307 do t' <- if AssertTotal `elem` opts

308 then return $ Total []

309 else calcTotality path fc n pats

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

367 ist <- getIState

368 case lookupCtxt n (idris_callgraph ist) of

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

371 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"

372 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"

372 ++ show pats ++ "\n" ++ show sc

373 ++ show pats ++ "\n" ++ show sc

373 let newscg = buildSCG' ist (rights pats) args

374 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

649 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

650 i <- getIState

651 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

653 do let calls = findCalls sc' scargs'

655 do let calls = findCalls sc' scargs'

654 let used = findUsedArgs sc' scargs'

656 let used = findUsedArgs sc' scargs'

655 -- let scg = buildSCG i sc scargs

657 -- let scg = buildSCG i sc scargs

src/Idris/IBC.hs+19−15

@@ -23,7 +23,7 @@ import Debug.Trace

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 35

26+ibcVersion = 36

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -691,6 +691,17 @@ instance Binary CaseAlt where

691 return (FnCase x1 x2 x3)

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

693

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+

694instance Binary CaseInfo where

705instance Binary CaseInfo where

695 put x@(CaseInfo x1 x2) = do put x1

706 put x@(CaseInfo x1 x2) = do put x1

696 put x2

707 put x2

@@ -710,16 +721,12 @@ instance Binary Def where

710 put x2

721 put x2

711 -- all primitives just get added at the start, don't write

722 -- all primitives just get added at the start, don't write

712 Operator x1 x2 x3 -> do return ()

723 Operator x1 x2 x3 -> do return ()

713− CaseOp x1 x2 x3 x3a x4 x5 x6 x7 ->

724+ CaseOp x1 x2 x3 x3a x4 -> do putWord8 3

714− do putWord8 3

715− put x1

725+ put x1

716− put x2

726+ put x2

717− put x3

727+ put x3

718− -- no x3a

728+ -- no x3a

719− put x4

729+ put x4

720− put x5

721− put x6

722− put x7

723 get

730 get

724 = do i <- getWord8

731 = do i <- getWord8

725 case i of

732 case i of

@@ -738,10 +745,7 @@ instance Binary Def where

738 x3 <- get

745 x3 <- get

739 -- x3 <- get always []

746 -- x3 <- get always []

740 x4 <- get

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

745 _ -> error "Corrupted binary data for Def"

749 _ -> error "Corrupted binary data for Def"

746

750

747instance Binary Accessibility where

751instance 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 ""]

16-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

17getProvided :: 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

19 , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply result =

20 case err of

21 Constant (Str msg) -> ierror . ProviderError $ msg

22 _ -> 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

24 , (P _ (NS (UN "Provide") ["Providers"]) _, [_, res]) <- unApply result =

25 return res

26 | otherwise = fail $ "Internal type provider error: result was not " ++