toss-devel-svn Mailing List for Toss (Page 9)

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 422-6466

Revision: 1549
          http://toss.svn.sourceforge.net/toss/?rev=1549&view=rev
Author:   lukaszkaiser
Date:     2011-08-29 21:08:20 +0000 (Mon, 29 Aug 2011)
Log Message:
-----------
Starting to add let-in to formulas and real exprs.

Modified Paths:
--------------
    trunk/Toss/Formula/Formula.ml
    trunk/Toss/Formula/Formula.mli
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOpsTest.ml
    trunk/Toss/Formula/FormulaParser.mly
    trunk/Toss/Formula/Lexer.mll
    trunk/Toss/Formula/Tokens.mly

Modified: trunk/Toss/Formula/Formula.ml
===================================================================

--- trunk/Toss/Formula/Formula.ml	2011-08-28 23:14:56 UTC (rev 1548)
+++ trunk/Toss/Formula/Formula.ml	2011-08-29 21:08:20 UTC (rev 1549)
@@ -115,6 +115,7 @@
   | All of var list * formula
   | Lfp of [ mso_var | so_var ] * fo_var array * formula
   | Gfp of [ mso_var | so_var ] * fo_var array * formula
+  | Let of string * string list * formula * formula
 
 and real_expr =    
   | RVar of string
@@ -124,6 +125,7 @@
   | Fun of string * fo_var
   | Char of formula
   | Sum of fo_var list * formula * real_expr
+  | RLet of string * real_expr * real_expr
 
 
 let is_atom = function
@@ -211,6 +213,10 @@
     Format.fprintf f "@[<1>gfp %a(%a) = (%a)@]" fprint_var r
       (Aux.fprint_sep_list "," fprint_var) (Array.to_list vs)
       (fprint_prec prec) fpphi
+  | Let (r, args, rphi, inphi) ->
+    Format.fprintf f "@[<1>let %s(%s) = %a in %a@]" r (String.concat ", " args)
+      (fprint_prec prec) rphi (fprint_prec prec) inphi
+    
 
 (* Bracket-savvy precedences: 0 +, 2 * *)
 and fprint_real_prec prec f = function
@@ -231,6 +237,9 @@
       Format.fprintf f "@[<1>Sum@ (@,%a@ |@ %a@ :@ %a@,)@]" 
         (Aux.fprint_sep_list "," fprint_var) vl (fprint_prec 0) phi
         (fprint_real_prec 0) r
+  | RLet (v, lre, inre) ->
+    Format.fprintf f "@[<1>let %s = %a in %a@]" v
+      (fprint_real_prec prec) lre (fprint_real_prec prec) inre
 
 
 let fprint f phi = fprint_prec 0 f phi
@@ -298,6 +307,7 @@
   | RealExpr (re, sgn) -> size_real ~acc:(acc + 1) re
   | Not phi   | Ex (_, phi) | All (_, phi) | Lfp (_,_,phi) | Gfp (_,_,phi) -> 
     size ~acc:(acc + 1) phi
+  | Let (_, _, def, phi) -> size ~acc:(size ~acc:(acc + 2) def) phi
   | And flist | Or flist -> 
     List.fold_left (fun i f -> size ~acc:i f) (acc + 1) flist
 and size_real ?(acc=0) = function
@@ -307,6 +317,7 @@
   | Char phi -> size ~acc phi
   | Sum (_, phi, re) -> 
     let sr = size_real ~acc:(acc + 1) re in size ~acc:sr phi
+  | RLet (_, rdef, re) -> size_real ~acc:(size_real ~acc:(acc + 2) rdef) re
 
 
 let rec rec_compare phi1 phi2 = 
@@ -359,6 +370,13 @@
 	      rec_compare psi1 psi2
     | (Lfp _, _) -> -1
     | (_, Lfp _) -> 1
+    | (Gfp _, _) -> -1
+    | (_, Gfp _) -> 1
+    | (Let (r1, a1, def1, phi1), Let (r2, a2, def2, phi2)) ->
+      let rc = Pervasives.compare r1 r2 in if rc <> 0 then rc else
+	  let ac = Pervasives.compare a1 a2 in if ac <> 0 then ac else
+	      let dc = rec_compare def1 def2 in if dc <> 0 then dc else
+		  rec_compare phi1 phi2
 
 and rec_compare_re re1 re2 =
   match (re1, re2) with
@@ -418,6 +436,8 @@
     | Gfp (r, vs, phi) -> 
       (match flatten_f f_or f_and phi with
 	| Or [] -> Or [] | And [] -> And [] | f -> Gfp (r, vs, f))
