GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-26 17:32:30 +03:00
Code Issues Projects Releases Wiki Activity

Make a module for the instantiation code

Browse Source
This commit is contained in:
Iavor Diatchki 2022-12-12 16:55:50 -08:00
parent f834e24313
commit 02a5e80c53
6 changed files with 65 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
cryptol.cabal
View File

@ -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,

2
src/Cryptol/ModuleSystem/Base.hs
View File

@ -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

6
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -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) =

8
src/Cryptol/Parser/AST.hs
View File

@ -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) =

67
src/Cryptol/TypeCheck/Module.hs
View File

@ -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)

16
src/Cryptol/TypeCheck/ModuleBacktickInstance.hs Normal file
View File

@ -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