Typed term

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

@@ -54,14 +54,13 @@ import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf)
 import Cryptol.Utils.PP (pretty)
 
 import Verifier.SAW.Cryptol.Panic
-import Verifier.SAW.Conversion
 import Verifier.SAW.FiniteValue (FirstOrderType(..), FirstOrderValue(..))
 import qualified Verifier.SAW.Simulator.Concrete as SC
+import qualified Verifier.SAW.Simulator.Value as SC
 import Verifier.SAW.Prim (BitVector(..))
-import Verifier.SAW.Rewriter
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Simulator.MonadLazy (force)
-import Verifier.SAW.TypedAST (mkSort, mkModuleName, FieldName, LocalName)
+import Verifier.SAW.TypedAST (mkSort, FieldName, LocalName)
 
 import GHC.Stack
 
@@ -1566,89 +1565,58 @@ pIsNeq ty = case C.tNoUser ty of
 --------------------------------------------------------------------------------
 -- Utilities
 
-asCryptolTypeValue :: SC.TValue SC.Concrete -> Maybe C.Type
+asCryptolTypeValue :: SC.TValue SC.Concrete -> Maybe (Either C.Kind C.Type)
 asCryptolTypeValue v =
   case v of
-    SC.VBoolType -> return C.tBit
-    SC.VIntType -> return C.tInteger
-    SC.VIntModType n -> return (C.tIntMod (C.tNum n))
+    SC.VBoolType -> return (Right C.tBit)
+    SC.VIntType -> return (Right C.tInteger)
+    SC.VIntModType n -> return (Right (C.tIntMod (C.tNum n)))
     SC.VArrayType v1 v2 -> do
-      t1 <- asCryptolTypeValue v1
-      t2 <- asCryptolTypeValue v2
-      return $ C.tArray t1 t2
+      Right t1 <- asCryptolTypeValue v1
+      Right t2 <- asCryptolTypeValue v2
+      return (Right (C.tArray t1 t2))
     SC.VVecType n v2 -> do
-      t2 <- asCryptolTypeValue v2
-      return (C.tSeq (C.tNum n) t2)
-    SC.VDataType "Prelude.Stream" [v1] ->
-      case v1 of
-        SC.TValue tv -> C.tSeq C.tInf <$> asCryptolTypeValue tv
-        _ -> Nothing
-    SC.VUnitType -> return (C.tTuple [])
+      Right t2 <- asCryptolTypeValue v2
+      return (Right (C.tSeq (C.tNum n) t2))
+
+    SC.VDataType "Prelude.Stream" [SC.TValue v1] ->
+        do Right t1 <- asCryptolTypeValue v1
+           return (Right (C.tSeq C.tInf t1))
+
+    SC.VDataType "Cryptol.Num" [] ->
+      return (Left C.KNum)
+
+    SC.VDataType _ _ -> Nothing
+
+    SC.VUnitType -> return (Right (C.tTuple []))
     SC.VPairType v1 v2 -> do
-      t1 <- asCryptolTypeValue v1
-      t2 <- asCryptolTypeValue v2
+      Right t1 <- asCryptolTypeValue v1
+      Right t2 <- asCryptolTypeValue v2
       case C.tIsTuple t2 of
