From 02a5e80c53d08edf469f101d454db1d196a95ab6 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 12 Dec 2022 16:55:50 -0800 Subject: [PATCH] Make a module for the instantiation code --- cryptol.cabal | 1 + src/Cryptol/ModuleSystem/Base.hs | 2 +- src/Cryptol/ModuleSystem/Renamer.hs | 6 +- src/Cryptol/Parser/AST.hs | 8 +-- src/Cryptol/TypeCheck/Module.hs | 67 +++++++++++-------- .../TypeCheck/ModuleBacktickInstance.hs | 16 +++++ 6 files changed, 65 insertions(+), 35 deletions(-) create mode 100644 src/Cryptol/TypeCheck/ModuleBacktickInstance.hs diff --git a/cryptol.cabal b/cryptol.cabal index af43c616..217b93f3 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -177,6 +177,7 @@ library Cryptol.TypeCheck.FFI.FFIType, Cryptol.TypeCheck.Module, Cryptol.TypeCheck.ModuleInstance, + Cryptol.TypeCheck.ModuleBacktickInstance, Cryptol.TypeCheck.Solver.Types, Cryptol.TypeCheck.Solver.SMT, diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index fa61748e..035fa6e5 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -468,7 +468,7 @@ findDeps' m = DefaultInstArg a -> loadInstArg a DefaultInstAnonArg ds -> mconcat (map depsOfDecl ds) NamedInstArgs args -> mconcat (map loadNamedInstArg args) - BacktickInstnace -> mempty + BacktickInstance -> mempty in fds <> ads InterfaceModule s -> mconcat (map loadImpD (sigImports s)) where diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index c8274605..36d7a34c 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -292,7 +292,7 @@ checkFunctorArgs args = panic "checkFunctorArgs" ["Nested DefaultInstAnonArg"] DefaultInstArg l -> checkArg l NamedInstArgs as -> mapM_ checkNamedArg as - BacktickInstnace -> pure () + BacktickInstance -> pure () where checkNamedArg (ModuleInstanceNamedArg _ l) = checkArg l @@ -481,7 +481,7 @@ renameTopDecls' ds = DefaultInstArg arg -> depsOfArg arg NamedInstArgs args -> concatMap depsOfNamedArg args DefaultInstAnonArg {} -> [] - BacktickInstnace -> [] + BacktickInstance -> [] where depsOfNamedArg (ModuleInstanceNamedArg _ a) = depsOfArg a depsOfArg a = case thing a of @@ -795,7 +795,7 @@ instance Rename ModuleInstanceArgs where DefaultInstArg a -> DefaultInstArg <$> rnLocated rename a NamedInstArgs xs -> NamedInstArgs <$> traverse rename xs DefaultInstAnonArg {} -> panic "rename" ["DefaultInstAnonArg"] - BacktickInstnace -> pure BacktickInstnace + BacktickInstance -> pure BacktickInstance instance Rename ModuleInstanceNamedArg where rename (ModuleInstanceNamedArg x m) = diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index f2997319..6c78a019 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -282,9 +282,9 @@ data ModuleInstanceArgs name = | NamedInstArgs [ModuleInstanceNamedArg name] - | BacktickInstnace + | BacktickInstance -- ^ The module instance is computed by adding the functor arguments - -- as explicit parameters to all declarations + -- as explicit parameters to all declarations. deriving (Show, Generic, NFData) -- | A named argument in a functor instantiation @@ -867,7 +867,7 @@ instance (Show name, PPName name) => PP (ModuleInstanceArgs name) where DefaultInstArg x -> braces (pp (thing x)) DefaultInstAnonArg ds -> "where" $$ indent 2 (vcat (map pp ds)) NamedInstArgs xs -> braces (commaSep (map pp xs)) - BacktickInstnace -> "{}" + BacktickInstance -> "{}" instance (Show name, PPName name) => PP (ModuleInstanceNamedArg name) where ppPrec _ (ModuleInstanceNamedArg x y) = pp (thing x) <+> "=" <+> pp (thing y) @@ -1363,7 +1363,7 @@ instance NoPos (ModuleInstanceArgs name) where DefaultInstArg a -> DefaultInstArg (noPos a) DefaultInstAnonArg ds -> DefaultInstAnonArg (noPos ds) NamedInstArgs xs -> NamedInstArgs (noPos xs) - BacktickInstnace -> BacktickInstnace + BacktickInstance -> BacktickInstance instance NoPos (ModuleInstanceNamedArg name) where noPos (ModuleInstanceNamedArg x y) = diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 102b1f9f..d6497ab8 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -24,6 +24,7 @@ import Cryptol.TypeCheck.Solve(proveImplication) import Cryptol.TypeCheck.Monad import Cryptol.TypeCheck.Instantiate(instantiateWith) import Cryptol.TypeCheck.ModuleInstance +import Cryptol.TypeCheck.ModuleBacktickInstance(doBacktickInstance) doFunctorInst :: Located (P.ImpName Name) {- ^ Name for the new module -} -> @@ -39,24 +40,25 @@ doFunctorInst m f as inst doc = inRange (srcRange m) do mf <- lookupFunctor (thing f) argIs <- checkArity (srcRange f) mf as - (tySus,decls) <- unzip <$> mapM checkArg argIs + m2 <- case argIs of + UseArgs ais -> + do (tySus,decls) <- unzip <$> mapM checkArg ais + let ?tSu = mergeDistinctSubst tySus + ?vSu = inst + let m1 = moduleInstance mf + m2 = m1 { mName = m + , mDoc = Nothing + , mParamTypes = mempty + , mParamFuns = mempty + , mParamConstraints = mempty + , mParams = mempty + , mDecls = map NonRecursive (concat decls) ++ + mDecls m1 + } + newGoals CtModuleInstance (map thing (mParamConstraints m1)) + pure m2 - - let ?tSu = mergeDistinctSubst tySus - ?vSu = inst - let m1 = moduleInstance mf - m2 = m1 { mName = m - , mDoc = Nothing - , mParamTypes = mempty - , mParamFuns = mempty - , mParamConstraints = mempty - , mParams = mempty - -- XXX: Should we modify `mImports` to record dependencies - -- on parameters? - , mDecls = map NonRecursive (concat decls) ++ mDecls m1 - } - - newGoals CtModuleInstance (map thing (mParamConstraints m1)) + AddParamsToDecls -> doBacktickInstance m mf inst case thing m of P.ImpTop mn -> newModuleScope mn (mExports m2) @@ -75,6 +77,15 @@ doFunctorInst m f as inst doc = P.ImpNested {} -> endSubmodule >> pure Nothing + +data ActualArg = + UseParameter ModParam -- ^ Instantiate using this parameter + | UseModule (IfaceG ()) -- ^ Instantiate using this module + +data ActualArgs = + UseArgs [(Range, ModParam, ActualArg)] + | AddParamsToDecls + {- | Validate a functor application, just checking the argument names. @@ -88,7 +99,7 @@ checkArity :: Range {- ^ Location for reporting errors -} -> ModuleG () {- ^ The functor being instantiated -} -> P.ModuleInstanceArgs Name {- ^ The arguments -} -> - InferM [ (Range, ModParam, Either ModParam (IfaceG ())) ] + InferM ActualArgs {- ^ Associates functor parameters with the interfaces of the instantiating modules -} checkArity r mf args = @@ -102,8 +113,9 @@ checkArity r mf args = P.NamedInstArgs as -> checkArgs [] ps0 as - P.DefaultInstAnonArg {} -> panic "checkArity" [ "DefaultInstAnonArg" ] + P.BacktickInstance -> pure AddParamsToDecls + P.DefaultInstAnonArg {} -> panic "checkArity" [ "DefaultInstAnonArg" ] where ps0 = mParams mf @@ -112,13 +124,13 @@ checkArity r mf args = [] -> do forM_ (Map.keys ps) \p -> recordErrorLoc (Just r) (FunctorInstanceMissingArgument p) - pure done + pure (UseArgs done) P.ModuleInstanceNamedArg ll lm : more -> case Map.lookup (thing ll) ps of Just i -> do arg <- case thing lm of - P.ModuleArg m -> Just . Right <$> lookupModule m + P.ModuleArg m -> Just . UseModule <$> lookupModule m P.ParameterArg p -> do mb <- lookupModParam p case mb of @@ -126,7 +138,7 @@ checkArity r mf args = do inRange (srcRange lm) (recordError (MissingModParam p)) pure Nothing - Just a -> pure (Just (Left a)) + Just a -> pure (Just (UseParameter a)) let next = case arg of Nothing -> done Just a -> (srcRange lm, i, a) : done @@ -148,7 +160,7 @@ Returns: values. -} checkArg :: - (Range, ModParam, Either ModParam (IfaceG ())) -> InferM (Subst, [Decl]) + (Range, ModParam, ActualArg) -> InferM (Subst, [Decl]) checkArg (r,expect,actual') = do tRens <- mapM (checkParamType r tyMap) (Map.toList (mpnTypes params)) let renSu = listParamSubst (concat tRens) @@ -175,15 +187,16 @@ checkArg (r,expect,actual') = vMap :: Map Ident (Name, Schema) (tyMap,vMap) = case actual' of - Left mp -> ( nameMapToIdentMap fromTP (mpnTypes ps) - , nameMapToIdentMap fromVP (mpnFuns ps) - ) + UseParameter mp -> + ( nameMapToIdentMap fromTP (mpnTypes ps) + , nameMapToIdentMap fromVP (mpnFuns ps) + ) where ps = mpParameters mp fromTP tp = (mtpKind tp, TVar (TVBound (mtpParam tp))) fromVP vp = (mvpName vp, mvpType vp) - Right actual -> + UseModule actual -> ( Map.unions [ nameMapToIdentMap fromTS (ifTySyns decls) , nameMapToIdentMap fromNewtype (ifNewtypes decls) , nameMapToIdentMap fromPrimT (ifAbstractTypes decls) diff --git a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs new file mode 100644 index 00000000..46348024 --- /dev/null +++ b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs @@ -0,0 +1,16 @@ +module Cryptol.TypeCheck.ModuleBacktickInstance where + +import Data.Map(Map) +import qualified Data.Map as Map + +import Cryptol.Parser.Position (Located(..), thing) +import qualified Cryptol.Parser.AST as P +import Cryptol.TypeCheck.AST +import Cryptol.TypeCheck.Monad + +doBacktickInstance :: + Located (P.ImpName Name) {- ^ Name for the new module -} -> + ModuleG () {- ^ The functor -} -> + Map Name Name {- ^ The instantiation: functor name -> instance name -} -> + InferM (ModuleG (Located (P.ImpName Name))) +doBacktickInstance m mf inst = undefined