Skip to content

Commit

Permalink
Store the enum flag in the type_body
Browse files Browse the repository at this point in the history
  • Loading branch information
@Halbaroth
Halbaroth committed Jun 12, 2024
1 parent 36d143d commit 73739aa
Show file tree
Hide file tree
Showing 8 changed files with 124 additions and 115 deletions.
29 changes: 10 additions & 19 deletions src/lib/frontend/d_cnf.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -546,8 +546,8 @@ and handle_ty_app ?(update = false) ty_c l =
apply_ty_substs tysubsts tv
)

| Tadt (hs, tyl, enum) ->
Tadt (hs, List.map (apply_ty_substs tysubsts) tyl, enum)
| Tadt (hs, tyl) ->
Tadt (hs, List.map (apply_ty_substs tysubsts) tyl)

| Trecord ({ args; lbs; _ } as rcrd) ->
Trecord {
Expand All @@ -565,7 +565,7 @@ and handle_ty_app ?(update = false) ty_c l =
(* Recover the initial versions of the types and apply them on the provided
type arguments stored in [tyl]. *)
match Cache.find_ty ty_c with
| Tadt (hs, _, enum) -> Tadt (hs, tyl, enum)
| Tadt (hs, _) -> Tadt (hs, tyl)

| Trecord { args; _ } as ty ->
let tysubsts =
Expand Down Expand Up @@ -615,10 +615,9 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
let uid = Uid.of_dolmen ty_c in
let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
Cache.store_ty ty_c (Ty.t_adt uid tyvl);
let rev_cs, is_enum =
let rev_cs =
Array.fold_left (
fun (accl, is_enum) DE.{ cstr; dstrs; _ } ->
let is_enum = is_enum && Array.length dstrs = 0 in
fun accl DE.{ cstr; dstrs; _ } ->
let rev_fields =
Array.fold_left (
fun acc tc_o ->
Expand All @@ -628,12 +627,11 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
| None -> assert false
) [] dstrs
in
(Uid.of_dolmen cstr, List.rev rev_fields) :: accl, is_enum
) ([], true) cases
(Uid.of_dolmen cstr, List.rev rev_fields) :: accl
) [] cases
in
let body = Some (List.rev rev_cs) in
let kind = if is_enum then `Enum else `Adt in
let ty = Ty.t_adt ~kind ~body uid tyvl in
let ty = Ty.t_adt ~body uid tyvl in
Cache.store_ty ty_c ty

| None | Some Abstract ->
Expand Down Expand Up @@ -693,7 +691,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
in
Cache.store_ty ty_c ty

