From fdac6c60e115297a58f5b81da0c4b7f18ac758f2 Mon Sep 17 00:00:00 2001
From: funemy
Date: Tue, 25 Oct 2022 00:14:40 -0700
Subject: symbolic

---
 entries/funemy/symbolic/phib.py | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 entries/funemy/symbolic/phib.py

(limited to 'entries/funemy')

diff --git a/entries/funemy/symbolic/phib.py b/entries/funemy/symbolic/phib.py
new file mode 100644
index 0000000..30d68a8
--- /dev/null
+++ b/entries/funemy/symbolic/phib.py
@@ -0,0 +1,21 @@
+from typing import List
+ 
+def phib(xs: List[int]) -> bool:
+    """
+    Instructions:
+        1. `pip install crosshair-tool`
+        2.  modify the precondition `pre` to control the length of your fib sequence
+        3. run `crosshair check phib.py` in your terminal
+
+    pre: len(xs) >= 10
+    post: __return__ != True
+    """
+    if xs[0] != 0:
+        return False
+    if len(xs) > 1:
+        if xs[1] != 1:
+            return False
+        for i in range(2,len(xs)):
+            if xs[i] != xs[i-1] + xs[i-2]:
+                return False
+        return True
-- 
cgit v1.2.3-70-g09d2


From f6cbd54537b48f6815bf518393c5bc7ac6b2a7bd Mon Sep 17 00:00:00 2001
From: funemy
Date: Tue, 25 Oct 2022 00:16:19 -0700
Subject: minor

---
 entries/funemy/symbolic/phib.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'entries/funemy')

