Module GDL

module GDL: sig .. end

Game Description Language.

Type definitions, helper functions.

val playout_fixpoint : bool Pervasives.ref
val set_timeout : (unit -> bool) -> unit

Datalog programs: Type definitions and saturation.

type term = 
| Const of string
| Var of string
| Func of string * term array
type rel_atom = string * term array 
type atom = 
| Distinct of term array
| Rel of rel_atom
| Role of term
| True of term
| Does of term * term
type literal = 
| Pos of atom
| Neg of atom
| Disj of literal list
type gdl_rule = rel_atom * rel_atom list * rel_atom list 
Positive and negative literals separated, disjunctions expanded-out.

Collect rules by relations.

type def_branch = term array * rel_atom list * rel_atom list 
type gdl_defs = (string * def_branch list) list 
type clause = rel_atom * literal list 
type path = (string * int) list 
type path_set 
type request = 
| Start of string * term * clause list * int * int (*prepare game: match id, role, game, startclock, playclock*)
| Play of string * term list (*request a move: match id, actions on previous step*)
| Stop of string * term list (*game ends here: match id, actions on previous step*)
module Terms: Set.S  with type elt = term
val add_terms : term list -> Terms.t -> Terms.t
val terms_of_list : term list -> Terms.t
val atoms_of_body : literal list -> atom list
val rel_of_atom : atom -> rel_atom
val term_vars : term -> Aux.Strings.t
val terms_vars : term array -> Aux.Strings.t
val clause_vars : clause -> Aux.Strings.t
val clauses_vars : clause list -> Aux.Strings.t
val literals_vars : literal list -> Aux.Strings.t
val defs_of_rules : gdl_rule list -> gdl_defs
val rules_of_clause : clause -> gdl_rule list
val nnf_dnf : literal list -> literal list list
type substitution = (string * term) list 
val unify : substitution -> term list -> term list -> substitution
val unify_args : ?sb:substitution -> term array -> term array -> substitution
Match terms on the left to ground terms on the right, ignoring Const "_BLANK_" on the right.
val match_nonblank : substitution -> term list -> term list -> substitution
Check for equality modulo ground terms on the right.
val mask_blank : term list -> term list -> bool
val unify_all : substitution -> term list -> substitution
val unify_rels : ?sb:substitution -> rel_atom -> rel_atom -> substitution
val rels_unify : rel_atom -> rel_atom -> bool
val subst : substitution -> term -> term
val subst_consts : substitution -> term -> term
val subst_rel : substitution -> rel_atom -> rel_atom
val subst_rels : substitution -> rel_atom list -> rel_atom list
val subst_literal : substitution -> literal -> literal
val subst_literals : substitution -> literal list -> literal list
val subst_clause : substitution -> clause -> clause
val subst_consts_literals : substitution -> literal list -> literal list
val subst_consts_clause : substitution -> clause -> clause
module Tuples: Set.S  with type elt = term array
type graph = Tuples.t Aux.StrMap.t 
val graph_mem : string -> term array -> graph -> bool
val merge_graphs : graph -> graph -> graph
val build_graph : rel_atom list -> graph
val graph_to_atoms : graph -> rel_atom list
val gdl_rel_graph : string -> graph -> term array list
Saturation currently exposed for testing purposes.
val saturate : graph -> gdl_rule list -> graph

Continuation-based Prolog interpreter

val run_prolog_aggregate : bool Pervasives.ref
The interpreter can reinterpret "does" atoms as "legal" atoms for aggregate playout. For random playout, remember to compute legal moves, select randomly one for each player and add "does" atoms to the program.
val reorder_clauses : bool Pervasives.ref
type prolog_program 
val preprocess_program : clause list -> prolog_program
val restore_program : ?t_cls:clause list ->
?d_cls:clause list -> prolog_program -> prolog_program
val run_prolog_atom : rel_atom -> prolog_program -> rel_atom list
Compute all implied instantiations of the given atom, return sorted unique instances.

Compute all variable substitutions that satisfy the given conjunction of literals. The substitutions are not unique (there is as many of them as there are different proofs of the goal).

val run_prolog_goal : literal list -> prolog_program -> substitution list
Just check if the atom / conjunction of literals is satisfiable. Should be faster than checking non-emptiness of run_prolog_goal result.
val run_prolog_check_atom : rel_atom -> prolog_program -> bool
val run_prolog_check_goal : literal list -> prolog_program -> bool
val optimize_goal : testground:prolog_program ->
?head_sb:substitution -> literal list -> literal list
val optimize_program : testground:prolog_program -> prolog_program -> prolog_program

Transformations of GDL clauses: inlining, negation.

val expand_definitions : gdl_defs -> def_branch list -> def_branch list
Expand branches of a definition inlining the provided definitions. Iterate expansion to support nesting of definitions.
val atom_of_rel : rel_atom -> atom
Remember that rel_of_atom inverts polarity of "distinct" -- invert back after using atom_of_rel if needed.
val negate_bodies : literal list list -> (substitution * literal list) list
Form clause bodies whose disjunction is equivalent to the negation of disjunction of given clause bodies. Keep the substitution so that the heads of corresponding clauses can be substituted too.
val rename_clauses : clause list -> Aux.Strings.t Pervasives.ref * clause list
Rename clauses so that they have disjoint variables. Return a cell storing all variables.
val func_graph : string -> term list -> term array list
val elim_pattern_args : string list -> clause list -> string list * clause list
Eliminate arguments of relations that are defined by non-wildcard pattern matching (i.e. do not have a variable in any of the defining clauses). Return the new clauses, and also the new relation set.
val elim_ground_distinct : clause list -> clause list
val state_cls : term list -> clause list

GDL translation helpers.

val blank : term
val counter_n : string
val term_str : term -> string
val terms_str : term array -> string
val term_to_name : ?nested:bool -> term -> string
val state_terms : literal list -> term list
val pos_state_terms : literal list -> term list
val term_arities : term -> (string * int) list
val atom_str : atom -> string
val rel_atom_str : rel_atom -> string
val rel_atoms_str : rel_atom list -> string
val gdl_rule_str : gdl_rule -> string
val gdl_rules_str : gdl_rule list -> string
val def_str : string * def_branch list -> string
val literal_str : literal -> string
val literals_str : literal list -> string
val clause_str : clause -> string
val clauses_str : clause list -> string
val sb_str : (string * term) list -> string
val program_clauses : prolog_program -> clause list
val topsort_callgraph : clause list -> string list

GDL whole-game operations.

Aggregate and random playout, player-denoting variable elimination.

val static_rels : gdl_defs -> string list * string list
Partition relations into static (not depending, even indirectly, on "true") and remaining ones.
val playout_satur : aggregate:bool ->
term array ->
int ->
gdl_rule list ->
gdl_rule list * gdl_rule list * graph * term list *
(term array list list * term list list * term list)
Besides the aggregate or random playout, also return the separation of rules into static and dynamic. Note that the list of playout states is one longer than that of playout actions.

When aggregate_drop_negative is true, to keep monotonicity, besides removing negative literals from "legal" clauses, we also add old terms to the state. (Only when ~aggregate:true.)

~aggregate:true performs an aggregate ply, ~aggregate:false performs a random ply. Aggregate playouts are "deprecated", especially for uses other than generating all possible state terms.

val playout_prolog : aggregate:bool ->
term array ->
int ->
prolog_program ->
term array list list * term list list * term list
val find_cycle : term option list -> term option list
val expand_players : clause list -> clause list

Paths and operations involving terms and paths.

val simult_subst : path_set -> term -> term -> term
simult_subst ps s t substitutes s at all t paths that belong to the set ps, returns $tps \ot s$.
val map_paths : (path -> term -> 'a) -> path_set -> term -> 'a list
Find the list of results of a function applied to paths from the given set that are in the term, and to subterms at these paths.
val rel_on_paths : string -> path list -> string
Toss relations hold between subterms of GDL state terms: generate Toss relation name.
val pred_on_path_subterm : path -> term -> string
Some Toss predicates are generated from a path and an expected subterm at that path.
val term_paths : ?prefix_only:bool -> (term -> bool) -> term -> path_set
All paths in a term pointing to subterms that satisfy a predicate. With ~prefix_only:true, paths that contain a path that has been included, are not included.
val at_path : term -> path -> term
Find the subterm at given path, if the term does not have the path, raise Not_found; at_path p t is $t \tpos p$.
val merge_terms : term -> term -> path_set * int * int
The set of paths that merges two terms, the cardinality of this set, and the size of the largest common subtree.
val at_paths : ?fail_at_missing:bool -> path_set -> term -> term list
Find the list of subterms at paths from the given set, if the term does not have some of the paths, ignore them if ~fail_at_missing:false, raise Not_found if ~fail_at_missing:true.
val empty_path_set : path_set
val eps_path_set : path_set
Add path to a set. First argument gives term arities.
val add_path : (string -> int) -> path -> path_set -> path_set
val paths_union : path_set -> path_set -> path_set
val paths_intersect : path_set -> path_set -> path_set
val paths_to_list : path_set -> path list
List the paths in a set.
val path_str : path -> string
val ground_vars_at_paths : (clause -> literal list) ->
(path * term list) list -> clause list -> clause list
ground_vars_at_paths prepare_lits ps_sterms clauses expands subterms that have occurrences at paths in ps_sterms in some state term of a clause (from which pre-processed literals are extracted by prepare_lits), by substituting their variables with corresponding subterms of terms provided in ps_sterms.
val blank_outside_subterm : (string * int) list -> path -> term -> term
val blank_outside_subterms : (string * int) list -> (path * term) list -> term
val refine_leaf_paths : path_set -> term list -> path_set
If some path points only to bigger than one (i.e. non-leaf) subterms in the given set of terms, then expand/split it to longer paths that together cover all leafs the original path covered.
val refine_paths_avoiding : path_set ->
(term -> bool) -> (term -> bool) -> term list -> path_set
refine_paths_avoiding paths avoid_later avoid_now terms splits paths in the set until, if possible, none of subterms at the paths meets the predicate avoid_later; it does not descend subterms for which avoid_now holds. Also removes paths not present in terms.
type argpaths = (path * int) list list 
The integers should be all-distinct and from 0 to N-1.
val find_rel_arg : term list -> term array -> (path * int) list -> term
val complete_paths_for : path_set -> argpaths -> bool
Check whether each of argpaths covers some tree in c_paths completely.