git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/DataOpts.hs
112 lines 4.5 kB history raw
1{-|
2Module : Idris.DataOpts
3Description : Optimisations for Idris code i.e. Forcing, detagging and collapsing.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE FlexibleInstances, PatternGuards #-}
10module Idris.DataOpts(applyOpts) where
12import Idris.AbsSyntax
13import Idris.Core.TT
15class Optimisable term where
16 applyOpts :: term -> Idris term
18instance (Optimisable a, Optimisable b) => Optimisable (a, b) where
19 applyOpts (x, y) = (,) <$> applyOpts x <*> applyOpts y
21instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where
22 applyOpts (v, x, y) = (,,) v <$> applyOpts x <*> applyOpts y
24instance Optimisable a => Optimisable [a] where
25 applyOpts = mapM applyOpts
27instance Optimisable a => Optimisable (Either a (a, a)) where
28 applyOpts (Left t) = Left <$> applyOpts t
29 applyOpts (Right t) = Right <$> applyOpts t
31-- Raw is for compile time optimisation (before type checking)
32-- Term is for run time optimisation (after type checking, collapsing allowed)
33-- Compile time: no collapsing
35instance Optimisable Raw where
36 applyOpts t@(RApp f a)
37 | (Var n, args) <- raw_unapply t -- MAGIC HERE
38 = raw_apply (Var n) <$> mapM applyOpts args
39 | otherwise = RApp <$> applyOpts f <*> applyOpts a
41 applyOpts (RBind n b t) = RBind n <$> applyOpts b <*> applyOpts t
42 applyOpts t = return t
44-- Erase types (makes ibc smaller, and we don't need them)
45instance Optimisable (Binder (TT Name)) where
46 applyOpts (Let r t v) = Let r <$> return Erased <*> applyOpts v
47 applyOpts b = return (b { binderTy = Erased })
49instance Optimisable (Binder Raw) where
50 applyOpts b = do t' <- applyOpts (binderTy b)
51 return (b { binderTy = t' })
53-- Run-time: do everything
55prel = [txt "Nat", txt "Prelude"]
57instance Optimisable (TT Name) where
58 applyOpts (P _ (NS (UN fn) mod) _)
59 | fn == txt "plus" && mod == prel
60 = return (P Ref (sUN "prim__addBigInt") Erased)
61 applyOpts (P _ (NS (UN fn) mod) _)
62 | fn == txt "mult" && mod == prel
63 = return (P Ref (sUN "prim__mulBigInt") Erased)
64 applyOpts (P _ (NS (UN fn) mod) _)
65 | fn == txt "divNat" && mod == prel
66 = return (P Ref (sUN "prim__sdivBigInt") Erased)
67 applyOpts (P _ (NS (UN fn) mod) _)
68 | fn == txt "modNat" && mod == prel
69 = return (P Ref (sUN "prim__sremBigInt") Erased)
70 applyOpts (App _ (P _ (NS (UN fn) mod) _) x)
71 | fn == txt "fromIntegerNat" && mod == prel
72 = applyOpts x
73 applyOpts (P _ (NS (UN fn) mod) _)
74 | fn == txt "fromIntegerNat" && mod == prel
75 = return (App Complete (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)
76 applyOpts (P _ (NS (UN fn) mod) _)
77 | fn == txt "toIntegerNat" && mod == prel
78 = return (App Complete (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)
79 applyOpts c@(P (DCon t arity uniq) n _)
80 = return $ applyDataOptRT n t arity uniq []
81 applyOpts t@(App s f a)
82 | (c@(P (DCon t arity uniq) n _), args) <- unApply t
83 = applyDataOptRT n t arity uniq <$> mapM applyOpts args
84 | otherwise = App s <$> applyOpts f <*> applyOpts a
85 applyOpts (Bind n b t) = Bind n <$> applyOpts b <*> applyOpts t
86 applyOpts (Proj t i) = Proj <$> applyOpts t <*> pure i
87 applyOpts t = return t
89-- | Need to saturate arguments first to ensure that optimisation happens uniformly
90applyDataOptRT :: Name -> Int -> Int -> Bool -> [Term] -> Term
91applyDataOptRT n tag arity uniq args
92 | length args == arity = doOpts n args
93 | otherwise = let extra = satArgs (arity - length args)
94 tm = doOpts n (map (weakenTm (length extra)) args ++ map (\n -> P Bound n Erased) extra)
95 in bind extra tm
96 where
97 satArgs n = map (\i -> sMN i "sat") [1..n]
99 bind [] tm = tm
100 bind (n:ns) tm = Bind n (Lam RigW Erased) (pToV n (bind ns tm))
102 -- Nat special cases
103 -- TODO: Would be nice if this was configurable in idris source!
104 -- Issue #1597 https://github.com/idris-lang/Idris-dev/issues/1597
105 doOpts (NS (UN z) [nat, prelude]) []
106 | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"
107 = Constant (BI 0)
108 doOpts (NS (UN s) [nat, prelude]) [k]
109 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"
110 = App Complete (App Complete (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))
112 doOpts n args = mkApp (P (DCon tag arity uniq) n Erased) args