7604451 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Cache argument types for building case trees

7604451Edwin Brady13 years ago

src/IRTS/Compiler.hs+1−1

compare with master

unifiedsplit

@@ -157,7 +157,7 @@ declArgs args inl n x = LFun (if inl then [Inline] else []) n args x

157

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

159 return (declArgs [] True n e)

160−mkLDecl n (CaseOp ci _ _ pats cd)

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

161 = let (args, sc) = cases_runtime cd in

162 do e <- ir (args, sc)

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

src/Idris/Core/CaseTree.hs+6−3

@@ -183,9 +183,10 @@ data Phase = CompileTime | RunTime

183-- Work Right to Left

184

185simpleCase :: Bool -> Bool -> Bool ->

186+ Phase -> FC -> [Type] ->

186− Phase -> FC -> [([Name], Term, Term)] ->

187+ [([Name], Term, Term)] ->

187 TC CaseDef

188 TC CaseDef

188−simpleCase tc cover reflect phase fc cs

189+simpleCase tc cover reflect phase fc argtys cs

189 = sc' tc cover phase fc (filter (\(_, _, r) ->

190 = sc' tc cover phase fc (filter (\(_, _, r) ->

190 case r of

191 case r of

191 Impossible -> False

192 Impossible -> False

@@ -205,7 +206,8 @@ simpleCase tc cover reflect phase fc cs

205 ns = take numargs args

206 ns = take numargs args

206 (ns', ps') = order ns pats

207 (ns', ps') = order ns pats

207 (tree, st) = runState

208 (tree, st) = runState

208− (match ns' ps' (defaultCase cover)) ([], numargs, [])

209+ (match ns' ps' (defaultCase cover))

210+ ([], numargs, [])

209 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in

211 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in

210 if proj then return (stripLambdas t)

212 if proj then return (stripLambdas t)

211 else if checkSameTypes (lstT st) tree

213 else if checkSameTypes (lstT st) tree

@@ -255,6 +257,7 @@ checkSameTypes _ _ = True

255-- at a specific constructor for a polymorphic argument. I *think* this

257-- at a specific constructor for a polymorphic argument. I *think* this

256-- is sufficient, but if it turns out not to be, fix it!

258-- is sufficient, but if it turns out not to be, fix it!

257isType n t | (P (TCon _ _) _ _, _) <- unApply t = True

259isType n t | (P (TCon _ _) _ _, _) <- unApply t = True

260+isType n t | (P Ref _ _, _) <- unApply t = True

258isType n t = False

261isType n t = False

259

262

260isConstType (I _) (AType (ATInt ITNative)) = True

263isConstType (I _) (AType (ATInt ITNative)) = True

src/Idris/Core/Evaluate.hs+22−20

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

211 ev ntimes (n:stk) True env tm

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

213 return $ VP nt n vty

214− [(CaseOp ci _ _ _ cd, acc)]

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

215 | (acc /= Frozen) &&

216 null (fst (cases_totcheck cd)) -> -- unoptimised version

217 let (ns, tree) = getCases cd in

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

284 reapply ntimes stk top env f@(VP Ref n ty) args

285 = let val = lookupDefAcc n (spec || atRepl) ctxt in

286 case val of

287− [(CaseOp ci _ _ _ cd, acc)] ->

287+ [(CaseOp ci _ _ _ _ cd, acc)] ->

288 let (ns, tree) = getCases cd in

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

290 case c of

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

310 if u then

311 do let val = lookupDefAcc n (spec || atRepl) ctxt

312 case val of

313− [(CaseOp ci _ _ _ cd, acc)]

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

314 | acc /= Frozen -> -- unoptimised version

315 let (ns, tree) = getCases cd in

316 if blockSimplify ci n stk

@@ -561,8 +561,8 @@ convEq ctxt = ceq [] where

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

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

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

564− ([CaseOp _ _ _ _ xd],

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

565− [CaseOp _ _ _ _ yd])

565+ [CaseOp _ _ _ _ _ yd])

566 -> let (_, xdef) = cases_compiletime xd

567 (_, ydef) = cases_compiletime yd in

568 caseeq ((x,y):ps) xdef ydef

@@ -588,6 +588,7 @@ data Def = Function !Type !Term

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

589 | CaseOp CaseInfo

590 !Type

591+ ![Type] -- argument types

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

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

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

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

593 !CaseDefs

594 !CaseDefs

@@ -620,7 +621,7 @@ instance Show Def where

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

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

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

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

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

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

623− show (CaseOp (CaseInfo inlc inlr) ty ps_in ps cd)

624+ show (CaseOp (CaseInfo inlc inlr) ty atys ps_in ps cd)

624 = let (ns, sc) = cases_compiletime cd

625 = let (ns, sc) = cases_compiletime cd

625 (ns_t, sc_t) = cases_totcheck cd

626 (ns_t, sc_t) = cases_totcheck cd

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

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

@@ -752,6 +753,7 @@ addDatatype (Data n tag ty cons) uctxt

