GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-16 09:20:24 +03:00
Code Issues Projects Releases Wiki Activity

Add a separate notation for imposing constraints on multiple module parameters

Browse Source
This commit is contained in:
Iavor Diatchki 2022-06-10 10:44:00 -07:00
parent 381612d4f1
commit 64ba445019
12 changed files with 112 additions and 114 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/Cryptol/ModuleSystem/Binds.hs
View File

@ -326,8 +326,11 @@ instance BindsNames (InModule (TopDecl PName)) where
Include _ -> mempty
DImport {} -> mempty -- see 'openLoop' in the renamer
DModule m -> namingEnv (InModule ns (tlValue m))
DModParam {} -> mempty-- handled in the renamer as we need to resolve
-- the signature name first (similar to import)
DModParam {} -> mempty -- shouldn't happen
DInterfaceConstraint {} -> mempty
-- handled in the renamer as we need to resolve
-- the signature name first (similar to import)
instance BindsNames (InModule (NestedModule PName)) where
namingEnv (InModule ~(Just m) (NestedModule mdef)) = BuildNamingEnv $

1
src/Cryptol/ModuleSystem/Exports.hs
View File

@ -26,6 +26,7 @@ exportedNames decl =
Include {} -> []
DImport {} -> []
DParamDecl {} -> []
DInterfaceConstraint {} -> []
DModule nested ->
case tlValue nested of
NestedModule x ->

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

@ -31,7 +31,7 @@ import Prelude ()
import Prelude.Compat
import Data.Either(partitionEithers)
import Data.Maybe(fromJust,mapMaybe)
import Data.Maybe(mapMaybe)
import Data.List(find,groupBy,sortBy)
import Data.Function(on)
import Data.Foldable(toList)
@ -47,7 +47,7 @@ import Cryptol.ModuleSystem.Name
import Cryptol.ModuleSystem.Names
import Cryptol.ModuleSystem.NamingEnv
import Cryptol.ModuleSystem.Exports
import Cryptol.Parser.Position(getLoc,Range)
import Cryptol.Parser.Position(Range)
import Cryptol.Parser.AST
import Cryptol.Parser.Selector(selName)
import Cryptol.Utils.Panic (panic)
@ -467,6 +467,7 @@ renameTopDecls' ds =
DPrimType {} -> False
TDNewtype {} -> False
DParamDecl {} -> False
DInterfaceConstraint {} -> False
DModule tl -> any usesCtrs (mDecls m)
@ -517,18 +518,7 @@ topDeclName topDecl =
DModule d -> hasName (thing (mName m))
where NestedModule m = tlValue d
DParamDecl ds ->
case ds of
[] -> noName
c : _ ->
case c of
DParameterConstraint cs ->
case cs of
[] -> noName
_ -> Right (topDecl, ConstratintAt (fromJust (getLoc cs)))
DParameterType {} -> bad "DParameterType"
DParameterFun {} -> bad "DParameterFun"
DInterfaceConstraint _ ds -> Right (topDecl, ConstratintAt (srcRange ds))
DImport {} -> noName
@ -537,6 +527,7 @@ topDeclName topDecl =
(mpName m))
Include {} -> bad "Include"
DParamDecl {} -> bad "DParamDecl"
where
noName = Left topDecl
hasName n = Right (topDecl, NamedThing n)
@ -642,20 +633,10 @@ instance Rename TopDecl where
DModule m -> DModule <$> traverse rename m
DImport li -> DImport <$> renI li
DModParam mp -> DModParam <$> rename mp
DParamDecl ds -> DParamDecl <$> traverse rename ds
instance Rename ParamDecl where
rename pd =
case pd of
DParameterFun f -> DParameterFun <$> rename f
DParameterType f -> DParameterType <$> rename f
DParameterConstraint ds ->
case ds of
[] -> pure (DParameterConstraint [])
_ -> depsOf (ConstratintAt (fromJust (getLoc ds)))
$ DParameterConstraint <$> mapM (rnLocated rename) ds
DInterfaceConstraint d ds ->
depsOf (ConstratintAt (srcRange ds))
(DInterfaceConstraint d <$> rnLocated (mapM rename) ds)
DParamDecl {} -> panic "rename" ["DParamDecl"]

10
src/Cryptol/Parser.y
View File

