Commit 616f63a3 authored by Daisuke Ishii's avatar Daisuke Ishii

include the actual code of Mathematica driver

parent 7283d40a
/Users/ishii/workspace/whybrid/tmp/math_driver/drivers/mathematica.drv
\ No newline at end of file
(* Why driver for Mathematica *)
prelude "(* this is a prelude for Mathematica *)"
printer "mathematica"
filename "%f-%t-%g.m"
valid "\\bTrue\\b"
unknown "\\bFalse\\b" "\\bFalse\\b"
time "why3cpulimit time : %s s"
(*transformation "simplify_recursive_definition"*)
(*transformation "inline_trivial"*)
(*transformation "inline_all"*)
transformation "eliminate_builtin"
(*transformation "eliminate_definition"*)
(*transformation "eliminate_recursion"*)
(*transformation "eliminate_inductive"*)
(*transformation "eliminate_algebraic"*)
(*transformation "eliminate_algebraic_math"*)
(*transformation "eliminate_if"*)
transformation "eliminate_let"
(*transformation "split_premise"*)
transformation "simplify_formula"
(*transformation "simplify_unknown_lsymbols"*)
transformation "simplify_trivial_quantification"
(*transformation "introduce_premises"*)
(*transformation "instantiate_predicate"*)
(*transformation "abstract_unknown_lsymbols"*)
theory BuiltIn
syntax type int "Integers"
syntax type real "Reals"
syntax predicate (=) "(%1 == %2)"
meta "encoding : kept" type int
end
(* int *)
theory int.Int
prelude "(* this is a prelude for Mathematica integer arithmetic *)"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 %2)"
syntax function (-_) "(-%1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
meta "inline : no" predicate (<=)
meta "inline : no" predicate (>=)
meta "inline : no" predicate (>)
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type int
end
theory int.Abs
syntax function abs "Abs[%1]"
end
theory int.EuclideanDivision
syntax function div "Quotient[%1, %2]"
syntax function mod "Mod[%1, %2]"
remove prop Mod_bound
remove prop Div_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
meta "encoding : kept" type int
end
(* real *)
theory real.Real
prelude "(* this is a prelude for Mathematica real arithmetic *)"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (/) "(%1 / %2)"
syntax function (-_) "(-%1)"
syntax function inv "(1 / %1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
meta "inline : no" predicate (<=)
meta "inline : no" predicate (>=)
meta "inline : no" predicate (>)
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
(*meta "encoding : kept" type real*)
end
theory real.Abs
syntax function abs "Abs[%1]"
end
theory real.MinMax
syntax function min "Min[%1, %2]"
syntax function max "Max[%1, %2]"
end
theory real.Square
syntax function sqr "Power[%1,2]"
syntax function sqrt "Sqrt[%1]"
end
theory real.ExpLog
syntax function exp "Exp[%1]"
syntax function e "E"
syntax function log "Log[%1]"
syntax function log2 "Log[2, %1]"
syntax function log10 "Log[10, %1]"
remove prop Exp_zero
remove prop Exp_sum
remove prop Log_one
remove prop Log_mul
remove prop Log_exp
remove prop Exp_log
end
theory real.PowerInt
syntax function power "Power[%1, %2]"
end
theory real.PowerReal
syntax function pow "Power[%1, %2]"
end
theory real.Trigonometry
syntax function cos "Cos[%1]"
syntax function sin "Sin[%1]"
syntax function tan "Tan[%1]"
syntax function atan "ArcTan[%1]"
syntax function pi "Pi"
end
theory real.Hyperbolic
syntax function sinh "Sinh[%1]"
syntax function cosh "Cosh[%1]"
syntax function tanh "Tanh[%1]"
syntax function asinh "ArcSinh[%1]"
syntax function acosh "ArcCosh[%1]"
syntax function atanh "ArcTanh[%1]"
end
theory real.FromInt
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
/Users/ishii/workspace/whybrid/tmp/math_driver/src/printer/mathematica.ml
\ No newline at end of file
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2012 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(** Mathematica printer *)
open Format
open Pp
open Printer
open Ident
open Ty
open Term
open Decl
open Theory
open Task
(* patterns (TODO: add a parser and generalize it out of Mathematica) *)
type pattern =
| PatHole of int
| PatApp of Env.pathname * string * string list * pattern list
let incremental_pat_match env holes =
let rec aux p t =
match p, t.t_node with
| PatHole i, _ ->
begin match holes.(i) with
| None -> holes.(i) <- Some t
| Some t' -> if not (t_equal t t') then raise Not_found
end
| PatApp (sp,ss,sl,pl), Tapp (ls,tl) ->
if List.length pl <> List.length tl then raise Not_found;
let th = try Env.find_theory env sp ss with Env.TheoryNotFound _ -> raise Not_found in
let s = ns_find_ls th.th_export sl in
if not (ls_equal s ls) then raise Not_found;
List.iter2 aux pl tl
| _, _ -> raise Not_found in
aux
let pat_match env nb_holes p t =
let holes = Array.make nb_holes None in
incremental_pat_match env holes p t;
Array.map (function None -> raise Not_found | Some t -> t) holes
(* Mathematica pre-compilation *)
type info = {
info_env : Env.env;
info_symbols : Sid.t;
info_ops_of_rel : (string * string * string) Mls.t;
info_syn : syntax_map;
mutable info_vars : vsymbol list;
}
let int_minus = ref ps_equ
let real_minus = ref ps_equ
(** lsymbol, ""/"not ", op, rev_op *)
let arith_meta = register_meta "math arith"
[MTlsymbol;MTstring;MTstring;MTstring]
~desc:"Specify@ how@ to@ pretty-print@ arithmetic@ \
operations@ in@ the@ Mathematica@ format:@\n \
@[\
@[<hov 2>- first@ argument:@ the@ symbol@]@\n\
@[<hov 2>- second@ argument:@ the@ prefix@ to@ put@ before@ the@ term@]@\n\
@[<hov 2>- third@ argument:@ the@ operator@ to@ print@]@\n\
@[<hov 2>- fourth@ argument:@ the@ inverse@ operator@]\
@]"
let find_th env file th =
let theory = Env.find_theory env [file] th in
fun id -> Theory.ns_find_ls theory.Theory.th_export [id]
let get_info env task =
(* unary minus for constants *)
int_minus := find_th env "int" "Int" "prefix -";
real_minus := find_th env "real" "Real" "prefix -";
(* handling of inequalities *)
let ops = on_meta arith_meta (fun acc meta_arg ->
match meta_arg with
| [MAls ls; MAstr s; MAstr op; MAstr rev_op] ->
Mls.add ls (s,op,rev_op) acc
| _ -> assert false) Mls.empty task in
(* sets of known symbols *)
let syn = get_syntax_map task in
let symb = Mid.map (Util.const ()) syn in
let symb = Mls.fold (fun ls _ acc -> Sid.add ls.ls_name acc) ops symb in
let symb = Sid.add ps_equ.ls_name symb in
{
info_env = env;
info_symbols = symb;
info_ops_of_rel = ops;
info_syn = syn;
info_vars = [];
}
(* Mathematica printing *)
let ident_printer =
let bls = [] in (* TODO *)
let san = sanitizer char_to_lalpha char_to_alnum in
create_ident_printer bls ~sanitizer:san
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
let print_const fmt c =
let number_format = {
Number.long_int_support = true;
Number.dec_int_support = Number.Number_default;
Number.hex_int_support = Number.Number_default;
Number.oct_int_support = Number.Number_unsupported;
Number.bin_int_support = Number.Number_unsupported;
Number.def_int_support = Number.Number_unsupported;
Number.dec_real_support = (*Number.Number_default*) Number.Number_unsupported;
Number.hex_real_support = (*Number.Number_default*) Number.Number_unsupported;
Number.frac_real_support = (*Number.Number_unsupported;*)
Number.Number_custom (Number.PrintFracReal ("%s", "(%s/%s)", "(%s/%s)"));
Number.def_real_support = Number.Number_unsupported;
} in
(Number.print number_format) fmt c
let constant_value =
fun t -> match t.t_node with
| Tconst c ->
fprintf str_formatter "%a" print_const c;
flush_str_formatter ()
| Tapp(ls, [{ t_node = Tconst c}])
when ls_equal ls !int_minus || ls_equal ls !real_minus ->
fprintf str_formatter "-%a" print_const c;
flush_str_formatter ()
| _ -> raise Not_found
let rel_error_pat =
PatApp (["real"], "Real", ["infix <="], [
PatApp (["real"], "Abs", ["abs"], [
PatApp (["real"], "Real", ["infix -"], [
PatHole 0;
PatHole 1])]);
PatApp (["real"], "Real", ["infix *"], [
PatHole 2;
PatApp (["real"], "Abs", ["abs"], [
PatHole 1])])])
(* terms *)
let rec print_term info fmt t =
let term = print_term info in
let fmla = print_fmla info in
match t.t_node with
| Tconst c ->
(*Pretty.print_const fmt c*)
print_const fmt c
| Tvar { vs_name = id } ->
print_ident fmt id
| Tapp ( { ls_name = id } ,[] ) ->
begin match query_syntax info.info_syn id with
| Some s -> syntax_arguments s term fmt []
| None -> print_ident fmt id
end
| Tapp ( { ls_name = id } ,[t] )
when try String.sub id.id_string 0 6 = "index_" with Invalid_argument _ -> false ->
fprintf fmt "%a" term t
| Tapp (ls, tl) ->
begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s term fmt tl
(*| None ->
unsupportedTerm t
("math: function '" ^ ls.ls_name.id_string ^ "' is not supported")*)
| None -> begin match tl with
| [] -> fprintf fmt "%a" print_ident ls.ls_name
| _ -> fprintf fmt "%a[%a]"
print_ident ls.ls_name (print_list comma term) tl
end
end
| Tif (f, t1, t2) ->
fprintf fmt "If[%a,@ %a,@ %a]" fmla f term t1 term t2
(*| Tif _ -> unsupportedTerm t
"math: you must eliminate if_then_else"*)
| Tlet _ -> unsupportedTerm t
"math: you must eliminate let in term"
| Tcase _ -> unsupportedTerm t
"math: you must eliminate match"
(*| Tcase (t,bl) ->
print_case print_term info fmt t bl*)
| Teps _ -> unsupportedTerm t
"math: you must eliminate epsilon"
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
(*and print_case _pp info fmt t _bl =
let ts = match t.t_ty with
| Some { ty_node = Tyapp (ts,_) } -> ts
| _ -> Printer.unsupportedTerm t "math: unknown type"
in
fprintf fmt "Match%a[%a]" print_ident ts.ts_name (print_term info) t*)
(* predicates *)
(*let rec*) and print_fmla info fmt f =
let term = print_term info in
let fmla = print_fmla info in
match f.t_node with
| Tapp ({ ls_name = id }, []) ->
begin match query_syntax info.info_syn id with
| Some s -> syntax_arguments s term fmt []
| None -> fprintf fmt "%a == 0" print_ident id
end
| Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
(* TODO: distinguish between type of t1 and t2
the following is OK only for real of integer
*)
begin try
let c1 = constant_value t1 in
fprintf fmt "%a == %s" term t2 c1
with Not_found ->
try
let c2 = constant_value t2 in
fprintf fmt "%a == %s" term t1 c2
with Not_found ->
fprintf fmt "%a - %a == 0" term t1 term t2
end
| Tapp (ls, [t1;t2]) when Mls.mem ls info.info_ops_of_rel ->
let s,op,rev_op = try Mls.find ls info.info_ops_of_rel
with Not_found -> assert false
in
begin try
let t = pat_match info.info_env 3 rel_error_pat f in
let c = constant_value t.(2) in
fprintf fmt "|%a -/ %a| <= %s" term t.(0) term t.(1) c
with Not_found -> try
let c1 = constant_value t1 in
fprintf fmt "%s%a %s %s" s term t2 rev_op c1
with Not_found ->
try
let c2 = constant_value t2 in
fprintf fmt "%s%a %s %s" s term t1 op c2
with Not_found ->
fprintf fmt "%s%a - %a %s 0" s term t1 term t2 op
end
| Tapp (ls, tl) ->
begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s term fmt tl
| None ->
(*unsupportedTerm f
("math: predicate '" ^ ls.ls_name.id_string ^ "' is not supported")*)
begin match tl with
| [] -> fprintf fmt "%a" print_ident ls.ls_name
| _ -> fprintf fmt "%a[%a]"
print_ident ls.ls_name (print_list comma (print_term info)) tl
end
end
(*| Tquant _ ->
unsupportedTerm f "math: quantifiers are not supported"*)
| Tquant (Tforall, fq) ->
let vl, _tl, f = t_open_quant fq in
info.info_vars <- List.append info.info_vars vl;
fprintf fmt "%a" fmla f
| Tquant (Texists, fq) ->
let vl, _tl, f = t_open_quant fq in
let var fmt v = (* TODO: type check v.vs_ty *)
print_ident fmt v.vs_name in
fprintf fmt "Exists[{%a}, %a]"
(print_list comma var) vl fmla f
| Tbinop (Tand, f1, f2) ->
fprintf fmt "(%a &&@ %a)" fmla f1 fmla f2
| Tbinop (Tor, f1, f2) ->
fprintf fmt "(%a ||@ %a)" fmla f1 fmla f2
| Tbinop (Timplies, f1, f2) ->
fprintf fmt "Implies[%a,@ %a]" fmla f1 fmla f2
| Tbinop (Tiff, f1, f2) ->
fprintf fmt "Equivalent[%a,@ %a]" fmla f1 fmla f2
| Tnot f ->
fprintf fmt "Not[%a]" fmla f
| Ttrue ->
fprintf fmt "True"
| Tfalse ->
fprintf fmt "False"
| Tif (f1, f2, f3) ->
fprintf fmt "If[%a,@ %a,@ %a]" fmla f1 fmla f2 fmla f3
| Tlet _ -> unsupportedTerm f
"math: you must eliminate let in formula"
| Tcase _ -> unsupportedTerm f
"math: you must eliminate match"
(*| Tcase (t,bl) ->
print_case print_fmla info fmt t bl*)
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
exception AlreadyDefined
(* TODO *)
let is_number = function
| Tyapp (ts, _) ->
ts.ts_name.id_string = "int" || ts.ts_name.id_string = "real"
| _ -> false
let filter_logic info ((params,funs,preds,types) as acc) (ls,ld) =
if (not (Mid.mem ls.ls_name info.info_symbols)) then
match ls.ls_args, ls.ls_value with
(*| [], Some ty -> if is_number ty.ty_node then (* params (functions without args) *)
((ls,ld)::params,funs,preds,types)
else
(printf "param: %a" print_ident ls.ls_name;
acc)
*)
| _, Some _ty (*when is_number ty.ty_node*) -> (* functions *)
(params,(ls,ld)::funs,preds,types)
| _, None -> (* predicates *)
(params,funs,(ls,ld)::preds,types)
(*| _, _, None -> (* funs/preds without definitions *)
(*unsupported "math: funs/preds without definitions"*)
acc
*)
else acc
let rec filter_hyp info params defs eqs hyps pr f =
match f.t_node with
| Tapp(ls,[t1;t2]) when ls == ps_equ -> (* parameter definition *)
let try_equality t1 t2 =
match t1.t_node with
| Tapp(l,[]) ->
if Hid.mem defs l.ls_name then raise AlreadyDefined;
Hid.add defs l.ls_name ();
t_s_fold (fun _ _ -> ()) (fun _ ls -> Hid.replace defs ls.ls_name ()) () t2;
(* filters out the defined parameter *)
let params = List.filter (fun p -> p.ls_name <> l.ls_name) params in
(*info.info_vars <- List.filter (fun v -> v.vs_name = l.ls_name) info.info_vars;*)
(params, (pr,t1,t2)::eqs, hyps)
| _ -> raise AlreadyDefined in
begin try
try_equality t1 t2
with AlreadyDefined -> try
try_equality t2 t1
with AlreadyDefined ->
(params, eqs, (pr,f)::hyps)
end
| Tbinop (Tand, f1, f2) ->
let (params,eqs,hyps) = filter_hyp info params defs eqs hyps pr f2 in
filter_hyp info params defs eqs hyps pr f1
| Tapp(_,[]) ->
(* Discard (abstracted) predicate variables.
While Mathematica would handle them, it is usually just noise from
Mathematica's point of view and better delegated to a SAT solver. *)
(params,eqs,hyps)
| Ttrue -> (params,eqs,hyps)
| _ ->
(params, eqs, (pr,f)::hyps)
type filter_goal =
| Goal_good of Decl.prsymbol * term
| Goal_bad of string
| Goal_none
let filter_goal pr f =
match f.t_node with
| Tapp(ps,[]) ->