Skip to content

Commit 6eb7a6c

Browse files
robdockinsrobdockins
committed
Updates flowing from cryptol PRs
GaloisInc/cryptol#1048 GaloisInc/cryptol#1136 GaloisInc/cryptol#1165 GaloisInc/cryptol#1171
1 parent 6af4873 commit 6eb7a6c

File tree

10 files changed

+103
-75
lines changed

10 files changed

+103
-75
lines changed

‎cryptol-saw-core/saw/Cryptol.sawcore

+26-11
Original file line numberDiff line numberDiff line change
@@ -1208,22 +1208,37 @@ ecCat =
12081208
-- Case for (TCNum m, TCInf)
12091209
(\ (a:sort 0) -> streamAppend a m));
12101210

1211-
ecSplitAt : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a ->
1212-
#(seq m a, seq n a);
1213-
ecSplitAt =
1211+
ecTake : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq m a;
1212+
ecTake =
1213+
Num_rec
1214+
(\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> seq m a)
1215+
1216+
(\ (m:Nat) ->
1217+
Num_rec
1218+
(\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> Vec m a)
1219+
-- The case (TCNum m, TCNum n)
1220+
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> take a m n xs)
1221+
-- The case (TCNum m, infinity)
1222+
(\ (a:sort 0) -> \ (xs: Stream a) -> streamTake a m xs))
1223+
1224+
(Num_rec
1225+
(\ (n:Num) -> (a:sort 0) -> seq (tcAdd TCInf n) a -> Stream a)
1226+
-- The case (TCInf, TCNum n)
1227+
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs)
1228+
-- The case (TCInf, TCInf)
1229+
(\ (a:sort 0) -> \ (xs:Stream a) -> xs));
1230+
1231+
ecDrop : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq n a;
1232+
ecDrop =
12141233
finNumRec
1215-
(\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a ->
1216-
#(seq m a, seq n a))
1234+
(\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> seq n a)
12171235
(\ (m:Nat) ->
12181236
Num_rec
1219-
(\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a ->
1220-
#(Vec m a, seq n a))
1237+
(\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> seq n a)
12211238
-- The case (TCNum n, TCNum m)
1222-
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) ->
1223-
(take a m n xs, drop a m n xs))
1239+
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> drop a m n xs)
12241240
-- The case (TCNum m, infinity)
1225-
(\ (a:sort 0) -> \ (xs: Stream a) ->
1226-
(streamTake a m xs, streamDrop a m xs)));
1241+
(\ (a:sort 0) -> \ (xs: Stream a) -> streamDrop a m xs));
12271242

12281243
ecJoin : (m n : Num) -> (a : sort 0) -> seq m (seq n a) -> seq (tcMul m n) a;
12291244
ecJoin m =

‎cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

+46-37
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,8 @@ import Text.URI
3535

3636
import qualified Cryptol.Eval.Type as TV
3737
import qualified Cryptol.Backend.Monad as V
38+
import qualified Cryptol.Backend.SeqMap as V
39+
import qualified Cryptol.Backend.WordValue as V
3840
import qualified Cryptol.Eval.Value as V
3941
import qualified Cryptol.Eval.Concrete as V
4042
import Cryptol.Eval.Type (evalValType)
@@ -45,6 +47,7 @@ import qualified Cryptol.ModuleSystem.Name as C
4547
import qualified Cryptol.Utils.Ident as C
4648
( Ident, PrimIdent(..), mkIdent, prelPrim, floatPrim, arrayPrim
4749
, ModName, modNameToText, identText, interactiveName
50+
, ModPath(..), modPathSplit
4851
)
4952
import qualified Cryptol.Utils.RecordMap as C
5053
import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf)
@@ -740,7 +743,8 @@ prelPrims =
740743

741744
-- -- Sequences primitives
742745
, ("#", flip scGlobalDef "Cryptol.ecCat") -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d
743-
, ("splitAt", flip scGlobalDef "Cryptol.ecSplitAt") -- {a,b,c} (fin a) => [a+b] c -> ([a]c,[b]c)
746+
, ("take", flip scGlobalDef "Cryptol.ecTake") -- {front, back, a} [front + back]a -> [front]a
747+
, ("drop", flip scGlobalDef "Cryptol.ecDrop") -- {front, back, a} (fin front) => [front + back]a -> [back]a
744748
, ("join", flip scGlobalDef "Cryptol.ecJoin") -- {a,b,c} (fin b) => [a][b]c -> [a * b]c
745749
, ("split", flip scGlobalDef "Cryptol.ecSplit") -- {a,b,c} (fin b) => [a * b] c -> [a][b] c
746750
, ("reverse", flip scGlobalDef "Cryptol.ecReverse") -- {a,b} (fin a) => [a] b -> [a] b
@@ -1231,18 +1235,20 @@ importName cnm =
12311235
case C.nameInfo cnm of
12321236
C.Parameter -> fail ("Cannot import non-top-level name: " ++ show cnm)
12331237
C.Declared modNm _
1234-
| modNm == C.interactiveName ->
1238+
| modNm == C.TopModule C.interactiveName ->
12351239
let shortNm = C.identText (C.nameIdent cnm)
12361240
aliases = [shortNm]
12371241
uri = cryptolURI [shortNm] (Just (C.nameUnique cnm))
12381242
in pure (ImportedName uri aliases)
12391243

12401244
| otherwise ->
1241-
let modNmTxt = C.modNameToText modNm
1242-
modNms = Text.splitOn "::" modNmTxt
1243-
shortNm = C.identText (C.nameIdent cnm)
1244-
aliases = [shortNm, modNmTxt <> "::" <> shortNm]
1245-
uri = cryptolURI (modNms ++ [shortNm]) Nothing
1245+
let (topMod, nested) = C.modPathSplit modNm
1246+
modNmTxt = C.modNameToText topMod
1247+
modNms = (Text.splitOn "::" modNmTxt) ++ map C.identText nested
1248+
shortNm = C.identText (C.nameIdent cnm)
1249+
longNm = Text.intercalate "::" ([modNmTxt] ++ map C.identText nested ++ [shortNm])
1250+
aliases = [shortNm, longNm]
1251+
uri = cryptolURI (modNms ++ [shortNm]) Nothing
12461252
in pure (ImportedName uri aliases)
12471253

12481254
-- | Currently this imports declaration groups by inlining all the
@@ -1639,22 +1645,22 @@ scCryptolEq sc x y =
16391645

16401646
-- | Convert from SAWCore's Value type to Cryptol's, guided by the
16411647
-- Cryptol type schema.
1642-
exportValueWithSchema :: C.Schema -> SC.CValue -> V.Value
1648+
exportValueWithSchema :: C.Schema -> SC.CValue -> V.Eval V.Value
16431649
exportValueWithSchema (C.Forall [] [] ty) v = exportValue (evalValType mempty ty) v
1644-
exportValueWithSchema _ _ = V.VPoly mempty (error "exportValueWithSchema")
1650+
exportValueWithSchema _ _ = pure (V.VPoly mempty (error "exportValueWithSchema"))
16451651
-- TODO: proper support for polymorphic values
16461652

1647-
exportValue :: TV.TValue -> SC.CValue -> V.Value
1653+
exportValue :: TV.TValue -> SC.CValue -> V.Eval V.Value
16481654
exportValue ty v = case ty of
16491655

16501656
TV.TVBit ->
1651-
V.VBit (SC.toBool v)
1657+
pure (V.VBit (SC.toBool v))
16521658

