[Toss-devel-svn] SF.net SVN: toss:[1508] trunk/Toss/GGP
Status: Beta
Brought to you by:
lukaszkaiser
From: <luk...@us...> - 2011-07-09 12:37:40
|
Revision: 1508 http://toss.svn.sourceforge.net/toss/?rev=1508&view=rev Author: lukstafi Date: 2011-07-09 12:37:34 +0000 (Sat, 09 Jul 2011) Log Message: ----------- missing files in Reimplementation of GDL to Toss translation: untested work in progress. Added Paths: ----------- trunk/Toss/GGP/TranslateFormula.ml trunk/Toss/GGP/TranslateGame.ml Added: trunk/Toss/GGP/TranslateFormula.ml =================================================================== --- trunk/Toss/GGP/TranslateFormula.ml (rev 0) +++ trunk/Toss/GGP/TranslateFormula.ml 2011-07-09 12:37:34 UTC (rev 1508) @@ -0,0 +1,341 @@ +(** {2 Translating GDL definition: formulas.} *) + +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 + + + +(* **************************************** *) +(* {3 Translate stable relations and fluents.} *) + +(* [separate_disj] is $\mathrm{TrDistr}$. Separate each disjunct, + splitting disjuncts if necessary, into "positive state terms", + "negative state terms" and "reminder". *) +let separate_disj disj = + 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 + | 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 + 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 + ) ls + | lit -> List.map (fun conj -> 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 pos_terms, neg_terms = + Aux.partition_map (function + | Pos _ as lit -> Left lit + | Neg _ as lit -> Right lit + | Disj ls as lit + when List.for_all (function Pos _ -> true | _ -> false) ls + -> Left lit + | Disj ls as lit + when List.for_all (function Neg _ -> true | _ -> false) ls + -> Right lit + | _ -> assert false + ) state_terms in + other, pos_terms, neg_terms) disj + +(* 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 * 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 *) + defined_rels : string list; + defrel_arg_type : (string * defrel_arg_type) list ref; + (* late binding to store $ArgType# data *) + term_arities : (string * int) list; +} + +let blank_out data t = + simult_subst data.f_paths blank t + +let var_of_term data t = + Formula.fo_var_of_string (blank_out data t) + +let blank_outside_subterm data path subterm = + let arities = data.term_arities in + List.fold_right + (fun (rel, pos) acc -> + let subterms = Array.make (List.assoc rel arities) blank in + subterms.(pos) <- acc; + Func (rel, subterms)) + path subterm + +let var_of_subterm data path subt = + Formula.fo_var_of_string (blank_outside_subterm data path t) + +(* placeholder *) +let translate_defrel = + ref (fun data sterms_all sterms_in s_subterms sign rel args -> + 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) + 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 = List.filter + (fun stup -> + List.exists (fun (sterm,_) -> List.mem sterm sterms_in) stup) + stuples in + let atoms = List.map + (fun stup -> + 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 + 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 + else transl_rel false rel args in + let rec aux = function + | Pos (Rel (rel, args)) -> transl_defrel true rel args + | Neg (Rel (rel, args)) -> transl_defrel false rel args + | Pos (Does _ | Role _) | Neg (Does _ | Role _) -> + [] + | Disj lits -> + [Formula.Or (List.map (fun l -> [aux l]) lits)] + | _ -> assert false in (* FIXME: what about Distinct? *) + Formula.And (Aux.concat_map aux rels_phi) + +let transl_state data phi = + let transl_sterm sterm = + let s_subterms = + map_paths (fun path subt -> subt, path) data.all_paths sterm in + let s_subterms = List.filter + (fun (subt, _) -> subt <> blank) s_subterms in + let vartup = [|var_of_term data sterm|] in + let anchor_and_fluent_preds = + List.map (fun (subt, path) -> + Formula.Rel (pred_on_path_subterm path subt, vartup)) s_subterms in + let mask_preds = Aux.map_some + (fun mask -> + if mask = simult_subst data.all_paths blank sterm + then Some (Formula.Rel (term_to_name mask, vartup)) + 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 + | 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)] + | _ -> assert false in (* FIXME: what about Distinct? *) + Formula.And (Aux.concat_map aux phi) + + +(* [translate_disjunct] is $\mathrm{Tr}(\Phi_i,E)$, [rels_phi] is + $G_i$, [pos_state_phi] is $ST^{+}_i$, [neg_state_phi] is + $ST^{-}_i$, [ext_phi] is $E$. *) +let transl_disjunct data rels_phi pos_state_phi neg_state_phi ext_phi = + let pos_terms = state_terms pos_state_phi in + let pos_vars = List.map (var_of_term data) pos_terms in + let neg_terms = state_terms pos_state_phi in + 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 + 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, + 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.And [ + transl_rels data rels_eqs all_terms pos_terms; + negated_neg_state_transl]))]) + + + +(* Translate a disjunction of conjunctions of literals (and disjs of lits). *) +let translate data disj = + let disj = separate_disj disj in + Formula.Or (List.map (fun (rels_phi, pos_state, neg_state) -> + transl_disjunct data rels_phi pos_state neg_state (Formula.And []) + ) disj) + + +(* **************************************** *) +(* {3 Build and use defined relations.} *) + +let build_defrels data clauses = + let all_branches = Aux.concat_map + (fun ((rel,args),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 *) + let branch_paths = + List.map (fun (args, body) -> + let sterms = state_terms body + and args = Array.of_list args in + Array.map (fun arg -> + Aux.concat_map (fun sterm -> + term_paths (fun subt -> subt = arg) data.m_paths sterm + ) sterms) args + ) branches in + let p_defside = List.fold_left + (Aux.array_map2 Aux.list_inter) branch_sterms 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 + 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)) + 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)) -> + let calls = Aux.assoc_all rel (rel_atoms phi) in + List.map (fun args -> args, phi) 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 + List.map (fun p -> p, ()) paths + ) call_branches in + let call_paths = List.map + (fun (p, ns) -> List.length ns, p) + (Aux.collect call_paths) in + (* decreasing order *) + match List.sort (fun (x,_) (y,_) -> y-x) call_paths with + | [] -> None + | (_,p)::_ -> Some p in + let p_callside = Array.mapi + (fun i -> + function Some _ -> None | None -> callside_for_arg i) + p_defside in + let arg_paths = Array.map2 + (fun defside callside -> + match defside, callside with + | Some p, _ | None, Some p -> p + | None, None -> (* find a good path *) + failwith "GGP/TranslateFormula: finding path for defined relation argument undetermined by state terms not implemented yet") + p_defside p_callside in + (* now building the translation *) + let defvars = Array.mapi (fun i _ -> + Formula.fo_var_of_string ("v"^string_of_int i)) arg_paths in + let defbody (args,(rels_phi,pos_state,neg_state)) s_defside = + let arg_eqs = Array.mapi + (fun i v -> + let in_I = p_defside.(i) <> None in + if in_I + then Formula.Eq (v, s_defside.(i)) + else Formula.Eq (v, + var_of_subterm data arg_paths.(i) args.(i))) + defvars in + let arg_eqs = Formula.And (Array.to_list arg_eqs) in + let callside_sterms = + Aux.array_mapi_some + (fun i -> function None -> None + | Some path -> + Some (blank_outside_subterm data path args.(i))) + p_defside in + let callside_sterms = Array.to_list + (Array.map (fun sterm -> 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 + (fun defside path -> defside <> None, path) + p_defside arg_paths in + 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 + (* 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) + 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 *) + | Some sterm -> var_of_term data sterm) + arg_type in + let defrel_phi = Formula.Rel (rel, var_args) in + let defrel_phi = + if sign then defrel_phi else Formula.Not defrel_phi in + let ex_vars = Array.to_list + (Aux.array_mapi_some (fun i (_,path) -> + if arg_sterms.(i) = None + then Some (var_of_subterm data path args.(i)) + else None) arg_type) in + 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 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)) + +let _ = translate_defrel := transl_defrel + Added: trunk/Toss/GGP/TranslateGame.ml =================================================================== --- trunk/Toss/GGP/TranslateGame.ml (rev 0) +++ trunk/Toss/GGP/TranslateGame.ml 2011-07-09 12:37:34 UTC (rev 1508) @@ -0,0 +1,476 @@ +(** {2 Translating GDL definition: Toss rules and initial structure.} + +*) + +open GDL + +(** Translate stable relations that otherwise would be translated as + structure relations, but have arity above the threshold, as + defined relations. *) +let defined_arity_above = ref 2 + +(** Treat "next" clauses which introduce a fluent position for a + 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].) *) +let nonerasing_frame_wave = ref true + +(** Limit on the number of steps for aggregate playout. *) +let agg_playout_horizon = ref 30 + +(** Use "true" atoms while computing rule cases. *) +let split_on_state_atoms = ref false + + +type tossrule_data = { + lead_legal : term; + (* the "legal"/"does" term of the player that performs the move, we + call its parameters "fixed variables" as they are provided externally *) + precond : Formula.formula; + (* the LHS match condition (the LHS structure and the precondition) *) + rhs_add : (string * string array) list; + (* the elements of LHS/RHS structures, corresponding to the "next" + terms *) + struc_elems : string list; + fixvar_elemvars : + (string * (term * (string * string list) list) list) list; + (* "state" terms indexed by variables that they contain, together + with the mask-path of the variable *) + elemvars : term Aux.StrMap.t; +(* "state" terms indexed by Toss variable names they generate *) +} + +(** Data to be used when translating moves. *) +type gdl_translation = { + (* map between structure elements and their term representations; + the reverse direction is by using element names *) + elem_term : term Aux.IntMap.t; + f_paths : paths; + m_paths : paths; + masks : term list; + tossrule_data : tossrule_data Aux.StrMap.t; + (* rule name to rule translation data *) +} + +(* [most_similar c ts] finds a term from [ts] most similar to [c], and + the set of paths that merges the found term and [c]; as in the + definition of $s_\calC$ and $t_\calC$ for a clause $\calC \in + \mathrm{Next}_{e}$. Among the most similar terms finds one that is + not a "frame wave", if not possible and if {!nonerasing_frame_wave} + is [true] -- raises [Not_found]. *) +let most_similar c ts = + let gens = List.map (fun t -> t, merge_terms c t) ts in + (* worse-or-equal as "leq" *) + let cmp (_, (_, pn1, siz1)) (_, (_, pn2, siz2)) = + not (siz1 > siz2) && pn2 >= pn1 in + let best = Aux.maximal cmp gens in + (* avoid "frame wave" if possible *) + let t, (ps, _, _) = + if !nonerasing_frame_wave + then + List.find (fun (t, (ps, _, _)) -> + c = t || + List.for_all + (fun fluent -> Aux.Strings.is_empty (term_vars fluent)) + (at_paths ps t)) best + else List.hd best in + t, ps + + + +(* Find $s_\calC$ and $t_\calC$ for a clause $\calC \in + \mathrm{Next}_{e}$, i.e. in expanded "next" clauses. Determine + which original clauses are frame clauses, and which have to + be dropped (under assumption of being "frame waves"). Return the + proper frame clauses, the non-frame clauses, and the fluent paths + (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 + let stable, nonstable = stable_rels defs in + let inline_defs = + List.filter (fun (rel,_) -> List.mem rel nonstable) defs in + (* To determine whether a clause is a frame, we need to know its + expansion, so we expand clauses separately. A proper frame clause + must have *all* expansions being proper frame clauses. But a + clause is dropped as "frame wave" if any of its expansions is + regarded as "frame wave". *) + let next_clauses = + 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 + 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 + (* "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 res = List.map (find_br_fluents s_C) c_e in + if List.for_all is_frame res + then Aux.Left c + else + let f_paths = + List.map (fun (t_C, ps, neg_true) -> + if neg_true + 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 + 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 + + +let rec contains_blank = function + | Const "_BLANK_" -> true + | Func args -> Aux.array_existsi (fun _ -> contains_blank) args + | _ -> false + + +(* Expand role variables, find fluent and mask paths, generate the + initial structure. *) +let create_init_struc clauses = + let players = + Aux.map_some (function + | ("role", [player]), _ -> Some player + | _ -> None + ) clauses in + let stable_rels, nonstable_rels, + stable_base, init_state, (agg_actions, agg_states) = + aggregate_playout players !agg_playout_horizon rules in + let frame_clauses, move_clauses, f_paths = + fluent_paths_and_frames clauses in + let next_clauses = + List.map (fun ((_,s_C),body_C) -> s_C, true, body_C) frame_clauses + @ List.map (fun ((_,s_C),body_C) -> s_C, false, body_C) + move_clauses in + let arities = + ("EQ_", 2):: + Aux.unique_sorted + (List.map (fun ((rel, args),_) -> rel, List.length args) + clauses) in + let element_terms = + List.fold_left (fun acc st -> Aux.unique_sorted (st @ acc)) [] + agg_states in + let element_reps = + 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 + let m_paths = + List.fold_left paths_union GDL.Empty m_paths in + let mask_reps = + Aux.unique_sorted (List.map (fun t -> + simult_subst m_paths blank t) element_reps) in + let m_pathl = paths_to_list m_paths in + let f_pathl = paths_to_list f_paths in + (* adding subterm equality relations and fact relations *) + let struc_rels, defined_rels = + List.partition (fun rel -> + List.assoc rel arities <= !defined_arity_above) stable_rels in + let struc_rels = "EQ_"::struc_rels in + let defined_rels = defined_rels @ nonstable_rels 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 path_tups = Aux.all_ntuples m_pathl arity in + List.fold_left (fun 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) + || List.mem (rel, tup) stable_base + then + Structure.add_rel_named_elems struc fact_rel + (Aux.array_map_of_list name_of_term tup) + else struc + ) struc elem_tups + ) struc path_tups + ) (Structure.empty ()) struc_rels in + (* adding anchor and fluent predicates *) + let add_pred struc paths elements = + List.fold_left (fun path -> + Aux.fold_left_try (fun elem -> + let pred = + pred_on_path_subterm path (at_path elem path) in + let tup = [|elem|] in + Structure.add_rel_named_elems struc pred + (Aux.array_map_of_list name_of_term tup) + ) struc elements + ) struc paths in + let struc = add_pred struc m_pathl element_reps in + let struc = add_pred struc f_pathl init_state in + (* adding mask predicates *) + let all_paths = paths_union m_paths f_paths in + let struc = + List.fold_left (fun struc m -> + let pred = term_to_name m in + List.fold_left (fun struc elem -> + if simult_subst all_paths blank elem = m + then + Structure.add_rel_named_elems struc pred + [|name_of_term elem|] + else struc + ) struc element_reps + ) struc maks_reps in + next_clauses, f_paths, m_paths, mask_rels, defined_rels, + stable_base, init_state, struc + + +(* Find the rule clauses $\ol{\calC},\ol{\calN}$. *) +let move_tuples used_vars next_cls legal_tuples = + (* computing the $d_i(\calN)$ for each $\calN$ *) + 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) = + List.fold_right (fun p (sb, dis) -> + let djs = + Aux.map_some (function + | Does (dp, d) when dp = p -> Some d + | _ -> None) body in + let sb = unify_all sb djs in + let d = + match djs with + | [] -> fresh_x_f () + | d::_ -> subst sb d in + sb, d::dis + ) players ([], []) in + let next_cls = + Aux.map_try (fun cl -> + let sb, ds = does_facts cl in + subst_clause sb cl, ds) next_cls in + (* selecting $\ol{\calC},\ol{\calN}$ clauses with + $\sigma_{\ol{\calC},\ol{\calN}}$ applied *) + let tup_unifies ts1 ts2 = + try unify [] ts1 ts2; true + with Not_found -> false in + let move_clauses cs = + (* bag of next clauses for each legal tuple *) + let next_clauses = + List.filter (fun (n_cl, ds) -> tup_unifies cs ds) next_cls in + (* two passes to ensure coverage and maximality *) + let rec coverage = function + | (n_cl, ds)::more_cls as all_cls + , ((sb, tup_ds, n_cls)::other_cl_tups as all_cl_tups) -> + (try + let sb, tup_ds = List.fold_right + (fun (di, acc_di) (sb, tup_ds) -> + let sb = unify sb [di] [acc_di] in + sb, subst sb di::tup_ds + ) (List.combine ds tup_ds) (sb, []) in + coverage (more_cls, (sb, tup_ds, n_cl::n_cls)::other_cl_tups) + with Not_found -> + (* start a new tuple *) + coverage (all_cls, ([], cs, [])::all_cl_tups) + ) + | [], all_cl_tups -> all_cl_tups + | _, [] -> assert false in + let cl_tups = + coverage (next_clauses, [[], cs, []]) in + let maximality cl_tup = + List.fold_left (fun (sb, tup_ds, n_cls as cl_tup) (n_cl, ds) -> + if List.mem n_cl n_cls then cl_tup + else + try + let sb, tup_ds = List.fold_right + (fun (di, acc_di) (sb, tup_ds) -> + let sb = unify sb [di] [acc_di] in + sb, subst sb di::tup_ds + ) (List.combine ds tup_ds) (sb, []) in + (sb, tup_ds, n_cl::n_cls) + with Not_found -> cl_tup + ) cl_tup next_clauses in + List.map maximality cl_tups in + Aux.concat_map move_clauses legal_tuples + + +let add_erasure_clauses (legal_tup, next_cls) = + 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 + (* two passes to ensure coverage and maximality *) + (* FIXME-TODO: treat fixed-vars as consts, by substituting them with + Const, and later substituting-back Var *) + let rec coverage = function + | (s, body)::more_cls + , ((sb, s_acc, bodies)::other_frames as all_frames) -> + (try + let sb = unify sb [s] [s_acc] in + let s_acc = subst sb s in + coverage (more_cls, (sb, s_acc, body::bodies)::other_frames) + with Not_found -> + (* start a new frame *) + coverage (more_cls, ([], s, [body])::all_frames) + ) + | [], all_frames -> all_frames + | (s, body)::more_cls, [] -> + coverage (more_cls, [[], s, [body]]) in + let frames = coverage (frame_cls, []) in + let maximality frame = + List.fold_left (fun (sb, s_acc, bodies as frame) (s, body) -> + if List.mem body bodies then frame + else + try + let sb = unify sb [s] [s_acc] in + let s_acc = subst sb s in + (sb, s_acc, body::bodies) + with Not_found -> frame + ) frame frame_cls in + let frames = List.map maximality frames in + let frames = + List.map (fun (sb, s, bodies) -> + s, List.map (subst_rels sb) bodies) in + let erasure_cls = + Aux.concat_map (fun (s, bodies) -> + let nbodies = negate_bodies bodies in + List.map (fun b -> s, b) nbodies + ) frames in + let next_cls = + Aux.map_some (fun (s, frame, body) -> + if not frame then Some (s, body) else None) next_cls in + legal_tup, next_cls @ erasure_cls + + +(* Assign rule clauses to rule cases, i.e. candidates for Toss + rules. Collect the conditions and RHS state terms together. *) +let rule_cases (legal_tup, next_cls) = + let atoms = Aux.concat_map + (fun (_, body) -> Aux.map_some (function + | Pos (Rel _ as a) | Neg (Rel _ as a) -> Some a + | (Pos (True _ as a) | Neg (True _ as a)) + when !split_on_state_atoms -> Some a + | _ -> None) body) next_cls in + let patterns = + let next_cls = Array.of_list next_cls in + List.map (fun a -> + Array.map (fun i (_, body) -> + if List.mem (Neg a) body then -1 + else if List.mem (Pos a) body then 1 + else 0 + ) next_cls, + a) atoms in + let patterns = Aux.collect patterns in + let patterns = List.filter (fun (pat, _) -> + Array.exists (fun v-> v < 1) pat && + Array.exists (fun v-> v > -1) pat) patterns in + let pos_choice = List.map (fun _ -> true) patterns in + let neg_choice = List.map (fun _ -> false) patterns in + let choices = Aux.product [pos_choice; neg_choice] in + let rule_case choice = + let separation_cond = + List.concat + (List.map2 (fun b (_, atoms) -> + if b then List.map (fun a -> Pos a) atoms + else List.map (fun a -> Neg a) atoms) choice patterns) in + let case_cls = + List.filter (fun (_, body) -> + List.for_all2 (fun b (_, atoms) -> + if b then (* atoms not excluded *) + List.for_all (fun a -> not (List.mem (Neg a) body)) atoms + else (* atoms not included *) + List.for_all (fun a -> not (List.mem (Pos a) body)) atoms + ) choice patterns + ) next_cls in + let case_rhs, case_conds = List.split case_cls in + case_rhs, separation_cond @ case_conds in + List.map (fun choice -> + let case_rhs, case_conds = rule_case choice in + let case_conds = case_conds @ + Aux.concat_map snd legal_tup in + case_rhs, case_conds) choices + + +(* The candidates need to be filtered before finishing the + translation of Toss rules. *) +let create_rule_cands used_vars next_cls clauses = + let players = (* Array.of_list *) + Aux.map_some (function + | ("role", [player]), _ -> Some player + | _ -> None + ) clauses in + let legal_cls = + List.filter (fun ((rel,_),_) -> rel="legal") clauses in + (* let next_cls = + List.filter (fun ((rel,_),_) -> rel="next") clauses in *) + (* constructing $(\calC_1,...,\calC_n)$ tuples *) + let legal_by_player = + List.map (fun p -> + Aux.map_some (function + | ("legal",[lp; l]), body when lp = p -> Some (l, body) + | _ -> None) legal_cls + ) players in + let legal_tuples = Aux.product legal_by_player in + let move_tups = move_tuples used_vars next_cls legal_tuples in + let move_tups = + List.map (fun (sb, legal_tup, n_cls) -> + List.map (subst sb) legal_tup, + List.map (subst_clause sb) n_cls) move_tups in + let move_tups = List.map add_erasure_clauses move_tups in + Aux.concat_map rule_cases move_tups + + +let filter_rule_cands stable_base defined_rels rule_cands = + let check_atom = function + | Pos (Rel (rel, _ as a)) -> + List.mem rel defined_rels || + List.exists (rels_unify a) stable_base + | Neg (Rel (rel, _ as a)) -> + List.mem rel defined_rels || + not (List.exists (rels_unify a) stable_base) + | _ -> true in + List.filter (fun (case_rhs, case_conds) -> + List.for_all check_atom case_conds + ) rule_cands + + +let translate_game clauses = + let clauses = expand_players clauses in + let used_vars, clauses = rename_clauses clauses in + let next_cls, f_paths, m_paths, mask_rels, defined_rels, + stable_base, init_state, struc = create_init_struc clauses in + let rule_cands = create_rule_cands used_vars next_cls clauses in + let rule_cands = filter_rule_cands stable_base rule_cands in + let all_state_terms = + Aux.concat_map state_terms (List.map snd clauses) in + let term_arities = Aux.unique_sorted + (Aux.concat_map term_arities all_state_terms) in + + + +(* ************************************************************ *) +(* ************************************************************ *) +(** {3 Translating Moves.} *) + + +let initialize_game player game_descr startcl = + let gdl_transl, state = translate_game player game_descr in + state, None, gdl_transl + + +let translate_last_action gdl_translation state actions = + if actions = [] then (* start of game -- Server will not perform a move *) + "", [] + else translate_incoming_move gdl_translation state actions + + +let translate_move gdl_translation new_state rule emb = + let res = translate_outgoing_move gdl_translation new_state rule emb in + (* {{{ log entry *) + if !debug_level > 0 then ( + Printf.printf "GDL.translate_move: %s\n%!" res + ); + (* }}} *) + res This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |