[Toss-devel-svn] SF.net SVN: toss:[1716] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1716] trunk/Toss
|
From: <luk...@us...> - 2012-05-27 21:18:11
|
Revision: 1716
http://toss.svn.sourceforge.net/toss/?rev=1716&view=rev
Author: lukaszkaiser
Date: 2012-05-27 21:18:03 +0000 (Sun, 27 May 2012)
Log Message:
-----------
Defining structures using term rewriting systems and syntax.
Modified Paths:
--------------
trunk/Toss/Makefile
trunk/Toss/Solver/Structure.ml
trunk/Toss/Solver/Structure.mli
trunk/Toss/Solver/StructureTest.ml
trunk/Toss/Term/BuiltinLang.ml
trunk/Toss/Term/BuiltinLang.mli
trunk/Toss/Term/TRS.ml
trunk/Toss/Term/TRS.mli
trunk/Toss/Term/TRSTest.ml
trunk/Toss/Term/Term.ml
trunk/Toss/Term/Term.mli
trunk/Toss/Term/lib/arithmetics.trs
trunk/Toss/Term/lib/basic.trs
trunk/Toss/Term/tests/short_checks.log
trunk/Toss/Term/tests/short_checks.trs
trunk/Toss/www/codebasics.xml
trunk/Toss/www/index.xml
trunk/Toss/www/ocaml.xml
trunk/Toss/www/pub/fmt12_slides.pdf
trunk/Toss/www/upload_sourceforge.sh
Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Makefile 2012-05-27 21:18:03 UTC (rev 1716)
@@ -20,8 +20,8 @@
RELEASE=0.8
Release: TossServer doc
- rm -f *~ MenhirLib/*~ Formula/*~ Solver/*~ Arena/*~ Play/*~ GGP/*~ \
- Learn/*~ Language/*~ Server/*~ www/*~ WebClient/~
+ rm -f *~ MenhirLib/*~ Formula/*~ Term/*~ Solver/*~ Arena/*~ Play/*~ \
+ GGP/*~ Learn/*~ Server/*~ www/*~ WebClient/~
make -C www/reference
make -C www
make -C .
@@ -135,17 +135,17 @@
FormulaINCSatINC=MenhirLib,Formula
FormulaINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll
-SolverINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num
-SolverINCRealQuantElimINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num
-TermINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num
-ArenaINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Term
-PlayINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Term,Arena
-LearnINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Term,Arena
-GGPINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Term,Arena,Play
-ServerINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Term,Arena,Play,GGP,Learn
-ClientINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Term,Arena,Play,GGP,Learn,Server
+TermINC=Formula,Term
+SolverINC=MenhirLib,Term,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num
+SolverINCRealQuantElimINC=MenhirLib,Term,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num
+ArenaINC=MenhirLib,Term,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver
+PlayINC=MenhirLib,Term,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena
+LearnINC=MenhirLib,Term,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena
+GGPINC=MenhirLib,Term,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena,Play
+ServerINC=MenhirLib,Term,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena,Play,GGP,Learn
+ClientINC=MenhirLib,Term,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena,Play,GGP,Learn,Server
-.INC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Term,Arena,Play,GGP,Learn,Server
+.INC=MenhirLib,Term,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena,Play,GGP,Learn,Server
%.native: %.ml $(EXTDEPS)
$(OCAMLBUILD) -Is $($(subst /,INC,$(dir $@))) $@
@@ -276,8 +276,8 @@
clean:
ocamlbuild -clean
- rm -f Client/JsHandler.js
+ rm -f Client/*~ Client/JsHandler.js
rm -f *.cmx *.cmi *.o *.cmo *.a *.cmxa *.cma *.annot *~ TossServer
rm -f Formula/*~ Solver/*~ Arena/*~ Learn/*~ Play/*~ GGP/*~ Server/*~
rm -f caml_extensions/*.cmo caml_extensions/*.cmi Formula/Resources.ml
- rm -f Term/lib/*.trs.parsed
+ rm -f Term/*~ Term/lib/*.trs.parsed
Modified: trunk/Toss/Solver/Structure.ml
===================================================================
--- trunk/Toss/Solver/Structure.ml 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Solver/Structure.ml 2012-05-27 21:18:03 UTC (rev 1716)
@@ -213,6 +213,7 @@
else if e = -1 then add_new_elem struc ~name ()
else {struc with elements = Elems.add e struc.elements}, e
+
(* --------- ADDING RELATION TUPLES POSSIBLY WITH NAMED ELEMENTS ---------- *)
(* Ensure relation named [rn] exists in [struc], check arity, add the
@@ -511,6 +512,28 @@
let clear_fun struc fn =
{ struc with functions = StringMap.remove fn struc.functions }
+(* --- Structure operations by TRS --- *)
+
+let trs_set_struc s = function
+ | ("addrel", te_rel, te_arglist) ->
+ let rname = Term.decode_string te_rel in
+ let args = Term.decode_list Term.term_to_string te_arglist in
+ let (struc, args) = List.fold_left (fun (st, a) e ->
+ let (s1, i) = find_or_new_elem st e in (s1, i :: a)) (s, []) args in
+ add_rel struc rname (Array.of_list (List.rev args))
+ | (str, te, arg) when String.length str > 3 && String.sub str 0 3 = "fun" ->
+ let fname = String.sub str 3 ((String.length str) - 3) in
+ let (struc, i) = find_or_new_elem s (Term.term_to_string te) in
+ let v = Term.decode_bit_list arg in
+ add_fun struc fname (i, float v)
+ | _-> raise (Term.DECODE "Structure.trs_set_struc not a structure update set")
+
+let struc_from_trs str =
+ let (o, trs, _) = TRS.run_shell_str str in
+ let svals = TRS.set_vals_of_sys trs in
+ (o, List.fold_left trs_set_struc (empty_structure ()) svals)
+
+
(* ------------------------ PRINTING STRUCTURES ----------------------------- *)
Modified: trunk/Toss/Solver/Structure.mli
===================================================================
--- trunk/Toss/Solver/Structure.mli 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Solver/Structure.mli 2012-05-27 21:18:03 UTC (rev 1716)
@@ -273,7 +273,12 @@
(** Differing relations (used in solver cache) *)
val diffrels_struc: structure -> structure -> string list option
+(** {2 Creating a structure from a TRS string} *)
+(** Parse the TRS string, output messages and the resulting structure. *)
+val struc_from_trs : string -> string * structure
+
+
(** {2 Parser Helpers} *)
exception Board_parse_error of string
Modified: trunk/Toss/Solver/StructureTest.ml
===================================================================
--- trunk/Toss/Solver/StructureTest.ml 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Solver/StructureTest.ml 2012-05-27 21:18:03 UTC (rev 1716)
@@ -351,6 +351,26 @@
\"";
);
+ "struc from trs" >::
+ (fun () ->
+ let s = "
+ Load state library:/basic.
+ New function ''id'' natural number as natural number.
+ New variable n as natural number.
+ Let id n be n.
+ Elements from 0 to 5 at id {}, id {}.
+ New function ''succ'' natural number as natural number list.
+ Let succ n be n, n+1.
+ Relation R on from 0 to 4 given by succ {}.
+ " in
+ let (_, st) = struc_from_trs s in
+ assert_equal ~printer:(fun x -> x)
+ ("[F0_0\\, F1_0\\, F2, F3, F4, F5 | R {(F0_0\\, F1_0\\); (F1_0\\, F2);"^
+ " (F2, F3); (F3, F4); (F4, F5)} | x {F0_0\\->0., F1_0\\->1.," ^
+ " F2->2., F3->3., F4->4., F5->5.}; y {F0_0\\->0., F1_0\\->1.," ^
+ " F2->2., F3->3., F4->4., F5->5.}]") (Structure.str st);
+ );
+
"sprint simple" >::
(fun () ->
test_sprint
Modified: trunk/Toss/Term/BuiltinLang.ml
===================================================================
--- trunk/Toss/Term/BuiltinLang.ml 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/BuiltinLang.ml 2012-05-27 21:18:03 UTC (rev 1716)
@@ -271,7 +271,15 @@
Tp (list_tp string_tp)], remove_command_tp)
let system_remove_name = name_of_sd system_remove_sd
+let set_command_sd = SDtype ([Str "set"; Str "command"])
+let set_command_name = name_of_sd set_command_sd
+let set_command_tp = type_of_sd set_command_sd
+let set_prop_sd = SDfun ([Str "set"; Tp (string_tp); Str "of";
+ Tp (Type_var "a"); Str "to"; Tp (Type_var "b")], set_command_tp)
+let set_prop_name = name_of_sd set_prop_sd
+
+
let preprocess_sd =
SDfun ([Str "#"; Str "#"; Str "#"; Tp (Type_var "p")], Type_var "q")
let preprocess_name = name_of_sd preprocess_sd
Modified: trunk/Toss/Term/BuiltinLang.mli
===================================================================
--- trunk/Toss/Term/BuiltinLang.mli 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/BuiltinLang.mli 2012-05-27 21:18:03 UTC (rev 1716)
@@ -186,12 +186,18 @@
val close_context_sd : syntax_def
val close_context_name : string
-val remove_command_sd : syntax_def
+(*val remove_command_sd : syntax_def
val remove_command_name : string
val remove_command_tp : TermType.term_type
val system_remove_sd : syntax_def
-val system_remove_name : string
+val system_remove_name : string*)
+val set_command_sd : syntax_def
+val set_command_name : string
+val set_command_tp : TermType.term_type
+val set_prop_sd : syntax_def
+val set_prop_name : string
+
val preprocess_sd : syntax_def
val preprocess_name : string
Modified: trunk/Toss/Term/TRS.ml
===================================================================
--- trunk/Toss/Term/TRS.ml 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/TRS.ml 2012-05-27 21:18:03 UTC (rev 1716)
@@ -12,60 +12,64 @@
(* The system type which is a container for syntax definitions with
names, type declarations, rewrite rules and list of all used names.
For now it also has list of loaded file names to prevent double-loading. *)
-type trs = Sys of
- (syntax_def * string) list * (* Syntax definitions *)
- (string, term_type) Hashtbl.t * (* Types *)
- (term TermHashtbl.t * (* Memory used by normalisation *)
- (string, Rewriting.rrules_set) Hashtbl.t) * (* Rewriting rules *)
- string list * (* Used names *)
- (string * term_type) list (* Objects with types for chronologic access *)
+type trs = {
+ sdefs : (syntax_def * string) list; (* Syntax definitions *)
+ types : (string, term_type) Hashtbl.t; (* Types *)
+ mem : (term TermHashtbl.t); (* Memory used by normalisation *)
+ rrules : (string, Rewriting.rrules_set) Hashtbl.t; (* Rewriting rules *)
+ names : string list; (* Used names *)
+ hist : (string * term_type) list; (* Chronologic access *)
+ setvals: (string * term * term) list; (* Values set *)
+}
-
(* Get syntax definitions from a TRS. *)
-let syntax_defs_of_sys = function | Sys (sdefs, _, _, _, _) -> sdefs
+let syntax_defs_of_sys sys = sys.sdefs
+(* Get set values (chronologically) from a TRS. *)
+let set_vals_of_sys sys = List.rev sys.setvals
+
(* --- Updating the TRS --- *)
(* Updating the system when a new syntax definition appears. *)
-let update_on_sd sd = function Sys (sdefs, tdeclsh, (_, rrs), names, ts) ->
- let n = unique_name_of_sd sd names in
- let new_mem = TermHashtbl.create 512 in
+let update_on_sd sd sys =
+ let n = unique_name_of_sd sd sys.names in
let tds = match sd_type sd with
- | None -> ts
- | Some t -> (Hashtbl.add tdeclsh n t; (n, t) :: ts) in
+ | None -> sys.hist
+ | Some t -> (Hashtbl.add sys.types n t; (n, t) :: sys.hist) in
let add_sdefs = map (fun sd -> (sd, n)) (sd :: (func_sd_of_sd sd)) in
- Sys (add_sdefs @ sdefs, tdeclsh, (new_mem, rrs), n :: names, tds)
+ { sys with
+ sdefs = add_sdefs @ sys.sdefs;
+ mem = TermHashtbl.create 512;
+ names = n :: sys.names;
+ hist = tds }
(* Updating the system when a new rewrite rule appears. *)
-let update_on_rr rr = function Sys (sdefs, tdecls, (_, rrs), names, ts) ->
- let new_mem = TermHashtbl.create 512 in
- let new_rrs = match rr with
+let update_on_rr rr sys =
+ (match rr with
| (Term (f, a), r) ->
- (try let rs = Hashtbl.find rrs f in
- (Hashtbl.replace rrs f (add_last_rule rs rr); rrs)
- with Not_found -> (Hashtbl.add rrs f (new_rules_set [rr]); rrs) )
- | _ -> rrs in
- Sys (sdefs, tdecls, (new_mem, new_rrs), names, ts)
+ (try let rs = Hashtbl.find sys.rrules f in
+ Hashtbl.replace sys.rrules f (add_last_rule rs rr)
+ with Not_found -> Hashtbl.add sys.rrules f (new_rules_set [rr]) )
+ | _ -> ()
+ ); { sys with mem = TermHashtbl.create 512 }
(* Updating the system when a new priority rewrite rule appears. *)
-let update_on_prio_rr rr =
- function Sys (sdefs, tdecls, (_, rrs), names, ts) ->
- let new_mem = TermHashtbl.create 512 in
- let new_rrs = match rr with
- | (Term (f, a), r) ->
- (try let rs = Hashtbl.find rrs f in
- (Hashtbl.replace rrs f (add_first_rule rs rr); rrs)
- with Not_found -> (Hashtbl.add rrs f (new_rules_set [rr]); rrs) )
- | _ -> rrs in
- Sys (sdefs, tdecls, (new_mem, new_rrs), names, ts)
+let update_on_prio_rr rr sys =
+ (match rr with
+ | (Term (f, a), r) ->
+ (try let rs = Hashtbl.find sys.rrules f in
+ Hashtbl.replace sys.rrules f (add_first_rule rs rr)
+ with Not_found -> Hashtbl.add sys.rrules f (new_rules_set [rr]) )
+ | _ -> ()
+ ); { sys with mem = TermHashtbl.create 512 }
(* Update system when close context term appears - remove variables. *)
-let update_on_close_context_term te (Sys (sdefs, th, rrs, nms, tl) as sys) =
+let update_on_close_context_term te sys =
match te with
| Term (n, [||]) when n = close_context_name ->
- let nsdefs = filter (function (SDvar _, _) -> false | x -> true) sdefs in
- Sys (nsdefs, th, rrs, nms, tl)
+ let nsds = filter (function (SDvar _, _) -> false | _-> true) sys.sdefs in
+ { sys with sdefs = nsds }
| _ -> sys
(* Decoding paths and load commands. *)
@@ -77,27 +81,37 @@
| Term (n, [|s|]) when n = path_file_name -> decode_string s
| _ -> raise (DECODE "outside path")
-let decode_load_command kn_path = function
+let decode_load_cmd kn_path = function
| Term (n, [|p|]) when n = load_file_name -> decode_path kn_path p
| _ -> raise (DECODE "load command")
+(* Decode set command *)
+let decode_set_command = function
+ | Term (n, [|s; a; b|]) when n = set_prop_name ->
+ (decode_string s, a, b)
+ | _ -> raise (DECODE "set command")
+let update_on_set (s, a, b) sys =
+ { sys with setvals = (s, a, b) :: sys.setvals }
+
(* Update system when a new term appears.
It updates accordingly if the term is a syntax definition or rewrite rule,
loads file or closes context and does nothing in the other cases. *)
let update_on_coded_list te sys =
+ let upd_set l = fold_left (fun s sd -> update_on_set sd s) sys l in
let upd_sd l = fold_left (fun s sd -> update_on_sd sd s) sys l in
let upd_rr l = fold_left (fun s rr -> update_on_rr rr s) sys l in
let upd_prr l = fold_left (fun s rr -> update_on_prio_rr rr s) sys l in
- try upd_sd (decode_list decode_syntax_definition te) with
+ try upd_set (decode_list decode_set_command te) with
| DECODE _ ->
- try upd_rr (decode_list decode_input_rewrite_rule te) with
- | DECODE _ ->
+ try upd_sd (decode_list decode_syntax_definition te) with
+ | DECODE _ ->
try upd_prr (decode_list decode_priority_input_rewrite_rule te) with
- | DECODE _ ->
- try upd_rr (decode_list decode_rewrite_rule te) with
+ | DECODE _ ->
+ try upd_rr (decode_list decode_input_rewrite_rule te) with
| DECODE _ ->
- update_on_close_context_term te sys
+ try upd_rr (decode_list decode_rewrite_rule te) with
+ | DECODE _ -> update_on_close_context_term te sys
(* Update on file loading command. *)
@@ -112,23 +126,27 @@
) in
let fname = file ^ ".trs.parsed" in
process (ref bs) (Aux.split_newlines (AuxIO.input_file fname))
-and update_on_term k te sys bs =
- try update_on_sd (decode_syntax_definition te) sys with
+
+and update_on_term k te sys bs =
+ try update_on_set (decode_set_command te) sys with
| DECODE _ ->
- try update_on_rr (decode_input_rewrite_rule te) sys with
+ try update_on_sd (decode_syntax_definition te) sys with
| DECODE _ ->
try update_on_prio_rr (decode_priority_input_rewrite_rule te) sys with
| DECODE _ ->
- try update_on_rr (decode_rewrite_rule te) sys with
- | DECODE _ ->
- try update_on_load_file k (decode_load_command k te) sys bs
- with DECODE _ -> update_on_coded_list te sys
+ try update_on_rr (decode_input_rewrite_rule te) sys with
+ | DECODE _ ->
+ try update_on_rr (decode_rewrite_rule te) sys with
+ | DECODE _ ->
+ try update_on_load_file k (decode_load_cmd k te) sys bs
+ with DECODE _ -> update_on_coded_list te sys
(* --- Normalisation with meta-functions using the TRS --- *)
(* Getting elements from the system (recently added comes first). *)
-let get_elems_of_sys c (Sys (_, _, _, _, tdecls)) =
+let get_elems_of_sys c sys =
+ let tdecls = sys.hist in
let elem_of_td (n, ty) =
if n.[0] = c then
match ty with
@@ -139,8 +157,8 @@
let get_funs_of_sys = get_elems_of_sys 'F'
-let get_types_of_sys (Sys (sdefs, _, _, _, _)) =
- let classes = filter (function (SDtype _, _) -> true | _ -> false) sdefs in
+let get_types_of_sys sys =
+ let classes = filter (function (SDtype _, _) -> true | _-> false) sys.sdefs in
let get_tys sels = filter (function Tp _ -> true | _ -> false) sels in
let td_of_sd (sd, n) = (n, length (get_tys (syntax_elems_of_sd sd))) in
map td_of_sd classes
@@ -167,16 +185,16 @@
| Term (n, [||]) when n = get_fun_definitions_name ->
code_list code_fun_definition (get_funs_of_sys sys)
| te -> te
-and normalise_with_sys (Sys (_, _, (mem, rrs), _, _) as sys) te =
+and normalise_with_sys sys te =
(* This is the main normalisation function. *)
- normalise mem rrs is_special_fun (rewrite_special_funs sys) te
+ normalise sys.mem sys.rrules is_special_fun (rewrite_special_funs sys) te
(* --- Disambiguation for full parsing --- *)
(* Parse a string using the given system. *)
-let parse_with_sys (Sys (sdefs, tdecls, _, _, _)) str =
- let elems = parse tdecls sdefs (split_input_string str) in
+let parse_with_sys sys str =
+ let elems = parse sys.types sys.sdefs (split_input_string str) in
let type_of_pe = function Token _ -> [] | Typed_term (_, te) -> [te] in
flatten (map type_of_pe elems)
@@ -260,8 +278,10 @@
try Some (decode_priority_input_rewrite_rule te) with DECODE _ -> None
let decode_load_command_opt kn_path te =
- try Some (decode_load_command kn_path te) with DECODE _ -> None
+ try Some (decode_load_cmd kn_path te) with DECODE _ -> None
+let decode_set_opt te = try Some (decode_set_command te) with DECODE _ -> None
+
let msg_for_sels sels =
let i = ref 0 in
let msg = function
@@ -276,13 +296,16 @@
| DECODE _ ->
try let _ = decode_list decode_priority_input_rewrite_rule te in
("priority rewrite rules", false) with
- | DECODE _ ->
+ | DECODE _ ->
try let _ = decode_list decode_input_rewrite_rule te in
("rewrite rules", false) with
| DECODE _ ->
try let _ = decode_list decode_rewrite_rule te in
("rewrite rules", false) with
- | DECODE _ -> ("", false)
+ | DECODE _ ->
+ try let _=decode_list decode_set_command te
+ in ("set commands", false) with
+ | DECODE _ -> ("", false)
let display_rr (l, r) =
@@ -310,6 +333,9 @@
| (te, _) when is_some (decode_rr_opt te) ->
let rr = decode_rewrite_rule te in
msg "New rewrite rule defined.\n" (display_rr rr)
+ | (te, _) when is_some (decode_set_opt te) ->
+ let (s, k, v) = decode_set_command te in
+ msg "New value set." (s ^" ("^(display_term k)^" ) = "^(display_term v))
| (te, raw) when is_some (decode_irr_opt te) -> (
try
let rr = decode_input_rewrite_rule raw in
@@ -341,7 +367,7 @@
| (Term (n, [||]), _) when n = close_context_name ->
msg "Closed context." ""
| (te, _) when is_some (decode_load_command_opt k te) ->
- let path = decode_load_command k te in
+ let path = decode_load_cmd k te in
msg ("Loaded state " ^ path ^ ".") ""
| (te, _) ->
let ty = type_of_term tydecls te in
@@ -357,7 +383,7 @@
let process_with_system_bs lp verbose s str xml_out bs outprint =
match parse_disambiguate_with_sys verbose s str with
| [] ->
- let msg = "NO PARSE" in
+ let msg = ("NO PARSE: " ^ str) in
(if (not xml_out) then outprint msg else ();
raise (FAILED_PARSE_OR_EXN msg))
| [x] ->
@@ -367,9 +393,8 @@
let msg = "TRS EXCEPTION:\n" ^ (display_term a) ^ "\n" in
raise (FAILED_PARSE_OR_EXN msg)
| _ ->
- let Sys (_, tds, _, _, _) = s in
(update_on_term lp te s bs, [te],
- message_for_term tds lp verbose xml_out (te, x))
+ message_for_term s.types lp verbose xml_out (te, x))
)
| ts ->
let msg = "AMBIGUOUS\n" ^ (terms_info verbose ts) in
@@ -395,10 +420,10 @@
let_major_be_sd; fun_definition_sd; fun_definition_cons_sd;
type_definition_sd; type_of_sd_sd; brackets_sd; verbatim_sd; if_then_else_sd;
code_as_term_sd; get_type_definitions_sd; get_fun_definitions_sd;
- outside_paths_sd; path_library_sd; path_file_sd;
+ outside_paths_sd; path_library_sd; path_file_sd; set_command_sd; set_prop_sd;
load_command_sd; load_file_sd; preprocess_sd; sys_commands_sd;
close_context_sd; exception_cl_sd; exception_sd; exn_ok_sd; preferred_to_sd;
- additional_xslt_sd; string_quote_sd; eq_bool_sd]
+ additional_xslt_sd; string_quote_sd; eq_bool_sd]
let basic_rules = flatten [
brackets_rules; verbatim_rules; if_then_else_rules; preprocess_rules;
@@ -406,9 +431,15 @@
let basic_system () =
let upd sys sd = update_on_sd sd sys in
- let mem_rrs = (TermHashtbl.create 512, Hashtbl.create 512) in
- let emptys = Sys ([], Hashtbl.create 512, mem_rrs, [], []) in
- let system1 = fold_left upd emptys basic_sdefs in
+ let empty_sys = {
+ sdefs = [];
+ types = Hashtbl.create 512;
+ mem = TermHashtbl.create 512;
+ rrules = Hashtbl.create 512;
+ names = [];
+ hist = [];
+ setvals = []; } in
+ let system1 = fold_left upd empty_sys basic_sdefs in
let updr sys rr = update_on_rr rr sys in
fold_left updr system1 basic_rules
@@ -510,3 +541,28 @@
else outprint msg;
nsys
) else sys
+
+
+let rec run_shell lp v sys chann xmlo res outprint =
+ try
+ (sys := step_shell lp v !sys chann xmlo res outprint;
+ run_shell lp v sys chann xmlo res outprint)
+ with
+ | End_of_file -> ()
+ | FAILED_PARSE_OR_EXN msg ->
+ if xmlo then (
+ outprint "\n<trs-failure>\n";
+ outprint (make_xml_compatible msg);
+ outprint "\n</trs-failure>\n";
+ outprint "\n</trs-response>\n";
+ );
+ raise (FAILED_PARSE_OR_EXN msg)
+
+let run_shell_str ?(libpath="./Term/lib") str =
+ let s = ref str in
+ let rds () = if !s = "" then raise End_of_file else (
+ let c = !s.[0] in s := String.sub !s 1 ((String.length !s)-1); c) in
+ let o, sys, terms = ref "", ref (basic_system ()), ref [] in
+ let print_o str = o := !o ^ str ^ "\n" in
+ run_shell libpath false sys rds false terms print_o;
+ (!o, !sys, List.rev !terms)
Modified: trunk/Toss/Term/TRS.mli
===================================================================
--- trunk/Toss/Term/TRS.mli 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/TRS.mli 2012-05-27 21:18:03 UTC (rev 1716)
@@ -4,9 +4,13 @@
type trs
+(** Get syntax definitions from a TRS. *)
val syntax_defs_of_sys : trs -> (syntax_def * string) list
+(** Get set values (chronologically) from a TRS. *)
+val set_vals_of_sys : trs -> (string * Term.term * Term.term) list
+
(** {2 Operating on the TRS} *)
val update_on_term : string -> Term.term -> trs -> trs -> trs
@@ -34,3 +38,14 @@
should raise End_of_file on end of channel, as does input_char. *)
val step_shell : string -> bool -> trs -> (unit -> char) ->
bool -> Term.term list ref -> (string -> unit) -> trs
+
+(** A full run of the TRS computation. The channel (unit -> char) argument
+ should raise End_of_file on end of channel, as does input_char.
+ The trs reference gets updated to the result, and the term list reference
+ to the list of parsed terms. *)
+val run_shell : string -> bool -> trs ref -> (unit -> char) ->
+ bool -> Term.term list ref -> (string -> unit) -> unit
+
+(** Simplified interface to TRS computation, returns the messages,
+ resulting system and the list of parsed terms, chronologically. *)
+val run_shell_str: ?libpath: string -> string -> (string * trs * Term.term list)
Modified: trunk/Toss/Term/TRSTest.ml
===================================================================
--- trunk/Toss/Term/TRSTest.ml 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/TRSTest.ml 2012-05-27 21:18:03 UTC (rev 1716)
@@ -4,55 +4,14 @@
open Term
open TRS
open SyntaxDef
-
open OUnit
-let rec run lp v grammar_path xslt_path out_path sys chann xmlo res outprint =
- let save_parsed () =
- let parsed_strs = map term_to_string (rev !res) in
- AuxIO.output_file ~fname:out_path ((String.concat "\n" parsed_strs)^"\n") in
- let save_xslt () =
- let addon_term = Term (BuiltinLang.additional_xslt_name, [||]) in
- let addon_str = decode_string (normalise_with_sys !sys addon_term) in
- let xslt_str = print_xslt addon_str (syntax_defs_of_sys !sys) in
- AuxIO.output_file ~fname:xslt_path xslt_str in
- let save_grammar () =
- let grammar_str =
- let sys_sdefs = fst (List.split (syntax_defs_of_sys !sys)) in
- print_grammar (flat_grammar_of_sd_list (sys_sdefs)) in
- AuxIO.output_file ~fname:grammar_path grammar_str in
- let save_requested () = (
- if (not (grammar_path = "")) then save_grammar () else ();
- if (not (xslt_path = "")) then save_xslt () else ();
- if (not (out_path = "")) then save_parsed () else ();
- ) in
- try
- (sys := step_shell lp v !sys chann xmlo res outprint;
- run lp v grammar_path xslt_path out_path sys chann xmlo res outprint)
- with
- | End_of_file -> save_requested ();
- | FAILED_PARSE_OR_EXN msg ->
- (save_requested ();
- if xmlo then
- (outprint "\n<trs-failure>\n";
- outprint (make_xml_compatible msg);
- outprint "\n</trs-failure>\n";
- outprint "\n</trs-response>\n";)
- else ();
- failwith msg)
-
-
let test fname =
- let s = ref (AuxIO.input_file ("./Term/tests/" ^ fname ^ ".trs")) in
- let read_s () = if !s = "" then raise End_of_file else (
- let c = !s.[0] in s := String.sub !s 1 ((String.length !s)-1); c) in
- let o = ref "" in
- let print_o str = o := !o ^ str ^ "\n" in
- run "./Term/lib" false "" "" "" (ref (basic_system ())) read_s false (ref [])
- print_o;
+ let s = AuxIO.input_file ("./Term/tests/" ^ fname ^ ".trs") in
+ let (o, _, _) = run_shell_str s in
assert_equal ~printer:(fun x -> x) (Aux.normalize_spaces (
AuxIO.input_file ("./Term/tests/" ^ fname ^ ".log")))
- (Aux.normalize_spaces !o)
+ (Aux.normalize_spaces o)
let tests = "TRS" >::: [
"basic operation" >::
@@ -69,6 +28,15 @@
assert_equal ~printer:(fun x -> x) "Result: {[] as ?a._.5 list}" m;
);
+ "simple parsing" >::
+ (fun () ->
+ let s = "Load state library:/basic.\n From 0 to 5." in
+ let (o, _, _) = run_shell_str s in
+ assert_equal ~printer:(fun x->x)
+ ("Loaded state ./Term/lib/basic.\n\n" ^
+ "Result: {[0, 1, 2, 3, 4, 5] as natural number list}\n") o;
+ );
+
"test short_checks" >::
(fun () -> test "short_checks";);
]
@@ -113,19 +81,33 @@
if !lib_path = "N/O/N/I/N/T/E/R" then
ignore (OUnit.run_test_tt ~verbose:true tests)
else (
- let parsed_terms = ref [] in
- let basic_sys = ref (basic_system ()) in
+ let parsed_terms, sys = ref [], ref (basic_system ()) in
if !builtin_out then
let defs = String.concat "\n" (map pretty_print_sd basic_sdefs) in
AuxIO.print ("// TRS BUILT-IN DEFS.\n" ^ defs ^ "\n\n")
else (
if (!xml_out) then AuxIO.print "<trs-response>\n" else ();
- run !lib_path !verbose !grammar_path !xslt_path !out_path basic_sys
- AuxIO.input_stdin_char !xml_out parsed_terms
- (fun s -> AuxIO.print s; AuxIO.print "\n");
+ run_shell !lib_path !verbose sys AuxIO.input_stdin_char !xml_out
+ parsed_terms (fun s -> AuxIO.print s; AuxIO.print "\n");
+ if not (!out_path = "") then (
+ let parsed_strs = map term_to_string (rev !parsed_terms) in
+ AuxIO.output_file ~fname:!out_path
+ ((String.concat "\n" parsed_strs) ^ "\n");
+ );
+ if (not (!grammar_path = "")) then (
+ let grammar_str =
+ let sys_sdefs = fst (List.split (syntax_defs_of_sys !sys)) in
+ print_grammar (flat_grammar_of_sd_list (sys_sdefs)) in
+ AuxIO.output_file ~fname:!grammar_path grammar_str
+ );
+ if (not (!xslt_path = "")) then (
+ let addon_term = Term (BuiltinLang.additional_xslt_name, [||]) in
+ let addon_str = decode_string (normalise_with_sys !sys addon_term) in
+ let xslt_str = print_xslt addon_str (syntax_defs_of_sys !sys) in
+ AuxIO.output_file ~fname:!xslt_path xslt_str
+ );
if (!xml_out) then AuxIO.print "</trs-response>\n" else ();
)
)
-
let _ = AuxIO.run_if_target "TRSTest" main
Modified: trunk/Toss/Term/Term.ml
===================================================================
--- trunk/Toss/Term/Term.ml 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/Term.ml 2012-05-27 21:18:03 UTC (rev 1716)
@@ -72,6 +72,7 @@
| Term (n, [||]) when n = bit_1_cons_name -> 1
| _ -> raise (DECODE "bit")
+let decode_bit_list bl = bits_to_int (decode_list decode_bit bl)
let code_char c =
let bits = int_to_bits (Char.code c) in
@@ -79,13 +80,11 @@
let eight_bits = bits @ zeros (8 - List.length bits) in
Term (char_cons_name, of_list (List.map code_bit eight_bits))
-
let decode_char = function
| Term (n, bits) when n = char_cons_name ->
Char.chr (bits_to_int (to_list (map decode_bit bits)))
| _ -> raise (DECODE "char")
-
let code_string s =
let rec char_list i = if i < 0 then [] else s.[i] :: char_list (i-1) in
let chars = List.rev (char_list ((String.length s) - 1)) in
Modified: trunk/Toss/Term/Term.mli
===================================================================
--- trunk/Toss/Term/Term.mli 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/Term.mli 2012-05-27 21:18:03 UTC (rev 1716)
@@ -39,6 +39,7 @@
val bits_to_int : int list -> int
val code_bit : int -> term
val decode_bit : term -> int
+val decode_bit_list : term -> int
val code_char : char -> term
val decode_char : term -> char
val code_string : string -> term
Modified: trunk/Toss/Term/lib/arithmetics.trs
===================================================================
--- trunk/Toss/Term/lib/arithmetics.trs 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/lib/arithmetics.trs 2012-05-27 21:18:03 UTC (rev 1716)
@@ -89,6 +89,12 @@
New variable m' as binary number.
New variable k' as binary number.
+New function ''to_bits'' ''('' binary number '')'' as bit list.
+Let to_bits (0) be [bit 0].
+Let to_bits (1) be [bit 1].
+Let to_bits (n0) be bit 0, to_bits (n).
+Let to_bits (n1) be bit 1, to_bits (n).
+
New function binary number ''+'' binary number as binary number.
See (n+(m0)) preferred to (n'+m')0.
See (n+(m1)) preferred to (n'+m')1.
@@ -427,6 +433,9 @@
as natural number.
Let min (k, n) be if k <= n then k else n.
+Function ''from'' natural number ''to'' natural number as natural number list.
+Let from n to m be if m < n then [] else n, from n+1 to m.
+
Close context.
Modified: trunk/Toss/Term/lib/basic.trs
===================================================================
--- trunk/Toss/Term/lib/basic.trs 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/lib/basic.trs 2012-05-27 21:18:03 UTC (rev 1716)
@@ -2,4 +2,35 @@
Load state library:/lists.
+// SET COMMANDS FOR ELEMENTS AND RELATIONS IN STRUCTURES.
+New variable x as ?a.
+New variable n as natural number.
+New variable m as natural number.
+New function ''put'' ?a ''at'' natural number '','' natural number
+ as set command list.
+Let put x at n, m be set funx of x to to_bits (to_binary (n)),
+ set funy of x to to_bits (to_binary (m)).
+
+New function ''elements'' ?a list ''at'' funtype [?a] -> natural number
+ '','' funtype [?a] -> natural number as set command list.
+New variable ''f'' ''('' ?a '')'' as natural number.
+New variable ''g'' ''('' ?a '')'' as natural number.
+New variable l as ?a list.
+Let elements [] at f({}), g({}) be [].
+Let elements x, l at f({}), g({}) be
+ put x at f(x), g(x) + elements l at f({}), g({}).
+
+Close context.
+
+New function ''relation'' string ''on'' ?a list ''given'' ''by''
+ funtype [?a] -> (?a list) as set command list.
+New variable s as string.
+New variable ''f'' ''('' ?a '')'' as ?a list.
+New variable x as ?a.
+New variable l as ?a list.
+Let relation s on [] given by f ({}) be [].
+Let relation s on x, l given by f ({}) be
+ set addrel of s to f(x), relation s on l given by f({}).
+
+Close context.
Modified: trunk/Toss/Term/tests/short_checks.log
===================================================================
--- trunk/Toss/Term/tests/short_checks.log 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/tests/short_checks.log 2012-05-27 21:18:03 UTC (rev 1716)
@@ -58,6 +58,11 @@
Result: {false as boolean}
+// SETTING STRUCTURE ELEMENTS BASIC TEST.
+
+Processed multiple set commands from:
+ put ""a"" at 10 , 20.
+
// LISTS TEST.
New function "swap" "(" X_1 ")" declared.
Modified: trunk/Toss/Term/tests/short_checks.trs
===================================================================
--- trunk/Toss/Term/tests/short_checks.trs 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/Term/tests/short_checks.trs 2012-05-27 21:18:03 UTC (rev 1716)
@@ -37,7 +37,10 @@
apply dbn {} 18.
+// SETTING STRUCTURE ELEMENTS BASIC TEST.
+Put "a" at 10, 20.
+
// LISTS TEST.
New function ''swap('' boolean '')'' as boolean.
Modified: trunk/Toss/www/codebasics.xml
===================================================================
--- trunk/Toss/www/codebasics.xml 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/www/codebasics.xml 2012-05-27 21:18:03 UTC (rev 1716)
@@ -15,17 +15,22 @@
and the last one contains the main executable and uses all previous ones.
<itemize>
<item><em>Formula</em> contains the type definition for formulas and
- functions which operate on formulas only — substitutions for
- variables, normal forms, simplifications, parsing and printing.
- We also keep the module <em>Aux</em>, with many useful auxiliary
- functions, in this directory.
+ functions which operate on formulas only — substitutions for
+ variables, normal forms, simplifications, parsing and printing.
+ We also keep the module <em>Aux</em>, with many useful auxiliary
+ functions, in this directory.
</item>
+ <item><em>Term</em> contains the type definition for typed terms and
+ functions for term rewriting, type reconstruction and type-aware parsing.
+ It also contains a basic term rewriting language which is then used for
+ example for defining structures.
+ </item>
<item><em>Solver</em> directory contains type definitions for structures,
- variable assignments to structure elements, and the solver module for
- calculating the assignments which satisfy a formula on
- a structure.
+ variable assignments to structure elements, and the solver module for
+ calculating the assignments which satisfy a formula on
+ a structure.
</item>
- <item><em>Arena</em> is the directory in which we define structure
+ <item><em>Arena</em> is the directory in which we define structure
rewriting games — discrete and continuous rewriting rules first,
and finally the whole games in the <em>Arena</em> module.
Discrete rule application is handled in the <em>DiscreteRule</em> module
@@ -33,27 +38,29 @@
is split into the <em>Term</em> module and <em>ContinuousRule</em>.
The parser for complete Toss games, i.e. the <em>.toss</em> files,
is defined in <em>ArenaParser.mly</em>.
- </item>
- <item><em>Play</em> contains the modules related to making Toss play
+ </item>
+ <item><em>Play</em> contains the modules related to making Toss play
any defined game automatically — we generate heuristics in
the <em>Heuristic</em> module and use <em>GameTree</em> to implement
a search to finally <em>Play</em>.
- </item>
- <item><em>GGP</em> is a directory devoted to translating games in the GDL
+ </item>
+ <item><em>GGP</em> is a directory devoted to translating games in the GDL
language (Game Description Language) to the Toss format. We implement
GDL parsing, basic operations, stepwise translation and finally some
simplification of the resulting games. There are also tests in the
<em>GGP/examples</em> sub-directory.
- </item>
- <item><em>Language</em> is not used for now, we keep it because we plan
- to experiment with better syntax for Toss in the future.
- </item>
- <item><em>Server</em> contains the main executable of Toss (in the file
+ </item>
+ <item><em>Learn</em> contains the algorithm for differentiating structures
+ by formulas of various logics, which is then used to learn games from
+ example plays. We also keep there a program to recognize plays from
+ videos, which allows to go from video demonstrations to game playing.
+ </item>
+ <item><em>Server</em> contains the main executable of Toss (in the file
<em>Server.ml</em>) and the main request handler in the
<em>ReqHandler</em> module, with other files as needed
(e.g. database connection handler in <em>DB</em>). We also keep
the lists of all unit tests there, in <em>Server/Tests.ml</em>.
- </item>
+ </item>
</itemize>
The command <em>make TossFullTest</em> runs all unit tests for all modules
from all directories. As this takes some time, we often execute only
@@ -70,7 +77,7 @@
so if you intend to only operate on formulas, you should add your module
to the <em>Formula</em> directory. If you want to be able to use all
functions of Toss (or just not worry about the dependencies for now),
- add your module to the <em>Server</em> directory, which incldues all
+ add your module to the <em>Server</em> directory, which includes all
other directories in its dependency list.<br/>
As a starting example, let's add a module that parses a formula and
a structure from strings and returns a print-out of the satisfying
Modified: trunk/Toss/www/index.xml
===================================================================
--- trunk/Toss/www/index.xml 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/www/index.xml 2012-05-27 21:18:03 UTC (rev 1716)
@@ -35,6 +35,8 @@
<section title="News">
<itemize>
+ <newsitem date="27/05/12">
+ First structures defined using the term rewriting system syntax</newsitem>
<newsitem date="24/05/12">
Code for Term functions cleaned up and made JS compatible</newsitem>
<newsitem date="13/05/12">
Modified: trunk/Toss/www/ocaml.xml
===================================================================
--- trunk/Toss/www/ocaml.xml 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/www/ocaml.xml 2012-05-27 21:18:03 UTC (rev 1716)
@@ -12,7 +12,7 @@
<section title="Task: Simple Formula Library">
We think it is best to illustrate the problems encountered and how we
- decided to organise code in Toss on an example task. In this
+ decided to organize code in Toss on an example task. In this
tutorial, we will build a very simple program to manipulate propositional
formulas. Let's state the task as follows: <em>Build a program to
compute the NNF of formulas given on input.</em> We will construct the
@@ -76,7 +76,7 @@
</section>
<section title="Step 3 — Lexer and Parser">
- To allow the user to input formuas, we have to construct a lexer and
+ To allow the user to input formulas, we have to construct a lexer and
a parser. We will not do it by hand, but use a parser generator called
<a href="http://gallium.inria.fr/~fpottier/menhir/">menhir</a>. Here is
the simple lexer file we use for lexing formulas.
@@ -345,19 +345,19 @@
functions <em>formula_of_string</em> and <em>nnf</em> as in previous steps.
The only difference is that we have to convert from JavaScript strings to
OCaml with <em>Js.to_string</em> and back with <em>Js.string</em>. In the
- last line, we regiser the <em>js_nnf</em> OCaml function under the name
+ last line, we register the <em>js_nnf</em> OCaml function under the name
<em>nnf</em> in JavaScript. It is then called in JavaScript using the
invocation <em>ASYNCH ("nnf", [args], continuation)</em>, as shown above in
the <em>index.html</em> file. Here is how we compile <em>JsClient.ml</em>.
<pre>
-camlbuild -use-menhir -menhir "menhir --external-tokens Lexer" \
+ocamlbuild -use-menhir -menhir "menhir --external-tokens Lexer" \
-pp "camlp4o -I /opt/local/lib/ocaml/site-lib js_of_ocaml/pa_js.cmo" \
-cflags -I,+js_of_ocaml,-I,+site-lib/js_of_ocaml -libs js_of_ocaml \
-lflags -I,+js_of_ocaml,-I,+site-lib/js_of_ocaml JsClient.byte
js_of_ocaml JsClient.byte
</pre>
Note that the first command is just a standard ocamlbuild call, only this
- time we compile to bytcode, not to a native executable, and we use the
+ time we compile to bytecode, not to a native executable, and we use the
preprocessor that comes with js_of_ocaml (used e.g. in the call
<em>event##data##args</em>). The second command invokes <em>js_of_ocaml</em>
and compiles the bytecode to a JavaScript file <em>JsClient.js</em>.
Modified: trunk/Toss/www/pub/fmt12_slides.pdf
===================================================================
--- trunk/Toss/www/pub/fmt12_slides.pdf 2012-05-26 22:28:13 UTC (rev 1715)
+++ trunk/Toss/www/pub/fmt12_slides.pdf 2012-05-27 21:18:03 UTC (rev 1716)
@@ -3727,22 +3727,15 @@
/Filter /FlateDecode
>>
stream
-x\xDA\xC5XMo\xE36\xBD\xE7W\xF0(\xC3\xEF\x8FܲE\xEC\xB6(\xBAY=\xA4{\xD0ڌ \xAC-\xA5\xB1\xD2\xFD\xFB \x8A\x92cɲ\xB4\x86\xB8( [\x94E\xCE{ \xCE\xE3\x8CH\xD0twEzW
-W
-\xD7\xE0 \x82\xB8b\xD8p\x89\x98f\x982\x85^ z\xBC\xFAx2\xE8\xFF\xBA\xB6dO\x9Ec\x85\xC2W\xE75\xEA\xDC\xDF\xFF |