diff --git a/entries/funemy/symbolic/phib.py b/entries/funemy/symbolic/phib.py
index 30d68a8..c6fb23e 100644
--- a/entries/funemy/symbolic/phib.py
+++ b/entries/funemy/symbolic/phib.py
@@ -4,7 +4,7 @@ def phib(xs: List[int]) -> bool:
     """
     Instructions:
         1. `pip install crosshair-tool`
-        2.  modify the precondition `pre` to control the length of your fib sequence
+        2. modify the precondition `pre` to control the length of your fib sequence
         3. run `crosshair check phib.py` in your terminal
 
     pre: len(xs) >= 10
-- 
cgit v1.2.3-70-g09d2


From 2f43aade2ed78389b32fd48598a2bf85ca9fdd9c Mon Sep 17 00:00:00 2001
From: funemy
Date: Tue, 25 Oct 2022 02:13:02 -0700
Subject: a different z3 constraint encoding

---
 entries/funemy/z3/z4fib.sh | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100755 entries/funemy/z3/z4fib.sh

(limited to 'entries/funemy')

diff --git a/entries/funemy/z3/z4fib.sh b/entries/funemy/z3/z4fib.sh
new file mode 100755
index 0000000..97ae59b
--- /dev/null
+++ b/entries/funemy/z3/z4fib.sh
@@ -0,0 +1,40 @@
+#!/bin/bash
+# z3 fib, but better
+
+# Instructions:
+#  1. having z3 installed and put under your $PATH
+#  2. making sure z4fib.sh is executable, by `chmod +x z3fib.sh`
+#  3. running as `./z4fib.sh [length of the fib sequence]`
+#  4. having fun :)
+
+if [ -e fib.smt2 ]
+then
+    rm -f fib.smt2
+    touch fib.smt2
+else
+    touch fib.smt2
+fi
+
+if [ "$1" -lt "0" ]; then
+  echo "Argument must be larger than 0."
+  exit 1
+fi
+
+echo "(declare-const fib (Seq Int))" >> fib.smt2
+echo "" >> fib.smt2
+echo "(assert" >> fib.smt2
+echo "  (and" >> fib.smt2
+echo "    (= (seq.len fib) $1)" >> fib.smt2
+echo "    (= (seq.nth fib 0) 0)" >> fib.smt2
+echo "    (= (seq.nth fib 1) 1)" >> fib.smt2
+echo "    (forall ((i Int))" >> fib.smt2
+echo "      (=> (and (> i 1) (< i (seq.len fib)))" >> fib.smt2
+echo "        (= (seq.nth fib i)" >> fib.smt2
+echo "          (+ (seq.nth fib (- i 1))" >> fib.smt2
+echo "            (seq.nth fib (- i 2))))))))" >> fib.smt2
+
+
+echo "(check-sat)" >> fib.smt2
+echo "(get-model)" >> fib.smt2
+
+z3 fib.smt2
-- 
cgit v1.2.3-70-g09d2


From cf530ca49024dbdac4234c52a6838fb209ab6cb6 Mon Sep 17 00:00:00 2001
From: funemy
Date: Tue, 25 Oct 2022 02:18:23 -0700
Subject: when i still have chance to format

---
 entries/funemy/z3/z4fib.sh | 1 +
 1 file changed, 1 insertion(+)

(limited to 'entries/funemy')

diff --git a/entries/funemy/z3/z4fib.sh b/entries/funemy/z3/z4fib.sh
index 97ae59b..b7488e4 100755
--- a/entries/funemy/z3/z4fib.sh
+++ b/entries/funemy/z3/z4fib.sh
@@ -32,6 +32,7 @@ echo "      (=> (and (> i 1) (< i (seq.len fib)))" >> fib.smt2
 echo "        (= (seq.nth fib i)" >> fib.smt2
 echo "          (+ (seq.nth fib (- i 1))" >> fib.smt2
 echo "            (seq.nth fib (- i 2))))))))" >> fib.smt2
+echo "" >> fib.smt2
 
 
 echo "(check-sat)" >> fib.smt2
-- 
cgit v1.2.3-70-g09d2


From 1f35f0d22a4cd0bd837b26e8b019345532da89e6 Mon Sep 17 00:00:00 2001
From: funemy
Date: Tue, 25 Oct 2022 02:21:15 -0700
Subject: minor

---
 entries/funemy/z3/z3fib.sh | 2 +-
 entries/funemy/z3/z4fib.sh | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'entries/funemy')

diff --git a/entries/funemy/z3/z3fib.sh b/entries/funemy/z3/z3fib.sh
index 07ab418..e96226f 100755
--- a/entries/funemy/z3/z3fib.sh
+++ b/entries/funemy/z3/z3fib.sh
@@ -15,7 +15,7 @@ else
 fi
 
 if [ "$1" -lt "0" ]; then
-  echo "Argument must be larger than 0."
+  echo "Argument must be larger or equal to 0."
   exit 1
 fi
 
diff --git a/entries/funemy/z3/z4fib.sh b/entries/funemy/z3/z4fib.sh
index b7488e4..983a752 100755
--- a/entries/funemy/z3/z4fib.sh
+++ b/entries/funemy/z3/z4fib.sh
@@ -16,7 +16,7 @@ else
 fi
 
 if [ "$1" -lt "0" ]; then
-  echo "Argument must be larger than 0."
+  echo "Argument must be larger or equal to 0."
   exit 1
 fi
 
-- 
cgit v1.2.3-70-g09d2


From ae3c469407df59439fb0346344990c0155dcd7a2 Mon Sep 17 00:00:00 2001
From: funemy
Date: Tue, 25 Oct 2022 02:23:05 -0700
Subject: redundant line

---
 entries/funemy/z3/z4fib.sh | 1 -
 1 file changed, 1 deletion(-)

(limited to 'entries/funemy')

diff --git a/entries/funemy/z3/z4fib.sh b/entries/funemy/z3/z4fib.sh
index 983a752..d5ad2d9 100755
--- a/entries/funemy/z3/z4fib.sh
+++ b/entries/funemy/z3/z4fib.sh
@@ -34,7 +34,6 @@ echo "          (+ (seq.nth fib (- i 1))" >> fib.smt2
 echo "            (seq.nth fib (- i 2))))))))" >> fib.smt2
 echo "" >> fib.smt2
 
-
 echo "(check-sat)" >> fib.smt2
 echo "(get-model)" >> fib.smt2
 
-- 
cgit v1.2.3-70-g09d2


From cdec98dc53617c3ad5c297f8f5d127013c111b6d Mon Sep 17 00:00:00 2001
From: funemy
Date: Tue, 25 Oct 2022 12:54:05 -0700
Subject: typo

---
 entries/funemy/z3/z4fib.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'entries/funemy')

diff --git a/entries/funemy/z3/z4fib.sh b/entries/funemy/z3/z4fib.sh
index d5ad2d9..f7a1e48 100755
--- a/entries/funemy/z3/z4fib.sh
+++ b/entries/funemy/z3/z4fib.sh
@@ -3,7 +3,7 @@
 
 # Instructions:
 #  1. having z3 installed and put under your $PATH
-#  2. making sure z4fib.sh is executable, by `chmod +x z3fib.sh`
+#  2. making sure z4fib.sh is executable, by `chmod +x z4fib.sh`
 #  3. running as `./z4fib.sh [length of the fib sequence]`
 #  4. having fun :)
 
-- 
cgit v1.2.3-70-g09d2


From 0269509a887fb154f32b88f5dfbeb883e16f628c Mon Sep 17 00:00:00 2001
From: funemy
Date: Tue, 25 Oct 2022 16:00:17 -0700
Subject: learning new language

---
 entries/funemy/koka/fib.kk | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 entries/funemy/koka/fib.kk

(limited to 'entries/funemy')

diff --git a/entries/funemy/koka/fib.kk b/entries/funemy/koka/fib.kk
new file mode 100644
index 0000000..5b7e66b
--- /dev/null
+++ b/entries/funemy/koka/fib.kk
@@ -0,0 +1,12 @@
+effect fib
+  ctl fib(n : int) : int
+
+fun doFib(inp : int) : div int
+  with ctl fib(n)
+    if n == 0 then 0
+    else if n == 1 then 1
+    else (doFib(n - 1) : int) + doFib(n - 2)
+  fib(inp)
+
+fun main()
+  print(doFib(20))
-- 
cgit v1.2.3-70-g09d2


From a92d2f2a96c36e758291d7150b4ff175ec2ec768 Mon Sep 17 00:00:00 2001
From: funemy
Date: Tue, 25 Oct 2022 16:10:58 -0700
Subject: minor

---
 entries/funemy/.gitignore | 1 +
 people.json               | 4 ++++
 2 files changed, 5 insertions(+)

(limited to 'entries/funemy')

diff --git a/entries/funemy/.gitignore b/entries/funemy/.gitignore
index acb903a..3d2fbd5 100644
--- a/entries/funemy/.gitignore
+++ b/entries/funemy/.gitignore
@@ -1,3 +1,4 @@
 .DS_Store
 *.agdai
 *.smt2
+**/.koka/*
diff --git a/people.json b/people.json
index a9be376..c2db098 100644
--- a/people.json
+++ b/people.json
@@ -87,6 +87,10 @@
             {
                 "name": "symbolic",
                 "link": "./entries/funemy/symbolic/phib.py"
+            },
+            {
+                "name": "koka",
+                "link": "./entries/funemy/koka/fib.kk"
             }
         ]
     },
-- 
cgit v1.2.3-70-g09d2


From 97e2651a917e68b5e59595fe538b97d65f4508e7 Mon Sep 17 00:00:00 2001
From: funemy
Date: Tue, 25 Oct 2022 19:59:44 -0700
Subject: yet another haskell fib

---
 entries/funemy/.gitignore         |  2 ++
 entries/funemy/haskell/morphib.hs | 43 +++++++++++++++++++++++++++++++++++++++
 people.json                       |  4 ++++
 3 files changed, 49 insertions(+)
 create mode 100644 entries/funemy/haskell/morphib.hs

(limited to 'entries/funemy')

diff --git a/entries/funemy/.gitignore b/entries/funemy/.gitignore
index 3d2fbd5..9211bbd 100644
--- a/entries/funemy/.gitignore
+++ b/entries/funemy/.gitignore
@@ -2,3 +2,5 @@
 *.agdai
 *.smt2
 **/.koka/*
+*.hi
+*.o
diff --git a/entries/funemy/haskell/morphib.hs b/entries/funemy/haskell/morphib.hs
new file mode 100644
index 0000000..1fae449
--- /dev/null
+++ b/entries/funemy/haskell/morphib.hs
@@ -0,0 +1,43 @@
+-- Fantastic Morphisms
+newtype Free f = Free {unFree :: f (Free f)}
+
+cata :: Functor f => (f a -> a) -> Free f -> a
+cata phi (Free x) = phi $ fmap (cata phi) x
+
+ana :: Functor f => (a -> f a) -> a -> Free f
+ana phi x = Free $ fmap (ana phi) (phi x)
+
+data FibF a =
+      Fib0
+    | Fib1
+    | FibN a a
+    deriving (Eq, Show)
+
+instance Functor FibF where
+    fmap f Fib0       = Fib0
+    fmap f Fib1       = Fib1
+    fmap f (FibN l r) = FibN (f l) (f r)
+
+type Fib a = Free FibF
+
+gen :: Int -> FibF Int
+gen 0 = Fib0
+gen 1 = Fib1
+gen n = FibN (n-1) (n-2)
+
+interp :: FibF Int -> Int
+interp Fib0       = 0
+interp Fib1       = 1
+interp (FibN l r) = l + r
+
+bif :: Int -> Fib Int
+bif = ana gen
+
+fib' :: Fib Int -> Int
+fib' = cata interp
+
+fib :: Int -> Int
+fib = fib' . bif
+
+main :: IO ()
+main = print (fib 14)
diff --git a/people.json b/people.json
index c2db098..efe917e 100644
--- a/people.json
+++ b/people.json
@@ -88,6 +88,10 @@
                 "name": "symbolic",
                 "link": "./entries/funemy/symbolic/phib.py"
             },
+            {
+                "name": "morphism",
+                "link": "./entries/funemy/haskell/morphib.hs"
+            },
             {
                 "name": "koka",
                 "link": "./entries/funemy/koka/fib.kk"
-- 
cgit v1.2.3-70-g09d2