diff --git a/crucible-mir-comp/src/Mir/Compositional/State.hs b/crucible-mir-comp/src/Mir/Compositional/State.hs index 3351f79419..f339dd757a 100644 --- a/crucible-mir-comp/src/Mir/Compositional/State.hs +++ b/crucible-mir-comp/src/Mir/Compositional/State.hs @@ -4,7 +4,6 @@ module Mir.Compositional.State where import Control.Monad(foldM) -import qualified Data.ByteString as BS import Data.IORef import Data.Set(Set) import qualified Data.Set as Set @@ -47,7 +46,6 @@ newMirState = sc <- SAW.mkSharedContext SAW.scLoadPreludeModule sc SAW.scLoadCryptolModule sc - let ?fileReader = BS.readFile env <- newIORef =<< SAW.initCryptolEnv sc unintRef <- newIORef mempty sawcoreState <- SAW.newSAWCoreState sc diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 5b9b228222..c270d444b9 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -17,7 +17,6 @@ where import Control.Lens (use, (^.), (^?), to, ix) import Control.Monad import Control.Monad.IO.Class -import qualified Data.ByteString as BS import Data.IORef import qualified Data.Kind as Kind import Data.String (fromString) @@ -237,16 +236,15 @@ loadCryptolFunc col sig modulePath name = do sym <- getSymInterface let mirState = sym ^. W4.userState let sc = mirSharedContext mirState - let ?fileReader = BS.readFile ce <- liftIO (readIORef (mirCryEnv mirState)) let modName = Cry.textToModName modulePath ce' <- liftIO $ SAW.importCryptolModule sc ce (Right modName) Nothing False SAW.PublicAndPrivate Nothing liftIO (writeIORef (mirCryEnv mirState) ce') -- (m, _ce') <- liftIO $ SAW.loadCryptolModule sc ce (Text.unpack modulePath) -- tt <- liftIO $ SAW.extractDefFromCryptolModule m (Text.unpack name) - (tt, ce'') <- liftIO $ SAW.parseTypedTerm sc ce' $ + tt <- liftIO $ SAW.parseTypedTerm sc ce' $ SAW.InputText name "" 1 1 - liftIO (writeIORef (mirCryEnv mirState) ce'') + liftIO (writeIORef (mirCryEnv mirState) ce') ppopts <- liftIO $ SAW.scGetPPOpts sc args <- diff --git a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs index 57951f87c0..5c871b0c68 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs @@ -25,8 +25,7 @@ between these two modules is mostly a function of historical accident. -} module CryptolSAWCore.Cryptol - ( ImportVisibility(..) - , CryptolEnv(..) + ( module CryptolSAWCore.GlobalCryptolEnv , isErasedProp , proveProp @@ -44,8 +43,6 @@ module CryptolSAWCore.Cryptol , importExpr , importTopLevelDeclGroups - , getAllIfaceDecls - , refreshCryptolEnv , translateType , translateSchema , translateExpr @@ -99,8 +96,6 @@ import qualified Cryptol.Utils.Ident as C import qualified Cryptol.Utils.RecordMap as C import Cryptol.TypeCheck.Type as C (NominalType(..)) import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf) -import qualified Cryptol.ModuleSystem.Env as ME -import qualified Cryptol.ModuleSystem.Interface as MI import qualified Cryptol.ModuleSystem.NamingEnv as MN import qualified Cryptol.ModuleSystem.Renamer as MR @@ -121,244 +116,27 @@ import qualified SAWCore.QualName as QN -- local modules: import CryptolSAWCore.Panic import qualified CryptolSAWCore.Pretty as CryPP - --------------------------------------------------------------------------------- - --- | ImportVisibility is an enumeration that indicates how we handle --- the visibility of the symbols in an imported module. --- --- `OnlyPublic` makes only the public/exported symbols of a module --- visible from SAW. `PublicAndPrivate` instead makes all symbols --- visible, as if one is working inside it. The latter is often useful --- (or necessary) for verification and code generation. --- --- `PublicAndPrivate` is akin to setting the module focus in the --- Cryptol REPL; however, it uses a simpler internal mechanism and is --- only settable at import time. --- --- (See 'CryptolEnv.importCryptolModule'.) --- --- NOTE: this notion of public vs. private symbols is specific to --- SAWScript and distinct from Cryptol's notion of private --- definitions. --- --- FUTURE: this should probably be replaced with a way to manipulate --- the module focus like the Cryptol REPL uses. What you really want --- is not to expose module innards that weren't meant to be exposed, --- but to go inside to prove things in the module's internal context. --- -data ImportVisibility - = OnlyPublic -- ^ behaves like a normal Cryptol @import@ - | PublicAndPrivate -- ^ allows viewing of both @private@ sections - -- and (arbitrarily nested) submodules. - deriving (Eq, Show) - - --- | The environment for capturing the Cryptol state, both Cryptol's --- own state and the state associated with importing/translating --- into SAWCore. --- --- In addition to those bits, this structure also holds information --- about "extra names", which are additional Cryptol-level bindings --- that have been defined from SAW and thus aren't in any Cryptol --- module. --- --- FUTURE: Cryptol has its own functionality for additional bindings --- (it uses it for things created from the Cryptol REPL) and we ought --- to be able to use it instead of bolting on our own additional layer --- of material. Doing so would avoid various inconsistencies and --- irregularities that can creep in when we reimplement Cryptol name --- resolution. --- --- Note that prior to 202603 there were two environment types, --- `CryptolEnv` carrying around the persistent bits and generally --- being (in most places) the external interface; and another type --- called (far too generically) @Env@ used by the import logic in this --- file. There was a bunch of code for copying bits from `CryptolEnv` --- into an empty @Env@ on the fly, calling into here, then pouring the --- results back. This code was arbitrary and in some cases possibly --- wrong. Furthermore, having the import code tied to an incompatible --- type made a bunch of external code calling directly into it pass an --- empty environment instead, which caused further problems. --- --- While this was being fixed the prior @Env@ type got renamed to --- @ImportEnv@. There should be no references to it or its field names --- (@imp*@ rather than @env*@) left, but in case some are hiding in --- comments the transitional field names are also documented below. --- --- There is now one environment type. The history above remains --- relevant until all the leftover warts and weaknesses arising from --- the old structure get cleaned out, which may take a while. --- --- (FUTURE: once that's done, remove the historical notes; they are --- only of value while they remain relevant to the current code.) --- --- --- The elements of `CryptolEnv` are as follows. --- --- == First, the pieces relating to Cryptol primitives: --- --- `eRefPrims` maps Cryptol primitives to their reference --- implementations that Cryptol keeps around. Currently this field is --- only populated during initialization; it isn't clear if that's a --- bug. (If there are really no further uses after initialization, --- regardless of what the user does, dropping the contents allows the --- memory to be reclaimed. But if it's possible to construct such --- uses, they're likely to panic.) --- --- Before the environment types were merged, this field was found only --- in @Env@ and called @envRefPrims@ (transitionally @impRefPrims@). --- --- `ePrims` maps names of Cryptol primitives to their implementations --- as SAWCore terms. Before the environment types were merged, it was --- also present in @Env@ under the name @envPrims@ (transitionally --- @impPrims@). --- --- `ePrimTypes` maps names of Cryptol primitive types to their --- implementations as SAWCore terms (that are types). Before the --- environment types were merged, it was also present in @Env@ under --- the name @envPrimTypes@ (transitionally @impPrimTypes@). --- --- == Second, the pieces that track Cryptol-level objects and types: --- --- `eImports` is a list of all the modules that have been imported, --- and the visibility setting for each. This does not include, for --- example, builtin modules that exist but that have not been --- imported. --- --- `eModuleEnv` is the Cryptol-level module environment; it holds all --- the modules that have been loaded. Its type is also the state for --- Cryptol's `ME.ModuleM` monad. --- --- `eExtraTySyns`, formerly @eExtraTSyns@, holds the expansions for --- the "extra names" that are type aliases (synonyms). Maps names to --- `T.TySyn`, which wraps Cryptol types and among other things allows --- synonyms to take parameters. --- --- `eExtraVars`, formerly @eExtraTypes@, holds the Cryptol-level --- types for "extra names" that are value/term variables. Maps names --- to type schemes. --- --- 'eExtraNaming', formerly @eExtraNames@ is, a Cryptol renamer --- environment for the SAW "extra names". --- --- Before the environment types were merged, the above five fields --- were not accessible via @Env@, which turned out to cause --- complications. --- --- `eAllVars` is a map from Cryptol names to Cryptol types. This is --- used to call `fastTypeOf` and `fastSchemaOf` on Cryptol expressions --- to fetch their types. This table is derived from information --- properly kept elsewhere and is a headache to have. --- --- Before the environment types were merged, this was found only in --- @Env@ under the name @envC@. It was built on the fly when calling --- into the import code using @Env@ and thrown away afterwards, with --- the result that (pending further cleanup) we can't really be sure --- it's up to date, so we rebuild it at the points where previously --- it was generated on the fly. XXX: this is super ugly. --- --- (Transitionally it was called @impCry@ and then @impAllVars@.) --- --- == Third, the pieces that track imported SAWCore bits: --- --- `eTyVars` maps Cryptol type variable IDs to SAWCore types. This is --- only nonempty during import, when working inside a forall-binding. --- Before the environment types were merged, this was only needed in --- (and only found in) @Env@ as @envT@. Transitionally, it was called --- @impTy@ and then @impTyVars@. --- --- `eTyProps` maps Cryptol `C.Prop`, which are type constraints, to --- corresponding SAWCore information. There is both a term and a list --- of `FieldName`. The actual class dictionary we need is obtained by --- applying the given field selectors (in reverse order!) to the term. --- (This arises when a dictionary comes from a superclass; the field --- projections traverse the subclass dictionaries.) --- --- The constraints are referenced implicitly by their types. --- --- Like `eTyVars`, this table is only nonempty during import, when --- working inside a forall-binding, and carries the info from that --- binding. --- --- Before the environment types were merged, this was only needed in --- (and only found in) @Env@ as @envP@. Transitionally, it was called --- @impProp@ and then @envTyProps@. --- --- `eAllTerms`, formerly @eTermEnv@, holds the translations for all --- Cryptol names in scope. It maps names to SAWCore terms. Apparently --- it includes types as well as values. It isn't immediately obvious --- if it also holds the contents of `ePrims` and/or `ePrimTypes`. --- --- Before the environment types were merged, it was also found in @Env@ --- under the name @envE@. --- --- XXX: It is not clear if `eAllTerms` and `eAllVars` have the same --- keys. Nor is it clear if they should. But if they do, they should --- probably get merged. If not, someone should replace this paragraph --- with actual documentation about which things do and don't go in --- each table. --- --- `eFFITypes` maps SAWCore names to Cryptol FFI info where relevant. --- Before the environment types were merged, this was unavailable in --- @Env@. --- --- --- FUTURE: in principle we should be able to use the SAWCore types of --- the SAWCore terms after importing them, instead of `fastTypeOf` and --- `fastSchemaOf`, and drop the `eAllVars` table. In practice, doing --- that relies (in some cases) on being able to call `scCryptolType` --- to reconstruct the Cryptol-level type; that in turn requires, when --- inside a forall-binding, logic to intercept and lift SAWCore type --- variables back to their Cryptol parents. That requires a table we --- don't currently have, as well as additional lookup logic that --- doesn't currently exist. Furthermore, while we've fixed many of the --- ways the Cryptol -> SAWCore type mapping is noninjective, it still --- won't work for enumerations. And beyond that, when handling --- polymorphic type schemes we erase certain typeclasses in the --- translation, and that loses info, so we might need to translate --- those classes to placeholders instead of erasing them. It may then --- also be that the one use of `fastSchemaOf` can't actually be --- avoided; that isn't super clear. --- -data CryptolEnv = CryptolEnv - { eImports :: [(ImportVisibility, C.Import)] - , eModuleEnv :: ME.ModuleEnv - , eExtraNaming :: MR.NamingEnv - , eExtraVars :: Map C.Name C.Schema - , eExtraTySyns :: Map C.Name C.TySyn - , eAllVars :: Map C.Name C.Schema - , eTyVars :: Map Int Term - , eTyProps :: Map C.Prop (Term, [FieldName]) - , eAllTerms :: Map C.Name Term - , eRefPrims :: Map C.PrimIdent C.Expr - , ePrims :: Map C.PrimIdent Term - , ePrimTypes :: Map C.PrimIdent Term - , eFFITypes :: Map NameInfo C.FFI - } - +import CryptolSAWCore.GlobalCryptolEnv -- | bindTParam' - create a binding for a type parameter, returning 3-tuple: -- - environment -- - the SAWCore kind of the parameter -- - the SAWCore term for the type variable. -bindTParam' :: SharedContext -> C.TParam -> CryptolEnv -> IO (CryptolEnv, Term, Term) -bindTParam' sc tp env = +bindTParam' :: SharedContext -> C.TParam -> IO (Term, Term) +bindTParam' sc tp = do k <- importKind sc (C.tpKind tp) v <- scFreshVariable sc (tparamToLocalName tp) k - let env' = env { - eTyVars = Map.insert (C.tpUnique tp) v (eTyVars env) - } - return (env', v, k) + addTyVars sc (Map.singleton (C.tpUnique tp) v) + return (v, k) -- | bindTParam - create a binding for a type parameter, just return -- the new environment and the new sawcore type var (as Term). -bindTParam :: SharedContext -> C.TParam -> CryptolEnv -> IO (CryptolEnv, Term) -bindTParam sc tp env = +bindTParam :: SharedContext -> C.TParam -> IO Term +bindTParam sc tp = do - (env', v, _) <- bindTParam' sc tp env - return (env', v) + (v, _) <- bindTParam' sc tp + return v -- | bindName - create a new binding, adding to appropriate @@ -366,25 +144,21 @@ bindTParam sc tp env = -- - the updated environment, -- - the new SAWCore var (as a Term), and -- - the SAWCore type of the variable. -bindName :: SharedContext -> C.Name -> C.Schema -> CryptolEnv -> IO (CryptolEnv, Term, Term) -bindName sc name schema env = do - ty <- importSchema sc env schema +bindName :: SharedContext -> C.Name -> C.Schema -> IO (Term, Term) +bindName sc name schema = do + ty <- importSchema sc schema v <- scFreshVariable sc (nameToLocalName name) ty - let env' = env { - eAllTerms = Map.insert name v (eAllTerms env), - eAllVars = Map.insert name schema (eAllVars env) - } - return (env', v, ty) - -bindProp :: SharedContext -> C.Prop -> Text -> CryptolEnv -> IO (CryptolEnv, Term) -bindProp sc prop nm env = + addAllTerms sc (Map.singleton name v) + addAllVars sc (Map.singleton name schema) + return (v, ty) + +bindProp :: SharedContext -> C.Prop -> Text -> IO (Term) +bindProp sc prop nm = do - ty <- importType sc env prop + ty <- importType sc prop v <- scFreshVariable sc nm ty - let env' = env { - eTyProps = insertSupers prop [] v (eTyProps env) - } - return (env', v) + addTyProps sc (insertSupers prop [] v mempty) + return v -- | When we insert a non-erasable prop into the environment, make -- sure to also insert all its superclasses. We arrange it so @@ -488,8 +262,10 @@ importPC sc pc = -- imported such that they are accessible as values of type @Num@ at -- the SAWScript level. -- -importType :: HasCallStack => SharedContext -> CryptolEnv -> C.Type -> IO Term -importType sc env ty = +importType :: HasCallStack => SharedContext -> C.Type -> IO Term +importType sc ty = do + tyVars <- eTyVars sc + primTypes <- ePrimTypes sc case ty of C.TVar tvar -> case tvar of @@ -497,7 +273,7 @@ importType sc env ty = panic "importType" [ "TVFree in TVar is not supported: " <> CryPP.pp ty ] - C.TVBound v -> case Map.lookup (C.tpUnique v) (eTyVars env) of + C.TVBound v -> case Map.lookup (C.tpUnique v) tyVars of Just t -> pure t Nothing -> panic "importType" [ @@ -519,12 +295,12 @@ importType sc env ty = scGlobalApply sc (identOfEnumType n) =<< traverse go ts C.Abstract | Just prim' <- C.asPrim n - , Just t <- Map.lookup prim' (ePrimTypes env) -> + , Just t <- Map.lookup prim' primTypes -> scApplyAllBeta sc t =<< traverse go ts | Just prim' <- C.asPrim n -> do ppopts <- scGetPPOpts sc let envNote - | Map.null (ePrimTypes env) = + | Map.null primTypes = " (the primitive types environment is empty)" | otherwise = "" fail $ PPS.render ppopts $ PP.vsep @@ -583,7 +359,7 @@ importType sc env ty = C.TError _k -> panic "importType" ["found TError"] where - go = importType sc env + go = importType sc isErasedPC :: C.PC -> Bool isErasedPC pc = @@ -633,28 +409,28 @@ isErasedProp prop = -- if the 'C.Prop' holds. This function will 'panic' for 'C.Prop's that are not -- numeric constraints, such as @Integral@. In other words, this function -- supports the same set of 'C.Prop's that constraint guards do. -importNumericConstraintAsBool :: SharedContext -> CryptolEnv -> C.Prop -> IO Term -importNumericConstraintAsBool sc env prop = +importNumericConstraintAsBool :: SharedContext -> C.Prop -> IO Term +importNumericConstraintAsBool sc prop = case prop of C.TCon (C.PC C.PEqual) [lhs, rhs] -> eqTerm lhs rhs C.TCon (C.PC C.PNeq) [lhs, rhs] -> eqTerm lhs rhs >>= scNot sc C.TCon (C.PC C.PGeq) [lhs, rhs] -> do -- Convert 'lhs >= rhs' into '(rhs < lhs) \/ (rhs == lhs)' - lhs' <- importType sc env lhs - rhs' <- importType sc env rhs + lhs' <- importType sc lhs + rhs' <- importType sc rhs lt <- scGlobalApply sc "Cryptol.tcLt" [rhs', lhs'] eq <- scGlobalApply sc "Cryptol.tcEqual" [rhs', lhs'] scOr sc lt eq C.TCon (C.PC C.PFin) [x] -> do - x' <- importType sc env x + x' <- importType sc x scGlobalApply sc "Cryptol.tcFin" [x'] C.TCon (C.PC C.PAnd) [lhs, rhs] -> do - lhs' <- importType sc env lhs - rhs' <- importType sc env rhs + lhs' <- importType sc lhs + rhs' <- importType sc rhs scAnd sc lhs' rhs' C.TCon (C.PC C.PTrue) [] -> scBool sc True C.TCon (C.TError _) _ -> scBool sc False - C.TUser _ _ t -> importNumericConstraintAsBool sc env t + C.TUser _ _ t -> importNumericConstraintAsBool sc t _ -> panic "importNumericConstraintAsBool" [ "Called with non-numeric constraint: " <> CryPP.pp prop @@ -663,17 +439,17 @@ importNumericConstraintAsBool sc env prop = -- | Construct a term for equality of two types eqTerm :: C.Type -> C.Type -> IO Term eqTerm lhs rhs = do - lhs' <- importType sc env lhs - rhs' <- importType sc env rhs + lhs' <- importType sc lhs + rhs' <- importType sc rhs scGlobalApply sc "Cryptol.tcEqual" [lhs', rhs'] -importPropsType :: SharedContext -> CryptolEnv -> [C.Prop] -> C.Type -> IO Term -importPropsType sc env [] ty = importType sc env ty -importPropsType sc env (prop : props) ty - | isErasedProp prop = importPropsType sc env props ty +importPropsType :: SharedContext -> [C.Prop] -> C.Type -> IO Term +importPropsType sc [] ty = importType sc ty +importPropsType sc (prop : props) ty + | isErasedProp prop = importPropsType sc props ty | otherwise = - do p <- importType sc env prop - t <- importPropsType sc env props ty + do p <- importType sc prop + t <- importPropsType sc props ty scFun sc p t nameToLocalName :: C.Name -> LocalName @@ -685,30 +461,31 @@ tparamToLocalName tp = nameToLocalName (C.tpName tp) -importPolyType :: SharedContext -> CryptolEnv -> [C.TParam] -> [C.Prop] -> C.Type -> IO Term -importPolyType sc env [] props ty = importPropsType sc env props ty -importPolyType sc env (tp : tps) props ty = - do (env',a) <- bindTParam sc tp env - t <- importPolyType sc env' tps props ty +importPolyType :: SharedContext -> [C.TParam] -> [C.Prop] -> C.Type -> IO Term +importPolyType sc [] props ty = importPropsType sc props ty +importPolyType sc (tp : tps) props ty = + do a <- bindTParam sc tp + t <- importPolyType sc tps props ty scGeneralizeTerms sc [a] t -- | Import a Cryptol `C.Schema` (polymorphic type scheme). -importSchema :: SharedContext -> CryptolEnv -> C.Schema -> IO Term -importSchema sc env (C.Forall tparams props ty) = - importPolyType sc env tparams props ty +importSchema :: SharedContext -> C.Schema -> IO Term +importSchema sc (C.Forall tparams props ty) = + importPolyType sc tparams props ty -- | Find the SAWCore dictionary for a Cryptol typeclass. -proveProp :: HasCallStack => SharedContext -> CryptolEnv -> C.Prop -> IO Term -proveProp sc env prop = provePropRec sc env prop prop +proveProp :: HasCallStack => SharedContext -> C.Prop -> IO Term +proveProp sc prop = provePropRec sc prop prop -- internal recursive version -- -- (we carry around the original prop when recursing as "prop0", in -- case we get stuck and need to bail out, at which point we want to -- be able to print it) -provePropRec :: HasCallStack => SharedContext -> CryptolEnv -> C.Prop -> C.Prop -> IO Term -provePropRec sc env prop0 prop = - case Map.lookup (normalizeProp prop) (eTyProps env) of +provePropRec :: HasCallStack => SharedContext -> C.Prop -> C.Prop -> IO Term +provePropRec sc prop0 prop = do + tyProps <- eTyProps sc + case Map.lookup (normalizeProp prop) tyProps of -- Class dictionary was provided as an argument Just (prf, fs) -> @@ -727,40 +504,40 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PZeroInteger" [] -- instance Zero (Z n) (C.pIsZero -> Just (C.tIsIntMod -> Just n)) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PZeroIntModNum" [n'] -- instance Zero Rational (C.pIsZero -> Just (C.tIsRational -> True)) -> do scGlobalApply sc "Cryptol.PZeroRational" [] -- instance Zero [n] (C.pIsZero -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True))) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PZeroSeqBool" [n'] -- instance ValidFloat e p => Zero (Float e p) (C.pIsZero -> Just (C.tIsFloat -> Just (e, p))) - -> do e' <- importType sc env e - p' <- importType sc env p + -> do e' <- importType sc e + p' <- importType sc p scGlobalApply sc "Cryptol.PZeroFloat" [e', p'] -- instance (Zero a) => Zero [n]a (C.pIsZero -> Just (C.tIsSeq -> Just (n, a))) - -> do n' <- importType sc env n - a' <- importType sc env a - pa <- provePropRec sc env prop0 (C.pZero a) + -> do n' <- importType sc n + a' <- importType sc a + pa <- provePropRec sc prop0 (C.pZero a) scGlobalApply sc "Cryptol.PZeroSeq" [n', a', pa] -- instance (Zero b) => Zero (a -> b) (C.pIsZero -> Just (C.tIsFun -> Just (a, b))) - -> do a' <- importType sc env a - b' <- importType sc env b - pb <- provePropRec sc env prop0 (C.pZero b) + -> do a' <- importType sc a + b' <- importType sc b + pb <- provePropRec sc prop0 (C.pZero b) scGlobalApply sc "Cryptol.PZeroFun" [a', b', pb] -- instance (Zero a, Zero b, ...) => Zero (a, b, ...) (C.pIsZero -> Just (C.tIsTuple -> Just ts)) - -> do ps <- traverse (provePropRec sc env prop0 . C.pZero) ts + -> do ps <- traverse (provePropRec sc prop0 . C.pZero) ts scTuple sc ps -- instance (Zero a, Zero b, ...) => Zero { x : a, y : b, ... } (C.pIsZero -> Just (C.tIsRec -> Just fm)) -> do let fields = map (\(i, t) -> (C.identText i, t)) (C.canonicalFields fm) - fields' <- traverse (traverse (provePropRec sc env prop0 . C.pZero)) fields + fields' <- traverse (traverse (provePropRec sc prop0 . C.pZero)) fields scRecordValue sc fields' -- instance Logic Bit @@ -768,29 +545,29 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PLogicBit" [] -- instance Logic [n] (C.pIsLogic -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True))) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PLogicSeqBool" [n'] -- instance (Logic a) => Logic [n]a (C.pIsLogic -> Just (C.tIsSeq -> Just (n, a))) - -> do n' <- importType sc env n - a' <- importType sc env a - pa <- provePropRec sc env prop0 (C.pLogic a) + -> do n' <- importType sc n + a' <- importType sc a + pa <- provePropRec sc prop0 (C.pLogic a) scGlobalApply sc "Cryptol.PLogicSeq" [n', a', pa] -- instance (Logic b) => Logic (a -> b) (C.pIsLogic -> Just (C.tIsFun -> Just (a, b))) - -> do a' <- importType sc env a - b' <- importType sc env b - pb <- provePropRec sc env prop0 (C.pLogic b) + -> do a' <- importType sc a + b' <- importType sc b + pb <- provePropRec sc prop0 (C.pLogic b) scGlobalApply sc "Cryptol.PLogicFun" [a', b', pb] -- instance Logic () (C.pIsLogic -> Just (C.tIsTuple -> Just [])) -> do scGlobalApply sc "Cryptol.PLogicUnit" [] -- instance (Logic a, Logic b) => Logic (a, b) (C.pIsLogic -> Just (C.tIsTuple -> Just (t : ts))) - -> do a <- importType sc env t - b <- importType sc env (C.tTuple ts) - pa <- provePropRec sc env prop0 (C.pLogic t) - pb <- provePropRec sc env prop0 (C.pLogic (C.tTuple ts)) + -> do a <- importType sc t + b <- importType sc (C.tTuple ts) + pa <- provePropRec sc prop0 (C.pLogic t) + pb <- provePropRec sc prop0 (C.pLogic (C.tTuple ts)) scGlobalApply sc "Cryptol.PLogicPair" [a, b, pa, pb] -- instance (Logic a, Logic b, ...) => instance Logic { x : a, y : b, ... } (C.pIsLogic -> Just (C.tIsRec -> Just fm)) @@ -801,41 +578,41 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PRingInteger" [] -- instance Ring (Z n) (C.pIsRing -> Just (C.tIsIntMod -> Just n)) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PRingIntModNum" [n'] -- instance Ring Rational (C.pIsRing -> Just (C.tIsRational -> True)) -> do scGlobalApply sc "Cryptol.PRingRational" [] -- instance (fin n) => Ring [n] (C.pIsRing -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True))) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PRingSeqBool" [n'] -- instance ValidFloat e p => Ring (Float e p) (C.pIsRing -> Just (C.tIsFloat -> Just (e, p))) - -> do e' <- importType sc env e - p' <- importType sc env p + -> do e' <- importType sc e + p' <- importType sc p scGlobalApply sc "Cryptol.PRingFloat" [e', p'] -- instance (Ring a) => Ring [n]a (C.pIsRing -> Just (C.tIsSeq -> Just (n, a))) - -> do n' <- importType sc env n - a' <- importType sc env a - pa <- provePropRec sc env prop0 (C.pRing a) + -> do n' <- importType sc n + a' <- importType sc a + pa <- provePropRec sc prop0 (C.pRing a) scGlobalApply sc "Cryptol.PRingSeq" [n', a', pa] -- instance (Ring b) => Ring (a -> b) (C.pIsRing -> Just (C.tIsFun -> Just (a, b))) - -> do a' <- importType sc env a - b' <- importType sc env b - pb <- provePropRec sc env prop0 (C.pRing b) + -> do a' <- importType sc a + b' <- importType sc b + pb <- provePropRec sc prop0 (C.pRing b) scGlobalApply sc "Cryptol.PRingFun" [a', b', pb] -- instance Ring () (C.pIsRing -> Just (C.tIsTuple -> Just [])) -> do scGlobalApply sc "Cryptol.PRingUnit" [] -- instance (Ring a, Ring b) => Ring (a, b) (C.pIsRing -> Just (C.tIsTuple -> Just (t : ts))) - -> do a <- importType sc env t - b <- importType sc env (C.tTuple ts) - pa <- provePropRec sc env prop0 (C.pRing t) - pb <- provePropRec sc env prop0 (C.pRing (C.tTuple ts)) + -> do a <- importType sc t + b <- importType sc (C.tTuple ts) + pa <- provePropRec sc prop0 (C.pRing t) + pb <- provePropRec sc prop0 (C.pRing (C.tTuple ts)) scGlobalApply sc "Cryptol.PRingPair" [a, b, pa, pb] -- instance (Ring a, Ring b, ...) => instance Ring { x : a, y : b, ... } (C.pIsRing -> Just (C.tIsRec -> Just fm)) @@ -846,7 +623,7 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PIntegralInteger" [] -- instance Integral [n] (C.pIsIntegral -> Just (C.tIsSeq -> (Just (n, C.tIsBit -> True)))) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PIntegralSeqBool" [n'] -- instance Field Rational @@ -854,12 +631,12 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PFieldRational" [] -- instance (prime p) => Field (Z p) (C.pIsField -> Just (C.tIsIntMod -> Just n)) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PFieldIntModNum" [n'] -- instance (ValidFloat e p) => Field (Float e p) (C.pIsField -> Just (C.tIsFloat -> Just (e, p))) - -> do e' <- importType sc env e - p' <- importType sc env p + -> do e' <- importType sc e + p' <- importType sc p scGlobalApply sc "Cryptol.PFieldFloat" [e', p'] -- instance Round Rational @@ -867,8 +644,8 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PRoundRational" [] -- instance (ValidFloat e p) => Round (Float e p) (C.pIsRound -> Just (C.tIsFloat -> Just (e, p))) - -> do e' <- importType sc env e - p' <- importType sc env p + -> do e' <- importType sc e + p' <- importType sc p scGlobalApply sc "Cryptol.PRoundFloat" [e', p'] -- instance Eq Bit @@ -879,35 +656,35 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PEqInteger" [] -- instance Eq (Z n) (C.pIsEq -> Just (C.tIsIntMod -> Just n)) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PEqIntModNum" [n'] -- instance Eq Rational (C.pIsEq -> Just (C.tIsRational -> True)) -> do scGlobalApply sc "Cryptol.PEqRational" [] -- instance Eq (Float e p) (C.pIsEq -> Just (C.tIsFloat -> Just (e, p))) - -> do e' <- importType sc env e - p' <- importType sc env p + -> do e' <- importType sc e + p' <- importType sc p scGlobalApply sc "Cryptol.PEqFloat" [e', p'] -- instance (fin n) => Eq [n] (C.pIsEq -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True))) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PEqSeqBool" [n'] -- instance (fin n, Eq a) => Eq [n]a (C.pIsEq -> Just (C.tIsSeq -> Just (n, a))) - -> do n' <- importType sc env n - a' <- importType sc env a - pa <- provePropRec sc env prop0 (C.pEq a) + -> do n' <- importType sc n + a' <- importType sc a + pa <- provePropRec sc prop0 (C.pEq a) scGlobalApply sc "Cryptol.PEqSeq" [n', a', pa] -- instance Eq () (C.pIsEq -> Just (C.tIsTuple -> Just [])) -> do scGlobalApply sc "Cryptol.PEqUnit" [] -- instance (Eq a, Eq b) => Eq (a, b) (C.pIsEq -> Just (C.tIsTuple -> Just (t : ts))) - -> do a <- importType sc env t - b <- importType sc env (C.tTuple ts) - pa <- provePropRec sc env prop0 (C.pEq t) - pb <- provePropRec sc env prop0 (C.pEq (C.tTuple ts)) + -> do a <- importType sc t + b <- importType sc (C.tTuple ts) + pa <- provePropRec sc prop0 (C.pEq t) + pb <- provePropRec sc prop0 (C.pEq (C.tTuple ts)) scGlobalApply sc "Cryptol.PEqPair" [a, b, pa, pb] -- instance (Eq a, Eq b, ...) => instance Eq { x : a, y : b, ... } (C.pIsEq -> Just (C.tIsRec -> Just fm)) @@ -924,28 +701,28 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PCmpRational" [] -- instance Cmp (Float e p) (C.pIsCmp -> Just (C.tIsFloat -> Just (e, p))) - -> do e' <- importType sc env e - p' <- importType sc env p + -> do e' <- importType sc e + p' <- importType sc p scGlobalApply sc "Cryptol.PCmpFloat" [e', p'] -- instance (fin n) => Cmp [n] (C.pIsCmp -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True))) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PCmpSeqBool" [n'] -- instance (fin n, Cmp a) => Cmp [n]a (C.pIsCmp -> Just (C.tIsSeq -> Just (n, a))) - -> do n' <- importType sc env n - a' <- importType sc env a - pa <- provePropRec sc env prop0 (C.pCmp a) + -> do n' <- importType sc n + a' <- importType sc a + pa <- provePropRec sc prop0 (C.pCmp a) scGlobalApply sc "Cryptol.PCmpSeq" [n', a', pa] -- instance Cmp () (C.pIsCmp -> Just (C.tIsTuple -> Just [])) -> do scGlobalApply sc "Cryptol.PCmpUnit" [] -- instance (Cmp a, Cmp b) => Cmp (a, b) (C.pIsCmp -> Just (C.tIsTuple -> Just (t : ts))) - -> do a <- importType sc env t - b <- importType sc env (C.tTuple ts) - pa <- provePropRec sc env prop0 (C.pCmp t) - pb <- provePropRec sc env prop0 (C.pCmp (C.tTuple ts)) + -> do a <- importType sc t + b <- importType sc (C.tTuple ts) + pa <- provePropRec sc prop0 (C.pCmp t) + pb <- provePropRec sc prop0 (C.pCmp (C.tTuple ts)) scGlobalApply sc "Cryptol.PCmpPair" [a, b, pa, pb] -- instance (Cmp a, Cmp b, ...) => instance Cmp { x : a, y : b, ... } (C.pIsCmp -> Just (C.tIsRec -> Just fm)) @@ -953,23 +730,23 @@ provePropRec sc env prop0 prop = -- instance (fin n) => SignedCmp [n] (C.pIsSignedCmp -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True))) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PSignedCmpSeqBool" [n'] -- instance (fin n, SignedCmp a) => SignedCmp [n]a (C.pIsSignedCmp -> Just (C.tIsSeq -> Just (n, a))) - -> do n' <- importType sc env n - a' <- importType sc env a - pa <- provePropRec sc env prop0 (C.pSignedCmp a) + -> do n' <- importType sc n + a' <- importType sc a + pa <- provePropRec sc prop0 (C.pSignedCmp a) scGlobalApply sc "Cryptol.PSignedCmpSeq" [n', a', pa] -- instance SignedCmp () (C.pIsSignedCmp -> Just (C.tIsTuple -> Just [])) -> do scGlobalApply sc "Cryptol.PSignedCmpUnit" [] -- instance (SignedCmp a, SignedCmp b) => SignedCmp (a, b) (C.pIsSignedCmp -> Just (C.tIsTuple -> Just (t : ts))) - -> do a <- importType sc env t - b <- importType sc env (C.tTuple ts) - pa <- provePropRec sc env prop0 (C.pSignedCmp t) - pb <- provePropRec sc env prop0 (C.pSignedCmp (C.tTuple ts)) + -> do a <- importType sc t + b <- importType sc (C.tTuple ts) + pa <- provePropRec sc prop0 (C.pSignedCmp t) + pb <- provePropRec sc prop0 (C.pSignedCmp (C.tTuple ts)) scGlobalApply sc "Cryptol.PSignedCmpPair" [a, b, pa, pb] -- instance (SignedCmp a, SignedCmp b, ...) => instance SignedCmp { x : a, y : b, ... } (C.pIsSignedCmp -> Just (C.tIsRec -> Just fm)) @@ -987,19 +764,19 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PLiteralInteger" [] -- instance Literal val (Z n) (C.pIsLiteral -> Just (_, C.tIsIntMod -> Just n)) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PLiteralIntModNum" [n'] -- instance Literal val Rational (C.pIsLiteral -> Just (_, C.tIsRational -> True)) -> do scGlobalApply sc "Cryptol.PLiteralRational" [] -- instance (fin n, n >= width val) => Literal val [n] (C.pIsLiteral -> Just (_, C.tIsSeq -> Just (n, C.tIsBit -> True))) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PLiteralSeqBool" [n'] -- instance ValidFloat e p => Literal val (Float e p) (with extra constraints) (C.pIsLiteral -> Just (_, C.tIsFloat -> Just (e, p))) - -> do e' <- importType sc env e - p' <- importType sc env p + -> do e' <- importType sc e + p' <- importType sc p scGlobalApply sc "Cryptol.PLiteralFloat" [e', p'] -- instance (2 >= val) => LiteralLessThan val Bit @@ -1010,19 +787,19 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PLiteralInteger" [] -- instance (fin n, n >= 1, n >= val) LiteralLessThan val (Z n) (C.pIsLiteralLessThan -> Just (_, C.tIsIntMod -> Just n)) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PLiteralIntModNum" [n'] -- instance Literal val Rational (C.pIsLiteralLessThan -> Just (_, C.tIsRational -> True)) -> do scGlobalApply sc "Cryptol.PLiteralRational" [] -- instance (fin n, n >= lg2 val) => Literal val [n] (C.pIsLiteralLessThan -> Just (_, C.tIsSeq -> Just (n, C.tIsBit -> True))) - -> do n' <- importType sc env n + -> do n' <- importType sc n scGlobalApply sc "Cryptol.PLiteralSeqBool" [n'] -- instance ValidFloat e p => Literal val (Float e p) (with extra constraints) (C.pIsLiteralLessThan -> Just (_, C.tIsFloat -> Just (e, p))) - -> do e' <- importType sc env e - p' <- importType sc env p + -> do e' <- importType sc e + p' <- importType sc p scGlobalApply sc "Cryptol.PLiteralFloat" [e', p'] -- Note that in the FLiteral instances below, we intentionally do not @@ -1034,14 +811,14 @@ provePropRec sc env prop0 prop = -> do scGlobalApply sc "Cryptol.PFLiteralRational" [] -- instance ValidFloat e p => FLiteral m n r (Float e p) (with extra constraints) (C.pIsFLiteral -> Just (_, _, _, C.tIsFloat -> Just (e, p))) - -> do e' <- importType sc env e - p' <- importType sc env p + -> do e' <- importType sc e + p' <- importType sc p scGlobalApply sc "Cryptol.PFLiteralFloat" [e', p'] _ -> do let prop0' = " " <> CryPP.pp prop0 prop' = " " <> CryPP.pp prop - env' = map (\p -> " " <> CryPP.pp p) $ Map.keys $ eTyProps env + env' = map (\p -> " " <> CryPP.pp p) $ Map.keys $ tyProps message = [ "Cannot find or infer typeclass instance", "Property needed:", @@ -1062,8 +839,8 @@ provePropRec sc env prop0 prop = pure (a, pa) go ((i, t) : ts) = do s <- scString sc (C.identText i) - a <- importType sc env t - pa <- provePropRec sc env prop0 (p t) + a <- importType sc t + pa <- provePropRec sc prop0 (p t) (b, pb) <- go ts c <- scGlobalApply sc "Prelude.RecordType" [s, a, b] pc <- scGlobalApply sc cons [s, a, b, pa, pb] @@ -1138,45 +915,48 @@ we omit the numeric types `m`, `n`, and `r` from the translation, leaving only `a`. -} -importPrimitive :: SharedContext -> ImportPrimitiveOptions -> CryptolEnv -> C.Name -> C.Schema -> IO Term -importPrimitive sc primOpts env n sch +importPrimitive :: SharedContext -> ImportPrimitiveOptions -> C.Name -> C.Schema -> IO Term +importPrimitive sc primOpts n sch = do + refPrims <- eRefPrims sc + prims <- ePrims sc + if -- lookup primitive in the main primitive lookup table - | Just nm <- C.asPrim n, Just term <- Map.lookup nm allPrims = term sc + | Just nm <- C.asPrim n, Just term <- Map.lookup nm allPrims -> term sc - -- lookup primitive in the main reference implementation lookup table - | Just nm <- C.asPrim n, Just expr <- Map.lookup nm (eRefPrims env) = - do t <- importSchema sc env sch - e <- importExpr sc env expr - nmi <- importName n - e' <- scAscribe sc e t - scDefineConstant sc nmi e' + -- lookup primitive in the main reference implementation lookup table + | Just nm <- C.asPrim n, Just expr <- Map.lookup nm refPrims -> + do t <- importSchema sc sch + e <- importExpr sc expr + nmi <- importName n + e' <- scAscribe sc e t + scDefineConstant sc nmi e' - -- lookup primitive in the extra primitive lookup table - | Just nm <- C.asPrim n, Just t <- Map.lookup nm (ePrims env) = return t + -- lookup primitive in the extra primitive lookup table + | Just nm <- C.asPrim n, Just t <- Map.lookup nm prims -> return t - -- Optionally, create an opaque constant representing the primitive - -- if it doesn't match one of the ones we know about. - | Just _ <- C.asPrim n, allowUnknownPrimitives primOpts = - importOpaque sc env n sch + -- Optionally, create an opaque constant representing the primitive + -- if it doesn't match one of the ones we know about. + | Just _ <- C.asPrim n, allowUnknownPrimitives primOpts -> + importOpaque sc n sch - -- Panic if we don't know the given primitive (TODO? probably shouldn't be a panic) - | Just nm <- C.asPrim n = - panic "importPrimitive" ["Unknown Cryptol primitive name: " <> CryPP.pp nm] + -- Panic if we don't know the given primitive (TODO? probably shouldn't be a panic) + | Just nm <- C.asPrim n -> + panic "importPrimitive" ["Unknown Cryptol primitive name: " <> CryPP.pp nm] - | otherwise = - panic "importPrimitive" ["Improper Cryptol primitive name: " <> CryPP.pp n] + | otherwise -> + panic "importPrimitive" ["Improper Cryptol primitive name: " <> CryPP.pp n] -- | Create an opaque constant with the given name and schema -importOpaque :: SharedContext -> CryptolEnv -> C.Name -> C.Schema -> IO Term -importOpaque sc env n sch = do - t <- importSchema sc env sch +importOpaque :: SharedContext -> C.Name -> C.Schema -> IO Term +importOpaque sc n sch = do + t <- importSchema sc sch nmi <- importName n scOpaqueConstant sc nmi t -importConstant :: SharedContext -> CryptolEnv -> C.Name -> C.Schema -> Term -> IO Term -importConstant sc env n sch rhs = +importConstant :: SharedContext -> C.Name -> C.Schema -> Term -> IO Term +importConstant sc n sch rhs = do nmi <- importName n - t <- importSchema sc env sch + t <- importSchema sc sch rhs' <- scAscribe sc rhs t scDefineConstant sc nmi rhs' @@ -1393,26 +1173,26 @@ primeECPrims = -- 'scTypeOf' on the result of @'importExpr' sc env expr@ must yield a -- SAWCore type that is equivalent (i.e. convertible) to the one returned by -- @'importSchema' sc env ('fastTypeOf' ('eAllVars' env) expr)@. -importExpr :: HasCallStack => SharedContext -> CryptolEnv -> C.Expr -> IO Term -importExpr sc env expr = +importExpr :: HasCallStack => SharedContext -> C.Expr -> IO Term +importExpr sc expr = case expr of C.EList es t -> - do t' <- importType sc env t - es' <- traverse (importExpr' sc env (C.tMono t)) es + do t' <- importType sc t + es' <- traverse (importExpr' sc (C.tMono t)) es scVector sc t' es' C.ETuple es -> - do es' <- traverse (importExpr sc env) es + do es' <- traverse (importExpr sc) es scTuple sc es' C.ERec fm -> do let fields = map (\(i, t) -> (C.identText i, t)) (C.canonicalFields fm) - fields' <- traverse (traverse (importExpr sc env)) fields + fields' <- traverse (traverse (importExpr sc)) fields scRecordValue sc fields' C.ESel e sel -> do -- Elimination for tuple/record/list - e' <- importExpr sc env e + e' <- importExpr sc e case sel of C.TupleSel i _maybeLen -> scTupleSelector sc e' i @@ -1452,22 +1232,22 @@ importExpr sc env expr = "Type: " <> CryPP.pp t1 ] Just ts -> - do e1' <- importExpr sc env e1 - ts' <- mapM (importType sc env) ts + do e1' <- importExpr sc e1 + ts' <- mapM (importType sc) ts let t2 = ts !! i let t2' = ts' !! i - e2' <- importExpr' sc env (C.tMono t2) e2 + e2' <- importExpr' sc (C.tMono t2) e2 f <- scGlobalApply sc "Cryptol.const" [t2', t2', e2'] g <- tupleUpdate sc f i ts' scApply sc g e1' C.RecordSel x _ -> case C.tNoUser t1 of C.TRec fields -> - importRecordUpdate sc env e1 e2 x fields + importRecordUpdate sc e1 e2 x fields C.TNominal nt ts -> case C.ntDef nt of C.Struct con -> - importRecordUpdate sc env e1 e2 x (newtypeRecordFields nt ts con) + importRecordUpdate sc e1 e2 x (newtypeRecordFields nt ts con) C.Enum {} -> panic "importExpr" [ "ESet/RecordSel/TNominal: expected newtype, saw enum", @@ -1489,42 +1269,45 @@ importExpr sc env expr = panic "importExpr" ("ListSel is unsupported in ESet:" : Text.lines expr') C.EIf e1 e2 e3 -> - do e1' <- importExpr sc env e1 - e2' <- importExpr sc env e2 + do e1' <- importExpr sc e1 + e2' <- importExpr sc e2 + allvars <- eAllVars sc -- FUTURE: In principle we can use scCryptolType to -- reconstruct ty from ty', but in practice it does not work -- without at least fetching forall-bound type variables from -- the environment first. - let ty = fastTypeOf (eAllVars env) e2 + let ty = fastTypeOf allvars e2 ty' <- scTypeOf sc e2' - e3' <- importExpr' sc env (C.tMono ty) e3 + e3' <- importExpr' sc (C.tMono ty) e3 scGlobalApply sc "Prelude.ite" [ty', e1', e2', e3'] C.EComp len eltty e mss -> - importComp sc env len eltty e mss + importComp sc len eltty e mss - C.EVar qname -> - case Map.lookup qname (eAllTerms env) of + C.EVar qname -> do + allterms <- eAllTerms sc + case Map.lookup qname allterms of Just e' -> pure e' Nothing -> panic "importExpr / EVar" ["Unknown variable: " <> CryPP.pp qname] C.ETAbs tp e -> - do (env',a) <- bindTParam sc tp env - e' <- importExpr sc env' e + do a <- bindTParam sc tp + e' <- importExpr sc e scAbstractTerms sc [a] e' C.ETApp e t -> - do e' <- importExpr sc env e - t' <- importType sc env t + do e' <- importExpr sc e + t' <- importType sc t scApply sc e' t' C.EApp e1 e2 -> - do e1' <- importExpr sc env e1 + do e1' <- importExpr sc e1 + allvars <- eAllVars sc -- FUTURE: In principle we can use scTypeOf and scCryptolType -- to reconstruct the Cryptol type of e1, but in practice it -- does not work without at least fetching forall-bound type -- variables from the environment first. - let t1 = fastTypeOf (eAllVars env) e1 + let t1 = fastTypeOf allvars e1 t1a = case C.tIsFun t1 of Just (a, _) -> a Nothing -> @@ -1532,28 +1315,29 @@ importExpr sc env expr = "EApp: expected function type", "Type: " <> CryPP.pp t1 ] - e2' <- importExpr' sc env (C.tMono t1a) e2 + e2' <- importExpr' sc (C.tMono t1a) e2 scApply sc e1' e2' C.EAbs x t e -> - do (env',v,_) <- bindName sc x (C.tMono t) env - e' <- importExpr sc env' e + do (v,_) <- bindName sc x (C.tMono t) + e' <- importExpr sc e scAbstractTerms sc [v] e' C.EProofAbs prop e - | isErasedProp prop -> importExpr sc env e + | isErasedProp prop -> importExpr sc e | otherwise -> - do (env',v) <- bindProp sc prop "_P" env - e' <- importExpr sc env' e + do v <- bindProp sc prop "_P" + e' <- importExpr sc e scAbstractTerms sc [v] e' - C.EProofApp e -> - case fastSchemaOf (eAllVars env) e of + C.EProofApp e -> do + allvars <- eAllVars sc + case fastSchemaOf allvars e of C.Forall [] (p : _ps) _ty - | isErasedProp p -> importExpr sc env e + | isErasedProp p -> importExpr sc e | otherwise -> - do e' <- importExpr sc env e - prf <- proveProp sc env p + do e' <- importExpr sc e + prf <- proveProp sc p scApply sc e' prf s -> do ppopts <- scGetPPOpts sc @@ -1570,15 +1354,15 @@ importExpr sc env expr = panic "importExpr" ("EProofApp: invalid type" : info') C.EWhere e dgs -> - do env' <- importDeclGroups sc env dgs - importExpr sc env' e + do importDeclGroups sc dgs + importExpr sc e C.ELocated _ e -> - importExpr sc env e + importExpr sc e C.EPropGuards arms typ -> do -- Convert prop guards to nested if-then-elses - typ' <- importType sc env typ + typ' <- importType sc typ errMsg <- scString sc "No constraints satisfied in constraint guard" err <- scGlobalApply sc "Prelude.error" [typ', errMsg] -- NOTE: Must use a right fold to maintain order of prop guards in @@ -1586,13 +1370,14 @@ importExpr sc env expr = Fold.foldrM (propGuardToIte typ') err arms C.ECase s alts dflt -> do + allvars <- eAllVars sc -- We need the result type of the whole expression at the -- SAWCore level, and at least for the time being it's awkward -- to get it from the SAWCore terms constructed by importCase, -- so get the Cryptol-level type here and lower it. FUTURE: tidy -- this up. - let tyResult = fastTypeOf (eAllVars env) expr - importCase sc env tyResult s alts dflt + let tyResult = fastTypeOf allvars expr + importCase sc tyResult s alts dflt where -- | Translate an erased 'C.Prop' to a term and return the conjunction of the @@ -1602,7 +1387,7 @@ importExpr sc env expr = -- conjunction over singleton lists. conjoinErasedProps :: Maybe Term -> C.Prop -> IO (Maybe Term) conjoinErasedProps mt p = do - p' <- importNumericConstraintAsBool sc env p + p' <- importNumericConstraintAsBool sc p case mt of Just t -> Just <$> scAnd sc t p' Nothing -> pure $ Just p' @@ -1616,7 +1401,7 @@ importExpr sc env expr = propGuardToIte typ (props, body) falseBranch = do mCondition <- Fold.foldlM conjoinErasedProps Nothing props condition <- maybe (scBool sc True) pure mCondition - trueBranch <- importExpr sc env body + trueBranch <- importExpr sc body scGlobalApply sc "Prelude.ite" [typ, condition, trueBranch, falseBranch] @@ -1629,8 +1414,8 @@ importExpr sc env expr = -- Essentially, this function should be used when the expression's type is known -- (such as with a type annotation), and 'importExpr' should be used when the -- type must be inferred. -importExpr' :: HasCallStack => SharedContext -> CryptolEnv -> C.Schema -> C.Expr -> IO Term -importExpr' sc env schema expr = +importExpr' :: HasCallStack => SharedContext -> C.Schema -> C.Expr -> IO Term +importExpr' sc schema expr = case expr of C.ETuple es -> do ty <- the "Expected a mono type in ETuple" (C.isMono schema) @@ -1647,10 +1432,10 @@ importExpr' sc env schema expr = C.EIf e1 e2 e3 -> do ty <- the "Expected a mono type in EIf" (C.isMono schema) - ty' <- importType sc env ty - e1' <- importExpr sc env e1 - e2' <- importExpr' sc env schema e2 - e3' <- importExpr' sc env schema e3 + ty' <- importType sc ty + e1' <- importExpr sc e1 + e2' <- importExpr' sc schema e2 + e3' <- importExpr' sc schema e3 scGlobalApply sc "Prelude.ite" [ty', e1', e2', e3'] C.ETAbs tp e -> @@ -1664,15 +1449,15 @@ importExpr' sc env schema expr = "Unexpected empty params in type abstraction (ETAbs)", " " <> CryPP.pp expr ] - (env',v) <- bindTParam sc tp env - e' <- importExpr' sc env' schema' e + v <- bindTParam sc tp + e' <- importExpr' sc schema' e scAbstractTerms sc [v] e' C.EAbs x _ e -> do ty <- the "expected a mono schema in EAbs" (C.isMono schema) (a, b) <- the "expected a function type in EAbs" (C.tIsFun ty) - (env',v,_) <- bindName sc x (C.tMono a) env - e' <- importExpr' sc env' (C.tMono b) e + (v,_) <- bindName sc x (C.tMono a) + e' <- importExpr' sc (C.tMono b) e scAbstractTerms sc [v] e' C.EProofAbs _ e -> @@ -1690,17 +1475,17 @@ importExpr' sc env schema expr = "Schema: " <> CryPP.pp schema ] if isErasedProp prop - then importExpr' sc env schema' e - else do (env',v) <- bindProp sc prop "_P" env - e' <- importExpr' sc env' schema' e + then importExpr' sc schema' e + else do v <- bindProp sc prop "_P" + e' <- importExpr' sc schema' e scAbstractTerms sc [v] e' C.EWhere e dgs -> - do env' <- importDeclGroups sc env dgs - importExpr' sc env' schema e + do importDeclGroups sc dgs + importExpr' sc schema e C.ELocated _ e -> - importExpr' sc env schema e + importExpr' sc schema e C.ECase {} -> fallback C.EList {} -> fallback @@ -1715,7 +1500,7 @@ importExpr' sc env schema expr = where go :: C.Type -> C.Expr -> IO Term - go t = importExpr' sc env (C.tMono t) + go t = importExpr' sc (C.tMono t) -- XXX find this a better name the :: Text -> Maybe a -> IO a @@ -1723,10 +1508,11 @@ importExpr' sc env schema expr = fallback :: IO Term fallback = - do let t1 = fastTypeOf (eAllVars env) expr + do allvars <- eAllVars sc + let t1 = fastTypeOf allvars expr t2 <- the "fallback: schema is not mono" (C.isMono schema) - expr' <- importExpr sc env expr - coerceTerm sc env t1 t2 expr' + expr' <- importExpr sc expr + coerceTerm sc t1 t2 expr' tupleUpdate :: SharedContext -> Term -> Int -> [Term] -> IO Term tupleUpdate sc f 0 (a : ts) = @@ -1742,7 +1528,6 @@ tupleUpdate _ _ _ [] = panic "tupleUpdate" ["empty tuple"] -- for updating both record and newtype values. importRecordUpdate :: SharedContext -> - CryptolEnv -> -- | The type of the overall expression to convert. C.Expr -> -- | The type of the expression to update at the given field. @@ -1752,12 +1537,12 @@ importRecordUpdate :: -- | The names and types of all fields in the record or newtype. C.RecordMap C.Ident C.Type -> IO Term -importRecordUpdate sc env e1 e2 x fields = - do e1' <- importExpr sc env e1 - fields' <- mapM (importType sc env) fields +importRecordUpdate sc e1 e2 x fields = + do e1' <- importExpr sc e1 + fields' <- mapM (importType sc) fields t2 <- the "field name not found" (C.lookupField x fields) t2' <- the "field name not found" (C.lookupField x fields') - e2' <- importExpr' sc env (C.tMono t2) e2 + e2' <- importExpr' sc (C.tMono t2) e2 f <- scGlobalApply sc "Cryptol.const" [t2', t2', e2'] let canonicalFields = C.canonicalFields fields' let canonicalFields' = map (first C.identText) canonicalFields @@ -1866,12 +1651,12 @@ importName cnm = -- | Map 'bindName' over a list of names and signatures, returning an updated -- 'CryptolEnv' and a list of fresh SAWCore variables. -bindNames :: SharedContext -> [(C.Name, C.Schema)] -> CryptolEnv -> IO (CryptolEnv, [Term]) -bindNames _ [] env0 = pure (env0, []) -bindNames sc ((nm, ty) : binds) env0 = - do (env1, v, _) <- bindName sc nm ty env0 - (env2, vs) <- bindNames sc binds env1 - pure (env2, v : vs) +bindNames :: SharedContext -> [(C.Name, C.Schema)] -> IO [Term] +bindNames _ [] = pure [] +bindNames sc ((nm, ty) : binds) = + do (v, _) <- bindName sc nm ty + vs <- bindNames sc binds + pure (v : vs) -- | Recognize 'Term's of the form @PairType1 a b@. asPairType1 :: Term -> Maybe (Term, Term) @@ -1968,15 +1753,15 @@ scFixedPoints sc vts = -- For Cryptol @foreign@ declarations, we import them as regular -- Cryptol expressions if a Cryptol implementation exists, and as an -- opaque constant otherwise. -importDeclGroup :: DeclGroupOptions -> SharedContext -> CryptolEnv -> C.DeclGroup -> IO CryptolEnv -importDeclGroup declOpts sc env0 (C.Recursive decls) = +importDeclGroup :: DeclGroupOptions -> SharedContext -> C.DeclGroup -> IO () +importDeclGroup declOpts sc (C.Recursive decls) = do let binds = [ (C.dName d, C.dSignature d) | d <- decls ] - (env2, vs) <- bindNames sc binds env0 + vs <- bindNames sc binds let extractDeclExpr decl = case C.dDefinition decl of C.DExpr expr -> - importExpr' sc env2 (C.dSignature decl) expr + importExpr' sc (C.dSignature decl) expr C.DForeign _ mexpr -> case mexpr of Nothing -> @@ -1986,7 +1771,7 @@ importDeclGroup declOpts sc env0 (C.Recursive decls) = , " " <> CryPP.pp decl ] Just expr -> - importExpr' sc env2 (C.dSignature decl) expr + importExpr' sc (C.dSignature decl) expr C.DPrim -> panic "importDeclGroup" [ "Primitive declarations cannot be recursive: " @@ -2015,20 +1800,19 @@ importDeclGroup declOpts sc env0 (C.Recursive decls) = -- NOTE: The eAllTerms fields of env2 and the following Env -- are different. The same names bound in env2 are now bound to -- the output of the fixed-point operator: - pure $ env0 { - eAllTerms = Map.union rhss (eAllTerms env0), - eAllVars = eAllVars env2 - } + addAllTerms sc rhss + addAllVars sc (Map.fromList binds) -importDeclGroup declOpts sc env (C.NonRecursive decl) = do + +importDeclGroup declOpts sc (C.NonRecursive decl) = do rhs <- case C.dDefinition decl of C.DForeign _ mexpr | TopLevelDeclGroup _ <- declOpts -> case mexpr of - Nothing -> importOpaque sc env (C.dName decl) (C.dSignature decl) + Nothing -> importOpaque sc (C.dName decl) (C.dSignature decl) Just expr -> do - rhs <- importExpr' sc env (C.dSignature decl) expr - importConstant sc env (C.dName decl) (C.dSignature decl) rhs + rhs <- importExpr' sc (C.dSignature decl) expr + importConstant sc (C.dName decl) (C.dSignature decl) rhs | otherwise -> panic "importDeclGroup" [ "Foreign declarations only allowed at top level: " <> @@ -2037,7 +1821,7 @@ importDeclGroup declOpts sc env (C.NonRecursive decl) = do C.DPrim | TopLevelDeclGroup primOpts <- declOpts -> - importPrimitive sc primOpts env (C.dName decl) (C.dSignature decl) + importPrimitive sc primOpts (C.dName decl) (C.dSignature decl) | otherwise -> panic "importDeclGroup" [ "Primitive declarations only allowed at top-level: " <> @@ -2045,16 +1829,13 @@ importDeclGroup declOpts sc env (C.NonRecursive decl) = do ] C.DExpr expr -> do - rhs <- importExpr' sc env (C.dSignature decl) expr + rhs <- importExpr' sc (C.dSignature decl) expr case declOpts of TopLevelDeclGroup _ -> - importConstant sc env (C.dName decl) (C.dSignature decl) rhs + importConstant sc (C.dName decl) (C.dSignature decl) rhs NestedDeclGroup -> return rhs - - pure env { - eAllTerms = Map.insert (C.dName decl) rhs (eAllTerms env), - eAllVars = Map.insert (C.dName decl) (C.dSignature decl) (eAllVars env) - } + addAllTerms sc (Map.singleton (C.dName decl) rhs) + addAllVars sc (Map.singleton (C.dName decl) (C.dSignature decl)) -- | Type holding a setting for the way we import Cryptol primitives. -- @@ -2081,77 +1862,77 @@ data DeclGroupOptions | NestedDeclGroup -- | Import a list of (non-top-level) Cryptol `C.DeclGroup` into the `CryptolEnv`. -importDeclGroups :: SharedContext -> CryptolEnv -> [C.DeclGroup] -> IO CryptolEnv -importDeclGroups sc = foldM (importDeclGroup NestedDeclGroup sc) +importDeclGroups :: SharedContext -> [C.DeclGroup] -> IO () +importDeclGroups sc = mapM_ (importDeclGroup NestedDeclGroup sc) -- | Import a list of top-level Cryptol `C.DeclGroup` into the `CryptolEnv`. -importTopLevelDeclGroups :: SharedContext -> ImportPrimitiveOptions -> CryptolEnv -> [C.DeclGroup] -> IO CryptolEnv -importTopLevelDeclGroups sc primOpts = foldM (importDeclGroup (TopLevelDeclGroup primOpts) sc) +importTopLevelDeclGroups :: SharedContext -> ImportPrimitiveOptions -> [C.DeclGroup] -> IO () +importTopLevelDeclGroups sc primOpts = mapM_ (importDeclGroup (TopLevelDeclGroup primOpts) sc) -coerceTerm :: SharedContext -> CryptolEnv -> C.Type -> C.Type -> Term -> IO Term -coerceTerm sc env t1 t2 e +coerceTerm :: SharedContext -> C.Type -> C.Type -> Term -> IO Term +coerceTerm sc t1 t2 e | t1 == t2 = do return e | otherwise = - do t1' <- importType sc env t1 - t2' <- importType sc env t2 + do t1' <- importType sc t1 + t2' <- importType sc t2 same <- scSubtype sc t1' t2' case same of True -> pure e -- ascribe type t2' to e False -> - do q <- proveEq sc env t1 t2 + do q <- proveEq sc t1 t2 scGlobalApply sc "Prelude.coerce" [t1', t2', q, e] -proveEq :: SharedContext -> CryptolEnv -> C.Type -> C.Type -> IO Term -proveEq sc env t1 t2 +proveEq :: SharedContext -> C.Type -> C.Type -> IO Term +proveEq sc t1 t2 | t1 == t2 = do s <- scSort sc (mkSort 0) - t' <- importType sc env t1 + t' <- importType sc t1 scGlobalApply sc "Prelude.Refl" [s, t'] | otherwise = case (C.tNoUser t1, C.tNoUser t2) of (C.tIsSeq -> Just (n1, a1), C.tIsSeq -> Just (n2, a2)) -> - do n1' <- importType sc env n1 - n2' <- importType sc env n2 - a1' <- importType sc env a1 - a2' <- importType sc env a2 + do n1' <- importType sc n1 + n2' <- importType sc n2 + a1' <- importType sc a1 + a2' <- importType sc a2 num <- scGlobalApply sc "Cryptol.Num" [] nEq <- if n1 == n2 then scGlobalApply sc "Prelude.Refl" [num, n1'] else scGlobalApply sc "Prelude.unsafeAssert" [num, n1', n2'] - aEq <- proveEq sc env a1 a2 + aEq <- proveEq sc a1 a2 if a1 == a2 then scGlobalApply sc "Cryptol.seq_cong1" [n1', n2', a1', nEq] else scGlobalApply sc "Cryptol.seq_cong" [n1', n2', a1', a2', nEq, aEq] (C.tIsIntMod -> Just n1, C.tIsIntMod -> Just n2) -> - do n1' <- importType sc env n1 - n2' <- importType sc env n2 + do n1' <- importType sc n1 + n2' <- importType sc n2 num <- scGlobalApply sc "Cryptol.Num" [] nEq <- if n1 == n2 then scGlobalApply sc "Prelude.Refl" [num, n1'] else scGlobalApply sc "Prelude.unsafeAssert" [num, n1', n2'] scGlobalApply sc "Cryptol.IntModNum_cong" [n1', n2', nEq] (C.tIsFun -> Just (a1, b1), C.tIsFun -> Just (a2, b2)) -> - do a1' <- importType sc env a1 - a2' <- importType sc env a2 - b1' <- importType sc env b1 - b2' <- importType sc env b2 - aEq <- proveEq sc env a1 a2 - bEq <- proveEq sc env b1 b2 + do a1' <- importType sc a1 + a2' <- importType sc a2 + b1' <- importType sc b1 + b2' <- importType sc b2 + aEq <- proveEq sc a1 a2 + bEq <- proveEq sc b1 b2 scGlobalApply sc "Cryptol.fun_cong" [a1', a2', b1', b2', aEq, bEq] (tIsPair -> Just (a1, b1), tIsPair -> Just (a2, b2)) -> - do a1' <- importType sc env a1 - a2' <- importType sc env a2 - b1' <- importType sc env b1 - b2' <- importType sc env b2 - aEq <- proveEq sc env a1 a2 - bEq <- proveEq sc env b1 b2 + do a1' <- importType sc a1 + a2' <- importType sc a2 + b1' <- importType sc b1 + b2' <- importType sc b2 + aEq <- proveEq sc a1 a2 + bEq <- proveEq sc b1 b2 if b1 == b2 then scGlobalApply sc "Cryptol.pair_cong1" [a1', a2', b1', aEq] else if a1 == a2 then scGlobalApply sc "Cryptol.pair_cong2" [a1', b1', b2', bEq] else scGlobalApply sc "Cryptol.pair_cong" [a1', a2', b1', b2', aEq, bEq] (tIsRecord -> Just (s1, a1, b1), tIsRecord -> Just (s2, a2, b2)) | s1 == s2 -> - proveRecordEq sc env s1 a1 b1 a2 b2 + proveRecordEq sc s1 a1 b1 a2 b2 (C.tIsNominal -> Just (nt1, ts1), C.tIsNominal -> Just (nt2, ts2)) -- We prove equality between newtype values by equating the types of @@ -2161,7 +1942,7 @@ proveEq sc env t1 t2 , Just (s1, a1, b1) <- tIsRecord (C.tRec (newtypeRecordFields nt1 ts1 con1)) , Just (s2, a2, b2) <- tIsRecord (C.tRec (newtypeRecordFields nt2 ts2 con2)) , s1 == s2 -> - proveRecordEq sc env s1 a1 b1 a2 b2 + proveRecordEq sc s1 a1 b1 a2 b2 | C.Enum {} <- C.ntDef nt1 , C.Enum {} <- C.ntDef nt2 -> @@ -2193,7 +1974,6 @@ proveEq sc env t1 t2 -- values. proveRecordEq :: SharedContext -> - CryptolEnv -> -- | The @RecordType@ field's name. C.Ident -> -- | The left-hand-side @RecordType@'s field type. @@ -2205,13 +1985,13 @@ proveRecordEq :: -- | The rest of the right-hand-side @RecordType@'s type. C.Type -> IO Term -proveRecordEq sc env s a1 b1 a2 b2 = - do a1' <- importType sc env a1 - a2' <- importType sc env a2 - b1' <- importType sc env b1 - b2' <- importType sc env b2 - aEq <- proveEq sc env a1 a2 - bEq <- proveEq sc env b1 b2 +proveRecordEq sc s a1 b1 a2 b2 = + do a1' <- importType sc a1 + a2' <- importType sc a2 + b1' <- importType sc b1 + b2' <- importType sc b2 + aEq <- proveEq sc a1 a2 + bEq <- proveEq sc b1 b2 s' <- scString sc (C.identText s) if b1 == b2 then scGlobalApply sc "Cryptol.record_cong1" [s', a1', a2', b1', aEq] @@ -2257,18 +2037,18 @@ tIsRecord t = -------------------------------------------------------------------------------- -- List comprehensions -importComp :: SharedContext -> CryptolEnv -> C.Type -> C.Type -> C.Expr -> [[C.Match]] -> IO Term -importComp sc env lenT elemT expr mss = +importComp :: SharedContext -> C.Type -> C.Type -> C.Expr -> [[C.Match]] -> IO Term +importComp sc lenT elemT expr mss = do let zipAll [] = panic "importComp" ["zero-branch list comprehension"] zipAll [branch] = - do (xs, len, ty, args) <- importMatches sc env branch - m <- importType sc env len - a <- importType sc env ty + do (xs, len, ty, args) <- importMatches sc branch + m <- importType sc len + a <- importType sc ty return (xs, m, a, [args], len) zipAll (branch : branches) = - do (xs, len, ty, args) <- importMatches sc env branch - m <- importType sc env len - a <- importType sc env ty + do (xs, len, ty, args) <- importMatches sc branch + m <- importType sc len + a <- importType sc ty (ys, n, b, argss, len') <- zipAll branches ab <- scTupleType sc [a, b] if len == len' then @@ -2279,35 +2059,35 @@ importComp sc env lenT elemT expr mss = mn <- scGlobalApply sc "Cryptol.tcMin" [m, n] return (zs, mn, ab, args : argss, C.tMin len len') (xs, n, a, argss, lenT') <- zipAll mss - f <- lambdaTuples sc env elemT expr argss - b <- importType sc env elemT + f <- lambdaTuples sc elemT expr argss + b <- importType sc elemT ys <- scGlobalApply sc "Cryptol.seqMap" [a, b, n, f, xs] -- The resulting type might not match the annotation, so we coerce - coerceTerm sc env (C.tSeq lenT' elemT) (C.tSeq lenT elemT) ys + coerceTerm sc (C.tSeq lenT' elemT) (C.tSeq lenT elemT) ys -lambdaTuples :: SharedContext -> CryptolEnv -> C.Type -> C.Expr -> [[(C.Name, C.Type)]] -> IO Term -lambdaTuples sc env ty expr [] = importExpr' sc env (C.tMono ty) expr -lambdaTuples sc env ty expr (args : argss) = - do f <- lambdaTuple sc env ty expr argss args +lambdaTuples :: SharedContext -> C.Type -> C.Expr -> [[(C.Name, C.Type)]] -> IO Term +lambdaTuples sc ty expr [] = importExpr' sc (C.tMono ty) expr +lambdaTuples sc ty expr (args : argss) = + do f <- lambdaTuple sc ty expr argss args if null args || null argss then return f - else do a <- importType sc env (tNestedTuple (map snd args)) - b <- importType sc env (tNestedTuple (map (tNestedTuple . map snd) argss)) - c <- importType sc env ty + else do a <- importType sc (tNestedTuple (map snd args)) + b <- importType sc (tNestedTuple (map (tNestedTuple . map snd) argss)) + c <- importType sc ty scGlobalApply sc "Prelude.uncurry" [a, b, c, f] -lambdaTuple :: SharedContext -> CryptolEnv -> C.Type -> C.Expr -> [[(C.Name, C.Type)]] -> [(C.Name, C.Type)] -> IO Term -lambdaTuple sc env ty expr argss [] = lambdaTuples sc env ty expr argss -lambdaTuple sc env ty expr argss ((x, t) : args) = - do a <- importType sc env t - (env',x',_) <- bindName sc x (C.Forall [] [] t) env - e <- lambdaTuple sc env' ty expr argss args +lambdaTuple :: SharedContext -> C.Type -> C.Expr -> [[(C.Name, C.Type)]] -> [(C.Name, C.Type)] -> IO Term +lambdaTuple sc ty expr argss [] = lambdaTuples sc ty expr argss +lambdaTuple sc ty expr argss ((x, t) : args) = + do a <- importType sc t + (x',_) <- bindName sc x (C.Forall [] [] t) + e <- lambdaTuple sc ty expr argss args f <- scAbstractTerms sc [x'] e if null args then return f - else do b <- importType sc env (tNestedTuple (map snd args)) + else do b <- importType sc (tNestedTuple (map snd args)) let tuple = tNestedTuple (map (tNestedTuple . map snd) argss) - c <- importType sc env (if null argss then ty else C.tFun tuple ty) + c <- importType sc (if null argss then ty else C.tFun tuple ty) scGlobalApply sc "Prelude.uncurry" [a, b, c, f] tNestedTuple :: [C.Type] -> C.Type @@ -2320,19 +2100,20 @@ tNestedTuple (t : ts) = C.tTuple [t, tNestedTuple ts] -- variables. -- -- XXX: clean up the cutpaste -importMatches :: SharedContext -> CryptolEnv -> [C.Match] +importMatches :: SharedContext -> [C.Match] -> IO (Term, C.Type, C.Type, [(C.Name, C.Type)]) -importMatches _sc _env [] = +importMatches _sc [] = panic "importMatches" ["empty comprehension branch"] -importMatches sc env [C.From name _len _eltty expr] = do - xs <- importExpr sc env expr +importMatches sc [C.From name _len _eltty expr] = do + xs <- importExpr sc expr + allvars <- eAllVars sc -- FUTURE: we could use scTypeOf here and return SAWCore types out; -- the only complication appears to be that we'd have to lift the -- length type back to Cryptol in the caller, and for the moment -- that's problematic without at least tracking forall-bound tyvars -- in the environment. - let ty'expr = fastTypeOf (eAllVars env) expr + let ty'expr = fastTypeOf allvars expr (len, ty) <- case C.tIsSeq ty'expr of Just x -> return x Nothing -> @@ -2342,10 +2123,11 @@ importMatches sc env [C.From name _len _eltty expr] = do ] return (xs, len, ty, [(name, ty)]) -importMatches sc env (C.From name _len _eltty expr : matches) = do - xs <- importExpr sc env expr +importMatches sc (C.From name _len _eltty expr : matches) = do + xs <- importExpr sc expr + allvars <- eAllVars sc -- FUTURE: likewise as above - let ty'expr = fastTypeOf (eAllVars env) expr + let ty'expr = fastTypeOf allvars expr (len1, ty1) <- case C.tIsSeq ty'expr of Just x -> return x Nothing -> @@ -2353,18 +2135,18 @@ importMatches sc env (C.From name _len _eltty expr : matches) = do "Not sequence type: " <> CryPP.pp ty'expr, "Expression: " <> CryPP.pp expr ] - m <- importType sc env len1 - a <- importType sc env ty1 - (env',v,_) <- bindName sc name (C.Forall [] [] ty1) env - (body, len2, ty2, args) <- importMatches sc env' matches - n <- importType sc env len2 - b <- importType sc env ty2 + m <- importType sc len1 + a <- importType sc ty1 + (v,_) <- bindName sc name (C.Forall [] [] ty1) + (body, len2, ty2, args) <- importMatches sc matches + n <- importType sc len2 + b <- importType sc ty2 f <- scAbstractTerms sc [v] body result <- scGlobalApply sc "Cryptol.from" [a, b, m, n, xs, f] return (result, C.tMul len1 len2, C.tTuple [ty1, ty2], (name, ty1) : args) -importMatches sc env [C.Let decl] = +importMatches sc [C.Let decl] = case C.dDefinition decl of C.DForeign{} -> @@ -2380,18 +2162,18 @@ importMatches sc env [C.Let decl] = ] C.DExpr expr -> do - e <- importExpr sc env expr + e <- importExpr sc expr ty1 <- case C.dSignature decl of C.Forall [] [] ty1 -> return ty1 _ -> panic "importMatches" [ "Unimplemented: polymorphic Let", " " <> CryPP.pp decl ] - a <- importType sc env ty1 + a <- importType sc ty1 result <- scGlobalApply sc "Prelude.single" [a, e] return (result, C.tOne, ty1, [(C.dName decl, ty1)]) -importMatches sc env (C.Let decl : matches) = +importMatches sc (C.Let decl : matches) = case C.dDefinition decl of C.DForeign{} -> @@ -2407,18 +2189,18 @@ importMatches sc env (C.Let decl : matches) = ] C.DExpr expr -> do - e <- importExpr sc env expr + e <- importExpr sc expr ty1 <- case C.dSignature decl of C.Forall [] [] ty1 -> return ty1 _ -> panic "importMatches" [ "Unimplemented: polymorphic Let", " " <> CryPP.pp decl ] - (env', v, _) <- bindName sc (C.dName decl) (C.dSignature decl) env - (body, len, ty2, args) <- importMatches sc env' matches - n <- importType sc env len - a <- importType sc env ty1 - b <- importType sc env ty2 + (v, _) <- bindName sc (C.dName decl) (C.dSignature decl) + (body, len, ty2, args) <- importMatches sc matches + n <- importType sc len + a <- importType sc ty1 + b <- importType sc ty2 f <- scAbstractTerms sc [v] body result <- scGlobalApply sc "Cryptol.mlet" [a, b, n, e, f] return (result, len, C.tTuple [ty1, ty2], (C.dName decl, ty1) : args) @@ -2427,78 +2209,30 @@ importMatches sc env (C.Let decl : matches) = ------------------------------------------------------------ -- Translate (wrappers around import) -getAllIfaceDecls :: ME.ModuleEnv -> MI.IfaceDecls -getAllIfaceDecls me = - mconcat - (map (MI.ifDefines . ME.lmInterface) - (ME.getLoadedModules (ME.meLoadedModules me))) --- | Regenerate the `eAllVars` field. --- --- This is necessary, for now, because before we merged `CryptolEnv` --- with the separate @Env@ type used by the import logic in --- Cryptol.hs, the `eAllVars` field was built on the fly when --- dropping to @Env@ and thrown away when coming back. The calls to --- this function correspond to the places `eAllVars` it was --- previously built on the fly. --- --- `eAllVars` may or may not actually go out of date. That depends --- on whether everything else that /should/ update it actually --- /does/, which might or might not be true (because we would have --- gotten away with not doing so in the past, in at least some --- cases) and requires a general audit of everything in these two --- files to resolve. --- -refreshCryptolEnv :: CryptolEnv -> IO CryptolEnv -refreshCryptolEnv env = - do -- Drop the existing eAllVars and regenerate it from scratch. - -- (We used to not carry it around and always just build it here, - -- so it's not clear if the copy we carry around is still valid.) - let modEnv = eModuleEnv env - let ifaceDecls = getAllIfaceDecls modEnv - let newtypeCons = Map.fromList - [ con - | nt <- Map.elems (MI.ifNominalTypes ifaceDecls) - , con <- C.nominalTypeConTypes nt - ] - vars = Map.map MI.ifDeclSig $ MI.ifDecls ifaceDecls - allvars = newtypeCons `Map.union` vars - let allvars' = Map.union (eExtraVars env) allvars - pure $ env { - eAllVars = allvars' - } - -translateType :: SharedContext -> CryptolEnv -> C.Type -> IO Term -translateType sc env ty = do - env' <- refreshCryptolEnv env - importType sc env' ty - -translateSchema :: SharedContext -> CryptolEnv -> C.Schema -> IO Term -translateSchema sc env ty = do - env' <- refreshCryptolEnv env - importSchema sc env' ty - -translateExpr :: SharedContext -> CryptolEnv -> C.Expr -> IO Term -translateExpr sc env expr = - do env' <- refreshCryptolEnv env - -- Does not change the environment (obviously) - importExpr sc env' expr +translateType :: SharedContext -> C.Type -> IO Term +translateType sc ty = importType sc ty + +translateSchema :: SharedContext -> C.Schema -> IO Term +translateSchema sc ty = importSchema sc ty + +translateExpr :: SharedContext -> C.Expr -> IO Term +translateExpr sc expr = importExpr sc expr translateDeclGroups :: SharedContext -> CryptolEnv -> [C.DeclGroup] -> IO CryptolEnv -translateDeclGroups sc env0 dgs = - do env1 <- refreshCryptolEnv env0 +translateDeclGroups sc env1 dgs = + do -- updates eAllTerms and eAllVars, leaves the rest alone - env2 <- importTopLevelDeclGroups sc defaultPrimitiveOptions env1 dgs + importTopLevelDeclGroups sc defaultPrimitiveOptions dgs let decls = concatMap C.groupDecls dgs let newNames = map C.dName decls let newVars = Map.fromList [ (C.dName d, C.dSignature d) | d <- decls ] + addExtraVars sc newVars + let addName name = MR.shadowing (MN.singletonNS C.NSValue (C.mkUnqual (C.nameIdent name)) name) - pure env2 { - eExtraNaming = foldr addName (eExtraNaming env2) newNames, - eExtraVars = Map.union (eExtraVars env2) newVars - } + return $ mapNaming (\ne -> foldr addName ne newNames) env1 -------------------------------------------------------------------------------- -- Utilities: @@ -2681,14 +2415,14 @@ exportRecordValue fields v = genCodeForNominalTypes :: HasCallStack => - SharedContext -> Map C.Name NominalType -> CryptolEnv -> IO CryptolEnv -genCodeForNominalTypes sc nominalMap env0 = - foldM updateEnvForNominal env0 nominalMap + SharedContext -> Map C.Name NominalType -> IO () +genCodeForNominalTypes sc nominalMap = + mapM_ updateEnvForNominal nominalMap where - updateEnvForNominal :: CryptolEnv -> NominalType -> IO CryptolEnv - updateEnvForNominal env nt = do + updateEnvForNominal :: NominalType -> IO () + updateEnvForNominal nt = do let kinds = map C.tpKind (C.ntParams nt) unless (all (`elem` [C.KType, C.KNum]) kinds) $ panic "genCodeForNominalTypes" [ @@ -2696,23 +2430,22 @@ genCodeForNominalTypes sc nominalMap env0 = Text.unlines $ map CryPP.pp kinds ] - constrs <- newDefsForNominal env nt + constrs <- newDefsForNominal nt let conTs = C.nominalTypeConTypes nt - return env { - eAllTerms = foldr (uncurry Map.insert) (eAllTerms env) constrs, - eAllVars = foldr (uncurry Map.insert) (eAllVars env) conTs - } + addAllTerms sc (Map.fromList constrs) + addAllVars sc (Map.fromList conTs) + -- NOTE: the Cryptol schemas for the Struct & Enum constructors get added to -- the Cryptol environment. -- | Create functions/constructors for different 'NominalType's. newDefsForNominal :: - HasCallStack => CryptolEnv -> NominalType -> IO [(C.Name,Term)] - newDefsForNominal env nt = + HasCallStack => NominalType -> IO [(C.Name,Term)] + newDefsForNominal nt = case C.ntDef nt of C.Abstract -> return [] - C.Enum x -> genCodeForEnum sc env nt x + C.Enum x -> genCodeForEnum sc nt x -- returns constructors, everything else put directly into -- SAWCore environment. @@ -2727,7 +2460,7 @@ genCodeForNominalTypes sc nominalMap env0 = -- FIXME: this doesn't seem foolproof! fn = C.EAbs paramName recTy (C.EVar paramName) fnWithTAbs = foldr C.ETAbs fn (C.ntParams nt) - e <- importExpr sc env fnWithTAbs + e <- importExpr sc fnWithTAbs return [(conNm, e)] @@ -2758,8 +2491,8 @@ genCodeForNominalTypes sc nominalMap env0 = -- genCodeForEnum :: HasCallStack => - SharedContext -> CryptolEnv -> NominalType -> [C.EnumCon] -> IO [(C.Name,Term)] -genCodeForEnum sc env nt ctors = + SharedContext -> NominalType -> [C.EnumCon] -> IO [(C.Name,Term)] +genCodeForEnum sc nt ctors = do let ntName' = ntName nt numCtors = length ctors @@ -2777,13 +2510,13 @@ genCodeForEnum sc env nt ctors = -- | create variables for the type Params: -- tyParamsVars <- mapM (scVariable sc) tyParamsECs - (envWithTParams,tks) <- + ((),tks) <- mapAccumLM - (\env' tpi -> do - (env'',ty,k) <- bindTParam' sc tpi env' - return (env'', (ty,k)) + (\() tpi -> do + (ty,k) <- bindTParam' sc tpi + return ((), (ty,k)) ) - env + () tyParamsInfo let (tyParamsVars, tyParamsKinds) = unzip tks @@ -2852,7 +2585,7 @@ genCodeForEnum sc env nt ctors = (argTypes_eachCtor :: [[Term]]) <- forM ctors $ \c-> -- for each constructor forM (C.ecFields c) -- for each constructor field (type) - (importType sc envWithTParams) + (importType sc) -- map the list of types to the product type: represType_eachCtor <- forM argTypes_eachCtor $ \ts -> @@ -3048,13 +2781,14 @@ genCodeForEnum sc env nt ctors = -- importCase :: HasCallStack => - SharedContext -> CryptolEnv -> + SharedContext -> C.Type -> C.Expr -> Map C.Ident C.CaseAlt -> Maybe C.CaseAlt -> IO Term -importCase sc env tyResult scrutinee altsMap mDfltAlt = +importCase sc tyResult scrutinee altsMap mDfltAlt = do + allvars <- eAllVars sc -- FUTURE: consider using scTypeOf once we have an information- -- preserving translation of enum types into SAWCore. - let scrutineeTy = fastTypeOf (eAllVars env) scrutinee + let scrutineeTy = fastTypeOf allvars scrutinee (nm,ctors,tyParams,tyArgs) <- case scrutineeTy of (C.tIsNominal -> Just (C.NominalType{C.ntDef=C.Enum ctors, ntName=nm, ntParams=tyParams},tyArgs)) -> @@ -3169,10 +2903,10 @@ importCase sc env tyResult scrutinee altsMap mDfltAlt = alts -- the Cryptol to SAWCore translations: - tyArgs' <- mapM (importType sc env) tyArgs - tyResult' <- importType sc env tyResult -- type of whole case expr - scrutinee' <- importExpr sc env scrutinee - funcs' <- mapM (importExpr sc env) funcs + tyArgs' <- mapM (importType sc) tyArgs + tyResult' <- importType sc tyResult -- type of whole case expr + scrutinee' <- importExpr sc scrutinee + funcs' <- mapM (importExpr sc) funcs caseExpr <- scGlobalApply sc (identOfEnumCase nm) $ tyArgs' -- case is expecting the type arguments -- that the enumtype is instantiated to diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index f79dc80c13..ba3240e499 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -27,7 +27,8 @@ module CryptolSAWCore.CryptolEnv -- needs to be reorganized, after which these exports can go away. -- (The definitions used to live here.) ( ImportVisibility(..) - , CryptolEnv(..) + , CryptolEnv + , withFileReader , ExtCryptolModule(..) , prettyExtCryptolModule @@ -37,7 +38,6 @@ module CryptolSAWCore.CryptolEnv , bindExtCryptolModule , extractDefFromExtCryptolModule - , restoreCryptolEnv , importCryptolModule , bindExtraVar , withExtraVar @@ -45,10 +45,12 @@ module CryptolSAWCore.CryptolEnv , bindIntegerType , parseTypedTerm , pExprToTypedTerm + , inferExpr , parseDecls , parseSchema , declareName , getNamingEnv + , getCompleteNamingEnv , InputText(..) , lookupIn , resolveIdentifier @@ -60,7 +62,7 @@ module CryptolSAWCore.CryptolEnv -- base & standard modules: import Control.Monad(when) -import Data.ByteString (ByteString) +import Data.ByteString as BS (ByteString, readFile) import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe (fromMaybe) @@ -68,6 +70,7 @@ import qualified Data.Set as Set import Data.Set (Set) import qualified Data.Text as Text import Data.Text (Text, pack, splitOn) +import Data.Typeable import GHC.Stack import System.Environment (lookupEnv) import System.Environment.Executable (splitExecutablePath) @@ -79,7 +82,6 @@ import Prettyprinter ((<+>)) -- cryptol pkg: import qualified Cryptol.Eval as E -import qualified Cryptol.ModuleSystem as M import qualified Cryptol.ModuleSystem.Base as MB import qualified Cryptol.ModuleSystem.Env as ME import Cryptol.ModuleSystem.Env (ModContextParams(NoParams)) @@ -111,18 +113,16 @@ import Cryptol.Utils.Logger (quietLogger) -- local: import qualified CryptolSAWCore.Cryptol as C -import CryptolSAWCore.Cryptol (ImportVisibility(..), CryptolEnv(..)) - -- These used to live in this file, so import them - -- unqualified for now. - -- XXX: tidy up +import CryptolSAWCore.GlobalCryptolEnv import CryptolSAWCore.Panic import qualified CryptolSAWCore.Pretty as CryPP import CryptolSAWCore.TypedTerm import SAWCore.Name (nameInfo) import SAWCore.Recognizer (asConstant) -import SAWCore.SharedTerm (NameInfo, SharedContext, Term, ppTerm) +import SAWCore.SharedTerm (NameInfo, SharedContext, Term, ppTerm, IsMetadata(..), scGetData, scWithData) import SAWSupport.Console import qualified SAWSupport.Pretty as PPS +import Control.Monad.IO.Class ---- Key Types ----------------------------------------------------------------- @@ -181,6 +181,14 @@ nameMatcher nm0 = in last cs == identText (C.ogName og) && init cs == C.modNameChunksText top ++ map identText ns +newtype FileReader = FileReader (FilePath -> IO ByteString) + deriving Typeable + +instance IsMetadata FileReader where + initMetadata = return $ FileReader BS.readFile + +withFileReader :: (MonadIO m) => SharedContext -> (FilePath -> IO ByteString) -> m a -> m a +withFileReader sc fileReader = scWithData sc (\_ -> FileReader fileReader) -- Initialize ------------------------------------------------------------------ @@ -192,11 +200,8 @@ nameMatcher nm0 = -- NOTE: submodules in these built-in modules are supported in this code. -- initCryptolEnv :: - (?fileReader :: FilePath -> IO ByteString) => SharedContext -> IO CryptolEnv initCryptolEnv sc = do - modEnv0 <- M.initialModuleEnv - -- Set the Cryptol include path (TODO: we may want to do this differently) (binDir, _) <- splitExecutablePath let instDir = normalise . joinPath . init . splitPath $ binDir @@ -211,20 +216,20 @@ initCryptolEnv sc = do #else splitSearchPath path #endif - let modEnv1 = modEnv0 { ME.meSearchPath = cryptolPaths ++ - (instDir "lib") : ME.meSearchPath modEnv0 } - - -- Load Cryptol prelude and magic Array module - (_, modEnv2) <- - liftModuleM modEnv1 $ - do _ <- MB.loadModuleFrom False (MM.FromModule preludeName) - _ <- MB.loadModuleFrom False (MM.FromModule arrayName) - return () - - -- Load Cryptol reference implementation - ((_,refTop), modEnv3) <- - liftModuleM modEnv2 $ - MB.loadModuleFrom False (MM.FromModule preludeReferenceName) + + -- initialize the module environment stored in the context + initModEnv <- ME.initialModuleEnv + setModuleEnv sc $ initModEnv + { ME.meSearchPath = cryptolPaths ++ + (instDir "lib") : ME.meSearchPath initModEnv + } + (_,refTop) <- liftModuleM sc $ do + -- Load Cryptol prelude and magic Array module + _ <- MB.loadModuleFrom False (MM.FromModule preludeName) + _ <- MB.loadModuleFrom False (MM.FromModule arrayName) + -- Load Cryptol reference implementation + MB.loadModuleFrom False (MM.FromModule preludeReferenceName) + let refMod = T.tcTopEntityToModule refTop -- Set up reference implementation redirections @@ -240,51 +245,30 @@ initCryptolEnv sc = do preludeReferenceName' = locatedUnknown preludeReferenceName arrayName' = locatedUnknown arrayName - let env0 = CryptolEnv - { eImports = + let env0 = C.mapImports (\_ -> [ mkImport OnlyPublic preludeName' Nothing Nothing , mkImport OnlyPublic preludeReferenceName' (Just preludeReferenceName) Nothing , mkImport OnlyPublic arrayName' Nothing Nothing - ] - , eModuleEnv = modEnv3 - , eExtraNaming = mempty - , eExtraVars = Map.empty - , eExtraTySyns = Map.empty - , eAllVars = Map.empty - , eTyVars = Map.empty - , eTyProps = Map.empty - , eAllTerms = Map.empty - , eRefPrims = refPrims - , ePrims = Map.empty - , ePrimTypes = Map.empty - , eFFITypes = Map.empty - } - + ]) $ C.initEnv + C.addRefPrims sc refPrims -- Generate SAWCore translations for all values in scope - env1 <- genTermEnv sc modEnv3 env0 - - -- Clear `eRefPrims`. This preserves the behavior from before - -- `CryptolEnv` and the old additional `Env` type were merged. It - -- isn't clear if this is correct or not, but I don't want the code - -- cleanup to change the behavior. - return env1 { - eRefPrims = Map.empty - } + genTermEnv sc + return env0 -- | Translate all declarations in all loaded modules to SAWCore terms. -- NOTE: used only for initialization code. -- -genTermEnv :: SharedContext -> ME.ModuleEnv -> C.CryptolEnv -> IO C.CryptolEnv -genTermEnv sc modEnv env0 = do +genTermEnv :: SharedContext -> IO () +genTermEnv sc = do + modEnv <- eModuleEnv sc let declGroups = concatMap T.mDecls $ filter (not . T.isParametrizedModule) $ ME.loadedModules modEnv nominals = loadedNonParamNominalTypes modEnv -- These update eAllTerms and eAllVars and leave the rest alone - env1 <- C.genCodeForNominalTypes sc nominals env0 - env2 <- C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions env1 declGroups - return env2 + C.genCodeForNominalTypes sc nominals + C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions declGroups -- Parse ----------------------------------------------------------------------- @@ -324,23 +308,41 @@ ioParseResult res = case res of -- NamingEnv and Related ------------------------------------------------------- -- | Get the full 'MR.NamingEnv' based on all the imports (from --- `eImports`), plus all the local "extra" decls too. Note that the --- imports are combined with `mconcat`, which uses the `Semigroup` +-- all `sImports` in the scope stack), +-- plus all the local "extra" decls too. +-- At each scoping level, the imports are combined with `mconcat`, +-- which uses the `Semigroup` -- instance for `MR.NamingEnv` to ambiguate any names that appear --- more than once, but the "extra" decls are (specifically) bolted --- on with `MR.shadowing` so they hide any previous occurrences. +-- more than once. The "extra" declarations are then (specifically) bolted +-- on with `MR.shadowing` so they hide any imported occurrences. +-- The environment for each scoping level then shadows everything +-- above it. + -- --- Note that while `eImports` is (mostly) maintained with more +-- Note that while each `sImports` is (mostly) maintained with more -- recent imports at the front of the list, this should be -- irrelevant to name resolution. -- -getNamingEnv :: CryptolEnv -> MR.NamingEnv -getNamingEnv env = - eExtraNaming env - `MR.shadowing` - (mconcat $ map (getNamingEnvForImport (eModuleEnv env)) - (eImports env) - ) + +getNamingEnv :: SharedContext -> CryptolEnv -> IO MR.NamingEnv +getNamingEnv sc env = do + modEnv <- eModuleEnv sc + return $ eExtraNaming env + `MR.shadowing` + (mconcat $ map (getNamingEnvForImport modEnv) + (eImports env) + ) + +-- | Compute a 'MR.NamingEnv' that includes *all* +-- public and private names from all loaded modules and signatures. +getCompleteNamingEnv :: SharedContext -> CryptolEnv -> IO MR.NamingEnv +getCompleteNamingEnv sc env = do + modEnv <- eModuleEnv sc + let lms = ME.meLoadedModules modEnv + return $ eExtraNaming env `MR.shadowing` + ((mconcat $ map (\lm -> computeNamingEnv lm PublicAndPrivate) + (ME.lmLoadedModules lms ++ ME.lmLoadedParamModules lms)) + <> (mconcat $ map ME.lmNamingEnv (ME.lmLoadedSignatures lms))) -- | Get the `MR.NamingEnv` for one `T.Import`. getNamingEnvForImport :: ME.ModuleEnv @@ -454,27 +456,6 @@ runInferOutput out = MM.typeCheckingFailed nm errs ----- Misc Exports -------------------------------------------------------------- - --- | Restore a `CryptolEnv` from a checkpoint. The first argument --- @chkEnv@ is the `CryptolEnv` saved by / copied into the --- checkpoint; the second argument @newEnv@ is the current one --- we wish to overwrite by rolling back to the checkpoint. --- --- We need to keep the newer name supply so as to not reuse names --- already issued, in case some of those are still floating around --- after the restore. (They should not... but bugs happen.) --- --- We also ought to invalidate terms constructed since the checkpoint --- was taken, like SAWCore does. See #2859. --- -restoreCryptolEnv :: CryptolEnv -> CryptolEnv -> CryptolEnv -restoreCryptolEnv chkEnv newEnv = - let newMEnv = eModuleEnv newEnv - chkMEnv = eModuleEnv chkEnv - menv' = chkMEnv { ME.meNameSeeds = ME.meNameSeeds newMEnv } - in - chkEnv { eModuleEnv = menv' } ---- Types and functions for CryptolModule & ExtCryptolModule ------------------ @@ -546,17 +527,16 @@ prettyExtCryptolModule = -- user binds the `CryptolModule` returned here at the SAW -- command line. loadExtCryptolModule :: - (?fileReader :: FilePath -> IO ByteString) => SharedContext -> - CryptolEnv -> FilePath -> - IO (ExtCryptolModule, CryptolEnv) -loadExtCryptolModule sc env path = + IO ExtCryptolModule +loadExtCryptolModule sc path = do - (m, env') <- loadAndTranslateModule sc env (Left path) + m <- loadAndTranslateModule sc (Left path) + cm <- mkCryptolModule sc m let doc = PP.vsep [ "Public interface", - prettyCryptolModule (mkCryptolModule m env') + prettyCryptolModule cm ] -- How to show, need to compute this here, because the show function -- (of course) has no access to the state. @@ -568,7 +548,7 @@ loadExtCryptolModule sc env path = -- -- FUTURE: there's no remaining barrier to giving -- prettyCryptolModule access to whatever state it wants. - return (ECM_LoadedModule (locatedUnknown (T.mName m)) doc, env') + return (ECM_LoadedModule (locatedUnknown (T.mName m)) doc) -- | loadCryptolModule - load a Cryptol module and return a handle to it @@ -586,15 +566,13 @@ loadExtCryptolModule sc env path = -- of the module in a `CryptolModule` structure. -- loadCryptolModule :: - (?fileReader :: FilePath -> IO ByteString) => SharedContext -> - CryptolEnv -> FilePath -> - IO (CryptolModule, CryptolEnv) -loadCryptolModule sc env path = + IO (CryptolModule) +loadCryptolModule sc path = do - (mod', env') <- loadAndTranslateModule sc env (Left path) - return (mkCryptolModule mod' env', env') + mod' <- loadAndTranslateModule sc (Left path) + mkCryptolModule sc mod' -- | mkCryptolModule m env - translate a @m :: T.Module@ to a `CryptolModule` @@ -607,15 +585,17 @@ loadCryptolModule sc env path = -- `loadExtCryptolModule` as part of generating the print output. -- Ideally all of this could be consolidated. -- -mkCryptolModule :: T.Module -> CryptolEnv -> CryptolModule -mkCryptolModule m env = +mkCryptolModule :: SharedContext -> T.Module -> IO CryptolModule +mkCryptolModule sc m = do + modEnv <- eModuleEnv sc + allterms <- eAllTerms sc let - ifaceDecls = C.getAllIfaceDecls (eModuleEnv env) + ifaceDecls = C.getAllIfaceDecls modEnv types = Map.map MI.ifDeclSig (MI.ifDecls ifaceDecls) -- we're keeping only the exports of `m`: vNameSet = MEx.exported C.NSValue (T.mExports m) tNameSet = MEx.exported C.NSType (T.mExports m) - in + return $ CryptolModule -- create Map of type synonyms: (Map.filterWithKey @@ -628,7 +608,7 @@ mkCryptolModule m env = $ Map.intersectionWith (\t x -> TypedTerm (TypedTermSchema t) x) types - (eAllTerms env) + allterms ) -- | bindExtCryptolModule - add extra bindings to the Cryptol @@ -666,30 +646,19 @@ mkCryptolModule m env = -- @CHANGES.md@. -- bindExtCryptolModule :: - (P.ModName, ExtCryptolModule) -> CryptolEnv -> CryptolEnv -bindExtCryptolModule (modName, ecm) = + SharedContext -> (P.ModName, ExtCryptolModule) -> CryptolEnv -> IO CryptolEnv +bindExtCryptolModule sc (modName, ecm) = case ecm of - ECM_CryptolModule cm -> bindCryptolModule (modName, cm) - ECM_LoadedModule nm _ -> bindLoadedModule (modName, nm) + ECM_CryptolModule cm -> bindCryptolModule sc (modName, cm) + ECM_LoadedModule nm _ -> bindLoadedModule sc (modName, nm) -- | bindLoadedModule - when we have a @cryptol_load@ created object, -- add the module into the import list. bindLoadedModule :: - (P.ModName, P.Located C.ModName) -> CryptolEnv -> CryptolEnv -bindLoadedModule (asName, origName) env = - env {eImports = mkImport PublicAndPrivate origName (Just asName) Nothing - : eImports env - } - --- | Undo `bindLoadedModule`. Not a general removal function. Not --- exported, and used exactly once below where we want to add a --- module to the import list temporarily. -unbindLoadedModule :: CryptolEnv -> CryptolEnv -unbindLoadedModule env = - env { eImports = pop (eImports env) } - where - pop (_ : imports) = imports - pop [] = panic "unbindLoadedModule" ["Nothing here"] + SharedContext -> (P.ModName, P.Located C.ModName) -> CryptolEnv -> IO CryptolEnv +bindLoadedModule _ (asName, origName) env = + return $ C.mapImports + ((:) (mkImport PublicAndPrivate origName (Just asName) Nothing)) env -- | bindCryptolModule - when we have the @cryptol_prims ()@ created -- object, add the `CryptolModule` to the relevant maps in the @@ -702,15 +671,13 @@ unbindLoadedModule env = -- to handle that stuff better / more like a real module (#2645), it -- can and should be removed. -- -bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv -bindCryptolModule (modName, CryptolModule sm tm) env = - env { eExtraNaming = flip (foldr addName) (Map.keys tm') $ - flip (foldr addTSyn) (Map.keys sm) $ - eExtraNaming env - , eExtraTySyns = Map.union sm (eExtraTySyns env) - , eExtraVars = Map.union (fmap fst tm') (eExtraVars env) - , eAllTerms = Map.union (fmap snd tm') (eAllTerms env) - } +bindCryptolModule :: SharedContext -> (P.ModName, CryptolModule) -> CryptolEnv -> IO CryptolEnv +bindCryptolModule sc (modName, CryptolModule sm tm) env0 = do + addExtraTySyns sc sm + addExtraVars sc (fmap fst tm') + addAllTerms sc (fmap snd tm') + return $ C.mapNaming (flip (foldr addName) (Map.keys tm') . + flip (foldr addTSyn) (Map.keys sm)) env0 where -- | `tm'` is the typed terms from `tm` that have Cryptol schemas tm' = Map.mapMaybe f tm @@ -742,8 +709,7 @@ bindCryptolModule (modName, CryptolModule sm tm) env = -- `unbindLoadedModule`.) -- extractDefFromExtCryptolModule :: - (?fileReader :: FilePath -> IO ByteString) => - SharedContext -> CryptolEnv -> ExtCryptolModule -> Text -> IO (TypedTerm, CryptolEnv) + SharedContext -> CryptolEnv -> ExtCryptolModule -> Text -> IO TypedTerm extractDefFromExtCryptolModule sc env_0 ecm name = case ecm of ECM_LoadedModule loadedModName _ -> @@ -752,18 +718,17 @@ extractDefFromExtCryptolModule sc env_0 ecm name = , C.modNameToText (P.thing loadedModName) ] -- Temporarily insert the module into the imports list - env_1 = bindLoadedModule (localMN, loadedModName) env_0 - expr = noLoc (C.modNameToText localMN <> "::" <> name) - (tt, env_2) <- parseTypedTerm sc env_1 expr - let env_3 = unbindLoadedModule env_2 - pure (tt, env_3) + env_1 <- bindLoadedModule sc (localMN, loadedModName) env_0 + let expr = noLoc (C.modNameToText localMN <> "::" <> name) + tt <- parseTypedTerm sc env_1 expr + pure tt -- FIXME: error message for bad `name` exposes the -- `localMN` to user. Fixing locally is challenging, as -- the error is not an exception we can handle here. ECM_CryptolModule (CryptolModule _ tm) -> case Map.lookup (mkIdent name) (Map.mapKeys MN.nameIdent tm) of - Just t -> return (t, env_0) + Just t -> return t Nothing -> fail $ Text.unpack $ "Binding not found: " <> name -- NOTE RE CALLS TO THIS: @@ -791,14 +756,12 @@ extractDefFromExtCryptolModule sc env_0 ecm name = -- These can probably be unified. -- loadAndTranslateModule :: - (?fileReader :: FilePath -> IO ByteString) => SharedContext {- ^ Shared context for creating terms -} -> - CryptolEnv {- ^ Extend this environment -} -> Either FilePath P.ModName {- ^ Where to find the module -} -> - IO (T.Module, CryptolEnv) -loadAndTranslateModule sc env0 src = - do let modEnv = eModuleEnv env0 - (mtop, modEnv') <- liftModuleM modEnv $ + IO T.Module +loadAndTranslateModule sc src = + do modEnv <- eModuleEnv sc + mtop <- liftModuleM sc $ case src of Left path -> MB.loadModuleByPath True path Right mn -> snd <$> MB.loadModuleFrom True (MM.FromModule mn) @@ -814,7 +777,7 @@ loadAndTranslateModule sc env0 src = ++ " is an interface." checkNotParameterized m - let env1 = env0 { eModuleEnv = modEnv' } + modEnv' <- eModuleEnv sc -- Regenerate SharedTerm environment: let oldModNames = map ME.lmName @@ -829,17 +792,16 @@ loadAndTranslateModule sc env0 src = newNominal = Map.difference (loadedNonParamNominalTypes modEnv') (loadedNonParamNominalTypes modEnv) - env2 <- C.refreshCryptolEnv env1 - -- These update eAllTerms and eAllVars and leave the rest alone - env3 <- C.genCodeForNominalTypes sc newNominal env2 - env4 <- C.importTopLevelDeclGroups - sc C.defaultPrimitiveOptions env3 newDeclGroups + C.genCodeForNominalTypes sc newNominal + C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions newDeclGroups + allterms <- eAllTerms sc + ffiTypes <- eFFITypes sc - ffiTypes' <- updateFFITypes sc m (eAllTerms env4) (eFFITypes env4) - let env5 = env4 { eFFITypes = ffiTypes' } + ffiTypes' <- updateFFITypes sc m allterms ffiTypes + addFFITypes sc ffiTypes' - return (m, env5) + return m -- | Reject unapplied functors. checkNotParameterized :: T.Module -> IO () @@ -891,7 +853,6 @@ updateFFITypes sc m allTerms' eFFITypes' = do -- and public) definitions. -- importCryptolModule :: - (?fileReader :: FilePath -> IO ByteString) => SharedContext {- ^ Shared context for creating terms -} -> CryptolEnv {- ^ Extend this environment -} -> Either FilePath P.ModName {- ^ Where to find the module -} -> @@ -903,9 +864,9 @@ importCryptolModule :: importCryptolModule sc env src as False vis imps = -- importing full module: do - (mod', env') <- loadAndTranslateModule sc env src + mod' <- loadAndTranslateModule sc src let import' = mkImport vis (locatedUnknown (T.mName mod')) as imps - return $ env' {eImports = import' : eImports env } + return $ C.mapImports ((:) import') env importCryptolModule _sc _env (Right __nm) _as True _vis _imps = -- importing submodule by name: -- FIXME: this will be implemented in #2618 (soon). @@ -943,31 +904,25 @@ mkImport vis nm as imps = -- -- XXX: should probably be unified with `declareName`. -- -bindIdent :: Ident -> CryptolEnv -> (T.Name, CryptolEnv) -bindIdent ident env = (name, env') - where - modEnv = eModuleEnv env - supply = ME.meSupply modEnv +bindIdent :: SharedContext -> Ident -> IO T.Name +bindIdent sc ident = withModEnvSupply sc $ \supply -> + let fixity = Nothing (name, supply') = MN.mkDeclared C.NSValue (C.TopModule interactiveName) MN.UserName ident fixity P.emptyRange supply - modEnv' = modEnv { ME.meSupply = supply' } - env' = env { eModuleEnv = modEnv' } + in (name, supply') -- | Add a new variable as an "extra" declaration. -bindExtraVar :: (Ident, TypedTerm) -> CryptolEnv -> CryptolEnv -bindExtraVar (ident, TypedTerm (TypedTermSchema schema) trm) env = - env' { eExtraNaming = MR.shadowing (MN.singletonNS C.NSValue pname name) - (eExtraNaming env) - , eExtraVars = Map.insert name schema (eExtraVars env) - , eAllTerms = Map.insert name trm (eAllTerms env) - } - where - pname = P.mkUnqual ident - (name, env') = bindIdent ident env +bindExtraVar :: SharedContext -> (Ident, TypedTerm) -> CryptolEnv -> IO CryptolEnv +bindExtraVar sc (ident, TypedTerm (TypedTermSchema schema) trm) env0 = do + name <- bindIdent sc ident + let pname = P.mkUnqual ident + addExtraVars sc (Map.singleton name schema) + addAllTerms sc (Map.singleton name trm) + return $ C.mapNaming (MR.shadowing $ MN.singletonNS C.NSValue pname name) env0 -- Only bind terms that have Cryptol schemas. -- @@ -975,98 +930,48 @@ bindExtraVar (ident, TypedTerm (TypedTermSchema schema) trm) env = -- inappropriate attempts is a policy more appropriate for the -- caller. (Although there are enough callers that this warrants -- some thought before jumping.) -bindExtraVar _ env = env +bindExtraVar _ _ env = pure env -- | Like `bindExtraVar` but temporary within a passed-in operation. -- -- That is, it adds a new variable as an "extra" declaration while -- running the passed in @op@ on the `CryptolEnv`, then drops it --- again, preserving unrelated changes to the `CryptolEnv`. --- --- XXX: This will come unstuck if the wrapped operation touches --- XXX: `eExtraNaming`, `eExtraVars`, or `eAllTerms`. We need a --- XXX: better way to do this; however, there's no way to undo --- XXX: `MR.shadowing` so there aren't many choices. --- --- The right way to do this is probably to extend `CryptolEnv` to --- support scopes, and then to have the caller create a temporary --- scope and use `bindExtraVar`. (Scope support should happen --- anyway. Right now the SAWScript interpreter creates stacks of --- environments to handle scopes, which was an ad hoc solution to an --- immediate need, isn't the right way, and creates its own --- problems.) +-- out of scope, preserving unrelated changes to the `CryptolEnv`. -- + withExtraVar :: + SharedContext -> (Ident, TypedTerm) -> CryptolEnv -> (CryptolEnv -> IO (a, CryptolEnv)) -> IO (a, CryptolEnv) -withExtraVar (ident, TypedTerm (TypedTermSchema schema) trm) env_0 op = do - -- Note: bindIdent only updates the name supply, arguably it is misnamed - let (name, env_1) = bindIdent ident env_0 - - -- Extract the original state - let naming_1 = eExtraNaming env_1 - extravars_1 = eExtraVars env_1 - allterms_1 = eAllTerms env_1 - - -- Generate an updated state and a working environment - let pname = P.mkUnqual ident - naming_2 = MR.shadowing (MN.singletonNS C.NSValue pname name) naming_1 - extravars_2 = Map.insert name schema extravars_1 - allterms_2 = Map.insert name trm allterms_1 - let env_2 = env_1 { - eExtraNaming = naming_2, - eExtraVars = extravars_2, - eAllTerms = allterms_2 - } - - -- Call the op - (ret, env_3) <- op env_2 - - -- Restore the original state - let env_4 = env_3 { - eExtraNaming = naming_1, - eExtraVars = extravars_1, - eAllTerms = allterms_1 - } - - -- done - pure (ret, env_4) - --- Maybe this should panic. The caller presumably meant it to do --- something, so it'd be a mistake if they passed in a binding that --- can't be made visible. -withExtraVar _ env_0 op = - op env_0 +withExtraVar sc b env0 op = withFreshScope env0 $ \env1 -> do + env2 <- bindExtraVar sc b env1 + op env2 -- | Add a new type synonym as an "extra" declaration. -- -- XXX: this should probably fail on inappropriate types; silently -- ignoring them is a policy decision more appropriate for the caller. -- -bindTySyn :: (Ident, T.Schema) -> CryptolEnv -> CryptolEnv -bindTySyn (ident, T.Forall [] [] ty) env = - env' { eExtraNaming = MR.shadowing (MN.singletonNS C.NSType pname name) (eExtraNaming env) - , eExtraTySyns = Map.insert name tysyn (eExtraTySyns env) - } - where - pname = P.mkUnqual ident - (name, env') = bindIdent ident env - tysyn = T.TySyn name [] [] ty Nothing -bindTySyn _ env = env -- only monomorphic types may be bound +bindTySyn :: SharedContext -> (Ident, T.Schema) -> CryptolEnv -> IO CryptolEnv +bindTySyn sc (ident, T.Forall [] [] ty) env = do + name <- bindIdent sc ident + let tysyn = T.TySyn name [] [] ty Nothing + addExtraTySyns sc (Map.singleton name tysyn) + let pname = P.mkUnqual ident + return $ C.mapNaming (MR.shadowing (MN.singletonNS C.NSType pname name)) env + +bindTySyn _ _ env = pure env -- only monomorphic types may be bound -- | Add a new Cryptol integer type as an "extra" declration. -bindIntegerType :: (Ident, Integer) -> CryptolEnv -> CryptolEnv -bindIntegerType (ident, n) env = - env' { eExtraNaming = MR.shadowing (MN.singletonNS C.NSType pname name) (eExtraNaming env) - , eExtraTySyns = Map.insert name tysyn (eExtraTySyns env) - } - where - pname = P.mkUnqual ident - (name, env') = bindIdent ident env - tysyn = T.TySyn name [] [] (T.tNum n) Nothing - +bindIntegerType :: SharedContext -> (Ident, Integer) -> CryptolEnv -> IO CryptolEnv +bindIntegerType sc (ident, n) env = do + name <- bindIdent sc ident + let tysyn = T.TySyn name [] [] (T.tNum n) Nothing + addExtraTySyns sc (Map.singleton name tysyn) + let pname = P.mkUnqual ident + return $ C.mapNaming (MR.shadowing (MN.singletonNS C.NSType pname name)) env -------------------------------------------------------------------------------- @@ -1083,9 +988,9 @@ meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env) -- | Look up an identifier in the Cryptol environment and return its -- full name. resolveIdentifier :: - (HasCallStack, ?fileReader :: FilePath -> IO ByteString) => - CryptolEnv -> Text -> IO (Maybe T.Name) -resolveIdentifier env nm = + (HasCallStack) => + SharedContext -> CryptolEnv -> Text -> IO (Maybe T.Name) +resolveIdentifier sc env nm = do case splitOn (pack "::") nm of [] -> pure Nothing -- FIXME: shouldn't this be error? @@ -1095,38 +1000,21 @@ resolveIdentifier env nm = -- FIXME: Is there no function that parses Text into PName? where - modEnv = eModuleEnv env - nameEnv = getNamingEnv env - - doResolve pnm = - -- Note: this throws away the potentially-updated state returned - -- by MM.runModuleM. However, it should really not have changed - -- anything, and as of this writing does not, so we'll leave it - -- like this. It would be more robust to not throw the state away; - -- maybe at some point in the future it will be less awkward to - -- keep it. - SMT.withSolver (return ()) (meSolverConfig modEnv) $ \solver -> - do let minp = MM.ModuleInput { - MM.minpCallStacks = True, - MM.minpSaveRenamed = False, - MM.minpEvalOpts = pure defaultEvalOpts, - MM.minpByteReader = ?fileReader, - MM.minpModuleEnv = modEnv, - MM.minpTCSolver = solver - } - (res, _ws) <- MM.runModuleM minp $ - MM.interactive (MB.rename interactiveName nameEnv - (MR.resolveNameUse C.NSValue pnm) - ) - case res of - Left _ -> pure Nothing - Right (x,_) -> pure (Just x) + + doResolve pnm = do + nameEnv <- getNamingEnv sc env + (res, _ws) <- liftModuleM' sc $ + MM.interactive (MB.rename interactiveName nameEnv + (MR.resolveNameUse C.NSValue pnm)) + case res of + Left _ -> return Nothing + Right x -> pure (Just x) -- | Read a Cryptol expression from `InputText` and return it as a -- `TypedTerm`. parseTypedTerm :: - (HasCallStack, ?fileReader :: FilePath -> IO ByteString) => - SharedContext -> CryptolEnv -> InputText -> IO (TypedTerm, CryptolEnv) + (HasCallStack) => + SharedContext -> CryptolEnv -> InputText -> IO TypedTerm parseTypedTerm sc env input = do -- Parse: pexpr <- ioParseExpr input @@ -1141,53 +1029,58 @@ parseTypedTerm sc env input = do -- efficient) than printing to text and parsing the text. -- pExprToTypedTerm :: - (?fileReader :: FilePath -> IO ByteString) => - SharedContext -> CryptolEnv -> P.Expr P.PName -> IO (TypedTerm, CryptolEnv) + SharedContext -> CryptolEnv -> P.Expr P.PName -> IO TypedTerm pExprToTypedTerm sc env pexpr = do - let modEnv = eModuleEnv env - - ((expr, schema), modEnv') <- liftModuleM modEnv $ do + nameEnv <- getNamingEnv sc env + (expr, schema) <- inferExpr sc nameEnv pexpr >>= moduleCmdResult + -- Translate + trm <- C.translateExpr sc expr + return (TypedTerm (TypedTermSchema schema) trm) +inferExpr :: + SharedContext -> + MR.NamingEnv -> + P.Expr P.PName -> + IO (Either MM.ModuleError (T.Expr, T.Schema), [MM.ModuleWarning]) +inferExpr sc nameEnv pexpr = do + extraVars <- eExtraVars sc + extraTySyns <- eExtraTySyns sc + liftModuleM' sc $ do -- Eliminate patterns: npe <- MM.interactive (MB.noPat pexpr) - - let nameEnv = getNamingEnv env + let npe' = MR.rename npe re <- MM.interactive (MB.rename interactiveName nameEnv npe') -- NOTE: if a name is not in scope, it is reported here. -- Infer types - let ifDecls = C.getAllIfaceDecls modEnv + ifDecls <- C.getAllIfaceDecls <$> MM.getModuleEnv let range = fromMaybe P.emptyRange (P.getLoc re) prims <- MB.getPrimMap -- noIfaceParams because we don't support functors yet tcEnv <- MB.genInferInput range prims NoParams ifDecls - let tcEnv' = tcEnv { TM.inpVars = Map.union (eExtraVars env) (TM.inpVars tcEnv) - , TM.inpTSyns = Map.union (eExtraTySyns env) (TM.inpTSyns tcEnv) + let tcEnv' = tcEnv { TM.inpVars = Map.union extraVars (TM.inpVars tcEnv) + , TM.inpTSyns = Map.union extraTySyns (TM.inpTSyns tcEnv) } out <- MM.io (T.tcExpr re tcEnv') MM.interactive (runInferOutput out) - let env' = env { eModuleEnv = modEnv' } - - -- Translate - trm <- C.translateExpr sc env' expr - return (TypedTerm (TypedTermSchema schema) trm, env') -- | Read Cryptol declarations from `InputText` and ingest them into -- the `CryptolEnv`. parseDecls :: - (?fileReader :: FilePath -> IO ByteString) => SharedContext -> CryptolEnv -> InputText -> IO CryptolEnv parseDecls sc env input = do - let modEnv = eModuleEnv env - let ifaceDecls = C.getAllIfaceDecls modEnv + ifaceDecls <- C.getAllIfaceDecls <$> eModuleEnv sc + namingEnv <- getNamingEnv sc env + extraVars <- eExtraVars sc + extraTySyns <- eExtraTySyns sc -- Parse (decls :: [P.Decl P.PName]) <- ioParseDecls input - (tmodule, modEnv') <- liftModuleM modEnv $ do + tmodule <- liftModuleM sc $ do -- Eliminate patterns (npdecls :: [P.Decl P.PName]) <- MM.interactive (MB.noPat decls) @@ -1203,7 +1096,7 @@ parseDecls sc env input = do -- Resolve names (_nenv, rdecls) <- MM.interactive (MB.rename interactiveName - (getNamingEnv env) + namingEnv (MR.renameTopDecls topdecls) ) @@ -1219,8 +1112,8 @@ parseDecls sc env input = do prims <- MB.getPrimMap -- noIfaceParams because we don't support functors yet tcEnv <- MB.genInferInput range prims NoParams ifaceDecls - let tcEnv' = tcEnv { TM.inpVars = Map.union (eExtraVars env) (TM.inpVars tcEnv) - , TM.inpTSyns = Map.union (eExtraTySyns env) (TM.inpTSyns tcEnv) + let tcEnv' = tcEnv { TM.inpVars = Map.union extraVars (TM.inpVars tcEnv) + , TM.inpTSyns = Map.union extraTySyns (TM.inpTSyns tcEnv) } out <- MM.io (TM.runInferM tcEnv' (TI.inferTopModule rmodule)) @@ -1232,10 +1125,9 @@ parseDecls sc env input = do return m -- Add new type synonyms and their name bindings to the environment - let syns' = Map.union (eExtraTySyns env) (T.mTySyns tmodule) let addName name = MR.shadowing (MN.singletonNS C.NSType (P.mkUnqual (MN.nameIdent name)) name) - let naming' = foldr addName (eExtraNaming env) (Map.keys (T.mTySyns tmodule)) - let env' = env { eModuleEnv = modEnv', eExtraNaming = naming', eExtraTySyns = syns' } + addExtraTySyns sc (T.mTySyns tmodule) + let env' = C.mapNaming (\ne -> foldr addName ne (Map.keys (T.mTySyns tmodule))) env -- Translate let dgs = T.mDecls tmodule @@ -1243,28 +1135,27 @@ parseDecls sc env input = do -- | Read a Cryptol type scheme from `InputText`. parseSchema :: - (?fileReader :: FilePath -> IO ByteString) => - CryptolEnv -> InputText -> IO (T.Schema, CryptolEnv) -parseSchema env input = do - let modEnv = eModuleEnv env + SharedContext -> CryptolEnv -> InputText -> IO T.Schema +parseSchema sc env input = do + nameEnv <- getNamingEnv sc env + extraTySyns <- eExtraTySyns sc -- Parse pschema <- ioParseSchema input - (schema, modEnv') <- liftModuleM modEnv $ do + schema <- liftModuleM sc $ do -- Resolve names - let nameEnv = getNamingEnv env rschema <- MM.interactive $ MB.rename interactiveName nameEnv (MR.renameSchema pschema pure) - let ifDecls = C.getAllIfaceDecls modEnv + ifDecls <- C.getAllIfaceDecls <$> MM.getModuleEnv let range = fromMaybe P.emptyRange (P.getLoc rschema) prims <- MB.getPrimMap -- noIfaceParams because we don't support functors yet tcEnv <- MB.genInferInput range prims NoParams ifDecls - let tcEnv' = tcEnv { TM.inpTSyns = Map.union (eExtraTySyns env) (TM.inpTSyns tcEnv) } + let tcEnv' = tcEnv { TM.inpTSyns = Map.union extraTySyns (TM.inpTSyns tcEnv) } let infer = case rschema of P.Forall [] [] t _ -> do @@ -1276,9 +1167,7 @@ parseSchema env input = do (schema, _goals) <- MM.interactive (runInferOutput out) --mapM_ (MM.io . print . TP.ppWithNames TP.emptyNameMap) goals return (schemaNoUser schema) - - let env' = env { eModuleEnv = modEnv' } - return (schema, env') + return schema -- | Prepare an identifier for adding to the Cryptol environment. -- May update the name supply. @@ -1286,16 +1175,11 @@ parseSchema env input = do -- XXX: much the same as, and should probably be unified with, `bindIdent`. -- declareName :: - (?fileReader :: FilePath -> IO ByteString) => - CryptolEnv -> P.ModName -> Text -> IO (T.Name, CryptolEnv) -declareName env mname input = do + SharedContext -> P.ModName -> Text -> IO T.Name +declareName sc mname input = do let pname = P.mkUnqual (mkIdent input) - let modEnv = eModuleEnv env - (cname, modEnv') <- - liftModuleM modEnv $ MM.interactive $ + liftModuleM sc $ MM.interactive $ MN.liftSupply (MN.mkDeclared C.NSValue (C.TopModule mname) MN.UserName (P.getIdent pname) Nothing P.emptyRange) - let env' = env { eModuleEnv = modEnv' } - return (cname, env') -- | Remove type synonym annotations from a Cryptol type. -- @@ -1336,41 +1220,51 @@ noLoc x = InputText locatedUnknown :: a -> P.Located a locatedUnknown x = P.Located P.emptyRange x +liftModuleM' :: + SharedContext -> MM.ModuleM a -> IO (Either MM.ModuleError a, [MM.ModuleWarning]) +liftModuleM' sc m = do + FileReader fileReader <- scGetData sc + env <- eModuleEnv sc + let minp solver = MM.ModuleInput { + MM.minpCallStacks = True, + MM.minpSaveRenamed = False, + MM.minpEvalOpts = pure defaultEvalOpts, + MM.minpByteReader = fileReader, + MM.minpModuleEnv = env, + MM.minpTCSolver = solver + } + (res, ws) <- SMT.withSolver (return ()) (meSolverConfig env) $ \solver -> + MM.runModuleM (minp solver) m + case res of + Right (a, env') -> do + setModuleEnv sc env' + return (Right a, ws) + Left err -> return (Left err, ws) + -- | Run a `MM.ModuleM` (Cryptol module environment monad) -- computation. -- -- XXX: misnamed, it's not a lift, it's a run. -liftModuleM :: - (?fileReader :: FilePath -> IO ByteString) => - ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv) -liftModuleM env m = - do let minp solver = MM.ModuleInput { - MM.minpCallStacks = True, - MM.minpSaveRenamed = False, - MM.minpEvalOpts = pure defaultEvalOpts, - MM.minpByteReader = ?fileReader, - MM.minpModuleEnv = env, - MM.minpTCSolver = solver - } - SMT.withSolver (return ()) (meSolverConfig env) $ \solver -> - MM.runModuleM (minp solver) m >>= moduleCmdResult - +liftModuleM :: SharedContext -> MM.ModuleM a -> IO a +liftModuleM sc m = liftModuleM' sc m >>= moduleCmdResult -- | Default `E.EvalOpts` for evaluating Cryptol. defaultEvalOpts :: E.EvalOpts defaultEvalOpts = E.EvalOpts quietLogger E.defaultPPOpts --- | Process an `M.ModuleRes` (result of a `MM.ModuleM` computation) --- Print errors and warnings. +moduleCmdResult :: (Either MM.ModuleError a, [MM.ModuleWarning]) -> IO a +moduleCmdResult (res, ws) = do + moduleWarns ws + case res of + Left err -> errX' $ "Cryptol:" <+> CryPP.pretty err + Right a -> return a + +-- | Print warnings. -- -- Suppress warnings about defaulting types. -- -moduleCmdResult :: M.ModuleRes a -> IO (a, ME.ModuleEnv) -moduleCmdResult (res, ws) = do - mapM_ (warnN' . CryPP.pretty) (concatMap suppressDefaulting ws) - case res of - Right (a, me) -> return (a, me) - Left err -> errX' $ "Cryptol:" <+> CryPP.pretty err +moduleWarns :: [MM.ModuleWarning] -> IO () +moduleWarns ws = mapM_ (warnN' . CryPP.pretty) (concatMap suppressDefaulting ws) where -- If all warnings are about type defaults, pretend there are no warnings at -- all to avoid displaying an empty warning container. diff --git a/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs new file mode 100644 index 0000000000..a9cc8807f8 --- /dev/null +++ b/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs @@ -0,0 +1,593 @@ +{- | +Module : CryptolSAWCore.GlobalCryptolEnv +Description : Cryptol to SAWCore import logic +Copyright : Galois, Inc. 2012-2026 +License : BSD3 +Maintainer : saw@galois.com +Stability : experimental +Portability : non-portable (language extensions) + +-} + +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ViewPatterns #-} + +module CryptolSAWCore.GlobalCryptolEnv + ( ImportVisibility(..) + , isToplevel + , sameHeight + , pushScope + , popScope + , initEnv + , CryptolEnv + , withModEnvSupply + , mapNaming + , mapImports + , setModuleEnv + , eExtraNaming + , eImports + , eModuleEnv + , eExtraVars + , addExtraVars + , eExtraTySyns + , addExtraTySyns + , eAllVars + , addAllVars + , eTyVars + , addTyVars + , eTyProps + , addTyProps + , eAllTerms + , addAllTerms + , eRefPrims + , addRefPrims + , ePrims + , addPrims + , ePrimTypes + , addPrimTypes + , eFFITypes + , addFFITypes + , withFreshScope + , getAllIfaceDecls + ) where + +import Data.List.NonEmpty (NonEmpty(..), (<|)) +import qualified Data.List.NonEmpty as NE +import Data.Map (Map) +import qualified Data.Map as Map + + +import qualified Cryptol.ModuleSystem.Env as ME +import qualified Cryptol.ModuleSystem.Name as C +import qualified Cryptol.ModuleSystem.Renamer as MR + +import qualified Cryptol.TypeCheck.AST as C +import qualified Cryptol.Utils.Ident as C + +import SAWCore.SharedTerm +import SAWCore.Term.Functor (FieldName) + +import CryptolSAWCore.Panic +import qualified Cryptol.ModuleSystem as MI +import Control.Monad (unless) + +-------------------------------------------------------------------------------- + +-- | ImportVisibility is an enumeration that indicates how we handle +-- the visibility of the symbols in an imported module. +-- +-- `OnlyPublic` makes only the public/exported symbols of a module +-- visible from SAW. `PublicAndPrivate` instead makes all symbols +-- visible, as if one is working inside it. The latter is often useful +-- (or necessary) for verification and code generation. +-- +-- `PublicAndPrivate` is akin to setting the module focus in the +-- Cryptol REPL; however, it uses a simpler internal mechanism and is +-- only settable at import time. +-- +-- (See 'CryptolEnv.importCryptolModule'.) +-- +-- NOTE: this notion of public vs. private symbols is specific to +-- SAWScript and distinct from Cryptol's notion of private +-- definitions. +-- +-- FUTURE: this should probably be replaced with a way to manipulate +-- the module focus like the Cryptol REPL uses. What you really want +-- is not to expose module innards that weren't meant to be exposed, +-- but to go inside to prove things in the module's internal context. +-- +data ImportVisibility + = OnlyPublic -- ^ behaves like a normal Cryptol @import@ + | PublicAndPrivate -- ^ allows viewing of both @private@ sections + -- and (arbitrarily nested) submodules. + deriving (Eq, Show) + + +-- | The global environment for capturing the Cryptol state, both +-- Cryptol's own state and the state associated with +-- importing/translating into SAWCore. +-- This is intended to be a write-once record of any work done +-- during translation, analagous to the 'SharedContext' from +--- SAWCore. Rather than directly accessing this environment, +-- operations take/return a 'CryptolEnv', which additionally +-- includes a scoped naming environment via 'CryptolScope'. + + +-- +-- Note that prior to 202603 there were two environment types, +-- `CryptolEnv` carrying around the persistent bits and generally +-- being (in most places) the external interface; and another type +-- called (far too generically) @Env@ used by the import logic in this +-- file. There was a bunch of code for copying bits from `CryptolEnv` +-- into an empty @Env@ on the fly, calling into here, then pouring the +-- results back. This code was arbitrary and in some cases possibly +-- wrong. Furthermore, having the import code tied to an incompatible +-- type made a bunch of external code calling directly into it pass an +-- empty environment instead, which caused further problems. +-- +-- While this was being fixed the prior @Env@ type got renamed to +-- @ImportEnv@. There should be no references to it or its field names +-- (@imp*@ rather than @env*@) left, but in case some are hiding in +-- comments the transitional field names are also documented below. +-- +-- There is now one environment type. The history above remains +-- relevant until all the leftover warts and weaknesses arising from +-- the old structure get cleaned out, which may take a while. +-- +-- (FUTURE: once that's done, remove the historical notes; they are +-- only of value while they remain relevant to the current code.) +data GlobalCryptolEnv = GlobalCryptolEnv + { geModuleEnv :: ME.ModuleEnv + -- | Invariant: This is a subset of 'geAllVars', which is + -- enforced by 'addExtraVars' + , geExtraVars :: Map C.Name C.Schema + , geExtraTySyns :: Map C.Name C.TySyn + , geAllVars :: Map C.Name C.Schema + , geTyVars :: Map Int Term + , geTyProps :: Map C.Prop (Term, [FieldName]) + , geAllTerms :: Map C.Name Term + , geRefPrims :: Map C.PrimIdent C.Expr + , gePrims :: Map C.PrimIdent Term + , gePrimTypes :: Map C.PrimIdent Term + , geFFITypes :: Map NameInfo C.FFI + } + +-- | Initialize the global environment with the given 'ME.ModuleEnv', +-- and populate the 'geAllVars' accordingly. +initGlobalEnv :: ME.ModuleEnv -> GlobalCryptolEnv +initGlobalEnv modEnv = refreshCryptolEnv $ + GlobalCryptolEnv modEnv + mempty mempty mempty mempty mempty mempty mempty mempty mempty + mempty + +instance IsMetadata GlobalCryptolEnv where + initMetadata = initGlobalEnv <$> ME.initialModuleEnv + +-- | Restore a `GlobalCryptolEnv` from a checkpoint. The first argument +-- @chkEnv@ is the `GlobalCryptolEnv` saved by / copied into the +-- checkpoint; the second argument @newEnv@ is the current one +-- we wish to overwrite by rolling back to the checkpoint. +-- The 'ME.meNameSeeds' and 'ME.meSupply' from the +-- module environment are not rolled back, to avoid re-using old +-- names. +-- NOTE: This effectively +-- invalidates any translated 'Term's or Cryptol expressions created +-- after the checkpoint. Attempting to use them in the restored +-- environment will have unpredictable results, and likely will +-- result in a panic. Similarly, 'CryptolEnv's captured after the +-- checkpoint are no longer safe to use in the resulting environment. + +-- We also ought to invalidate terms constructed since the checkpoint +-- was taken, like SAWCore does. See #2859. + +-- We could, for example, have 'CryptolScope' track which +-- identifiers it references, and check that they are in a valid +-- range with respect to the corresponding global environment +-- before combining them into a 'CryptolEnv'. + restoreMetadata chk now = return $ + let newMEnv = geModuleEnv chk + chkMEnv = geModuleEnv now + in chk { geModuleEnv = chkMEnv + { ME.meNameSeeds = ME.meNameSeeds newMEnv + , ME.meSupply = ME.meSupply newMEnv + } + } + +-- | A scope frame that captures which Cryptol names are accessible. +-- `fNamingEnv` is the local naming environment, which can be extended +-- ad-hoc with additional declarations. `fImports` is a list of all +-- the modules that have been imported, and a visibility setting for +-- each. This does not include, for example, builtin modules that +-- exist but that have not been imported. + +data CryptolFrame = + CryptolFrame { fNamingEnv :: MR.NamingEnv + , fImports :: [(ImportVisibility, C.Import)] + } + +initFrame :: CryptolFrame +initFrame = CryptolFrame mempty mempty + +-- | A nonempty list of 'CryptolFrame's, where the first element is the +-- "bottom" frame that takes highest precedence when looking up +-- names. Each individual frame only contains values declared at +-- exactly that level. The full scope is computed by collecting +-- everything in this stack, via 'eExtraNaming' and 'eImports'. +newtype CryptolEnv = CryptolEnv (NonEmpty CryptolFrame) + +initEnv :: CryptolEnv +initEnv = CryptolEnv (initFrame :| []) + +isToplevel :: CryptolEnv -> Bool +isToplevel (CryptolEnv (_ :| frames)) = null frames + +-- | Test if the scopes have the same number of frames pushed. +sameHeight :: CryptolEnv -> CryptolEnv -> Bool +sameHeight (CryptolEnv scope1) (CryptolEnv scope2) = + NE.length scope1 == NE.length scope2 + +mapCurFrame :: + (CryptolFrame -> CryptolFrame) -> + CryptolEnv -> + CryptolEnv +mapCurFrame f (CryptolEnv (frame :| frames)) = + CryptolEnv (f frame :| frames) + +-- | Push a fresh frame onto the stack. +pushScope :: CryptolEnv -> CryptolEnv +pushScope (CryptolEnv frames) = CryptolEnv (initFrame <| frames) + +-- | Pop the current frame from the stack, discarding its +-- contents. Panics if this is the only frame. +popScope :: CryptolEnv -> CryptolEnv +popScope (CryptolEnv frames) = case snd (NE.uncons frames) of + Nothing -> panic "popScope" [ "Popping topmost scope"] + Just frames' -> CryptolEnv frames' + +-- | Map the naming environment of the frame currently in scope. +mapNaming :: + (MR.NamingEnv -> MR.NamingEnv) -> + CryptolEnv -> + CryptolEnv +mapNaming f = mapCurFrame $ + \fr -> fr {fNamingEnv = f (fNamingEnv fr) } + +-- | Map the module imports of the frame currently in scope. +mapImports :: + ([(ImportVisibility, C.Import)] -> [(ImportVisibility, C.Import)] ) -> + CryptolEnv -> + CryptolEnv +mapImports f = mapCurFrame $ + \fr -> fr {fImports = f (fImports fr) } + +-- | Run the inner action bracketed new frame pushed/popped on +-- the 'CryptolScope' stack. +-- Fails if the inner action changes the scope height +-- (i.e. it does not properly bracket its pushes and pops). +withFreshScope :: + MonadFail m => + CryptolEnv -> + (CryptolEnv -> + m (a, CryptolEnv)) -> + m (a, CryptolEnv) +withFreshScope env0 f = do + let env1 = pushScope env0 + (a, env2) <- f env1 + unless (sameHeight env1 env2) $ + fail "withFreshScope: mismatched push/pops" + let env3 = popScope env2 + return (a, env3) + +-- | Access the 'C.Supply' in the global 'ME.ModuleEnv' for generating +-- fresh names. More efficient than directly modifying the +-- environment and using 'setModuleEnv', as it avoids any other +-- bookkeeping. +withModEnvSupply :: SharedContext -> (C.Supply -> (a, C.Supply)) -> IO a +withModEnvSupply sc f = do + modEnv <- eModuleEnv sc + let (a, supply) = f $ ME.meSupply modEnv + mapModEnv sc (\modEnv_ -> modEnv_ { ME.meSupply = supply } ) + return a + +------------------------------------- +-- Environment Access -- + +getGlobal :: (GlobalCryptolEnv -> a) -> SharedContext -> IO a +getGlobal f sc = f <$> scGetData sc + +mapGlobal :: SharedContext -> (GlobalCryptolEnv -> GlobalCryptolEnv) -> IO () +mapGlobal = scUpdateData + +mapModEnv :: SharedContext -> (ME.ModuleEnv -> ME.ModuleEnv) -> IO () +mapModEnv sc f = mapGlobal sc (\genv -> genv { geModuleEnv = f (geModuleEnv genv) }) + +-- The "getters" below were historically fields in 'CryptolEnv', which +-- are now defined functions that access either the 'GlobalCryptolEnv' +-- or the 'CryptolScope' as appropriate. In contrast, updates were +-- historically made by directly accessing 'CryptolEnv' fields, and are +-- now restricted to only adding new entries to the maps in +-- 'GlobalCryptolEnv' (e.g. 'addExtraVars'). This enforces the policy +-- that the global environment is intended to be a complete record of +-- all work done during translation/import, regardless of scope. Since +-- the maps in the global environment are all keyed on globally-unique +-- values, these operations are expected to only add entries and never +-- overwrite existing ones. +-- +-- NOTE: We could enforce a write-once policy here, but it's +-- not immediately obvious if we need to support key clashes +-- for equal entries (not possible for +-- some times like 'C.Expr'), or if it is even useful to do so. + +-- == Maps from 'GlobalCryptolEnv': + +-- == Pieces relating to Cryptol primitives: + +-- | Maps Cryptol primitives to their reference +-- implementations that Cryptol keeps around. Currently this field is +-- only populated during initialization; it isn't clear if that's a +-- bug. (If there are really no further uses after initialization, +-- regardless of what the user does, dropping the contents allows the +-- memory to be reclaimed. But if it's possible to construct such +-- uses, they're likely to panic.) +-- +-- Before the environment types were merged, this field was found only +-- in @Env@ and called @envRefPrims@ (transitionally @impRefPrims@). +eRefPrims :: SharedContext -> IO (Map C.PrimIdent C.Expr) +eRefPrims = getGlobal geRefPrims + +-- | Add entries to 'eRefPrims' +addRefPrims :: SharedContext -> Map C.PrimIdent C.Expr -> IO () +addRefPrims sc m = mapGlobal sc $ \genv -> + genv { geRefPrims = Map.union m (geRefPrims genv) } + +-- | Maps names of Cryptol primitives to their implementations +-- as SAWCore terms. Before the environment types were merged, it was +-- also present in @Env@ under the name @envPrims@ (transitionally +-- @impPrims@). +ePrims :: SharedContext -> IO (Map C.PrimIdent Term) +ePrims = getGlobal gePrims + +-- | Add entries to 'ePrims' +addPrims :: SharedContext -> Map C.PrimIdent Term -> IO () +addPrims sc m = mapGlobal sc $ \genv -> + genv { gePrims = Map.union m (gePrims genv) } + +-- | Maps names of Cryptol primitive types to their +-- implementations as SAWCore terms (that are types). Before the +-- environment types were merged, it was also present in @Env@ under +-- the name @envPrimTypes@ (transitionally @impPrimTypes@). +ePrimTypes :: SharedContext -> IO (Map C.PrimIdent Term) +ePrimTypes = getGlobal gePrimTypes + +-- | Add entries to 'ePrimTypes' +addPrimTypes :: SharedContext -> Map C.PrimIdent Term -> IO () +addPrimTypes sc m = mapGlobal sc $ \genv -> + genv { gePrimTypes = Map.union m (gePrimTypes genv) } + +-- == Second, the pieces that track Cryptol-level objects and types: + +-- | The Cryptol-level module environment; it holds all +-- the modules that have been loaded. Its type is also the state for +-- Cryptol's `ME.ModuleM` monad. +eModuleEnv :: SharedContext -> IO ME.ModuleEnv +eModuleEnv = getGlobal geModuleEnv + +-- | Update 'eModuleEnv', adding new entries to 'eAllVars' as needed. + +-- TODO: sanity checks? This only makes sense if set of loaded modules +-- in the given environment is a superset of those in the current +-- environment. Additionally, the supply and seeds should necessarily +-- be more recent. Finally, the environment refresh is only necessary +-- if more modules were actually added (and technically only required +-- for the new modules). +setModuleEnv :: SharedContext -> ME.ModuleEnv -> IO () +setModuleEnv sc modEnv = mapGlobal sc $ \genv -> + refreshCryptolEnv $ genv { geModuleEnv = modEnv } + + +-- | Formerly @eExtraTSyns@, holds the expansions for +-- the "extra names" that are type aliases (synonyms). Maps names to +-- `T.TySyn`, which wraps Cryptol types and among other things allows +-- synonyms to take parameters. +eExtraTySyns :: SharedContext -> IO (Map C.Name C.TySyn) +eExtraTySyns = getGlobal geExtraTySyns + +-- | Add entries to 'eExtraTySyns' +addExtraTySyns :: SharedContext -> Map C.Name C.TySyn -> IO () +addExtraTySyns sc m = mapGlobal sc $ \genv -> + genv { geExtraTySyns = Map.union m (geExtraTySyns genv) } + +-- | Formerly @eExtraTypes@, holds the Cryptol-level +-- types for "extra names" that are value/term variables. Maps names +-- to type schemes. +eExtraVars :: SharedContext -> IO (Map C.Name C.Schema) +eExtraVars = getGlobal geExtraVars + +-- | Add entries to both 'eExtraVars' and 'eAllVars' +addExtraVars :: SharedContext -> Map C.Name C.Schema -> IO () +addExtraVars sc m = mapGlobal sc $ \genv -> + genv { geExtraVars = Map.union m (geExtraVars genv) + , geAllVars = Map.union m (geAllVars genv) + } + +-- Before the environment types were merged, the above five fields +-- were not accessible via @Env@, which turned out to cause +-- complications. + +-- | Map from Cryptol names to Cryptol types. This is +-- used to call `fastTypeOf` and `fastSchemaOf` on Cryptol expressions +-- to fetch their types. This table is derived from information +-- properly kept elsewhere and is a headache to have. +-- +-- Before the environment types were merged, this was found only in +-- @Env@ under the name @envC@. It was built on the fly when calling +-- into the import code using @Env@ and thrown away afterwards. +-- Now it is updated every time the module environment is modified +-- via 'setModuleEnv'. +-- (Transitionally it was called @impCry@ and then @impAllVars@.) + +-- FUTURE: in principle we should be able to use the SAWCore types of +-- the SAWCore terms after importing them, instead of `fastTypeOf` and +-- `fastSchemaOf`, and drop the `eAllVars` table. In practice, doing +-- that relies (in some cases) on being able to call `scCryptolType` +-- to reconstruct the Cryptol-level type; that in turn requires, when +-- inside a forall-binding, logic to intercept and lift SAWCore type +-- variables back to their Cryptol parents. That requires a table we +-- don't currently have, as well as additional lookup logic that +-- doesn't currently exist. Furthermore, while we've fixed many of the +-- ways the Cryptol -> SAWCore type mapping is noninjective, it still +-- won't work for enumerations. And beyond that, when handling +-- polymorphic type schemes we erase certain typeclasses in the +-- translation, and that loses info, so we might need to translate +-- those classes to placeholders instead of erasing them. It may then +-- also be that the one use of `fastSchemaOf` can't actually be +-- avoided; that isn't super clear. +eAllVars :: SharedContext -> IO (Map C.Name C.Schema) +eAllVars = getGlobal geAllVars + +-- | Add entries to 'eAllVars' +addAllVars :: SharedContext -> Map C.Name C.Schema -> IO () +addAllVars sc m = mapGlobal sc $ \genv -> + genv { geAllVars = Map.union m (geAllVars genv) } + +-- == Third, the pieces that track imported SAWCore bits: + +-- | Maps Cryptol type variable IDs to SAWCore types. This is +-- only nonempty during import, when working inside a forall-binding. +-- Before the environment types were merged, this was only needed in +-- (and only found in) @Env@ as @envT@. Transitionally, it was called +-- @impTy@ and then @impTyVars@. +eTyVars :: SharedContext -> IO (Map Int Term) +eTyVars = getGlobal geTyVars + +-- | Add entries to 'eTyVars' +addTyVars :: SharedContext -> Map Int Term -> IO () +addTyVars sc m = mapGlobal sc $ \genv -> + genv { geTyVars = Map.union m (geTyVars genv) } + +-- | Maps Cryptol `C.Prop`, which are type constraints, to +-- corresponding SAWCore information. There is both a term and a list +-- of `FieldName`. The actual class dictionary we need is obtained by +-- applying the given field selectors (in reverse order!) to the term. +-- (This arises when a dictionary comes from a superclass; the field +-- projections traverse the subclass dictionaries.) +-- The constraints are referenced implicitly by their types. +-- +-- Like `eTyVars`, this table is only nonempty during import, when +-- working inside a forall-binding, and carries the info from that +-- binding. +-- +-- Before the environment types were merged, this was only needed in +-- (and only found in) @Env@ as @envP@. Transitionally, it was called +-- @impProp@ and then @envTyProps@. +eTyProps :: SharedContext -> IO (Map C.Prop (Term, [FieldName])) +eTyProps = getGlobal geTyProps + +-- | Add entries to 'eTyProps'. + +-- The one current use of this function in 'CryptolSAWCore.Cryptol' +-- collects all of the superclasses of the given 'C.Prop' as well. +-- It may make sense to move that logic here, as the current +-- approach involves redundantly re-computing the entries for +-- all superclasses for each individual entry. +-- This is not expensive, but would become problematic +-- if we wanted to enforce a write-once policy. +addTyProps :: SharedContext -> Map C.Prop (Term, [FieldName]) -> IO () +addTyProps sc m = mapGlobal sc $ \genv -> + genv { geTyProps = Map.union m (geTyProps genv) } + +-- | Formerly @eTermEnv@, holds the translations for all +-- Cryptol names in scope. It maps names to SAWCore terms. Apparently +-- it includes types as well as values. Does not include the contents +-- of `ePrims` or `ePrimTypes` (which are not identified with a +-- 'C.Name'). +-- Note that the keys in this map are not necessarily a superset of +-- those in 'eAllVars', which may contain variables that have not been +-- translated into SAWCore yet. For entries with matching keys, the +-- 'Term' in 'eAllTerms' should be a 'Variable' with a type that is the +-- imported 'C.Schema' from 'eAllVars'. +-- +-- Before the environment types were merged, it was also found in @Env@ +-- under the name @envE@. +eAllTerms :: SharedContext -> IO (Map C.Name Term) +eAllTerms = getGlobal geAllTerms + +-- | Add entries to 'eAllTerms' +addAllTerms :: SharedContext -> Map C.Name Term -> IO () +addAllTerms sc m = mapGlobal sc $ \genv -> + genv { geAllTerms = Map.union m (geAllTerms genv) } + +-- | Maps SAWCore names to Cryptol FFI info where relevant. +-- Before the environment types were merged, this was unavailable in +-- @Env@. +eFFITypes :: SharedContext -> IO (Map NameInfo C.FFI) +eFFITypes = getGlobal geFFITypes + +-- | Add entries to 'eFFITypes' +addFFITypes :: SharedContext -> Map NameInfo C.FFI -> IO () +addFFITypes sc m = mapGlobal sc $ \genv -> + genv { geFFITypes = Map.union m (geFFITypes genv) } + +-- == Scoped entries from 'CryptolEnv': + +-- | The "extra" naming environment that captures Cryptol names +-- which don't correspond to any imported module. Generally these +-- result from names created in SAW which have been reflected into +-- the Cryptol environment. +-- This is scoped content, where the accessible names are expected +-- to be managed by SAW and correspond to the same SAW values that +-- are in scope. + +-- FUTURE: Cryptol has its own functionality for additional bindings +-- (it uses it for things created from the Cryptol REPL) and we ought +-- to be able to use it instead of bolting on our own additional layer +-- of material. Doing so would avoid various inconsistencies and +-- irregularities that can creep in when we reimplement Cryptol name +-- resolution. +eExtraNaming :: CryptolEnv -> MR.NamingEnv +eExtraNaming (CryptolEnv (frame :| frames)) = + foldr (\fr ne -> ne `MR.shadowing` (fNamingEnv fr)) (fNamingEnv frame) frames + +-- | The list of Cryptol modules which have been brought into the +-- current scope. This essentially acts as a filter on the full set +-- of loaded modules in the global module environment ('eModuleEnv'), +-- where the contents of the selected modules are brought into scope +-- according to the associated 'ImportVisibility'. The modules here +-- should only correspond to modules that are present in the module +-- environment *and* have been translated into SAWCore. +eImports :: CryptolEnv -> [(ImportVisibility, C.Import)] +eImports (CryptolEnv frames) = + concat $ map fImports $ NE.toList frames + + +-- | Refresh 'geAllVars' after updating the module environment. +-- Previously (before 'GlobalCryptolEnv'), this would overwrite the +-- 'eAllVars' field. Now this will add new vars (i.e. from +-- newly-added modules) but keep existing ones, as the +-- 'GlobalCryptolEnv' should never drop entries. If the module +-- environment has been managed properly, we expect any clashing keys +-- to have equal elements, but this is not checked/enforced. Not +-- exported. +refreshCryptolEnv :: GlobalCryptolEnv -> GlobalCryptolEnv +refreshCryptolEnv genv = + let modEnv = geModuleEnv genv + ifaceDecls = getAllIfaceDecls modEnv + newtypeCons = Map.fromList + [ con + | nt <- Map.elems (MI.ifNominalTypes ifaceDecls) + , con <- C.nominalTypeConTypes nt + ] + vars = Map.map MI.ifDeclSig $ MI.ifDecls ifaceDecls + -- note that we don't need to re-add geExtraVars, because + -- it is already included in the existing geAllVars + allvars = newtypeCons `Map.union` vars + allvars' = Map.union allvars (geAllVars genv) + in genv { geAllVars = allvars' } + +---- Misc Exports -------------------------------------------------------------- + +getAllIfaceDecls :: ME.ModuleEnv -> MI.IfaceDecls +getAllIfaceDecls me = + mconcat + (map (MI.ifDefines . ME.lmInterface) + (ME.getLoadedModules (ME.meLoadedModules me))) \ No newline at end of file diff --git a/cryptol-saw-core/src/CryptolSAWCore/SAWCoreCryptol.hs b/cryptol-saw-core/src/CryptolSAWCore/SAWCoreCryptol.hs new file mode 100644 index 0000000000..33ab789224 --- /dev/null +++ b/cryptol-saw-core/src/CryptolSAWCore/SAWCoreCryptol.hs @@ -0,0 +1,1120 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE GeneralisedNewtypeDeriving #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} +{- +Provides a (very) partial mapping from SAWCore terms back to Cryptol expressions. +-} + +module CryptolSAWCore.SAWCoreCryptol + ( termToSchemaExpr + , propToSchemaExpr + , prettyTTError + , termToPExpr + ) where + +import Control.Applicative +import Control.Exception (try, IOException) +import Control.Monad +import Control.Monad.Except + ( MonadError, throwError, catchError, ExceptT, runExceptT + , handleError) +import Control.Monad.Reader +import Control.Monad.Writer + +import Data.IntMap (IntMap) +import qualified Data.IntMap as IntMap +import Data.IORef +import qualified Data.List.NonEmpty as NE +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Maybe (mapMaybe,catMaybes, isJust) +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Text (Text) +import qualified Data.Text as Text + +import qualified Cryptol.Parser.AST as P +import qualified Cryptol.Parser.Position as P +import qualified Cryptol.ModuleSystem.Name as C +import qualified Cryptol.ModuleSystem.Names as C +import qualified Cryptol.ModuleSystem.NamingEnv as C +import qualified Cryptol.Parser.Position as Pos +import qualified Cryptol.Utils.Ident as C +import qualified Cryptol.TypeCheck.AST as C +import qualified Cryptol.Utils.RecordMap as C + +import qualified SAWCore.Name as SAW +import SAWCore.Recognizer +import SAWCore.SharedTerm +import SAWCore.Term.Functor +import qualified SAWCore.Term.Pretty as SAW + +import qualified SAWSupport.Pretty as PPS + +import qualified CryptolSAWCore.CryptolEnv as CrySAW +import qualified CryptolSAWCore.Cryptol as CrySAW +import CryptolSAWCore.GlobalCryptolEnv (CryptolEnv) + +import qualified Prettyprinter as PP +import Cryptol.TypeCheck.PP (pp, pretty) + + +import Cryptol.ModuleSystem.Env (lookupModule, lmInterface) +import Cryptol.ModuleSystem.Interface (ifacePrimMap) + + + + +revMap :: (Ord k, Ord u) => (v -> Maybe u) -> Map k v -> Map u k +revMap f m = Map.fromList $ mapMaybe (\(k,v) -> (,k) <$> (f v)) (Map.toList m) + +extraPrims :: C.PrimMap -> [(SAW.Ident, C.Name)] +extraPrims pm = map go + [ -- types from Prelude.sawcore + ("Prelude.Integer", "Integer") + , ("Prelude.Bool", "Bit") + -- types from Cryptol.sawcore + + -- from CryptolSAWCore.Cryptol.importPC + , ("Cryptol.PZero" , "Zero") + , ("Cryptol.PLogic" , "Logic") + , ("Cryptol.PRing" , "Ring") + , ("Cryptol.PIntegral" , "Integral") + , ("Cryptol.PField" , "Field") + , ("Cryptol.PRound" , "Round") + , ("Cryptol.PEq" , "Eq") + , ("Cryptol.PCmp" , "Cmp") + , ("Cryptol.PSignedCmp" , "SignedCmp") + , ("Cryptol.PLiteral" , "Literal") + , ("Cryptol.PLiteralLessThan" , "LiteralLessThan") + , ("Cryptol.PFLiteral" , "FLiteral") + -- from CryptolSAWCore.Cryptol.importTFun + , ("Cryptol.tcWidth" , "width") + , ("Cryptol.tcAdd" , "+") + , ("Cryptol.tcSub" , "-") + , ("Cryptol.tcMul" , "*") + , ("Cryptol.tcDiv" , "/") + , ("Cryptol.tcMod" , "%") + , ("Cryptol.tcExp" , "^^") + , ("Cryptol.tcMin" , "min") + , ("Cryptol.tcMax" , "max") + , ("Cryptol.tcCeilDiv" , "/^") + , ("Cryptol.tcCeilMod" , "%^") + , ("Cryptol.tcLenFromThenTo" , "lengthFromThenTo") + ] + where + go (x,txt) = (x, C.lookupPrimType (C.prelPrim txt) pm) + +initTTEnv :: SharedContext -> CryptolEnv -> IO TTEnv +initTTEnv sc env = do + modEnv <- CrySAW.eModuleEnv sc + case lookupModule C.preludeName modEnv of + Just prelude -> do + allPrims <- CrySAW.ePrims sc + allPrimTypes <- CrySAW.ePrimTypes sc + allTerms <- CrySAW.eAllTerms sc + envVarsRef <- newIORef IntMap.empty + usedNamesRef <- newIORef Set.empty + eCacheRef <- newIORef IntMap.empty + tCacheRef <- newIORef IntMap.empty + constTypesRef <- newIORef Map.empty + let + pmap = ifacePrimMap $ lmInterface prelude + exprPrims = fmap (\x -> C.lookupPrimDecl x pmap) $ revMap asConstant allPrims + typePrims = fmap (\x -> C.lookupPrimType x pmap) $ revMap asConstant allPrimTypes + gvmap = IntMap.fromList $ + mapMaybe (\(nm,t) -> (\(vn,_) -> (SAW.vnIndex vn, nm)) <$> asVariable t) + (Map.toList allTerms) + nenv <- CrySAW.getCompleteNamingEnv sc env + return $ + TTEnv + { ttAllEnvVars = envVarsRef + , ttUsedNames = usedNamesRef + , ttConstMap = Map.unions [revMap asConstant allTerms, exprPrims, typePrims] + , ttExtras = Map.fromList (extraPrims pmap) + , ttCryEnv = env + , ttSc = sc + , ttGlobalNamingEnv = nenv + , ttGlobalVarMap = gvmap + , ttBoundExprs = IntMap.empty + , ttExprCache = [eCacheRef] + , ttTypeCache = [tCacheRef] + , ttVarTypes = Map.empty + , ttConstTypes = constTypesRef + } + Nothing -> fail "initTTEnv: missing Cryptol prelude" + +checkConvertible :: Term -> Term -> TT () +checkConvertible t1 t2 = do + sc <- asks ttSc + (liftIO $ scConvertible sc t1 t2) >>= \case + True -> return () + False -> do + let ppts = do + t1' <- liftIO $ prettyTerm sc t1 + t2' <- liftIO $ prettyTerm sc t2 + return $ PP.vcat [t1', PP.indent 2 "vs.",t2'] + withContext (CallContext "checkConvertible" ppts) $ + errMsg "Terms are not convertible" + +prettySawName :: SAW.Name -> String +prettySawName nm = Text.unpack (SAW.toAbsoluteName $ SAW.nameInfo nm) + +revTopProofs :: C.Expr -> C.Expr +revTopProofs = go [] + where + unwind prfs e = case prfs of + x:xs -> C.EProofAbs x (unwind xs e) + [] -> e + go prfs = \case + C.ETAbs tp e -> C.ETAbs tp (go prfs e) + C.ELocated loc e -> C.ELocated loc (go prfs e) + C.EProofAbs prf e -> go (prf:prfs) e + e -> unwind prfs e + +-- | SAW sometimes reverses the guards when importing expressions, in which case we need to reverse the +-- result after type inference in order to recover the original type/term +revGuards :: (Expr, C.Expr, C.Schema) -> (Expr, C.Expr, C.Schema) +revGuards (pe, e,s) = (pe, revTopProofs e, s { C.sProps = reverse (C.sProps s)}) + +validateImport :: Term -> (Expr, C.Expr, C.Schema) -> TT (Expr, C.Expr, C.Schema) +validateImport t (pe, e, s) = do + sc <- asks ttSc + s' <- liftIO $ CrySAW.importSchema sc s + e' <- liftIO $ CrySAW.importExpr sc e + tT <- liftIO $ scTypeOf sc t + checkConvertible tT s' + checkConvertible e' t + return (pe,e,s) + + +inferSchemaExpr :: Term -> TT (Expr, C.Expr, C.Schema) +inferSchemaExpr t = do + sc <- asks ttSc + (pe,ttout) <- listen $ translateAsExprShared t + (res,_) <- liftIO $ CrySAW.inferExpr sc (ttNamingEnv ttout) pe + case res of + Left e -> errMsg (pretty e) + Right (expr,schema) -> do + let r = (pe,expr,schema) + -- the order of the guards is somewhat inconsistent, so we try + -- either the original or reverse orderings and return the one that validates + -- in most cases the reversed order seems to be preferred + validateImport t (revGuards r) <|> validateImport t r + +-- | Attempt to convert a SAWCore term into an equivalent Cryptol expression and corresponding +-- schema. Validates that the resulting type-checked expression and schema will +-- re-produce the given term if imported. +termToSchemaExpr :: + SharedContext -> CryptolEnv -> Term -> IO (Either TTError (Expr, C.Expr, C.Schema)) +termToSchemaExpr sc cenv t = do + env <- initTTEnv sc cenv + runTT env $ inferSchemaExpr t + +-- | Attempt to convert a SAWCore term into an untyped Cryptol expression. +-- Does not validate that the result will correctly translate back into +-- the given term. +termToPExpr :: + SharedContext -> CryptolEnv -> Term -> IO (Either TTError Expr) +termToPExpr sc cenv t = do + env <- initTTEnv sc cenv + runTT env $ translateAsExpr t + +lookupName :: C.Name -> TT Term +lookupName cnm = do + sc <- asks ttSc + allTerms <- liftIO $ CrySAW.eAllTerms sc + mreturn $ Map.lookup cnm allTerms + +lookupPrim :: Text -> TT Term +lookupPrim nm = do + sc <- asks ttSc + modEnv <- liftIO $ CrySAW.eModuleEnv sc + prelude <- mreturn $ lookupModule C.preludeName modEnv + let pmap = ifacePrimMap $ lmInterface prelude + let pnm = C.prelPrim nm + cnm <- mreturn $ Map.lookup pnm (C.primDecls pmap) + lookupName cnm + +propToLambda :: Term -> TT Term +propToLambda t = withTermContext "propToLambda" t $ go t + where + go :: Term -> TT Term + go e = case asPi e of + Just (vn, tp, body) -> do + sc <- asks ttSc + case asEqTrue tp of + Just tp' -> do + body' <- go body + imp <- lookupPrim "==>" + liftIO $ scApplyAll sc imp [tp',body'] + Nothing -> do + body' <- go body + liftIO $ scLambda sc vn tp body' + Nothing -> case asEqTrue e of + Just e' -> return e' + Nothing -> errMsg "Unexpected term shape" + +-- | Attempt to convert a SAWCore proposition into an equivalent Cryptol predicate and corresponding +-- schema. Validates that the resulting type-checked expression and schema will +-- re-produce the given term if imported. +propToSchemaExpr :: SharedContext -> CryptolEnv -> Term -> IO (Either TTError (Expr, C.Expr, C.Schema)) +propToSchemaExpr sc cenv t = do + env <- initTTEnv sc cenv + runTT env $ propToLambda t >>= inferSchemaExpr + +type Name = P.PName +type Type = P.Type Name +type Expr = P.Expr Name +type Prop = P.Prop Name + +data CryptolVar = CryTParam Name | CryParam Name + + +data TTEnv = TTEnv + { ttAllEnvVars :: IORef (IntMap Name) + -- ^ global map from SAW VarIndex to Cryptol variable names + , ttUsedNames :: IORef (Set Name) + -- ^ all generated Cryptol names (codomain of ttAllEnvVars) + , ttConstMap :: Map SAW.Name C.Name + -- ^ map from SAW constants back to Cryptol + , ttExtras :: Map Ident C.Name + -- ^ map from SAW identifiers back to Cryptol + , ttCryEnv :: CryptolEnv + , ttSc :: SharedContext + , ttGlobalNamingEnv :: C.NamingEnv + -- ^ global naming environment, used to check for name clashes + , ttGlobalVarMap :: IntMap C.Name + -- ^ map from global SAW variables (i.e. "invented" variables) back to Cryptol, and + -- the SAW type of the variable + , ttBoundExprs :: IntMap Name + -- ^ map from terms to corresponding let-bound variables + , ttExprCache :: [IORef (IntMap (CachedResult Expr))] + -- ^ cached results (including failed attempts) for 'translateAsExpr' + , ttTypeCache :: [IORef (IntMap (CachedResult Type))] + -- ^ cached results (including failed attempts) for 'translateAsType' + , ttVarTypes :: Map Name (Either Type P.Kind) + -- ^ map from Cryptol variable names to their type/kind + , ttConstTypes :: IORef (Map Name (P.Schema Name)) + -- ^ map from Cryptol const names to their types + } + +type CachedResult a = Either TTError (a, TTOut) + +data CallContext = CallContext { ctxMsg :: String, ctxtContent :: IO PPS.Doc } + +prettyContext :: CallContext -> IO PPS.Doc +prettyContext ctx | debug = do + doc <- ctxtContent ctx + return $ PP.vcat $ [PP.pretty (ctxMsg ctx) PP.<> ": ", PP.indent 2 doc] +prettyContext ctx = ctxtContent ctx + +data TTError = TTError { _ttErrMsg :: String, ttErrContext :: [CallContext], ttErrCommitted :: Bool } + +debug :: Bool +debug = False + +prettyTTError :: TTError -> IO PPS.Doc +prettyTTError (TTError msg ts _) | debug = do + docs <- mapM prettyContext ts + return $ PP.vcat $ [ "Translation to Cryptol failed: ", PP.pretty msg ] ++ docs +prettyTTError (TTError msg ts _) | Just ts' <- NE.nonEmpty ts = do + prettyFirst <- prettyContext (NE.head ts') + case length ts > 1 of + True -> do + prettyLast <- prettyContext (NE.last ts') + return $ PP.vcat + [ "Translation to Cryptol failed:" + , PP.pretty msg PP.<> ":" + , PP.indent 2 prettyFirst + , "in subterm:" + , PP.indent 2 prettyLast + ] + False -> do + return $ PP.vcat $ + [ "Translation to Cryptol failed:" + , PP.pretty msg PP.<> ":" + , PP.indent 2 prettyFirst + ] +prettyTTError (TTError msg _ _) = return $ PP.vcat + [ "Translation to Cryptol failed: ", PP.pretty msg ] + +bindVar :: Name -> Either Type P.Kind -> TTEnv -> TTEnv +bindVar nm tyk env = + env { ttVarTypes = Map.insert nm tyk (ttVarTypes env) } + +lookupVar :: VarIndex -> TT CryptolVar +lookupVar idx = do + m <- deref ttAllEnvVars + vts <- asks ttVarTypes + case IntMap.lookup idx m of + Just nm -> do + tyk <- mreturn $ Map.lookup nm vts + case tyk of + Left{} -> return $ CryParam nm + Right{} -> return $ CryTParam nm + Nothing -> do + g <- asks ttGlobalVarMap + case IntMap.lookup idx g of + Just nm -> do + nm' <- uncheckName nm + case isValueName nm of + True -> return $ CryParam nm' + False -> return $ CryTParam nm' + Nothing -> errMsg $ "lookupVarName: could not find variable: " ++ show idx + +constToName :: SAW.Name -> TT C.Name +constToName nm = do + m <- asks ttConstMap + mT <- asks ttExtras + msum + [ mreturn $ Map.lookup nm m + , do SAW.ModuleIdentifier ident <- return $ SAW.nameInfo nm + mreturn $ Map.lookup ident mT + , errMsg $ "No corresponding Cryptol name for SAW constant: " ++ + Text.unpack (SAW.toAbsoluteName $ SAW.nameInfo nm) + ] + +mkFreshName :: Text -> TT Name +mkFreshName txt = go 0 + where + go :: Integer -> TT Name + go i = do + let + txt' = if i == 0 then txt else (txt <> Text.pack (show i)) + nm = P.UnQual' (C.mkIdent txt') C.SystemName + nm' = P.UnQual' (C.mkIdent txt') C.UserName + m <- deref ttUsedNames + ne <- asks ttGlobalNamingEnv + case Set.member nm m of + False | + Nothing <- C.lookupNS C.NSValue nm ne + , Nothing <- C.lookupNS C.NSValue nm' ne + , Nothing <- C.lookupNS C.NSType nm ne + , Nothing <- C.lookupNS C.NSType nm' ne + -> do + usedNamesRef <- asks ttUsedNames + liftIO $ modifyIORef' usedNamesRef (Set.insert nm) + return nm + _ -> go (i+1) + +deref :: (TTEnv -> IORef a) -> TT a +deref f = do + ref <- asks f + liftIO $ readIORef ref + +mkVarName :: SAW.VarName -> TT Name +mkVarName vn = do + envVarsRef <- asks ttAllEnvVars + envVars <- liftIO $ readIORef envVarsRef + case IntMap.lookup (SAW.vnIndex vn) envVars of + Just nm -> return nm + Nothing -> do + nm <- mkFreshName (SAW.vnName vn) + liftIO $ modifyIORef' envVarsRef $ + IntMap.insert (SAW.vnIndex vn) nm + return nm + +withFreshVar :: SAW.VarName -> Type -> TT a -> TT a +withFreshVar vn ty f = do + nm <- mkVarName vn + local (bindVar nm (Left ty)) f + +withFreshTVar :: SAW.VarName -> P.Kind -> TT a -> TT a +withFreshTVar vn k f = do + nm <- mkVarName vn + local (bindVar nm (Right k)) f + +mreturn :: MonadPlus m => Maybe a -> m a +mreturn (Just a) = return a +mreturn Nothing = empty + +newtype TTOut = TTOut { ttNamingEnv :: C.NamingEnv } + deriving (Semigroup,Monoid) + +newtype TT a = TT { unTT :: ExceptT TTError (WriterT TTOut (ReaderT TTEnv IO)) a } + deriving (Functor, Applicative, Monad, MonadReader TTEnv, MonadError TTError, MonadWriter TTOut ) + +addName :: Name -> C.Name -> TT () +addName pnm nm = + tell $ TTOut (C.singletonNS (C.nameNamespace nm) pnm nm) + +instance MonadIO TT where + liftIO f = do + mres <- TT $ liftIO (try f) + case mres of + Left (e :: IOException) -> throwError $ TTError (show e) [] True + Right a -> return a + +-- Copied from Control.Monad.Error base 2.3 +withError :: MonadError e m => (e -> e) -> m a -> m a +withError f = handleError (throwError . f) + +tryError :: MonadError e m => m a -> m (Either e a) +tryError f = (Right <$> f) `catchError` (pure . Left) + +tryMaybe :: MonadError e m => m a -> m (Maybe a) +tryMaybe f = (Just <$> f) `catchError` (\_ -> pure Nothing) + +-- | Commit to an alternative by considering any uncaught errors thrown +-- by the sub-computation to be unrecoverable. +commit :: TT a -> TT a +commit = withError (\e -> (e {ttErrCommitted = True})) + +-- | Ignore committed errors in the sub-computation +uncommit :: TT a -> TT a +uncommit = withError (\e -> (e {ttErrCommitted = False})) + +withContext :: CallContext -> TT a -> TT a +withContext ctx f = withError (\e -> (e {ttErrContext = ctx : ttErrContext e})) f + +withTermContext :: String -> Term -> TT a -> TT a +withTermContext msg t f = do + sc <- asks ttSc + withContext (CallContext msg (prettyTerm sc t)) f + +withNameContext :: String -> SAW.Name -> TT a -> TT a +withNameContext msg nm = withContext $ CallContext msg (return $ PP.pretty $ prettySawName nm) + +-- Alternative branches are implicit try-catches as long as the +-- thrown error is not committed (i.e. uncaught during a 'commit' action). +instance Alternative TT where + empty = throwError $ TTError "" [] False + f <|> g = + catchError f $ \e -> case ttErrCommitted e of + -- re-throw any committed errors from 'f', as they are considered non-recoverable + True -> throwError e + -- otherwise, attempt the alternative 'g' + False -> catchError g $ \e2 -> case e2 of + -- if the second error is from "empty" (i.e. no more alternatives in an msum), then + -- re-throw the original error, as it is likely to be more informative + TTError "" [] False -> throwError e + _ -> throwError e2 + +instance MonadPlus TT + +instance MonadFail TT where + fail _ = empty + +-- | Use this instead of 'fail', which drops the error message. +errMsg :: String -> TT a +errMsg msg = throwError $ TTError msg [] False + +alts :: String -> Term -> [TT a] -> TT a +alts msg t ttfs = withTermContext msg t $ msum ttfs + +runTT :: TTEnv -> TT a -> IO (Either TTError a) +runTT env f = runReaderT (fst <$> runWriterT (runExceptT (unTT f))) env + +noLoc :: a -> Pos.Located a +noLoc = Pos.Located Pos.emptyRange + +userT :: Name -> [Type] -> Type +userT nm ts = P.TUser (noLoc nm) ts + +lookupCache :: + [IORef (IntMap a)] -> Int -> TT (Maybe a) +lookupCache [] _ = return Nothing +lookupCache (ref:refs) i = do + ecached <- liftIO $ readIORef ref + case IntMap.lookup i ecached of + Just cr -> return $ Just cr + Nothing -> lookupCache refs i + +translateCached :: + (TTEnv -> [IORef (IntMap (CachedResult a))]) -> + (Term -> TT a) -> + Term -> + TT a +translateCached getrefs f t = do + refs <- asks getrefs + mres <- lookupCache refs (termIndex t) + case mres of + Just (Right (a,tout)) -> tell tout >> return a + Just (Left err) -> throwError err + Nothing -> do + me <- tryError (listen $ f t) + -- only save new results in the top of the stack + case refs of + [] -> return () + (ref:_) -> + liftIO $ modifyIORef' ref (IntMap.insert (termIndex t) me) + case me of + Left err -> throwError err + Right (a,tout) -> tell tout >> return a + +-- | NOTE: this will not reliably reproduce all of the constraints +-- originally associated with this type. For this, we need to first translate +-- into an 'Expr' and then use type inference (see 'termToSchemaExpr') +translateAsSchema :: Term -> TT (P.Schema Name) +translateAsSchema t | Just (vn, a, b) <- asPi t = + alts "translateAsSchema" t + [ do k <- translateAsKind a + withFreshTVar vn k $ do + CryTParam nm <- lookupVar (SAW.vnIndex vn) + P.Forall tvs ps tT rng <- translateAsSchema b + return $ P.Forall (P.TParam nm (Just k) Nothing:tvs) ps tT rng + , do ta <- translateAsType a + P.Forall tvs ps tb rng <- translateAsSchema b + return $ P.Forall tvs ps (P.TFun ta tb) rng + , do p <- translateAsConstraint a + P.Forall tvs ps tb rng <- translateAsSchema b + return $ P.Forall tvs (p:ps) tb rng + ] + +translateAsSchema t = do + t' <- translateAsType t + return $ P.Forall [] [] t' Nothing + +translateAsType :: Term -> TT Type +translateAsType = + translateCached ttTypeCache translateAsType' + +translateAsType' :: Term -> TT Type +translateAsType' t = alts "translateAsType" t + [ translateAsInfixTypeApp t + , do [n,a] <- mreturn $ asGlobalApply "Cryptol.seq" t + commit $ do + n' <- translateAsType n + a' <- translateAsType a + return $ P.TSeq n' a' + , do [n] <- mreturn $ asGlobalApply "Cryptol.TCNum" t + n' <- mreturn $ (asNat n <|> asPos n) + return $ P.TNum (fromIntegral n') + , do mreturn $ asBoolType t + return $ P.TBit + -- NOTE: this will intentionally fail if 'b' depends on 'a' + , do (_, a, b) <- mreturn $ asPi t + b' <- translateAsType b + commit $ do + a' <- translateAsType a + return $ P.TFun a' b' + , do (vn, _) <- mreturn $ asVariable t + CryTParam nm <- lookupVar (SAW.vnIndex vn) + return $ userT nm [] + , do (n,a) <- mreturn $ asVectorType t + n' <- translateAsType n + commit $ do + a' <- translateAsType a + return $ P.TSeq n' a' + , do n <- mreturn $ (asNat t <|> asPos t) + let i = fromIntegral n + return $ P.TNum i + , do ts@(_:_) <- mreturn $ asTupleType t + commit $ do + ts' <- mapM translateAsType ts + return $ P.TTuple ts' + , do flds@(_:_) <- mreturn $ asRecordType t + commit $ do + flds' <- forM flds $ \(fld,fldT) -> do + fldT' <- translateAsType fldT + return (C.mkIdent fld,(P.emptyRange, fldT')) + return $ P.TRecord $ C.recordFromFields flds' + , do (tc, nm, ts) <- translateAsTCon t + case tc of + C.TC _ -> return () + C.TF _ -> return () + _ -> errMsg $ "Unexpected type constructor: " ++ (show $ pp tc) + commit $ do + ts' <- mapM translateAsType ts + return $ userT nm ts' + ] + +nameToTCon :: SAW.Name -> TT (C.TCon, Name) +nameToTCon nm = withNameContext "nameToTCon" nm $ msum + [ do nm' <- constToName nm + tc <- mreturn $ C.builtInType nm' + pnm <- uncheckName nm' + return $ (tc, pnm) + , errMsg $ "Could not find Cryptol type for: " ++ prettySawName nm + ] + +translateAsTCon :: Term -> TT (C.TCon, Name, [Term]) +translateAsTCon t = do + let (f, ts) = asApplyAll t + nm <- mreturn $ asConstant f + (tc, pnm) <- nameToTCon nm + return $ (tc, pnm, ts) + +translateAsConstraint :: Term -> TT Prop +translateAsConstraint t = withTermContext "translateAsConstraint" t $ do + (C.PC _ , nm, ts) <- translateAsTCon t + commit $ do + ts' <- mapM translateAsType ts + return $ P.CType $ userT nm ts' + +translateAsKind :: Term -> TT P.Kind +translateAsKind t = alts "translateAsKind" t + [ mreturn $ isGlobalDef "Cryptol.Num" t >> return P.KNum + , mreturn $ asNatType t >> return P.KNum + , do (TypeSort 0) <- mreturn $ asSort t + return P.KType + ] + +nameUses :: C.Namespace -> Name -> TT Int +nameUses ns pn = do + ne <- asks ttGlobalNamingEnv + case C.lookupNS ns pn ne of + Just (C.One{}) -> return 1 + Just (C.Ambig s) -> return $ Set.size s + Nothing -> return 0 + +nameAliases :: C.Namespace -> Name -> TT Int +nameAliases ns nm = case nm of + P.UnQual' ident _ -> do + i <- nameUses ns (P.UnQual' ident C.SystemName) + j <- nameUses ns (P.UnQual' ident C.UserName) + return $ (i + j) + _ -> nameUses ns nm + +uncheckName :: C.Name -> TT Name +uncheckName nm = do + let checkAmbig pn = do + i <- nameAliases (C.nameNamespace nm) pn + if i > 1 then empty else return pn + pnm <- msum + [ checkAmbig (C.nameToDefPName nm) + , checkAmbig (C.nameToPNameWithQualifiers nm) + , do C.GlobalName _ og <- return $ C.nameInfo nm + let mnm = C.topModuleFor $ C.ogModule og + pnm <- case C.nameToPNameWithQualifiers nm of + P.UnQual' i _ -> return $ P.mkQual mnm i + P.Qual ps i -> + let mnm' = C.packModName $ C.modNameChunksText mnm ++ C.modNameChunksText ps + in return $ P.mkQual mnm' i + _ -> empty + checkAmbig pnm + , commit $ errMsg $ "Could not disambiguate name: " ++ show (pp nm) + ] + addName pnm nm + return pnm + +termType :: Term -> TT Term +termType t = case termSortOrType t of + Left s -> errMsg $ "termType: unexpected sort: " ++ show s + Right tT -> return tT + +translateApp :: Bool -> [Term] -> TT ([Type],[Expr]) +translateApp _ [] = return ([],[]) +translateApp useType (arg:args) = do + (argTs,argEs) <- translateApp useType args + alts "translateApp" arg + [ do argT <- termType arg + _ <- translateAsConstraint argT + return (argTs, argEs) + , do arg' <- if useType + then translateAsTypedExpr arg + else translateAsExpr arg + return (argTs,arg':argEs) + , do arg' <- translateAsType arg + return (arg':argTs,argEs) + ] + +eApps :: P.Expr n -> [P.Expr n] -> P.Expr n +eApps e [] = e +eApps e (arg:args) = eApps (P.EApp e arg) args + +isValueName :: C.Name -> Bool +isValueName nm = case C.nameNamespace nm of + C.NSValue -> True + C.NSConstructor -> True + _ -> False + +shouldMemoizeExpr :: Expr -> Bool +shouldMemoizeExpr = \case + P.ETyped e _ -> shouldMemoizeExpr e + P.ELocated e _ -> shouldMemoizeExpr e + P.ELit{} -> False + P.EVar{} -> False + P.EParens e -> shouldMemoizeExpr e + P.ETypeVal{} -> False + _ -> True + + +inCacheFrame :: TT a -> TT a +inCacheFrame f = do + eref <- liftIO $ newIORef IntMap.empty + tref <- liftIO $ newIORef IntMap.empty + local (\env -> env { ttExprCache = eref:(ttExprCache env) + , ttTypeCache = tref:(ttTypeCache env)}) + f + + + +withShared1 :: Term -> (Maybe (Name,Expr,Type) -> TT a) -> TT a +withShared1 t f = do + m <- asks ttBoundExprs + case IntMap.member (termIndex t) m of + True -> f Nothing + False -> tryError (translateAsExpr t) >>= \case + Right e | shouldMemoizeExpr e -> do + nm <- mkFreshName "x" + tT <- typeOfExpr e >>= \case + Nothing -> termType t >>= translateAsType + Just tT -> return tT + local (\env -> env + { ttBoundExprs = IntMap.insert (termIndex t) nm (ttBoundExprs env) + }) $ local (bindVar nm (Left tT)) $ inCacheFrame $ f (Just (nm,e,tT)) + _ -> f Nothing + +mkBind :: Name -> Expr -> Type -> P.Bind Name +mkBind nm e t = P.Bind + { P.bName = noLoc nm + , P.bParams = P.noParams + , P.bDef = noLoc (P.DImpl (P.DExpr e)) + , P.bSignature = Just $ noLoc $ P.Forall [] [] t Nothing + , P.bInfix = False + , P.bFixity = Nothing + , P.bPragmas = [] + , P.bMono = True + , P.bDoc = Nothing + , P.bExport = P.Private + } + + +-- | First extract any shared subterms (at this binding level) and generate +-- where-bindings. Then translate with the fresh bindings in scope, where +-- the bound name will be used in place of the shared term during +-- translation. +translateAsExprShared :: Term -> TT Expr +translateAsExprShared t = do + let shared = map fst $ IntMap.elems $ + IntMap.filter (\(t',cnt) -> cnt >= 2 && SAW.shouldMemoizeTerm t') $ + SAW.scTermCount False t + go shared [] + where + go :: [Term] -> [(Name,Expr,Type)] -> TT Expr + go [] [] = translateAsExpr t + go [] acc = do + e <- translateAsExpr t + return $ P.EWhere e $ map (\(nm,e',tT) -> (P.DBind $ mkBind nm e' tT)) acc + go (t':ts) acc = withShared1 t' $ \case + Nothing -> go ts acc + Just (nm,e,tT) -> go ts ((nm,e,tT):acc) + +translateLambda :: [(SAW.VarName, Term)] -> Term -> TT Expr +translateLambda vars fn = withVars vars $ do + let asParam (vn,tT) = + (do CryParam nm <- lookupVar (SAW.vnIndex vn) + tT' <- translateAsType tT + return $ Just $ P.PTyped (P.PVar (noLoc nm)) tT') + <|> return Nothing + vars' <- catMaybes <$> mapM asParam vars + fn' <- translateAsExprShared fn + case vars' of + [] -> return fn' + _ -> return $ P.EFun P.emptyFunDesc vars' fn' + +lookupSAWConst :: Ident -> TT SAW.Name +lookupSAWConst i = do + sc <- asks ttSc + t <- liftIO $ scGlobalDef sc i + mreturn $ asConstant t + +getConstType :: Name -> TT (P.Schema Name) +getConstType nm = do + m <- deref ttConstTypes + mreturn $ Map.lookup nm m + +translateAsConst :: Term -> TT (Name, Maybe C.Fixity) +translateAsConst t = do + nm <- mreturn $ asConstant t + nm' <- constToName nm + True <- return $ isValueName nm' + pnm <- uncheckName nm' + ref <- asks ttConstTypes + m <- liftIO $ readIORef ref + case Map.lookup pnm m of + Just{} -> return () + Nothing -> do + tT <- termType t + (tryMaybe $ translateAsSchema tT) >>= \case + Just sch -> liftIO $ modifyIORef' ref (Map.insert pnm sch) + Nothing -> return () + return (pnm, C.nameFixity nm') + + +asInfixExprOp :: Term -> TT (Name, C.Fixity) +asInfixExprOp t = alts "asInfixExprOp" t + [ do (pnm,Just fx) <- translateAsConst t + return (pnm, fx) + , do mreturn $ isGlobalDef "Prelude.bvslt" t + nm <- constToName =<< lookupSAWConst "Cryptol.ecSLt" + fx <- mreturn $ C.nameFixity nm + pnm <- uncheckName nm + return (pnm, fx) + ] + +translateAsPrefixExprApp :: Term -> TT Expr +translateAsPrefixExprApp t = do + (fn, args@(_:_)) <- return $ asApplyAll t + (_,[e1]) <- translateApp False args + eop <- asPrefixExprOp fn + asTypedExpr (P.EPrefix eop e1) t + +asPrefixExprOp :: Term -> TT P.PrefixOp +asPrefixExprOp t = alts "asPrefixExprOp" t + [ do mreturn $ isGlobalDef "Cryptol.ecNeg" t + return $ P.PrefixNeg + , do mreturn $ isGlobalDef "Cryptol.ecCompl" t + return $ P.PrefixComplement + ] + +asInfixTypeOp :: Term -> TT (Name, C.Fixity) +asInfixTypeOp t = alts "asInfixTypeOp" t + [ do nm <- mreturn $ asConstant t + nm' <- constToName nm + False <- return $ isValueName nm' + fx <- mreturn $ C.nameFixity nm' + pnm <- uncheckName nm' + return (pnm, fx) + , do mreturn $ isGlobalDef "Prelude.addNat" t + nm <- constToName =<< lookupSAWConst "Cryptol.tcAdd" + fx <- mreturn $ C.nameFixity nm + pnm <- uncheckName nm + return (pnm, fx) + ] + +-- Add type parentheses if needed to make presentation +-- unambiguous +tParens :: Type -> Type +tParens t = case t of + P.TInfix{} -> P.TParens t Nothing + P.TFun{} -> P.TParens t Nothing + P.TLocated t' rng -> P.TLocated (tParens t') rng + _ -> t + +translateAsInfixTypeApp :: Term -> TT Type +translateAsInfixTypeApp t = do + (fn, args@(_:_)) <- return $ asApplyAll t + ([t1,t2],[]) <- translateApp False args + (nm, fx) <- asInfixTypeOp fn + tT <- termType t + _ <- translateAsKind tT + return $ P.TInfix (tParens t1) (noLoc nm) fx (tParens t2) + +-- Add expr parentheses if needed to make presentation +-- unambiguous +eParens :: Expr -> Expr +eParens e = case e of + P.EInfix{} -> pe + P.EPrefix{} -> pe + P.ELocated e' rng -> P.ELocated (eParens e') rng + P.EIf{} -> pe + P.EApp{} -> pe + P.ECase{} -> pe + P.ETyped{} -> pe + P.EFun{} -> pe + _ -> e + where + pe = P.EParens e + +eTyped :: Expr -> Type -> TT Expr +eTyped e t = typeOfExpr e >>= \case + Just{} -> return e + Nothing -> return $ P.ETyped e t + +dropType :: Expr -> Expr +dropType e = case e of + P.ETyped e1 _ -> e1 + _ -> e + +-- | Given a 'Term' as the source of a translated 'Expr', annotate +-- the 'Expr' with an appropriate type if it can't be deduced +-- from the context. +asTypedExpr :: Expr -> Term -> TT Expr +asTypedExpr e t = typeOfExpr e >>= \case + Just{} -> return e + Nothing -> do + tt <- termType t + tt' <- translateAsType tt + return $ P.ETyped e tt' + +-- | Try to deduce the type of an 'Expr' from the current context. +-- Used to drop redundant type annotations as a post-processing step. +typeOfExpr :: Expr -> TT (Maybe Type) +typeOfExpr e0 = tryMaybe $ go e0 + where + go :: Expr -> TT Type + go e = case e of + P.EVar nm -> do + vts <- asks ttVarTypes + case Map.lookup nm vts of + Just (Left ty) -> return ty + _ -> do + (P.Forall [] [] ty _) <- getConstType nm + return ty + P.ETyped _ ty -> return ty + P.EInfix e1 (Pos.thing -> nm) _ e2 -> do + isBinop nm >>= \case + True -> go e1 <|> go e2 + False -> empty + P.EParens e1 -> go e1 + P.ELocated e1 _ -> go e1 + P.EList (es@(e1:_)) -> P.TSeq (P.TNum (fromIntegral $ length es)) <$> go e1 + P.ETuple es -> P.TTuple <$> mapM go es + P.EFun desc ((P.PTyped (P.PVar (Pos.thing -> nm)) tArg):ps) e1 -> + local (bindVar nm (Left tArg)) $ do + t1 <- go (P.EFun desc ps e1) + return $ P.TFun tArg t1 + P.EFun _ [] e1 -> go e1 + P.EWhere e2 (P.DBind d:ds) | + (P.bSignature -> Just (P.thing -> P.Forall [] [] tT _)) <- d -> + let nm = Pos.thing (P.bName d) + in local (bindVar nm (Left tT)) $ go $ P.EWhere e2 ds + P.EWhere e2 [] -> go e2 + -- NOTE: Cryptol has only two prefix operations, which are both + -- type-preserving + P.EPrefix _ e1 -> go e1 + _ -> empty + +-- | Check if this constant is a +-- (possibly polymorphic) type-preserving binary operation +isBinop :: Name -> TT Bool +isBinop nm = fmap isJust $ tryMaybe $ do + P.Forall _ _ (P.TFun t1 (P.TFun t2 t3)) _ <- getConstType nm + True <- return $ t1 == t2 && t2 == t3 + return () + +translateAsInfixExprApp :: Term -> TT Expr +translateAsInfixExprApp t = do + (fn, args@(_:_)) <- return $ asApplyAll t + (nm, fx) <- asInfixExprOp fn + binOp <- isBinop nm + (_,[e1,e2]) <- translateApp True args + -- if the operand is always a type-preserving binop, then + -- we can strip the individual type annotations + let (e1',e2') = if binOp then (dropType e1, dropType e2) else (e1,e2) + let t' = P.EInfix (eParens e1') (noLoc nm) fx (eParens e2') + asTypedExpr t' t + +translateAsTypedExpr :: Term -> TT Expr +translateAsTypedExpr t = do + t' <- translateAsExpr t + case t' of + P.ETyped{} -> return t' + P.EVar{} -> return t' + _ -> asTypedExpr t' t + +stripTyped :: Expr -> Expr +stripTyped = \case + P.ETyped e _ -> stripTyped e + e -> e + +unNumber :: Expr -> TT Expr +unNumber e = case e of + P.EAppT (P.EVar nm) [P.PosInst val, P.PosInst rep] -> do + number <- (uncheckName =<< constToName =<< lookupSAWConst "Cryptol.ecNumber") + case nm == number of + True -> unNumber =<< eTyped (P.ETypeVal val) rep + False -> return e + P.ETyped (P.ETypeVal (P.TNum n)) rep -> do + let i = fromIntegral n + eTyped (P.ELit (P.ECNum i (P.DecLit (Text.pack $ show i)))) rep + _ -> return e + +translateLetBound :: Term -> TT Expr +translateLetBound t = do + m <- asks ttBoundExprs + nm <- mreturn $ IntMap.lookup (termIndex t) m + return $ P.EVar nm + +translateAsExpr :: Term -> TT Expr +translateAsExpr t = alts "translateAsExpr" t + -- we need to attempt translating as a let-bound variable before + -- consulting the cache, since let-bound terms will always be + -- in the cache, and we want to use the name rather than inlining it + [ translateLetBound t + , translateCached ttExprCache translateAsExpr' t + ] + +translateAsExpr' :: Term -> TT Expr +translateAsExpr' t = unNumber =<< alts "translateAsExpr'" t + [ translateLetBound t + , do n' <- mreturn $ (asNat t <|> asPos t) + let i = fromIntegral n' + return $ P.ELit (P.ECNum i (P.DecLit (Text.pack $ show i))) + , do (recv,fld) <- mreturn $ asRecordSelector t + commit $ do + recv' <- translateAsExpr recv + return $ P.ESel recv' (P.RecordSel (C.mkIdent fld) Nothing) + , do [n,x] <- mreturn $ asGlobalApply "Prelude.bvNat" t + n' <- translateAsType n + x' <- translateAsType x + eTyped (P.ETypeVal x') (P.TSeq n' P.TBit) + , do (fn, _) <- return $ asApplyAll t + mreturn $ isGlobalDef "Prelude.headRecord" fn + commit $ do + (t1,t2) <- mreturn $ asApp t + t1' <- translateAsExpr t1 + alts "headRecord" t2 [ + do t2' <- translateAsExpr t2 + return $ P.EApp t1' t2' + , do t2' <- translateAsType t2 + return $ P.EAppT t1' [P.PosInst t2'] + ] + , translateAsInfixExprApp t + , translateAsPrefixExprApp t + , do (fn, args@(_:_)) <- return $ asApplyAll t + fn' <- translateAsExpr fn + commit $ do + (argTs,argEs) <- translateApp False args + return $ eApps (P.EAppT fn' (map P.PosInst argTs)) argEs + , do (vars@(_:_), fn) <- return $ asLambdaList t + commit $ translateLambda vars fn + , do (vn,_) <- mreturn $ asVariable t + CryParam nm <- lookupVar (SAW.vnIndex vn) + return $ P.EVar nm + , do (tT :*: p :*: caseTrue :*: caseFalse) <- mreturn $ asMux t + _ <- translateAsType tT + commit $ do + caseTrue' <- translateAsExpr caseTrue + caseFalse' <- translateAsExpr caseFalse + p' <- translateAsExpr p + return $ P.EIf (stripTyped p') caseTrue' caseFalse' + , do ts <- mreturn $ asTupleValue t + commit $ do + ts' <- mapM translateAsExpr ts + return $ P.ETuple ts' + , do (tup, i) <- mreturn $ asTupleSelector t + commit $ do + tup' <- translateAsExpr tup + return $ P.ESel tup' (P.TupleSel i Nothing) + , do flds <- mreturn $ asRecordValue t + commit $ do + flds' <- forM flds $ \(fld,fldE) -> do + fldE' <- translateAsExpr fldE + return (C.mkIdent fld,(P.emptyRange, fldE')) + return $ P.ERecord $ C.recordFromFields flds' + , do (nm, _) <- translateAsConst t + return $ P.EVar nm + ] + +withVars :: [(SAW.VarName, Term)] -> TT a -> TT a +withVars [] f = f +withVars ((vn,t):vs) f = withVar vn t $ withVars vs $ f + +withVar :: SAW.VarName -> Term -> TT a -> TT a +withVar vn t f = alts "withVar" t + [ do t' <- translateAsType t + uncommitNat $ withFreshVar vn t' f + , do _ <- translateAsConstraint t + commit $ f + , do t' <- translateAsKind t + uncommitNat $ withFreshTVar vn t' f + ] + where + -- Nat can be treated as both a value and a type, so + -- we may need to attempt both translations, ignoring + -- otherwise unrecoverable errors + uncommitNat :: TT a -> TT a + uncommitNat g = case asNatType t of + Just () -> uncommit g + Nothing -> commit g diff --git a/cryptol-saw-core/src/CryptolSAWCore/TypedTerm.hs b/cryptol-saw-core/src/CryptolSAWCore/TypedTerm.hs index fcc15a0631..5bfbc25565 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/TypedTerm.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/TypedTerm.hs @@ -56,7 +56,7 @@ import qualified Cryptol.Utils.RecordMap as C (recordFromFields) import qualified SAWSupport.Pretty as PPS (Opts, renderText) import qualified CryptolSAWCore.Pretty as CryPP -import CryptolSAWCore.Cryptol (scCryptolType, CryptolEnv, importKind, translateSchema) +import CryptolSAWCore.Cryptol (scCryptolType, importKind, translateSchema) import SAWCore.FiniteValue import SAWCore.Name (VarName(..)) import SAWCore.Recognizer (asVariable) @@ -173,11 +173,11 @@ ppTypedTermPure opts t = -- | Convert the 'ttType' field of a 'TypedTerm' to a SAWCore term -ttTypeAsTerm :: SharedContext -> CryptolEnv -> TypedTerm -> IO Term -ttTypeAsTerm sc env (TypedTerm (TypedTermSchema schema) _) = - translateSchema sc env schema -ttTypeAsTerm sc _ (TypedTerm (TypedTermKind k) _) = importKind sc k -ttTypeAsTerm _ _ (TypedTerm (TypedTermOther tp) _) = return tp +ttTypeAsTerm :: SharedContext -> TypedTerm -> IO Term +ttTypeAsTerm sc (TypedTerm (TypedTermSchema schema) _) = + translateSchema sc schema +ttTypeAsTerm sc (TypedTerm (TypedTermKind k) _) = importKind sc k +ttTypeAsTerm _ (TypedTerm (TypedTermOther tp) _) = return tp ttTermLens :: Functor f => (Term -> f Term) -> TypedTerm -> f TypedTerm ttTermLens f tt = tt `seq` fmap (\x -> tt{ttTerm = x}) (f (ttTerm tt)) diff --git a/intTests/test2304/test03.log.good b/intTests/test2304/test03.log.good index 919e652ca3..46e82ec3a4 100644 --- a/intTests/test2304/test03.log.good +++ b/intTests/test2304/test03.log.good @@ -1,7 +1,13 @@ Loading file "test03.saw" +True +True +True +Error: Cryptol: [error] at test03.saw:16:25--16:26 + Value not in scope: y Stack trace: - (builtin) (at top level) -Attempt to register name with duplicate qualified name - x`4785@cryptol + (builtin) in (callback) + (builtin) in fails + test03.saw:16:4-16:49 (at top level) -FAILED +(Failure was expected, continuing) +True diff --git a/intTests/test2304/test03.saw b/intTests/test2304/test03.saw index bcdd08fd69..87268d55e1 100644 --- a/intTests/test2304/test03.saw +++ b/intTests/test2304/test03.saw @@ -1,12 +1,18 @@ do { let {{ x = 3 : [8] }}; - do { + let g = do { let {{ x = 4 : Integer }}; + print {{ x == (4 : Integer) }}; return (); }; + g; do { let {{ x = 5 : Integer }}; + let {{ y = x : Integer }}; + print {{ x == (5 : Integer) }}; + g; return (); }; + fails (do { print {{ y == (5 : Integer) }}; }); print {{ x == (3 : [8]) }}; }; diff --git a/intTests/test2304/test04.log.good b/intTests/test2304/test04.log.good index 7e1d2bfcb9..5c535cfbd4 100644 --- a/intTests/test2304/test04.log.good +++ b/intTests/test2304/test04.log.good @@ -1,7 +1,7 @@ Loading file "test04.saw" ("a", \(u1218 : isort 0) -> \(_P : PLiteral u1218) -> ecNumber (TCNum 3) u1218 _P) -("b", \(u1218 : isort 0) -> - \(_P : PLiteral u1218) -> ecNumber (TCNum 4) u1218 _P) -("c", \(u1218 : isort 0) -> - \(_P : PLiteral u1218) -> ecNumber (TCNum 5) u1218 _P) +("b", \(u1220 : isort 0) -> + \(_P : PLiteral u1220) -> ecNumber (TCNum 4) u1220 _P) +("c", \(u1222 : isort 0) -> + \(_P : PLiteral u1222) -> ecNumber (TCNum 5) u1222 _P) diff --git a/intTests/test2304/test05.log.good b/intTests/test2304/test05.log.good index 46b4fabde0..0171fb0b31 100644 --- a/intTests/test2304/test05.log.good +++ b/intTests/test2304/test05.log.good @@ -1,7 +1,7 @@ Loading file "test05.saw" ("a", \(u1218 : isort 0) -> \(_P : PLiteral u1218) -> ecNumber (TCNum 3) u1218 _P) -("b", \(u1218 : isort 0) -> - \(_P : PLiteral u1218) -> ecNumber (TCNum 4) u1218 _P) -("c", \(u1218 : isort 0) -> - \(_P : PLiteral u1218) -> ecNumber (TCNum 5) u1218 _P) +("b", \(u1220 : isort 0) -> + \(_P : PLiteral u1220) -> ecNumber (TCNum 4) u1220 _P) +("c", \(u1222 : isort 0) -> + \(_P : PLiteral u1222) -> ecNumber (TCNum 5) u1222 _P) diff --git a/intTests/test2304/test06.cry b/intTests/test2304/test06.cry new file mode 100644 index 0000000000..87af43f4eb --- /dev/null +++ b/intTests/test2304/test06.cry @@ -0,0 +1,5 @@ +x : Integer +x = 3 + +y : Integer +y = 5 \ No newline at end of file diff --git a/intTests/test2304/test06.log.good b/intTests/test2304/test06.log.good new file mode 100644 index 0000000000..3c293103ce --- /dev/null +++ b/intTests/test2304/test06.log.good @@ -0,0 +1,2 @@ +Loading file "test06.saw" +Success diff --git a/intTests/test2304/test06.saw b/intTests/test2304/test06.saw new file mode 100644 index 0000000000..f8bed5a1eb --- /dev/null +++ b/intTests/test2304/test06.saw @@ -0,0 +1,21 @@ +let {{ x = 4 : Integer }}; + +let g z = return {{ `(z) + x == 6 }}; +let f z = do { return {{ `(z) + x == 6 }}; }; + +import "test06.cry"; +// local binding takes precedence after import +prove_print z3 {{ x == 4 }}; +prove_print z3 {{ y == 5 }}; +t <- f 2; +prove_print z3 t; +t2 <- g 2; +prove_print z3 t2; + +import "test06.cry" as test06; + +// previous import is still available +prove_print z3 {{ y == 5 }}; +prove_print z3 {{ test06::x == 3 }}; + +print "Success"; \ No newline at end of file diff --git a/intTests/test3167/Bar.cry b/intTests/test3167/Bar.cry new file mode 100644 index 0000000000..38b1eb56cb --- /dev/null +++ b/intTests/test3167/Bar.cry @@ -0,0 +1,4 @@ +module Bar where + +bar : [8] +bar = 1 \ No newline at end of file diff --git a/intTests/test3167/Foo.cry b/intTests/test3167/Foo.cry new file mode 100644 index 0000000000..3dbc9dad45 --- /dev/null +++ b/intTests/test3167/Foo.cry @@ -0,0 +1,4 @@ +module Foo where + +foo : [8] +foo = 0 \ No newline at end of file diff --git a/intTests/test3167/test.saw b/intTests/test3167/test.saw new file mode 100644 index 0000000000..1a7f86679e --- /dev/null +++ b/intTests/test3167/test.saw @@ -0,0 +1,9 @@ +import "Foo.cry"; + +let foo (m: CryptolModule) = do { + return {{ foo }}; +}; + +bar <- cryptol_load "Bar.cry"; + +foo bar; diff --git a/intTests/test3167/test.sh b/intTests/test3167/test.sh new file mode 100644 index 0000000000..f7eeb6ad15 --- /dev/null +++ b/intTests/test3167/test.sh @@ -0,0 +1,2 @@ +set -e +$SAW test.saw diff --git a/intTests/test_saw_to_cryptol/test.cry b/intTests/test_saw_to_cryptol/test.cry new file mode 100644 index 0000000000..4a0d177007 --- /dev/null +++ b/intTests/test_saw_to_cryptol/test.cry @@ -0,0 +1,16 @@ +tcPlusTest : {n, m} (fin n, fin m) => [n] -> [m] -> [m + n] +tcPlusTest _ _ = 0 + +tcMinusTest : {n, m} (fin n, fin m, n <= m) => [n] -> [m] -> [m - n] +tcMinusTest _ _ = 0 + + +sharedTest : {n} (fin n, n >= 1) => [n] -> [n] +sharedTest x = (z - y) * z + where + y = x + 1 + z = y * y + + +unaryMinusTest : {n} (fin n) => [n] -> [n] +unaryMinusTest x = -x diff --git a/intTests/test_saw_to_cryptol/test.log.good b/intTests/test_saw_to_cryptol/test.log.good new file mode 100644 index 0000000000..535090eb48 --- /dev/null +++ b/intTests/test_saw_to_cryptol/test.log.good @@ -0,0 +1,94 @@ +Loading file "test.saw" +if x <$ (100 : [32]) then 100 : [32] else x +[32] +if x <$ (100 : [32]) then 100 : [32] else x +[32] +\(__p0 : [n]) (__p1 : [m]) -> 0 : [n + m] +{n, m} (fin n, fin m) => [n] -> [m] -> [n + m] +\(__p2 : [n]) (__p3 : [m]) -> 0 : [m - n] +{n, m} (fin n, fin m, m >= n) => [n] -> [m] -> [m - n] +\(x : [n]) -> +(x2 - x1) * x2 +where + x2 : [n] + x2 := x1 * x1 + x1 : [n] + x1 := x + 1 +{n} (fin n, n >= 1) => [n] -> [n] +\(x : [n]) -> -x +{n} (fin n) => [n] -> [n] +\(xs : [n][a]) (ys : [n][a]) -> +Main::sum`{n, a} (Main::zip`{n, [a]} (*)`{[a]} xs ys) +{n, a} (fin n, fin a) => [n][a] -> [n][a] -> [a] +Warning: [warning] at ../../examples/ecdsa/cryptol-spec/bv.cry:33:9--33:12 + This binding for `sum` shadows the existing binding at + Cryptol:1177:1--1177:4 +Warning: [warning] at ../../examples/ecdsa/cryptol-spec/mul_java.cry:149:36--149:44 + Unused name: ij_final +Warning: [warning] at ../../examples/ecdsa/cryptol-spec/ref_ec_mul.cry:31:4--31:5 + Unused name: f +[warning] at ../../examples/ecdsa/cryptol-spec/ref_ec_mul.cry:96:13--96:16 + This binding for `abs` shadows the existing binding at + Cryptol:605:1--605:4 +[warning] at ../../examples/ecdsa/cryptol-spec/ref_ec_mul.cry:97:12--97:15 + Unused name: c00 +[warning] at ../../examples/ecdsa/cryptol-spec/ref_ec_mul.cry:97:44--97:47 + Unused name: c10 +Warning: [warning] at ../../examples/ecdsa/cryptol-spec/p384_ec_mul.cry:20:13--20:16 + This binding for `sum` shadows the existing binding at + Cryptol:1177:1--1177:4 +[warning] at ../../examples/ecdsa/cryptol-spec/p384_ec_mul.cry:189:4--189:5 + Unused name: f +[warning] at ../../examples/ecdsa/cryptol-spec/p384_ec_mul.cry:190:4--190:5 + Unused name: g +Warning: [warning] at ../../examples/ecdsa/cryptol-spec/ecc.cry:119:5--119:8 + This binding for `sum` shadows the existing binding at + Cryptol:1177:1--1177:4 +({affinify : + {x : [384], y : [384], z : [384]} -> {x : [384], y : [384]}, + base : {x : [384], y : [384]}, + mul : + ([384], {x : [384], y : [384]}) -> + {x : [384], y : [384], z : [384]}, + point_ops : + {add : + ({x : [384], y : [384], z : [384]}, {x : [384], y : [384]}) -> + {x : [384], y : [384], z : [384]}, + double : + {x : [384], y : [384], z : [384]} -> + {x : [384], y : [384], z : [384]}, + field : + {add : ([384], [384]) -> [384], + div : ([384], [384]) -> [384], + field_unit : [384], + field_zero : [384], + half : [384] -> [384], + is_equal : ([384], [384]) -> Bit, + is_val : [384] -> Bit, + mul : ([384], [384]) -> [384], + neg : [384] -> [384], + normalize : [384] -> [384], + sq : [384] -> [384], + sub : ([384], [384]) -> [384]}, + group_field : + {add : ([384], [384]) -> [384], + div : ([384], [384]) -> [384], + field_unit : [384], + field_zero : [384], + half : [384] -> [384], + is_equal : ([384], [384]) -> Bit, + is_val : [384] -> Bit, + mul : ([384], [384]) -> [384], + neg : [384] -> [384], + normalize : [384] -> [384], + sq : [384] -> [384], + sub : ([384], [384]) -> [384]}, + sub : + ({x : [384], y : [384], z : [384]}, {x : [384], y : [384]}) -> + {x : [384], y : [384], z : [384]}}, + twin_mul : + ([384], {x : [384], y : [384]}, [384], {x : [384], y : [384]}) -> + {x : [384], y : [384], z : [384]}}, + [384], + ([384], [384]), + {x : [384], y : [384]}) -> Bit diff --git a/intTests/test_saw_to_cryptol/test.saw b/intTests/test_saw_to_cryptol/test.saw new file mode 100644 index 0000000000..c4277425c1 --- /dev/null +++ b/intTests/test_saw_to_cryptol/test.saw @@ -0,0 +1,42 @@ +enable_experimental; + +let assert_tyeq t1 t2 = do { + let tT1 = type t1; + let tT2 = type t2; + let f1 = {{ \(x : tT1) -> x }}; + let f2 = {{ \(x : tT2) -> x }}; + b <- is_convertible f1 f2; + if b then return () else + fail (str_concats ["Types are incompatible.",show f1,"\nvs:\n",show f2]); +}; + +let roundtrip t1 = do { + // strip TypedTermSchema by round-trip through parser + let t2 = parse_core (show_term t1); + let s1 = show_cryptol_term t1; + assert_tyeq t1 t2; + print s1; + print (show (type t1)); +}; + +let {{ x = (0 : [32]) }}; + +roundtrip {{ if (x : [32]) <$ (100 : [32]) then (100 : [32]) else x }}; +roundtrip (parse_core "let { x`1 = bvNat 32 100;} in ite (Vec 32 Bool) (bvslt 32 x x`1) x`1 x"); + +import "test.cry"; + +roundtrip (unfold_term ["tcPlusTest"] ({{ tcPlusTest }})); +roundtrip (unfold_term ["tcMinusTest"] ({{ tcMinusTest }})); +roundtrip (unfold_term ["sharedTest"] ({{ sharedTest }})); +roundtrip (unfold_term ["unaryMinusTest"] ({{ unaryMinusTest }})); + +import "../../examples/llvm/dotprod.cry"; +roundtrip (unfold_term ["dotprod"] {{ dotprod }}); + +import "../../examples/ecdsa/cryptol-spec/ecc.cry"; +let t1 = unfold_term ["ecdsa_public_verify_imp"] {{ ecdsa_public_verify_imp }}; +let t2 = parse_core (show_term t1); + +assert_tyeq t1 t2; +print (show (type t2)); diff --git a/intTests/test_saw_to_cryptol/test.sh b/intTests/test_saw_to_cryptol/test.sh new file mode 100755 index 0000000000..5fcd79d0a6 --- /dev/null +++ b/intTests/test_saw_to_cryptol/test.sh @@ -0,0 +1 @@ +exec ${TEST_SHELL:-bash} ../support/test-and-diff.sh "$@" diff --git a/otherTests/cryptol-saw-core/CryptolVerifierTC.hs b/otherTests/cryptol-saw-core/CryptolVerifierTC.hs index 836b82ee99..3d8193e90d 100644 --- a/otherTests/cryptol-saw-core/CryptolVerifierTC.hs +++ b/otherTests/cryptol-saw-core/CryptolVerifierTC.hs @@ -4,7 +4,6 @@ module Main (main) where -import qualified Data.ByteString as BS import Data.Text (Text) import Text.Heredoc (there) @@ -21,7 +20,6 @@ main = C.scLoadPreludeModule sc C.scLoadCryptolModule sc putStrLn "Loaded Cryptol.sawcore!" - let ?fileReader = BS.readFile cenv0 <- CEnv.initCryptolEnv sc putStrLn "Translated Cryptol.cry!" let importCryptolModule' cenv nm = diff --git a/saw-central/src/SAWCentral/Bisimulation.hs b/saw-central/src/SAWCentral/Bisimulation.hs index 142f45b51b..9185959c78 100644 --- a/saw-central/src/SAWCentral/Bisimulation.hs +++ b/saw-central/src/SAWCentral/Bisimulation.hs @@ -177,8 +177,8 @@ scRelation rel relLhs relRhs = do -- | Import a Cryptol type and define a fresh variable of that type. importFresh :: SharedContext -> C.CryptolEnv -> Text.Text -> C.Type -> IO Term -importFresh sc cryenv name t = do - t' <- C.translateType sc cryenv t +importFresh sc _cryenv name t = do + t' <- C.translateType sc t scFreshVariable sc name t' -- | Build the COMPOSITION SIDE CONDITION for 'bc' and 'bt'. See the @@ -766,11 +766,10 @@ replaceConstantTerm constant constantRetType term = ["rsApp should always exist when rsVariable exists"] Nothing -> do sc <- lift getSharedContext - cryenv <- lift getCryptolEnv -- Generate a 'Variable' and return it, thereby replacing 'termF' -- with it. - tp <- liftIO $ C.translateType sc cryenv constantRetType + tp <- liftIO $ C.translateType sc constantRetType name <- lift $ constantName $ unwrapTermF x v <- liftIO $ scFreshVariable sc name tp State.modify $ \st -> st { rsVariable = Just v, rsApp = Just termF } diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index f36df2a111..354c1e1925 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -35,6 +35,7 @@ module SAWCentral.Builtins ( show_term, print_term, print_term_depth, + show_cryptol_term, write_goal, print_goal, print_goal_inline, @@ -259,6 +260,7 @@ import Text.Read (readMaybe) import Prettyprinter ((<+>)) import qualified CryptolSAWCore.Simpset as Cryptol +import qualified CryptolSAWCore.SAWCoreCryptol as Cryptol -- saw-support import qualified SAWSupport.PanicSupport as PanicSupport @@ -315,7 +317,7 @@ import qualified Cryptol.Eval.Value as C (fromVBit, fromVWord) import qualified Cryptol.Eval.Concrete as C (Concrete(..), bvVal) import qualified Cryptol.Utils.Ident as C (packModName, textToModName, PrimIdent(..)) - +import qualified Cryptol.Parser.AST as P -- crucible import Lang.Crucible.CFG.Common (freshGlobalVar) @@ -354,8 +356,7 @@ showPrim v = do definePrim :: Text -> TypedTerm -> TopLevel TypedTerm definePrim name (TypedTerm (TypedTermSchema schema) rhs) = do sc <- getSharedContext - cryenv <- SV.getCryptolEnv - ty <- io $ CSC.translateSchema sc cryenv schema + ty <- io $ CSC.translateSchema sc schema rhs' <- io $ scAscribe sc rhs ty t <- io $ scFreshConstant sc name rhs' return $ TypedTerm (TypedTermSchema schema) t @@ -637,6 +638,47 @@ print_term_depth d t = output <- SV.withPPOpts adjust $ ppTerm sc t printOutLnTop Info output +data CryptolResult = + CryptolResultErr String + | CryptolResultPartial String (P.Expr P.PName) + -- ^ Translation into an untyped Cryptol expression succeeded, + -- but the result did not re-translate back into the source + -- term. + | CryptolResultSuccess (P.Expr P.PName) C.Expr C.Schema + -- ^ The untyped and typechecked expression, with the corresponding + -- schema. Indicates that both the expression and schema will translate + -- back into the source 'Term' and its type, respectively. + +saw_to_cryptol :: Term -> TopLevel CryptolResult +saw_to_cryptol t = do + sc <- getSharedContext + cenv <- SV.getCryptolEnv + ppopts <- io $ scGetPPOpts sc + res <- io $ Cryptol.termToSchemaExpr sc cenv t + case res of + Left er -> do + msg <- io $ Cryptol.prettyTTError er + let errtxt = PPS.render ppopts msg + pres <- io $ Cryptol.termToPExpr sc cenv t + case pres of + Left{} -> return $ CryptolResultErr errtxt + Right pe -> return $ CryptolResultPartial errtxt pe + Right (pe,e,s) -> return $ CryptolResultSuccess pe e s + +show_cryptol_term :: TypedTerm -> TopLevel Text +show_cryptol_term tt = do + sc <- getSharedContext + ppopts <- io $ scGetPPOpts sc + res <- saw_to_cryptol (ttTerm tt) + case res of + CryptolResultErr er -> fail er + CryptolResultPartial er pe -> do + printOutLnTop Warn $ unlines + [ "Cryptol extraction failed during type-checking:", er] + return $ PPS.renderText ppopts $ CryPP.pretty pe + CryptolResultSuccess pe _ _ -> + return $ PPS.renderText ppopts $ CryPP.pretty pe + goalSummary :: ProofGoal -> String goalSummary goal = unlines $ concat [ [ "Goal " ++ goalName goal ++ " (goal number " ++ (show $ goalNum goal) ++ "): " ++ goalType goal @@ -763,8 +805,7 @@ resolveNames nms = resolveNameIO :: SharedContext -> CSC.CryptolEnv -> Text -> IO [VarIndex] resolveNameIO sc cenv nm = do scnms <- scResolveName sc nm - let ?fileReader = StrictBS.readFile - res <- CSC.resolveIdentifier cenv nm + res <- CSC.resolveIdentifier sc cenv nm case res of Just cnm -> do importedName <- CSC.importName cnm @@ -933,10 +974,14 @@ term_type tt = case ttType tt of TypedTermSchema sch -> pure sch tp -> do - sc <- getSharedContext - opts <- SV.getPPOpts - tp' <- liftIO $ prettyTypedTermType sc tp - fail $ PPS.render opts $ "Term does not have a Cryptol type:" <+> tp' + res <- saw_to_cryptol (ttTerm tt) + case res of + CryptolResultSuccess _ _ sch -> return sch + _ -> do + sc <- getSharedContext + opts <- SV.getPPOpts + tp' <- liftIO $ prettyTypedTermType sc tp + fail $ PPS.render opts $ "Term does not have a Cryptol type:" <+> tp' goal_eval :: [Text] -> ProofScript () goal_eval unints = @@ -1643,12 +1688,11 @@ print_type t = do check_term :: TypedTerm -> TopLevel () check_term tt = do sc <- getSharedContext - cenv <- SV.getCryptolEnv let t = ttTerm tt ty <- io $ scTypeOf sc t expectedTy <- case ttType tt of - TypedTermSchema schema -> io $ CSC.translateSchema sc cenv schema + TypedTermSchema schema -> io $ CSC.translateSchema sc schema TypedTermKind k -> io $ CSC.importKind sc k TypedTermOther ty' -> pure ty' convertible <- io $ scConvertible sc ty expectedTy @@ -1675,8 +1719,7 @@ check_goal = freshSymbolicPrim :: Text -> C.Schema -> TopLevel TypedTerm freshSymbolicPrim x schema@(C.Forall [] [] ct) = do sc <- getSharedContext - cryenv <- SV.getCryptolEnv - cty <- io $ CSC.translateType sc cryenv ct + cty <- io $ CSC.translateType sc ct vn <- io $ scFreshInventedVar sc x cty tm <- io $ scVariable sc vn cty return $ TypedTerm (TypedTermSchema schema) tm @@ -1906,7 +1949,6 @@ list_term :: [TypedTerm] -> TopLevel TypedTerm list_term [] = fail "list_term: invalid empty list" list_term tts@(tt0 : _) = do sc <- getSharedContext - cryenv <- SV.getCryptolEnv a <- case ttType tt0 of TypedTermSchema (C.Forall [] [] a) -> return a _ -> fail "list_term: not a monomorphic element type" @@ -1915,7 +1957,7 @@ list_term tts@(tt0 : _) = unless (all eqa (map ttType tts)) $ fail "list_term: non-uniform element types" - a' <- io $ CSC.translateType sc cryenv a + a' <- io $ CSC.translateType sc a trm <- io $ scVectorReduced sc a' (map ttTerm tts) let n = C.tNum (length tts) return (TypedTerm (TypedTermSchema (C.tMono (C.tSeq n a))) trm) @@ -1931,9 +1973,8 @@ eval_list t = Just (_ty, ts) -> pure (map (TypedTerm (TypedTermSchema (C.tMono a))) ts) Nothing -> - do cryenv <- SV.getCryptolEnv - n' <- io $ scNat sc (fromInteger n) - a' <- io $ CSC.translateType sc cryenv a + do n' <- io $ scNat sc (fromInteger n) + a' <- io $ CSC.translateType sc a idxs <- io $ traverse (scNat sc) $ map fromInteger [0 .. n - 1] ts <- io $ traverse (scAt sc n' a' (ttTerm t)) idxs pure (map (TypedTerm (TypedTermSchema (C.tMono a))) ts) @@ -1950,13 +1991,13 @@ default_typed_term :: TypedTerm -> TopLevel TypedTerm default_typed_term tt = do sc <- getSharedContext cenv <- SV.getCryptolEnv - let cfg = CSC.meSolverConfig (CSC.eModuleEnv cenv) + cfg <- CSC.meSolverConfig <$> (io $ CSC.eModuleEnv sc) opts <- getOptions io $ defaultTypedTerm opts sc cenv cfg tt -- | Default the values of the type variables in a typed term. defaultTypedTerm :: Options -> SharedContext -> CSC.CryptolEnv -> C.SolverConfig -> TypedTerm -> IO TypedTerm -defaultTypedTerm opts sc cryenv cfg tt@(TypedTerm (TypedTermSchema schema) trm) +defaultTypedTerm opts sc _cryenv cfg tt@(TypedTerm (TypedTermSchema schema) trm) | null (C.sVars schema) = return tt | otherwise = do mdefault <- C.withSolver (return ()) cfg (\s -> C.defaultReplExpr s undefined schema) @@ -1972,12 +2013,12 @@ defaultTypedTerm opts sc cryenv cfg tt@(TypedTerm (TypedTermSchema schema) trm) mapM_ (warnDefault ppopts nms) (zip vars tys) let applyType :: Term -> C.Type -> IO Term applyType t ty = do - ty' <- CSC.translateType sc cryenv ty + ty' <- CSC.translateType sc ty scApply sc t ty' let dischargeProp :: Term -> C.Prop -> IO Term dischargeProp t p | CSC.isErasedProp p = return t - | otherwise = scApply sc t =<< CSC.proveProp sc cryenv p + | otherwise = scApply sc t =<< CSC.proveProp sc p trm' <- foldM applyType trm tys let su = C.listSubst (zip (map C.tpVar vars) tys) let props = map (plainSubst su) (C.sProps schema) @@ -2212,35 +2253,29 @@ cryptol_prims = parsePrim :: (Text, Ident, Text) -> TopLevel (C.Name, TypedTerm) parsePrim (n, i, s) = do sc <- getSharedContext - SV.CryptolEnvStack cenv cenvs <- SV.getCryptolEnvStack - unless (null cenvs) $ do + cenv <- SV.getCryptolEnv + unless (CSC.isToplevel cenv) $ do fail "cryptol_prims is an import operation and may not be done in a nested block" let mname = C.packModName ["Prims"] - let ?fileReader = StrictBS.readFile - (n', cenv') <- io $ CSC.declareName cenv mname n - (s', cenv'') <- io $ CSC.parseSchema cenv' (noLoc s) + n' <- io $ CSC.declareName sc mname n + s' <- io $ CSC.parseSchema sc cenv (noLoc s) t' <- io $ scGlobalDef sc i - SV.setCryptolEnv cenv'' return (n', TypedTerm (TypedTermSchema s') t') cryptol_load :: (FilePath -> IO StrictBS.ByteString) -> FilePath -> TopLevel CSC.ExtCryptolModule cryptol_load fileReader path = do sc <- getSharedContext - SV.CryptolEnvStack ce ces <- SV.getCryptolEnvStack - unless (null ces) $ do + ce <- SV.getCryptolEnv + unless (CSC.isToplevel ce) $ do fail "cryptol_load is an import operation and is not permitted in nested blocks" - let ?fileReader = fileReader - (m, ce') <- io $ CSC.loadExtCryptolModule sc ce path - SV.setCryptolEnv ce' + m <- io $ CSC.withFileReader sc fileReader $ CSC.loadExtCryptolModule sc path return m cryptol_extract :: CSC.ExtCryptolModule -> Text -> TopLevel TypedTerm cryptol_extract ecm var = do sc <- getSharedContext ce <- SV.getCryptolEnv - let ?fileReader = StrictBS.readFile - (tt, ce') <- io $ CSC.extractDefFromExtCryptolModule sc ce ecm var - SV.setCryptolEnv ce' + tt <- io $ CSC.extractDefFromExtCryptolModule sc ce ecm var return tt -- XXX: This is kind of a top-level style operation; should it be @@ -2251,25 +2286,22 @@ cryptol_extract ecm var = do -- probably a bad idea.) cryptol_add_path :: FilePath -> TopLevel () cryptol_add_path path = do - ce <- SV.getCryptolEnv - let me = CSC.eModuleEnv ce + sc <- getSharedContext + me <- io $ CSC.eModuleEnv sc let me' = me { C.meSearchPath = path : C.meSearchPath me } - let ce' = ce { CSC.eModuleEnv = me' } - SV.setCryptolEnv ce' + io $ CSC.setModuleEnv sc me' cryptol_add_prim :: Text -> Text -> TypedTerm -> TopLevel () cryptol_add_prim mnm nm trm = do - ce <- SV.getCryptolEnv + sc <- getSharedContext let prim_name = C.PrimIdent (C.textToModName mnm) nm - prims' = Map.insert prim_name (ttTerm trm) (CSC.ePrims ce) - SV.setCryptolEnv $ ce { CSC.ePrims = prims' } + io $ CSC.addPrims sc (Map.singleton prim_name (ttTerm trm)) cryptol_add_prim_type :: Text -> Text -> TypedTerm -> TopLevel () cryptol_add_prim_type mnm nm tp = do - ce <- SV.getCryptolEnv + sc <- getSharedContext let prim_name = C.PrimIdent (C.textToModName mnm) nm - prim_types' = Map.insert prim_name (ttTerm tp) (CSC.ePrimTypes ce) - SV.setCryptolEnv $ ce { CSC.ePrimTypes = prim_types' } + io $ CSC.addPrimTypes sc (Map.singleton prim_name (ttTerm tp)) parseSharpSATResult :: String -> Maybe Integer parseSharpSATResult s = parse (lines s) diff --git a/saw-central/src/SAWCentral/Crucible/Common/Setup/Type.hs b/saw-central/src/SAWCentral/Crucible/Common/Setup/Type.hs index 6ab02309d7..dafb83fd50 100644 --- a/saw-central/src/SAWCentral/Crucible/Common/Setup/Type.hs +++ b/saw-central/src/SAWCentral/Crucible/Common/Setup/Type.hs @@ -124,8 +124,8 @@ freshTypedVariable :: Text {- ^ variable name -} -> Cryptol.Type {- ^ variable type -} -> CrucibleSetupT arch m TypedVariable -freshTypedVariable sc env name cty = - do ty <- liftIO $ Cryptol.translateType sc env cty +freshTypedVariable sc _env name cty = + do ty <- liftIO $ Cryptol.translateType sc cty vn <- liftIO $ scFreshInventedVar sc name ty let tt = TypedVariable cty vn ty currentState . MS.csFreshVars %= cons tt diff --git a/saw-central/src/SAWCentral/Crucible/JVM/Override.hs b/saw-central/src/SAWCentral/Crucible/JVM/Override.hs index 259008d52d..648f97beed 100644 --- a/saw-central/src/SAWCentral/Crucible/JVM/Override.hs +++ b/saw-central/src/SAWCentral/Crucible/JVM/Override.hs @@ -689,8 +689,8 @@ learnPointsTo opts sc cc spec prepost pt = valueToSC sym md failMsg tval jval when (len > toInteger (maxBound :: Int)) $ fail "jvm_array_is: array length too long" - let cryenv = cc ^. jccCryptolEnv - ety_tm <- liftIO $ Cryptol.translateType sc cryenv ety + let _cryenv = cc ^. jccCryptolEnv + ety_tm <- liftIO $ Cryptol.translateType sc ety ts <- traverse load [0 .. fromInteger len - 1] realTerm <- liftIO $ scVector sc ety_tm ts matchTerm sc md prepost realTerm (ttTerm tt) @@ -873,12 +873,12 @@ doEntireArrayStore bak glob ref vs = foldM store glob (zip [0..] vs) -- along with a list of its projected components. Return 'Nothing' if -- the 'TypedTerm' does not have a vector type. destVecTypedTerm :: SharedContext -> Cryptol.CryptolEnv -> TypedTerm -> IO (Maybe (Cryptol.Type, [TypedTerm])) -destVecTypedTerm sc env (TypedTerm ttp t) = +destVecTypedTerm sc _env (TypedTerm ttp t) = case asVec of Nothing -> pure Nothing Just (len, ety) -> do len_tm <- scNat sc (fromInteger len) - ty_tm <- Cryptol.translateType sc env ety + ty_tm <- Cryptol.translateType sc ety idxs <- traverse (scNat sc) (map fromInteger [0 .. len-1]) ts <- traverse (scAt sc len_tm ty_tm t) idxs pure $ Just (ety, map (TypedTerm (TypedTermSchema (Cryptol.tMono ety))) ts) diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs b/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs index f82ce8b87c..fc9f745baa 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs @@ -72,7 +72,7 @@ import SAWCentral.LLVMBuiltins import SAWCentral.Panic import SAWCentral.Value import qualified CryptolSAWCore.Pretty as CryPP -import CryptolSAWCore.CryptolEnv +import CryptolSAWCore.GlobalCryptolEnv import SAWCore.Module (Def(..), ResolvedName(..), lookupVarIndexInMap) import SAWCore.Name (Name(..)) import SAWCore.OpenTerm (OpenTerm) @@ -143,9 +143,9 @@ llvm_ffi_setup TypedTerm { ttTerm = appTerm } = do let (funTerm, tyArgTerms) = asApplyAll appTerm sc <- lll getSharedContext let ?ctx = FFISetupCtx {..} - cryEnv <- lll getCryptolEnv + ffiTypes <- lio $ eFFITypes sc case asConstant funTerm of - Just nm -> case Map.lookup (nameInfo nm) (eFFITypes cryEnv) of + Just nm -> case Map.lookup (nameInfo nm) ffiTypes of Nothing -> do opts <- lll $ getPPOpts nm' <- lio $ ppName sc opts nm diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs index 9de519942d..4452aaa344 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs @@ -1056,9 +1056,8 @@ resolveSAWTerm cc tp tm = _ -> fail ("Invalid bitvector width: " ++ show sz) Cryptol.TVSeq sz tp' -> do let sc = sawCoreSharedContext (cc ^. ccSym) - let cryenv = cc ^. ccCryptolEnv sz_tm <- scNat sc (fromIntegral sz) - tp_tm <- translateType sc cryenv (Cryptol.tValTy tp') + tp_tm <- translateType sc (Cryptol.tValTy tp') let f i = do i_tm <- scNat sc (fromIntegral i) tm' <- scAt sc sz_tm tp_tm tm i_tm resolveSAWTerm cc tp' tm' @@ -1218,9 +1217,8 @@ memArrayToSawCoreTerm crucible_context endianess typed_term = do let data_layout = Crucible.llvmDataLayout $ ccTypeCtx crucible_context let sc = sawCoreSharedContext sym ppopts <- scGetPPOpts sc - let cryenv = crucible_context ^. ccCryptolEnv - byte_type_term <- translateType sc cryenv $ Cryptol.tValTy $ Cryptol.TVSeq 8 Cryptol.TVBit + byte_type_term <- translateType sc $ Cryptol.tValTy $ Cryptol.TVSeq 8 Cryptol.TVBit offset_type_term <- scBitvector sc $ natValue ?ptrWidth let updateArray :: Natural -> Term -> StateT Term IO () @@ -1239,7 +1237,6 @@ memArrayToSawCoreTerm crucible_context endianess typed_term = do then forM_ [0 .. (byte_count - 1)] $ \byte_index -> do bit_type_term <- liftIO $ translateType sc - cryenv (Cryptol.tValTy Cryptol.TVBit) byte_index_term <- liftIO $ scNat sc $ byte_index * 8 byte_size_term <- liftIO $ scNat sc 8 @@ -1272,7 +1269,6 @@ memArrayToSawCoreTerm crucible_context endianess typed_term = do size_term <- liftIO $ scNat sc $ fromInteger size elem_type_term <- liftIO $ translateType sc - cryenv (Cryptol.tValTy element_cryptol_type) index_term <- liftIO $ scNat sc $ fromInteger element_index inner_saw_term <- liftIO $ scAt diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs index 7c62a84f8e..5a26cf96d1 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs @@ -71,6 +71,7 @@ import Data.Parameterized.Nonce (GlobalNonceGenerator) import Data.Parameterized.Context hiding (view, zipWithM) import CryptolSAWCore.CryptolEnv +import CryptolSAWCore.GlobalCryptolEnv import SAWCore.FiniteValue import SAWCore.Module (Def(..), ResolvedName(..), lookupVarIndexInMap) import SAWCore.Name (Name(..), VarName(..)) @@ -265,8 +266,9 @@ cryptolUninterpreted :: SharedContext -> [Term] -> m UninterpResult -cryptolUninterpreted path func env nm sc xs = - case lookupIn nm $ eAllTerms env of +cryptolUninterpreted path func _env nm sc xs = do + allTerms <- liftIO $ eAllTerms sc + case lookupIn nm allTerms of Left _err -> throwX86func path func $ "Failed to look up Cryptol name \"" <> nm <> "\" in Cryptol environment" Right t -> UninterpOne <$> liftIO (scApplyAll sc t xs) diff --git a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs index c9a1eab087..0b0370616f 100644 --- a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs +++ b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs @@ -92,7 +92,6 @@ import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Reader (runReaderT) import Control.Monad.State (MonadState(..), StateT(..), execStateT, gets) import Control.Monad.Trans.Class (MonadTrans(..)) -import qualified Data.ByteString as BSS import qualified Data.ByteString.Lazy as BSL import Data.Char (chr) import Data.Foldable (for_, toList) @@ -1117,8 +1116,9 @@ mir_vec_of prefix elemTy contents = do -- Set up Cryptol environment sc <- mirTopLevel getSharedContext let transCry cryEnv e = do - let ?fileReader = BSS.readFile - CryEnv.pExprToTypedTerm sc cryEnv e + tt <- CryEnv.pExprToTypedTerm sc cryEnv e + return (tt,cryEnv) + cryEnv <- mirTopLevel getCryptolEnv let sizeBits = knownNat @Mir.SizeBits @@ -1142,7 +1142,7 @@ mir_vec_of prefix elemTy contents = do let capIdent = "cap" maxCap = maxSigned sizeBits `div` toInteger elemSize ((prop1, prop2), cryEnv') <- MIRSetupM $ liftIO $ - CryEnv.withExtraVar (capIdent, cap) cryEnv $ \cryEnv_1 -> do + CryEnv.withExtraVar sc (capIdent, cap) cryEnv $ \cryEnv_1 -> do -- cap <= isize::MAX / sizeof:: (prop1, cryEnv_2) <- transCry cryEnv_1 (C.var capIdent C.<= C.intLit maxCap) diff --git a/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs index 4be122833c..bc0dd0987b 100644 --- a/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs +++ b/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs @@ -1357,10 +1357,10 @@ indexSeqTerm :: {- ^ length and Cryptol element type of the sequence -} -> Term {- ^ term to index into -} -> IO (Int -> IO Term) -- ^ the indexing function -indexSeqTerm cryenv sym (sz, elemTp) tm = do +indexSeqTerm _cryenv sym (sz, elemTp) tm = do let sc = sawCoreSharedContext sym sz_tm <- scNat sc (fromInteger sz) - elemTp_tm <- translateType sc cryenv (Cryptol.tValTy elemTp) + elemTp_tm <- translateType sc (Cryptol.tValTy elemTp) pure $ \i -> do i_tm <- scNat sc (fromIntegral i) scAt sc sz_tm elemTp_tm tm i_tm diff --git a/saw-central/src/SAWCentral/JavaExpr.hs b/saw-central/src/SAWCentral/JavaExpr.hs index c2ef47a90c..f958d82c6d 100644 --- a/saw-central/src/SAWCentral/JavaExpr.hs +++ b/saw-central/src/SAWCentral/JavaExpr.hs @@ -265,11 +265,11 @@ javaTypeToActual tp | otherwise = Nothing narrowTypeOfActual :: SharedContext -> CryptolEnv -> JavaActualType -> IO (Maybe Term) -narrowTypeOfActual sc env at = +narrowTypeOfActual sc _env at = case cryptolTypeOfActual at of Nothing -> return Nothing Just cty -> - do t <- translateType sc env cty + do t <- translateType sc cty return (Just t) cryptolTypeOfActual :: JavaActualType -> Maybe Cryptol.Type diff --git a/saw-central/src/SAWCentral/Prover/Exporter.hs b/saw-central/src/SAWCentral/Prover/Exporter.hs index 2a6544cbee..df917cfa48 100644 --- a/saw-central/src/SAWCentral/Prover/Exporter.hs +++ b/saw-central/src/SAWCentral/Prover/Exporter.hs @@ -52,7 +52,6 @@ import Control.Monad (unless) import Control.Monad.Except (runExceptT) import Control.Monad.State (gets, liftIO) import qualified Data.AIG as AIG -import qualified Data.ByteString as BS import Data.Maybe (mapMaybe) import Data.Parameterized.Nonce (globalNonceGenerator) import Data.Parameterized.Some (Some(..)) @@ -79,7 +78,6 @@ import SAWCore.Recognizer (asPi) import SAWCore.SATQuery import SAWCore.SharedTerm as SC -import CryptolSAWCore.Cryptol (refreshCryptolEnv) import CryptolSAWCore.CryptolEnv (initCryptolEnv, loadCryptolModule) import CryptolSAWCore.Prelude (cryptolModule, scLoadPreludeModule, scLoadCryptolModule) import CryptolSAWCore.TypedTerm @@ -508,13 +506,12 @@ writeRocqCryptolModule inputFile outputFile notations skips = io $ do sc <- mkSharedContext () <- scLoadPreludeModule sc () <- scLoadCryptolModule sc - let ?fileReader = BS.readFile env <- initCryptolEnv sc cryptolPrimitivesForSAWCoreModule <- scFindModule sc nameOfCryptolPrimitivesForSAWCoreModule - (cm, _) <- loadCryptolModule sc env inputFile + cm <- loadCryptolModule sc inputFile -- NOTE: implementation of loadCryptolModule, now uses this default: -- defaultPrimitiveOptions = ImportPrimitiveOptions{allowUnknownPrimitives=True} - import_env <- refreshCryptolEnv env + let import_env = env mm <- scGetModuleMap sc let ?mm = mm let cryptolPreludeDecls = diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs index d6db82fe81..4574c8be2b 100644 --- a/saw-central/src/SAWCentral/Value.hs +++ b/saw-central/src/SAWCentral/Value.hs @@ -55,26 +55,16 @@ module SAWCentral.Value ( pushScope, popScope, -- used by SAWCentral.Builtins, SAWScript.ValueOps, SAWScript.Interpreter, -- SAWServer.SAWServer - CryptolEnvStack(..), - -- used by SAWCentral.Crucible.LLVM.FFI, SAWCentral.Crucible.LLVM.X86, - -- SAWCentral.Crucible.MIR.Builtins, SAWCentral.Builtins, - -- SAWScript.Interpreter, SAWScript.REPL.Monad getCryptolEnv, -- used by SAWCentral.Builtins - getCryptolEnvStack, - -- used by SAWCentral.Builtins, SAWScript.Interpreter, SAWScript.REPL.Monad setCryptolEnv, -- used by SAWScript.REPL.Monad, SAWServer.Eval, -- SAWServer.ProofScript, SAWServer.CryptolSetup, SAWServer.CryptolExpression, -- SAWServer.LLVMVerify, SAWServer.JVMVerify, SAWServer.MIRVerify, SAWServer.Yosys, rwGetCryptolEnv, -- used by SAWScript.ValueOps - rwGetCryptolEnvStack, - -- used by SAWServer.CryptolSetup rwSetCryptolEnv, -- used by SAWScript.ValueOps - rwSetCryptolEnvStack, - -- used by SAWScript.REPL.Monad, SAWServer.SAWServer, SAWServer.Yosys rwModifyCryptolEnv, -- used by SAWScript.Interpreter, and implicitly by SAWScript.REPL and Main TopLevelShellHook, ProofScriptShellHook, @@ -279,7 +269,8 @@ import SAWCentral.Yosys.Theorem (YosysTheorem) import SAWCentral.Yosys.State (YosysSequential) import SAWCore.Name (VarName(..)) -import CryptolSAWCore.CryptolEnv as CEnv +import qualified CryptolSAWCore.CryptolEnv as CEnv +import qualified CryptolSAWCore.GlobalCryptolEnv as CEnv import SAWCore.FiniteValue (FirstOrderValue, prettyFirstOrderValue) import SAWCore.Rewriter (Simpset, lhsRewriteRule, rhsRewriteRule, ctxtRewriteRule, listRules) import SAWCore.SharedTerm @@ -866,12 +857,6 @@ type VarEnv = ScopedMap SS.Name (SS.Pos, SS.PrimitiveLifecycle, -- builtin types that aren't special cases in the AST appear) type TyEnv = ScopedMap SS.Name (SS.PrimitiveLifecycle, SS.NamedType) --- | The full Cryptol environment. We maintain a stack of plain --- Cryptol environments and push/pop them as we enter and leave --- scopes; otherwise the Cryptol environment doesn't track SAWScript --- scopes and horribly confusing wrong things happen. -data CryptolEnvStack = CryptolEnvStack CEnv.CryptolEnv [CEnv.CryptolEnv] - -- | Type for the ordinary interpreter environment. -- -- There's one environment that maps variable names to values, and @@ -885,7 +870,7 @@ data CryptolEnvStack = CryptolEnvStack CEnv.CryptolEnv [CEnv.CryptolEnv] data Environ = Environ { eVarEnv :: VarEnv, eTyEnv :: TyEnv, - eCryptol :: CryptolEnvStack + eCryptolEnv :: CEnv.CryptolEnv } -- | The extra environment for rebindable globals. @@ -898,35 +883,30 @@ type RebindableEnv = Map SS.Name (SS.Pos, SS.Schema, Value) -- | Enter a scope. pushScope :: TopLevel () pushScope = do - Environ varenv tyenv cryenv <- gets rwEnviron + Environ varenv tyenv cenv <- gets rwEnviron let varenv' = ScopedMap.push varenv tyenv' = ScopedMap.push tyenv - cryenv' = cryptolPush cryenv - modifyTopLevelRW (\rw -> rw { rwEnviron = Environ varenv' tyenv' cryenv' }) + cenv' = CEnv.pushScope cenv + modifyTopLevelRW $ \rw -> rw + { rwEnviron = Environ varenv' tyenv' cenv' } -- | Leave a scope. This will panic if you try to leave the last scope; -- pushes and pops should be matched. popScope :: TopLevel () popScope = do - Environ varenv tyenv cryenv <- gets rwEnviron + Environ varenv tyenv cenv <- gets rwEnviron let varenv' = ScopedMap.pop varenv tyenv' = ScopedMap.pop tyenv - cryenv' = cryptolPop cryenv - modifyTopLevelRW (\rw -> rw { rwEnviron = Environ varenv' tyenv' cryenv' }) + cenv' = CEnv.popScope cenv + modifyTopLevelRW $ \rw -> rw + { rwEnviron = Environ varenv' tyenv' cenv' } -- | Get the current Cryptol environment. getCryptolEnv :: TopLevel CEnv.CryptolEnv getCryptolEnv = do - Environ _varenv _tyenv cryenvs <- gets rwEnviron - let CryptolEnvStack ce _ = cryenvs - return ce - --- | Get the current full stack of Cryptol environments. -getCryptolEnvStack :: TopLevel CryptolEnvStack -getCryptolEnvStack = do - Environ _varenv _tyenv cryenvs <- gets rwEnviron - return cryenvs + Environ _varenv _tyenv cenv <- gets rwEnviron + return cenv -- | Update the current Cryptol environment. -- @@ -934,10 +914,10 @@ getCryptolEnvStack = do -- value applied has not become stale. setCryptolEnv :: CEnv.CryptolEnv -> TopLevel () setCryptolEnv ce = do - Environ varenv tyenv cryenvs <- gets rwEnviron - let CryptolEnvStack _ ces = cryenvs - let cryenvs' = CryptolEnvStack ce ces - modify (\rw -> rw { rwEnviron = Environ varenv tyenv cryenvs' }) + Environ varenv tyenv _ <- gets rwEnviron + modify $ \rw -> rw + { rwEnviron = Environ varenv tyenv ce + } -- | Get the current Cryptol environment from a TopLevelRW. -- @@ -948,18 +928,8 @@ setCryptolEnv ce = do -- all. rwGetCryptolEnv :: TopLevelRW -> CEnv.CryptolEnv rwGetCryptolEnv rw = - let Environ _varenv _tyenv cryenvs = rwEnviron rw - CryptolEnvStack ce _ = cryenvs - in - ce - --- | Get the current full stack of Cryptol environments from a --- TopLevelRW. Used by the checkpointing logic, in a fairly dubious --- way. (XXX) -rwGetCryptolEnvStack :: TopLevelRW -> CryptolEnvStack -rwGetCryptolEnvStack rw = - let Environ _varenv _tyenv cryenvs = rwEnviron rw in - cryenvs + let Environ _varenv _tyenv cenv = rwEnviron rw + in cenv -- | Update the current Cryptol environment in a TopLevelRW. -- @@ -974,23 +944,9 @@ rwGetCryptolEnvStack rw = -- all. rwSetCryptolEnv :: CEnv.CryptolEnv -> TopLevelRW -> TopLevelRW rwSetCryptolEnv ce rw = - let Environ varenv tyenv cryenvs = rwEnviron rw - CryptolEnvStack _ ces = cryenvs - cryenvs' = CryptolEnvStack ce ces - in - rw { rwEnviron = Environ varenv tyenv cryenvs' } - --- | Update the current full stack of Cryptol environments in a --- TopLevelRW. Used by the checkpointing logic, in a fairly --- dubious way. (XXX) --- --- Overwrites the previous stack; caller must ensure they haven't --- done anything to make the value they're working with stale. -rwSetCryptolEnvStack :: CryptolEnvStack -> TopLevelRW -> TopLevelRW -rwSetCryptolEnvStack cryenvs rw = - let Environ varenv tyenv _ = rwEnviron rw in - rw { rwEnviron = Environ varenv tyenv cryenvs } - + let Environ varenv tyenv _ = rwEnviron rw + in rw { rwEnviron = Environ varenv tyenv ce } + -- | Modify the current Cryptol environment in a TopLevelRW. -- -- (Accessor method for use in SAWServer and SAWScript.REPL, which @@ -1000,26 +956,9 @@ rwSetCryptolEnvStack cryenvs rw = -- all. rwModifyCryptolEnv :: (CEnv.CryptolEnv -> CEnv.CryptolEnv) -> TopLevelRW -> TopLevelRW rwModifyCryptolEnv f rw = - let Environ varenv tyenv cryenvs = rwEnviron rw - CryptolEnvStack ce ces = cryenvs - ce' = f ce - cryenvs' = CryptolEnvStack ce' ces - in - rw { rwEnviron = Environ varenv tyenv cryenvs' } - --- | Push a new scope on the Cryptol environment stack. -cryptolPush :: CryptolEnvStack -> CryptolEnvStack -cryptolPush (CryptolEnvStack ce ces) = - -- Each entry is the whole environment, so duplicate the top entry - CryptolEnvStack ce (ce : ces) - --- | Pop the current scope off the Cryptol environment stack. -cryptolPop :: CryptolEnvStack -> CryptolEnvStack -cryptolPop (CryptolEnvStack _ ces) = - -- Discard the top - case ces of - [] -> panic "cryptolPop" ["Cryptol environment scope stack ran out"] - ce : ces' -> CryptolEnvStack ce ces' + let Environ varenv tyenv cenv = rwEnviron rw + in rw { rwEnviron = Environ varenv tyenv (f cenv) } + -- | Type for the function to start a new REPL in TopLevel. -- @@ -1428,7 +1367,7 @@ extendEnv pos name rb ty doc v = do modname = T.packModName [name] -- Update the SAWScript environment. - Environ varenv tyenv cryenvs <- gets rwEnviron + Environ varenv tyenv _ <- gets rwEnviron rbenv <- gets rwRebindables let (varenv', rbenv') = case rb of SS.ReadOnlyVar -> @@ -1447,30 +1386,29 @@ extendEnv pos name rb ty doc v = do (varenv, re') -- Mirror the value into the Cryptol environment if appropriate. - let CryptolEnvStack ce ces = cryenvs + ce <- getCryptolEnv ce' <- - case v of + io $ case v of VTerm t -> - pure $ CEnv.bindExtraVar (ident, t) ce + CEnv.bindExtraVar sc (ident, t) ce VType s -> - pure $ CEnv.bindTySyn (ident, s) ce + CEnv.bindTySyn sc (ident, s) ce VInteger n -> - pure $ CEnv.bindIntegerType (ident, n) ce + CEnv.bindIntegerType sc (ident, n) ce VCryptolModule m -> - pure $ CEnv.bindExtCryptolModule (modname, m) ce + CEnv.bindExtCryptolModule sc (modname, m) ce VString s -> - do tt <- io $ typedTermOfString sc (Text.unpack s) - pure $ CEnv.bindExtraVar (ident, tt) ce + do tt <- typedTermOfString sc (Text.unpack s) + CEnv.bindExtraVar sc (ident, tt) ce VBool b -> - do tt <- io $ typedTermOfBool sc b - pure $ CEnv.bindExtraVar (ident, tt) ce + do tt <- typedTermOfBool sc b + CEnv.bindExtraVar sc (ident, tt) ce _ -> pure ce - let cryenvs' = CryptolEnvStack ce' ces -- Drop the new bits into place. modify (\rw -> rw { - rwEnviron = Environ varenv' tyenv cryenvs', + rwEnviron = Environ varenv' tyenv ce', rwRebindables = rbenv' }) diff --git a/saw-central/src/SAWCentral/Yosys/Theorem.hs b/saw-central/src/SAWCentral/Yosys/Theorem.hs index 11e28f5614..36fd73c8c8 100644 --- a/saw-central/src/SAWCentral/Yosys/Theorem.hs +++ b/saw-central/src/SAWCentral/Yosys/Theorem.hs @@ -98,7 +98,7 @@ buildTheorem :: Maybe SC.TypedTerm -> SC.TypedTerm -> IO YosysTheorem -buildTheorem sc env ymod newmod precond body = do +buildTheorem sc _env ymod newmod precond body = do cty <- case SC.ttType ymod of SC.TypedTermSchema (C.Forall [] [] cty) -> pure cty @@ -107,8 +107,8 @@ buildTheorem sc env ymod newmod precond body = do case cty of C.TCon (C.TC C.TCFun) [ci, co] -> pure (ci, co) _ -> yosysError YosysErrorInvalidOverrideTarget - inpTy <- CSC.translateType sc env cinpTy - outTy <- CSC.translateType sc env coutTy + inpTy <- CSC.translateType sc cinpTy + outTy <- CSC.translateType sc coutTy nmi <- case reduceSelectors (SC.ttTerm ymod) of (R.asConstant -> Just (SC.Name _ nmi)) -> pure nmi diff --git a/saw-core-rocq/src/SAWCoreRocq/CryptolModule.hs b/saw-core-rocq/src/SAWCoreRocq/CryptolModule.hs index f15d1ddb9b..229dd83967 100644 --- a/saw-core-rocq/src/SAWCoreRocq/CryptolModule.hs +++ b/saw-core-rocq/src/SAWCoreRocq/CryptolModule.hs @@ -46,10 +46,10 @@ translateCryptolModule :: [Rocq.Ident] -> CryptolModule -> IO (Either TranslationError [Rocq.Decl]) -translateCryptolModule sc env configuration globalDecls (CryptolModule _ tm) = +translateCryptolModule sc _env configuration globalDecls (CryptolModule _ tm) = do defs <- forM (Map.assocs tm) $ \(nm, t) -> - do tp <- ttTypeAsTerm sc env t + do tp <- ttTypeAsTerm sc t return (nm, ttTerm t, tp) mm <- scGetModuleMap sc return diff --git a/saw-core/src/SAWCore/SharedTerm.hs b/saw-core/src/SAWCore/SharedTerm.hs index 3515c3a94c..128b3a8462 100644 --- a/saw-core/src/SAWCore/SharedTerm.hs +++ b/saw-core/src/SAWCore/SharedTerm.hs @@ -76,6 +76,7 @@ module SAWCore.SharedTerm , IsMetadata(..) , scGetData , scUpdateData + , scWithData -- * Term builders , scTermF , scFlatTermF @@ -2388,11 +2389,4 @@ scTreeSizeAux = go case Map.lookup (termIndex t) seen of Just sz' -> (sz + sz', seen) Nothing -> (sz + sz', Map.insert (termIndex t) sz' seen') - where (sz', seen') = foldl' go (1, seen) (unwrapTermF t) - -scUpdateData :: - IsMetadata a => SharedContext -> (a -> a) -> IO () -scUpdateData sc f = execSCM sc (scmUpdateData f) - -scGetData :: IsMetadata a => SharedContext -> IO a -scGetData sc = execSCM sc scmGetData \ No newline at end of file + where (sz', seen') = foldl' go (1, seen) (unwrapTermF t) \ No newline at end of file diff --git a/saw-core/src/SAWCore/Term/Certified.hs b/saw-core/src/SAWCore/Term/Certified.hs index 2621dd3bac..cbe41c64bd 100644 --- a/saw-core/src/SAWCore/Term/Certified.hs +++ b/saw-core/src/SAWCore/Term/Certified.hs @@ -36,7 +36,10 @@ module SAWCore.Term.Certified -- * Term metadata , IsMetadata(..) , scmGetData + , scGetData , scmUpdateData + , scUpdateData + , scWithData -- * Term building monad , TermError(..) , SCM @@ -452,8 +455,10 @@ restoreMetadataStore sc chk = do -- contents and return the original ref reinit_now :: Metadata IORef a -> IO (Maybe (Metadata IORef a)) reinit_now m@(Metadata ref) = do + a_now <- readIORef ref a_init <- initMetadata - writeIORef ref a_init + a_restored <- restoreMetadata a_init a_now + writeIORef ref a_restored return $ Just m restoreSharedContext :: SharedContextCheckpoint -> SharedContext -> IO () @@ -626,20 +631,55 @@ scmVariable x t = scmUpdateData :: IsMetadata a => (a -> a) -> SCM () scmUpdateData f = do sc <- scmSharedContext - ts <- liftIO $ readIORef (scMetadata sc) - liftIO $ case TypedStore.lookup ts of + liftIO $ scUpdateData sc f + +scUpdateData :: + IsMetadata a => + SharedContext -> + (a -> a) -> + IO () +scUpdateData sc f = do + ts <- readIORef (scMetadata sc) + case TypedStore.lookup ts of Just (Metadata ref) -> modifyIORef' ref f Nothing -> do a <- initMetadata ref <- Metadata <$> newIORef (f a) modifyIORef' (scMetadata sc) (TypedStore.insert ref) + +-- | Modify the global metadata for type 'a', +-- run the given action, and then restore the +-- metadata to the previous state (using 'restoreMetadata') +-- before returning. +scWithData :: + (MonadIO m, IsMetadata a) => + SharedContext -> + (a -> a) -> + m b -> + m b +scWithData sc f m = do + a <- liftIO $ do + a <- scGetData sc + scUpdateData sc (\_ -> f a) + return a + b <- m + liftIO $ do + a' <- scGetData sc + a'' <- restoreMetadata a a' + scUpdateData sc (\_ -> a'') + return b + -- | Return the global metadata of type 'a'. scmGetData :: IsMetadata a => SCM a scmGetData = do sc <- scmSharedContext - ts <- liftIO $ readIORef (scMetadata sc) - liftIO $ case TypedStore.lookup ts of + liftIO $ scGetData sc + +scGetData :: IsMetadata a => SharedContext -> IO a +scGetData sc = do + ts <- readIORef (scMetadata sc) + case TypedStore.lookup ts of Just (Metadata ref) -> readIORef ref Nothing -> do a <- initMetadata @@ -647,6 +687,7 @@ scmGetData = do modifyIORef' (scMetadata sc) (TypedStore.insert ref) return a + -- | Check whether the given 'VarName' occurs free in the type of -- another variable in the context of the given 'Term', and fail if it -- does. diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index 06d48535a6..94cba954e0 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -104,6 +104,7 @@ import SAWCore.Prim (rethrowEvalError) import SAWCore.Rewriter (emptySimpset) import SAWCore.SharedTerm import qualified CryptolSAWCore.CryptolEnv as CEnv +import qualified CryptolSAWCore.GlobalCryptolEnv as CEnv import qualified CryptolSAWCore.Prelude as CryptolSAW @@ -547,7 +548,6 @@ applyValue pos v1info v1 v2 = -- interpretExpr :: SS.Expr -> TopLevel Value interpretExpr expr = - let ?fileReader = BS.readFile in case expr of SS.Bool _ b -> return $ VBool b @@ -561,14 +561,13 @@ interpretExpr expr = --io $ putStrLn $ "Parsing code: " ++ show str --showCryptolEnv' cenv let str' = toInputText pos str - (t, cenv') <- io $ CEnv.parseTypedTerm sc cenv str' - setCryptolEnv cenv' + t <- io $ CEnv.parseTypedTerm sc cenv str' return (VTerm t) SS.CType pos str -> do + sc <- getSharedContext cenv <- getCryptolEnv let str' = toInputText pos str - (s, cenv') <- io $ CEnv.parseSchema cenv str' - setCryptolEnv cenv' + s <- io $ CEnv.parseSchema sc cenv str' return (VType s) SS.Array _pos es -> VArray <$> traverse interpretExpr es @@ -843,7 +842,6 @@ interpretMonadAction fromHow v = case v of -- interpretDoStmt :: forall m. InterpreterMonad m => SS.Stmt -> m () interpretDoStmt stmt = - let ?fileReader = BS.readFile in -- XXX are the uses of push/popPosition here suitable? not super clear case stmt of SS.StmtBind pos pat e -> do @@ -1015,8 +1013,6 @@ interpretTopStmt :: InterpreterMonad m => SS.Stmt -> m () interpretTopStmt printBinds replTypingHacks stmt = do - let ?fileReader = BS.readFile - avail <- liftTopLevel $ gets rwPrimsAvail ctx <- getMonadContext @@ -1263,7 +1259,6 @@ buildTopLevelEnv opts scriptArgv tlhook pshook = do let proxy = AIGProxy AIG.compactProxy let mn = mkModuleName ["SAWScript"] sc <- mkSharedContext - let ?fileReader = BS.readFile CryptolSAW.scLoadPreludeModule sc CryptolSAW.scLoadCryptolModule sc scLoadModule sc (emptyModule mn) @@ -1288,12 +1283,11 @@ buildTopLevelEnv opts scriptArgv tlhook pshook = do , biBasicSS = ss } ce0 <- CEnv.initCryptolEnv sc - let cryenv0 = CryptolEnvStack ce0 [] jvmTrans <- CJ.mkInitialJVMContext halloc let rw0 = TopLevelRW - { rwEnviron = primEnviron opts bic cryenv0 + { rwEnviron = primEnviron opts bic ce0 , rwRebindables = Map.empty , rwPosition = SS.Unknown , rwStackTrace = Trace.empty @@ -2342,7 +2336,7 @@ print_value (VString s) = printOutLnTop Info (Text.unpack s) print_value (VTerm t) = do sc <- getSharedContext cenv <- getCryptolEnv - let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv) + cfg <- CEnv.meSolverConfig <$> (io $ CEnv.eModuleEnv sc) unless (closedTerm (ttTerm t)) $ fail "term contains symbolic variables" sawopts <- getOptions @@ -3589,6 +3583,14 @@ primitives = Map.fromList $ Current [ "Pretty-print the given term in SAWCore syntax." ] + , prim "show_cryptol_term" "Term -> String" + (funVal1 show_cryptol_term) + Experimental + [ "Pretty-print the given term in Cryptol syntax, yielding a" + , "String. Fails if the term cannot be represented as" + , "a Cryptol expression." + ] + , prim "print_term_depth" "Int -> Term -> TopLevel ()" (pureVal print_term_depth) Current @@ -7729,8 +7731,8 @@ primValueEnv opts bic = Map.mapWithKey extract primitives (pos, primitiveLife p, primitiveType p, (primitiveFn p) opts bic, Just $ doc n p) -primEnviron :: Options -> BuiltinContext -> CryptolEnvStack -> Environ -primEnviron opts bic cryenvs = +primEnviron :: Options -> BuiltinContext -> CEnv.CryptolEnv -> Environ +primEnviron opts bic env = -- Do a scope push so the builtins live by themselves in their own -- scope layer. This has the result of separating them from the @@ -7741,5 +7743,5 @@ primEnviron opts bic cryenvs = let tyenv = ScopedMap.push primNamedTypeEnv varenv = ScopedMap.push $ ScopedMap.seed $ primValueEnv opts bic in - Environ varenv tyenv cryenvs + Environ varenv tyenv env diff --git a/saw-script/src/SAWScript/REPL/Data.hs b/saw-script/src/SAWScript/REPL/Data.hs index 3a11c8ae44..04a67e0858 100644 --- a/saw-script/src/SAWScript/REPL/Data.hs +++ b/saw-script/src/SAWScript/REPL/Data.hs @@ -44,19 +44,24 @@ import qualified SAWCentral.AST as AST import SAWCentral.Value (TopLevelRW(..), Environ(..)) import SAWScript.REPL.Monad +import Control.Monad.IO.Class (liftIO) -- | Get visible Cryptol variable names. getCryptolExprNames :: REPL [Text] getCryptolExprNames = - do fNames <- fmap getNamingEnv getCryptolEnv + do sc <- rwSharedContext <$> getTopLevelRW + cenv <- getCryptolEnv + fNames <- liftIO $ getNamingEnv sc cenv let keys = Map.keys (MN.namespaceMap NSValue fNames) return (map CryPP.pp keys) -- | Get visible Cryptol type names. getCryptolTypeNames :: REPL [Text] -getCryptolTypeNames = - do fNames <- fmap getNamingEnv getCryptolEnv +getCryptolTypeNames = + do sc <- rwSharedContext <$> getTopLevelRW + cenv <- getCryptolEnv + fNames <- liftIO $ getNamingEnv sc cenv let keys = Map.keys (MN.namespaceMap NSType fNames) return (map CryPP.pp keys) diff --git a/saw-script/src/SAWScript/ValueOps.hs b/saw-script/src/SAWScript/ValueOps.hs index 1fb666f0b7..e9b5521e75 100644 --- a/saw-script/src/SAWScript/ValueOps.hs +++ b/saw-script/src/SAWScript/ValueOps.hs @@ -59,8 +59,6 @@ import qualified Data.Map as Map import SAWSupport.Position import SAWCore.SharedTerm -import CryptolSAWCore.CryptolEnv as CEnv - import qualified SAWCentral.Position as SS --import qualified SAWCentral.AST as SS --import qualified SAWCentral.Crucible.JVM.MethodSpecIR () @@ -155,23 +153,6 @@ makeCheckpoint = do scc <- liftIO $ checkpointSharedContext (rwSharedContext rw) return $ TopLevelCheckpoint rw scc --- | Restore the Cryptol environment stack (full Cryptol environment) --- from a checkpoint. --- --- Caution: the stack merge may have unexpected results if the number --- of scopes doesn't match, e.g. by using a checkpoint to teleport out --- of (or into) a nested block. But, it doesn't make sense to do that --- in the first place. Caveat emptor... --- -restoreCryptolEnvStack :: CryptolEnvStack -> CryptolEnvStack -> CryptolEnvStack -restoreCryptolEnvStack chk'cryenv now'cryenv = - let CryptolEnvStack chk'cenv chk'cenvs = chk'cryenv - CryptolEnvStack now'cenv now'cenvs = now'cryenv - result'cenv = CEnv.restoreCryptolEnv chk'cenv now'cenv - result'cenvs = zipWith CEnv.restoreCryptolEnv chk'cenvs now'cenvs - in - CryptolEnvStack result'cenv result'cenvs - -- | Restore a SAWScript checkpoint. restoreCheckpoint :: TopLevelCheckpoint -> TopLevel () restoreCheckpoint (TopLevelCheckpoint chk'rw scc) = do @@ -182,16 +163,7 @@ restoreCheckpoint (TopLevelCheckpoint chk'rw scc) = do -- which reference to it we use.) let sc = rwSharedContext now'rw liftIO $ restoreSharedContext scc sc - - -- Second, attend to the Cryptol environment so the Cryptol name - -- supply gets handled properly. - let chk'cryenv = rwGetCryptolEnvStack chk'rw - now'cryenv = rwGetCryptolEnvStack now'rw - result'cryenv = restoreCryptolEnvStack chk'cryenv now'cryenv - - -- Restore the old TopLevelRW with the adjusted Cryptol environment - let chk'rw' = rwSetCryptolEnvStack result'cryenv chk'rw - putTopLevelRW chk'rw' + putTopLevelRW chk'rw -- | User-facing checkpoint command. Returns an action in TopLevel -- that, if invoked, rolls back the state. diff --git a/saw-server/src/SAWServer/CryptolExpression.hs b/saw-server/src/SAWServer/CryptolExpression.hs index f78b84936e..19735c9330 100644 --- a/saw-server/src/SAWServer/CryptolExpression.hs +++ b/saw-server/src/SAWServer/CryptolExpression.hs @@ -35,8 +35,8 @@ import SAWCentral.Value (biSharedContext, rwGetCryptolEnv) import CryptolSAWCore.Cryptol ( getAllIfaceDecls, translateExpr, - CryptolEnv(eExtraVars, eExtraTySyns, eModuleEnv) ) -import CryptolSAWCore.CryptolEnv (getNamingEnv, meSolverConfig) + CryptolEnv, eExtraVars, eExtraTySyns, eModuleEnv, setModuleEnv ) +import CryptolSAWCore.CryptolEnv (getNamingEnv, meSolverConfig, withFileReader) import SAWCore.SharedTerm (SharedContext) import CryptolSAWCore.TypedTerm(TypedTerm(..),TypedTermType(..)) @@ -59,9 +59,8 @@ getTypedTerm inputExpr = do getTypedTermOfCExp :: (FilePath -> IO B.ByteString) -> SharedContext -> CryptolEnv -> Expr PName -> IO (ModuleRes TypedTerm) -getTypedTermOfCExp fileReader sc cenv expr = - do let ?fileReader = fileReader - let env = eModuleEnv cenv +getTypedTermOfCExp fileReader sc cenv expr = withFileReader sc fileReader $ + do env <- eModuleEnv sc let minp solver = ModuleInput { minpCallStacks = True, minpSaveRenamed = False, @@ -70,13 +69,15 @@ getTypedTermOfCExp fileReader sc cenv expr = minpModuleEnv = env, minpTCSolver = solver } + extraTySyns <- eExtraTySyns sc + extraVars <- eExtraVars sc + nameEnv <- getNamingEnv sc cenv mres <- withSolver (return ()) (meSolverConfig env) $ \solver -> runModuleM (minp solver) $ do npe <- interactive (noPat expr) -- eliminate patterns -- resolve names - let nameEnv = getNamingEnv cenv re <- interactive (rename interactiveName nameEnv (MR.rename npe)) -- infer types @@ -84,16 +85,16 @@ getTypedTermOfCExp fileReader sc cenv expr = let range = fromMaybe emptyRange (getLoc re) prims <- getPrimMap tcEnv <- genInferInput range prims NoParams ifDecls - let tcEnv' = tcEnv { inpVars = Map.union (eExtraVars cenv) (inpVars tcEnv) - , inpTSyns = Map.union (eExtraTySyns cenv) (inpTSyns tcEnv) + let tcEnv' = tcEnv { inpVars = Map.union extraVars (inpVars tcEnv) + , inpTSyns = Map.union extraTySyns (inpTSyns tcEnv) } out <- liftIO (tcExpr re tcEnv') interactive (runInferOutput out) case mres of (Right ((checkedExpr, schema), modEnv'), ws) -> - do let env' = cenv { eModuleEnv = modEnv' } - trm <- liftIO $ translateExpr sc env' checkedExpr + do liftIO $ setModuleEnv sc modEnv' + trm <- liftIO $ translateExpr sc checkedExpr return (Right (TypedTerm (TypedTermSchema schema) trm, modEnv'), ws) (Left err, ws) -> return (Left err, ws) diff --git a/saw-server/src/SAWServer/CryptolSetup.hs b/saw-server/src/SAWServer/CryptolSetup.hs index 076f70440b..cee5c821d7 100644 --- a/saw-server/src/SAWServer/CryptolSetup.hs +++ b/saw-server/src/SAWServer/CryptolSetup.hs @@ -41,8 +41,8 @@ cryptolLoadModule (CryptolLoadModuleParams modName) = let qual = Nothing -- TODO add field to params let importSpec = Nothing -- TODO add field to params fileReader <- Argo.getFileReader - let ?fileReader = fileReader - cenv' <- liftIO $ try $ CEnv.importCryptolModule sc cenv (Right modName) qual False CEnv.PublicAndPrivate importSpec + cenv' <- liftIO $ try $ CEnv.withFileReader sc fileReader $ + CEnv.importCryptolModule sc cenv (Right modName) qual False CEnv.PublicAndPrivate importSpec case cenv' of Left (ex :: SomeException) -> Argo.raise $ cryptolError (show ex) Right cenv'' -> @@ -77,8 +77,8 @@ cryptolLoadFile (CryptolLoadFileParams fileName) = let qual = Nothing -- TODO add field to params let importSpec = Nothing -- TODO add field to params fileReader <- Argo.getFileReader - let ?fileReader = fileReader - cenv' <- liftIO $ try $ CEnv.importCryptolModule sc cenv (Left fileName) qual False CEnv.PublicAndPrivate importSpec + cenv' <- liftIO $ try $ CEnv.withFileReader sc fileReader $ + CEnv.importCryptolModule sc cenv (Left fileName) qual False CEnv.PublicAndPrivate importSpec case cenv' of Left (ex :: SomeException) -> Argo.raise $ cryptolError (show ex) Right cenv'' -> diff --git a/saw-server/src/SAWServer/JVMCrucibleSetup.hs b/saw-server/src/SAWServer/JVMCrucibleSetup.hs index 529c83b8f5..78cde68f6a 100644 --- a/saw-server/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-server/src/SAWServer/JVMCrucibleSetup.hs @@ -21,6 +21,7 @@ import Control.Monad (unless) import Control.Monad.IO.Class ( MonadIO(liftIO) ) import Data.Aeson (FromJSON(..), withObject, (.:)) import Data.ByteString (ByteString) +import Data.Foldable (foldrM) import Data.Text (Text) --import qualified Data.Text as Text import Data.Map (Map) @@ -122,7 +123,8 @@ compileJVMContract fileReader bic ghostEnv cenv0 c = return (n, t) setupState allocs (env, cenv) vars = do freshTerms <- mapM setupFresh vars - let cenv' = foldr (\(ServerName n, t) -> CEnv.bindExtraVar (mkIdent n, t)) cenv freshTerms + let sc = biSharedContext bic + cenv' <- JVMSetupM $ liftIO $ foldrM (\(ServerName n, t) -> CEnv.bindExtraVar sc (mkIdent n, t)) cenv freshTerms let env' = Map.union env $ Map.fromList $ [ (n, Val (MS.SetupTerm t)) | (n, t) <- freshTerms ] ++ [ (n, Val v) | (n, v) <- allocs ] diff --git a/saw-server/src/SAWServer/LLVMCrucibleSetup.hs b/saw-server/src/SAWServer/LLVMCrucibleSetup.hs index e010b653bb..079f80ab07 100644 --- a/saw-server/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-server/src/SAWServer/LLVMCrucibleSetup.hs @@ -25,6 +25,7 @@ import Control.Monad (unless) import Control.Monad.IO.Class import Data.Aeson (FromJSON(..), withObject, (.:)) import Data.ByteString (ByteString) +import Data.Foldable (foldrM) import Data.Map (Map) import qualified Data.Map as Map @@ -119,7 +120,8 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c = setupState allocs (env, cenv) vars = do freshTerms <- mapM setupFresh vars - let cenv' = foldr (\(ServerName n, t) -> CEnv.bindExtraVar (mkIdent n, t)) cenv freshTerms + let sc = biSharedContext bic + cenv' <- LLVMCrucibleSetupM $ liftIO $ foldrM (\(ServerName n, t) -> CEnv.bindExtraVar sc (mkIdent n, t)) cenv freshTerms let env' = Map.union env $ Map.fromList $ [ (n, Val (CMS.anySetupTerm t)) | (n, t) <- freshTerms ] ++ [ (n, Val v) | (n, v) <- allocs ] diff --git a/saw-server/src/SAWServer/MIRCrucibleSetup.hs b/saw-server/src/SAWServer/MIRCrucibleSetup.hs index 689f4bf901..c417f7cdd4 100644 --- a/saw-server/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-server/src/SAWServer/MIRCrucibleSetup.hs @@ -17,6 +17,7 @@ import Control.Monad.State ( MonadState(..) ) import Control.Monad.Trans ( MonadTrans(lift) ) import Data.Aeson ( FromJSON(..), withObject, (.:) ) import Data.ByteString (ByteString) +import Data.Foldable (foldrM) import Data.Map (Map) import qualified Data.Map as Map @@ -117,7 +118,8 @@ compileMIRContract fileReader bic ghostEnv cenv0 sawenv c = return (n, t) setupState allocs (env, cenv) vars = do freshTerms <- mapM (setupFresh cenv) vars - let cenv' = foldr (\(ServerName n, t) -> CEnv.bindExtraVar (mkIdent n, t)) cenv freshTerms + let sc = biSharedContext bic + cenv' <- MIRSetupM $ liftIO $ foldrM (\(ServerName n, t) -> CEnv.bindExtraVar sc (mkIdent n, t)) cenv freshTerms let env' = Map.union env $ Map.fromList $ [ (n, Val (MS.SetupTerm t)) | (n, t) <- freshTerms ] ++ [ (n, Val v) | (n, v) <- allocs ] diff --git a/saw-server/src/SAWServer/SAWServer.hs b/saw-server/src/SAWServer/SAWServer.hs index d4c4484d7d..48c6e17b99 100644 --- a/saw-server/src/SAWServer/SAWServer.hs +++ b/saw-server/src/SAWServer/SAWServer.hs @@ -72,12 +72,12 @@ import SAWCentral.Options (processEnv, defaultOptions) import SAWCentral.Position (Pos(..)) import SAWCentral.Prover.Rewrite (basic_ss) import SAWCentral.Proof (emptyTheoremDB) -import SAWCentral.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, Environ(..), TopLevelRO(..), TopLevelRW(..), SAWSimpset, JavaCodebase(..), CryptolEnvStack(..), LLVMGlobalAllocMode(LLVMAllocConstantGlobals), rwModifyCryptolEnv, prettySimpset) +import SAWCentral.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, Environ(..), TopLevelRO(..), TopLevelRW(..), SAWSimpset, JavaCodebase(..), LLVMGlobalAllocMode(LLVMAllocConstantGlobals), rwSetCryptolEnv, rwGetCryptolEnv, prettySimpset) import SAWCentral.Yosys.State (YosysSequential) import SAWCentral.Yosys.Theorem (YosysTheorem) import SAWCentral.Yosys (YosysImport) import qualified CryptolSAWCore.Prelude as CryptolSAW -import CryptolSAWCore.CryptolEnv (initCryptolEnv, bindExtraVar) +import CryptolSAWCore.CryptolEnv (initCryptolEnv, bindExtraVar, withFileReader) import qualified Cryptol.Utils.Ident as Cryptol import SAWCentral.SolverCache (lazyOpenSolverCache) @@ -293,12 +293,10 @@ getHandleAlloc = roHandleAlloc . view sawTopLevelRO <$> Argo.getState initialState :: (FilePath -> IO ByteString) -> IO SAWState initialState readFileFn = - let ?fileReader = readFileFn in -- silence prevents output on stdout, which suppresses defaulting -- warnings from the Cryptol type checker - silence $ - do sc <- mkSharedContext - opts <- processEnv defaultOptions + silence $ mkSharedContext >>= \sc -> withFileReader sc readFileFn $ + do opts <- processEnv defaultOptions CryptolSAW.scLoadPreludeModule sc CryptolSAW.scLoadCryptolModule sc let mn = mkModuleName ["SAWScript"] @@ -308,7 +306,6 @@ initialState readFileFn = , biBasicSS = ss } cenv <- initCryptolEnv sc - let cryenvs = CryptolEnvStack cenv [] halloc <- Crucible.newHandleAllocator jvmTrans <- CJ.mkInitialJVMContext halloc cwd <- getCurrentDirectory @@ -330,7 +327,7 @@ initialState readFileFn = , roProofSubshell = \_ _ _ -> fail "SAW server does not support subshells." } rw = TopLevelRW - { rwEnviron = Environ ScopedMap.empty ScopedMap.empty cryenvs + { rwEnviron = Environ ScopedMap.empty ScopedMap.empty cenv , rwRebindables = Map.empty , rwPosition = PosInternal "SAWServer" , rwStackTrace = Trace.empty @@ -595,8 +592,12 @@ getServerValEither (SAWEnv serverEnv) n = bindCryptolVar :: Text -> TypedTerm -> Argo.Command SAWState () bindCryptolVar x t = - do Argo.modifyState $ over sawTopLevelRW $ rwModifyCryptolEnv $ \cenv -> - bindExtraVar (Cryptol.mkIdent x, t) cenv + do rw <- view sawTopLevelRW <$> Argo.getState + let + sc = rwSharedContext rw + cenv = rwGetCryptolEnv rw + cenv' <- liftIO $ bindExtraVar sc (Cryptol.mkIdent x, t) cenv + Argo.modifyState $ over sawTopLevelRW $ rwSetCryptolEnv $ cenv' getJVMClass :: ServerName -> Argo.Command SAWState JSS.Class getJVMClass n = diff --git a/saw-server/src/SAWServer/Yosys.hs b/saw-server/src/SAWServer/Yosys.hs index 87cb0d70d3..f54cc4d881 100644 --- a/saw-server/src/SAWServer/Yosys.hs +++ b/saw-server/src/SAWServer/Yosys.hs @@ -17,7 +17,7 @@ module SAWServer.Yosys ( yosysExtractSequentialDescr ) where -import Control.Lens (view, (%=)) +import Control.Lens (view) import Control.Monad (forM) import Control.Monad.IO.Class (liftIO) @@ -36,14 +36,14 @@ import qualified Argo.Doc as Doc import CryptolServer.Data.Expression (Expression(..), getCryptolExpr) -import SAWServer.SAWServer (SAWState, ServerName (ServerName), sawTask, setServerVal, getYosysImport, getYosysTheorem, getYosysSequential, sawTopLevelRW) +import SAWServer.SAWServer (SAWState, ServerName (ServerName), sawTask, setServerVal, getYosysImport, getYosysTheorem, getYosysSequential) import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp) import SAWServer.Exceptions (notAtTopLevel) import SAWServer.OK (OK, ok) import SAWServer.ProofScript (ProofScript, interpretProofScript) import SAWServer.TopLevel (tl) -import SAWCentral.Value (getSharedContext, getTopLevelRW, rwGetCryptolEnv, rwModifyCryptolEnv) +import SAWCentral.Value (getSharedContext, getTopLevelRW, rwGetCryptolEnv, getCryptolEnv, setCryptolEnv) import SAWCentral.Yosys (YosysImport(..), loadYosysIR, yosysIRToYosysImport, yosys_verify, yosys_import_sequential, yosys_extract_sequential) data YosysImportParams = YosysImportParams @@ -217,8 +217,11 @@ yosysExtractSequential params = do m <- getYosysSequential $ yosysExtractSequentialModule params s <- tl $ yosys_extract_sequential m (yosysExtractSequentialCycles params) let sn@(ServerName n) = yosysExtractSequentialServerName params - doBind cenv = CEnv.bindExtraVar (mkIdent n, s) cenv - sawTopLevelRW %= rwModifyCryptolEnv doBind + tl $ do + sc <- getSharedContext + cenv <- getCryptolEnv + cenv' <- liftIO $ CEnv.bindExtraVar sc (mkIdent n, s) cenv + setCryptolEnv cenv' setServerVal sn s ok diff --git a/saw-tools/css/Main.hs b/saw-tools/css/Main.hs index b5f7a1855f..5745140957 100644 --- a/saw-tools/css/Main.hs +++ b/saw-tools/css/Main.hs @@ -7,7 +7,6 @@ import System.Environment( getArgs ) import System.Exit( exitFailure ) import System.Console.GetOpt import System.IO -import qualified Data.ByteString as BS import Data.Text ( pack ) import GHC.IO.Encoding (setLocaleEncoding) @@ -98,7 +97,6 @@ cssMain css [inputModule,name] | cssMode css == NormalMode = do C.scLoadPreludeModule sc C.scLoadCryptolModule sc - let ?fileReader = BS.readFile cryenv <- C.initCryptolEnv sc cryenv' <- C.importCryptolModule sc cryenv (Left inputModule) Nothing False C.PublicAndPrivate Nothing @@ -134,8 +132,7 @@ extractCryptol sc cryenv input = do C.inpCol = 1 } - let ?fileReader = BS.readFile - (tt, _cryenv') <- C.parseTypedTerm sc cryenv input' + tt <- C.parseTypedTerm sc cryenv input' schema <- case TT.ttType tt of TT.TypedTermSchema s -> pure s diff --git a/saw.cabal b/saw.cabal index 0c015ccf07..ba2e241af1 100644 --- a/saw.cabal +++ b/saw.cabal @@ -253,9 +253,11 @@ library cryptol-saw-core exposed-modules: CryptolSAWCore.Cryptol CryptolSAWCore.CryptolEnv + CryptolSAWCore.GlobalCryptolEnv CryptolSAWCore.Prelude CryptolSAWCore.Pretty CryptolSAWCore.Simpset + CryptolSAWCore.SAWCoreCryptol CryptolSAWCore.TypedTerm other-modules: CryptolSAWCore.Module