[sledge] Document function symbols

Reviewed By: jvillard

Differential Revision: D24306086

fbshipit-source-id: 00f2f92d8

sledge/src/ses/funsym.mli

@@ -7,24 +7,36 @@
 
 (** Function Symbols *)
 
+(** [Uninterp] functions symbols are treated as uninterpreted, while the
+    others support some ad hoc simplification. For example, function symbols
+    applied to literal values of the expected sorts are reduced to literal
+    values. *)
 type t =
   | Float of string
   | Label of {parent: string; name: string}
-  | Mul
-  | Div
+  | Mul  (** Multiplication *)
+  | Div  (** Division, for integers result is truncated toward zero *)
   | Rem
+      (** Remainder of division, satisfies [a = b * div a b + rem a b] and
+          for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)
   | EmptyRecord
   | RecRecord of int
-  | BitAnd
-  | BitOr
-  | BitXor
-  | BitShl
-  | BitLshr
-  | BitAshr
+  | BitAnd  (** Bitwise logical And *)
+  | BitOr  (** Bitwise logical inclusive Or *)
+  | BitXor  (** Bitwise logical eXclusive or *)
+  | BitShl  (** Bitwise Shift left *)
+  | BitLshr  (** Bitwise Logical shift right *)
+  | BitAshr  (** Bitwise Arithmetic shift right *)
   | Signed of int
+      (** [Signed n] interprets its argument as an [n]-bit signed integer.
+          That is, it two's-complement--decodes the low [n] bits of the
+          infinite two's-complement encoding of the argument. *)
   | Unsigned of int
+      (** [Unsigned n] interprets its argument as an [n]-bit unsigned
+          integer. That is, it unsigned-binary--decodes the low [n] bits of
+          the infinite two's-complement encoding of the argument. *)
   | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t}
-  | Uninterp of string
+  | Uninterp of string  (** Uninterpreted function symbol *)
 [@@deriving compare, equal, sexp]
 
 val pp : t pp