symbolic mathematics engine in OCaml with differentiation, integration, simplification, and numerical methods
1open Expr
2
3let rec substitute var replacement = function
4 | Const _ as c -> c
5 | SymConst _ as s -> s
6 | Var v -> if v = var then replacement else Var v
7 | Add (e1, e2) -> Add (substitute var replacement e1, substitute var replacement e2)
8 | Sub (e1, e2) -> Sub (substitute var replacement e1, substitute var replacement e2)
9 | Mul (e1, e2) -> Mul (substitute var replacement e1, substitute var replacement e2)
10 | Div (e1, e2) -> Div (substitute var replacement e1, substitute var replacement e2)
11 | Pow (e1, e2) -> Pow (substitute var replacement e1, substitute var replacement e2)
12 | Neg e -> Neg (substitute var replacement e)
13 | Sin e -> Sin (substitute var replacement e)
14 | Cos e -> Cos (substitute var replacement e)
15 | Tan e -> Tan (substitute var replacement e)
16 | Sinh e -> Sinh (substitute var replacement e)
17 | Cosh e -> Cosh (substitute var replacement e)
18 | Tanh e -> Tanh (substitute var replacement e)
19 | Asin e -> Asin (substitute var replacement e)
20 | Acos e -> Acos (substitute var replacement e)
21 | Atan e -> Atan (substitute var replacement e)
22 | Atan2 (e1, e2) -> Atan2 (substitute var replacement e1, substitute var replacement e2)
23 | Exp e -> Exp (substitute var replacement e)
24 | Ln e -> Ln (substitute var replacement e)
25 | Log (e1, e2) -> Log (substitute var replacement e1, substitute var replacement e2)
26 | Sqrt e -> Sqrt (substitute var replacement e)
27 | Abs e -> Abs (substitute var replacement e)
28
29let substitute_many subs expr =
30 List.fold_left (fun e (var, repl) -> substitute var repl e) expr subs
31
32type pattern =
33 | PVar of string
34 | PWild
35 | PConst of float
36 | PSymConst of sym_const
37 | POp of string * pattern list
38
39type bindings = (string * expr) list
40
41let rec matches (pat : pattern) (e : expr) : bindings option =
42 match (pat, e) with
43 | PWild, _ -> Some []
44 | PVar v, e -> Some [(v, e)]
45 | PConst c1, Const c2 when c1 = c2 -> Some []
46 | PSymConst s1, SymConst s2 when s1 = s2 -> Some []
47 | POp ("Add", [p1; p2]), Add (e1, e2) ->
48 matches_binary p1 p2 e1 e2
49 | POp ("Sub", [p1; p2]), Sub (e1, e2) ->
50 matches_binary p1 p2 e1 e2
51 | POp ("Mul", [p1; p2]), Mul (e1, e2) ->
52 matches_binary p1 p2 e1 e2
53 | POp ("Div", [p1; p2]), Div (e1, e2) ->
54 matches_binary p1 p2 e1 e2
55 | POp ("Pow", [p1; p2]), Pow (e1, e2) ->
56 matches_binary p1 p2 e1 e2
57 | POp ("Neg", [p]), Neg e ->
58 matches p e
59 | POp ("Sin", [p]), Sin e ->
60 matches p e
61 | POp ("Cos", [p]), Cos e ->
62 matches p e
63 | POp ("Tan", [p]), Tan e ->
64 matches p e
65 | POp ("Sinh", [p]), Sinh e ->
66 matches p e
67 | POp ("Cosh", [p]), Cosh e ->
68 matches p e
69 | POp ("Tanh", [p]), Tanh e ->
70 matches p e
71 | POp ("Asin", [p]), Asin e ->
72 matches p e
73 | POp ("Acos", [p]), Acos e ->
74 matches p e
75 | POp ("Atan", [p]), Atan e ->
76 matches p e
77 | POp ("Atan2", [p1; p2]), Atan2 (e1, e2) ->
78 matches_binary p1 p2 e1 e2
79 | POp ("Exp", [p]), Exp e ->
80 matches p e
81 | POp ("Ln", [p]), Ln e ->
82 matches p e
83 | POp ("Log", [p1; p2]), Log (e1, e2) ->
84 matches_binary p1 p2 e1 e2
85 | POp ("Sqrt", [p]), Sqrt e ->
86 matches p e
87 | POp ("Abs", [p]), Abs e ->
88 matches p e
89 | _ -> None
90
91and matches_binary p1 p2 e1 e2 =
92 match matches p1 e1 with
93 | None -> None
94 | Some b1 ->
95 match matches p2 e2 with
96 | None -> None
97 | Some b2 -> Some (b1 @ b2)
98
99let rec instantiate (template : pattern) (bindings : bindings) : expr option =
100 match template with
101 | PWild -> None
102 | PVar v -> List.assoc_opt v bindings
103 | PConst c -> Some (Const c)
104 | PSymConst s -> Some (SymConst s)
105 | POp ("Add", [p1; p2]) ->
106 (match (instantiate p1 bindings, instantiate p2 bindings) with
107 | Some e1, Some e2 -> Some (Add (e1, e2))
108 | _ -> None)
109 | POp ("Sub", [p1; p2]) ->
110 (match (instantiate p1 bindings, instantiate p2 bindings) with
111 | Some e1, Some e2 -> Some (Sub (e1, e2))
112 | _ -> None)
113 | POp ("Mul", [p1; p2]) ->
114 (match (instantiate p1 bindings, instantiate p2 bindings) with
115 | Some e1, Some e2 -> Some (Mul (e1, e2))
116 | _ -> None)
117 | POp ("Div", [p1; p2]) ->
118 (match (instantiate p1 bindings, instantiate p2 bindings) with
119 | Some e1, Some e2 -> Some (Div (e1, e2))
120 | _ -> None)
121 | POp ("Pow", [p1; p2]) ->
122 (match (instantiate p1 bindings, instantiate p2 bindings) with
123 | Some e1, Some e2 -> Some (Pow (e1, e2))
124 | _ -> None)
125 | POp ("Neg", [p]) ->
126 (match instantiate p bindings with
127 | Some e -> Some (Neg e)
128 | None -> None)
129 | POp ("Sin", [p]) ->
130 (match instantiate p bindings with
131 | Some e -> Some (Sin e)
132 | None -> None)
133 | POp ("Cos", [p]) ->
134 (match instantiate p bindings with
135 | Some e -> Some (Cos e)
136 | None -> None)
137 | POp ("Tan", [p]) ->
138 (match instantiate p bindings with
139 | Some e -> Some (Tan e)
140 | None -> None)
141 | POp ("Sinh", [p]) ->
142 (match instantiate p bindings with
143 | Some e -> Some (Sinh e)
144 | None -> None)
145 | POp ("Cosh", [p]) ->
146 (match instantiate p bindings with
147 | Some e -> Some (Cosh e)
148 | None -> None)
149 | POp ("Tanh", [p]) ->
150 (match instantiate p bindings with
151 | Some e -> Some (Tanh e)
152 | None -> None)
153 | POp ("Asin", [p]) ->
154 (match instantiate p bindings with
155 | Some e -> Some (Asin e)
156 | None -> None)
157 | POp ("Acos", [p]) ->
158 (match instantiate p bindings with
159 | Some e -> Some (Acos e)
160 | None -> None)
161 | POp ("Atan", [p]) ->
162 (match instantiate p bindings with
163 | Some e -> Some (Atan e)
164 | None -> None)
165 | POp ("Atan2", [p1; p2]) ->
166 (match (instantiate p1 bindings, instantiate p2 bindings) with
167 | Some e1, Some e2 -> Some (Atan2 (e1, e2))
168 | _ -> None)
169 | POp ("Exp", [p]) ->
170 (match instantiate p bindings with
171 | Some e -> Some (Exp e)
172 | None -> None)
173 | POp ("Ln", [p]) ->
174 (match instantiate p bindings with
175 | Some e -> Some (Ln e)
176 | None -> None)
177 | POp ("Log", [p1; p2]) ->
178 (match (instantiate p1 bindings, instantiate p2 bindings) with
179 | Some e1, Some e2 -> Some (Log (e1, e2))
180 | _ -> None)
181 | POp ("Sqrt", [p]) ->
182 (match instantiate p bindings with
183 | Some e -> Some (Sqrt e)
184 | None -> None)
185 | POp ("Abs", [p]) ->
186 (match instantiate p bindings with
187 | Some e -> Some (Abs e)
188 | None -> None)
189 | _ -> None
190
191let rewrite pattern template expr =
192 match matches pattern expr with
193 | None -> None
194 | Some bindings -> instantiate template bindings