diff --git a/backend/cn/baseTypes.ml b/backend/cn/baseTypes.ml index 8f0a1d321..9e4798bee 100644 --- a/backend/cn/baseTypes.ml +++ b/backend/cn/baseTypes.ml @@ -10,7 +10,7 @@ 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 @@ -18,9 +18,6 @@ type 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 index f294ca2ae..4aaee8ce1 100644 --- 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 index 271b6483d..c3afbd38e 100644 --- a/backend/cn/surfaceBaseTypes.ml +++ b/backend/cn/surfaceBaseTypes.ml @@ -12,7 +12,7 @@ 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 @@ -20,8 +20,6 @@ type 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 index 7c7ec1dbc..da3ec7826 100644 --- 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: