tweak to basetype definition

rems-project · Sep 6, 2023 · 22dd425 · 22dd425
1 parent 467aa77
commit 22dd425
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 25 deletions.
diff --git a/backend/cn/baseTypes.ml b/backend/cn/baseTypes.ml
@@ -10,17 +10,14 @@ type basetype =
  | CType
  | Struct of Sym.t
  | Datatype of Sym.t
- | Record of member_types
+ | Record of (Id.t * basetype) list
  | Map of basetype * basetype
  | List of basetype
  | Tuple of basetype list
  | Set of basetype
  (* | Option of basetype *)
 [@@deriving eq, ord]
 
-and member_types =
- (Id.t * basetype) list
-
 
 type t = basetype
 
@@ -31,10 +28,10 @@ let compare = compare_basetype
 
 type datatype_info = {
  dt_constrs: Sym.t list;
- dt_all_params: member_types;
+ dt_all_params: (Id.t * basetype) list;
 }
 type constr_info = {
- c_params: member_types;
+ c_params: (Id.t * basetype) list;
  c_datatype_tag: Sym.t
 }
 

diff --git a/backend/cn/solver.ml b/backend/cn/solver.ml
@@ -143,8 +143,8 @@ module Translate = struct
  | StructFunc of { tag : Sym.t }
  | CompFunc of { bts : BT.t list; i : int }
  | TupleFunc of { bts : BT.t list }
- | RecordFunc of { mbts : BT.member_types }
- | RecordMemberFunc of { mbts : BT.member_types; member : Id.t }
+ | RecordFunc of { mbts : (Id.t * basetype) list }
+ | RecordMemberFunc of { mbts : (Id.t * basetype) list; member : Id.t }
  | DefaultFunc of { bt : BT.t }
  | DatatypeConsFunc of { nm: Sym.t }
  | DatatypeConsRecogFunc of { nm: Sym.t }

diff --git a/backend/cn/surfaceBaseTypes.ml b/backend/cn/surfaceBaseTypes.ml
@@ -12,16 +12,14 @@ type basetype =
  | Loc of Sctypes.t option
  | Struct of Sym.t
  | Datatype of Sym.t
- | Record of member_types
+ | Record of (Id.t * basetype) list
  | Map of basetype * basetype
  | List of basetype
  | Tuple of basetype list
  | Set of basetype
  (* | Option of basetype *)
 [@@deriving eq, ord]
 
-and member_types =
- (Id.t * basetype) list
 
 
 type t = basetype
@@ -31,19 +29,6 @@ let equal = equal_basetype
 let compare = compare_basetype
 
 
-type datatype_info = {
- dt_constrs: Sym.t list;
- dt_all_params: member_types;
-}
-type constr_info = {
- c_params: member_types;
- c_datatype_tag: Sym.t
-}
-
-let cons_dom_rng info =
- (Record info.c_params, Datatype info.c_datatype_tag)
-
-
 let rec pp = function
  | Unit -> !^"void"
  | Bool -> !^"bool"

diff --git a/backend/cn/typing.mli b/backend/cn/typing.mli
@@ -100,7 +100,7 @@ val ensure_base_type: Locations.t -> expect:LogicalSorts.t -> LogicalSorts.t ->
 val make_return_record: 
  Locations.t ->
  string ->
- BaseTypes.member_types ->
+ (Id.t * BaseTypes.t) list ->
  (IndexTerms.t * IndexTerms.t list) m
 
 val bind_logical_return: