From 352b2973fafcd87d0448b176f40afa5f5cc35b63 Mon Sep 17 00:00:00 2001
From: logicmoo <logicmoo@gmail.com>
Date: Tue, 3 Dec 2024 03:07:41 -0800
Subject: [PATCH] testing updates

---
 .gitignore                                    |   1 +
 .../00a_lang_compiled_case.metta.answers      |  15 -
 .../direct_comp/add_atom_match.metta.answers  |   6 -
 .../compiler_walkthru.metta.answers           |  15 -
 .../direct_comp/define_if_like.metta.answers  |   9 -
 tests/direct_comp/easy/efail.metta            |   1 +
 tests/direct_comp/morph/add_atom_match.metta  |  17 ++
 tests/direct_comp/morph/and_or.metta          |   9 +
 tests/direct_comp/morph/collapse.metta        |   2 +
 tests/direct_comp/morph/factorial.metta       |  17 ++
 tests/direct_comp/morph/hyperpose.metta       |  37 +++
 tests/direct_comp/morph/identity.metta        |   4 +
 tests/direct_comp/morph/if.metta              |   4 +
 .../morph/let_superpose_if_case.metta         |  24 ++
 .../morph/let_superpose_list.metta            |  10 +
 .../morph/let_superpose_list2.metta           |   9 +
 tests/direct_comp/morph/letlet.metta          |   3 +
 tests/direct_comp/morph/match_feval.metta     |   3 +
 .../morph/match_superposed_spaces.metta       |  19 ++
 tests/direct_comp/morph/match_void.metta      |  29 ++
 tests/direct_comp/morph/multifunction.metta   |   9 +
 .../direct_comp/morph/nested_parameters.metta |   4 +
 tests/direct_comp/morph/peano.metta           |   4 +
 .../direct_comp/morph/sequential_nested.metta |  26 ++
 tests/direct_comp/morph/states_spaces.metta   |  12 +
 tests/direct_comp/morph/supercollapse.metta   |  38 +++
 .../direct_comp/morph/superpose_nested.metta  |   4 +
 tests/direct_comp/morph/types.metta           |   4 +
 tests/direct_comp/morph/types2.metta          |  15 +
 tests/direct_comp/morph/types3.metta          |  19 ++
 tests/direct_comp/morph/zeroargs.metta        |   4 +
 tests/direct_comp/peasy/_e2_states_dia.metta  |  68 +++++
 tests/direct_comp/peasy/a1_symbols.metta      |  69 +++++
 tests/direct_comp/peasy/a2_opencoggy.metta    |  35 +++
 tests/direct_comp/peasy/a3_twoside.metta      |  52 ++++
 .../peasy/b0_chaining_prelim.metta            |  57 ++++
 tests/direct_comp/peasy/b1_equal_chain.metta  |  70 +++++
 tests/direct_comp/peasy/b2_backchain.metta    |  99 +++++++
 tests/direct_comp/peasy/b3_direct.metta       |  48 ++++
 tests/direct_comp/peasy/b4_nondeterm.metta    | 130 +++++++++
 tests/direct_comp/peasy/b5_types_prelim.metta | 261 ++++++++++++++++++
 .../direct_comp/peasy/c1_grounded_basic.metta | 172 ++++++++++++
 tests/direct_comp/peasy/c2_spaces.metta       |  58 ++++
 tests/direct_comp/peasy/c2_spaces_kb.metta    |  18 ++
 tests/direct_comp/peasy/c3_pln_stv.metta      | 104 +++++++
 tests/direct_comp/peasy/d1_gadt.metta         |  98 +++++++
 tests/direct_comp/peasy/d2_higherfunc.metta   | 237 ++++++++++++++++
 tests/direct_comp/peasy/d3_deptypes.metta     |  75 +++++
 tests/direct_comp/peasy/d4_type_prop.metta    | 171 ++++++++++++
 tests/direct_comp/peasy/d5_auto_types.metta   |  65 +++++
 tests/direct_comp/peasy/e1_kb_write.metta     |  34 +++
 tests/direct_comp/peasy/e2_states.metta       |  99 +++++++
 tests/direct_comp/peasy/e3_match_states.metta |  61 ++++
 tests/direct_comp/peasy/f1_imports.metta      | 120 ++++++++
 tests/direct_comp/peasy/f1_moduleA.metta      |  17 ++
 tests/direct_comp/peasy/f1_moduleB.metta      |   7 +
 tests/direct_comp/peasy/f1_moduleC.metta      |   9 +
 tests/direct_comp/peasy/g1_docs.metta         | 117 ++++++++
 .../00a_lang_compiled_case.metta              |   0
 .../{ => previous}/add_atom_match.metta       |   0
 .../{ => previous}/compiler_walkthru.metta    |   0
 .../{ => previous}/define_if_like.metta       |   0
 ...gs_ordered.metta => mqueens_ordered.metta} |   4 +-
 ...ered.metta.pl => mqueens_ordered.metta.md} |  34 ++-
 ...ead.pl => mqueens_ordered_low_overhead.pl} |   0
 .../compare_algo/nqueens/n_queens.pl          |  72 +++++
 .../nqueens/n_queens_clpfd_sics.pl            |  81 ++++++
 .../compare_algo/nqueens/nqueens_compiled.pl  | 163 +++++++++++
 .../nqueens/nqueens_compiled_sics.pl          | 160 +++++++++++
 .../nqueens/nqueens_test_in_java.sh           |  89 ++++++
 70 files changed, 3269 insertions(+), 58 deletions(-)
 delete mode 100644 tests/direct_comp/00a_lang_compiled_case.metta.answers
 delete mode 100644 tests/direct_comp/add_atom_match.metta.answers
 delete mode 100644 tests/direct_comp/compiler_walkthru.metta.answers
 delete mode 100644 tests/direct_comp/define_if_like.metta.answers
 create mode 100644 tests/direct_comp/easy/efail.metta
 create mode 100755 tests/direct_comp/morph/add_atom_match.metta
 create mode 100755 tests/direct_comp/morph/and_or.metta
 create mode 100755 tests/direct_comp/morph/collapse.metta
 create mode 100755 tests/direct_comp/morph/factorial.metta
 create mode 100644 tests/direct_comp/morph/hyperpose.metta
 create mode 100755 tests/direct_comp/morph/identity.metta
 create mode 100755 tests/direct_comp/morph/if.metta
 create mode 100755 tests/direct_comp/morph/let_superpose_if_case.metta
 create mode 100755 tests/direct_comp/morph/let_superpose_list.metta
 create mode 100755 tests/direct_comp/morph/let_superpose_list2.metta
 create mode 100755 tests/direct_comp/morph/letlet.metta
 create mode 100755 tests/direct_comp/morph/match_feval.metta
 create mode 100755 tests/direct_comp/morph/match_superposed_spaces.metta
 create mode 100755 tests/direct_comp/morph/match_void.metta
 create mode 100755 tests/direct_comp/morph/multifunction.metta
 create mode 100755 tests/direct_comp/morph/nested_parameters.metta
 create mode 100755 tests/direct_comp/morph/peano.metta
 create mode 100755 tests/direct_comp/morph/sequential_nested.metta
 create mode 100755 tests/direct_comp/morph/states_spaces.metta
 create mode 100755 tests/direct_comp/morph/supercollapse.metta
 create mode 100755 tests/direct_comp/morph/superpose_nested.metta
 create mode 100755 tests/direct_comp/morph/types.metta
 create mode 100755 tests/direct_comp/morph/types2.metta
 create mode 100755 tests/direct_comp/morph/types3.metta
 create mode 100755 tests/direct_comp/morph/zeroargs.metta
 create mode 100644 tests/direct_comp/peasy/_e2_states_dia.metta
 create mode 100755 tests/direct_comp/peasy/a1_symbols.metta
 create mode 100644 tests/direct_comp/peasy/a2_opencoggy.metta
 create mode 100644 tests/direct_comp/peasy/a3_twoside.metta
 create mode 100644 tests/direct_comp/peasy/b0_chaining_prelim.metta
 create mode 100644 tests/direct_comp/peasy/b1_equal_chain.metta
 create mode 100644 tests/direct_comp/peasy/b2_backchain.metta
 create mode 100644 tests/direct_comp/peasy/b3_direct.metta
 create mode 100644 tests/direct_comp/peasy/b4_nondeterm.metta
 create mode 100755 tests/direct_comp/peasy/b5_types_prelim.metta
 create mode 100644 tests/direct_comp/peasy/c1_grounded_basic.metta
 create mode 100644 tests/direct_comp/peasy/c2_spaces.metta
 create mode 100644 tests/direct_comp/peasy/c2_spaces_kb.metta
 create mode 100644 tests/direct_comp/peasy/c3_pln_stv.metta
 create mode 100644 tests/direct_comp/peasy/d1_gadt.metta
 create mode 100644 tests/direct_comp/peasy/d2_higherfunc.metta
 create mode 100644 tests/direct_comp/peasy/d3_deptypes.metta
 create mode 100644 tests/direct_comp/peasy/d4_type_prop.metta
 create mode 100644 tests/direct_comp/peasy/d5_auto_types.metta
 create mode 100644 tests/direct_comp/peasy/e1_kb_write.metta
 create mode 100644 tests/direct_comp/peasy/e2_states.metta
 create mode 100644 tests/direct_comp/peasy/e3_match_states.metta
 create mode 100755 tests/direct_comp/peasy/f1_imports.metta
 create mode 100755 tests/direct_comp/peasy/f1_moduleA.metta
 create mode 100644 tests/direct_comp/peasy/f1_moduleB.metta
 create mode 100644 tests/direct_comp/peasy/f1_moduleC.metta
 create mode 100644 tests/direct_comp/peasy/g1_docs.metta
 rename tests/direct_comp/{ => previous}/00a_lang_compiled_case.metta (100%)
 rename tests/direct_comp/{ => previous}/add_atom_match.metta (100%)
 rename tests/direct_comp/{ => previous}/compiler_walkthru.metta (100%)
 rename tests/direct_comp/{ => previous}/define_if_like.metta (100%)
 rename tests/performance/compare_algo/nqueens/{format_args_ordered.metta => mqueens_ordered.metta} (93%)
 rename tests/performance/compare_algo/nqueens/{format_args_ordered.metta.pl => mqueens_ordered.metta.md} (96%)
 rename tests/performance/compare_algo/nqueens/{format_args_ordered_low_overhead.pl => mqueens_ordered_low_overhead.pl} (100%)
 create mode 100644 tests/performance/compare_algo/nqueens/n_queens.pl
 create mode 100644 tests/performance/compare_algo/nqueens/n_queens_clpfd_sics.pl
 create mode 100644 tests/performance/compare_algo/nqueens/nqueens_compiled.pl
 create mode 100644 tests/performance/compare_algo/nqueens/nqueens_compiled_sics.pl
 create mode 100755 tests/performance/compare_algo/nqueens/nqueens_test_in_java.sh

diff --git a/.gitignore b/.gitignore
index 32e2e795b83..503ef697b07 100755
--- a/.gitignore
+++ b/.gitignore
@@ -20,6 +20,7 @@ ftp.flybase.net/**
 venv/
 src/canary-*/
 .*
+*.answers
 *.qlf
 *.datalog
 *-wam.vpw?*
