mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Top-level instatiations.
This commit is contained in:
parent
6bd2ab6bc8
commit
e774861966
@ -18,7 +18,7 @@
|
||||
module Cryptol.ModuleSystem.Base where
|
||||
|
||||
import qualified Control.Exception as X
|
||||
import Control.Monad (unless,when)
|
||||
import Control.Monad (unless,when,forM)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Monoid ((<>))
|
||||
import Data.Text.Encoding (decodeUtf8')
|
||||
@ -116,7 +116,7 @@ noPat a = do
|
||||
|
||||
-- Parsing ---------------------------------------------------------------------
|
||||
|
||||
parseModule :: ModulePath -> ModuleM (Fingerprint, P.Module PName)
|
||||
parseModule :: ModulePath -> ModuleM (Fingerprint, [P.Module PName])
|
||||
parseModule path = do
|
||||
getBytes <- getByteReader
|
||||
|
||||
@ -160,26 +160,30 @@ loadModuleByPath :: FilePath -> ModuleM T.Module
|
||||
loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
|
||||
let fileName = takeFileName path
|
||||
foundPath <- findFile fileName
|
||||
(fp, pm) <- parseModule (InFile foundPath)
|
||||
let n = thing (P.mName pm)
|
||||
(fp, pms) <- parseModule (InFile foundPath)
|
||||
last <$>
|
||||
forM pms \pm ->
|
||||
do let n = thing (P.mName pm)
|
||||
|
||||
-- Check whether this module name has already been loaded from a different file
|
||||
env <- getModuleEnv
|
||||
-- path' is the resolved, absolute path, used only for checking
|
||||
-- whether it's already been loaded
|
||||
path' <- io (canonicalizePath foundPath)
|
||||
-- Check whether this module name has already been loaded from a
|
||||
-- different file
|
||||
env <- getModuleEnv
|
||||
-- path' is the resolved, absolute path, used only for checking
|
||||
-- whether it's already been loaded
|
||||
path' <- io (canonicalizePath foundPath)
|
||||
|
||||
case lookupModule n env of
|
||||
-- loadModule will calculate the canonical path again
|
||||
Nothing -> doLoadModule False (FromModule n) (InFile foundPath) fp pm
|
||||
Just lm
|
||||
| path' == loaded -> return (lmModule lm)
|
||||
| otherwise -> duplicateModuleName n path' loaded
|
||||
where loaded = lmModuleId lm
|
||||
case lookupModule n env of
|
||||
-- loadModule will calculate the canonical path again
|
||||
Nothing -> doLoadModule False (FromModule n) (InFile foundPath) fp pm
|
||||
Just lm
|
||||
| path' == loaded -> return (lmModule lm)
|
||||
| otherwise -> duplicateModuleName n path' loaded
|
||||
where loaded = lmModuleId lm
|
||||
|
||||
|
||||
-- | Load a module, unless it was previously loaded.
|
||||
loadModuleFrom :: Bool {- ^ quiet mode -} -> ImportSource -> ModuleM (ModulePath,T.Module)
|
||||
loadModuleFrom ::
|
||||
Bool {- ^ quiet mode -} -> ImportSource -> ModuleM (ModulePath,T.Module)
|
||||
loadModuleFrom quiet isrc =
|
||||
do let n = importedModule isrc
|
||||
mb <- getLoadedMaybe n
|
||||
@ -188,9 +192,9 @@ loadModuleFrom quiet isrc =
|
||||
Nothing ->
|
||||
do path <- findModule n
|
||||
errorInFile path $
|
||||
do (fp, pm) <- parseModule path
|
||||
m <- doLoadModule quiet isrc path fp pm
|
||||
return (path,m)
|
||||
do (fp, pms) <- parseModule path
|
||||
ms <- mapM (doLoadModule quiet isrc path fp) pms
|
||||
return (path,last ms)
|
||||
|
||||
-- | Load dependencies, typecheck, and add to the eval environment.
|
||||
doLoadModule ::
|
||||
@ -217,7 +221,8 @@ doLoadModule quiet isrc path fp pm0 =
|
||||
let ?evalPrim = \i -> Right <$> Map.lookup i tbl
|
||||
callStacks <- getCallStacks
|
||||
let ?callStacks = callStacks
|
||||
unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm)
|
||||
unless (T.isParametrizedModule tcm)
|
||||
$ modifyEvalEnv (E.moduleEnv Concrete tcm)
|
||||
loadedModule path fp nameEnv tcm
|
||||
|
||||
return tcm
|
||||
@ -299,11 +304,7 @@ addPrelude m
|
||||
newDef =
|
||||
case mDef m of
|
||||
NormalModule ds -> NormalModule (importPrelude : ds)
|
||||
FunctorInstance f as ins -> FunctorInstance f as' ins
|
||||
where
|
||||
as' = case as of
|
||||
DefaultInstAnonArg ds -> DefaultInstAnonArg (importPrelude : ds)
|
||||
_ -> as
|
||||
FunctorInstance f as ins -> FunctorInstance f as ins
|
||||
|
||||
importedMods = map (P.iModule . P.thing) (P.mImports m)
|
||||
importPrelude = P.DImport P.Located
|
||||
@ -416,10 +417,10 @@ getPrimMap =
|
||||
checkModule ::
|
||||
ImportSource -> ModulePath -> P.Module PName ->
|
||||
ModuleM (R.NamingEnv, T.Module)
|
||||
checkModule isrc path m =
|
||||
case mDef m of
|
||||
NormalModule _ -> checkSingleModule T.tcModule isrc path m
|
||||
checkModule isrc path m = checkSingleModule T.tcModule isrc path m
|
||||
{-
|
||||
case mDef m of
|
||||
NormalModule _ ->
|
||||
FunctorInstanceAnon fmName _ ->
|
||||
do mbtf <- getLoadedMaybe (thing fmName)
|
||||
case mbtf of
|
||||
|
@ -42,7 +42,6 @@ import Cryptol.ModuleSystem.Interface
|
||||
|
||||
data TopDef = TopMod ModName (Mod ())
|
||||
| TopInst ModName (ImpName PName) (ModuleInstanceArgs PName)
|
||||
| TopInstAnon ModName ModName (Mod ())
|
||||
|
||||
-- | Things defined by a module
|
||||
data Mod a = Mod
|
||||
@ -130,9 +129,7 @@ topModuleDefs :: Module PName -> ModBuilder TopDef
|
||||
topModuleDefs m =
|
||||
case mDef m of
|
||||
NormalModule ds -> TopMod mname <$> declsToMod (Just (TopModule mname)) ds
|
||||
FunctorInstance f as _ ->
|
||||
pure (TopInst mname (thing f) as)
|
||||
|
||||
FunctorInstance f as _ -> pure (TopInst mname (thing f) as)
|
||||
where
|
||||
mname = thing (mName m)
|
||||
|
||||
|
@ -131,12 +131,7 @@ renameModule m0 =
|
||||
case mDef m0 of
|
||||
NormalModule ds ->
|
||||
NormalModule (addImplicitNestedImports ds)
|
||||
FunctorInstance f as i -> FunctorInstance f as' i
|
||||
where
|
||||
as' = case as of
|
||||
DefaultInstAnonArg ds ->
|
||||
DefaultInstAnonArg (addImplicitNestedImports ds)
|
||||
_ -> as
|
||||
FunctorInstance f as i -> FunctorInstance f as i
|
||||
}
|
||||
|
||||
-- Step 2: compute what's defined
|
||||
@ -267,6 +262,8 @@ renameModule' mname m =
|
||||
checkFunctorArgs :: ModuleInstanceArgs Name -> RenameM ()
|
||||
checkFunctorArgs args =
|
||||
case args of
|
||||
DefaultInstAnonArg {} ->
|
||||
panic "checkFunctorArgs" ["Nested DefaultInstAnonArg"]
|
||||
DefaultInstArg l -> checkIsModule (srcRange l) (thing l)
|
||||
NamedInstArgs as -> mapM_ checkArg as
|
||||
where
|
||||
@ -676,6 +673,7 @@ instance Rename ModuleInstanceArgs where
|
||||
case args of
|
||||
DefaultInstArg a -> DefaultInstArg <$> rnLocated rename a
|
||||
NamedInstArgs xs -> NamedInstArgs <$> traverse rename xs
|
||||
DefaultInstAnonArg {} -> panic "rename" ["DefaultInstAnonArg"]
|
||||
|
||||
instance Rename ModuleInstanceArg where
|
||||
rename (ModuleInstanceArg x m) =
|
||||
|
@ -74,13 +74,8 @@ processModule ~(DModule m) =
|
||||
|
||||
FunctorInstance f as is -> ([new], [])
|
||||
where
|
||||
new = DModule m { tlValue = NestedModule m1 { mDef = newDef } }
|
||||
newDef = FunctorInstance f as' is
|
||||
as' =
|
||||
case as of
|
||||
DefaultInstAnonArg ds ->
|
||||
DefaultInstAnonArg (addImplicitNestedImports ds)
|
||||
_ -> as
|
||||
new = DModule m { tlValue = NestedModule m1 { mDef = newDef } }
|
||||
newDef = FunctorInstance f as is
|
||||
|
||||
|
||||
|
||||
|
@ -112,7 +112,6 @@ type ResolvedLocal = ResolvedModule NamingEnv
|
||||
type ResolvedExt = ResolvedModule ()
|
||||
|
||||
|
||||
-- XXX: should we report errors here, or they going to be caught later?
|
||||
resolveImports ::
|
||||
(ImpName Name -> Mod ()) ->
|
||||
TopDef ->
|
||||
@ -404,7 +403,7 @@ doImportStep s = foldl' tryImport s1 (modImports (curMod s))
|
||||
{- | Try to instantiate a functor. This succeeds if we can resolve the functor
|
||||
and the arguments and the both refer to already resolved names.
|
||||
Note: at the moment we ignore the arguments, but we'd have to do that in
|
||||
order to implment applicative behavior throuhg caching. -}
|
||||
order to implment applicative behavior with caching. -}
|
||||
tryInstanceMaybe ::
|
||||
HasCurScope a =>
|
||||
CurState' a ->
|
||||
|
@ -165,9 +165,9 @@ import Paths_cryptol
|
||||
%%
|
||||
|
||||
|
||||
vmodule :: { Module PName }
|
||||
: 'module' module_def { $2 }
|
||||
| 'v{' vmod_body 'v}' { mkAnonymousModule $2 }
|
||||
vmodule :: { [Module PName] }
|
||||
: 'module' module_def { mkTopMods $2 }
|
||||
| 'v{' vmod_body 'v}' { [mkAnonymousModule $2] }
|
||||
|
||||
|
||||
module_def :: { Module PName }
|
||||
@ -897,7 +897,7 @@ parseProgramWith cfg s = case res s of
|
||||
Layout -> programLayout
|
||||
NoLayout -> program
|
||||
|
||||
parseModule :: Config -> Text -> Either ParseError (Module PName)
|
||||
parseModule :: Config -> Text -> Either ParseError [Module PName]
|
||||
parseModule cfg = parse cfg { cfgModuleScope = True } vmodule
|
||||
|
||||
parseProgram :: Layout -> Text -> Either ParseError (Program PName)
|
||||
|
@ -253,6 +253,7 @@ data ModuleInstanceArgs name =
|
||||
|
||||
| DefaultInstAnonArg [TopDecl name]
|
||||
-- ^ Single parameter instantitaion using this anonymous module
|
||||
-- Only appears while parsing, shouldn't be in the results of the parser.
|
||||
|
||||
| NamedInstArgs [ModuleInstanceArg name]
|
||||
deriving (Show, Generic, NFData)
|
||||
|
@ -165,15 +165,10 @@ noIncludeModule :: ModuleG mname PName -> NoIncM (ModuleG mname PName)
|
||||
noIncludeModule m =
|
||||
do newDef <- case mDef m of
|
||||
NormalModule ds -> NormalModule <$> doDecls ds
|
||||
FunctorInstance f as ds ->
|
||||
FunctorInstance f <$> doArgs as <*> pure ds
|
||||
FunctorInstance f as is -> pure (FunctorInstance f as is)
|
||||
pure m { mDef = newDef }
|
||||
where
|
||||
doDecls = fmap concat . collectErrors noIncTopDecl
|
||||
doArgs as = case as of
|
||||
DefaultInstAnonArg ds ->
|
||||
DefaultInstAnonArg . concat <$> mapM noIncTopDecl ds
|
||||
_ -> pure as
|
||||
|
||||
-- | Remove includes from a program.
|
||||
noIncludeProgram :: Program PName -> NoIncM (Program PName)
|
||||
|
@ -338,15 +338,9 @@ noPatModule m =
|
||||
do def <-
|
||||
case mDef m of
|
||||
NormalModule ds -> NormalModule <$> noPatTopDs ds
|
||||
FunctorInstance f as i -> FunctorInstance f <$> noPatModArg as <*> pure i
|
||||
FunctorInstance f as i -> pure (FunctorInstance f as i)
|
||||
pure m { mDef = def }
|
||||
|
||||
noPatModArg :: ModuleInstanceArgs PName -> NoPatM (ModuleInstanceArgs PName)
|
||||
noPatModArg as =
|
||||
case as of
|
||||
DefaultInstAnonArg ds -> DefaultInstAnonArg <$> noPatTopDs ds
|
||||
_ -> pure as
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data AnnotMap = AnnotMap
|
||||
|
@ -40,7 +40,9 @@ import Cryptol.Parser.Token(SelectorType(..))
|
||||
import Cryptol.Parser.Position
|
||||
import Cryptol.Parser.Utils (translateExprToNumT,widthIdent)
|
||||
import Cryptol.Utils.Ident( packModName,packIdent,modNameChunks
|
||||
, anonymousSignatureIdent, anonymousModuleIdent)
|
||||
, anonymousSignatureIdent, anonymousModuleIdent
|
||||
, modNameArg
|
||||
)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic
|
||||
import Cryptol.Utils.RecordMap
|
||||
@ -929,6 +931,23 @@ mkSelector tok =
|
||||
_ -> panic "mkSelector" [ "Unexpected selector token", show tok ]
|
||||
|
||||
|
||||
mkTopMods :: Module PName -> [Module PName]
|
||||
mkTopMods mo =
|
||||
case mDef mo of
|
||||
FunctorInstance f as i
|
||||
| DefaultInstAnonArg ds <- as ->
|
||||
let nm = modNameArg <$> mName mo
|
||||
-- NOTE: order here is important as we want to load the argument
|
||||
-- before the the instantiation.
|
||||
in [ Module { mName = nm
|
||||
, mDef = NormalModule ds
|
||||
}
|
||||
|
||||
, mo { mDef = FunctorInstance f (DefaultInstArg (ImpTop <$> nm)) i }
|
||||
]
|
||||
|
||||
_ -> [mo]
|
||||
|
||||
mkModBody :: [TopDecl PName] -> [TopDecl PName]
|
||||
mkModBody = collect 1 [] []
|
||||
where
|
||||
|
@ -75,6 +75,12 @@ inferModule m =
|
||||
proveModuleTopLevel
|
||||
endModule
|
||||
|
||||
P.FunctorInstance f as inst ->
|
||||
do mb <- doFunctorInst (P.ImpTop <$> P.mName m) f as inst
|
||||
case mb of
|
||||
Just mo -> pure mo
|
||||
Nothing -> panic "inferModule" ["Didnt' get a module"]
|
||||
|
||||
-- | Construct a Prelude primitive in the parsed AST.
|
||||
mkPrim :: String -> InferM (P.Expr Name)
|
||||
mkPrim str =
|
||||
@ -1078,7 +1084,9 @@ checkTopDecls = mapM_ checkTopDecl
|
||||
proveModuleTopLevel
|
||||
endSubmodule
|
||||
|
||||
P.FunctorInstance f as inst -> doFunctorInst (P.mName m) f as inst
|
||||
P.FunctorInstance f as inst ->
|
||||
do _ <- doFunctorInst (P.ImpNested <$> P.mName m) f as inst
|
||||
pure ()
|
||||
|
||||
where P.NestedModule m = P.tlValue tl
|
||||
|
||||
|
@ -26,14 +26,14 @@ import Cryptol.TypeCheck.Instantiate(instantiateWith)
|
||||
import Cryptol.TypeCheck.ModuleInstance
|
||||
|
||||
doFunctorInst ::
|
||||
Located Name {- ^ Name for the new module -} ->
|
||||
Located (P.ImpName Name) {- ^ Name for the new module -} ->
|
||||
Located (P.ImpName Name) {- ^ Functor being instantiation -} ->
|
||||
P.ModuleInstanceArgs Name {- ^ Instance arguments -} ->
|
||||
Map Name Name
|
||||
{- ^ Instantitation. These is the renaming for the fuctor that arises from
|
||||
{- ^ Instantitation. These is the renaming for the functor that arises from
|
||||
generativity (i.e., it is something that will make the names "fresh").
|
||||
-} ->
|
||||
InferM ()
|
||||
InferM (Maybe Module)
|
||||
doFunctorInst m f as inst =
|
||||
inRange (srcRange m)
|
||||
do mf <- lookupFunctor (thing f)
|
||||
@ -55,7 +55,10 @@ doFunctorInst m f as inst =
|
||||
}
|
||||
newGoals CtModuleInstance (map thing (mParamConstraints m1))
|
||||
|
||||
newSubmoduleScope (thing m) (mImports m2) (mExports m2)
|
||||
case thing m of
|
||||
P.ImpTop mn -> newModuleScope mn (mImports m2) (mExports m2)
|
||||
P.ImpNested mn -> newSubmoduleScope mn (mImports m2) (mExports m2)
|
||||
|
||||
mapM_ addTySyn (Map.elems (mTySyns m2))
|
||||
mapM_ addNewtype (Map.elems (mNewtypes m2))
|
||||
mapM_ addPrimType (Map.elems (mPrimTypes m2))
|
||||
@ -63,7 +66,10 @@ doFunctorInst m f as inst =
|
||||
addSubmodules (mSubmodules m2)
|
||||
addFunctors (mFunctors m2)
|
||||
mapM_ addDecls (mDecls m2)
|
||||
endSubmodule
|
||||
|
||||
case thing m of
|
||||
P.ImpTop {} -> Just <$> endModule
|
||||
P.ImpNested {} -> endSubmodule >> pure Nothing
|
||||
|
||||
|
||||
|
||||
|
@ -31,6 +31,7 @@ module Cryptol.Utils.Ident
|
||||
, interactiveName
|
||||
, noModuleName
|
||||
, exprModName
|
||||
, modNameArg
|
||||
|
||||
, isParamInstModName
|
||||
, paramInstModName
|
||||
@ -74,6 +75,8 @@ import qualified Data.Text as T
|
||||
import Data.String (IsString(..))
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -133,16 +136,29 @@ modPathSplit p0 = (top,reverse xs)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- | Top-level Module names are just text.
|
||||
data ModName = ModName T.Text
|
||||
data ModName = ModName T.Text ModNameFlavor
|
||||
deriving (Eq,Ord,Show,Generic)
|
||||
|
||||
data ModNameFlavor = NormalModName | AnonModArgName
|
||||
deriving (Eq,Ord,Show,Generic)
|
||||
|
||||
instance NFData ModName
|
||||
instance NFData ModNameFlavor
|
||||
|
||||
modNameArg :: ModName -> ModName
|
||||
modNameArg (ModName m fl) =
|
||||
case fl of
|
||||
NormalModName -> ModName m AnonModArgName
|
||||
AnonModArgName -> panic "modNameArg" ["Name is already an argument"]
|
||||
|
||||
modNameToText :: ModName -> T.Text
|
||||
modNameToText (ModName x) = x
|
||||
modNameToText (ModName x fl) =
|
||||
case fl of
|
||||
NormalModName -> x
|
||||
AnonModArgName -> x <> "$argument"
|
||||
|
||||
textToModName :: T.Text -> ModName
|
||||
textToModName = ModName
|
||||
textToModName txt = ModName txt NormalModName
|
||||
|
||||
modNameChunks :: ModName -> [String]
|
||||
modNameChunks = unfoldr step . modNameToText . notParamInstModName
|
||||
@ -153,21 +169,22 @@ modNameChunks = unfoldr step . modNameToText . notParamInstModName
|
||||
(a,b) -> Just (T.unpack a,T.drop (T.length modSep) b)
|
||||
|
||||
isParamInstModName :: ModName -> Bool
|
||||
isParamInstModName (ModName x) = modInstPref `T.isPrefixOf` x
|
||||
isParamInstModName (ModName x _) = modInstPref `T.isPrefixOf` x
|
||||
|
||||
-- | Convert a parameterized module's name to the name of the module
|
||||
-- containing the same definitions but with explicit parameters on each
|
||||
-- definition.
|
||||
-- XXX: This will go away
|
||||
paramInstModName :: ModName -> ModName
|
||||
paramInstModName (ModName x)
|
||||
| modInstPref `T.isPrefixOf` x = ModName x
|
||||
| otherwise = ModName (T.append modInstPref x)
|
||||
paramInstModName (ModName x f)
|
||||
| modInstPref `T.isPrefixOf` x = ModName x f
|
||||
| otherwise = ModName (T.append modInstPref x) f
|
||||
|
||||
|
||||
notParamInstModName :: ModName -> ModName
|
||||
notParamInstModName (ModName x)
|
||||
| modInstPref `T.isPrefixOf` x = ModName (T.drop (T.length modInstPref) x)
|
||||
| otherwise = ModName x
|
||||
notParamInstModName (ModName x f)
|
||||
| modInstPref `T.isPrefixOf` x = ModName (T.drop (T.length modInstPref) x) f
|
||||
| otherwise = ModName x f
|
||||
|
||||
|
||||
packModName :: [T.Text] -> ModName
|
||||
|
3
tests/modsys/functors/T010.cry
Normal file
3
tests/modsys/functors/T010.cry
Normal file
@ -0,0 +1,3 @@
|
||||
module T010 = T010_F where
|
||||
type n = 8
|
||||
x = 7
|
2
tests/modsys/functors/T010.icry
Normal file
2
tests/modsys/functors/T010.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:load T010.cry
|
||||
y
|
9
tests/modsys/functors/T010.icry.stdout
Normal file
9
tests/modsys/functors/T010.icry.stdout
Normal file
@ -0,0 +1,9 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T010$argument
|
||||
Loading module T010_S
|
||||
Loading module T010_F
|
||||
Loading module T010
|
||||
[warning] at ./T010_F.cry:4:18--4:19
|
||||
Unused name: T010_F::A::n
|
||||
0x0a
|
7
tests/modsys/functors/T010_F.cry
Normal file
7
tests/modsys/functors/T010_F.cry
Normal file
@ -0,0 +1,7 @@
|
||||
module T010_F where
|
||||
|
||||
import T010_S
|
||||
import signature A
|
||||
|
||||
y = x + 3
|
||||
|
8
tests/modsys/functors/T010_S.cry
Normal file
8
tests/modsys/functors/T010_S.cry
Normal file
@ -0,0 +1,8 @@
|
||||
module T010_S where
|
||||
|
||||
signature A where
|
||||
type n : #
|
||||
x : [n]
|
||||
type constraint (fin n, n >= 8)
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user