[Toss-devel-svn] SF.net SVN: toss:[1285] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1285] trunk/Toss
|
From: <luk...@us...> - 2011-01-29 00:22:20
|
Revision: 1285
http://toss.svn.sourceforge.net/toss/?rev=1285&view=rev
Author: lukstafi
Date: 2011-01-29 00:22:13 +0000 (Sat, 29 Jan 2011)
Log Message:
-----------
GDL translation work in progress: preparing GDL rules to be translated as Toss rules.
Modified Paths:
--------------
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/Formula/AuxTest.ml
trunk/Toss/Play/GDL.ml
trunk/Toss/Play/GDL.mli
trunk/Toss/Play/GDLTest.ml
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2011-01-23 21:35:16 UTC (rev 1284)
+++ trunk/Toss/Formula/Aux.ml 2011-01-29 00:22:13 UTC (rev 1285)
@@ -15,6 +15,10 @@
(c = '0') || (c = '1') || (c = '2') || (c = '3') || (c = '4') ||
(c = '5') || (c = '6') || (c = '7') || (c = '8') || (c = '9')
+let fst3 (a,_,_) = a
+let snd3 (_,a,_) = a
+let trd3 (_,_,a) = a
+
(* {2 Helper functions on lists and other functions lacking from the
standard library.} *)
let concat_map f l =
@@ -47,6 +51,17 @@
List.rev (List.map (fun (k,vs) -> k, List.fold_left redf red0 vs)
((k0,vs)::l))
+let collect l =
+ match List.sort (fun x y -> compare (fst x) (fst y)) l with
+ | [] -> []
+ | (k0, v0)::tl ->
+ let k0, vs, l = List.fold_left (fun (k0, vs, l) (kn, vn) ->
+ if k0 = kn then k0, vn::vs, l
+ else kn, [vn], (k0,List.rev vs)::l)
+ (k0, [v0], []) tl in
+ List.rev ((k0,List.rev vs)::l)
+
+
let list_remove v l = List.filter (fun w->v<>w) l
let rec rev_assoc l x = match l with
@@ -60,6 +75,13 @@
if b = x then aux (a::acc) l else aux acc l in
aux [] l
+let assoc_all x l =
+ let rec aux acc = function
+ | [] -> acc
+ | (a,b)::l ->
+ if a = x then aux (b::acc) l else aux acc l in
+ aux [] l
+
let rec replace_assoc k v = function
| [] -> [k, v]
| (a, b as pair) :: l ->
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2011-01-23 21:35:16 UTC (rev 1284)
+++ trunk/Toss/Formula/Aux.mli 2011-01-29 00:22:13 UTC (rev 1285)
@@ -9,6 +9,10 @@
val is_digit : char -> bool
+val fst3 : 'a * 'b * 'c -> 'a
+val snd3 : 'a * 'b * 'c -> 'b
+val trd3 : 'a * 'b * 'c -> 'c
+
(** {2 Helper functions on lists and other functions lacking from the
standard library.} *)
@@ -28,6 +32,10 @@
val map_reduce :
('a -> 'b * 'c) -> ('d -> 'c -> 'd) -> 'd -> 'a list -> ('b * 'd) list
+(** Collects elements by key. Same as
+ [map_reduce (fun x -> x) (fun y x->x::y) []]. *)
+val collect : ('a * 'b) list -> ('a * 'b list) list
+
(** Remove all elements equal to the argument, using structural
inequality. *)
val list_remove : 'a -> 'a list -> 'a list
@@ -40,6 +48,9 @@
value (using structural equality). Returns elements in reverse order. *)
val rev_assoc_all : ('a * 'b) list -> 'b -> 'a list
+(** Return all values of a key. *)
+val assoc_all : 'a -> ('a * 'b) list -> 'b list
+
(** Replace the value of a first occurrence of a key, or place it at
the end of the assoc list. *)
val replace_assoc : 'a -> 'b -> ('a * 'b) list -> ('a * 'b) list
Modified: trunk/Toss/Formula/AuxTest.ml
===================================================================
--- trunk/Toss/Formula/AuxTest.ml 2011-01-23 21:35:16 UTC (rev 1284)
+++ trunk/Toss/Formula/AuxTest.ml 2011-01-29 00:22:13 UTC (rev 1285)
@@ -4,6 +4,9 @@
let print_alist f l =
String.concat ", " (List.map (fun (k,v) -> k^": "^f v) l)
+let print_list f l =
+ "["^String.concat "; " (List.map f l)^"]"
+
let tests = "Aux" >::: [
"concat_map, map_some, array_map_some" >::
(fun () ->
@@ -26,7 +29,7 @@
(Aux.array_map_some f [|`A;`B;`C;`D|]);
);
- "map_reduce" >::
+ "map_reduce, collect" >::
(fun () ->
let mapf = function `A -> "1", ["a";"b"] | `B -> "2", ["c"]
| `C -> "1", [] | `D -> "2", ["d";"e"] in
@@ -39,6 +42,11 @@
["abra",3; "bra", 1; "cada",2]
(Aux.map_reduce (fun k->k,1) (+) 0
["abra"; "cada"; "abra"; "bra"; "cada"; "abra"]);
+
+ assert_equal ~msg:"collect"
+ ~printer:(print_alist (print_list string_of_int))
+ ["1",[2;3;2]; "2",[1;5;3]; "3",[7]]
+ (Aux.collect ["1",2;"1",3;"2",1;"2",5;"1",2;"3",7;"2",3])
);
"rev_assoc, rev_assoc_all" >::
@@ -205,6 +213,12 @@
["a";"c";"e";"b";"d"]
(Aux.unique (=) ["a";"c";"e"; "b"; "d"; "e"; "c"; "e"]);
+ assert_bool "not unique"
+ (Aux.not_unique ["a";"c";"b"; "d"; "c"]);
+
+ assert_bool "unique"
+ (not (Aux.not_unique ["a";"c";"b";"d"]));
+
assert_equal ~printer:(String.concat "; ")
~msg:"should remove duplicates"
["a";"b";"c";"d";"e"]
Modified: trunk/Toss/Play/GDL.ml
===================================================================
--- trunk/Toss/Play/GDL.ml 2011-01-23 21:35:16 UTC (rev 1284)
+++ trunk/Toss/Play/GDL.ml 2011-01-29 00:22:13 UTC (rev 1285)
@@ -38,7 +38,7 @@
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 additionally constant.
+ 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
@@ -111,19 +111,16 @@
over the tuple of subterms selected from the element terms by the
corresponding paths.
- (Relations that do not hold for any tuple of element terms in the
- whole aggregate playout can be removed.)
-
(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.) Collect all terms under "true" and
- "next" predicates in the game definition. For each mask-path
- pointing to a constant in some of the terms and that constant,
- introduce a new predicate with semantics: "matches the mask and
- has the constant at the path position".
+ (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
@@ -131,13 +128,12 @@
initial state. (Some relations introduced in this step might not
be fluents.)
- Collect all terms under "true" and "next" predicates in the game
- definition. For each 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
+ (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
@@ -202,77 +198,122 @@
(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 solely on the player in the location and in
- the "legal" definition (currently, we do not allow simultaneous
- moves). Consequently, we define rules on a per-player basis rather
- than a per-location basis. 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.
+ 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 branch of "legal" unifies with all (usually
- one, but we allow zero or more) occurrences of "does" with a
- single unifier per "next" branch. Split the unifiers into
- equivalence classes (w.r.t. substitution), each class will be a
- different rewrite rule (or set of rules). 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.
+ 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. We remember all variables
- in the "legal"/"does" instantiation as "fixed variables". We
- replace all occurrences of "does" with the body of the selected
- "legal" branch.
+ 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) We seggregate "next" atoms into these that contain some fixed
- variables or no variables at all, and other containing only
- unfixed variables. Eliminate unfixed variables from "next"
- atoms with fixed variables by enumerating their domains and
- duplicating whole "next" branches with each instantiation. (They
- will not have unfixed variables.)
+ (7d) Add all branches of equiv classes smaller than a given equiv
+ class to its branch set.
- (This perhaps could be done in a better way by better integrating
- (7d) and (7e)...)
+ 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) Branches with (only) unfixed variables in "next" atoms are
- the "frame" branches. Check that each "frame" branch is an
- identity: the "next" atom is equal to one of the positive "true"
- atoms. If not, expand all variables (as they are unfixed)
- duplicating that branch for each instantiation (the duplicated
- branches become regular branches -- with constant "next"
- atoms).
+ (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.
- (7e1) Transform the remaining proper "frame" branches into
- "erasure" branches: negate the body, push negation inside (using
- de Morgan laws etc.), reduce to DNF and 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.
+ (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.
- (7f) Introduce a new element variable for each class of "next" and
+ (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".)
+ 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)).
- (7g) 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).
-
- (7h) For all subterms of "next" and "true" atoms, identify the
+ (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 the result will be equivalent to a disjunction of
- negations of generated atoms.)
+ 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) Identify variables in "next" & "true" terms that are
+ (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
@@ -280,11 +321,13 @@
position). (Note that since branches do not have unfixed variables
anymore, we do not rename variables during duplication.)
- (7j) 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, see
- below). Build a pre-lattice of branch bodies w.r.t. subsumption,
+ (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"
@@ -296,12 +339,20 @@
necessary so that all applicable changes are applied in the
translated game when making a move).
- (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.)
+ (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.
- (7l) Include translated negation of the terminal condition.
+ (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
@@ -317,8 +368,8 @@
"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 (7f)-(7k), but treating "goal" branches separately -- when
- (7i) duplicates a branch, new branches add new sum elements.
+ using (7h)-(7m), but treating "goal" branches separately -- when
+ (7k) duplicates a branch, new branches add new sum elements.
*)
@@ -381,6 +432,20 @@
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
@@ -410,6 +475,13 @@
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
@@ -495,12 +567,6 @@
| stratum, rules -> stratify (stratum::strata) rules
-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 subst_one (x, term as sb) = function
| Var y when x=y -> term
| MVar y when x=y -> term
@@ -524,7 +590,7 @@
(List.map (subst_one sb1) terms1)
(List.map (subst_one sb1) terms2)
| (Var x::_, term::_ | term::_, Var x::_)
- when List.mem x (vars term) ->
+ 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
@@ -539,8 +605,9 @@
let rec match_meta sb m_sb terms1 terms2 =
match terms1, terms2 with
| [], [] -> sb, m_sb
- | (Const a | Var a)::terms1, (Const b | Var b)::terms2 when a=b ->
- match_meta sb m_sb terms1 terms2
+ | (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 ->
@@ -609,8 +676,19 @@
let subst_rel sb (rel, args) = rel, List.map (subst sb) args
let subst_rels sb body = List.map (subst_rel sb) body
-let compose_sb sb1 sb = Aux.map_prepend sb1 (fun (x,t)->x, subst sb1 t) sb
+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) ^")"
@@ -621,11 +699,11 @@
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) =
- let neg_facts_str negs =
- String.concat " "
- (List.map (fun d -> "(not (and "^facts_str d^"))") negs) in
String.concat "\n" (List.map (fun (args, body, neg_body) ->
"("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
" " ^ neg_facts_str neg_body ^ ")"
@@ -651,14 +729,16 @@
| head, cond1::body, neg_body ->
Aux.map_try (fun fact ->
(* {{{ log entry *)
- if !debug_level > 4 then (
+
+ 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 > 4 then (
+ if !debug_level > 5 then (
Printf.printf "instantiate_one: succeeded with %s\n%!"
(sb_str sb)
);
@@ -671,20 +751,22 @@
let rec inst_stratum old_base old_irules cur_base cur_irules =
(* {{{ log entry *)
- if !debug_level > 3 then (
+
+ 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 > 3 then (
+ if !debug_level > 4 then (
Printf.printf "inst_stratum: cur-cur = %s\n%!"
(facts_str new_base1)
);
@@ -692,7 +774,7 @@
let new_base2, new_irules2 =
Aux.partition_choice (instantiate_one base cur_base old_irules) in
(* {{{ log entry *)
- if !debug_level > 3 then (
+ if !debug_level > 4 then (
Printf.printf "inst_stratum: cur-old = %s\n%!"
(facts_str new_base2)
);
@@ -700,7 +782,7 @@
let new_base3, new_irules3 =
Aux.partition_choice (instantiate_one base old_base cur_irules) in
(* {{{ log entry *)
- if !debug_level > 3 then (
+ if !debug_level > 4 then (
Printf.printf "inst_stratum: old-cur = %s\n%!"
(facts_str new_base3)
);
@@ -740,32 +822,48 @@
(* 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 =
- let fresh_count = ref 0 in
- let map_branch (args, body, neg_body) =
- incr fresh_count;
- let rec map_vnames = function
- | Var x -> Var (x^string_of_int !fresh_count)
- | MVar x -> MVar (x^string_of_int !fresh_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 in
- List.map map_branch
+ 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 : exp_def_branch) : exp_def_branch 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) ->
@@ -774,7 +872,7 @@
Some (
subst_rels sb1 (dbody @ pos_sol),
List.map (subst_rels sb1) (dneg_body @ neg_sol),
- compose_sb sb1 sb)
+ extend_sb sb1 sb)
with Not_found -> None
) def
) sols
@@ -823,70 +921,40 @@
loop (base @ step) strata in
match stratify ~def:true [] (defs_of_rules rules) with
| [] -> []
- | [no_defined_rels] ->
- if more_defs = [] then no_defined_rels
- else List.map (fun (rel, branches) ->
- rel, Aux.concat_map (subst_def_branch more_defs) branches)
- no_defined_rels
- | def_base::def_strata -> loop def_base def_strata
+ | [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. *)
- (*
-let subst_legal_rule (legal_defs : exp_def_branch list)
- (head, body, neg_body : exp_def_branch) : exp_def_branch list =
- (* 6a *)
- let sols =
- List.fold_left (fun sols (rel, args as atom) ->
- (let try def =
- freshen_def_branches (List.assoc rel defs) in
- 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),
- compose_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
- *)
+(* 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
@@ -946,17 +1014,21 @@
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
@@ -976,7 +1048,8 @@
(String.concat " " (List.map term_str init_state))
);
(* }}} *)
- static_rules, dynamic_rules, static_base, loop [] [] 0 init_state
+ static_rules, dynamic_rules, static_base, init_state,
+ loop [] [] 0 init_state
let find_cycle cands =
@@ -1000,13 +1073,49 @@
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, (agg_actions, agg_states) =
+ 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
@@ -1022,7 +1131,8 @@
(* 2a *)
List.map (function
| player, [Const _ as noop] -> player, Some noop
- | player, _ -> player, None) actions) agg_actions in
+ | player, _ -> player, None) actions
+ ) agg_actions in
let control_cands = List.map (fun noop_cands ->
List.fold_left (fun accu -> function
| player, None ->
@@ -1032,15 +1142,59 @@
("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 cycle = find_cycle control_cands in
+ 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") cycle))
+ (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), _, _) ->
@@ -1049,10 +1203,12 @@
| _ -> 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 =
@@ -1076,10 +1232,12 @@
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
@@ -1110,11 +1268,8 @@
(String.concat " " (List.map term_str masks))
);
(* }}} *)
- let cmp_masks t1 t2 =
- Printf.printf "cmp_masks: %s <= %s .. " (term_str t1) (term_str t2);
- try ignore (match_meta [] [] [t1] [t2]); Printf.printf "true\n%!"; true
- with Not_found -> Printf.printf "false\n%!"; false in
- let masks = Aux.maximal cmp_masks masks in
+ (* 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%!"
@@ -1167,72 +1322,75 @@
let mask_paths = Aux.concat_map (function _, [] -> assert false
| mask, (sb,_)::_ -> List.map (fun (v,_)->mask, v) sb) elements in
(* 4a *)
- (* TODO: move generation of static rels graphs to the end and
- filter to only generate used relations *)
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,
+ rel, List.length args,
Aux.all_tuples_for args mask_paths) static_rels in
- let static_base =
- Aux.map_reduce (fun x->x) (fun x y->y::x) [] static_base 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, 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
+ 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 > 1 then (
- Printf.printf "static-rel: %s, of... %!" rname;
+ 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);
);
(* }}} *)
- 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
+ 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
@@ -1255,53 +1413,553 @@
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);
- );
- (* }}} *)
- let res = Structure.unsafe_add_rels struc rname elem_tups in
- (* {{{ log entry *)
- if !debug_level > 1 then (
- Printf.printf " done\n%!";
- );
- (* }}} *)
- res
+ (* {{{ 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 mask_paths in
- (* 4c: TODO -- see laziness TODO 4 *)
- (* 5: TODO *)
+ (* 4c *)
+ let struc = List.fold_left (fun struc mask ->
+ let rname = term_to_name mask in
+ let struc =
+ Structure.add_rel_name rname 1 struc in
+ let elems = List.assoc mask elements in
+ (* {{{ log entry *)
+ if !debug_level > 0 then (
+ Printf.printf "Adding mask anchor predicate %s over %d elements.\n%!"
+ rname (List.length elems);
+ );
+ (* }}} *)
+ let elem_tups =
+ List.map (fun (sb, e) -> [|e|]) elems in
+ Structure.unsafe_add_rels struc rname elem_tups
+ ) struc masks in
+ let struc = List.fold_left (fun struc (mask, elems) ->
+ List.fold_left (fun struc (sb, elem) ->
+ List.fold_left (fun struc (v,t as v_sb) ->
+ let rname = term_to_name (subst_one v_sb mask) in
+ Structure.add_rel struc rname [|elem|]) struc sb) struc elems
+ ) struc elements in
+ (* 5 *)
+ let term_to_blank next_arg =
+ let mask_cands =
+ Aux.map_try (fun mask ->
+ mask, match_meta [] [] [next_arg] [mask]
+ ) masks in
+ let mask, sb, m_sb = match mask_cands with
+ | [mask, (sb, m_sb)] -> mask, sb, m_sb
+ | _ -> assert false in
+ mask, sb, m_sb, blank_out (next_arg, mask) in
+ let struc = List.fold_left (fun struc term ->
+ let mask, sb, m_sb, blanked = term_to_blank term in
+ let e =
+ let elems = List.assoc mask elements in
+ List.assoc sb elems in
+ List.fold_left (fun struc (v,t as v_sb) ->
+ let rname = term_to_name (subst_one v_sb mask) in
+ if List.mem term init_state then
+ Structure.add_rel struc rname [|e|]
+ else Structure.add_rel_name rname 1 struc) struc m_sb
+ ) struc element_terms in
+
(* 7a *)
let legal_rules =
Aux.concat_map (function [Const _; _], _, _ as lrule -> [lrule]
| [Var v; lterm], body, neg_body ->
Array.to_list
- (Array.map (fun player -> [player; lterm], body, neg_body)
+ (Array.map (fun player ->
+ let sb = [v, player] in
+ [player; subst sb lterm],
+ List.map (subst_rel sb) body,
+ List.map (List.map (subst_rel sb)) neg_body)
player_terms)
| [Func _; lterm], _, _ ->
(* TODO: easy to fix *)
failwith "GDL.translate_game: bigger player terms not handled yet"
| _ -> assert false) legal_rules in
- (* indexed by players, then "legal" branches, then by MGUs for
- unifier equivalence classes *)
- (*
- let player_next =
- Aux.map_reduce (fun ()) in
- *)
+ (* expanded "next" branches indexed by locations, then "legal"
+ branches, then by MGUs for unifier equivalence classes *)
+ let loc_lead_legal, loc_noop_legal =
+ (* actions of the player *of the location* *)
+ let loc_lead_legal = Array.make loc_n [] in
+ (* noop actions in locations -- cannot have choice *)
+ let loc_noop_legal =
+ Array.make_matrix loc_n players_n None in
+ List.iter (function
+ | [player; action], _, _ as legal ->
+ for i=0 to loc_n - 1 do
+ if List.mem i (find_player_locs player)
+ then
+ if not (List.mem legal loc_lead_legal.(i))
+ then loc_lead_legal.(i) <- legal :: loc_lead_legal.(i);
+ for p=0 to players_n - 1 do
+ match loc_noops.(i).(p) with None -> ()
+ | Some noop ->
+ if p = find_player player && (
+ try ignore (match_meta [] [] [noop] [action]); true
+ with Not_found -> false)
+ then
+ if loc_noop_legal.(i).(p) <> None
+ && loc_noop_legal.(i).(p) <> Some legal
+ then (
+ Printf.printf "Multiple noops: %s, %s\n%!"
+ (term_str (Func ("legal", Aux.fst3 legal)))
+ (term_str (Func ("legal", Aux.fst3
+ (Aux.unsome loc_noop_legal.(i).(p)))));
+ assert false)
+ else loc_noop_legal.(i).(p) <- Some legal
+ done
+ done
+ | _ -> assert false
+ ) legal_rules;
+ loc_lead_legal, loc_noop_legal in
+ (* the joint actions available in a location *)
+ let loc_joint_legal =
+ Array.mapi (fun i lead ->
+ let cur_player = find_player loc_players.(i) in
+ let p_acts = Array.to_list
+ (Array.mapi
+ (fun p noop ->
+ if p = cur_player then lead
+ else match noop with
+ | Some noop -> [noop] | None -> assert false)
+ loc_noop_legal.(i)) in
+ Aux.product p_acts
+ ) loc_lead_legal in
+ (* 7b *)
+ let grtr ((lead1,_,_), _) ((lead2,_,_), _) = cmp_masks lead2 lead1 in
+ let loc_next_classes =
+ Array.mapi (fun loc joint_legal_branches ->
+ Aux.concat_map (fun joint_legal ->
+ let lead_legal, noop_legals =
+ List.partition (function
+ | [player; action],_,_ -> player=loc_players.(loc)
+ | _ -> assert false) joint_legal in
+ let lead_legal =
+ match lead_legal with [lead_legal] -> lead_legal
+ | _ -> assert false in
+ (* 7b1 *)
+ let noop_branches = Aux.concat_map (fun legal ->
+ Aux.map_some
+ (fun next_br ->
+ subst_legal_rule legal (freshen_branch next_br))
+ next_rules) noop_legals in
+ let noop_branches =
+ List.map snd noop_branches in
+ (* now, continue with the lead player *)
+ let unifs = Aux.map_some (* and substituted legal br-es *)
+ (fun next_br ->
+ match
+ subst_legal_rule lead_legal (freshen_branch next_br)
+ with None -> None
+ | Some (([_; lead],lead_body,lead_neg_body), br) ->
+ Some ((lead,lead_body,lead_neg_body), br)
+ | _ -> assert false)
+ next_rules in
+ (* building "Hasse layers" imperatively *)
+ let unifs = ref unifs in
+ let hasse_layer () =
+ let minimal = Aux.maximal grtr !unifs in
+ (* 7c *)
+ List.map (fun (min_head, _, _ as min_lead, _) ->
+ let branches =
+ Aux.map_try (fun ((head, _, _), br as lbr) ->
+ let renaming, _ =
+ match_meta [] [] [min_head] [head] in
+ unifs := Aux.list_remove lbr !unifs;
+ subst_br renaming br) !unifs in
+ min_lead, branches
+ ) minimal in
+ let layers = ref [] in
+ while !unifs <> [] do
+ layers := hasse_layer () :: !layers
+ done;
+ let layers = List.rev !layers in
+ (* 7d *)
+ let rules_brs = List.fold_left
+ (* folding reverses order so the maximal layer will
+ generate the returned classes *)
+ (fun rules_brs layer ->
+ List.map
+ (fun (new_lead, new_brs as nrule) ->
+ let smaller = List.filter (grtr nrule) rules_brs in
+ new_lead,
+ List.concat (new_brs::List.map snd smaller)
+ ) layer
+ ) [] layers in
+ (* 7b1 continued *)
+ let rules_brs = List.map (fun (lead, brs) ->
+ lead, noop_branches @ brs) rules_brs in
+ (* 7e -- TODO (together with non-maximal (7d) classes) *)
+ (* 7f *)
+ let rules_brs =
+ List.map (fun (lead_head, lead_body, lead_neg_body as lead,
+ branches) ->
+ let fixed_vars = term_vars lead_head in
+ let fixed_brs, other_brs = List.partition
+ (function
+ | [next_arg],_,_ ->
+ Aux.Strings.subset (term_vars next_arg) fixed_vars
+ | _ -> assert false) branches in
+ let frame_brs, to_expand = List.partition
+ (function
+ | [next_arg],_,_ ->
+ Aux.Strings.is_empty
+ (Aux.Strings.inter (term_vars next_arg) fixed_vars)
+ | _ -> assert false) other_brs in
+ (* 7f1 *)
+ let frame_brs, more_to_expand = List.partition
+ (fun (args, body, neg_body) ->
+ List.exists
+ (fun (rel, r_args) -> rel="true" && r_args=args) body
+ ) frame_brs in
+ let unfixed_brs =
+ to_expand @ more_to_expand in
+ if unfixed_brs <> [] then failwith
+ ("GDL.translate_game: parametric non-frame actions "^
+ "not implemented yet (7g):\n" ^
+ def_str ("action",unfixed_brs));
+ (* 7f2 *)
+ let leq3 (head1, _, _) (head2, _, _) =
+ try
+ let sb, _ = match_meta [] [] head2 head1 in
+ List.for_all (fun (v,_)->
+ not (Aux.Strings.mem v fixed_vars)) sb
+ with Not_found -> false in
+ let frames =
+ Aux.maximal leq3 frame_brs in
+ let frames =
+ List.map (fun repr ->
+ List.filter (fun cl->leq3 cl repr) frame_brs)
+ frames in
+ (* collect and rename multi-bodies *)
+ let frames = List.map (function
+ | [] -> assert false
+ | [head, body, neg_body] -> head, [body, neg_body]
+ | (head, body, neg_body)::f_brs ->
+ let multi_body = List.map
+ (fun (head2, body2, neg_body2) ->
+ let sb, _ = match_meta [] [] head head2 in
+ List.map (subst_rel sb) body2,
+ List.map (List.map (subst_rel sb)) neg_body2
+ ) f_brs in
+ head, (body, neg_body)::multi_body
+ ) frames in
+ (* 7f3 *)
+ let erasure_brs = Aux.concat_map
+ (function
+ | [next_arg] as next_args,multi_body ->
+ let mask, _, _, blank_arg = term_to_blank next_arg in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ Printf.printf "Blanking-out of %s by %s\n%!"
+ (term_str next_arg) (term_str mask)
+ );
+ (* }}} *)
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ Printf.printf "Frame multibody:\n%s\n%!"
+ ( String.concat "\n" (List.map (
+ fun (body, neg_body) ->
+ "("^ facts_str body ^
+ " " ^ neg_facts_str neg_body ^ ")"
+ ) multi_body))
+ );
+ (* }}} *)
+ let multi_body = List.map (fun (body, neg_body) ->
+ let body =
+ Aux.map_some (fun (rel, args) ->
+ if rel <> "role" &&
+ (rel <> "true" || args <> next_args)
+ then Some (Aux.Left (rel, args))
+ else None) body in
+ let neg_body =
+ List.map
+ (function
+ | ["distinct", []] -> assert false
+ | ["distinct", arg::more_args] ->
+ let _, sb =
+ List.fold_left (fun (base, sb) arg ->
+ let sb = unify sb [base] [arg] in
+ subst sb base, sb)
+ (arg, []) more_args in
+ (* inverting unfixed-to-fixed *)
+ let sb = List.map (function
+ | v1, Var v2
+ when Aux.Strings.mem v1 fixed_vars
+ -> v2, Var v1
+ | vsb -> vsb) sb in
+ Aux.Right (Aux.Right sb)
+ | conj when List.mem_assoc "distinct" conj ->
+ assert false
+ | conj ->
+ Aux.Right (Aux.Left conj))
+ neg_body in
+ body @ neg_body) multi_body in
+ let erasures = List.map Aux.partition_choice
+ (Aux.unique_sorted (Aux.product multi_body)) in
+ let erasures =
+ Aux.map_some (fun (neg_body, body) ->
+ try
+ let body, sbs = Aux.partition_choice body in
+ let body = List.concat body in
+ let sb = List.fold_left compose_sb [] sbs in
+ if List.exists (fun (v,_)->
+ Aux.Strings.mem v fixed_vars) sb
+ then None
+ else
+ let body = List.map (subst_rel sb) body in
+ let neg_body =
+ List.map (fun a -> [subst_rel sb a]) neg_body in
+ let head = subst sb blank_arg in
+ if
+ (* TODO: (7g) instead *)
+ Aux.Strings.subset (term_vars head)
+ fixed_vars &&
+ (* (7f4) *)
+ not (List.exists (fun pos ->
+ List.mem [pos] lead_neg_body
+ ) body) &&
+ not (List.exists (fun neg ->
+ List.for_all
+ (fun neg->List.mem neg lead_body) neg
+ ) neg_body)
+ then Some ([head], body, neg_body)
+ else None
+ with Not_found -> None) erasures in
+ let erasures = Aux.unique_sorted
+ (List.map (fun (head, body, neg_body) ->
+ head, Aux.unique_sorted body,
+ Aux.unique_sorted neg_body) erasures) in
+ erasures
+ (* TODO: (7g) *)
+ | _ -> assert false) frames in
+ (* TODO: (7f5) we ignore the possibility that "lead" is
+ instantiated by some of erasure substitutions, since
+ we already ignore non-maximal "legal" classes *)
+ lead, fixed_brs @ erasure_brs
+ ) rules_brs in
+ (* let rules_inds = Array.of_list rules_brs in *)
+ rules_brs
+ ) joint_legal_branches
+ ) loc_joint_legal in
+ (* {{{ log entry *)
+ if !debug_level > 1 then (
+ Array.iteri (fun loc rules_brs ->
+ Printf.printf "Rule precursors for loc %d:\n%!" loc;
+ List.iter (fun ((lead,_,_), brs) ->
+ Printf.printf "Rule-precursor: player %s move %s\n%s\n%!"
+ (term_str loc_players.(loc)) (term_str lead)
+ (def_str ("action", brs))
+ ) rules_brs;
+ ) loc_next_classes;
+ );
+ (* }}} *)
+ (* 7h *)
+ let toss_var term =
+ let mask, _, _, blank = term_to_blank term in
+ mask, Formula.fo_var_of_string (term_to_name blank) in
+ (* 7i *)
+ let state_terms =
+ Array.fold_left (fun acc rules_brs ->
+ List.fold_left (fun acc (lead, brs) ->
+ List.fold_left (fun acc -> function
+ | [next_arg], body, neg_body ->
+ let res =
+ ...
[truncated message content] |
