From f834e24313bbca3d93e6ee4538310adafa9c2fa9 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 12 Dec 2022 14:19:07 -0800 Subject: [PATCH 01/21] Add scaffolfing for backtick imports --- src/Cryptol/ModuleSystem/Base.hs | 1 + src/Cryptol/ModuleSystem/Renamer.hs | 3 +++ src/Cryptol/Parser/AST.hs | 6 ++++++ 3 files changed, 10 insertions(+) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 3b382fa05..fa61748eb 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -468,6 +468,7 @@ findDeps' m = DefaultInstArg a -> loadInstArg a DefaultInstAnonArg ds -> mconcat (map depsOfDecl ds) NamedInstArgs args -> mconcat (map loadNamedInstArg args) + BacktickInstnace -> mempty in fds <> ads InterfaceModule s -> mconcat (map loadImpD (sigImports s)) where diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index abaaffc14..c8274605f 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -292,6 +292,7 @@ checkFunctorArgs args = panic "checkFunctorArgs" ["Nested DefaultInstAnonArg"] DefaultInstArg l -> checkArg l NamedInstArgs as -> mapM_ checkNamedArg as + BacktickInstnace -> pure () where checkNamedArg (ModuleInstanceNamedArg _ l) = checkArg l @@ -480,6 +481,7 @@ renameTopDecls' ds = DefaultInstArg arg -> depsOfArg arg NamedInstArgs args -> concatMap depsOfNamedArg args DefaultInstAnonArg {} -> [] + BacktickInstnace -> [] where depsOfNamedArg (ModuleInstanceNamedArg _ a) = depsOfArg a depsOfArg a = case thing a of @@ -793,6 +795,7 @@ instance Rename ModuleInstanceArgs where DefaultInstArg a -> DefaultInstArg <$> rnLocated rename a NamedInstArgs xs -> NamedInstArgs <$> traverse rename xs DefaultInstAnonArg {} -> panic "rename" ["DefaultInstAnonArg"] + BacktickInstnace -> pure BacktickInstnace instance Rename ModuleInstanceNamedArg where rename (ModuleInstanceNamedArg x m) = diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 9df414043..f2997319a 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -281,6 +281,10 @@ data ModuleInstanceArgs name = -- (parser only) | NamedInstArgs [ModuleInstanceNamedArg name] + + | BacktickInstnace + -- ^ The module instance is computed by adding the functor arguments + -- as explicit parameters to all declarations deriving (Show, Generic, NFData) -- | A named argument in a functor instantiation @@ -863,6 +867,7 @@ instance (Show name, PPName name) => PP (ModuleInstanceArgs name) where DefaultInstArg x -> braces (pp (thing x)) DefaultInstAnonArg ds -> "where" $$ indent 2 (vcat (map pp ds)) NamedInstArgs xs -> braces (commaSep (map pp xs)) + BacktickInstnace -> "{}" instance (Show name, PPName name) => PP (ModuleInstanceNamedArg name) where ppPrec _ (ModuleInstanceNamedArg x y) = pp (thing x) <+> "=" <+> pp (thing y) @@ -1358,6 +1363,7 @@ instance NoPos (ModuleInstanceArgs name) where DefaultInstArg a -> DefaultInstArg (noPos a) DefaultInstAnonArg ds -> DefaultInstAnonArg (noPos ds) NamedInstArgs xs -> NamedInstArgs (noPos xs) + BacktickInstnace -> BacktickInstnace instance NoPos (ModuleInstanceNamedArg name) where noPos (ModuleInstanceNamedArg x y) = From 02a5e80c53d08edf469f101d454db1d196a95ab6 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 12 Dec 2022 16:55:50 -0800 Subject: [PATCH 02/21] Make a module for the instantiation code --- cryptol.cabal | 1 + src/Cryptol/ModuleSystem/Base.hs | 2 +- src/Cryptol/ModuleSystem/Renamer.hs | 6 +- src/Cryptol/Parser/AST.hs | 8 +-- src/Cryptol/TypeCheck/Module.hs | 69 +++++++++++-------- .../TypeCheck/ModuleBacktickInstance.hs | 16 +++++ 6 files changed, 66 insertions(+), 36 deletions(-) create mode 100644 src/Cryptol/TypeCheck/ModuleBacktickInstance.hs diff --git a/cryptol.cabal b/cryptol.cabal index af43c6169..217b93f35 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -177,6 +177,7 @@ library Cryptol.TypeCheck.FFI.FFIType, Cryptol.TypeCheck.Module, Cryptol.TypeCheck.ModuleInstance, + Cryptol.TypeCheck.ModuleBacktickInstance, Cryptol.TypeCheck.Solver.Types, Cryptol.TypeCheck.Solver.SMT, diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index fa61748eb..035fa6e56 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -468,7 +468,7 @@ findDeps' m = DefaultInstArg a -> loadInstArg a DefaultInstAnonArg ds -> mconcat (map depsOfDecl ds) NamedInstArgs args -> mconcat (map loadNamedInstArg args) - BacktickInstnace -> mempty + BacktickInstance -> mempty in fds <> ads InterfaceModule s -> mconcat (map loadImpD (sigImports s)) where diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index c8274605f..36d7a34ca 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -292,7 +292,7 @@ checkFunctorArgs args = panic "checkFunctorArgs" ["Nested DefaultInstAnonArg"] DefaultInstArg l -> checkArg l NamedInstArgs as -> mapM_ checkNamedArg as - BacktickInstnace -> pure () + BacktickInstance -> pure () where checkNamedArg (ModuleInstanceNamedArg _ l) = checkArg l @@ -481,7 +481,7 @@ renameTopDecls' ds = DefaultInstArg arg -> depsOfArg arg NamedInstArgs args -> concatMap depsOfNamedArg args DefaultInstAnonArg {} -> [] - BacktickInstnace -> [] + BacktickInstance -> [] where depsOfNamedArg (ModuleInstanceNamedArg _ a) = depsOfArg a depsOfArg a = case thing a of @@ -795,7 +795,7 @@ instance Rename ModuleInstanceArgs where DefaultInstArg a -> DefaultInstArg <$> rnLocated rename a NamedInstArgs xs -> NamedInstArgs <$> traverse rename xs DefaultInstAnonArg {} -> panic "rename" ["DefaultInstAnonArg"] - BacktickInstnace -> pure BacktickInstnace + BacktickInstance -> pure BacktickInstance instance Rename ModuleInstanceNamedArg where rename (ModuleInstanceNamedArg x m) = diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index f2997319a..6c78a019d 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -282,9 +282,9 @@ data ModuleInstanceArgs name = | NamedInstArgs [ModuleInstanceNamedArg name] - | BacktickInstnace + | BacktickInstance -- ^ The module instance is computed by adding the functor arguments - -- as explicit parameters to all declarations + -- as explicit parameters to all declarations. deriving (Show, Generic, NFData) -- | A named argument in a functor instantiation @@ -867,7 +867,7 @@ instance (Show name, PPName name) => PP (ModuleInstanceArgs name) where DefaultInstArg x -> braces (pp (thing x)) DefaultInstAnonArg ds -> "where" $$ indent 2 (vcat (map pp ds)) NamedInstArgs xs -> braces (commaSep (map pp xs)) - BacktickInstnace -> "{}" + BacktickInstance -> "{}" instance (Show name, PPName name) => PP (ModuleInstanceNamedArg name) where ppPrec _ (ModuleInstanceNamedArg x y) = pp (thing x) <+> "=" <+> pp (thing y) @@ -1363,7 +1363,7 @@ instance NoPos (ModuleInstanceArgs name) where DefaultInstArg a -> DefaultInstArg (noPos a) DefaultInstAnonArg ds -> DefaultInstAnonArg (noPos ds) NamedInstArgs xs -> NamedInstArgs (noPos xs) - BacktickInstnace -> BacktickInstnace + BacktickInstance -> BacktickInstance instance NoPos (ModuleInstanceNamedArg name) where noPos (ModuleInstanceNamedArg x y) = diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 102b1f9f8..d6497ab82 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -24,6 +24,7 @@ import Cryptol.TypeCheck.Solve(proveImplication) import Cryptol.TypeCheck.Monad import Cryptol.TypeCheck.Instantiate(instantiateWith) import Cryptol.TypeCheck.ModuleInstance +import Cryptol.TypeCheck.ModuleBacktickInstance(doBacktickInstance) doFunctorInst :: Located (P.ImpName Name) {- ^ Name for the new module -} -> @@ -39,24 +40,25 @@ doFunctorInst m f as inst doc = inRange (srcRange m) do mf <- lookupFunctor (thing f) argIs <- checkArity (srcRange f) mf as - (tySus,decls) <- unzip <$> mapM checkArg argIs - - - let ?tSu = mergeDistinctSubst tySus - ?vSu = inst - let m1 = moduleInstance mf - m2 = m1 { mName = m - , mDoc = Nothing - , 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 - } - - newGoals CtModuleInstance (map thing (mParamConstraints m1)) + m2 <- case argIs of + UseArgs ais -> + do (tySus,decls) <- unzip <$> mapM checkArg ais + let ?tSu = mergeDistinctSubst tySus + ?vSu = inst + let m1 = moduleInstance mf + m2 = m1 { mName = m + , mDoc = Nothing + , mParamTypes = mempty + , mParamFuns = mempty + , mParamConstraints = mempty + , mParams = mempty + , mDecls = map NonRecursive (concat decls) ++ + mDecls m1 + } + newGoals CtModuleInstance (map thing (mParamConstraints m1)) + pure m2 + + AddParamsToDecls -> doBacktickInstance m mf inst case thing m of P.ImpTop mn -> newModuleScope mn (mExports m2) @@ -75,6 +77,15 @@ doFunctorInst m f as inst doc = P.ImpNested {} -> endSubmodule >> pure Nothing + +data ActualArg = + UseParameter ModParam -- ^ Instantiate using this parameter + | UseModule (IfaceG ()) -- ^ Instantiate using this module + +data ActualArgs = + UseArgs [(Range, ModParam, ActualArg)] + | AddParamsToDecls + {- | Validate a functor application, just checking the argument names. @@ -88,7 +99,7 @@ checkArity :: Range {- ^ Location for reporting errors -} -> ModuleG () {- ^ The functor being instantiated -} -> P.ModuleInstanceArgs Name {- ^ The arguments -} -> - InferM [ (Range, ModParam, Either ModParam (IfaceG ())) ] + InferM ActualArgs {- ^ Associates functor parameters with the interfaces of the instantiating modules -} checkArity r mf args = @@ -102,8 +113,9 @@ checkArity r mf args = P.NamedInstArgs as -> checkArgs [] ps0 as - P.DefaultInstAnonArg {} -> panic "checkArity" [ "DefaultInstAnonArg" ] + P.BacktickInstance -> pure AddParamsToDecls + P.DefaultInstAnonArg {} -> panic "checkArity" [ "DefaultInstAnonArg" ] where ps0 = mParams mf @@ -112,13 +124,13 @@ checkArity r mf args = [] -> do forM_ (Map.keys ps) \p -> recordErrorLoc (Just r) (FunctorInstanceMissingArgument p) - pure done + pure (UseArgs done) P.ModuleInstanceNamedArg ll lm : more -> case Map.lookup (thing ll) ps of Just i -> do arg <- case thing lm of - P.ModuleArg m -> Just . Right <$> lookupModule m + P.ModuleArg m -> Just . UseModule <$> lookupModule m P.ParameterArg p -> do mb <- lookupModParam p case mb of @@ -126,7 +138,7 @@ checkArity r mf args = do inRange (srcRange lm) (recordError (MissingModParam p)) pure Nothing - Just a -> pure (Just (Left a)) + Just a -> pure (Just (UseParameter a)) let next = case arg of Nothing -> done Just a -> (srcRange lm, i, a) : done @@ -148,7 +160,7 @@ Returns: values. -} checkArg :: - (Range, ModParam, Either ModParam (IfaceG ())) -> InferM (Subst, [Decl]) + (Range, ModParam, ActualArg) -> InferM (Subst, [Decl]) checkArg (r,expect,actual') = do tRens <- mapM (checkParamType r tyMap) (Map.toList (mpnTypes params)) let renSu = listParamSubst (concat tRens) @@ -175,15 +187,16 @@ checkArg (r,expect,actual') = vMap :: Map Ident (Name, Schema) (tyMap,vMap) = case actual' of - Left mp -> ( nameMapToIdentMap fromTP (mpnTypes ps) - , nameMapToIdentMap fromVP (mpnFuns ps) - ) + UseParameter mp -> + ( nameMapToIdentMap fromTP (mpnTypes ps) + , nameMapToIdentMap fromVP (mpnFuns ps) + ) where ps = mpParameters mp fromTP tp = (mtpKind tp, TVar (TVBound (mtpParam tp))) fromVP vp = (mvpName vp, mvpType vp) - Right actual -> + UseModule actual -> ( Map.unions [ nameMapToIdentMap fromTS (ifTySyns decls) , nameMapToIdentMap fromNewtype (ifNewtypes decls) , nameMapToIdentMap fromPrimT (ifAbstractTypes decls) diff --git a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs new file mode 100644 index 000000000..463480245 --- /dev/null +++ b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs @@ -0,0 +1,16 @@ +module Cryptol.TypeCheck.ModuleBacktickInstance where + +import Data.Map(Map) +import qualified Data.Map as Map + +import Cryptol.Parser.Position (Located(..), thing) +import qualified Cryptol.Parser.AST as P +import Cryptol.TypeCheck.AST +import Cryptol.TypeCheck.Monad + +doBacktickInstance :: + Located (P.ImpName Name) {- ^ Name for the new module -} -> + ModuleG () {- ^ The functor -} -> + Map Name Name {- ^ The instantiation: functor name -> instance name -} -> + InferM (ModuleG (Located (P.ImpName Name))) +doBacktickInstance m mf inst = undefined From e0d013596fdbd61631684b5b62cb514c3489c1a9 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 13 Dec 2022 14:44:08 -0800 Subject: [PATCH 03/21] Rearrange so that each functor parameter can be "backtick" instantiated separately. XXX: The order in which parameters should be added is very unclear. --- src/Cryptol/ModuleSystem/Base.hs | 1 - src/Cryptol/ModuleSystem/Renamer.hs | 7 +- src/Cryptol/Parser/AST.hs | 10 +- src/Cryptol/TypeCheck/Error.hs | 14 ++ src/Cryptol/TypeCheck/Module.hs | 127 ++++++++++++------ .../TypeCheck/ModuleBacktickInstance.hs | 13 +- 6 files changed, 117 insertions(+), 55 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 035fa6e56..3b382fa05 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -468,7 +468,6 @@ findDeps' m = DefaultInstArg a -> loadInstArg a DefaultInstAnonArg ds -> mconcat (map depsOfDecl ds) NamedInstArgs args -> mconcat (map loadNamedInstArg args) - BacktickInstance -> mempty in fds <> ads InterfaceModule s -> mconcat (map loadImpD (sigImports s)) where diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 36d7a34ca..013c6051f 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -292,7 +292,6 @@ checkFunctorArgs args = panic "checkFunctorArgs" ["Nested DefaultInstAnonArg"] DefaultInstArg l -> checkArg l NamedInstArgs as -> mapM_ checkNamedArg as - BacktickInstance -> pure () where checkNamedArg (ModuleInstanceNamedArg _ l) = checkArg l @@ -302,6 +301,7 @@ checkFunctorArgs args = | isFakeName m -> pure () | otherwise -> checkIsModule (srcRange l) m AModule ParameterArg {} -> pure () -- we check these in the type checker + AddParams -> pure () mkInstMap :: Maybe Range -> Map Name Name -> ImpName Name -> ImpName Name -> RenameM (Map Name Name) @@ -481,10 +481,10 @@ renameTopDecls' ds = DefaultInstArg arg -> depsOfArg arg NamedInstArgs args -> concatMap depsOfNamedArg args DefaultInstAnonArg {} -> [] - BacktickInstance -> [] where depsOfNamedArg (ModuleInstanceNamedArg _ a) = depsOfArg a depsOfArg a = case thing a of + AddParams -> [] ModuleArg {} -> [] ParameterArg p -> case Map.lookup p localParams of @@ -795,7 +795,6 @@ instance Rename ModuleInstanceArgs where DefaultInstArg a -> DefaultInstArg <$> rnLocated rename a NamedInstArgs xs -> NamedInstArgs <$> traverse rename xs DefaultInstAnonArg {} -> panic "rename" ["DefaultInstAnonArg"] - BacktickInstance -> pure BacktickInstance instance Rename ModuleInstanceNamedArg where rename (ModuleInstanceNamedArg x m) = @@ -806,7 +805,7 @@ instance Rename ModuleInstanceArg where case arg of ModuleArg m -> ModuleArg <$> rename m ParameterArg a -> pure (ParameterArg a) - + AddParams -> pure AddParams instance Rename NestedModule where rename (NestedModule m) = diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 6c78a019d..fcdd751a6 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -282,9 +282,6 @@ data ModuleInstanceArgs name = | NamedInstArgs [ModuleInstanceNamedArg name] - | BacktickInstance - -- ^ The module instance is computed by adding the functor arguments - -- as explicit parameters to all declarations. deriving (Show, Generic, NFData) -- | A named argument in a functor instantiation @@ -296,6 +293,8 @@ data ModuleInstanceNamedArg name = data ModuleInstanceArg name = ModuleArg (ImpName name) -- ^ An argument that is a module | ParameterArg Ident -- ^ An argument that is a parameter + | AddParams -- ^ Arguments adds extra parameters to decls. + -- ("backtick" import) deriving (Show, Generic, NFData) @@ -867,7 +866,6 @@ instance (Show name, PPName name) => PP (ModuleInstanceArgs name) where DefaultInstArg x -> braces (pp (thing x)) DefaultInstAnonArg ds -> "where" $$ indent 2 (vcat (map pp ds)) NamedInstArgs xs -> braces (commaSep (map pp xs)) - BacktickInstance -> "{}" instance (Show name, PPName name) => PP (ModuleInstanceNamedArg name) where ppPrec _ (ModuleInstanceNamedArg x y) = pp (thing x) <+> "=" <+> pp (thing y) @@ -876,8 +874,9 @@ instance (Show name, PPName name) => PP (ModuleInstanceNamedArg name) where instance (Show name, PPName name) => PP (ModuleInstanceArg name) where ppPrec _ arg = case arg of - ModuleArg x -> pp x + ModuleArg x -> pp x ParameterArg i -> "parameter" <+> pp i + AddParams -> "{}" instance (Show name, PPName name) => PP (Program name) where @@ -1363,7 +1362,6 @@ instance NoPos (ModuleInstanceArgs name) where DefaultInstArg a -> DefaultInstArg (noPos a) DefaultInstAnonArg ds -> DefaultInstAnonArg (noPos ds) NamedInstArgs xs -> NamedInstArgs (noPos xs) - BacktickInstance -> BacktickInstance instance NoPos (ModuleInstanceNamedArg name) where noPos (ModuleInstanceNamedArg x y) = diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index 565285ac3..84cf2b874 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -155,6 +155,8 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind | FunctorInstanceMissingArgument Ident | FunctorInstanceBadArgument Ident | FunctorInstanceMissingName Namespace Ident + | FunctorInstanceBadBacktickArgument Ident Ident + -- ^ Name of functor argument, name of bad value | UnsupportedFFIKind TypeSource TParam Kind -- ^ Kind is not supported for FFI @@ -191,6 +193,7 @@ errorImportance err = MissingModParam {} -> 10 FunctorInstanceBadArgument {} -> 10 FunctorInstanceMissingName {} -> 9 + FunctorInstanceBadBacktickArgument {} -> 9 KindMismatch {} -> 10 @@ -297,6 +300,7 @@ instance TVars Error where FunctorInstanceMissingArgument {} -> err FunctorInstanceBadArgument {} -> err FunctorInstanceMissingName {} -> err + FunctorInstanceBadBacktickArgument {} -> err UnsupportedFFIKind {} -> err UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e @@ -345,6 +349,7 @@ instance FVS Error where FunctorInstanceMissingArgument {} -> Set.empty FunctorInstanceBadArgument {} -> Set.empty FunctorInstanceMissingName {} -> Set.empty + FunctorInstanceBadBacktickArgument {} -> Set.empty UnsupportedFFIKind {} -> Set.empty UnsupportedFFIType _ t -> fvs t @@ -562,6 +567,15 @@ instance PP (WithNames Error) where NSType -> "type" NSModule -> "module" + FunctorInstanceBadBacktickArgument i x -> + nested "Value parameter may not have a polymorphic type:" $ + vcat + [ "Module parameter:" <+> pp i + , "Value parameter:" <+> pp x + , "When instantiatiating a functor using parameterization," + , "the value parameters need to have a simple type." + ] + UnsupportedFFIKind src param k -> nested "Kind of type variable unsupported for FFI: " $ vcat diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index d6497ab82..8299ee17d 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -1,9 +1,11 @@ {-# Language BlockArguments, ImplicitParams #-} module Cryptol.TypeCheck.Module (doFunctorInst) where +import Data.List(partition) import Data.Text(Text) import Data.Map(Map) import qualified Data.Map as Map +import Data.Set (Set) import qualified Data.Set as Set import Control.Monad(unless,forM_) @@ -40,25 +42,34 @@ doFunctorInst m f as inst doc = inRange (srcRange m) do mf <- lookupFunctor (thing f) argIs <- checkArity (srcRange f) mf as - m2 <- case argIs of - UseArgs ais -> - do (tySus,decls) <- unzip <$> mapM checkArg ais - let ?tSu = mergeDistinctSubst tySus - ?vSu = inst - let m1 = moduleInstance mf - m2 = m1 { mName = m - , mDoc = Nothing - , mParamTypes = mempty - , mParamFuns = mempty - , mParamConstraints = mempty - , mParams = mempty - , mDecls = map NonRecursive (concat decls) ++ - mDecls m1 - } - newGoals CtModuleInstance (map thing (mParamConstraints m1)) - pure m2 - - AddParamsToDecls -> doBacktickInstance m mf inst + m2 <- do as2 <- mapM checkArg argIs + let (tySus,decls) = unzip [ (su,ds) | DefinedInst su ds <- as2 ] + let ?tSu = mergeDistinctSubst tySus + ?vSu = inst + let m1 = moduleInstance mf + m2 = m1 { mName = m + , mDoc = Nothing + , mParamTypes = mempty + , mParamFuns = mempty + , mParamConstraints = mempty + , mParams = mempty + , mDecls = map NonRecursive (concat decls) ++ + mDecls m1 + } + let (tps,tcs,vps) = + unzip3 [ (xs,cs,fs) | ParamInst xs cs fs <- as2 ] + tpSet = Set.unions tps + emit p = Set.null (freeParams p `Set.intersection` tpSet) + + (emitPs,delayPs) = + partition emit (map thing (mParamConstraints m1)) + + newGoals CtModuleInstance emitPs + + doBacktickInstance (Set.toList tpSet) + (delayPs ++ concat tcs) + (Map.unions vps) + m2 case thing m of P.ImpTop mn -> newModuleScope mn (mExports m2) @@ -77,14 +88,11 @@ doFunctorInst m f as inst doc = P.ImpNested {} -> endSubmodule >> pure Nothing - data ActualArg = UseParameter ModParam -- ^ Instantiate using this parameter | UseModule (IfaceG ()) -- ^ Instantiate using this module + | AddDeclParams -- ^ Instantiate by adding parameters -data ActualArgs = - UseArgs [(Range, ModParam, ActualArg)] - | AddParamsToDecls @@ -99,7 +107,7 @@ checkArity :: Range {- ^ Location for reporting errors -} -> ModuleG () {- ^ The functor being instantiated -} -> P.ModuleInstanceArgs Name {- ^ The arguments -} -> - InferM ActualArgs + InferM [(Range, ModParam, ActualArg)] {- ^ Associates functor parameters with the interfaces of the instantiating modules -} checkArity r mf args = @@ -113,8 +121,6 @@ checkArity r mf args = P.NamedInstArgs as -> checkArgs [] ps0 as - P.BacktickInstance -> pure AddParamsToDecls - P.DefaultInstAnonArg {} -> panic "checkArity" [ "DefaultInstAnonArg" ] where ps0 = mParams mf @@ -124,7 +130,7 @@ checkArity r mf args = [] -> do forM_ (Map.keys ps) \p -> recordErrorLoc (Just r) (FunctorInstanceMissingArgument p) - pure (UseArgs done) + pure done P.ModuleInstanceNamedArg ll lm : more -> case Map.lookup (thing ll) ps of @@ -139,6 +145,7 @@ checkArity r mf args = (recordError (MissingModParam p)) pure Nothing Just a -> pure (Just (UseParameter a)) + P.AddParams -> pure (Just AddDeclParams) let next = case arg of Nothing -> done Just a -> (srcRange lm, i, a) : done @@ -150,6 +157,13 @@ checkArity r mf args = checkArgs done ps more +data ArgInst = DefinedInst Subst [Decl] -- ^ Argument that defines the params + | ParamInst (Set TParam) [Prop] (Map Name Type) + -- ^ Argument that add parameters + -- The type parameters are in their module type parameter + -- form (i.e., tpFlav is TPModParam) + + {- | Check the argument to a functor parameter. Returns: @@ -158,31 +172,45 @@ Returns: * Some declarations that define the parameters in terms of the provided values. + + * XXX: Extra parameters for instantiation by adding params -} checkArg :: - (Range, ModParam, ActualArg) -> InferM (Subst, [Decl]) + (Range, ModParam, ActualArg) -> InferM ArgInst checkArg (r,expect,actual') = - do tRens <- mapM (checkParamType r tyMap) (Map.toList (mpnTypes params)) - let renSu = listParamSubst (concat tRens) + case actual' of + AddDeclParams -> paramInst + UseParameter {} -> definedInst + UseModule {} -> definedInst - {- Note: the constraints from the signature are already added to the - constraints for the functor and they are checked all at once in - doFunctorInst -} + where + paramInst = + do let as = Set.fromList (map mtpParam (Map.elems (mpnTypes params))) + cs = map thing (mpnConstraints params) + check = checkSimpleParameterValue r (mpName expect) + fs <- Map.mapMaybeWithKey (\_ v -> v) <$> mapM check (mpnFuns params) + pure (ParamInst as cs fs) + definedInst = + do tRens <- mapM (checkParamType r tyMap) (Map.toList (mpnTypes params)) + let renSu = listParamSubst (concat tRens) - vDecls <- concat <$> - mapM (checkParamValue r vMap) - [ s { mvpType = apSubst renSu (mvpType s) } - | s <- Map.elems (mpnFuns params) ] + {- Note: the constraints from the signature are already added to the + constraints for the functor and they are checked all at once in + doFunctorInst -} - pure (renSu, vDecls) + vDecls <- concat <$> + mapM (checkParamValue r vMap) + [ s { mvpType = apSubst renSu (mvpType s) } + | s <- Map.elems (mpnFuns params) ] + pure (DefinedInst renSu vDecls) - where params = mpParameters expect + -- Things provided by the argument module tyMap :: Map Ident (Kind, Type) vMap :: Map Ident (Name, Schema) (tyMap,vMap) = @@ -209,6 +237,7 @@ checkArg (r,expect,actual') = localNames = ifsPublic (ifNames actual) isLocal x = x `Set.member` localNames + -- Things defined by the argument module decls = filterIfaceDecls isLocal (ifDefines actual) fromD d = (ifDeclName d, ifDeclSig d) @@ -216,6 +245,8 @@ checkArg (r,expect,actual') = fromNewtype nt = (kindOf nt, TNewtype nt []) fromPrimT pt = (kindOf pt, TCon (abstractTypeTC pt) []) + AddDeclParams -> panic "checkArg" ["AddDeclParams"] + nameMapToIdentMap :: (a -> b) -> Map Name a -> Map Ident b @@ -273,6 +304,24 @@ checkParamValue r vMap mp = pure [d] + + +checkSimpleParameterValue :: + Range {- ^ Location for error reporting -} -> + Ident {- ^ Name of functor parameter -} -> + ModVParam {- ^ Module parameter -} -> + InferM (Maybe Type) {- ^ Type to add to things, `Nothing` on err -} +checkSimpleParameterValue r i mp = + case (sVars sch, sProps sch) of + ([],[]) -> pure (Just (sType sch)) + _ -> + do recordErrorLoc (Just r) + (FunctorInstanceBadBacktickArgument i (nameIdent (mvpName mp))) + pure Nothing + where + sch = mvpType mp + + {- | Make an "adaptor" that instantiates the paramter into the form expected by the functor. If the actual type is: diff --git a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs index 463480245..815530281 100644 --- a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs @@ -8,9 +8,12 @@ import qualified Cryptol.Parser.AST as P import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Monad +-- | Rewrite declarations to add the given module parameters. +-- Assumes the renaming due to the instantiation has already happened. doBacktickInstance :: - Located (P.ImpName Name) {- ^ Name for the new module -} -> - ModuleG () {- ^ The functor -} -> - Map Name Name {- ^ The instantiation: functor name -> instance name -} -> - InferM (ModuleG (Located (P.ImpName Name))) -doBacktickInstance m mf inst = undefined + [TParam] -> + [Prop] -> + Map Name Type -> + ModuleG name -> + InferM (ModuleG name) +doBacktickInstance = undefined From 99906b31499c7f294ca4cf79154b6446312f7104 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Fri, 16 Dec 2022 14:56:07 -0800 Subject: [PATCH 04/21] A not very tested implantation of backitick imports The actual backtick syntactic sugar still needs to be implemented, at the moment we use module M = F {_} The plan is that import `F is syntactic sugar for module M = F {_} import M --- src/Cryptol/Parser.y | 2 + src/Cryptol/TypeCheck/AST.hs | 6 +- src/Cryptol/TypeCheck/Error.hs | 51 ++- src/Cryptol/TypeCheck/Module.hs | 5 +- .../TypeCheck/ModuleBacktickInstance.hs | 349 +++++++++++++++++- src/Cryptol/TypeCheck/Monad.hs | 17 +- src/Cryptol/Utils/Ident.hs | 9 + 7 files changed, 412 insertions(+), 27 deletions(-) diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index 85ebe6ce2..ccd7cd453 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -196,6 +196,8 @@ namedModInstParam :: { ModuleInstanceNamedArg PName } modInstParam :: { Located (ModuleInstanceArg PName) } : impName { fmap ModuleArg $1 } | 'interface' ident { fmap ParameterArg $2 } + | '_' { Located { thing = AddParams + , srcRange = $1 } } vmod_body :: { [TopDecl PName] } : vtop_decls { reverse $1 } diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index d4a67b969..81a30075a 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -19,7 +19,7 @@ module Cryptol.TypeCheck.AST , Name() , TFun(..) , Selector(..) - , Import, ImportG(..) + , Import, ImportG(..), ImpName(..) , ImportSpec(..) , ExportType(..) , ExportSpec(..), isExportedBind, isExportedType, isExported @@ -41,7 +41,9 @@ import Cryptol.ModuleSystem.Exports(ExportSpec(..) import Cryptol.Parser.AST ( Selector(..),Pragma(..) , Import , ImportG(..), ImportSpec(..), ExportType(..) - , Fixity(..)) + , Fixity(..) + , ImpName(..) + ) import Cryptol.Utils.RecordMap import Cryptol.TypeCheck.FFI.FFIType import Cryptol.TypeCheck.PP diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index 84cf2b874..124e41a3e 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -155,8 +155,7 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind | FunctorInstanceMissingArgument Ident | FunctorInstanceBadArgument Ident | FunctorInstanceMissingName Namespace Ident - | FunctorInstanceBadBacktickArgument Ident Ident - -- ^ Name of functor argument, name of bad value + | FunctorInstanceBadBacktick BadBacktickInstance | UnsupportedFFIKind TypeSource TParam Kind -- ^ Kind is not supported for FFI @@ -180,6 +179,14 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind -- implementation. deriving (Show, Generic, NFData) +data BadBacktickInstance = + BIPolymorphicArgument Ident Ident + | BINested [(BIWhat, Name)] + deriving (Show, Generic, NFData) + +data BIWhat = BIFunctor | BIInterface | BIPrimitive | BIForeign | BIAbstractType + deriving (Show, Generic, NFData) + -- | When we have multiple errors on the same location, we show only the -- ones with the has highest rating according to this function. errorImportance :: Error -> Int @@ -193,7 +200,7 @@ errorImportance err = MissingModParam {} -> 10 FunctorInstanceBadArgument {} -> 10 FunctorInstanceMissingName {} -> 9 - FunctorInstanceBadBacktickArgument {} -> 9 + FunctorInstanceBadBacktick {} -> 9 KindMismatch {} -> 10 @@ -300,7 +307,7 @@ instance TVars Error where FunctorInstanceMissingArgument {} -> err FunctorInstanceBadArgument {} -> err FunctorInstanceMissingName {} -> err - FunctorInstanceBadBacktickArgument {} -> err + FunctorInstanceBadBacktick {} -> err UnsupportedFFIKind {} -> err UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e @@ -349,7 +356,7 @@ instance FVS Error where FunctorInstanceMissingArgument {} -> Set.empty FunctorInstanceBadArgument {} -> Set.empty FunctorInstanceMissingName {} -> Set.empty - FunctorInstanceBadBacktickArgument {} -> Set.empty + FunctorInstanceBadBacktick {} -> Set.empty UnsupportedFFIKind {} -> Set.empty UnsupportedFFIType _ t -> fvs t @@ -567,14 +574,32 @@ instance PP (WithNames Error) where NSType -> "type" NSModule -> "module" - FunctorInstanceBadBacktickArgument i x -> - nested "Value parameter may not have a polymorphic type:" $ - vcat - [ "Module parameter:" <+> pp i - , "Value parameter:" <+> pp x - , "When instantiatiating a functor using parameterization," - , "the value parameters need to have a simple type." - ] + FunctorInstanceBadBacktick bad -> + case bad of + BIPolymorphicArgument i x -> + nested "Value parameter may not have a polymorphic type:" $ + bullets + [ "Module parameter:" <+> pp i + , "Value parameter:" <+> pp x + , "When instantiatiating a functor using parameterization," + $$ "the value parameters need to have a simple type." + ] + + BINested what -> + nested "Invalid declarations in parameterized instantiation:" $ + bullets $ + [ it <+> pp n + | (w,n) <- what + , let it = case w of + BIFunctor -> "functor" + BIInterface -> "interface" + BIPrimitive -> "primitive" + BIAbstractType -> "abstract type" + BIForeign -> "foreign import" + ] ++ + [ "A functor instantiated using parameterization," $$ + "may not contain nested functors, interfaces, or primitives." + ] UnsupportedFFIKind src param k -> nested "Kind of type variable unsupported for FFI: " $ diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 8299ee17d..8207c53c1 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -30,7 +30,7 @@ import Cryptol.TypeCheck.ModuleBacktickInstance(doBacktickInstance) doFunctorInst :: Located (P.ImpName Name) {- ^ Name for the new module -} -> - Located (P.ImpName Name) {- ^ Functor being instantiation -} -> + Located (P.ImpName Name) {- ^ Functor being instantiated -} -> P.ModuleInstanceArgs Name {- ^ Instance arguments -} -> Map Name Name {- ^ Instantitation. These is the renaming for the functor that arises from @@ -316,7 +316,8 @@ checkSimpleParameterValue r i mp = ([],[]) -> pure (Just (sType sch)) _ -> do recordErrorLoc (Just r) - (FunctorInstanceBadBacktickArgument i (nameIdent (mvpName mp))) + (FunctorInstanceBadBacktick + (BIPolymorphicArgument i (nameIdent (mvpName mp)))) pure Nothing where sch = mvpType mp diff --git a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs index 815530281..6226927ce 100644 --- a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs @@ -1,19 +1,352 @@ +{-# Language ImplicitParams #-} +{-# Language FlexibleInstances #-} +{-# Language RecursiveDo #-} +{-# Language BlockArguments #-} +{-# Language RankNTypes #-} module Cryptol.TypeCheck.ModuleBacktickInstance where import Data.Map(Map) import qualified Data.Map as Map +import MonadLib -import Cryptol.Parser.Position (Located(..), thing) -import qualified Cryptol.Parser.AST as P +import Cryptol.Utils.Ident(ModPath(..), modPathIsOrContains,Namespace(..)) +import Cryptol.Utils.PP(pp) +import Cryptol.Utils.Panic(panic) +import Cryptol.Utils.RecordMap(RecordMap) +import Cryptol.Parser.Position +import Cryptol.ModuleSystem.Name(nameModPath, nameModPathMaybe, nameIdent) import Cryptol.TypeCheck.AST -import Cryptol.TypeCheck.Monad +import Cryptol.TypeCheck.Error +import qualified Cryptol.TypeCheck.Monad as TC --- | Rewrite declarations to add the given module parameters. --- Assumes the renaming due to the instantiation has already happened. +{- | Rewrite declarations to add the given module parameters. +Assumes the renaming due to the instantiation has already happened. +The module being rewritten should not contain any nested functors +(or module with only top-level constraints) because it is not clear +how to parameterize the parameters. +-} doBacktickInstance :: [TParam] -> [Prop] -> Map Name Type -> - ModuleG name -> - InferM (ModuleG name) -doBacktickInstance = undefined + ModuleG (Located (ImpName Name)) -> + TC.InferM (ModuleG (Located (ImpName Name))) +doBacktickInstance as ps mp m + | null as && null ps && Map.null mp = pure m + | otherwise = + runReaderT + RO { isOurs = \x -> case nameModPathMaybe x of + Nothing -> False + Just y -> ourPath `modPathIsOrContains` y + , tparams = as + , constraints = ps + , vparams = Map.toList mp + , newNewtypes = Map.empty + } + + do unless (null bad) + (recordError (FunctorInstanceBadBacktick (BINested bad))) + + rec + ts <- doAddParams nt mTySyns + nt <- doAddParams nt mNewtypes + ds <- doAddParams nt mDecls + + pure m + { mTySyns = ts + , mNewtypes = nt + , mDecls = ds + } + + where + bad = mkBad mFunctors BIFunctor + ++ mkBad mPrimTypes BIAbstractType + ++ mkBad mSignatures BIInterface + + mkBad sel a = [ (a,k) | k <- Map.keys (sel m) ] + + ourPath = case thing (mName m) of + ImpTop mo -> TopModule mo + ImpNested mo -> Nested (nameModPath mo) (nameIdent mo) + + doAddParams nt sel = + mapReader (\ro -> ro { newNewtypes = nt }) (addParams (sel m)) + + +type RewM = ReaderT RO TC.InferM + +recordError :: Error -> RewM () +recordError e = lift (TC.recordError e) + +data RO = RO + { isOurs :: Name -> Bool + , tparams :: [TParam] + , constraints :: [Prop] + , vparams :: [(Name,Type)] + , newNewtypes :: Map Name Newtype + } + + +class AddParams t where + addParams :: t -> RewM t + +instance AddParams a => AddParams (Map Name a) where + addParams = mapM addParams + +instance AddParams a => AddParams [a] where + addParams = mapM addParams + +instance AddParams Newtype where + addParams nt = + do (tps,cs) <- newTypeParams TPNewtypeParam + rProps <- rewTypeM tps (ntConstraints nt) + rFields <- rewTypeM tps (ntFields nt) + pure nt + { ntParams = pDecl tps ++ ntParams nt + , ntConstraints = cs ++ rProps + , ntFields = rFields + } + +instance AddParams TySyn where + addParams ts = + do (tps,cs) <- newTypeParams TPTySynParam + rProps <- rewTypeM tps (tsConstraints ts) + rDef <- rewTypeM tps (tsDef ts) + pure ts + { tsParams = pDecl tps ++ tsParams ts + , tsConstraints = cs ++ rProps + , tsDef = rDef + } + +instance AddParams DeclGroup where + addParams dg = + case dg of + Recursive ds -> Recursive <$> addParams ds + NonRecursive d -> NonRecursive <$> addParams d + +instance AddParams Decl where + addParams d = + case dDefinition d of + DPrim -> bad BIPrimitive + DForeign {} -> bad BIForeign + DExpr e -> + do (tps,cs) <- newTypeParams TPSchemaParam + (vps,bs) <- newValParams tps + let s = dSignature d + + ty1 <- rewTypeM tps (sType s) + let ty2 = foldr tFun ty1 (map snd bs) + + e1 <- rewValM tps (length cs) vps e + let (das,e2) = splitWhile splitTAbs e1 + (dcs,e3) = splitWhile splitProofAbs e2 + e4 = foldr (uncurry EAbs) e3 bs + e5 = foldr EProofAbs e4 (cs ++ dcs) + e6 = foldr ETAbs e5 (pDecl tps ++ das) + + s1 = Forall + { sVars = pDecl tps ++ sVars s + , sProps = cs ++ sProps s + , sType = ty2 + } + + pure d { dDefinition = DExpr e6 + , dSignature = s1 + } + where + bad w = + do recordError (FunctorInstanceBadBacktick (BINested [(w,dName d)])) + pure d + +data Params decl use = Params + { pDecl :: [decl] + , pUse :: [use] + , pSubst :: Map decl use + } + +type TypeParams = Params TParam Type +type ValParams = Params Name Expr + +newTypeParams :: (Name -> TPFlavor) -> RewM (TypeParams,[Prop]) +newTypeParams flav = + do ro <- ask + as <- lift (mapM (TC.freshTParam flav) (tparams ro)) + let ts = map (TVar . TVBound) as + su = Map.fromList (zip (tparams ro) ts) + ps = Params { pDecl = as, pUse = ts, pSubst = su } + cs <- rewTypeM ps (constraints ro) + pure (ps,cs) + +newValParams :: TypeParams -> RewM (ValParams, [(Name,Type)]) +newValParams tps = + do ro <- ask + (xs,ys,ts) <- + unzip3 <$> + forM (vparams ro) \(x,t) -> + do y <- lift (TC.newLocalName NSValue (nameIdent x)) + t1 <- rewTypeM tps t + pure (x,y,t1) + let us = map EVar ys + ps = Params { pDecl = ys + , pUse = us + , pSubst = Map.fromList (zip xs us) + } + pure (ps, zip ys ts) + + +liftRew :: + ((?isOurs :: Name -> Bool, ?newNewtypes :: Map Name Newtype) => a) -> + RewM a +liftRew x = + do ro <- ask + let ?isOurs = isOurs ro + ?newNewtypes = newNewtypes ro + pure x + +rewTypeM :: RewType t => TypeParams -> t -> RewM t +rewTypeM ps x = + do let ?tparams = ps + liftRew rewType <*> pure x + +rewValM :: RewVal t => TypeParams -> Int -> ValParams -> t -> RewM t +rewValM ts cs vs x = + do let ?tparams = ts + ?cparams = cs + ?vparams = vs + liftRew rew <*> pure x + +class RewType t where + rewType :: + ( ?isOurs :: Name -> Bool + , ?newNewtypes :: Map Name Newtype -- Lazy + , ?tparams :: TypeParams + ) => t -> t + +instance RewType Type where + rewType ty = + case ty of + + TCon tc ts + | TC (TCAbstract (UserTC x _)) <- tc + , ?isOurs x -> TCon tc (pUse ?tparams ++ rewType ts) + | otherwise -> TCon tc (rewType ts) + + TVar x -> + case x of + TVBound x' -> + case Map.lookup x' (pSubst ?tparams) of + Just t -> t + Nothing -> ty + TVFree {} -> panic "rawType" ["Free unification variable"] + + TUser f ts t + | ?isOurs f -> TUser f (pUse ?tparams ++ rewType ts) (rewType t) + | otherwise -> TUser f (rewType ts) (rewType t) + + TRec fs -> TRec (rewType fs) + + TNewtype tdef ts + | ?isOurs nm -> TNewtype tdef' (pUse ?tparams ++ rewType ts) + | otherwise -> TNewtype tdef (rewType ts) + where + nm = ntName tdef + tdef' = case Map.lookup nm ?newNewtypes of + Just yes -> yes + Nothing -> panic "rewType" [ "Missing recursive newtype" + , show (pp nm) ] + +instance RewType a => RewType [a] where + rewType = fmap rewType + +instance RewType b => RewType (RecordMap a b) where + rewType = fmap rewType + +instance RewType Schema where + rewType sch = + Forall { sVars = sVars sch + , sProps = rewType (sProps sch) + , sType = rewType (sType sch) + } + + +class RewVal t where + rew :: + ( ?isOurs :: Name -> Bool + , ?newNewtypes :: Map Name Newtype -- Lazy + , ?tparams :: TypeParams + , ?cparams :: Int -- Number of constraitns + , ?vparams :: ValParams + ) => t -> t + +instance RewVal a => RewVal [a] where + rew = fmap rew + +instance RewVal b => RewVal (RecordMap a b) where + rew = fmap rew + +{- x as cs vs --> + e (newAs ++ as) (newCS ++ cs) (newVS ++ vs) +-} +instance RewVal Expr where + rew expr = + case expr of + EList es t -> EList (rew es) (rewType t) + ETuple es -> ETuple (rew es) + ERec fs -> ERec (rew fs) + ESel e l -> ESel (rew e) l + ESet t e1 s e2 -> ESet (rewType t) (rew e1) s (rew e2) + EIf e1 e2 e3 -> EIf (rew e1) (rew e2) (rew e3) + EComp t1 t2 e mss -> EComp (rewType t1) (rewType t2) (rew e) (rew mss) + EVar x -> tryVarApp + case Map.lookup x (pSubst ?vparams) of + Just p -> p + Nothing -> expr + + ETApp e t -> tryVarApp (ETApp (rew e) (rewType t)) + EProofApp e -> tryVarApp (EProofApp (rew e)) + + EApp e1 e2 -> EApp (rew e1) (rew e2) + ETAbs a e -> ETAbs a (rew e) + EAbs x t e -> EAbs x (rewType t) (rew e) + ELocated r e -> ELocated r (rew e) + EProofAbs p e -> EProofAbs (rewType p) (rew e) + EWhere e ds -> EWhere (rew e) (rew ds) + EPropGuards gs t -> EPropGuards gs' (rewType t) + where gs' = [ (rewType <$> p, rew e) | (p,e) <- gs ] + + where + tryVarApp orElse = + case splitExprInst expr of + (EVar x, ts, cs) | ?isOurs x -> + let ets = foldl ETApp (EVar x) (pUse ?tparams ++ rewType ts) + eps = iterate EProofApp ets !! (?cparams + cs) + evs = foldl EApp eps (pUse ?vparams) + in evs + _ -> orElse + + +instance RewVal DeclGroup where + rew dg = + case dg of + Recursive ds -> Recursive (rew ds) + NonRecursive d -> NonRecursive (rew d) + +instance RewVal Decl where + rew d = d { dDefinition = rew (dDefinition d) + , dSignature = rewType (dSignature d) + } + +instance RewVal DeclDef where + rew def = + case def of + DPrim -> def + DForeign {} -> def + DExpr e -> DExpr (rew e) + +instance RewVal Match where + rew ma = + case ma of + From x t1 t2 e -> From x (rewType t1) (rewType t2) (rew e) + Let d -> Let (rew d) + + diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 3c187d9f8..096bab196 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -39,7 +39,7 @@ import Control.DeepSeq import MonadLib hiding (mapM) import Cryptol.ModuleSystem.Name - (FreshM(..),Supply,mkLocal + (FreshM(..),Supply,mkLocal,asLocal , nameInfo, NameInfo(..),NameSource(..), nameTopModule) import qualified Cryptol.ModuleSystem.Interface as If import Cryptol.Parser.Position @@ -605,7 +605,7 @@ checkParamKind :: TParam -> TPFlavor -> Kind -> InferM () checkParamKind tp flav k = case flav of - TPModParam _ -> return () -- All kinds allowed as module parameters + TPModParam _ -> starOrHash TPPropSynParam _ -> starOrHashOrProp TPTySynParam _ -> starOrHash TPSchemaParam _ -> starOrHash @@ -646,6 +646,19 @@ newTParam nm flav k = checkParamKind tp flav k return tp +-- | Generate a new version of a type parameter. We use this when +-- instantiating module parameters (the "backtick" imports) +freshTParam :: (Name -> TPFlavor) -> TParam -> InferM TParam +freshTParam mkF tp = newName \s -> + let u = seedTVar s + in ( tp { tpUnique = u + , tpFlav = case tpName tp of + Just n -> mkF (asLocal NSType n) + Nothing -> tpFlav tp -- shouldn't happen? + } + , s { seedTVar = u + 1 } + ) + -- | Generate an unknown type. The doc is a note about what is this type about. newType :: TypeSource -> Kind -> InferM Type diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs index 9e8b74f5a..808860ab2 100644 --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -15,6 +15,7 @@ module Cryptol.Utils.Ident ModPath(..) , apPathRoot , modPathCommon + , modPathIsOrContains , topModuleFor , modPathSplit , modPathIsNormal @@ -127,6 +128,14 @@ modPathCommon p1 p2 (x:xs',y:ys') | x == y -> findCommon (Nested com x) xs' ys' _ -> (com, xs, ys) +-- | Does the first module path contain the second? +-- This returns true if the paths are the same. +modPathIsOrContains :: ModPath -> ModPath -> Bool +modPathIsOrContains p1 p2 = + case modPathCommon p1 p2 of + Just (_,[],_) -> True + _ -> False + modPathSplit :: ModPath -> (ModName, [Ident]) modPathSplit p0 = (top,reverse xs) where From 3d4f2abd5e5f29c37d539db0681fb08e34006552 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 19 Dec 2022 15:43:13 -0800 Subject: [PATCH 05/21] Have a go at fixing #1483 This is also fixes some longstanding tech debt where we were reusing the name for the type of a newtype and the constructor of a newtype --- src/Cryptol/Eval.hs | 2 +- src/Cryptol/Eval/Concrete.hs | 2 +- src/Cryptol/Eval/Reference.lhs | 2 +- src/Cryptol/IR/TraverseNames.hs | 12 +++++++----- src/Cryptol/ModuleSystem/Binds.hs | 10 ++++------ src/Cryptol/ModuleSystem/Exports.hs | 5 +++-- src/Cryptol/ModuleSystem/NamingEnv.hs | 10 ++++++++-- src/Cryptol/ModuleSystem/Renamer.hs | 9 ++++++--- src/Cryptol/Parser.y | 4 ++-- src/Cryptol/Parser/AST.hs | 17 ++++++++++------- src/Cryptol/Parser/Names.hs | 4 ++++ src/Cryptol/Symbolic.hs | 2 +- src/Cryptol/TypeCheck/Interface.hs | 1 + src/Cryptol/TypeCheck/Kind.hs | 3 ++- src/Cryptol/TypeCheck/ModuleInstance.hs | 2 +- src/Cryptol/TypeCheck/Monad.hs | 11 +++++++---- src/Cryptol/TypeCheck/Type.hs | 1 + 17 files changed, 60 insertions(+), 37 deletions(-) diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index 3553dcb39..5e852b51a 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -319,7 +319,7 @@ evalNewtypeDecl :: Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym) -evalNewtypeDecl _sym nt = pure . bindVarDirect (ntName nt) (foldr tabs con (ntParams nt)) +evalNewtypeDecl _sym nt = pure . bindVarDirect (ntConName nt) (foldr tabs con (ntParams nt)) where con = PFun PPrim diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs index d7fb80e4b..bdb60d79e 100644 --- a/src/Cryptol/Eval/Concrete.hs +++ b/src/Cryptol/Eval/Concrete.hs @@ -87,7 +87,7 @@ toExpr prims t0 v0 = findOne (go t0 v0) case res of Left _ -> mismatch -- different fields Right efs -> - let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntName nt)) ts + let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntConName nt)) ts in pure (EApp f (ERec efs)) (TVTuple ts, VTuple tvs) -> diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index ad56b3d10..e4ea83bc9 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -545,7 +545,7 @@ newtypes is thus basically just an identity function that consumes and ignores its type arguments. > evalNewtypeDecl :: Env -> Newtype -> Env -> evalNewtypeDecl env nt = bindVar (ntName nt, pure val) env +> evalNewtypeDecl env nt = bindVar (ntConName nt, pure val) env > where > val = foldr tabs con (ntParams nt) > con = VFun (\x -> x) diff --git a/src/Cryptol/IR/TraverseNames.hs b/src/Cryptol/IR/TraverseNames.hs index d9c289d29..9f365d0a8 100644 --- a/src/Cryptol/IR/TraverseNames.hs +++ b/src/Cryptol/IR/TraverseNames.hs @@ -209,14 +209,16 @@ instance TraverseNames Newtype where traverseNamesIP nt = mk <$> traverseNamesIP (ntName nt) <*> traverseNamesIP (ntParams nt) <*> traverseNamesIP (ntConstraints nt) + <*> traverseNamesIP (ntConName nt) <*> traverseRecordMap (\_ -> traverseNamesIP) (ntFields nt) where - mk a b c d = nt { ntName = a - , ntParams = b - , ntConstraints = c - , ntFields = d - } + mk a b c d e = nt { ntName = a + , ntParams = b + , ntConstraints = c + , ntConName = d + , ntFields = e + } instance TraverseNames ModTParam where traverseNamesIP nt = mk <$> traverseNamesIP (mtpName nt) diff --git a/src/Cryptol/ModuleSystem/Binds.hs b/src/Cryptol/ModuleSystem/Binds.hs index 80757bb9d..a112e51f2 100644 --- a/src/Cryptol/ModuleSystem/Binds.hs +++ b/src/Cryptol/ModuleSystem/Binds.hs @@ -359,15 +359,13 @@ instance BindsNames (InModule (ParameterType PName)) where ntName <- newTop NSType ns thing Nothing srcRange return (singletonNS NSType thing ntName) --- NOTE: we use the same name at the type and expression level, as there's only --- ever one name introduced in the declaration. The names are only ever used in --- different namespaces, so there's no ambiguity. instance BindsNames (InModule (Newtype PName)) where namingEnv (InModule ~(Just ns) Newtype { .. }) = BuildNamingEnv $ do let Located { .. } = nName - ntName <- newTop NSType ns thing Nothing srcRange - -- XXX: the name reuse here is sketchy - return (singletonNS NSType thing ntName `mappend` singletonNS NSValue thing ntName) + ntName <- newTop NSType ns thing Nothing srcRange + ntConName <- newTop NSValue ns thing Nothing srcRange + return (singletonNS NSType thing ntName `mappend` + singletonNS NSValue thing ntConName) -- | The naming environment for a single declaration. instance BindsNames (InModule (Decl PName)) where diff --git a/src/Cryptol/ModuleSystem/Exports.hs b/src/Cryptol/ModuleSystem/Exports.hs index d35110b64..3e9c01468 100644 --- a/src/Cryptol/ModuleSystem/Exports.hs +++ b/src/Cryptol/ModuleSystem/Exports.hs @@ -11,7 +11,7 @@ import Control.DeepSeq(NFData) import GHC.Generics (Generic) import Cryptol.Parser.AST -import Cryptol.Parser.Names(namesD,tnamesD,tnamesNT) +import Cryptol.Parser.Names(namesD,tnamesD,namesNT,tnamesNT) import Cryptol.ModuleSystem.Name exportedDecls :: Ord name => [TopDecl name] -> ExportSpec name @@ -23,7 +23,8 @@ exportedNames decl = Decl td -> map exportBind (names namesD td) ++ map exportType (names tnamesD td) DPrimType t -> [ exportType (thing . primTName <$> t) ] - TDNewtype nt -> map exportType (names tnamesNT nt) + TDNewtype nt -> map exportType (names tnamesNT nt) ++ + map exportBind (names namesNT nt) Include {} -> [] DImport {} -> [] DParamDecl {} -> [] diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index dc4f931eb..42e41ab47 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -264,8 +264,14 @@ unqualifiedEnv IfaceDecls { .. } = tySyns = mconcat [ singletonNS NSType (toPName n) n | n <- Map.keys ifTySyns ] - ntTypes = mconcat [ singletonNS NSType (toPName n) n - | n <- Map.keys ifNewtypes ] + ntTypes = mconcat [ n + | nt <- Map.elems ifNewtypes + , let tname = T.ntName nt + cname = T.ntConName nt + , n <- [ singletonNS NSType (toPName tname) tname + , singletonNS NSValue (toPName cname) cname + ] + ] absTys = mconcat [ singletonNS NSType (toPName n) n | n <- Map.keys ifAbstractTypes ] diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 013c6051f..87d5d91e1 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -873,11 +873,14 @@ instance Rename Decl where instance Rename Newtype where rename n = shadowNames (nParams n) $ - do name' <- rnLocated (renameType NameBind) (nName n) - depsOf (NamedThing (thing name')) $ + do nameT <- rnLocated (renameType NameBind) (nName n) + nameC <- renameVar NameBind (nConName n) + + depsOf (NamedThing (thing nameT)) $ do ps' <- traverse rename (nParams n) body' <- traverse (traverse rename) (nBody n) - return Newtype { nName = name' + return Newtype { nName = nameT + , nConName = nameC , nParams = ps' , nBody = body' } diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index ccd7cd453..6e5531372 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -467,9 +467,9 @@ propguards_quals :: { [Located (Prop PName)] } newtype :: { Newtype PName } : 'newtype' qname '=' newtype_body - { Newtype $2 [] (thing $4) } + { Newtype $2 [] (thing $2) (thing $4) } | 'newtype' qname tysyn_params '=' newtype_body - { Newtype $2 (reverse $3) (thing $5) } + { Newtype $2 (reverse $3) (thing $2) (thing $5) } newtype_body :: { Located (RecordMap Ident (Range, Type PName)) } : '{' '}' {% mkRecord (rComb $1 $2) (Located emptyRange) [] } diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index fcdd751a6..eeda50662 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -490,10 +490,12 @@ data Pragma = PragmaNote String | PragmaProperty deriving (Eq, Show, Generic, NFData) -data Newtype name = Newtype { nName :: Located name -- ^ Type name - , nParams :: [TParam name] -- ^ Type params - , nBody :: Rec (Type name) -- ^ Body - } deriving (Eq, Show, Generic, NFData) +data Newtype name = Newtype + { nName :: Located name -- ^ Type name + , nParams :: [TParam name] -- ^ Type params + , nConName :: !name -- ^ Constructor function name + , nBody :: Rec (Type name) -- ^ Body + } deriving (Eq, Show, Generic, NFData) -- | A declaration for a type with no implementation. data PrimType name = PrimType { primTName :: Located name @@ -1440,9 +1442,10 @@ instance NoPos (Decl name) where DLocated x _ -> noPos x instance NoPos (Newtype name) where - noPos n = Newtype { nName = noPos (nName n) - , nParams = nParams n - , nBody = fmap noPos (nBody n) + noPos n = Newtype { nName = noPos (nName n) + , nParams = nParams n + , nConName = nConName n + , nBody = fmap noPos (nBody n) } instance NoPos (Bind name) where diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index 64fe28b6d..b20a02dc1 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -20,6 +20,7 @@ module Cryptol.Parser.Names , tnamesD , namesB , namesP + , namesNT , boundNames , boundNamesSet @@ -35,6 +36,9 @@ import qualified Data.Set as Set tnamesNT :: Newtype name -> ([Located name], ()) tnamesNT x = ([ nName x ], ()) +namesNT :: Newtype name -> ([Located name], ()) +namesNT x = ([ (nName x) { thing = nConName x } ], ()) + -- | The names defined and used by a group of mutually recursive declarations. namesDs :: Ord name => [Decl name] -> ([Located name], Set name) namesDs ds = (defs, boundLNames defs (Set.unions frees)) diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs index bc0a5127a..7c02598bc 100644 --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -349,7 +349,7 @@ varToExpr prims = go in case res of Left _ -> mismatch -- different fields Right efs -> - let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntName nt)) ts + let f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar (ntConName nt)) ts in EApp f (ERec efs) (FTRecord tfs, VarRecord vfs) -> diff --git a/src/Cryptol/TypeCheck/Interface.hs b/src/Cryptol/TypeCheck/Interface.hs index 1c9c89684..17538b4cd 100644 --- a/src/Cryptol/TypeCheck/Interface.hs +++ b/src/Cryptol/TypeCheck/Interface.hs @@ -38,6 +38,7 @@ genModDefines m = Set.unions [ Map.keysSet (mTySyns m) , Map.keysSet (mNewtypes m) + , Set.fromList (map ntConName (Map.elems (mNewtypes m))) , Map.keysSet (mPrimTypes m) , Set.fromList (map dName (concatMap groupDecls (mDecls m))) , Map.keysSet (mSubmodules m) diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs index 96cb8d185..1773d03ac 100644 --- a/src/Cryptol/TypeCheck/Kind.hs +++ b/src/Cryptol/TypeCheck/Kind.hs @@ -135,7 +135,7 @@ checkPropSyn (P.PropSyn x _ as ps) mbD = -- | Check a newtype declaration. -- XXX: Do something with constraints. checkNewtype :: P.Newtype Name -> Maybe Text -> InferM Newtype -checkNewtype (P.Newtype x as fs) mbD = +checkNewtype (P.Newtype x as con fs) mbD = do ((as1,fs1),gs) <- collectGoals $ inRange (srcRange x) $ do r <- withTParams NoWildCards newtypeParam as $ @@ -147,6 +147,7 @@ checkNewtype (P.Newtype x as fs) mbD = return Newtype { ntName = thing x , ntParams = as1 , ntConstraints = map goal gs + , ntConName = con , ntFields = fs1 , ntDoc = mbD } diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index 518cbeef8..ea6e2d098 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -9,7 +9,6 @@ import qualified Data.Set as Set import Cryptol.Parser.Position(Located) import Cryptol.ModuleSystem.Interface(IfaceNames(..)) import Cryptol.IR.TraverseNames(TraverseNames,mapNames) -import Cryptol.Parser.AST(ImpName(..)) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Subst(Subst,TVars,apSubst) @@ -97,6 +96,7 @@ instance ModuleInstance Newtype where Newtype { ntName = moduleInstance (ntName nt) , ntParams = ntParams nt , ntConstraints = moduleInstance (ntConstraints nt) + , ntConName = moduleInstance (ntConName nt) , ntFields = moduleInstance <$> ntFields nt , ntDoc = ntDoc nt } diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 096bab196..b8114e644 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -56,7 +56,7 @@ import Cryptol.TypeCheck.Error( Warning(..),Error(..) import qualified Cryptol.TypeCheck.SimpleSolver as Simple import qualified Cryptol.TypeCheck.Solver.SMT as SMT import Cryptol.TypeCheck.PP(NameMap) -import Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets) +import Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets,debugShowUniques) import Cryptol.Utils.Ident(Ident,Namespace(..),ModName) import Cryptol.Utils.Panic(panic) @@ -129,7 +129,10 @@ runInferM info m0 = let allPs = inpParams info let env = Map.map ExtVar (inpVars info) - <> Map.map (ExtVar . newtypeConType) (inpNewtypes info) + <> Map.fromList + [ (ntConName nt, ExtVar (newtypeConType nt)) + | nt <- Map.elems (inpNewtypes info) + ] <> Map.map (ExtVar . mvpType) (mpnFuns allPs) let ro = RO { iRange = inpRange info @@ -774,7 +777,7 @@ lookupVar x = panic "lookupVar" $ [ "Undefined vairable" , show x , "IVARS" - ] ++ map (show . pp) (Map.keys mp) + ] ++ map (show . debugShowUniques . pp) (Map.keys mp) -- | Lookup a type variable. Return `Nothing` if there is no such variable -- in scope, in which case we must be dealing with a type constant. @@ -1150,7 +1153,7 @@ addTySyn t = addNewtype :: Newtype -> InferM () addNewtype t = do updScope \r -> r { mNewtypes = Map.insert (ntName t) t (mNewtypes r) } - IM $ sets_ \rw -> rw { iBindTypes = Map.insert (ntName t) + IM $ sets_ \rw -> rw { iBindTypes = Map.insert (ntConName t) (newtypeConType t) (iBindTypes rw) } diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index 417e341a8..691ea5f8a 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -315,6 +315,7 @@ data TySyn = TySyn { tsName :: Name -- ^ Name data Newtype = Newtype { ntName :: Name , ntParams :: [TParam] , ntConstraints :: [Prop] + , ntConName :: !Name , ntFields :: RecordMap Ident Type , ntDoc :: Maybe Text } deriving (Show, Generic, NFData) From e0d595289a189e77b0fd722b2966e43b0f77e694 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 20 Dec 2022 09:55:14 -0800 Subject: [PATCH 06/21] Add some tests --- tests/modsys/functors/T035.cry | 23 +++++++++++++++++++++++ tests/modsys/functors/T035.icry | 1 + tests/modsys/functors/T035.icry.stdout | 15 +++++++++++++++ tests/modsys/functors/T036.cry | 6 ++++++ tests/modsys/functors/T036.icry | 3 +++ tests/modsys/functors/T036.icry.stdout | 9 +++++++++ tests/modsys/functors/T036_A.cry | 8 ++++++++ tests/modsys/functors/T036_B.cry | 2 ++ 8 files changed, 67 insertions(+) create mode 100644 tests/modsys/functors/T035.cry create mode 100644 tests/modsys/functors/T035.icry create mode 100644 tests/modsys/functors/T035.icry.stdout create mode 100644 tests/modsys/functors/T036.cry create mode 100644 tests/modsys/functors/T036.icry create mode 100644 tests/modsys/functors/T036.icry.stdout create mode 100644 tests/modsys/functors/T036_A.cry create mode 100644 tests/modsys/functors/T036_B.cry diff --git a/tests/modsys/functors/T035.cry b/tests/modsys/functors/T035.cry new file mode 100644 index 000000000..cbd4ae84f --- /dev/null +++ b/tests/modsys/functors/T035.cry @@ -0,0 +1,23 @@ + +submodule A where + newtype T = { x : Integer } + +submodule F where + parameter + type n : # + type constraint (fin n) + + newtype X = { x : [n] } + f : X -> X + f x = x + +submodule M = submodule F { _ } +submodule N = submodule F { _ } + +import submodule M as M +import submodule N as N + +// This is a type error because currently F's instantiation is generative +// If we make it applicative, then we should change this test +x = M::f (N::X { x = 0 }) + diff --git a/tests/modsys/functors/T035.icry b/tests/modsys/functors/T035.icry new file mode 100644 index 000000000..32a88f35e --- /dev/null +++ b/tests/modsys/functors/T035.icry @@ -0,0 +1 @@ +:load T035.cry diff --git a/tests/modsys/functors/T035.icry.stdout b/tests/modsys/functors/T035.icry.stdout new file mode 100644 index 000000000..1c73a1303 --- /dev/null +++ b/tests/modsys/functors/T035.icry.stdout @@ -0,0 +1,15 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +[warning] at T035.cry:12:5--12:6 + This binding for `x` shadows the existing binding at + T035.cry:22:1--22:2 + +[error] at T035.cry:22:11--22:15: + Type mismatch: + Expected type: Main::M::X ?m + Inferred type: Main::N::X 0 + Context: _ -> ERROR + When checking function call + where + ?m is type argument 'n' of 'Main::M::f' at T035.cry:22:5--22:9 diff --git a/tests/modsys/functors/T036.cry b/tests/modsys/functors/T036.cry new file mode 100644 index 000000000..90e2a44e2 --- /dev/null +++ b/tests/modsys/functors/T036.cry @@ -0,0 +1,6 @@ +module T036 where + +import T036_B + +x = T { x = 0 } + diff --git a/tests/modsys/functors/T036.icry b/tests/modsys/functors/T036.icry new file mode 100644 index 000000000..fd1bd35be --- /dev/null +++ b/tests/modsys/functors/T036.icry @@ -0,0 +1,3 @@ +:load T036.cry +x + diff --git a/tests/modsys/functors/T036.icry.stdout b/tests/modsys/functors/T036.icry.stdout new file mode 100644 index 000000000..4d84d0830 --- /dev/null +++ b/tests/modsys/functors/T036.icry.stdout @@ -0,0 +1,9 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module `parameter` interface of T036_A +Loading module T036_A +Loading module T036_B +Loading module T036 +Showing a specific instance of polymorphic result: + * Using '0' for type argument 'n' of 'T036_B::T' +{x = 0x0} diff --git a/tests/modsys/functors/T036_A.cry b/tests/modsys/functors/T036_A.cry new file mode 100644 index 000000000..f0e833d24 --- /dev/null +++ b/tests/modsys/functors/T036_A.cry @@ -0,0 +1,8 @@ +module T036_A where + parameter + type n : # + type constraint (fin n) + + newtype T = { x : [n] } + + diff --git a/tests/modsys/functors/T036_B.cry b/tests/modsys/functors/T036_B.cry new file mode 100644 index 000000000..25c0a06ae --- /dev/null +++ b/tests/modsys/functors/T036_B.cry @@ -0,0 +1,2 @@ +module T036_B = T036_A { _ } + From bf9995377f0434b04be912fd7cc83de61487854a Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 20 Dec 2022 14:31:32 -0800 Subject: [PATCH 07/21] Fixes #1484 --- src/Cryptol/TypeCheck/Monad.hs | 40 +++++++++++++++++++++----- tests/modsys/functors/T037.cry | 19 ++++++++++++ tests/modsys/functors/T037.icry | 2 ++ tests/modsys/functors/T037.icry.stdout | 4 +++ 4 files changed, 58 insertions(+), 7 deletions(-) create mode 100644 tests/modsys/functors/T037.cry create mode 100644 tests/modsys/functors/T037.icry create mode 100644 tests/modsys/functors/T037.icry.stdout diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index b8114e644..33f108831 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -857,7 +857,7 @@ lookupModule iname = do localMods <- getScope mSubmodules case Map.lookup m localMods of Just names -> - do n <- genIfaceWithNames names <$> getCurScope + do n <- genIfaceWithNames names <$> getCurDecls pure (If.ifaceForgetName n) Nothing -> @@ -1128,12 +1128,38 @@ getScope f = rw <- IM get pure (sconcat (f (iExtScope ro) :| map f (iScope rw))) -getCurScope :: InferM (ModuleG ScopeName) -getCurScope = - do rw <- IM get - case iScope rw of - m : _ -> pure m - [] -> panic "getCurScope" ["No current scope."] +getCurDecls :: InferM (ModuleG ()) +getCurDecls = + do ro <- IM ask + rw <- IM get + pure (foldr (\m1 m2 -> mergeDecls (forget m1) m2) + (forget (iExtScope ro)) (iScope rw)) + + where + forget m = m { mName = () } + + mergeDecls m1 m2 = + Module + { mName = () + , mDoc = Nothing + , mExports = mempty + , mParams = mempty + , mParamTypes = mempty + , mParamConstraints = mempty + , mParamFuns = mempty + , mNested = mempty + + , mTySyns = uni mTySyns + , mNewtypes = uni mNewtypes + , mPrimTypes = uni mPrimTypes + , mDecls = uni mDecls + , mSubmodules = uni mSubmodules + , mFunctors = uni mFunctors + , mSignatures = uni mSignatures + } + where + uni f = f m1 <> f m2 + addDecls :: DeclGroup -> InferM () addDecls ds = diff --git a/tests/modsys/functors/T037.cry b/tests/modsys/functors/T037.cry new file mode 100644 index 000000000..29e55c2f8 --- /dev/null +++ b/tests/modsys/functors/T037.cry @@ -0,0 +1,19 @@ +module T037 where + +interface submodule I where + x : [8] + +submodule F where + import interface submodule I + y = x + 1 + +submodule P where + x = 11 + +submodule X where + submodule M = submodule F { submodule P } + import submodule M + + z = y + +import submodule X diff --git a/tests/modsys/functors/T037.icry b/tests/modsys/functors/T037.icry new file mode 100644 index 000000000..55047c14f --- /dev/null +++ b/tests/modsys/functors/T037.icry @@ -0,0 +1,2 @@ +:load T037.cry +z diff --git a/tests/modsys/functors/T037.icry.stdout b/tests/modsys/functors/T037.icry.stdout new file mode 100644 index 000000000..57806c2c7 --- /dev/null +++ b/tests/modsys/functors/T037.icry.stdout @@ -0,0 +1,4 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T037 +0x0c From b3a0858cb50198ad663d2f08aafce78633f5820a Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 20 Dec 2022 14:32:50 -0800 Subject: [PATCH 08/21] Remove a bunch of SAFE annotation. These don't really check anything --- src/Cryptol/TypeCheck/Infer.hs | 2 -- src/Cryptol/TypeCheck/Instantiate.hs | 1 - src/Cryptol/TypeCheck/Kind.hs | 1 - src/Cryptol/TypeCheck/Monad.hs | 1 - src/Cryptol/TypeCheck/Solve.hs | 1 - src/Cryptol/TypeCheck/Solver/Selector.hs | 2 +- 6 files changed, 1 insertion(+), 7 deletions(-) diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 50b82b668..a4b8eef42 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -14,8 +14,6 @@ {-# LANGUAGE RecursiveDo #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE BlockArguments #-} -{-# LANGUAGE Safe #-} --- {-# LANGUAGE Trustworthy #-} -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {-# LANGUAGE LambdaCase #-} diff --git a/src/Cryptol/TypeCheck/Instantiate.hs b/src/Cryptol/TypeCheck/Instantiate.hs index 1acb477e1..0a8b17bff 100644 --- a/src/Cryptol/TypeCheck/Instantiate.hs +++ b/src/Cryptol/TypeCheck/Instantiate.hs @@ -6,7 +6,6 @@ -- Stability : provisional -- Portability : portable {-# Language OverloadedStrings #-} -{-# Language Safe #-} module Cryptol.TypeCheck.Instantiate ( instantiateWith , TypeArg(..) diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs index 1773d03ac..72f1d19c2 100644 --- a/src/Cryptol/TypeCheck/Kind.hs +++ b/src/Cryptol/TypeCheck/Kind.hs @@ -8,7 +8,6 @@ {-# LANGUAGE RecursiveDo #-} {-# LANGUAGE BlockArguments #-} -{-# LANGUAGE Safe #-} -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.TypeCheck.Kind diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 33f108831..5dfb3ac80 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -5,7 +5,6 @@ -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable -{-# LANGUAGE Safe #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs index fb9987f0c..c777082e0 100644 --- a/src/Cryptol/TypeCheck/Solve.hs +++ b/src/Cryptol/TypeCheck/Solve.hs @@ -7,7 +7,6 @@ -- Portability : portable {-# LANGUAGE PatternGuards, BangPatterns, RecordWildCards #-} -{-# LANGUAGE Safe #-} module Cryptol.TypeCheck.Solve ( simplifyAllConstraints , proveImplication diff --git a/src/Cryptol/TypeCheck/Solver/Selector.hs b/src/Cryptol/TypeCheck/Solver/Selector.hs index 1677f05a4..60fc9fca2 100644 --- a/src/Cryptol/TypeCheck/Solver/Selector.hs +++ b/src/Cryptol/TypeCheck/Solver/Selector.hs @@ -5,7 +5,7 @@ -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable -{-# LANGUAGE PatternGuards, Safe #-} +{-# LANGUAGE PatternGuards #-} module Cryptol.TypeCheck.Solver.Selector (tryHasGoal) where import Cryptol.Parser.Position(Range) From cfa6d8f89e768b5dcc4ff81990b6080f4a6c6854 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 20 Dec 2022 14:54:39 -0800 Subject: [PATCH 09/21] Debugging code to dump parsed AST --- src/Cryptol/ModuleSystem/Base.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 3b382fa05..6fe2ae077 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -194,6 +194,11 @@ parseModule path = do case as it would help guide the design. -} InMem {} -> pure (pms, Set.empty) +--{- + case path of + InFile {} -> io $ print (T.vcat (map T.pp pm1)) + InMem {} -> pure () +--} fp `seq` return (fp, deps, pm1) Left err -> moduleParseError path err From f36dbb465e1c9c41521ba13bdfec00661e1911b9 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 20 Dec 2022 15:20:01 -0800 Subject: [PATCH 10/21] Disallow direct functor instantiation in interfaces. The reason for this is that we don't have anywhere to place the generated module---we could put it outside the interface, but that wont' work if the instantiation used an imported module, and it would be inconsistent with how other such imports work. Instead, users need to make the substantiation manually outside the interface. Fixes #1485 --- src/Cryptol/Parser.y | 6 ++-- src/Cryptol/Parser/ParserUtils.hs | 40 +++++++++++++++++++------- tests/modsys/functors/T038.cry | 21 ++++++++++++++ tests/modsys/functors/T038.icry | 1 + tests/modsys/functors/T038.icry.stdout | 6 ++++ 5 files changed, 61 insertions(+), 13 deletions(-) create mode 100644 tests/modsys/functors/T038.cry create mode 100644 tests/modsys/functors/T038.icry create mode 100644 tests/modsys/functors/T038.icry.stdout diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index 6e5531372..d9ff88433 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -297,9 +297,9 @@ sig_def :: { (Located PName, Signature PName) } { ($3, $6) } sig_body :: { Signature PName } - : par_decls { mkInterface [] $1 } - | imports1 'v;' par_decls { mkInterface (reverse $1) $3 } - | imports1 ';' par_decls { mkInterface (reverse $1) $3 } + : par_decls {% mkInterface [] $1 } + | imports1 'v;' par_decls {% mkInterface (reverse $1) $3 } + | imports1 ';' par_decls {% mkInterface (reverse $1) $3 } mod_param_decl :: { ModParam PName } diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index 44bccb720..679bd0487 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -909,20 +909,32 @@ mkInterfaceConstraint mbDoc ty = pure [DInterfaceConstraint (thing <$> mbDoc) ps] mkParDecls :: [ParamDecl PName] -> TopDecl PName -mkParDecls ds = DParamDecl loc (mkInterface [] ds) +mkParDecls ds = DParamDecl loc (mkInterface' [] ds) where loc = rCombs (mapMaybe getLoc ds) -mkInterface :: [Located (ImportG (ImpName PName))] -> +onlySimpleImports :: [Located (ImportG (ImpName PName))] -> ParseM () +onlySimpleImports = mapM_ check + where + check i = + case iInst (thing i) of + Nothing -> pure () + Just _ -> + errorMessage (srcRange i) + [ "Functor instantiations are not supported in this context." + , "The imported entity needs to be just the name of a module." + , "A workaround would be to do the instantion in the outer context." + ] + +mkInterface' :: [Located (ImportG (ImpName PName))] -> [ParamDecl PName] -> Signature PName -mkInterface is = +mkInterface' is = foldl' add - Signature { sigImports = is - , sigTypeParams = [] - , sigDecls = [] - , sigConstraints = [] - , sigFunParams = [] - } - + Signature { sigImports = is + , sigTypeParams = [] + , sigDecls = [] + , sigConstraints = [] + , sigFunParams = [] + } where add s d = case d of @@ -931,6 +943,14 @@ mkInterface is = DParameterDecl pd -> s { sigDecls = pd : sigDecls s } DParameterFun pf -> s { sigFunParams = pf : sigFunParams s } + + +mkInterface :: [Located (ImportG (ImpName PName))] -> + [ParamDecl PName] -> ParseM (Signature PName) +mkInterface is ps = + do onlySimpleImports is + pure (mkInterface' is ps) + mkIfacePropSyn :: Maybe Text -> Decl PName -> ParamDecl PName mkIfacePropSyn mbDoc d = case d of diff --git a/tests/modsys/functors/T038.cry b/tests/modsys/functors/T038.cry new file mode 100644 index 000000000..3573394d1 --- /dev/null +++ b/tests/modsys/functors/T038.cry @@ -0,0 +1,21 @@ +module T038 where + +interface submodule I where + x : [8] + +submodule F where + import interface submodule I + y = x + 1 + +submodule P where + import submodule F { submodule Q } + x = 11 + +submodule Q where + x = 11 + +interface submodule J where + import submodule F { submodule P } + x : [8] + + diff --git a/tests/modsys/functors/T038.icry b/tests/modsys/functors/T038.icry new file mode 100644 index 000000000..4aa0579f5 --- /dev/null +++ b/tests/modsys/functors/T038.icry @@ -0,0 +1 @@ +:load T038.cry diff --git a/tests/modsys/functors/T038.icry.stdout b/tests/modsys/functors/T038.icry.stdout new file mode 100644 index 000000000..7a4c28fb0 --- /dev/null +++ b/tests/modsys/functors/T038.icry.stdout @@ -0,0 +1,6 @@ +Loading module Cryptol + +Parse error at T038.cry:18:3--18:21 + Functor instantiations are not supported in this context. + The imported entity needs to be just the name of a module. + A workaround would be to do the instantion in the outer context. From 4b70911e1aa02034b7d52800ce266c6023bf10e5 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 20 Dec 2022 15:53:10 -0800 Subject: [PATCH 11/21] Remove debugging stuff --- src/Cryptol/ModuleSystem/Base.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 6fe2ae077..3e8c08b15 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -194,7 +194,7 @@ parseModule path = do case as it would help guide the design. -} InMem {} -> pure (pms, Set.empty) ---{- +{- case path of InFile {} -> io $ print (T.vcat (map T.pp pm1)) InMem {} -> pure () From 7f7fc61ea21075df54c030159fd254c4b18767a2 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 20 Dec 2022 15:54:08 -0800 Subject: [PATCH 12/21] Syntactic sugar to support backtick imports --- src/Cryptol/Parser.y | 10 ++++++++-- src/Cryptol/Parser/ParserUtils.hs | 11 +++++++++++ tests/modsys/functors/T039.cry | 9 +++++++++ tests/modsys/functors/T039.icry | 3 +++ tests/modsys/functors/T039.icry.stdout | 4 ++++ 5 files changed, 35 insertions(+), 2 deletions(-) create mode 100644 tests/modsys/functors/T039.cry create mode 100644 tests/modsys/functors/T039.icry create mode 100644 tests/modsys/functors/T039.icry.stdout diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index d9ff88433..6dacba61f 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -215,6 +215,7 @@ imports1 :: { [ Located (ImportG (ImpName PName)) ] } import :: { Located (ImportG (ImpName PName)) } : 'import' impName optInst mbAs mbImportSpec optImportWhere {% mkImport $1 $2 $3 $4 $5 $6 } + | 'import' impNameBT mbAs mbImportSpec {% mkBacktickImport $1 $2 $3 $4 } optImportWhere :: { Maybe (Located [Decl PName]) } : 'where' whereClause { Just $2 } @@ -224,10 +225,17 @@ optInst :: { Maybe (ModuleInstanceArgs PName) } : '{' modInstParams '}' { Just $2 } | {- empty -} { Nothing } + impName :: { Located (ImpName PName) } : 'submodule' qname { ImpNested `fmap` $2 } | modName { ImpTop `fmap` $1 } +impNameBT :: { Located (ImpName PName) } + : 'submodule' '`' qname { ImpNested `fmap` $3 } + | '`' modName { ImpTop `fmap` $2 } + + + mbAs :: { Maybe (Located ModName) } : 'as' modName { Just $2 } @@ -880,8 +888,6 @@ smodName :: { Located ModName } modName :: { Located ModName } : smodName { $1 } | 'module' smodName { $2 } - | '`' smodName {% errorMessage $1 ["Backtick module imports are no longer supported."] } - qname :: { Located PName } : name { $1 } diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index 679bd0487..4cf70eb2d 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -1040,6 +1040,17 @@ mkSelector tok = Selector (RecordSelectorTok t) -> RecordSel (mkIdent t) Nothing _ -> panic "mkSelector" [ "Unexpected selector token", show tok ] +mkBacktickImport :: + Range -> + Located (ImpName PName) -> + Maybe (Located ModName) -> + Maybe (Located ImportSpec) -> + ParseM (Located (ImportG (ImpName PName))) +mkBacktickImport loc impName mbAs mbImportSpec = + mkImport loc impName (Just inst) mbAs mbImportSpec Nothing + where + inst = DefaultInstArg (fmap (const AddParams) impName) + mkImport :: Range -> diff --git a/tests/modsys/functors/T039.cry b/tests/modsys/functors/T039.cry new file mode 100644 index 000000000..0061e033e --- /dev/null +++ b/tests/modsys/functors/T039.cry @@ -0,0 +1,9 @@ +module T039 where + +submodule F where + parameter + x : [8] + y = x + 1 + +import submodule `F + diff --git a/tests/modsys/functors/T039.icry b/tests/modsys/functors/T039.icry new file mode 100644 index 000000000..38bf3f5e3 --- /dev/null +++ b/tests/modsys/functors/T039.icry @@ -0,0 +1,3 @@ +:load T039.cry +:t y + diff --git a/tests/modsys/functors/T039.icry.stdout b/tests/modsys/functors/T039.icry.stdout new file mode 100644 index 000000000..78c8d4c7e --- /dev/null +++ b/tests/modsys/functors/T039.icry.stdout @@ -0,0 +1,4 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T039 +y : [8] -> [8] From 40149dc3da7d6132c402195a18d2f0543e6b3061 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 21 Dec 2022 10:13:52 -0800 Subject: [PATCH 13/21] During backtick instantiation pass all value parameters in a record This is how the system used to work. This commit also restores some of the old tests. --- src/Cryptol/TypeCheck/Error.hs | 8 +++ .../TypeCheck/ModuleBacktickInstance.hs | 57 +++++++++++++------ tests/issues/issue565.icry.stdout | 8 ++- tests/modsys/T11.icry | 1 + tests/modsys/T11.icry.stdout | 5 ++ tests/modsys/T11/A.cry | 12 ++++ tests/modsys/T11/Main.cry | 9 +++ tests/modsys/T9.icry | 3 + tests/modsys/T9.icry.stdout | 7 +++ tests/modsys/T9/A.cry | 10 ++++ tests/modsys/T9/Main.cry | 7 +++ tests/modsys/functors/T039.icry.stdout | 2 +- 12 files changed, 110 insertions(+), 19 deletions(-) create mode 100644 tests/modsys/T11.icry create mode 100644 tests/modsys/T11.icry.stdout create mode 100644 tests/modsys/T11/A.cry create mode 100644 tests/modsys/T11/Main.cry create mode 100644 tests/modsys/T9.icry create mode 100644 tests/modsys/T9.icry.stdout create mode 100644 tests/modsys/T9/A.cry create mode 100644 tests/modsys/T9/Main.cry diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index 124e41a3e..e46df4864 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -182,6 +182,7 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind data BadBacktickInstance = BIPolymorphicArgument Ident Ident | BINested [(BIWhat, Name)] + | BIMultipleParams Ident deriving (Show, Generic, NFData) data BIWhat = BIFunctor | BIInterface | BIPrimitive | BIForeign | BIAbstractType @@ -600,6 +601,13 @@ instance PP (WithNames Error) where [ "A functor instantiated using parameterization," $$ "may not contain nested functors, interfaces, or primitives." ] + BIMultipleParams x -> + nested "Repeated parameter name in parameterized instantiation:" $ + bullets + [ "Parameter name:" <+> pp x + , "Parameterized instantiation requires distinct parameter names" + ] + UnsupportedFFIKind src param k -> nested "Kind of type variable unsupported for FFI: " $ diff --git a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs index 6226927ce..d3faed8f0 100644 --- a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs @@ -3,16 +3,18 @@ {-# Language RecursiveDo #-} {-# Language BlockArguments #-} {-# Language RankNTypes #-} +{-# Language OverloadedStrings #-} module Cryptol.TypeCheck.ModuleBacktickInstance where import Data.Map(Map) import qualified Data.Map as Map import MonadLib -import Cryptol.Utils.Ident(ModPath(..), modPathIsOrContains,Namespace(..)) +import Cryptol.Utils.Ident(ModPath(..), modPathIsOrContains,Namespace(..), + mkIdent) import Cryptol.Utils.PP(pp) import Cryptol.Utils.Panic(panic) -import Cryptol.Utils.RecordMap(RecordMap) +import Cryptol.Utils.RecordMap(RecordMap,recordFromFields,recordFromFieldsErr) import Cryptol.Parser.Position import Cryptol.ModuleSystem.Name(nameModPath, nameModPathMaybe, nameIdent) import Cryptol.TypeCheck.AST @@ -40,7 +42,7 @@ doBacktickInstance as ps mp m Just y -> ourPath `modPathIsOrContains` y , tparams = as , constraints = ps - , vparams = Map.toList mp + , vparams = mp , newNewtypes = Map.empty } @@ -82,7 +84,7 @@ data RO = RO { isOurs :: Name -> Bool , tparams :: [TParam] , constraints :: [Prop] - , vparams :: [(Name,Type)] + , vparams :: Map Name Type , newNewtypes :: Map Name Newtype } @@ -164,6 +166,13 @@ data Params decl use = Params , pSubst :: Map decl use } +noParams :: Params decl use +noParams = Params + { pDecl = [] + , pUse = [] + , pSubst = Map.empty + } + type TypeParams = Params TParam Type type ValParams = Params Name Expr @@ -177,22 +186,38 @@ newTypeParams flav = cs <- rewTypeM ps (constraints ro) pure (ps,cs) +-- Note: we pass all value parameters as a record newValParams :: TypeParams -> RewM (ValParams, [(Name,Type)]) newValParams tps = do ro <- ask - (xs,ys,ts) <- - unzip3 <$> - forM (vparams ro) \(x,t) -> - do y <- lift (TC.newLocalName NSValue (nameIdent x)) - t1 <- rewTypeM tps t - pure (x,y,t1) - let us = map EVar ys - ps = Params { pDecl = ys - , pUse = us - , pSubst = Map.fromList (zip xs us) + let vps = vparams ro + if Map.null vps + then pure (noParams, []) + else do xts <- forM (Map.toList vps) \(x,t) -> + do t1 <- rewTypeM tps t + pure (x,t1) + let (xs,ts) = unzip xts + ls = map nameIdent xs + fs = zip ls ts + sel x = RecordSel (nameIdent x) (Just ls) + + t <- case recordFromFieldsErr fs of + Right ok -> pure (TRec ok) + Left (x,_) -> + do recordError (FunctorInstanceBadBacktick + (BIMultipleParams x)) + pure (TRec (recordFromFields fs)) + + r <- lift (TC.newLocalName NSValue (mkIdent "params")) + let e = EVar r + pure + ( Params + { pDecl = [r] + , pUse = [e] + , pSubst = Map.fromList [ (x,ESel e (sel x)) | x <- xs ] } - pure (ps, zip ys ts) - + , [ (r,t) ] + ) liftRew :: ((?isOurs :: Name -> Bool, ?newNewtypes :: Map Name Newtype) => a) -> diff --git a/tests/issues/issue565.icry.stdout b/tests/issues/issue565.icry.stdout index 3fbacd08a..8b0d09529 100644 --- a/tests/issues/issue565.icry.stdout +++ b/tests/issues/issue565.icry.stdout @@ -1,4 +1,8 @@ Loading module Cryptol +Loading module Cryptol +Loading module T +Loading module I -Parse error at issue565/I.cry:3:8--3:9 - Backtick module imports are no longer supported. +[error] at issue565/I.cry:3:1--3:10 + • Expected a functor + • `T` is a module diff --git a/tests/modsys/T11.icry b/tests/modsys/T11.icry new file mode 100644 index 000000000..c1d02e79d --- /dev/null +++ b/tests/modsys/T11.icry @@ -0,0 +1 @@ +:module T11::Main diff --git a/tests/modsys/T11.icry.stdout b/tests/modsys/T11.icry.stdout new file mode 100644 index 000000000..84ed2cac6 --- /dev/null +++ b/tests/modsys/T11.icry.stdout @@ -0,0 +1,5 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module `parameter` interface of T11::A +Loading module T11::A +Loading module T11::Main diff --git a/tests/modsys/T11/A.cry b/tests/modsys/T11/A.cry new file mode 100644 index 000000000..b64c1773d --- /dev/null +++ b/tests/modsys/T11/A.cry @@ -0,0 +1,12 @@ +module T11::A where + +parameter + type X : # + type Y : # + +type T = ([X],[Y]) + +f : T -> [X] +f (x,_) = x + + diff --git a/tests/modsys/T11/Main.cry b/tests/modsys/T11/Main.cry new file mode 100644 index 000000000..a3e3b2361 --- /dev/null +++ b/tests/modsys/T11/Main.cry @@ -0,0 +1,9 @@ +module T11::Main where + +import `T11::A as X + + +f : X::T 1 2 -> [1] +f = X::f + + diff --git a/tests/modsys/T9.icry b/tests/modsys/T9.icry new file mode 100644 index 000000000..fc0bfd618 --- /dev/null +++ b/tests/modsys/T9.icry @@ -0,0 +1,3 @@ +:module T9::Main +:t main +main diff --git a/tests/modsys/T9.icry.stdout b/tests/modsys/T9.icry.stdout new file mode 100644 index 000000000..86d7a6926 --- /dev/null +++ b/tests/modsys/T9.icry.stdout @@ -0,0 +1,7 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module `parameter` interface of T9::A +Loading module T9::A +Loading module T9::Main +main : [16] +0x1010 diff --git a/tests/modsys/T9/A.cry b/tests/modsys/T9/A.cry new file mode 100644 index 000000000..6991df41d --- /dev/null +++ b/tests/modsys/T9/A.cry @@ -0,0 +1,10 @@ +module T9::A where + +parameter + type n : # + type constraint (fin n) + x : [n] + +f : [n+n] +f = x # x + diff --git a/tests/modsys/T9/Main.cry b/tests/modsys/T9/Main.cry new file mode 100644 index 000000000..3cd1ecaa0 --- /dev/null +++ b/tests/modsys/T9/Main.cry @@ -0,0 +1,7 @@ +module T9::Main where + +import `T9::A + +main = f { x = 0x10 } + + diff --git a/tests/modsys/functors/T039.icry.stdout b/tests/modsys/functors/T039.icry.stdout index 78c8d4c7e..7273ac7fc 100644 --- a/tests/modsys/functors/T039.icry.stdout +++ b/tests/modsys/functors/T039.icry.stdout @@ -1,4 +1,4 @@ Loading module Cryptol Loading module Cryptol Loading module T039 -y : [8] -> [8] +y : {x : [8]} -> [8] From 213bb3a5de68e24d22d50015e1d9daa4b4f722af Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 21 Dec 2022 11:14:59 -0800 Subject: [PATCH 14/21] Fix windows test --- tests/issues/issue565.icry.stdout.mingw32 | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/tests/issues/issue565.icry.stdout.mingw32 b/tests/issues/issue565.icry.stdout.mingw32 index 201cbc61e..c17f9ab68 100644 --- a/tests/issues/issue565.icry.stdout.mingw32 +++ b/tests/issues/issue565.icry.stdout.mingw32 @@ -1,4 +1,8 @@ Loading module Cryptol +Loading module Cryptol +Loading module T +Loading module I -Parse error at issue565\I.cry:3:8--3:9 - Backtick module imports are no longer supported. +[error] at issue565\I.cry:3:1--3:10 + • Expected a functor + • `T` is a module From ca7c47b2fd7acb6fcb0d4c5b0b17347c0cee5242 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 21 Dec 2022 14:21:06 -0800 Subject: [PATCH 15/21] Bugfix, apply substitution to schema's constraints. --- src/Cryptol/TypeCheck/ModuleBacktickInstance.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs index d3faed8f0..b17022148 100644 --- a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs @@ -137,6 +137,7 @@ instance AddParams Decl where let s = dSignature d ty1 <- rewTypeM tps (sType s) + ps1 <- rewTypeM tps (sProps s) let ty2 = foldr tFun ty1 (map snd bs) e1 <- rewValM tps (length cs) vps e @@ -148,7 +149,7 @@ instance AddParams Decl where s1 = Forall { sVars = pDecl tps ++ sVars s - , sProps = cs ++ sProps s + , sProps = cs ++ ps1 , sType = ty2 } From b527506dee3470c120e30f67034ff71e5bcecaa9 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 21 Dec 2022 14:33:38 -0800 Subject: [PATCH 16/21] Check for repeated parameter names in types --- src/Cryptol/TypeCheck/ModuleBacktickInstance.hs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs index b17022148..5c7578c65 100644 --- a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs @@ -9,6 +9,8 @@ module Cryptol.TypeCheck.ModuleBacktickInstance where import Data.Map(Map) import qualified Data.Map as Map import MonadLib +import Data.List(group,sort) +import Data.Maybe(mapMaybe) import Cryptol.Utils.Ident(ModPath(..), modPathIsOrContains,Namespace(..), mkIdent) @@ -181,6 +183,12 @@ newTypeParams :: (Name -> TPFlavor) -> RewM (TypeParams,[Prop]) newTypeParams flav = do ro <- ask as <- lift (mapM (TC.freshTParam flav) (tparams ro)) + let bad = [ x + | x : _ : _ <- group (sort (map nameIdent (mapMaybe tpName as))) + ] + forM_ bad \i -> + recordError (FunctorInstanceBadBacktick (BIMultipleParams i)) + let ts = map (TVar . TVBound) as su = Map.fromList (zip (tparams ro) ts) ps = Params { pDecl = as, pUse = ts, pSubst = su } From b96f77f1f1f563c058716b3a49933c5db9331a97 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 21 Dec 2022 14:54:25 -0800 Subject: [PATCH 17/21] Apply the substitution after fixing up the types in module parameters. --- src/Cryptol/TypeCheck/Module.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 8207c53c1..0104dd6ee 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -364,7 +364,7 @@ mkParamDef r (pname,wantedS) (arg,actualS) = let res = foldr ETAbs res1 (sVars wantedS) res1 = foldr EProofAbs (apSubst su e) (sProps wantedS) - pure res + applySubst res From e1919276807e6f745ce9e09effb1da7f8077632c Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 21 Dec 2022 16:20:50 -0800 Subject: [PATCH 18/21] Add a function for updating the identifier of a name --- src/Cryptol/ModuleSystem/Name.hs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index 1b1f14134..7a4c57635 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -27,6 +27,7 @@ module Cryptol.ModuleSystem.Name ( , NameSource(..) , nameUnique , nameIdent + , mapNameIdent , nameInfo , nameLoc , nameFixity @@ -210,6 +211,14 @@ nameIdent n = case nInfo n of GlobalName _ og -> ogName og LocalName _ i -> i +mapNameIdent :: (Ident -> Ident) -> Name -> Name +mapNameIdent f n = + n { nInfo = + case nInfo n of + GlobalName x og -> GlobalName x og { ogName = f (ogName og) } + LocalName x i -> LocalName x (f i) + } + nameNamespace :: Name -> Namespace nameNamespace n = case nInfo n of GlobalName _ og -> ogNamespace og From 7c9e75e27d48cd74b8d4832eeaa6aeb1e4fcd1ca Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 21 Dec 2022 16:21:28 -0800 Subject: [PATCH 19/21] Keep track of the qualifiers of module parameters in the typed AST --- src/Cryptol/TypeCheck/Infer.hs | 1 + src/Cryptol/TypeCheck/ModuleInstance.hs | 1 + src/Cryptol/TypeCheck/Type.hs | 6 +++++- 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index a4b8eef42..17c6f56ea 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -1362,6 +1362,7 @@ checkTopDecls = mapM_ checkTopDecl ModParam { mpName = P.mpName p , mpIface = thing (P.mpSignature p) + , mpQual = P.mpAs p , mpParameters = ModParamNames { mpnTypes = Map.fromList [ (mtpName tp, tp) diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index ea6e2d098..d041a3665 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -159,6 +159,7 @@ instance ModuleInstance ModParam where ModParam { mpName = mpName p , mpIface = moduleInstance (mpIface p) , mpParameters = moduleInstance (mpParameters p) + , mpQual = mpQual p } diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index 691ea5f8a..412ab03fc 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -28,7 +28,7 @@ import Cryptol.Parser.Selector import Cryptol.Parser.Position(Located,thing,Range,emptyRange) import Cryptol.Parser.AST(ImpName(..)) import Cryptol.ModuleSystem.Name -import Cryptol.Utils.Ident (Ident, isInfixIdent, exprModName, ogModule) +import Cryptol.Utils.Ident (Ident, isInfixIdent, exprModName, ogModule, ModName) import Cryptol.TypeCheck.TCon import Cryptol.TypeCheck.PP import Cryptol.TypeCheck.Solver.InfNat @@ -66,6 +66,10 @@ data ModParam = ModParam { mpName :: Ident -- ^ The name of a functor parameter. + , mpQual :: !(Maybe ModName) + -- ^ This is the qualifier for the parameter. We use it to + -- derive parameter names when doing `_` imports. + , mpIface :: ImpName Name -- ^ The interface corresponding to this parameter. -- This is thing in `import interface` From 94d60a8ec6d2f6e598e7789ab5eac02cc6aa6866 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 21 Dec 2022 16:22:47 -0800 Subject: [PATCH 20/21] Change the names of the parametres in _ imports Now the names take into account the qualifiers of the parameters. Thus if a module has a value parameter `I::x` the record of parameters will have a field `I'x` --- src/Cryptol/TypeCheck/Module.hs | 18 +++--- .../TypeCheck/ModuleBacktickInstance.hs | 56 +++++++++++++------ 2 files changed, 50 insertions(+), 24 deletions(-) diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 0104dd6ee..cebc8d825 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -26,7 +26,7 @@ import Cryptol.TypeCheck.Solve(proveImplication) import Cryptol.TypeCheck.Monad import Cryptol.TypeCheck.Instantiate(instantiateWith) import Cryptol.TypeCheck.ModuleInstance -import Cryptol.TypeCheck.ModuleBacktickInstance(doBacktickInstance) +import Cryptol.TypeCheck.ModuleBacktickInstance(MBQual, doBacktickInstance) doFunctorInst :: Located (P.ImpName Name) {- ^ Name for the new module -} -> @@ -58,15 +58,16 @@ doFunctorInst m f as inst doc = } let (tps,tcs,vps) = unzip3 [ (xs,cs,fs) | ParamInst xs cs fs <- as2 ] - tpSet = Set.unions tps - emit p = Set.null (freeParams p `Set.intersection` tpSet) + tpSet = Set.unions tps + tpSet' = Set.map snd (Set.unions tps) + emit p = Set.null (freeParams p `Set.intersection` tpSet') (emitPs,delayPs) = partition emit (map thing (mParamConstraints m1)) newGoals CtModuleInstance emitPs - doBacktickInstance (Set.toList tpSet) + doBacktickInstance tpSet (delayPs ++ concat tcs) (Map.unions vps) m2 @@ -158,12 +159,13 @@ checkArity r mf args = data ArgInst = DefinedInst Subst [Decl] -- ^ Argument that defines the params - | ParamInst (Set TParam) [Prop] (Map Name Type) + | ParamInst (Set (MBQual TParam)) [Prop] (Map (MBQual Name) Type) -- ^ Argument that add parameters -- The type parameters are in their module type parameter -- form (i.e., tpFlav is TPModParam) + {- | Check the argument to a functor parameter. Returns: @@ -185,11 +187,13 @@ checkArg (r,expect,actual') = where paramInst = - do let as = Set.fromList (map mtpParam (Map.elems (mpnTypes params))) + do let as = Set.fromList + (map (qual . mtpParam) (Map.elems (mpnTypes params))) cs = map thing (mpnConstraints params) check = checkSimpleParameterValue r (mpName expect) + qual a = (mpQual expect, a) fs <- Map.mapMaybeWithKey (\_ v -> v) <$> mapM check (mpnFuns params) - pure (ParamInst as cs fs) + pure (ParamInst as cs (Map.mapKeys qual fs)) definedInst = do tRens <- mapM (checkParamType r tyMap) (Map.toList (mpnTypes params)) diff --git a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs index 5c7578c65..212cd10e3 100644 --- a/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleBacktickInstance.hs @@ -4,25 +4,36 @@ {-# Language BlockArguments #-} {-# Language RankNTypes #-} {-# Language OverloadedStrings #-} -module Cryptol.TypeCheck.ModuleBacktickInstance where +module Cryptol.TypeCheck.ModuleBacktickInstance + ( MBQual + , doBacktickInstance + ) where +import Data.Set(Set) +import qualified Data.Set as Set import Data.Map(Map) import qualified Data.Map as Map import MonadLib import Data.List(group,sort) import Data.Maybe(mapMaybe) +import qualified Data.Text as Text -import Cryptol.Utils.Ident(ModPath(..), modPathIsOrContains,Namespace(..), - mkIdent) +import Cryptol.Utils.Ident(ModPath(..), modPathIsOrContains,Namespace(..) + , Ident, mkIdent, identText + , ModName, modNameChunksText ) import Cryptol.Utils.PP(pp) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.RecordMap(RecordMap,recordFromFields,recordFromFieldsErr) import Cryptol.Parser.Position -import Cryptol.ModuleSystem.Name(nameModPath, nameModPathMaybe, nameIdent) +import Cryptol.ModuleSystem.Name( + nameModPath, nameModPathMaybe, nameIdent, mapNameIdent) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Error import qualified Cryptol.TypeCheck.Monad as TC + +type MBQual a = (Maybe ModName, a) + {- | Rewrite declarations to add the given module parameters. Assumes the renaming due to the instantiation has already happened. The module being rewritten should not contain any nested functors @@ -30,9 +41,9 @@ The module being rewritten should not contain any nested functors how to parameterize the parameters. -} doBacktickInstance :: - [TParam] -> + Set (MBQual TParam) -> [Prop] -> - Map Name Type -> + Map (MBQual Name) Type -> ModuleG (Located (ImpName Name)) -> TC.InferM (ModuleG (Located (ImpName Name))) doBacktickInstance as ps mp m @@ -42,7 +53,7 @@ doBacktickInstance as ps mp m RO { isOurs = \x -> case nameModPathMaybe x of Nothing -> False Just y -> ourPath `modPathIsOrContains` y - , tparams = as + , tparams = Set.toList as , constraints = ps , vparams = mp , newNewtypes = Map.empty @@ -84,9 +95,9 @@ recordError e = lift (TC.recordError e) data RO = RO { isOurs :: Name -> Bool - , tparams :: [TParam] + , tparams :: [MBQual TParam] , constraints :: [Prop] - , vparams :: Map Name Type + , vparams :: Map (MBQual Name) Type , newNewtypes :: Map Name Newtype } @@ -176,13 +187,23 @@ noParams = Params , pSubst = Map.empty } +qualLabel :: Maybe ModName -> Ident -> Ident +qualLabel mb i = + case mb of + Nothing -> i + Just mn -> + let txt = Text.intercalate "'" (modNameChunksText mn ++ [identText i]) + in mkIdent txt + + type TypeParams = Params TParam Type type ValParams = Params Name Expr newTypeParams :: (Name -> TPFlavor) -> RewM (TypeParams,[Prop]) newTypeParams flav = do ro <- ask - as <- lift (mapM (TC.freshTParam flav) (tparams ro)) + let newFlaf q = flav . mapNameIdent (qualLabel q) + as <- lift (forM (tparams ro) \(q,a) -> TC.freshTParam (newFlaf q) a) let bad = [ x | x : _ : _ <- group (sort (map nameIdent (mapMaybe tpName as))) ] @@ -190,7 +211,7 @@ newTypeParams flav = recordError (FunctorInstanceBadBacktick (BIMultipleParams i)) let ts = map (TVar . TVBound) as - su = Map.fromList (zip (tparams ro) ts) + su = Map.fromList (zip (map snd (tparams ro)) ts) ps = Params { pDecl = as, pUse = ts, pSubst = su } cs <- rewTypeM ps (constraints ro) pure (ps,cs) @@ -202,13 +223,13 @@ newValParams tps = let vps = vparams ro if Map.null vps then pure (noParams, []) - else do xts <- forM (Map.toList vps) \(x,t) -> + else do xts <- forM (Map.toList vps) \((q,x),t) -> do t1 <- rewTypeM tps t - pure (x,t1) - let (xs,ts) = unzip xts - ls = map nameIdent xs + let l = qualLabel q (nameIdent x) + pure (x, l, t1) + let (xs,ls,ts) = unzip3 xts fs = zip ls ts - sel x = RecordSel (nameIdent x) (Just ls) + sel l = RecordSel l (Just ls) t <- case recordFromFieldsErr fs of Right ok -> pure (TRec ok) @@ -223,7 +244,8 @@ newValParams tps = ( Params { pDecl = [r] , pUse = [e] - , pSubst = Map.fromList [ (x,ESel e (sel x)) | x <- xs ] + , pSubst = Map.fromList [ (x,ESel e (sel l)) + | (x,l) <- zip xs ls ] } , [ (r,t) ] ) From 7f793d786b6326c0c921af27cb6ec149b1f5208d Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 21 Dec 2022 16:39:27 -0800 Subject: [PATCH 21/21] Update the reference manual to document instantiating with `_` --- docs/RefMan/Modules.rst | 103 ++++++++++++++++++ docs/RefMan/_build/doctrees/Modules.doctree | Bin 63536 -> 78522 bytes .../RefMan/_build/doctrees/environment.pickle | Bin 139519 -> 140002 bytes docs/RefMan/_build/html/Modules.html | 93 ++++++++++++++++ docs/RefMan/_build/html/RefMan.html | 1 + .../_build/html/_sources/Modules.rst.txt | 103 ++++++++++++++++++ docs/RefMan/_build/html/searchindex.js | 2 +- 7 files changed, 301 insertions(+), 1 deletion(-) diff --git a/docs/RefMan/Modules.rst b/docs/RefMan/Modules.rst index c20fc4fc3..cbf82b8c3 100644 --- a/docs/RefMan/Modules.rst +++ b/docs/RefMan/Modules.rst @@ -735,6 +735,109 @@ in an instantiation. Here is an example: x = 5 +Instantiation by Parametrizing Declarations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +It is also possible to instantiate a functor parameter *without* providing +an implementation module. Instead, the declarations in the instantiated +module all get additional parameters corresponding to the functor's parameters. +This is done by providing ``_`` as the parameter to a functor: + +.. code-block:: cryptol + :caption: Instantiation by Parametrizing Declarations + + submodule F where + parameter + type n : # + x : [n] + + f : (fin n) => [n] -> [n] + f v = v + x + + submodule M = submodule F { _ } + import submodule M as M + +This example defines module ``M`` by instantiating ``F`` without +a parameter. Here is the resulting type of ``f``: + +.. code-block:: + + Main> :t M::f + M::f : {n} (fin n) => {x : [n]} -> [n] -> [n] + +Note that ``f`` has a new type parameter ``n``, and a new value parameter +of a record type. The type parameter ``n`` corresponds to the functor's +type parameter while the record parameter has one field for each value +parameter of the functor. + +.. warning:: + + The order in which type parameters are added to a declaration is not + specified, so you'd have to use a *named* type application to apply + a type explicitly. + +Functors with multiple parameters may use ``_`` as argument for more +than one parameter, and may also provide implementations for some of +the parameters and use ``_`` for others. + +**[Parameter Names]** The names of the parameters in the declarations +are the same as the names that are in scope, unless a parameter came +in through a qualified interface import (i.e., the interface import +uses the ``as`` clause). In the case the name of the parameter is +computed by replacing the ``::`` with ``'`` because ``::`` may not appear +in type parameters or record fields. For example, if a module had +a parameter ``I::x``, then its ``_`` instantiation will use a +record with a field named ``I'x``. + +**[Restrictions]** There are some restrictions on functor parameters +that can be defined with ``_``: + + * The functor should not contain other functors nested in it. + This is because it is unclear how to parameterize the parameters of + nested functors. + + * All values coming through ``_`` parameters should have simple + (i.e., non-polymorphic) types. This is because Cryptol does not + support records with polymorphic fields. + + * All types and values coming through ``_`` parameters should have + distinct names. This is because the fields in the record and + type names use labels derived. Generally this should not be a + problem unless a functor defined some parameters that have + ``'`` in the middle. + + +**[Backtick Imports]** For backward compatibility, we also provide +syntactic sugar for importing a functor with a single interface parameter +and instantiating it: + +.. code-block:: cryptol + :caption: Backtick Import + + submodule F where + parameter + type n : # + x : [n] + + f : (fin n) => [n] -> [n] + f v = v + x + + import submodule `F + +This is equivalent to writing: + +.. code-block:: cryptol + + import submodule F { _ } + +This, in turn, is syntactic sugar for creating an anonymous module: + +.. code-block:: cryptol + + submodule M = F { _ } + import submodule M + + diff --git a/docs/RefMan/_build/doctrees/Modules.doctree b/docs/RefMan/_build/doctrees/Modules.doctree index 704333f901d760d227add51d5c1a9926fef7bdab..135ad6ea8833a16495c973a85f13da17dfd01e35 100644 GIT binary patch delta 11504 zcmc&)Yiu0V6}C5t7f+C#HIS!c-vFtd_1ZuhNMi_1FbY_(DU|#`K$;!zjy<#4o!QLH z#&*&$;YS}rD^Zw*rnCZtDD zcGr#r2(Udf_uO;OJ?A^$Irl#Q!Lpa%Ti$kj#iK1PtuM62-*-=!x}AYh-Lhrf)?`~V zbT&54?vPEnsMw}u70FH{`d{ zk8X9Dx^b`C@16!g7-M1~V4egkm!}m($1ua)FhEc@)!PS;I6Ht7Paj5$R*A3L7u$S=%uCtjL!` z(moaXja&a-W=I^9WS-9jrA4)3Ua{u(VOWk+g>2No` z-s!%5vQz0F*L0?DVLNYR_v-uEApapTHqH*So%nBnO-Yhf9`o=Zjfdf1d)QHSfE|;7 zFNSGHUZly!X@5&*&04&mvj+ReBlOGI{?)rKN_z%zANbxSt=rvelG|d~t=CfP9g9Pg zG9?p8vYY~gC>Hb9o5`dBPQa@W90}?&nLT*yL4qWQNC!~8RWTJpI>JJrW4T~+aGWkF z%oxYW@k}O!v+jMP1dQ{{9(r=6yPlR53r}D*C%WC={j59o9QXKLPxye;HG2UO$#cC8 z@&k5vRyQq~%rd*VOI188A10(w0)jA$Z<~#l?u5NFjZtHOPLB4M}&%v-3 zqSpDhh+2`40p4MxT%VRT{YExyv-I%rxJ3VB!|bSjj75C+=oFqIY>s(xB=Ot$qU02o5|>zOp3{R&U=4YE|eo5NN`vgPK-RC<7468`{34di3!MnqvzoKGq`{> zW5}ec5rg3&!lj2wk+wt<#xt4kbl$pZ$w0oW~FVav#%6y z!cbh{D`zNtJlOKtJ5B`T!tA*dQp_mHyT6VyeM_lIH`NA;NmyR%f816CDlN-kH=oi2 zRN5=?N!iqq1*&c}NX6fzKtfzW6f!X40X|+EBnVn$5-@KC!AE2`7nUNFV06Qltdf$| z5GmmBC=I5Ka$nAYpC0DbLD|A^meiqfE-8e|rBXr5iZXy?;?HU1FFvs{Mej7bFfF1f zEI}#@QPx?Iwo9cfg}%m3>MXfU;mo-idPX8`V#Y>(VaaxK=A3Y=kxr^l`r_WE`k7`0 z-{Vjzo(FI5bRWKCefy)&Zf)WJxE+_Tc1AkADrInC4iRLd$^r*+rGtXk{qDp-JWc`f zS)j@49=9~Q+}R18A|WGE+TLglT>0T1QB_);daxp~DxzyaJ^*8rrx|&?Ur!=>CdyRw z@*Gk$OhrOY)Ol_Rh7sn%VQH)=u6fxE{#H{lTU>-?6p6w?O3l2KJ;Qk^Um5tqw8E5> ztgk!>W2k+&hm{7yYDU3)2Rn%X)-8o>f#3&yA25lgH*2P)u@ctjc#Vz9Cow$?6>Gv$ zU*VS87Fgmuwp4 z2^H@SmE{6YCm4t%H!f#+C{S_NuMH_f=oDeXneQaHzo>UI8QDT%l)bbdIIZ52AbwXs@(cwrS`S=_m!bY)(J$F+DNMM?!4i`2H;6 zd&+r6pyyM5P`|#Ej?~zX91xhLccgHsl?Ll^78V(e7qr0jq?(Hi;?hqMLa%eb_=8Qc zmpHz#VAJ+8beZQ4nVoe)CSs;K5;oP75bE`hI9rx~gDch_DApztZe$|=i9fKr2chaa zZEIinC3n(4aCt+4y!Ifd!w)NwhrZNxE?4J6KHLe0AK1O zlBoQT+d?bD2k0!Wy|QwwTqr2En^4y{`IC_^Di6bI!IoM$7DGFUkRxm0APlsJvpN3* zl+$nq&=S1R?C`wGryv?XfI|^d0QF$1fnFMp;(QXP9U&^_)YJv26g-jMiI_Dc2{#DH zVC8E|s-n|`j*V3G9d$99p^!Qc>owFYVBPuShzxk!{q(~>NJYKqzPWYtMd=OXHAmoO zUUm5zd;(7&k`PDE?KSonHbL?VdnHOBCA*)H( zBG`siDSP%(8iyz<(E?d`7)d$J!r55XX1r?k119h~z$pqbF9Zl# z=r6D2!i=K5EDByK#|rY8QoscR#ncWfxgmCoqAR9cC`@AFvl#1`aKZ@;8cL(UlP@+r%_SM<#3xqnhEZAUwoc6LJ^O-8W`yU+Q@0fNDHzN zPcDQ7S2p82*G1x`sR885CmRFAF9krH^a0|{=q5*C{=%BxIdA`**Ypv)&A&F}rFy}4 z0sTt2)z13CH~-?oO|DmW{+@60aIndpK7e@P8nMx=S7HW2#4899UkMO#WrRz(r!w7F zRN4gltX5i+bRL^86D1KxvYdyQ!PxO12_E7f4Ds7vwN37)Q8?TrXAjz1_8=SOcPe;e zkXl${c#cz~9PyMA&Tq!Ff@V*r*d(xw-wG3rYso!zy4UeZt*BIFW`WtDSswQ70#w5V zB_eIX4LICw(Cj&@n$>eF=kvv`h~{fO)k7Qeimfw2)y<7wziMT|t8Oa1MfdTpFQAf@ zh0ShFqjbo+zdgNf&-vSULw;p~=iQ{JbLj5S4V^O_z_;(L=fM*4gRmsrbRglj7Pqe% zB4Pc)xZ!n%shJmlc1Nx;%zyD`*2SL89$%qZ5=R#;F<1(BlN||hVaHntzp(R}$c3GI zdN{8}N>>h*HP8+^;z2PsY2t>WJ|UbJIi}HP!L0eagaPkN;4a^%$J5t~?GUv^&83jF zv+UvBfbxwp{|CWre2oXZHSY9w9{q~05n2{n)ZjT~Q^zls`_}2pwr5QR;f}aO4?;$% zfik1)Ur!3wI``OX>W>Xn${!L2Ft`Dn^zL~L&>!CYqMKmz-~aLr()@rxn>e@7F>WCz zJyNTSqW02V+D-ebm4OIsp#mG59`sO6T-+Uuo|RN(^$K(gHqRQyucC@7-n;KxGt52r zN7nl8i_-f)jm3VEc=6Of|GF&xG>nyhGU2}Z;r{sJ^!wKn?v-cm+n9fZ{&)!gD_7cy zmU3=PSAX+QCtUZ;aP0Af`{tP)o&3YSWpxw1f}q6N`(lt`oE?kPXj~n5@z-bDTD$Tm zaP@@W;mhAf&-)YZZ_b@>`_V@` F{tp(z9p3-| delta 170 zcmdn>lx4#QX0`^_sj5F1HnOq5*`BG!c!-H9iEq2ECgTfcb{jqhhAd0I=`y;EvFs)w zjv?Rl23^J&;nE(?yu{qplFEYA;wiOLG_q{?rvKDsv|=*hn{KMdXvtZcp$HNNYOd8| zj9~)myRFBVwB22wk(qINoB`t}wgRAe-cr-U3>h~to#LB5QI=7WJwrD`I_o&!Z<}v;+Vq#4-v1 diff --git a/docs/RefMan/_build/doctrees/environment.pickle b/docs/RefMan/_build/doctrees/environment.pickle index a63af4eadde94c6fda833ce20dd6416997c8decf..c148994affc2cb2ac069ba9a07aaba89bff81be3 100644 GIT binary patch delta 24122 zcmb_kcVHCN*5^*>vyg;jQ(*}NNFp_Kksf+ksvrtN2oW+s0x1f7Anl2O`$U+98$|^~ zMG$FG^B#zzC?$$mkd8DJf+(U0C<5O(_ilFX-kmK^$sc#xxxaIM=bT$Jvv)tNeD0IV zTe`&7tJ*a^FDql{^eLHnPKVlk+LYYPyu7TOY`Ch_KWALQB)G5Ntr^|Wp)$!K)3fu_ zr#T%VJ$m$ZIw}s%e5`+Zw$l-Y2;DL>CZ*@5=NGMuJrGi@rBbe3&n`zVmKL9`c&BJ? zt@kRBmip?1y84*JFGO5HpNm)E&}o?iuRhZs!$XVZEAen}MG`){QJ8~Q<6qc_hsYP-z{Ad$-p9kt zRXgy|b`86_@yaf|`p>H$!9oAO*T2$JRt~D&uy=M|etLF(R(d{oB4OY7a%O&R z){Ly|@%n+!<61ca2qly`gZWZ>8JwY&>T}no>Sqe02BU8rRnxOGCgkL11G3Z6C^1V^ z+IZ~r##2P4jmNp1%kT=cHxaN&2owzZ2Y_y?H+#7%IS*&Oiu$knH>rqP`bHL=d84yZ zuTv<9cEU=X;Y@d?%yrIkCbPIV~q5`cQYA**OQ>Jqf0GQ>}^7*0cX-IBf zz6)W?#w0*Ey0I2nq+j3Im@L-oz11e{S&-M3VDTIlOZACwHJI&y(`3!_k;B6CHKBL* zxXfwJeCJ%JB%wVI)t+`PaE^T%Qa3L%JvU>5Q(FZ$CnRd7km?X71o0oADIltbJ*)Nj zO>-f4UfMKl=pr-_iwTJfoEpWe!m=yW;!*|AUdO9-WzRO?m4>l-6VBlACcJ@e)Hdrq zH-AL-=~cHpZ#j;4zrf<_P?}zy#OZh6ZJ{19?iN+rT9ZUw#v3dtE*X#96_V*+A*4p) z1$>0z?OUG93NY}fV61jn?{YguKep`w%U>oiEv$bCcLB=^SlWf6c}1IuqK4^HyQS(G z?_|_6^i<(`#A^DQ`y%xl?~F|JRPMrZTUg0$&8m0XSsI6dBH0V|?i231t#KoS147lX zqG83e6s295o}SQbs1}Pg;;@K^Vv$x8N=K!P-04&Db0#@88(hwEy4qO+igAW+%t+2h zRLuBH-rl!y3d*w(_-BT8aX(kzalhq3tmVaQuyEJg3L9tk@s9n9GWH%ZtHVtf6*Fc@ zAM_5I8QR5}?fIacWtPCfow&>?t^VY?^ zkEy#1Ieo;w5tdJlYoilbwm*#Q(!=+Ail6?zo2fHi4@}Z_w z|En!B(O>$so#l=o;!Y3s7~W;+^Shq<*`uler2Asr--jtx!*t7m z5lVEpeoy+40p4m@OS^j@J?PxQ$n)HJ_w)9a=HWnA?n4rr3U|G8XE@89?1NjQx}Y3$ zRVSf_+m)utF@jg{RKb#?==Cqs6s7+?^3@~WdYG@~e?1^*Um;WOtK>uXTPB!rY>}8L z-1YXAhQ3;R>JYINc*}|TcF zk&|=0_3%OMSnypxx`;d3a=f)=n~4uvByJY&dOLXAehtN%7F=uAczaVHm^?qm7O#0M=B z{}AqaJ9!~<@}p-?M5#5(T74BflX?&H@pUoh;HiT7O5b(1jS^i0JIH@Ny#CvVno@oK zxj)q;!(4sg`O%i<#8-wtAxTB{?-me`3ckAjr9MPs$mwPXq+M&ftIyQ~WzsW&WrTor(PCjRq2Yyrx)OVgDn?-At} zeW)odO8oI@VtZELV?ue~U>Q?M9|#b_)xVzC~J>sb7T#XAVP4SnILg1Za( zY4~-^x0=KWp<{>&Xm}h0y_h@GhjOdwKG6_fffea4T!>wW-A+JG+WX!quFAJ z8O;_C%xIi~J3_L?r8>2b(Lv09m`XNq5nvMsMu3fOi~#F`k%0C`QMK#+NJZ{dee{ii zDGWrK?RUh!48UER8ctj}@6nImcpz#Is$|WfPXwIFeOoQFjOfHGd>jgSU{w+$^wl>< z+;1#oJMzc!(jr}(0BT`}B#R$#Jr7sA_2z$Q>Ug*EuV7gnt+2lPKK;@kt<(bdqa1qn zB(X>28aMC^sV*JRT;KU;9N|4axz$=-Ulwb(3dbIIY z6lFQ#pBtLUJ^u0CH1!nLV)?`4lz7~@VWK-4Q}P`LX+hLWh9E5=WTE=IaD&t*X>_$h z!pSANO(B1INRuRZi2F573{tV&bWiOb&eWWAQ+bj_Un@@*C}EN4%ZLB5FKhWwTUuOP zfwUvGgh;o0%DiC=SS2*H5^1NV7&4UcrjC zs6u8DTbiN6#10*%j}=+FYHqRRwO$K~2mYl;p!fRl|zMg_2OBJadmSqLB|prNwu{ z$g9M*(%@qf3Ho6TaN?_mj2w!U^pOZM%sOT}V;ZpcaHqhrET$QL2D1BNCu$J}j1W~he^8Ri%v>R8>i91x=}p!&A11GjF! zXdT_rg!}}?t#3+35Zg^dvA1#8XhJG9I1(i_IHM!DSzMAz{zX&)#_~~vhK%p2z=Np z`*C?l=k_G6gYF`*k@GI1S})RE?IYO8x`>{}jj|RbbP;1&7qO!k$so4j-jYUJE1{%- zM9=|!NQyef5R}Kv;qpM;g%^eaQoX0GVwW{lK;b z5~?ue8BTxbM?O{snk+J={ognq8BgbdNznf#*~txMRrI~-|0ej*lR-BOAoie>0K>?W zz&?<)Qnw3EU`bGH+%QRkJeCA^2a;mNw%1!yOoD+A!g})yLq?AOUOHhYDG3VYyg!uh z9weOup>!Pvwp^D`ge*cTm_>BVa594qA5Ipj0z3NSaPo#)CB~ym=|E3BM8=W5wDSnk z!b2Jt&Zcd+fJad9Fugc}tgxmcGV4T|dg@4{haVumv z_4&v93vO^d{H~QgG?I){MN`j2DT(ybNYXjzRKsN9sWxX6>8)l6aWo+EXmm zx<5)P5o<0=G7n8L>ac_|b@bC*R=_X*bTmm-lsU{*tqfQ3w@YA0D`)cL%c@A4Ts14^r{|8(go&QMtwK~MkzG?6B0|B(Bur#!MeuHYn8;S zUI)A(?Yykx@Grt67XIRM8RSbvd5f{?X|NJE>&j>6WM{(bPN3fJPMsSYq8~{+k0+ID zBh5_h9N$G93`*0r@Aw72E|pGq{y-X7hohY=G=kUYE8|JiitMGTrS!;nQl~m%X-h$t z_aGG~klw`lsk`oeJacXB;f9cDST}p?`8Em2!{UiN4o7|_UvHIDkV-&X$sW~JeyafJ7Anx5iLdWL77&%I^NEjnWFau1P z|A#Xl#v~#P6NdnrNdF55X=D9AH-qVtGJn{Q%k+mZ`fVb5xZwtJZ8F`;xuiBJp~<;0 zv3N<+DA0S}H@)qg-U^wX&K0^H%jmu5wr9Jf%#@xByI7{D2TSj4KBEWIoc8Lsl172v zao_abKaXDbxw#jlu0;*7HpMmCqUnRXd2?531FQf|H z9VS^IWawa~(A1>e-24GdLTG^f08MOwYyil2)6JEX`NM{Qd(!O}&pL#_4RFOmV)LTw zq@OG#N$Lv80)g%_-*i85MOUWlkm%lCL|R$jcGKM^DKn+(!rm;?bp%Uy{4*xeJw)j< z5Z%L)1p?i#eAC^_=^m8nekRdn(Y@xT`>UkPl&%Z=icI&jVClAh7B-ya$y#JhI_X)` zK#i*Dv)R|6>B~u5Q=9g4zVN;lNC??%0W_~{Ziy;*8!*0s3RbwV-p<7pgvVfDd z(50jkj3xt?LN_{0QYiFIgKOgd7~_Nif3P8JHl8Fe1HcJ}4C`LK0fn9!0ojQ1<1*+c zXZ)?ITXd-E_*+#AoKW>;sj86AgPB83WAG`D*8n-b{Wv3c=ggY#PE^6-yF*gu5BooI zeES6%-zMnz5;~N^@P1lSD1_sLSA0(x!e;SpSO|bu4H>58EjRIhmOgxX=4(waJL~Us`JojA%O~ z1B4hAGkvBOeaWqVTV}geV#`LfV{W!bBxU}v56Nt|2FdoLwWJlK^v$)9Mz&?md9Vb3K>z|=GhWul=uj(8j7%pA|T6S=WAdc#-?+vdu6~LB>uY)bk zB|r~bd}im@+_r0SysmO%J+pI=o67)6nQ6RS*!^r$7j!kqc-37`M%Z!;O=e+Wz3((b zM(z`GY;yk;0C36%2+m@^fIe5t-*9J6VuXdJo&|7Xf6kJBJ?dbIu};!v>P#2*s|;IM zEoa%-WZfdpZ`kf!80^T6%^5enY)38z?>3|TPms`XN5%Z{xj6+>T+fciuzmRF-y*GJ zgss&wf3yG0(W&s_K!_F}LzPXWckKYLRZ?vesmb49rCTi-b3*|VWCfx4WM4uR*&eOeW+~eUPIVjER4@|v ztxYFM=eVVf=+z>R33duM$K9NVzD*vm_HtwQ_#d#-7`8B@NTFTchyOzx3D|&Z@9*BP zb2(!G-wl>`N$b38vWlEa2fhod$UMm~p;OCYT1>t09rwZ{*$Y{c7Zw)7R{K)77nVrM z{9!v}FJv(<2t)2;T$u-3r8JZ_DkQZc}Y5T;!UNjsDkx82PI{uj9u8D$&A+r%Q$|e3FE7vnl@VrjDM4i5Ex(a&G;f`a9L(t z3TV*q+>AT#B)zTS31y5!@l2RIn=*D`Tjx^*`Y zZXwwq5N^s;ni_S96K=#Lgux{R&_u%ZcR^AQLKQ5;10-esu=_D=VQ@)FkavR2vKkn} zzXBrYh7XCwYddHv-TNWTCi5gS1kO3WIbY@+Cdr($JUOq}O=j7a7#hk36mj1j*Bxr1 zAtNu-me8gjgM@(M`vpChSq|AF$*19{h^Tww*UrnDv2^z9zlY z%Z7~H2cDE-oic z*GM7DK4nt3OKdN9Yzm25KA9hQIEwudbxhVaVi9jIMeJops6v|`)oEh)|UB$OJ)%i~xbY${xFne3y-u9IrC{AE(23aGwA85%H@nLm+H)(NPcb%Bpbc9@3J z>O#%nmO&^x|4fD}O8z|xrGd}7ij=FQIvM=GMsV3x5~bK21|RPTrqVsXf$x_aGCYEY z?;Z4^Yow2VloGn@8Z^E)WEA7Y8V4QrJG?OL*On6c_V0kQ!w*VvpX;OnQ3V*^fv+7f z@Re?oA=YE4js^aRq}Vj@^<1cjK$y4Tqc>qIUHSeV1>V4CfnW9K-wAx>TO?Pp-8T4m z2fl=|zPn;Q&weY`2pLu{7`uEo^r-kpTihX?0%5YAJXXRKCU>`KgS+sVaRAHq+=Vn~ z8}P@e>0p5v=3DzQXaQt#f3 zQwBcE@jjK6ztOoBRaRahwsi&{vmDQ>s`OH~7&7wkw2oR;rF9^bk=2#1>TU@|$N@A0 zhbP+DqQua879~j)?D8GGcD|xlTD;GqJWgyU4V`A}m|fo+GBUf9#W$-f7DW|cd>hlj zw=r|Wl^9~XV<<8+hJAQaslI1-BBb>l+BZVEsR}5*ZAtTGi+lQYJW_eUS|7Esv`&=t znx=IR7it0sv$UqVRmoIR>))HKHsD!SFOE_|T|>6;w!SdwqVQ?Q!7KC!p z^?aUL76fe`y%eo0?G!(J%O0I(!WF_HV4b#>(GWd7YIvSb39`e?Z9>I)Ae3TTsF-<83%B)b2nD z{O`h{e^`=ME@C$7BMVNo>`<- zLdo)zag*zvm0_$5hjO8oTmvsAWa95UM!>0E zi-Z#Fje^50rxwExaS_xWr=-lrFQwA+w3_@be)$2S`0WSWw6UAX+AwtW5G*#q9qmml zj$m;Ji>~-tWhX4U;YV9tuy`Abtyql0?=v38;v}wFmPR53pczU!g0G;^pks$Q}PLswLyZ3m19X0xWQipxwX%Cym+~>_>5E)zT1}^+sAf z<|wTJKP1Bef_EQ3G~$OQ{LqXan)5?TI6w-uiYQkPesfxD4VPM5C?GwsZS<|0_mp$6 zQ)|zqJ5pLxX--PfHI;74V(b9hSlB!7tT%nSKK@b?T~kY`L*~)lwUnf| z&H!N7x^S2@cH!!U^f5PT(gd5*B89nC`gd_QGuVvDiHl>|y1G4w*%EXoBA)C@o z-Db$J!A;l<+EAZuHkt0&xPHwsBLYRNI9!uj%FlW#Ino8H0G%t-Qy$612WQg?^bQO1@os9Xn98jSh627*9%6KP zY|$vX{I7f=UFJT#nl8yp;uO5}c(j~y@9X2~(rMY_bop?38+vzfMIq(xe(VLhG+p&9 zU0!?QzjT?kdIw!H*Ye!Or{194%TK?F7yaIfk19Jnw;006^z7)$-Ou+_QsN@&)X{q2 z1FZ$#>F&1oxo5jmwI}h3OH0H@F0G~BX5)2<$^1Trr_I9Yc`LkMsI|uQF1MDd-@Ebd zC_=u=U0PbMXvG}oYW>2Y_~R4T&mxO6cv|v z5%f)M5Mjrrc*xTaZE6qW^?I8#A~lrPCQ>qqlF7PjbL+BvyiL{2ugb$kgcAoAjLVzu zE^*)Iwn%8DSnNUfeD~M~v0@bGD z`bPTAztX$kD7lEqLhW}<%j@M9&6rYBILWR3f!W#aQf&jd>=KCyVsyu?X)0(K)N&fb zb`EMEN~UmM2PQ;D3BR7-*;VZ*2~Y@A(q!I7y;Bf+=CyYfxbcb*YAH-MsO5yzT?2w9 zL`Dfh&+Y1_j+6w5Q1S?ww;|LH%U0>5-~7&zPjcLS<7Ej%$V&Ufrd)d=Y6ch1*|+_wYexxc&GxCt_qyR&_@WJ?NfsLA!?N3D>Bfc2%=X z#9Ya}WZuR#8o6fO8=r!6SWP)&ef#>e?&|GQ#8Tge=_Q{}R}Bz;>)Ry3)ohjU>4Zar zK`FjMJ}s=FM~q8f1mBI5Z-igZe$hpJ*hJoyyh!G4{5qZds;~WWne*|Qaz?-2^3@pi zX(?jy>*IRkuUDuB2)}-vDfpVL5`IlS(h8KEGI6!lU6 zp4l=#YN{&Re%}t9nUX|x)MPDhq!<0rTkR!9cr9;1c^<$_z47ULR0D)xvMc>qfn?#w z8OrTfi0mpqYN{&3&O8WCO){|~yWyuSwOEP}*>Fi#i(;qaA=Xh2X>Os$07t}I+fDD* z)Ub#*yWh`h3AIeK_504u-TTWhrEDd!T26^VQ;o}n(2nj>DH%@5P)Zh3GM|$A)HXvYxsj6VDOo_t zJW4*Il966nL2l$JLr$eEm1!nYo1`As@qT%W6qD|2y0F0RDI6}ULKivznjsEY%- zO0~!kTECNj1f=53vMKY69WLp6GG<^k&ErU8xhyFyJ;UP=jPI$ZyW!u=&jB25$ zP=QXMzAYu$#t>Mb9*_^vZ++O@y3hpPX3OfrC6jQ@9ngmz35BRM8N67*!K~flS++C` zCa?uzFkksm_;%#K^=-T#wN;+S>OnVfUXqlmy&=b{3U;ABbW=l{`aH&I(^68o6zwT* z0CPb#ATT7J)&6ufkS5tD`!!>c3bVnPAXQYCHkhH)ggaG=pcPqaH061{NMJh~!To_T z_Om-1Lr?X3Gf31C(k4Lg4TfU{D~!MxjE{infdMPHQ7$u{$*4yoAyYLFfJ>E8q*K)JgqZ)yL!HeBOJQI+Rd6g&;iX_Agj7}(QI(S>uQj3o}!*o_Vt5g24Y z+vb3qRNV{`F5@t*DQh_wVpGc@(K{swY!nYeg&EEehH0!rGq|%ho1Sk5gVa|nAO@S5 zD+ba6gH*7a;vq|Y-vT0Q=`@xZ3$EHgo{oi~>X85-uI7+gD@b#=QN0iVq!JblZEYC!LC;5-5e=nX$7~j zk*%S1Z6IgoKzFqyFi2dqR!kC{5gCR3Qw7UugC*w&D0#6B98(P(xFcKGIkKyOzJ;Cd z0vY?LqFQFsb^JNxD}MD2+t#JAs0NiT?3O8=W|l0om-Bj!Ay0Vlp(i-%j*A} zgQoh;4Y4-h`8V+fVd8qLiR{S^a0aS8=G3^_7(25tGgP6VJv@ z@BpX=6#oYG76$D%8pK-8fDSCO3pk_Xkmq%-iv%;-^ezykWH{J?O_0HMcYziLNpCGo zC&?kIVTM3fv}BVq;I5!&K{S66v!H}b=%A)tWo*B$oQW&j)JM^BY!!42>jIEP4EtNF=!L?hO# z9}da4Ng3oL_85k+BR!ydZN`X6c zTpJQM=g|O28+zl=7mQ2R2LSQ(!2u^2ke361tj+>=V2}zntS=5Ydo3Wc0~x~3^o1^g zLA(+E+6)q92ob))YPo_%^oMI$Sbw;_Ho(#SG3MvZfToyZxDuk4l7OfLLPH~#Gyn^R zG&8optZ<_x*8b4oW8VF=vFoyLuh{^^T4~%s=n`}66Xd&y4u=gr7JmE=Brzg zp_drTdx<9p;mF|ZR8vy6w+fbU6OL8gr3~+QWk@@*mu`X^YXfOA7(s>v0C{FG6x0UN z$%P1tV!e)KkAU}r0(m_E$evrF zXKf&@Zo@_ENB%)PuiOR=K{fDU_}{%})f2J^yYF^b3+q_&9ni@nNGn|1NolEwmcgBD z?;Wt*(I}?6XHe-*Y&_7o!(O=)BAd(k!Ylz0hEk$39lsOyKy&s@E~F3qx7z?daOx~# z*o~tgM>U%I{3yr`x<*l@5H%`yGz?UGn0UF8yUV;yjhe@6RO%S02M!lW@?P^MS%&J3 zt%n~Jq6T=+rX1*~z@6Mj*ZF)TPH5l`RN>^wc?BijWu&2;G>i2c2U^%~6!-_(_HmHV z!d46mpxL49{5Xh(hD^FVL=|A{Xyjcx6gdgG!1RqCY5$;JGuGUpgipuZlmHctTfb{qkStfbbcs@tvLm) z9i7Nj9svVyHg5u48^%u=O=ho7fR>HvoRKyeWkrAR{R9{Yj%R#j*VCP^X4^+^b4@i{ zC&Em}D?SvD31wh2iw7$Oz>93nBzU6!9u!7L?xm14(K;}x z8493^ISMdn7ktmpnY3la+YPqcg~~HAZ0Z!qTwVy_^-l@CKXSc_R>j&ELVriY*lIV{ zr#tBi+hvy*Hk7R`fz0r_zOtuc`0}7pNKxT5Z>2rXRcFB-wtWg*4d00xD78183W-fB zaEso!Yo5XSPKCB=SF`MK!dsVP2va%}_3N7qb_zYTZ zR%Xl2i>+JP6$ZmD$@;I4@~|;uuDx^27`L`eG};RG?LA2QRkI}q+S~op-YIBTT4`^w zrG3ap`!lmLTiRaiPpq`J1Vft|&=WHt1B1%9HU2a!G;AMSjHPYC=BevxSBrO87o}`< ze{P(PY?_JQYSi4+8f)T3neniOSFow~;{Hy;KPlN|7MAR2E@_C+MeY(?FaB3>`o$Wd z^GMRv?B>meY{yVi!JXhTD+`33&34Vh6^U$i=Yx$b zAmjx*vj@+`g8TkK!N>=&Rvq~V1rJie^X7tvCQ#6vCJY(2b>dUZT{y!*q+j1;8 z(_GLH*t8b@`|G{leu{hF*iQ*Ia$?IH?n=_Z=MT)R%{H=LY_~PCsluKh`l%)>p%q3p zVye^%k!}1K!tIkX6j_72JOSLbPq2T{>aMMbX6n|tyM81c++9DI zwb{DMi~XI|U0Z{8*X~u&72WmMD&*HV-qiFA?rO-EK4EGI4W+1^yZ)~V;S!~cr6CBo zXgMDyIBE!yZ2BIEXO&Mv3pKr#;)ZrqU7U?rO%3oL6pUR1-PwmvLTH%mdJOSx7|)x7 zZRh);2v@y$nqnB5LtVki(i}?3I3C|(vzdXgr*Le;^rfz_Cy3^-|0$bsY}xX4IE*o~ z0S3A{*Jo?d0b%?SE8E3ZwtN_S$;Y%NEu5V<{A2dJAL3(NLfqqR?%YN?y;oz+y@(Vc7ww$bupr#dZD>wQ5-D|7>lbY@Fcc2VFR z?=4cs((z_HtxNS<@P@yDu^Ar_57#NSgbxa54&a0h4ZSa-nL2V__2-ceUN7dFwFSbS zV|8X<n0|y~t&%|{6grOhz`inp4Rl(zagPX`!zhKN-xeF1mTlbT;Wf5# zPYZdAAlvyO)Q^&zyz z)v%21aJ?hNhn*BWb^^yX3?-on)*7Y=^=)a-i&tPT({}9W6#SQjiD(F}kXhzRh;M3L zJPbyg*x;3rq7E@zXXuEtxh7jzd@EEBu)3lzf|*<~@fF-^pG+#atrN}40%7M{UC~## z!Z51#7TRi3j(7~>Yb*~Jv+y0b8h*rVf`RWM|9nph^A}k8&Jz~Mo;qtM^l@w?6`bz| zvoc%0UhHSBeCGwv_wQ9UeD|@_uOZ(L%_bQ5?)A_2lraAtE8i+B-{jX}pyP~>?`g9# zTfScGQ&zrJLGh){jxNJZvJ1dK-sy1Bn0gbY8pit)A)|tf!{! z0cVY#ZY|ozHav+v-8#QkuJ-S&pMvyoz-$g2T)p*^k%(iNHv3FVt zuMC#3>peVhWbN9ICbF{kuq7NfTVSXgNBq-0C#?U{O7{?gndo}<;!qDQtLa`gE3>8R z#lB>vdnj1Cv|6e`w`EI)Cw1GX$z+Qh!3}g1Sk4E28vX@Aw*{9lH2hcuGtqtP1MKH| z`RMjAE3>8R#qQ3r4MTctOFpF6GLChsvAJDu%$P}crw7>G&SAy-@t?i9X4?#o813H? zzX(U%X?4U%t0OiZfE>qtK1Y<9mDxJNi#^Ngh><}#g1W#yA45`&@q8`2=VNH6t}|O; zpu5^X-QNV=RaUwyt#r420%gwEr3$+)aL7RzpuQtzEM4I1?EFFOeGDM}yFjm9JFTu- z8MLcO2^nS!3|lCjxI$Z#{t$FKa0x?~&>q1|UBdh?knVqc zbcdUj1;QR`rQ1G798QLkxKOp2sax7|PE7`R|W< z4)&>IQ%*rFi})GTpdwcKGhC%O^Ch905o^Sr`xTu%Rm$*)NoVJ?>wkkmfk7(Ry5DdY z_W=utJQbeLx?aRXz5y+%VC*7-F#jN)_P;}GPz@;l!=6xU*njvR40pUl+IZM2&3bKH zWr`Pc3(AUCx#JHC^R6osW*)ULy|_#U{^5NHy@LN6!AzI zEP^NI0r+IZ?#dp!Qr#8@&3LamNlc1Kq=#Xb-h;k>?hVn~YL`gHFL>Wxs-onpMj)p1&+2^6kZM6Zq z!Vs{R8PLS-SeTNj8UpFRmS0_KE#F#C8SWTO%6Kim%dFP6b4&Mv-j1@C&W$y0pv+*Q z4V2}|#FQ&D5=m`h{?nnM5?trDyrJ?GIOj@2cJ+NkxH3R3mok*RE2o zcR;J^I(^x!*0$&F=LNllvb;{SdzvYEN~2a+rV>kds>BX9IYx;HJVN8w8OiKqj54U! z{|*g_RYn_xvdR5oHC7!6Z4}!VtMrCZEV8-cD0`a!qRe`pR?uhI&tc-7kuFi_*JfVe z?>6#u6HhnubPJ{$|9{9fyvqiyQe0l-Z(ri+cAk3Zg`&Momr(5$ae0-$D%-&?J273L zy@qLdgVK`m?K9gKPq^Eyy-p9pic5+nvR z7Ej74&M(TFGASn)KcaYto-26;ZtXq1b7^~d`hHXy|1H;jnA2RyR{MZI|B$Eqd3u1S zAMx~Ko_@m9gP4jX&!;^98K(H5#UZ>b&<!hYW#s`PV@9fo}R&Uf%X&K=jYMSC7#7wmv#07fAEK?S~@xZT1pm6U9u#7Q4S#!-?;AJ@cFvV@Yw zlypTXtqUbD)8h3aJ>%b-@DEMqmnC6-E+tnJej7|mwMz!QF0RwX^|`n%{83^Aad90k zj_=~wE{?lEn~!KN4rllwByK(bRT*ym=xXcBH2zyO+B|U!+=Hnk&)5 zP8&;iw1&_=ri7-I+HC60Xz0}v2%2|TS{*bAL#l{NUA$oM!o;P%xHJ@(aB*oYE|GY_ zD%2#pP73}IvlfL}ttlpmMQtOyVevfo&2BA5NH=FQok}`X(Jv(FTav=qdrl=w8Q+TU z>F|$f_#7g)75$JAdmuq+iCs=bg3`v>0s&lFynspI8DAGwI+lR~*=@O7E&n+#z{+d= zfv8?=bfVJDIiJ}3K={Uoah>T&RI=2Er3?)?hJB&=t@uWa?dFa5rxSZblZXR`vo~5Q mx2Mam_6o#Q$@(#9jy4fphJK$UF1R<9r1XW&?9n7;=>G%T&o3hY diff --git a/docs/RefMan/_build/html/Modules.html b/docs/RefMan/_build/html/Modules.html index 3877d2687..47fddecbf 100644 --- a/docs/RefMan/_build/html/Modules.html +++ b/docs/RefMan/_build/html/Modules.html @@ -67,6 +67,7 @@
  • Anonymous Instantiation Arguments
  • Anonymous Import Instantiations
  • Passing Through Module Parameters
    • +
  • Instantiation by Parametrizing Declarations
    • @@ -771,6 +772,98 @@

    Passing Through Module Parameters +

    Instantiation by Parametrizing Declarations

    +

    It is also possible to instantiate a functor parameter without providing +an implementation module. Instead, the declarations in the instantiated +module all get additional parameters corresponding to the functor’s parameters. +This is done by providing _ as the parameter to a functor:

    +
    +
    Instantiation by Parametrizing Declarations
    +
    submodule F where
