Add stubs for new cryptol float primitives to cryptol-saw-core.

This adapts cryptol-saw-core to GaloisInc/cryptol#1066.

(Note: saw-core PR #158 was intended to adapt to the same cryptol
PR, but missing translations for the new cryptol primitives caused
the cryptol-saw-core test suite to fail. This PR fixes the test
suite failure.)

cryptol-saw-core/saw/Cryptol.sawcore

@@ -1498,15 +1498,41 @@ ecFpMul e p _ _ _ = error (TCFloat e p) "Unimplemented: fpMul";
 ecFpDiv : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpDiv e p _ _ _ = error (TCFloat e p) "Unimplemented: fpDiv";
 
-ecFpIsFinite : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
-ecFpIsFinite e p _ = error Bool "Unimplemented: fpIsFinite";
-
 ecFpToRational : (e : Num) -> (p : Num) -> TCFloat e p -> Rational;
 ecFpToRational e p _ = error Rational "Unimplemented: fpToRational";
 
 ecFpFromRational : (e : Num) -> (p : Num) -> Vec 3 Bool -> Rational -> TCFloat e p;
 ecFpFromRational e p _ _ = error (TCFloat e p) "Unimplemented: fpFromRational";
 
+fpIsNaN : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsNaN e p x = error Bool "Unimplemented: fpIsNaN";
+
+fpIsInf : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsInf e p x = error Bool "Unimplemented: fpIsInf";
+
+fpIsZero : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsZero e p x = error Bool "Unimplemented: fpIsZero";
+
+fpIsNeg : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsNeg e p x = error Bool "Unimplemented: fpIsNeg";
+
+fpIsNormal : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsNormal e p x = error Bool "Unimplemented: fpIsNormal";
+
+fpIsSubnormal : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsSubnormal e p x = error Bool "Unimplemented: fpIsSubnormal";
+
+fpFMA :
+  (e : Num) -> (p : Num) -> Vec 3 Bool ->
+  TCFloat e p -> TCFloat e p -> TCFloat e p -> TCFloat e p;
+fpFMA e p r x y z = error (TCFloat e p) "Unimplemented: fpFMA";
+
+fpAbs : (e : Num) -> (p : Num) -> TCFloat e p -> TCFloat e p;
+fpAbs e p x = error (TCFloat e p) "Unimplemented: fpAbs";
+
+fpSqrt : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p;
+fpSqrt e p r x = error (TCFloat e p) "Unimplemented: fpSqrt";
+
 
 --------------------------------------------------------------------------------
 -- Extra primitives

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

@@ -763,9 +763,17 @@ floatPrims =
   , ("fpSub",          flip scGlobalDef "Cryptol.ecFpSub")
   , ("fpMul",          flip scGlobalDef "Cryptol.ecFpMul")
   , ("fpDiv",          flip scGlobalDef "Cryptol.ecFpDiv")
-  , ("fpIsFinite",     flip scGlobalDef "Cryptol.ecFpIsFinite")
   , ("fpToRational",   flip scGlobalDef "Cryptol.ecFpToRational")
   , ("fpFromRational", flip scGlobalDef "Cryptol.ecFpFromRational")
+  , ("fpIsNaN",        flip scGlobalDef "Cryptol.fpIsNaN")
+  , ("fpIsInf",        flip scGlobalDef "Cryptol.fpIsInf")
+  , ("fpIsZero",       flip scGlobalDef "Cryptol.fpIsZero")
+  , ("fpIsNeg",        flip scGlobalDef "Cryptol.fpIsNeg")
+  , ("fpIsNormal",     flip scGlobalDef "Cryptol.fpIsNormal")
+  , ("fpIsSubnormal",  flip scGlobalDef "Cryptol.fpIsSubnormal")
+  , ("fpFMA",          flip scGlobalDef "Cryptol.fpFMA")
+  , ("fpAbs",          flip scGlobalDef "Cryptol.fpAbs")
+  , ("fpSqrt",         flip scGlobalDef "Cryptol.fpSqrt")
   ]