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.