unfy/unfy.3

.TH Unfy 3 "October 2017" "Version 1.0" "libunfy API"
.SH Name
unfy \- unification algorithm library using rids.
.SH SYNOPSIS
.B #include <rid.h>
.br
.B #include <stdint.h>
.sp
.B #include <nit/list.h>
.br
.B #include <nit/set.h>
.br
.B #include <nit/map.h>
.sp
.B #include <unfy.h>
.sp
Link with \fI\-lrid\fP, \fI\-lnit\fP and \fI\-lbsd\fP.
.SH DESCRIPTION
A library to create terms and unify them if possible.
.SS Types
.B Unfy_type
denotes a type for a
.B Unfy_term
it is defined as:
.sp
.nf
typedef enum {
	UNFY_CONST = 0,
	UNFY_LIST,
	UNFY_VAR,
} Unfy_type;
.fi
.sp
.B Unfy_stat
denotes the result of unification in terms of success of not, it is defined as:
.sp
.nf
typedef enum {
	UNFY_YES,
	UNFY_NO,
	UNFY_ERR,
} Unfy_stat;
.fi
.sp
.B Unfy_term
is a term that can be unified. It is defined as:
.sp
.nf
typedef struct {
	Unfy_type type;

	union {
		Rid id;
		Unfy_list *list;
		void *dat;
	} u;
} Unfy_term;
.fi
.sp
.B Unfy_list
is a list of terms. It is defined as:
.sp
.nf
struct Unfy_list {
	Nit_list next;
	Unfy_term *term;
};
.fi
.sp
.B Unfy_recycle
stores information for recycling terms and lists. You should not depend on how it is implemented.
.SS Functions
.BI "void unfy_recycle_init(Unfy_recycle *" rec ");"
.br
.BI "void unfy_recycle_empty(Unfy_recycle *" rec ");"
.br
.BI "void unfy_recycle_term(Unfy_recycle *" rec ", Unfy_term *" term ");"
.br
.BI "void unfy_recycle_list(Unfy_recycle *" rec ", Unfy_list *" list ");"
.sp
.BI "Unfy_term * unfy_term(Unfy_type " type ", void *" dat ", Unfy_recycle *" rec ");"
.br
.BI "Unfy_term * unfy_term_copy(const Unfy_term *" term ", Unfy_recycle *" rec ");"
.br
.BI "void unfy_term_init(Unfy_term *" term ", Unfy_type " type ", void *" dat ");"
.br
.BI "int unfy_term_init_copy(Unfy_term *" des ", const Unfy_term *" src ", Unfy_recycle *" rec ");"
.br
.BI "Unfy_stat unfy_term_same(const Unfy_term *" des ", const Unfy_term *" src ", Nit_map *" binds ",  Nit_entry **" entries ", Unfy_recycle *" rec ");"
.sp
.BI "Unfy_list * unfy_list(Unfy_term *" term ", Unfy_list *" next ", Unfy_recycle *" rec ");"
.br
.BI "Unfy_list * unfy_list_copy(const Unfy_list *" list ", Unfy_recycle *" rec ");"
.br
.BI "void unfy_list_init(Unfy_list *" list ", Unfy_term *" term ", Unfy_list *" next ");"
.br
.BI "int unfy_list_init_copy(Unfy_list *" copy ", const Unfy_list *" list ", Unfy_recycle *" rec ");"
.br
.BI "Unfy_stat unfy_list_same(const Unfy_list *" des ", const Unfy_list *" src ", Nit_map *" binds ", Nit_entry **" entries ", Unfy_recycle *" rec ");"
.br
.BI "Unfy_list ** unfy_list_append(Unfy_list **" tail ", Unfy_term *" term ", Unfy_recycle *" rec ");"
.sp
.BI "Unfy_term * unfy_term_bind(const Unfy_term *" term ", const Nit_map *" binds ", Unfy_recycle *" rc ");"
.br
.BI "int unfy_term_bind_set(Unfy_term *" term ", const Nit_map *" binds ", Unfy_recycle *" rec ");"
.br
.BI "void unfy_binds_free(void *" key ", void *" val ", void *" rec ");"
.sp
.BI "Unfy_stat unfy_unify(const Unfy_term *" left ", const Unfy_term *" right ", Nit_map *" lbinds ", Nit_map *" rbinds ", Nit_entry **" entries ", Unfy_recycle *" rec ");"
.SS Function Explanations
.B unfy_recycle_init ()
initializes
.I rec
to be used in other functions.
.sp
.B unfy_recycle_empty ()
frees all memory (recycled terms and lists) that are held by
.IR "rec" .
.sp
.B unfy_recycle_term ()
recycles memory used by
.I term
and stores it in
.IR "rec" .
.sp
.B unfy_recycle_list ()
recycles memory used by
.I list
and stores it in
.IR "rec" .
.sp
.B unfy_term ()
return a term where
.I type
denotes the type of the term and
.I dat
sets what value the term should have, in the case of
.I type
being
.B UNFY_CONST
or
.B UNFY_VAR
this should be an Rid, but if the type is
.B UNFY_LIST
this should be a Unfy_list.
.sp
.B unfy_term_copy ()
returns a copy of
.IR term "."
.sp
.B unfy_term_init ()
and
.B unfy_term_init_copy ()
work similar to the functions with the same name minus "init", except instead of returning a term they initialize the first argument passed to them.
.sp
.B unfy_term_same ()
determines if the two input terms have the same structure (if everything is between them is the same except specific variable names).
.I binds
is set so that variables in
.I des
can be changed to have the same names as variables in
.I src
allowing for
.I des
to effectively become the same as
.IR src ","
if it is possible. The return value is UNFY_YES if the two terms are the same in structure, UNFY_NO if they are not, and UNFY_ERR if an error occurred.
.I entries
refers to recycled values of type Nit_entry, a reference to a NULL pointer of that type can be used here and freed later using the nit function
.B nit_entry_stack_free ()
.sp
.B unfy_list ()
returns a list initialized using the arguments passed to the function.
.sp
.B unfy_list_copy ()
returns a copy of
.IR list "."
.sp
.B unfy_list_init ()
and
.B unfy_list_init_copy ()
work similar to the functions with the same name minus "init", except instead of returning a list they initialize the first argument passed to them.
.sp
.B unfy_list_same ()
is similar to
.B unfy_term_same ()
except it is on lists instead of terms.
.sp
.B unfy_list_append ()
takes
.IR tail ","
a reference to the next value of the last element of a Unfy_list (which should be NULL), and a term
.RI "(" term ")."
It then uses
.I tail
to append to the end of the list a Unfy_list using
.I term
as the term. It then returns a reference to the next value of the new last element of the list (which can be used to append another element to the end of the list which makes this function useful in loops).
.sp
.B unfy_term_bind ()
returns a copy of
.I term
replaces its variables using their corresponding bindings from
.IR binds "."
.sp
.B unfy_term_bind_set ()
works like
.B unfy_term_bind ()
except instead of making a copy, it changes
.I term
directly.
.sp
.B unfy_binds_free ()
should not be used directly, but instead passed to a function for freeing binds and used for the argument of type Nit_map_free. The argument
.I extra
should be a of type Unfy_recycle.
.sp
.B unfy_unify ()
tries to unify the terms
.I left
and
.I right
where bound variables for
.I left
are stored in
.I lbinds
and bound variables for
.I right
are stored in
.IR rbinds "."
The return value is UNFY_YES if the two terms can be unified, UNFY_NO if they cannot and UNFY_ERR if an error occurred.
.SH "Return Values"
All functions returning a value can fail, if they do it is due to running out of memory. On failure if the return value is a pointer (of any type) it will be NULL, if the value is an int it will be less than 0, and if they type is Unfy_stat it will be UNFY_ERR.
.SH EXAMPLES
See the
.I examples
folder in the repository of unfy for an example repl that takes two terms and tries to unify them.
.SH AUTHOR
Uladox (coming up with terms)
.SH "AVAILABILITY AND SOURCE"
.B unfy
can be found in its repository at https://www.notabug.org/Uladox/unfy
.SH "SEE ALSO"
.BR rid (3)