| Tadt (hs, tyl, _), Some (Adt { cases; ty = ty_c; _ }) ->
| Tadt (hs, tyl), Some (Adt { cases; ty = ty_c; _ }) ->
let rev_cs =
Array.fold_left (
fun accl DE.{ cstr; dstrs; _ } ->
Expand Down Expand Up @@ -737,21 +735,14 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
fun acc tdef ->
match tdef with
| DE.Adt { cases; record; ty = ty_c; } as adt ->
let is_enum =
Array.fold_left (
fun is_enum DE.{ dstrs; _ } ->
is_enum && Array.length dstrs = 0
) true cases
in
let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
let uid = Uid.of_dolmen ty_c in
let ty =
if (record || Array.length cases = 1) && not contains_adts
then
Ty.trecord ~record_constr:uid tyvl uid []
else
let kind = if is_enum then `Enum else `Adt in
Ty.t_adt ~kind uid tyvl
Ty.t_adt uid tyvl
in
Cache.store_ty ty_c ty;
(ty, Some adt) :: acc
Expand Down
26 changes: 12 additions & 14 deletions src/lib/frontend/typechecker.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,14 +69,10 @@ module Types = struct
match ty with
| Ty.Text (lty', s)
| Ty.Trecord { Ty.args = lty'; name = s; _ }
| Ty.Tadt (s,lty',`Adt) ->
| Ty.Tadt (s,lty') ->
if List.length lty <> List.length lty' then
Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
lty'
| Ty.Tadt (s,lty',`Enum) ->
if List.length lty <> 0 || List.length lty' <> 0 then
Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
[]
| _ -> assert false

let equal_pp_vars lpp lvars =
Expand Down Expand Up @@ -149,7 +145,7 @@ module Types = struct
if not (Lists.is_empty ty_vars) then
Errors.typing_error (PolymorphicEnum id) loc;
let body = List.map (fun constr -> Uid.of_string constr, []) l in
let ty = Ty.t_adt ~kind:`Enum ~body:(Some body) (Uid.of_string id) [] in
let ty = Ty.t_adt ~body:(Some body) (Uid.of_string id) [] in
ty, { env with to_ty = MString.add id ty env.to_ty }
| Record (record_constr, lbs) ->
let lbs =
Expand Down Expand Up @@ -275,8 +271,9 @@ module Env = struct
let add_fpa_enum map =
let ty = Fpa_rounding.fpa_rounding_mode in
match ty with
| Ty.Tadt (name, [], `Enum) ->
let Adt cases = Ty.type_body name [] in
| Ty.Tadt (name, []) ->
let Ty.{ cases; kind } = Ty.type_body name [] in
assert (Stdlib.(kind = Ty.Enum));
let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
List.fold_left
(fun m c ->
Expand All @@ -301,8 +298,9 @@ module Env = struct

let find_builtin_cstr ty n =
match ty with
| Ty.Tadt (name, [], `Enum) ->
let Adt cases = Ty.type_body name [] in
| Ty.Tadt (name, []) ->
let Ty.{ cases; kind } = Ty.type_body name [] in
assert (Stdlib.(kind = Ty.Enum));
let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
List.find (Uid.equal n) cstrs
| _ ->
Expand Down Expand Up @@ -1005,8 +1003,8 @@ let rec type_term ?(call_from_type_form=false) env f =
let e = type_term env e in
let ty = Ty.shorten e.c.tt_ty in
let ty_body = match ty with
| Ty.Tadt (name, params, _) ->
let Ty.Adt cases = Ty.type_body name params in
| Ty.Tadt (name, params) ->
let Ty.{ cases; _ } = Ty.type_body name params in
cases
| Ty.Trecord { Ty.record_constr; lbs; _ } ->
[{Ty.constr = record_constr; destrs = lbs}]
Expand Down Expand Up @@ -1413,8 +1411,8 @@ and type_form ?(in_theory=false) env f =
let e = type_term env e in
let ty = e.c.tt_ty in
let ty_body = match ty with
| Ty.Tadt (name, params, _) ->
let Ty.Adt cases = Ty.type_body name params in
| Ty.Tadt (name, params) ->
let Ty.{ cases; _ } = Ty.type_body name params in
cases
| Ty.Trecord { Ty.record_constr; lbs; _ } ->
[{Ty.constr = record_constr ; destrs = lbs}]
Expand Down
8 changes: 4 additions & 4 deletions src/lib/reasoners/adt.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,9 +54,9 @@ let constr_of_destr ty dest =
~module_name:"Adt" ~function_name:"constr_of_destr"
"ty = %a" Ty.print ty;
match ty with
| Ty.Tadt (s, params, _) ->
| Ty.Tadt (s, params) ->
begin
let Ty.Adt cases = Ty.type_body s params in
let Ty.{ cases; _ } = Ty.type_body s params in
try
List.find
(fun { Ty.destrs; _ } ->
Expand Down Expand Up @@ -173,8 +173,8 @@ module Shostak (X : ALIEN) = struct
in
let xs = List.rev sx in
match f, xs, ty with
| Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params, _) ->
let Ty.Adt cases = Ty.type_body name params in
| Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) ->
let Ty.{ cases; _ } = Ty.type_body name params in
let case_hs =
try Ty.assoc_destrs hs cases with Not_found -> assert false
in
Expand Down
23 changes: 14 additions & 9 deletions src/lib/reasoners/adt_rel.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,14 +83,14 @@ module Domain = struct

let unknown ty =
match ty with
| Ty.Tadt (name, params, _) ->
| Ty.Tadt (name, params) ->
(* Return the list of all the constructors of the type of [r]. *)
let Adt body = Ty.type_body name params in
let Ty.{ cases; _ } = Ty.type_body name params in
let constrs =
List.fold_left
(fun acc Ty.{ constr; _ } ->
TSet.add constr acc
) TSet.empty body
) TSet.empty cases
in
assert (not @@ TSet.is_empty constrs);
{ constrs; ex = Ex.empty }
Expand Down Expand Up @@ -156,7 +156,12 @@ module Domains = struct

let is_enum r =
match X.type_info r with
| Ty.Tadt (_, [], `Enum) -> true
| Ty.Tadt (name, params) ->
let Ty.{ kind; _ } = Ty.type_body name params in
begin match kind with
| Enum -> true
| Adt -> false
end
| _ -> false

let internal_update r nd t =
Expand Down Expand Up @@ -477,10 +482,10 @@ let build_constr_eq r c =
match Th.embed r with
| Alien r ->
begin match X.type_info r with
| Ty.Tadt (name, params, _) as ty ->
let Ty.Adt body = Ty.type_body name params in
| Ty.Tadt (name, params) as ty ->
let Ty.{ cases; _ } = Ty.type_body name params in
let ds =
try Ty.assoc_destrs c body with Not_found -> assert false
try Ty.assoc_destrs c cases with Not_found -> assert false
in
let xs = List.map (fun (_, ty) -> E.fresh_name ty) ds in
let cons = E.mk_constr c xs ty in
Expand Down Expand Up @@ -578,9 +583,9 @@ let two = Numbers.Q.from_int 2
(* TODO: we should compute this reverse map in `Ty` and store it there. *)
let constr_of_destr ty d =
match ty with
| Ty.Tadt (name, params, _) ->
| Ty.Tadt (name, params) ->
begin
let Ty.Adt cases = Ty.type_body name params in
let Ty.{ cases; _ } = Ty.type_body name params in
try
let r =
List.find
Expand Down
2 changes: 1 addition & 1 deletion src/lib/reasoners/theory.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ module Main_Default : S = struct
(* cannot do better for records ? *)
Uid.Map.add name ty mp

| Tadt (hs, _, _) ->
| Tadt (hs, _) ->
(* cannot do better for ADT ? *)
Uid.Map.add hs ty mp
)sty Uid.Map.empty
Expand Down
2 changes: 1 addition & 1 deletion src/lib/structures/fpa_rounding.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode =
let body =
List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs
in
let ty = Ty.t_adt ~kind:`Enum ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
let ty = Ty.t_adt ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
DE.Ty.apply ty_cst [], d_cstrs, ty

let rounding_mode_of_smt_hs =
Expand Down
Loading

0 comments on commit 73739aa

Please sign in to comment.