diff --git a/src/Cryptol/ModuleSystem/Binds.hs b/src/Cryptol/ModuleSystem/Binds.hs index b1fe54aa..ffb05c31 100644 --- a/src/Cryptol/ModuleSystem/Binds.hs +++ b/src/Cryptol/ModuleSystem/Binds.hs @@ -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 $ diff --git a/src/Cryptol/ModuleSystem/Exports.hs b/src/Cryptol/ModuleSystem/Exports.hs index 45380d25..05da90ad 100644 --- a/src/Cryptol/ModuleSystem/Exports.hs +++ b/src/Cryptol/ModuleSystem/Exports.hs @@ -26,6 +26,7 @@ exportedNames decl = Include {} -> [] DImport {} -> [] DParamDecl {} -> [] + DInterfaceConstraint {} -> [] DModule nested -> case tlValue nested of NestedModule x -> diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 757baac8..792349db 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -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"] diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index 50a40659..64f53690 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -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] } diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index fde47132..19d1be95 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -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 = diff --git a/src/Cryptol/Parser/NoInclude.hs b/src/Cryptol/Parser/NoInclude.hs index 66423e7a..917ae52d 100644 --- a/src/Cryptol/Parser/NoInclude.hs +++ b/src/Cryptol/Parser/NoInclude.hs @@ -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 diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index c3158c04..e9400cc6 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -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 diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index 515c30d6..87e329e1 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index a25b03ff..5713ff65 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -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 ] diff --git a/tests/modsys/functors/T004.cry b/tests/modsys/functors/T004.cry index 4205cd7e..1e164c5a 100644 --- a/tests/modsys/functors/T004.cry +++ b/tests/modsys/functors/T004.cry @@ -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 diff --git a/tests/modsys/functors/T005.cry b/tests/modsys/functors/T005.cry index c9fbf1a8..0b023332 100644 --- a/tests/modsys/functors/T005.cry +++ b/tests/modsys/functors/T005.cry @@ -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 diff --git a/tests/modsys/functors/T006.cry b/tests/modsys/functors/T006.cry index 740b10bb..7daad822 100644 --- a/tests/modsys/functors/T006.cry +++ b/tests/modsys/functors/T006.cry @@ -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