@@ -665,6 +665,36 @@ let bin ?comment (op : J.binop) (e0 : t) (e1 : t) : t =
665665let string_of_expression = ref (fun _ -> " " )
666666let debug = false
667667
668+ (* *
669+ [push_negation e] attempts to simplify a negated expression by pushing the negation
670+ deeper into the expression tree. Returns [Some simplified] if simplification is possible,
671+ [None] otherwise.
672+
673+ Simplification rules:
674+ - [!(not e)] -> [e]
675+ - [!true] -> [false]
676+ - [!false] -> [true]
677+ - [!(a === b)] -> [a !== b]
678+ - [!(a !== b)] -> [a === b]
679+ - [!(a && b)] -> [!a || !b] (De Morgan's law)
680+ - [!(a || b)] -> [!a && !b] (De Morgan's law)
681+ *)
682+ let rec push_negation (e : t ) : t option =
683+ match e.expression_desc with
684+ | Js_not e -> Some e
685+ | Bool b -> Some (bool (not b))
686+ | Bin (EqEqEq, a , b ) -> Some {e with expression_desc = Bin (NotEqEq , a, b)}
687+ | Bin (NotEqEq, a , b ) -> Some {e with expression_desc = Bin (EqEqEq , a, b)}
688+ | Bin (And, a , b ) -> (
689+ match (push_negation a, push_negation b) with
690+ | Some a_ , Some b_ -> Some {e with expression_desc = Bin (Or , a_, b_)}
691+ | _ -> None )
692+ | Bin (Or, a , b ) -> (
693+ match (push_negation a, push_negation b) with
694+ | Some a_ , Some b_ -> Some {e with expression_desc = Bin (And , a_, b_)}
695+ | _ -> None )
696+ | _ -> None
697+
668698(* *
669699 [simplify_and e1 e2] attempts to simplify the boolean AND expression [e1 && e2].
670700 Returns [Some simplified] if simplification is possible, [None] otherwise.
@@ -802,6 +832,16 @@ let rec simplify_and (e1 : t) (e2 : t) : t option =
802832 - [e || true] -> [true]
803833 - [false || e] -> [e]
804834 - [e || false] -> [e]
835+
836+ Algebraic transformation strategy:
837+ When basic rules don't apply, attempts to leverage [simplify_and] by:
838+ 1. Using the equivalence: [e1 || e2 ≡ !(!(e1) && !(e2))]
839+ 2. Applying [push_negation] to get [!(e1)] and [!(e2)]
840+ 3. Using [simplify_and] on these negated terms
841+ 4. If successful, applying [push_negation] again to get the final result
842+
843+ This transformation allows reuse of [simplify_and]'s more extensive optimizations
844+ in the context of OR expressions.
805845*)
806846and simplify_or (e1 : t ) (e2 : t ) : t option =
807847 if debug then
@@ -813,7 +853,13 @@ and simplify_or (e1 : t) (e2 : t) : t option =
813853 | _ , Bool true -> Some true_
814854 | Bool false , _ -> Some e2
815855 | _ , Bool false -> Some e1
816- | _ -> None
856+ | _ -> (
857+ match (push_negation e1, push_negation e2) with
858+ | Some e1_ , Some e2_ -> (
859+ match simplify_and e1_ e2_ with
860+ | Some e -> push_negation e
861+ | None -> None )
862+ | _ -> None )
817863
818864let and_ ?comment (e1 : t ) (e2 : t ) : t =
819865 match (e1.expression_desc, e2.expression_desc) with
0 commit comments