rename prop to bool

src/base-term/Base_types.ml

@@ -61,7 +61,7 @@ and ty = {
 }
 
 and ty_view =
-  | Ty_prop
+  | Ty_bool
   | Ty_atomic of {
       def: ty_def;
       args: ty list;
@@ -139,7 +139,7 @@ let pp_value out = function
 let pp_db out (i,_) = Format.fprintf out "%%%d" i
 
 let rec pp_ty out t = match t.ty_view with
-  | Ty_prop -> Fmt.string out "prop"
+  | Ty_bool -> Fmt.string out "prop"
   | Ty_atomic {def=Ty_uninterpreted id; args=[]; _} -> ID.pp out id
   | Ty_atomic {def=Ty_uninterpreted id; args; _} ->
     Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp_ty) args

src/base-term/Model.ml

@@ -62,7 +62,7 @@ let empty : t = {
     (* get or make a default value for this type *)
     let rec get_ty_default (ty:Ty.t) : Value.t =
       match Ty.view ty with
-      | Ty_prop -> Value.true_
+      | Ty_bool -> Value.true_
       | Ty_atomic { def = Ty_uninterpreted _;_} ->
         (* domain element *)
         Ty_tbl.get_or_add ty_tbl ~k:ty

src/base-term/Term.ml

@@ -39,7 +39,7 @@ type state = {
 }
 
 let[@inline] make st (c:t term_view) : t =
-  let t = {term_id= -1; term_ty=Ty.prop; term_view=c} in
+  let t = {term_id= -1; term_ty=Ty.bool; term_view=c} in
   let t' = H.hashcons st.tbl t in
   if t == t' then (
     t'.term_ty <- Term_cell.ty c;

src/base-term/Term_cell.ml

@@ -78,7 +78,7 @@ let if_ a b c =
   If (a,b,c)
 
 let ty (t:t): Ty.t = match t with
-  | Bool _ | Eq _ | Not _ -> Ty.prop
+  | Bool _ | Eq _ | Not _ -> Ty.bool
   | App_cst (f, args) ->
     begin match Cst.view f with
       | Cst_undef fty -> 

src/base-term/Ty.ml

@@ -21,14 +21,14 @@ let equal_def d1 d2 = match d1, d2 with
 module H = Hashcons.Make(struct
     type t = ty
     let equal a b = match a.ty_view, b.ty_view with
-      | Ty_prop, Ty_prop -> true
+      | Ty_bool, Ty_bool -> true
       | Ty_atomic a1, Ty_atomic a2 ->
         equal_def a1.def a2.def && CCList.equal equal a1.args a2.args
-      | Ty_prop, _ | Ty_atomic _, _
+      | Ty_bool, _ | Ty_atomic _, _
        -> false
 
     let hash t = match t.ty_view with
-      | Ty_prop -> 1
+      | Ty_bool -> 1
       | Ty_atomic {def=Ty_uninterpreted id; args; _} ->
         Hash.combine3 10 (ID.hash id) (Hash.list hash args)
       | Ty_atomic {def=Ty_def d; args; _} ->
@@ -47,10 +47,10 @@ let make_ : ty_view -> t =
     H.hashcons tbl ty
 
 let card t = match view t with
-  | Ty_prop -> Finite
+  | Ty_bool -> Finite
   | Ty_atomic {card=lazy c; _} -> c
 
-let prop = make_ Ty_prop
+let bool = make_ Ty_bool
 
 let atomic def args : t =
   let card = lazy (
@@ -63,8 +63,8 @@ let atomic def args : t =
 
 let atomic_uninterpreted id = atomic (Ty_uninterpreted id) []
 
-let is_prop t =
-  match t.ty_view with | Ty_prop -> true | _ -> false
+let is_bool t =
+  match t.ty_view with | Ty_bool -> true | _ -> false
 
 let is_uninterpreted t =
   match t.ty_view with | Ty_atomic {def=Ty_uninterpreted _; _} -> true | _ -> false

src/base-term/Ty.mli

@@ -10,14 +10,14 @@ type def = Base_types.ty_def
 val id : t -> int
 val view : t -> view
 
-val prop : t
+val bool : t
 val atomic : def -> t list -> t
 
 val atomic_uninterpreted : ID.t -> t
 
 val card : t -> ty_card
 
-val is_prop : t -> bool
+val is_bool : t -> bool
 val is_uninterpreted : t -> bool
 
 include Intf.EQ with type t := t