+    | Let (r, a, def, phi) -> 
+      Let (r, a, flatten_f f_or f_and def, flatten_f f_or f_and phi)
 
 and flatten_re_f f_or f_and = function
   | RVar _ | Const _ | Fun _ as re -> re
@@ -428,8 +448,9 @@
   | Char (phi) -> Char (flatten_f f_or f_and phi)
   | Sum (vl, phi, r) ->
     Sum (vl, flatten_f f_or f_and phi, flatten_re_f f_or f_and r)
+  | RLet (v, def, re) -> 
+    RLet (v, flatten_re_f f_or f_and def, flatten_re_f f_or f_and re)
 
-
 (* Basic function to flatten formulas. *)
 let flatten psi = flatten_f (fun x -> x) (fun x -> x) psi
 let flatten_re psi = flatten_re_f (fun x -> x) (fun x -> x) psi
@@ -535,6 +556,8 @@
       let sgok = if is_mso (r :> var) then Array.length vs = 1 else
 	  ok_sg (var_str r) (Array.length vs) in
       sgok && (syntax_ok ~sg ~fp:(((var_str r), pos) :: fp) ~pos phi)
+    | Let (_, _, rphi, inphi) -> (* FIXME!! stupid let-check for now *)
+      syntax_ok ~sg ~fp ~pos rphi && syntax_ok ~sg ~fp ~pos inphi
 
 and syntax_ok_re ?(sg=ref []) ?(fp=[]) ?(pos=true) = function
   | RVar _ | Const _ | Fun _ -> true
@@ -543,3 +566,5 @@
   | Char phi -> syntax_ok ~sg ~fp ~pos phi
   | Sum (_, phi, r) ->
     syntax_ok ~sg ~fp ~pos phi && syntax_ok_re ~sg ~fp ~pos r
+  | RLet (_, re, inre) -> (* FIXME!! stupid let-check for now *)
+    syntax_ok_re ~sg ~fp ~pos re && syntax_ok_re ~sg ~fp ~pos inre

Modified: trunk/Toss/Formula/Formula.mli
===================================================================
--- trunk/Toss/Formula/Formula.mli	2011-08-28 23:14:56 UTC (rev 1548)
+++ trunk/Toss/Formula/Formula.mli	2011-08-29 21:08:20 UTC (rev 1549)
@@ -60,6 +60,7 @@
   | All of var list * formula
   | Lfp of [mso_var | so_var] * fo_var array * formula
   | Gfp of [mso_var | so_var] * fo_var array * formula
+  | Let of string * string list * formula * formula
 
 (** Real-valued terms allow counting, characteristic functions, arithmetic. *)
 and real_expr =
@@ -70,8 +71,8 @@
   | Fun of string * fo_var
   | Char of formula
   | Sum of fo_var list * formula * real_expr
+  | RLet of string * real_expr * real_expr
 
-
 val pow : real_expr -> int -> real_expr
 
 val size : ?acc : int -> formula -> int

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-08-28 23:14:56 UTC (rev 1548)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-08-29 21:08:20 UTC (rev 1549)
@@ -47,8 +47,9 @@
     | Gfp (r, vs, phi) when neg ->
       Lfp (r, vs, nnf ~neg:true ~rev:((var_str r) :: rev) phi)
     | Gfp (r, vs, phi) -> Gfp (r, vs, nnf ~neg:false ~rev phi)
+    | Let (r, args, body, phi) -> (* subst_rels [(rel, (args, body))] phi *)
+      Let (r, args, nnf body, nnf phi)
 
-
 (* -------------------------- FREE VARIABLES -------------------------------- *)
 
 (* Helper function: remove duplicates from sorted list of variables. *)

Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml	2011-08-28 23:14:56 UTC (rev 1548)
+++ trunk/Toss/Formula/FormulaOpsTest.ml	2011-08-29 21:08:20 UTC (rev 1549)
@@ -41,8 +41,8 @@
 	"all :x, :y (not :x^2 -0.5 < :y^2 -1)";
       nnf_eq "ex x :(all y (R (x, y))) > 0"
 	"ex x :(all y (R (x, y))) > 0";
