symbolic mathematics engine in OCaml with differentiation, integration, simplification, and numerical methods
17

Configure Feed

Select the types of activity you want to include in your feed.

leibniz / lib / substitute.ml
6.6 kB 194 lines
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