Comparison predicates added to Agda translation

verification/Examples/PROOF-appendIsAssoc.agda

@@ -28,7 +28,8 @@ append (Cons y z) u = Cons y (append z u)
 
 ---------------------------------------------------------------------------
 
-appendIsAssoc : {a : Set} → (x : List a) → (y : List a) → (z : List a) → (append (append x y) z) ≡ (append x (append y z))
+appendIsAssoc : {a : Set} → (x : List a) → (y : List a) → (z : List a)
+              → (append (append x y) z) ≡ (append x (append y z))
 appendIsAssoc Empty y z = refl
 appendIsAssoc (Cons x xs) y z rewrite appendIsAssoc xs y z = refl
 

verification/ToAgda.curry

@@ -112,6 +112,10 @@ rename4agda allnames qn@(mn,fn)
   | (mn,fn) == pre "False" = "ff"
   | (mn,fn) == nat "Z"     = "zero"
   | (mn,fn) == nat "S"     = "suc"
+  | (mn,fn) == pre "<"     = "_<_"
+  | (mn,fn) == pre ">"     = "_>_"
+  | (mn,fn) == pre "<="    = "_\x2264_"
+  | (mn,fn) == pre ">="    = "_\x2265_"
   | otherwise
   = maybe fn
           (const (showQName qn))

verification/ToVerifier.curry

@@ -18,6 +18,7 @@ import Maybe             (fromJust)
 import SCC               (scc)
 import System            (exitWith, getArgs)
 
+import Rewriting.Files   (showQName)
 import PropertyUsage
 import ToAgda
 import VerifyOptions
@@ -84,6 +85,11 @@ generateTheorem opts qpropname = do
   let alltypenames = foldr union []
                            (map (\fd -> tconsOfType (funcType fd)) allfuncs)
   alltypes <- getAllTypeDecls opts allprogs alltypenames []
+  when (optVerb opts > 2) $ do
+    putStrLn $ "Theorem `" ++ snd qpropname ++ "':\nInvolved operations:"
+    putStrLn $ unwords (map (showQName . funcName) allfuncs)
+    putStrLn $ "Involved types:"
+    putStrLn $ unwords (map (showQName . typeName) alltypes)
   case optTarget opts of
     "agda" -> theoremToAgda newopts qpropname allfuncs alltypes
     t      -> error $ "Unknown translation target: " ++ t

verification/VerifyOptions.curry

@@ -52,7 +52,8 @@ defaultOptions  = Options
 -- target verifier.
 isUntranslatedFunc :: QName -> Bool
 isUntranslatedFunc qn =
-  qn `elem` [pre "?", pre "==", pre "+", pre "*", pre "length", pre "map"] ||
+  qn `elem` map pre ["?","==","+","*","<",">","<=",">=","length","map",
+                     "if_then_else"] ||
   fst qn `elem` ["Test.Prop","Test.EasyCheck"]
 
 -- Primitive functions that are not extracted and translated to the verifier.
@@ -71,7 +72,7 @@ options =
            "run quietly (no output, only exit code)"
   , Option "v" ["verbosity"]
             (OptArg (maybe (checkVerb 2) (safeReadNat checkVerb)) "<n>")
-            "verbosity level:\n0: quiet (same as `-q')\n1: show progress (default)\n2: show generated output (same as `-v')\n3: show generated output"
+            "verbosity level:\n0: quiet (same as `-q')\n1: show progress (default)\n2: show generated output (same as `-v')\n3: show more details about translation"
   , Option "p" ["property"]
            (ReqArg addPropName "<n>")
            "name of property to be translated as theorem\n(default: translate all properties in module)"