curry2verify examples added

.gitignore

@@ -2,6 +2,7 @@
 *~
 .curry
 Curry_Main_Goal.curry
+*.agdai
 
 # executables
 addtypes/AddTypes

verification/Examples/Double.curry

+import Nat
+import Test.Prop
+
+double x = add x x
+
+coin x = x ? S x
+
+even Z = True
+even (S Z) = False
+even (S (S n)) = even n
+
+theorem'evendoublecoin x = always (even (double (coin x)))
+

verification/Examples/MyList.curry

+import Test.Prop
+
+data List a = Empty | Cons a (List a)
+
+append Empty       ys = ys
+append (Cons x xs) ys = Cons x (append xs ys)
+
+theorem'assoc xs ys zs = append (append xs ys) zs -=- append xs (append ys zs)

verification/Examples/PROOF-assoc.agda

+-- Agda program using the Iowa Agda library
+
+open import bool
+
+module PROOF-assoc
+  (Choice : Set)
+  (choose : Choice → 𝔹)
+  (lchoice : Choice → Choice)
+  (rchoice : Choice → Choice)
+  where
+
+open import eq
+open import bool
+open import nat
+open import list
+open import maybe
+
+---------------------------------------------------------------------------
+-- Translated Curry operations:
+
+data List (a : Set) : Set where
+   Empty : List a
+   Cons : a → List a → List a
+
+append : {a : Set} → List a → List a → List a
+append Empty x = x
+append (Cons y z) u = Cons y (append z u)
+
+---------------------------------------------------------------------------
+
+theorem'assoc : {a : Set} → (x : List a) → (y : List a) → (z : List a) → (append (append x y) z) ≡ (append x (append y z))
+theorem'assoc Empty y z = refl
+theorem'assoc (Cons x xs) y z rewrite theorem'assoc xs y z = refl
+
+---------------------------------------------------------------------------

verification/Examples/PROOF-evendoublecoin.agda

+-- Agda program using the Iowa Agda library
+
+open import bool
+
+module PROOF-evendouble
+  (Choice : Set)
+  (choose : Choice → 𝔹)
+  (lchoice : Choice → Choice)
+  (rchoice : Choice → Choice)
+  where
+
+open import eq
+open import bool
+open import nat
+open import list
+open import maybe
+
+---------------------------------------------------------------------------
+-- Translated Curry operations:
+
+add : ℕ → ℕ → ℕ
+add zero x = x
+add (suc y) z = suc (add y z)
+
+coin : Choice → ℕ → ℕ
+coin c1 x = if choose c1 then x else suc x
+
+double : ℕ → ℕ
+double x = add x x
+
+even : ℕ → 𝔹
+even zero = tt
+even (suc zero) = ff
+even (suc (suc x)) = even x
+
+---------------------------------------------------------------------------
+
+add-suc : ∀ (x y : ℕ) → add x (suc y) ≡ suc (add x y)
+add-suc zero y = refl
+add-suc (suc x) y rewrite add-suc x y = refl
+
+-- auxiliary property for x+x instead of double:
+even-add-x-x : ∀ (x : ℕ) → even (add x x) ≡ tt
+even-add-x-x zero = refl
+even-add-x-x (suc x) rewrite add-suc x x | even-add-x-x x = refl
+
+theorem'evendouble : (c1 : Choice) → (x : ℕ)
+                  → (even (double (coin c1 x))) ≡ tt
+theorem'evendouble c1 x rewrite even-add-x-x (coin c1 x) = refl
+
+---------------------------------------------------------------------------

verification/Examples/PROOF-permlength.agda

+-- Agda program using the Iowa Agda library
+
+open import bool
+
+module PROOF-permlength
+  (Choice : Set)
+  (choose : Choice → 𝔹)
+  (lchoice : Choice → Choice)
+  (rchoice : Choice → Choice)
+  where
+
+open import eq
+open import bool
+open import nat
+open import list
+open import maybe
+
+---------------------------------------------------------------------------
+-- Translated Curry operations:
+
+insert : {a : Set} → Choice → a → 𝕃 a → 𝕃 a
+insert c1 x [] = x :: []
+insert c1 y (z :: u) = if choose c1 then y :: (z :: u) else z :: (insert (lchoice c1) y u)
+
+perm : {a : Set} → Choice → 𝕃 a → 𝕃 a
+perm c1 [] = []
+perm c1 (x :: y) = insert c1 x (perm (lchoice c1) y)
+
+---------------------------------------------------------------------------
+
+insert-inc-length : ∀ {a : Set} → (ch : Choice) (x : a) (xs : 𝕃 a)
+                 → length (insert ch x xs) ≡ suc (length xs)
+insert-inc-length ch x [] = refl
+insert-inc-length ch x (y :: ys) with choose ch
+... | tt = refl
+... | ff rewrite insert-inc-length (lchoice ch) x ys = refl
+
+
+theorem'permlength : {a : Set} → (c1 : Choice) → (x : 𝕃 a) → (length x) ≡ (length (perm c1 x))
+theorem'permlength c1 [] = refl
+theorem'permlength c1 (x :: xs)
+ rewrite insert-inc-length c1 x (perm (lchoice c1) xs)
+         | theorem'permlength (lchoice c1) xs
+  = refl
+
+---------------------------------------------------------------------------

