Revert "tweak to basetype definition"

This reverts commit 22dd425.
rems-project · Sep 6, 2023 · 907f909 · 907f909
1 parent 22dd425
commit 907f909
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 7 deletions.
diff --git a/backend/cn/baseTypes.ml b/backend/cn/baseTypes.ml
@@ -10,14 +10,17 @@ type basetype =
   | CType
   | Struct of Sym.t
   | Datatype of Sym.t
-  | Record of (Id.t * basetype) list
+  | Record of member_types
   | 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
 
@@ -28,10 +31,10 @@ let compare = compare_basetype
 
 type datatype_info = {
   dt_constrs: Sym.t list;
-  dt_all_params: (Id.t * basetype) list;
+  dt_all_params: member_types;
 }
 type constr_info = {
-  c_params: (Id.t * basetype) list;
+  c_params: member_types;
   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 : (Id.t * basetype) list }
-    | RecordMemberFunc of { mbts : (Id.t * basetype) list; member : Id.t }
+    | RecordFunc of { mbts : BT.member_types }
+    | RecordMemberFunc of { mbts : BT.member_types; 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,14 +12,16 @@ type basetype =
   | Loc of Sctypes.t option
   | Struct of Sym.t
   | Datatype of Sym.t
-  | Record of (Id.t * basetype) list
+  | Record of member_types
   | 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
@@ -29,6 +31,19 @@ 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 ->
-    (Id.t * BaseTypes.t) list ->
+    BaseTypes.member_types ->
     (IndexTerms.t * IndexTerms.t list) m
 
 val bind_logical_return: