Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Functors iface tysyn #1459

Closed
wants to merge 70 commits into from
Closed
Changes from 1 commit
Commits
Show all changes
70 commits
Select commit Hold shift + click to select a range
6ab1470
New module system
yav Jun 13, 2022
1e3ad37
Don't crash on undefined names.
yav Jun 14, 2022
3839b3a
Add an example of passing a submodule as an argument to a functor.
yav Jun 14, 2022
ed90c0a
Remove unused things
yav Jun 14, 2022
67b5bde
Make the remote API compile
yav Jun 14, 2022
a643a19
only use top-level imports in implicit interface, get more tests working
m-yac Jun 15, 2022
70d9600
fix error for parameterized module instantiations, add tests like T5
m-yac Jun 21, 2022
4b3eac5
Fix fixities not registering when defined in REPL
qsctr Jun 24, 2022
2c179b1
fix #1372 by excluding defns from functor instances in `warnUnused`
m-yac Jul 14, 2022
2a8f755
fix remaining tests
m-yac Jul 14, 2022
1419108
Implement functor imports with instantiation.
yav Jul 14, 2022
26121c9
Update docs to document `where` imports
yav Jul 14, 2022
488ceec
Fix spacing in a test
yav Jul 14, 2022
18e1b92
Implement insantiating imports with { }
yav Jul 14, 2022
b76ec46
Update documentation
yav Jul 14, 2022
f9cd75b
accept whitespace changes in mono-binds tests
m-yac Jul 14, 2022
510d185
update AES examples with import instantiation syntax
m-yac Jul 14, 2022
83f4575
Rename `ModuleInstanceArg` to `ModuleInstanceNamedArg`
yav Jul 15, 2022
5ece8bb
Correct the order of declaratoins in functors.
yav Jul 15, 2022
a2bc669
First stab at passing through functor parameters
yav Jul 15, 2022
694282e
Add more tests for passing on parameters
yav Jul 18, 2022
ff30033
Document passing through arguments
yav Jul 18, 2022
62dddb0
Change 'signature' to interface, and also list funcotors
yav Jul 25, 2022
5bf24a2
Use more descriptive names for internally generated names.
yav Jul 25, 2022
84694d7
Don't show unusable anonymous modules when browsing.
yav Jul 25, 2022
24b1ba6
Clean up browsing of signatures
yav Jul 25, 2022
9c9d0db
Don't discrad documentation during type checking
yav Jul 25, 2022
180c90f
Use simple language
yav Jul 25, 2022
d413e35
Detailed help for interfaces.
yav Jul 25, 2022
5c1b0bc
Fix tests
yav Jul 25, 2022
d5d9f42
Print documentation for module parameters when inside a functor
yav Jul 26, 2022
ccb563c
Show fixities for value parameters.
yav Jul 26, 2022
6e8ab5a
Show documentation for modules, functors, and interfaces
yav Jul 26, 2022
25f92f5
Update test with new naming convention
yav Jul 26, 2022
a370845
Fix more tests
yav Jul 26, 2022
3eae908
Fix special cases for windows
yav Jul 26, 2022
5b801fc
Merge branch 'master' into functors-merge
yav Aug 4, 2022
dfdbd12
Merge branch 'master' into functors-merge
yav Aug 4, 2022
f77e5cc
Merge remote-tracking branch 'origin/master' into functors-merge
yav Aug 12, 2022
bd55b96
Fix typo
yav Aug 12, 2022
516ad74
Remove unused functoion
yav Sep 22, 2022
ddcc67b
Resolve Has selectors for each nested module separately.
yav Sep 22, 2022
09b68e2
Fix typos in comments
yav Sep 24, 2022
b72a5d9
Don't try to get information for undefined names.
yav Sep 24, 2022
441e163
Merge branch 'master' into functors-merge
yav Sep 27, 2022
489ded4
Fix tests
yav Sep 27, 2022
6fea305
Fix test
yav Sep 27, 2022
bed32f8
`TraverseNames` for `EPropGuards`
yav Sep 28, 2022
4f8bc65
Disallow foreign with the same name and in functors
yav Sep 28, 2022
58a351c
Update evaluator to account for TError of kind prop.
yav Sep 28, 2022
29e71d1
Merge branch 'master' into functors-merge
yav Sep 28, 2022
12967c4
Fix tests for Mac and Windows
yav Sep 28, 2022
39c6026
Handle some more cases where fake names caused problems.
yav Sep 29, 2022
e1e3fe6
Squash yet another fake name issue
yav Sep 29, 2022
3dc316a
Remove unused function
yav Oct 11, 2022
043bd69
Add a function to support translation to SAW core
yav Oct 11, 2022
91dbed4
Add a function that can split up a module name in Text, rather than s…
yav Oct 11, 2022
efc3fe7
Include one Ubuntu 20.04 configuration (#1447)
RyanGlScott Oct 6, 2022
fa3cc20
Pretty printing for Core Lint errors
yav Oct 13, 2022
0cefb92
Don't use syntactic equality for numeric types, collect constraints i…
yav Oct 13, 2022
f35648c
Filter out really trivial goals, so we can see the actual interesting…
yav Oct 13, 2022
ab0d1c8
Merge remote-tracking branch 'origin/T1451' into functors-merge
yav Oct 13, 2022
b0ccbb7
Preserve number of predicates in schema when applying a substitution
yav Oct 14, 2022
b66d990
Rename "signature" to "interface" to follow standard naming
yav Oct 14, 2022
8de5a79
Add pretty printing instances for parameters.
yav Oct 14, 2022
8922877
Allow loading interfaces.
yav Oct 14, 2022
9701b37
Check that when evaluating things we do not use either value or type …
yav Oct 20, 2022
20f8a36
Add/improve haddocks
yav Oct 21, 2022
c5e8662
Rename Signature to Iface + comments
yav Oct 21, 2022
dc4b344
Have a go at allowing type synonyms in interfaces.
yav Oct 25, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Have a go at allowing type synonyms in interfaces.
Not at all tested.
  • Loading branch information
yav committed Oct 25, 2022

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
commit dc4b34411c1fa3a3f12845bb6b3a7c5af9636b76
13 changes: 13 additions & 0 deletions src/Cryptol/IR/TraverseNames.hs
Original file line number Diff line number Diff line change
@@ -249,4 +249,17 @@ instance TraverseNames FFIType where
FFITuple ts -> FFITuple <$> traverseNamesIP ts
FFIRecord mp -> FFIRecord <$> traverseRecordMap
(\_ -> traverseNamesIP) mp
instance TraverseNames TySyn where
traverseNamesIP ts = mk <$> traverseNamesIP (tsName ts)
<*> traverseNamesIP (tsParams ts)
<*> traverseNamesIP (tsConstraints ts)
<*> traverseNamesIP (tsDef ts)
where mk n ps cs t =
TySyn { tsName = n
, tsParams = ps
, tsConstraints = cs
, tsDef = t
, tsDoc = tsDoc ts
}


11 changes: 10 additions & 1 deletion src/Cryptol/ModuleSystem/Binds.hs
Original file line number Diff line number Diff line change
@@ -165,7 +165,7 @@ sigToMod mp sig =
, modInstances = mempty
, modMods = mempty
, modDefines = env
, modPublic = mempty -- unused
, modPublic = namingEnvNames env
, modState = ()
}

