===========================================================
.___ __ __
_________________ __ __ __| _/|__|/ |_
/ ___\_` __ \__ \ | | \/ __ | | \\_ __\
/ /_/ > | \// __ \| | / /_/ | | || |
\___ /|__| (____ /____/\____ | |__||__|
/_____/ \/ \/
grep rough audit - static analysis tool
v2.8 written by @Wireghoul
=================================[justanotherhacker.com]===
agda-2.6.1/doc/release-notes/2.5.1.md-76-
agda-2.6.1/doc/release-notes/2.5.1.md:77: Environment variables in the paths (of the form `$VAR` or `${VAR}`)
agda-2.6.1/doc/release-notes/2.5.1.md-78- are expanded. The location of the libraries file used can be
##############################################
agda-2.6.1/doc/release-notes/2.4.0.md-62- Agda-2.3.4 on a standard single-ghc Linux system it would be
agda-2.6.1/doc/release-notes/2.4.0.md:63: `$HOME/.cabal/share/Agda-2.3.4` or something similar.
agda-2.6.1/doc/release-notes/2.4.0.md-64-
##############################################
agda-2.6.1/dist/build/Agda/Syntax/Parser/Parser.hs-8064-
agda-2.6.1/dist/build/Agda/Syntax/Parser/Parser.hs:8065:indexShortOffAddr (HappyA# arr) off =
agda-2.6.1/dist/build/Agda/Syntax/Parser/Parser.hs-8066- Happy_GHC_Exts.narrow16Int# i
##############################################
agda-2.6.1/dist/build/Agda/Syntax/Parser/Lexer.hs-1498-{-# INLINE alexIndexInt16OffAddr #-}
agda-2.6.1/dist/build/Agda/Syntax/Parser/Lexer.hs:1499:alexIndexInt16OffAddr (AlexA# arr) off =
agda-2.6.1/dist/build/Agda/Syntax/Parser/Lexer.hs-1500-#ifdef WORDS_BIGENDIAN
##############################################
agda-2.6.1/dist/build/Agda/Syntax/Parser/Lexer.hs-1515-{-# INLINE alexIndexInt32OffAddr #-}
agda-2.6.1/dist/build/Agda/Syntax/Parser/Lexer.hs:1516:alexIndexInt32OffAddr (AlexA# arr) off =
agda-2.6.1/dist/build/Agda/Syntax/Parser/Lexer.hs-1517-#ifdef WORDS_BIGENDIAN
##############################################
agda-2.6.1/src/full/Agda/Utils/ListT.hs-99-mapMListT_alt f = runMListT . foldListT cons (return nilListT)
agda-2.6.1/src/full/Agda/Utils/ListT.hs:100: where cons a ml = consMListT (f a) <$> ml
agda-2.6.1/src/full/Agda/Utils/ListT.hs-101-
##############################################
agda-2.6.1/src/full/Agda/Interaction/Library.hs-305- let ann (ln, fp) (e, ws) = (first (Just pos,) e, map (LibWarning pos) ws)
agda-2.6.1/src/full/Agda/Interaction/Library.hs:306: where pos = LibPositionInfo (lfPath <$> mlibFile) ln fp
agda-2.6.1/src/full/Agda/Interaction/Library.hs-307- let (xs, warns) = unzip $ zipWith ann files (map runP rs')
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/SizedTypes.hs-151- reportSDoc "tc.size" 60 $
agda-2.6.1/src/full/Agda/TypeChecking/SizedTypes.hs:152: text ("minSizeVal (n:ns) = " ++ show (take (length ts + 2) $ n:ns) ++
agda-2.6.1/src/full/Agda/TypeChecking/SizedTypes.hs-153- " t =") <+> (text . show) t -- prettyTCM t -- Wrong context!
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Serialise.hs-286- | otherwise = Just $ B.runGet getH $ L.take 16 s
agda-2.6.1/src/full/Agda/TypeChecking/Serialise.hs:287: where getH = (,) <$> B.get <*> B.get
agda-2.6.1/src/full/Agda/TypeChecking/Serialise.hs-288-
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Injectivity.hs-163-updateHeads f m = joinHeadMaps <$> mapM f' (Map.toList m)
agda-2.6.1/src/full/Agda/TypeChecking/Injectivity.hs:164: where f' (h, c) = (`Map.singleton` c) <$> f h c
agda-2.6.1/src/full/Agda/TypeChecking/Injectivity.hs-165-
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Substitute.hs-609- EmptyTel `abstract` tel = tel
agda-2.6.1/src/full/Agda/TypeChecking/Substitute.hs:610: ExtendTel arg xtel `abstract` tel = ExtendTel arg $ xtel <&> (`abstract` tel)
agda-2.6.1/src/full/Agda/TypeChecking/Substitute.hs-611-
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Monad/MetaVars.hs-420- mapMaybe f . filter (not . ipSolved . snd) . Map.toList <$> useR stInteractionPoints
agda-2.6.1/src/full/Agda/TypeChecking/Monad/MetaVars.hs:421: where f (ii, ip) = (ii,) <$> ipMeta ip
agda-2.6.1/src/full/Agda/TypeChecking/Monad/MetaVars.hs-422-
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Rules/LHS.hs-540-
agda-2.6.1/src/full/Agda/TypeChecking/Rules/LHS.hs:541: where continue = (eq:) <$> check vars eqs
agda-2.6.1/src/full/Agda/TypeChecking/Rules/LHS.hs-542-
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Rules/LHS.hs-1475-
agda-2.6.1/src/full/Agda/TypeChecking/Rules/LHS.hs:1476: where notData = liftTCM $ SplitError . NotADatatype <$> buildClosure a
agda-2.6.1/src/full/Agda/TypeChecking/Rules/LHS.hs-1477-
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Application.hs-1242- az = unArg a `apply` [iz]
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Application.hs:1243: ty <- elInf $ primPartial <#> (pure $ unArg l `apply` [iz]) <@> (pure $ unArg phi) <@> (pure $ unArg a `apply` [iz])
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Application.hs-1244- bAz <- el' (pure $ lz) (pure $ az)
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs-383- case cmd of
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs:384: DoHComp -> return $ Con con ConOSystem (map Apply $ withArgInfo fsT bodies)
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs:385: DoTransp | null boundary -> return $ Con con ConOSystem (map Apply $ withArgInfo fsT bodies)
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs-386- | otherwise -> do
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs-567- -- Γ , (d : T) ⊢ Φ[n ↦ proj n d]
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs:568: fieldTypes = ([ Def f [] `apply` [argN $ var 0] | f <- reverse names ] ++# raiseS 1) `applySubst`
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs-569- flattenTel fsT -- Γ , Φ ⊢ Φ
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs-578- conp = defaultNamedArg $ ConP con cpi $ teleNamedArgs fsT
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs:579: sigma = Con con ConOSystem (map Apply $ teleArgs fsT) `consS` raiseS (size fsT)
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs-580- clause = empty
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs-961- -- Γ, i : I ⊢ (flatten Φ')[n ↦ f_n (fillR Γ i)]
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs:962: filled_types = parallelS [raise 1 fillTerm `apply` [argN $ var 0] `applyProj` (unArg fn)
agda-2.6.1/src/full/Agda/TypeChecking/Rules/Data.hs-963- | fn <- reverse fns] `applySubst`
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Primitive/Cubical.hs-225- y' <- return $ sin `apply` [a,bA ,phi,argN $ unArg y]
agda-2.6.1/src/full/Agda/TypeChecking/Primitive/Cubical.hs:226: w' <- return $ sin `apply` [a,argN $ path `apply` [a,bA,x,y],phi,argN $ unArg w]
agda-2.6.1/src/full/Agda/TypeChecking/Primitive/Cubical.hs-227- redReturn $ unArg f `apply` [phi, defaultArg y', defaultArg w']
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Primitive/Cubical.hs-1582- tEFun <- getTerm builtin_unglue builtinEquivFun
agda-2.6.1/src/full/Agda/TypeChecking/Primitive/Cubical.hs:1583: redReturn $ tEFun `apply` [lb,la,argH $ unArg bT `apply` [argOne],bA, argN $ unArg e `apply` [argOne],b]
agda-2.6.1/src/full/Agda/TypeChecking/Primitive/Cubical.hs-1584- _ -> do
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Primitive/Cubical.hs-1770- transpTel (Abs "j" $ raise 1 delta `lazyAbsApp` (imin `apply` (map argN [var 0, raise 1 r])))
agda-2.6.1/src/full/Agda/TypeChecking/Primitive/Cubical.hs:1771: (imax `apply` [argN $ ineg `apply` [argN r], argN phi])
agda-2.6.1/src/full/Agda/TypeChecking/Primitive/Cubical.hs-1772- args
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Reduce/Fast.hs-1000- runAM' (Eval cl (NatSucK m : ctrl)) =
agda-2.6.1/src/full/Agda/TypeChecking/Reduce/Fast.hs:1001: runAM (Eval (mkValue (notBlocked ()) $ plus m cl) ctrl)
agda-2.6.1/src/full/Agda/TypeChecking/Reduce/Fast.hs-1002- where
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs-203- -- other cases
agda-2.6.1/src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs:204: Label Lt w `meet` Label Lt w' = Label Lt $ w `meet` w'
agda-2.6.1/src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs:205: Label Le w `meet` Label Le w' = Label Le $ w `meet` w'
agda-2.6.1/src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs:206: Label Lt w `meet` Label Le w' = Label Lt $ w `meet` succ w'
agda-2.6.1/src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs:207: Label Le w `meet` Label Lt w' = Label Lt $ succ w `meet` w'
agda-2.6.1/src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs-208-
##############################################
agda-2.6.1/src/full/Agda/TypeChecking/Pretty/Call.hs-27-sayWhere :: MonadPretty m => HasRange a => a -> m Doc -> m Doc
agda-2.6.1/src/full/Agda/TypeChecking/Pretty/Call.hs:28:sayWhere x d = applyUnless (null r) (prettyTCM r $$) d
agda-2.6.1/src/full/Agda/TypeChecking/Pretty/Call.hs-29- where r = getRange x
##############################################
agda-2.6.1/src/full/Agda/Syntax/Parser/Parser.y-667- return $ Lam r bs (AbsurdLam r h)
agda-2.6.1/src/full/Agda/Syntax/Parser/Parser.y:668: where r = fuseRange $1 bs
agda-2.6.1/src/full/Agda/Syntax/Parser/Parser.y-669- Right es -> do -- it is of the form @\ { p1 ... () }@
##############################################
agda-2.6.1/.pc/var-lib-agda/src/full/Agda/Interaction/Library.hs-299- let ann (ln, fp) (e, ws) = (first (Just pos,) e, map (LibWarning pos) ws)
agda-2.6.1/.pc/var-lib-agda/src/full/Agda/Interaction/Library.hs:300: where pos = LibPositionInfo (lfPath <$> mlibFile) ln fp
agda-2.6.1/.pc/var-lib-agda/src/full/Agda/Interaction/Library.hs-301- let (xs, warns) = unzip $ zipWith ann files (map runP rs')