[Toss-devel-svn] SF.net SVN: toss:[1710] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1710] trunk/Toss
|
From: <luk...@us...> - 2012-05-19 21:37:26
|
Revision: 1710
http://toss.svn.sourceforge.net/toss/?rev=1710&view=rev
Author: lukaszkaiser
Date: 2012-05-19 21:37:16 +0000 (Sat, 19 May 2012)
Log Message:
-----------
Moving ODE from Term to Formula as expected, adjusting examples and tests, making old speagram left-linear.
Modified Paths:
--------------
trunk/Toss/Arena/Arena.ml
trunk/Toss/Arena/ArenaParser.mly
trunk/Toss/Arena/ContinuousRule.ml
trunk/Toss/Arena/ContinuousRule.mli
trunk/Toss/Arena/ContinuousRuleParser.mly
trunk/Toss/Arena/ContinuousRuleTest.ml
trunk/Toss/Formula/Formula.ml
trunk/Toss/Formula/Formula.mli
trunk/Toss/Formula/FormulaParser.mly
trunk/Toss/Formula/FormulaTest.ml
trunk/Toss/Language/BuiltinLang.ml
trunk/Toss/Language/BuiltinLang.mli
trunk/Toss/Language/Makefile
trunk/Toss/Language/ParseArc.ml
trunk/Toss/Language/ParseArc.mli
trunk/Toss/Language/Rewriting.ml
trunk/Toss/Language/Rewriting.mli
trunk/Toss/Language/SyntaxDef.ml
trunk/Toss/Language/SyntaxDef.mli
trunk/Toss/Language/System.ml
trunk/Toss/Language/System.mli
trunk/Toss/Language/Term.ml
trunk/Toss/Language/Term.mli
trunk/Toss/Language/Type.ml
trunk/Toss/Language/Type.mli
trunk/Toss/Language/library/Makefile
trunk/Toss/Language/library/arithmetics.spg
trunk/Toss/Language/library/core.spg
trunk/Toss/Language/library/lists.spg
trunk/Toss/Language/speagram.ml
trunk/Toss/Language/testsuite/differentiation.log
trunk/Toss/Language/testsuite/differentiation.spg
trunk/Toss/Language/testsuite/short_checks.log
trunk/Toss/Language/testsuite/simple_algo.log
trunk/Toss/Language/testsuite/simple_algo.spg
trunk/Toss/examples/Bounce.toss
trunk/Toss/examples/Cell-Cycle-Tyson-1991.toss
trunk/Toss/examples/Rewriting-Example.toss
trunk/Toss/menhir_conf
Removed Paths:
-------------
trunk/Toss/Arena/Term.ml
trunk/Toss/Arena/Term.mli
trunk/Toss/Arena/TermParser.mly
trunk/Toss/Arena/TermTest.ml
trunk/Toss/Language/Normalisation.ml
trunk/Toss/Language/Normalisation.mli
Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Arena/Arena.ml 2012-05-19 21:37:16 UTC (rev 1710)
@@ -95,7 +95,7 @@
f ^ ": " ^ (string_of_float fs) ^ " -- " ^ (string_of_float fe) in
let par_str = if param_intervals = [] then " " else
", " ^ (String.concat ", " (List.map fpstr param_intervals)) in
- (rr) ^ ", " ^ fpstr ("t", t_interval) ^ par_str
+ (rr) ^ ", " ^ fpstr (":t", t_interval) ^ par_str
(* Print a move as string. *)
let move_str (lb, i) = Printf.sprintf "[%s -> %i]" (label_str lb) i
@@ -112,11 +112,11 @@
lb_rule=r; time_in=(t_l, t_r); parameters_in=params}, target) ->
Format.fprintf f "[@,@[<1>%s" r;
if t_l <> cDEFAULT_TIMESTEP || t_r <> cDEFAULT_TIMESTEP then
- Format.fprintf f ",@ @[<1>t:@ %F@ --@ %F@]" t_l t_r;
+ Format.fprintf f ",@ @[<1>:t@ :@ %F@ --@ %F@]" t_l t_r;
if params <> [] then
Format.fprintf f ",@ %a"
(Aux.fprint_sep_list "," (fun f (pn, (p_l, p_r)) ->
- Format.fprintf f "@[<1>%s:@ %F@ --@ %F@]" pn p_l p_r)) params;
+ Format.fprintf f "@[<1>%s@ :@ %F@ --@ %F@]" pn p_l p_r)) params;
Format.fprintf f "@ ->@ %d@]@,]" target)) moves
) (in_p, in_m)
@@ -139,7 +139,7 @@
Format.fprintf f "@[<1>[%s@ %F@ ->@ %i@ emb@ %s]%s@]" rn t l m_s rt
else (
let p_s = String.concat ", "
- (List.map (fun (p, v) -> Printf.sprintf "%s: %F" p v) pl) in
+ (List.map (fun (p, v) -> Printf.sprintf "%s : %F" p v) pl) in
Format.fprintf f "@[<1>[%s@ %F,@ %s@ ->@ %i@ emb@ %s]%s@]" rn t p_s l m_s rt
)
@@ -303,7 +303,7 @@
let make_move_arena rname params target_loc =
let time_in, parameters_in =
- try Aux.pop_assoc "t" params
+ try Aux.pop_assoc ":t" params
with Not_found -> (cDEFAULT_TIMESTEP, cDEFAULT_TIMESTEP), params in
{ lb_rule = rname;
time_in = time_in;
Modified: trunk/Toss/Arena/ArenaParser.mly
===================================================================
--- trunk/Toss/Arena/ArenaParser.mly 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Arena/ArenaParser.mly 2012-05-19 21:37:16 UTC (rev 1710)
@@ -23,10 +23,13 @@
| ID { $1 }
| INT { string_of_int $1 }
+param:
+ | COLON ID { ":" ^ $2 }
+
move:
| OPENSQ RULE_SPEC? r = id_int COMMA?
params = separated_list (
- COMMA, separated_pair (ID, COLON,
+ COMMA, separated_pair (param, COLON,
separated_pair (FLOAT, INTERV, FLOAT)))
RARR LOC_MOD? target = INT CLOSESQ
{ make_move_arena r params target }
Modified: trunk/Toss/Arena/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Arena/ContinuousRule.ml 2012-05-19 21:37:16 UTC (rev 1710)
@@ -10,11 +10,9 @@
(* Specification of a continuous rewriting rule, as in modelling document. *)
type rule = {
- discrete : DiscreteRule.rule; (* The discrete part *)
- dynamics : ((string * string) * Term.term) list; (* Equation system calD *)
- update : ((string * string) * Formula.real_expr) list;
- (* Update equations calT *)
- (* Note that, for efficiency, the precondition is part of DiscreteRule. *)
+ discrete : DiscreteRule.rule; (* The discrete part, with precondition *)
+ dynamics : ((string * string) * Formula.real_expr) list; (* Equations calD *)
+ update : ((string * string) * Formula.real_expr) list; (* Update eqs calT*)
inv : Formula.formula; (* Invariant for the evolution *)
post : Formula.formula; (* Postcondition for application *)
}
@@ -90,10 +88,13 @@
(* Differential equations for a rule and a match, renamed to structure names. *)
let rule_dynamics struc params (r, m) =
- let (p_vars, t_vals) = params in
- let subst_params tm = List.hd (Term.subst_simp p_vars t_vals [tm]) in
+ let subst_params tm = FormulaSubst.subst_real params tm in
let d = List.map (fun (lhs, rhs) -> (lhs, subst_params rhs)) r.dynamics in
- Term.subst_names (List.map (fun (a,i)-> (a, Structure.elem_name struc i)) m) d
+ let subst_names subst ((v, e), rhs) =
+ let replace a = try List.assoc a subst with Not_found -> a in
+ ((v, replace e), FormulaSubst.subst_vars_expr subst rhs) in
+ let subst_names_l subst l = List.map (subst_names subst) l in
+ subst_names_l (List.map (fun (a,i)-> (a, Structure.elem_name struc i)) m) d
(* Construct diff equation system and initial values for dynamics. *)
let construct_dynamics struc params rms =
@@ -101,12 +102,13 @@
let rec sum_common = function
| [] -> []
| (x, t) :: (y, s) :: rest when x = y ->
- sum_common ((x, Term.Plus (t, s)) :: rest)
+ sum_common ((x, Formula.Plus (t, s)) :: rest)
| eq :: rest-> eq :: (sum_common rest) in
let cmp ((f, x), t) ((g, y), s) =
let c = String.compare f g in if c <> 0 then c else
- let d = String.compare x y in if d <> 0 then d else Term.compare t s in
- let dyn = Term.subst_simp_eq [] [] (sum_common (List.sort cmp dyns)) in
+ let d = String.compare x y in if d <> 0 then d else
+ Formula.compare_re t s in
+ let dyn = sum_common (List.sort cmp dyns) in
(*LOG 1 "%s" (Term.eq_str dyn);*)
let fval f e = Structure.fun_val struc f (Structure.elem_nbr struc e) in
let init_vals = List.map (fun ((f, a), _) -> fval f a) dyn in
@@ -117,18 +119,18 @@
let rewrite_single_nocheck struc univs cur_time m r t params =
let univ_mts = Aux.concat_map
(fun r -> List.map (fun m -> (r, m)) (matches struc r)) univs in
- let tparams =
- let p_vars, p_vals = List.split params in
- (p_vars, List.map (fun f -> Term.Const f) p_vals) in
+ let tparams = List.map (fun (v, f) -> (v, Formula.Const f)) params in
+ (*let p_vars, p_vals = List.split params in
+ (p_vars, List.map (fun f -> Term.Const f) p_vals) in *)
let (dyn, init_vals) = construct_dynamics struc tparams ((r,m) :: univ_mts) in
- let dyn_c = Term.compile "t" dyn in
+ let dyn_c = Formula.compile ":t" dyn in
LOG 1 "current time: %f" cur_time;
let time = ref cur_time in
let diff_step, t_mod_diff = !time_step /. (float_of_int dIFFM), ref 0 in
let step vals t0 =
(*LOG 1 "step at time %s" (Term.str t0);
LOG 2 "%s" (Term.eq_str (List.combine (List.map fst dyn) vals));*)
- Term.rk4_step_c t0 diff_step dyn_c vals in
+ Formula.rk4_step t0 diff_step dyn_c vals in
(* add the trace of the embedding to the structure, for invariants *)
let cur_struc = ref (List.fold_left (fun s (le, se) ->
Structure.add_rel s ("_lhs_" ^ le) [|se|]) struc m) in
@@ -218,7 +220,7 @@
(DiscreteRule.fprint_full print_compiled) r.discrete;
if has_dynamics r then
Format.fprintf f "@ @[<hv>dynamics@ %a@]"
- (Term.fprint_eqs ~diff:true) (List.sort Pervasives.compare r.dynamics);
+ (Formula.fprint_eqs ~diff:true) (List.sort Pervasives.compare r.dynamics);
if has_update r then
Format.fprintf f "@ @[<hv>update@ %a@]"
(Formula.fprint_eqs ~diff:false) (List.sort Pervasives.compare r.update);
Modified: trunk/Toss/Arena/ContinuousRule.mli
===================================================================
--- trunk/Toss/Arena/ContinuousRule.mli 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Arena/ContinuousRule.mli 2012-05-19 21:37:16 UTC (rev 1710)
@@ -10,7 +10,7 @@
Function named foo on element i is, in a term, given by variable foo_i. *)
type rule = {
discrete : DiscreteRule.rule; (** The discrete part *)
- dynamics : Term.eq_sys; (** Equation system calD *)
+ dynamics : Formula.eq_sys; (** Equation system calD *)
update : Formula.eq_sys; (** Update equations calT *)
(** Note that, for efficiency, the precondition is part of DiscreteRule. *)
inv : Formula.formula; (** Invariant for the evolution *)
@@ -21,7 +21,7 @@
val make_rule :
(string * (string list * Formula.formula)) list -> (** defined rels *)
(DiscreteRule.rule) ->
- Term.eq_sys -> Formula.eq_sys ->
+ Formula.eq_sys -> Formula.eq_sys ->
?inv:Formula.formula ->
?post:Formula.formula -> unit -> rule
Modified: trunk/Toss/Arena/ContinuousRuleParser.mly
===================================================================
--- trunk/Toss/Arena/ContinuousRuleParser.mly 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Arena/ContinuousRuleParser.mly 2012-05-19 21:37:16 UTC (rev 1710)
@@ -25,7 +25,7 @@
%public rule_expr:
| discr = discrete_rule_expr
- dyn = loption (preceded (DYNAMICS, eq_sys))
+ dyn = loption (preceded (DYNAMICS, expr_eq_sys))
upd = loption (preceded (UPDATE, expr_eq_sys))
pre = option (preceded (PRE, precond_expr))
inv = option (preceded (INV, formula_expr))
Modified: trunk/Toss/Arena/ContinuousRuleTest.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRuleTest.ml 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Arena/ContinuousRuleTest.ml 2012-05-19 21:37:16 UTC (rev 1710)
@@ -43,12 +43,12 @@
let r = rule_of_str s signat [] "rule2" in
eq_str "2. update" s (str r);
- let dyn_eq = ":f(a)' = 2. * :f(a) + t; :f(b)' = :f(b)" in
+ let dyn_eq = ":f(a)' = 2. * :f(a) + :t; :f(b)' = :f(b)" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq in
let r = rule_of_str s signat [] "rule3" in
eq_str "3. dynamics" s (str r);
- let dyn_eq = ":f(a)' = 2. * :f(a) + t; :f(b)' = :f(b)" in
+ let dyn_eq = ":f(a)' = 2. * :f(a) + :t; :f(b)' = :f(b)" in
let upd_eq = " :f(c) = 2. * :f(a);\n :f(d) = :f(b)\n" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ "\nupdate\n" ^ upd_eq in
let r = rule_of_str s signat [] "rule4" in
@@ -71,7 +71,7 @@
let r = rule_of_str s signat [] "rule2" in
assert_equal ~msg:"2. update" ~printer:(fun x->x) s (sprint r);
- let dyn_eq1 = " :f(a)' = 2. * :f(a) + t;"
+ let dyn_eq1 = " :f(a)' = 2. * :f(a) + :t;"
and dyn_eq2 = " :f(b)' = :f(b)" in
let dyn_eq = dyn_eq1 ^ dyn_eq2 in
let s = discr ^ "\n dynamics" ^ dyn_eq in
@@ -88,7 +88,7 @@
let dr =
"[| P { (a) } | ] -> [| P:1{}; Q { (b) } | ] emb P with [b<-a]" in
let signat = ["P", 1; "Q", 1] in
- let dyn_eq = ":x(a)' = :x(a) + t" in
+ let dyn_eq = ":x(a)' = :x(a) + :t" in
(* due to optimization (RHS renamed to match LHS), below it is
:x(a)=:x(a) rather than :x(b)=:x(a) *)
let upd_eq = ":x(a) = :x(a)" in
@@ -107,7 +107,7 @@
(fun () ->
let dr =
"[| P { (a) } | ] -> [| P:1{}; Q { (b) } | ] emb P with [b<-a]" in
- let dyn_eq = ":x(a)' = :x(a) + t" in
+ let dyn_eq = ":x(a)' = :x(a) + :t" in
(* due to optimization (RHS renamed to match LHS), below it is
:x(a)=:x(a) rather than :x(b)=:x(a) *)
let upd_eq = ":x(a) = :x(a)" in
@@ -153,11 +153,11 @@
(ContinuousRule.compare_diff r1 r2);
let upd_eq = " :f(a) = 2. * :f(a);\n :f(b) = :f(b)\n" in
- let dyn_eq = " :f(a)' = (2. * :f(a)) + t;\n :f(b)' = :f(b)" in
+ let dyn_eq = " :f(a)' = (2. * :f(a)) + :t;\n :f(b)' = :f(b)" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ "\nupdate\n" ^ upd_eq ^
" inv true post true" in
let r1 = rule_of_str s signat [] "rule4" in
- let dyn_eq = " :f(a)' = (3. * :f(a)) + t;\n :f(b)' = :f(b)" in
+ let dyn_eq = " :f(a)' = (3. * :f(a)) + :t;\n :f(b)' = :f(b)" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ "\nupdate\n" ^ upd_eq ^
" inv true post true" in
let r2 = rule_of_str s signat [] "rule5" in
Deleted: trunk/Toss/Arena/Term.ml
===================================================================
--- trunk/Toss/Arena/Term.ml 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Arena/Term.ml 2012-05-19 21:37:16 UTC (rev 1710)
@@ -1,261 +0,0 @@
-(* Represent terms and basic operations on them. *)
-
-(* ---------------------- BASIC TYPE DEFINITION ----------------------------- *)
-
-let simp_symb = ref false
-
-type term =
- | Var of string
- | FVar of string * string
- | Const of float
- | Times of term * term
- | Plus of term * term
- | Div of term * term
-
-type eq_sys = ((string * string) * term) list
-
-(* Power function used in parser. *)
-let rec pow p n =
- if n = 0 then Const 1. else if n = 1 then p else Times (p, pow p (n-1))
-
-let compare t1 t2 = match (t1, t2) with
- | (Const x, Const y) -> if x > y then 1 else if y > x then -1 else 0
- | (Const _, _) -> -1
- | (_, Const _) -> 1
- | (Var x, Var y) -> String.compare x y
- | (Var _, _) -> -1
- | (_, Var _) -> 1
- | (FVar (f, x), FVar (g, y)) ->
- let c = String.compare f g in if c <> 0 then c else String.compare x y
- | (FVar _, _) -> -1
- | (_, FVar _) -> 1
- | _ -> Pervasives.compare t1 t2
-
-
-(* Variables (pure, not applied functions) in a term. *)
-let vars t =
- let rec vars_acc = function
- | Const _ | FVar _ -> []
- | Var x -> [x]
- | Plus (t, s) | Times (t, s) | Div (t, s) -> (vars_acc t) @ (vars_acc s) in
- Aux.unique_sorted (vars_acc t)
-
-
-(* ------------------------ PRINTING FUNCTION ------------------------------- *)
-
-(* Bracket-savvy precedences: + 0, - 1, * 2, / 3 *)
-let rec fprint ?(smt2=false) ?(prec=0) ppf = function
- | Var s -> Format.pp_print_string ppf s
- | FVar (f, a) -> if smt2 then Format.fprintf ppf "%s_of_%s" f a else
- Format.fprintf ppf ":%s(%s)" f a
- | Const n -> if smt2 then if n >= 0. then Format.fprintf ppf "%F" n else
- Format.fprintf ppf "(* minusone %F)" ((-1.) *. n)
- else Format.fprintf ppf "%F" n
- | Times (p, q) ->
- let lb, rb = if prec > 2 then "(", ")" else "", "" in
- if smt2 then Format.fprintf ppf "@[<1>(* %a@ %a)@]"
- (fprint ~smt2 ~prec:2) p (fprint ~smt2 ~prec:2) q
- else Format.fprintf ppf "@[<1>%s%a@ *@ %a%s@]" lb
- (fprint ~smt2 ~prec:2) p (fprint ~smt2 ~prec:2) q rb
- | Plus (p, Times (Const c, q)) when not smt2 && c = -1. ->
- let lb, rb = if prec > 0 then "(", ")" else "", "" in
- Format.fprintf ppf "@[<1>%s%a@ -@ %a%s@]" lb
- (fprint ~smt2 ~prec:0) p (fprint ~smt2 ~prec:1) q rb
- | Plus (p, Const c) when not smt2 && c < 0. ->
- let lb, rb = if prec > 0 then "(", ")" else "", "" in
- Format.fprintf ppf "@[<1>%s%a@ -@ %a%s@]" lb
- (fprint ~smt2 ~prec:0) p (fprint ~smt2 ~prec:1) (Const (-. c)) rb
- | Plus (p, q) ->
- let lb, rb = if prec > 0 then "(", ")" else "", "" in
- if smt2 then Format.fprintf ppf "@[<1>(+ %a@ %a)@]"
- (fprint ~smt2 ~prec:0) p (fprint ~smt2 ~prec:0) q
- else Format.fprintf ppf "@[<1>%s%a@ +@ %a%s@]" lb
- (fprint ~smt2 ~prec:0) p (fprint ~smt2 ~prec:0) q rb
- | Div (p, q) ->
- let lb, rb = if prec > 2 then "(", ")" else "", "" in
- if smt2 then Format.fprintf ppf "@[<1>(/ %a@ %a)@]"
- (fprint ~smt2 ~prec:2) p (fprint ~smt2 ~prec:3) q
- else Format.fprintf ppf "@[<1>%s%a@ /@ %a%s@]" lb
- (fprint ~smt2 ~prec:2) p (fprint ~smt2 ~prec:2) q rb
-
-let print r = AuxIO.print_of_fprint fprint r
-let sprint r = AuxIO.sprint_of_fprint fprint r
-let str = sprint
-let str_smt2 r = AuxIO.sprint_of_fprint (fprint ~smt2:true) r
-
-(* Print an equation system. *)
-let fprint_eqs ?(diff=true) ppf eqs =
- let sing ppf ((f, a), t) =
- let mid_str = if diff then "'" else "" in
- Format.fprintf ppf "@[<1>:%s(%s)%s@ =@ @[<1>%a@]@]"
- f a mid_str (fprint ~smt2:false ~prec:0) t in
- Format.fprintf ppf "@[<hv>%a@]" (Aux.fprint_sep_list ";" sing) eqs
-
-let print_eqs ?diff r = AuxIO.print_of_fprint (fprint_eqs ?diff) r
-let sprint_eqs ?diff r = AuxIO.sprint_of_fprint (fprint_eqs ?diff) r
-let eq_str = sprint_eqs
-
-
-(* -------------------- SIMPLIFICATION OF CONSTANTS ------------------------- *)
-
-(* Basic simplification, reduces constant terms to floats. *)
-let rec simp_const_only = function
- | Var s -> Var s
- | FVar (f, a) -> FVar (f, a)
- | Const n -> Const n
- | Times (p, q) -> (
- match (simp_const_only p, simp_const_only q) with
- | (Const n, Const m) -> Const (n *. m)
- | (t, s) -> Times (t, s)
- )
- | Plus (p, q) -> (
- match (simp_const_only p, simp_const_only q) with
- | (Const n, Const m) -> Const (n +. m)
- | (t, s) -> Plus (t, s)
- )
- | Div (p, q) ->
- match (simp_const_only p, simp_const_only q) with
- | (Const n, Const m) -> Const (n /. m)
- | (t, s)-> Div (t, s)
-
-let simp_const t =
- let rec to_poly = function
- | Var s -> Poly.Var ("V" ^ s)
- | FVar (f, a) -> Poly.Var ("F" ^ f ^ "#" ^ a)
- | Const n -> Poly.Const n
- | Times (p, q) -> Poly.Times (to_poly p, to_poly q)
- | Plus (p, q) -> Poly.Plus (to_poly p, to_poly q)
- | Div _ -> raise Not_found in
- let rec from_ord = function
- | OrderedPoly.Const _ -> failwith "num after non-num translation"
- | OrderedPoly.FConst num -> Const (num)
- | OrderedPoly.Poly (v, coefs) ->
- let w = if v.[0]= 'V' then Var (String.sub v 1 ((String.length v)-1)) else
- let i, l = String.index v '#', String.length v in
- FVar (String.sub v 1 (i-1), String.sub v (i+1) (l-i-1)) in
- let res = List.fold_left (fun acc (a, j) ->
- if j = 0 then Plus (acc, from_ord a) else
- match from_ord a with
- | Const n when n = 1. -> Plus (acc, pow w j)
- | ordt -> Plus (acc, Times (ordt, pow w j))
- ) (Const 0.) coefs in
- LOG 1 "res %s" (str res);
- let rec del_zero = function
- | Plus (Const n, t) when n = 0. -> t
- | Plus (t, s) -> Plus (del_zero t, s)
- | t -> t in
- del_zero res in
- match simp_const_only t with
- | Const n -> Const n
- | t -> if not !simp_symb then t else
- try let p = to_poly t in
- from_ord (Poly.make_ordered ~use_num:false [] p)
- with Not_found -> t
-
-(* Convert a term to float, fail on non-constant term. *)
-let term_val t = match simp_const t with
- | Const f -> f
- | t -> failwith ("getting value from non-constant term (" ^ str t ^ ")")
-
-
-(* Convert an equation system to float assciation list, fail on non-consts. *)
-let eq_vals eqs = List.map (fun (l, r) -> (l, term_val r)) eqs
-
-
-(* ----------------------- SIMPLE OPERATIONS ------------------------------- *)
-
-let add t1 t2 = simp_const (Plus (t1, t2))
-let ladd1 t tl = List.map (fun x -> add t x) tl
-let ladd tl1 tl2 = List.map2 add tl1 tl2
-
-let mul t1 t2 = simp_const (Times (t1, t2))
-let lmul1 t tl = List.map (fun x -> mul t x) tl
-let lmul tl1 tl2 = List.map2 mul tl1 tl2
-
-
-(* ------------------ SUBSTITUTION FOR VARIABLES --------------------------- *)
-
-(* Substitute terms for variables as in [dict] in the given term. *)
-let rec subst dict = function
- | Var s as t -> (try List.assoc s dict with Not_found -> t)
- | FVar _ | Const _ as t -> t
- | Plus (p, q) -> Plus (subst dict p, subst dict q)
- | Times (p, q) -> Times (subst dict p, subst dict q)
- | Div (p, q) -> Div (subst dict p, subst dict q)
-
-(* Substitute [vals] for [vars] in [terms] and simplify. *)
-let subst_simp vars vals terms =
- List.map (fun t -> simp_const (subst (List.combine vars vals) t)) terms
-
-
-(* Substitute terms for function variables as in [dict] in the given term. *)
-let rec subst_f dict = function
- | FVar (g, b) as t -> (try List.assoc (g, b) dict with Not_found -> t)
- | Var _ | Const _ as t -> t
- | Plus (p, q) -> Plus (subst_f dict p, subst_f dict q)
- | Times (p, q) -> Times (subst_f dict p, subst_f dict q)
- | Div (p, q) -> Div (subst_f dict p, subst_f dict q)
-
-(* Substitute [vals] for function [vars] in [terms] and simplify. *)
-let subst_simp_f vars vals terms =
- List.map (fun t -> simp_const (subst_f (List.combine vars vals) t)) terms
-
-(* Substitute variables and function vals in an equation system and simplify. *)
-let subst_simp_eq vlst flst eqs =
- let ((lhs, rhs), (vvars, vvals), (fvars, fvals)) =
- (List.split eqs, List.split vlst, List.split flst) in
- List.combine lhs (subst_simp vvars vvals (subst_simp_f fvars fvals rhs))
-
-(* Substitute function argument names in an equation system, left and right. *)
-let subst_names subst eqs =
- let (lhs, rhs) = List.split eqs in
- let replace a = try List.assoc a subst with Not_found -> a in
- let subst_vals = List.map (fun (f, a) -> FVar (f, replace a)) lhs in
- let new_rhs = subst_simp_f lhs subst_vals rhs in
- List.combine (List.map (fun (f, a) -> (f, replace a)) lhs) new_rhs
-
-let rec compile_term tv eqs = function
- | Const c -> (fun _ _ -> c)
- | Var v -> (fun t _ -> if v = tv then t else failwith "non time var compile")
- | FVar (f, x) -> (fun _ a -> a.(Aux.find_index (f, x) eqs))
- | Plus (p, q) -> (let cp, cq = compile_term tv eqs p, compile_term tv eqs q in
- (fun t a -> (cp t a) +. (cq t a)))
- | Times (p, q) -> (let cp, cq= compile_term tv eqs p, compile_term tv eqs q in
- (fun t a -> (cp t a) *. (cq t a)))
- | Div (p, q) -> (let cp, cq = compile_term tv eqs p, compile_term tv eqs q in
- (fun t a -> (cp t a) /. (cq t a)))
-
-let compile tv eqs =
- let lhs = fst (List.split eqs) in
- let ceqs = Array.of_list (List.map (fun (_,t)-> compile_term tv lhs t) eqs) in
- (fun t a -> Array.map (fun f -> f t a) ceqs)
-
-
-(* ---------------- RUNGE - KUTTA METHOD FOR TERM EQUATIONS ---------------- *)
-
-(* Perform a Runge-Kutta (RK4) step for [vars] with [vals_init] and right-hand
- side [eq_terms]. Time variable [tvar] starts at [tinit] and moves [tstep]. *)
-let rk4_step tvar tinit tstep eq_sys vals_init =
- let (vars, eq_terms) = List.split eq_sys in
- let tstepdiv6 = mul (Div (Const 1., Const 6.)) tstep in
- let htstep = mul (Const 0.5) tstep in
- let f_of t x = subst_simp_f vars x (subst_simp [tvar] [t] eq_terms) in
- let k1 = f_of tinit vals_init in
- let k2 = f_of (add tinit htstep) (ladd vals_init (lmul1 htstep k1)) in
- let k3 = f_of (add tinit htstep) (ladd vals_init (lmul1 htstep k2)) in
- let k4 = f_of (add tinit tstep) (ladd vals_init (lmul1 tstep k3)) in
- let (dk2, dk3) = (lmul1 (Const 2.) k2, lmul1 (Const 2.) k3) in
- ladd vals_init (lmul1 tstepdiv6 (ladd k1 (ladd dk2 (ladd dk3 k4))))
-
-let amul c arr = Array.map (fun x -> c *. x) arr
-let aadd a1 a2 = Aux.array_map2 (fun x1 x2 -> x1 +. x2) a1 a2
-
-let rk4_step_c tinit tstep eq_f vals_arr =
- let tstepdiv6 = tstep /. 6. in
- let htstep = tstep /. 2. in
- let k1 = eq_f tinit vals_arr in
- let k2 = eq_f (tinit +. htstep) (aadd vals_arr (amul htstep k1)) in
- let k3 = eq_f (tinit +. htstep) (aadd vals_arr (amul htstep k2)) in
- let k4 = eq_f (tinit +. tstep) (aadd vals_arr (amul tstep k3)) in
- let (dk2, dk3) = (amul (2.) k2, amul (2.) k3) in
- aadd vals_arr (amul tstepdiv6 (aadd k1 (aadd dk2 (aadd dk3 k4))))
Deleted: trunk/Toss/Arena/Term.mli
===================================================================
--- trunk/Toss/Arena/Term.mli 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Arena/Term.mli 2012-05-19 21:37:16 UTC (rev 1710)
@@ -1,109 +0,0 @@
-(** Represent terms and their operations. *)
-
-(** {2 Basic Type Definition.} *)
-
-type term =
- | Var of string
- | FVar of string * string
- | Const of float
- | Times of term * term
- | Plus of term * term
- | Div of term * term
-
-type eq_sys = ((string * string) * term) list
-
-(** Compare two terms. *)
-val compare : term -> term -> int
-
-(** Variables (pure, not applied functions) in a term. *)
-val vars : term -> string list
-
-
-(** {2 Basic functions.} *)
-
-(*
-(** Whether to simplify symbolically or not. Set to false by default.
- It is nice for symbolic stuff, but slows down numerics. *)
-val simp_symb : bool ref
-
-(** Print a term as a string, maybe in the smt2 format. *)
-val str : term -> string
-val str_smt2 : term -> string
-
-val fprint : ?smt2:bool -> ?prec:int -> Format.formatter -> term -> unit
-val print : term -> unit
-val sprint : term -> string
-
-
-(** Print an equation system as a string. *)
-val eq_str : ?diff : bool -> eq_sys -> string
-*)
-val fprint_eqs : ?diff : bool -> Format.formatter -> eq_sys -> unit
-(*
-val print_eqs : ?diff : bool -> eq_sys -> unit
-val sprint_eqs : ?diff : bool -> eq_sys -> string
-
-
-(** Power function used in parser. *)
-val pow : term -> int -> term
-
-(** Basic simplification, reduces constant terms to floats. *)
-val simp_const : term -> term
-
-(** Convert a term to float, fail on non-constant term. *)
-val term_val : term -> float
-
-(** Convert an equation system to float assciation list, fail on non-consts. *)
-val eq_vals : eq_sys -> ((string * string) * float) list
-*)
-
-(** {2 Simple operations.} *)
-(*
-val add : term -> term -> term
-val ladd1 : term -> term list -> term list
-val ladd : term list -> term list -> term list
-
-val mul : term -> term -> term
-val lmul1 : term -> term list -> term list
-val lmul : term list -> term list -> term list
-
-
-(** {2 Substitution for variables.} *)
-
-(** Substitute terms for variables as in [dict] in the given term. *)
-val subst : (string * term) list -> term -> term
-
-*)
-(** Substitute [vals] for [vars] in [terms] and simplify. *)
-val subst_simp : string list -> term list -> term list -> term list
-
-(*
-(** Substitute terms for function variables as in [dict] in the given term. *)
-val subst_f : ((string * string) * term) list -> term -> term
-
-(** Substitute [vals] for function [vars] in [terms] and simplify. *)
-val subst_simp_f : (string * string) list -> term list -> term list -> term list
-*)
-
-(** Substitute variables and function vals in an eq. system and simplify. *)
-val subst_simp_eq : (string * term) list -> ((string * string) * term) list ->
- eq_sys -> eq_sys
-
-(** Substitute function argument names in an equation system, left and right. *)
-val subst_names : (string * string) list -> eq_sys -> eq_sys
-
-
-(** {2 Runge-Kutta Method for Term Equations} *)
-
-
-(** Perform a Runge-Kutta (RK4) step for [vars] with [vals_init] and right-hand
- side [eq_terms]. Time variable [tvar] starts at [tinit] and moves [tstep]. *)
-(*val rk4_step : string -> term -> term -> eq_sys -> term list -> term list*)
-
-
-(** Compile eq_sys to function. *)
-val compile : string -> eq_sys -> (float -> float array -> float array)
-
-(** RK4 with compiled system. *)
-val rk4_step_c : float -> float -> (float -> float array -> float array) ->
- float array -> float array
Deleted: trunk/Toss/Arena/TermParser.mly
===================================================================
--- trunk/Toss/Arena/TermParser.mly 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Arena/TermParser.mly 2012-05-19 21:37:16 UTC (rev 1710)
@@ -1,46 +0,0 @@
-/* Parser for Terms used in equations. */
-
-/* Tokens taken from Lexer.mll in directory above. */
-%{
- open Lexer
-%}
-
-%start parse_term parse_eqs
-%type <Term.term> parse_term term_expr
-%type <(string * string) * Term.term> eq_expr
-%type <Term.eq_sys> parse_eqs eq_sys
-
-
-%%
-
-
-%public term_expr:
- | INT { Term.Const (float_of_int $1) }
- | FLOAT { Term.Const ($1) }
- | ID { Term.Var ($1) }
- | MINUS ID { Term.Times (Term.Const (-1.), Term.Var ($2)) }
- | COLON ID OPEN ID CLOSE { Term.FVar ($2, $4) }
- | COLON ID OPEN INT CLOSE { Term.FVar ($2, string_of_int $4) }
- | term_expr FLOAT { Term.Plus ($1, Term.Const $2) }
- | term_expr INT { Term.Plus ($1, Term.Const (float_of_int $2)) }
- | term_expr PLUS term_expr { Term.Plus ($1, $3) }
- | term_expr MINUS term_expr { Term.Plus ($1, Term.Times(Term.Const(-1.), $3))}
- | term_expr TIMES term_expr { Term.Times ($1, $3) }
- | term_expr DIV term_expr { Term.Div ($1, $3) }
- | OPEN term_expr CLOSE { $2 }
-
-eq_expr: /* differential equations only */
- | COLON ID OPEN ID CLOSE APOSTROPHE EQ term_expr
- { (($2, $4), $8) }
- | COLON ID OPEN INT CLOSE APOSTROPHE EQ term_expr
- { (($2, string_of_int $4), $8) }
-
-%public eq_sys:
- | eq_expr { [$1] }
- | eq_expr SEMICOLON eq_sys { $1 :: $3 }
-
-parse_term:
- term_expr EOF { $1 }
-
-parse_eqs:
- eq_sys EOF { $1 };
Deleted: trunk/Toss/Arena/TermTest.ml
===================================================================
--- trunk/Toss/Arena/TermTest.ml 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Arena/TermTest.ml 2012-05-19 21:37:16 UTC (rev 1710)
@@ -1,147 +0,0 @@
-(* Test for terms and their behaviour. *)
-
-open OUnit
-open Term
-
-let term_of_string s =
- TermParser.parse_term Lexer.lex (Lexing.from_string s)
-
-let eqs_of_string s =
- TermParser.parse_eqs Lexer.lex (Lexing.from_string s)
-
-let tyson_model_eqs () = eqs_of_string
- (" :y(e1)' = 0.015 + -200. * :y(e1) * :y(e4); " ^
- ":y(e2)' = -0.6 * :y(e2) + k6 * :y(e5); " ^
- ":y(e3)' = -100. * :y(e3) + k6 * :y(e5) + 100. * :y(e4); " ^
- ":y(e4)' = -100.*:y(e4) + 100.*:y(e3) + -200.*:y(e1) * :y(e4); " ^
- ":y(e5)' = -k6 * :y(e5) + 0.018 * :y(e6) + " ^
- " k4 * :y(e6) * :y(e5) * :y(e5); " ^
- ":y(e6)' = -0.018 * :y(e6) + 200. * :y(e1) * :y(e4) + " ^
- " -k4 * :y(e6) * :y(e5) * :y(e5)")
-
-let tests = "Term" >::: [
- "parse" >::
- (fun () ->
- let s = "(x - 0.2) / (z * y - 3.)" in
- assert_equal ~printer:(fun x->x) s (str (term_of_string s));
-
- let t0s = ":f(a) + t" in
- assert_equal ~printer:(fun x->x) t0s (str (term_of_string t0s));
-
- let eqs = ":f(a)' = :f(a) + t" in
- assert_equal ~printer:(fun x->x) eqs
- (eq_str ~diff:true (eqs_of_string eqs));
-
- );
-
- "fprint" >::
- (fun () ->
- let s = "(x - 0.2) / (z * y - 3.)" in
- assert_equal ~printer:(fun x->x) s (sprint (term_of_string s));
-
- let t0s = ":f(a) + t" in
- assert_equal ~printer:(fun x->x) t0s (sprint (term_of_string t0s));
-
- let eqs = ":f(a)' = :f(a) + t" in
- assert_equal ~printer:(fun x->x) eqs
- (sprint_eqs ~diff:true (eqs_of_string eqs));
-
- );
-
- "substitute" >::
- (fun () ->
- let t0 = term_of_string ":f(a) + t" in
- let t1 = subst [("t", (Const 2.))] t0 in
- assert_equal ~printer:(fun x->x) ":f(a) + 2." (str t1);
-
- assert_equal ~printer:(fun x->x) "5."
- (str (List.hd (subst_simp_f ["f", "a"] [Const 3.] [t1])));
- );
-
- "subst names" >::
- (fun () ->
- let t0 = term_of_string "-100 * :y(e1)" in
- let t0s = term_of_string "-100 * :y(e2)" in
- let t1 = term_of_string "100. * :y(e1)" in
- let t1s = term_of_string "100. * :y(e2)" in
- let eq = [(("y", "e1"), t0); (("y", "e2"), t1)] in
- let eqs = [(("y", "e2"), t0s); (("y", "e1"), t1s)] in
- assert_equal ~printer:(fun x->x) (eq_str eqs)
- (eq_str (subst_names [("e1", "e2"); ("e2", "e1")] eq))
- );
-
- "rk4" >::
- (fun () ->
- let t0 = term_of_string ":f(a) + t" in
-
- assert_equal ~printer:(fun x->x) "0.005"
- (String.sub (str (List.hd (
- rk4_step "t" (Const 0.) (Const 0.1)
- [("f", "a"), t0] [Const 0.]))) 0 5);
-
- let eqs = eqs_of_string ":f(a)' = :f(a) + t" in
- assert_equal ~printer:(fun x->x) "0.005"
- (String.sub (str (List.hd (
- rk4_step "t" (Const 0.) (Const 0.1) eqs [Const 0.]))) 0 5);
- );
-
- "rk4 eq" >::
- (fun () ->
- (* Runge-Kutta symbolically with 2 free parameters. *)
- let tyson = tyson_model_eqs () in
- let init = [Const 0.; Const 0.; Const 1.; Const 0.; Const 0.; Const 0.] in
- Term.simp_symb := true;
- let res = rk4_step "t" (Const 0.) (Const 0.005) tyson init in
- Term.simp_symb := false;
- let val_str vs = String.concat ", " (List.map str vs) in
- assert_equal ~printer:(fun x->x)
- ("6.6076722582e-05, 3.515625e-13 * k6, 3.515625e-13 * k6 + " ^
- "0.687499267591, 0.312491809132, -3.515625e-13 * k6 + " ^
- "6.08239621818e-28 * k4 + 2.02139802246e-10, " ^
- "-6.08239621818e-28 * k4 + 8.9230752782e-06") (val_str res);
- );
-]
-
-
-(* Generate RK4 equations symbolically for [eq], step [n]. *)
-let generate_rksymb eqs nsteps tstep =
- AuxIO.print "(set-logic QF_NRA)\n";
- AuxIO.print "(set-info :source | generated symbolic RK4 in smt2 format |)\n";
- let init m = Array.to_list (Array.mapi (fun i _ ->
- Term.Var (Printf.sprintf "v%iat%i" i m)) (Array.of_list eqs)) in
- let print_var_str vs = AuxIO.print ("(declare-fun " ^ vs ^ " () Real)\n") in
- let print_var v = print_var_str (Term.str_smt2 v) in
- print_var_str "minusone";
- let fv = List.concat (List.map (fun (_, rhs) -> Term.vars rhs) eqs) in
- List.iter print_var_str (Aux.unique_sorted fv);
- let gen_init_vars i = List.iter print_var (init i) in
- List.iter gen_init_vars (Aux.range (nsteps+1));
- AuxIO.print "(assert (= (+ minusone 1.) 0.))\n";
- let gen_step i =
- let time_i = (float i) *. tstep in
- let res_i = rk4_step "t" (Const time_i) (Const tstep) eqs (init i) in
- List.iter2 (fun t v -> AuxIO.print (
- "(assert (= " ^ (Term.str_smt2 t) ^" "^ (Term.str_smt2 v) ^ "))\n"
- )) (init (i+1)) res_i in
- List.iter gen_step (Aux.range nsteps);
- AuxIO.print "(check-sat)\n"
-
-
-(* Calling the generation from bash. *)
-let main () =
- AuxIO.set_optimized_gc ();
- let (eqs, nsteps, tstep) = (ref (tyson_model_eqs ()), ref 0, ref 0.005) in
- let dbg_level i = (AuxIO.set_debug_level "Term" i) in
- let opts = [
- ("-v", Arg.Unit (fun () -> dbg_level 1), "be verbose");
- ("-d", Arg.Int (fun i -> dbg_level i), "set debug level");
- ("-eqs", Arg.String (fun s -> eqs := eqs_of_string s), "parse ODE system");
- ("-steps", Arg.Int (fun i -> nsteps := i), "number of steps to generate");
- ("-tstep", Arg.Float (fun f -> tstep := f), "time step (default 0.005)");
- ] in
- Arg.parse opts (fun _ -> ()) "Try -help for help or one of the following.";
- if !nsteps <> 0 then (
- generate_rksymb !eqs !nsteps !tstep
- ) else ignore (OUnit.run_test_tt ~verbose:true tests)
-
-let _ = AuxIO.run_if_target "TermTest" main
Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Formula/Formula.ml 2012-05-19 21:37:16 UTC (rev 1710)
@@ -402,6 +402,11 @@
if phi1 == phi2 then 0 else
let (s1, s2) = (size phi1, size phi2) in
if s1 <> s2 then s1 - s2 else rec_compare phi1 phi2
+
+let compare_re re1 re2 =
+ if re1 == re2 then 0 else
+ let (s1, s2) = (size_real re1, size_real re2) in
+ if s1 <> s2 then s1 - s2 else rec_compare_re re1 re2
(* --------------- BASIC HELPER FUNCTIONS USED IN PARSER ------------------- *)
@@ -591,3 +596,34 @@
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
+
+
+(* --- Runge - Kutta method for real-expr defined equation systems. --- *)
+
+let rec compile_re tv eqs = function
+ | Const c -> (fun _ _ -> c)
+ | RVar v -> (fun t _ -> if v = tv then t else failwith "non time var compile")
+ | Fun (f, x) -> (fun _ a -> a.(Aux.find_index (f, var_str x) eqs))
+ | Plus (p, q) -> (let cp, cq = compile_re tv eqs p, compile_re tv eqs q in
+ (fun t a -> (cp t a) +. (cq t a)))
+ | Times (p, q) -> (let cp, cq= compile_re tv eqs p, compile_re tv eqs q in
+ (fun t a -> (cp t a) *. (cq t a)))
+ | re -> failwith ("compilation for " ^ real_str re ^ " not implemented yet")
+
+let compile tv eqs =
+ let lhs = fst (List.split eqs) in
+ let ceqs = Array.of_list (List.map (fun (_,t)-> compile_re tv lhs t) eqs) in
+ (fun t a -> Array.map (fun f -> f t a) ceqs)
+
+let amul c arr = Array.map (fun x -> c *. x) arr
+let aadd a1 a2 = Aux.array_map2 (fun x1 x2 -> x1 +. x2) a1 a2
+
+let rk4_step tinit tstep eq_f vals_arr =
+ let tstepdiv6 = tstep /. 6. in
+ let htstep = tstep /. 2. in
+ let k1 = eq_f tinit vals_arr in
+ let k2 = eq_f (tinit +. htstep) (aadd vals_arr (amul htstep k1)) in
+ let k3 = eq_f (tinit +. htstep) (aadd vals_arr (amul htstep k2)) in
+ let k4 = eq_f (tinit +. tstep) (aadd vals_arr (amul tstep k3)) in
+ let (dk2, dk3) = (amul (2.) k2, amul (2.) k3) in
+ aadd vals_arr (amul tstepdiv6 (aadd k1 (aadd dk2 (aadd dk3 k4))))
Modified: trunk/Toss/Formula/Formula.mli
===================================================================
--- trunk/Toss/Formula/Formula.mli 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Formula/Formula.mli 2012-05-19 21:37:16 UTC (rev 1710)
@@ -79,6 +79,7 @@
val size_real : ?acc : int -> real_expr -> int
val compare : formula -> formula -> int
+val compare_re : real_expr -> real_expr -> int
val is_atom : formula -> bool
val is_literal : formula -> bool
@@ -135,3 +136,13 @@
val flatten_sort : formula -> formula
val flatten_sort_re : real_expr -> real_expr
+
+(** {2 Runge - Kutta method for real-expr defined equation systems.} **)
+
+(** Compile eq_sys to function. *)
+val compile : string -> eq_sys -> (float -> float array -> float array)
+
+(** Perform a Runge-Kutta (RK4) step for [vars] with [vals_init] and right-hand
+ side [eq_terms]. Time variable [tvar] starts at [tinit] and moves [tstep]. *)
+val rk4_step : float -> float -> (float -> float array -> float array) ->
+ float array -> float array
Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Formula/FormulaParser.mly 2012-05-19 21:37:16 UTC (rev 1710)
@@ -43,6 +43,7 @@
| INT { Const (float_of_int $1) }
| FLOAT { Const ($1) }
| COLON ID { RVar (":" ^ $2) }
+ | MINUS COLON ID { Times (Const (-1.), RVar (":" ^ $3)) }
| COLON ID OPEN ID CLOSE { Fun ($2, fo_var_of_s $4) }
| COLON ID OPEN INT CLOSE { Fun ($2, fo_var_of_s (string_of_int $4)) }
| real_expr FLOAT { Plus ($1, Const $2) } /* in x-1, "-1" is int */
@@ -129,6 +130,9 @@
expr_eq_expr: /* only standard equations here for now (no differentials) */
| COLON ID OPEN ID CLOSE EQ real_expr { (($2, $4), $7) }
| COLON ID OPEN INT CLOSE EQ real_expr { (($2, string_of_int $4), $7) }
+ | COLON ID OPEN ID CLOSE APOSTROPHE EQ real_expr { (($2, $4), $8) }
+ | COLON ID OPEN INT CLOSE APOSTROPHE EQ real_expr
+ { (($2, string_of_int $4), $8) }
%public expr_eq_sys:
| expr_eq_expr { [$1] }
Modified: trunk/Toss/Formula/FormulaTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaTest.ml 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Formula/FormulaTest.ml 2012-05-19 21:37:16 UTC (rev 1710)
@@ -4,6 +4,9 @@
let formula_of_string s =
FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
+let eqs_of_string s =
+ FormulaParser.parse_expr_eqs Lexer.lex (Lexing.from_string s)
+
let rel r i = Rel (r, Array.make i (`FO "x"))
@@ -53,5 +56,30 @@
test_pp "(:x - (:y + :z) < 0)";
test_pp "(:x - :y + :z < 0)";
);
+
+ "rk4" >::
+ (fun () ->
+ let float_arr_str n fa = String.concat ", " (List.map (fun f ->
+ String.sub (string_of_float f) 0 n) (Array.to_list fa)) in
+ let eqs = eqs_of_string ":f(a)' = :f(a) + :t" in
+ let ceqs = compile ":t" eqs in
+ assert_equal ~printer:(fun x -> x) "0.00517"
+ (float_arr_str 7 (rk4_step 0. 0.1 ceqs [| 0. |]));
+
+ let tyson_model_eqs = eqs_of_string
+ (" :y(e1)' = 0.015 + -200. * :y(e1) * :y(e4); " ^
+ ":y(e2)' = -0.6 * :y(e2) + 1. * :y(e5); " ^
+ ":y(e3)' = -100. * :y(e3) + 1. * :y(e5) + 100. * :y(e4); " ^
+ ":y(e4)' = -100. * :y(e4) + 100.*:y(e3) + -200.*:y(e1) * :y(e4); "^
+ ":y(e5)' = -1. * :y(e5) + 0.018 * :y(e6) + " ^
+ " 180. * :y(e6) * :y(e5) * :y(e5); " ^
+ ":y(e6)' = -0.018 * :y(e6) + 200. * :y(e1) * :y(e4) + " ^
+ " -180. * :y(e6) * :y(e5) * :y(e5)") in
+ let ceqs = compile ":t" tyson_model_eqs in
+ let init = [| 0.; 0.; 1.; 0.; 0.; 0. |] in
+ assert_equal ~printer:(fun x -> x)
+ "0.00110, 3.6e-10, 2.99999, -1.9991, 7.16443, -0.0008"
+ (float_arr_str 7 (rk4_step 0. 0.02 ceqs init));
+ );
]
Modified: trunk/Toss/Language/BuiltinLang.ml
===================================================================
--- trunk/Toss/Language/BuiltinLang.ml 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Language/BuiltinLang.ml 2012-05-19 21:37:16 UTC (rev 1710)
@@ -1,41 +1,8 @@
-(*
- Speagram
+(* Basic Built-in Language Syntax for Speagram. *)
- Copyright (c) 2003-2006, Speagram Authors.
-
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions are met:
-
- * Redistributions of source code must retain the above copyright notice,
- this list of conditions and the following disclaimer.
- * Redistributions in binary form must reproduce the above copyright notice,
- this list of conditions and the following disclaimer in the documentation
- and/or other materials provided with the distribution.
-
- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
- OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
- WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
- OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
- EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
- ------------------------------------------------------------
-
- Basic Built-in Language Syntax for Speagram.
-
-*)
-
open Type;;
open SyntaxDef;;
-(* * #load "Type.cmo";; *)
-(* * #load "SyntaxDef.cmo";; *)
-
(* ---------------- BASIC TYPES AND SYNTAX DEFS ----------------------- *)
let bit_sd = SDtype [Str "bit"];;
Modified: trunk/Toss/Language/BuiltinLang.mli
===================================================================
--- trunk/Toss/Language/BuiltinLang.mli 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Language/BuiltinLang.mli 2012-05-19 21:37:16 UTC (rev 1710)
@@ -1,35 +1,5 @@
-(*
- Speagram
+(* Signature for Built-in Langauge Definitions. *)
- Copyright (c) 2003-2006, Speagram Authors.
-
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions are met:
-
- * Redistributions of source code must retain the above copyright notice,
- this list of conditions and the following disclaimer.
- * Redistributions in binary form must reproduce the above copyright notice,
- this list of conditions and the following disclaimer in the documentation
- and/or other materials provided with the distribution.
-
- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
- OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
- WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
- OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
- EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
- ------------------------------------------------------------
-
- Signature for Built-in Langauge Definitions.
-
-*)
-
open SyntaxDef;;
Modified: trunk/Toss/Language/Makefile
===================================================================
--- trunk/Toss/Language/Makefile 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Language/Makefile 2012-05-19 21:37:16 UTC (rev 1710)
@@ -27,10 +27,10 @@
OCAMLTOP = ocaml -I +camlp4 camlp4o.cma str.cma
-OCAMLCARGS = -thread -I +camlp4 -pp "camlp4o" str.cma unix.cma threads.cma
+OCAMLCARGS = -I +camlp4 -pp "camlp4o" str.cma unix.cma
OCAMLC = ocamlc $(OCAMLCARGS)
-OCAMLOPTARGS = -thread -I +camlp4 -pp "camlp4o" str.cmxa unix.cmxa threads.cmxa
+OCAMLOPTARGS = -I +camlp4 -pp "camlp4o" str.cmxa unix.cmxa
OCAMLOPT = ocamlopt $(OCAMLOPTARGS)
@@ -100,11 +100,10 @@
Term.cmi Term.cmo Term.cmx \
ParseArc.cmi ParseArc.cmo ParseArc.cmx \
Rewriting.cmi Rewriting.cmo Rewriting.cmx \
- Normalisation.cmi Normalisation.cmo Normalisation.cmx \
System.cmi System.cmo System.cmx
$(USEDOCAML) \
Type.cmx SyntaxDef.cmx BuiltinLang.cmx Term.cmx Rewriting.cmx \
- Normalisation.cmx ParseArc.cmx System.cmx speagram.ml -o speagram
+ ParseArc.cmx System.cmx speagram.ml -o speagram
parsed: speagram
Deleted: trunk/Toss/Language/Normalisation.ml
===================================================================
--- trunk/Toss/Language/Normalisation.ml 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Language/Normalisation.ml 2012-05-19 21:37:16 UTC (rev 1710)
@@ -1,202 +0,0 @@
-(*
- Speagram
-
- Copyright (c) 2003-2006, Speagram Authors.
-
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions are met:
-
- * Redistributions of source code must retain the above copyright notice,
- this list of conditions and the following disclaimer.
- * Redistributions in binary form must reproduce the above copyright notice,
- this list of conditions and the following disclaimer in the documentation
- and/or other materials provided with the distribution.
-
- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
- OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
- WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
- OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
- EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
- ------------------------------------------------------------
-
- Contains the functions responsible for rewriting and normalisation.
-
-*)
-
-
-open List;;
-open Str;;
-
-open Type;;
-open SyntaxDef;;
-open BuiltinLang;;
-open Term;;
-open Rewriting;;
-(* * #load "Type.cmo";; *)
-(* * #load "SyntaxDef.cmo";; *)
-(* * #load "BuiltinLang.cmo";; *)
-(* * #load "Term.cmo";; *)
-(* * #load "Rewriting.cmo";; *)
-
-
-(* -------------------------- NORMALISATION ------------------------ *)
-
-
-let rec normalise_special_id_one name = function
- Term (n, [|a|]) when n = name -> a
- | Term (n, a) -> Term (n, Array.map (normalise_special_id_one name) a)
- | Var (n, ty, d, a) ->
- Var (n, ty, d, Array.map (normalise_special_id_one name) a)
-;;
-let rec normalise_special_id_all name = function
- Term (n, [|a|]) when n = name -> normalise_special_id_all name a
- | Term (n, a) -> Term (n, Array.map (normalise_special_id_all name) a)
- | Var (n, ty, d, a) ->
- Var (n, ty, d, Array.map (normalise_special_id_all name) a)
-;;
-
-let normalise_brackets = normalise_special_id_all brackets_name;;
-let normalise_verbatim = normalise_special_id_one verbatim_name;;
-
-let rec normalise_special rr_spec = function
- Term (n, [|a|]) as te when n = verbatim_name -> te
- | Term (n, a) when n.[0] = 'F' ->
- let normalised = Term (n, Array.map (normalise_special rr_spec) a) in
- rr_spec normalised
- | Term (n, a) ->
- Term (n, Array.map (normalise_special rr_spec) a)
- | Var (n, ty, d, a) ->
- Var (n, ty, d, Array.map (normalise_special rr_spec) a)
-;;
-
-let cTHREAD_MAX = 2;;
-let cMEM_USE_INCREASE_FACTOR = 128;;
-
-let rec basic_normalise_t_r rr rr_spec m lock th_no res te =
- res := basic_normalise rr rr_spec m lock th_no te;
-and basic_normalise_th rr rr_spec m lock th_no te =
- let res = ref (0, Term ("", [||])) in
- if !th_no < cTHREAD_MAX then (
- Mutex.lock lock; th_no := !th_no+1; Mutex.unlock lock;
- let thread =
- Thread.create (basic_normalise_t_r rr rr_spec m lock th_no res) te in
- (Some (thread), res)
- )
- else
- (None, ref (basic_normalise rr rr_spec m lock th_no te))
-and basic_normalise_arr rr rr_spec m lock th_no = function
- [||] -> (0, [||])
- | [|x|] ->
- let (steps, res) = basic_normalise rr rr_spec m lock th_no x in
- (steps, [|res|])
- | arr ->
- let th_arr =
- Array.map (basic_normalise_th rr rr_spec m lock th_no) arr in
- let steps = ref 0 in
- let res_arr =
- Array.map (function
- (Some (th), res) ->
- (Thread.join th;
- Mutex.lock lock; th_no := !th_no-1; Mutex.unlock lock;
- steps := !steps + fst (!res);
- snd (!res))
- | (None, res) ->
- (steps := !steps + fst (!res); snd (!res))
- ) th_arr in
- (!steps, res_arr)
-and basic_normalise rr rr_spec m lock th_no = function
- Term (n, [|Term (f, a); r|]) when n = let_major_be_name ->
- let (steps_l, na) = basic_normalise_arr rr rr_spec m lock th_no a in
- let (steps_r, rs) = basic_normalise rr rr_spec m lock th_no r in
- (steps_l + steps_r, Term (n, [|Term (f, na); rs|]))
- | Term (n, [|a|]) as te when n = verbatim_name -> (0, te)
- | Term (nm, [|c; y; n|]) when nm = if_then_else_name ->
- let (steps_c, norm_cond) = basic_normalise rr rr_spec m lock th_no c in
- let norm_cond_te = Term (nm, [|norm_cond; y; n|]) in
- let rewritten = rr norm_cond_te in
- if (rewritten = norm_cond_te) then
- (steps_c, Term (nm, [|norm_cond; normalise_special rr_spec y;
- normalise_special rr_spec n|]))
- else
- let (steps, res) = basic_normalise rr rr_spec m lock th_no rewritten in
- (steps + steps_c + 1, res)
- | Term (n, a) when n.[0] = 'F' -> (
- let (prev_steps, prev_res) =
- basic_normalise_arr rr rr_spec m lock th_no a in
- let nmlized = Term (n, prev_res) in
- let found = (
- Mutex.lock lock;
- let res = try
- Some (TermHashtbl.find m nmlized)
- with
- Not_found -> None in
- Mutex.unlock lock;
- res
- ) in
- match found with Some (r) -> (prev_steps, r) | None ->
- let rewritten = rr nmlized in
- if rewritten = nmlized then
- (prev_steps, rewritten)
- else
- let (steps, res) = basic_normalise rr rr_spec m lock th_no rewritten in
- let memory_size = TermHashtbl.length m in
- let threshold = (memory_size / cMEM_USE_INCREASE_FACTOR) + 1 in
- let size_addon = min (size_up_to 256 nmlized) threshold in
- if steps > threshold + size_addon then
- (Mutex.lock lock;
- TermHashtbl.add m nmlized res;
- Mutex.unlock lock;
- (0, res))
- else
- (prev_steps + steps + 1, res)
- )
- | Term (n, a) ->
- let (steps, res) = basic_normalise_arr rr rr_spec m lock th_no a in
- (steps, Term (n, res))
- | Var (n, ty, d, a) ->
- let (steps, res) = basic_normalise_arr rr rr_spec m lock th_no a in
- (steps, Var (n, ty, d, res))
-;;
-
-
-let normalise mem rules is_special rewrite_special inp_term =
- let term = normalise_brackets inp_term in
- let rr = function
- Term (n, a) as te when (is_special n) ->
- rewrite_special (normalise_verbatim te)
- | Term (n, a) as te -> (
- try
- rewrite (Hashtbl.find rules n) te
- with
- Not_found -> te
- )
- | te -> te in
- let (_, normalised) =
- basic_normalise rr rewrite_special mem (Mutex.create ()) (ref 1) term in
- normalise_verbatim normalised
-;;
-
-
-(* TESTS *
- let var_x_b = Var ("x", boolean_tp, 0, [||]);;
- let var_y_b = Var ("y", boolean_tp, 0, [||]);;
- let rr1 =
- (Term ("Fand", [|code_bool true; code_bool true|]), code_bool true);;
- let rr2 = (Term ("Fand", [|var_x_b; var_y_b|]), code_bool false);;
- let rrs = [("Fand", [rr1; rr2])];;
-
- let t1 = Term ("Fand", [|code_bool true; code_bool true|]);;
- let t2 = Term ("Fand", [|code_bool true; t1|]);;
- let t3 = Term ("Fand", [|var_x_b; t1|]);;
- let t4 = Term (if_then_else_name, [|var_x_b; t1; t1|]);;
- let t5 = Term ("Ckot", [|var_x_b; t1; t1|]);;
- let _ = map (normalise rrs (fun x -> false) (fun x -> x)) [t2; t3; t4; t5];;
-*)
-
Deleted: trunk/Toss/Language/Normalisation.mli
===================================================================
--- trunk/Toss/Language/Normalisation.mli 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Language/Normalisation.mli 2012-05-19 21:37:16 UTC (rev 1710)
@@ -1,41 +0,0 @@
-(*
- Speagram
-
- Copyright (c) 2003-2006, Speagram Authors.
-
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions are met:
-
- * Redistributions of source code must retain the above copyright notice,
- this list of conditions and the following disclaimer.
- * Redistributions in binary form must reproduce the above copyright notice,
- this list of conditions and the following disclaimer in the documentation
- and/or other materials provided with the distribution.
-
- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
- OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
- WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
- OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
- EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
- ------------------------------------------------------------
-
- Signature for Rewriting module.
-
-*)
-
-
-(* ----------------------- NORMALISATION ---------------------------- *)
-
-val normalise_brackets : Term.term -> Term.term;;
-
-val normalise : (Term.term Term.TermHashtbl.t) -> (* memory *)
- (string, Rewriting.rrules_set) Hashtbl.t -> (* rules *)
- (string -> bool) -> (Term.term -> Term.term) -> Term.term -> Term.term;;
-
Modified: trunk/Toss/Language/ParseArc.ml
===================================================================
--- trunk/Toss/Language/ParseArc.ml 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Language/ParseArc.ml 2012-05-19 21:37:16 UTC (rev 1710)
@@ -1,37 +1,7 @@
-(*
- Speagram
+(* Contains the bottom-up chart-based parser that uses syntax definitions
+ and checks if terms are well-typed when closing arcs. *)
- Copyright (c) 2003-2006, Speagram Authors.
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions are met:
-
- * Redistributions of source code must retain the above copyright notice,
- this list of conditions and the following disclaimer.
- * Redistributions in binary form must reproduce the above copyright notice,
- this list of conditions and the following disclaimer in the documentation
- and/or other materials provided with the distribution.
-
- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
- OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
- WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
- OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
- EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
- ------------------------------------------------------------
-
- Contains the bottom-up chart-based parser that uses syntax definitions
- and checks if terms are well-typed when closing arcs.
-
-*)
-
-
open List;;
open Str;;
Modified: trunk/Toss/Language/ParseArc.mli
===================================================================
--- trunk/Toss/Language/ParseArc.mli 2012-05-18 21:22:13 UTC (rev 1709)
+++ trunk/Toss/Language/ParseArc.mli 2012-05-19 21:37:16 UTC (rev 1710)
@@ -1,35 +1,5 @@
-(*
- Speagram
+(* Signature for Parser module. *)
- Copyright (c) 2003-2006, Speagram Authors.
-
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions are met:
-
- * Redistributions of source code must retain the above copyright notice,
- this list of conditions and the following disclaimer.
- * Redistributions in binary form must reproduce the above copyright notice,
- this list of conditions and the following disclaimer in the documentation
- and/or other materials provided with the distribution.
-
- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
- EXEMPLARY, OR CONSEQUENTIAL DAMAGE...
[truncated message content] |