@ -277,7 +277,8 @@ vtop_decl :: { [TopDecl PName] }
| mbDoc newtype { [exportNewtype Public $1 $2] }
| prim_bind { $1 }
| private_decls { $1 }
| parameter_decls { [ DParamDecl $1 ] }
| mbDoc 'interface' 'constraint' type {% mkInterfaceConstraint $1 $4 }
| parameter_decls { [ $1 ] }
| mbDoc 'submodule'
module_def {% ((:[]) . exportModule $1) `fmap` mkNested $3 }
@ -287,6 +288,7 @@ vtop_decl :: { [TopDecl PName] }
-- we allow for documentation here to avoid conflicts with module paramaters
-- currently that odcumentation is just discarded
sig_def :: { (Located PName, Signature PName) }
: 'interface' 'submodule' name 'where' 'v{' sig_body 'v}'
{ ($3, $6) }
@ -324,9 +326,9 @@ prim_bind :: { [TopDecl PName] }
| mbDoc 'primitive' 'type' schema ':' kind {% mkPrimTypeDecl $1 $4 $6 }
parameter_decls :: { [ParamDecl PName] }
: 'parameter' 'v{' par_decls 'v}' { reverse $3 }
| doc 'parameter' 'v{' par_decls 'v}' { reverse $4 }
parameter_decls :: { TopDecl PName }
: 'parameter' 'v{' par_decls 'v}' { mkParDecls (reverse $3) }
| doc 'parameter' 'v{' par_decls 'v}' { mkParDecls (reverse $4) }
-- Reversed
par_decls :: { [ParamDecl PName] }

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

@ -230,15 +230,18 @@ data TopDecl name =
| TDNewtype (TopLevel (Newtype name)) -- ^ @newtype T as = t
| Include (Located FilePath) -- ^ @include File@ (until NoPat)
| DParamDecl [ParamDecl name]
-- ^ @parameter ...@
-- After parsing, there should be only DParamConstraint in this.
| DParamDecl Range (Signature name) -- ^ @parameter ...@ (parser only)
| DModule (TopLevel (NestedModule name)) -- ^ @submodule M where ...@
| DImport (Located (ImportG (ImpName name))) -- ^ @import X@
| DModParam (ModParam name) -- ^ @import interface X ...@
| DInterfaceConstraint (Maybe Text) (Located [Prop name])
-- ^ @interface constraint@
deriving (Show, Generic, NFData)
-- | Things that maybe appear in an interface/parameter block.
-- These only exist during parsering.
data ParamDecl name =
DParameterType (ParameterType name) -- ^ @parameter type T : #@ (parser only)
@ -669,7 +672,8 @@ instance HasLoc (TopDecl name) where
DModule d -> getLoc d
DImport d -> getLoc d
DModParam d -> getLoc d
DParamDecl ds -> foldr rCombMaybe Nothing (map getLoc ds)
DParamDecl r _ -> Just r
DInterfaceConstraint _ ds -> getLoc ds
instance HasLoc (ParamDecl name) where
getLoc pd =
@ -761,7 +765,7 @@ instance (Show name, PPName name) => PP (ModuleDefinition name) where
]
instLines = [ " *" <+> pp k <+> "->" <+> pp v
| (k,v) <- Map.toList inst ]
InterfaceModule s -> pp s
InterfaceModule s -> ppInterface "where" s
instance (Show name, PPName name) => PP (ModuleInstanceArgs name) where
@ -787,7 +791,13 @@ instance (Show name, PPName name) => PP (TopDecl name) where
DModule d -> pp d
DImport i -> pp (thing i)
DModParam s -> pp s
DParamDecl ds -> "parameter" $$ indent 2 (vcat (map pp ds))
DParamDecl _ ds -> ppInterface "parameter" ds
DInterfaceConstraint _ ds ->
"interface constraint" <+>
case map pp (thing ds) of
[x] -> x
[] -> "()"
xs -> nest 1 (parens (commaSepFill xs))
instance (Show name, PPName name) => PP (ParamDecl name) where
ppPrec _ pd =
@ -800,9 +810,8 @@ instance (Show name, PPName name) => PP (ParamDecl name) where
[] -> "()"
xs -> nest 1 (parens (commaSepFill xs))
instance (Show name, PPName name) => PP (Signature name) where
ppPrec _ sig = "where" $$ indent 2 (vcat (is ++ ds))
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)
@ -1242,7 +1251,9 @@ instance NoPos (TopDecl name) where
DModule d -> DModule (noPos d)
DImport d -> DImport (noPos d)
DModParam d -> DModParam (noPos d)
DParamDecl ds -> DParamDecl (noPos ds)
DParamDecl _ ds -> DParamDecl rng (noPos ds)
where rng = Range { from = Position 0 0, to = Position 0 0, source = "" }
DInterfaceConstraint d ds -> DInterfaceConstraint d (noPos (noPos <$> ds))
instance NoPos (ParamDecl name) where
noPos pd =