+  parameter
+    type n : #
+    x : [n]
+
+  f : (fin n) => [n] -> [n]
+  f v = v + x
+
+submodule M = submodule F { _ }
+import submodule M as M
+
    +
    +
    +

    This example defines module M by instantiating F without +a parameter. Here is the resulting type of f:

    +
    Main> :t M::f
+M::f : {n} (fin n) => {x : [n]} -> [n] -> [n]
+
    +
    +

    Note that f has a new type parameter n, and a new value parameter +of a record type. The type parameter n corresponds to the functor’s +type parameter while the record parameter has one field for each value +parameter of the functor.

    +
    +

    Warning

    +

    The order in which type parameters are added to a declaration is not +specified, so you’d have to use a named type application to apply +a type explicitly.

    +
    +

    Functors with multiple parameters may use _ as argument for more +than one parameter, and may also provide implementations for some of +the parameters and use _ for others.

    +

    [Parameter Names] The names of the parameters in the declarations +are the same as the names that are in scope, unless a parameter came +in through a qualified interface import (i.e., the interface import +uses the as clause). In the case the name of the parameter is +computed by replacing the :: with ' because :: may not appear +in type parameters or record fields. For example, if a module had +a parameter I::x, then its _ instantiation will use a +record with a field named I'x.

    +

    [Restrictions] There are some restrictions on functor parameters +that can be defined with _:

    +
    +
      +

    • The functor should not contain other functors nested in it. +This is because it is unclear how to parameterize the parameters of +nested functors.

      • +

    • All values coming through _ parameters should have simple +(i.e., non-polymorphic) types. This is because Cryptol does not +support records with polymorphic fields.

      • +

    • All types and values coming through _ parameters should have +distinct names. This is because the fields in the record and +type names use labels derived. Generally this should not be a +problem unless a functor defined some parameters that have +' in the middle.

      • +
    +
    +

    [Backtick Imports] For backward compatibility, we also provide +syntactic sugar for importing a functor with a single interface parameter +and instantiating it:

    +
    +
    Backtick Import
    +
    submodule F where
