Checkpoint

src/interpreter/Preprocessor.kt

@@ -65,7 +65,7 @@ open class Preprocessor {
                     Functor.of("clause/2") -> ClauseOp(args[0] as Head, args[1] as Body)
                     Functor.of("atomic/1") -> AtomicOp(args[0])
                     Functor.of("compound/1") -> CompoundOp(args[0])
-                    Functor.of("univ/2") -> Univ(args[0], args[1])
+                    Functor.of("=../2") -> Univ(args[0], args[1])
 
                     // Arithmetic
                     Functor.of("inf/0") -> Integer(Int.MAX_VALUE)

src/parser/grammars/TermsGrammar.kt

@@ -5,8 +5,11 @@ import com.github.h0tk3y.betterParse.grammar.parser
 import com.github.h0tk3y.betterParse.parser.Parser
 import prolog.ast.arithmetic.Float
 import prolog.ast.arithmetic.Integer
+import prolog.ast.lists.List
 import prolog.ast.terms.*
 import prolog.builtins.Dynamic
+import prolog.ast.lists.List.Empty
+import prolog.ast.lists.List.Cons
 
 /**
  * Precedence is based on the following table:
@@ -65,6 +68,7 @@ open class TermsGrammar : Tokens() {
     // Base terms (atoms, compounds, variables, numbers)
     protected val baseTerm: Parser<Term> by (dummy
             or (-leftParenthesis * parser(::term) * -rightParenthesis)
+            or parser(::list)
             or compound
             or atom
             or variable
@@ -112,6 +116,20 @@ open class TermsGrammar : Tokens() {
         t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
     }
 
+    // Lists
+    protected val list: Parser<List> by (-leftBracket * separated(
+        parser(::termNoConjunction),
+        comma,
+        acceptZero = true
+    ) * -rightBracket) use {
+        var list: List = Empty
+        // Construct the list in reverse order
+        for (term in this.terms.reversed()) {
+            list = Cons(term, list)
+        }
+        list
+    }
+
     // Term - highest level expression
     protected val term: Parser<Term> by term1200
     protected val termNoConjunction: Parser<Term> by term700

src/parser/grammars/Tokens.kt

@@ -10,6 +10,8 @@ import com.github.h0tk3y.betterParse.lexer.token
 abstract class Tokens : Grammar<Any>() {
     protected val leftParenthesis: Token by literalToken("(")
     protected val rightParenthesis: Token by literalToken(")")
+    protected val leftBracket: Token by literalToken("[")
+    protected val rightBracket: Token by literalToken("]")
     protected val exclamation: Token by literalToken("!")
     // 1200
     protected val neck by literalToken(":-")

src/prolog/builtins/unificationOperators.kt

@@ -22,7 +22,7 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
         val t1 = applySubstitution(term1, subs)
         val t2 = applySubstitution(term2, subs)
 
-        yieldAll(unifyLazy(t1, t2, subs))
+        yieldAll(unifyLazy(t1, t2, emptyMap()))
     }
 
     override fun applySubstitution(subs: Substitutions): Unify = Unify(
@@ -45,7 +45,7 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
         val t1 = applySubstitution(term1, subs)
         val t2 = applySubstitution(term2, subs)
 
-        if (equivalent(t1, t2, subs)) {
+        if (equivalent(t1, t2, emptyMap())) {
             yield(Result.success(emptyMap()))
         }
     }

src/prolog/logic/unification.kt

@@ -85,6 +85,7 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
                 val args1 = structure1.arguments
                 val args2 = structure2.arguments
                 if (args1.size == args2.size) {
+                    // Keep track of the substitutions so far
                     val results = args1.zip(args2).map { (arg1, arg2) ->
                         unifyLazy(arg1, arg2, subs)
                     }
@@ -145,7 +146,11 @@ fun unify(term1: Term, term2: Term): Answer {
 fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean {
     return when {
         term1 is Atom && term2 is Atom -> compare(term1, term2, subs) == 0
-        term1 is Structure && term2 is Structure -> compare(term1, term2, subs) == 0
+        term1 is Structure && term2 is Structure -> {
+            term1.functor == term2.functor && term1.arguments.zip(term2.arguments).all { (arg1, arg2) ->
+                equivalent(arg1, arg2, subs)
+            }
+        }
         term1 is Integer && term2 is Integer -> compare(term1, term2, subs) == 0
         term1 is Number && term2 is Number -> compare(term1, term2, subs) == 0
         term1 is Variable && term2 is Variable -> term1 == term2