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

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

Revision: 1517
          http://toss.svn.sourceforge.net/toss/?rev=1517&view=rev
Author:   lukstafi
Date:     2011-07-26 19:50:54 +0000 (Tue, 26 Jul 2011)

Log Message:
-----------
GDL translation work in progress (simple debugging). Does not compile yet.

Modified Paths:
--------------
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/TranslateFormula.ml
    trunk/Toss/GGP/TranslateFormula.mli
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-07-19 15:20:56 UTC (rev 1516)
+++ trunk/Toss/GGP/GDL.ml	2011-07-26 19:50:54 UTC (rev 1517)
@@ -18,20 +18,22 @@
   | Var of string
   | Func of string * term array
 
-type rel_atom = string * term list
+type rel_atom = string * term array
 (** Positive and negative literals separated, disjunctions expanded-out. *)
 type gdl_rule = rel_atom * rel_atom list * rel_atom list
 (** Collect rules by relations. *)
-type def_branch = term list * rel_atom list * rel_atom list
+type def_branch = term array * rel_atom list * rel_atom list
 type gdl_defs = (string * def_branch list) list
 
+type substitution = (string * term) list
+
 module Terms = Set.Make (
   struct type t = term let compare = Pervasives.compare end)
 module Atoms = Set.Make (
   struct type t = rel_atom let compare = Pervasives.compare end)
 
 type atom =
-  | Distinct of term list
+  | Distinct of term array
   | Rel of rel_atom
   | Role of term
   | True of term
@@ -58,15 +60,15 @@
   | Var v -> "?"^v
   | Func (f, args) ->
     "(" ^ f ^ " " ^ 
-      String.concat " " (List.map term_str (Array.to_list args)) ^ ")"
+      String.concat " " (Array.to_list (Array.map term_str args)) ^ ")"
 
 let rec term_to_name ?(nested=false) = function
   | Const c -> c
   | Var v -> v
   | Func (f, args) ->
     f ^ "_" ^ (if nested then "_S_" else "") ^
-      String.concat "_" (List.map (term_to_name ~nested:true) 
-			   (Array.to_list args)) ^
+      String.concat "_"
+      (Array.to_list (Array.map (term_to_name ~nested:true) args)) ^
       (if nested then "_Z_" else "")
 
 let rec term_vars = function
@@ -75,27 +77,36 @@
   | Func (f, args) -> terms_vars args
 
 and terms_vars args =
-  List.fold_left Aux.Strings.union Aux.Strings.empty
-    (List.map term_vars (Array.to_list args))
+  Array.fold_left Aux.Strings.union Aux.Strings.empty
+    (Array.map term_vars args)
   
+let rec atoms_of_body body =
+  Aux.concat_map
+    (function Pos a -> [a] | Neg a -> [a]
+      | Disj ds -> atoms_of_body ds) body
 
+let atoms_of_clause (rel_atom, body) =
+  Rel rel_atom :: atoms_of_body body
+
 let rel_of_atom = function
-  | Distinct args -> "distinct", args   (* not a proper relation -- avoid *)
+  | Distinct args -> "distinct", args
+     (* not a proper relation -- avoid *)
   | Rel (rel, args) -> rel, args
-  | Role arg -> "role", [arg]
-  | True arg -> "true", [arg]
-  | Does (arg1, arg2) -> "does", [arg1; arg2]
+  | Role arg -> "role", [|arg|]
+  | True arg -> "true", [|arg|]
+  | Does (arg1, arg2) -> "does", [|arg1; arg2|]
 
 let atom_of_rel = function
-  | "distinct", args -> Distinct args   (* not a proper relation -- avoid *)
-  | "role", [arg] -> Role arg
-  | "true", [arg] -> True arg
-  | "does", [arg1; arg2] -> Does (arg1, arg2)
+  | "distinct", args -> Distinct args
+     (* not a proper relation -- avoid *)
+  | "role", [|arg|] -> Role arg
+  | "true", [|arg|] -> True arg
+  | "does", [|arg1; arg2|] -> Does (arg1, arg2)
   | rel, args -> Rel (rel, args)
 
 let rec body_of_literal = function
   | Pos (Distinct args) ->
-    [Aux.Right ("distinct", args)]        (* not negated actually! *)
+    [Aux.Right ("distinct", args)] (* not negated actually! *)
   | Neg (Distinct _) -> assert false
   | Pos atom -> [Aux.Left (rel_of_atom atom)]
   | Neg atom -> [Aux.Right (rel_of_atom atom)]
@@ -106,33 +117,31 @@
   Aux.map_some (function Func (g, args) when f=g -> Some args | _-> None) terms
 
 
-let gdl_rule_vars (head, body, neg_body) =
+let gdl_rule_vars ((_,head_args), body, neg_body) =
   List.fold_left Aux.Strings.union Aux.Strings.empty
     (List.map terms_vars
-       (head::List.map snd (body @ neg_body)))
+       (head_args::List.map snd (body @ neg_body)))
 
 let gdl_rules_vars brs =
   List.fold_left Aux.Strings.union Aux.Strings.empty
     (List.map gdl_rule_vars brs)
 
-let rels_vars body =
+let rels_vars (body : (string * term array) list) =
   List.fold_left Aux.Strings.union Aux.Strings.empty
     (List.map (fun (_,args)->terms_vars args) body)
 
 let gdl_defs_vars defs =
-  List.fold_left
-    (fun acc rels -> Aux.Strings.union acc (rels_vars rels))
-    Aux.Strings.empty
-    (Aux.concat_map (fun (hd,body,neg_body) ->
-      ("",hd)::body @ neg_body) (Aux.concat_map snd defs))  
+    rels_vars
+      (Aux.concat_map (fun (hd,body,neg_body) ->
+        ("",hd)::body @ neg_body) (Aux.concat_map snd defs))  
 
-let rules_of_clause (head, body) =
+let rule_of_clause (head, body) =
   let body, neg_body =
     Aux.partition_choice (Aux.concat_map body_of_literal body) in
   head, body, neg_body
 
 
-let clause_vars cl = gdl_rule_vars (rules_of_clause cl)
+let clause_vars cl = gdl_rule_vars (rule_of_clause cl)
 
 let defs_of_rules rules =
   Aux.map_reduce (fun ((rel, args), body, neg_body) ->
@@ -191,7 +200,7 @@
   | Var y when x=y -> term
   | (Const _ | Var _ as t) -> t
   | Func (f, args) ->
-    Func (f, List.map (subst_one sb) args)
+    Func (f, Array.map (subst_one sb) args)
 
 (* Eliminate [terms1] variables when possible. *)
 let rec unify sb terms1 terms2 =
@@ -200,7 +209,7 @@
     | 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)
+      unify sb (Array.to_list args1 @ terms1) (Array.to_list args2 @ terms2)
     | Var x::terms1, Var y::terms2 when x=y ->
       unify sb terms1 terms2
     | (Var x::terms1, (Var _ | Const _ as term)::terms2
@@ -219,13 +228,15 @@
         (List.map (subst_one sb1) terms2)
     | _ -> raise Not_found
 
+let unify_args args1 args2 =
+  unify [] (Array.to_list args1) (Array.to_list args2)
 
 let rec subst sb = function
   | Var 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)
+    Func (f, Array.map (subst sb) args)
 
 let rec unify_all sb = function
   | [] | [_] -> sb
@@ -241,14 +252,14 @@
   with Not_found -> false
 
 let unify_rels (rel1, args1) (rel2, args2) =
-  if rel1 = rel2 then unify [] args1 args2
+  if rel1 = rel2 then unify_args args1 args2
   else raise Not_found
 
 let rels_unify atom1 atom2 =
   try ignore (unify_rels atom1 atom2); true
   with Not_found -> false
 
-let subst_rel sb (rel, args) = rel, List.map (subst sb) args
+let subst_rel sb (rel, args) = rel, Array.map (subst sb) args
 let subst_rels sb body = List.map (subst_rel sb) body
 
 let compose_sb sb1 sb2 =
@@ -258,13 +269,13 @@
   unify [] var_terms (terms1 @ terms2)
 
 let subst_br sb (args, body, neg_body) =
