Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove uid module #1253

Merged
merged 9 commits into from
Oct 9, 2024
Merged

Remove uid module #1253

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
54d4975
Do not use Uid.of_hstring for Fpa constructors
Halbaroth Oct 8, 2024
58830b0
Remove unification in Ty
Halbaroth Oct 8, 2024
5d8cba8
Remove Hstring constructor in Uid
Halbaroth Oct 8, 2024
c6f00a6
Remove Uid module
Halbaroth Oct 8, 2024
da5d51c
Too long lines
Halbaroth Oct 8, 2024
e3a6539
Use Compat.List.find_map
Halbaroth Oct 9, 2024
12175c7
More defensive programming!
Halbaroth Oct 9, 2024
a84dc94
clean up
Halbaroth Oct 9, 2024
8224c9d
Review changes
Halbaroth Oct 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/lib/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@
; structures
Commands Errors Explanation Fpa_rounding
Parsed Profiling Satml_types Symbols
Expr Var Ty Typed Xliteral ModelMap Id Uid Objective Literal
Expr Var Ty Typed Xliteral ModelMap Id Objective Literal
; util
Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
Options Timers Util Vec Version Steps Printer
Expand Down
19 changes: 10 additions & 9 deletions src/lib/frontend/models.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ module Sy = Symbols
module X = Shostak.Combine
module E = Expr
module MS = Map.Make(String)
module DE = Dolmen.Std.Expr

let constraints = ref MS.empty

Expand Down Expand Up @@ -110,15 +111,15 @@ module Pp_smtlib_term = struct

| Sy.L_built (Sy.IsConstr hs), [e] ->
if Options.get_output_smtlib () then
fprintf fmt "((_ is %a) %a)" Uid.pp hs print e
fprintf fmt "((_ is %a) %a)" DE.Term.Const.print hs print e
else
fprintf fmt "(%a ? %a)" print e Uid.pp hs
fprintf fmt "(%a ? %a)" print e DE.Term.Const.print hs

| Sy.L_neg_built (Sy.IsConstr hs), [e] ->
if Options.get_output_smtlib () then
fprintf fmt "(not ((_ is %a) %a))" Uid.pp hs print e
fprintf fmt "(not ((_ is %a) %a))" DE.Term.Const.print hs print e
else
fprintf fmt "not (%a ? %a)" print e Uid.pp hs
fprintf fmt "not (%a ? %a)" print e DE.Term.Const.print hs

