changed the translation of large integer literals to use Coq's Z type

GaloisInc · Dec 1, 2021 · 966ab60 · 966ab60
1 parent 2bdc607
commit 966ab60
Showing 1 changed file with 5 additions and 1 deletion.
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 > 20 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)