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

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

Revision: 1628
          http://toss.svn.sourceforge.net/toss/?rev=1628&view=rev
Author:   lukaszkaiser
Date:     2011-11-11 22:08:39 +0000 (Fri, 11 Nov 2011)
Log Message:
-----------
More tail-recursiveness corrections for GDL translation, some added timeouts.

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/TranslateGame.ml

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-11-11 00:56:17 UTC (rev 1627)
+++ trunk/Toss/Formula/Aux.ml	2011-11-11 22:08:39 UTC (rev 1628)
@@ -246,23 +246,24 @@
     try f hd
     with Not_found -> find_try f tl
 
-let rec fold_left_try f accu l =
-  match l with
-      [] -> accu
-    | a::l ->
-      try
-        fold_left_try f (f accu a) l
-      with Not_found -> fold_left_try f accu l
+let rec fold_left_try f accu = function
+  | [] -> accu
+  | a::l ->
+    let new_accu = try f accu a with Not_found -> accu in
+    fold_left_try f new_accu l
 
-let rec power dom img =
-  List.fold_right (fun v sbs ->
-    concat_map (fun e -> List.map (fun sb -> (v,e)::sb) sbs) img)
-    dom [[]]
+let rec power ?(timeout = fun () -> false) dom img =
+  List.fold_left (fun sbs v ->
+    concat_map (fun e -> if timeout () then raise (Timeout "Aux.product") else
+	List.rev (List.rev_map (fun sb -> (v,e)::sb) sbs)) img)
+    [[]] (List.rev dom)
 
-let product l =
-  List.fold_right (fun set prod ->
-    concat_map (fun el -> List.map (fun tup -> el::tup) prod) set)
-    l [[]]
+let product ?(timeout = fun () -> false) l =
+  List.fold_left (fun prod set ->
+    concat_map (fun el -> if timeout () then raise (Timeout "Aux.product") else
+	List.rev (List.rev_map (fun tup -> el::tup) prod)
+    ) set)
+    [[]] (List.rev l) 
 
 let rec pairs l =
   match l with

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-11-11 00:56:17 UTC (rev 1627)
+++ trunk/Toss/Formula/Aux.mli	2011-11-11 22:08:39 UTC (rev 1628)
@@ -159,11 +159,11 @@
 val fold_left_try : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
 
 (** [power dom img] generates all functions with domain [dom] and
-    image [img], as graphs. *)
-val power : 'a list -> 'b list -> ('a * 'b) list list
+    image [img], as graphs. *) 
+val power : ?timeout:(unit -> bool) -> 'a list -> 'b list -> ('a * 'b) list list
 
 (** Cartesian product of lists. Not tail recursive. *)
-val product : 'a list list -> 'a list list
+val product : ?timeout:(unit -> bool) -> 'a list list -> 'a list list
 
 (** A list of all pairs of elements that preserve the order of
     elements from the list. *)

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-11-11 00:56:17 UTC (rev 1627)
+++ trunk/Toss/GGP/GDL.ml	2011-11-11 22:08:39 UTC (rev 1628)
@@ -934,6 +934,7 @@
       (Aux.Strings.elements br_vars) in
     let sb = List.map (fun (v,t) -> v, Var t) sb in
     List.map (subst_br sb) brs in
+
   let expand_pos_atom (rel, args as atom)
       (sb, (head, r_body, r_neg_body)) =
     (let try def_brs = freshen_brs (List.assoc rel defs) in
@@ -946,9 +947,11 @@
      ) def_brs
      with Not_found ->
        [sb, (head, (subst_rel sb atom)::r_body, r_neg_body)]) in
+
   let pack_lits body neg_body =
     List.map (fun a->Aux.Left a) body @
       List.map (fun a->Aux.Right a) neg_body in
+
   let expand_neg_atom (rel, args as atom)
       (sb, (head, r_body, r_neg_body)) =
     (let try def_brs = freshen_brs (List.assoc rel defs) in
@@ -963,14 +966,14 @@
        def_brs in
      if def_brs = [] then
        [sb, (head, r_body, r_neg_body)]
-     else
+     else (
        (* DNF of the negation of [def_brs] disjunction --
           [Left]/[Right] switch meaning *)
-       let dnf_of_neg = Aux.product def_brs in
+       let dnf_of_neg = Aux.product ~timeout:!timeout def_brs in
        List.map (fun dnf_br ->
          let d_neg_body, d_body = Aux.partition_choice dnf_br in
          sb, (head, d_body @ r_body, d_neg_body @ r_neg_body)
-       ) dnf_of_neg
+       ) dnf_of_neg )
      with Not_found ->
        [sb, (head, r_body, (subst_rel sb atom)::r_neg_body)]) in
 