752

753

753-- FIXME: Too many arguments! Refactor all these Bools.

754-- FIXME: Too many arguments! Refactor all these Bools.

754addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

755addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

756+ [Type] -> -- argument types

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

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

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

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

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

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

@@ -759,16 +761,16 @@ addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

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

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

760 Type -> Context -> Context

762 Type -> Context -> Context

761addCasedef n ci@(CaseInfo alwaysInline tcdict)

763addCasedef n ci@(CaseInfo alwaysInline tcdict)

762− tcase covering reflect asserted ps_in

764+ tcase covering reflect asserted argtys

763− ps_tot ps_inl ps_ct ps_rt ty uctxt

765+ ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

764 = let ctxt = definitions uctxt

766 = let ctxt = definitions uctxt

765 access = case lookupDefAcc n False uctxt of

767 access = case lookupDefAcc n False uctxt of

766 [(_, acc)] -> acc

768 [(_, acc)] -> acc

767 _ -> Public

769 _ -> Public

768− ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC ps_tot,

770+ ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC argtys ps_tot,

769− simpleCase tcase covering reflect CompileTime emptyFC ps_ct,

771+ simpleCase tcase covering reflect CompileTime emptyFC argtys ps_ct,

770− simpleCase tcase covering reflect CompileTime emptyFC ps_inl,

772+ simpleCase tcase covering reflect CompileTime emptyFC argtys ps_inl,

771− simpleCase tcase covering reflect RunTime emptyFC ps_rt) of

773+ simpleCase tcase covering reflect RunTime emptyFC argtys ps_rt) of

772 (OK (CaseDef args_tot sc_tot _),

774 (OK (CaseDef args_tot sc_tot _),

773 OK (CaseDef args_ct sc_ct _),

775 OK (CaseDef args_ct sc_ct _),

774 OK (CaseDef args_inl sc_inl _),

776 OK (CaseDef args_inl sc_inl _),

@@ -781,7 +783,7 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)

781 (args_inl, sc_inl)

783 (args_inl, sc_inl)

782 (args_rt, sc_rt) in

784 (args_rt, sc_rt) in

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

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

784− ty ps_in ps_tot cdef,

786+ ty argtys ps_in ps_tot cdef,

785 access, Unchecked, EmptyMI) ctxt in

787 access, Unchecked, EmptyMI) ctxt in

