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

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

Revision: 1334
          http://toss.svn.sourceforge.net/toss/?rev=1334&view=rev
Author:   lukstafi
Date:     2011-02-26 12:52:28 +0000 (Sat, 26 Feb 2011)

Log Message:
-----------
GDL translation: better frame/erasure generation (fix). Aux: cleaner fresh names (optional).

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

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-02-25 00:02:36 UTC (rev 1333)
+++ trunk/Toss/Formula/Aux.ml	2011-02-26 12:52:28 UTC (rev 1334)
@@ -406,6 +406,13 @@
   else fold_n f (f accu) (n-1)
 
 
+(* Character classes. *)
+let is_uppercase c = c >= 'A' && c <= 'Z'
+let is_lowercase c = c >= 'a' && c <= 'z'
+let is_digit c = c >= '0' && c <= '9'
+let is_letter c = is_uppercase c || is_lowercase c
+let is_alphanum c = is_letter c || is_digit c
+
 (* Return the result of the first index [i] that passes the
    given test, and [i+1]. *)
 let rec first_i n gen test =
@@ -418,7 +425,13 @@
     snd (first_i 1 (fun i->basename^(string_of_int i)^suffix)
       (fun fname->not (Sys.file_exists fname)))
 
-let not_conflicting_name names s =
+let not_conflicting_name ?(truncate=false) names s =
+  let s =
+    if truncate then
+      let i = ref (String.length s - 1) in
+      while !i > 0 && is_digit s.[!i] do decr i done;
+      String.sub s 0 (!i + 1)
+    else s in
   if not (Strings.mem s names) then s
   else
     snd (first_i 0 (fun i -> s^(string_of_int i))
@@ -431,13 +444,6 @@
 	(fun v -> not (Strings.mem v names)) in
     i', v::res) (0,[]) n))
 
-(* Character classes. *)
-let is_uppercase c = c >= 'A' && c <= 'Z'
-let is_lowercase c = c >= 'a' && c <= 'z'
-let is_digit c = c >= '0' && c <= '9'
-let is_letter c = is_uppercase c || is_lowercase c
-let is_alphanum c = is_letter c || is_digit c
-
 (* Printing. *)
 
 let list_fprint e_printf outchan l =

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-02-25 00:02:36 UTC (rev 1333)
+++ trunk/Toss/Formula/Aux.mli	2011-02-26 12:52:28 UTC (rev 1334)
@@ -217,8 +217,9 @@
 (** Generate a fresh filename of the form [base ^ n ^ suffix]. *)
 val new_filename : string -> string -> string
 
-(** Returns a string proloning [s] and not appearing in [names]. *)
-val not_conflicting_name : Strings.t -> string -> string
+(** Returns a string proloning [s] and not appearing in [names]. If
+    [truncate] is true, remove numbers from the end of [s]. *)
+val not_conflicting_name : ?truncate:bool -> Strings.t -> string -> string
 
 (** Returns [n] strings proloning [s] and not appearing in [names]. *)
 val not_conflicting_names :

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-02-25 00:02:36 UTC (rev 1333)
+++ trunk/Toss/GGP/GDL.ml	2011-02-26 12:52:28 UTC (rev 1334)
@@ -258,7 +258,7 @@
     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.
+    (unapplicable) rules. TODO: rethink, compare with (7f2).
 
     (7e) Associate negation of equalities specific to the unifiers
     strictly less general than the equivalence class with it, so that
@@ -281,9 +281,6 @@
     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
@@ -804,7 +801,7 @@
     | [], [] -> sb, m_sb
     | (Const _ (* | Var _ *) as a)::terms1,
       (Const _ (* | Var _ *) as b)::terms2
-      when a=b -> match_meta sb m_sb terms1 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 ->
@@ -817,9 +814,17 @@
         if List.mem_assoc x sb then
           if List.assoc x sb = term then sb
           else raise Not_found
-        else sb1::List.map (fun (x,t)->x, subst_one sb1 t) sb in
+        else sb1::sb in
       match_meta sb m_sb terms1 terms2
-    | _ -> raise Not_found
+    | _ ->
+      (* {{{ log entry *)
+      if !debug_level > 4 then (
+        Printf.printf "match_meta: unmatched (%s) against pattern (%s)\n%!"
+          (String.concat ", " (List.map term_str terms1))
+          (String.concat ", " (List.map term_str terms2))
+      );
+      (* }}} *)
+      raise Not_found
 
 
 (* 3c1 *)
@@ -1055,14 +1060,14 @@
     | Var x ->
       if List.mem_assoc x !sb then Var (List.assoc x !sb)
       else
-        let x1 = Aux.not_conflicting_name !var_support x in
+        let x1 = Aux.not_conflicting_name ~truncate:true !var_support x in
         var_support := Aux.Strings.add x1 !var_support;
         sb := (x,x1)::!sb;
         Var x1
     | MVar x ->
       if List.mem_assoc x !sb then MVar (List.assoc x !sb)
       else
-        let x1 = Aux.not_conflicting_name !var_support x in
+        let x1 = Aux.not_conflicting_name ~truncate:true !var_support x in
         var_support := Aux.Strings.add x1 !var_support;
         sb := (x,x1)::!sb;
         MVar x1
@@ -1076,7 +1081,7 @@
       List.map (fun x ->
         if List.mem_assoc x !sb then List.assoc x !sb
         else
-          let x1 = Aux.not_conflicting_name !var_support x in
+          let x1 = Aux.not_conflicting_name ~truncate:true !var_support x in
           var_support := Aux.Strings.add x1 !var_support;
           sb := (x,x1)::!sb; x1
       ) (Aux.Strings.elements vs) in
@@ -1781,7 +1786,7 @@
   let conjs = Aux.unique_sorted
     (Aux.concat_map FormulaOps.flatten_ands conjs) in
   (* {{{ log entry *)
-  if !debug_level > 2 then (
+  if !debug_level > 4 then (
     Printf.printf "lift_universal: vars %s -- conjs:\n%s\n%!"
       (String.concat ", "
          (List.map Formula.var_str (uni_vars :> Formula.var list)))
@@ -1802,7 +1807,7 @@
       Formula.And (global @ [
         Formula.All (used_uni_vars, Formula.And local)]) in
   (* {{{ log entry *)
-  if !debug_level > 2 then (
+  if !debug_level > 4 then (
     Printf.printf "lift_universal: result\n%s\n%!"
       (Formula.sprint res)
   );
@@ -2426,25 +2431,45 @@
                   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
+              Aux.unique_sorted
+                (List.map (fun repr ->
+                  List.filter (fun cl->leq3 cl repr) frame_brs)
+                   frame_brs) in
+            (* {{{ log entry *)
+            if !debug_level > 3 then (
+              Printf.printf "frames: heads partitioning =\n%s\n%!"
+                (String.concat "\n"
+                   (List.map (fun l ->
+                     String.concat ", "
+                       (List.map (function [head],_,_->term_str head
+                         | _ -> assert false) l)) frames))
+            );
+            (* }}} *)
             (* 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 ->
+              | f_brs ->
+                let repr_head =
+                  match Aux.maximal leq3 f_brs with
+                    | [head, _, _] -> head
+                    | _ -> assert false in
                 let multi_body = List.map
                   (fun (head2, body2, neg_body2) ->
-                    let sb, _ = match_meta [] [] head head2 in
+                    let sb, _ = match_meta [] [] repr_head head2 in
                     subst_rels sb body2,
                     List.map (fun (uni_vs,neg) ->
                       uni_vs, subst_rels sb neg) neg_body2
                   ) f_brs in
-                head, (body, neg_body)::multi_body
+                repr_head, multi_body
             ) frames in
+            (* {{{ log entry *)
+            if !debug_level > 2 then (
+              Printf.printf "frames: heads = %s\n%!"
+                (String.concat ", " (List.map (function [h],_ ->term_str h
+                  | _ -> assert false) frames))
+            );
+            (* }}} *)
             (* 7f3 *)
             let erasure_brs : exp_def_branch list = Aux.concat_map
               (function

Modified: trunk/Toss/GGP/GDLTest.ml
===================================================================
--- trunk/Toss/GGP/GDLTest.ml	2011-02-25 00:02:36 UTC (rev 1333)
+++ trunk/Toss/GGP/GDLTest.ml	2011-02-26 12:52:28 UTC (rev 1334)
@@ -113,5 +113,6 @@
   DiscreteRule.debug_level := 4;
   let breakthrough = load_rules "./GGP/examples/breakthrough.gdl" in
   let connect5 = load_rules "./GGP/examples/connect5.gdl" in
+  let tictactoe = load_rules "./GGP/examples/tictactoe.gdl" in
   let gdef = GDL.translate_game (Const "x") connect5 in
-  ignore gdef; ignore connect5; ignore breakthrough
+  ignore gdef; ignore connect5; ignore breakthrough; ignore tictactoe


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