-        Just ts -> return (C.tTuple (t1 : ts))
-        Nothing -> return (C.tTuple [t1, t2])
-    SC.VPiType v1 f -> do
-      case v1 of
-        -- if we see that the parameter is a Cryptol.Num, it's a
-        -- pretty good guess that it originally was a
-        -- polymorphic number type.
-        SC.VDataType "Cryptol.Num" [] ->
-          let msg= unwords ["asCryptolTypeValue: can't infer a polymorphic Cryptol"
-                           ,"type. Please, make sure all numeric types are"
-                           ,"specialized before constructing a typed term."
-                           ]
-          in error msg
-            -- otherwise we issue a generic error about dependent type inference
-        _ -> do
-          let msg = unwords ["asCryptolTypeValue: can't infer a Cryptol type"
-                            ,"for a dependent SAW-Core type."
-                            ]
-          let v2 = SC.runIdentity (f (error msg))
-          t1 <- asCryptolTypeValue v1
-          t2 <- asCryptolTypeValue v2
-          return (C.tFun t1 t2)
-    _ -> Nothing
-
--- | Deprecated.
-scCryptolType :: SharedContext -> Term -> IO C.Type
+        Just ts -> return (Right (C.tTuple (t1 : ts)))
+        Nothing -> return (Right (C.tTuple [t1, t2]))
+
+    SC.VPiType _nm v1 (SC.VNondependentPi v2) ->
+      do Right t1 <- asCryptolTypeValue v1
+         Right t2 <- asCryptolTypeValue v2
+         return (Right (C.tFun t1 t2))
+
+    SC.VSort s
+      | s == mkSort 0 -> return (Left C.KType)
+      | otherwise     -> Nothing
+
+    -- TODO?
+    SC.VPiType _nm _v1 (SC.VDependentPi _) -> Nothing
+    SC.VRecordType{} -> Nothing
+    SC.VTyTerm{} -> Nothing
+
+
+scCryptolType :: SharedContext -> Term -> IO (Maybe (Either C.Kind C.Type))
 scCryptolType sc t =
   do modmap <- scGetModuleMap sc
      case SC.evalSharedTerm modmap Map.empty Map.empty t of
-       SC.TValue (asCryptolTypeValue -> Just ty) -> return ty
-       _ -> panic "scCryptolType" ["scCryptolType: unsupported type " ++ showTerm t]
-
--- | Deprecated.
-scCryptolEq :: SharedContext -> Term -> Term -> IO Term
-scCryptolEq sc x y =
-  do rules <- concat <$> traverse defRewrites defs
-     let ss = addConvs natConversions (addRules rules emptySimpset :: Simpset ())
-     tx <- scTypeOf sc x >>= rewriteSharedTerm sc ss >>= scCryptolType sc . snd
-     ty <- scTypeOf sc y >>= rewriteSharedTerm sc ss >>= scCryptolType sc . snd
-     unless (tx == ty) $
-       panic "scCryptolEq"
-                 [ "scCryptolEq: type mismatch between"
-                 , pretty tx
-                 , "and"
-                 , pretty ty
-                 ]
-
-     -- Actually apply the equality function, along with the Eq class dictionary
-     t <- scTypeOf sc x
-     c <- scCryptolType sc t
-     k <- importType sc emptyEnv c
-     eqPrf <- proveProp sc emptyEnv (C.pEq c)
-     scGlobalApply sc "Cryptol.ecEq" [k, eqPrf, x, y]
-
-  where
-    defs = map (mkIdent (mkModuleName ["Cryptol"])) ["seq", "ty"]
-    defRewrites ident =
-      do maybe_def <- scFindDef sc ident
-         case maybe_def of
-           Nothing -> return []
-           Just def -> scDefRewriteRules sc def
+       SC.TValue tv -> return (asCryptolTypeValue tv)
+       _ -> return Nothing
 
 -- | Convert from SAWCore's Value type to Cryptol's, guided by the
 -- Cryptol type schema.

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

@@ -366,7 +366,7 @@ loadCryptolModule sc env path = do
 
   let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name
   let tm' = Map.filterWithKey (\k _ -> Set.member k names) $
-            Map.intersectionWith TypedTerm types newTermEnv
+            Map.intersectionWith (\t x -> TypedTerm (TypedTermSchema t) x) types newTermEnv
   let env' = env { eModuleEnv = modEnv''
                  , eTermEnv = newTermEnv
                  }
@@ -375,13 +375,18 @@ loadCryptolModule sc env path = do
 
 bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv
 bindCryptolModule (modName, CryptolModule sm tm) env =