verification/Examples/Perm.curry

+-- Definition of permutations and theorem about their length
+
+import Test.Prop
+
+insert x []     = [x]
+insert x (y:ys) = (x : y : ys) ? (y : insert x ys)
+
+perm []     = []
+perm (x:xs) = insert x (perm xs)
+
+theorem'permlength xs = length xs <~> length (perm xs)

verification/Examples/test.sh

+#!/bin/sh
+# Shell script to test the current set of examples
+
+CURRYBIN="../../../bin"
+
+ALLTESTS="Double MyList Perm"
+
+VERBOSE=no
+if [ "$1" = "-v" ] ; then
+  VERBOSE=yes
+fi
+
+# use the right Curry system for the tests:
+PATH=$CURRYBIN:$PATH
+export PATH
+
+LOGFILE=xxx$$
+
+# clean up before
+$CURRYBIN/cleancurry
+rm -f TO-PROVE-* $LOGFILE
+
+# execute all tests:
+# Check whether the Agda compiler compiles the generated programs.
+AGDA=`which agda`
+AGDAIMPORTS="-i . -i /home/mh/home/languages_systems/agda/ial -i /usr/share/agda-stdlib"
+AGDAOPTS="--allow-unsolved-metas"
+
+if [ -z "$AGDA" ] ; then
+  echo "WARNING: cannot check curry2verify ('agda' not found)"
+  exit
+fi
+
+for CP in $ALLTESTS ; do
+  if [ $VERBOSE = yes ] ; then
+    $CURRYBIN/curry2verify $CP
+    $AGDA $AGDAIMPORTS $AGDAOPTS TO-PROVE-*
+    if [ $? -gt 0 ] ; then
+      exit 1
+    fi
+  else
+    $CURRYBIN/curry2verify $CP >> $LOGFILE 2>&1
+    $AGDA $AGDAIMPORTS $AGDAOPTS TO-PROVE-* >> $LOGFILE 2>&1
+    if [ $? -gt 0 ] ; then
+      echo "ERROR in curry2verify:"
+      cat $LOGFILE
+      exit 1
+    fi
+  fi
+  /bin/rm TO-PROVE-*
+done
+
+################ end of tests ####################
+# Clean:
+$CURRYBIN/cleancurry

verification/ToAgda.curry

@@ -34,12 +34,17 @@ theoremToAgda opts qtheoname allfuncs alltypes = do
          partition (\ (fn,_,_) -> isTheoremName (snd (readQN fn))) typedrules
       theoname = fromTheoremName (snd qtheoname)
       mname = "TO-PROVE-" ++ theoname
-      agdaprog = agdaHeader mname ++
-                 unlines (map typeDeclAsAgda alltypes) ++
-                 unlines (map (\ (fn,te,trs) ->
+      hrule = take 75 (repeat '-')
+      agdaprog = unlines $
+                  agdaHeader mname ++
+                  [hrule, "-- Translated Curry operations:",""] ++
+                  map typeDeclAsAgda alltypes ++
+                  map (\ (fn,te,trs) ->
                                   showTypedTRSAsAgda opts rename fn te trs)
-                              funcrules) ++
-                 unlines (map (theoremAsAgda rename) theorules)
+                      funcrules ++
+                  [hrule, ""] ++
+                  map (theoremAsAgda rename) theorules ++
+                  [hrule]
   --putStr agdaprog
   let agdafile = mname ++ ".agda"
   when (optVerb opts > 1 || not (optStore opts)) $ putStr agdaprog
@@ -49,8 +54,8 @@ theoremToAgda opts qtheoname allfuncs alltypes = do
      "Agda module '" ++ agdafile ++ "' written.\n" ++
      "If you completed the proof, rename it to 'PROOF-" ++ theoname ++ ".agda'."
 
-agdaHeader :: String -> String
-agdaHeader mname = unlines $
+agdaHeader :: String -> [String]
+agdaHeader mname =
   [ "-- Agda program using the Iowa Agda library\n"
   , "open import bool\n"
   , "module " ++ mname