@@ -9,6 +9,7 @@ import Idris.AbsSyntax
9import Idris.Core.CaseTree
9import Idris.Core.CaseTree
10import Idris.Core.TT
10import Idris.Core.TT
11import Idris.Core.Evaluate
11import Idris.Core.Evaluate
12+import Idris.Primitives
13import Debug.Trace
14import Debug.Trace
14import System.IO.Unsafe
15import System.IO.Unsafe
@@ -27,6 +28,7 @@ import Data.IntSet (IntSet)
27import Data.Map (Map)
28import Data.Map (Map)
28import Data.IntMap (IntMap)
29import Data.IntMap (IntMap)
29import Data.Text (pack)
30import Data.Text (pack)
31+import qualified Data.Text as T
31-- UseMap maps names to the set of used (reachable) argument positions.
33-- UseMap maps names to the set of used (reachable) argument positions.
32type UseMap = Map Name IntSet
34type UseMap = Map Name IntSet
@@ -82,40 +84,34 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
83 -- mini-DSL for postulates
85 -- mini-DSL for postulates
84 (==>) ds rs = (S.fromList ds, S.fromList rs)
86 (==>) ds rs = (S.fromList ds, S.fromList rs)
85− (.:) ms n = NS (UN $ pack n) (map pack $ reverse ms)
87+ (.:) ms n = NS (sUN n) (map pack $ reverse ms)
86− it n is = [(UN $ pack n, Arg i) | i <- is]
88+ it n is = [(sUN n, Arg i) | i <- is]
87 mn n is = [(MN 0 $ pack n, Arg i) | i <- is]
89 mn n is = [(MN 0 $ pack n, Arg i) | i <- is]
91+ -- believe_me is special because it does not use all its arguments
92+ specialPrims = S.fromList [sUN "prim__believe_me"]
93+ usedNames = allNames deps S.\\ specialPrims
94+ usedPrims = [(p_name p, p_arity p) | p <- primitives, p_name p `S.member` usedNames]
89 postulates =
96 postulates =
90 [ [] ==> concat
97 [ [] ==> concat
91− [ [(["Main"] .: "main", Result)] -- These two, Main.main and run__IO, are always evaluated
98+ -- These two, Main.main and run__IO, are always evaluated
92− , [(UN (pack "run__IO"), Result)] -- but evade analysis since they come from the seed term.
99+ -- but they evade analysis since they come from the seed term.
93− , it "prim__believe_me" [2]
100+ [ [(["Main"] .: "main", Result)]
94− , it "prim__strCons" [0,1]
101+ , [(sUN "run__IO", Result)]
95− , it "prim__strHead" [0]
102+
96− , it "prim__strTail" [0]
103+ -- these have been discovered as builtins but are not listed
97− , it "prim_lenString" [0] -- not a typo, just a single underscore
104+ -- among Idris.Primitives.primitives
98− , it "prim__concat" [0,1]
99 , it "mkForeignPrim" [2]
105 , it "mkForeignPrim" [2]
100 , it "mkForeign" [1]
106 , it "mkForeign" [1]
101− , it "prim__toStrBigInt" [0]
102− , it "prim__addBigInt" [0,1]
103− , it "prim__subBigInt" [0,1]
104− , it "prim__sextInt_BigInt" [0]
105− , it "prim__zextInt_BigInt" [0]
106− , it "prim__eqString" [0,1]
107− , it "prim__eqChar" [0,1]
108− , it "prim__eqBigInt" [0,1]
109− , it "prim__charToInt" [0]
110− , it "prim__sltBigInt" [0,1]
111− , it "prim__sltChar" [0,1]
112− , it "prim__toStrInt" [0,1]
113− , it "prim__addInt" [0,1]
114− , it "prim__eqInt" [0,1]
115− , it "prim__sltInt" [0,1]
116− , it "prim__subInt" [0,1]
117− , mn "__MkPair" [0,1]
107+ , mn "__MkPair" [0,1]
109+ -- special prims: believe_me only uses its third argument
110+ , it "prim__believe_me" [2]
112+ -- in general, all other primitives use all their arguments
113+ , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]
121 -- perform depth-first search
117 -- perform depth-first search
@@ -128,15 +124,15 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
128 | otherwise = dfs (S.insert n visited) (M.unionWith S.union deps' deps) (next ++ ns)
124 | otherwise = dfs (S.insert n visited) (M.unionWith S.union deps' deps) (next ++ ns)
130 next = [n | n <- S.toList depn, n `S.notMember` visited]
126 next = [n | n <- S.toList depn, n `S.notMember` visited]
131− depn = S.delete n $ depNames deps'
127+ depn = S.delete n $ allNames deps'
132 deps' = getDeps n
128 deps' = getDeps n
134− -- extract all names that a function depends on
130+ -- extract all names that a function depends on
135− -- from the Deps of the function
131+ -- from the Deps of the function
136− depNames :: Deps -> Set Name
132+ allNames :: Deps -> Set Name
137− depNames = S.unions . map names . M.toList
133+ allNames = S.unions . map names . M.toList
139− names (cs, ns) = S.map fst cs `S.union` S.map fst ns
135+ names (cs, ns) = S.map fst cs `S.union` S.map fst ns
141 -- get Deps for a Name
137 -- get Deps for a Name
142 getDeps :: Name -> Deps
138 getDeps :: Name -> Deps