# trial for specifying a resolution engine with n3

# list and array primitives

# list

:list a rdfs:Class.

:l :contains {
:a :b :c.
:d :e :f.
....
:v :w :z.}

:x = {:head :of :l}.    # :x is :a :b :c.
:xs = {:tail :of :l}.   # :xs is {:d :e :f. .... :v :w :z.}

:l :add {:x :y :z}.     # l = {:x :y :z} ++ l

# :head, :tail  and :add must be interpreted by a basic program

# array

:array a rdfs:Class.

:arr :contains {
:a :b :c.
:d :e :f.
....
:v :w :z.}

:w = {:2 :element_of :l}    # :w = {:d :e :f}

{:x :y :z} :replace {:2 :element_of :array}   # array entry 2 = {:x :y :z}
{:x :y :z} :add_element :array.               # array size is augmented
                                      # with one by element {:x :y :z}


:tripleList a :list.
:tripleList :elements :triple.


:t1 a :triple.
:t2 a :triple.

:t1 is {:a :b :x}.
:t2 is {:y :d :e}.

{:subst a :substitution. :a :subst :b.} log:implies {:a a :var. :b a :term}.

{:a a :var. :b a :uri. :a :unification :b} log:implies {:a :subst :b}.
{:a a :uri. :b a :var. :a :unification :b} log:implies {:b :subst :a}.
{:a a :uri. :b a :uri. :a :unification :b} log:implies :no_unification.