-  List.map (subst sb) args,
+  Array.map (subst sb) args,
   subst_rels sb body,
-  List.map (fun (uni_vs,neg) -> uni_vs, subst_rels sb neg) neg_body
+  subst_rels sb neg_body
 
 
 let subst_atom sb = function
-  | Distinct args -> Distinct (List.map (subst sb) args)
+  | Distinct args -> Distinct (Array.map (subst sb) args)
   | Rel rel_atom -> Rel (subst_rel sb rel_atom)
   | Role arg -> Role (subst sb arg)
   | True arg -> True (subst sb arg)
@@ -279,13 +290,9 @@
   subst_rel sb head, List.map (subst_literal sb) body
 
 let rel_atom_str (rel, args) =
-  "(" ^ rel ^ " " ^ String.concat " " (List.map term_str args) ^ ")"
+  "(" ^ rel ^ " " ^
+    String.concat " " (Array.to_list (Array.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 terms_str facts =
   String.concat ", " (List.map term_str facts)
 
@@ -309,7 +316,7 @@
   String.concat ", " (List.map (fun (v,t)->v^":="^term_str t) sb)
 
 let proto_rel_str (rel, args) =
-  rel ^"(" ^ String.concat ", " (Array.to_list args) ^")"
+  rel ^"(" ^ String.concat ", " args ^")"
 
 
 (* TODO: optimize by using rel-indexing (also in [aggregate_playout]).
@@ -317,16 +324,17 @@
 (* Variables still left after saturation have universal interpretation! *)
 let saturate base rules =
 
-  let instantiate_one tot_base cur_base irules =
+  let instantiate_one (tot_base : rel_atom list)
+      (cur_base : rel_atom list) 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 ||
+          rel = "distinct" && Aux.not_unique (Array.to_list args) ||
             (* faster option: *)
             (* List.mem neg_atom tot_base *)
             (* accurate option: *)
-            List.exists (unifies neg_atom) tot_base
+            List.exists (rels_unify neg_atom) tot_base
         ) neg_body then []
         else [Aux.Left head]
       | head, cond1::body, neg_body ->
@@ -423,27 +431,28 @@
         v, Aux.not_conflicting_name ~truncate:true !used_vars v)
       (Aux.Strings.elements br_vars) in
     used_vars := Aux.add_strings (List.map snd sb) !used_vars;
+    let sb = List.map (fun (v,t) -> v, Var t) sb in
     List.map (subst_br sb) brs in
-  let expand_atom (rel, args as atom) result =
+  (* FIXME: make sure it's OK!!! *)
+  let expand_atom (rel, args as atom)
+      (sb, (head, r_body, r_neg_body)) =
     (let try def_brs = freshen_brs (List.assoc rel defs) in
-     Aux.concat_map (fun (sb, (head, r_body, r_neg_body)) ->
-       let args = subst_terms sb args in
-       List.map (fun (params,d_body,d_neg_body) ->
-         let sb = unify sb params args in
-         let r_br =
-           head, d_body @ r_body, d_neg_body @ r_neg_body in
-         sb, subst_br sb r_br
-       ) def_brs
-     ) result
+     let args = Array.map (subst sb) args in
+     List.map (fun (params,d_body,d_neg_body) ->
+       let sb = unify sb (Array.to_list params) (Array.to_list args) in
+       let r_br =
+         head, d_body @ r_body, d_neg_body @ r_neg_body in
+       sb, subst_br sb r_br
+     ) def_brs
      with Not_found ->
-       List.map (fun (sb,(head,r_body,r_neg_body)) ->
-         sb, atom::r_body, r_neg_body) result) in
+         [sb, (head, atom::r_body, r_neg_body)]) in
   let expand_br (head, body, neg_body) =
     let init = [[], (head, [], neg_body)] in
     Aux.concat_foldr expand_atom body init in
   let rec fix n_brs brs i =
     let brs = Aux.concat_map expand_br brs in
     let new_n_brs = List.length brs in
+    let brs = List.map snd brs in
     if new_n_brs > n_brs && i > 0 then fix new_n_brs brs (i-1)
     else brs in
   fix (List.length brs) brs 5
@@ -454,19 +463,19 @@
 let negate_bodies conjs =
   let placeholder = "", [] in
   let clauses = List.map (fun body -> placeholder, body) conjs in
-  let clauses = List.map rules_of_clause clauses in
+  let clauses = List.map rule_of_clause clauses in
   let clauses = List.map (fun (_,body,neg_body) ->
-    List.map (fun a -> Pos (atom_of_clause a)) body @
-      List.map (fun a -> Neg (atom_of_clause a)) neg_body) clauses in
+    List.map (fun a -> Pos (atom_of_rel a)) body @
+      List.map (fun a -> Neg (atom_of_rel a)) neg_body) clauses in
   let negated = Aux.product clauses in
   (* can raise [Not_found] in case of unsatisfiable "not distinct" *)
   let nclause body =
     let uniterms, lits =
       Aux.partition_map (function
-        | Neg (Distinct terms) -> Left terms
-        | Neg atom -> Pos atom
-        | Pos atom -> Neg atom
-        | Disjunction _ -> assert false) body in
+        | Neg (Distinct terms) -> Aux.Left (Array.to_list terms)
+        | Neg atom -> Aux.Right (Pos atom)
+        | Pos atom -> Aux.Right (Neg atom)
+        | Disj _ -> assert false) body in
     let sb = List.fold_left unify_all [] uniterms in
     List.map (subst_literal sb) lits in
   Aux.map_try nclause negated
@@ -482,8 +491,8 @@
       List.map (fun v ->
         let nv = Aux.not_conflicting_name ~truncate:true !used_vars v in
         used_vars := Aux.Strings.add nv !used_vars;
-        v, nv
-      ) cl_vars in
+        v, Var nv
+      ) (Aux.Strings.elements cl_vars) in
     subst_clause sb cl
   ) clauses in
   used_vars, clauses    
@@ -507,7 +516,7 @@
         | Pos a -> Neg a
         | Neg a -> Pos a
         | _ -> assert false) lits
-  ) (List.map flatten_disjs body)
+  ) (flatten_disjs body)
 
 
 (* ************************************************************ *)
@@ -522,7 +531,7 @@
 
 let aggregate_ply players static current rules =
   let base =
