Skip to content

Commit

Permalink
Remove Uid module
Browse files Browse the repository at this point in the history 
This PR removes the interface Uid. We know use `term_cst` and `ty_cst`
of Dolmen directly!
  • Loading branch information
@Halbaroth
Halbaroth committed Oct 8, 2024
1 parent 071fa24 commit b6776de
Show file tree
Hide file tree
Showing 24 changed files with 234 additions and 389 deletions.
2 changes: 1 addition & 1 deletion src/lib/dune
View file
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
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
55 changes: 25 additions & 30 deletions src/lib/frontend/translate.ml
View file
Original file line number Diff line number Diff line change
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 @@ -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.str "%a" 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.str "%a" 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,7 +920,7 @@ let mk_add translate sy ty l =
E.mk_term sy args ty

let mk_rounding fpar =
let tcst = Uid.of_term_cst @@ Fpa_rounding.tcst_of_rounding_mode fpar in
let tcst = Fpa_rounding.tcst_of_rounding_mode fpar in
let ty = Fpa_rounding.fpa_rounding_mode in
E.mk_constr tcst [] ty

Expand Down Expand Up @@ -961,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 @@ -1006,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 @@ -1028,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 @@ -1038,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 @@ -1314,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

0 comments on commit b6776de

Please sign in to comment.