mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Partially functional module system. Still some bugs to fix.
This commit is contained in:
parent
bdb0e12519
commit
2ec12a4c05
@ -153,6 +153,7 @@ library
|
||||
Cryptol.TypeCheck.TypeOf,
|
||||
Cryptol.TypeCheck.Sanity,
|
||||
Cryptol.TypeCheck.Module,
|
||||
Cryptol.TypeCheck.ModuleInstance,
|
||||
|
||||
Cryptol.TypeCheck.Solver.Types,
|
||||
Cryptol.TypeCheck.Solver.SMT,
|
||||
|
@ -37,6 +37,9 @@ instance TraverseNames a => TraverseNames (Located a) where
|
||||
instance TraverseNames Name where
|
||||
traverseNamesIP = ?name
|
||||
|
||||
instance (Ord a, TraverseNames a) => TraverseNames (ExportSpec a) where
|
||||
traverseNamesIP (ExportSpec mp) = ExportSpec <$> traverse traverseNamesIP mp
|
||||
|
||||
instance TraverseNames Expr where
|
||||
traverseNamesIP expr =
|
||||
case expr of
|
||||
@ -161,18 +164,18 @@ instance TraverseNames Type where
|
||||
TRec rm -> TRec <$> traverseRecordMap (\_ -> traverseNamesIP) rm
|
||||
TNewtype nt ts -> TNewtype <$> traverseNamesIP nt <*> traverseNamesIP ts
|
||||
|
||||
-- XXX: It might be better to arrange to not have names here?
|
||||
|
||||
instance TraverseNames TCon where
|
||||
traverseNamesIP tcon =
|
||||
case tcon of
|
||||
TC tc -> TC <$> traverseNamesIP tc
|
||||
_ -> pure tcon
|
||||
_ -> pure tcon
|
||||
|
||||
instance TraverseNames TC where
|
||||
traverseNamesIP tc =
|
||||
case tc of
|
||||
TCAbstract ut -> TCAbstract <$> traverseNamesIP ut
|
||||
_ -> pure tc
|
||||
_ -> pure tc
|
||||
|
||||
instance TraverseNames UserTC where
|
||||
traverseNamesIP (UserTC x k) = UserTC <$> traverseNamesIP x <*> pure k
|
||||
|
@ -46,7 +46,6 @@ module Cryptol.ModuleSystem.Name (
|
||||
, mkLocal
|
||||
, mkModParam
|
||||
, toParamInstName
|
||||
, asParamName
|
||||
, paramModRecParam
|
||||
|
||||
-- ** Unique Supply
|
||||
@ -241,9 +240,6 @@ toParamInstName n =
|
||||
}
|
||||
_ -> n
|
||||
|
||||
asParamName :: Name -> Name
|
||||
asParamName n = n { nInfo = LocalName (nameNamespace n) (nameIdent n) }
|
||||
|
||||
|
||||
asOrigName :: Name -> Maybe OrigName
|
||||
asOrigName n =
|
||||
|
@ -13,7 +13,7 @@ import Data.Ord(comparing)
|
||||
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.Parser.Position(thing)
|
||||
import Cryptol.ModuleSystem.Name(toParamInstName,asParamName,nameIdent
|
||||
import Cryptol.ModuleSystem.Name(toParamInstName,nameIdent
|
||||
,paramModRecParam)
|
||||
import Cryptol.Utils.Ident(paramInstModName)
|
||||
import Cryptol.Utils.RecordMap(recordFromFields)
|
||||
|
@ -76,8 +76,7 @@ data ModuleG mname =
|
||||
-- ^ Submodules, functors, and signature nested directly
|
||||
-- in this module
|
||||
|
||||
-- These have everything from this module and
|
||||
-- all submodules
|
||||
-- These have everything from this module and all submodules
|
||||
, mTySyns :: Map Name TySyn
|
||||
, mNewtypes :: Map Name Newtype
|
||||
, mPrimTypes :: Map Name AbstractType
|
||||
|
@ -1,5 +1,4 @@
|
||||
{-# Language BlockArguments #-}
|
||||
{-# Language Trustworthy #-}
|
||||
{-# Language BlockArguments, ImplicitParams #-}
|
||||
module Cryptol.TypeCheck.Module (doFunctorInst) where
|
||||
|
||||
import Data.Map(Map)
|
||||
@ -8,8 +7,7 @@ import qualified Data.Set as Set
|
||||
import Control.Monad(unless,forM_)
|
||||
|
||||
|
||||
import Cryptol.Utils.Panic(xxxTODO)
|
||||
import Cryptol.Utils.Ident(Ident,Namespace(..))
|
||||
import Cryptol.Utils.Ident(Ident,Namespace(..),isInfixIdent)
|
||||
import Cryptol.Parser.Position (Range,Located(..), thing)
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.ModuleSystem.Name(nameIdent)
|
||||
@ -20,23 +18,50 @@ import Cryptol.ModuleSystem.Interface
|
||||
)
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Error
|
||||
import Cryptol.TypeCheck.Subst(Subst,abstractSubst,listParamSubst,apSubst)
|
||||
import Cryptol.TypeCheck.Subst( Subst,abstractSubst,apSubst
|
||||
, mergeDistinctSubst)
|
||||
import Cryptol.TypeCheck.Solve(proveImplication)
|
||||
import Cryptol.TypeCheck.Monad
|
||||
import Cryptol.TypeCheck.Instantiate(instantiateWith)
|
||||
import Cryptol.TypeCheck.ModuleInstance
|
||||
|
||||
doFunctorInst ::
|
||||
Located Name {- ^ Name for the new module -} ->
|
||||
Located (P.ImpName Name) {- ^ Functor being instantiation -} ->
|
||||
P.ModuleInstanceArgs Name {- ^ Instance arguments -} ->
|
||||
Map Name Name {- ^ Basic instantiation -} ->
|
||||
Map Name Name
|
||||
{- ^ Instantitation. These is the renaming for the fuctor that arises from
|
||||
generativity (i.e., it is something that will make the names "fresh").
|
||||
-} ->
|
||||
InferM ()
|
||||
doFunctorInst m f as inst =
|
||||
do mf <- lookupFunctor (thing f)
|
||||
argIs <- checkArity (srcRange f) mf as
|
||||
(tySus,valRens) <- unzip <$> mapM checkArg argIs
|
||||
(tySus,decls) <- unzip <$> mapM checkArg argIs
|
||||
let ?tSu = mergeDistinctSubst tySus
|
||||
?vSu = inst
|
||||
let m1 = moduleInstance mf
|
||||
m2 = m1 { mName = m
|
||||
, 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
|
||||
}
|
||||
|
||||
newSubmoduleScope (thing m) (mImports m2) (mExports m2)
|
||||
mapM_ addTySyn (Map.elems (mTySyns m2))
|
||||
mapM_ addNewtype (Map.elems (mNewtypes m2))
|
||||
mapM_ addPrimType (Map.elems (mPrimTypes m2))
|
||||
addSignatures (mSignatures m2)
|
||||
addSubmodules (mSubmodules m2)
|
||||
addFunctors (mFunctors m2)
|
||||
mapM_ addDecls (mDecls m2)
|
||||
endSubmodule
|
||||
|
||||
|
||||
pure ()
|
||||
|
||||
|
||||
-- | Validate a functor application, just checking the argument names
|
||||
@ -80,7 +105,7 @@ checkArity r mf args =
|
||||
checkArgs done ps more
|
||||
|
||||
|
||||
checkArg :: (Range, IfaceModParam, IfaceG ()) -> InferM (Subst, Map Name Expr)
|
||||
checkArg :: (Range, IfaceModParam, IfaceG ()) -> InferM (Subst, [Decl])
|
||||
checkArg (r,expect,actual) =
|
||||
do tRens <- mapM (checkParamType r tyMap) (Map.toList (ifParamTypes params))
|
||||
let renSu = abstractSubst (concat tRens)
|
||||
@ -95,12 +120,12 @@ checkArg (r,expect,actual) =
|
||||
let fromD d = (ifDeclName d, ifDeclSig d)
|
||||
vMap = nameMapToIdentMap fromD (ifDecls decls)
|
||||
|
||||
vRen <- Map.fromList . concat <$>
|
||||
vDecls <- concat <$>
|
||||
mapM (checkParamValue r vMap)
|
||||
[ (i, s { mvpType = apSubst renSu (mvpType s) })
|
||||
| (i,s) <- Map.toList (ifParamFuns params) ]
|
||||
[ s { mvpType = apSubst renSu (mvpType s) }
|
||||
| s <- Map.elems (ifParamFuns params) ]
|
||||
|
||||
pure (renSu, vRen)
|
||||
pure (renSu, vDecls)
|
||||
|
||||
|
||||
|
||||
@ -155,10 +180,11 @@ checkParamType r tyMap (name,mp) =
|
||||
checkParamValue ::
|
||||
Range {- ^ Location for error reporting -} ->
|
||||
Map Ident (Name,Schema) {- ^ Actual values -} ->
|
||||
(Name, ModVParam) {- ^ The parameter we are checking -} ->
|
||||
InferM [(Name,Expr)] {- ^ Mapping from parameter name to actual names -}
|
||||
checkParamValue r vMap (name,mp) =
|
||||
let i = nameIdent name
|
||||
ModVParam {- ^ The parameter we are checking -} ->
|
||||
InferM [Decl] {- ^ Mapping from parameter name to definition -}
|
||||
checkParamValue r vMap mp =
|
||||
let name = mvpName mp
|
||||
i = nameIdent name
|
||||
expectT = mvpType mp
|
||||
in case Map.lookup i vMap of
|
||||
Nothing ->
|
||||
@ -166,13 +192,16 @@ checkParamValue r vMap (name,mp) =
|
||||
pure []
|
||||
Just actual ->
|
||||
do e <- mkParamDef r (name,expectT) actual
|
||||
pure [(name,e)]
|
||||
{-
|
||||
do unless (sameSchema expectT actualT) $
|
||||
(recordErrorLoc (Just r) (SchemaMismatch i expectT actualT))
|
||||
pure [(name,EVar actualName)]
|
||||
-}
|
||||
let d = Decl { dName = name
|
||||
, dSignature = expectT
|
||||
, dDefinition = DExpr e
|
||||
, dPragmas = []
|
||||
, dInfix = isInfixIdent (nameIdent name)
|
||||
, dFixity = mvpFixity mp
|
||||
, dDoc = mvpDoc mp
|
||||
}
|
||||
|
||||
pure [d]
|
||||
|
||||
{- | Make an "adaptor" that instantiates the paramter into the form expected
|
||||
by the functor. If the actual type is:
|
||||
|
160
src/Cryptol/TypeCheck/ModuleInstance.hs
Normal file
160
src/Cryptol/TypeCheck/ModuleInstance.hs
Normal file
@ -0,0 +1,160 @@
|
||||
{-# Language ImplicitParams, ConstraintKinds #-}
|
||||
module Cryptol.TypeCheck.ModuleInstance where
|
||||
|
||||
import Data.Map(Map)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Set(Set)
|
||||
import qualified Data.Set as Set
|
||||
|
||||
import Cryptol.Parser.Position(Located)
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
(IfaceParams(..), IfaceNames(..), IfaceModParam(..))
|
||||
import Cryptol.IR.TraverseNames(TraverseNames,mapNames)
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Subst(Subst,TVars,apSubst)
|
||||
|
||||
|
||||
{- | `?tSu` should be applied to all types.
|
||||
`?vSu` shoudl be applied to all values. -}
|
||||
type Su = (?tSu :: Subst, ?vSu :: Map Name Name)
|
||||
|
||||
-- | Has value names but no types.
|
||||
doVInst :: (Su, TraverseNames a) => a -> a
|
||||
doVInst = mapNames (\x -> Map.findWithDefault x x ?vSu)
|
||||
|
||||
-- | Has types but not values.
|
||||
doTInst :: (Su, TVars a) => a -> a
|
||||
doTInst = apSubst ?tSu
|
||||
|
||||
-- | Has both value names and types.
|
||||
doTVInst :: (Su, TVars a, TraverseNames a) => a -> a
|
||||
doTVInst = apSubst ?tSu . doVInst
|
||||
|
||||
doMap :: (Su, ModuleInstance a) => Map Name a -> Map Name a
|
||||
doMap mp =
|
||||
Map.fromList [ (moduleInstance x, moduleInstance d) | (x,d) <- Map.toList mp ]
|
||||
|
||||
doSet :: Su => Set Name -> Set Name
|
||||
doSet = Set.fromList . map moduleInstance . Set.toList
|
||||
|
||||
|
||||
|
||||
|
||||
class ModuleInstance t where
|
||||
moduleInstance :: Su => t -> t
|
||||
|
||||
instance ModuleInstance a => ModuleInstance [a] where
|
||||
moduleInstance = map moduleInstance
|
||||
|
||||
instance ModuleInstance a => ModuleInstance (Located a) where
|
||||
moduleInstance l = moduleInstance <$> l
|
||||
|
||||
instance ModuleInstance Name where
|
||||
moduleInstance = doVInst
|
||||
|
||||
instance ModuleInstance (ModuleG name) where
|
||||
moduleInstance m =
|
||||
Module { mName = mName m
|
||||
, mExports = doVInst (mExports m)
|
||||
, mImports = mImports m
|
||||
, mParamTypes = doMap (mParamTypes m)
|
||||
, mParamFuns = doMap (mParamFuns m)
|
||||
, mParamConstraints = moduleInstance (mParamConstraints m)
|
||||
, mParams = moduleInstance <$> mParams m
|
||||
, mFunctors = doMap (mFunctors m)
|
||||
, mNested = doSet (mNested m)
|
||||
, mTySyns = doMap (mTySyns m)
|
||||
, mNewtypes = doMap (mNewtypes m)
|
||||
, mPrimTypes = doMap (mPrimTypes m)
|
||||
, mDecls = moduleInstance (mDecls m)
|
||||
, mSubmodules = doMap (mSubmodules m)
|
||||
, mSignatures = doMap (mSignatures m)
|
||||
}
|
||||
|
||||
instance ModuleInstance Type where
|
||||
moduleInstance = doTInst
|
||||
|
||||
instance ModuleInstance Schema where
|
||||
moduleInstance = doTInst
|
||||
|
||||
instance ModuleInstance TySyn where
|
||||
moduleInstance ts =
|
||||
TySyn { tsName = moduleInstance (tsName ts)
|
||||
, tsParams = tsParams ts
|
||||
, tsConstraints = moduleInstance (tsConstraints ts)
|
||||
, tsDef = moduleInstance (tsDef ts)
|
||||
, tsDoc = tsDoc ts
|
||||
}
|
||||
|
||||
instance ModuleInstance Newtype where
|
||||
moduleInstance nt =
|
||||
Newtype { ntName = moduleInstance (ntName nt)
|
||||
, ntParams = ntParams nt
|
||||
, ntConstraints = moduleInstance (ntConstraints nt)
|
||||
, ntFields = moduleInstance <$> ntFields nt
|
||||
, ntDoc = ntDoc nt
|
||||
}
|
||||
|
||||
instance ModuleInstance AbstractType where
|
||||
moduleInstance at =
|
||||
AbstractType { atName = moduleInstance (atName at)
|
||||
, atKind = atKind at
|
||||
, atCtrs = let (ps,cs) = atCtrs at
|
||||
in (ps, moduleInstance cs)
|
||||
, atFixitiy = atFixitiy at
|
||||
, atDoc = atDoc at
|
||||
}
|
||||
|
||||
instance ModuleInstance DeclGroup where
|
||||
moduleInstance dg =
|
||||
case dg of
|
||||
Recursive ds -> Recursive (moduleInstance ds)
|
||||
NonRecursive d -> NonRecursive (moduleInstance d)
|
||||
|
||||
instance ModuleInstance Decl where
|
||||
moduleInstance = doTVInst
|
||||
|
||||
|
||||
instance ModuleInstance name => ModuleInstance (IfaceNames name) where
|
||||
moduleInstance ns =
|
||||
IfaceNames { ifsName = moduleInstance (ifsName ns)
|
||||
, ifsNested = doSet (ifsNested ns)
|
||||
, ifsDefines = doSet (ifsDefines ns)
|
||||
, ifsPublic = doSet (ifsPublic ns)
|
||||
}
|
||||
|
||||
instance ModuleInstance IfaceParams where
|
||||
moduleInstance si =
|
||||
IfaceParams { ifParamTypes = doMap (ifParamTypes si)
|
||||
, ifParamConstraints = moduleInstance (ifParamConstraints si)
|
||||
, ifParamFuns = doMap (ifParamFuns si)
|
||||
, ifParamDoc = ifParamDoc si
|
||||
}
|
||||
|
||||
instance ModuleInstance ModTParam where
|
||||
moduleInstance mp =
|
||||
ModTParam { mtpName = moduleInstance (mtpName mp)
|
||||
, mtpKind = mtpKind mp
|
||||
, mtpDoc = mtpDoc mp
|
||||
, mtpNumber = mtpNumber mp
|
||||
}
|
||||
|
||||
instance ModuleInstance ModVParam where
|
||||
moduleInstance mp =
|
||||
ModVParam { mvpName = moduleInstance (mvpName mp)
|
||||
, mvpType = moduleInstance (mvpType mp)
|
||||
, mvpDoc = mvpDoc mp
|
||||
, mvpFixity = mvpFixity mp
|
||||
}
|
||||
|
||||
instance ModuleInstance IfaceModParam where
|
||||
moduleInstance p =
|
||||
IfaceModParam { ifmpName = ifmpName p
|
||||
, ifmpSignature = moduleInstance (ifmpSignature p)
|
||||
, ifmpParameters = moduleInstance (ifmpParameters p)
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
@ -1036,6 +1036,21 @@ addParamType :: ModTParam -> InferM ()
|
||||
addParamType a =
|
||||
updScope \r -> r { mParamTypes = Map.insert (mtpName a) a (mParamTypes r) }
|
||||
|
||||
addSignatures :: Map Name If.IfaceParams -> InferM ()
|
||||
addSignatures mp =
|
||||
updScope \r -> r { mSignatures = Map.union mp (mSignatures r) }
|
||||
|
||||
addSubmodules :: Map Name (If.IfaceNames Name) -> InferM ()
|
||||
addSubmodules mp =
|
||||
updScope \r -> r { mSubmodules = Map.union mp (mSubmodules r) }
|
||||
|
||||
addFunctors :: Map Name (ModuleG Name) -> InferM ()
|
||||
addFunctors mp =
|
||||
updScope \r -> r { mFunctors = Map.union mp (mFunctors r) }
|
||||
|
||||
|
||||
|
||||
|
||||
-- | The sub-computation is performed with the given abstract function in scope.
|
||||
addParamFun :: ModVParam -> InferM ()
|
||||
addParamFun x =
|
||||
|
@ -37,6 +37,7 @@ module Cryptol.TypeCheck.Subst
|
||||
, applySubstToVar
|
||||
, substToList
|
||||
, fmap', (!$), (.$)
|
||||
, mergeDistinctSubst
|
||||
) where
|
||||
|
||||
import Data.Maybe
|
||||
@ -96,6 +97,30 @@ emptySubst =
|
||||
, suDefaulting = False
|
||||
}
|
||||
|
||||
mergeDistinctSubst :: [Subst] -> Subst
|
||||
mergeDistinctSubst sus =
|
||||
case sus of
|
||||
[] -> emptySubst
|
||||
_ -> foldr1 merge sus
|
||||
|
||||
where
|
||||
merge s1 s2 = S { suFreeMap = jn suFreeMap s1 s2
|
||||
, suBoundMap = jn suBoundMap s1 s2
|
||||
, suAbstractMap = jn suAbstractMap s1 s2
|
||||
, suDefaulting = if suDefaulting s1 || suDefaulting s2
|
||||
then err
|
||||
else False
|
||||
}
|
||||
|
||||
err = panic "mergeDistinctSubst" [ "Not distinct" ]
|
||||
bad _ _ = err
|
||||
jn f x y = IntMap.unionWith bad (f x) (f y)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
-- | Reasons to reject a single-variable substitution.
|
||||
data SubstError
|
||||
= SubstRecursive
|
||||
@ -442,6 +467,7 @@ instance TVars DeclDef where
|
||||
apSubst su (DExpr e) = DExpr !$ (apSubst su e)
|
||||
apSubst _ DPrim = DPrim
|
||||
|
||||
-- WARNING: This applies the substitution only to the declarations.
|
||||
instance TVars Module where
|
||||
apSubst su m =
|
||||
let !decls' = apSubst su (mDecls m)
|
||||
|
Loading…
Reference in New Issue
Block a user