| (Sy.L_built (Sy.LT | Sy.LE | Sy.BVULE)
| Sy.L_neg_built (Sy.LT | Sy.LE | Sy.BVULE)
Expand Down Expand Up @@ -152,9 +153,9 @@ module Pp_smtlib_term = struct

| Sy.Op (Sy.Access field), [e] ->
if Options.get_output_smtlib () then
fprintf fmt "(%a %a)" Uid.pp field print e
fprintf fmt "(%a %a)" DE.Term.Const.print field print e
else
fprintf fmt "%a.%a" print e Uid.pp field
fprintf fmt "%a.%a" print e DE.Term.Const.print field

| Sy.Op (Sy.Record), _ ->
begin match ty with
Expand All @@ -163,7 +164,7 @@ module Pp_smtlib_term = struct
fprintf fmt "{";
ignore (List.fold_left2 (fun first (field,_) e ->
fprintf fmt "%s%a = %a" (if first then "" else "; ")
Uid.pp field print e;
DE.Term.Const.print field print e;
false
) true lbs xs);
fprintf fmt "}";
Expand All @@ -178,7 +179,7 @@ module Pp_smtlib_term = struct

(* TODO: introduce PrefixOp in the future to simplify this ? *)
| Sy.Op (Sy.Constr hs), ((_::_) as l) ->
fprintf fmt "%a(%a)" Uid.pp hs print_list l
fprintf fmt "%a(%a)" DE.Term.Const.print hs print_list l

| Sy.Op _, [e1; e2] ->
if Options.get_output_smtlib () then
Expand All @@ -187,7 +188,7 @@ module Pp_smtlib_term = struct
fprintf fmt "(%a %a %a)" print e1 Sy.print f print e2

| Sy.Op Sy.Destruct hs, [e] ->
fprintf fmt "%a#%a" print e Uid.pp hs
fprintf fmt "%a#%a" print e DE.Term.Const.print hs


| Sy.In(lb, rb), [t] ->
Expand Down
64 changes: 29 additions & 35 deletions src/lib/frontend/translate.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ let fpa_rounding_mode, rounding_modes, add_rounding_modes =
| `App ((`Generic ty_cst), []) ->
let constrs = Fpa_rounding.d_constrs in
let add_constrs map =
List.fold_left (fun map ((c : DE.term_cst), _) ->
List.fold_left (fun map (c : DE.term_cst) ->
let name = get_basename c.path in
DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term }
(fun env _ ->
Expand Down Expand Up @@ -237,7 +237,7 @@ let inject_ae_to_smt2 id =
in
{id with name}
else
match Fpa_rounding.rounding_mode_of_ae_hs (Hstring.make n) with
match Fpa_rounding.rounding_mode_of_ae n with
| rm ->
let name =
Dolmen_std.Name.simple (Fpa_rounding.string_of_rounding_mode rm)
Expand Down Expand Up @@ -273,8 +273,8 @@ let ae_fpa_builtins =
DE.Term.apply_cst float_cst [] [prec; exp; mode; x]
in
let mode m =
let cst, _ =
List.find (fun (cst, _args) ->
let cst =
List.find (fun cst ->
match cst.DE.path with
| Absolute { name; _ } -> String.equal name m
| Local _ -> false)
Expand Down Expand Up @@ -580,31 +580,28 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
(* Records and adts that only have one case are treated in the same way,
and considered as records. *)
Nest.attach_orders [adt];
let uid = Uid.of_ty_cst ty_c in
let tyvl = Cache.store_ty_vars_ret id_ty in
let lbs =
Array.fold_right (
fun c acc ->
match c with
| Some (DE.{ id_ty; _ } as id) ->
let pty = dty_to_ty id_ty in
(Uid.of_term_cst id, pty) :: acc
(id, pty) :: acc
| _ ->
Fmt.failwith
"Unexpected null label for some field of the record type %a"
DE.Ty.Const.print ty_c

) dstrs []
in
let record_constr = Uid.of_term_cst cstr in
let ty = Ty.trecord ~record_constr tyvl uid lbs in
let ty = Ty.trecord ~record_constr:cstr tyvl ty_c lbs in
Cache.store_ty ty_c ty

| Some (Adt { cases; _ } as adt) ->
Nest.attach_orders [adt];
let uid = Uid.of_ty_cst 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);
Cache.store_ty ty_c (Ty.t_adt ty_c tyvl);
let cs =
Array.fold_right (
fun DE.{ cstr; dstrs; _ } accl ->
Expand All @@ -613,21 +610,21 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
fun tc_o acc ->
match tc_o with
| Some (DE.{ id_ty; _ } as field) ->
(Uid.of_term_cst field, dty_to_ty id_ty) :: acc
(field, dty_to_ty id_ty) :: acc
| None -> assert false
) dstrs []
in
(Uid.of_term_cst cstr, fields) :: accl
(cstr, fields) :: accl
) cases []
in
let ty = Ty.t_adt ~body:(Some cs) uid tyvl in
let ty = Ty.t_adt ~body:(Some cs) ty_c tyvl in
Cache.store_ty ty_c ty

| None | Some Abstract ->
let ty_params = []
(* List.init ty_c.id_ty.arity (fun _ -> Ty.fresh_tvar ()) *)
in
let ty = Ty.text ty_params (Uid.of_ty_cst ty_c) in
let ty = Ty.text ty_params ty_c in
Cache.store_ty ty_c ty

(** Handles term declaration by storing the eventual present type variables
Expand Down Expand Up @@ -667,7 +664,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
match c with
| Some (DE.{ id_ty; _ } as id) ->
let pty = dty_to_ty id_ty in
(Uid.of_term_cst id, pty) :: acc
(id, pty) :: acc
| _ ->
Fmt.failwith
"Unexpected null label for some field of the record type %a"
Expand All @@ -688,11 +685,11 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
fun tc_o acc ->
match tc_o with
| Some (DE.{ id_ty; _ } as id) ->
(Uid.of_term_cst id, dty_to_ty id_ty) :: acc
(id, dty_to_ty id_ty) :: acc
| None -> assert false
) dstrs []
in
(Uid.of_term_cst cstr, fields) :: accl
(cstr, fields) :: accl
) cases []
in
let ty = Ty.t_adt ~body:(Some cs) hs tyl in
Expand Down Expand Up @@ -723,14 +720,13 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
match tdef with
| DE.Adt { cases; record; ty = ty_c; } as adt ->
let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
let uid = Uid.of_ty_cst ty_c in
let record_constr = Uid.of_term_cst cases.(0).cstr in
let record_constr = cases.(0).cstr in
let ty =
if (record || Array.length cases = 1) && not contains_adts
then
Ty.trecord ~record_constr tyvl uid []
Ty.trecord ~record_constr tyvl ty_c []
else
Ty.t_adt uid tyvl
Ty.t_adt ty_c tyvl
in
Cache.store_ty ty_c ty;
(ty, Some adt) :: acc
Expand All @@ -748,14 +744,14 @@ let handle_patt_var id (DE.{ term_descr; _ } as term) =
match term_descr with
| Cst ({ builtin = B.Base; id_ty; _ } as ty_c) ->
let ty = dty_to_ty id_ty in
let v = Var.of_string @@ Uid.show id in
let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in
let sy = Sy.Var v in
Cache.store_sy ty_c sy;
v, id, ty

