Summary:
Apply normalization to conditional terms similar to conditional
formulas: evaluate terms with literal conditions, equal branches, and
ensure the condition is not negative.
Reviewed By: jvillard
Differential Revision: D24532344
fbshipit-source-id: 7818dc496
Summary:
Operations over the core representation are more useful in the core
representation modules.
Reviewed By: ngorogiannis
Differential Revision: D24532340
fbshipit-source-id: f1eab822d
Summary:
The Fol.Term and Fol.Formula provide an interface which supports
if-then-else terms and formulas, while the underlying representation
in Trm does not and Fml only supports if-then-else over formulas, not
terms. The implementation of the rest of the first-order solver needs
to use the underlying, normalized, representation. This diff exports
Trm and Fml to separate modules for this purpose. Later, they will be
packed into a library for the first-order solver, and only used from
within.
Reviewed By: ngorogiannis
Differential Revision: D24532351
fbshipit-source-id: 7310827da
Summary:
And add Monad.Make to implement the full interface from return and
bind.
Reviewed By: ngorogiannis
Differential Revision: D24532341
fbshipit-source-id: 5740ba1c2
Summary:
The iterator is simpler to define and all the traversals are then
available through Iter.
Reviewed By: jvillard
Differential Revision: D24401743
fbshipit-source-id: 81f0653d9
Summary:
It is redundant to include the unit of conjunction in conjunction
formulas (resp., disjunction).
Reviewed By: jvillard
Differential Revision: D24371084
fbshipit-source-id: 6edc151e5
Summary: Simplify output of arithmetic terms, and omit trivial pure part of Sh.
Reviewed By: jvillard
Differential Revision: D24371082
fbshipit-source-id: 91f2117d3
Summary:
Normalization of literal formulas is determined by their term
arguments. Logically, this is part of the theories, so move this code
out of the Propositional module which is theory-independent and into
Fol, which is theory-sensitive.
Reviewed By: jvillard
Differential Revision: D24371081
fbshipit-source-id: f80a19ab8
Summary:
Change the type of `fold` functions to enable them to compose
better. The guiding reasoning behind using types such as:
```
val fold : 'a t -> 's -> f:('a -> 's -> 's) -> 's
```
is:
1. The function argument should be labeled. This is so that it can be
reordered relative to the others, since it is often a multi-line
`fun` expression.
2. The function argument should come last. This enables its
arguments (which are often polymorphic) to benefit from type-based
disambiguation information determined by the types of the other
arguments at the call sites.
3. The function argument's type should produce an
accumulator-transformer when partially-applied. That is,
`f x : 's -> 's`. This composes well with other functions designed
to produce transformers/endofunctions when partially applied, and
in particular improves the common case of composing folds into
"state-passing style" code.
4. The fold function itself should produce an accumulator-transformer
when partially applied. So `'a t -> 's -> f:_ -> 's` rather than
`'s -> 'a t -> f:_ -> 's` or `'a t -> init:'s -> f:_ -> 's` etc.
Reviewed By: jvillard
Differential Revision: D24306063
fbshipit-source-id: 13bd8bbee
Summary:
The changes in set_intf.ml dictate the rest. The previous API
minimized changes when changing the backing implementation. But that
API is hostile toward composition, partial application, and
state-passing style code.
Reviewed By: jvillard
Differential Revision: D24306089
fbshipit-source-id: 00a09f486
Summary:
Preceding commit reversed Map.to_iter to match the previous behavior
of to_list.
Reviewed By: jvillard
Differential Revision: D24306051
fbshipit-source-id: aad12e434
Summary:
The changes in map_intf.ml dictate the rest. The previous API
minimized changes when changing the backing implementation. But that
API is hostile toward composition, partial application, and
state-passing style code.
Reviewed By: jvillard
Differential Revision: D24306050
fbshipit-source-id: 71e286d4e
Summary:
Remove `-error-style short` from the compilation flags since it causes
merlin to complain, see https://github.com/ocaml/merlin/issues/1176.
After this diff, developers will need to set `OCAML_ERROR_STYLE=short`
in their environment.
Reviewed By: jvillard
Differential Revision: D24306066
fbshipit-source-id: 9c4f26393
Summary:
The usage of equal_or_opposite boils down to evaluating formulas on
propositional constants, which seems clearer.
Reviewed By: jvillard
Differential Revision: D24306104
fbshipit-source-id: df5d07628
Summary:
Represent And and Or formulas as pairs of sets of formulas. One set is
interpreted as positive and the other as negative. This results in
normalization with respect to associativity, commutativity, and unit
laws. This does not normalize distributivity laws, e.g. formulas are
not expanded to disjunctive-normal form or conjunctive-normal
form. Additionally, "zero" laws P ∧ ¬P iff ⊥ and P ∨ ¬P iff ⊤ are
cheaply detected and normalized. Note that formulas are already in
negation-normal form.
Reviewed By: jvillard
Differential Revision: D24306072
fbshipit-source-id: e52265a44
Summary:
Some Iter and Containers functions take optional arguments that
default to polymorphic comparison. This diff wraps all of these making
the argument non-optional to avoid silently using polymorphic compare.
Reviewed By: ngorogiannis
Differential Revision: D24306074
fbshipit-source-id: 34772ee86
Summary:
Expressing the sort of short-circuit evaluation in the changed code is
conceptually more direct using iterators.
Also, when using With_return, getting usable backtraces relies on the
compiler recognizing that the `raise` in the implementation of
`Base.Exn.raise_without_backtrace` should be a `reraise`. Using
iterators avoids this potential fragility.
Reviewed By: jvillard
Differential Revision: D24306094
fbshipit-source-id: b1abe04fb
Summary:
Change implementation of IArray from a wrapper of
Core_kernel.Array.Permissioned to NS.Array, and remove magic. Also
add operations to Array and Iter in order to ensure that IArray is an
extremely thin wrapper of Array: only defining conversions to/from
arrays as well as adding hashing support.
Reviewed By: jvillard
Differential Revision: D24306095
fbshipit-source-id: 97b9187be
Summary:
Term.const_of is misleading as it is easy to expect it checks if a
term is a constant, or to expect that it returns the constant part of
a term. Instead, Term.split_const is clearer:
```
val split_const : t -> t * Q.t
(** Splits a term into the sum of its constant and non-constant parts.
That is, [split_const a] is [(b, c)] such that [a = b + c] and the
absolute value of [c] is maximal. *)
```
Reviewed By: ngorogiannis
Differential Revision: D24306065
fbshipit-source-id: ba15958ad
Josh Berdine