@@ -49,15 +49,15 @@ type Var = Set Node
4949type Vars = Map Name Var
5050
5151-- Find the minimal consistent usage by forward chaining.
52−minimalUsage :: Deps -> UseMap
52+minimalUsage :: Deps -> (Set Name, UseMap)
5353minimalUsage = gather . forwardChain
5454 where
55− gather :: Set (Name, Arg) -> UseMap
56− gather = foldr ins M.empty . S.toList
55+ gather :: Set (Name, Arg) -> (Set Name, UseMap)
56+ gather = foldr ins (S.empty, M.empty) . S.toList
5757 where
58− ins :: Node -> UseMap -> UseMap
59− ins (n, Result) = id
60− ins (n, Arg i ) = M.insertWith IS.union n (IS.singleton i)
58+ ins :: Node -> (Set Name, UseMap) -> (Set Name, UseMap)
59+ ins (n, Result) (ns, umap) = (S.insert n ns, umap)
60+ ins (n, Arg i ) (ns, umap) = (ns, M.insertWith IS.union n (IS.singleton i) umap)
6161
6262forwardChain :: Deps -> Set Node
6363forwardChain deps
@@ -82,23 +82,23 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
8282 -- mini-DSL for postulates
8383 (==>) ds rs = (S.fromList ds, S.fromList rs)
8484 (.:) ms n = NS (UN $ pack n) (map pack ms)
85− name = UN . pack
85+ it n is = [(UN $ pack n, Arg i) | i <- is]
8686
8787 postulates =
88− [ [] ==>
89− [ (["Main"] .: "main", Result) -- These two, Main.main and run__IO, are always evaluated
90− , (name "run__IO", Result) -- but evade analysis since they come from the seed term.
91− , (name "prim__believe_me", Arg 2)
92− , (name "prim__strCons", Arg 0)
93− , (name "prim__strCons", Arg 1)
94− , (name "prim__strHead", Arg 0)
95− , (name "prim__strTail", Arg 0)
96− , (name "prim__lenString", Arg 0)
97− , (name "prim__concat", Arg 0)
98− , (name "prim__concat", Arg 1)
99− , (name "prim__zextInt_BigInt", Arg 0)
100− , (name "mkForeignPrim", Arg 2)
101− , (name "mkForeign", Arg 1)
88+ [ [] ==> concat
89+ [ [(["Main"] .: "main", Result)] -- These two, Main.main and run__IO, are always evaluated
90+ , [(UN (pack "run__IO"), Result)] -- but evade analysis since they come from the seed term.
91+ , it "prim__believe_me" [2]
92+ , it "prim__strCons" [0,1]
93+ , it "prim__strHead" [0]
94+ , it "prim__strTail" [0]
95+ , it "prim_lenString" [0] -- not a typo, just a single underscore
96+ , it "prim__concat" [0,1]
97+ , it "mkForeignPrim" [2]
98+ , it "mkForeign" [1]
99+ , it "prim__toStrBigInt" [0]
100+ , it "prim__addBigInt" [0,1]
101+ , it "prim__zextInt_BigInt" [0]
102102 ]
103103 ]
104104
@@ -126,8 +126,8 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
126126 getDeps :: Name -> Deps
127127 getDeps n = case lookupDef n ctx of
128128 [def] -> getDepsDef n def
129− [] -> error $ "erasure checker: unknown name: " ++ show n
130− _ -> error $ "erasure checker: ambiguous name: " ++ show n
129+ [] -> error $ "erasure checker: unknown reference: " ++ show n
130+ _ -> error $ "erasure checker: ambiguous reference: " ++ show n
131131
132132 getDepsDef :: Name -> Def -> Deps
133133 getDepsDef fn (Function ty t) = error "a function encountered" -- TODO
@@ -149,7 +149,7 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
149149
150150 etaExpand :: [Name] -> Term -> Term
151151 etaExpand [] t = t
152− etaExpand (n : ns) t = App (etaExpand ns t) (P Bound n Erased)
152+ etaExpand (n : ns) t = etaExpand ns (App t (P Bound n Erased))
153153
154154 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
155155 getDepsSC fn es vs ImpossibleCase = M.empty
@@ -177,9 +177,9 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
177177
178178 -- named variables introduce dependencies as described in `vs'
179179 getDepsTerm vs bs cd (P _ n _)
180− | Just var <- M.lookup n vs = M.singleton cd var -- this condition gives rise to these dependencies
181− | otherwise = M.empty
182−
180+ | Just var <- M.lookup n vs = M.singleton cd var -- found among local variables
181+ | otherwise = M.singleton cd (S.singleton (n, Result)) -- assumed to be a global reference
182+
183183 -- dependencies of de bruijn variables are described in `bs'
184184 getDepsTerm vs bs cd (V i) = (bs !! i) cd
185185
@@ -208,6 +208,8 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
208208
209209 -- a bound variable might draw in additional dependencies,
210210 -- think: f x = x 0 <-- here, `x' _is_ used
211+ -- also, the arguments must be considered used
212+ -- since we don't know what's in the variable
211213 P Bound n _ -> var n `ins` unconditionalDeps args
212214
213215 -- we interpret applied lambdas as lets in order to reuse code here