diff --git a/tests/direct_comp/00a_lang_compiled_case.metta.answers b/tests/direct_comp/00a_lang_compiled_case.metta.answers
deleted file mode 100644
index 895d711b0e8..00000000000
--- a/tests/direct_comp/00a_lang_compiled_case.metta.answers
+++ /dev/null
@@ -1,15 +0,0 @@
-[]
-[]
-[]
-[]
-[]
-[]
-[]
-[]
-[]
-[]
-[]
-[]
-[]
-0.14user 0.01system 0:00.15elapsed 99%CPU (0avgtext+0avgdata 28792maxresident)k
-0inputs+0outputs (0major+3286minor)pagefaults 0swaps
diff --git a/tests/direct_comp/add_atom_match.metta.answers b/tests/direct_comp/add_atom_match.metta.answers
deleted file mode 100644
index 82dc0695404..00000000000
--- a/tests/direct_comp/add_atom_match.metta.answers
+++ /dev/null
@@ -1,6 +0,0 @@
-[(Error (assertEqualToResult (sequential ((add-atom GroundingSpace-top (man mortal)) (match GroundingSpace-top ($M mortal) (mortal $M)))) ((mortal man))) 
-Expected: [(mortal man)]
-Got: [(), (mortal man)]
-Excessive result: ())]
-0.04user 0.01system 0:00.06elapsed 87%CPU (0avgtext+0avgdata 33704maxresident)k
-5408inputs+0outputs (31major+3637minor)pagefaults 0swaps
diff --git a/tests/direct_comp/compiler_walkthru.metta.answers b/tests/direct_comp/compiler_walkthru.metta.answers
deleted file mode 100644
index 65ba283991a..00000000000
--- a/tests/direct_comp/compiler_walkthru.metta.answers
+++ /dev/null
@@ -1,15 +0,0 @@
-[(pfcWatch!)]
-[()]
-[()]
-[()]
-[()]
-[()]
-[(load-ontology!)]
-[(-> List)]
-[(function-arity prog-argv)]
-[(Error (assertEqual (function-arity prog-argv) 0) 
-Expected: [0]
-Got: [(function-arity prog-argv)]
-Missed result: 0)]
-0.00user 0.01system 0:00.05elapsed 45%CPU (0avgtext+0avgdata 24816maxresident)k
-24184inputs+0outputs (149major+2923minor)pagefaults 0swaps
diff --git a/tests/direct_comp/define_if_like.metta.answers b/tests/direct_comp/define_if_like.metta.answers
deleted file mode 100644
index 6f68792f2b3..00000000000
--- a/tests/direct_comp/define_if_like.metta.answers
+++ /dev/null
@@ -1,9 +0,0 @@
-[()]
-[()]
-[(), ()]
-[(Error (assertEqual :fail :pass) 
-Expected: [:pass]
-Got: [:fail]
-Missed result: :pass)]
-0.17user 0.00system 0:00.18elapsed 100%CPU (0avgtext+0avgdata 33132maxresident)k
-0inputs+0outputs (0major+3463minor)pagefaults 0swaps
diff --git a/tests/direct_comp/easy/efail.metta b/tests/direct_comp/easy/efail.metta
new file mode 100644
index 00000000000..80ba77548d7
--- /dev/null
+++ b/tests/direct_comp/easy/efail.metta
@@ -0,0 +1 @@
+!(1 (empty) 2)
diff --git a/tests/direct_comp/morph/add_atom_match.metta b/tests/direct_comp/morph/add_atom_match.metta
new file mode 100755
index 00000000000..7abeaa1925c
--- /dev/null
+++ b/tests/direct_comp/morph/add_atom_match.metta
@@ -0,0 +1,17 @@
+
+(: sequential (-> Expression %Undefined%))
+(= (sequential $1) (superpose $1))
+
+; Used to work
+;!(assertEqualToResult
+;  (sequential
+;	( (add-atom &self (man mortal))
+;	  (match &self ($A mortal) (mortal $A))))
+;  ((mortal man)))
+
+!(sequential
+	( (add-atom &self (man mortal))
+	  (match &self ($A mortal) (mortal $A))))
+  
+
+
diff --git a/tests/direct_comp/morph/and_or.metta b/tests/direct_comp/morph/and_or.metta
new file mode 100755
index 00000000000..ae32595b05a
--- /dev/null
+++ b/tests/direct_comp/morph/and_or.metta
@@ -0,0 +1,9 @@
+(: If (-> Bool Atom Atom))
+(= (If True $then) $then)
+(= (If False $then) (let $x 0 (let $x 1 $x)))
+
+(: If (-> Bool Atom Atom Atom))
+(= (If $cond $then $else) (if $cond $then $else))
+
+
+!(If (or (and True False) True) 1 2)
diff --git a/tests/direct_comp/morph/collapse.metta b/tests/direct_comp/morph/collapse.metta
new file mode 100755
index 00000000000..8644485ca39
--- /dev/null
+++ b/tests/direct_comp/morph/collapse.metta
@@ -0,0 +1,2 @@
+!(collapse (1 2 3))
+
diff --git a/tests/direct_comp/morph/factorial.metta b/tests/direct_comp/morph/factorial.metta
new file mode 100755
index 00000000000..866616bf104
--- /dev/null
+++ b/tests/direct_comp/morph/factorial.metta
@@ -0,0 +1,17 @@
+(: If (-> Bool Atom Atom Atom))
+(= (If $cond $then $else) (if $cond $then $else))
+
+(= (facF $n)
+   (If (== $n 0)
+	   1
+	   (* $n (facF (- $n 1)))))
+
+(= (facf $n)
+   (if (== $n 0)
+	   1
+	   (* $n (facf (- $n 1)))))
+
+
+!(facF 10)
+
+!(facf 10)
diff --git a/tests/direct_comp/morph/hyperpose.metta b/tests/direct_comp/morph/hyperpose.metta
new file mode 100644
index 00000000000..23bccbb0dfa
--- /dev/null
+++ b/tests/direct_comp/morph/hyperpose.metta
@@ -0,0 +1,37 @@
+(: If (-> Bool Atom Atom))
+(= (If True $then) $then)
+(= (If False $then) (let $x 0 (let $x 1 $x)))
+
+(: If (-> Bool Atom Atom Atom))
+(= (If $cond $then $else) (if $cond $then $else))
+
+
+!(assertEqual (hyperpose (1 2)) (superpose (1 2)))
+
+!(assertEqual (hyperpose (1 (If (== 1 2) 1)))
+  (superpose  (1 (If (== 1 2) 1))))
+
+!(assertEqual (hyperpose ((If (== 1 2) 1) 1))
+  (superpose  ((If (== 1 2) 1) 1)))
+
+!(assertEqual (hyperpose (1 2 3))
+  (superpose  (1 2 3)))
+
+!(assertEqual (hyperpose ((If (== 1 2) 1) 2 3))
+  (superpose  ((If (== 1 2) 1) 2 3)))
+
+!(assertEqual (hyperpose (1 (If (== 1 2) 1) 3))
+  (superpose  (1 (If (== 1 2) 1) 3)))
+
+!(assertEqual (hyperpose (1 2 (If (== 1 2) 1)))
+  (superpose  (1 2 (If (== 1 2) 1))))
+
+!(assertEqual (hyperpose (1 (If (== 1 2) 1) (If (== 1 2) 1)))
+  (superpose  (1 (If (== 1 2) 1) (If (== 1 2) 1))))
+
+!(assertEqual (hyperpose (1 2 3 4))
+  (superpose  (1 2 3 4)))
+
+!(assertEqual (hyperpose ((1 2) (3 4)))
+  (superpose  ((1 2) (3 4))))
+
diff --git a/tests/direct_comp/morph/identity.metta b/tests/direct_comp/morph/identity.metta
new file mode 100755
index 00000000000..400ba82fbf9
--- /dev/null
+++ b/tests/direct_comp/morph/identity.metta
@@ -0,0 +1,4 @@
+(= (f $x) (* $x $x))
+
+!(f 1)
+
diff --git a/tests/direct_comp/morph/if.metta b/tests/direct_comp/morph/if.metta
new file mode 100755
index 00000000000..7abccc7e601
--- /dev/null
+++ b/tests/direct_comp/morph/if.metta
@@ -0,0 +1,4 @@
+(: If (-> Bool Atom Atom Atom))
+(= (If $cond $then $else) (if $cond $then $else))
+
+!(If (> 1 2) (3 4) (5 6))
diff --git a/tests/direct_comp/morph/let_superpose_if_case.metta b/tests/direct_comp/morph/let_superpose_if_case.metta
new file mode 100755
index 00000000000..b9aec4ca184
--- /dev/null
+++ b/tests/direct_comp/morph/let_superpose_if_case.metta
@@ -0,0 +1,24 @@
+(: If (-> Bool Atom Atom))
+(= (If True $then) $then)
+(= (If False $then) (let $x 0 (let $x 1 $x)))
+
+(: If (-> Bool Atom Atom Atom))
+(= (If $cond $then $else) (if $cond $then $else))
+
+(= (f $x) 42)
+
+!(let $y (superpose (3 4 5))
+      (If (> $y 3)
+          (case (1 $y)
+	               (((1 3) (f 0))
+                        ((1 4) (42 42))
+                        ($else (1 1))))))
+
+!(assertEqualToResult
+   (let $y (superpose (3 4 5))
+      (If (> $y 3)
+          (case (1 $y) (((1 3) (f 0))
+                        ((1 4) (42 42))
+                       ($else (1 1))))))
+     ((42 42) (1 1)))
+
diff --git a/tests/direct_comp/morph/let_superpose_list.metta b/tests/direct_comp/morph/let_superpose_list.metta
new file mode 100755
index 00000000000..b57743043f7
--- /dev/null
+++ b/tests/direct_comp/morph/let_superpose_list.metta
@@ -0,0 +1,10 @@
+(= (wuza $x)
+   (let* (($y (* 2 $x))
+          ($z (superpose (4 5))))
+          ($y $z)))
+
+!(wuza 5)
+
+!(assertEqual
+  (wuza 5)
+  (superpose ((10 4) (10 5))))
diff --git a/tests/direct_comp/morph/let_superpose_list2.metta b/tests/direct_comp/morph/let_superpose_list2.metta
new file mode 100755
index 00000000000..cb1d2f84751
--- /dev/null
+++ b/tests/direct_comp/morph/let_superpose_list2.metta
@@ -0,0 +1,9 @@
+(= (wuzaL $x $L)
+   (let* (($y (* 2 $x))
+            ($z (superpose $L)))
+        ($y $z)))
+
+
+!(assertEqual
+  (wuzaL 2 (3 4))
+  (superpose ((4 3)(4 4))))
diff --git a/tests/direct_comp/morph/letlet.metta b/tests/direct_comp/morph/letlet.metta
new file mode 100755
index 00000000000..329d9750980
--- /dev/null
+++ b/tests/direct_comp/morph/letlet.metta
@@ -0,0 +1,3 @@
+!(let $T (1.0 0.9)
+      (let* ((($f1 $c1) $T))
+            ($f1 $c1)))
diff --git a/tests/direct_comp/morph/match_feval.metta b/tests/direct_comp/morph/match_feval.metta
new file mode 100755
index 00000000000..b53e677cbd4
--- /dev/null
+++ b/tests/direct_comp/morph/match_feval.metta
@@ -0,0 +1,3 @@
+(= (f $x) (* 2 $x))
+
+!(match &self (= (f $x) $y) $y)
diff --git a/tests/direct_comp/morph/match_superposed_spaces.metta b/tests/direct_comp/morph/match_superposed_spaces.metta
new file mode 100755
index 00000000000..a7967792813
--- /dev/null
+++ b/tests/direct_comp/morph/match_superposed_spaces.metta
@@ -0,0 +1,19 @@
+!(bind! &attentional_focus (new-space))
+!(add-atom &attentional_focus 1)
+!(bind! &concepts (new-space))
+!(add-atom &concepts 2)
+
+;; check they are added
+!(assertEqualToResult
+  (match &attentional_focus $1 $1)
+   (1))
+
+!(assertEqualToResult
+  (match &concepts $1 $1)
+   (2))
+
+;; check superposing spaces
+!(assertEqualToResult
+   (match (superpose (&attentional_focus &concepts)) $1 $1)
+   (1 2))
+
diff --git a/tests/direct_comp/morph/match_void.metta b/tests/direct_comp/morph/match_void.metta
new file mode 100755
index 00000000000..2a3cfbeedd1
--- /dev/null
+++ b/tests/direct_comp/morph/match_void.metta
@@ -0,0 +1,29 @@
+!(bind! &belief_events (new-space))
+!(bind! &goal_events (new-space))
+!(match &belief_events $1 $1)
+!(add-atom &belief_events belief1)
+!(match &belief_events $1 $1)
+!(case belief1
+    ((%void% 42
+      )))
+!(case (match &belief_events $1 $1)
+    ((%void% 42
+      )))
+!(assertEqualToResult (case (match &belief_events $1 $1)
+    ((belief1 yes) (%void% 42
+     ))) (yes))
+!(assertEqualToResult (case (match &goal_events $1 $1)
+   ((%void% 42
+   ))) (42))
+!(assertEqualToResult (case (match &goal_events $1 $1)
+  ((goal1 yes)
+    (%void%
+      42))) (42))
+!(add-atom &goal_events goal1)
+!(assertEqualToResult (case (match &goal_events $1 $1)
+   ((goal1 yes) (%void%
+     42))) (yes))
+!(assertEqualToResult (case (match &goal_events $1 $1) ((
+  %void% 42
+  ))) ())
+
diff --git a/tests/direct_comp/morph/multifunction.metta b/tests/direct_comp/morph/multifunction.metta
new file mode 100755
index 00000000000..5339a28aed6
--- /dev/null
+++ b/tests/direct_comp/morph/multifunction.metta
@@ -0,0 +1,9 @@
+(= (g $x) $x)
+(= (g $x) (* 2 $x))
+(= (g test ($y $z)) (* (* 1 $y) $z))
+(= (g 3 ($y $z)) (* $y $z))
+(= (g $x ($y $z)) (* (* $x $y) 42))
+(= (g $x ($y $z)) (* (* 42 $x) $y))
+(= (g a ($y w)) $y)
+
+!(g 42 (1 2))
diff --git a/tests/direct_comp/morph/nested_parameters.metta b/tests/direct_comp/morph/nested_parameters.metta
new file mode 100755
index 00000000000..8fc962d5914
--- /dev/null
+++ b/tests/direct_comp/morph/nested_parameters.metta
@@ -0,0 +1,4 @@
+(= (Truth_Deduction ($f1 $c1) ($f2 $c2))
+   ((* $f1 $f2) (* (* $f1 $f2) (* $c1 $c2))))
+
+!(Truth_Deduction (1.0 0.9) (1.0 0.9))
diff --git a/tests/direct_comp/morph/peano.metta b/tests/direct_comp/morph/peano.metta
new file mode 100755
index 00000000000..17a97d8860a
--- /dev/null
+++ b/tests/direct_comp/morph/peano.metta
@@ -0,0 +1,4 @@
+(= (Add $x Z) $x)
+(= (Add $x (S $y)) (Add (S $x) $y))
+
+!(Add (S (S Z)) (S (S (S Z))))
diff --git a/tests/direct_comp/morph/sequential_nested.metta b/tests/direct_comp/morph/sequential_nested.metta
new file mode 100755
index 00000000000..a8629065889
--- /dev/null
+++ b/tests/direct_comp/morph/sequential_nested.metta
@@ -0,0 +1,26 @@
+(: sequential (-> Expression %Undefined%))
+(= (sequential $1) (superpose $1))
+
+(: do (-> Expression %Undefined%))
+(= (do $1) (case $1 ()))
+
+
+
+!(bind! &var (new-state 1))
+(= (increment)
+   (superpose ((do (change-state! &var (+ 1 (get-state &var))))
+               (get-state &var))))
+
+!(sequential ((increment) (increment)))
+!(sequential ((increment) (increment) (increment)))
+!(sequential ((sequential ((increment) (increment) (increment)))))
+!(sequential ((sequential ((increment) (increment) (increment))) (sequential ((increment) (increment) (increment)))))
+!(sequential ((sequential ((increment) (increment) (increment))) (increment) (increment) (increment)))
+!(do (sequential ((sequential ((increment) (increment) (increment))) (increment) (increment) (increment))))
+!(get-state &var)
+!(sequential ((increment)))
+!(increment)
+!(get-state &var)
+!(sequential ((change-state! &var (+ 1 (get-state &var)))))
+!(get-state &var)
+
diff --git a/tests/direct_comp/morph/states_spaces.metta b/tests/direct_comp/morph/states_spaces.metta
new file mode 100755
index 00000000000..a349dd65636
--- /dev/null
+++ b/tests/direct_comp/morph/states_spaces.metta
@@ -0,0 +1,12 @@
+!(bind! &FIFO (new-state 42))
+!(bind! &WU (new-space))
+!(change-state! &FIFO 45)
+!(get-state &FIFO)
+!(add-atom &WU a)
+!(match &WU $1 $1)
+!(add-atom &WU b)
+!(remove-atom &WU a)
+
+!(assertEqual
+  (match &WU $1 $1)
+  (get-atoms &WU))
diff --git a/tests/direct_comp/morph/supercollapse.metta b/tests/direct_comp/morph/supercollapse.metta
new file mode 100755
index 00000000000..c9b7f3f780d
--- /dev/null
+++ b/tests/direct_comp/morph/supercollapse.metta
@@ -0,0 +1,38 @@
+
+
+(: If (-> Bool Atom Atom Atom))
+(= (If $cond $then $else) (if $cond $then $else))
+
+; (: TupleConcat (-> Any Any AnyRet))
+
+(= (TupleConcat $Ev1 $Ev2) 
+  (let ($V1 $V2) ($Ev1 $Ev2)
+		 (collapse (superpose ((superpose $V1) (superpose $V2))))))
+
+!(TupleConcat (a b c) (e f g))
+!(TupleConcat () (e f g))
+!(TupleConcat (a b c) ())
+
+(= (range $K $N)
+   (If (< $K $N)
+       (TupleConcat ($K) (range (+ $K 1) $N))
+       ()))
+
+!(TupleConcat (a b c) (range 1 1))
+
+(unused
+	(pragma! trace-on-exec False)
+	(pragma! trace-on-eval False)
+	(pragma! trace-length 1090)
+	(pragma! stack-max 100))
+
+
+!(range 1 1)
+
+!(range 1 3)
+
+!(range 2 6)
+
+!(range 1 10)
+
+
diff --git a/tests/direct_comp/morph/superpose_nested.metta b/tests/direct_comp/morph/superpose_nested.metta
new file mode 100755
index 00000000000..09c4ea85452
--- /dev/null
+++ b/tests/direct_comp/morph/superpose_nested.metta
@@ -0,0 +1,4 @@
+!(superpose (a b c))
+!(superpose ((superpose (a b c))))
+!(superpose ((superpose (a b c)) (superpose (x y z))))
+!(superpose ((superpose (a b c)) x y z ))
diff --git a/tests/direct_comp/morph/types.metta b/tests/direct_comp/morph/types.metta
new file mode 100755
index 00000000000..75949ceaa59
--- /dev/null
+++ b/tests/direct_comp/morph/types.metta
@@ -0,0 +1,4 @@
+(: f (-> Number Number))
+(= (f $x) $x)
+
+!(f 42)
diff --git a/tests/direct_comp/morph/types2.metta b/tests/direct_comp/morph/types2.metta
new file mode 100755
index 00000000000..f55c10cc1b8
--- /dev/null
+++ b/tests/direct_comp/morph/types2.metta
@@ -0,0 +1,15 @@
+(: Cat Atom)
+(: Lion Cat)
+
+(: reproduce (-> Lion Lion Lion))
+(= (reproduce $x $y) childlion)
+
+(: lion1 Lion)
+(: lion2 Lion)
+!(get-type lion1)
+
+!(reproduce lion1 lion2)
+
+!(get-type Lion)
+!(match &self (: Lion $1) $1)
+!(match &self (: reproduce $1) $1)
diff --git a/tests/direct_comp/morph/types3.metta b/tests/direct_comp/morph/types3.metta
new file mode 100755
index 00000000000..54302df64ae
--- /dev/null
+++ b/tests/direct_comp/morph/types3.metta
@@ -0,0 +1,19 @@
+(: If (-> Bool Atom Atom))
+(= (If True $then) $then)
+(= (If False $then) (let $x 0 (let $x 1 $x)))
+
+(: If (-> Bool Atom Atom Atom))
+(= (If $cond $then $else) (if $cond $then $else))
+
+
+
+
+(GreaterThan 42 21)
+
+(= (EqualOrGreater $x $y)
+   (or (> $x $y) (== $x $y)))
+
+!(match &self (GreaterThan $x $y)
+    (If (and (== (get-type $x) Number) (== (get-type $y) Number))
+        (If (EqualOrGreater $x $y) yay)))
+
diff --git a/tests/direct_comp/morph/zeroargs.metta b/tests/direct_comp/morph/zeroargs.metta
new file mode 100755
index 00000000000..9205137add3
--- /dev/null
+++ b/tests/direct_comp/morph/zeroargs.metta
@@ -0,0 +1,4 @@
+(= (f) 42)
+
+!(z)
+!(f)
diff --git a/tests/direct_comp/peasy/_e2_states_dia.metta b/tests/direct_comp/peasy/_e2_states_dia.metta
new file mode 100644
index 00000000000..70808f4eae3
--- /dev/null
+++ b/tests/direct_comp/peasy/_e2_states_dia.metta
@@ -0,0 +1,68 @@
+; This example rewritten with `case` works (as per 19 Oct 22),
+; but it might not be good as a unit test:
+; - what's going on is not obvious
+; - there might be a better way to implement what the code is doing
+; - processing commands with side effect and empty results and
+;   chaining them might not be idiomatic
+; - it's relatively slow (why? FIXME?)
+
+!(bind! &memory (new-space))
+
+; catching empty results
+(: dood (-> Atom %Undefined%))
+(= (dood $expr)
+   (case $expr
+     (($x $x)
+      (%void% None))))
+
+; `remove-state` will return an empty result if there is no
+; corresponding state in the memory
+(= (remove-state $var)
+   (match &memory (state $var $y)
+         (remove-atom &memory (state $var $y))))
+
+; using `do` assures that the next clause will be executed
+; even if the result of the previous clause is empty
+(= (change-state $var $value)
+   (nop (dood (remove-state $var))
+        (dood (add-atom &memory (state $var $value)))))
+
+(= (get-state $var)
+   (match &memory (state $var $value) $value))
+
+; Earlier, `(get-state (person name))` got cached, and it changes
+; in one equality for `listen` didn't affect other equalities.
+; `case` accepts an `Atom` and forcefully evaluates it.
+; However, the idea of using equalities as sequentially processed
+; rules with side effects is still questionable
+(= (listen (My name is $x))
+   (case (get-state (person name))
+       (($x (Yes, I remember))
+        ; $y cannot be %void%
+        ($y (I thought you are $y)))
+   )
+)
+
+(= (listen (My name is $x))
+   (change-state (person name) $x))
+
+(= (listen $_)
+   (case (get-state greeted)
+      ((%void%
+          (case (get-state (person name))
+                ((%void% (Hi. What is your name?))
+                 ($p-name (Nice to meet you $p-name)))))
+      )
+    )
+)
+
+(= (listen $_)
+   (nop (change-state greeted True)))
+
+;!(listen (Hello))
+;!(listen (My name is Alexey))
+;!(listen (My name is Alexey))
+;!(listen (My name is Ben))
+
+;!(call:get_atoms &memory)
+
diff --git a/tests/direct_comp/peasy/a1_symbols.metta b/tests/direct_comp/peasy/a1_symbols.metta
new file mode 100755
index 00000000000..fb5e14a3043
--- /dev/null
+++ b/tests/direct_comp/peasy/a1_symbols.metta
@@ -0,0 +1,69 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `match` searches for all expressions corresponding to
+; the given pattern and produces the output pattern.
+; It doesn't search in subexpressions.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Some expressions to be matched
+((leaf1 leaf2) leaf3)
+(((leaf0 leaf1) leaf2) leaf3)
+; This one contains `((leaf1 leaf2) leaf3)` as a subexpression
+; and thus will not be matched
+(top ((leaf1 leaf2) leaf3))
+; `assertEqualToResult` checks all the results of the first
+; expression; it doesn't evaluate the second expression,
+; which is treated as a set of expected results.
+!(assertEqualToResult
+  (match &self (($x leaf2) leaf3) $x)
+  (leaf1
+   (leaf0 leaf1)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Symbols can be arranged in arbitrary expressions
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(Sam is a frog)
+(Tom is a cat)
+(Sophia is a robot)
+; `match` can bind more that one variable
+!(assertEqualToResult
+  (match &self ($who is a $what) ($who the $what))
+  ((Sam the frog)
+   (Tom the cat)
+   (Sophia the robot)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; More examples of pattern matching
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `:=` is a custom symbol. These are still purely symbolic expressions
+(:= (Green Sam) T)
+(:= (White Tom) T)
+(:= (Green Tom) F)
+!(assertEqualToResult
+  (match &self (:= (Green $who) T) ($who is really green))
+  ((Sam is really green)))
+!(assertEqualToResult
+  (match &self (:= ($color $who) T) ($who is really $color))
+  ((Sam is really Green)
+   (Tom is really White)))
+!(assertEqualToResult
+  (match &self (:= ($color $who) $tv) (It's $tv that $who is $color))
+  ((It's T that Sam is Green)
+   (It's T that Tom is White)
+   (It's F that Tom is Green)))
+; This type of query works as a sort of evaluation/reduction
+!(assertEqualToResult
+  (match &self (:= (Green Tom) $tv) $tv)
+  (F))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; One more example
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(isa red color)
+(isa green color)
+(isa blue color)
+!(assertEqualToResult
+  (match &self (isa $color color) $color)
+  (red green blue))
diff --git a/tests/direct_comp/peasy/a2_opencoggy.metta b/tests/direct_comp/peasy/a2_opencoggy.metta
new file mode 100644
index 00000000000..7376689ef29
--- /dev/null
+++ b/tests/direct_comp/peasy/a2_opencoggy.metta
@@ -0,0 +1,35 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; We can use Nodes and Links in the OpenCog Classic style,
+; because these are also symbolic expressions,
+; although Concept and List will not be turned into types
+; and will remain just symbols in expressions
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(EvaluationLink
+  (PredicateNode "eats")
+  (ListLink
+     (ConceptNode "Sam")
+     (ConceptNode "flies")))
+
+(EvaluationLink
+  (PredicateNode "eats")
+  (ListLink
+     (ConceptNode "Bill")
+     (ConceptNode "pizza")))
+
+(EvaluationLink
+  (PredicateNode "eats")
+  (ListLink
+     (ConceptNode "Fritz")
+     (ConceptNode "flies")))
+
+!(assertEqualToResult
+  (match &self
+    (EvaluationLink
+      (PredicateNode "eats")
+        (ListLink
+          $x
+          (ConceptNode "flies")))
+     $x)
+  ((ConceptNode "Sam")
+   (ConceptNode "Fritz")))
diff --git a/tests/direct_comp/peasy/a3_twoside.metta b/tests/direct_comp/peasy/a3_twoside.metta
new file mode 100644
index 00000000000..da1773abc21
--- /dev/null
+++ b/tests/direct_comp/peasy/a3_twoside.metta
@@ -0,0 +1,52 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Variables can appear in knowledge base entries
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(implies (Frog $x) (Green $x))
+(implies (Frog $x) (Eats-flies $x))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Bound variables on both sides will be substituted
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+  (match &self
+    (implies (Frog Sam) $what)
+    $what)
+  ((Green Sam)
+   (Eats-flies Sam)))
+
+!(assertEqualToResult
+  (match &self
+    (implies ($P $x) (Green Sam))
+    ($x might be $P))
+  ((Sam might be Frog)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Composite queries
+; The comma is used to form a conjunction of queries with shared
+; variables, which should be satisfied simultaneously.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Some facts
+(Frog Sam)
+(Robot Sophia)
+
+!(assertEqualToResult
+  (match &self
+    (, (Frog $x)
+       (implies (Frog $x) $y))
+    $y)
+  ((Green Sam)
+   (Eats-flies Sam)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Variables in queries can remain unbound
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+  (match &self
+    (, (implies ($P $x) (Green $x))
+       (implies ($P $x) (Eats-flies $x)))
+    (Then it is definitely $P))
+  ((Then it is definitely Frog)))
diff --git a/tests/direct_comp/peasy/b0_chaining_prelim.metta b/tests/direct_comp/peasy/b0_chaining_prelim.metta
new file mode 100644
index 00000000000..210f758c285
--- /dev/null
+++ b/tests/direct_comp/peasy/b0_chaining_prelim.metta
@@ -0,0 +1,57 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; From matching to evaluation of expressions via equality queries chaining
+; It's possible to chain together matching queries
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Some knowledge base entries
+; `:=` is a custom symbol
+; Combinatory logic rules
+(:= (I $x) $x)
+(:= ((K $x) $y) $x)
+(:= (K $x $y) $x)
+(:= (S $x $y $z) ($x $z ($y $z)))
+
+; A single matching step
+!(assertEqualToResult
+  (match &self
+    (:= (S K K x) $r)
+    $r)
+  ((K x (K x))))
+
+; A second matching step; the result of the previous
+; step is manually used as input for the next query
+!(assertEqualToResult
+  (match &self
+    (:= (K x (K x)) $r)
+    $r)
+  (x))
+
+; Combined reduction via matching in two steps
+!(assertEqualToResult
+  (match &self
+    (:= (S K K x) $r)
+    (match &self (:= $r $r2)
+      $r2))
+  (x))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Another example (Peano summation)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(:= (Add $x Z) $x)
+(:= (Add $x (S $y)) (Add (S $x) $y))
+
+; First step
+!(assertEqualToResult
+  (match &self
+    (:= (Add (S Z) (S Z)) $r)
+    $r)
+  ((Add (S (S Z)) Z)))
+
+; Two steps together
+!(assertEqualToResult
+  (match &self
+    (:= (Add (S Z) (S Z)) $r)
+    (match &self (:= $r $r2)
+      $r2))
+  ((S (S Z))))
diff --git a/tests/direct_comp/peasy/b1_equal_chain.metta b/tests/direct_comp/peasy/b1_equal_chain.metta
new file mode 100644
index 00000000000..db595767c2b
--- /dev/null
+++ b/tests/direct_comp/peasy/b1_equal_chain.metta
@@ -0,0 +1,70 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; The equality sign is specially treated by the interpreter.
+
+; The evaluation of any (expr) in MeTTa is done via
+; constructing the following equality query:
+; (match &self (= (expr) $r) $r)
+; The result $r is recursively evaluated in the same way,
+; until the match is empty (when the equality match is
+; empty, the expression is evaluated to itself).
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (I $x) $x)
+(= ((K $x) $y) $x) ; Note that `(K $x)` is allowed here
+(= (K $x $y) $x)
+(= (S $x $y $z) ($x $z ($y $z)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `assertEqual` compares (sets of) results of evaluation
+; of two expressions (both expressions can have empty
+; sets of results, so `assertEqualToResult` is safer)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (S K K x)
+  x)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Here, we use `assertEqualToResult` to make sure
+; that the expression is evaluated to itself
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+   (expression without known equalities)
+  ((expression without known equalities)))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Another example
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (Add $x Z) $x)
+(= (Add $x (S $y)) (Add (S $x) $y))
+
+!(assertEqual
+  (Add (S Z) (S Z))
+  (S (S Z)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; In the current implementation, child expressions
+; are reduced
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (Something? (Add (S Z) (S Z)))
+  (Something? (S (S Z))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Note that the same variable can be used multiple times on the left
+; side of expressions, and that the "function" doesn't need to
+; cover all possible inputs (i.e. it can be "non-total")
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (eq $x $x) T)
+!(assertEqual
+  (eq (S K K x) x)
+  T)
+!(assertEqualToResult
+   (eq Green Blue)
+  ((eq Green Blue)))
+
diff --git a/tests/direct_comp/peasy/b2_backchain.metta b/tests/direct_comp/peasy/b2_backchain.metta
new file mode 100644
index 00000000000..c9cd36ec5cd
--- /dev/null
+++ b/tests/direct_comp/peasy/b2_backchain.metta
@@ -0,0 +1,99 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `match` can be used inside equalities, which is typically
+; used for querying and reasoning over declarative knowledge
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Fact
+(Frog Sam)
+(= (frog $x) (match &self (Frog $x) T))
+; `(Frog Sam)` is not reduced; it is just a declaration
+!(assertEqualToResult
+   (Frog Sam)
+  ((Frog Sam)))
+; `frog` uses this declaration
+!(assertEqual
+  (frog Sam)
+  T)
+!(assertEqualToResult
+  (frog Fritz)
+  ())
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; The result of matching is also chained
+; Example from OpenCog Classic wiki on PLN Backward Chaining
+; `And` and `T` are custom symbols (they are used here
+; to avoid mixing them up with symbols from common lib)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Some facts in the knowledge base
+(Evaluation (philosopher Plato))
+(Evaluation (likes-to-wrestle Plato))
+
+; An implication rule
+(Implication
+   (And (Evaluation (philosopher $x))
+        (Evaluation (likes-to-wrestle $x)))
+   (Evaluation (human $x)))
+
+; Another implication rule
+(Implication
+   (Evaluation (human $x))
+   (Evaluation (mortal $x)))
+
+; Deduction case when the desired evaluation is present in
+; the knowledge base
+(= (deduce (Evaluation ($P $x)))
+   (match &self (Evaluation ($P $x)) T))
+
+; Deduction case when the desired evaluation is the result
+; of an implication, which implies a recursion
+(= (deduce (Evaluation ($P $x)))
+   (match &self
+     (Implication $a (Evaluation ($P $x)))
+     (deduce $a)))
+
+; Deduction case for generic "And" expressions;
+; also recursive
+(= (deduce (And $a $b))
+   (And (deduce $a) (deduce $b)))
+
+; True & True = True
+(= (And T T) T)
+
+; Test deduction that Plato is mortal
+!(assertEqual
+  (deduce (Evaluation (mortal Plato)))
+  T)
+
+; TODO : Some variables are not substituted
+(= (ift T $then) $then)
+(ift (deduce (Evaluation (mortal $x))) $x)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Another example of backchaining
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Definition of explain when the desired Evaluation is
+; in the knowledge base
+(= (explain (Evaluation ($P $x)))
+   (match &self (Evaluation ($P $x)) ($P $x)))
+
+; Definition of explain when the desired Evaluation is
+; the result of an implication
+(= (explain (Evaluation ($P $x)))
+   (match &self
+     (Implication $a (Evaluation ($P $x)))
+     (($P $x) proven by (explain $a))))
+
+; Definition of explain for And
+(= (explain (And $a $b))
+   (And (explain $a) (explain $b)))
+
+; Example of explain why Plato is mortal
+!(assertEqual
+  (explain (Evaluation (mortal Plato)))
+  ((mortal Plato)
+    proven by ((human Plato)
+      proven by (And
+        (philosopher Plato)
+        (likes-to-wrestle Plato)))))
diff --git a/tests/direct_comp/peasy/b3_direct.metta b/tests/direct_comp/peasy/b3_direct.metta
new file mode 100644
index 00000000000..07b916cfa88
--- /dev/null
+++ b/tests/direct_comp/peasy/b3_direct.metta
@@ -0,0 +1,48 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Example from OpenCog Classic wiki on PLN Backward Chaining
+; No explicit backward chaining is needed
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; facts
+(= (croaks Fritz) T)
+(= (eat_flies Fritz) T)
+; Rules
+(= (And T T) T)
+(= (frog $x)
+   (And (croaks $x)
+        (eat_flies $x)))
+(= (green $x)
+   (frog $x))
+
+; Conclusion from facts and rules
+!(assertEqual
+  (green Fritz)
+  T)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; This is not just functional programming,
+; because we can do inference
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(= (ift T $then) $then)
+
+!(set-debug! e)
+;!(rtrace! (ift (green $x) $x))
+;!(break!)
+; !(rtrace! (, (green $x) (println! $x)))
+
+
+!(assertEqual
+  (ift (green $x) $x)
+  Fritz)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; We can also use expressions with `=` in `match`
+; NOTE: `=` is not an ordinary symbol, and declarative reasoning over expressions
+; with it may work differently from that over purely symbolic expressions
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+  (match &self (= ($p Fritz) T) $p)
+  (croaks eat_flies))
diff --git a/tests/direct_comp/peasy/b4_nondeterm.metta b/tests/direct_comp/peasy/b4_nondeterm.metta
new file mode 100644
index 00000000000..14576f924b7
--- /dev/null
+++ b/tests/direct_comp/peasy/b4_nondeterm.metta
@@ -0,0 +1,130 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Nondeterminism in matching and interpretation
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (color) green)
+(= (color) yellow)
+(= (color) red)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; In `a1_symbols` we saw that `match` can return multiple or no results
+; The same is true for equality queries
+; `superpose` turns a tuple into a non-deterministic result (for comparison here)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (match &self (= (color) $x) $x)
+  (superpose (red yellow green)))
+;!(assertEqual (match &self (= (color) $x) $x) (color))
+
+
+;!(assertEqual (collapse (color)) (red yellow green))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `collapse` converts a nondeterministic result into a tuple
+; We don't use it above, because the order of non-deterministic results
+; is not guaranteed
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (collapse
+    (match &self (= (shape) $x) $x))
+  ())
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Multiple results from equality queries
+; are also returned by the interpreter
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (color)
+  (superpose (red yellow green)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `superpose` reverts `collapse`
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `let` is used to introduce temporary variable bindings within an expression
+!(assertEqual
+  (color)
+  (let $x (collapse (color)) (superpose $x)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; In contrast to `match`, if the equality query returns an empty result
+; the interpreter doesn't reduce a symbolic expression
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (collapse (shape))
+  ((shape)))
+!(assertEqualToResult
+   (shape)
+  ((shape)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; If the expression is composed over nondeterministic
+; expressions, all combinations will be produced
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (bin) A)
+(= (bin) B)
+(= (pair $x $y) ($x $y))
+!(assertEqualToResult
+  (pair (bin) (bin))
+  ((A A) (A B) (B A) (B B)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; For the ordinary symbolic expression, if its subexpressions
+; are nondeterministic, and no reduction rule is available
+; for some combinations of their values, the whole expression
+; for these values will appear in the set of final results,
+; but without reduction. However, `match` can be called
+; directly to filter out non-reducible results
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (foo) red)
+(= (foo) boo)
+(= (eq $x $x) T)
+(= (find-equal $x $y)
+   (match &self (= (eq $x $y) T) $x))
+!(assertEqual
+  (find-equal (color) (foo))
+  red)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; One can pass nondeterministic expressions to an ordinary
+; function and get multiple results.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (rev $x $y) ($y $x))
+!(assertEqualToResult
+  (rev A (superpose (B C D)))
+  ((B A) (C A) (D A)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Extended example
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Some rules
+(= (ift T $then) $then)
+(= (And T T) T)
+(= (make $x) (ift (makes $y $x) (start $y)))
+(= (make $x) (ift (And (prevents (making $y) (making $x))
+                       (makes $z $y)) (stop $z)))
+
+; Add facts to knowledge base
+(= (prevents (making (air dry)) (making (air wet))) T)
+(= (prevents (making (air wet)) (making (air dry))) T)
+(= (makes humidifier (air wet)) T)
+(= (makes kettle (air wet)) T)
+(= (makes ventilation (air dry)) T)
+(= (is (air dry)) (make (air wet)))
+(= (is (air wet)) (make (air dry)))
+
+; the results are not sequential in sense that their order is arbitrary
+!(assertEqual
+  (is (air dry))
+  (superpose ((stop ventilation) (start kettle) (start humidifier))))
+!(assertEqual
+  (is (air wet))
+  (superpose ((stop kettle) (stop humidifier) (start ventilation))))
diff --git a/tests/direct_comp/peasy/b5_types_prelim.metta b/tests/direct_comp/peasy/b5_types_prelim.metta
new file mode 100755
index 00000000000..169a3764e3d
--- /dev/null
+++ b/tests/direct_comp/peasy/b5_types_prelim.metta
@@ -0,0 +1,261 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Symbols are typed. If no type definition is provided,
+; the type is %Undefined%, which can match against any
+; other type in a gradual typing fashion.
+; Automatic type checking is off by default ATM, so
+; incorrectly typed expressions can be added to Atomspace.
+; However, the interpreter checks types in runtime, and
+; evaluation of badly typed expressions leads to a error expression.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (Add $x Z) $x)
+(= (Add $x (S $y)) (Add (S $x) $y))
+
+; `(Add S Z)` will be reduced to `S` without type definitions
+!(assertEqual
+  (Add S Z)
+  S)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Adding type definitions.
+; Arrow (->) is a built-in symbol of the type system
+; `Nat` is a custom symbol
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(: Z Nat)
+; (: S Oper)
+(: S (-> Nat Nat))
+(: Add (-> Nat Nat Nat))
+
+!(set-debug! e)
+
+; Now the result of its evaluation will be a error expression, because `S` is not `Nat`
+!(assertEqualToResult
+  (Add S Z)
+  ((Error S BadType)))
+; But these other examples works normally
+!(assertEqual
+  (Add (S Z) Z)
+  (S Z))
+!(assertEqual
+  (Add Z (S Z))
+  (S Z))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Adding to an untyped symbol (Something) will still work,
+; because it might be `Nat`
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (Add Something Z)
+  Something)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Types can be nondeterministic
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(: Ten Nat)
+(: Ten Int)
+; The following will be accepted by the interpreter
+!(assertEqualToResult
+   (Add Z Ten)
+  ((Add Z Ten)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Types can be parameterized
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; List has a function type. Its argument should be of Type type.
+; The type of the whole expression, e.g. (List String), will also have Type type.
+(: List (-> Type Type))
+
+; Nil's type is parametrized as the type returned by List when it
+; takes parameter $t (which, per the definition above,
+; is the same type as $t)
+(: Nil (List $t))
+
+; Cons is defined as a parametrized List constructor
+; Based on the definition of List above, Cons' arguments
+; are equally typed, and it returns the same type
+; as its arguments.
+(: Cons (-> $t (List $t) (List $t)))
+
+; This list is well typed and evaluated to itself
+!(assertEqualToResult
+   (Cons (S Z) (Cons Z Nil))
+  ((Cons (S Z) (Cons Z Nil))))
+
+; TODO: MINIMAL This test has different behavior in old and new versions of the
+;       interpreter versions. Uncomment it after migration to the minimal MeTTa.
+; This list is badly typed, because S and Z are not the same type
+!(assertEqualToResult
+  (Cons S (Cons Z Nil))
+  ((Error (Cons Z Nil) BadType)))
+;; We uncomment this because it still works in MeTTaLog !
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Another example
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(: T Type)
+; The type definition of `eq` specifies both its arguments
+; must be of the same type, but its own type is left undefined,
+; just as a Type.
+(: eq (-> $t $t Type))
+; The definition of `eq` specifies its actual type (T)
+(= (eq $x $x) T)
+; Accepted and reduced
+!(assertEqual
+  (eq (Add Z Z) Z)
+  T)
+; Accepted, not reduced because no definition is known
+; for `eq` when its arguments are not the same
+!(assertEqualToResult
+   (eq Z (S Z))
+  ((eq Z (S Z))))
+; Not accepted, because Z and S are not the same type
+!(assertEqualToResult
+  (eq Z S)
+  ((Error S BadType)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Type (symbols) are not prohibited from being elements
+; of other custom types
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(: Color Property)
+(: Green Color)
+(: Red Color)
+(: Shape Property)
+(: Square Shape)
+(: Circle Shape)
+; This type definition is the same as that of `eq` above
+(: of-same-type (-> $t $t Type))
+; It returns True for any pair of arguments, as long as there
+; is not Type error
+
+; Accepted
+(= (of-same-type $x $y) T)
+!(assertEqual
+  (of-same-type Color Shape)
+  T)
+!(assertEqual
+  (of-same-type Green Red)
+  T)
+
+; Not accepted
+!(assertEqualToResult
+  (of-same-type Green Color)
+  ((Error Color BadType)))
+
+!(assertEqualToResult
+  (of-same-type Green Circle)
+  ((Error Circle BadType)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; There are some meta-types, which may influence
+; the process of interpretation. One of them is `Atom`.
+; If a function expects `Atom` as its argument,
+; this argument is not reduced before passing to
+; the function, so the function can process the
+; original expression itself.
+; The `match` function expects an `Atom` type as argument.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; In the following example, `(Green $who)` is evaluated
+; to `T`. However, it is not reduced as `match` argument,
+; and the query returns `Sam`.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(Green Sam)
+(= (Green Sam) T)
+!(assertEqual
+  (Green $who)
+  T)
+!(assertEqual
+  (match &self (Green $who) $who)
+  Sam)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; It should be noted that the result of `match` will be
+; evaluated further. In the following, `match` first
+; returns `(Green Sam)`, which is then evaluated to `T`.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (match &self (Green $who) (Green $who))
+  T)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; If one wants to evaluate an expression before passing it
+; to `match`, `let` can be used:
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (let $r (Add (S Z) Z)
+    (match &self (= (eq $r (S Z)) $tv) $tv))
+  T)
+; but it will not work inside `match`:
+!(assertEqualToResult
+  (match &self (= (eq (Add (S Z) Z) (S Z)) $tv) $tv)
+  ())
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; The second argument of `let` is not `Atom` and evaluated
+; by the interpreter before executing `let`, while
+; the third argument is `Atom`, which is transformed by `let`
+; as an expression, and then returned for further evaluation.
+; `match` and `let` are implemented as an ordinary grounded operations
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; In fact, one can use patterns instead of variables in `let`
+; in order to deconstruct the result immediately.
+; This example binds the result of (Add (S Z) (S Z)) to
+; the whole pattern (S (S $r)), and extracts the inner variable $r
+; This is cleaner than binding and re-matching.
+!(assertEqual
+  (let (S (S $r)) (Add (S Z) (S Z)) $r)
+  Z)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; One can use `let*` for convenience, when multiple consequent
+; substitutions are needed
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (let* (($r1 (Add Z Z))
+         ($r2 (Add $r1 (S Z)))
+         ($r3 (Add $r2 (S Z))))
+        (match &self (= (eq (S (S Z)) $r3) $tv) $tv))
+  T)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Atom type can be required in custom functions
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `eqa` will compare expressions:
+(: eqa (-> Atom Atom Type))
+(= (eqa $x $x) T)
+; These expressions are identical:
+!(assertEqual
+   (eqa (Add Z Z) (Add Z Z))
+   T)
+; while this will not be reduced because the expressions
+; are not the same (even if their evaluation would be)
+; (`eqa` is not total)
+!(assertEqualToResult
+    (eqa Z (Add Z Z))
+   ((eqa Z (Add Z Z))))
+
+;;!(repl!)
+
+; In contrast to this:
+!(assertEqual
+   (eq Z (Add Z Z))
+   T)
+
+; Or this:
+!(assertEqual
+   (let $z (Add Z Z)
+     (eqa Z $z))
+   T)
+
diff --git a/tests/direct_comp/peasy/c1_grounded_basic.metta b/tests/direct_comp/peasy/c1_grounded_basic.metta
new file mode 100644
index 00000000000..9a8a57e8818
--- /dev/null
+++ b/tests/direct_comp/peasy/c1_grounded_basic.metta
@@ -0,0 +1,172 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; The standard library contains a few basic grounded operations
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Implementation of grounded arithmetics may change location,
+; but these examples should work
+!(assertEqualToResult
+  (+ 2 (* 3 5.5))
+  (18.5))
+
+!(assertEqualToResult
+  (- 8 (/ 4 6.4))
+  (7.375))
+
+!(assertEqualToResult
+  (% 21 17)
+  (4))
+
+!(assertEqualToResult
+  (< 4 (+ 2 (* 3 5)))
+  (True))
+
+!(assertEqualToResult
+  (and (> 4 2) (< 4 3))
+  (False))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Currently, `ln` is not a grounded symbol.
+; If we don't define its type, then its application
+; will not be refused, but it will be unreduced.
+; Currently, its grounded argument will be reduced.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+  (ln (+ 2 2))
+  ((ln 4)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Similarly, passing ordinary symbols to grounded
+; operations will not cause errors and simply remain
+; unreduced, if it type-checks.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+  (> 4 (+ ln 2))
+  ((> 4 (+ ln 2))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; This will also remain unreduced unless
+; grounded operations can do pattern matching
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+  (> 4 (+ $x 2))
+  ((> 4 (+ $x 2))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `==` is now implemented to work with both grounded and
+; symbolic atoms (while remaining a grounded operation)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+  (== 4 (+ 2 2))
+  (True))
+!(assertEqualToResult
+  (== 2 3)
+  (False))
+!(assertEqualToResult
+  (== (A B) (A B))
+  (True))
+!(assertEqualToResult
+  (== (A B) (A (B C)))
+  (False))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Unlike `<` or `>`, `==` will not remain unreduced if one
+; of its arguments is grounded, while another is not.
+; Instead, it will return `False`
+!(assertEqualToResult
+  (== 4 (+ ln 2))
+  (False))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Grounded symbols have predefined types.
+; Evaluation of ill-typed expressions produces
+; a error expression
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+  (+ 2 "String")
+  ((Error "String" BadType)))
+
+; Custom symbols as arguments of grounded operations
+; work similarly
+(: ln LN)
+!(assertEqualToResult
+  (== 4 (+ ln 2))
+  ((Error ln BadType)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Custom functions over grounded functions behave ordinarily
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (sqr $x) (* $x $x))
+!(assertEqualToResult
+  (sqr 4)
+  (16))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Evaluation of grounded operations over nondeterministic
+; expressions work in the same way as of custom symbols
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (+ (superpose (1 2 3)) 1)
+  (superpose (2 3 4)))
+
+(= (bin) 0)
+(= (bin) 1)
+
+!(assertEqualToResult (bin) (0 1))
+
+
+!(assertEqualToResult
+  (+ 1 (bin))
+  (1 2))
+
+!(assertEqualToResult
+  (let $x (+ 2 3)
+    (* $x $x))
+  (25))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; basic recursion
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (fact $n) (if (== $n 0) 1 (* (fact (- $n 1)) $n)))
+!(assertEqual (fact 5) 120)
+
+; ensure we only return one result
+!(assertEqualToResult (fact 5) (120))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Grounded symbols work with non-determinism based "reasoning"
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Uses the grounded call `bin`, which returns a list of
+; both possible bits (0, 1), to recursively construct all possible
+; binary lists of length `$n`, appending bits one by one.
+(= (gen $n)
+   (if (> $n 0)
+       (:: (bin) (gen (- $n 1)))
+       nil))
+; Note: `::` is just a custom symbol, used here as a constructor,
+; but any other symbol can be used for this.
+
+; Calculates the sum of element-wise products between two lists
+(= (subsum nil nil) 0)
+(= (subsum (:: $x $xs) (:: $b $bs))
+   (+ (* $x $b)
+      (subsum $xs $bs)))
+
+; Non-determinism "reasoning":
+; Among all 3-bit binary lists, return the one whose `subsum`
+; with (:: 3 (:: 7 (:: 5 nil))) equals 8, or `nop` if not found
+; (`superpose` is used to return an empty result acting as termination
+; of evaluation of the branch)
+!(assertEqualToResult
+  (let $t (gen 3)
+    (if (== (subsum (:: 3 (:: 7 (:: 5 nil))) $t) 8) $t (superpose ())))
+  ((:: 1 (:: 0 (:: 1 nil)))))
diff --git a/tests/direct_comp/peasy/c2_spaces.metta b/tests/direct_comp/peasy/c2_spaces.metta
new file mode 100644
index 00000000000..9617ea14afd
--- /dev/null
+++ b/tests/direct_comp/peasy/c2_spaces.metta
@@ -0,0 +1,58 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Spaces are also represented as grounded symbols in the program.
+; Importing another script into a separate space
+; TODO: replace symbol by string
+!(import! &kb c2_spaces_kb)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; We can `match` over `&self` or another space
+!(assertEqualToResult
+  (match &kb
+    (, ($obj is $prop)
+       ($prop is-a Color)
+       ($obj is-a Planet))
+    (Color of Planet $obj is $prop))
+  ((Color of Planet Mars is Red)))
+
+; The knowledge in `&kb` is not in `&self`
+!(assertEqualToResult
+  (match &self ($p is-a Color) $p)
+  ())
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Checking that grounded symbols from different spaces are compatible
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (match &kb
+    (, (Venus orbit $x au)
+       (Mars orbit $y au))
+    (- $y $x))
+  0.8)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Different spaces can be used
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(Ball is Red)
+(Chair is High)
+
+!(assertEqualToResult
+  (match &kb ($prop is-a Color)
+    (match &self ($obj is $prop)
+       $obj))
+  (Ball))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; We can import into `&self`
+; TODO: replace symbol by string
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(import! &self c2_spaces_kb)
+!(assertEqualToResult
+  (match &self
+    (, ($obj is $prop)
+       ($prop is-a Color)
+       ($obj is-a Planet))
+    (Color of Planet $obj is $prop))
+  ((Color of Planet Mars is Red)))
diff --git a/tests/direct_comp/peasy/c2_spaces_kb.metta b/tests/direct_comp/peasy/c2_spaces_kb.metta
new file mode 100644
index 00000000000..c0ffa20edf7
--- /dev/null
+++ b/tests/direct_comp/peasy/c2_spaces_kb.metta
@@ -0,0 +1,18 @@
+(Green is-a Color)
+(White is-a Color)
+(Blue is-a Color)
+(Red is-a Color)
+(Brown is-a Color)
+(Yellow is-a Color)
+
+(Earth is-a Planet)
+(Mars is-a Planet)
+(Venus is-a Planet)
+
+(Mars is Red)
+
+(Blood is Red)
+
+(Venus orbit 0.7 au)
+(Earth orbit 1 au)
+(Mars orbit 1.5 au)
diff --git a/tests/direct_comp/peasy/c3_pln_stv.metta b/tests/direct_comp/peasy/c3_pln_stv.metta
new file mode 100644
index 00000000000..9e571c70fd3
--- /dev/null
+++ b/tests/direct_comp/peasy/c3_pln_stv.metta
@@ -0,0 +1,104 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; The examples in this file is inspired by OpenCog Classic examples
+; from github.com/opencog/pln, in particular from
+; examples/pln/conjunction, extended with implication
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Some helpful definitions
+(= (min $a $b) (if (< $a $b) $a $b))
+(= (s-tv (stv $s $c)) $s)
+(= (c-tv (stv $s $c)) $c)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `TV` "metarule" based on `match` to run
+; `.tv` is a custom symbol, which is used to connect
+; PLN-like expressions with their truth values.
+; Some `.tv` facts will be defined below
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (TV $x)
+   (match &self
+     (.tv $x $stv)
+     $stv
+   )
+)
+
+; Definition of TV for a conjunction
+; we could use `(.tv (And $a $b) (stv ...))` instead of this
+(= (TV (And $a $b))
+   (stv (min (s-tv (TV $a)) (s-tv (TV $b)))
+        (min (c-tv (TV $a)) (c-tv (TV $b)))
+   )
+)
+
+; Definition of TV for $x when it's the consequent of an implication
+(= (TV $x)
+   (match &self
+     (.tv (Implication $y $x)
+          (stv $s $c))
+     (stv (* $s (s-tv (TV $y)))
+          (* $c (c-tv (TV $y))))
+   )
+)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; First example
+; .tv serves as a special type of equality when
+; matched by the TV "metarules" above
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Some facts
+(.tv (Evaluation (Predicate P) (Concept A))
+     (stv 0.5 0.8))
+(.tv (Evaluation (Predicate P) (Concept B))
+     (stv 0.3 0.9))
+(.tv (Implication (Evaluation (Predicate P) (Concept A))
+                  (Evaluation (Predicate F) (Concept A)))
+     (stv 0.8 1.0))
+
+; FIXME? `(PA)` and `(PB)` are used because otherwise
+; substitution is not invoked (atm of test creation)
+(= (PA) (Evaluation (Predicate P) (Concept A)))
+(= (PB) (Evaluation (Predicate P) (Concept B)))
+(= (FA) (Evaluation (Predicate F) (Concept A)))
+
+; Tests
+!(assertEqual (TV (And (PA) (PB))) (stv 0.3 0.8))
+!(assertEqual (TV (FA)) (stv 0.4 0.8))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Second example
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Implication rule
+(.tv
+  (Implication
+     (And (croaks $x)
+          (eat_flies $x))
+     (frog $x))
+  (stv 0.9 0.8)
+)
+
+; Some facts
+(.tv (croaks Fritz)
+     (stv 0.95 0.85))
+(.tv (eat_flies Fritz)
+     (stv 0.87 0.95))
+
+(.tv
+  (Implication
+     (frog $x)
+     (green $x))
+  (stv 0.9 1.0)
+)
+
+; Tests
+!(assertEqual
+  (TV (croaks Fritz))
+  (stv 0.95 0.85))
+!(assertEqual
+  (TV (frog Fritz))
+  (stv 0.783 0.68))
+!(assertEqual
+  (TV (green Fritz))
+  (stv 0.7047 0.68))
diff --git a/tests/direct_comp/peasy/d1_gadt.metta b/tests/direct_comp/peasy/d1_gadt.metta
new file mode 100644
index 00000000000..bea7aae4a96
--- /dev/null
+++ b/tests/direct_comp/peasy/d1_gadt.metta
@@ -0,0 +1,98 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Basic types of grounded symbols
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `get-type` returns the type of its argument
+!(assertEqual
+  (get-type 5)
+  Number)
+!(assertEqual
+  (get-type (+ 5 7))
+  Number)
+
+; It works for built-in symbols too
+!(assertEqual
+  (get-type +)
+  (-> Number Number Number))
+
+; If its argument is a badly typed expression,
+; `get-type` returns the empty set
+!(assertEqualToResult
+  (get-type (+ 5 "4"))
+  ())
+!(assertEqualToResult
+  (get-type (+ -))
+  ())
+
+; Also works for custom types
+(: Either Type)
+!(assertEqual
+  (get-type Either)
+  Type)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Arrow types of functions and constructors
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(: Left (-> %Undefined% Either))
+(: Right (-> %Undefined% Either))
+
+!(assertEqual
+  (get-type (Left 5))
+  Either)
+
+(: isLeft (-> Either Bool))
+(= (isLeft (Left $x)) True)
+(= (isLeft (Right $x)) False)
+
+!(assertEqual
+  (get-type (isLeft (Right 5)))
+  Bool)
+
+; Badly typed expression
+!(assertEqualToResult
+  (get-type (isLeft 5))
+  ())
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Parameterized types
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(: EitherP (-> $t Type))
+(: LeftP (-> $t (EitherP $t)))
+(: RightP (-> $t (EitherP $t)))
+
+!(assertEqual
+  (get-type (LeftP 5))
+  (EitherP Number))
+
+(: Pair (-> $a $b Type))
+(: pair (-> $a $b (Pair $a $b)))
+
+!(assertEqual
+  (get-type (pair (LeftP 5) "String"))
+  (Pair (EitherP Number) String))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Recursively parameterized types
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(: List (-> $a Type))
+(: Nil (List $a))
+(: Cons (-> $a (List $a) (List $a)))
+
+!(assertEqual
+  (get-type (Cons 5 (Cons 6 Nil)))
+  (List Number))
+!(assertEqualToResult
+  (get-type (Cons 5 (Cons "6" Nil)))
+  ())
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `let` can be convenient to extract information from `get-type` results
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (let (List $t) (get-type (Cons 5 (Cons 6 Nil)))
+       $t)
+  Number)
diff --git a/tests/direct_comp/peasy/d2_higherfunc.metta b/tests/direct_comp/peasy/d2_higherfunc.metta
new file mode 100644
index 00000000000..41293dcabcb
--- /dev/null
+++ b/tests/direct_comp/peasy/d2_higherfunc.metta
@@ -0,0 +1,237 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Higher-order functions
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Type definition for `curry` function
+(: curry (-> (-> $a $b $c) (-> $a (-> $b $c))))
+; A trick to define `curry` in MeTTa without `lambda`
+(= (((curry $f) $x) $y) ($f $x $y))
+
+; Type checks
+!(assertEqual
+  (get-type (curry +))
+  (-> Number (-> Number Number)))
+!(assertEqual
+  (get-type ((curry +) 2))
+  (-> Number Number))
+
+; Partial application is not reduced, basically
+!(assertEqualToResult
+   ((curry +) 2)
+  (((curry +) 2)))
+; Full application will be reduced
+!(assertEqual
+  (((curry +) 2) 3)
+  5)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Curry with first application
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Definitions
+(: curry-a (-> (-> $a $b $c) $a (-> $b $c)))
+(= ((curry-a $f $a) $b) ($f $a $b))
+
+; Tests
+!(assertEqual
+  (get-type (curry-a + 2))
+  (-> Number Number))
+!(assertEqual
+  (get-type ((curry-a + 2) 3))
+  Number)
+; Badly typed
+!(assertEqualToResult
+  (get-type ((curry-a + 2) "S"))
+  ())
+; Full application works
+!(assertEqual
+  ((curry-a + 2) 3)
+  5)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; More tests with partial application wrapping
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Definitions
+(: Socrates Entity)
+(: Human Entity)
+(: is (-> Entity Entity Bool))
+; Facts
+(= (is Socrates Human) True)
+(= (is-socrates) (curry-a is Socrates))
+
+; Tests
+!(assertEqualToResult
+  (is-socrates)
+  ((curry-a is Socrates)))
+; not reduced
+!(assertEqual
+  ((curry-a is Socrates) Human)
+  (is Socrates Human))
+; reduced
+!(assertEqual
+  ((is-socrates) Human)
+  True)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; The same trick works for defining lambda
+; (basically, `lambda` is curried `let`)
+; FIXME: how to make parameterized type here?
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Definitions
+(: lambda (-> Atom $t (-> $a $t)))
+(= ((lambda $var $body) $arg)
+   (let $var $arg $body))
+
+; Tests
+!(assertEqual
+  ((lambda $x (+ $x 1)) 2)
+  3)
+!(assertEqual
+  ((lambda ($x $y) (+ $x $y)) (2 7))
+  9)
+
+; Another example
+(= (part-appl $f $x)
+   (lambda $y ($f $x $y)))
+(= (inc) (part-appl + 1))
+!(assertEqual
+  ((inc) 5)
+  6)
+; REM:
+;   (get-type (lambda ($x $y) (+ $x $y)))
+; returns (-> %Undefined% Number), because the type of `($x $y)` is not defined.
+; It is also not clear how to check that the type of `$var` is suitable for `$body`
+; (it should somehow be done on`let` side)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Let's introduce some functors
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(: Maybe (-> $t Type))
+(: Nothing (-> (Maybe $t)))
+(: Something (-> $t (Maybe $t)))
+
+(: Either (-> $t Type))
+(: Left (-> $t (Either $t)))
+(: Right (-> $t (Either $t)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; We can implement a generic `fmap`, but it requires
+; concrete patterns in the type constructors above
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Instead, we implement `fmap` as:
+(: fmap (-> (-> $a $b) ($F $a) ($F $b)))
+; Mapping over empty functor, returns empty functor
+(= (fmap $f ($C0))
+  ($C0))
+; Inductive case for singleton functor: apply $f to the
+; element and rewrap in $C.
+(= (fmap $f ($C $x))
+  ($C ($f $x)))
+; Inductive case for non-empty functor: apply to the
+; head and recurse on the tail.
+(= (fmap $f ($C $x $xs))
+  ($C ($f $x) (fmap $f $xs)))
+
+; NOTE: We had to define `Nothing` as a functional constructor.
+;       Otherwise, we'd have to define `(= (fmap $f $C0) $C0)`,
+;       and `$C0` would match both `Nothing` and `(Something 2)`
+; TODO? This could be avoided if we could indicate that $C0
+;       is a `Symbol` (not `Expression` or `Atom` in general)
+
+; Tests
+!(assertEqual
+  (fmap (curry-a + 2) (Something 5))
+  (Something 7))
+!(assertEqual
+  (fmap (curry-a + 2) (Nothing))
+  (Nothing))
+
+; Type inference works
+!(assertEqual
+  (get-type (fmap (curry-a + 1) (Left 5)))
+  (Either Number))
+
+; It works for untyped constructors as well, if they
+; follow the patterns in `fmap` equalities
+!(assertEqual
+  (fmap (curry-a + 2) (UntypedC 5))
+  (UntypedC 7))
+!(assertEqual
+  (fmap (curry-a + 2) (UntypedC 5 (UntypedC 8 (Null))))
+  (UntypedC 7 (UntypedC 10 (Null))))
+
+; Type mismatches are detected:
+!(assertEqualToResult
+  (get-type (fmap (curry-a + 2) (Left "5")))
+  ())
+!(assertEqualToResult
+  (get-type (fmap (curry-a + 2) (UntypedC "5")))
+  ())
+!(assertEqualToResult
+  (get-type (fmap (curry-a + 2) (UntypedC (Null) 5)))
+  ())
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; It is possible to implement `fmap` only as an interface
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Type definition is the same as `fmap` above
+(: fmap-i (-> (-> $a $b) ($F $a) ($F $b)))
+; Custom implementations for different functors will be
+; possible (and needed):
+(= (fmap-i $f (Left $x)) (Left ($f $x)))
+(= (fmap-i $f (Right $x)) (Right ($f $x)))
+!(assertEqual
+  (fmap-i (curry-a - 7) (Right 3))
+  (Right 4))
+
+; More examples
+(: List (-> $a Type))
+(: Nil (List $a))
+(: Cons (-> $a (List $a) (List $a)))
+(= (fmap-i $f Nil) Nil)
+(= (fmap-i $f (Cons $x $xs))
+   (Cons ($f $x) (fmap-i $f $xs)))
+
+!(set-debug! defn)
+
+!(assertEqual
+  (fmap-i (curry-a * 2) (Cons 3 (Cons 4 Nil)))
+  (Cons 6 (Cons 8 Nil)))
+
+; Thus, there is no problem in having different implementations
+; of the same function for different types. But it will not
+; work "for free" (it requires explicit implementation for each type)
+!(assertEqualToResult
+   (fmap-i (curry-a + 2) (Untyped 5))
+  ((fmap-i (curry-a + 2) (Untyped 5))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; As per issue
+;
+; https://github.com/trueagi-io/hyperon-experimental/issues/104
+;
+; Test if adding type declaration to List data structure does
+; not interfere with executing functions operating on List.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Insert an element in a presumably sorted list
+(= (insert $x Nil) (Cons $x Nil))
+(= (insert $x (Cons $head $tail))
+  (case (< $x $head)
+      ((True  (Cons $x (Cons $head $tail)))
+       (False (Cons $head (insert $x $tail))))))
+
+; Sort a list
+(= (sort Nil) Nil)
+(= (sort (Cons $head $tail)) (insert $head (sort $tail)))
+!(assertEqual
+  (insert 3 (insert 2 (insert 1 Nil)))
+  (Cons 1 (Cons 2 (Cons 3 Nil))))
+!(assertEqual
+  (sort (Cons 3 (Cons 1 (Cons 2 Nil))))
+  (Cons 1 (Cons 2 (Cons 3 Nil))))
diff --git a/tests/direct_comp/peasy/d3_deptypes.metta b/tests/direct_comp/peasy/d3_deptypes.metta
new file mode 100644
index 00000000000..af5b34a769f
--- /dev/null
+++ b/tests/direct_comp/peasy/d3_deptypes.metta
@@ -0,0 +1,75 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; A classical example of dependent types
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Simple type definitions:
+; Defines the natural numbers `Nat` for counting
+(: Nat Type)
+(: Z Nat)
+(: S (-> Nat Nat))
+
+; `Vec` takes a `$t` type and a `Nat` length.
+(: Vec (-> $t Nat Type))
+; `Cons` and `Nil` construct `Vec` values, with `Cons` incrementing the length by 1.
+(: Cons (-> $t (Vec $t $x) (Vec $t (S $x))))
+(: Nil (Vec $t Z))
+
+; We can query the derived type
+!(assertEqual
+  (get-type (Cons 0 (Cons 1 Nil)))
+  (Vec Number (S (S Z))))
+
+; `drop` removes the head from a `Vec`, returning a `Vec` with length decrease by 1
+(: drop (-> (Vec $t (S $x)) (Vec $t $x)))
+(= (drop (Cons $x $xs)) $xs)
+
+; Query type
+!(assertEqual
+  (get-type (drop (Cons 1 Nil)))
+  (Vec Number Z))
+; Check length after dropping
+!(assertEqual
+  (drop (Cons 2 (Cons 1 Nil)))
+  (Cons 1 Nil))
+
+; Types can protect against misuse, like dropping from empty Vec
+!(assertEqualToResult
+  (get-type (drop Nil))
+  ())
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; The result returned by `get-type` is reduced, thus,
+; grounded operations in type declarations work (kind of)
+; NOTE: tests below is the current behavior, which may be changed
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `VecN` and `ConsN` use grounded `+` to increment the length.
+(: VecN (-> $t Number Type))
+(: ConsN (-> $t (VecN $t $x) (VecN $t (+ $x 1))))
+(: NilN (VecN $t 0))
+
+; When querying types, grounded ops are reduced
+!(assertEqual
+  (get-type (ConsN "1" (ConsN "2" NilN)))
+  (VecN String 2))
+
+; Similarly, `-` reduces the length in `dropN` type.
+(: dropN (-> (VecN $t $x) (VecN $t (- $x 1))))
+(= (dropN (ConsN $x $xs)) $xs)
+
+!(assertEqual
+  (get-type (dropN (ConsN "1" NilN)))
+  (VecN String 0))
+
+; TODO: doesn't work after type checking fixes
+; However, without any validation, invalid lengths like -1 can be derived.
+(assertEqual
+  ((get-type (dropN (dropN (ConsN "1" NilN)))))
+   (VecN String -1))
+
+; Applying `dropN` to `NilN` is not badly typed, but it
+; doesn't reduce, since there are no definitions for this case.
+!(assertEqualToResult
+   (dropN NilN)
+  ((dropN NilN)))
diff --git a/tests/direct_comp/peasy/d4_type_prop.metta b/tests/direct_comp/peasy/d4_type_prop.metta
new file mode 100644
index 00000000000..5d03a270c0f
--- /dev/null
+++ b/tests/direct_comp/peasy/d4_type_prop.metta
@@ -0,0 +1,171 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Types as propositions can be used in MeTTa but with nuances
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Entities
+(: Entity Type)
+(: Socrates Entity)
+(: Plato Entity)
+
+; Predicates (functions) from `Entity` to `Type`
+(: Human (-> Entity Type))
+(: Mortal (-> Entity Type))
+
+; `(Mortal Plato)` is an expression of `Type` type
+; It represents the proposition "Plato is mortal"
+; but doesn't mean this proposition is inhabited/proven
+!(assertEqual
+  (get-type (Mortal Plato))
+  Type)
+
+; A function type as an implication
+; `HumansAreMortal` represents the implication:
+; "For all x, if Human(x) then Mortal(x)"
+(: HumansAreMortal (-> (Human $t) (Mortal $t)))
+; NOTE: MeTTa doesn't differentiate between type constructors and
+;       other symbols (including functional) of the same type.
+;       Thus, ATM, we cannot prove any proposition with universal
+;       quantification (e.g., that all humans are mortal) by
+;       providing a total function as an instance of a
+;       corresponding type.
+
+; These might be considered as assertions that Plato and
+; Socrates are Humans:
+(: SocratesIsHuman (Human Socrates))
+(: PlatoIsHuman (Human Plato))
+
+; `(HumansAreMortal SocratesIsHuman)` might be considered
+; as a proof that that `(Mortal Socrates)`.
+!(assertEqual
+  (get-type (HumansAreMortal SocratesIsHuman))
+  (Mortal Socrates))
+; Bad typing
+!(assertEqualToResult
+  (get-type (HumansAreMortal (Human Socrates)))
+  ())
+
+; We can write this code, but it will make not too much
+; difference for the assertion that "all humans are mortal"
+(: SocratesIsMortal (Mortal Socrates))
+(= (HumansAreMortal SocratesIsHuman) SocratesIsMortal)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Equality can be typed. If some equality is well-typed,
+; it means that it can be true.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(nop (remove-atom &self (: = (-> Atom Atom Atom))))
+(nop (remove-atom &corlib (: = (-> Atom Atom Atom))))
+(: = (-> $t $t Type))
+
+!("sameTypes" (get-type SocratesIsMortal) (get-type (HumansAreMortal SocratesIsHuman)))
+!(assertEqual
+  (get-type (= SocratesIsMortal (HumansAreMortal SocratesIsHuman)))
+  Type)
+; This equality is well-typed, because both its arguments are of `Type`.
+; It doesn't mean they are both inhabited (true propositions), and
+; it doesn't mean that the equality itself is true (an inhabited type).
+
+!("sameTypes" (get-type (Mortal Socrates)) (get-type (Mortal Plato)))
+!(assertEqual
+  (get-type (= (Mortal Socrates) (Mortal Plato)))
+  Type)
+
+
+!("!sameTypes" (get-type SocratesIsMortal) (get-type (HumansAreMortal PlatoIsHuman)))
+; Wrong proof
+!(assertEqualToResult
+  (get-type (= SocratesIsMortal (HumansAreMortal PlatoIsHuman)))
+  ())
+
+
+!("!sameTypes" (get-type SocratesIsHuman) (get-type PlatoIsHuman))
+; Wrong equalities
+!(assertEqualToResult
+  (get-type (= SocratesIsHuman PlatoIsHuman))
+  ())
+
+!("!sameTypes" (get-type SocratesIsHuman) (get-type SocratesIsMortal))
+!(assertEqualToResult
+  (get-type (= SocratesIsHuman SocratesIsMortal))
+  ())
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; A standard type-theoretic way of saying that some equality is true
+; is to present an instance of the corresponding equality type.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; (: Refl (-> (: $x $T) (= $x $x))).
+; As per https://github.com/trueagi-io/hyperon-experimental/issues/177 ,
+; there is no way to match both argument and its type in type definition.
+; Such syntax `(: (Refl $x) (-> Type (= $x $x)))` also doesn't work now.
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Another (MeTTa) way is to have explicit reduction of types to True
+; (equalities over equalities), although a more practical way would
+; be just to use a dedicated comparison operator
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(: T Type)
+(= (= $x $x) T)
+
+; These equalities will be true
+!(assertEqual
+  (= SocratesIsMortal (HumansAreMortal SocratesIsHuman))
+  T)
+!(assertEqual
+  (= (+ 1 1) (- 3 1))
+  T)
+
+; One can also define an equality for directly inhabited types
+(= (= $type T)
+   (match &self (: $x $type) T))
+!(assertEqual
+  (= (Mortal Socrates) T)
+  T)
+
+; It will not immediately work for implications
+!(assertEqualToResult
+  (= (Mortal Plato) T)
+  ())
+
+; But we can add 'reasoning'
+(= (= $type T)
+   (match &self (: $impl (-> $cause $type))
+      (= $cause T)))
+!(assertEqual
+  (= (Mortal Plato) T)
+  T)
+(: Sam Entity)
+!(assertEqualToResult
+  (= (Human Sam) T)
+  ())
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Types by themselves will not be reduced
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+   (Mortal Plato)
+  ((Mortal Plato)))
+; Refl rule itself equals to True
+!(assertEqual
+  (= (= $x $x) T)
+  T)
+
+; We can also add direct equalities
+; (= (Human Socrates) T)
+(= (Human Plato) T)
+(= (Mortal Socrates) T)
+(= (Mortal $x) (Human $x))
+; Then, the type of type itself will be reduced
+!(assertEqual
+  (Mortal Plato)
+  T)
+
+; We can even try backward chaining
+(: ift (-> Type $t $t))
+(= (ift T $then) $then)
+!(assertEqualToResult
+  (ift (Mortal $x) $x)
+  (Socrates Plato))
diff --git a/tests/direct_comp/peasy/d5_auto_types.metta b/tests/direct_comp/peasy/d5_auto_types.metta
new file mode 100644
index 00000000000..c5e316cab22
--- /dev/null
+++ b/tests/direct_comp/peasy/d5_auto_types.metta
@@ -0,0 +1,65 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Auto type-checking can be enabled
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(pragma! type-check auto)
+
+; checking grounded types
+!(assertEqualToResult
+   (+ 5 "S")
+  ((Error "S" BadType)))
+!(assertEqualToResult
+   (== 5 "S")
+  ((Error "S" BadType)))
+
+; declaring some custom types
+(: Entity Type)
+(: Socrates Entity)
+(: Human (-> Entity Type))
+(: Mortal (-> Entity Type))
+(: HumansAreMortal (-> (Human $t) (Mortal $t)))
+(: SocratesIsHuman (Human Socrates))
+(: SamIsMortal (Mortal Sam))
+
+; well typed
+(HumansAreMortal SocratesIsHuman)
+(== Mortal Human)
+
+; badly typed examples produce `Error` grounded values describing the issue:
+!(assertEqualToResult
+   (== SocratesIsHuman SamIsMortal)
+  ((Error SamIsMortal BadType)))
+!(assertEqualToResult
+   (HumansAreMortal (Human Socrates))
+  ((Error (Human Socrates) BadType)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `collapse` evaluates its argument, so it shows a type error
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqualToResult
+   (collapse (+ 5 "S"))
+   (((Error "S" BadType))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `match` does not perform type checking on its pattern,
+; so it accepts a badly typed expression, which is expected.
+; It can be useful to deal with "wrong" MeTTa programs on
+; a meta-level in MeTTa itself, so this behavior of `match`
+; allows us to write code that analyzes badly typed expressions
+; within MeTTa (e.g. for self-reflective genetic programming).
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(match &self (== SocratesIsHuman SamIsMortal) Really?)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; internal call doesn't pass type check even if wrapped
+; by a function with type parameter:
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; let binds without type checking, but errors when used
+!(let $x (+ 5 "S") $x)
+(: f (-> $t Number))
+!(assertEqualToResult
+   (f (+ 5 "S"))
+   ((Error "S" BadType)))
diff --git a/tests/direct_comp/peasy/e1_kb_write.metta b/tests/direct_comp/peasy/e1_kb_write.metta
new file mode 100644
index 00000000000..377e45f2f78
--- /dev/null
+++ b/tests/direct_comp/peasy/e1_kb_write.metta
@@ -0,0 +1,34 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; MeTTa allows to use a separate knowledge base (Space) &kb
+; to accumulate inferred knowledge
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Bind &kb to a new empty Space
+!(bind! &kb (new-space))
+
+; Some knowledge
+(= (frog $x)
+   (and (croaks $x)
+        (eat_flies $x)))
+(= (croaks Fritz) True)
+(= (eat_flies Fritz) True)
+(= (croaks Sam) True)
+(= (eat_flies Sam) True)
+(= (green $x)
+   (frog $x))
+
+; Define conditional
+(: ift (-> Bool Atom Atom))
+(= (ift True $then) $then)
+
+; For anything that is green, assert it is Green in &kb
+; There should be two green things
+!(assertEqualToResult
+  (ift (green $x)
+       (add-atom &kb (Green $x)))
+  (() ()))
+
+; Retrieve the inferred Green things: Fritz and Sam.
+!(assertEqualToResult
+  (match &kb (Green $x) $x)
+  (Fritz Sam))
diff --git a/tests/direct_comp/peasy/e2_states.metta b/tests/direct_comp/peasy/e2_states.metta
new file mode 100644
index 00000000000..ccdd62f1e84
--- /dev/null
+++ b/tests/direct_comp/peasy/e2_states.metta
@@ -0,0 +1,99 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; State atoms
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `new-state` creates a new state atom wrapping the initial value (A B).
+; Then it binds this state atom to the token `&state-token`,
+; which is replaced by the corresponding atom at parse-time.
+!(bind! &state-token (new-state (A B)))
+
+; &state-token is replaced by the state atom in the code below its creation
+; we wrap it into a function to show that it's not the token that changes, but
+; the content of the state atom
+(= (get-token) &state-token)
+
+; `new-state $x` creates a `(State $x)` structure,
+; and `get-token` will show its content
+!(assertEqual
+   (get-state (get-token))
+   (A B))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; States can be equal even if they are wrapped into different state atoms
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+   (get-token)
+   (new-state (A B)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; State atoms are of StateMonad type
+; These are inferred types based on new-state and change-state! signatures
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (get-type (new-state 2))
+  (StateMonad Number))
+
+!(assertEqual
+  (get-type (change-state! (new-state "S") "V"))
+  (StateMonad String))
+
+; These are the types of State grounded atom
+!(assertEqual
+  (let $v (new-state 1) (get-type $v))
+  (StateMonad Number))
+
+; atm, meta-types for states of non-grounded types are used
+!(assertEqual
+  (get-type &state-token)
+  (StateMonad Expression))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; State atoms have a defined type based on initial state
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; &state-token was initialized with state of type (A B), so
+; it cannot be changed to int
+;!(rtrace!
+!(assertEqual
+  (change-state! &state-token 1)
+  (Error 1 BadType))
+   ;)
+
+; the new state here is int, so it cannot be changed to string
+!(assertEqual
+  (change-state! (new-state 1) "S")
+  (Error "S" BadType))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Changing the content of the state atom
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; nop is used to ignore the result and return unit
+; as expected by unit tests
+!(nop (change-state! &state-token (C D)))
+
+; The same state atom has different content now
+!(assertEqual
+   (get-state (get-token))
+   (C D))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; MeTTa provides proper encapsulated state manipulation
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; scoping doesn't conflict between let bound variables and state atom types.
+!(assertEqual
+  (let $x (new-state 1)
+     (change-state! $x (+ (get-state $x) 1)))
+  (new-state 2))
+
+; Checking that there is no conflict between variable names in
+; let-expression and type definition of new-state
+!(assertEqual
+   (let $tnso (new-state 1) $tnso)
+   (new-state 1))
+
+; FIXME: doesn't work as for 25 May 2023
+; !(get-state (let $x (new-state 1) $x))
diff --git a/tests/direct_comp/peasy/e3_match_states.metta b/tests/direct_comp/peasy/e3_match_states.metta
new file mode 100644
index 00000000000..00fe3606560
--- /dev/null
+++ b/tests/direct_comp/peasy/e3_match_states.metta
@@ -0,0 +1,61 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; This function creates a symbolic expression, which wraps a novel state,
+; and puts it into &self.
+; This is a way to address particular state atoms without creating
+; unique tokens for them (it can be used for any grounded atom)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(= (new-goal-status! $goal $status)
+    (let $new-state (new-state $status)
+         (add-atom &self
+		   (= (status (Goal $goal)) $new-state))
+    )
+)
+
+! (new-goal-status! lunch-order inactive)
+! (new-goal-status! meditation inactive)
+
+; We can use `status` as a function to access corresponding state
+!(assertEqual
+  (get-state (status (Goal lunch-order)))
+  inactive)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `status` returns a `State`, which can be altered
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; `nop` is used only to get () for passing unit tests
+!(nop (change-state! (status (Goal lunch-order)) active))
+
+; The result is now different. This might be surprising, since
+; the content of Space is not changed. However, this is the whole
+; intention behind states: the atom remains the same, and we don't
+; need to reinsert it into Space, but the state it wraps changes
+; (even if it is inside equality).
+!(assertEqual
+  (get-state (status (Goal lunch-order)))
+  active)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Introducing tokens for states is not recommended, because these states are mutable
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(bind! &state-active (new-state active))
+!(nop (change-state! &state-active inactive))
+; We cannot put `(new-state active)` inside `match`, because it doesn't
+; reduce the input pattern expression. Instead, we should use
+; `(let $state-active (new-state active)) ...) here.
+
+; In any case, direct matching against expressions with states work:
+!(assertEqual
+    (match &self (= (status (Goal $goal)) &state-active) $goal)
+    meditation)
+
+; But we can also find all goal statuses, unwrap them from State,
+; and compare to the desirable result
+!(assertEqual
+  (if (== (get-state (status (Goal $goal)))
+          active)
+      $goal
+      (superpose ()))
+  lunch-order)
diff --git a/tests/direct_comp/peasy/f1_imports.metta b/tests/direct_comp/peasy/f1_imports.metta
new file mode 100755
index 00000000000..322fe038fad
--- /dev/null
+++ b/tests/direct_comp/peasy/f1_imports.metta
@@ -0,0 +1,120 @@
+; NOTE: This test won't work outside the test environment because it relies on
+;  specific atoms in a specific order in the space, and loading the default environment's
+;  init.metta will break the assumptions in this test
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Even at the very beginning of the main script `(get-atoms &self)`
+; returns one atom, which wraps the space of stdlib.
+; The type of this atom is the same as of `&self`
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;!(get-atoms &self)
+;;!(get-type (get-atoms &self))
+!(get-type &self)
+
+!(assertEqual
+  ((let $x (get-atoms &self) (get-type $x)))
+  ((get-type &self)))
+
+; stdlib is already loaded
+!(assertEqual
+  (if (> 1 2) 1 2)
+  2)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Importing the module into new space
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(import! &m f1_moduleA.metta)
+
+; It's first atom is a space
+;!(assertEqual
+;  (let* (($x (collapse (get-atoms &m)))
+;         ($y (car-atom $x)))
+;        (get-type $y))
+;  (get-type &self))
+
+
+; FIXME? Now, it is moduleC space.
+;        Should it be `stdlib` atom for a separately imported space
+; !(let $x (collapse (get-atoms &m)) (car-atom $x))
+
+
+; MeTTLog:  xlisting('&m').
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Without additional means like `(&m.f 2)` notation or `(interpret &m (f 2))`,
+; we cannot execute functions from the separate space - we can only use `match`.
+; Although `&m` imports another space with definition of `g`, it is not reduced
+; because it is not defined in the context of `&self`. This is the expected
+; behavior, but it shows that this way of importing spaces is not too useful
+; for importing modules with functions.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(assertEqual
+  (match &m (= (f 2) $x) $x)
+  (g 3))
+
+; Importing the same space into `&self` should break nothing
+; TODO? If stdlib space would be in `&m`, which should check that it is not
+; there anymore since in should be removed after importing it to `&self`
+!(import! &self f1_moduleA.metta)
+
+; Now indirectly imported `g` works and `f` fully works
+!(assertEqual (g 2) 102)
+!(assertEqual (f 2) 103)
+
+
+
+; MeTTLog:  xlisting('&self').
+
+
+; `&self` contains 3 atoms-spaces now:
+; - stdlib
+; - moduleC imported by moduleA and removed from A after its import to &self
+; - moduleA itself, which is the same as &m
+!(assertEqual &m
+  (let* (($a (collapse (get-atoms &self)))
+          ($x (cdr-atom $a))
+          ($y (cdr-atom $x)))
+         (car-atom $y)))
+
+; NOTE: now the first atom, which was a space, is removed from `&m`,
+; because we load modules only once, and we collect atoms-spaces to
+; prevent duplication
+!(assertEqual
+  (== (let* (($x (collapse (get-atoms &m)))
+             ($y (car-atom $x)))
+            (get-type $y))
+        (get-type &self))
+   False)
+
+; Let's check that `if` from stdlib is not duplicated and gives only one result
+!(assertEqual
+  (if (> 1 2) 1 2)
+  2)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Let's import one more module into `&self` with a diamond dependence
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(import! &self f1_moduleB.metta)
+; `g` from moduleC imported via two paths as well as `f`, which uses `g`,
+; are not duplicated and produce deterministic results
+!(assertEqual (g 2) 102)
+!(assertEqual (f 2) 103)
+
+; Function declared in different imported modules will still produce
+; non-deterministic results
+!(assertEqualToResult
+  (dup 2)
+  (12 102))
+
+; Let's import f1_moduleB.metta once more using a different path.
+; Such import should be ignored and thus f, g and dup should remain
+; unchanged.
+!(import! &self ../hyperon-experimental_scripts/f1_moduleB.metta)
+!(assertEqual (g 2) 102)
+!(assertEqual (f 2) 103)
+!(assertEqualToResult
+  (dup 2)
+  (12 102))
diff --git a/tests/direct_comp/peasy/f1_moduleA.metta b/tests/direct_comp/peasy/f1_moduleA.metta
new file mode 100755
index 00000000000..545aa533ccb
--- /dev/null
+++ b/tests/direct_comp/peasy/f1_moduleA.metta
@@ -0,0 +1,17 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Example file used by f1_imports.metta
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(import! &self f1_moduleC.metta)
+
+; FIXME? stdlib space is not available at importing time -
+; only tokens / grounded operations work, while symbolic functions
+; (like `if`) don't work.
+; FIXME? Exceptions are not caught by `importOp`
+!(assertEqual (+ 1 2) 3)
+!(assertEqual (if True "S" "F") "S")
+
+(= (dup $x) (if (== $x 0) (+ $x 10) (g $x)))
+
+(: f (-> Number Number))
+(= (f $x) (if (< $x 0) (- 0 $x) (g (+ 1 $x))))
diff --git a/tests/direct_comp/peasy/f1_moduleB.metta b/tests/direct_comp/peasy/f1_moduleB.metta
new file mode 100644
index 00000000000..c58eecde0b3
--- /dev/null
+++ b/tests/direct_comp/peasy/f1_moduleB.metta
@@ -0,0 +1,7 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Example file used by f1_imports.metta
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+!(import! &self f1_moduleC.metta)
+
+(= (dup $x) (if (== $x 0) (g $x) (+ $x 10)))
diff --git a/tests/direct_comp/peasy/f1_moduleC.metta b/tests/direct_comp/peasy/f1_moduleC.metta
new file mode 100644
index 00000000000..db630b5d828
--- /dev/null
+++ b/tests/direct_comp/peasy/f1_moduleC.metta
@@ -0,0 +1,9 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Example file used by f1_imports.metta
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(: __g (-> Number))
+(= (__g) 100)
+
+(: g (-> Number Numer))
+(= (g $x) (+ $x (__g)))
diff --git a/tests/direct_comp/peasy/g1_docs.metta b/tests/direct_comp/peasy/g1_docs.metta
new file mode 100644
index 00000000000..c6178108693
--- /dev/null
+++ b/tests/direct_comp/peasy/g1_docs.metta
@@ -0,0 +1,117 @@
+; This script demonstrates how one can document MeTTa code and get
+; help using the documenatation.
+
+; Let's document a function which has two arguments and returns value.
+; One can use `@doc` expression to do it. First argument of the expression is an
+; atom being documented. Other arguments describe the atom, describe function
+; parameters and return value.
+(@doc some-func
+     (@desc "Test function")
+     (@params (
+              (@param "First argument")
+              (@param "Second argument")
+              ))
+     (@return "Return value")
+     )
+; Function type is required to document the function
+(: Arg1Type Type)
+(: Arg2Type Type)
+(: ReturnType Type)
+(: some-func (-> Arg1Type Arg2Type ReturnType))
+
+; `get-doc` function returns a `@doc-formal` expression which contains the full
+; documentation of the atom including user defined description and types.
+!(assertEqual
+   (get-doc some-func)
+   (@doc-formal (@item some-func) (@kind function)
+               (@type (-> Arg1Type Arg2Type ReturnType))
+               (@desc "Test function")
+               (@params (
+                        (@param (@type Arg1Type) (@desc "First argument"))
+                        (@param (@type Arg2Type) (@desc "Second argument"))))
+               (@return (@type ReturnType) (@desc "Return value"))))
+
+; Same approach can be used to document single atom of any @kind.
+(@doc SomeSymbol (@desc "Test symbol atom having specific type"))
+(: SomeSymbol SomeType)
+
+!(assertEqual
+   (get-doc SomeSymbol)
+   (@doc-formal (@item SomeSymbol) (@kind atom) (@type SomeType)
+               (@desc "Test symbol atom having specific type")))
+
+; Grounded atoms are also can be documented using `@doc` expressions. Type of
+; the grounded atom is a part of its implementation.
+(@doc some-gnd-atom
+     (@desc "Test function")
+     (@params (
+              (@param "First argument")
+              (@param "Second argument")
+              ))
+     (@return "Return value")
+     )
+
+; As some-gnd-function is not imported really in this example type is not
+; available and @doc-formal contains %Undefined% instead.
+!(assertEqual
+   (get-doc some-gnd-atom)
+   (@doc-formal (@item some-gnd-atom) (@kind function)
+               (@type %Undefined%)
+               (@desc "Test function")
+               (@params (
+                        (@param (@type %Undefined%) (@desc "First argument"))
+                        (@param (@type %Undefined%) (@desc "Second argument"))))
+               (@return (@type %Undefined%) (@desc "Return value"))))
+
+; If atom is not documented then `get-doc` returns "No documentation"
+; description.
+!(assertEqual
+   (get-doc NoSuchAtom)
+   (@doc-formal (@item NoSuchAtom) (@kind atom) (@type %Undefined%) (@desc "No documentation")))
+
+; Same result is returned if for instance documentation for the function
+; application is queried.
+!(assertEqual
+   (get-doc (some-func arg1 arg2))
+   (@doc-formal (@item (some-func arg1 arg2)) (@kind atom) (@type ReturnType) (@desc "No documentation")))
+
+; `help!` function gets the documentation and prints it in a human readable
+; format.
+!(help! some-func)
+; Output:
+;
+; Function some-func: (-> Arg1Type Arg2Type ReturnType) Test function
+; Parameters:
+;   Arg1Type First argument
+;   Arg2Type Second argument
+; Return: (@type ReturnType) Return value
+;
+
+!(help! SomeSymbol)
+; Output:
+;
+; Atom SomeSymbol: SomeType Test symbol atom having specific type
+;
+
+!(help! some-gnd-atom)
+; Output:
+;
+; Function some-gnd-atom: %Undefined% Test function
+; Parameters:
+;   %Undefined% First argument
+;   %Undefined% Second argument
+; Return: (@type %Undefined%) Return value
+;
+
+
+!(help! NoSuchAtom)
+; Output:
+;
+; Atom NoSuchAtom: %Undefined% No documentation
+;
+
+!(help! (some-func arg1 arg2))
+; Output:
+;
+; Atom (some-func arg1 arg2): ReturnType No documentation
+;
diff --git a/tests/direct_comp/00a_lang_compiled_case.metta b/tests/direct_comp/previous/00a_lang_compiled_case.metta
similarity index 100%
rename from tests/direct_comp/00a_lang_compiled_case.metta
rename to tests/direct_comp/previous/00a_lang_compiled_case.metta
diff --git a/tests/direct_comp/add_atom_match.metta b/tests/direct_comp/previous/add_atom_match.metta
similarity index 100%
rename from tests/direct_comp/add_atom_match.metta
rename to tests/direct_comp/previous/add_atom_match.metta
diff --git a/tests/direct_comp/compiler_walkthru.metta b/tests/direct_comp/previous/compiler_walkthru.metta
similarity index 100%
rename from tests/direct_comp/compiler_walkthru.metta
rename to tests/direct_comp/previous/compiler_walkthru.metta
diff --git a/tests/direct_comp/define_if_like.metta b/tests/direct_comp/previous/define_if_like.metta
similarity index 100%
rename from tests/direct_comp/define_if_like.metta
rename to tests/direct_comp/previous/define_if_like.metta
diff --git a/tests/performance/compare_algo/nqueens/format_args_ordered.metta b/tests/performance/compare_algo/nqueens/mqueens_ordered.metta
similarity index 93%
rename from tests/performance/compare_algo/nqueens/format_args_ordered.metta
rename to tests/performance/compare_algo/nqueens/mqueens_ordered.metta
index 9661dbe1d30..1d9f499af4d 100644
--- a/tests/performance/compare_algo/nqueens/format_args_ordered.metta
+++ b/tests/performance/compare_algo/nqueens/mqueens_ordered.metta
@@ -29,7 +29,5 @@
 (= (nqueens $n)
     (let $r (range 1 $n) (nqueens_aux $r ())))
 
-; !(call-string ":- time(findall(X,mc__nqueens(12,X),_)).")
-
-!(nqueens 7)
+!(nqueens 12)
 
diff --git a/tests/performance/compare_algo/nqueens/format_args_ordered.metta.pl b/tests/performance/compare_algo/nqueens/mqueens_ordered.metta.md
similarity index 96%
rename from tests/performance/compare_algo/nqueens/format_args_ordered.metta.pl
rename to tests/performance/compare_algo/nqueens/mqueens_ordered.metta.md
index 2fa383999ab..a2afb86f4ca 100644
--- a/tests/performance/compare_algo/nqueens/format_args_ordered.metta.pl
+++ b/tests/performance/compare_algo/nqueens/mqueens_ordered.metta.md
@@ -1,7 +1,5 @@
-
-:- ensure_loaded('/home/deb12user/metta-wam-royward-dev/src/canary/metta_runtime').
-
 /*
+```metta
 ;           #(set_option_value compat false)
 ;           #(set_option_value compatio false)
 ;           #(set_option_value src_indents false)
@@ -30,16 +28,16 @@
 ;         #(set_option_value html true)
 ;         #(is_cmd_option execute compile --compile=save save)
 ;          #(set_option_value compile save)
-
+```
+```info
 ; #( : user #(load_metta_file &self tests/direct_comp/easy/format_args_ordered.metta) )
 ;                       #(track_load_into_file /home/deb12user/metta-wam/tests/direct_comp/easy/format_args_ordered.metta)
 ;                                        #(load_answer_file /home/deb12user/metta-wam/tests/direct_comp/easy/format_args_ordered.metta.answers /home/deb12user/metta-wam/tests/direct_comp/easy/format_args_ordered.metta)
 Info: File /home/deb12user/metta-wam/tests/direct_comp/easy/format_args_ordered.metta is 1.14K bytes (35 lines)
 ;                                        #(load_answer_file /home/deb12user/metta-wam/tests/direct_comp/easy/format_args_ordered.metta.answers /home/deb12user/metta-wam/tests/direct_comp/easy/format_args_ordered.metta)
+```metta
 ;;; (= (select $x) ((car-atom $x) (cdr-atom $x)))
 ;;; (= (select $x) (let* (($y (car-atom $x)) ($z (cdr-atom $x)) (($u $v) (select $z))) ($u (cons-atom $y $v))))
-```
-```metta
  (= (select $x)
   (if
     (== $x ())
@@ -408,6 +406,15 @@
   (let $r
     (range 1 $n)
     (nqueens_aux $r ())))
+
+
+
+    (add-atom (lessThan Nat Nat))
+body1  (add-atom    (= (lessThan $x $y) ..)
+    (add-atom (lessThan Int Int))
+body2  (add-atom (= (lessThan $x $y) ..)
+    (add-atom (lessThan Number Number))
+
 ```
 ```load
 ; Action: load=metta_atom_asserted('&self',[=,[nqueens,_n],[let,_r,[range,1,_n],[nqueens_aux,_r,[]]]])
@@ -426,8 +433,15 @@
 ```
 ```prolog
 */
-
-mc__nqueens(_n, A) :-
+src(
+ my_src([=,[nqueens,_n],[let,_r,[range,1,_n],[nqueens_aux,_r,[]]),
+    mc__nqueens(_n, A) :-
+        mc__range(1, _n, _r),
+        B=[],
+        mc__nqueens_aux(_r, B, A)).
+
+mc__nqueens(_n01, _n11, A) :-
+    argcksOut(mc__nqueens,[_n01, _n11],[_n010, _n11O]),
     mc__range(1, _n, _r),
     B=[],
     mc__nqueens_aux(_r, B, A).
@@ -441,10 +455,10 @@
 ```prolog
 */
 
-%:- do_metta_runtime(A, mc__nqueens(12, A)).
+:- do_metta_runtime(A, mc__nqueens(7, A)).
 %:- do_metta_runtime(A, mc__nqueens(13, A)).
 %:- do_metta_runtime(A, mc__nqueens(14, A)). 500 secs
-:- do_metta_runtime(A, mc__nqueens(15, A)).
+%:- do_metta_runtime(A, mc__nqueens(15, A)).
 %:- do_metta_runtime(A, mc__nqueens(16, A)).
 
 
diff --git a/tests/performance/compare_algo/nqueens/format_args_ordered_low_overhead.pl b/tests/performance/compare_algo/nqueens/mqueens_ordered_low_overhead.pl
similarity index 100%
rename from tests/performance/compare_algo/nqueens/format_args_ordered_low_overhead.pl
rename to tests/performance/compare_algo/nqueens/mqueens_ordered_low_overhead.pl
diff --git a/tests/performance/compare_algo/nqueens/n_queens.pl b/tests/performance/compare_algo/nqueens/n_queens.pl
new file mode 100644
index 00000000000..84bba6945ce
--- /dev/null
+++ b/tests/performance/compare_algo/nqueens/n_queens.pl
@@ -0,0 +1,72 @@
+
+% N-Queens Solver optimized with backtracking to find all solutions
+n_queens(N, Solutions) :-
+    length(Board, N),
+    nums_list(1, N, List),
+    findall(Board, place_queens(List, Board), Solutions).
+
+% Generate a list of numbers from Start to End
+nums_list(Start, End, [Start|Rest]) :-
+    Start =< End,
+    NewStart is Start + 1,
+    nums_list(NewStart, End, Rest).
+nums_list(Start, End, []) :-
+    Start > End.
+
+% Place queens on the board ensuring safety
+place_queens([], []).
+place_queens(Available, [Queen|Rest]) :-
+    select(Queen, Available, NextAvailable),
+    place_queens(NextAvailable, Rest),
+    safe_position(Queen, Rest, 1).
+
+% Check safe placement: no queens attack each other
+safe_position(_, [], _).
+safe_position(Queen, [Other|Rest], Dist) :-
+    Queen \= Other,
+    abs(Queen - Other) =\= Dist,
+    NextDist is Dist + 1,
+    safe_position(Queen, Rest, NextDist).
+
+
+:- current_prolog_flag(stack_limit,X),X_16 is X * 16, set_prolog_flag(stack_limit,X_16).
+
+nqueens(N, L):- n_queens(N, L).
+
+% N-Queens Solver optimized with backtracking to find all solutions
+aqueens(N, Solutions) :-
+    findall(Board, nqueens(N, Board), Solutions).
+
+% Function to solve N-Queens for a given N and time it
+time_sols(Solutions, Call) :-
+    statistics(runtime, [StartCPU, _]),
+    statistics(walltime, [StartWall, _]),
+
+    copy_term(Call, Copy), numbervars(Copy, 0, _),
+    once(Call),
+
+    statistics(runtime, [EndCPU, _]),
+    statistics(walltime, [EndWall, _]),
+
+    CPUTime is EndCPU - StartCPU,
+    WallTime is EndWall - StartWall,
+
+    length(Solutions, NumSolutions),
+    format("N = ~q: Found ~d solution(s) in ~d ms (CPU) and ~d ms (Wall)\n",
+           [Copy, NumSolutions, CPUTime, WallTime]).
+
+:- use_module(library(lists)).
+:- use_module(library(between)).
+
+% Main function to solve the N-Queens problem for sizes S to E
+solve_for_sizes(S, E) :-
+    between(S, E, N),
+    format("Solving for N = ~d\n", [N]),
+    % time_sols([OneSol], nqueens(N, OneSol)),
+    time_sols(Solutions, aqueens(N, Solutions)),
+    fail; % Forces Prolog to backtrack and try the next N
+    true.
+
+% Run the main function
+:- solve_for_sizes(10, 15).
+
diff --git a/tests/performance/compare_algo/nqueens/n_queens_clpfd_sics.pl b/tests/performance/compare_algo/nqueens/n_queens_clpfd_sics.pl
new file mode 100644
index 00000000000..46e53e54659
--- /dev/null
+++ b/tests/performance/compare_algo/nqueens/n_queens_clpfd_sics.pl
@@ -0,0 +1,81 @@
+:- use_module(library(clpfd)).
+
+queens(N, L, LabelingType) :-
+     length(L, N),
+     domain(L, 1, N),
+     constrain_all(L),
+     labeling(LabelingType, L).
+
+constrain_all([]).
+constrain_all([X|Xs]) :-
+     constrain_between(X, Xs, 1),
+     constrain_all(Xs).
+
+constrain_between(_X, [], _N).
+constrain_between(X, [Y|Ys], N) :-
+     no_threat(X, Y, N),
+     N1 is N+1,
+     constrain_between(X, Ys, N1).
+
+no_threat(X, Y, I) :-
+        X   #\= Y,
+        X+I #\= Y,
+        X-I #\= Y.
+
+% version 1: weak but efficient
+no_threat(X, Y, I) +:
+     X in \({Y} \/ {Y+I} \/ {Y-I}),
+     Y in \({X} \/ {X+I} \/ {X-I}).
+
+/*
+% version 2: strong but very inefficient version
+no_threat(X, Y, I) +:
+    X in unionof(B,dom(Y),\({B} \/ {B+I} \/ {B-I})),
+    Y in unionof(B,dom(X),\({B} \/ {B+I} \/ {B-I})).
+
+% version 3: strong but somewhat inefficient version
+no_threat(X, Y, I) +:
+    X in (4..card(Y)) ? (inf..sup) \/
+          unionof(B,dom(Y),\({B} \/ {B+I} \/ {B-I})),
+    Y in (4..card(X)) ? (inf..sup) \/
+          unionof(B,dom(X),\({B} \/ {B+I} \/ {B-I})).
+*/
+
+nqueens(N, L):- queens(N, L, [ff]).
+
+% N-Queens Solver optimized with backtracking to find all solutions
+aqueens(N, Solutions) :-
+    findall(Board, nqueens(N, Board), Solutions).
+
+% Function to solve N-Queens for a given N and time it
+time_sols(Solutions, Call) :-
+    statistics(runtime, [StartCPU, _]),
+    statistics(walltime, [StartWall, _]),
+
+    copy_term(Call, Copy), numbervars(Copy, 0, _),
+    once(Call),
+
+    statistics(runtime, [EndCPU, _]),
+    statistics(walltime, [EndWall, _]),
+
+    CPUTime is EndCPU - StartCPU,
+    WallTime is EndWall - StartWall,
+
+    length(Solutions, NumSolutions),
+    format("N = ~q: Found ~d solution(s) in ~d ms (CPU) and ~d ms (Wall)\n",
+           [Copy, NumSolutions, CPUTime, WallTime]).
+
+:- use_module(library(between)).
+
+% Main function to solve the N-Queens problem for sizes S to E
+solve_for_sizes(S, E) :-
+    between(S, E, N),
+    format("Solving for N = ~d\n", [N]),
+    % time_sols([OneSol], nqueens(N, OneSol)),
+    time_sols(Solutions, aqueens(N, Solutions)),
+    fail; % Forces Prolog to backtrack and try the next N
+    true.
+
+% Run the main function
+:- solve_for_sizes(10, 15).
+
diff --git a/tests/performance/compare_algo/nqueens/nqueens_compiled.pl b/tests/performance/compare_algo/nqueens/nqueens_compiled.pl
new file mode 100644
index 00000000000..d43a5744e62
--- /dev/null
+++ b/tests/performance/compare_algo/nqueens/nqueens_compiled.pl
@@ -0,0 +1,163 @@
+
+'mc__+'(A,B,R) :- number(A),number(B),!,plus(A,B,R).
+'mc__+'(A,B,['+',A,B]).
+
+'mc__-'(A,B,R) :- number(A),number(B),!,plus(B,R,A).
+'mc__-'(A,B,['-',A,B]).
+
+'mc__*'(A,B,R) :- number(A),number(B),!,R is A*B.
+'mc__*'(A,B,['*',A,B]).
+
+%%%%%%%%%%%%%%%%%%%%% logic
+
+mc__and(A,B,B):- atomic(A), A\=='False', A\==0.
+mc__and(_,_,'False').
+
+mc__or(A,B,B):- (\+ atomic(A); A='False'; A=0), !.
+mc__or(_,_,'True').
+
+%%%%%%%%%%%%%%%%%%%%% comparison
+
+'mc__=='(A,A,1) :- !.
+'mc__=='(_,_,0).
+
+'mc__<'(A,B,R) :- number(A),number(B),!,(A<B -> R=1 ; R=0).
+'mc__<'(A,B,['<',A,B]).
+
+%%%%%%%%%%%%%%%%%%%%% lists
+
+'mc__car-atom'([H|_],H).
+
+'mc__cdr-atom'([_|T],T).
+
+'mc__cons-atom'(A,B,[A|B]).
+
+%%%%%%%%%%%%%%%%%%%%% misc
+
+'mc__empty'(_) :- fail.
+
+is_True(T):- atomic(T), T\=='False', T\==0.
+
+%%%%%%%%%%%%%%%%%%%%% nqueens
+
+(If *-> Then ; Else):- if(If, Then, Else).
+
+mc__select(A, B) :-
+    (   C=[],
+        'mc__=='(A, C, D),
+        is_True(D)
+    *-> mc__empty(E),
+        B=E
+    ;   'mc__car-atom'(A, F),
+        'mc__cdr-atom'(A, G),
+        B=[F, G]
+    ).
+mc__select(A, B) :-
+    (   C=[],
+        'mc__=='(A, C, D),
+        is_True(D)
+    *-> mc__empty(E),
+        B=E
+    ;   'mc__car-atom'(A, F),
+        'mc__cdr-atom'(A, G),
+        mc__select(G, H),
+        H=[I, J],
+        'mc__cons-atom'(F, J, K),
+        B=[I, K]
+    ).
+
+mc__range(A, B, C) :-
+    (   'mc__=='(A, B, D),
+        is_True(D)
+    *-> C=[A]
+    ;   'mc__+'(A, 1, E),
+        mc__range(E, B, F),
+        'mc__cons-atom'(A, F, G),
+        C=G
+    ).
+
+mc__nqueens_aux(A, B, C) :-
+    (   D=[],
+        'mc__=='(A, D, E),
+        is_True(E)
+    *-> C=B
+    ;   mc__select(A, F),
+        F=[G, H],
+        (   mc__not_attack(G, 1, B, I),
+            is_True(I)
+        *-> 'mc__cons-atom'(G, B, J),
+            mc__nqueens_aux(H, J, K),
+            L=K
+        ;   mc__empty(M),
+            L=M
+        ),
+        C=L
+    ).
+
+mc__not_attack(A, B, C, D) :-
+    (   E=[],
+        'mc__=='(C, E, F),
+        is_True(F)
+    *-> G='True',
+        D=G
+    ;   'mc__car-atom'(C, H),
+        'mc__cdr-atom'(C, I),
+        (   'mc__=='(A, H, J),
+            'mc__+'(B, H, K),
+            'mc__=='(A, K, L),
+            'mc__+'(A, B, M),
+            'mc__=='(H, M, N),
+            mc__or(L, N, O),
+            mc__or(J, O, P),
+            is_True(P)
+        *-> Q='False',
+            R=Q
+        ;   'mc__+'(B, 1, S),
+            mc__not_attack(A, S, I, T),
+            R=T
+        ),
+        D=R
+    ).
+
+nqueens(A, B) :-
+    mc__range(1, A, C),
+    D=[], !,
+    mc__nqueens_aux(C, D, B).
+
+% N-Queens Solver optimized with backtracking to find all solutions
+all_nqueens(N, Solutions) :-
+    findall(Board, nqueens(N, Board), Solutions).
+
+% Function to solve N-Queens for a given N and time it
+time_sols(Solutions, Call) :-
+    statistics(runtime, [StartCPU, _]),
+    statistics(walltime, [StartWall, _]),
+
+    copy_term(Call, Copy),
+    once(Call),
+
+    statistics(runtime, [EndCPU, _]),
+    statistics(walltime, [EndWall, _]),
+
+    CPUTime is EndCPU - StartCPU,
+    WallTime is EndWall - StartWall,
+
+    length(Solutions, NumSolutions),
+    format("N = ~q: Found ~d solution(s) in ~d ms (CPU) and ~d ms (Wall)\n",
+           [Copy, NumSolutions, CPUTime, WallTime]).
+
+:- if(exists_source(library(between))).
+:- use_module(library(between)).
+:- endif.
+
+% Main function to solve the N-Queens problem for sizes S to E
+solve_for_sizes(S, E) :-
+    between(S, E, N),
+    format("Solving for N = ~d\n", [N]),
+    time_sols([OneSol], nqueens(N, OneSol)),
+    time_sols(Solutions, all_nqueens(N, Solutions)),
+    fail; % Forces Prolog to backtrack and try the next N
+    true.
+
+% Run the main function
+:- solve_for_sizes(10, 15).
diff --git a/tests/performance/compare_algo/nqueens/nqueens_compiled_sics.pl b/tests/performance/compare_algo/nqueens/nqueens_compiled_sics.pl
new file mode 100644
index 00000000000..7e234a8a512
--- /dev/null
+++ b/tests/performance/compare_algo/nqueens/nqueens_compiled_sics.pl
@@ -0,0 +1,160 @@
+
+'mc__+'(A,B,R) :- number(A),number(B),!,R is A+B.
+'mc__+'(A,B,['+',A,B]).
+
+'mc__-'(A,B,R) :- number(A),number(B),!,R is A-B.
+'mc__-'(A,B,['-',A,B]).
+
+'mc__*'(A,B,R) :- number(A),number(B),!,R is A*B.
+'mc__*'(A,B,['*',A,B]).
+
+%%%%%%%%%%%%%%%%%%%%% logic
+
+mc__and(A,B,B):- atomic(A), A\=='False', A\==0.
+mc__and(_,_,'False').
+
+mc__or(A,B,B):- ( \+ atomic(A); A='False'; A=0), !.
+mc__or(_,_,'True').
+
+%%%%%%%%%%%%%%%%%%%%% comparison
+
+'mc__=='(A,A,1) :- !.
+'mc__=='(_,_,0).
+
+'mc__<'(A,B,R) :- number(A),number(B),!,(A<B -> R=1 ; R=0).
+'mc__<'(A,B,['<',A,B]).
+
+%%%%%%%%%%%%%%%%%%%%% lists
+
+'mc__car-atom'([H|_],H).
+
+'mc__cdr-atom'([_|T],T).
+
+'mc__cons-atom'(A,B,[A|B]).
+
+%%%%%%%%%%%%%%%%%%%%% misc
+
+'mc__empty'(_) :- fail.
+
+is_True(T):- atomic(T), T\=='False', T\==0.
+
+%%%%%%%%%%%%%%%%%%%%% nqueens
+
+
+mc__select(A, B) :-
+    if((  C=[],
+        'mc__=='(A, C, D),
+        is_True(D)
+    ),( mc__empty(E),
+        B=E
+    ),(   'mc__car-atom'(A, F),
+        'mc__cdr-atom'(A, G),
+        B=[F, G]
+    )).
+mc__select(A, B) :-
+    if((   C=[],
+        'mc__=='(A, C, D),
+        is_True(D)
+    ),( mc__empty(E),
+        B=E
+    ),(   'mc__car-atom'(A, F),
+        'mc__cdr-atom'(A, G),
+        mc__select(G, H),
+        H=[I, J],
+        'mc__cons-atom'(F, J, K),
+        B=[I, K]
+    )).
+
+mc__range(A, B, C) :-
+    if((   'mc__=='(A, B, D),
+        is_True(D)
+    ),( C=[A]
+    ),(   'mc__+'(A, 1, E),
+        mc__range(E, B, F),
+        'mc__cons-atom'(A, F, G),
+        C=G
+    )).
+
+mc__nqueens_aux(A, B, C) :-
+    if((   D=[],
+        'mc__=='(A, D, E),
+        is_True(E)
+    ),( C=B
+    ),(   mc__select(A, F),
+        F=[G, H],
+        if((   mc__not_attack(G, 1, B, I),
+            is_True(I)
+        ),( 'mc__cons-atom'(G, B, J),
+            mc__nqueens_aux(H, J, K),
+            L=K
+        ),(   mc__empty(M),
+            L=M
+        )),
+        C=L
+    )).
+
+mc__not_attack(A, B, C, D) :-
+    if((   E=[],
+        'mc__=='(C, E, F),
+        is_True(F)
+    ),( G='True',
+        D=G
+    ),(   'mc__car-atom'(C, H),
+        'mc__cdr-atom'(C, I),
+        if((   'mc__=='(A, H, J),
+            'mc__+'(B, H, K),
+            'mc__=='(A, K, L),
+            'mc__+'(A, B, M),
+            'mc__=='(H, M, N),
+            mc__or(L, N, O),
+            mc__or(J, O, P),
+            is_True(P)
+        ),( Q='False',
+            R=Q
+        ),(   'mc__+'(B, 1, S),
+            mc__not_attack(A, S, I, T),
+            R=T
+        )),
+        D=R
+    )).
+
+nqueens(A, B) :-
+    mc__range(1, A, C),
+    D=[], !,
+    mc__nqueens_aux(C, D, B).
+
+% N-Queens Solver optimized with backtracking to find all solutions
+aqueens(N, Solutions) :-
+    findall(Board, nqueens(N, Board), Solutions).
+
+% Function to solve N-Queens for a given N and time it
+time_sols(Solutions, Call) :-
+    statistics(runtime, [StartCPU, _]),
+    statistics(walltime, [StartWall, _]),
+
+    copy_term(Call, Copy), numbervars(Copy, 0, _),
+    once(Call),
+
+    statistics(runtime, [EndCPU, _]),
+    statistics(walltime, [EndWall, _]),
+
+    CPUTime is EndCPU - StartCPU,
+    WallTime is EndWall - StartWall,
+
+    length(Solutions, NumSolutions),
+    format("N = ~q: Found ~d solution(s) in ~d ms (CPU) and ~d ms (Wall)\n",
+           [Copy, NumSolutions, CPUTime, WallTime]).
+
+:- use_module(library(between)).
+
+% Main function to solve the N-Queens problem for sizes S to E
+solve_for_sizes(S, E) :-
+    between(S, E, N),
+    format("Solving for N = ~d\n", [N]),
+    % time_sols([OneSol], nqueens(N, OneSol)),
+    time_sols(Solutions, aqueens(N, Solutions)),
+    fail; % Forces Prolog to backtrack and try the next N
+    true.
+
+% Run the main function
+:- solve_for_sizes(10, 15).
diff --git a/tests/performance/compare_algo/nqueens/nqueens_test_in_java.sh b/tests/performance/compare_algo/nqueens/nqueens_test_in_java.sh
new file mode 100755
index 00000000000..998247a3612
--- /dev/null
+++ b/tests/performance/compare_algo/nqueens/nqueens_test_in_java.sh
@@ -0,0 +1,89 @@
+#!/bin/bash
+
+# Create the Java program file
+cat > NQueensSolver.java <<'EOF'
+public class NQueensSolver {
+
+    // Check if placing a queen at (row, col) is safe
+    private static boolean isSafe(int[] board, int row, int col) {
+        for (int i = 0; i < col; i++) {
+            if (board[i] == row || Math.abs(board[i] - row) == Math.abs(i - col)) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    // Recursive backtracking solution for the N-Queens problem
+    private static void solveNQueens(int[] board, int col, int n, int[] count) {
+        if (col == n) {
+            count[0]++;
+            return;
+        }
+        for (int row = 0; row < n; row++) {
+            if (isSafe(board, row, col)) {
+                board[col] = row;
+                solveNQueens(board, col + 1, n, count);
+            }
+        }
+    }
+
+    // Solve N-Queens for a given board size
+    public static int nQueens(int n) {
+        int[] board = new int[n]; // Array to store queen positions
+        int[] count = new int[1]; // Count of solutions (use array to pass by reference)
+        solveNQueens(board, 0, n, count);
+        return count[0];
+    }
+
+    public static void main(String[] args) {
+        if (args.length != 1) {
+            System.out.println("Usage: java NQueensSolver <board size>");
+            return;
+        }
+
+        int n;
+        try {
+            n = Integer.parseInt(args[0]);
+        } catch (NumberFormatException e) {
+            System.out.println("Invalid input. Please provide an integer for the board size.");
+            return;
+        }
+
+        if (n < 1) {
+            System.out.println("Board size must be a positive integer.");
+            return;
+        }
+
+        long startTime = System.nanoTime();
+        int solutions = nQueens(n);
+        long endTime = System.nanoTime();
+
+        double timeTaken = (endTime - startTime) / 1e9; // Convert to seconds
+        System.out.printf("N=%d: %d solutions found in %.6f seconds\n", n, solutions, timeTaken);
+    }
+}
+EOF
+
+# Compile the Java program
+echo "Compiling NQueensSolver.java..."
+javac NQueensSolver.java
+
+# Check if compilation was successful
+if [ $? -ne 0 ]; then
+    echo "Compilation failed. Exiting."
+    exit 1
+fi
+
+# Benchmark the program for board sizes 4 through 15
+echo "Benchmarking N-Queens (Java implementation)"
+for n in {4..15}; do
+    echo "N=$n:"
+    /usr/bin/time -f "Elapsed Time: %E" java NQueensSolver $n
+    echo
+done
+
+# Clean up
+echo "Cleaning up..."
+rm -f NQueensSolver.java NQueensSolver.class
+