3Description : Utilities to erase stuff not necessary for runtime.
6Maintainer : The Idris Community.
8{-# LANGUAGE PatternGuards #-}
10module Idris.Erasure (performUsageAnalysis, mkFieldName) where
14import Idris.Core.CaseTree
15import Idris.Core.Evaluate
19import Idris.Primitives
21import Prelude hiding (id, (.))
24import Control.Category
25import Control.Monad.State
26import Data.IntMap (IntMap)
27import qualified Data.IntMap as IM
28import Data.IntSet (IntSet)
29import qualified Data.IntSet as IS
32import qualified Data.Map as M
35import qualified Data.Set as S
36import Data.Text (pack)
37import qualified Data.Text as T
39-- | UseMap maps names to the set of used (reachable) argument
41type UseMap = Map Name (IntMap (Set Reason))
43data Arg = Arg Int | Result deriving (Eq, Ord)
45instance Show Arg where
49type Node = (Name, Arg)
50type Deps = Map Cond DepSet
51type Reason = (Name, Int) -- function name, argument index
53-- | Nodes along with sets of reasons for every one.
54type DepSet = Map Node (Set Reason)
56-- | "Condition" is the conjunction of elementary assumptions along
57-- the path from the root. Elementary assumption (f, i) means that
58-- "function f uses the argument i".
61-- | Variables carry certain information with them.
63 { viDeps :: DepSet -- ^ dependencies drawn in by the variable
64 , viFunArg :: Maybe Int -- ^ which function argument this variable came from (defined only for patvars)
65 , viMethod :: Maybe Name -- ^ name of the metamethod represented by the var, if any
69type Vars = Map Name VarInfo
71-- | Perform usage analysis, write the relevant information in the
72-- internal structures, returning the list of reachable names.
73performUsageAnalysis :: [Name] -> Idris [Name]
74performUsageAnalysis startNames = do
75 ctx <- tt_ctxt <$> getIState
77 [] -> return [] -- no main -> not compiling -> reachability irrelevant
79 ci <- idris_interfaces <$> getIState
80 cg <- idris_callgraph <$> getIState
81 opt <- idris_optimisation <$> getIState
82 used <- idris_erasureUsed <$> getIState
83 externs <- idris_externs <$> getIState
85 -- Build the dependency graph.
86 let depMap = buildDepMap ci used (S.toList externs) ctx main
88 -- Search for reachable nodes in the graph.
89 let (residDeps, (reachableNames, minUse)) = minimalUsage depMap
90 usage = M.toList minUse
92 -- Print some debug info.
93 logErasure 5 $ "Original deps:\n" ++ unlines (map fmtItem . M.toList $ depMap)
94 logErasure 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)
95 logErasure 4 $ "Minimal usage:\n" ++ fmtUseMap usage
96 logErasure 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)
98 -- Check that everything reachable is accessible.
99 checkEnabled <- (WarnReach `elem`) . opt_cmdline . idris_options <$> getIState
101 mapM_ (checkAccessibility opt) usage
103 -- Check that no postulates are reachable.
104 reachablePostulates <- S.intersection reachableNames . idris_postulates <$> getIState
105 when (not . S.null $ reachablePostulates)
106 $ ifail ("reachable postulates:\n" ++ intercalate "\n" [" " ++ show n | n <- S.toList reachablePostulates])
108 -- Store the usage info in the internal state.
109 mapM_ storeUsage usage
111 return $ S.toList reachableNames
115 fmtItem :: (Cond, DepSet) -> String
116 fmtItem (cond, deps) = indent $ show (S.toList cond) ++ " -> " ++ show (M.toList deps)
118 fmtUseMap :: [(Name, IntMap (Set Reason))] -> String
119 fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ fmtIxs is)
121 fmtIxs :: IntMap (Set Reason) -> String
122 fmtIxs = intercalate ", " . map fmtArg . IM.toList
126 | otherwise = show i ++ " from " ++ intercalate ", " (map show $ S.toList rs)
128 storeUsage :: (Name, IntMap (Set Reason)) -> Idris ()
129 storeUsage (n, args) = fputState (cg_usedpos . ist_callgraph n) flat
131 flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]
133 checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
134 checkAccessibility opt (n, reachable)
135 | Just (Optimise inaccessible dt force) <- lookupCtxtExact n opt
136 , eargs@(_:_) <- [fmt n (S.toList rs) | (i,n) <- inaccessible, rs <- maybeToList $ IM.lookup i reachable]
137 = warn $ show n ++ ": inaccessible arguments reachable:\n " ++ intercalate "\n " eargs
139 | otherwise = return ()
141 fmt n [] = show n ++ " (no more information available)"
142 fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]
145type Constraint = (Cond, DepSet)
147-- | Find the minimal consistent usage by forward chaining.
149-- We use a cleverer implementation that:
150-- 1. First transforms Deps into a collection of numbered constraints
151-- 2. For each node, we remember the numbers of constraints
152-- that contain that node among their preconditions.
153-- 3. When performing forward chaining, we perform unit propagation
154-- only on the relevant constraints, not all constraints.
156-- Typical numbers from the current version of Blodwen:
157-- * 56 iterations until fixpoint
158-- * out of 20k constraints total, 5-1000 are relevant per iteration
159minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
161 = fromNumbered *** gather
162 $ forwardChain (index numbered) seedDeps seedDeps numbered
164 numbered = toNumbered deps
166 -- The initial solution. Consists of nodes that are
167 -- reachable immediately, without any preconditions.
169 seedDeps = M.unionsWith S.union [ds | (cond, ds) <- IM.elems numbered, S.null cond]
171 toNumbered :: Deps -> IntMap Constraint
172 toNumbered = IM.fromList . zip [0..] . M.toList
174 fromNumbered :: IntMap Constraint -> Deps
175 fromNumbered = IM.foldr addConstraint M.empty
177 addConstraint (ns, vs) = M.insertWith (M.unionWith S.union) ns vs
179 -- Build an index that maps every node to the set of constraints
180 -- where the node appears among the preconditions.
181 index :: IntMap Constraint -> Map Node IntSet
182 index = IM.foldrWithKey (
183 -- for each clause (i. ns --> _ds)
184 \i (ns, _ds) ix -> foldr (
185 -- for each node `n` in `ns`
186 \n ix' -> M.insertWith IS.union n (IS.singleton i) ix'
190 -- Convert a solution of constraints into:
191 -- 1. the list of names used in the program
192 -- 2. the list of arguments used, together with their reasons
193 gather :: DepSet -> (Set Name, UseMap)
194 gather = foldr ins (S.empty, M.empty) . M.toList
196 ins :: (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)
197 ins ((n, Result), rs) (ns, umap) = (S.insert n ns, umap)
198 ins ((n, Arg i ), rs) (ns, umap) = (ns, M.insertWith (IM.unionWith S.union) n (IM.singleton i rs) umap)
200-- | In each iteration, we find the set of nodes immediately reachable
201-- from the current set of constraints, and then reduce the set of constraints
202-- based on that knowledge.
204-- In the implementation, this is phase-shifted. We first reduce the set
205-- of constraints, given the newly reachable nodes from the previous iteration,
206-- and then compute the set of currently reachable nodes.
207-- Then we decide whether to iterate further.
209 :: Map Node IntSet -- ^ node index
210 -> DepSet -- ^ all reachable nodes found so far
211 -> DepSet -- ^ nodes reached in the previous iteration
212 -> IntMap Constraint -- ^ numbered constraints
213 -> (IntMap Constraint, DepSet)
214forwardChain index solution previouslyNew constrs
215 -- no newly reachable nodes, fixed point has been reached
216 | M.null currentlyNew
217 = (constrs, solution)
219 -- some newly reachable nodes, iterate more
222 (M.unionWith S.union solution currentlyNew)
226 -- which constraints could give new results,
227 -- given that `previouslyNew` has been derived in the last iteration
228 affectedIxs = IS.unions [
229 M.findWithDefault IS.empty n index
230 | n <- M.keys previouslyNew
233 -- traverse all (potentially) affected constraints, building:
234 -- 1. a set of newly reached nodes
235 -- 2. updated set of constraints where the previously
236 -- reached nodes have been removed
237 (currentlyNew, constrs')
239 (reduceConstraint $ M.keysSet previouslyNew)
243 -- Update the pair (newly reached nodes, numbered constraint set)
244 -- by reducing the constraint with the given number.
246 :: Set Node -- ^ nodes reached in the previous iteration
247 -> Int -- ^ constraint number
248 -> (DepSet, IntMap (Cond, DepSet))
249 -> (DepSet, IntMap (Cond, DepSet))
250 reduceConstraint previouslyNew i (news, constrs)
251 | Just (cond, deps) <- IM.lookup i constrs
252 = case cond S.\\ previouslyNew of
254 -- This constraint's set of preconditions has shrunk
255 -- to the empty set. We can add its RHS to the set of newly
256 -- reached nodes, and remove the constraint altogether.
258 -> (M.unionWith S.union news deps, IM.delete i constrs)
260 -- This constraint's set of preconditions has shrunk
261 -- so we need to overwrite the numbered slot
262 -- with the updated constraint.
263 | S.size cond' < S.size cond
264 -> (news, IM.insert i (cond', deps) constrs)
266 -- This constraint's set of preconditions hasn't changed
267 -- so we do not do anything about it.
271 -- Constraint number present in index but not found
272 -- among the constraints. This happens more and more frequently
273 -- as we delete constraints from the set.
274 | otherwise = (news, constrs)
276-- | Build the dependency graph, starting the depth-first search from
278buildDepMap :: Ctxt InterfaceInfo -> [(Name, Int)] -> [(Name, Int)] ->
279 Context -> [Name] -> Deps
280buildDepMap ci used externs ctx startNames
281 = addPostulates used $ dfs S.empty M.empty startNames
283 -- mark the result of Main.main as used with the empty assumption
284 addPostulates :: [(Name, Int)] -> Deps -> Deps
285 addPostulates used deps = foldr (\(ds, rs) -> M.insertWith (M.unionWith S.union) ds rs) deps (postulates used)
287 -- mini-DSL for postulates
288 (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])
289 it n is = [(sUN n, Arg i) | i <- is]
291 -- believe_me is special because it does not use all its arguments
292 specialPrims = S.fromList [sUN "prim__believe_me"]
293 usedNames = allNames deps S.\\ specialPrims
294 usedPrims = [(p_name p, p_arity p) | p <- primitives, p_name p `S.member` usedNames]
298 -- Main.main ( + export lists) and run__IO, are always evaluated
299 -- but they elude analysis since they come from the seed term.
300 [(map (\n -> (n, Result)) startNames)
301 ,[(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]
302 ,[(sUN "call__IO", Result), (sUN "call__IO", Arg 2)]
304 -- Explicit usage declarations from a %used pragma
305 , map (\(n, i) -> (n, Arg i)) used
307 -- MkIO is read by run__IO,
308 -- but this cannot be observed in the source code of programs.
312 -- Foreign calls are built with pairs, but mkForeign doesn't
313 -- have an implementation so analysis won't see them
315 (pairCon, Arg 3)] -- Used in foreign calls
317 -- these have been discovered as builtins but are not listed
318 -- among Idris.Primitives.primitives
319 --, mn "__MkPair" [2,3]
321 , it "unsafePerformPrimIO" [1]
323 -- believe_me is a primitive but it only uses its third argument
324 -- it is special-cased in usedNames above
325 , it "prim__believe_me" [2]
327 -- in general, all other primitives use all their arguments
328 , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]
330 -- %externs are assumed to use all their arguments
331 , [(n, Arg i) | (n,arity) <- externs, i <- [0..arity-1]]
333 -- mkForeign* functions are special-cased below
337 -- perform depth-first search
338 -- to discover all the names used in the program
339 -- and call getDeps for every name
340 dfs :: Set Name -> Deps -> [Name] -> Deps
341 dfs visited deps [] = deps
342 dfs visited deps (n : ns)
343 | n `S.member` visited = dfs visited deps ns
344 | otherwise = dfs (S.insert n visited) (M.unionWith (M.unionWith S.union) deps' deps) (next ++ ns)
346 next = [n | n <- S.toList depn, n `S.notMember` visited]
347 depn = S.delete n $ allNames deps'
350 -- extract all names that a function depends on
351 -- from the Deps of the function
352 allNames :: Deps -> Set Name
353 allNames = S.unions . map names . M.toList
355 names (cs, ns) = S.map fst cs `S.union` S.map fst (M.keysSet ns)
357 -- get Deps for a Name
358 getDeps :: Name -> Deps
359 getDeps (SN (WhereN i (SN (ImplementationCtorN interfaceN)) (MN i' field)))
360 = M.empty -- these deps are created when applying implementation ctors
361 getDeps n = case lookupDefExact n ctx of
362 Just def -> getDepsDef n def
363 Nothing -> error $ "erasure checker: unknown reference: " ++ show n
365 getDepsDef :: Name -> Def -> Deps
366 getDepsDef fn (Function ty t) = error "a function encountered" -- TODO
367 getDepsDef fn (TyDecl ty t) = M.empty
368 getDepsDef fn (Operator ty n' f) = M.empty -- TODO: what's this?
369 getDepsDef fn (CaseOp ci ty tys def tot cdefs)
370 = getDepsSC fn etaVars (etaMap `M.union` varMap) sc
372 -- we must eta-expand the definition with fresh variables
373 -- to capture these dependencies as well
374 etaIdx = [length vars .. length tys - 1]
375 etaVars = [eta i | i <- etaIdx]
376 etaMap = M.fromList [varPair (eta i) i | i <- etaIdx]
377 eta i = MN i (pack "eta")
379 -- the variables that arose as function arguments only depend on (n, i)
380 varMap = M.fromList [varPair v i | (v,i) <- zip vars [0..]]
382 varPair n argNo = (n, VI
383 { viDeps = M.singleton (fn, Arg argNo) S.empty
384 , viFunArg = Just argNo
388 (vars, sc) = cases_runtime cdefs
389 -- we use cases_runtime in order to have case-blocks
390 -- resolved to top-level functions before our analysis
392 etaExpand :: [Name] -> Term -> Term
394 etaExpand (n : ns) t = etaExpand ns (App Complete t (P Ref n Erased))
396 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
397 getDepsSC fn es vs ImpossibleCase = M.empty
398 getDepsSC fn es vs (UnmatchedCase msg) = M.empty
400 -- for the purposes of erasure, we can disregard the projection
401 getDepsSC fn es vs (ProjCase (Proj t i) alts) = getDepsSC fn es vs (ProjCase t alts) -- step
402 getDepsSC fn es vs (ProjCase (P _ n _) alts) = getDepsSC fn es vs (Case Shared n alts) -- base
404 -- other ProjCase's are not supported
405 getDepsSC fn es vs (ProjCase t alts) = error $ "ProjCase not supported:\n" ++ show (ProjCase t alts)
407 getDepsSC fn es vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)
408 getDepsSC fn es vs (Case sh n alts)
409 -- we case-split on this variable, which marks it as used
410 -- (unless there is exactly one case branch)
411 -- hence we add a new dependency, whose only precondition is
412 -- that the result of this function is used at all
413 = addTagDep $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree
415 addTagDep = case alts of
416 [_] -> id -- single branch, tag not used
417 _ -> M.insertWith (M.unionWith S.union) (S.singleton (fn, Result)) (viDeps casedVar)
418 casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
420 getDepsAlt :: Name -> [Name] -> Vars -> VarInfo -> CaseAlt -> Deps
421 getDepsAlt fn es vs var (FnCase n ns sc) = M.empty -- can't use FnCase at runtime
422 getDepsAlt fn es vs var (ConstCase c sc) = getDepsSC fn es vs sc
423 getDepsAlt fn es vs var (DefaultCase sc) = getDepsSC fn es vs sc
424 getDepsAlt fn es vs var (SucCase n sc)
425 = getDepsSC fn es (M.insert n var vs) sc -- we're not inserting the S-dependency here because it's special-cased
428 getDepsAlt fn es vs var (ConCase n cnt ns sc)
429 = getDepsSC fn es (vs' `M.union` vs) sc -- left-biased union
431 -- Here we insert dependencies that arose from pattern matching on a constructor.
432 -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
433 vs' = M.fromList [(v, VI
434 { viDeps = M.insertWith S.union (n, Arg j) (S.singleton (fn, varIdx)) (viDeps var)
435 , viFunArg = viFunArg var
438 | (v, j) <- zip ns [0..]]
440 -- this is safe because it's certainly a patvar
441 varIdx = fromJust (viFunArg var)
443 -- generate metamethod names, "n" is the implementation ctor
444 meth :: Int -> Maybe Name
445 meth | SN (ImplementationCtorN interfaceName) <- n = \j -> Just (mkFieldName n j)
446 | otherwise = \j -> Nothing
448 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
449 getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> Term -> Deps
451 -- named variables introduce dependencies as described in `vs'
452 getDepsTerm vs bs cd (P _ n _)
453 -- de bruijns (lambda-bound, let-bound vars)
454 | Just deps <- lookup n bs
457 -- ctor-bound/arg-bound variables
458 | Just var <- M.lookup n vs
459 = M.singleton cd (viDeps var)
461 -- sanity check: machine-generated names shouldn't occur at top-level
463 = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)
465 -- assumed to be a global reference
466 | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)
468 -- dependencies of de bruijn variables are described in `bs'
469 getDepsTerm vs bs cd (V i) = snd (bs !! i) cd
471 getDepsTerm vs bs cd (Bind n bdr body)
472 -- here we just push IM.empty on the de bruijn stack
473 -- the args will be marked as used at the usage site
474 | Lam _ ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body
475 | Pi _ _ ty _ <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body
477 -- let-bound variables can get partially evaluated
478 -- it is sufficient just to plug the Cond in when the bound names are used
479 | Let rig ty t <- bdr = var t cd `union` getDepsTerm vs ((n, const M.empty) : bs) cd body
480 | NLet ty t <- bdr = var t cd `union` getDepsTerm vs ((n, const M.empty) : bs) cd body
482 var t cd = getDepsTerm vs bs cd t
484 -- applications may add items to Cond
485 getDepsTerm vs bs cd app@(App _ _ _)
486 | (fun, args) <- unApply app = case fun of
487 -- implementation constructors -> create metamethod deps
488 P (DCon _ _ _) ctorName@(SN (ImplementationCtorN interfaceName)) _
489 -> conditionalDeps ctorName args -- regular data ctor stuff
490 `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff
492 -- ordinary constructors
493 P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything
494 P (DCon _ _ _) n _ -> conditionalDeps n args -- depends on whether (n,#) is used
496 -- mkForeign* calls must be special-cased because they are variadic
497 -- All arguments must be marked as used, except for the first four,
498 -- which define the call type and are not needed at runtime.
500 | n == T.pack "mkForeignPrim"
501 -> unconditionalDeps $ drop 4 args
503 -- a bound variable might draw in additional dependencies,
504 -- think: f x = x 0 <-- here, `x' _is_ used
506 -- debruijn-bound name
507 | Just deps <- lookup n bs
508 -> deps cd `union` unconditionalDeps args
510 -- local name that refers to a method
511 | Just var <- M.lookup n vs
512 , Just meth <- viMethod var
513 -> viDeps var `ins` conditionalDeps meth args -- use the method instead
516 | Just var <- M.lookup n vs
518 -> viDeps var `ins` unconditionalDeps args
522 -- depends on whether the referred thing uses its argument
523 -> conditionalDeps n args
525 -- TODO: could we somehow infer how bound variables use their arguments?
526 V i -> snd (bs !! i) cd `union` unconditionalDeps args
528 -- we interpret applied lambdas as lets in order to reuse code here
529 Bind n (Lam _ ty) t -> getDepsTerm vs bs cd (lamToLet app)
531 -- and we interpret applied lets as lambdas
532 Bind n (Let _ ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam RigW ty) t) t')
533 Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam RigW ty) t) t')
536 -> error $ "cannot[0] analyse projection !" ++ show i ++ " of " ++ show t
540 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args
542 union = M.unionWith $ M.unionWith S.union
543 ins = M.insertWith (M.unionWith S.union) cd
545 unconditionalDeps :: [Term] -> Deps
546 unconditionalDeps = unionMap (getDepsTerm vs bs cd)
548 conditionalDeps :: Name -> [Term] -> Deps
550 = ins (M.singleton (n, Result) S.empty) . unionMap (getDepsArgs n) . zip indices
552 indices = map Just [0 .. getArity n - 1] ++ repeat Nothing
553 getDepsArgs n (Just i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t -- conditional
554 getDepsArgs n (Nothing, t) = getDepsTerm vs bs cd t -- unconditional
556 methodDeps :: Name -> (Int, Term) -> Deps
557 methodDeps ctorName (methNo, t)
558 = getDepsTerm (vars `M.union` vs) (bruijns ++ bs) cond body
560 vars = M.fromList [(v, VI
564 }) | (v, i) <- zip args [0..]]
565 deps i = M.singleton (metameth, Arg i) S.empty
566 bruijns = reverse [(n, \cd -> M.singleton cd (deps i)) | (i, n) <- zip [0..] args]
567 cond = S.singleton (metameth, Result)
568 metameth = mkFieldName ctorName methNo
569 (args, body) = unfoldLams t
572 getDepsTerm vs bs cd (Proj t (-1)) = getDepsTerm vs bs cd t -- naturals, (S n) -> n
573 getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t
576 getDepsTerm vs bs cd (Inferred t) = getDepsTerm vs bs cd t
579 getDepsTerm vs bs cd (Constant _) = M.empty
580 getDepsTerm vs bs cd (TType _) = M.empty
581 getDepsTerm vs bs cd (UType _) = M.empty
582 getDepsTerm vs bs cd Erased = M.empty
583 getDepsTerm vs bs cd Impossible = M.empty
585 getDepsTerm vs bs cd t = error $ "cannot get deps of: " ++ show t
587 -- Get the number of arguments that might be considered for erasure.
588 getArity :: Name -> Int
589 getArity (SN (WhereN i' ctorName (MN i field)))
590 | Just (TyDecl (DCon _ _ _) ty) <- lookupDefExact ctorName ctx
591 = let argTys = map snd $ getArgTys ty
592 in if i <= length argTys
593 then length $ getArgTys (argTys !! i)
594 else error $ "invalid field number " ++ show i ++ " for " ++ show ctorName
596 | otherwise = error $ "unknown implementation constructor: " ++ show ctorName
598 getArity n = case lookupDefExact n ctx of
599 Just (CaseOp ci ty tys def tot cdefs) -> length tys
600 Just (TyDecl (DCon tag arity _) _) -> arity
601 Just (TyDecl (Ref) ty) -> length $ getArgTys ty
602 Just (Operator ty arity op) -> arity
603 Just df -> error $ "Erasure/getArity: unrecognised entity '"
604 ++ show n ++ "' with definition: " ++ show df
605 Nothing -> error $ "Erasure/getArity: definition not found for " ++ show n
607 -- convert applications of lambdas to lets
608 -- note that this transformation preserves de bruijn numbering
609 lamToLet :: Term -> Term
610 lamToLet tm = lamToLet' args f
612 (f, args) = unApply tm
614 lamToLet' :: [Term] -> Term -> Term
615 lamToLet' (v:vs) (Bind n (Lam rig ty) tm) = Bind n (Let rig ty v) $ lamToLet' vs tm
617 lamToLet' vs tm = error $
618 "Erasure.hs:lamToLet': unexpected input: "
619 ++ "vs = " ++ show vs ++ ", tm = " ++ show tm
621 -- split "\x_i -> T(x_i)" into [x_i] and T
622 unfoldLams :: Term -> ([Name], Term)
623 unfoldLams (Bind n (Lam _ ty) t) = let (ns,t') = unfoldLams t in (n:ns, t')
624 unfoldLams t = ([], t)
626 union :: Deps -> Deps -> Deps
627 union = M.unionWith (M.unionWith S.union)
629 unionMap :: (a -> Deps) -> [a] -> Deps
630 unionMap f = M.unionsWith (M.unionWith S.union) . map f
632-- | Make a field name out of a data constructor name and field number.
633mkFieldName :: Name -> Int -> Name
634mkFieldName ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list