16531659
TV.TVInteger ->
1654-
V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer")
1660+
pure (V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer"))
16551661

16561662
TV.TVIntMod _modulus ->
1657-
V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod")
1663+
pure (V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod"))
16581664

16591665
TV.TVArray{} -> error $ "exportValue: (on array type " ++ show ty ++ ")"
16601666

@@ -1666,28 +1672,29 @@ exportValue ty v = case ty of
16661672
case v of
16671673
SC.VWord w -> V.word V.Concrete (toInteger (width w)) (unsigned w)
16681674
SC.VVector xs
1669-
| TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) (V.ready (V.LargeBitsVal (fromIntegral (Vector.length xs))
1670-
(V.finiteSeqMap . map (V.ready . V.VBit . SC.toBool . SC.runIdentity . force) $ Fold.toList xs)))
1671-
| otherwise -> V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap $
1672-
map (V.ready . exportValue e . SC.runIdentity . force) $ Vector.toList xs
1675+
| TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) <$>
1676+
V.bitmapWordVal V.Concrete (toInteger (Vector.length xs))
1677+
(V.finiteSeqMap V.Concrete . map (V.ready . SC.toBool . SC.runIdentity . force) $ Fold.toList xs)
1678+
| otherwise -> pure . V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap V.Concrete $
1679+
map (\x -> exportValue e (SC.runIdentity (force x))) (Vector.toList xs)
16731680
_ -> error $ "exportValue (on seq type " ++ show ty ++ ")"
16741681

16751682
-- infinite streams
16761683
TV.TVStream e ->
16771684
case v of
1678-
SC.VExtra (SC.CStream trie) -> V.VStream (V.IndexSeqMap $ \i -> V.ready $ exportValue e (IntTrie.apply trie i))
1685+
SC.VExtra (SC.CStream trie) -> pure $ V.VStream (V.indexSeqMap $ \i -> exportValue e (IntTrie.apply trie i))
16791686
_ -> error $ "exportValue (on seq type " ++ show ty ++ ")"
16801687

16811688
-- tuples
1682-
TV.TVTuple etys -> V.VTuple (exportTupleValue etys v)
1689+
TV.TVTuple etys -> pure $ V.VTuple $ exportTupleValue etys v
16831690

16841691
-- records
16851692
TV.TVRec fields ->
1686-
V.VRecord (C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v)
1693+
pure . V.VRecord . C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v
16871694

16881695
-- functions
16891696
TV.TVFun _aty _bty ->
1690-
V.VFun mempty (error "exportValue: TODO functions")
1697+
pure $ V.VFun mempty (error "exportValue: TODO functions")
16911698