| Var ({ builtin = B.Base; id_ty; _ } as ty_v) ->
let ty = dty_to_ty id_ty in
let v = Var.of_string @@ Uid.show id in
let v = Var.of_string @@ Fmt.to_to_string DE.Term.Const.print id in
let sy = Sy.Var v in
Cache.store_sy ty_v sy;
v, id, ty
Expand All @@ -781,7 +777,7 @@ let mk_pattern DE.{ term_descr; _ } =
Array.fold_right (
fun v acc ->
match v with
| Some dstr -> Uid.of_term_cst dstr :: acc
| Some dstr -> dstr :: acc
| _ -> assert false
) dstrs []
| _ ->
Expand All @@ -799,10 +795,10 @@ let mk_pattern DE.{ term_descr; _ } =
) [] vnames pargs
in
let args = List.rev rev_args in
Typed.Constr {name = Uid.of_term_cst cst; args}
Typed.Constr {name = cst; args}

| Cst ({ builtin = B.Constructor _; _ } as cst) ->
Typed.Constr {name = Uid.of_term_cst cst; args = []}
Typed.Constr {name = cst; args = []}

| Var ({ builtin = B.Base; path; _ } as t_v) ->
(* Should the type be passed as an argument
Expand Down Expand Up @@ -924,10 +920,9 @@ let mk_add translate sy ty l =
E.mk_term sy args ty

let mk_rounding fpar =
let name = Hstring.make @@ Fpa_rounding.string_of_rounding_mode fpar in
let tcst = Fpa_rounding.term_cst_of_rounding_mode fpar in
let ty = Fpa_rounding.fpa_rounding_mode in
let sy = Sy.Op (Sy.Constr (Uid.of_hstring name)) in
E.mk_term sy [] ty
E.mk_constr tcst [] ty

(** [mk_expr ~loc ~name_base ~toplevel ~decl_kind term]
Expand Down Expand Up @@ -962,7 +957,7 @@ let rec mk_expr
| Trecord _ as ty ->
E.mk_record [] ty
| Tadt _ as ty ->
E.mk_constr (Uid.of_term_cst tcst) [] ty
E.mk_constr tcst [] ty
| ty ->
Fmt.failwith "unexpected type %a@." Ty.print ty
end
Expand Down Expand Up @@ -1007,9 +1002,9 @@ let rec mk_expr
let sy =
match Cache.find_ty adt with
| Trecord _ ->
Sy.Op (Sy.Access (Uid.of_term_cst destr))
Sy.Op (Sy.Access destr)
| Tadt _ ->
Sy.destruct (Uid.of_term_cst destr)
Sy.destruct destr
| _ -> assert false
in
E.mk_term sy [e] ty
Expand All @@ -1029,7 +1024,6 @@ let rec mk_expr
cstr = { builtin = B.Constructor { adt; _ }; _ } as cstr; _
}, [x] ->
begin
let builtin = Sy.IsConstr (Uid.of_term_cst cstr) in
let ty_c =
match DT.definition adt with
| Some (
Expand All @@ -1039,7 +1033,7 @@ let rec mk_expr
in
match Cache.find_ty ty_c with
| Ty.Tadt _ ->
E.mk_builtin ~is_pos:true builtin [aux_mk_expr x]
E.mk_tester cstr (aux_mk_expr x)

| Ty.Trecord _ ->
(* The typechecker allows only testers whose the
Expand Down Expand Up @@ -1315,7 +1309,7 @@ let rec mk_expr
begin match ty with
| Ty.Tadt _ ->
let l = List.map (fun t -> aux_mk_expr t) args in
E.mk_constr (Uid.of_term_cst tcst) l ty
E.mk_constr tcst l ty
| Ty.Trecord _ ->
let l = List.map (fun t -> aux_mk_expr t) args in
E.mk_record l ty
Expand Down
Loading
Loading