let type_of_string_sexpr = function | HStringSExpr.Atom s when s == s_int -> Type.t_int | HStringSExpr.Atom s when s == s_real -> Type.t_real | HStringSExpr.Atom s when s == s_bool -> Type.t_bool | HStringSExpr.List [HStringSExpr.Atom s; HStringSExpr.Atom i; HStringSExpr.Atom j] when s == s_subrange -> Type.mk_int_range (Numeral.of_string (HString.string_of_hstring i)) (Numeral.of_string (HString.string_of_hstring j)) | HStringSExpr.Atom _ | HStringSExpr.List _ as s -> raise (Invalid_argument (Format.asprintf "Sort %a not supported" HStringSExpr.pp_print_sexpr s))