mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Treat parameter groups specially if they contain only constraints
This commit is contained in:
Iavor Diatchki
parent
7e3d65090c
commit
ca17f7f6df
@ -322,9 +322,7 @@ instance BindsNames (InModule (TopDecl PName)) where
|
||||
Decl d -> namingEnv (InModule ns (tlValue d))
|
||||
DPrimType d -> namingEnv (InModule ns (tlValue d))
|
||||
TDNewtype d -> namingEnv (InModule ns (tlValue d))
|
||||
DParameterType {} -> panic "namingEnv" ["DParameterType"]
|
||||
DParameterFun {} -> panic "namingEnv" ["DParameterFun"]
|
||||
DParameterConstraint {} -> mempty
|
||||
DParamDecl {} -> mempty
|
||||
Include _ -> mempty
|
||||
DImport {} -> mempty -- see 'openLoop' in the renamer
|
||||
DModule m -> namingEnv (InModule ns (tlValue m))
|
||||
|
||||
@ -9,7 +9,6 @@ import Data.Foldable(fold)
|
||||
import Control.DeepSeq(NFData)
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Parser.AST
|
||||
import Cryptol.Parser.Names(namesD,tnamesD,tnamesNT)
|
||||
import Cryptol.ModuleSystem.Name
|
||||
@ -26,9 +25,7 @@ exportedNames decl =
|
||||
TDNewtype nt -> map exportType (names tnamesNT nt)
|
||||
Include {} -> []
|
||||
DImport {} -> []
|
||||
DParameterFun {} -> panic "exportedNames" ["DParameterFun"]
|
||||
DParameterType {} -> panic "exportedNames" ["DParameterType"]
|
||||
DParameterConstraint {} -> []
|
||||
DParamDecl {} -> []
|
||||
DModule nested ->
|
||||
case tlValue nested of
|
||||
NestedModule x ->
|
||||
|
||||
@ -466,7 +466,7 @@ renameTopDecls' ds =
|
||||
Decl tl -> isValDecl (tlValue tl)
|
||||
DPrimType {} -> False
|
||||
TDNewtype {} -> False
|
||||
DParameterConstraint {} -> False
|
||||
DParamDecl {} -> False
|
||||
|
||||
|
||||
DModule tl -> any usesCtrs (mDecls m)
|
||||
@ -474,8 +474,6 @@ renameTopDecls' ds =
|
||||
DImport {} -> False
|
||||
DModParam {} -> False -- no definitions here
|
||||
Include {} -> bad "Include"
|
||||
DParameterType {} -> bad "DParameterType"
|
||||
DParameterFun {} -> bad "DParameterFun"
|
||||
|
||||
isValDecl d =
|
||||
case d of
|
||||
@ -519,18 +517,25 @@ topDeclName topDecl =
|
||||
DModule d -> hasName (thing (mName m))
|
||||
where NestedModule m = tlValue d
|
||||
|
||||
DParameterConstraint ds ->
|
||||
DParamDecl ds ->
|
||||
case ds of
|
||||
[] -> noName
|
||||
_ -> Right (topDecl, ConstratintAt (fromJust (getLoc ds)))
|
||||
[] -> noName
|
||||
c : _ ->
|
||||
case c of
|
||||
DParameterConstraint cs ->
|
||||
case cs of
|
||||
[] -> noName
|
||||
_ -> Right (topDecl, ConstratintAt (fromJust (getLoc cs)))
|
||||
|
||||
DParameterType {} -> bad "DParameterType"
|
||||
DParameterFun {} -> bad "DParameterFun"
|
||||
|
||||
DImport {} -> noName
|
||||
|
||||
DModParam m -> Right ( topDecl
|
||||
, ModParamName (srcRange (mpSignature m))
|
||||
(mpName m))
|
||||
|
||||
DParameterType {} -> bad "DParameterType"
|
||||
DParameterFun {} -> bad "DParameterFun"
|
||||
Include {} -> bad "Include"
|
||||
where
|
||||
noName = Left topDecl
|
||||
@ -634,6 +639,15 @@ instance Rename TopDecl where
|
||||
DPrimType d -> DPrimType <$> traverse rename d
|
||||
TDNewtype n -> TDNewtype <$> traverse rename n
|
||||
Include n -> return (Include n)
|
||||
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
|
||||
|
||||
@ -643,9 +657,7 @@ instance Rename TopDecl where
|
||||
_ -> depsOf (ConstratintAt (fromJust (getLoc ds)))
|
||||
$ DParameterConstraint <$> mapM (rnLocated rename) ds
|
||||
|
||||
DModule m -> DModule <$> traverse rename m
|
||||
DImport li -> DImport <$> renI li
|
||||
DModParam mp -> DModParam <$> rename mp
|
||||
|
||||
|
||||
renI :: Located (ImportG (ImpName PName)) ->
|
||||
RenameM (Located (ImportG (ImpName Name)))
|
||||
|
||||
@ -277,7 +277,7 @@ vtop_decl :: { [TopDecl PName] }
|
||||
| mbDoc newtype { [exportNewtype Public $1 $2] }
|
||||
| prim_bind { $1 }
|
||||
| private_decls { $1 }
|
||||
| parameter_decls { $1 }
|
||||
| parameter_decls { [ DParamDecl $1 ] }
|
||||
| mbDoc 'submodule'
|
||||
module_def {% ((:[]) . exportModule $1) `fmap` mkNested $3 }
|
||||
|
||||
@ -324,17 +324,17 @@ prim_bind :: { [TopDecl PName] }
|
||||
| mbDoc 'primitive' 'type' schema ':' kind {% mkPrimTypeDecl $1 $4 $6 }
|
||||
|
||||
|
||||
parameter_decls :: { [TopDecl PName] }
|
||||
parameter_decls :: { [ParamDecl PName] }
|
||||
: 'parameter' 'v{' par_decls 'v}' { reverse $3 }
|
||||
| doc 'parameter' 'v{' par_decls 'v}' { reverse $4 }
|
||||
|
||||
-- Reversed
|
||||
par_decls :: { [TopDecl PName] }
|
||||
par_decls :: { [ParamDecl PName] }
|
||||
: par_decl { [$1] }
|
||||
| par_decls ';' par_decl { $3 : $1 }
|
||||
| par_decls 'v;' par_decl { $3 : $1 }
|
||||
|
||||
par_decl :: { TopDecl 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)
|
||||
|
||||
@ -73,6 +73,7 @@ module Cryptol.Parser.AST
|
||||
, NestedModule(..)
|
||||
, Signature(..)
|
||||
, ModParam(..)
|
||||
, ParamDecl(..)
|
||||
|
||||
-- * Interactive
|
||||
, ReplInput(..)
|
||||
@ -201,9 +202,7 @@ isParamDecl :: TopDecl a -> Bool
|
||||
isParamDecl d =
|
||||
case d of
|
||||
DModParam {} -> True
|
||||
DParameterType {} -> True
|
||||
DParameterConstraint {} -> True
|
||||
DParameterFun {} -> True
|
||||
DParamDecl {} -> True
|
||||
_ -> False
|
||||
|
||||
|
||||
@ -231,19 +230,27 @@ data TopDecl name =
|
||||
| TDNewtype (TopLevel (Newtype name)) -- ^ @newtype T as = t
|
||||
| Include (Located FilePath) -- ^ @include File@ (until NoPat)
|
||||
|
||||
-- Sugar for anonymous module parameters (parser only)
|
||||
| DParameterType (ParameterType name) -- ^ @parameter type T : #@ (parser only)
|
||||
| DParameterFun (ParameterFun name) -- ^ @parameter someVal : [256]@
|
||||
-- (parser only)
|
||||
|
||||
| DParameterConstraint [Located (Prop name)]
|
||||
-- ^ @parameter type constraint (fin T)@
|
||||
| DParamDecl [ParamDecl name]
|
||||
-- ^ @parameter ...@
|
||||
-- After parsing, there should be only DParamConstraint in this.
|
||||
|
||||
| DModule (TopLevel (NestedModule name)) -- ^ @submodule M where ...@
|
||||
| DImport (Located (ImportG (ImpName name))) -- ^ @import X@
|
||||
| DModParam (ModParam name) -- ^ @import interface X ...@
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
data ParamDecl name =
|
||||
|
||||
DParameterType (ParameterType name) -- ^ @parameter type T : #@ (parser only)
|
||||
| DParameterFun (ParameterFun name) -- ^ @parameter someVal : [256]@
|
||||
-- (parser only)
|
||||
|
||||
| DParameterConstraint [Located (Prop name)]
|
||||
-- ^ @parameter type constraint (fin T)@
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
|
||||
|
||||
data ModuleInstanceArgs name =
|
||||
DefaultInstArg (Located (ImpName name))
|
||||
-- ^ Single parameter instantitaion
|
||||
@ -659,12 +666,17 @@ instance HasLoc (TopDecl name) where
|
||||
DPrimType pt -> getLoc pt
|
||||
TDNewtype n -> getLoc n
|
||||
Include lfp -> getLoc lfp
|
||||
DParameterType d -> getLoc d
|
||||
DParameterFun d -> getLoc d
|
||||
DParameterConstraint d -> getLoc d
|
||||
DModule d -> getLoc d
|
||||
DImport d -> getLoc d
|
||||
DModParam d -> getLoc d
|
||||
DParamDecl ds -> foldr rCombMaybe Nothing (map getLoc ds)
|
||||
|
||||
instance HasLoc (ParamDecl name) where
|
||||
getLoc pd =
|
||||
case pd of
|
||||
DParameterType d -> getLoc d
|
||||
DParameterFun d -> getLoc d
|
||||
DParameterConstraint d -> getLoc d
|
||||
|
||||
instance HasLoc (ModParam name) where
|
||||
getLoc mp = getLoc (mpSignature mp)
|
||||
@ -772,17 +784,22 @@ instance (Show name, PPName name) => PP (TopDecl name) where
|
||||
DPrimType p -> pp p
|
||||
TDNewtype n -> pp n
|
||||
Include l -> text "include" <+> text (show (thing l))
|
||||
DModule d -> pp d
|
||||
DImport i -> pp (thing i)
|
||||
DModParam s -> pp s
|
||||
DParamDecl ds -> "parameter" $$ indent 2 (vcat (map pp ds))
|
||||
|
||||
instance (Show name, PPName name) => PP (ParamDecl name) where
|
||||
ppPrec _ pd =
|
||||
case pd of
|
||||
DParameterFun d -> pp d
|
||||
DParameterType d -> pp d
|
||||
DParameterConstraint d ->
|
||||
"parameter" <+> "type" <+> "constraint" <+> prop
|
||||
DParameterConstraint d -> "type" <+> "constraint" <+> prop
|
||||
where prop = case map (pp . thing) d of
|
||||
[x] -> x
|
||||
[] -> "()"
|
||||
xs -> nest 1 (parens (commaSepFill xs))
|
||||
DModule d -> pp d
|
||||
DImport i -> pp (thing i)
|
||||
DModParam s -> pp s
|
||||
|
||||
|
||||
instance (Show name, PPName name) => PP (Signature name) where
|
||||
ppPrec _ sig = "where" $$ indent 2 (vcat (is ++ ds))
|
||||
@ -822,11 +839,11 @@ instance (Show name, PPName name) => PP (PrimType name) where
|
||||
"primitive" <+> "type" <+> pp (primTName pt) <+> ":" <+> pp (primTKind pt)
|
||||
|
||||
instance (Show name, PPName name) => PP (ParameterType name) where
|
||||
ppPrec _ a = text "parameter" <+> text "type" <+>
|
||||
ppPrec _ a = text "type" <+>
|
||||
ppPrefixName (ptName a) <+> text ":" <+> pp (ptKind a)
|
||||
|
||||
instance (Show name, PPName name) => PP (ParameterFun name) where
|
||||
ppPrec _ a = text "parameter" <+> ppPrefixName (pfName a) <+> text ":"
|
||||
ppPrec _ a = ppPrefixName (pfName a) <+> text ":"
|
||||
<+> pp (pfSchema a)
|
||||
|
||||
|
||||
@ -1222,12 +1239,17 @@ instance NoPos (TopDecl name) where
|
||||
DPrimType t -> DPrimType (noPos t)
|
||||
TDNewtype n -> TDNewtype(noPos n)
|
||||
Include x -> Include (noPos x)
|
||||
DParameterFun d -> DParameterFun (noPos d)
|
||||
DParameterType d -> DParameterType (noPos d)
|
||||
DParameterConstraint d -> DParameterConstraint (noPos d)
|
||||
DModule d -> DModule (noPos d)
|
||||
DImport d -> DImport (noPos d)
|
||||
DModParam d -> DModParam (noPos d)
|
||||
DParamDecl ds -> DParamDecl (noPos ds)
|
||||
|
||||
instance NoPos (ParamDecl name) where
|
||||
noPos pd =
|
||||
case pd of
|
||||
DParameterFun d -> DParameterFun (noPos d)
|
||||
DParameterType d -> DParameterType (noPos d)
|
||||
DParameterConstraint d -> DParameterConstraint (noPos d)
|
||||
|
||||
instance NoPos (Signature name) where
|
||||
noPos sig = Signature { sigImports = sigImports sig
|
||||
|
||||
@ -29,7 +29,6 @@ import MonadLib
|
||||
import System.Directory (makeAbsolute)
|
||||
import System.FilePath (takeDirectory,(</>),isAbsolute)
|
||||
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.PP hiding ((</>))
|
||||
import Cryptol.Parser (parseProgramWith)
|
||||
import Cryptol.Parser.AST
|
||||
@ -183,9 +182,7 @@ noIncTopDecl td = case td of
|
||||
Decl _ -> pure [td]
|
||||
DPrimType {} -> pure [td]
|
||||
TDNewtype _-> pure [td]
|
||||
DParameterConstraint {} -> pure [td]
|
||||
DParameterType {} -> panic "noIncTopDecl" ["DParameterType"]
|
||||
DParameterFun {} -> panic "noIncTopDecl" ["DParameterFun"]
|
||||
DParamDecl {} -> pure [td]
|
||||
Include lf -> resolveInclude lf
|
||||
DModule tl ->
|
||||
case tlValue tl of
|
||||
|
||||
@ -377,10 +377,7 @@ annotTopDs tds =
|
||||
let d1 = DPrimType tl { tlValue = pt }
|
||||
(d1 :) <$> annotTopDs ds
|
||||
|
||||
DParameterConstraint {} -> (d :) <$> annotTopDs ds
|
||||
|
||||
DParameterType {} -> panic "annotTopDs" ["DParameterType"]
|
||||
DParameterFun {} -> panic "annotTopDs" ["DParameterFun"]
|
||||
DParamDecl {} -> (d :) <$> annotTopDs ds
|
||||
|
||||
-- XXX: we may want to add pragmas to newtypes?
|
||||
TDNewtype {} -> (d :) <$> annotTopDs ds
|
||||
|
||||
@ -503,7 +503,7 @@ exportModule mbDoc m = DModule TopLevel { tlExport = Public
|
||||
mkParFun :: Maybe (Located Text) ->
|
||||
Located PName ->
|
||||
Schema PName ->
|
||||
TopDecl PName
|
||||
ParamDecl PName
|
||||
mkParFun mbDoc n s = DParameterFun ParameterFun { pfName = n
|
||||
, pfSchema = s
|
||||
, pfDoc = thing <$> mbDoc
|
||||
@ -513,7 +513,7 @@ mkParFun mbDoc n s = DParameterFun ParameterFun { pfName = n
|
||||
mkParType :: Maybe (Located Text) ->
|
||||
Located PName ->
|
||||
Located Kind ->
|
||||
ParseM (TopDecl PName)
|
||||
ParseM (ParamDecl PName)
|
||||
mkParType mbDoc n k =
|
||||
do num <- P $ \_ _ s -> let nu = sNextTyParamNum s
|
||||
in Right (nu, s { sNextTyParamNum = nu + 1 })
|
||||
@ -537,9 +537,7 @@ changeExport e = map change
|
||||
DModParam {} -> decl
|
||||
Include{} -> decl
|
||||
DImport{} -> decl
|
||||
DParameterType {} -> decl
|
||||
DParameterFun {} -> decl
|
||||
DParameterConstraint {} -> decl
|
||||
DParamDecl{} -> decl
|
||||
|
||||
mkTypeInst :: Named (Type PName) -> TypeInst PName
|
||||
mkTypeInst x | nullIdent (thing (name x)) = PosInst (value x)
|
||||
@ -839,7 +837,7 @@ mkSigDecl doc (nm,sig) =
|
||||
}
|
||||
|
||||
mkInterface :: [Located (ImportG (ImpName PName))] ->
|
||||
[TopDecl PName] -> Signature PName
|
||||
[ParamDecl PName] -> Signature PName
|
||||
mkInterface is =
|
||||
foldl' add
|
||||
Signature { sigImports = is
|
||||
@ -855,7 +853,7 @@ mkInterface is =
|
||||
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@.
|
||||
mkAnonymousModule :: [TopDecl PName] -> ParseM [Module PName]
|
||||
@ -980,7 +978,8 @@ desugarMod mo =
|
||||
case ms of
|
||||
m : _ | InterfaceModule si <- mDef m
|
||||
, l : _ <- map (srcRange . ptName) (sigTypeParams si) ++
|
||||
map (srcRange . pfName) (sigFunParams si) ->
|
||||
map (srcRange . pfName) (sigFunParams si) ++
|
||||
map srcRange (sigConstraints si) ->
|
||||
errorMessage l
|
||||
[ "Module argument may not be a functor" ]
|
||||
_ -> pure ()
|
||||
@ -1003,16 +1002,16 @@ desugarTopDs ::
|
||||
Located name ->
|
||||
[TopDecl PName] ->
|
||||
ParseM ([ModuleG name PName], [TopDecl PName])
|
||||
desugarTopDs ownerName = go [] [] []
|
||||
desugarTopDs ownerName = go [] [] [] []
|
||||
|
||||
where
|
||||
go is ts fs ds =
|
||||
go is ts cs fs ds =
|
||||
|
||||
case ds of
|
||||
|
||||
[] ->
|
||||
case (ts,fs) of
|
||||
([],[]) -> pure ([],[])
|
||||
case (ts,cs,fs) of
|
||||
([],[],[]) -> pure ([],[])
|
||||
_ ->
|
||||
do let nm = mkAnon AnonIfaceMod <$> ownerName
|
||||
pure ( [ Module { mName = nm
|
||||
@ -1020,7 +1019,7 @@ desugarTopDs ownerName = go [] [] []
|
||||
Signature
|
||||
{ sigImports = reverse is
|
||||
, sigTypeParams = reverse ts
|
||||
, sigConstraints = []
|
||||
, sigConstraints = reverse cs
|
||||
, sigFunParams = reverse fs
|
||||
}
|
||||
}
|
||||
@ -1038,23 +1037,38 @@ desugarTopDs ownerName = go [] [] []
|
||||
)
|
||||
|
||||
d : more ->
|
||||
let cont emit is' ts' fs' =
|
||||
do (ms,ds') <- go is' ts' fs' more
|
||||
let cont emit is' ts' cs' fs' =
|
||||
do (ms,ds') <- go is' ts' cs' fs' more
|
||||
pure (ms, emit ++ ds')
|
||||
in
|
||||
case d of
|
||||
-- collect to add to interface module, if any
|
||||
DImport i -> cont [d] (i : is) ts fs
|
||||
DImport i -> cont [d] (i : is) ts cs fs
|
||||
|
||||
-- these go in an interface module
|
||||
DParameterType pt -> cont [] is (pt : ts) fs
|
||||
DParameterFun pf -> cont [] is ts (pf : 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)
|
||||
|
||||
DModule tl | NestedModule mo <- tlValue tl ->
|
||||
do ms <- desugarMod mo
|
||||
cont [ DModule tl { tlValue = NestedModule m } | m <- ms ] is ts fs
|
||||
|
||||
_ -> cont [d] is ts fs
|
||||
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)
|
||||
|
||||
|
||||
|
||||
@ -1075,9 +1075,14 @@ checkTopDecls = mapM_ checkTopDecl
|
||||
addPrimType t
|
||||
|
||||
|
||||
P.DParameterConstraint cs ->
|
||||
do cs1 <- checkParameterConstraints cs
|
||||
addParameterConstraints cs1
|
||||
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.DModule tl ->
|
||||
@ -1142,8 +1147,6 @@ checkTopDecls = mapM_ checkTopDecl
|
||||
|
||||
P.DImport {} -> pure ()
|
||||
P.Include {} -> bad "Include"
|
||||
P.DParameterType{} -> bad "DParameterType"
|
||||
P.DParameterFun{} -> bad "DParameterFun"
|
||||
|
||||
|
||||
bad x = panic "checkTopDecl" [ x ]
|
||||
|
||||
@ -1,3 +1,4 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading interface module test$interface
|
||||
Loading module test
|
||||
|
||||
Loading…
Reference in New Issue
Block a user