@@ -240,6 +240,7 @@ signatureDefs :: ModPath -> Signature PName -> BuildNamingEnv
signatureDefs m sig =
mconcat [ namingEnv (InModule loc p) | p <- sigTypeParams sig ]
<> mconcat [ namingEnv (InModule loc p) | p <- sigFunParams sig ]
<> mconcat [ namingEnv (InModule loc p) | p <- sigConstraints sig ]
where
loc = Just m
--------------------------------------------------------------------------------
@@ -395,6 +396,14 @@ instance BindsNames (InModule (Decl PName)) where
do n <- mkName NSType ln f
return (singletonNS NSType (thing ln) n)

instance BindsNames (InModule (SigDecl PName)) where
namingEnv (InModule m d) =
case d of
SigConstraint {} -> mempty
SigTySyn ts _ -> namingEnv (InModule m (DType ts))
SigPropSyn ps _ -> namingEnv (InModule m (DProp ps))




--------------------------------------------------------------------------------
5 changes: 4 additions & 1 deletion src/Cryptol/ModuleSystem/NamingEnv.hs
Original file line number Diff line number Diff line change
@@ -236,7 +236,8 @@ modParamsNamingEnv :: T.ModParamNames -> NamingEnv
modParamsNamingEnv T.ModParamNames { .. } =
NamingEnv $ Map.fromList
[ (NSValue, Map.fromList $ map fromFu $ Map.keys mpnFuns)
, (NSType, Map.fromList $ map fromTy $ Map.elems mpnTypes)
, (NSType, Map.fromList $ map fromTS (Map.elems mpnTySyn) ++
map fromTy (Map.elems mpnTypes))
]
where
toPName n = mkUnqual (nameIdent n)
@@ -246,6 +247,8 @@ modParamsNamingEnv T.ModParamNames { .. } =