16921699
-- abstract types
16931700
TV.TVAbstract{} ->
@@ -1702,8 +1709,8 @@ exportTupleValue :: [TV.TValue] -> SC.CValue -> [V.Eval V.Value]
17021709
exportTupleValue tys v =
17031710
case (tys, v) of
17041711
([] , SC.VUnit ) -> []
1705-
([t] , _ ) -> [V.ready $ exportValue t v]
1706-
(t : ts, SC.VPair x y) -> (V.ready $ exportValue t (run x)) : exportTupleValue ts (run y)
1712+
([t] , _ ) -> [exportValue t v]
1713+
(t : ts, SC.VPair x y) -> (exportValue t (run x)) : exportTupleValue ts (run y)
17071714
_ -> error $ "exportValue: expected tuple"
17081715
where
17091716
run = SC.runIdentity . force
@@ -1712,12 +1719,11 @@ exportRecordValue :: [(C.Ident, TV.TValue)] -> SC.CValue -> [(C.Ident, V.Eval V.
17121719
exportRecordValue fields v =
17131720
case (fields, v) of
17141721
([] , SC.VUnit ) -> []
1715-
([(n, t)] , _ ) -> [(n, V.ready $ exportValue t v)]
1716-
((n, t) : ts, SC.VPair x y) ->
1717-
(n, V.ready $ exportValue t (run x)) : exportRecordValue ts (run y)
1722+
([(n, t)] , _ ) -> [(n, exportValue t v)]
1723+
((n, t) : ts, SC.VPair x y) -> (n, exportValue t (run x)) : exportRecordValue ts (run y)
17181724
(_, SC.VRecordValue (alistAllFields
17191725
(map (C.identText . fst) fields) -> Just ths)) ->
1720-
zipWith (\(n,t) x -> (n, V.ready $ exportValue t (run x))) fields ths
1726+
zipWith (\(n,t) x -> (n, exportValue t (run x))) fields ths
17211727
_ -> error $ "exportValue: expected record"
17221728
where
17231729
run = SC.runIdentity . force
@@ -1726,20 +1732,23 @@ fvAsBool :: FirstOrderValue -> Bool
17261732
fvAsBool (FOVBit b) = b
17271733
fvAsBool _ = error "fvAsBool: expected FOVBit value"
17281734

1729-
exportFirstOrderValue :: FirstOrderValue -> V.Value
1735+
exportFirstOrderValue :: FirstOrderValue -> V.Eval V.Value
17301736
exportFirstOrderValue fv =
17311737
case fv of
1732-
FOVBit b -> V.VBit b
1733-
FOVInt i -> V.VInteger i
1734-
FOVIntMod _ i -> V.VInteger i
1735-
FOVWord w x -> V.word V.Concrete (toInteger w) x
1738+
FOVBit b -> pure (V.VBit b)
1739+
FOVInt i -> pure (V.VInteger i)
1740+
FOVIntMod _ i -> pure (V.VInteger i)
1741+
FOVWord w x -> V.word V.Concrete (toInteger w) x
17361742
FOVVec t vs
1737-
| t == FOTBit -> V.VWord len (V.ready (V.LargeBitsVal len (V.finiteSeqMap . map (V.ready . V.VBit . fvAsBool) $ vs)))
1738-
| otherwise -> V.VSeq len (V.finiteSeqMap (map (V.ready . exportFirstOrderValue) vs))
1743+
| t == FOTBit -> V.VWord len <$> (V.bitmapWordVal V.Concrete len
1744+
(V.finiteSeqMap V.Concrete . map (V.ready . fvAsBool) $ vs))
1745+
| otherwise -> pure (V.VSeq len (V.finiteSeqMap V.Concrete (map exportFirstOrderValue vs)))
17391746
where len = toInteger (length vs)
17401747
FOVArray{} -> error $ "exportFirstOrderValue: unsupported FOT Array"
1741-
FOVTuple vs -> V.VTuple (map (V.ready . exportFirstOrderValue) vs)
1742-
FOVRec vm -> V.VRecord $ C.recordFromFields [ (C.mkIdent n, V.ready $ exportFirstOrderValue v) | (n, v) <- Map.assocs vm ]
1748+
FOVTuple vs -> pure $ V.VTuple $ map exportFirstOrderValue vs
1749+
FOVRec vm ->
1750+
do let vm' = fmap exportFirstOrderValue vm
1751+
pure $ V.VRecord $ C.recordFromFields [ (C.mkIdent n, v) | (n, v) <- Map.assocs vm' ]
17431752

17441753
importFirstOrderValue :: FirstOrderType -> V.Value -> IO FirstOrderValue
17451754
importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0)
@@ -1748,7 +1757,7 @@ importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0)
17481757
go t v = case (t,v) of
17491758
(FOTBit , V.VBit b) -> return (FOVBit b)
17501759
(FOTInt , V.VInteger i) -> return (FOVInt i)
1751-
(FOTVec _ FOTBit, V.VWord w wv) -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete =<< wv)
1760+
(FOTVec _ FOTBit, V.VWord w wv) -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete wv)
17521761
(FOTVec _ ty , V.VSeq len xs) -> FOVVec ty <$> traverse (go ty =<<) (V.enumerateSeqMap len xs)
17531762
(FOTTuple tys , V.VTuple xs) -> FOVTuple <$> traverse (\(ty, x) -> go ty =<< x) (zip tys xs)
17541763
(FOTRec fs , V.VRecord xs) ->

‎cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs

+14-16
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ module Verifier.SAW.CryptolEnv
3232
, InputText(..)
3333
, lookupIn
3434
, resolveIdentifier
35+
, meSolverConfig
3536
)
3637
where
3738

@@ -152,7 +153,7 @@ nameMatcher xs =
152153
case modNameChunks (textToModName (pack xs)) of
153154
[] -> const False
154155
[x] -> (packIdent x ==) . MN.nameIdent
155-
cs -> let m = MN.Declared (packModName (map pack (init cs))) MN.UserName
156+
cs -> let m = MN.Declared (C.TopModule (packModName (map pack (init cs)))) MN.UserName
156157
i = packIdent (last cs)
157158
in \n -> MN.nameIdent n == i && MN.nameInfo n == m
158159