+  parameter
+    type n : #
+    x : [n]
+
+  f : (fin n) => [n] -> [n]
+  f v = v + x
+
+import submodule `F
+
    +
    +
    +

    This is equivalent to writing:

    +
    import submodule F { _ }
+
    +
    +

    This, in turn, is syntactic sugar for creating an anonymous module:

    +
    submodule M = F { _ }
+import submodule M
+
    +
    + diff --git a/docs/RefMan/_build/html/RefMan.html b/docs/RefMan/_build/html/RefMan.html index fb0b60319..2e3732e6d 100644 --- a/docs/RefMan/_build/html/RefMan.html +++ b/docs/RefMan/_build/html/RefMan.html @@ -150,6 +150,7 @@

    Cryptol Reference ManualAnonymous Instantiation Arguments
  • Anonymous Import Instantiations
  • Passing Through Module Parameters
    • +
  • Instantiation by Parametrizing Declarations
    • diff --git a/docs/RefMan/_build/html/_sources/Modules.rst.txt b/docs/RefMan/_build/html/_sources/Modules.rst.txt index c20fc4fc3..cbf82b8c3 100644 --- a/docs/RefMan/_build/html/_sources/Modules.rst.txt +++ b/docs/RefMan/_build/html/_sources/Modules.rst.txt @@ -735,6 +735,109 @@ in an instantiation. Here is an example: x = 5 +Instantiation by Parametrizing Declarations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +It is also possible to instantiate a functor parameter *without* providing +an implementation module. Instead, the declarations in the instantiated +module all get additional parameters corresponding to the functor's parameters. +This is done by providing ``_`` as the parameter to a functor: + +.. code-block:: cryptol + :caption: Instantiation by Parametrizing Declarations + + submodule F where + parameter + type n : # + x : [n] + + f : (fin n) => [n] -> [n] + f v = v + x + + submodule M = submodule F { _ } + import submodule M as M + +This example defines module ``M`` by instantiating ``F`` without +a parameter. Here is the resulting type of ``f``: + +.. code-block:: + + Main> :t M::f + M::f : {n} (fin n) => {x : [n]} -> [n] -> [n] + +Note that ``f`` has a new type parameter ``n``, and a new value parameter +of a record type. The type parameter ``n`` corresponds to the functor's +type parameter while the record parameter has one field for each value +parameter of the functor. + +.. warning:: + + The order in which type parameters are added to a declaration is not + specified, so you'd have to use a *named* type application to apply + a type explicitly. + +Functors with multiple parameters may use ``_`` as argument for more +than one parameter, and may also provide implementations for some of +the parameters and use ``_`` for others. + +**[Parameter Names]** The names of the parameters in the declarations +are the same as the names that are in scope, unless a parameter came +in through a qualified interface import (i.e., the interface import +uses the ``as`` clause). In the case the name of the parameter is +computed by replacing the ``::`` with ``'`` because ``::`` may not appear +in type parameters or record fields. For example, if a module had +a parameter ``I::x``, then its ``_`` instantiation will use a +record with a field named ``I'x``. + +**[Restrictions]** There are some restrictions on functor parameters +that can be defined with ``_``: + + * The functor should not contain other functors nested in it. + This is because it is unclear how to parameterize the parameters of + nested functors. + + * All values coming through ``_`` parameters should have simple + (i.e., non-polymorphic) types. This is because Cryptol does not + support records with polymorphic fields. + + * All types and values coming through ``_`` parameters should have + distinct names. This is because the fields in the record and + type names use labels derived. Generally this should not be a + problem unless a functor defined some parameters that have + ``'`` in the middle. + + +**[Backtick Imports]** For backward compatibility, we also provide +syntactic sugar for importing a functor with a single interface parameter +and instantiating it: + +.. code-block:: cryptol + :caption: Backtick Import + + submodule F where + parameter + type n : # + x : [n] + + f : (fin n) => [n] -> [n] + f v = v + x + + import submodule `F + +This is equivalent to writing: + +.. code-block:: cryptol + + import submodule F { _ } + +This, in turn, is syntactic sugar for creating an anonymous module: + +.. code-block:: cryptol + + submodule M = F { _ } + import submodule M + + diff --git a/docs/RefMan/_build/html/searchindex.js b/docs/RefMan/_build/html/searchindex.js index 751034bba..0e4fc4063 100644 --- a/docs/RefMan/_build/html/searchindex.js +++ b/docs/RefMan/_build/html/searchindex.js @@ -1 +1 @@ -Search.setIndex({docnames:["BasicSyntax","BasicTypes","Expressions","FFI","Modules","OverloadedOperations","RefMan","TypeDeclarations"],envversion:{"sphinx.domains.c":2,"sphinx.domains.changeset":1,"sphinx.domains.citation":1,"sphinx.domains.cpp":4,"sphinx.domains.index":1,"sphinx.domains.javascript":2,"sphinx.domains.math":2,"sphinx.domains.python":3,"sphinx.domains.rst":2,"sphinx.domains.std":2,"sphinx.ext.todo":2,sphinx:56},filenames:["BasicSyntax.rst","BasicTypes.rst","Expressions.rst","FFI.rst","Modules.rst","OverloadedOperations.rst","RefMan.rst","TypeDeclarations.rst"],objects:{},objnames:{},objtypes:{},terms:{"0":[0,1,2,3],"0254":0,"0b":0,"0b1010":0,"0b1010111":0,"0b11010":0,"0b11111110":0,"0b_0000_0010":0,"0o":0,"0o1234":0,"0o376":0,"0x":0,"0x00000003":3,"0x01":4,"0x02":4,"0x03":4,"0x04":4,"0x0f":3,"0x1234":0,"0x30":0,"0x_ffff_ffea":0,"0xaf":3,"0xf":3,"0xfe":0,"1":[0,1,2,3,4,7],"10":[0,1,3,4],"100":1,"11":4,"12":[0,4],"13":2,"15":1,"16":[0,3],"1p4":0,"2":[0,1,2,3,4,7],"20":[1,3],"22":2,"25":1,"254":0,"26":4,"2e3":0,"3":[0,1,2,4,7],"30":[1,4],"32":[3,4],"33":2,"4":[0,3],"5":[0,1,2,4],"6":[0,7],"64":[0,3],"7":[0,2,4],"8":[2,3,4],"9":2,"case":[3,4],"do":[0,2,3,4,7],"float":[0,6],"function":[0,4,6,7],"import":[0,1,2,6],"long":0,"new":[4,7],"public":4,"return":6,"static":[0,3],"true":[1,3],"try":[3,4],"void":3,"while":[0,1,3],A:[0,1,3,4,7],For:[0,1,2,3,4,7],If:[2,3,4],In:[3,4],It:[3,4],On:3,Such:[0,4],That:3,The:[0,1,2,3,4],Then:[3,4],There:[0,1],These:3,To:4,_:[0,1],a1:3,ab:5,abbrevi:1,abl:4,about:4,abov:[2,3,4],access:[2,3,6],accommod:2,across:[3,4],actual:[0,3],ad:[2,3,4],add:[3,4],addit:[0,4],adjac:3,after:3,ak:3,alias:0,all:[0,2,3,4,7],alloc:3,allow:[0,3,4,7],along:3,alphabet:1,alreadi:3,also:[0,1,3,4],alwai:3,an:[0,1,2,3,6],ani:[3,4,7],annot:6,anonym:6,anoth:4,appear:[1,4,7],appli:[0,3],applic:2,appropri:3,ar:[0,1,2,3,4,7],arbitrari:3,arbitrarili:0,argument:[3,6,7],arithmet:[1,6],arr:1,arrai:3,associ:0,assum:0,assumpt:[0,4],attempt:0,automat:[2,3],avail:4,avoid:4,awai:4,b:[0,3,4,5,7],back:1,backtick:2,baddef:1,base:[0,2],basic:6,becaus:[0,3,4],befor:[3,4],begin:0,behav:3,behavior:[0,1,3],being:4,belong:0,between:[0,6],binari:[0,3],bind:[1,3],bit:[0,1,2,4,5,6],bitvector:1,block:[0,6],bodi:[3,7],both:[1,3,4],bound:[1,3],brace:1,branch:[0,2],bring:[4,7],built:[3,6],c1:3,c:6,call:[1,3,4,6],can:[0,1,2,3,4,7],cannot:[0,2],care:3,cc:3,ceil:[0,5],certain:3,chang:0,charact:0,check:[0,3],checker:[0,7],chosen:2,clash:4,claus:4,clear:3,close:0,closest:0,cmp:5,cn:3,code:[4,6],collect:[1,7],collis:4,combin:4,comma:1,command:3,comment:6,compar:1,comparison:6,compil:6,complement:5,complex:1,compon:[1,3],comprehens:1,comput:[0,1],concaten:1,concret:4,condit:6,consid:[0,4,7],consist:0,constant:[3,4],constrain:0,constraint:6,construct:[1,2,4],contain:[0,1,3,4],content:4,context:[0,2],contigu:3,control:0,conveni:4,convent:3,convers:3,convert:6,correct:3,correspond:[2,3],could:3,coupl:4,cours:4,creat:7,cry:[3,4],cryptol:[0,2,4],cryptolpath:4,cumbersom:[3,4],curli:1,current:3,curri:3,data:1,dealloc:3,decim:0,decis:0,declar:[3,4,6],defin:[0,1,3,4,7],definit:[0,1,2,4],defint:2,degre:0,demot:[0,6],depend:[0,3],deriv:4,describ:[3,4],descript:1,desrib:4,determin:[0,1],differ:[0,3,4],digit:0,dimens:3,dimension:1,directli:[3,7],directori:[3,4],distance2:1,distinct:7,divis:[0,6],dll:3,document:0,doe:[0,3],don:3,done:[3,4],doubl:3,down:[0,1],downward:1,drop:0,dylib:3,dynam:3,dynamiclib:3,e11:1,e12:1,e1:1,e21:1,e22:1,e2:1,e3:1,e:[0,1,4,5],each:[0,3,4,7],earlier:3,easi:4,easier:4,effect:0,either:[0,3,4],element:[1,2,3],els:[0,2,4],empti:3,enclos:[1,4],end:[0,4],english:0,enough:3,entri:1,enumer:1,environment:0,eq:5,equal:[0,1,6,7],equat:1,equival:4,error:[3,4],etc:0,evalu:[2,6],even:[0,7],everi:7,everyth:4,ex:1,exact:3,examin:1,exampl:[0,1,2,4,6],except:[0,3,4],exclus:1,exhaust:0,exist:[4,7],expand:3,explicit:[1,4,6],explicitli:[0,3],expon:0,exponenti:0,express:[0,1,4,6,7],extend:4,extens:3,extern:0,extra:3,extract:7,f1:3,f2:3,f:[0,1,2,3,4],fact:0,fals:[1,3],famili:0,few:4,ffi:3,field:[3,5,6,7],file:[3,4],fill:4,fin:[0,3,4],finit:[1,2],first:[0,1,3,4],fit:3,fix:[0,1,3],flatten:3,float32:3,float64:3,floor:5,fn:3,follow:[0,1,2,3,4],foo:3,foreign:6,form:7,fpic:3,fraction:0,from:[0,1,2,3,4],frominteg:5,front:1,fulli:3,functoin:0,functor:4,furthermor:3,g:[0,2,4],gener:[1,3],get:1,getfst:1,given:3,glu:4,gmp:3,good:4,group:[0,4,7],guard:6,h:[2,3,4],ha:[0,1,2,3],had:7,handi:1,handl:3,happen:4,hash:4,have:[0,1,2,3,4,7],header:3,help:[3,4],helper1:4,helper2:4,helper:4,here:[0,2,4],hexadecim:0,hide:[0,6],hierarch:6,high:3,highest:0,hold:[1,3],how:3,howev:3,i:[0,1,4],identifi:[1,4,6],ignor:3,impl1:4,impl2:4,impl:4,implement:[3,4],implicit:6,implict:0,impos:4,improv:[0,3],in0:3,in1_a:3,in1_b:3,includ:[0,3],indent:[0,4],independ:0,index:1,individu:3,inf:[1,5],infer:[0,2],inffrom:5,inffromthen:5,infinit:1,infix:[0,6],infixl:0,infixr:0,inform:1,init:3,input:3,instanc:3,instanti:6,instead:[0,3,4,7],insuffici:1,integ:[0,2,3,5,7],integr:[3,6],intend:4,interfac:[0,6],introduc:4,invalid:1,involv:3,irrelev:7,isposit:1,issu:0,its:[0,3,4],itself:[3,4],j:[1,4],just:[3,4,7],k:3,keword:4,keyword:[4,6],kind:[2,3],know:3,known:1,l:[1,3],label:1,lambda:[1,2],languag:[0,3],larg:[2,3],larger:3,last:[0,2,3],layout:[4,6],left:[0,1],len:0,length:[0,1],less:0,let:[0,3],letter:0,level:[4,6],lexicograph:1,lg2:0,libffi:3,librari:3,lift:1,like:[3,4,7],limit:3,line:[0,7],link:4,linux:3,list:[0,3,6],liter:[2,6],load:3,local:[0,4,6],locat:[1,4],logarithm:0,logic:6,longer_nam:0,longernam:0,look:[3,4],lowest:0,m:4,maco:3,mai:[0,1,2,3,4,7],main:3,make:4,manag:[3,6],mani:[3,4],manual:3,map:3,mark:0,match:[0,1,3],math:6,matter:3,max:[0,5],maximum:0,mayb:4,mean:[0,3],member:7,memori:6,mention:[3,7],might:4,min:[0,5],minimum:0,mirror:1,modifi:3,modul:[0,3,6],modulu:0,more:[0,4],moreov:7,most:[1,4],mpq_t:3,mpz_q:3,mpz_t:3,multidimension:3,multipl:[0,1,2,3,4],must:[0,3,4],my:4,myf:4,n1:3,n2:3,n:[0,1,3,4],name1:0,name2:0,name:[0,1,3,6,7],need:[0,2,3,4],negat:5,nest:[0,1,3,6],newt:7,newtyp:[0,4,6],ni:3,nk:3,non:[0,3],nonzero:3,notat:[0,1,2,4],note:[1,3,4],noth:4,notion:4,now:3,number:[0,1,2,3],numer:[3,4,6],o:3,obtain:[1,3,4],occasion:4,octal:0,often:1,old:1,onc:[3,4],one:[0,2,3,4],onli:[0,1,3,4,7],open:0,oper:[3,6],option:[0,7],order:[1,3,4],ordinari:4,organ:0,other:[0,3,4,7],otherwis:7,our:3,out:3,out_0:3,out_1:3,outer:4,output:3,outsid:4,over:0,overal:6,overload:[0,6],overview:2,ox:0,p11:1,p12:1,p1:1,p21:1,p22:1,p2:1,p3:1,p4:1,p:[0,1,4],packag:1,pad:[0,3],pair:2,paramet:[0,2,6],parameter:6,paren:2,parenthes:1,parmaet:4,pass:[2,3,6],pattern:[1,2],piec:3,place:4,platform:6,point:[1,6],pointer:3,pointwis:1,polymorph:[2,3],polynomi:0,portabl:3,posit:1,possibl:[2,3,4],practic:[3,4],pragma:0,pre:7,preced:[2,4],precis:[0,3],prefix:[0,4,6],presum:4,previou:[0,4],prime:0,primit:0,primtiv:2,principl:0,privat:[0,6],process:3,program:1,programm:0,project:7,properti:0,prototyp:3,prove:0,provid:[0,2,4],pt:1,purpos:[1,7],qualifi:6,quick:6,quickli:1,quit:[0,1,4],r:1,rather:0,ration:[0,3],read:3,readabl:[0,3],recip:5,record:[6,7],recurs:[3,4,7],reduc:4,refer:4,reject:0,rel:1,relat:4,remain:4,repl:1,repres:[0,3],represent:[0,3],requir:[0,3,4],respect:3,result:[0,1,2,3,4],right:[0,1],ring:5,rotat:1,round:[0,6],roundawai:5,roundtoeven:5,rule:3,runtim:3,s:[0,2,3,4],same:[0,1,3,4,7],satisfi:[0,3],scope:[2,4,7],search:4,section:[2,3,4],see:[0,4],selector:1,semant:4,separ:[1,4],seq:7,sequenc:[0,6],set:[0,1,3],sha256:4,shadow:4,shape:1,share:3,shift:1,should:[0,1,2,3],sign:[1,6],signatur:[3,6],signedcmp:5,similar:[0,3],similarli:1,simpl:[3,4],simpli:0,sinc:[3,4],singl:4,site:7,situat:4,size:[0,1,3],size_t:3,slight:4,smaller:3,so:[0,1,2,3,4],some:[0,4],someth:3,sometim:4,somewher:4,sort:4,sourc:[3,4],special:0,specif:3,specifi:[0,2,4],split:[1,3],standard:3,start:[0,1],statement:0,step:[1,4],still:3,store:3,straight:4,stream:1,stride:1,structur:[4,6],sub:[1,4],submdul:4,submodul:[0,4],submould:4,subtract:0,suffici:[1,2],sugar:[2,4],suitabl:2,sum:7,sumbodul:4,support:[0,4,6],suppos:3,sure:4,symbol:[0,3,4],synonym:[4,6],syntact:4,syntax:[1,2,6],system:[3,4],t1:[1,3],t2:[1,3],t3:1,t:[0,1,2,3,4,7],tabl:[0,3],take:3,tend:4,term:0,termin:0,test:3,text:0,than:[0,3,4],thei:[0,1,3,4,7],them:4,themselv:3,thi:[0,1,2,3,4],thing:4,those:[1,4],though:7,three:1,through:[1,6],thu:[1,4],ti:3,time:4,tm:3,tn:3,togeth:[1,4],tointeg:5,too:3,top:[3,4],tr:3,translat:3,transpar:7,treat:[3,4,7],trunc:5,tupl:6,two:[0,1,2,4,7],typaram:2,type:[4,6],typecheck:7,typeclass:7,u1:3,u2:3,u:3,ui:3,uint16_t:3,uint32_t:3,uint64_t:3,uint8_t:3,un:3,unari:[0,2],undefin:3,underscor:0,understand:[3,4],unfold:7,uniniti:3,unlik:7,up:0,updat:6,updateend:1,updatesend:1,us:[0,1,2,3,4,7],usag:6,user:7,usual:2,v1:3,v2:3,valid:1,valu:[0,1,4,6,7],variabl:[2,3],variat:4,varieti:0,vector:6,version:3,vi:3,via:1,vn:3,w:4,wa:4,wai:[1,3,4],want:[3,4],warn:0,warnnonexhaustiveconstraintguard:0,we:[1,3,4],weakest:2,what:3,when:[0,1,2,3,4],where:[0,1,2,3,4],wherea:1,which:[0,2,3,4,7],whole:[2,3,4],width:[0,4],window:3,wise:1,withing:4,without:4,word:[1,3],work:[3,4],worth:3,would:[3,4,7],write:[0,1,3],written:[0,1,2,3,7],x:[0,1,2,3,4,7],xpo:1,xs:[0,1],y:[0,1,2,3,4],you:[2,3,4],your:3,ypo:1,z:[0,2,3,4],zero:[2,3,6]},titles:["Basic Syntax","Basic Types","Expressions","Foreign Function Interface","Modules","Overloaded Operations","Cryptol Reference Manual","Type Declarations"],titleterms:{"float":3,"function":[1,2,3],"import":4,"return":3,access:1,an:4,annot:2,anonym:4,argument:[2,4],arithmet:5,basic:[0,1,3,5],between:3,bit:3,block:[2,4],built:0,c:3,call:2,code:3,comment:0,comparison:5,compil:3,condit:2,constraint:[0,4],convert:3,cryptol:[3,6],declar:[0,2,7],demot:2,divis:5,equal:5,evalu:3,exampl:3,explicit:2,express:2,field:1,foreign:3,guard:0,hide:4,hierarch:4,identifi:0,implicit:4,infix:2,instanti:[2,4],integr:5,interfac:[3,4],keyword:0,layout:0,level:0,list:4,liter:0,local:2,logic:5,manag:4,manual:6,math:3,memori:3,modul:4,name:4,nest:4,newtyp:7,numer:[0,2],oper:[0,1,2,5],overal:3,overload:5,paramet:[3,4],parameter:4,pass:4,platform:3,point:3,preced:0,prefix:2,privat:4,qualifi:4,quick:3,record:[1,3],refer:[3,6],round:5,sequenc:[1,3],sign:5,signatur:0,structur:3,support:3,synonym:[3,7],syntax:0,through:4,todo:[0,2],tupl:[1,3],type:[0,1,2,3,7],updat:1,usag:3,valu:[2,3],vector:3,zero:5}}) \ No newline at end of file +Search.setIndex({docnames:["BasicSyntax","BasicTypes","Expressions","FFI","Modules","OverloadedOperations","RefMan","TypeDeclarations"],envversion:{"sphinx.domains.c":2,"sphinx.domains.changeset":1,"sphinx.domains.citation":1,"sphinx.domains.cpp":4,"sphinx.domains.index":1,"sphinx.domains.javascript":2,"sphinx.domains.math":2,"sphinx.domains.python":3,"sphinx.domains.rst":2,"sphinx.domains.std":2,"sphinx.ext.todo":2,sphinx:56},filenames:["BasicSyntax.rst","BasicTypes.rst","Expressions.rst","FFI.rst","Modules.rst","OverloadedOperations.rst","RefMan.rst","TypeDeclarations.rst"],objects:{},objnames:{},objtypes:{},terms:{"0":[0,1,2,3],"0254":0,"0b":0,"0b1010":0,"0b1010111":0,"0b11010":0,"0b11111110":0,"0b_0000_0010":0,"0o":0,"0o1234":0,"0o376":0,"0x":0,"0x00000003":3,"0x01":4,"0x02":4,"0x03":4,"0x04":4,"0x0f":3,"0x1234":0,"0x30":0,"0x_ffff_ffea":0,"0xaf":3,"0xf":3,"0xfe":0,"1":[0,1,2,3,4,7],"10":[0,1,3,4],"100":1,"11":4,"12":[0,4],"13":2,"15":1,"16":[0,3],"1p4":0,"2":[0,1,2,3,4,7],"20":[1,3],"22":2,"25":1,"254":0,"26":4,"2e3":0,"3":[0,1,2,4,7],"30":[1,4],"32":[3,4],"33":2,"4":[0,3],"5":[0,1,2,4],"6":[0,7],"64":[0,3],"7":[0,2,4],"8":[2,3,4],"9":2,"case":[3,4],"do":[0,2,3,4,7],"float":[0,6],"function":[0,4,6,7],"import":[0,1,2,6],"long":0,"new":[4,7],"public":4,"return":6,"static":[0,3],"true":[1,3],"try":[3,4],"void":3,"while":[0,1,3,4],A:[0,1,3,4,7],For:[0,1,2,3,4,7],If:[2,3,4],In:[3,4],It:[3,4],On:3,Such:[0,4],That:3,The:[0,1,2,3,4],Then:[3,4],There:[0,1,4],These:3,To:4,_:[0,1,4],a1:3,ab:5,abbrevi:1,abl:4,about:4,abov:[2,3,4],access:[2,3,6],accommod:2,across:[3,4],actual:[0,3],ad:[2,3,4],add:[3,4],addit:[0,4],adjac:3,after:3,ak:3,alias:0,all:[0,2,3,4,7],alloc:3,allow:[0,3,4,7],along:3,alphabet:1,alreadi:3,also:[0,1,3,4],alwai:3,an:[0,1,2,3,6],ani:[3,4,7],annot:6,anonym:6,anoth:4,appear:[1,4,7],appli:[0,3,4],applic:[2,4],appropri:3,ar:[0,1,2,3,4,7],arbitrari:3,arbitrarili:0,argument:[3,6,7],arithmet:[1,6],arr:1,arrai:3,associ:0,assum:0,assumpt:[0,4],attempt:0,automat:[2,3],avail:4,avoid:4,awai:4,b:[0,3,4,5,7],back:1,backtick:[2,4],backward:4,baddef:1,base:[0,2],basic:6,becaus:[0,3,4],becom:[],befor:[3,4],begin:0,behav:3,behavior:[0,1,3],being:4,belong:0,between:[0,6],binari:[0,3],bind:[1,3],bit:[0,1,2,4,5,6],bitvector:1,block:[0,6],bodi:[3,7],both:[1,3,4],bound:[1,3],brace:1,branch:[0,2],bring:[4,7],built:[3,6],c1:3,c:6,call:[1,3,4,6],came:4,can:[0,1,2,3,4,7],cannot:[0,2],care:3,cc:3,ceil:[0,5],certain:3,chang:0,charact:0,check:[0,3],checker:[0,7],chosen:2,clash:4,claus:4,clear:3,close:0,closest:0,cmp:5,cn:3,code:[4,6],collect:[1,7],collis:4,combin:4,come:4,comma:1,command:3,comment:6,compar:1,comparison:6,compat:4,compil:6,complement:5,complex:1,compon:[1,3],comprehens:1,comput:[0,1,4],concaten:1,concret:4,condit:6,consid:[0,4,7],consist:0,constant:[3,4],constrain:0,constraint:6,construct:[1,2,4],contain:[0,1,3,4],content:4,context:[0,2],contigu:3,control:0,conveni:4,convent:3,convers:3,convert:6,correct:3,correspond:[2,3,4],could:3,coupl:4,cours:4,creat:[4,7],cry:[3,4],cryptol:[0,2,4],cryptolpath:4,cumbersom:[3,4],curli:1,current:3,curri:3,d:4,data:1,dealloc:3,decim:0,decis:0,declar:[3,6],defin:[0,1,3,4,7],definit:[0,1,2,4],defint:2,degre:0,demot:[0,6],depend:[0,3],deriv:4,describ:[3,4],descript:1,desrib:4,determin:[0,1],differ:[0,3,4],digit:0,dimens:3,dimension:1,directli:[3,7],directori:[3,4],distance2:1,distinct:[4,7],divis:[0,6],dll:3,document:0,doe:[0,3,4],don:3,done:[3,4],doubl:3,down:[0,1],downward:1,drop:0,dylib:3,dynam:3,dynamiclib:3,e11:1,e12:1,e1:1,e21:1,e22:1,e2:1,e3:1,e:[0,1,4,5],each:[0,3,4,7],earlier:3,easi:4,easier:4,effect:0,either:[0,3,4],element:[1,2,3],els:[0,2,4],empti:3,enclos:[1,4],end:[0,4],english:0,enough:3,entri:1,enumer:1,environment:0,eq:5,equal:[0,1,6,7],equat:1,equival:4,error:[3,4],etc:0,evalu:[2,6],even:[0,7],everi:7,everyth:4,ex:1,exact:3,examin:1,exampl:[0,1,2,4,6],except:[0,3,4],exclus:1,exhaust:0,exist:[4,7],expand:3,explicit:[1,4,6],explicitli:[0,3,4],expon:0,exponenti:0,express:[0,1,4,6,7],extend:4,extens:3,extern:0,extra:3,extract:7,f1:3,f2:3,f:[0,1,2,3,4],fact:0,fals:[1,3],famili:0,few:4,ffi:3,field:[3,4,5,6,7],file:[3,4],fill:4,fin:[0,3,4],finit:[1,2],first:[0,1,3,4],fit:3,fix:[0,1,3],flatten:3,float32:3,float64:3,floor:5,fn:3,follow:[0,1,2,3,4],foo:3,foreign:6,form:7,fpic:3,fraction:0,from:[0,1,2,3,4],frominteg:5,front:1,fulli:3,functoin:0,functor:4,furthermor:3,g:[0,2,4],gener:[1,3,4],get:[1,4],getfst:1,given:3,glu:4,gmp:3,good:4,group:[0,4,7],guard:6,h:[2,3,4],ha:[0,1,2,3,4],had:[4,7],handi:1,handl:3,happen:4,hash:4,have:[0,1,2,3,4,7],header:3,help:[3,4],helper1:4,helper2:4,helper:4,here:[0,2,4],hexadecim:0,hide:[0,6],hierarch:6,high:3,highest:0,hold:[1,3],how:[3,4],howev:3,i:[0,1,4],identifi:[1,4,6],ignor:3,impl1:4,impl2:4,impl:4,implement:[3,4],implicit:6,implict:0,impo:[],impos:4,improv:[0,3],in0:3,in1_a:3,in1_b:3,includ:[0,3],indent:[0,4],independ:0,index:1,individu:3,inf:[1,5],infer:[0,2],inffrom:5,inffromthen:5,infinit:1,infix:[0,6],infixl:0,infixr:0,inform:1,init:3,input:3,instanc:3,instanti:6,instead:[0,3,4,7],instnati:[],insuffici:1,integ:[0,2,3,5,7],integr:[3,6],intend:4,interfac:[0,6],introduc:4,invalid:1,involv:3,irrelev:7,isposit:1,issu:0,its:[0,3,4],itself:[3,4],j:[1,4],just:[3,4,7],k:3,keword:4,keyword:[4,6],kind:[2,3],know:3,known:1,l:[1,3],label:[1,4],lambda:[1,2],languag:[0,3],larg:[2,3],larger:3,last:[0,2,3],layout:[4,6],left:[0,1],len:0,length:[0,1],less:0,let:[0,3],letter:0,level:[4,6],lexicograph:1,lg2:0,libffi:3,librari:3,lift:1,like:[3,4,7],limit:3,line:[0,7],link:4,linux:3,list:[0,3,6],liter:[2,6],load:3,local:[0,4,6],locat:[1,4],logarithm:0,logic:6,longer_nam:0,longernam:0,look:[3,4],lowest:0,m:4,maco:3,mai:[0,1,2,3,4,7],main:[3,4],make:4,manag:[3,6],mani:[3,4],manual:3,map:3,mark:0,match:[0,1,3],math:6,matter:3,max:[0,5],maximum:0,mayb:4,mean:[0,3],member:7,memori:6,mention:[3,7],middl:4,might:4,min:[0,5],minimum:0,mirror:1,mix:[],modifi:3,modul:[0,3,6],modulu:0,more:[0,4],moreov:7,most:[1,4],mpq_t:3,mpz_q:3,mpz_t:3,multidimension:3,multipl:[0,1,2,3,4],must:[0,3,4],my:4,myf:4,n1:3,n2:3,n:[0,1,3,4],name1:0,name2:0,name:[0,1,3,6,7],need:[0,2,3,4],negat:5,nest:[0,1,3,6],newt:7,newtyp:[0,4,6],ni:3,nk:3,non:[0,3,4],nonzero:3,normal:[],notat:[0,1,2,4],note:[1,3,4],noth:4,notion:4,now:3,number:[0,1,2,3],numer:[3,4,6],o:3,obtain:[1,3,4],occasion:4,octal:0,often:1,old:1,onc:[3,4],one:[0,2,3,4],onli:[0,1,3,4,7],open:0,oper:[3,6],option:[0,7],order:[1,3,4],ordinari:4,organ:0,other:[0,3,4,7],otherwis:7,our:3,out:3,out_0:3,out_1:3,outer:4,output:3,outsid:4,over:0,overal:6,overload:[0,6],overview:2,ox:0,p11:1,p12:1,p1:1,p21:1,p22:1,p2:1,p3:1,p4:1,p:[0,1,4],packag:1,pad:[0,3],pair:2,paramet:[0,2,6],parameter:6,parametr:6,paren:2,parenthes:1,parmaet:4,pass:[2,3,6],pattern:[1,2],piec:3,place:4,platform:6,point:[1,6],pointer:3,pointwis:1,polymorph:[2,3,4],polynomi:0,portabl:3,posit:1,possibl:[2,3,4],practic:[3,4],pragma:0,pre:7,preced:[2,4],precis:[0,3],prefix:[0,4,6],presum:4,previou:[0,4],prime:0,primit:0,primtiv:2,principl:0,privat:[0,6],problem:4,process:3,program:1,programm:0,project:7,properti:0,prototyp:3,prove:0,provid:[0,2,4],pt:1,purpos:[1,7],qualifi:6,quick:6,quickli:1,quit:[0,1,4],r:1,rather:0,ration:[0,3],read:3,readabl:[0,3],recip:5,record:[4,6,7],recurs:[3,4,7],reduc:4,refer:4,reject:0,rel:1,relat:4,remain:4,repl:1,replac:4,repres:[0,3],represent:[0,3],requir:[0,3,4],respect:3,restrict:4,result:[0,1,2,3,4],right:[0,1],ring:5,rotat:1,round:[0,6],roundawai:5,roundtoeven:5,rule:3,runtim:3,s:[0,2,3,4],same:[0,1,3,4,7],satisfi:[0,3],scope:[2,4,7],search:4,section:[2,3,4],see:[0,4],selector:1,semant:4,separ:[1,4],seq:7,sequenc:[0,6],set:[0,1,3],sha256:4,shadow:4,shape:1,share:3,shift:1,should:[0,1,2,3,4],sign:[1,6],signatur:[3,6],signedcmp:5,similar:[0,3],similarli:1,simpl:[3,4],simpli:0,sinc:[3,4],singl:4,site:7,situat:4,size:[0,1,3],size_t:3,slight:4,smaller:3,so:[0,1,2,3,4],some:[0,4],someth:3,sometim:4,somewher:4,sort:4,sourc:[3,4],special:0,specif:3,specifi:[0,2,4],split:[1,3],standard:3,start:[0,1],statement:0,step:[1,4],still:3,store:3,straight:4,stream:1,stride:1,structur:[4,6],sub:[1,4],submdul:4,submodul:[0,4],submould:4,subtract:0,suffici:[1,2],sugar:[2,4],suitabl:2,sum:7,sumbodul:4,support:[0,4,6],suppos:3,sure:4,symbol:[0,3,4],synonym:[4,6],syntact:4,syntax:[1,2,6],system:[3,4],t1:[1,3],t2:[1,3],t3:1,t:[0,1,2,3,4,7],tabl:[0,3],take:3,tend:4,term:0,termin:0,test:3,text:0,than:[0,3,4],thei:[0,1,3,4,7],them:4,themselv:3,thi:[0,1,2,3,4],thing:4,those:[1,4],though:7,three:1,through:[1,6],thu:[1,4],ti:3,time:4,tm:3,tn:3,togeth:[1,4],tointeg:5,too:3,top:[3,4],tr:3,translat:3,transpar:7,treat:[3,4,7],trunc:5,tupl:6,turn:4,two:[0,1,2,4,7],typaram:2,type:[4,6],typecheck:7,typeclass:7,u1:3,u2:3,u:3,ui:3,uint16_t:3,uint32_t:3,uint64_t:3,uint8_t:3,un:3,unari:[0,2],unclear:4,undefin:3,underscor:0,understand:[3,4],unfold:7,uniniti:3,unless:4,unlik:7,up:0,updat:6,updateend:1,updatesend:1,us:[0,1,2,3,4,7],usag:6,user:7,usual:2,v1:3,v2:3,v:4,valid:1,valu:[0,1,4,6,7],variabl:[2,3],variat:4,varieti:0,vector:6,version:3,vi:3,via:1,vn:3,w:4,wa:4,wai:[1,3,4],want:[3,4],warn:0,warnnonexhaustiveconstraintguard:0,we:[1,3,4],weakest:2,what:3,when:[0,1,2,3,4],where:[0,1,2,3,4],wherea:1,which:[0,2,3,4,7],whole:[2,3,4],width:[0,4],window:3,wise:1,withing:4,without:4,word:[1,3],work:[3,4],worth:3,would:[3,4,7],write:[0,1,3,4],written:[0,1,2,3,7],x:[0,1,2,3,4,7],xpo:1,xs:[0,1],y:[0,1,2,3,4],you:[2,3,4],your:3,ypo:1,z:[0,2,3,4],zero:[2,3,6]},titles:["Basic Syntax","Basic Types","Expressions","Foreign Function Interface","Modules","Overloaded Operations","Cryptol Reference Manual","Type Declarations"],titleterms:{"float":3,"function":[1,2,3],"import":4,"return":3,access:1,an:4,annot:2,anonym:4,argument:[2,4],arithmet:5,basic:[0,1,3,5],between:3,bit:3,block:[2,4],built:0,c:3,call:2,code:3,comment:0,comparison:5,compil:3,condit:2,constraint:[0,4],convert:3,cryptol:[3,6],declar:[0,2,4,7],demot:2,divis:5,equal:5,evalu:3,exampl:3,explicit:2,express:2,field:1,foreign:3,guard:0,hide:4,hierarch:4,identifi:0,implicit:4,infix:2,instanti:[2,4],integr:5,interfac:[3,4],keyword:0,layout:0,level:0,list:4,liter:0,local:2,logic:5,manag:4,manual:6,math:3,memori:3,modul:4,name:4,nest:4,newtyp:7,numer:[0,2],oper:[0,1,2,5],overal:3,overload:5,paramet:[3,4],parameter:4,parametr:4,pass:4,platform:3,point:3,preced:0,prefix:2,privat:4,qualifi:4,quick:3,record:[1,3],refer:[3,6],round:5,sequenc:[1,3],sign:5,signatur:0,structur:3,support:3,synonym:[3,7],syntax:0,through:4,todo:[0,2],tupl:[1,3],type:[0,1,2,3,7],updat:1,usag:3,valu:[2,3],vector:3,zero:5}}) \ No newline at end of file