[Toss-devel-svn] SF.net SVN: toss:[1287] trunk/Toss

[<luk...@us...>]

Revision: 1287
          http://toss.svn.sourceforge.net/toss/?rev=1287&view=rev
Author:   lukaszkaiser
Date:     2011-01-29 16:49:51 +0000 (Sat, 29 Jan 2011)

Log Message:
-----------
Rearangement for ggp testing, added automated test with java gamecontroller.

Modified Paths:
--------------
    trunk/Toss/.cvsignore
    trunk/Toss/Makefile
    trunk/Toss/Play/GameTest.ml
    trunk/Toss/Toss.py
    trunk/Toss/TossTest.ml

Added Paths:
-----------
    trunk/Toss/GGP/
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/GDLParser.mly
    trunk/Toss/GGP/GDLTest.ml
    trunk/Toss/GGP/KIFLexer.mll
    trunk/Toss/GGP/Makefile
    trunk/Toss/GGP/examples/
    trunk/Toss/GGP/examples/breakthrough.gdl
    trunk/Toss/GGP/examples/checkers.gdl
    trunk/Toss/GGP/examples/chess.gdl
    trunk/Toss/GGP/examples/connect5.gdl
    trunk/Toss/GGP/examples/tictactoe.gdl
    trunk/Toss/GGP/gamecontroller-cli.jar
    trunk/Toss/Server/
    trunk/Toss/Server/Makefile
    trunk/Toss/Server/Server.ml
    trunk/Toss/Server/ServerGDLTest.in
    trunk/Toss/Server/ServerGDLTest.out
    trunk/Toss/Server/ServerTest.in
    trunk/Toss/Server/ServerTest.ml
    trunk/Toss/Server/ServerTest.out

Removed Paths:
-------------
    trunk/Toss/Play/GDL.ml
    trunk/Toss/Play/GDL.mli
    trunk/Toss/Play/GDLParser.mly
    trunk/Toss/Play/GDLTest.ml
    trunk/Toss/Play/KIFLexer.mll
    trunk/Toss/Play/Server.ml
    trunk/Toss/Play/ServerGDLTest.in
    trunk/Toss/Play/ServerGDLTest.out
    trunk/Toss/Play/ServerTest.in
    trunk/Toss/Play/ServerTest.out
    trunk/Toss/examples/breakthrough.gdl
    trunk/Toss/examples/checkers.gdl
    trunk/Toss/examples/chess.gdl
    trunk/Toss/examples/connect5.gdl

Property Changed:
----------------
    trunk/Toss/


Property changes on: trunk/Toss
___________________________________________________________________
Modified: svn:ignore
   - # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

Toss.docdir
_build
Server
*.native
*Profile.log
gmon.out
*~
*.annot
*.cmx
*.cmi
*.o
*.cmo
*.a
*.cmxa
log.*

   + # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

Toss.docdir
_build
TossServer
*.native
*Profile.log
gmon.out
*~
*.annot
*.cmx
*.cmi
*.o
*.cmo
*.a
*.cmxa
log.*


Modified: trunk/Toss/.cvsignore
===================================================================
--- trunk/Toss/.cvsignore	2011-01-29 13:11:29 UTC (rev 1286)
+++ trunk/Toss/.cvsignore	2011-01-29 16:49:51 UTC (rev 1287)
@@ -4,7 +4,7 @@
 
 Toss.docdir
 _build
-Server
+TossServer
 *.native
 *Profile.log
 gmon.out

Copied: trunk/Toss/GGP/GDL.ml (from rev 1286, trunk/Toss/Play/GDL.ml)
===================================================================
--- trunk/Toss/GGP/GDL.ml	                        (rev 0)
+++ trunk/Toss/GGP/GDL.ml	2011-01-29 16:49:51 UTC (rev 1287)
@@ -0,0 +1,2123 @@
+(** {2 Game Description Language.}
+
+    Type definitions, helper functions, game specification
+    translation.
+
+    The translation is not complete (yet), and not yet guaranteed to
+    be sound (but aiming at it) -- report any cases where the
+    algorithm does not fail explicitly but does not preserve
+    semantics.
+
+    (1) Aggregate playout: generate successive states as if all moves
+    legal in the previous state were performed. Do not check the
+    termination predicate.
+
+    (1a) Reason for unsoundness: "legal" or "next" preconditions can
+    depend negatively on state, preventing further moves in the
+    aggregate state that would be possible in some of valid game
+    states; the aggregate state does not have enough terms as a
+    result. Workaround: remove negative literals from "legal"/"next"
+    conditions for generating aggregate playout.
+
+    (1b) Saturation works on definitions stratified
+    w.r.t. negation. Positive literals are instantiated one by one,
+    then negative literals are checked over the facts derived from
+    previous strata. To avoid redundancy, new facts and new
+    instantiations are kept separate for the next iteration within a
+    stratum.
+
+    (1c) Heuristic reason for unsoundness: while we check for fixpoint
+    in the playout, we rule out state terms "F(X)" where X is a player
+    (assuming that "F" means "control"). Workaround: turn off fixpoint
+    checking [aggregate_fixpoint].
+
+    (2) Arena graph: currently, only a simple cycle is allowed. The
+    succession of players is determined from the aggregate playout.
+
+    (2a) We need to recognize which player actually makes a move in a
+    state. For this we need to locate the "noop" arguments to "legal"
+    and "does" relations. A noop action in a location is the only
+    action in the corresponding state of an aggregate playout for the
+    player that is also constant.
+
+    (2b) We determine the player of a location by requiring that at
+    most one player has a non-noop action in an aggregate
+    state. When all players are noops we select the control player so
+    that the smallest "game cycle" is preserved. Otherwise (more than
+    one no-noop move) we fail (simultaneous moves not supported). We
+    remember the noop actions for each location and player.
+
+    (3) Currently, a constant number of elements is assumed. The rules
+    processed in (3a)-(3b) are already expanded by (6).
+
+    (3a) Element terms are collected from the aggregate playout: the
+    sum of state terms (the "control" function could be dropped but we
+    are not taking the effort to identify it).
+
+    (3b) Element masks are generated by generalization from all "next"
+    rules where the "does" relations are expanded by all unifying
+    "legal" rules (see also (7a)).
+
+    (3c) Generalization in a single expanded "next" rule is by finding
+    for the "next" term the closest "true" term in the lexicographic
+    ordering of (# of matched variables, # of other matched leaves),
+    but in case the closest term is found in the negative part, it is
+    further processed.
+
+    (3c1) Unmatched subterms are replaced by meta-variables.
+    
+    (3c2) When the generalization comes from the negative part, we
+    replace all constant leaves with meta-variables.  Warning: this
+    heuristic is a reason for unsoundness -- search for a workaround
+    once a real counterexample is encountered.
+
+    (3d) The masks are all the minimal w.r.t. matching (substitution)
+    of the generalized terms, with only meta-variable positions of the
+    mask matching meta-variable positions of a generalized
+    term.
+
+    (3e) The elements are the equivalence classes of element terms,
+    where terms are equivalent when they both match a single mask and
+    their matching substitutions differ only at
+    meta-variables. (I.e. for t1 and t2 there exists a mask m and
+    substitutions s1 and s2 such that s1(m)=t1 and s2(m)=t2 and
+    s1(x)=/=s2(x) implies that x is/contains a meta-variable.)
+
+    (Note that there is "nothing wrong" with a given equiv class not
+    having any member in the initial state or some other state. The
+    element is still there in the structure, still participating in
+    the "static" relations, but not in the "dynamic" predicates in
+    that particular state. We use a special _BLANK_ term/predicate to
+    faciliate operations on such "absent" elements.)
+    
+    (4) Static relations (their tuples do not change during the game)
+    are derived from static facts with subterms common with element
+    terms but not below meta-variables.
+
+    Define mask-paths as the set of a mask together with a path in it
+    to a position that is not below (or at) a meta-variable.
+
+    Implementation: currently we approximate paths by only taking the
+    positions of variables in the mask.
+
+    (4a) (Fact relations.) For a static fact (a relation that does not
+    depend on "true" or "init") (unless it is expanded -- see (6)),
+    introduce a relation for each mask-paths tuple with arity of the
+    relation (i.e., introduced relations are a dependent product of
+    static fact relations and a cartesian n-th power of the mask-paths
+    set where n is the arity of the relation). An introduced relation
+    holds over a tuple of elements, iff the corresponding element
+    terms match the respective masks, and the original relation holds
+    over the tuple of subterms selected from the element terms by the
+    corresponding paths.
+
+    (4b) (Equality relations.) For each mask-path, introduce a binary
+    relation that holds over elements which have the same subterm at
+    the mask-path position. (Because of mask-paths definition, same
+    for all element terms in element's equivalence class.)
+
+    (4c) (Anchor predicates.) Add a predicate for being derived from a
+    mask. For each mask-path pointing to a constant in some of the
+    elements and that constant, introduce a new predicate with
+    semantics: "matches the mask and has the constant at the path
+    position".
+
+    (5) (Mostly) dynamic relations ("fluents": their tuples change
+    during the game), relations derived from all below-meta-variable
+    subterms of element terms, initialized by those that appear in the
+    initial state. (Some relations introduced in this step might not
+    be fluents.)
+
+    (See also (7k).) For each element term, find the element mask it
+    matches, and introduce relations for each meta-variable of the
+    element mask, associated with the subterm that matches the
+    meta-variable. The semantic is that the relation selects the
+    element terms that match the mask with the associated subterm
+    subsituted for the corresponding meta-variable, with existential
+    interpretation. A relation holds initially over an element, if in
+    the initial set of element terms at least one from the element's
+    equivalence class is selected by the relation. An occurrence of
+    "true" or "next" relation is replaced by a conjunction of
+    relations whose substituted-masks match the relation's term.
+
+    When generating predicates that hold over an element term, no
+    predicate is generated for any its meta-variable position that
+    contains _BLANK_.
+
+    (6) Currently how to introduce defined relations in translation is
+    not yet solved in the presented framework. Currently, we simply
+    expand relations that are not static, or (optionally) are static
+    but do not contain ground facts, by duplicating the branch in
+    which body an atom of the relation occurs, for each branch of the
+    relation definition, unifying and applying the unifier. (If the
+    duplication turns out prohibitive, this will be a *huge* TODO for
+    this translation framework.)
+
+    (6a) The definition:
+
+    [(r, params1) <= body1 ... (r, params_n) <= body_n]
+
+    provides a DNF defining formula (using negation-as-failure):
+
+    [(r, args) <=> exist vars1 (args = params1 /\ body1) \/ ...
+    \/ exist vars_n (args = params_n /\ body_n)]
+
+    which expands in a natural way for positive occurrences. We
+    duplicate the branch where [(r, args)] is substitued for each
+    disjunct and apply the unifier of [args = params_i] in the whole
+    [i]th cloned branch. We freshen each [vars_i] to avoid capture. If
+    unification fails, we drop the corresponding branch clone.
+
+    (6b) For negative occurrences we transform the defining formula
+    to:
+
+    [not (r, args) <=> not exist vars1 (args = params1 /\ body1) /\ ...
+    /\ not exist vars_n (args = params_n /\ body_n)]
+
+    Currently we do not allow defined dynamic relations with negative
+    occurrences to have negative literals (or atoms of defined
+    relations with negative part) in any of [body_i]. (The limitation
+    can be lifted but it would further complicate the implementation.)
+    We therefore allow conjunctions of atoms to be negated (not only
+    literals) in a branch. We expand [not (r, args)] (in general, [not
+    (and (...(r args)...))]) into the conjunction of negations, with
+    no branch duplication (in general, duplicating the negated
+    subformula inside a branch). We only apply the unifier of [args =
+    params_i] to [body_i] (in general, the whole negated
+    subformula). Still, we freshen each [vars_i] to avoid capture. If
+    unification fails, we drop the corresponding negated
+    subformula. If unification succeeds but the corresponding [body_i]
+    is empty (and, in general, no other disjuncts in the negated
+    subformula are left), we drop the branch.
+
+    (6b1) The general case is not implemented yet since it slightly
+    complicates the code, and expressivity gain is very small.
+
+    (7) Generation of rewrite rules when the dynamic relations are not
+    recursive and are expanded in the GDL definition.
+
+    (7a) We translate each branch of the "legal" relation definition
+    as one or more rewrite rules. Currently, we base availability of
+    rules in a location on the player in the location and noop actions
+    of other players in it, compared to the the "legal" definition
+    branch (currently, we do not allow simultaneous moves). If the
+    branch of "legal" definition has a variable for a player, it is
+    instantiated for each player in the game, and the variable
+    substituted in the body of the "legal" branch. A rewrite rule is
+    associated with a single "lead legal" branch of the location's
+    player.
+
+    (7b) We collect all the branches of the "next" relation definition
+    for which the selected branches of "lead legal" and "noop legal"
+    (the "joint legal" actions) unify with all (usually one, but we
+    allow zero or more) occurrences of "does" with a single unifier
+    per "next" branch. (A "noop legal" actually only matches and
+    substitutes the local variables of "next" branches.) Split the
+    unifiers into equivalence classes (w.r.t. substitution), each
+    class will be a different rewrite rule (or set of rules). (Note
+    that equivalent unifiers turn out to be those that when truncated
+    to variables of the "legal" branch are renamings of each other.)
+
+    (7b1) Since the "noop legals" are constants (by current
+    assumption), we do not need to construct equivalence classes for
+    them. Their branches will join every rule generated for the "joint
+    legal" choice.
+
+    (7c) Find a single MGU that unifies the "legal" atom argument and
+    all the "does" atoms arguments into a single instance, and apply
+    it to all "next" branches of the rule (i.e. after applying the
+    original unifier, apply a renaming that makes the unifier equal to
+    all other unifiers in the equiv. class). We replace all
+    occurrences of "does" with the body of the selected "legal"
+    branch.
+
+    (7d) Add all branches of equiv classes smaller than a given equiv
+    class to its branch set.
+
+    Implementation TODO (reason for unsoundness): currently, we
+    discard non-maximal equivalence classes, because negation (7e) is
+    not implemented, and with negation it would still be preferable to
+    have exhaustiveness check so as to not generate spurious
+    (unapplicable) rules.
+
+    (7e) Associate negation of equalities specific to the unifiers
+    strictly less general than the equivalence class with it, so that
+    the resulting conditions form a partition of the space of
+    substitutions for the "legal" branch processed.
+
+    (7f) We remember all variables in the "legal"/"does" instantiation
+    as "fixed variables". We seggregate "next" atoms into these that
+    contain some fixed variables or no variables at all, and other
+    containing only unfixed variables.
+
+    (7f1) Branches with (only) unfixed variables in "next" atoms that
+    are "identities" are the "frame" branches. "Identity" here means
+    the "next" atom is equal to one of the positive "true" atoms.
+
+    (7f2) Transform the "frame" branches into "erasure" branches:
+    distribute them into equivalence classes of head terms
+    (w.r.t. substitution but treating fixed variables as constants),
+    add smaller elements and negation of larger elements (in the same
+    manner as in (7b) and (7d) for the "legal" term), disjoin bodies
+    in each class (a "multi-body"), then:
+
+    implementation TODO: currently, we only use maximal equivalence
+    classes (see note at 7d)
+
+    (7f3) negate the multi-body, push negation inside (using de Morgan
+    laws etc.), split into separate "erasure" branch for each
+    disjunct, place the original "next" atom but with meta-variable
+    positions replaced by _BLANK_ as the head of the "erasure" branch,
+    apply (and remove) unification atoms resulting from negating the
+    "distinct" relation.
+
+    (7f4) Drop the erasure branches that contradict the "legal"
+    condition of their rule.
+
+    (7f5) Redistribute the erasure branches in case they were
+    substituted with the "not distinct" unifier to proper equivalence
+    classes (remove equivalence classes that become empty).
+
+    (7g) Instantiate remaining unfixed variables. Implementation TODO.
+
+    (7h) Introduce a new element variable for each class of "next" and
+    "true" terms equal modulo mask (i.e. there is a mask matching them
+    and they differ only at-or-below metavariables). (Remember the
+    atoms "corresponding variable".) From now on until (7m1) we keep
+    both the (partially) Toss-translated versions and the (complete)
+    GDL-originals of branches (so to use GDL atoms for "subsumption
+    checking" in (7m)).
+
+    (7i-4a) For all subterms of "next" and "true" atoms, identify the
+    sets of <mask-path, element variable> they "inhabit". Replace a
+    static fact relation by relations built over a cartesian product
+    of <mask-path, element variable> sets derived for each static
+    fact's argument by applying corresponding (4a) relations. For a
+    negative literal generate result equivalent to a conjunction of
+    negations of generated atoms (FIXME: why disjunction is wrong?).
+
+    (7i-4c) Include the (4c) relations for "next" and "true" positive
+    atoms. Negative atoms are added with (5) relations since they are
+    under a common negation.
+
+    (7i-4b) Add an appropriate equality relation of (4b) for each case
+    of variable shared by terms corresponding to different element
+    variables (regardless if the element terms are in positive or
+    negative literals). FIXME: any shared subterm, not limited to
+    variables, right?
+
+    Implementation: instead of all subterms we currently only consider
+    subterms that instantiate (ordinary) variables in the mask
+    corresponding to the "next"/"true" atom.
+
+    (7i1) Remove branches that are unsatisfiable by their static
+    relations (4a), (4b) and (4c) alone.
+
+    (7j) Identify variables in "next" & "true" terms that are
+    at-or-below meta-variables in the corresponding mask. (Most of
+    such variables should be already removed as belonging to "frame"
+    branches.) Expand them by duplicating given branch for all
+    instantiations (all (5) predicates derived from the considered
+    position). (Note that since branches do not have unfixed variables
+    anymore, we do not rename variables during duplication.)
+
+    (7k) Replace the "next" and "true" atoms by the conjunction of
+    (4c) and (5) predicates over their corresponding variable. (For
+    negative "true" literals this will be equivalent to a disjunction
+    of negations of the predicates.) Note that positive static
+    relations are already added in (7i-4c).
+
+    (7l) Build a pre-lattice of branch bodies w.r.t. subsumption,
+    in a manner similar to (7b). The subsumption test has to say "no"
+    when there exists a game state where the antecedent holds but the
+    consequent does not, but does not need to always say "yes"
+    otherwise. Build a rewrite rule for each equivalence class
+    w.r.t. subsumption, including also branches that are below the
+    equiv class, and including negation of conditions that make the
+    branches strictly above more specific -- so that the classes form
+    a partition of the nonterminal game states (it is semantically
+    necessary so that all applicable changes are applied in the
+    translated game when making a move).
+
+    (7l1) Since all variables are fixed, the lattice is built by
+    summing rule bodies. To avoid contradictions and have a complete
+    partition, we construct the set of all bit vectors indexed by all
+    atoms occurring in the bodies. With every index-bit value we
+    associate the set of branches that do not allow such literal. For
+    every vector we calculate the complement of the sum of branch sets
+    associated with every bit. The unique resulting sets are exactly
+    the Toss rules precursors.
+
+    (7m) Include translated negation of the terminal condition. (Now we
+    build rewrite rules for a refinement of an equivalence class of
+    (7b): from the branches with unifiers in the equiv class, from
+    branches with unifiers more general than the equiv class, and from
+    the disjointness conditions and the terminal condition.)
+
+    The rewrite rule is generated by joining the derived conjunctions
+    from "next" atoms as RHS, and from bodies as the
+    precondition. Exactly the RHS variables are listed in the LHS
+    (other variables are existentially closed in the precondition).
+
+    (8) We use a single payoff matrix for all locations. Goal patterns
+    are expanded to regular goals by instantiating the value variable
+    by all values in its domain (for example, as gathered from the
+    aggregate playout), and expanding all atoms that contained value
+    variables (both static and dynamic) using (6); fail if a goal
+    value cannot be determined. The payoff formula is the sum of
+    "goal" value times the characterisic function of the "goal"
+    body. We do not translate the body if the value is zero (we drop
+    the zero goal branches from the definition). Translate the body
+    using (7h)-(7m), but treating "goal" branches separately -- when
+    (7k) duplicates a branch, new branches add new sum elements.
+
+*)
+
+let debug_level = ref 0
+let aggregate_drop_negative = ref false
+let aggregate_fixpoint = ref true
+(** Expand static relations that do not have ground facts and have
+    arity above the threshold. *)
+let expand_arity_above = ref 0
+
+type term =
+  | Const of string
+  | Var of string
+  | MVar of string                      (* meta-variable, not used in GDL *)
+  | Func of string * term list
+
+type atom =
+  | Distinct of term list
+  | Rel of string * term list
+  | Currently of term
+  | Does of term * term
+
+type literal =
+  | Pos of atom
+  | Neg of atom
+  | Disj of literal list
+
+type game_descr_entry =
+  | Datalog of string * term list * literal list
+  | Next of term * literal list
+  | Legal of term * term * literal list
+  | Goal of term * int * literal list
+  | GoalPattern of term * string * literal list
+  | Terminal of literal list
+  | Role of term
+  | Initial of term * literal list
+  | Atomic of string * term list
+
+type request =
+  | Start of string * term * game_descr_entry 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 *)
+
+let rec term_str = function
+  | Const c -> c
+  | Var v -> "?"^v
+  | MVar v -> "@"^v
+  | Func (f, args) ->
+    "(" ^ f ^ " " ^ String.concat " " (List.map term_str args) ^ ")"
+
+let rec term_to_name ?(nested=false) = function
+  | Const c -> c
+  | Var v -> v
+  | MVar v -> v
+  | Func (f, args) ->
+    f ^ "_" ^ (if nested then "_S_" else "") ^
+      String.concat "_" (List.map (term_to_name ~nested:true) args) ^
+      (if nested then "_Z_" else "")
+
+let rec vars ?(meta=false) = function
+  | Const _ -> []
+  | Var x -> [x]
+  | MVar x -> if meta then [x] else []
+  | Func (_, args) -> Aux.concat_map vars args
+
+let rec term_vars = function
+  | Const _ -> Aux.Strings.empty
+  | Var v | MVar v -> Aux.Strings.singleton v
+  | Func (f, args) -> terms_vars args
+and terms_vars args =
+  List.fold_left Aux.Strings.union Aux.Strings.empty
+    (List.map term_vars args)
+
+let fact_of_atom = function
+  | Distinct args -> assert false
+  | Rel (rel, args) -> rel, args
+  | Currently arg -> "true", [arg]
+  | Does (arg1, arg2) -> "does", [arg1; arg2]
+
+let rec body_of_literal = function
+  | Pos (Distinct args) ->
+    [Aux.Right ("distinct", args)]        (* not negated actually! *)
+  | Neg (Distinct _) -> assert false
+  | Pos atom -> [Aux.Left (fact_of_atom atom)]
+  | Neg atom -> [Aux.Right (fact_of_atom atom)]
+  | Disj disjs ->
+    Aux.concat_map body_of_literal disjs
+
+let func_graph f terms =
+  Aux.map_some
+    (function Func (g, args) when f=g -> Some args | _ -> None) terms
+
+(* Type shortcuts (mostly for documentation). *)
+type gdl_atom = string * term list
+type gdl_rule = gdl_atom * gdl_atom list * gdl_atom list
+(* Definition with expanded definitions: expansion of a negated
+   relation brings negated conjunctions. *)
+type exp_def_branch =
+    term list * gdl_atom list * gdl_atom list list
+type exp_def =
+    string * exp_def_branch list
+
+module Terms = Set.Make (
+  struct type t = term let compare = Pervasives.compare end)
+
+(*
+let branch_vars (args, body, neg_body) =
+*)  
+
+let rules_of_entry = function
+  | Datalog (rel, args, body) ->
+    let head = rel, args in
+    let bodies = Aux.product (List.map body_of_literal body) in
+    List.map (fun body ->
+      let pos_body, neg_body = Aux.partition_choice body in
+      head, pos_body, neg_body) bodies
+  | Next (head, body) ->
+    let head = "next", [head] in
+    let bodies = Aux.product (List.map body_of_literal body) in
+    List.map (fun body ->
+      let pos_body, neg_body = Aux.partition_choice body in
+      head, pos_body, neg_body) bodies
+  | Legal (arg1, arg2, body) ->
+    let head = "legal", [arg1; arg2] in
+    let bodies = Aux.product (List.map body_of_literal body) in
+    List.map (fun body ->
+      let pos_body, neg_body = Aux.partition_choice body in
+      head, pos_body, neg_body) bodies
+  | Goal (arg, payoff, body) ->
+    let head = "goal", [arg; Const (string_of_int payoff)] in
+    let bodies = Aux.product (List.map body_of_literal body) in
+    List.map (fun body ->
+      let pos_body, neg_body = Aux.partition_choice body in
+      head, pos_body, neg_body) bodies
+  | GoalPattern (arg, var, body) ->
+    let head = "goal", [arg; Var var] in
+    let bodies = Aux.product (List.map body_of_literal body) in
+    List.map (fun body ->
+      let pos_body, neg_body = Aux.partition_choice body in
+      head, pos_body, neg_body) bodies
+  | Terminal body ->
+    let head = "terminal", [] in
+    let bodies = Aux.product (List.map body_of_literal body) in
+    List.map (fun body ->
+      let pos_body, neg_body = Aux.partition_choice body in
+      head, pos_body, neg_body) bodies
+  | Role arg -> [("role", [arg]), [], []]
+  | Initial (arg, body) ->
+    let head = "init", [arg] in
+    let bodies = Aux.product (List.map body_of_literal body) in
+    List.map (fun body ->
+      let pos_body, neg_body = Aux.partition_choice body in
+      head, pos_body, neg_body) bodies
+  | Atomic (rel, args) -> [(rel, args), [], []]
+
+let defs_of_rules rules : (string * exp_def_branch list) list =
+  Aux.map_reduce
+    (fun ((drel, params), body, neg_body) ->
+      drel,(params, body, List.map (fun a->[a]) neg_body))
+    (fun x y->y::x) [] rules
+
+(* Only use [rules_of_defs] when sure that no multi-premise negative
+   literal has been expanded. *)
+let rules_of_defs (defs : exp_def list) =
+  Aux.concat_map (fun (rel, branches) ->
+    List.map (fun (args, body, neg_body) ->
+      let neg_body =
+        List.map (function [a]->a | _ -> assert false) neg_body in
+      (rel, args), body, neg_body) branches) defs
+
+(* Stratify either w.r.t. the dependency graph ([~def:true]) or its
+   subgraph the negation graph ([~def:false]). *)
+let rec stratify ?(def=false) strata (defs : exp_def list) =
+  match
+    List.partition (fun (_, branches) ->
+      List.for_all (fun (_, body, neg_body) ->
+        List.for_all (fun (rel1,_) ->
+          rel1 = "distinct" || rel1 = "true" || rel1 = "does" ||
+            not (List.mem_assoc rel1 defs))
+          (if def then body @ List.concat neg_body
+           else List.concat neg_body)) branches) defs
+  with
+    | [], [] -> List.rev strata
+    | stratum, [] -> List.rev (stratum::strata)
+    | [], _ ->
+      if def then raise
+        (Lexer.Parsing_error
+           "GDL.stratify: recursive non-static definitions not handled yet")
+      else raise
+        (Lexer.Parsing_error
+           "GDL.stratify: cyclic negation dependency")
+    | stratum, rules -> stratify (stratum::strata) rules
+      
+
+let rec subst_one (x, term as sb) = function
+  | Var y when x=y -> term
+  | MVar y when x=y -> term
+  | (Const _ | Var _ | MVar _ as t) -> t
+  | Func (f, args) ->
+    Func (f, List.map (subst_one sb) args)
+
+let rec unify sb terms1 terms2 =
+  match terms1, terms2 with
+    | [], [] -> sb
+    | Const a::terms1, Const b::terms2 when a=b ->
+      unify sb terms1 terms2
+    | Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g ->
+      unify sb (args1 @ terms1) (args2 @ terms2)
+    | Var x::terms1, Var y::terms2 when x=y ->
+      unify sb terms1 terms2
+    | (Var x::terms1, (Var _ | Const _ as term)::terms2
+          | (Const _ as term)::terms1, Var x::terms2) ->
+      let sb1 = x, term in
+      unify (sb1::List.map (fun (x,t)->x, subst_one sb1 t) sb)
+        (List.map (subst_one sb1) terms1)
+        (List.map (subst_one sb1) terms2)
+    | (Var x::_, term::_ | term::_, Var x::_)
+        when Aux.Strings.mem x (term_vars term) ->
+      raise Not_found
+    | Var x::terms1, term::terms2 | term::terms1, Var x::terms2 ->
+      let sb1 = x, term in
+      unify (sb1::List.map (fun (x,t)->x, subst_one sb1 t) sb)
+        (List.map (subst_one sb1) terms1)
+        (List.map (subst_one sb1) terms2)
+    | _ -> raise Not_found
+
+(* 3d *)
+(* Match the first argument as term against the second argument as
+   pattern. Allow nonlinear (object) variables. *)
+let rec match_meta sb m_sb terms1 terms2 =
+  match terms1, terms2 with
+    | [], [] -> sb, m_sb
+    | (Const _ (* | Var _ *) as a)::terms1,
+      (Const _ (* | Var _ *) as b)::terms2
+      when a=b -> match_meta sb m_sb terms1 terms2
+    | Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g ->
+      match_meta sb m_sb (args1 @ terms1) (args2 @ terms2)
+    | term::terms1, MVar x::terms2 ->
+      (* we don't substitute because metavariables are linear *)
+      match_meta sb ((x, term)::m_sb) terms1 terms2
+    | MVar _::_, _ -> raise Not_found
+    | term::terms1, Var x::terms2 ->
+      let sb1 = x, term in
+      let sb = 
+        if List.mem_assoc x sb then
+          if List.assoc x sb = term then sb
+          else raise Not_found
+        else sb1::sb in
+      match_meta sb m_sb terms1 terms2
+    | _ -> raise Not_found
+
+
+(* 3c1 *)
+let generalize term1 term2 =
+  let fresh_count = ref 0 in
+  let rec loop pf terms1 terms2 =
+  match terms1, terms2 with
+    | [], [] -> (0, 0), []
+    | (Const a as cst)::terms1, Const b::terms2 when a=b ->
+      let (good_vars, good_csts), gens = loop pf terms1 terms2 in
+      (good_vars, good_csts+1), cst::gens
+    | Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g ->
+      let (good_vars1, good_csts1), gen_args = loop f args1 args2 in
+      let (good_vars2, good_csts2), gens = loop pf terms1 terms2 in
+      (good_vars1+good_vars2, good_csts1+good_csts2),
+      (Func (f,gen_args))::gens
+    | (Var x as var)::terms1, Var y::terms2 when x=y ->
+      let (good_vars, good_csts), gens = loop pf terms1 terms2 in
+      (good_vars+1, good_csts), var::gens
+    | _::terms1, _::terms2 ->
+      let measure, gens = loop pf terms1 terms2 in
+      incr fresh_count;
+      measure, MVar ("MV"^string_of_int !fresh_count)::gens
+    | _::_, [] | [], _::_ -> raise
+      (Lexer.Parsing_error
+         ("GDL.generalize: arity mismatch at function "^pf)) in
+  let measure, gens = loop "impossible" [term1] [term2] in
+  measure, !fresh_count, List.hd gens
+
+(* 3c2 *)
+let abstract_consts fresh_count term =
+  let fresh_count = ref fresh_count in
+  let rec loop = function
+    | Const _ -> incr fresh_count; MVar ("MV"^string_of_int !fresh_count)
+    | Func (f,args) -> Func (f, List.map loop args)
+    | term -> term in
+  loop term
+
+let rec subst sb = function
+  | Var y as t ->
+    (try List.assoc y sb with Not_found -> t)
+  | MVar y as t ->
+    (try List.assoc y sb with Not_found -> t)
+  | Const _ as t -> t
+  | Func (f, args) ->
+    Func (f, List.map (subst sb) args)
+
+let unify_rels (rel1, args1) (rel2, args2) =
+  if rel1 = rel2 then unify [] args1 args2
+  else raise Not_found
+
+let subst_rel sb (rel, args) = rel, List.map (subst sb) args
+let subst_rels sb body = List.map (subst_rel sb) body
+let extend_sb sb1 sb = Aux.map_prepend sb1 (fun (x,t)->x, subst sb1 t) sb
+
+let compose_sb sb1 sb2 =
+  let vars1, terms1 = List.split sb1 in
+  let vars2, terms2 = List.split sb2 in
+  let var_terms = List.map (fun v->Var v) (vars1 @ vars2) in
+  unify [] var_terms (terms1 @ terms2)
+
+let subst_br sb (head, body, neg_body) =
+  List.map (subst sb) head,
+  List.map (subst_rel sb) body,
+  List.map (List.map (subst_rel sb)) neg_body
+
+let fact_str (rel, args) =
+  "("^rel^" "^String.concat " " (List.map term_str args) ^")"
+
+let tuples_str tups =
+  let tup_str tup =
+    "("^String.concat " " (List.map term_str tup) ^")" in
+  String.concat " " (List.map tup_str tups)
+
+let facts_str facts =
+  String.concat " " (List.map fact_str facts)
+let neg_facts_str negs =
+  String.concat " "
+    (List.map (fun d -> "(not (and "^facts_str d^"))") negs)
+
+let def_str (rel, branches) =
+  String.concat "\n" (List.map (fun (args, body, neg_body) ->
+    "("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
+      " " ^ neg_facts_str neg_body ^ ")"
+  ) branches)
+
+let sb_str sb =
+  String.concat ", " (List.map (fun (v,t)->v^":="^term_str t) sb)
+
+(* 1b *)
+
+(* TODO: optimize by using rel-indexing (also in [aggregate_playout]).
+   TODO: optimize by using constant-time append data structure. *)
+let saturate base rules =
+
+  let instantiate_one tot_base cur_base irules =
+    Aux.concat_map (function
+      | head, [], neg_body ->
+        if List.mem head tot_base then []
+        else if List.exists (fun (rel,args as neg_atom) ->
+          rel = "distinct" && Aux.not_unique args ||
+            List.mem neg_atom tot_base) neg_body then []
+        else [Aux.Left head]
+      | head, cond1::body, neg_body ->
+        Aux.map_try (fun fact ->
+          (* {{{ log entry *)
+
+          if !debug_level > 5 then (
+            Printf.printf "instantiate_one: trying to unify %s and %s\n%!"
+              (fact_str fact) (fact_str cond1)
+          );
+
+          (* }}} *)
+          let sb = unify_rels fact cond1 in
+          (* {{{ log entry *)
+          if !debug_level > 5 then (
+            Printf.printf "instantiate_one: succeeded with %s\n%!"
+              (sb_str sb)
+          );
+          (* }}} *)
+          let irule =
+            subst_rel sb head,
+            subst_rels sb body, subst_rels sb neg_body in
+          Aux.Right irule
+        ) cur_base) irules in
+
+  let rec inst_stratum old_base old_irules cur_base cur_irules =
+    (* {{{ log entry *)
+
+    if !debug_level > 4 then (
+      Printf.printf "inst_stratum: old_base = %s; cur_base = %s\n%!"
+        (facts_str old_base) (facts_str cur_base);
+      Printf.printf
+        "inst_stratum: #old_irules = %d, #cur_irules = %d\n%!"
+        (List.length old_irules) (List.length cur_irules)
+    );
+
+    (* }}} *)
+    let base = Aux.unique_sorted (cur_base @ old_base)
+    and irules = Aux.unique_sorted (cur_irules @ old_irules) in
+    let new_base1, new_irules1 =
+      Aux.partition_choice (instantiate_one base cur_base cur_irules) in
+    (* {{{ log entry *)
+    if !debug_level > 4 then (
+      Printf.printf "inst_stratum: cur-cur = %s\n%!"
+        (facts_str new_base1)  
+    );
+    (* }}} *)
+    let new_base2, new_irules2 =
+      Aux.partition_choice (instantiate_one base cur_base old_irules) in
+    (* {{{ log entry *)
+    if !debug_level > 4 then (
+      Printf.printf "inst_stratum: cur-old = %s\n%!"
+        (facts_str new_base2)  
+    );
+    (* }}} *)
+    let new_base3, new_irules3 =
+      Aux.partition_choice (instantiate_one base old_base cur_irules) in
+    (* {{{ log entry *)
+    if !debug_level > 4 then (
+      Printf.printf "inst_stratum: old-cur = %s\n%!"
+        (facts_str new_base3)  
+    );
+    (* }}} *)
+    let new_base = Aux.unique_sorted (new_base1 @ new_base2 @ new_base3)
+    and new_irules = Aux.unique_sorted
+      (new_irules1 @ new_irules2 @ new_irules3) in
+    let new_base =
+      List.filter (fun f->not (List.mem f base)) new_base in
+    let new_irules =
+      List.filter (fun f->not (List.mem f irules)) new_irules in    
+    if new_base = [] && new_irules = []
+    then base
+    else inst_stratum base irules new_base new_irules in
+  
+  let rec instantiate base = function
+    | [] -> base
+    | stratum::strata ->
+      instantiate (inst_stratum [] [] base stratum) strata in
+
+  instantiate base
+    (List.map rules_of_defs (stratify [] (defs_of_rules rules)))
+
+
+let playing_as = ref (Const "uninitialized")
+let game_description = ref []
+let player_terms = ref [| |]
+
+let state_of_file s =
+  Printf.printf "GDL: Loading file %s...\n%!" s;
+  let f = open_in s in
+  let res =
+    ArenaParser.parse_game_state Lexer.lex
+      (Lexing.from_channel f) in
+  Printf.printf "GDL: File %s loaded.\n%!" s;
+  res
+
+(* 6 *)
+
+(* Need a global access so that the count can be reset between
+   different translations. (Generalization uses a local [fresh_count]
+   state.) *)
+let freshen_count = ref 0
+
+(* TODO: do proper elegant renaming... *)
+let freshen_branch (args, body, neg_body) =
+  incr freshen_count;
+  let rec map_vnames = function
+    | Var x -> Var (x^string_of_int !freshen_count)
+    | MVar x -> MVar (x^string_of_int !freshen_count)
+    | Const _ as t -> t
+    | Func (f, args) ->
+      Func (f, List.map map_vnames args) in
+  let map_rel (rel, args) =
+    rel, List.map map_vnames args in
+  List.map map_vnames args,
+  List.map map_rel body,
+  List.map (List.map map_rel) neg_body
+
+let freshen_def_branches =
+  List.map freshen_branch
+
+(* assumption: [defs] bodies are already clean of defined relations *)
+let subst_def_branch (defs : exp_def list)
+    (head, body, neg_body as br : exp_def_branch) : exp_def_branch list =
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "Expanding branch %s\n%!" (def_str ("BRANCH", [br]));
+  );
+  (* }}} *)
+  (* 6a *)
+  let sols =
+    List.fold_left (fun sols (rel, args as atom) ->
+      (let try def =
+         freshen_def_branches (List.assoc rel defs) in
+       (* {{{ log entry *)
+       if !debug_level > 3 then (
+         Printf.printf "Expanding positive %s by %s\n%!" rel
+           (def_str (rel, def))
+       );
+       (* }}} *)
+       Aux.concat_map (fun (pos_sol, neg_sol, sb) ->
+         let args = List.map (subst sb) args in
+         Aux.map_some (fun (dparams, dbody, dneg_body) ->
+           try
+             let sb1 = unify [] dparams args in
+             Some (
+               subst_rels sb1 (dbody @ pos_sol),
+               List.map (subst_rels sb1) (dneg_body @ neg_sol),
+               extend_sb sb1 sb)
+           with Not_found -> None
+         ) def
+       ) sols
+       with Not_found ->
+         List.map (fun (pos_sol, neg_sol, sb) ->
+           subst_rel sb atom::pos_sol, neg_sol, sb) sols))
+      ([[],[],[]]) body in
+  (* 6b *)
+  let sols =
+    List.fold_left (fun sols -> function [rel, args as atom] ->
+      (let try def =
+         freshen_def_branches (List.assoc rel defs) in
+       List.map (fun (pos_sol, neg_sol, sb) ->
+         let args = List.map (subst sb) args in
+         let more_neg =
+           Aux.map_some (fun (dparams, dbody, dneg_body) ->
+             if dneg_body <> [] then
+               failwith
+                 ("GDL.subst_def_branch: negation in negatively used" ^
+                     " defined rels not supported yet, relation "^rel);
+             try
+               let sb1 = unify [] dparams args in
+               Some (subst_rels sb1 dbody)
+             with Not_found -> None
+           ) def in
+         pos_sol, more_neg @ neg_sol, sb
+       ) sols
+       with Not_found ->
+         List.map (fun (pos_sol, neg_sol, sb) ->
+           pos_sol, [subst_rel sb atom]::neg_sol, sb) sols)
+      | _ -> failwith
+        "GDL.subst_def_branch: unimplemented, see (6b1) of spec")
+      sols neg_body in
+  Aux.map_some (fun (pos_sol, neg_sol, sb) ->
+    if List.mem [] neg_sol then None
+    else Some (List.map (subst sb) head, pos_sol, neg_sol)) sols
+
+(* Stratify and expand all relations in the given set. *)
+let expand_def_rules ?(more_defs=[]) rules =
+  let rec loop base = function
+    | [] -> base
+    | stratum::strata ->
+      let step = List.map (fun (rel, branches) ->
+        rel, Aux.concat_map
+          (subst_def_branch (more_defs@base)) branches) stratum in
+      loop (base @ step) strata in
+  match stratify ~def:true [] (defs_of_rules rules) with
+    | [] -> []
+    | [no_defined_rels] when more_defs=[] -> no_defined_rels
+    | def_base::def_strata when more_defs=[] -> loop def_base def_strata
+    | def_strata -> loop more_defs def_strata
+
+
+(* As [subst_def_branch], but specifically for "legal" definition and
+   result structured by "legal" definition branches. *)
+(* 7b *)
+let subst_legal_rule
+    (legal_args, legal_body, legal_neg_body : exp_def_branch)
+    (head, body, neg_body : exp_def_branch)
+    : (exp_def_branch * exp_def_branch) option =
+  if List.exists (List.exists (fun (rel,_)->rel="does")) neg_body
+  then failwith
+    "GDL.translate_game: negated \"does\" conditions not implemented yet";
+  try
+    let body, more_neg_body, sb =
+    List.fold_left (fun (body,more_neg_body,sb) (rel, args as atom) ->
+      if rel = "does" then
+        List.rev_append legal_body body,
+        List.rev_append legal_neg_body more_neg_body,
+        unify sb legal_args args
+      else atom::body, more_neg_body, sb) ([],[],[]) body in
+                   
+    Some (
+      (List.map (subst sb) legal_args,
+       List.map (subst_rel sb) legal_body,
+       List.map (List.map (subst_rel sb)) legal_neg_body),
+      (List.map (subst sb) head,
+       List.map (subst_rel sb) (List.rev body),
+       List.map (List.map (subst_rel sb))
+         (List.rev_append more_neg_body neg_body)))
+  with Not_found -> None
+
+(* 1 *)
+
+(* Collect the aggregate playout, but also the actions available in
+   the state. *)
+let aggregate_ply players static current rules =
+  let base =
+    Aux.map_prepend static (fun term -> "true", [term]) current in
+  let base = saturate (base @ static) rules in
+  let does = Aux.map_some (fun (rel, args) ->
+    if rel = "legal" then Some ("does", args) else None) base in
+  if                                    (* no move *)
+    Aux.array_existsi (fun _ player ->
+      List.for_all (function _, (actor::_) -> player <> actor | _ -> true)
+        does) players
+  then raise Not_found
+  else
+    let step = saturate (does @ base) rules in
+    let step = Aux.map_some (function ("next", [arg]) -> Some arg
+      | _ -> None) step in
+    if !aggregate_fixpoint &&           (* fixpoint reached *)
+      List.for_all (function
+        | Func (_,[arg]) when
+            Aux.array_existsi (fun _ player -> arg=player) players -> true
+        | term -> List.mem term current
+      ) step
+    then raise Not_found
+    else
+      List.map snd does, step
+
+(* Besides the aggregate 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. *)
+let aggregate_playout players horizon rules =
+  (* separate and precompute the static part *)
+  let rec separate static_rels state_rels =
+    let static, more_state =
+      List.partition (fun rel ->
+        List.for_all (fun ((rule,_), body, neg_body) ->
+          rule <> rel || List.for_all (fun srel ->
+            not (List.mem_assoc srel (neg_body @ body))) state_rels)
+          rules) static_rels in
+    if more_state = [] then static_rels, state_rels
+    else separate static (more_state @ state_rels) in
+  let static_rels, state_rels =
+    separate (List.map (fun ((r,_),_,_)->r) rules)
+      ["init"; "does"; "true"; "next"; "terminal"; "goal"] in
+  let static_rules, dynamic_rules = List.partition
+    (fun ((rel,_),_,_) -> List.mem rel static_rels) rules in
+  let static_base = saturate [] static_rules in
+  let state_rules =
+    (* 1a *)
+    if !aggregate_drop_negative then
+      List.map (function
+        | ("legal", _ as head), body, _ -> head, body, []
+        | ("does", _ as head), body, _ -> head, body, []
+        | rule -> rule) dynamic_rules
+    else dynamic_rules in    
+  let rec loop actions_accu state_accu step state =
+    (* {{{ log entry *)
+
+    if !debug_level > 0 then (
+      Printf.printf "aggregate_playout: step %d...\n%!" step
+    );
+
+    (* }}} *)
+    (let try actions, next =
+       aggregate_ply players static_base state state_rules in
+    (* {{{ log entry *)
+
+    if !debug_level > 0 then (
+      Printf.printf "aggregate_playout: state %s\n%!"
+        (String.concat " " (List.map term_str next))
+    );
+
+    (* }}} *)
+    if step < horizon then
+      loop (actions::actions_accu) (state::state_accu) (step+1) next
+    else 
+      List.rev (actions::actions_accu),
+      List.rev (next::state::state_accu)
+     with Not_found ->
+       List.rev actions_accu, List.rev (state::state_accu)) in
+  (* FIXME: this is identity, right? remove *)
+  let init_base = saturate static_base state_rules in
+  let init_state =
+    Aux.map_some (function ("init", [arg]) -> Some arg
+      | _ -> None) init_base in
+  (* {{{ log entry *)
+  if !debug_level > 0 then (
+    Printf.printf "aggregate_playout: init %s\n%!"
+      (String.concat " " (List.map term_str init_state))
+  );
+  (* }}} *)
+  static_rules, dynamic_rules, static_base, init_state,
+    loop [] [] 0 init_state
+
+
+let find_cycle cands =
+  let rec loop cycle trav pref rem path =
+    if cycle = [] then
+      let ini = [List.hd path] in
+      loop ini ini ini [] (List.tl path)
+    else match path, rem with
+      | _, [] -> loop cycle trav [] cycle path
+      | [], _ -> cycle                  (* consumed the whole path *)
+      | x::tail, y::rem when x=y || x = None->
+        (* either elements agree or indifferent path element *)
+        loop cycle (x::trav) (y::pref) rem tail
+      | x::tail, None::rem ->
+        (* instantiating undecided cycle element *)
+        loop (List.rev pref @ [x] @ rem) (x::trav) (x::pref) rem tail
+      | x::tail, _::_ ->
+        (* mismatch: grow the cycle to current point *)
+        let trav = x::trav in
+        let cycle = List.rev trav in
+        loop cycle trav [] cycle tail in
+  loop [] [] [] [] cands
+
+let cmp_masks t1 t2 =
+  (* {{{ log entry *)
+  if !debug_level > 4 then (
+    Printf.printf "cmp_masks: %s <= %s .. " (term_str t1) (term_str t2);
+  );
+  (* }}} *)
+  try ignore (match_meta [] [] [t2] [t1]);
+      (* {{{ log entry *)
+      if !debug_level > 4 then (
+        Printf.printf "true\n%!";
+      );
+      (* }}} *)
+      true
+  with Not_found ->
+    (* {{{ log entry *)
+    if !debug_level > 4 then (
+      Printf.printf "false\n%!";
+    );
+    (* }}} *)
+    false
+
+let rec blank_out = function
+  | Const a as c, Const b when a = b -> c
+  | (*Var _ as*) v, Var _ -> v
+  | t, MVar _ -> Const "_BLANK_"
+  | Func (f, f_args), Func (g, g_args) when f = g ->
+    Func (f, List.map blank_out (List.combine f_args g_args))
+  | a, b ->
+    Printf.printf "blank_out mismatch: term %s, mask %s\n%!"
+      (term_str a) (term_str b);
+    assert false
+
+let translate_game game_descr =
+  freshen_count := 0;
+  let player_terms =
+    Array.of_list
+      (Aux.map_some (function Role p -> Some p | _ -> None) game_descr) in
+  let players_n = Array.length player_terms in
+  let find_player player =
+    Aux.array_argfind (fun p->p=player) player_terms in
+  let rules = Aux.concat_map rules_of_entry game_descr in
+  let static_rules, dynamic_rules, static_base, init_state,
+    (agg_actions, agg_states) =
+    aggregate_playout player_terms 30 rules in
+  (* (8) -- drop zero goal branches, "first round" *)
+  let dynamic_rules = List.filter
+    (function ("goal", [_; Const "0"]), _, _ -> false | _ -> true)
+    dynamic_rules in
+  let element_terms : term list =
+    List.fold_left (fun acc st -> Aux.unique_sorted (st @ acc)) []
+      agg_states in
+  let noop_cands = List.map (fun actions ->
+    let actions = Aux.map_reduce
+      (function [player; action] -> player, action
+        | _ -> assert false) (fun y x->x::y) [] actions in
+    (* 2a *)
+    List.map (function
+      | player, [Const _ as noop] -> player, Some noop
+      | player, _ -> player, None) actions
+  ) agg_actions in
+  let control_cands = List.map (fun noop_cands ->
+    List.fold_left (fun accu -> function
+      | player, None ->
+        if accu = None then Some player
+        else raise
+          (Lexer.Parsing_error
+             ("GDL.initialize_game: branching arena graphs"^
+                 " or simultaneous moves not supported yet"))
+      | _, Some _ -> accu) None noop_cands) noop_cands in
+  let noop_cands = List.map Aux.collect noop_cands in
+  (* throw in players with (multiple) constant actions *)
+  let control_noop_cands = List.map2 (fun ccand noops ->
+    let nccands, noops = Aux.partition_map
+      (function player, [] -> assert false
+        | player, [noop] -> Aux.Right (player, noop)
+        | player, more_actions -> Aux.Left player) noops in
+    match ccand, nccands with
+      | None, [player] -> Some player, noops
+      | Some _, [] -> ccand, noops
+      | _ -> failwith
+        "GDL.initialize_game: simultaneous moves not supported yet"
+  ) control_cands noop_cands in
+  let control_cands, noop_cands =
+    List.split control_noop_cands in
+  (* 2b *)
+  let loc_players = find_cycle control_cands in
+  (* {{{ log entry *)
+  if !debug_level > 0 then (
+    Printf.printf "translate_game: location players %s\n%!"
+      (String.concat " "
+         (List.map (function Some t->term_str t | None->"None")
+            loc_players))
+  );
+  (* }}} *)
+  let loc_players = Array.of_list
+    (List.map (function Some p -> p | None -> player_terms.(0))
+       loc_players) in
+  let loc_n = Array.length loc_players in
+  let find_player_locs player =
+    Aux.array_argfind_all (fun p->p=player) loc_players in
+  (* noop actions of a player in a location *)
+  let loc_noops =
+    let i = ref 0 in
+    let noops = ref noop_cands in
+    let loc_noops = Array.make_matrix loc_n players_n None in
+    while !noops <> [] do
+      List.iter (function _, None -> ()
+        | player, (Some _ as noop) ->
+          let p_i = find_player player in
+          if loc_noops.(!i).(p_i) = None
+          then loc_noops.(!i).(p_i) <- noop
+          else if loc_noops.(!i).(p_i) <> noop
+          (* moves are not simultaneous, but different [noop] actions
+             are used by the same player -- can be resolved by
+             introducing separate locations for each noop case *)
+          then failwith
+            "GDL.translate_game: noop-driven location splits unimplemented")
+        (List.hd !noops);
+      incr i; if !i = loc_n then i := 0;
+      noops := List.tl !noops
+    done;
+    loc_noops in
+  (* 6 *)
+  let static_rules, exp_static_rules =
+    List.partition (fun ((rel,args), _, _) ->
+      List.length args <= !expand_arity_above ||
+        List.exists (function ((r,_),[],[]) when rel=r-> true
+          | _ -> false) static_rules
+    ) static_rules in
+  (* {{{ log entry *)
+
+  if !debug_level > 0 then (
+    Printf.printf "translate_game: expanded static rules: %s\n%!"
+      (String.concat ", " (List.map (fun ((r,_),_,_)->r) exp_static_rules));
+  );
+
+  (* }}} *)
+  let static_exp_defs = expand_def_rules exp_static_rules in
+  let static_rules =
+    if static_exp_defs = [] then static_rules
+    else rules_of_defs
+      (List.map (fun (rel,branches) ->
+        rel, Aux.concat_map (subst_def_branch static_exp_defs) branches)
+         (defs_of_rules static_rules)) in
+  let exp_defs =
+    expand_def_rules ~more_defs:static_exp_defs dynamic_rules in
+  (* {{{ log entry *)
+  if !debug_level > 0 then (
+    Printf.printf "translate_game: All expanded dynamic rules:\n%s\n%!"
+      (String.concat "\n" (List.map def_str exp_defs))
+  );
+  (* }}} *)
+  (* 3 *)
+  let legal_rules = List.assoc "legal" exp_defs in
+  let next_rules = List.assoc "next" exp_defs in
+  (* 3b *)
+  let exp_next =
+    Aux.concat_map (subst_def_branch ["does", legal_rules]) next_rules in
+  (* {{{ log entry *)
+
+  if !debug_level > 0 then (
+    Printf.printf "translate_game: \"next\" rules with \"does\"<-\"legal\":\n%s\n%!"
+      (def_str ("next", exp_next))
+  );
+
+  (* }}} *)
+  (* 3c *)
+  let masks = List.map (function
+    | [next_arg], body, neg_body ->
+      let collect = Aux.map_some
+        (function "true", [arg] -> Some arg
+          | "true", _ -> raise
+            (Lexer.Parsing_error
+               ("GDL.initialize_game: invalid arity of \"true\" atom"))
+          | _ -> None) in
+      let pos_cands = collect body in
+      let neg_cands = Aux.concat_map collect neg_body in
+      let pos_gens = List.map (generalize next_arg) pos_cands in
+      let neg_gens = List.map (generalize next_arg) neg_cands in
+      (* using the fact that Pervasives.compare is lexicographic *)
+      let pos_gen = List.fold_left max ((-1,0),0,Const "") pos_gens in
+      let neg_gen = List.fold_left max ((-1,0),0,Const "") neg_gens in
+      let (_, fresh_count, mask as gen) = max pos_gen neg_gen in
+      if gen == pos_gen then mask
+      else abstract_consts fresh_count mask
+    | _ -> raise
+      (Lexer.Parsing_error
+         ("GDL.initialize_game: invalid arity of \"next\" atom")))
+    exp_next in
+  (* {{{ log entry *)
+  if !debug_level > 1 then (
+    Printf.printf "translate_game: Generalized element terms (mask candidates):\n%s\n%!"
+      (String.concat " " (List.map term_str masks))
+  );
+  (* }}} *)
+  (* find minimal *)
+  let masks = Aux.maximal (fun t1 t2->cmp_masks t2 t1) masks in
+  (* {{{ log entry *)
+  if !debug_level > 1 then (
+    Printf.printf "translate_game: Masks:\n%s\n%!"
+      (String.concat " " (List.map term_str masks))
+  );
+  (* }}} *)
+  (* 3e *)
+  let elements = List.fold_left (fun elements term ->
+    let mask, sb, m_sb =
+      match
+        Aux.map_try (fun mask ->
+          mask, match_meta [] [] [term] [mask]) masks
+      with [mask, (sb, m_sb)] -> mask, sb, m_sb
+        | _ -> assert false in          (* masks are minimal *)
+    let sbs, elements =
+      try Aux.pop_assoc mask elements
+      with Not_found -> [], elements in
+    (mask, if List.mem sb sbs then sbs else sb::sbs)::elements
+  ) [] element_terms in
+  let struc = Structure.empty_structure () in
+  let struc, elements =
+    List.fold_left (fun (struc, elements) (mask, sbs) ->
+      (* {{{ log entry *)
+      if !debug_level > 2 then (
+        Printf.printf "mask-elements:";
+      );
+      (* }}} *)
+      let struc, m_elements =
+        List.fold_left (fun (struc, m_elements) sb ->
+          let e_term = subst sb mask in
+          (* {{{ log entry *)
+          if !debug_level > 2 then (
+            Printf.printf ", %s%!" (term_to_name e_term)
+          );
+          (* }}} *)
+          let struc, elem =
+            Structure.add_new_elem struc ~name:(term_to_name e_term) () in
+          struc, (sb, elem)::m_elements
+        ) (struc, []) sbs in
+      (* {{{ log entry *)
+      if !debug_level > 2 then (
+        Printf.printf "\n%!";
+      );      
+      (* }}} *)
+      struc, (mask, m_elements)::elements
+    ) (struc, []) elements in
+  (* 4 *)
+  (* currently, position paths are approximated by variables
+     (non-variable positions are ignored) *)
+  let mask_paths = Aux.concat_map (function _, [] -> assert false
+    | mask, (sb,_)::_ -> List.map (fun (v,_)->mask, v) sb) elements in
+  (* 4a *)
+  let static_rels =
+    Aux.unique_sorted
+      (List.map (fun ((rname,args),_,_) ->
+        rname, List.map (fun _ -> ()) args) static_rules) in
+  let static_rels =
+    List.map (fun (rel,args) ->
+      rel, List.length args,
+      Aux.all_tuples_for args mask_paths) static_rels in
+  let static_base = Aux.collect static_base in
+  (* TODO: optimize by indexing elements by path position
+     terms (currently, substitution values) *)
+  let struc =
+    List.fold_left (fun struc (brel, arity, path_tups) ->
+      let brel_tups = List.assoc brel static_base in
+      (* {{{ log entry *)
+      if !debug_level > 0 then (
+        Printf.printf "Translating static relation %s with %d tuples:\n%s\n%!"
+          brel (List.length brel_tups) (tuples_str brel_tups);
+      );
+      (* }}} *)
+      List.fold_left (fun struc ptup ->
+        let rname = brel ^ "__" ^ String.concat "__"
+          (List.map (fun (mask,v)->
+            term_to_name mask ^ "_" ^ v) ptup) in
+        let struc =
+          Structure.add_rel_name rname (List.length ptup) struc in
+        (* {{{ log entry *)
+        if !debug_level > 1 then (
+          Printf.printf "static-rel: %s, of... %!" rname;
+        );
+        (* }}} *)
+        let elem_sets =
+          List.map (fun (mask,v)->
+            List.map (fun (sb,elem)->
+              try List.assoc v sb, elem
+              with Not_found -> assert false)
+              (List.assoc mask elements)) ptup in
+        (* {{{ log entry *)
+        if !debug_level > 1 then (
+          Printf.printf "%s ... %!" (String.concat "x" (
+            List.map (fun x-> string_of_int (List.length x)) elem_sets));
+        );
+        (* }}} *)
+        let elem_tups =
+          Aux.concat_map (fun ttup ->
+            let elem_sets = List.map2 (fun term elems ->
+              Aux.map_some (fun (tcand, e) ->
+                if tcand=term then Some e else None) elems
+            ) ttup elem_sets in
+            List.map Array.of_list (Aux.product elem_sets)
+          ) brel_tups in
+        (* {{{ log entry *)
+        if !debug_level > 1 then (
+          Printf.printf "%d tuples, adding to struc...%!"
+            (List.length elem_tups);
+        );
+        (* }}} *)
+        let res = Structure.unsafe_add_rels struc rname elem_tups in
+        (* {{{ log entry *)
+
+        if !debug_level > 1 then (
+          Printf.printf " done\n%!";
+        );
+
+        (* }}} *)
+        res
+      ) struc path_tups
+    ) struc static_rels in
+
+  (* 4b *)
+  let struc = List.fold_left (fun struc (mask,v) ->
+    let rname = "EQ___" ^ term_to_name mask ^ "_" ^ v in
+    let struc =
+      Structure.add_rel_name rname 2 struc in
+    let elems = List.assoc mask elements in
+    (* {{{ log entry *)
+    if !debug_level > 0 then (
+      Printf.printf "Adding static EQ relation %s over %d elements.\n%!"
+        rname (List.length elems);
+    );
+    (* }}} *)
+    let elem_tups =
+      List.fold_left (fun tups (sb1, e1) ->
+        List.fold_left (fun tups (sb2, e2) ->
+          try
+            if List.assoc v sb1 = List.assoc v sb2
+            then [|e1; e2|]::[|e2; e1|]::tups
+            else tups
+          with Not_found -> assert false
+        ) tups elems      
+      ) [] elems in
+    (* {{{ log entry *)
+    if !debug_level > 1 then (
+      Printf.printf "%d tuples, adding to struc...%!" (List.length elem_tups);
+    );
+    (* }}} *)
+    l...
 
[truncated message content]