@@ -978,6 +981,7 @@
     let init = [[], (head, [], [])] in
     Aux.concat_foldr expand_neg_atom neg_body
       (Aux.concat_foldr expand_pos_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
@@ -1000,7 +1004,7 @@
   let clauses = List.map (fun (_,body,neg_body) ->
     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
+  let negated = Aux.product ~timeout:!timeout clauses in
   (* can raise [Not_found] in case of unsatisfiable "not distinct" *)
   let nclause body =
     let uniterms, lits =
@@ -1602,7 +1606,7 @@
       (player_vars_of (List.map rel_of_atom (atoms_of_clause clause))) in
     if plvars = [] then [clause]
     else
-      let sbs = Aux.power plvars players in
+      let sbs = Aux.power ~timeout:!timeout plvars players in
       List.map (fun sb -> subst_clause sb clause) sbs in
   Aux.concat_map exp_clause clauses
 

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-11-11 00:56:17 UTC (rev 1627)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-11-11 22:08:39 UTC (rev 1628)
@@ -1179,7 +1179,7 @@
     );
     (* }}} *)
     List.map (fun sb->subst_clause sb g_cl) v_sbs in
-  Aux.concat_map expand goal_cls @ clauses
+  List.rev_append (List.rev (Aux.concat_map expand goal_cls)) clauses
 
 let prepare_relations_and_structure
     ground_state_terms f_paths c_paths element_reps root_reps
@@ -1816,26 +1816,27 @@
         (String.concat " "(List.map literal_str goal));
     );
       (* }}} *)
-    let res =
-      run_prolog_check_goal static_goal program &&
-        let goal = optimize_goal ~testground goal in
-          (* {{{ log entry *)
+    let res_prolog = run_prolog_check_goal static_goal program in
+    let res = res_prolog &&
+      let goal = optimize_goal ~testground goal in
+        (* {{{ log entry *)
         if !debug_level > 3 then (
           Printf.printf
             "goal=%s\n%!" (String.concat " "(List.map literal_str goal))
         );
-          (* }}} *)
-        List.exists
+        (* }}} *)
+      List.exists
           (fun state ->
-              (* {{{ log entry *)
+            (* {{{ log entry *)
             if !debug_level > 3 then Printf.printf ".%!";
-              (* }}} *)
-            run_prolog_check_goal goal
-              (replace_rel_in_program "true" (state_cls state) program))
+            (* }}} *)
+	    let repl_program =
+	      replace_rel_in_program "true" (state_cls state) program in
+            run_prolog_check_goal goal repl_program)
           playout_states in
-      (* {{{ log entry *)
+    (* {{{ log entry *)
     if !debug_level > 3 then Printf.printf " %B\n%!" res;
-      (* }}} *)
+    (* }}} *)
     res in
   let unrequired_cls = Aux.map_some
     (function
@@ -1909,9 +1910,10 @@
       Array.iteri print_cl (Array.of_list unrequired_cls)
     );
     (* }}} *)
-    let choices = Aux.power split_atoms [false; true] in
+    let choices = Aux.power ~timeout:!timeout split_atoms [false; true] in
     let unrequired_cls = Array.of_list unrequired_cls in
     let rule_case choice =
+      check_timeout ~print:false "rule_cases: internal rule_case: start";
       let separation_cond =
         List.map (fun (a,b) -> if b then Pos a else Neg a) choice in
       let case =
@@ -1928,7 +1930,7 @@
         ) unrequired_cls in
       let ids, cls = List.split (Array.to_list case) in
       Aux.ints_of_list ids, separation_cond, cls in
-    let cases = List.map rule_case choices in
+    let cases = List.rev (List.rev_map rule_case choices) in
     let process_case (ids, separation_cond, case_cls) =
       let case_cls = Aux.map_prepend case_cls
         (fun (h,b) -> h, Legal_cl, b) required_cls in

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.