-    Aux.map_prepend static (fun term -> "true", [term]) current in
+    Aux.map_prepend static (fun term -> "true", [|term|]) current in
   let base = saturate (base @ static) rules in
   (* {{{ log entry *)
   if !debug_level > 4 then (
@@ -535,15 +544,15 @@
   if                                    (* no move *)
     Aux.array_existsi (fun _ player ->
       List.for_all (function
-        |_, (Var _::_) -> false
-        | _, (actor::_) -> player <> actor | _ -> true)
+        |_, [|Var _; _ |] -> false
+        | _, [|actor; _ |] -> player <> actor | _ -> true)
         does) players
   then (
     (* {{{ log entry *)
     if !debug_level > 0 then (
       let players_nomove =
         Aux.array_find_all (fun player ->
-          List.for_all (function _, (actor::_) -> player <> actor
+          List.for_all (function _, [|actor; _|] -> player <> actor
             | _ -> true)
             does) players in          
       Printf.printf
@@ -554,11 +563,11 @@
     raise Playout_over)
   else
     let step = saturate (does @ base) rules in
-    let step = Aux.map_some (function ("next", [arg]) -> Some arg
+    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
+        | Func (_,[|arg|]) when
             Aux.array_existsi (fun _ player -> arg=player) players -> true
         | term -> List.mem term current
       ) step
@@ -594,8 +603,8 @@
   let static_base = saturate [] static_rules in
   let state_rules =
     List.map (function
-      | ("legal", [player; _] as head), body, neg_body ->
-        head, ("role", [player])::body,
+      | ("legal", [|player; _|] as head), body, neg_body ->
+        head, ("role", [|player|])::body,
         if !aggregate_drop_negative then [] else neg_body
       | ("does", _ (* as head *)), body, _ -> assert false
         (* head, body, [] *)
@@ -624,7 +633,7 @@
   (* 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
+    Aux.map_some (function ("init", [|arg|]) -> Some arg
       | _ -> None) init_base in
   (* {{{ log entry *)
   if !debug_level > 0 then (
@@ -664,18 +673,23 @@
   loop [] [] [] [] cands
 
 
+let player_vars_of rels =
+  Aux.map_some (function
+    | "does", [|Var v; _|] -> Some v
+    | "legal", [|Var v; _|] -> Some v
+    | _ -> None) rels
+
+
 let expand_players clauses =
   let players =
     Aux.map_some (function
-      | ("role", [player]), _ -> Some player
+      | ("role", [|player|]), _ -> Some player
       | _ -> None
     ) clauses in
-  let exp_clause (rel, _ as head, body as clause) =
+  let exp_clause clause =
     (* determine variables standing for players *)
     let plvars =
-      let head = if rel = "role" then [] else [head] in
-      Aux.concat_map player_vars_of
-        (head @ List.map rel_of_atom body) in
+      player_vars_of (List.map rel_of_atom (atoms_of_clause clause)) in
     if plvars = [] then [clause]
     else
       let sbs = List.map (fun v ->
@@ -700,7 +714,7 @@
     else aux (more @ nonstable)
       (List.filter (fun (rel,_) -> not (List.mem rel more)) remaining)
     in
-  aux [] remaining
+  aux [] defs
 
 
 let state_terms body =
@@ -735,6 +749,8 @@
   | Here_and_below of (string * path_set array) list
 (* Subtries are in sorted order. *)
 
+let empty_path_set = Empty
+
 let path_str p =
   String.concat "_" (List.map (fun (rel, arg) ->
     rel ^ "_" ^ string_of_int arg) p)
@@ -742,7 +758,10 @@
 let paths_union ps1 ps2 =
   let rec aux = function
     | Empty, p | p, Empty -> p
-    | Here, Below ps | Below ps, Here -> Here_and_below ps
+    | Here, Here -> Here
+    | Here, Below ps | Below ps, Here
+    | Here, Here_and_below ps
+    | Here_and_below ps, Here -> Here_and_below ps
     | Below ps1, Below ps2 -> Below (merge (ps1, ps2))
     | Below ps1, Here_and_below ps2
     | Here_and_below ps2, Below ps1
@@ -751,7 +770,7 @@
   and merge = function
     | [], ps | ps, [] -> ps
     | ((rel1, args1)::ps1), ((rel2, args2)::ps2) when rel1 = rel2 ->
-      let args = Aux.array_map2 aux args1 args2 in
+      let args = Aux.array_map2 (fun x y->aux (x,y)) args1 args2 in
       (rel1, args)::merge (ps1, ps2)
     | ((rel1, _ as rel_ps)::ps1), ((rel2, _)::_ as ps2) when rel1 < rel2 ->
       rel_ps::merge (ps1, ps2)
@@ -761,12 +780,16 @@
 
 let add_path arities p ps =
   let rec aux = function
-    | [], Empty -> Here
+    | [], (Here | Empty) -> Here
     | [], (Below ps | Here_and_below ps) -> Here_and_below ps
     | (rel, pos)::suffix, Below ps ->
       Below (add suffix rel pos ps)
     | (rel, pos)::suffix, Here_and_below ps ->
       Here_and_below (add suffix rel pos ps)
+    | (rel, pos)::suffix, Empty ->
+      Below (add suffix rel pos [])
+    | (rel, pos)::suffix, Here ->
+      Here_and_below (add suffix rel pos [])
   and add p rel pos ps =
     (let try args, ps = Aux.pop_assoc rel ps in
      (* Keeping functional... *)
@@ -806,7 +829,7 @@
   aux (ps, t)
 
 (** Find the subterm at given path, if the term does not have the
-    path, return [Not_found]; [at_path p t] is $t \tpos p$. *)
+    path, raise [Not_found]; [at_path p t] is $t \tpos p$. *)
 let at_path t p =
   let rec aux = function
     | [], t -> t
@@ -825,13 +848,13 @@
     | Empty, t -> []
     | Here, t -> [t]
     | Here_and_below subps, t -> t::(aux (Below subps, t))
-    | Below subps, (Func (rel, args) as t)
+    | Below subps, (Func (rel, args))
       when not fail_at_missing ->
       (let try argps = List.assoc rel subps in
        let res = Aux.array_map2 (fun ps t -> aux (ps,t)) argps args in
        List.concat (Array.to_list res)
        with Not_found -> [])
-    | Below [rel1, argps], (Func (rel2, args) as t)
+    | Below [rel1, argps], (Func (rel2, args))
       when rel1 = rel2 (* && fail_at_missing *) ->
        let res = Aux.array_map2 (fun ps t -> aux (ps,t)) argps args in
        List.concat (Array.to_list res)
@@ -845,8 +868,8 @@
     | Empty, t -> []
     | Here, t -> [f (List.rev revp) t]
     | Here_and_below subps, t ->
-      f (List.rev revp) t::(aux path (Below subps, t))
-    | Below subps, (Func (rel, args) as t) ->
+      f (List.rev revp) t::(aux revp (Below subps, t))
+    | Below subps, (Func (rel, args)) ->
       (let try argps = List.assoc rel subps in
        let res =
          Array.mapi (fun i ps -> aux ((rel,i)::revp) (ps,args.(i))) argps in
@@ -860,13 +883,14 @@
     that has been included, are not included. *)
 let rec term_paths ?(prefix_only=false) cond = function
   | Func (rel, args) as t ->
-    let subps = Array.map (term_paths p) args in
-    let no_sub = Array.for_all (fun subp -> subp = Empty) subps in
+    let subps = Array.map (term_paths ~prefix_only cond) args in
+    let no_sub = Aux.array_for_all (fun subp -> subp = Empty) subps in
     let here =  cond t in
     if no_sub && not here then Empty
-    else if here && not no_sub && not prefix_only then Here_and_below subps
+    else if here && not no_sub && not prefix_only
+    then Here_and_below [rel, subps]
     else if here then Here
-    else Below subps
+    else Below [rel, subps]
   | t -> if cond t then Here else Empty
       
 (** The number of nodes in a term tree. *)
@@ -894,10 +918,11 @@
 let paths_to_list ps =
   let rec subpaths subps =
     Aux.concat_map (fun (rel, subps) ->
-      Array.to_list
-        (Array.mapi (fun i ps ->
-          let sub_res = aux ps in
-          List.map (fun p -> (rel, i)::p) sub_res) subps)) subps
+      List.concat
+        (Array.to_list
+           (Array.mapi (fun i ps ->
+             let sub_res = aux ps in
+             List.map (fun p -> (rel, i)::p) sub_res) subps))) subps
   and aux = function
     | Empty -> []
     | Here -> [[]]

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-07-19 15:20:56 UTC (rev 1516)
+++ trunk/Toss/GGP/GDL.mli	2011-07-26 19:50:54 UTC (rev 1517)
@@ -5,34 +5,16 @@
 val aggregate_drop_negative : bool ref
 val aggregate_fixpoint : bool ref
 
-(** Expand static relations that do not have ground facts and have
-    arity above the threshold. *)
-val expand_arity_above : int ref
+(** {3 Datalog programs: Type definitions and saturation.} *)
 
-(** Treat "next" clauses which introduce metavariables only for
-    variable-variable mismatch, as non-erasing frame clauses (to be
-    ignored). ("Wave" refers to the process of "propagating the frame
-    condition" that these clauses are assumed to do, if
-    [nonerasing_frame_wave] is set to [true].) *)
-val nonerasing_frame_wave : bool ref
-
 type term =
   | Const of string
   | Var of string
-  | Func of string * term list
+  | Func of string * term array
 
-type rel_atom = string * term list
-(** Positive and negative literals separated, disjunctions expanded-out. *)
-type gdl_rule = rel_atom * rel_atom list * rel_atom list
-(** Collect rules by relations. *)
-type def_branch = term list * rel_atom list * rel_atom list
-type gdl_defs = (string * def_branch list) list
-
-module Terms : Set.S with type elt = term
-module Atoms : Set.S with type elt = rel_atom
-
+type rel_atom = string * term array
 type atom =
-  | Distinct of term list
+  | Distinct of term array
   | Rel of rel_atom
   | Role of term
   | True of term
@@ -43,8 +25,19 @@
   | Neg of atom
   | Disj of literal list
 
+(** Positive and negative literals separated, disjunctions expanded-out. *)
+type gdl_rule = rel_atom * rel_atom list * rel_atom list
+(** 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 *)
@@ -53,67 +46,102 @@
   | Stop of string * term list
   (** game ends here: match id, actions on previous step *)
 
-val term_str : term -> string
-val terms_str : term list -> string
-val sb_str : (string * term) list -> string
-val rel_atom_str : rel_atom -> string
-val rel_atoms_str : rel_atom list -> string
-val def_str :
-  string * (term list * rel_atom list * rel_atom list) -> string
-val tuples_str : term list list -> string
-val proto_rel_str : string * string array -> string
 
-val gdl_rule_vars : gdl_rule -> Aux.Strings.t
-val gdl_rules_vars : gdl_rule list -> Aux.Strings.t
+val atoms_of_body : literal list -> atom list
+val rel_of_atom : atom -> rel_atom
 
-val branch_str : string -> def_branch -> string
+val term_vars : term -> Aux.Strings.t
+val clause_vars : clause -> Aux.Strings.t
 
-val func_graph : string -> term list -> term list list
+val defs_of_rules : gdl_rule list -> gdl_defs
+val rule_of_clause : clause -> gdl_rule
 
-val rules_of_clause : clause -> gdl_rule list
+val nnf_dnf : literal list -> literal list list
 
-val terms_vars : term list -> Aux.Strings.t
-val rels_vars : rel_atom list -> Aux.Strings.t
+type substitution = (string * term) list
 
+val unify : substitution -> term list -> term list -> substitution
+val unify_all : substitution -> term list -> substitution
+val subst : substitution -> term -> term
+val subst_rels : substitution -> rel_atom list -> rel_atom list
+val subst_clause : substitution -> clause -> clause
+
+(** {3 Transformations of GDL clauses: inlining, negation.} *)
+
+(** Expand branches of a definition inlining the provided definitions,
+    only expand positive literals. Iterate expansion to support
+    nesting of definitions. *)
+val expand_positive_lits : gdl_defs -> def_branch list -> def_branch list
+
+(** Form clause bodies whose disjunction is equivalent to the
+    negation of disjunction of given clause bodies. *)
+val negate_bodies : literal list list -> literal list list
+
+(** {3 GDL translation helpers.} *)
+
+val blank : term
+
 val term_to_name : ?nested:bool -> term -> string
-val term_vars : term -> Aux.Strings.t
 
-val compose_sb : (string * term) list -> (string * term) list ->
-  (string * term) list
+val state_terms : literal list -> term list
 
-val subst_one : string * term -> term -> term
-val subst : (string * term) list -> term -> term
-val subst_rel : (string * term) list -> rel_atom -> rel_atom
-val subst_rels : (string * term) list -> rel_atom list -> rel_atom list
-val subst_br : (string * term) list -> def_branch -> def_branch
 
-val defs_of_rules : gdl_rule list -> gdl_defs
+(** {3 GDL whole-game operations.}
 
-val unify :
-  (string * term) list -> term list -> term list -> (string * term) list
+    Aggregate playout, player-denoting variable elimination. *)
 
-val unifies : term -> term -> bool
+(** Partition relations into stable (not depending, even indirectly,
+    on "true") and remaining ones. *)
+val stable_rels : gdl_defs -> string list * string list
 
-val saturate : rel_atom list -> gdl_rule list -> rel_atom list
 
-val stratify : gdl_defs list -> gdl_defs -> gdl_defs list
-
+(** 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. *)
 val aggregate_playout :
   term array -> int -> gdl_rule list ->
-  gdl_rule list * gdl_rule list * (string * term list) list * 
-    term list * (term list list list * term list list)
+  gdl_rule list * gdl_rule list * 
+    rel_atom list * term list *
+    (term array list list * term list list)
 
-val find_cycle : term option list -> term option list
+(** {3 Paths and operations involving terms and paths.} *)
 
+(** [simult_subst ps s t] substitutes [s] at all [t] paths that belong
+    to the set [ps], returns $t[ps \ot s]$. *)
+val simult_subst : path_set -> term -> term -> term
 
-(** A path is a position in a tree together with labels on nodes from
-    the root to that position (but excluding the position). *)
-type path = (string * int) 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 map_paths : (path -> term -> 'a) -> path_set -> term -> 'a list
 
-(** A trie representing a set of paths. *)
-type path_set =
-  | Empty
-  | Here                              (** Singleton $\{\epsilon\}$. *)
-  | Below of (string * path_set array) list
-  | Here_and_below of (string * path_set array) list
-(* Subtries are in sorted order. *)
+(** Toss relations hold between subterms of GDL state terms: generate
+    Toss relation name. *)
+val rel_on_paths : string -> path list -> string
+
+(** Some Toss predicates are generated from a path and an expected
+    subterm at that path. *)
+val pred_on_path_subterm : path -> term -> string
+
+(** 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 term_paths : ?prefix_only:bool -> (term -> bool) -> term -> path_set
+
+(** 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 at_path : term -> path -> term
+
+(** The set of paths that merges two terms, the cardinality of this
+    set, and the size of the largest common subtree. *)
+val merge_terms : term -> term -> path_set * int * int
+
+(** 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 at_paths : ?fail_at_missing:bool -> path_set -> term -> term list
+
+val empty_path_set : path_set
+val paths_union : path_set -> path_set -> path_set
+
+(** List the paths in a set. *)
+val paths_to_list : path_set -> path list

Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml	2011-07-19 15:20:56 UTC (rev 1516)
+++ trunk/Toss/GGP/TranslateFormula.ml	2011-07-26 19:50:54 UTC (rev 1517)
@@ -3,12 +3,8 @@
 open GDL
 
 let rel_atoms body =
-  let rec aux = function
-    | Pos (Rel (rel, args)) -> [rel, args]
-    | Neg (Rel (rel, args)) -> [rel, args]
-    | Disj ls -> Aux.concat_map aux ls
-    | _ -> [] in
-  Aux.concat_map aux body
+  Aux.map_some (function Rel (rel, args) -> Some (rel, args)
+    | _ -> None) (atoms_of_body body)
 
 
 
@@ -22,33 +18,33 @@
   let aux conj =
     List.fold_right (fun lit acc -> match lit with
       | (Pos (True _) | Neg (True _)) as lit ->
-        List.map (fun conj -> Left lit::conj) acc
+        List.map (fun conj -> Aux.Left lit::conj) acc
       | Disj ls as lit ->
         if List.for_all (function Pos _ -> true | _ -> false) ls
           || List.for_all (function Neg _ -> true | _ -> false) ls
         then
-          List.map (fun conj -> Left lit::conj) acc
+          List.map (fun conj -> Aux.Left lit::conj) acc
         else
           Aux.concat_map (function
             | (Pos (True _) | Neg (True _)) as lit ->
-              List.map (fun conj -> Left lit::conj) acc
-            | lit -> List.map (fun conj -> Right lit::conj) acc
+              List.map (fun conj -> Aux.Left lit::conj) acc
+            | lit -> List.map (fun conj -> Aux.Right lit::conj) acc
           ) ls
-      | lit -> List.map (fun conj -> Right lit::conj) acc
+      | lit -> List.map (fun conj -> Aux.Right lit::conj) acc
     ) conj [[]] in
   let disj = Aux.concat_map aux disj in
   List.map (fun conj ->
-    let state_terms, other = Aux.split_choice conj in
+    let state_terms, other = Aux.partition_choice conj in
     let pos_terms, neg_terms =
       Aux.partition_map (function
-        | Pos _ as lit -> Left lit
-        | Neg _ as lit -> Right lit
+        | Pos _ as lit -> Aux.Left lit
+        | Neg _ as lit -> Aux.Right lit
         | Disj ls as lit
             when List.for_all (function Pos _ -> true | _ -> false) ls
-              -> Left lit
+              -> Aux.Left lit
         | Disj ls as lit
             when List.for_all (function Neg _ -> true | _ -> false) ls
-              -> Right lit
+              -> Aux.Right lit
         | _ -> assert false
       ) state_terms in
     other, pos_terms, neg_terms) disj
@@ -72,7 +68,7 @@
   simult_subst data.f_paths blank t
 
 let var_of_term data t =
-  Formula.fo_var_of_string (blank_out data t)
+  Formula.fo_var_of_string (term_to_name (blank_out data t))
 
 let blank_outside_subterm data path subterm =
   let arities = data.term_arities in
@@ -84,7 +80,8 @@
     path subterm
 
 let var_of_subterm data path subt =
-  Formula.fo_var_of_string (blank_outside_subterm data path t)
+  Formula.fo_var_of_string
+    (term_to_name (blank_outside_subterm data path subt))
 
 (* placeholder *)
 let translate_defrel =
@@ -92,18 +89,20 @@
     assert false)
 
 let transl_rels data rels_phi sterms_all sterms_in =
-  let s_subterms = List.map
-    (fun sterm -> sterm,
-      map_paths (fun path subt -> subt, (sterm, path)) data.f_paths sterm)
+  (* within-mask subterms to locate paths on which to generate relations *)
+  let s_subterms = Aux.concat_map
+    (fun sterm ->
+      map_paths (fun path subt -> subt, (sterm, path)) data.m_paths sterm)
     sterms_all in
   let s_subterms = List.filter
     (fun (subt, _) -> subt <> blank) s_subterms in
   let s_subterms = Aux.collect s_subterms in
   let transl_rel sign rel args =
     try
-      let stuples =
-        List.map (fun arg -> List.assoc arg s_subterms) args in
-      let stuples = Aux.product stuples in
+      let (stuples : (GDL.term * GDL.path) list list) =
+        List.map (fun arg -> List.assoc arg s_subterms)
+          (Array.to_list args) in
+      let (stuples : (GDL.term * GDL.path) list list) = Aux.product stuples in
       let stuples = List.filter
         (fun stup ->
           List.exists (fun (sterm,_) -> List.mem sterm sterms_in) stup)
@@ -113,14 +112,15 @@
           let vartup = List.map (fun (sterm,_) ->
             var_of_term data sterm) stup in
           let fact_rel = rel_on_paths rel (List.map snd stup) in
-          Formula.Rel (fact_rel, vartup)) stuples in
+          Formula.Rel (fact_rel, Array.of_list vartup)) stuples in
       if sign then atoms
       else List.map (fun a -> Formula.Not a) atoms
     with Not_found -> [] in
   let transl_defrel sign rel args =
     if List.mem rel data.defined_rels
     then
-      !translate_defrel data sterms_all sterms_in s_subterms sign rel args
+      [!translate_defrel data sterms_all sterms_in
+          s_subterms sign rel args]
     else transl_rel false rel args in
   let rec aux = function
     | Pos (Rel (rel, args)) -> transl_defrel true rel args
@@ -128,7 +128,7 @@
     | Pos (Does _ | Role _) | Neg (Does _ | Role _) ->
       []
     | Disj lits ->
-      [Formula.Or (List.map (fun l -> [aux l]) lits)]
+      [Formula.Or (Aux.concat_map (fun l -> aux l) lits)]
     | _ -> assert false in           (* FIXME: what about Distinct? *)
   Formula.And (Aux.concat_map aux rels_phi)
 
@@ -149,15 +149,15 @@
         else None) data.mask_reps in
     Formula.And (anchor_and_fluent_preds @ mask_preds) in
   let rec aux = function
-    | Pos (True sterm) -> transl_sterm sterm
+    | Pos (True sterm) -> [transl_sterm sterm]
     | Neg (True sterm) -> assert false
     | Pos (Does _ | Role _) | Neg (Does _ | Role _) ->
       []
     | Disj lits ->
       [Formula.Or (Aux.map_some (fun l ->
         match aux l with
-          | [] -> None | [phi] -> phi
-          | conjs -> Formula.And conjs) lits)]
+          | [] -> None | [phi] -> Some phi
+          | conjs -> Some (Formula.And conjs)) lits)]
     | _ -> assert false in           (* FIXME: what about Distinct? *)
   Formula.And (Aux.concat_map aux phi)
   
@@ -172,22 +172,23 @@
   let neg_vars = List.map (var_of_term data) neg_terms in
   let all_terms = pos_terms @ neg_terms in
   let phi_vars = clause_vars
-    (("", []),
+    (("", [| |]),
      rels_phi @ pos_state_phi @ neg_state_phi) in
   let eqs = 
-    List.map (fun v -> Pos (Rel ("EQ_", [v; v]))) phi_vars in
+    List.map (fun v -> Pos (Rel ("EQ_", [|Var v; Var v|])))
+      (Aux.Strings.elements phi_vars) in
   let rels_eqs = rels_phi @ eqs in
   let negated_neg_state_transl =
     (* negation-normal-form of "not neg_state_phi" *)
     Formula.Or (
-      List.map (tranls_state data) (nnf_dnf neg_state_phi)) in
-  Formula.Ex (pos_vars,
+      List.map (transl_state data) (nnf_dnf neg_state_phi)) in
+  Formula.Ex ((pos_vars :> Formula.var list),
               Formula.And [
                 ext_phi;
                 transl_rels data rels_eqs pos_terms pos_terms;
                 transl_state data pos_state_phi;
                 Formula.Not (
-                  Formula.Ex (neg_vars,
+                  Formula.Ex ((neg_vars :> Formula.var list),
                               Formula.And [
                                 transl_rels data rels_eqs all_terms pos_terms;
                                 negated_neg_state_transl]))])
@@ -206,51 +207,59 @@
 (* {3 Build and use defined relations.} *)
 
 let build_defrels data clauses =
+  (* let data = !data_ref in *)
   let all_branches = Aux.concat_map
     (fun ((rel,args),body) ->
-      List.map (fun phi -> rel, (args, phi)) separate_disj [body])
+      List.map (fun phi -> rel, (args, phi)) (separate_disj [body]))
     clauses in
   let build_defrel rel =
     (* searching for ArgType = DefSide,S,p *)
     let branches = Aux.assoc_all rel all_branches in
-    (* first find the paths, we will find the state terms later *)
+    (* first find the common paths, we will find the state terms later *)
     let branch_paths =
-      List.map (fun (args, body) ->
-        let sterms = state_terms body
-        and args = Array.of_list args in
+      List.map (fun (args, (_, sterms_pos, sterms_neg)) ->
+        let sterms = state_terms (sterms_pos @ sterms_neg) in
         Array.map (fun arg ->
           Aux.concat_map (fun sterm ->
-            term_paths (fun subt -> subt = arg) data.m_paths sterm
+            Aux.map_some (fun x->x)
+              (map_paths (fun p subt ->
+                if subt = arg then Some p else None) data.m_paths sterm)
           ) sterms) args
       ) branches in
     let p_defside = List.fold_left
-      (Aux.array_map2 Aux.list_inter) branch_sterms in
+      (Aux.array_map2 Aux.list_inter)
+      (List.hd branch_paths) (List.tl branch_paths) in
     let p_defside = Array.map
       (function path::_ -> Some path | [] -> None) p_defside in
     (* now find the mapping $\calS_i$ for the DefSide result *)
-    let branch_sterms (args, phi) =
-      let sterms = state_terms phi in
+    let branch_sterms (args, (_, sterms_pos, sterms_neg)) =
+      let sterms = state_terms (sterms_pos @ sterms_neg) in
       Aux.array_map2
         (fun arg -> function None -> None
           | Some path ->
             Some (List.find (fun sterm ->
-              List.mem path
-                (term_paths (fun subt -> subt = arg)
-                   data.m_paths sterm)) sterms))
+              List.mem (Some path)
+                (map_paths (fun p subt ->
+                  if subt = arg then Some p else None) data.m_paths sterm)
+            ) sterms))
         args p_defside in
     let s_defside = List.map branch_sterms branches in
     (* now computing the ArgType(R,i) = CallSide,p variant *)
     let call_branches = Aux.concat_map
-      (fun (_,(_, phi)) ->
+      (fun (_,(_, (phi, _, _ as body))) ->
         let calls = Aux.assoc_all rel (rel_atoms phi) in
-        List.map (fun args -> args, phi) calls
+        List.map (fun args -> args, body) calls
       ) all_branches in
     let callside_for_arg i =
       let call_paths = Aux.concat_map
-        (fun (args, phi) ->
-          let sterms = state_terms phi and subt = args.(i) in
-          let paths =
-            term_paths (fun subt -> subt = arg) data.m_paths sterm in
+        (fun (args, (_, sterms_pos, sterms_neg)) ->
+          let sterms = state_terms (sterms_pos @ sterms_neg)
+          and arg = args.(i) in
+          let paths = Aux.concat_map (fun sterm ->
+            Aux.map_some (fun x->x)
+              (map_paths (fun p subt ->
+                if subt = arg then Some p else None) data.m_paths sterm)
+          ) sterms in
           List.map (fun p -> p, ()) paths
         ) call_branches in
       let call_paths = List.map
@@ -264,7 +273,7 @@
       (fun i ->
         function Some _ -> None | None -> callside_for_arg i)
       p_defside in
-    let arg_paths = Array.map2
+    let arg_paths = Aux.array_map2
       (fun defside callside ->
         match defside, callside with
           | Some p, _ | None, Some p -> p
@@ -279,7 +288,11 @@
         (fun i v ->
           let in_I = p_defside.(i) <> None in
           if in_I
-          then Formula.Eq (v, s_defside.(i))
+          then
+            let s_i = match s_defside.(i) with
+              | Some s -> var_of_term data s
+              | None -> assert false in
+            Formula.Eq (v, s_i)
           else Formula.Eq (v,
             var_of_subterm data arg_paths.(i) args.(i)))
         defvars in
@@ -290,32 +303,34 @@
             | Some path ->
               Some (blank_outside_subterm data path args.(i)))
           p_defside in
+      (* packing sterms back as a formula *)
       let callside_sterms = Array.to_list
-        (Array.map (fun sterm -> True sterm) callside_sterms) in
+        (Array.map (fun sterm -> Pos (True sterm)) callside_sterms) in
       transl_disjunct data rels_phi
         (callside_sterms @ pos_state) neg_state arg_eqs in
     let def_disjuncts = List.map2 defbody branches s_defside in
-    let defrel_arg_type = Array.map2
+    let defrel_arg_type = Aux.array_map2
       (fun defside path -> defside <> None, path)
       p_defside arg_paths  in
     data.defrel_arg_type :=
-      (rel, defrel_arg_type) :: !data.defrel_arg_type;
+      (rel, defrel_arg_type) :: !(data.defrel_arg_type);
     rel, (defvars, Formula.Or def_disjuncts) in
   List.map build_defrel data.defined_rels
 
+
 let transl_defrel data sterms_all sterms_in s_subterms sign rel args =
-  let arg_type = List.assoc rel !data.defrel_arg_type in
+  let arg_type = List.assoc rel !(data.defrel_arg_type) in
   (* the $s \tpos_{p_{R,i}} = t_i$ state terms *)
   let arg_sterms = Array.mapi
     (fun i (defside, path) -> if defside then None else
         try Some (
-          List.find (fun s -> at_path path s = args.(i)) sterms_all)
+          List.find (fun s -> at_path s path = args.(i)) sterms_all)
         with Not_found -> None)
     arg_type in
   let var_args = Array.mapi
     (fun i (_, path) ->
       match arg_sterms.(i) with
-        | None -> var_of_subterm data path arg (* in J *)
+        | None -> var_of_subterm data path args.(i) (* in J *)
         | Some sterm -> var_of_term data sterm)
     arg_type in
   let defrel_phi = Formula.Rel (rel, var_args) in
@@ -329,13 +344,14 @@
   let in_J_eq_transl i (_,path) =
     if arg_sterms.(i) = None
     then
-      let eq_phi = [Pos (Rel ("EQ_", [args.(i); args.(i)]))] in
+      let eq_phi = [Pos (Rel ("EQ_", [|args.(i); args.(i)|]))] in
       let v = blank_outside_subterm data path args.(i) in
       Some (transl_rels data eq_phi (v::sterms_all) [v])
     else None in
   let eqs_phi = Array.to_list
     (Aux.array_mapi_some in_J_eq_transl arg_type) in
-  Formula.Ex (ex_vars, Formula.And (defrel_phi::eqs_phi))
+  Formula.Ex ((ex_vars :> Formula.var list),
+              Formula.And (defrel_phi::eqs_phi))
 
 let _ = translate_defrel := transl_defrel
 

Modified: trunk/Toss/GGP/TranslateFormula.mli
===================================================================
--- trunk/Toss/GGP/TranslateFormula.mli	2011-07-19 15:20:56 UTC (rev 1516)
+++ trunk/Toss/GGP/TranslateFormula.mli	2011-07-26 19:50:54 UTC (rev 1517)
@@ -1,17 +1,17 @@
+(* Whether $i$th argument is a $\mathrm{DefSide}$ or a
+   $\mathrm{CallSide}$, and the $p_{R,i}$ path for a relation $R$. *)
+type defrel_arg_type = (bool * GDL.path) array
 
 type transl_data = {
-  f_paths : path_set;                   (* fluent paths *)
-  m_paths : path_set;                   (* within-mask paths *)
-  all_paths : path_set;                 (* sum of f_paths and m_paths *)
-  mask_reps : term list;                (* mask terms *)
+  f_paths : GDL.path_set;             (** fluent paths *)
+  m_paths : GDL.path_set;             (** within-mask paths *)
+  all_paths : GDL.path_set;          (** sum of f_paths and m_paths *)
+  mask_reps : GDL.term list;         (** mask terms *)
   defined_rels : string list;
   defrel_arg_type : (string * defrel_arg_type) list ref;
-  (* late binding to store $ArgType# data *)
+  (** late binding to store $ArgType$ data *)
   term_arities : (string * int) list;
 }
 
 val translate :
   transl_data -> GDL.literal list list -> Formula.formula
-
-val build_defrels :
-  transl_data -> clause list -> (string * (string list * formula)) list

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-07-19 15:20:56 UTC (rev 1516)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-07-26 19:50:54 UTC (rev 1517)
@@ -31,13 +31,14 @@
   precond : Formula.formula;
   (* the LHS match condition (the LHS structure and the precondition) *)
   rhs_add : (string * string array) list;
+  struc_elems : string list;
   (* the elements of LHS/RHS structures, corresponding to the "next"
      terms *)
-  struc_elems : string list;
-  fixvar_elemvars : (string * (term * path)) list;
-  (* "state" terms indexed by variables that they contain, together
-     with the path to the variable *)
-  elemvars : term Aux.StrMap.t;
+  fixvar_terms : (string * (term * path) list) list;
+  (* "state" terms indexed by GDL variables that they contain, together
+     with the path to the variable; in [(term * path) list], terms
+     can repeat *)
+  rulevar_terms : term Aux.StrMap.t;
 (* "state" terms indexed by Toss variable names they generate *)
 }
 
@@ -57,6 +58,10 @@
   playing_as : int;
   (* "active" player *)
   is_concurrent : bool;
+  transl_data : TranslateFormula.transl_data;
+  (* mostly the same data as above, but packed for formula translation *)
+  element_terms : term Aux.IntMap.t;
+  (* term representatives of structure elements *)
 }
 
 (* [most_similar c ts] finds a term from [ts] most similar to [c], and
@@ -93,7 +98,7 @@
    (as in definition of $\calP_f$). *)
 let fluent_paths_and_frames clauses =
   let defs =
-    defs_of_rules (Aux.concat_map rules_of_clause clauses) in
+    defs_of_rules (List.map rule_of_clause clauses) in
   let stable, nonstable = stable_rels defs in
   let inline_defs =
     List.filter (fun (rel,_) -> List.mem rel nonstable) defs in
@@ -106,19 +111,25 @@
     List.filter (fun ((rel,_),_) -> rel="next") clauses in
   let next_e =
     List.map (fun c ->
-      c, expand_positive_lits inline_defs [c]) next_clauses in
+      (* it should actually be a single element association *)
+      let brs_c =
+        List.assoc "next" (defs_of_rules [rule_of_clause c]) in
+      c, expand_positive_lits inline_defs brs_c) next_clauses in
   let find_br_fluents s_C (_,body,neg_body) =
-    let p_ts = Aux.assoc_all "true" body in
-    let n_ts = Aux.assoc_all "true" neg_body in
-    let t_C, ps = most_similar t_C (p_ts @ n_ts) in
+    let true_args body = List.map
+      (function [|t|] -> t | _ -> assert false)
+      (Aux.assoc_all "true" body) in
+    let p_ts = true_args body in
+    let n_ts = true_args neg_body in
+    let t_C, ps = most_similar s_C (p_ts @ n_ts) in
     (* "negative true" check *)
     t_C, ps, List.mem t_C p_ts in
   let is_frame s_C (t_C, _, neg_true) =
     not neg_true && s_C = t_C in
   let find_fluents (c, c_e) =
-    let s_C = snd (fst c) in
+    let s_C = (snd (fst c)).(0) in
     let res = List.map (find_br_fluents s_C) c_e in
-    if List.for_all is_frame res
+    if List.for_all (is_frame s_C) res
     then Aux.Left c
     else
       let f_paths =
@@ -127,17 +138,17 @@
           then
             term_paths (function Const _ -> true | _ -> false) t_C
           else ps) res in
-      Aux.Right (c, List.fold_left paths_union GDL.Empty f_paths) in
+      Aux.Right (c, List.fold_left paths_union empty_path_set f_paths) in
   let res = Aux.map_try find_fluents next_e in
   let frames, fluents = Aux.partition_choice res in
   let move_clauses, f_paths = List.split fluents in
   frames, move_clauses,
-  List.fold_left paths_union GDL.Empty f_paths
+  List.fold_left paths_union empty_path_set f_paths
 
 
 let rec contains_blank = function
   | Const "_BLANK_" -> true
-  | Func args -> Aux.array_existsi (fun _ -> contains_blank) args
+  | Func (f,args) -> Aux.array_existsi (fun _ -> contains_blank) args
   | _ -> false
 
 
@@ -146,12 +157,18 @@
 let create_init_struc clauses =
   let players =
     Aux.map_some (function
-      | ("role", [player]), _ -> Some player
+      | ("role", [|player|]), _ -> Some player
       | _ -> None
     ) clauses in
-  let stable_rels, nonstable_rels,
+  let players = Array.of_list players in
+  let rules = List.map rule_of_clause clauses in
+  let stable_rel_defs, nonstable_rel_defs,
     stable_base, init_state, (agg_actions, agg_states) =
     aggregate_playout players !agg_playout_horizon rules in
+  let stable_rels = Aux.unique_sorted
+    (List.map (fun ((rel,_),_,_)->rel) stable_rel_defs) in
+  let nonstable_rels = Aux.unique_sorted
+    (List.map (fun ((rel,_),_,_)->rel) nonstable_rel_defs) in
   let frame_clauses, move_clauses, f_paths =
     fluent_paths_and_frames clauses in
   let next_clauses =
@@ -161,7 +178,7 @@
   let arities =
     ("EQ_", 2)::
       Aux.unique_sorted
-      (List.map (fun ((rel, args),_) -> rel, List.length args)
+      (List.map (fun ((rel, args),_) -> rel, Array.length args)
          clauses) in
   let element_terms =
     List.fold_left (fun acc st -> Aux.unique_sorted (st @ acc)) []
@@ -170,9 +187,9 @@
     Aux.unique_sorted (List.map (fun t ->
       simult_subst f_paths blank t) element_terms) in
   let m_paths = List.map
-    (term_paths ~prefix_only:true (neg contains_blank)) element_reps in
+    (term_paths ~prefix_only:true (Aux.neg contains_blank)) element_reps in
   let m_paths =
-    List.fold_left paths_union GDL.Empty m_paths in
+    List.fold_left paths_union empty_path_set m_paths in
   let mask_reps =
     Aux.unique_sorted (List.map (fun t ->
       simult_subst m_paths blank t) element_reps) in
@@ -185,36 +202,35 @@
   let struc_rels = "EQ_"::struc_rels in
   let defined_rels = defined_rels @ nonstable_rels in
   let elem_term_map = Aux.strmap_of_assoc
-    (List.map (fun e -> name_of_term e, e) elem_reps) in
+    (List.map (fun e -> term_to_name e, e) element_reps) in
   let struc =
     List.fold_left (fun struc rel ->
       let arity = List.assoc rel arities in
-      let elem_tups = Aux.all_ntuples elem_reps arity in
+      let elem_tups = Aux.all_ntuples element_reps arity in
       let path_tups = Aux.all_ntuples m_pathl arity in
-      List.fold_left (fun ptup ->
+      List.fold_left (fun struc ptup ->
         let fact_rel = rel_on_paths rel ptup in
-        Aux.fold_left_try (fun etup ->
-          let tup = List.map2 at_path etup ptup in
-          if rel = "EQ_" && arity = 2 &&
-            List.hd tup = List.hd (List.tl tup)
+        Aux.fold_left_try (fun struc etup ->
+          let tup = Array.of_list (List.map2 at_path etup ptup) in
+          if rel = "EQ_" && arity = 2 && tup.(0) = tup.(1)
             || List.mem (rel, tup) stable_base
           then
             Structure.add_rel_named_elems struc fact_rel
-              (Aux.array_map_of_list name_of_term tup)
+              (Array.map term_to_name tup)
           else struc
         ) struc elem_tups
       ) struc path_tups
-    ) (Structure.empty ()) struc_rels in
+    ) (Structure.empty_structure ()) struc_rels in
   (* adding anchor and fluent predicates *)
   let add_pred rels struc paths elements =
-    List.fold_left (fun path ->
-      Aux.fold_left_try (fun elem ->
+    List.fold_left (fun struc path ->
+      Aux.fold_left_try (fun struc elem ->
         let pred =
           pred_on_path_subterm path (at_path elem path) in
         rels := pred :: !rels;
         let tup = [|elem|] in
         Structure.add_rel_named_elems struc pred
-          (Aux.array_map_of_list name_of_term tup)
+          (Array.map term_to_name tup)
       ) struc elements
     ) struc paths in
   let stable_rels = ref [] in
@@ -231,10 +247,10 @@
         then (
           stable_rels := pred :: !stable_rels;
           Structure.add_rel_named_elems struc pred
-            [|name_of_term elem|])
+            [|term_to_name elem|])
         else struc
       ) struc element_reps
-    ) struc maks_reps in
+    ) struc mask_reps in
   next_clauses, f_paths, m_paths, mask_reps, defined_rels,
   !stable_rels, !fluents,
   stable_base, init_state, struc, agg_actions, elem_term_map
@@ -250,12 +266,13 @@
   let fresh_x_f () =
     let x_f = Aux.not_conflicting_name !used_vars "x_f" in
     used_vars := Aux.Strings.add x_f !used_vars;
-    x_f in
-  let does_facts (_,body as cl) =
+    Var x_f in
+  let does_facts (_,body) =
     List.fold_right (fun p (sb, dis) ->
       let djs =
+        (* FIXME: check if "negative true" is properly handled *)
         Aux.map_some (function
-          | Does (dp, d) when dp = p -> Some d
+          | (Pos (Does (dp, d)) | Neg (Does (dp, d))) when dp = p -> Some d
           | _ -> None) body in
       let sb = unify_all sb djs in
       let d =
@@ -269,8 +286,9 @@
   let next_cls =
     if mode = `Environment
     then
-      List.map_some (fun (_,body as cl) ->
-        if List.mem (function Does _ -> true | _ -> false) body
+      Aux.map_some (fun (_,body as cl) ->
+        if List.exists
+          (function Pos (Does _) | Neg (Does _) -> true | _ -> false) body
         then None
         else Some (cl, [])
       ) next_cls
@@ -281,7 +299,7 @@
   (* selecting $\ol{\calC},\ol{\calN}$ clauses with
      $\sigma_{\ol{\calC},\ol{\calN}}$ applied *)
   let tup_unifies ts1 ts2 =
-    try unify [] ts1 ts2; true
+    try ignore (unify [] ts1 ts2); true
     with Not_found -> false in
   let move_clauses cs =
     (* bag of next clauses for each legal tuple *)
@@ -324,7 +342,7 @@
 
 
 let add_erasure_clauses (legal_tup, next_cls) =
-  let fixed_vars = terms_vars legal_tup in
+  (* let fixed_vars = terms_vars legal_tup in *)
   let frame_cls =
     Aux.map_some (fun (s, frame, body) ->
       if frame then Some (s, body) else None) next_cls in
@@ -359,7 +377,7 @@
   let frames = List.map maximality frames in
   let frames =
     List.map (fun (sb, s, bodies) ->
-      s, List.map (subst_rels sb) bodies) in
+      s, List.map (subst_rels sb) bodies) frames in
   let erasure_cls =
     Aux.concat_map (fun (s, bodies) ->
       let nbodies = negate_bodies bodies in
@@ -447,8 +465,9 @@
 
    The "concurrent games" case is handled specifically. Instead of
    rules for tuples of "legal" terms, rules for a single legal term
-   are built. The rules are partitioned among players. The first
-   player is the environment, [env_player]. *)
+   are built. The rules are partitioned among players. The last
+   player is the environment, [env_player] (this way, the numbering of
+   players can be the same as in turn-based case). *)
 let create_rule_cands is_turn_based used_vars next_cls clauses =
   let players = (* Array.of_list *)
     Aux.map_some (function
@@ -485,11 +504,12 @@
     let legal_tuples = List.map (fun cl -> [cl]) legal_cls in
     let move_tups =
       process_rule_cands `Concurrent [player] legal_tuples in
-    player, Aux.concat_map nonint_rule_cases (move_tups @ env_tups)
+    player, Aux.concat_map nonint_rule_cases (move_tups @ env_tups) in
   if is_concurrent then
     let env_tups =
       env_player, process_rule_cands `Environment [] [[]] in
-    Right (env_tups @ List.map2 concurrent_rule_cands players legal_by_player)
+    Right
+      (List.map2 concurrent_rule_cands players legal_by_player @ env_tups)
   else
     let legal_tuples = Aux.product legal_by_player in
     let move_tups = process_rule_cands `General players legal_tuples in
@@ -565,8 +585,6 @@
     (List.map (function Some p -> p | None -> players.(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
@@ -629,7 +647,7 @@
     struc_elem_terms in
   let elemvars = Aux.strmap_of_assoc
     (List.combine struc_elems struc_elem_terms) in
-  let fixvar_elemvars = List.map
+  let fixvar_terms = List.map
     (fun sterm -> map_paths
       (fun path -> function Var v -> v, (sterm, path)
         | _ -> assert false)
@@ -640,7 +658,7 @@
     precond = precond;
     rhs_add = rhs_add;
     struc_elems = struc_elems;
-    fixvar_elemvars = fixvar_elemvars;
+    fixvar_terms = fixvar_terms;
     elemvars = elemvars;
   } in
   ((rname, tossrule_data), label), (rname, rule)
@@ -651,7 +669,6 @@
   let rules = ref [] in
   let tossr_data = ref [] in
   let loc_n = Array.length loc_players in
-  let player_rules = Aux.collect player_rules in
   let graph = Array.mapi
     (fun loc player ->
       let player_num = List.assoc (term_to_name player) player_nums in
@@ -688,7 +705,7 @@
 let loc_graph_general_int =
   failwith "GDL: General Interaction Games not implemented yet"
 
-(* Remember that "environment" is the 0th player -- also in payoffs
+(* Remember that "environment" is the last player -- also in payoffs
    list. [rule_cands] is a player-indexed array. [players] are all
    player terms, excluding "environment". *)
 let loc_graph_concurrent players
@@ -727,7 +744,7 @@
     (fun pl_num (pl, p_rules) ->
       let p_rules = List.map
         (fun rcand ->
-          if pl_num = 0 then            (* environment *)
+          if pl_num = num_players then  (* environment *)
             build_rule struc fluents all_players_precond [] rcand
           else
             build_rule struc fluents [] (player_marker pl) rcand)
@@ -798,7 +815,7 @@
           cands, struc
       | None, Left cands ->
         loc_graph_general_int
-      | None, Right cands
+      | None, Right cands ->
         let build_rule =
           build_toss_rule transl_data rule_names in
         loc_graph_concurrent players player_payoffs struc build_rule
@@ -832,70 +849,74 @@
 (* ************************************************************ *)
 (** {3 Translating Moves.} *)
 
-(* The common part between turn-based and concurrent case --
-   translate a non-noop action. *)
-let translate_incoming_single_action gdl state action rname =
+(* The common part between turn-based and concurrent case -- translate
+   a non-noop action. [move] is the instance of a "legal" term,
+   performed by [player] (a number). Returns an option, since it can
+   be called for multiple candidate rules. *)
+let translate_incoming_single_action data rdata state player move rname =
+  let fixed_inst, _ =
+    unify [] [move] [rdata.legal_tuple.(player)] in
+  let anchors = Aux.concat_map (fun (v,t) ->
+    let state_terms = List.assoc v rdata.fixvar_terms in
+    Aux.concat_map
+      (fun (sterm, path) -> 
+        let pred = pred_on_path_subterm path t in
+        Formula.Rel (pred, [|TranslateFormula.var_of_term data sterm|]))
+      state_terms
+  ) fixed_inst in
+  let precond = Formula.And (anchors @ [rdata.precond]) in
+  (* {{{ log entry *)
 
+  if !debug_level > 2 then (
+    Printf.printf
+      "GDL.translate_incoming_move: rule=%s; trying precond=\n%s\n...%!"
+      rname (Formula.sprint precond)
+  );
+
+  (* }}} *)
+  let signat = Structure.rel_signature struc in
+  let rule =
+    DiscreteRule.translate_from_precond ~precond ~add:rdata.rhs_add
+      ~emb_rels:gdl.fluents ~signat ~struc_elems:rdata.struc_elems in
+  let lhs_struc = rule.DiscreteRule.lhs_struc in
+  let rule = DiscreteRule.compile_rule signat [] rule in
+  let asgns =
+    DiscreteRule.find_matchings struc rule in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf "found %s\n%!" (AssignmentSet.str asgns)
+  );
+  (* }}} *)
+  (* faster *)
+  (* let emb =
+     DiscreteRule.choose_match (snd state).Arena.struc rule asgns in *)
+  (* but we should check whether there's no ambiguity... *)
+  match
+    DiscreteRule.enumerate_matchings struc rule asgns
+  with
+    | [] -> None
+    | [emb] -> Some (rname, emb, lhs_struc)
+    | _ -> failwith
+      ("GDL.translate_incoming_move: match ambiguity for rule "^rname)
+
+
 let translate_incoming_move_turnbased gdl state actions noops =
   let loc = (snd state).Arena.cur_loc in
   let actions = Array.of_list actions in
   let location = (fst state).Arena.graph.(loc) in
-  let player_action = actions.(Aux.array_argfind (fun l -> l.Arena.moves <> []) 
-				 location) in
+  let loc_player =
+    Aux.array_argfind (fun l -> l.Arena.moves <> []) location in
+  let move = actions.(loc_player) in
   let struc = (snd state).Arena.struc in
   let tossrules =
     Aux.strmap_filter (fun  _ rdata ->
-      try ignore (match_meta [] [] [player_action] [rdata.legal_tuple.(loc_player)]); true
+      try ignore (match_meta [] [] [move]
+                    [rdata.legal_tuple.(loc_player)]); true
       with Not_found -> false
     ) gdl.tossrule_data in
   let candidates = Aux.map_so...
 
[truncated message content]