From 5f6ded85665e7f9b548d49706a86c6a9ca4457f0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 1 Jun 2019 16:55:12 -0500 Subject: [PATCH] rename prop to bool --- src/base-term/Base_types.ml | 4 ++-- src/base-term/Model.ml | 2 +- src/base-term/Term.ml | 2 +- src/base-term/Term_cell.ml | 2 +- src/base-term/Ty.ml | 14 +++++++------- src/base-term/Ty.mli | 4 ++-- 6 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index 4b8a306b..09f584f8 100644 --- a/src/base-term/Base_types.ml +++ b/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 diff --git a/src/base-term/Model.ml b/src/base-term/Model.ml index 5e822c5a..7b894501 100644 --- a/src/base-term/Model.ml +++ b/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 diff --git a/src/base-term/Term.ml b/src/base-term/Term.ml index a3c9ca63..cf66f655 100644 --- a/src/base-term/Term.ml +++ b/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; diff --git a/src/base-term/Term_cell.ml b/src/base-term/Term_cell.ml index 02903cbf..13094c19 100644 --- a/src/base-term/Term_cell.ml +++ b/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 -> diff --git a/src/base-term/Ty.ml b/src/base-term/Ty.ml index d6e7fd40..8002fc85 100644 --- a/src/base-term/Ty.ml +++ b/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 diff --git a/src/base-term/Ty.mli b/src/base-term/Ty.mli index bdebcfd7..dcd03b94 100644 --- a/src/base-term/Ty.mli +++ b/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