Merge pull request #1530 from GaloisInc/saw-core-coq/efficient-arrays…

…-int-lits Coq translator: efficient array and integer literals
GaloisInc · Dec 3, 2021 · d8d4776 · d8d4776
2 parents 6bb79b6 + 668f357
commit d8d4776
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 9 deletions.
diff --git a/saw-core-coq/src/Language/Coq/Pretty.hs b/saw-core-coq/src/Language/Coq/Pretty.hs
@@ -133,7 +133,11 @@ ppTerm p e =
       parensIf (p > PrecLambda)
       (ppTerm PrecApp tm <+> text ":" <+> ppTerm PrecApp tp)
     NatLit i ->
-      integer i
+      if i > 1000 then
+        -- Explicitly convert from Z if an integer is too big
+        parensIf (p > PrecLambda) (text "Z.to_nat" <+> integer i <> text "%Z")
+      else
+        integer i
     ZLit i ->
       -- we use hex unless our integer is a positive or negitive digit
       if abs i > 9  then let ui = toInteger (fromInteger i :: Word64)

diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
@@ -46,7 +46,7 @@ import           Prettyprinter
 import           Data.Parameterized.Pair
 import           Data.Parameterized.NatRepr
 import qualified Data.BitVector.Sized                          as BV
-import qualified Data.Vector                                   as Vector (reverse, toList)
+import qualified Data.Vector                                   as Vector (toList)
 import qualified Language.Coq.AST                              as Coq
 import qualified Language.Coq.Pretty                           as Coq
 import           Verifier.SAW.Recognizer
@@ -290,13 +290,8 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
           return (Coq.App (Coq.Var "intToBv")
                   [Coq.NatLit (intValue w), Coq.ZLit (BV.asSigned w bv)])
     ArrayValue _ vec -> do
-      let addElement accum element = do
-            elementTerm <- translateTerm element
-            return (Coq.App (Coq.Var "Vector.cons")
-                    [Coq.Var "_", elementTerm, Coq.Var "_", accum]
-                   )
-        in
-        foldM addElement (Coq.App (Coq.Var "Vector.nil") [Coq.Var "_"]) (Vector.reverse vec)
+      elems <- Vector.toList <$> mapM translateTerm vec
+      return (Coq.App (Coq.Var "Vector.of_list") [Coq.List elems])
     StringLit s -> pure (Coq.Scope (Coq.StringLit (Text.unpack s)) "string")
 
     ExtCns ec ->