diff --git a/cabal.project b/cabal.project index 7435d31..a12fd94 100644 --- a/cabal.project +++ b/cabal.project @@ -1,8 +1,2 @@ packages: agda2lambox.cabal - -source-repository-package - type: git - location: https://github.com/agda/agda - tag: 5c29109f8212ef61b0091d62ef9c8bfdfa16cf36 - constraints: Agda +debug diff --git a/flake.nix b/flake.nix index a457e60..769035b 100644 --- a/flake.nix +++ b/flake.nix @@ -4,10 +4,6 @@ inputs = { nixpkgs.url = "github:NixOS/nixpkgs"; flake-utils.url = "github:numtide/flake-utils"; - agda = { - url = "github:agda/agda"; - flake = false; - }; }; outputs = @@ -35,7 +31,6 @@ haskellPackages = prev.haskellPackages.extend ( hfinal: hprev: { sexpresso = hLib.doJailbreak (hLib.markUnbroken hprev.sexpresso); - Agda = hLib.dontCheck (hLib.dontHaddock (hfinal.callCabal2nix "Agda" inputs.agda { })); agda2lambox = hLib.doJailbreak (hfinal.callCabal2nix "agda2lambox" ./. { }); } ); diff --git a/src/Agda/Utils/Treeless.hs b/src/Agda/Utils/Treeless.hs index 98a7c13..a8c822b 100644 --- a/src/Agda/Utils/Treeless.hs +++ b/src/Agda/Utils/Treeless.hs @@ -48,6 +48,7 @@ import Agda.Compiler.Treeless.AsPatterns import Agda.Compiler.Treeless.Builtin import Agda.Compiler.Treeless.Erase import Agda.Compiler.Treeless.Identity +import Agda.Compiler.Treeless.Simplify import Agda.Compiler.Treeless.Uncase import Agda.Compiler.Treeless.Unused import Agda.Compiler.Treeless.NormalizeNames @@ -85,7 +86,7 @@ getCompiledClauses q = do reportSDoc "treeless.convert" 70 $ caseMaybe mst "-- not using split tree" $ \st -> "-- using split tree" $$ pretty st - CC.compileClauses' translate cs mst + CC.compileClauses' q translate cs mst -- ** Types of pipelines; different backends might use their own custom pipeline. type BuildPipeline = Int -> QName -> Pipeline @@ -109,7 +110,7 @@ data CCSubst = EraseUnused | IgnoreUnused deriving Eq data CCEnv = CCEnv { ccCxt :: CCContext -- ^ Maps case tree de-bruijn indices to TTerm de-bruijn indices. - , ccCatchAll :: Maybe Int + , ccCatchall :: Maybe Int -- ^ TTerm de-bruijn index of the current catch all. -- If an inner case has no catch-all clause, we use the one from its parent. , ccEvaluation :: EvaluationStrategy @@ -124,7 +125,7 @@ type CCConfig = (EvaluationStrategy, CCSubst) initCCEnv :: CCConfig -> CCEnv initCCEnv (eval, su) = CCEnv { ccCxt = [] - , ccCatchAll = Nothing + , ccCatchall = Nothing , ccEvaluation = eval , ccSubstUnused = su } @@ -286,14 +287,14 @@ casetree cc = do CC.Case _ (CC.Branches True _ _ _ Just{} _ _) -> __IMPOSSIBLE__ CC.Case (Arg _ n) (CC.Branches True conBrs _ _ Nothing _ _) -> lambdasUpTo n $ do mkRecord =<< traverse casetree (CC.content <$> conBrs) - CC.Case (Arg i n) (CC.Branches False conBrs etaBr litBrs catchAll _ lazy) -> lambdasUpTo (n + 1) $ do + CC.Case (Arg i n) (CC.Branches False conBrs etaBr litBrs catchall _ lazy) -> lambdasUpTo (n + 1) $ do -- re #3733 TODO: revise when compiling --cubical conBrs <- fmap Map.fromList $ filterM (isConstructor . fst) (Map.toList conBrs) -- We can treat eta-matches as regular matches here. let conBrs' = caseMaybe etaBr conBrs $ \ (c, br) -> Map.insertWith (\ new old -> old) (conName c) br conBrs if Map.null conBrs' && Map.null litBrs then do -- there are no branches, just return default - updateCatchAll catchAll fromCatchAll + updateCatchall catchall fromCatchall else do -- Get the type of the scrutinee. caseTy <- @@ -311,9 +312,9 @@ casetree cc = do ([], LitQName _ : _) -> return C.CTQName _ -> __IMPOSSIBLE__ - updateCatchAll catchAll $ do + updateCatchall catchall $ do x <- asks (lookupLevel n . ccCxt) - def <- fromCatchAll + def <- fromCatchall let caseInfo = C.CaseInfo { caseType = caseTy , caseLazy = lazy @@ -327,8 +328,8 @@ casetree cc = do where -- normally, Agda should make sure that a pattern match is total, -- so we set the default to unreachable if no default has been provided. - fromCatchAll :: CC C.TTerm - fromCatchAll = asks (maybe C.tUnreachable C.TVar . ccCatchAll) + fromCatchall :: CC C.TTerm + fromCatchall = asks (maybe C.tUnreachable C.TVar . ccCatchall) commonArity :: CC.CompiledClauses -> Int commonArity cc = @@ -349,21 +350,21 @@ commonArity cc = wArities cxt (WithArity k c) = map (\ x -> x - k + 1) $ arities (cxt - 1 + k) c -updateCatchAll :: Maybe CC.CompiledClauses -> (CC C.TTerm -> CC C.TTerm) -updateCatchAll Nothing cont = cont -updateCatchAll (Just cc) cont = do +updateCatchall :: Maybe CC.CompiledClauses -> (CC C.TTerm -> CC C.TTerm) +updateCatchall Nothing cont = cont +updateCatchall (Just cc) cont = do def <- casetree cc cxt <- asks ccCxt reportS "treeless.convert.lambdas" 40 $ - [ "-- updateCatchAll:" + [ "-- updateCatchall:" , "-- cxt =" <+> prettyPure cxt , "-- def =" <+> prettyPure def ] - local (\ e -> e { ccCatchAll = Just 0, ccCxt = shift 1 cxt }) $ do + local (\ e -> e { ccCatchall = Just 0, ccCxt = shift 1 cxt }) $ do C.mkLet def <$> cont -- | Shrinks or grows the context to the given size. --- Does not update the catchAll expression, the catchAll expression +-- Does not update the catchall expression, the catchall expression -- MUST NOT be used inside `cont`. withContextSize :: Int -> CC C.TTerm -> CC C.TTerm withContextSize n cont = do @@ -430,8 +431,8 @@ withContextSize n cont = do cont <&> (`C.mkTApp` map C.TVar (downFrom diff')) -- | Prepend the given positive number of lambdas. --- Does not update the catchAll expression, --- the catchAll expression must be updated separately (or not be used). +-- Does not update the catchall expression, +-- the catchall expression must be updated separately (or not be used). createLambdas :: Int -> CC C.TTerm -> CC C.TTerm createLambdas diff cont = do unless (diff >= 1) __IMPOSSIBLE__ @@ -446,7 +447,7 @@ createLambdas diff cont = do cont <&> \ t -> List.iterate C.TLam t !! diff -- | Adds lambdas until the context has at least the given size. --- Updates the catchAll expression to take the additional lambdas into account. +-- Updates the catchall expression to take the additional lambdas into account. lambdasUpTo :: Int -> CC C.TTerm -> CC C.TTerm lambdasUpTo n cont = do diff <- asks (((n -) . length) . ccCxt) @@ -454,22 +455,22 @@ lambdasUpTo n cont = do if diff <= 0 then cont -- no new lambdas needed else do createLambdas diff $ do - asks ccCatchAll >>= \case - Just catchAll -> do + asks ccCatchall >>= \case + Just catchall -> do cxt <- asks ccCxt reportS "treeless.convert.lambdas" 40 $ [ "lambdasUpTo: n =" <+> (text . show) n , " diff =" <+> (text . show) n - , " catchAll =" <+> prettyPure catchAll + , " catchall =" <+> prettyPure catchall , " ccCxt =" <+> prettyPure cxt ] -- the catch all doesn't know about the additional lambdas, so just directly -- apply it again to the newly introduced lambda arguments. -- we also bind the catch all to a let, to avoid code duplication - local (\e -> e { ccCatchAll = Just 0 + local (\e -> e { ccCatchall = Just 0 , ccCxt = shift 1 cxt }) $ do - let catchAllArgs = map C.TVar $ downFrom diff - C.mkLet (C.mkTApp (C.TVar $ catchAll + diff) catchAllArgs) + let catchallArgs = map C.TVar $ downFrom diff + C.mkLet (C.mkTApp (C.TVar $ catchall + diff) catchallArgs) <$> cont Nothing -> cont @@ -499,7 +500,7 @@ replaceVar x n cont = do (ys, _:zs) = splitAt i cxt -- compute the de-bruijn indexes of the newly inserted variables ixs = [0..(n - 1)] - local (\e -> e { ccCxt = upd (ccCxt e) , ccCatchAll = (+ n) <$> ccCatchAll e }) $ + local (\e -> e { ccCxt = upd (ccCxt e) , ccCatchall = (+ n) <$> ccCatchall e }) $ cont @@ -651,4 +652,3 @@ substArgs = traverse substArg substArg :: Arg I.Term -> CC C.TTerm substArg x | usableModality x = substTerm (unArg x) | otherwise = return C.TErased - diff --git a/src/Main.hs b/src/Main.hs index 9f045eb..fde2e12 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -13,7 +13,7 @@ import Data.Maybe ( fromMaybe ) import Data.Version ( showVersion ) import Data.Text ( pack ) import GHC.Generics ( Generic ) -import System.Console.GetOpt ( OptDescr(Option), ArgDescr(..) ) +import Agda.Utils.GetOpt ( OptDescr(Option), ArgDescr(..) ) import System.Directory ( createDirectoryIfMissing ) import System.FilePath ( (), (-<.>) ) import Data.Text.Lazy.IO qualified as LText