vm.fail
symbolic mathematics engine in OCaml with differentiation, integration, simplification, and numerical methods
1open Expr
2open Simplify
3
4type domain =
5 | Real
6 | Complex
7 | Positive
8 | Negative
9 | NonNegative
10 | NonPositive
11 | Integer
12 | Natural
13 | Rational
14 | Even
15 | Odd
16
17type assumption = (string * domain) list
18
19let assume var domain assumptions =
20 (var, domain) :: List.remove_assoc var assumptions
21
22let get_domain var assumptions =
23 List.assoc_opt var assumptions
24
25let is_compatible domain1 domain2 =
26 match (domain1, domain2) with
27 | d1, d2 when d1 = d2 -> true
28 | Positive, (Real | Complex | NonNegative | Rational) -> true
29 | Negative, (Real | Complex | NonPositive | Rational) -> true
30 | NonNegative, (Real | Complex | Rational) -> true
31 | NonPositive, (Real | Complex | Rational) -> true
32 | Integer, (Real | Complex | Rational) -> true
33 | Natural, (Integer | Real | Complex | NonNegative | Rational) -> true
34 | Even, (Integer | Real | Complex | Rational) -> true
35 | Odd, (Integer | Real | Complex | Rational) -> true
36 | _ -> false
37
38let refine assumptions _expr _condition =
39 Some assumptions
40
41let simplify_with assumptions expr =
42 let rec simplify_expr = function
43 | Sqrt (Pow (Var v, Const 2.0)) ->
44 (match get_domain v assumptions with
45 | Some Positive | Some NonNegative -> Var v
46 | Some Negative | Some NonPositive -> Neg (Var v)
47 | _ -> Abs (Var v))
48 | Abs (Var v) as e ->
49 (match get_domain v assumptions with
50 | Some Positive | Some NonNegative -> Var v
51 | Some Negative | Some NonPositive -> Neg (Var v)
52 | _ -> e)
53 | Pow (Var v, Const n) as e when Float.is_integer n && int_of_float n mod 2 = 0 ->
54 (match get_domain v assumptions with
55 | Some Positive | Some NonNegative | Some Negative | Some NonPositive -> e
56 | _ -> e)
57 | Add (e1, e2) -> Add (simplify_expr e1, simplify_expr e2)
58 | Sub (e1, e2) -> Sub (simplify_expr e1, simplify_expr e2)
59 | Mul (e1, e2) -> Mul (simplify_expr e1, simplify_expr e2)
60 | Div (e1, e2) -> Div (simplify_expr e1, simplify_expr e2)
61 | Pow (e1, e2) -> Pow (simplify_expr e1, simplify_expr e2)
62 | Neg e -> Neg (simplify_expr e)
63 | Sin e -> Sin (simplify_expr e)
64 | Cos e -> Cos (simplify_expr e)
65 | Tan e -> Tan (simplify_expr e)
66 | Sinh e -> Sinh (simplify_expr e)
67 | Cosh e -> Cosh (simplify_expr e)
68 | Tanh e -> Tanh (simplify_expr e)
69 | Asin e -> Asin (simplify_expr e)
70 | Acos e -> Acos (simplify_expr e)
71 | Atan e -> Atan (simplify_expr e)
72 | Atan2 (e1, e2) -> Atan2 (simplify_expr e1, simplify_expr e2)
73 | Exp e -> Exp (simplify_expr e)
74 | Ln e -> Ln (simplify_expr e)
75 | Log (e1, e2) -> Log (simplify_expr e1, simplify_expr e2)
76 | Sqrt e -> Sqrt (simplify_expr e)
77 | Abs e -> Abs (simplify_expr e)
78 | e -> e
79 in
80 simplify (simplify_expr expr)
81
82let verify_inequality _expr _assumptions =
83 None