@@ -252,7 +253,7 @@ getNamingEnv env = eExtraNames env `MR.shadowing` nameEnv
252253
syms = case vis of
253254
OnlyPublic -> MI.ifPublic ifc
254255
PublicAndPrivate -> MI.ifPublic ifc `mappend` M.ifPrivate ifc
255-
return $ MN.interpImport i syms
256+
return $ MN.interpImportIface i syms
256257

257258
getAllIfaceDecls :: ME.ModuleEnv -> M.IfaceDecls
258259
getAllIfaceDecls me = mconcat (map (both . ME.lmInterface) (ME.getLoadedModules (ME.meLoadedModules me)))
@@ -363,13 +364,13 @@ loadCryptolModule sc env path = do
363364
newCryEnv <- C.importTopLevelDeclGroups sc oldCryEnv newDeclGroups
364365
newTermEnv <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)
365366

366-
let names = MEx.eBinds (T.mExports m) -- :: Set T.Name
367+
let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name
367368
let tm' = Map.filterWithKey (\k _ -> Set.member k names) $
368369
Map.intersectionWith TypedTerm types newTermEnv
369370
let env' = env { eModuleEnv = modEnv''
370371
, eTermEnv = newTermEnv
371372
}
372-
let sm' = Map.filterWithKey (\k _ -> Set.member k (MEx.eTypes (T.mExports m))) (T.mTySyns m)
373+
let sm' = Map.filterWithKey (\k _ -> Set.member k (MEx.exported C.NSType (T.mExports m))) (T.mTySyns m)
373374
return (CryptolModule sm' tm', env')
374375

375376
bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv
@@ -429,7 +430,7 @@ bindIdent ident env = (name, env')
429430
modEnv = eModuleEnv env
430431
supply = ME.meSupply modEnv
431432
fixity = Nothing
432-
(name, supply') = MN.mkDeclared interactiveName MN.UserName ident fixity P.emptyRange supply
433+
(name, supply') = MN.mkDeclared C.NSValue (C.TopModule interactiveName) MN.UserName ident fixity P.emptyRange supply
433434
modEnv' = modEnv { ME.meSupply = supply' }
434435
env' = env { eModuleEnv = modEnv' }
435436

@@ -466,6 +467,9 @@ bindInteger (ident, n) env =
466467

467468
--------------------------------------------------------------------------------
468469

470+
meSolverConfig :: ME.ModuleEnv -> TM.SolverConfig
471+
meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env)
472+
469473
resolveIdentifier ::
470474
(?fileReader :: FilePath -> IO ByteString) =>
471475
CryptolEnv -> Text -> IO (Maybe T.Name)
@@ -480,10 +484,10 @@ resolveIdentifier env nm =
480484
nameEnv = getNamingEnv env
481485

482486
doResolve pnm =
483-
SMT.withSolver (ME.meSolverConfig modEnv) $ \s ->
487+
SMT.withSolver (meSolverConfig modEnv) $ \s ->
484488
do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader modEnv
485489
(res, _ws) <- MM.runModuleM (minp s) $
486-
MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar pnm))
490+
MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar MR.NameUse pnm))
487491
case res of
488492
Left _ -> pure Nothing
489493
Right (x,_) -> pure (Just x)
@@ -544,18 +548,12 @@ parseDecls sc env input = do
544548
-- Convert from 'Decl' to 'TopDecl' so that types will be generalized
545549
let topdecls = [ P.Decl (P.TopLevel P.Public Nothing d) | d <- npdecls ]
546550

