specification.md

+# Specificiation 
+
+## Atoms
+
+There are two types of atoms in the NDL language:
+* integers, i.e. `0`
+* variables with Prolog syntax, i.e. `X`, `Variable`, `_OtherVariable`
+* variable indexes, that are terms with arity depending on the variable dimensionality, i.e. for a 2-dimension array of variable named `queen`, the variable's index takes form `queen(<integer>, <integer>)`, i.e. `queen(1,1)`.
+
+Additionaly string constants (lower case, as `name`) and the integer ranges (written as `0..10`) are used as a syntax sugar in model definitions, but aren't used in the NDL query itself.
+
+## Types
+
+Every atom has an associated type, storing additional information about the atom:
+
+* in case of the variable, type defines domain of the variable; language doesn't allow to change the variable's type, therefore all arithmetic operations are implemented in a way to satisfy the domain closure
+
+Types are defined in the NDL model as `constants` and are problem dependent.
+
+## Model
+
+NDL model is a typed Prolog program consisting of following predicates:
+
+* Constant related:
+  * `constant_definition(+Name:string, -Constant:integer)` - contains the constant definition. Constant should be understood as a type with only one possible value. The predicate should be used only using the compilation and shouldn't be used in the NDL queries.
+  * `constant_usages(+Name:string, -Context:list)` - another compile-only information. `Context` cotains information about all possible contexts, where the constant may be used, i.e. it allows to emulate the typed arguments in other predicates. Possible contexts include:
+    * domain of a variable
+    * indexing of a variable in a specific axis/dimension
+    * to be part of an arithmetic expression with a variable's value **FIXME**
+    * to be part of an arithmetic expression with a variable's index in a specific axis/dimension **FIXME**
+  * `constant(+Name:string, -Value:integer)` - allows to get constant value by it's name. Used in the NDL query.
+  * `constant_range_definition(+Name:string, -Range:range)` - analogically to the integer constant, this defines a type with a range of possible values.
+  * `constant_range_usages(+Name, -Context:list) - again, used to simulate typing in the Prolog program.
+  * `constant_range(+Name:string, -Value:integer) is nondet` - allows to non-deterministically get one of the type inhibitants. Used in the NDL query.
+* Variable related:
+  * `fixed(+Name:string)` - variables with this name shouldn't be modified by the NDL query. Used only during compilation.
+  * `variable(+Name:string, -Index:variable_index) is nondet` - allows to non-deterministically get an index of the variable named `Name`. Used in the NDL query.
+  * `new_value(+Name:string, -Value:Integer) is nondet` - allows to non-deterministically get an possible value for the variable named `Name`. Used in the NDL query.
+* Constraint related:
+  * `constraint(+Name:string, ?Index1:variable_index, ?Index2:variable_index) is nondet` - allows to non-deterministically check if two variables indexed `Index1` and `Index2` are constrained with a constraint named `Name`. Also allows to find indexes satisfying those requirements. Used in the NDL query.
+  * `is_satisfied(+Name:String, +Index1:variable_index, +Index2:variable_index)` - allows to check if the constraint named `Name` is satisfied on variables indexed `Index1` and `Index2`. Used in the NDL query. **FIXME**
+dynamic_predicate(constraint/3, public). 
\ No newline at end of file