-      nnf_eq "set R(x) = ex y C(x, y) in P(x) or R(x)"
-	"P(x) or ex y C(x, y)";
+      nnf_eq "let R(x) = not ex y C(x, y) in not (P(x) or R(x))"
+	"let R(x) = all y not C(x, y) in not P(x) and not R(x)";
       nnf_eq "not lfp T(x) = (P(x) or ex y (E(x, y) and y in T))"
 	"gfp T(x) = (not P(x) and all y (not E(x, y) or y in T))";
       nnf_eq "not lfp |R(x, y) = (P(x, y) or ex z (E(x, z) and |R(y, z)))"

Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly	2011-08-28 23:14:56 UTC (rev 1548)
+++ trunk/Toss/Formula/FormulaParser.mly	2011-08-29 21:08:20 UTC (rev 1549)
@@ -15,7 +15,7 @@
 %}
 
 %start parse_formula parse_real_expr
-%type <Formula.formula> parse_formula formula_with_set_expr formula_expr
+%type <Formula.formula> parse_formula formula_with_let_expr formula_expr
 %type <Formula.var list> var_list
 %type <Formula.fo_var list> fo_var_list
 %type <Formula.real_expr> parse_real_expr real_expr
@@ -116,17 +116,17 @@
         { Or [And [Not ($1); Not ($3)]; And [$1; $3]] }
   | OPEN formula_expr CLOSE          { $2 }
 
-formula_with_set_expr:
+formula_with_let_expr:
   | formula_expr { $1 }
-  | SET_CMD rel = ID
-    arg = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
+  | LET_CMD rel = ID
+    args = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
     EQ
-    body = formula_expr IN phi = formula_with_set_expr
-      { FormulaOps.subst_rels [(rel, (arg, body))] phi }
+    body = formula_expr IN phi = formula_with_let_expr
+      { Let (rel, args, body, phi) }
 
 
 parse_formula:
-  formula_with_set_expr EOF 
+  formula_with_let_expr EOF 
   { if Formula.syntax_ok $1 then $1 else 
       raise (Parsing_error "Wrong formula syntax (arities? fixed-points?)") };
 

Modified: trunk/Toss/Formula/Lexer.mll
===================================================================
--- trunk/Toss/Formula/Lexer.mll	2011-08-28 23:14:56 UTC (rev 1548)
+++ trunk/Toss/Formula/Lexer.mll	2011-08-29 21:08:20 UTC (rev 1549)
@@ -62,6 +62,7 @@
   | DEL_CMD
   | GET_CMD
   | SET_CMD
+  | LET_CMD
   | EVAL_CMD
   | ELEM_MOD
   | REL_MOD
@@ -201,6 +202,8 @@
   | "GET"           { GET_CMD }
   | "SET"           { SET_CMD }
   | "set"           { SET_CMD }
+  | "LET"           { LET_CMD }
+  | "let"           { LET_CMD }
   | "EVAL"          { EVAL_CMD }
   | "ELEM"          { ELEM_MOD }
   | "REL"           { REL_MOD }

Modified: trunk/Toss/Formula/Tokens.mly
===================================================================
--- trunk/Toss/Formula/Tokens.mly	2011-08-28 23:14:56 UTC (rev 1548)
+++ trunk/Toss/Formula/Tokens.mly	2011-08-29 21:08:20 UTC (rev 1549)
@@ -9,7 +9,7 @@
 %token OPENCUR CLOSECUR OPENSQ CLOSESQ OPEN CLOSE
 %token IN AND OR XOR NOT EX ALL TC
 %token WITH EMB  PRE INV POST UPDATE DYNAMICS TRUE FALSE ASSOC COND PAYOFF MOVES
-%token ADD_CMD DEL_CMD GET_CMD SET_CMD EVAL_CMD
+%token ADD_CMD DEL_CMD GET_CMD SET_CMD LET_CMD EVAL_CMD
 %token ELEM_MOD REL_MOD ALLOF_MOD SIG_MOD FUN_MOD DATA_MOD LOC_MOD TIMEOUT_MOD TIME_MOD PLAYER_MOD PLAYERS_MOD
 %token MODEL_SPEC RULE_SPEC STATE_SPEC LEFT_SPEC RIGHT_SPEC CLASS LFP GFP EOF
 

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





2010	Jan	Feb	Mar	Apr	May	Jun	Jul	Aug	Sep	Oct	Nov (25)	Dec (62)
2011	Jan (26)	Feb (38)	Mar (67)	Apr (22)	May (41)	Jun (30)	Jul (24)	Aug (32)	Sep (29)	Oct (34)	Nov (18)	Dec (2)
2012	Jan (19)	Feb (25)	Mar (16)	Apr (2)	May (18)	Jun (21)	Jul (11)	Aug	Sep	Oct	Nov	Dec

toss-devel-svn Mailing List for Toss (Page 9)

toss-devel-svn — Toss development: svn commits