7604451 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Cache argument types for building case trees

commit7604451ca41113cb4dec966319d4f4c4add90fe0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 12 Jan 2014, 01:04 (13 years ago) parent7e885b3

8 files changed+52−43

compare with master

unifiedsplit

src/IRTS/Compiler.hs+1−1 src/Idris/Core/CaseTree.hs+6−3 src/Idris/Core/Evaluate.hs+22−20 src/Idris/Core/Execute.hs+4−4 src/Idris/Coverage.hs+2−2 src/Idris/ElabDecls.hs+4−3 src/Idris/IBC.hs+11−9 src/Idris/Prover.hs+2−1

src/IRTS/Compiler.hs+1−1

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

157157

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

159159 return (declArgs [] True n e)

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

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

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

162162 do e <- ir (args, sc)

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

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

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

183183-- Work Right to Left

184184

185185simpleCase :: Bool -> Bool -> Bool ->

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

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

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

187188 TC CaseDef

188−simpleCase tc cover reflect phase fc cs

189+simpleCase tc cover reflect phase fc argtys cs

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

190191 case r of

191192 Impossible -> False

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

205206 ns = take numargs args

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

207208 (tree, st) = runState

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

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

210+ ([], numargs, [])

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

210212 if proj then return (stripLambdas t)

211213 else if checkSameTypes (lstT st) tree

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

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

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

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

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

258261isType n t = False

259262

260263isConstType (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

211211 ev ntimes (n:stk) True env tm

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

213213 return $ VP nt n vty

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

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

215215 | (acc /= Frozen) &&

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

217217 let (ns, tree) = getCases cd in

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

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

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

286286 case val of

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

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

288288 let (ns, tree) = getCases cd in

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

290290 case c of

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

310310 if u then

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

312312 case val of

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

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

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

315315 let (ns, tree) = getCases cd in

316316 if blockSimplify ci n stk

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

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

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

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

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

565− [CaseOp _ _ _ _ yd])

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

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

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

567567 (_, ydef) = cases_compiletime yd in

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

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

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

589589 | CaseOp CaseInfo

590590 !Type

591+ ![Type] -- argument types

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

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

593594 !CaseDefs

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

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

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

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

624625 = let (ns, sc) = cases_compiletime cd

625626 (ns_t, sc_t) = cases_totcheck cd

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

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

752753

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

754755addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

756+ [Type] -> -- argument types

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

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

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

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

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

760762 Type -> Context -> Context

761763addCasedef n ci@(CaseInfo alwaysInline tcdict)

762− tcase covering reflect asserted ps_in

763− ps_tot ps_inl ps_ct ps_rt ty uctxt

764+ tcase covering reflect asserted argtys

765+ ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

764766 = let ctxt = definitions uctxt

765767 access = case lookupDefAcc n False uctxt of

766768 [(_, acc)] -> acc

767769 _ -> Public

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

769− simpleCase tcase covering reflect CompileTime emptyFC ps_ct,

770− simpleCase tcase covering reflect CompileTime emptyFC ps_inl,

771− simpleCase tcase covering reflect RunTime emptyFC ps_rt) of

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

771+ simpleCase tcase covering reflect CompileTime emptyFC argtys ps_ct,

772+ simpleCase tcase covering reflect CompileTime emptyFC argtys ps_inl,

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

772774 (OK (CaseDef args_tot sc_tot _),

773775 OK (CaseDef args_ct sc_ct _),

774776 OK (CaseDef args_inl sc_inl _),

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

781783 (args_inl, sc_inl)

782784 (args_rt, sc_rt) in

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

784− ty ps_in ps_tot cdef,

786+ ty argtys ps_in ps_tot cdef,

785787 access, Unchecked, EmptyMI) ctxt in

786788 uctxt { definitions = ctxt' }

787789

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

790792simplifyCasedef n uctxt

791793 = let ctxt = definitions uctxt

792794 ctxt' = case lookupCtxt n ctxt of

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

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

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

796798 let ps_in' = map simpl ps_in

797799 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

799801 OK (CaseDef args sc _) ->

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

802804 acc, tot, metainf) ctxt

803805 Error err -> error (show err)

804806 _ -> ctxt in

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

836838 (Function ty _) -> return ty

837839 (TyDecl _ ty) -> return ty

838840 (Operator ty _ _) -> return ty

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

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

840842

841843isConName :: Name -> Context -> Bool

842844isConName n ctxt = isTConName n ctxt || isDConName n ctxt

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

861863 case tfst def of

862864 (Function _ _) -> return True

863865 (Operator _ _ _) -> return True

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

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

865867 _ -> return False

866868

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

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

870872 p <- case def of

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

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

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

875877 case snd p of

876878 Hidden -> []

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

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

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

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

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

192192 doExec env ctxt tm

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

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

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

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

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

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

328328 execApp' env ctxt r (drop arity args)

329329 Nothing -> return (mkEApp f args)

330330 else return (mkEApp f args)

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

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

332332 do rhs <- doExec env ctxt tm

333333 execApp' env ctxt rhs args

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

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

335335 do res <- execCase env ctxt ns sc args

336336 return $ fromMaybe (mkEApp f args) res

337337 thing -> return $ mkEApp f args

src/Idris/Coverage.hs+2−2

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

325325 t' <- case t of

326326 Unchecked ->

327327 case lookupDef n ctxt of

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

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

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

330330 then return $ Total []

331331 else calcTotality path fc n pats

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

389389 ist <- getIState

390390 case lookupCtxt n (idris_callgraph ist) of

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

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

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

393393 let (args, sc) = cases_totcheck cd in

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

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

906906

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

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

909− simpleCase tcase False reflect CompileTime fc pdef

909+ simpleCase tcase False reflect CompileTime fc atys pdef

910910 cov <- coverage

911911 pmissing <-

912912 if cov

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

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

955955

956956 tree' <- tclift $ simpleCase tcase knowncovering reflect

957− RunTime fc pdef'

957+ RunTime fc atys pdef'

958958 logLvl 3 (show tree)

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

960960 ctxt <- getContext

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

967967 tcase knowncovering

968968 reflect

969969 (AssertTotal `elem` opts)

970+ atys

970971 pats

971972 pdef pdef pdef_inl pdef' ty)

972973 addIBC (IBCDef n)

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

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

977978 i <- getIState

978979 case lookupDef n (tt_ctxt i) of

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

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

980981 let (scargs, sc) = cases_compiletime cd

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

982983 do let calls = findCalls sc' scargs'

src/Idris/IBC.hs+11−9

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

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 49

26+ibcVersion = 50

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

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

801801 put x2

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

803803 Operator x1 x2 x3 -> do return ()

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

805− put x1

806− put x2

807− put x3

808− -- no x3a

809− put x4

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

805+ put x1

806+ put x2

807+ put x2a

808+ put x3

809+ -- no x3a

810+ put x4

810811 get

811812 = do i <- getWord8

812813 case i of

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

820821 3 -> do x1 <- get

821822 x2 <- get

822823 x3 <- get

823− -- x3 <- get always []

824824 x4 <- get

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

825+ -- x3 <- get always []

826+ x5 <- get

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

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

827829

828830instance Binary Accessibility where

src/Idris/Prover.hs+2−1

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

6565 ideslavePutSExp "end-proof-mode" n

6666 let proofs = proof_list i

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

6969 logLvl 3 (show tree)

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

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

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

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

7676 ptm' <- applyOpts ptm

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

78+ []

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

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

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