786 uctxt { definitions = ctxt' }

788 uctxt { definitions = ctxt' }

787

789

@@ -790,15 +792,15 @@ simplifyCasedef :: Name -> Context -> Context

790simplifyCasedef n uctxt

792simplifyCasedef n uctxt

791 = let ctxt = definitions uctxt

793 = let ctxt = definitions uctxt

792 ctxt' = case lookupCtxt n ctxt of

794 ctxt' = case lookupCtxt n ctxt of

793− [(CaseOp ci ty [] ps _, acc, tot, metainf)] ->

795+ [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->

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

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

795− [(CaseOp ci ty ps_in ps cd, acc, tot, metainf)] ->

797+ [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->

796 let ps_in' = map simpl ps_in

798 let ps_in' = map simpl ps_in

797 pdef = map debind ps_in' in

799 pdef = map debind ps_in' in

798− case simpleCase False True False CompileTime emptyFC pdef of

800+ case simpleCase False True False CompileTime emptyFC atys pdef of

799 OK (CaseDef args sc _) ->

801 OK (CaseDef args sc _) ->

800 addDef n (CaseOp ci

802 addDef n (CaseOp ci

801− ty ps_in' ps (cd { cases_totcheck = (args, sc) }),

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

802 acc, tot, metainf) ctxt

804 acc, tot, metainf) ctxt

803 Error err -> error (show err)

805 Error err -> error (show err)

804 _ -> ctxt in

806 _ -> ctxt in

@@ -836,7 +838,7 @@ lookupTy n ctxt

836 (Function ty _) -> return ty

838 (Function ty _) -> return ty

837 (TyDecl _ ty) -> return ty

839 (TyDecl _ ty) -> return ty

838 (Operator ty _ _) -> return ty

840 (Operator ty _ _) -> return ty

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

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

840

842

841isConName :: Name -> Context -> Bool

843isConName :: Name -> Context -> Bool

842isConName n ctxt = isTConName n ctxt || isDConName n ctxt

844isConName n ctxt = isTConName n ctxt || isDConName n ctxt

@@ -861,7 +863,7 @@ isFnName n ctxt

861 case tfst def of

863 case tfst def of

862 (Function _ _) -> return True

864 (Function _ _) -> return True

863 (Operator _ _ _) -> return True

865 (Operator _ _ _) -> return True

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

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

865 _ -> return False

867 _ -> return False

866

868

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

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

@@ -870,7 +872,7 @@ lookupP n ctxt

870 p <- case def of

872 p <- case def of

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

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

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

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

873− (CaseOp _ ty _ _ _, a, _, _) -> return (P Ref n ty, a)

875+ (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

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

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

875 case snd p of

877 case snd p of

876 Hidden -> []

878 Hidden -> []

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

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

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

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

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

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

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

192 doExec env ctxt tm

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

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

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

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

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

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

328 execApp' env ctxt r (drop arity args)

329 Nothing -> return (mkEApp f args)

330 else return (mkEApp f args)

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

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

332 do rhs <- doExec env ctxt tm

333 execApp' env ctxt rhs args

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

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

335 do res <- execCase env ctxt ns sc args

336 return $ fromMaybe (mkEApp f args) res

337 thing -> return $ mkEApp f args

src/Idris/Coverage.hs+2−2

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

325 t' <- case t of

326 Unchecked ->

327 case lookupDef n ctxt of

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

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

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

330 then return $ Total []

331 else calcTotality path fc n pats

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

389 ist <- getIState

390 case lookupCtxt n (idris_callgraph ist) of

391 [cg] -> case lookupDef n (tt_ctxt ist) of

392− [CaseOp _ _ pats _ cd] ->

392+ [CaseOp _ _ _ pats _ cd] ->

393 let (args, sc) = cases_totcheck cd in

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

395 ++ show pats ++ "\n" ++ show sc

src/Idris/ElabDecls.hs+4−3

@@ -906,7 +906,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

906

907 let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats

908 tree@(CaseDef scargs sc _) <- tclift $

909− simpleCase tcase False reflect CompileTime fc pdef

909+ simpleCase tcase False reflect CompileTime fc atys pdef

910 cov <- coverage

911 pmissing <-

912 if cov

@@ -954,7 +954,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

954 let knowncovering = (pcover && cov) || AssertTotal `elem` opts

955

956 tree' <- tclift $ simpleCase tcase knowncovering reflect

957− RunTime fc pdef'

957+ RunTime fc atys pdef'

958 logLvl 3 (show tree)

959 logLvl 3 $ "Optimised: " ++ show tree'

960 ctxt <- getContext

@@ -967,6 +967,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

967 tcase knowncovering

968 reflect

969 (AssertTotal `elem` opts)

970+ atys

970 pats

971 pats

971 pdef pdef pdef_inl pdef' ty)

972 pdef pdef pdef_inl pdef' ty)

972 addIBC (IBCDef n)

973 addIBC (IBCDef n)

@@ -976,7 +977,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

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

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

977 i <- getIState

978 i <- getIState

978 case lookupDef n (tt_ctxt i) of

979 case lookupDef n (tt_ctxt i) of

979− (CaseOp _ _ _ _ cd : _) ->

980+ (CaseOp _ _ _ _ _ cd : _) ->

980 let (scargs, sc) = cases_compiletime cd

981 let (scargs, sc) = cases_compiletime cd

981 (scargs', sc') = cases_runtime cd in

982 (scargs', sc') = cases_runtime cd in

982 do let calls = findCalls sc' scargs'

983 do let calls = findCalls sc' scargs'

src/Idris/IBC.hs+11−9

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

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 49

26+ibcVersion = 50

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -801,12 +801,13 @@ instance Binary Def where

801 put x2

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

803 Operator x1 x2 x3 -> do return ()

804− CaseOp x1 x2 x3 x3a x4 -> do putWord8 3

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

805− put x1

805+ put x1

806− put x2

806+ put x2

807− put x3

807+ put x2a

808+ put x3

808− -- no x3a

809+ -- no x3a

809− put x4

810+ put x4

810 get

811 get

811 = do i <- getWord8

812 = do i <- getWord8

812 case i of

813 case i of

@@ -820,9 +821,10 @@ instance Binary Def where

820 3 -> do x1 <- get

821 3 -> do x1 <- get

821 x2 <- get

822 x2 <- get

822 x3 <- get

823 x3 <- get

823− -- x3 <- get always []

824 x4 <- get

825+ -- x3 <- get always []

826+ x5 <- get

825− return (CaseOp x1 x2 x3 [] x4)

827+ return (CaseOp x1 x2 x3 x4 [] x5)

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

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

827

829

828instance Binary Accessibility where

830instance Binary Accessibility where

src/Idris/Prover.hs+2−1

@@ -65,7 +65,7 @@ prove ctxt lit n ty

65 ideslavePutSExp "end-proof-mode" n

66 let proofs = proof_list i

67 putIState (i { proof_list = (n, prf) : proofs })

68− let tree = simpleCase False True False CompileTime (fileFC "proof") [([], P Ref n ty, tm)]

68+ let tree = simpleCase False True False CompileTime (fileFC "proof") [] [([], P Ref n ty, tm)]

69 logLvl 3 (show tree)

70 (ptm, pty) <- recheckC (fileFC "proof") [] tm

71 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

@@ -75,6 +75,7 @@ prove ctxt lit n ty

75 Error e -> ierror (CantUnify False ty pty e [] 0)

76 ptm' <- applyOpts ptm

77 updateContext (addCasedef n (CaseInfo True False) False False True False

78+ []

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

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

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

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

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