-  env { eExtraNames = flip (foldr addName) (Map.keys tm) $
+  env { eExtraNames = flip (foldr addName) (Map.keys tm') $
                       flip (foldr addTSyn) (Map.keys sm) $ eExtraNames env
       , eExtraTSyns = Map.union sm (eExtraTSyns env)
-      , eExtraTypes = Map.union (fmap (\(TypedTerm s _) -> s) tm) (eExtraTypes env)
-      , eTermEnv    = Map.union (fmap (\(TypedTerm _ t) -> t) tm) (eTermEnv env)
+      , eExtraTypes = Map.union (fmap fst tm') (eExtraTypes env)
+      , eTermEnv    = Map.union (fmap snd tm') (eTermEnv env)
       }
   where
+    -- select out those typed terms that have Cryptol schemas
+    tm' = Map.mapMaybe f tm
+    f (TypedTerm (TypedTermSchema s) x) = Just (s,x)
+    f _ = Nothing
+
     addName name = MN.shadowing (MN.singletonE (P.mkQual modName (MN.nameIdent name)) name)
     addTSyn name = MN.shadowing (MN.singletonT (P.mkQual modName (MN.nameIdent name)) name)
 
@@ -435,7 +440,7 @@ bindIdent ident env = (name, env')
     env' = env { eModuleEnv = modEnv' }
 
 bindTypedTerm :: (Ident, TypedTerm) -> CryptolEnv -> CryptolEnv
-bindTypedTerm (ident, TypedTerm schema trm) env =
+bindTypedTerm (ident, TypedTerm (TypedTermSchema schema) trm) env =
   env' { eExtraNames = MR.shadowing (MN.singletonE pname name) (eExtraNames env)
        , eExtraTypes = Map.insert name schema (eExtraTypes env)
        , eTermEnv    = Map.insert name trm (eTermEnv env)
@@ -444,6 +449,10 @@ bindTypedTerm (ident, TypedTerm schema trm) env =
     pname = P.mkUnqual ident
     (name, env') = bindIdent ident env
 
+-- Only bind terms that have Cryptol schemas
+bindTypedTerm _ env = env
+
+
 bindType :: (Ident, T.Schema) -> CryptolEnv -> CryptolEnv
 bindType (ident, T.Forall [] [] ty) env =
   env' { eExtraNames = MR.shadowing (MN.singletonT pname name) (eExtraNames env)
@@ -528,7 +537,7 @@ parseTypedTerm sc env input = do
 
   -- Translate
   trm <- translateExpr sc env' expr
-  return (TypedTerm schema trm)
+  return (TypedTerm (TypedTermSchema schema) trm)
 
 parseDecls ::
   (?fileReader :: FilePath -> IO ByteString) =>

cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs

@@ -5,6 +5,7 @@ License     : BSD3
 Maintainer  : huffman
 Stability   : provisional
 -}
+{-# LANGUAGE PatternGuards #-}
 module Verifier.SAW.TypedTerm where
 
 import Control.Monad (foldM)
@@ -32,29 +33,50 @@ import Verifier.SAW.SharedTerm
 
 data TypedTerm =
   TypedTerm
-  { ttSchema :: C.Schema
+  { ttType :: TypedTermType
   , ttTerm :: Term
   }
   deriving Show
 
+
+-- | The different notion of Cryptol types that
+--   as SAWCore term might have.
+data TypedTermType
+  = TypedTermSchema C.Schema
+  | TypedTermKind   C.Kind
+  | TypedTermOther  Term
+ deriving Show
+
+
 ttTermLens :: Functor f => (Term -> f Term) -> TypedTerm -> f TypedTerm
 ttTermLens f tt = tt `seq` fmap (\x -> tt{ttTerm = x}) (f (ttTerm tt))
 
--- | Deprecated.
+ttIsMono :: TypedTermType -> Maybe C.Type
+ttIsMono ttp =
+  case ttp of
+    TypedTermSchema sch -> C.isMono sch
+    _ -> Nothing
+
 mkTypedTerm :: SharedContext -> Term -> IO TypedTerm
 mkTypedTerm sc trm = do
   ty <- scTypeOf sc trm
   ct <- scCryptolType sc ty
-  return $ TypedTerm (C.Forall [] [] ct) trm
+  let ttt = case ct of
+        Nothing        -> TypedTermOther ty
+        Just (Left k)  -> TypedTermKind k
+        Just (Right t) -> TypedTermSchema (C.tMono t)
+  return (TypedTerm ttt trm)
 
 -- | Apply a function-typed 'TypedTerm' to an argument. This operation
 -- fails if the first 'TypedTerm' does not have a monomorphic function
 -- type.
 applyTypedTerm :: SharedContext -> TypedTerm -> TypedTerm -> IO TypedTerm
-applyTypedTerm sc (TypedTerm schema1 t1) (TypedTerm _schema2 t2) =
-  case C.tIsFun =<< C.isMono schema1 of
-    Nothing -> fail "applyTypedTerm: not a function type"
-    Just (_, cty') -> TypedTerm (C.tMono cty') <$> scApply sc t1 t2
+applyTypedTerm sc (TypedTerm tp t1) (TypedTerm _ t2)
+  | Just (_,cty') <- C.tIsFun =<< ttIsMono tp
+  = TypedTerm (TypedTermSchema (C.tMono cty')) <$> scApply sc t1 t2
+
+-- TODO? extend this to allow explicit application of types?
+applyTypedTerm _ _ _ = fail "applyTypedTerm: not a (monomorphic) function type"
 
 -- | Apply a 'TypedTerm' to a list of arguments. This operation fails
 -- if the first 'TypedTerm' does not have a function type of
@@ -72,23 +94,24 @@ defineTypedTerm sc name (TypedTerm schema t) =
 -- fails if any 'TypedTerm' in the list has a polymorphic type.
 tupleTypedTerm :: SharedContext -> [TypedTerm] -> IO TypedTerm
 tupleTypedTerm sc tts =
-  case traverse (C.isMono . ttSchema) tts of
+  case traverse (ttIsMono . ttType) tts of
     Nothing -> fail "tupleTypedTerm: invalid polymorphic term"
     Just ctys ->
-      TypedTerm (C.tMono (C.tTuple ctys)) <$> scTuple sc (map ttTerm tts)
+      TypedTerm (TypedTermSchema (C.tMono (C.tTuple ctys))) <$>
+        scTuple sc (map ttTerm tts)
 
 -- | Given a 'TypedTerm' with a tuple type, return a list of its
 -- projected components. This operation fails if the 'TypedTerm' does
 -- not have a tuple type.
 destTupleTypedTerm :: SharedContext -> TypedTerm -> IO [TypedTerm]
-destTupleTypedTerm sc (TypedTerm schema t) =
-  case C.tIsTuple =<< C.isMono schema of
+destTupleTypedTerm sc (TypedTerm tp t) =
+  case C.tIsTuple =<< ttIsMono tp of
     Nothing -> fail "asTupleTypedTerm: not a tuple type"
     Just ctys ->
       do let len = length ctys
          let idxs = take len [1 ..]
          ts <- traverse (\i -> scTupleSelector sc t i len) idxs
-         pure $ zipWith TypedTerm (map C.tMono ctys) ts
+         pure $ zipWith TypedTerm (map (TypedTermSchema . C.tMono) ctys) ts
 
 -- First order types and values ------------------------------------------------
 
@@ -117,7 +140,7 @@ typedTermOfFirstOrderValue sc fov =
   do let fot = firstOrderTypeOf fov
      let cty = cryptolTypeOfFirstOrderType fot
      t <- scFirstOrderValue sc fov
-     pure $ TypedTerm (C.tMono cty) t
+     pure $ TypedTerm (TypedTermSchema (C.tMono cty)) t
 
 -- Typed external constants ----------------------------------------------------
 
@@ -130,23 +153,32 @@ data TypedExtCns =
 
 -- | Recognize 'TypedTerm's that are external constants.
 asTypedExtCns :: TypedTerm -> Maybe TypedExtCns
-asTypedExtCns (TypedTerm schema t) =
-  do cty <- C.isMono schema
+asTypedExtCns (TypedTerm tp t) =
+  do cty <- ttIsMono tp
      ec <- asExtCns t
      pure $ TypedExtCns cty ec
 
 -- | Make a 'TypedTerm' from a 'TypedExtCns'.
 typedTermOfExtCns :: SharedContext -> TypedExtCns -> IO TypedTerm
 typedTermOfExtCns sc (TypedExtCns cty ec) =
-  TypedTerm (C.tMono cty) <$> scExtCns sc ec
+  TypedTerm (TypedTermSchema (C.tMono cty)) <$> scExtCns sc ec
 
 abstractTypedExts :: SharedContext -> [TypedExtCns] -> TypedTerm -> IO TypedTerm
-abstractTypedExts sc tecs (TypedTerm (C.Forall params props ty) trm) =
+abstractTypedExts sc tecs (TypedTerm (TypedTermSchema (C.Forall params props ty)) trm) =
   do let tys = map tecType tecs
      let exts = map tecExt tecs
      let ty' = foldr C.tFun ty tys
      trm' <- scAbstractExts sc exts trm
-     pure $ TypedTerm (C.Forall params props ty') trm'
+     pure $ TypedTerm (TypedTermSchema (C.Forall params props ty')) trm'
+abstractTypedExts sc tecs (TypedTerm (TypedTermKind k) trm) =
+  do let exts = map tecExt tecs
+     trm' <- scAbstractExts sc exts trm
+     pure $ TypedTerm (TypedTermKind k) trm'
+abstractTypedExts sc tecs (TypedTerm (TypedTermOther _tp) trm) =
+  do let exts = map tecExt tecs
+     trm' <- scAbstractExts sc exts trm
+     tp'  <- scTypeOf sc trm'
+     pure $ TypedTerm (TypedTermOther tp') trm'
 
 -- Typed modules ---------------------------------------------------------------
 
@@ -162,9 +194,12 @@ showCryptolModule (CryptolModule sm tm) =
   unlines $
     (if Map.null sm then [] else
        "Type Synonyms" : "=============" : map showTSyn (Map.elems sm) ++ [""]) ++
-    "Symbols" : "=======" : map showBinding (Map.assocs tm)
+    "Symbols" : "=======" : concatMap showBinding (Map.assocs tm)
   where
     showTSyn (C.TySyn name params _props rhs _doc) =
       "    " ++ unwords (pretty (nameIdent name) : map pretty params) ++ " = " ++ pretty rhs
-    showBinding (name, TypedTerm schema _) =
-      "    " ++ pretty (nameIdent name) ++ " : " ++ pretty schema
+
+    showBinding (name, TypedTerm (TypedTermSchema schema) _) =
+      ["    " ++ pretty (nameIdent name) ++ " : " ++ pretty schema]
+    showBinding _ =
+      []

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -274,7 +274,7 @@ flattenSValue nm v = do
         VNat n                    -> return ([], "_" ++ show n)
         TValue (suffixTValue -> Just s)
                                   -> return ([], s)
-        VFun _ -> fail $ "Cannot create uninterpreted higher-order function " ++ show nm
+        VFun _ _ -> fail $ "Cannot create uninterpreted higher-order function " ++ show nm
         _ -> fail $ "Cannot create uninterpreted function " ++ show nm ++ " with argument " ++ show v
 
 vWord :: SWord -> SValue
@@ -584,11 +584,11 @@ sbvSolveBasic sc addlPrims unintSet t = do
 parseUninterpreted :: [SVal] -> String -> TValue SBV -> IO SValue
 parseUninterpreted cws nm ty =
   case ty of
-    (VPiType _ f)
+    (VPiType _ _ body)
       -> return $
          strictFun $ \x -> do
            (cws', suffix) <- flattenSValue nm x
-           t2 <- f (ready x)
+           t2 <- applyPiBody body (ready x)
            parseUninterpreted (cws ++ cws') (nm ++ suffix) t2
 
     VBoolType