[sledge] Rename Fol core types to follow convention

Summary: Use Trm.t and Fml.t instead of Trm.trm and Fml.fml.

Reviewed By: ngorogiannis

Differential Revision: D24532345

fbshipit-source-id: a3b9b7dc9

sledge/src/fml.ml

@@ -8,9 +8,9 @@
 (** Formulas *)
 
 module Prop = Propositional.Make (Trm)
-module Fmls = Prop.Fmls
+module Set = Prop.Fmls
 
-type fmls = Fmls.t
+type set = Set.t
 
 include Prop.Fml
 
@@ -19,13 +19,13 @@ let ff = _Not tt
 let bool b = if b then tt else ff
 
 let _Eq0 x =
-  match (x : Trm.trm) with
+  match (x : Trm.t) with
   | Z z -> bool (Z.equal Z.zero z)
   | Q q -> bool (Q.equal Q.zero q)
   | x -> _Eq0 x
 
 let _Pos x =
-  match (x : Trm.trm) with
+  match (x : Trm.t) with
   | Z z -> bool (Z.gt z Z.zero)
   | Q q -> bool (Q.gt q Q.zero)
   | x -> _Pos x
@@ -35,7 +35,7 @@ let _Eq x y =
   else if y == Trm.zero then _Eq0 x
   else
     let sort_eq x y =
-      match Sign.of_int (Trm.compare_trm x y) with
+      match Sign.of_int (Trm.compare x y) with
       | Neg -> _Eq x y
       | Zero -> tt
       | Pos -> _Eq y x
@@ -51,8 +51,7 @@ let _Eq x y =
         let l = min m n in
         let length_common_prefix =
           let rec find_lcp i =
-            if i < l && Trm.equal_trm a.(i) b.(i) then find_lcp (i + 1)
-            else i
+            if i < l && Trm.equal a.(i) b.(i) then find_lcp (i + 1) else i
           in
           find_lcp 0
         in
@@ -60,8 +59,7 @@ let _Eq x y =
         else
           let length_common_suffix =
             let rec find_lcs i =
-              if Trm.equal_trm a.(m - 1 - i) b.(n - 1 - i) then
-                find_lcs (i + 1)
+              if Trm.equal a.(m - 1 - i) b.(n - 1 - i) then find_lcs (i + 1)
               else i
             in
             find_lcs 0

sledge/src/fml.mli

@@ -8,15 +8,13 @@
 (** Formulas *)
 
 open Propositional_intf
-include FORMULA with type trm := Trm.trm
-module Fmls : FORMULA_SET with type elt := fml with type t = fmls
+include FORMULA with type trm := Trm.t
+module Set : FORMULA_SET with type elt := t with type t = set
 
-type trm := Trm.trm
-
-val tt : fml
-val ff : fml
-val bool : bool -> fml
-val _Eq0 : trm -> fml
-val _Pos : trm -> fml
-val _Eq : trm -> trm -> fml
-val vars : fml -> Trm.Var.t iter
+val tt : t
+val ff : t
+val bool : bool -> t
+val _Eq0 : Trm.t -> t
+val _Pos : Trm.t -> t
+val _Eq : Trm.t -> Trm.t -> t
+val vars : t -> Var.t iter

sledge/src/fol.ml

@@ -9,6 +9,8 @@ open Trm
 open Fml
 
 type var = Var.t
