@@ -9,6 +9,7 @@ import Idris.AbsSyntax
99import Idris.Core.CaseTree
1010import Idris.Core.TT
1111import Idris.Core.Evaluate
12+import Idris.Primitives
1213
1314import Debug.Trace
1415import System.IO.Unsafe
@@ -27,6 +28,7 @@ import Data.IntSet (IntSet)
2728import Data.Map (Map)
2829import Data.IntMap (IntMap)
2930import Data.Text (pack)
31+import qualified Data.Text as T
3032
3133-- UseMap maps names to the set of used (reachable) argument positions.
3234type UseMap = Map Name IntSet
@@ -82,40 +84,34 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
8284 where
8385 -- mini-DSL for postulates
8486 (==>) ds rs = (S.fromList ds, S.fromList rs)
85− (.:) ms n = NS (UN $ pack n) (map pack $ reverse ms)
86− it n is = [(UN $ pack n, Arg i) | i <- is]
87+ (.:) ms n = NS (sUN n) (map pack $ reverse ms)
88+ it n is = [(sUN n, Arg i) | i <- is]
8789 mn n is = [(MN 0 $ pack n, Arg i) | i <- is]
8890
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]
95+
8996 postulates =
9097 [ [] ==> concat
91− [ [(["Main"] .: "main", Result)] -- 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.
93− , it "prim__believe_me" [2]
94− , it "prim__strCons" [0,1]
95− , it "prim__strHead" [0]
96− , it "prim__strTail" [0]
97− , it "prim_lenString" [0] -- not a typo, just a single underscore
98− , it "prim__concat" [0,1]
98+ -- These two, Main.main and run__IO, are always evaluated
99+ -- but they evade analysis since they come from the seed term.
100+ [ [(["Main"] .: "main", Result)]
101+ , [(sUN "run__IO", Result)]
102+
103+ -- these have been discovered as builtins but are not listed
104+ -- among Idris.Primitives.primitives
99105 , it "mkForeignPrim" [2]
100106 , 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]
118− ]
107+ , mn "__MkPair" [0,1]
108+
109+ -- special prims: believe_me only uses its third argument
110+ , it "prim__believe_me" [2]
111+
112+ -- in general, all other primitives use all their arguments
113+ , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]
114+ ]
119115 ]
120116
121117 -- perform depth-first search
@@ -128,15 +124,15 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
128124 | otherwise = dfs (S.insert n visited) (M.unionWith S.union deps' deps) (next ++ ns)
129125 where
130126 next = [n | n <- S.toList depn, n `S.notMember` visited]
131− depn = S.delete n $ depNames deps'
127+ depn = S.delete n $ allNames deps'
132128 deps' = getDeps n
133129
134− -- extract all names that a function depends on
135− -- from the Deps of the function
136− depNames :: Deps -> Set Name
137− depNames = S.unions . map names . M.toList
138− where
139− names (cs, ns) = S.map fst cs `S.union` S.map fst ns
130+ -- extract all names that a function depends on
131+ -- from the Deps of the function
132+ allNames :: Deps -> Set Name
133+ allNames = S.unions . map names . M.toList
134+ where
135+ names (cs, ns) = S.map fst cs `S.union` S.map fst ns
140136
141137 -- get Deps for a Name
142138 getDeps :: Name -> Deps