[sledge] Improve doc in Fol

Reviewed By: jvillard

Differential Revision: D24306056

fbshipit-source-id: ec35b7ad6

sledge/src/fol.ml

@@ -19,21 +19,26 @@ module Predsym = Ses.Predsym
 (** Terms, denoting functions from structures to values, built from
     variables and applications of function symbols from various theories. *)
 type trm =
+  (* variables *)
   | Var of {id: int; name: string}
+  (* arithmetic *)
   | Z of Z.t
   | Q of Q.t
   | Neg of trm
   | Add of trm * trm
   | Sub of trm * trm
   | Mulq of Q.t * trm
+  (* sequences (of non-fixed size) *)
   | Splat of trm
   | Sized of {seq: trm; siz: trm}
   | Extract of {seq: trm; off: trm; len: trm}
   | Concat of trm array
+  (* records (with fixed indices) *)
   | Select of {idx: int; rcd: trm}
   | Update of {idx: int; rcd: trm; elt: trm}
   | Record of trm array
   | Ancestor of int
+  (* uninterpreted *)
   | Apply of Funsym.t * trm array
 [@@deriving compare, equal, sexp]
 
@@ -87,21 +92,26 @@ let _Apply f es = Apply (f, es)
     first-order logic connectives. *)
 module Fml : sig
   type fml = private
+    (* propositional constants *)
     | Tt
     | Ff
+    (* equality *)
     | Eq of trm * trm
     | Dq of trm * trm
+    (* arithmetic *)
     | Eq0 of trm  (** [Eq0(x)] iff x = 0 *)
     | Dq0 of trm  (** [Dq0(x)] iff x ≠ 0 *)
     | Gt0 of trm  (** [Gt0(x)] iff x > 0 *)
     | Ge0 of trm  (** [Ge0(x)] iff x ≥ 0 *)
     | Lt0 of trm  (** [Lt0(x)] iff x < 0 *)
     | Le0 of trm  (** [Le0(x)] iff x ≤ 0 *)
+    (* propositional connectives *)
     | And of fml * fml
     | Or of fml * fml
     | Iff of fml * fml
     | Xor of fml * fml
     | Cond of {cnd: fml; pos: fml; neg: fml}
+    (* uninterpreted literals *)
     | UPosLit of Predsym.t * trm array
     | UNegLit of Predsym.t * trm array
   [@@deriving compare, equal, sexp]

sledge/src/fol.mli

@@ -41,26 +41,24 @@ module rec Term : sig
   (* variables *)
   val var : Var.t -> t
 
-  (* constants *)
+  (* arithmetic *)
   val zero : t
   val one : t
   val integer : Z.t -> t
   val rational : Q.t -> t
-
-  (* arithmetic *)
   val neg : t -> t
   val add : t -> t -> t
   val sub : t -> t -> t
   val mulq : Q.t -> t -> t
   val mul : t -> t -> t
 
-  (* sequences *)
+  (* sequences (of non-fixed size) *)
   val splat : t -> t
   val sized : seq:t -> siz:t -> t
   val extract : seq:t -> off:t -> len:t -> t
   val concat : t array -> t
 
-  (* records *)
+  (* records (with fixed indices) *)
   val select : rcd:t -> idx:int -> t
   val update : rcd:t -> idx:int -> elt:t -> t
   val record : t array -> t
@@ -115,9 +113,11 @@ and Formula : sig
   val tt : t
   val ff : t
 
-  (* comparisons *)
+  (* equality *)
   val eq : Term.t -> Term.t -> t
   val dq : Term.t -> Term.t -> t
+
+  (* arithmetic *)
   val eq0 : Term.t -> t
   val dq0 : Term.t -> t
   val gt0 : Term.t -> t