@@ -49,15 +49,15 @@ type Var = Set Node
49type Vars = Map Name Var
49type Vars = Map Name Var
51-- Find the minimal consistent usage by forward chaining.
51-- Find the minimal consistent usage by forward chaining.
52−minimalUsage :: Deps -> UseMap
52+minimalUsage :: Deps -> (Set Name, UseMap)
53minimalUsage = gather . forwardChain
53minimalUsage = gather . forwardChain
55− gather :: Set (Name, Arg) -> UseMap
55+ gather :: Set (Name, Arg) -> (Set Name, UseMap)
56− gather = foldr ins M.empty . S.toList
56+ gather = foldr ins (S.empty, M.empty) . S.toList
58− ins :: Node -> UseMap -> UseMap
58+ ins :: Node -> (Set Name, UseMap) -> (Set Name, UseMap)
59− ins (n, Result) = id
59+ ins (n, Result) (ns, umap) = (S.insert n ns, umap)
60− ins (n, Arg i ) = M.insertWith IS.union n (IS.singleton i)
60+ ins (n, Arg i ) (ns, umap) = (ns, M.insertWith IS.union n (IS.singleton i) umap)
62forwardChain :: Deps -> Set Node
62forwardChain :: Deps -> Set Node
63forwardChain deps
63forwardChain deps
@@ -82,23 +82,23 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
82 -- mini-DSL for postulates
82 -- mini-DSL for postulates
83 (==>) ds rs = (S.fromList ds, S.fromList rs)
83 (==>) ds rs = (S.fromList ds, S.fromList rs)
84 (.:) ms n = NS (UN $ pack n) (map pack ms)
84 (.:) ms n = NS (UN $ pack n) (map pack ms)
85− name = UN . pack
85+ it n is = [(UN $ pack n, Arg i) | i <- is]
87 postulates =
87 postulates =
88− [ [] ==>
88+ [ [] ==> concat
89− [ (["Main"] .: "main", Result) -- These two, Main.main and run__IO, are always evaluated
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.
90+ , [(UN (pack "run__IO"), Result)] -- but evade analysis since they come from the seed term.
91− , (name "prim__believe_me", Arg 2)
91+ , it "prim__believe_me" [2]
92− , (name "prim__strCons", Arg 0)
92+ , it "prim__strCons" [0,1]
93− , (name "prim__strCons", Arg 1)
94− , (name "prim__strHead", Arg 0)
93+ , it "prim__strHead" [0]
95− , (name "prim__strTail", Arg 0)
94+ , it "prim__strTail" [0]
96− , (name "prim__lenString", Arg 0)
95+ , it "prim_lenString" [0] -- not a typo, just a single underscore
97− , (name "prim__concat", Arg 0)
98− , (name "prim__concat", Arg 1)
96+ , it "prim__concat" [0,1]
99− , (name "prim__zextInt_BigInt", Arg 0)
100− , (name "mkForeignPrim", Arg 2)
97+ , it "mkForeignPrim" [2]
101− , (name "mkForeign", Arg 1)
98+ , it "mkForeign" [1]
99+ , it "prim__toStrBigInt" [0]
100+ , it "prim__addBigInt" [0,1]
101+ , it "prim__zextInt_BigInt" [0]
@@ -126,8 +126,8 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
126 getDeps :: Name -> Deps
126 getDeps :: Name -> Deps
127 getDeps n = case lookupDef n ctx of
127 getDeps n = case lookupDef n ctx of
128 [def] -> getDepsDef n def
128 [def] -> getDepsDef n def
129− [] -> error $ "erasure checker: unknown name: " ++ show n
129+ [] -> error $ "erasure checker: unknown reference: " ++ show n
130− _ -> error $ "erasure checker: ambiguous name: " ++ show n
130+ _ -> error $ "erasure checker: ambiguous reference: " ++ show n
132 getDepsDef :: Name -> Def -> Deps
132 getDepsDef :: Name -> Def -> Deps
133 getDepsDef fn (Function ty t) = error "a function encountered" -- TODO
133 getDepsDef fn (Function ty t) = error "a function encountered" -- TODO
@@ -149,7 +149,7 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
150 etaExpand :: [Name] -> Term -> Term
150 etaExpand :: [Name] -> Term -> Term
151 etaExpand [] t = t
151 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))
154 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
154 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
155 getDepsSC fn es vs ImpossibleCase = M.empty
155 getDepsSC fn es vs ImpossibleCase = M.empty
@@ -177,9 +177,9 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
178 -- named variables introduce dependencies as described in `vs'
178 -- named variables introduce dependencies as described in `vs'
179 getDepsTerm vs bs cd (P _ n _)
179 getDepsTerm vs bs cd (P _ n _)
180− | Just var <- M.lookup n vs = M.singleton cd var -- this condition gives rise to these dependencies
180+ | Just var <- M.lookup n vs = M.singleton cd var -- found among local variables
181− | otherwise = M.empty
181+ | otherwise = M.singleton cd (S.singleton (n, Result)) -- assumed to be a global reference
183 -- dependencies of de bruijn variables are described in `bs'
183 -- dependencies of de bruijn variables are described in `bs'
184 getDepsTerm vs bs cd (V i) = (bs !! i) cd
184 getDepsTerm vs bs cd (V i) = (bs !! i) cd
@@ -208,6 +208,8 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
209 -- a bound variable might draw in additional dependencies,
209 -- a bound variable might draw in additional dependencies,
210 -- think: f x = x 0 <-- here, `x' _is_ used
210 -- 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
211 P Bound n _ -> var n `ins` unconditionalDeps args
213 P Bound n _ -> var n `ins` unconditionalDeps args
213 -- we interpret applied lambdas as lets in order to reuse code here
215 -- we interpret applied lambdas as lets in order to reuse code here