547-
-- Label each TopDecl with the "interactive" module for unique name generation
548-
let (mdecls :: [MN.InModule (P.TopDecl P.PName)]) = map (MN.InModule interactiveName) topdecls
549-
nameEnv1 <- MN.liftSupply (MN.namingEnv' mdecls)
550-
551551
-- Resolve names
552-
let nameEnv = nameEnv1 `MR.shadowing` getNamingEnv env
553-
(rdecls :: [P.TopDecl T.Name]) <- MM.interactive (MB.rename interactiveName nameEnv (traverse MR.rename topdecls))
552+
(_nenv, rdecls) <- MM.interactive (MB.rename interactiveName (getNamingEnv env) (MR.renameTopDecls interactiveName topdecls))
554553

555554
-- Create a Module to contain the declarations
556555
let rmodule = P.Module { P.mName = P.Located P.emptyRange interactiveName
557556
, P.mInstance = Nothing
558-
, P.mImports = []
559557
, P.mDecls = rdecls
560558
}
561559

@@ -623,7 +621,7 @@ declareName env mname input = do
623621
let modEnv = eModuleEnv env
624622
(cname, modEnv') <-
625623
liftModuleM modEnv $ MM.interactive $
626-
MN.liftSupply (MN.mkDeclared mname MN.UserName (P.getIdent pname) Nothing P.emptyRange)
624+
MN.liftSupply (MN.mkDeclared C.NSValue (C.TopModule mname) MN.UserName (P.getIdent pname) Nothing P.emptyRange)
627625
let env' = env { eModuleEnv = modEnv' }
628626
return (cname, env')
629627

@@ -646,7 +644,7 @@ liftModuleM ::
646644
ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv)
647645
liftModuleM env m =
648646
do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader env
649-
SMT.withSolver (ME.meSolverConfig env) $ \s ->
647+
SMT.withSolver (meSolverConfig env) $ \s ->
650648
MM.runModuleM (minp s) m >>= moduleCmdResult
651649

652650
defaultEvalOpts :: E.EvalOpts

‎saw/SAWScript/REPL/Monad.hs

+3-2
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ import Cryptol.Parser (ParseError,ppError)
5555
import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
5656
import Cryptol.Parser.NoPat (Error)
5757
import qualified Cryptol.TypeCheck.AST as T
58+
import Cryptol.Utils.Ident (Namespace(..))
5859
import Cryptol.Utils.PP
5960

6061
#if !MIN_VERSION_base(4,8,0)
@@ -297,13 +298,13 @@ getNewtypes = do
297298
getExprNames :: REPL [String]
298299
getExprNames =
299300
do fNames <- fmap getNamingEnv getCryptolEnv
300-
return (map (show . pp) (Map.keys (MN.neExprs fNames)))
301+
return (map (show . pp) (Map.keys (MN.namespaceMap NSValue fNames)))
301302

302303
-- | Get visible type signature names.
303304
getTypeNames :: REPL [String]
304305
getTypeNames =
305306
do fNames <- fmap getNamingEnv getCryptolEnv
306-
return (map (show . pp) (Map.keys (MN.neTypes fNames)))
307+
return (map (show . pp) (Map.keys (MN.namespaceMap NSType fNames)))
307308

308309
getPropertyNames :: REPL [String]
309310
getPropertyNames =

‎src/SAWScript/AutoMatch/Cryptol.hs

+4-1
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,9 @@ import qualified Cryptol.TypeCheck.AST as AST
2525
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
2626
import Cryptol.Utils.PP
2727

28+
import Verifier.SAW.CryptolEnv( meSolverConfig )
29+
30+
2831
-- | Parse a Cryptol module into a list of declarations
2932
-- Yields an Interaction so that we can talk to the user about what went wrong
3033
getDeclsCryptol :: FilePath -> IO (Interaction (Maybe [Decl]))
@@ -33,7 +36,7 @@ getDeclsCryptol path = do
3336
modEnv <- M.initialModuleEnv
3437
let minp = M.ModuleInput True (pure evalOpts) BS.readFile modEnv
3538
(result, warnings) <-
36-
SMT.withSolver (M.meSolverConfig modEnv) $ \s ->
39+
SMT.withSolver (meSolverConfig modEnv) $ \s ->
3740
M.loadModuleByPath path (minp s)
3841
return $ do
3942
forM_ warnings $ liftF . flip Warning () . pretty

0 commit comments

Comments
 (0)