fromFu f = (toPName f, One f)

fromTS ts = (toPName (T.tsName ts), One (T.tsName ts))


-- | Generate a naming environment from a declaration interface, where none of
-- the names are qualified.
12 changes: 11 additions & 1 deletion src/Cryptol/ModuleSystem/Renamer.hs
Original file line number Diff line number Diff line change
@@ -608,6 +608,9 @@ doModParam mp =
(checkIsModule (srcRange sigName) sigName' ASignature)
sigEnv <- if isFake then pure mempty else lookupDefines sigName'


-- XXX: It seems a bit odd to use "newModParam" for the names to be used
-- for the instaciated type synonyms, but what other name could we use?
let newP x = do y <- lift (newModParam me (mpName mp) loc x)
sets_ (Map.insert y x)
pure y
@@ -716,7 +719,7 @@ renameIfaceModule nm sig =
-- that declare only types, and so appear "unused".
forM_ tps \tp -> recordUse (thing (ptName tp))

cts <- traverse (traverse rename) (sigConstraints sig)
cts <- traverse rename (sigConstraints sig)
fun <- traverse rename (sigFunParams sig)
pure Signature
{ sigImports = imps
@@ -789,6 +792,13 @@ instance Rename ParameterFun where
do sig' <- renameSchema (pfSchema a)
return a { pfName = n', pfSchema = snd sig' }

instance Rename SigDecl where
rename decl =
case decl of
SigConstraint ps -> SigConstraint <$> traverse (rnLocated rename) ps
SigTySyn ts mb -> SigTySyn <$> rename ts <*> pure mb
SigPropSyn ps mb -> SigPropSyn <$> rename ps <*> pure mb

instance Rename Decl where
rename d = case d of
DBind b -> DBind <$> rename b
26 changes: 19 additions & 7 deletions src/Cryptol/Parser.y
Original file line number Diff line number Diff line change
@@ -342,8 +342,15 @@ par_decls :: { [ParamDecl PName] }
par_decl :: { ParamDecl PName }
: mbDoc name ':' schema { mkParFun $1 $2 $4 }
| mbDoc 'type' name ':' kind {% mkParType $1 $3 $5 }
| mbDoc 'type' 'constraint' type {% fmap (DParameterConstraint . distrLoc)
(mkProp $4) }
| mbDoc 'type' 'constraint' '(' type ')'
{% fmap (DParameterConstraint .
SigConstraint . distrLoc) (mkProp $5)}
| mbDoc 'type' 'constraint' '(' tuple_types ')'
{% fmap (DParameterConstraint .
SigConstraint . distrLoc)
(mkProp (at ($4,$6) (TTuple $5))) }

| mbDoc typeOrPropSyn { mkIfacePropSyn (thing `fmap` $1) $2 }


doc :: { Located Text }
@@ -421,7 +428,16 @@ let_decl :: { Decl PName }

| 'let' vars_comma ':' schema { at (head $2,$4) $ DSignature (reverse $2) $4 }

| 'type' name '=' type {% at ($1,$4) `fmap` mkTySyn $2 [] $4 }
| typeOrPropSyn { $1 }

| 'infixl' NUM ops {% mkFixity LeftAssoc $2 (reverse $3) }
| 'infixr' NUM ops {% mkFixity RightAssoc $2 (reverse $3) }
| 'infix' NUM ops {% mkFixity NonAssoc $2 (reverse $3) }



typeOrPropSyn :: { Decl PName }
: 'type' name '=' type {% at ($1,$4) `fmap` mkTySyn $2 [] $4 }
| 'type' name tysyn_params '=' type
{% at ($1,$5) `fmap` mkTySyn $2 (reverse $3) $5 }
| 'type' tysyn_param op tysyn_param '=' type
@@ -434,10 +450,6 @@ let_decl :: { Decl PName }
| 'type' 'constraint' tysyn_param op tysyn_param '=' type
{% at ($2,$7) `fmap` mkPropSyn $4 [$3, $5] $7 }

| 'infixl' NUM ops {% mkFixity LeftAssoc $2 (reverse $3) }
| 'infixr' NUM ops {% mkFixity RightAssoc $2 (reverse $3) }
| 'infix' NUM ops {% mkFixity NonAssoc $2 (reverse $3) }




58 changes: 46 additions & 12 deletions src/Cryptol/Parser/AST.hs
Original file line number Diff line number Diff line change
@@ -74,6 +74,7 @@ module Cryptol.Parser.AST
, ParameterFun(..)
, NestedModule(..)
, Signature(..)
, SigDecl(..)
, ModParam(..)
, ParamDecl(..)
, PropGuardCase(..)
@@ -262,7 +263,7 @@ data ParamDecl name =
| DParameterFun (ParameterFun name) -- ^ @parameter someVal : [256]@
-- (parser only)

| DParameterConstraint [Located (Prop name)]
| DParameterConstraint (SigDecl name)
-- ^ @parameter type constraint (fin T)@
deriving (Show, Generic, NFData)

@@ -354,7 +355,7 @@ data ParameterFun name = ParameterFun
{- | Interface Modules (aka types of functor arguments)

IMPORTANT: Interface Modules are a language construct and are different from
the notion of "interface" in the Cyrptol implementation.
the notion of "interface" in the Cryptol implementation.

Note that the names *defined* in an interface module are only really used in the
other members of the interface module. When an interface module is "imported"
@@ -364,10 +365,20 @@ data Signature name = Signature
{ sigImports :: ![Located (ImportG (ImpName name))]
-- ^ Add things in scope
, sigTypeParams :: [ParameterType name] -- ^ Type parameters
, sigConstraints :: [Located (Prop name)] -- ^ Constraints on type params
, sigConstraints :: [SigDecl name]
-- ^ Constraints on the type parameters and type synonyms.
-- These are in order, because we should check them in the order they are written.

, sigFunParams :: [ParameterFun name] -- ^ Value parameters
} deriving (Show,Generic,NFData)

-- | A constraint or type synonym declared in an interface.
data SigDecl name =
SigConstraint [Located (Prop name)]
| SigTySyn (TySyn name) (Maybe Text)
| SigPropSyn (PropSyn name) (Maybe Text)
deriving (Show,Generic,NFData)

{- | A module parameter declaration.

> import interface A
@@ -744,6 +755,13 @@ instance HasLoc (ParamDecl name) where
DParameterFun d -> getLoc d
DParameterConstraint d -> getLoc d

instance HasLoc (SigDecl name) where
getLoc decl =
case decl of
SigConstraint ps -> getLoc ps
SigTySyn ts _ -> getLoc ts
SigPropSyn ps _ -> getLoc ps

instance HasLoc (ModParam name) where
getLoc mp = getLoc (mpSignature mp)

@@ -776,6 +794,13 @@ instance HasLoc (Newtype name) where
where
locs = catMaybes ([ getLoc (nName n)] ++ map (Just . fst . snd) (displayFields (nBody n)))

instance HasLoc (TySyn name) where
getLoc (TySyn x _ _ _) = getLoc x

instance HasLoc (PropSyn name) where
getLoc (PropSyn x _ _ _) = getLoc x



--------------------------------------------------------------------------------

@@ -874,23 +899,25 @@ instance (Show name, PPName name) => PP (ParamDecl name) where
case pd of
DParameterFun d -> pp d
DParameterType d -> pp d
DParameterConstraint d -> "type" <+> "constraint" <+> prop
where prop = case map (pp . thing) d of
[x] -> x
[] -> "()"
xs -> nest 1 (parens (commaSepFill xs))
DParameterConstraint d -> pp d

ppInterface :: (Show name, PPName name) => Doc -> Signature name -> Doc
ppInterface kw sig = kw $$ indent 2 (vcat (is ++ ds))
where
is = map pp (sigImports sig)
ds = map pp (sigTypeParams sig)
++ case map (pp . thing) (sigConstraints sig) of
[x] -> ["type constraint" <+> x]
[] -> []
xs -> ["type constraint" <+> parens (commaSep xs)]
++ map pp (sigConstraints sig)
++ map pp (sigFunParams sig)

instance (Show name, PPName name) => PP (SigDecl name) where
ppPrec p decl =
case decl of
SigConstraint ps ->
"type constraint" <+> parens (commaSep (map (pp . thing) ps))

SigTySyn ts _ -> ppPrec p ts
SigPropSyn ps _ -> ppPrec p ps


instance (Show name, PPName name) => PP (ModParam name) where
ppPrec _ mp = vcat ( mbDoc
@@ -1361,6 +1388,13 @@ instance NoPos (Signature name) where
, sigFunParams = map noPos (sigFunParams sig)
}

instance NoPos (SigDecl name) where
noPos decl =
case decl of
SigConstraint ps -> SigConstraint (map noPos ps)
SigTySyn ts mb -> SigTySyn (noPos ts) mb
SigPropSyn ps mb -> SigPropSyn (noPos ps) mb

instance NoPos (ModParam name) where
noPos mp = ModParam { mpSignature = noPos (mpSignature mp)
, mpAs = mpAs mp
19 changes: 13 additions & 6 deletions src/Cryptol/Parser/ParserUtils.hs
Original file line number Diff line number Diff line change
@@ -915,6 +915,7 @@ mkParDecls ds = DParamDecl loc (mkInterface [] ds)
mkInterface :: [Located (ImportG (ImpName PName))] ->
[ParamDecl PName] -> Signature PName
mkInterface is =
rev .
foldl' add
Signature { sigImports = is
, sigTypeParams = []
@@ -926,8 +927,17 @@ mkInterface is =
add s d =
case d of
DParameterType pt -> s { sigTypeParams = pt : sigTypeParams s }
DParameterConstraint ps -> s { sigConstraints = ps ++ sigConstraints s }
DParameterConstraint ps -> s { sigConstraints = ps : sigConstraints s }
DParameterFun pf -> s { sigFunParams = pf : sigFunParams s }
rev x = x { sigConstraints = reverse (sigConstraints x) }

mkIfacePropSyn :: Maybe Text -> Decl PName -> ParamDecl PName
mkIfacePropSyn mbDoc d =
case d of
DLocated d1 _ -> mkIfacePropSyn mbDoc d1
DType ts -> DParameterConstraint (SigTySyn ts mbDoc)
DProp ps -> DParameterConstraint (SigPropSyn ps mbDoc)
_ -> panic "mkIfacePropSyn" [ "Unexpected declaration", show (pp d) ]


-- | Make an unnamed module---gets the name @Main@.
@@ -1099,11 +1109,8 @@ desugarMod mo =
FunctorInstance f as _ | DefaultInstAnonArg lds <- as ->
do (ms,lds') <- desugarTopDs (mName mo) lds
case ms of
m : _ | InterfaceModule si <- mDef m
, l : _ <- map (srcRange . ptName) (sigTypeParams si) ++
map (srcRange . pfName) (sigFunParams si) ++
map srcRange (sigConstraints si) ->
errorMessage l
m : _ | InterfaceModule {} <- mDef m ->
errorMessage (srcRange (mName mo))
[ "Instantiation of a parameterized module may not itself be "
++ "parameterized" ]
_ -> pure ()
23 changes: 20 additions & 3 deletions src/Cryptol/TypeCheck/Infer.hs
Original file line number Diff line number Diff line change
@@ -1354,6 +1354,9 @@ checkTopDecls = mapM_ checkTopDecl
ips <- lookupSignature (thing (P.mpSignature p))
let actualTys = [ mapNames actualName mp
| mp <- Map.elems (mpnTypes ips) ]
actualTS = [ mapNames actualName ts
| ts <- Map.elems (mpnTySyn ips)
]
actualCtrs = [ mapNames actualName prop
| prop <- mpnConstraints ips ]
actualVals = [ mapNames actualName vp
@@ -1367,7 +1370,8 @@ checkTopDecls = mapM_ checkTopDecl
ModParamNames
{ mpnTypes = Map.fromList [ (mtpName tp, tp)
| tp <- actualTys ]

, mpnTySyn = Map.fromList [ (tsName ts, ts)
| ts <- actualTS ]
, mpnConstraints = actualCtrs
, mpnFuns = Map.fromList [ (mvpName vp, vp)
| vp <- actualVals ]
@@ -1378,6 +1382,7 @@ checkTopDecls = mapM_ checkTopDecl
mapM_ addParamType actualTys
addParameterConstraints actualCtrs
mapM_ addParamFun actualVals
mapM_ addTySyn actualTS
addModParam param

P.DImport {} -> pure ()
@@ -1393,14 +1398,26 @@ checkSignature sig =
do forM_ (P.sigTypeParams sig) \pt ->
addParamType =<< checkParameterType pt

addParameterConstraints =<<
checkParameterConstraints (P.sigConstraints sig)
mapM_ checkSigDecl (P.sigConstraints sig)

forM_ (P.sigFunParams sig) \f ->
addParamFun =<< checkParameterFun f

proveModuleTopLevel

checkSigDecl :: P.SigDecl Name -> InferM ()
checkSigDecl decl =
case decl of

P.SigConstraint cs ->
addParameterConstraints =<< checkParameterConstraints cs

P.SigTySyn ts mbD ->
addTySyn =<< checkTySyn ts mbD

P.SigPropSyn ps mbD ->
addTySyn =<< checkPropSyn ps mbD



checkDecl :: Bool -> P.Decl Name -> Maybe Text -> InferM ()
1 change: 1 addition & 0 deletions src/Cryptol/TypeCheck/ModuleInstance.hs
Original file line number Diff line number Diff line change
@@ -136,6 +136,7 @@ instance ModuleInstance ModParamNames where
ModParamNames { mpnTypes = doMap (mpnTypes si)
, mpnConstraints = moduleInstance (mpnConstraints si)
, mpnFuns = doMap (mpnFuns si)
, mpnTySyn = doMap (mpnTySyn si)
, mpnDoc = mpnDoc si
}

Loading