+type trm = Trm.t [@@deriving compare, equal, sexp]
+type fml = Fml.t [@@deriving compare, equal, sexp]
 
 (*
  * Conditional terms
@@ -47,11 +49,11 @@ let ppx_f strength fs fml =
       pf "(%a@ @<2>%s %a)" Q.pp (Q.neg c) op (Arith.ppx strength) a
     in
     let pp_join sep pos neg =
-      pf "(%a%t%a)" (Fmls.pp ~sep pp) pos
+      pf "(%a%t%a)" (Fml.Set.pp ~sep pp) pos
         (fun ppf ->
-          if (not (Fmls.is_empty pos)) && not (Fmls.is_empty neg) then
+          if (not (Fml.Set.is_empty pos)) && not (Fml.Set.is_empty neg) then
             Format.fprintf ppf sep )
-        (Fmls.pp ~sep (fun fs fml -> pp fs (_Not fml)))
+        (Fml.Set.pp ~sep (fun fs fml -> pp fs (_Not fml)))
         neg
     in
     match (fml : fml) with
@@ -114,8 +116,8 @@ let mapN f e cons xs =
   if xs' == xs then e else cons xs'
 
 let map_pos_neg f e cons ~pos ~neg =
-  let pos' = Fmls.map ~f pos in
-  let neg' = Fmls.map ~f neg in
+  let pos' = Fml.Set.map ~f pos in
+  let neg' = Fml.Set.map ~f neg in
   if pos' == pos && neg' == neg then e else cons ~pos:pos' ~neg:neg'
 
 (** map_trms *)
@@ -531,7 +533,7 @@ module Formula = struct
 
   let fold_pos_neg ~pos ~neg s ~f =
     let f_not p s = f (_Not p) s in
-    Fmls.fold ~f:f_not neg (Fmls.fold ~f pos s)
+    Fml.Set.fold ~f:f_not neg (Fml.Set.fold ~f pos s)
 
   let fold_dnf :
          meet1:('literal -> 'conjunction -> 'conjunction)

sledge/src/propositional.ml

@@ -10,12 +10,10 @@
 include Propositional_intf
 
 module Make (Trm : TERM) = struct
-  open Trm
-
   (** Sets of formulas *)
-  module rec Fmls : (FORMULA_SET with type elt := Fml.fml) = struct
+  module rec Fmls : (FORMULA_SET with type elt := Fml.t) = struct
     module T = struct
-      type t = Fml.fml [@@deriving compare, equal, sexp]
+      type t = Fml.t [@@deriving compare, equal, sexp]
     end
 
     include Set.Make (T)
@@ -25,23 +23,23 @@ module Make (Trm : TERM) = struct
   (** Formulas, built from literals with predicate symbols from various
       theories, and propositional constants and connectives. Denote sets of
       structures. *)
-  and Fml : (FORMULA with type trm := Trm.trm with type fmls := Fmls.t) =
+  and Fml : (FORMULA with type trm := Trm.t with type set := Fmls.t) =
   struct
-    type fml =
+    type t =
       | Tt
-      | Eq of trm * trm
-      | Eq0 of trm
-      | Pos of trm
-      | Not of fml
+      | Eq of Trm.t * Trm.t
+      | Eq0 of Trm.t
+      | Pos of Trm.t
+      | Not of t
       | And of {pos: Fmls.t; neg: Fmls.t}
       | Or of {pos: Fmls.t; neg: Fmls.t}
-      | Iff of fml * fml
-      | Cond of {cnd: fml; pos: fml; neg: fml}
-      | Lit of Ses.Predsym.t * trm array
+      | Iff of t * t
+      | Cond of {cnd: t; pos: t; neg: t}
+      | Lit of Ses.Predsym.t * Trm.t array
     [@@deriving compare, equal, sexp]
 
     let invariant f =
-      let@ () = Invariant.invariant [%here] f [%sexp_of: fml] in
+      let@ () = Invariant.invariant [%here] f [%sexp_of: t] in
       match f with
       (* formulas are in negation-normal form *)
       | Not (Not _ | And _ | Or _ | Cond _) -> assert false
@@ -55,7 +53,7 @@ module Make (Trm : TERM) = struct
       | Cond {cnd= Not _ | Or _} -> assert false
       | _ -> ()
 
-    let sort_fml x y = if compare_fml x y <= 0 then (x, y) else (y, x)
+    let sort x y = if compare x y <= 0 then (x, y) else (y, x)
 
     (** Some normalization is necessary for [embed_into_fml] (defined below)
         to be left inverse to [embed_into_cnd]. Essentially
@@ -93,7 +91,7 @@ module Make (Trm : TERM) = struct
     let _Or ~pos ~neg = _Join (fun ~pos ~neg -> Or {pos; neg}) tt ~pos ~neg
 
     let join _Cons zero split_pos_neg p q =
-      ( if equal_fml p zero || equal_fml q zero then zero
+      ( if equal p zero || equal q zero then zero
       else
         let pp, pn = split_pos_neg p in
         if Fmls.is_empty pp && Fmls.is_empty pn then q
@@ -126,22 +124,22 @@ module Make (Trm : TERM) = struct
 
     let rec eval_iff p q =
       match (p, q) with
-      | p, Not p' | Not p', p -> if equal_fml p p' then Some false else None
+      | p, Not p' | Not p', p -> if equal p p' then Some false else None
       | And {pos= ap; neg= an}, Or {pos= op; neg= on}
        |Or {pos= op; neg= on}, And {pos= ap; neg= an}
         when Fmls.equal ap on && Fmls.equal an op ->
           Some false
       | Cond {cnd= c; pos= p; neg= n}, Cond {cnd= c'; pos= p'; neg= n'} ->
-          if equal_fml c c' then
+          if equal c c' then
             match eval_iff p p' with
             | Some false -> (
               match eval_iff n n' with
               | Some false -> Some false
               | _ -> None )
-            | Some true -> if equal_fml n n' then Some true else None
+            | Some true -> if equal n n' then Some true else None
             | None -> None
           else None
-      | _ -> if equal_fml p q then Some true else None
+      | _ -> if equal p q then Some true else None
 
     let _Iff p q =
       ( match (p, q) with
@@ -151,7 +149,7 @@ module Make (Trm : TERM) = struct
         match eval_iff p q with
         | Some b -> bool b
         | None ->
-            let p, q = sort_fml p q in
+            let p, q = sort p q in
             Iff (p, q) ) )
       |> check invariant
 

sledge/src/propositional_intf.ml

@@ -10,7 +10,7 @@
 open Ses
 
 module type TERM = sig
-  type trm [@@deriving compare, equal, sexp]
+  type t [@@deriving compare, equal, sexp]
 end
 
 (** Formulas, built from literals with predicate symbols from various
@@ -18,9 +18,9 @@ end
     structures. *)
 module type FORMULA = sig
   type trm
-  type fmls
+  type set
 
-  type fml = private
+  type t = private
     (* propositional constants *)
     | Tt
     (* equality *)
@@ -29,28 +29,28 @@ module type FORMULA = sig
     | Eq0 of trm  (** [Eq0(x)] iff x = 0 *)
     | Pos of trm  (** [Pos(x)] iff x > 0 *)
     (* propositional connectives *)
-    | Not of fml
-    | And of {pos: fmls; neg: fmls}
-    | Or of {pos: fmls; neg: fmls}
-    | Iff of fml * fml
-    | Cond of {cnd: fml; pos: fml; neg: fml}
+    | Not of t
+    | And of {pos: set; neg: set}
+    | Or of {pos: set; neg: set}
+    | Iff of t * t
+    | Cond of {cnd: t; pos: t; neg: t}
     (* uninterpreted literals *)
     | Lit of Predsym.t * trm array
   [@@deriving compare, equal, sexp]
 
-  val mk_Tt : unit -> fml
-  val _Eq : trm -> trm -> fml
-  val _Eq0 : trm -> fml
-  val _Pos : trm -> fml
-  val _Not : fml -> fml
-  val _And : pos:fmls -> neg:fmls -> fml
-  val _Or : pos:fmls -> neg:fmls -> fml
-  val _Iff : fml -> fml -> fml
-  val _Cond : fml -> fml -> fml -> fml
-  val _Lit : Predsym.t -> trm array -> fml
-  val and_ : fml -> fml -> fml
-  val or_ : fml -> fml -> fml
-  val trms : fml -> trm iter
+  val mk_Tt : unit -> t
+  val _Eq : trm -> trm -> t
+  val _Eq0 : trm -> t
+  val _Pos : trm -> t
+  val _Not : t -> t
+  val _And : pos:set -> neg:set -> t
+  val _Or : pos:set -> neg:set -> t
+  val _Iff : t -> t -> t
+  val _Cond : t -> t -> t -> t
+  val _Lit : Predsym.t -> trm array -> t
+  val and_ : t -> t -> t
+  val or_ : t -> t -> t
+  val trms : t -> trm iter
 end
 
 (** Sets of formulas *)
@@ -61,7 +61,6 @@ module type FORMULA_SET = sig
 end
 
 module type MAKE = functor (Trm : TERM) -> sig
-  module rec Fml :
-    (FORMULA with type trm := Trm.trm with type fmls := Fmls.t)
-  and Fmls : (FORMULA_SET with type elt := Fml.fml)
+  module rec Fml : (FORMULA with type trm := Trm.t with type set := Fmls.t)
+  and Fmls : (FORMULA_SET with type elt := Fml.t)
 end

sledge/src/trm.ml

@@ -15,12 +15,12 @@ let pp_boxed fs fmt =
 
 (** Variable terms, represented as a subtype of general terms *)
 module rec Var : sig
-  include Ses.Var_intf.VAR with type t = private Trm.trm
+  include Ses.Var_intf.VAR with type t = private Trm.t
 
-  val of_ : Trm.trm -> t
+  val of_ : Trm.t -> t
 end = struct
   module T = struct
-    type t = Trm.trm [@@deriving compare, equal, sexp]
+    type t = Trm.t [@@deriving compare, equal, sexp]
 
     let invariant x =
       let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
@@ -39,20 +39,23 @@ end = struct
 end
 
 and Arith0 :
-  (Arithmetic.REPRESENTATION
-    with type var := Var.t
-    with type trm := Trm.trm) =
-  Arithmetic.Representation (Trm)
+  (Arithmetic.REPRESENTATION with type var := Var.t with type trm := Trm.t) =
+Arithmetic.Representation (struct
+  type trm = Trm.t [@@deriving compare, equal, sexp]
+  type var = Var.t
+
+  let ppx = Trm.ppx
+end)
 
 and Arith :
   (Arithmetic.S
     with type var := Var.t
-    with type trm := Trm.trm
+    with type trm := Trm.t
     with type t = Arith0.t) = struct
   include Arith0
 
   include Make (struct
-    let get_arith (e : Trm.trm) =
+    let get_arith (e : Trm.t) =
       match e with
       | Z z -> Some (Arith.const (Q.of_z z))
       | Q q -> Some (Arith.const q)
@@ -64,9 +67,7 @@ end
 (** Terms, built from variables and applications of function symbols from
     various theories. Denote functions from structures to values. *)
 and Trm : sig
-  type var = Var.t
-
-  type trm = private
+  type t = private
     (* variables *)
     | Var of {id: int; name: string}
     (* arithmetic *)
@@ -74,71 +75,69 @@ and Trm : sig
     | Q of Q.t
     | Arith of Arith.t
     (* sequences (of flexible size) *)
-    | Splat of trm
-    | Sized of {seq: trm; siz: trm}
-    | Extract of {seq: trm; off: trm; len: trm}
-    | Concat of trm array
+    | Splat of t
+    | Sized of {seq: t; siz: t}
+    | Extract of {seq: t; off: t; len: t}
+    | Concat of t array
     (* records (with fixed indices) *)
-    | Select of {idx: int; rcd: trm}
-    | Update of {idx: int; rcd: trm; elt: trm}
-    | Record of trm array
+    | Select of {idx: int; rcd: t}
+    | Update of {idx: int; rcd: t; elt: t}
+    | Record of t array
     | Ancestor of int
     (* uninterpreted *)
-    | Apply of Funsym.t * trm array
+    | Apply of Funsym.t * t array
   [@@deriving compare, equal, sexp]
 
-  val ppx : Var.t Var.strength -> trm pp
-  val _Var : int -> string -> trm
-  val _Z : Z.t -> trm
-  val _Q : Q.t -> trm
-  val _Arith : Arith.t -> trm
-  val _Splat : trm -> trm
-  val _Sized : trm -> trm -> trm
-  val _Extract : trm -> trm -> trm -> trm
-  val _Concat : trm array -> trm
-  val _Select : int -> trm -> trm
-  val _Update : int -> trm -> trm -> trm
-  val _Record : trm array -> trm
-  val _Ancestor : int -> trm
-  val _Apply : Funsym.t -> trm array -> trm
-  val add : trm -> trm -> trm
-  val sub : trm -> trm -> trm
-  val seq_size_exn : trm -> trm
-  val seq_size : trm -> trm option
+  val ppx : Var.t Var.strength -> t pp
+  val _Var : int -> string -> t
+  val _Z : Z.t -> t
+  val _Q : Q.t -> t
+  val _Arith : Arith.t -> t
+  val _Splat : t -> t
+  val _Sized : t -> t -> t
+  val _Extract : t -> t -> t -> t
+  val _Concat : t array -> t
+  val _Select : int -> t -> t
+  val _Update : int -> t -> t -> t
+  val _Record : t array -> t
+  val _Ancestor : int -> t
+  val _Apply : Funsym.t -> t array -> t
+  val add : t -> t -> t
+  val sub : t -> t -> t
+  val seq_size_exn : t -> t
+  val seq_size : t -> t option
 end = struct
-  type var = Var.t
-
-  type trm =
+  type t =
     | Var of {id: int; name: string}
     | Z of Z.t
     | Q of Q.t
     | Arith of Arith.t
-    | Splat of trm
-    | Sized of {seq: trm; siz: trm}
-    | Extract of {seq: trm; off: trm; len: trm}
-    | Concat of trm array
-    | Select of {idx: int; rcd: trm}
-    | Update of {idx: int; rcd: trm; elt: trm}
-    | Record of trm array
+    | Splat of t
+    | Sized of {seq: t; siz: t}
+    | Extract of {seq: t; off: t; len: t}
+    | Concat of t array
+    | Select of {idx: int; rcd: t}
+    | Update of {idx: int; rcd: t; elt: t}
+    | Record of t array
     | Ancestor of int
-    | Apply of Funsym.t * trm array
+    | Apply of Funsym.t * t array
   [@@deriving compare, equal, sexp]
 
-  let compare_trm x y =
+  let compare x y =
     if x == y then 0
     else
       match (x, y) with
       | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
           Int.compare i j
-      | _ -> compare_trm x y
+      | _ -> compare x y
 
-  let equal_trm x y =
+  let equal x y =
     x == y
     ||
     match (x, y) with
     | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
         Int.equal i j
-    | _ -> equal_trm x y
+    | _ -> equal x y
 
   let rec ppx strength fs trm =
     let rec pp fs trm =
@@ -190,7 +189,7 @@ end = struct
   let pp = ppx (fun _ -> None)
 
   let invariant e =
-    let@ () = Invariant.invariant [%here] e [%sexp_of: trm] in
+    let@ () = Invariant.invariant [%here] e [%sexp_of: t] in
     match e with
     | Q q -> assert (not (Z.equal Z.one (Q.den q)))
     | Arith a -> (
@@ -247,7 +246,7 @@ end = struct
   let _Sized seq siz =
     ( match seq_size seq with
     (* ⟨n,α⟩ ==> α when n ≡ |α| *)
-    | Some n when equal_trm siz n -> seq
+    | Some n when equal siz n -> seq
     | _ -> Sized {seq; siz} )
     |> check invariant
 
@@ -268,7 +267,7 @@ end = struct
       ~retn:(fun {pf} -> pf "%a" pp)
     @@ fun () ->
     (* _[_,0) ==> ⟨⟩ *)
-    ( if equal_trm len zero then empty_seq
+    ( if equal len zero then empty_seq
     else
       let o_l = add off len in
       match seq with
@@ -279,7 +278,7 @@ end = struct
       | Sized {siz= n; seq= Splat _ as e} when partial_ge n o_l ->
           _Sized e len
       (* ⟨n,a⟩[0,n) ==> ⟨n,a⟩ *)
-      | Sized {siz= n} when equal_trm off zero && equal_trm n len -> seq
+      | Sized {siz= n} when equal off zero && equal n len -> seq
       (* For (α₀^α₁)[o,l) there are 3 cases:
        *
        * ⟨...⟩^⟨...⟩
@@ -339,13 +338,12 @@ end = struct
       (* ⟨n,a⟩[o,k)^⟨n,a⟩[o+k,l) ==> ⟨n,a⟩[o,k+l) when n ≥ o+k+l *)
       | ( Extract {seq= Sized {siz= n} as na; off= o; len= k}
         , Extract {seq= na'; off= o_k; len= l} )
-        when equal_trm na na'
-             && equal_trm o_k (add o k)
-             && partial_ge n (add o_k l) ->
+        when equal na na' && equal o_k (add o k) && partial_ge n (add o_k l)
+        ->
           Some (_Extract na o (add k l))
       (* ⟨m,E^⟩^⟨n,E^⟩ ==> ⟨m+n,E^⟩ *)
       | Sized {siz= m; seq= Splat _ as a}, Sized {siz= n; seq= a'}
-        when equal_trm a a' ->
+        when equal a a' ->
           Some (_Sized a (add m n))
       | _ -> None
     in
@@ -359,9 +357,7 @@ end = struct
   let _Ancestor i = Ancestor i |> check invariant
 
   let _Apply f es =
-    ( match
-        Funsym.eval ~equal:equal_trm ~get_z ~ret_z:_Z ~get_q ~ret_q:_Q f es
-      with
+    ( match Funsym.eval ~equal ~get_z ~ret_z:_Z ~get_q ~ret_q:_Q f es with
     | Some c -> c
     | None -> Apply (f, es) )
     |> check invariant

sledge/src/trm.mli

@@ -9,7 +9,7 @@
 
 type arith
 
-type trm = private
+type t = private
   (* variables *)
   | Var of {id: int; name: string}
   (* arithmetic *)
@@ -17,49 +17,48 @@ type trm = private
   | Q of Q.t
   | Arith of arith
   (* sequences (of flexible size) *)
-  | Splat of trm
-  | Sized of {seq: trm; siz: trm}
-  | Extract of {seq: trm; off: trm; len: trm}
-  | Concat of trm array
+  | Splat of t
+  | Sized of {seq: t; siz: t}
+  | Extract of {seq: t; off: t; len: t}
+  | Concat of t array
   (* records (with fixed indices) *)
-  | Select of {idx: int; rcd: trm}
-  | Update of {idx: int; rcd: trm; elt: trm}
-  | Record of trm array
+  | Select of {idx: int; rcd: t}
+  | Update of {idx: int; rcd: t; elt: t}
+  | Record of t array
   | Ancestor of int
   (* uninterpreted *)
-  | Apply of Ses.Funsym.t * trm array
+  | Apply of Ses.Funsym.t * t array
 [@@deriving compare, equal, sexp]
 
 module Var : sig
+  type trm := t
+
   include Ses.Var_intf.VAR with type t = private trm
 
   val of_ : trm -> t
 end
 
 module Arith :
-  Arithmetic.S
-    with type var := Var.t
-    with type trm := trm
-    with type t = arith
+  Arithmetic.S with type var := Var.t with type trm := t with type t = arith
 
-val ppx : Var.t Var.strength -> trm pp
-val _Var : int -> string -> trm
-val _Z : Z.t -> trm
-val _Q : Q.t -> trm
-val _Arith : Arith.t -> trm
-val _Splat : trm -> trm
-val _Sized : trm -> trm -> trm
-val _Extract : trm -> trm -> trm -> trm
-val _Concat : trm array -> trm
-val _Select : int -> trm -> trm
-val _Update : int -> trm -> trm -> trm
-val _Record : trm array -> trm
-val _Ancestor : int -> trm
-val _Apply : Ses.Funsym.t -> trm array -> trm
-val add : trm -> trm -> trm
-val sub : trm -> trm -> trm
-val seq_size_exn : trm -> trm
-val seq_size : trm -> trm option
-val vars : trm -> Var.t iter
-val zero : trm
-val one : trm
+val ppx : Var.t Var.strength -> t pp
+val _Var : int -> string -> t
+val _Z : Z.t -> t
+val _Q : Q.t -> t
+val _Arith : Arith.t -> t
+val _Splat : t -> t
+val _Sized : t -> t -> t
+val _Extract : t -> t -> t -> t
+val _Concat : t array -> t
+val _Select : int -> t -> t
+val _Update : int -> t -> t -> t
+val _Record : t array -> t
+val _Ancestor : int -> t
+val _Apply : Ses.Funsym.t -> t array -> t
+val add : t -> t -> t
+val sub : t -> t -> t
+val seq_size_exn : t -> t
+val seq_size : t -> t option
+val vars : t -> Var.t iter
+val zero : t
+val one : t