1
src/Cryptol/Parser/NoInclude.hs
View File

@ -183,6 +183,7 @@ noIncTopDecl td = case td of
DPrimType {} -> pure [td]
TDNewtype _-> pure [td]
DParamDecl {} -> pure [td]
DInterfaceConstraint {} -> pure [td]
Include lf -> resolveInclude lf
DModule tl ->
case tlValue tl of

1
src/Cryptol/Parser/NoPat.hs
View File

@ -378,6 +378,7 @@ annotTopDs tds =
(d1 :) <$> annotTopDs ds
DParamDecl {} -> (d :) <$> annotTopDs ds
DInterfaceConstraint {} -> (d :) <$> annotTopDs ds
-- XXX: we may want to add pragmas to newtypes?
TDNewtype {} -> (d :) <$> annotTopDs ds

116
src/Cryptol/Parser/ParserUtils.hs
View File

@ -17,6 +17,7 @@ module Cryptol.Parser.ParserUtils where
import Data.Maybe(fromMaybe)
import Data.Bits(testBit,setBit)
import Data.Maybe(mapMaybe)
import Data.List(foldl')
import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
@ -538,6 +539,7 @@ changeExport e = map change
Include{} -> decl
DImport{} -> decl
DParamDecl{} -> decl
DInterfaceConstraint {} -> decl
mkTypeInst :: Named (Type PName) -> TypeInst PName
mkTypeInst x | nullIdent (thing (name x)) = PosInst (value x)
@ -836,6 +838,16 @@ mkSigDecl doc (nm,sig) =
}
}
mkInterfaceConstraint ::
Maybe (Located Text) -> Type PName -> ParseM [TopDecl PName]
mkInterfaceConstraint mbDoc ty =
do ps <- mkProp ty
pure [DInterfaceConstraint (thing <$> mbDoc) ps]
mkParDecls :: [ParamDecl PName] -> TopDecl PName
mkParDecls ds = DParamDecl loc (mkInterface [] ds)
where loc = rCombs (mapMaybe getLoc ds)
mkInterface :: [Located (ImportG (ImpName PName))] ->
[ParamDecl PName] -> Signature PName
mkInterface is =
@ -852,7 +864,6 @@ mkInterface is =
DParameterType pt -> s { sigTypeParams = pt : sigTypeParams s }
DParameterConstraint ps -> s { sigConstraints = ps ++ sigConstraints s }
DParameterFun pf -> s { sigFunParams = pf : sigFunParams s }
_ -> panic "mkSignature" ["Unexpected top-level declaration"]
-- | Make an unnamed module---gets the name @Main@.
@ -972,7 +983,6 @@ desugarMod :: MkAnon name => ModuleG name PName -> ParseM [ModuleG name PName]
desugarMod mo =
case mDef mo of
-- XXX: we should check that `lds` does not have parameter declarations
FunctorInstance f as _ | DefaultInstAnonArg lds <- as ->
do (ms,lds') <- desugarTopDs (mName mo) lds
case ms of
@ -1002,73 +1012,65 @@ desugarTopDs ::
Located name ->
[TopDecl PName] ->
ParseM ([ModuleG name PName], [TopDecl PName])
desugarTopDs ownerName = go [] [] [] []
desugarTopDs ownerName = go emptySig
where
go is ts cs fs ds =
isEmpty s =
null (sigTypeParams s) && null (sigConstraints s) && null (sigFunParams s)
emptySig = Signature
{ sigImports = []
, sigTypeParams = []
, sigConstraints = []
, sigFunParams = []
}
jnSig s1 s2 = Signature { sigImports = j sigImports
, sigTypeParams = j sigTypeParams
, sigConstraints = j sigConstraints
, sigFunParams = j sigFunParams
}
where
j f = f s1 ++ f s2
addI i s = s { sigImports = i : sigImports s }
go sig ds =
case ds of
[] ->
case (ts,cs,fs) of
([],[],[]) -> pure ([],[])
_ ->
do let nm = mkAnon AnonIfaceMod <$> ownerName
pure ( [ Module { mName = nm
, mDef = InterfaceModule
Signature
{ sigImports = reverse is
, sigTypeParams = reverse ts
, sigConstraints = reverse cs
, sigFunParams = reverse fs
}
}
]
, [ DModParam
ModParam
{ mpSignature = toImpName <$> nm
, mpAs = Nothing
, mpName = mkModParamName (toImpName <$> nm)
Nothing
, mpDoc = Nothing
, mpRenaming = mempty
}
]
)
[]
| isEmpty sig -> pure ([],[])
| otherwise ->
do let nm = mkAnon AnonIfaceMod <$> ownerName
pure ( [ Module { mName = nm
, mDef = InterfaceModule sig
}
]
, [ DModParam
ModParam
{ mpSignature = toImpName <$> nm
, mpAs = Nothing
, mpName = mkModParamName (toImpName <$> nm)
Nothing
, mpDoc = Nothing
, mpRenaming = mempty
}
]
)
d : more ->
let cont emit is' ts' cs' fs' =
do (ms,ds') <- go is' ts' cs' fs' more
let cont emit sig' =
do (ms,ds') <- go sig' more
pure (ms, emit ++ ds')
in
case d of
-- collect to add to interface module, if any
DImport i -> cont [d] (i : is) ts cs fs
{- Parameter declarations only containing constrains are left as is
while ones that are part of a group with some parameters are factored.
This is because we reuse `parameter type constraint C` to also impose
constraints between parameters imports from *different* interfaces. -}
DParamDecl ds' ->
case groupParamDecls [] [] [] ds' of
([], _, []) -> cont [DParamDecl ds'] is ts cs fs
(ts',cs',fs') -> cont [] is (ts'++ts) (cs'++cs) (fs'++fs)
DImport i -> cont [d] (addI i sig)
DParamDecl _ ds' -> cont [] (jnSig ds' sig)
DModule tl | NestedModule mo <- tlValue tl ->
do ms <- desugarMod mo
cont [ DModule tl { tlValue = NestedModule m } | m <- ms ]
is ts cs fs
_ -> cont [d] is ts cs fs
groupParamDecls ts cs fs ds =
case ds of
d : more ->
case d of
DParameterType t -> groupParamDecls (t:ts) cs fs more
DParameterFun f -> groupParamDecls ts cs (f:fs) more
DParameterConstraint c -> groupParamDecls ts (c++cs) fs more
[] -> (ts,cs,fs)
cont [ DModule tl { tlValue = NestedModule m } | m <- ms ] sig
_ -> cont [d] sig

14
src/Cryptol/TypeCheck/Infer.hs
View File

@ -1075,15 +1075,10 @@ checkTopDecls = mapM_ checkTopDecl
addPrimType t
P.DParamDecl ds ->
forM_ ds \d ->
case d of
P.DParameterConstraint cs ->
do cs1 <- checkParameterConstraints cs
addParameterConstraints cs1
P.DParameterType{} -> bad "DParameterType"
P.DParameterFun{} -> bad "DParameterFun"
P.DInterfaceConstraint _ cs ->
inRange (srcRange cs)
do cs1 <- checkParameterConstraints [ cs { thing = c } | c <- thing cs ]
addParameterConstraints cs1
P.DModule tl ->
case P.mDef m of
@ -1147,6 +1142,7 @@ checkTopDecls = mapM_ checkTopDecl
P.DImport {} -> pure ()
P.Include {} -> bad "Include"
P.DParamDecl {} -> bad "DParamDecl"
bad x = panic "checkTopDecl" [ x ]

2
tests/modsys/functors/T004.cry
View File

@ -7,7 +7,7 @@ submodule F where
import interface submodule A as X
import interface submodule A as Y
parameter type constraint (X::n == Y::n)
interface constraint (X::n == Y::n)
y : [X::n]
y = X::x + Y::x

2
tests/modsys/functors/T005.cry
View File

@ -7,7 +7,7 @@ submodule F where
import interface submodule A as X
import interface submodule A as Y
parameter type constraint (X::n == Y::n)
interface constraint (X::n == Y::n)
y : [X::n]
y = X::x + Y::x

4
tests/modsys/functors/T006.cry
View File

@ -6,11 +6,11 @@ interface submodule A where
submodule F where
import interface submodule A as X
parameter type constraint (X::n >= 3)
interface constraint (X::n >= 3)
submodule G where
import interface submodule A
parameter type constraint (X::n == n)
interface constraint (X::n == n)
y : [n]
y = 5 * X::x + x