Recursor refactor

cryptol-saw-core/cryptol-saw-core.cabal

@@ -39,6 +39,7 @@ library
     saw-core-what4,
     what4,
     sbv,
+    transformers,
     vector,
     text,
     executable-path,

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

@@ -1,5 +1,6 @@
 {-# OPTIONS_GHC -Wall #-}
 {-# LANGUAGE DoAndIfThenElse #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE ViewPatterns #-}
@@ -16,13 +17,14 @@ Portability : non-portable (language extensions)
 
 module Verifier.SAW.Cryptol where
 
-import Control.Monad (foldM, join, unless)
+import Control.Monad (foldM, join, unless, mzero, zipWithM)
+import Control.Monad.IO.Class
+import Control.Monad.Trans.Maybe
 import Data.Bifunctor (first)
 import qualified Data.Foldable as Fold
 import Data.List
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Maybe (fromMaybe)
-import qualified Data.IntTrie as IntTrie
 import Data.Map (Map)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
@@ -1553,7 +1555,7 @@ pIsNeq ty = case C.tNoUser ty of
 --------------------------------------------------------------------------------
 -- Utilities
 
-asCryptolTypeValue :: SC.TValue SC.Concrete -> Maybe C.Type
+asCryptolTypeValue :: SC.TValue SC.Concrete -> MaybeT IO C.Type
 asCryptolTypeValue v =
   case v of
     SC.VBoolType -> return C.tBit
@@ -1569,15 +1571,15 @@ asCryptolTypeValue v =
     SC.VDataType "Prelude.Stream" [v1] ->
       case v1 of
         SC.TValue tv -> C.tSeq C.tInf <$> asCryptolTypeValue tv
-        _ -> Nothing
+        _ -> mzero
     SC.VUnitType -> return (C.tTuple [])
     SC.VPairType v1 v2 -> do
       t1 <- asCryptolTypeValue v1
       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
+    SC.VPiType _nm 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
@@ -1593,19 +1595,24 @@ asCryptolTypeValue v =
           let msg = unwords ["asCryptolTypeValue: can't infer a Cryptol type"
                             ,"for a dependent SAW-Core type."
                             ]
-          let v2 = SC.runIdentity (f (error msg))
+          v2 <- liftIO (f (error msg))
           t1 <- asCryptolTypeValue v1
           t2 <- asCryptolTypeValue v2
           return (C.tFun t1 t2)
-    _ -> Nothing
+    _ -> mzero
 
 -- | Deprecated.
 scCryptolType :: SharedContext -> Term -> IO 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]
+     tm <- SC.evalSharedTerm modmap Map.empty Map.empty t
+     let err = panic "scCryptolType" ["scCryptolType: unsupported type " ++ showTerm t]
+     case tm of
+       SC.TValue tv ->
+         runMaybeT (asCryptolTypeValue tv) >>= \case
+           Just ty -> return ty
+           Nothing -> err
+       _ -> err
 
 -- | Deprecated.
 scCryptolEq :: SharedContext -> Term -> Term -> IO Term
@@ -1639,22 +1646,22 @@ scCryptolEq sc x y =
 
 -- | Convert from SAWCore's Value type to Cryptol's, guided by the
 -- Cryptol type schema.
-exportValueWithSchema :: C.Schema -> SC.CValue -> V.Value
+exportValueWithSchema :: C.Schema -> SC.CValue -> IO V.Value
 exportValueWithSchema (C.Forall [] [] ty) v = exportValue (evalValType mempty ty) v
-exportValueWithSchema _ _ = V.VPoly mempty (error "exportValueWithSchema")
+exportValueWithSchema _ _ = pure (V.VPoly mempty (error "exportValueWithSchema"))
 -- TODO: proper support for polymorphic values
 
-exportValue :: TV.TValue -> SC.CValue -> V.Value
+exportValue :: TV.TValue -> SC.CValue -> IO V.Value
 exportValue ty v = case ty of
 
   TV.TVBit ->
-    V.VBit (SC.toBool v)
+    pure (V.VBit (SC.toBool v))
 
   TV.TVInteger ->
-    V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer")
+    pure (V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer"))
 
   TV.TVIntMod _modulus ->
-    V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod")
+    pure (V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod"))
 
   TV.TVArray{} -> error $ "exportValue: (on array type " ++ show ty ++ ")"
 
@@ -1664,30 +1671,30 @@ exportValue ty v = case ty of
 
   TV.TVSeq _ e ->
     case v of
-      SC.VWord w -> V.word V.Concrete (toInteger (width w)) (unsigned w)
+      SC.VWord w -> pure (V.word V.Concrete (toInteger (width w)) (unsigned w))
       SC.VVector xs
-        | TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) (V.ready (V.LargeBitsVal (fromIntegral (Vector.length xs))
-                            (V.finiteSeqMap . map (V.ready . V.VBit . SC.toBool . SC.runIdentity . force) $ Fold.toList xs)))
-        | otherwise   -> V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap $
-                            map (V.ready . exportValue e . SC.runIdentity . force) $ Vector.toList xs
+        | TV.isTBit e -> pure $ V.VWord (toInteger (Vector.length xs)) (V.ready (V.LargeBitsVal (fromIntegral (Vector.length xs))
+                            (V.finiteSeqMap . map (\x -> V.VBit . SC.toBool <$> liftIO (force x)) $ Fold.toList xs)))
+        | otherwise   -> pure $ V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap $
+                            map (\x -> liftIO (exportValue e =<< force x)) $ Vector.toList xs
       _ -> error $ "exportValue (on seq type " ++ show ty ++ ")"
 
   -- infinite streams
   TV.TVStream e ->
     case v of
-      SC.VExtra (SC.CStream trie) -> V.VStream (V.IndexSeqMap $ \i -> V.ready $ exportValue e (IntTrie.apply trie i))
+      SC.VExtra st -> pure $ V.VStream (V.IndexSeqMap $ \i -> liftIO (exportValue e =<< SC.lookupCExtra st (fromInteger i)))
       _ -> error $ "exportValue (on seq type " ++ show ty ++ ")"
 
   -- tuples
-  TV.TVTuple etys -> V.VTuple (exportTupleValue etys v)
+  TV.TVTuple etys -> V.VTuple <$> exportTupleValue etys v
 
   -- records
   TV.TVRec fields ->
-      V.VRecord (C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v)
+      V.VRecord . C.recordFromFieldsWithDisplay (C.displayOrder fields) <$> exportRecordValue (C.canonicalFields fields) v
 
   -- functions
   TV.TVFun _aty _bty ->
-    V.VFun mempty (error "exportValue: TODO functions")
+    pure $ V.VFun mempty (error "exportValue: TODO functions")
 
   -- abstract types
   TV.TVAbstract{} ->
@@ -1698,29 +1705,39 @@ exportValue ty v = case ty of
     exportValue (TV.TVRec fields) v
 
 
-exportTupleValue :: [TV.TValue] -> SC.CValue -> [V.Eval V.Value]
+exportTupleValue :: [TV.TValue] -> SC.CValue -> IO [V.Eval V.Value]
 exportTupleValue tys v =
   case (tys, v) of
-    ([]    , SC.VUnit    ) -> []
-    ([t]   , _           ) -> [V.ready $ exportValue t v]
-    (t : ts, SC.VPair x y) -> (V.ready $ exportValue t (run x)) : exportTupleValue ts (run y)
-    _                      -> error $ "exportValue: expected tuple"
-  where
-    run = SC.runIdentity . force
-
-exportRecordValue :: [(C.Ident, TV.TValue)] -> SC.CValue -> [(C.Ident, V.Eval V.Value)]
+    ([]    , SC.VUnit    ) -> pure []
+    ([t]   , _           ) ->
+       do v' <- exportValue t v
+          pure [V.ready v']
+    (t : ts, SC.VPair x y) ->
+       do v1 <- exportValue t =<< force x
+          v2 <- exportTupleValue ts =<< force y
+          pure (V.ready v1:v2)
+    _ -> error $ "exportValue: expected tuple"
+
+exportRecordValue :: [(C.Ident, TV.TValue)] -> SC.CValue -> IO [(C.Ident, V.Eval V.Value)]
 exportRecordValue fields v =
   case (fields, v) of
-    ([]         , SC.VUnit    ) -> []
-    ([(n, t)]   , _           ) -> [(n, V.ready $ exportValue t v)]
+    ([]         , SC.VUnit    ) -> pure []
+
+    ([(n, t)]   , _           ) ->
+       do v' <- exportValue t v
+          pure [(n,V.ready v')]
+
     ((n, t) : ts, SC.VPair x y) ->
-      (n, V.ready $ exportValue t (run x)) : exportRecordValue ts (run y)
+       do v1 <- exportValue t =<< force x
+          v2 <- exportRecordValue ts =<< force y
+          pure ((n,V.ready v1):v2)
+
     (_, SC.VRecordValue (alistAllFields
                          (map (C.identText . fst) fields) -> Just ths)) ->
-      zipWith (\(n,t) x -> (n, V.ready $ exportValue t (run x))) fields ths
-    _                              -> error $ "exportValue: expected record"
-  where
-    run = SC.runIdentity . force
+      zipWithM (\(n,t) x -> do v' <- exportValue t =<< force x; pure (n,V.ready v'))
+         fields ths
+
+    _  -> error $ "exportValue: expected record"
 
 fvAsBool :: FirstOrderValue -> Bool
 fvAsBool (FOVBit b) = b

saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs

@@ -45,6 +45,7 @@ import Verifier.SAW.TypedAST
 import qualified Verifier.SAW.Simulator.Concrete as Concrete
 import qualified Verifier.SAW.Prim as Prim
 import qualified Verifier.SAW.Recognizer as R
+import Verifier.SAW.Utils (panic)
 
 import qualified Data.AIG as AIG
 
@@ -151,7 +152,7 @@ bvShiftOp bvOp natOp =
   strictFun $ \y ->
     case y of
       VNat n   -> return (vWord (natOp x n))
-      VToNat v -> fmap vWord (bvOp x =<< toWord v)
+      VBVToNat _ v -> fmap vWord (bvOp x =<< toWord v)
       _        -> error $ unwords ["Verifier.SAW.Simulator.BitBlast.shiftOp", show y]
 
 lvSShr :: LitVector l -> Natural -> LitVector l
@@ -296,19 +297,21 @@ lazyMux be muxFn c tm fm
       f <- fm
       muxFn c t f
 
-muxBVal :: AIG.IsAIG l g => g s -> l s -> BValue (l s) -> BValue (l s) -> IO (BValue (l s))
+muxBVal :: AIG.IsAIG l g => g s -> TValue (BitBlast (l s)) -> l s -> BValue (l s) -> BValue (l s) -> IO (BValue (l s))
 muxBVal be = Prims.muxValue (prims be)
 
 muxInt :: a -> Integer -> Integer -> IO Integer
 muxInt _ x y = if x == y then return x else fail $ "muxBVal: VInt " ++ show (x, y)
 
-muxBExtra :: AIG.IsAIG l g => g s -> l s -> BExtra (l s) -> BExtra (l s) -> IO (BExtra (l s))
-muxBExtra be c x y =
+muxBExtra :: AIG.IsAIG l g => g s ->
+  TValue (BitBlast (l s)) -> l s -> BExtra (l s) -> BExtra (l s) -> IO (BExtra (l s))
+muxBExtra be (VDataType "Prelude.Stream" [TValue tp]) c x y =
   do let f i = do xi <- lookupBStream (VExtra x) i
                   yi <- lookupBStream (VExtra y) i
-                  muxBVal be c xi yi
+                  muxBVal be tp c xi yi
      r <- newIORef Map.empty
      return (BStream f r)
+muxBExtra _ tp _ _ _ = panic "AIG: muxBExtra" ["Type mismatch", show tp]
 
 -- | Barrel-shifter algorithm. Takes a list of bits in big-endian order.
 genShift ::
@@ -396,13 +399,13 @@ mkStreamOp =
 -- streamGet :: (a :: sort 0) -> Stream a -> Nat -> a;
 streamGetOp :: AIG.IsAIG l g => g s -> BValue (l s)
 streamGetOp be =
-  constFun $
+  strictFun $ \(toTValue -> tp) -> return $
   strictFun $ \xs -> return $
   strictFun $ \case
     VNat n -> lookupBStream xs n
-    VToNat w ->
+    VBVToNat _ w ->
        do bs <- toWord w
-          AIG.muxInteger (lazyMux be (muxBVal be)) ((2 ^ AIG.length bs) - 1) bs (lookupBStream xs)
+          AIG.muxInteger (lazyMux be (muxBVal be tp)) ((2 ^ AIG.length bs) - 1) bs (lookupBStream xs)
     v -> fail (unlines ["Verifier.SAW.Simulator.BitBlast.streamGetOp", "Expected Nat value", show v])
 
 
@@ -446,9 +449,11 @@ bitBlastBasic :: AIG.IsAIG l g
               -> Term
               -> IO (BValue (l s))
 bitBlastBasic be m addlPrims ecMap t = do
+  let neutral _env nt = fail ("bitBlastBasic: could not evaluate neutral term: " ++ show nt)
   cfg <- Sim.evalGlobal m (Map.union (beConstMap be) (addlPrims be))
          (bitBlastExtCns ecMap)
          (const Nothing)
+         neutral
   Sim.evalSharedTerm cfg t
 
 bitBlastExtCns ::
@@ -509,11 +514,12 @@ withBitBlastedTerm proxy sc addlPrims t c = AIG.withNewGraph proxy $ \be -> do
 
 asFiniteType :: SharedContext -> Term -> IO FiniteType
 asFiniteType sc t =
-  scGetModuleMap sc >>= \modmap ->
-  case asFiniteTypeValue (Concrete.evalSharedTerm modmap Map.empty Map.empty t) of
-    Just ft -> return ft
-    Nothing ->
-      fail $ "asFiniteType: unsupported type " ++ scPrettyTerm defaultPPOpts t
+  do modmap <- scGetModuleMap sc
+     tm <- Concrete.evalSharedTerm modmap Map.empty Map.empty t
+     case asFiniteTypeValue tm of
+       Just ft -> return ft
+       Nothing ->
+         fail $ "asFiniteType: unsupported type " ++ scPrettyTerm defaultPPOpts t
 
 processVar ::
   (ExtCns Term, FirstOrderType) ->

saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

@@ -37,6 +37,7 @@ import           Data.Char                                     (isDigit)
 import qualified Data.IntMap                                   as IntMap
 import           Data.List                                     (intersperse, sortOn)
 import           Data.Maybe                                    (fromMaybe)
+import qualified Data.Map                                      as Map
 import qualified Data.Set                                      as Set
 import qualified Data.Text                                     as Text
 import           Prelude                                       hiding (fail)
@@ -217,19 +218,49 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
     -- TODO: maybe have more customizable translation of data types
     DataTypeApp n is as -> translateIdentWithArgs n (is ++ as)
     CtorApp n is as -> translateIdentWithArgs n (is ++ as)
+
+    RecursorType _d _params motive motiveTy ->
+      -- type of the motive looks like
+      --      (ix1 : _) -> ... -> (ixn : _) -> d ps ixs -> sort
+      -- to get the type of the recursor, we compute
+      --      (ix1 : _) -> ... -> (ixn : _) -> (x:d ps ixs) -> motive ixs x
+      do let (bs, _srt) = asPiList motiveTy
+         (varsT,bindersT) <- unzip <$>
+           (forM bs $ \ (b, bType) -> do
+             bTypeT <- translateTerm bType
+             b' <- freshenAndBindName b
+             return (Coq.Var b', Coq.PiBinder (Just b') bTypeT))
+
+         motiveT <- translateTerm motive
+         let bodyT = Coq.App motiveT varsT
+         return $ Coq.Pi bindersT bodyT
+
     -- TODO: support this next!
-    RecursorApp d parameters motive eliminators indices termEliminated ->
+    Recursor (CompiledRecursor d parameters motive _motiveTy eliminators elimOrder) ->
       do maybe_d_trans <- translateIdentToIdent d
          rect_var <- case maybe_d_trans of
            Just i -> return $ Coq.Var (show i ++ "_rect")
            Nothing ->
              errorTermM ("Recursor for " ++ show d ++
                          " cannot be translated because the datatype " ++
                          "is mapped to an arbitrary Coq term")
-         let args =
-               parameters ++ [motive] ++ map snd eliminators
-               ++ indices ++ [termEliminated]
-         Coq.App rect_var <$> mapM translateTerm args
+
+         let fnd c = case Map.lookup c eliminators of
+                       Just (e,_ety) -> translateTerm e
+                       Nothing -> errorTermM
+                          ("Recursor eliminator missing eliminator for constructor " ++ show c)
+
+         ps <- mapM translateTerm parameters
+         m  <- translateTerm motive
+         elimlist <- mapM fnd elimOrder
+
+         pure (Coq.App rect_var (ps ++ [m] ++ elimlist))
+
+    RecursorApp rec indices termEliminated ->
+      do rec' <- translateTerm rec
+         let args = indices ++ [termEliminated]
+         Coq.App rec' <$> mapM translateTerm args
+
     Sort s -> pure (Coq.Sort (translateSort s))
     NatLit i -> pure (Coq.NatLit (toInteger i))
     ArrayValue (asBoolType -> Just ()) (traverse asBool -> Just bits)