Elxlog v0.1.6 Prove View Source

Return value is tuple. {val,env,def} prove([predicate, y, env, def, n) y is succeeding predicate(s) env is environment. It is keyword-list n is nest level. Alpha conversion uses n to generate new variable.

prove_all(list, env, def, n)

prove_all/4 work with prove/5

prove_builtin(x, y, env, def, n)

evaluate native Elixir function change from function of elxlog to string. and eval as Elixir function

prove_pred(x, arg2, y, env, def, n)

prove_pred/6 is for predicate x is goal to prove d is set of difinition y is succeeding goals env is environment for variables n is nest lebel

reconsult(buf, def)

for builtin reconsult/1 parse file text and add difinition

trace(x, env, def, n, action)

when trace is true in def print trace data n is nest lebel action [try,succ,fail]

trace1(env, def)

unify(x, y, env)

unificate x and y env is environment. e.g. [[{:X,1},{:Y,2}],[{:Y,2},3] old variable is always left side in each environment element

unify1(x, y, xs, ys, env)

Link to this section Functions

alpha_conv(x, n)

ask(list, env)

for predicate ask/0 ask prints variables of goal

body(list)

compress_env(list, env)

debug(list, check)

debug1(list)

deref(x, env)

deref1(x, list, env)

eval(x, env)

eval/2 is for is builtin predicate evaluate formula formula e.g. [:formula,[:+,x,y]]

find_def(ls, name)

flatten_env(list)

func_to_str(list)

for builtin elixir predicate add prefix "Elxfunc"

head(list)

list_to_str(x)

for builtin predicate "elixir" change from elxlog data to string

list_to_str1(list)

list_to_str2(x)

listing(list, check)

for builtin listing/0 /1

listing1(arg1)

make_list(n)

make list [:,:,...] size n

older(x, y)

parallel1(list, env, def, n)

help function for parallel/n

parallel2(c, res)

power(x, y)

prove(list, y, env, def, n)

example

iex>Prove.prove([:builtin,[:true]],[],[],[],0) {true,[],[]} iex>Prove.prove([:builtin,[:fail]],[],[],[],0) {false,[],[]}