From 0b5c5982eee021021e7fca48d70fb671cfa889e7 Mon Sep 17 00:00:00 2001
From: Julin S <famubu@rawtext.club>
Date: Sat, 8 Apr 2023 14:18:37 +0530
Subject: [PATCH] [sml] add old sml files

---
 .gitignore      |  5 +++
 sml/README.org  |  4 +++
 sml/fibo.sml    | 19 ++++++++++
 sml/phoas.sml   | 18 ++++++++++
 sml/reverse.sml | 15 ++++++++
 sml/tree.sml    | 94 +++++++++++++++++++++++++++++++++++++++++++++++++
 6 files changed, 155 insertions(+)
 create mode 100644 sml/README.org
 create mode 100644 sml/fibo.sml
 create mode 100644 sml/phoas.sml
 create mode 100644 sml/reverse.sml
 create mode 100644 sml/tree.sml

diff --git a/.gitignore b/.gitignore
index 7fe0b23..26b8253 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,8 @@
+# Web
+coq/*.html
+coq/*.js
+coq/*.css
+
 # Haskell
 *.hi
 *.o
diff --git a/sml/README.org b/sml/README.org
new file mode 100644
index 0000000..2df4406
--- /dev/null
+++ b/sml/README.org
@@ -0,0 +1,4 @@
+ - fibo.sml: Fibonacci numbers
+ - reverse.sml: Reverse a list
+ - tree.sml: Representing a tree as a type
+ - phoas.sml: PHOAS example
diff --git a/sml/fibo.sml b/sml/fibo.sml
new file mode 100644
index 0000000..34c7009
--- /dev/null
+++ b/sml/fibo.sml
@@ -0,0 +1,19 @@
+(* Fibonacci series:
+
+Val: 1  1  2  3  5  8 13 21 34 55 89
+Idx: 0  1  2  3  4  5  6  7  8  9 10
+*)
+
+fun fibo n =
+  let
+    fun aux a b 0 = a
+      | aux a b n = aux b (a+b) (n-1)
+  in
+    aux 1 1 n
+  end
+
+(*
+sml> fibo 10;
+val it = 89 : int
+*)
+
diff --git a/sml/phoas.sml b/sml/phoas.sml
new file mode 100644
index 0000000..5049f0e
--- /dev/null
+++ b/sml/phoas.sml
@@ -0,0 +1,18 @@
+datatype 'v tm
+  = Var of 'v
+  | App of 'v tm * 'v tm
+  | Abs of 'v -> 'v tm
+		   
+val a = Abs (fn x=>App (Var x, Var x))
+val b = App (a, a)
+
+(* numVars : () tm -> int *)
+fun numVars t =
+  case t of
+    Var v => 1
+  | App (t1, t2) => (numVars t1) + (numVars t2)
+  | Abs f => numVars (f ())
+(* - numVars b; *)
+(* val it = 4 : int *)
+
+
diff --git a/sml/reverse.sml b/sml/reverse.sml
new file mode 100644
index 0000000..bc231ac
--- /dev/null
+++ b/sml/reverse.sml
@@ -0,0 +1,15 @@
+(* Reverse a list in O(n) time *)
+
+fun rev [] = []
+  | rev (x::xs) =
+    let
+      fun aux_rev [] rev = rev
+        | aux_rev (x::xs) rev = aux_rev xs (x::rev)
+    in
+      aux_rev xs [x]
+    end
+
+(*
+sml> rev [3,2,1,0];
+val it = [0,1,2,3] : int list
+*)
diff --git a/sml/tree.sml b/sml/tree.sml
new file mode 100644
index 0000000..ca98700
--- /dev/null
+++ b/sml/tree.sml
@@ -0,0 +1,94 @@
+(*
+10
+| \
+5  15
+|\  | \
+2 6 16 20
+
+5
+|\
+2 10
+  /\
+ 6  15
+    | \
+    16 20
+
+Node(Node(Null, 2, Null), 5, Node( Node(Null, 6, Null), 10, Node(Node(Null, 16, Null), 15, Node(Null, 20, Null))))
+
+
+Node(
+  Node(Empty, 2, Empty),
+  5,
+  Node(
+    Node(Empty, 6, Empty),
+    10,
+    Node(
+      Node(Empty, 16, Empty),
+      15,
+      Node(Empty, 20, Empty),
+    ),
+  )
+)
+
+
+Node(
+  Node(
+    Node(Empty,2,Empty),
+    5,
+    Node(Empty,6,Empty)
+  ),
+  10,
+  Node(
+    Node(Empty,16,Empty),
+    15,
+    Node(Empty,20,Empty)
+  )
+)
+*)
+datatype 'a Tree = Empty
+                 | Node of 'a Tree * 'a * 'a Tree
+
+(*
+  treemap :: ('a -> 'b) -> 'a Tree -> 'b Tree
+*)
+fun treemap f Empty = Empty
+  | treemap f (Node (l, x, r)) = Node (treemap f l, f x, treemap f r)
+(*
+λ> treemap (fn x => x+1) (Node (Empty, 3, Empty));
+val it = Node (Empty,4,Empty) : int Tree
+*)
+
+(*
+  inorder :: 'a Tree -> 'a list
+*)
+fun preorder Empty = []
+  | preorder (Node (l, x, r)) = [x] @ (preorder l) @ (preorder r)
+(*
+λ> preorder(Node (Empty, 3, Empty))
+val it = [3] : int list
+
+λ> preorder (Node( Node( Node(Empty,2,Empty), 5, Node(Empty,6,Empty)), 10, Node( Node(Empty,16,Empty), 15, Node(Empty,20,Empty))))
+= ;
+val it = [10,5,2,6,15,16,20] : int list
+*)
+
+fun postorder Empty = []
+  | postorder (Node (l, x, r)) = (postorder l) @ (postorder r) @ [x]
+(*
+λ> postorder (Node( Node( Node(Empty,2,Empty), 5, Node(Empty,6,Empty)), 10, Node( Node(Empty,16,Empty), 15, Node(Empty,20,Empty))));
+val it = [2,6,5,16,20,15,10] : int list
+*)
+
+fun inorder Empty = []
+  | inorder (Node (l, x, r)) = (inorder l) @ [x] @ (inorder r)
+(*
+λ> inorder (Node( Node( Node(Empty,2,Empty), 5, Node(Empty,6,Empty)), 10, Node( Node(Empty,16,Empty), 15, Node(Empty,20,Empty))));
+val it = [2,5,6,10,16,15,20] : int list
+*)
+
+(*
+  rotClock :: 'a tree -> 'a tree
+*)
+fun rotClock Empty = Empty
+fun rotClock (Node(Empty, x, r)) = Node(Empty, x, r)
+fun rotClock (Node(Node(ll, lx, lr), x, r)) = Node(ll, lx, Node(lr, x, r))