From 4ac01defd8f0ae1c52c41c1b27f7e56f6f2b3855 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Sun, 14 Apr 2024 13:05:16 +0200 Subject: [PATCH] Merge `Records` into `ADT` --- src/lib/dune | 2 +- src/lib/frontend/models.ml | 22 +---- src/lib/frontend/translate.ml | 158 +++------------------------------ src/lib/reasoners/adt.ml | 7 +- src/lib/reasoners/adt_rel.ml | 6 +- src/lib/reasoners/matching.ml | 20 ++--- src/lib/reasoners/relation.ml | 49 ++++------ src/lib/reasoners/shostak.ml | 105 ++++++---------------- src/lib/reasoners/shostak.mli | 3 - src/lib/reasoners/theory.ml | 24 +---- src/lib/structures/expr.ml | 62 +------------ src/lib/structures/expr.mli | 1 - src/lib/structures/symbols.ml | 13 +-- src/lib/structures/symbols.mli | 3 +- src/lib/structures/ty.ml | 129 ++++----------------------- src/lib/structures/ty.mli | 31 +------ src/lib/structures/typed.ml | 7 +- src/lib/structures/typed.mli | 4 +- 18 files changed, 105 insertions(+), 541 deletions(-) diff --git a/src/lib/dune b/src/lib/dune index 30cc3b00b..85cde88d4 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -51,7 +51,7 @@ Ac Arith Arrays_rel Bitv Ccx Shostak Relation Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel Instances IntervalCalculus Intervals_intf Intervals_core Intervals - Ite_rel Matching Matching_types Polynome Records Records_rel + Ite_rel Matching Matching_types Polynome Satml_frontend_hybrid Satml_frontend Satml Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Domains Domains_intf Rel_utils Bitlist ; structures diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index afa71e83d..25972083b 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -42,7 +42,7 @@ module Pp_smtlib_term = struct asprintf "%a" Ty.pp_smtlib t let rec print fmt t = - let {Expr.f;xs;ty; _} = Expr.term_view t in + let {Expr.f;xs; _} = Expr.term_view t in match f, xs with | Sy.Lit lit, xs -> @@ -151,26 +151,6 @@ module Pp_smtlib_term = struct | Sy.Op Sy.Extract (i, j), [e] -> fprintf fmt "%a^{%d,%d}" print e i j - | Sy.Op (Sy.Access field), [e] -> - if Options.get_output_smtlib () then - fprintf fmt "(%a %a)" DE.Term.Const.print field print e - else - fprintf fmt "%a.%a" print e DE.Term.Const.print field - - | Sy.Op (Sy.Record), _ -> - begin match ty with - | Ty.Trecord { Ty.lbs = lbs; _ } -> - assert (List.length xs = List.length lbs); - fprintf fmt "{"; - ignore (List.fold_left2 (fun first (field,_) e -> - fprintf fmt "%s%a = %a" (if first then "" else "; ") - DE.Term.Const.print field print e; - false - ) true lbs xs); - fprintf fmt "}"; - | _ -> assert false - end - (* TODO: introduce PrefixOp in the future to simplify this ? *) | Sy.Op op, [e1; e2] when op == Sy.Pow || op == Sy.Integer_round || op == Sy.Max_real || op == Sy.Max_int || diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 262eff96d..d3a417927 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -519,85 +519,17 @@ let rec dty_to_ty ?(update = false) ?(is_var = false) dty = | _ -> unsupported "Type %a" DE.Ty.print dty and handle_ty_app ?(update = false) ty_c l = - (* Applies the substitutions in [tysubsts] to each encountered type - variable. *) - let rec apply_ty_substs tysubsts ty = - match ty with - | Ty.Tvar { v; _ } -> - Ty.M.find v tysubsts - - | Text (tyl, hs) -> - Ty.Text (List.map (apply_ty_substs tysubsts) tyl, hs) - - | Tfarray (ti, tv) -> - Tfarray ( - apply_ty_substs tysubsts ti, - apply_ty_substs tysubsts tv - ) - - | Tadt (hs, tyl) -> - Tadt (hs, List.map (apply_ty_substs tysubsts) tyl) - - | Trecord ({ args; lbs; _ } as rcrd) -> - Trecord { - rcrd with - args = List.map (apply_ty_substs tysubsts) args; - lbs = List.map ( - fun (hs, t) -> - hs, apply_ty_substs tysubsts t - ) lbs; - } - - | _ -> ty - in let tyl = List.map (dty_to_ty ~update) l in (* 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, _) -> Tadt (hs, tyl) - - | Trecord { args; _ } as ty -> - let tysubsts = - List.fold_left2 ( - fun acc tv ty -> - match tv with - | Ty.Tvar { v; _ } -> Ty.M.add v ty acc - | _ -> assert false - ) Ty.M.empty args tyl - in - apply_ty_substs tysubsts ty - + | Tadt (hs, _, record) -> Tadt (hs, tyl, record) | Text (_, s) -> Text (tyl, s) | _ -> assert false (** Handles a simple type declaration. *) let mk_ty_decl (ty_c: DE.ty_cst) = match DT.definition ty_c with - | Some ( - (Adt - { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } as adt) - ) -> - (* Records and adts that only have one case are treated in the same way, - and considered as records. *) - Nest.attach_orders [adt]; - 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 - (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 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 tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in @@ -654,29 +586,7 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = let mk_mr_ty_decls (tdl: DE.ty_cst list) = let handle_ty_decl (ty: Ty.t) (tdef: DE.Ty.def option) = match ty, tdef with - | Trecord { args; name; record_constr; _ }, - Some ( - Adt { cases = [| { dstrs; _ } |]; ty = ty_c; _ } - ) -> - 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 - (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 ty = - Ty.trecord ~record_constr args name lbs - 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 cs = Array.fold_right ( fun DE.{ cstr; dstrs; _ } accl -> @@ -697,37 +607,15 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = | _ -> assert false in - (* If there are adts in the list of type declarations then records are - converted to adts, because that's how it's done in the legacy typechecker. - But it might be more efficient not to do that. *) - let rev_tdefs, contains_adts = - List.fold_left ( - fun (acc, ca) ty_c -> - match DT.definition ty_c with - | Some (Adt { record; cases; _ } as df) - when not record && Array.length cases > 1 -> - df :: acc, true - | Some (Adt _ as df) -> - df :: acc, ca - | Some Abstract | None -> - assert false - ) ([], false) tdl - in + let rev_tdefs = List.rev_map (fun td -> Option.get @@ DT.definition td) tdl in Nest.attach_orders rev_tdefs; let rev_l = List.fold_left ( fun acc tdef -> match tdef with - | DE.Adt { cases; record; ty = ty_c; } as adt -> + | DE.Adt { cases; ty = ty_c; _ } as adt -> let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty 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 ty_c [] - else - Ty.t_adt ty_c tyvl - in + let ty = Ty.t_adt ty_c tyvl in Cache.store_ty ty_c ty; (ty, Some adt) :: acc @@ -953,14 +841,8 @@ let rec mk_expr E.mk_term sy [] ty | B.Constructor _ -> - begin match dty_to_ty term_ty with - | Trecord _ as ty -> - E.mk_record [] ty - | Tadt _ as ty -> - E.mk_constr tcst [] ty - | ty -> - Fmt.failwith "unexpected type %a@." Ty.print ty - end + let ty = dty_to_ty term_ty in + E.mk_constr tcst [] ty | _ -> unsupported "Constant term %a" DE.Term.print term end @@ -1001,10 +883,7 @@ let rec mk_expr let e = aux_mk_expr x in let sy = match Cache.find_ty adt with - | Trecord _ -> - Sy.Op (Sy.Access destr) - | Tadt _ -> - Sy.destruct destr + | Tadt _ -> Sy.destruct destr | _ -> assert false in E.mk_term sy [e] ty @@ -1035,11 +914,6 @@ let rec mk_expr | Ty.Tadt _ -> E.mk_tester cstr (aux_mk_expr x) - | Ty.Trecord _ -> - (* The typechecker allows only testers whose the - two arguments have the same type. Thus, we can always - replace the tester of a record by the true literal. *) - E.vrai | _ -> assert false end @@ -1306,19 +1180,9 @@ let rec mk_expr | B.Constructor _, _ -> let ty = dty_to_ty term_ty in - begin match ty with - | Ty.Tadt _ -> - let l = List.map (fun t -> aux_mk_expr t) args in - 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 - | _ -> - Fmt.failwith - "Constructor error: %a does not belong to a record nor an\ - algebraic data type" - DE.Term.print app_term - end + let sy = Sy.constr tcst in + let l = List.map (fun t -> aux_mk_expr t) args in + E.mk_term sy l ty | B.Coercion, [ x ] -> begin match DT.view (DE.Term.ty x), DT.view term_ty with diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index fca71829f..92ebde84b 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -62,7 +62,7 @@ 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 cases = Ty.type_body s params in try @@ -182,7 +182,7 @@ 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) -> + | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params, _) -> let cases = Ty.type_body name params in let case_hs = try Ty.assoc_destrs hs cases with Not_found -> assert false @@ -203,9 +203,6 @@ module Shostak (X : ALIEN) = struct else sel_x, ctx (* canonization OK *) *) - | Sy.Op Sy.Constr _, _, Ty.Trecord _ -> - Fmt.failwith "unexpected record constructor %a@." E.print t - | _ -> assert false let hash x = diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 87e10b0bc..bafcb9a09 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -93,7 +93,7 @@ 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 cases = Ty.type_body name params in let constrs = @@ -462,7 +462,7 @@ 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 -> + | Ty.Tadt (name, params, _) as ty -> let cases = Ty.type_body name params in let ds = try Ty.assoc_destrs c cases with Not_found -> assert false @@ -548,7 +548,7 @@ 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 cases = Ty.type_body name params in try diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index 8e9dedd3d..b75a1bc29 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -314,11 +314,11 @@ module Make (X : Arg) : S with type theory = X.t = struct | _ , [] -> l1 | _ -> List.fold_left (fun acc e -> e :: acc) l2 (List.rev l1) - let xs_modulo_records t { Ty.lbs; _ } = - List.rev + (* let xs_modulo_records t { Ty.lbs; _ } = + List.rev (List.rev_map (fun (hs, ty) -> - E.mk_term (Symbols.Op (Symbols.Access hs)) [t] ty) lbs) + E.mk_term (Symbols.Op (Symbols.Access hs)) [t] ty) lbs) *) module SLE = (* sets of lists of terms *) Set.Make(struct @@ -413,13 +413,13 @@ module Make (X : Arg) : S with type theory = X.t = struct (fun t l -> let { E.f = f; xs = xs; ty = ty; _ } = E.term_view t in if Symbols.compare f_pat f = 0 then xs::l - else - begin - match f_pat, ty with - | Symbols.Op (Symbols.Record), Ty.Trecord record -> - (xs_modulo_records t record) :: l - | _ -> l - end + else l + (* begin + match f_pat, ty with + | Symbols.Op (Symbols.Record), Ty.Trecord record -> + (xs_modulo_records t record) :: l + | _ -> l + end *) ) cl [] in let cl = filter_classes mconf cl tbox in diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml index d36a88526..78eb6699a 100644 --- a/src/lib/reasoners/relation.ml +++ b/src/lib/reasoners/relation.ml @@ -31,15 +31,13 @@ module X = Shostak.Combine module Rel1 : Sig_rel.RELATION = IntervalCalculus -module Rel2 : Sig_rel.RELATION = Records_rel +module Rel2 : Sig_rel.RELATION = Bitv_rel -module Rel3 : Sig_rel.RELATION = Bitv_rel +module Rel3 : Sig_rel.RELATION = Arrays_rel -module Rel4 : Sig_rel.RELATION = Arrays_rel +module Rel4 : Sig_rel.RELATION = Adt_rel -module Rel5 : Sig_rel.RELATION = Adt_rel - -module Rel6 : Sig_rel.RELATION = Ite_rel +module Rel5 : Sig_rel.RELATION = Ite_rel (* This value is unused. *) let timer = Timers.M_None @@ -50,7 +48,6 @@ type t = { r3: Rel3.t; r4: Rel4.t; r5: Rel5.t; - r6: Rel6.t; } let empty uf = @@ -59,8 +56,7 @@ let empty uf = let r3, doms3 = Rel3.empty (Uf.set_domains uf doms2) in let r4, doms4 = Rel4.empty (Uf.set_domains uf doms3) in let r5, doms5 = Rel5.empty (Uf.set_domains uf doms4) in - let r6, doms6 = Rel6.empty (Uf.set_domains uf doms5) in - {r1; r2; r3; r4; r5; r6}, doms6 + {r1; r2; r3; r4; r5}, doms5 let (|@|) l1 l2 = if l1 == [] then l2 @@ -89,14 +85,10 @@ let assume env uf sa = Timers.with_timer Rel5.timer Timers.F_assume @@ fun () -> Rel5.assume env.r5 (Uf.set_domains uf doms4) sa in - let env6, doms6, ({ assume = a6; remove = rm6}:_ Sig_rel.result) = - Timers.with_timer Rel6.timer Timers.F_assume @@ fun () -> - Rel6.assume env.r6 (Uf.set_domains uf doms5) sa - in - {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6}, - doms6, - ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6; - remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 } + {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5}, + doms5, + ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5; + remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 } : _ Sig_rel.result) let assume_th_elt env th_elt dep = @@ -106,8 +98,7 @@ let assume_th_elt env th_elt dep = let env3 = Rel3.assume_th_elt env.r3 th_elt dep in let env4 = Rel4.assume_th_elt env.r4 th_elt dep in let env5 = Rel5.assume_th_elt env.r5 th_elt dep in - let env6 = Rel6.assume_th_elt env.r6 th_elt dep in - {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6} + {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5} let try_query (type a) (module R : Sig_rel.RELATION with type t = a) env uf a k = @@ -122,8 +113,7 @@ let query env uf a = try_query (module Rel2) env.r2 uf a @@ fun () -> try_query (module Rel3) env.r3 uf a @@ fun () -> try_query (module Rel4) env.r4 uf a @@ fun () -> - try_query (module Rel5) env.r5 uf a @@ fun () -> - try_query (module Rel6) env.r6 uf a @@ fun () -> None + try_query (module Rel5) env.r5 uf a @@ fun () -> None let case_split env uf ~for_model = Options.exec_thread_yield (); @@ -132,8 +122,7 @@ let case_split env uf ~for_model = let seq3 = Rel3.case_split env.r3 uf ~for_model in let seq4 = Rel4.case_split env.r4 uf ~for_model in let seq5 = Rel5.case_split env.r5 uf ~for_model in - let seq6 = Rel6.case_split env.r6 uf ~for_model in - let splits = [seq1; seq2; seq3; seq4; seq5; seq6] in + let splits = [seq1; seq2; seq3; seq4; seq5] in let splits = List.fold_left (|@|) [] splits in List.fast_sort (fun (_ ,_ , sz1) (_ ,_ , sz2) -> @@ -158,8 +147,7 @@ let optimizing_objective env uf o = Rel1.optimizing_objective env.r1 uf; Rel2.optimizing_objective env.r2 uf; Rel3.optimizing_objective env.r3 uf; - Rel4.optimizing_objective env.r4 uf; - Rel5.optimizing_objective env.r5 uf + Rel4.optimizing_objective env.r4 uf ] let add env uf r t = @@ -169,9 +157,7 @@ let add env uf r t = let r3, doms3, eqs3 =Rel3.add env.r3 (Uf.set_domains uf doms2) r t in let r4, doms4, eqs4 =Rel4.add env.r4 (Uf.set_domains uf doms3) r t in let r5, doms5, eqs5 =Rel5.add env.r5 (Uf.set_domains uf doms4) r t in - let r6, doms6, eqs6 =Rel6.add env.r6 (Uf.set_domains uf doms5) r t in - {r1;r2;r3;r4;r5;r6}, doms6, eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6 - + {r1;r2;r3;r4;r5}, doms5, eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5 let instantiate ~do_syntactic_matching t_match env uf selector = Options.exec_thread_yield (); @@ -185,10 +171,8 @@ let instantiate ~do_syntactic_matching t_match env uf selector = Rel4.instantiate ~do_syntactic_matching t_match env.r4 uf selector in let r5, l5 = Rel5.instantiate ~do_syntactic_matching t_match env.r5 uf selector in - let r6, l6 = - Rel6.instantiate ~do_syntactic_matching t_match env.r6 uf selector in - {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6}, - l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1 + {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5}, + l5 |@| l4 |@| l3 |@| l2 |@| l1 let new_terms env = Rel1.new_terms env.r1 @@ -196,4 +180,3 @@ let new_terms env = |> Expr.Set.union @@ Rel3.new_terms env.r3 |> Expr.Set.union @@ Rel4.new_terms env.r4 |> Expr.Set.union @@ Rel5.new_terms env.r5 - |> Expr.Set.union @@ Rel6.new_terms env.r6 diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 919783407..6ef1950c6 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -37,14 +37,11 @@ module rec CX : sig val extract1 : r -> ARITH.t option val embed1 : ARITH.t -> r - val extract2 : r -> RECORDS.t option - val embed2 : RECORDS.t -> r + val extract2 : r -> BITV.t option + val embed2 : BITV.t -> r - val extract3 : r -> BITV.t option - val embed3 : BITV.t -> r - - val extract4 : r -> ADT.t option - val embed4 : ADT.t -> r + val extract3 : r -> ADT.t option + val embed3 : ADT.t -> r end = struct @@ -53,7 +50,6 @@ struct | Term of Expr.t | Ac of AC.t | Arith of ARITH.t - | Records of RECORDS.t | Bitv of BITV.t | Adt of ADT.t @@ -68,7 +64,6 @@ struct if Options.get_term_like_pp () then begin match r.v with | Arith t -> fprintf fmt "%a" ARITH.print t - | Records t -> fprintf fmt "%a" RECORDS.print t | Bitv t -> fprintf fmt "%a" BITV.print t | Adt t -> fprintf fmt "%a" ADT.print t | Term t -> fprintf fmt "%a" Expr.print t @@ -78,8 +73,6 @@ struct match r.v with | Arith t -> fprintf fmt "Arith(%s):[%a]" ARITH.name ARITH.print t - | Records t -> - fprintf fmt "Records(%s):[%a]" RECORDS.name RECORDS.print t | Bitv t -> fprintf fmt "Bitv(%s):[%a]" BITV.name BITV.print t | Adt t -> @@ -161,7 +154,6 @@ struct let hash r = let res = match r.v with | Arith x -> 1 + 10 * ARITH.hash x - | Records x -> 2 + 10 * RECORDS.hash x | Bitv x -> 3 + 10 * BITV.hash x | Adt x -> 6 + 10 * ADT.hash x | Ac ac -> 9 + 10 * AC.hash ac @@ -172,7 +164,6 @@ struct let eq r1 r2 = match r1.v, r2.v with | Arith x, Arith y -> ARITH.equal x y - | Records x, Records y -> RECORDS.equal x y | Bitv x, Bitv y -> BITV.equal x y | Adt x, Adt y -> ADT.equal x y | Term x, Term y -> Expr.equal x y @@ -198,9 +189,8 @@ struct (* end: Hconsing modules and functions *) let embed1 x = hcons {v = Arith x; id = -1000 (* dummy *)} - let embed2 x = hcons {v = Records x; id = -1000 (* dummy *)} - let embed3 x = hcons {v = Bitv x; id = -1000 (* dummy *)} - let embed4 x = hcons {v = Adt x; id = -1000 (* dummy *)} + let embed2 x = hcons {v = Bitv x; id = -1000 (* dummy *)} + let embed3 x = hcons {v = Adt x; id = -1000 (* dummy *)} let ac_embed ({ Sig.l; _ } as t) = match l with @@ -215,9 +205,8 @@ struct let term_embed t = hcons {v = Term t; id = -1000 (* dummy *)} let extract1 = function { v=Arith r; _ } -> Some r | _ -> None - let extract2 = function { v=Records r; _ } -> Some r | _ -> None - let extract3 = function { v=Bitv r; _ } -> Some r | _ -> None - let extract4 = function { v=Adt r; _ } -> Some r | _ -> None + let extract2 = function { v=Bitv r; _ } -> Some r | _ -> None + let extract3 = function { v=Adt r; _ } -> Some r | _ -> None let ac_extract = function | { v = Ac t; _ } -> Some t @@ -226,7 +215,6 @@ struct let term_extract r = match r.v with | Arith _ -> ARITH.term_extract r - | Records _ -> RECORDS.term_extract r | Bitv _ -> BITV.term_extract r | Adt _ -> ADT.term_extract r | Ac _ -> None, false (* SYLVAIN : TODO *) @@ -236,7 +224,6 @@ struct let res = match r.v with | Arith _ -> ARITH.to_model_term r - | Records _ -> RECORDS.to_model_term r | Bitv _ -> BITV.to_model_term r | Adt _ -> ADT.to_model_term r | Term t when Expr.is_model_term t -> Some t @@ -251,7 +238,6 @@ struct let type_info = function | { v = Arith t; _ } -> ARITH.type_info t - | { v = Records t; _ } -> RECORDS.type_info t | { v = Bitv t; _ } -> BITV.type_info t | { v = Adt t; _ } -> ADT.type_info t | { v = Ac x; _ } -> AC.type_info x @@ -263,9 +249,8 @@ struct | Ac _ -> -1 | Term _ -> -2 | Arith _ -> -3 - | Records _ -> -4 - | Bitv _ -> -5 - | Adt _ -> -7 + | Bitv _ -> -4 + | Adt _ -> -5 let compare_tag a b = theory_num a - theory_num b @@ -274,7 +259,6 @@ struct else match a.v, b.v with | Arith _, Arith _ -> ARITH.compare a b - | Records _, Records _ -> RECORDS.compare a b | Bitv _, Bitv _ -> BITV.compare a b | Adt _, Adt _ -> ADT.compare a b | Term x, Term y -> Expr.compare x y @@ -289,7 +273,6 @@ struct | Term t -> Expr.hash t | Ac x -> AC.hash x | Arith x -> ARITH.hash x - | Records x -> RECORDS.hash x | Bitv x -> BITV.hash x | Arrays x -> ARRAYS.hash x | Adt x -> ADT.hash x @@ -318,7 +301,6 @@ struct let leaves r = match r.v with | Arith t -> ARITH.leaves t - | Records t -> RECORDS.leaves t | Bitv t -> BITV.leaves t | Adt t -> ADT.leaves t | Ac t -> r :: (AC.leaves t) @@ -327,7 +309,6 @@ struct let is_constant r = match r.v with | Arith t -> ARITH.is_constant t - | Records t -> RECORDS.is_constant t | Bitv t -> BITV.is_constant t | Adt t -> ADT.is_constant t | Term t -> @@ -344,7 +325,6 @@ struct if equal p v then r else match r.v with | Arith t -> ARITH.subst p v t - | Records t -> RECORDS.subst p v t | Bitv t -> BITV.subst p v t | Adt t -> ADT.subst p v t | Ac t -> if equal p r then v else AC.subst p v t @@ -355,32 +335,27 @@ struct let not_restricted = not @@ Options.get_restricted () in match ARITH.is_mine_symb sb, - not_restricted && RECORDS.is_mine_symb sb, not_restricted && BITV.is_mine_symb sb, not_restricted && ADT.is_mine_symb sb, AC.is_mine_symb sb with - | true, false, false, false, false -> + | true, false, false, false -> Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () -> ARITH.make t - | false, true, false, false, false -> - Timers.with_timer Timers.M_Records Timers.F_make @@ fun () -> - RECORDS.make t - - | false, false, true, false, false -> + | false, true, false, false -> Timers.with_timer Timers.M_Bitv Timers.F_make @@ fun () -> BITV.make t - | false, false, false, true, false -> + | false, false, true, false -> Timers.with_timer Timers.M_Adt Timers.F_make @@ fun () -> ADT.make t - | false, false, false, false, true -> + | false, false, false, true -> Timers.with_timer Timers.M_AC Timers.F_make @@ fun () -> AC.make t - | false, false, false, false, false -> + | false, false, false, false -> term_embed t, [] | _ -> assert false @@ -389,30 +364,26 @@ struct let not_restricted = not @@ Options.get_restricted () in match ARITH.is_mine_symb sb, - not_restricted && RECORDS.is_mine_symb sb, not_restricted && BITV.is_mine_symb sb, not_restricted && ADT.is_mine_symb sb, AC.is_mine_symb sb with - | true, false, false, false, false -> + | true, false, false, false -> ARITH.fully_interpreted sb - | false, true, false, false, false -> - RECORDS.fully_interpreted sb - | false, false, true, false, false -> + | false, true, false, false -> BITV.fully_interpreted sb - | false, false, false, true, false -> + | false, false, true, false -> ADT.fully_interpreted sb - | false, false, false, false, true -> + | false, false, false, true -> AC.fully_interpreted sb - | false, false, false, false, false -> + | false, false, false, false -> false | _ -> assert false let is_solvable_theory_symbol sb = ARITH.is_mine_symb sb || not (Options.get_restricted ()) && - (RECORDS.is_mine_symb sb || - BITV.is_mine_symb sb || + (BITV.is_mine_symb sb|| ADT.is_mine_symb sb) let is_a_leaf r = match r.v with @@ -426,18 +397,15 @@ struct | _ -> match ARITH.is_mine_symb ac.Sig.h, - RECORDS.is_mine_symb ac.Sig.h, BITV.is_mine_symb ac.Sig.h, ADT.is_mine_symb ac.Sig.h, AC.is_mine_symb ac.Sig.h with (*AC.is_mine may say F if Options.get_no_ac is set to F dynamically *) - | true, false, false, false, false -> + | true, false, false, false -> ARITH.color ac - | false, true, false, false, false -> - RECORDS.color ac - | false, false, true, false, false -> + | false, true, false, false -> BITV.color ac - | false, false, false, true, false -> + | false, false, true, false -> ADT.color ac | _ -> ac_embed ac @@ -445,7 +413,6 @@ struct Debug.debug_abstract_selectors a; match a.v with | Arith a -> ARITH.abstract_selectors a acc - | Records a -> RECORDS.abstract_selectors a acc | Bitv a -> BITV.abstract_selectors a acc | Adt a -> ADT.abstract_selectors a acc | Term _ -> a, acc @@ -527,10 +494,6 @@ struct Timers.with_timer ARITH.timer Timers.F_solve @@ fun () -> ARITH.solve ra rb pb - | Ty.Trecord _ -> - Timers.with_timer RECORDS.timer Timers.F_solve @@ fun () -> - RECORDS.solve ra rb pb - | Ty.Tbitv _ -> Timers.with_timer BITV.timer Timers.F_solve @@ fun () -> BITV.solve ra rb pb @@ -577,7 +540,6 @@ struct let opt = match r.v, type_info r with | _, Ty.Tint | _, Ty.Treal -> ARITH.assign_value r distincts eq - | _, Ty.Trecord _ -> RECORDS.assign_value r distincts eq | _, Ty.Tbitv _ -> BITV.assign_value r distincts eq | Term t, Ty.Tfarray _ -> begin @@ -642,24 +604,14 @@ and ARITH : Sig.SHOSTAK let embed = CX.embed1 end) -and RECORDS : Sig.SHOSTAK - with type r = CX.r - and type t = CX.r Records.abstract = - Records.Shostak - (struct - include CX - let extract = extract2 - let embed = embed2 - end) - and BITV : Sig.SHOSTAK with type r = CX.r and type t = CX.r Bitv.abstract = Bitv.Shostak (struct include CX - let extract = extract3 - let embed = embed3 + let extract = extract2 + let embed = embed2 end) and ADT : Sig.SHOSTAK @@ -668,8 +620,8 @@ and ADT : Sig.SHOSTAK Adt.Shostak (struct include CX - let extract = extract4 - let embed = embed4 + let extract = extract3 + let embed = embed3 end) (* Its signature is not Sig.SHOSTAK because it does not provide a solver *) @@ -711,7 +663,6 @@ module Combine = struct end module Arith = ARITH -module Records = RECORDS module Bitv = BITV module Adt = ADT module Polynome = TARITH diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli index 0fdc94591..d8fd29fc7 100644 --- a/src/lib/reasoners/shostak.mli +++ b/src/lib/reasoners/shostak.mli @@ -40,9 +40,6 @@ module Polynome : Polynome.T module Arith : Sig.SHOSTAK with type r = Combine.r and type t = Polynome.t -module Records : Sig.SHOSTAK - with type r = Combine.r and type t = Combine.r Records.abstract - module Bitv : Sig.SHOSTAK with type r = Combine.r and type t = Combine.r Bitv.abstract diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index ad9ad7962..4a3544961 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -164,18 +164,12 @@ module Main_Default : S = struct | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> mp | Tvar _ -> assert false - | Text (_, hs) | Trecord { name = hs; _ } when - Ty_map.mem hs mp -> mp - + | Text (_, hs) when Ty_map.mem hs mp -> mp | Text (l, hs) -> let l = List.map (fun _ -> Ty.fresh_tvar()) l in Ty_map.add hs (Text(l, hs)) mp - | Trecord { name; _ } -> - (* cannot do better for records ? *) - Ty_map.add name ty mp - - | Tadt (hs, _) -> + | Tadt (hs, _, _) -> (* cannot do better for ADT ? *) Ty_map.add hs ty mp )sty Ty_map.empty @@ -189,20 +183,6 @@ module Main_Default : S = struct | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> () | Tvar _ -> assert false | Text _ -> print_dbg ~flushed:false "type %a@ " Ty.print ty - | Trecord { Ty.lbs; _ } -> - print_dbg ~flushed:false ~header:false "type %a = " Ty.print ty; - begin match lbs with - | [] -> assert false - | (lbl, ty)::l -> - let print fmt (lbl,ty) = - Format.fprintf fmt " ; %a :%a" - DE.Term.Const.print lbl Ty.print ty in - print_dbg ~flushed:false ~header:false - "{ %a : %a%a" - DE.Term.Const.print lbl Ty.print ty - (pp_list_no_space print) l; - print_dbg ~flushed:false ~header:false " }@ " - end | Tadt _ -> print_dbg ~flushed:false ~header:false "%a@ " Ty.print_full ty )types; diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7945afddd..3389ce72f 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -445,20 +445,6 @@ module SmtPrinter = struct pp x.let_e pp_boxed x.in_e - | Sy.(Op Record), _ -> - begin - match ty with - | Ty.Trecord { Ty.lbs = lbs; record_constr; _ } -> - assert (List.compare_lengths xs lbs = 0); - Fmt.pf ppf "@[<2>(%a %a@])" - DE.Term.Const.print record_constr - Fmt.(list ~sep:sp pp |> box) xs - - | _ -> - (* Excluded by the typechecker. *) - assert false - end - | Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op | Sy.Op Minus, [e1; { f = Sy.Real q; _ }] when is_zero e1.f -> @@ -620,7 +606,7 @@ module AEPrinter = struct assert false and pp_silent ppf t = - let { f ; xs ; ty; bind; _ } = t in + let { f ; xs ; bind; _ } = t in match f, xs with | Sy.Form form, xs -> pp_formula ppf form xs bind @@ -647,25 +633,6 @@ module AEPrinter = struct | Sy.(Op Extract (i, j)), [e] -> Fmt.pf ppf "%a^{%d, %d}" pp e i j - | Sy.(Op (Access field)), [e] -> - Fmt.pf ppf "%a.%a" pp e DE.Term.Const.print field - - | Sy.(Op Record), _ -> - begin match ty with - | Ty.Trecord { Ty.lbs = lbs; _ } -> - assert (List.compare_lengths xs lbs = 0); - Fmt.pf ppf "{"; - ignore (List.fold_left2 (fun first (field,_) e -> - Fmt.pf ppf "%s%a = %a" (if first then "" else "; ") - DE.Term.Const.print field pp e; - false - ) true lbs xs); - Fmt.pf ppf "}"; - | _ -> - (* Excluded by the typechecker. *) - assert false - end - | Sy.(Op ((Pow | Integer_round | Max_real | Min_real | Max_int | Min_int) as op)), [e1; e2] -> Fmt.pf ppf "%a(%a, %a)" Symbols.pp_ae_operator op pp e1 pp e2 @@ -1112,7 +1079,7 @@ let mk_ite cond th el = let rec is_model_term e = match e.f, e.xs with - | (Op Constr _ | Op Record | Op Set), xs -> List.for_all is_model_term xs + | (Op Constr _ | Op Set), xs -> List.for_all is_model_term xs | Op Div, [{ f = Real _; _ }; { f = Real _; _ }] -> true | Op Minus, [{ f = Real q; _ }; { f = Real _; _ }] -> Q.equal q Q.zero | Op Minus, [{ f = Int i; _ }; { f = Int _; _ }] -> Z.equal i Z.zero @@ -1321,8 +1288,6 @@ let mk_constr c xs ty = let mk_tester cons t = mk_builtin ~is_pos:true (Sy.IsConstr cons) [t] -let mk_record xs ty = mk_term (Sy.Op Record) xs ty - let void = mk_constr Dolmen.Std.Expr.Term.Cstr.void [] Ty.tunit (** Substitutions *) @@ -1960,11 +1925,9 @@ module Triggers = struct | { f = Op (Get | Set) ; xs = [t1 ; t2]; _ } -> max (score_term t1) (score_term t2) - | { f = Op (Access _ | Destruct _ | Extract _) ; xs = [t]; _ } -> + | { f = Op (Destruct _ | Extract _) ; xs = [t]; _ } -> 1 + score_term t - | { f = Op Record; xs; _ } -> - 1 + (List.fold_left - (fun acc t -> max (score_term t) acc) 0 xs) + | { f = Op Set; xs = [t1; t2; t3]; _ } -> max (score_term t1) (max (score_term t2) (score_term t3)) @@ -2047,14 +2010,6 @@ module Triggers = struct | { f = Op Concat; _ }, _ -> -1 | _, { f = Op Concat; _ } -> 1 - | { f = Op (Access a1) ; xs=[t1]; _ }, - { f = Op (Access a2) ; xs=[t2]; _ } -> - let c = DE.Term.Const.compare a1 a2 in - if c<>0 then c else cmp_trig_term t1 t2 - - | { f = Op (Access _); _ }, _ -> -1 - | _, { f = Op (Access _); _ } -> 1 - | { f = Op (Destruct a1) ; xs = [t1]; _ }, { f = Op (Destruct a2) ; xs = [t2]; _ } -> let c = DE.Term.Const.compare a1 a2 in @@ -2063,11 +2018,6 @@ module Triggers = struct | { f = Op (Destruct _); _ }, _ -> -1 | _, { f =Op (Destruct _); _ } -> 1 - | { f = Op Record ; xs= lbs1; _ }, { f = Op Record ; xs = lbs2; _ } -> - Util.cmp_lists lbs1 lbs2 cmp_trig_term - | { f = Op Record; _ }, _ -> -1 - | _, { f = Op Record; _ } -> 1 - | { f = (Op _) as s1; xs=tl1; _ }, { f = (Op _) as s2; xs=tl2; _ } -> (* ops that are not infix or prefix *) let l1 = List.map score_term tl1 in @@ -2677,7 +2627,6 @@ let mk_match e cases = let mk_destr = match ty with | Ty.Tadt _ -> (fun hs -> Sy.destruct hs) - | Ty.Trecord _ -> (fun hs -> Sy.Op (Sy.Access hs)) | _ -> assert false in let mker = @@ -2686,9 +2635,6 @@ let mk_match e cases = (fun e name -> mk_builtin ~is_pos:true (Sy.IsConstr name) [e]) - | Ty.Trecord _ -> - (fun _e _name -> assert false) (* no need to test for records *) - | _ -> assert false in let res = compile_match mk_destr mker e cases e in diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index bdb726682..a541471ff 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -294,7 +294,6 @@ val mk_constr : Dolmen.Std.Expr.term_cst -> t list -> Ty.t -> t [Nest.attach_orders]. *) val mk_tester : Dolmen.Std.Expr.term_cst -> t -> t -val mk_record : t list -> Ty.t -> t (** Substitutions *) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 87e47fb45..a848d7092 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -37,8 +37,7 @@ type operator = (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow (* ADTs *) - | Access of DE.term_cst | Record - | Constr of DE.term_cst (* enums, adts *) + | Constr of DE.term_cst | Destruct of DE.term_cst (* Arrays *) | Get | Set @@ -188,7 +187,7 @@ let compare_kinds k1 k2 = let compare_operators op1 op2 = Util.compare_algebraic op1 op2 (function - | Access h1, Access h2 | Constr h1, Constr h2 + | Constr h1, Constr h2 | Destruct h1, Destruct h2 -> DE.Term.Const.compare h1 h2 | Extract (i1, j1), Extract (i2, j2) -> @@ -200,7 +199,7 @@ let compare_operators op1 op2 = | Int2BV n1, Int2BV n2 -> Int.compare n1 n2 | _ , (Plus | Minus | Mult | Div | Modulo | Real_is_int | Concat | Extract _ | Sign_extend _ | Repeat _ | Get | Set | Float - | Access _ | Record | Sqrt_real | Abs_int | Abs_real + | Sqrt_real | Abs_int | Abs_real | Real_of_int | Int_floor | Int_ceil | Sqrt_real_default | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int | Integer_log2 | Pow | Integer_round @@ -380,8 +379,6 @@ module AEPrinter = struct | Set -> Fmt.pf ppf "set" (* DT theory *) - | Record -> Fmt.pf ppf "@Record" - | Access tcst -> Fmt.pf ppf "@Access_%a" DE.Term.Const.print tcst | Constr tcst | Destruct tcst -> DE.Term.Const.print ppf tcst @@ -489,9 +486,7 @@ module SmtPrinter = struct | Set -> Fmt.pf ppf "store" (* DT theory *) - | Record -> () - | Access tcst | Constr tcst | Destruct tcst -> - DE.Term.Const.print ppf tcst + | Constr tcst | Destruct tcst -> DE.Term.Const.print ppf tcst (* Float theory *) | Float -> Fmt.pf ppf "ae.round" diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index eb93fb3e7..ac99780d8 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -35,8 +35,7 @@ type operator = (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow (* ADTs *) - | Access of Dolmen.Std.Expr.term_cst | Record - | Constr of Dolmen.Std.Expr.term_cst (* enums, adts *) + | Constr of Dolmen.Std.Expr.term_cst | Destruct of Dolmen.Std.Expr.term_cst (* Arrays *) | Get | Set diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 31716e50a..cd7be0e51 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -35,19 +35,10 @@ type t = | Tbitv of int | Text of t list * DE.ty_cst | Tfarray of t * t - | Tadt of DE.ty_cst * t list - | Trecord of trecord + | Tadt of DE.ty_cst * t list * bool and tvar = { v : int ; mutable value : t option } -and trecord = { - mutable args : t list; - name : DE.ty_cst; - mutable lbs : (DE.term_cst * t) list; - record_constr : DE.term_cst; - (* for ADTs that become records. default is "{" *) -} - module Smtlib = struct let rec pp ppf = function | Tint -> Fmt.pf ppf "Int" @@ -56,11 +47,9 @@ module Smtlib = struct | Tbitv n -> Fmt.pf ppf "(_ BitVec %d)" n | Tfarray (a_t, r_t) -> Fmt.pf ppf "(Array %a %a)" pp a_t pp r_t - | Text ([], name) - | Trecord { args = []; name; _ } | Tadt (name, []) -> + | Text ([], name) | Tadt (name, [], _) -> DE.Ty.Const.print ppf name - | Text (args, name) - | Trecord { args; name; _ } | Tadt (name, args) -> + | Text (args, name) | Tadt (name, args, _) -> Fmt.(pf ppf "(@[%a %a@])" DE.Ty.Const.print name (list ~sep:sp pp) args) | Tvar { v; value = None; _ } -> Fmt.pf ppf "A%d" v | Tvar { value = Some t; _ } -> pp ppf t @@ -96,7 +85,6 @@ let assoc_destrs hs cases = (*** pretty print ***) let print_generic body_of = - let h = Hashtbl.create 17 in let rec print = let open Format in fun body_of fmt -> function @@ -105,13 +93,6 @@ let print_generic body_of = | Tbool -> fprintf fmt "bool" | Tbitv n -> fprintf fmt "bitv[%d]" n | Tvar{v=v ; value = None} -> fprintf fmt "'a_%d" v - | Tvar{v=v ; value = Some (Trecord { args = l; name = n; _ } as t) } -> - if Hashtbl.mem h v then - fprintf fmt "%a %a" print_list l DE.Ty.Const.print n - else - (Hashtbl.add h v (); - (*fprintf fmt "('a_%d->%a)" v print t *) - print body_of fmt t) | Tvar{ value = Some t; _ } -> (*fprintf fmt "('a_%d->%a)" v print t *) print body_of fmt t @@ -121,22 +102,7 @@ let print_generic body_of = fprintf fmt "%a %a" print_list l DE.Ty.Const.print s | Tfarray (t1, t2) -> fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2 - | Trecord { args = lv; name = n; lbs = lbls; _ } -> - begin - fprintf fmt "%a %a" print_list lv DE.Ty.Const.print n; - if body_of != None then begin - fprintf fmt " = {"; - let first = ref true in - List.iter - (fun (s, t) -> - fprintf fmt "%s%a : %a" (if !first then "" else "; ") - DE.Term.Const.print s (print body_of) t; - first := false - ) lbls; - fprintf fmt "}" - end - end - | Tadt (n, lv) -> + | Tadt (n, lv, _) -> fprintf fmt "%a %a" print_list lv DE.Ty.Const.print n; begin match body_of with | None -> () @@ -212,16 +178,11 @@ let rec shorten ty = if t1 == t1' && t2 == t2' then ty else Tfarray(t1', t2') - | Trecord r -> - r.args <- List.map shorten r.args; - r.lbs <- List.map (fun (lb, ty) -> lb, shorten ty) r.lbs; - ty - - | Tadt (n, args) -> + | Tadt (n, args, record) -> let args' = List.map shorten args in shorten_body n args; (* should not rebuild the type if no changes are made *) - Tadt (n, args') + Tadt (n, args', record) | Tint | Treal | Tbool | Tbitv _ -> ty @@ -243,17 +204,7 @@ let rec compare t1 t2 = if c<>0 then c else compare ta2 tb2 | Tfarray _, _ -> -1 | _ , Tfarray _ -> 1 - | Trecord { args = a1; name = s1; lbs = l1; _ }, - Trecord { args = a2; name = s2; lbs = l2; _ } -> - let c = DE.Ty.Const.compare s1 s2 in - if c <> 0 then c else - let c = compare_list a1 a2 in - if c <> 0 then c else - let l1, l2 = List.map snd l1, List.map snd l2 in - compare_list l1 l2 - | Trecord _, _ -> -1 | _ , Trecord _ -> 1 - - | Tadt (s1, pars1), Tadt (s2, pars2) -> + | Tadt (s1, pars1, _), Tadt (s2, pars2, _) -> let c = DE.Ty.Const.compare s1 s2 in if c <> 0 then c else compare_list pars1 pars2 @@ -289,20 +240,10 @@ let rec equal t1 t2 = with Invalid_argument _ -> false) | Tfarray (ta1, ta2), Tfarray (tb1, tb2) -> equal ta1 tb1 && equal ta2 tb2 - | Trecord { args = a1; name = s1; lbs = l1; _ }, - Trecord { args = a2; name = s2; lbs = l2; _ } -> - begin - try - DE.Ty.Const.equal s1 s2 && List.for_all2 equal a1 a2 && - List.for_all2 - (fun (l1, ty1) (l2, ty2) -> - DE.Term.Const.equal l1 l2 && equal ty1 ty2) l1 l2 - with Invalid_argument _ -> false - end | Tint, Tint | Treal, Treal | Tbool, Tbool -> true | Tbitv n1, Tbitv n2 -> n1 =n2 - | Tadt (s1, pars1), Tadt (s2, pars2) -> + | Tadt (s1, pars1, _), Tadt (s2, pars2, _) -> begin try DE.Ty.Const.equal s1 s2 && List.for_all2 equal pars1 pars2 with Invalid_argument _ -> false @@ -327,13 +268,9 @@ let rec matching s pat t = List.fold_left2 matching s l1 l2 | Tfarray (ta1,ta2), Tfarray (tb1,tb2) -> matching (matching s ta1 tb1) ta2 tb2 - | Trecord r1, Trecord r2 when DE.Ty.Const.equal r1.name r2.name -> - let s = List.fold_left2 matching s r1.args r2.args in - List.fold_left2 - (fun s (_, p) (_, ty) -> matching s p ty) s r1.lbs r2.lbs | Tint , Tint | Tbool , Tbool | Treal , Treal -> s | Tbitv n , Tbitv m when n=m -> s - | Tadt(n1, args1), Tadt(n2, args2) when DE.Ty.Const.equal n1 n2 -> + | Tadt(n1, args1, _), Tadt(n2, args2, _) when DE.Ty.Const.equal n1 n2 -> List.fold_left2 matching s args1 args2 | _ , _ -> raise (TypeClash(pat,t)) @@ -353,20 +290,10 @@ let apply_subst = let t2' = apply_subst s t2 in if t1 == t1' && t2 == t2' then ty else Tfarray (t1', t2') - | Trecord r -> - let lbs, same1 = My_list.apply_right (apply_subst s) r.lbs in - let args, same2 = My_list.apply (apply_subst s) r.args in - if same1 && same2 then ty - else - Trecord - {r with args = args; - name = r.name; - lbs = lbs} - - | Tadt(name, params) + | Tadt(name, params, record) [@ocaml.ppwarning "TODO: detect when there are no changes "] -> - Tadt (name, List.map (apply_subst s) params) + Tadt (name, List.map (apply_subst s) params, record) | Tint | Treal | Tbool | Tbitv _ -> ty in @@ -394,18 +321,9 @@ let rec fresh ty subst = let ty1, subst = fresh ty1 subst in let ty2, subst = fresh ty2 subst in Tfarray (ty1, ty2), subst - | Trecord ({ args; name = n; lbs; _ } as r) -> + | Tadt(s,args, record) -> let args, subst = fresh_list args subst in - let lbs, subst = - List.fold_right - (fun (x,ty) (lbs, subst) -> - let ty, subst = fresh ty subst in - (x, ty)::lbs, subst) lbs ([], subst) - in - Trecord {r with args = args; name = n; lbs = lbs}, subst - | Tadt(s, args) -> - let args, subst = fresh_list args subst in - Tadt (s, args), subst + Tadt (s,args, record), subst | t -> t, subst (* Assume that [shorten] have been applied on [lty]. *) @@ -528,8 +446,8 @@ let fresh_empty_text = in text [] id -let t_adt ?(body=None) s ty_vars = - let ty = Tadt (s, ty_vars) in +let t_adt ?(record=false) ?(body=None) s ty_vars = + let ty = Tadt (s, ty_vars, record) in begin match body with | None -> () | Some [] -> assert false @@ -559,23 +477,13 @@ let tunit = let ty = t_adt ~body DE.Ty.Const.unit [] in ty -let trecord ~record_constr lv name lbs = - Trecord { record_constr; args = lv; name; lbs = lbs} - let rec hash t = match t with | Tvar{ v; _ } -> v | Text(l,s) -> abs (List.fold_left (fun acc x-> acc*19 + hash x) (DE.Ty.Const.hash s) l) | Tfarray (t1,t2) -> 19 * (hash t1) + 23 * (hash t2) - | Trecord { args; name = s; _ } -> - (* We do not hash constructors. *) - let h = - List.fold_left (fun h ty -> 27 * h + hash ty) (DE.Ty.Const.hash s) args - in - abs h - - | Tadt (ty, args) -> + | Tadt (ty, args, _) -> (* We do not hash constructors. *) let h = List.fold_left (fun h ty -> 31 * h + hash ty) (DE.Ty.Const.hash ty) args @@ -604,10 +512,7 @@ let vty_of t = | Tvar { v = i ; value = None } -> Svty.add i acc | Text(l,_) -> List.fold_left vty_of_rec acc l | Tfarray (t1,t2) -> vty_of_rec (vty_of_rec acc t1) t2 - | Trecord { args; lbs; _ } -> - let acc = List.fold_left vty_of_rec acc args in - List.fold_left (fun acc (_, ty) -> vty_of_rec acc ty) acc lbs - | Tadt(_, args) -> + | Tadt(_, args, _) -> List.fold_left vty_of_rec acc args | Tvar { value = Some _ ; _ } diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 4bb69218b..3f6e1fdea 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -51,7 +51,7 @@ type t = (** Functional arrays. [TFarray (src,dst)] maps values of type [src] to values of type [dst]. *) - | Tadt of Dolmen.Std.Expr.ty_cst * t list + | Tadt of Dolmen.Std.Expr.ty_cst * t list * bool (** Application of algebraic data types. [Tadt (a, params)] denotes the application of the polymorphic datatype [a] to the types parameters [params]. @@ -60,9 +60,6 @@ type t = value [Tadt (Hstring.make "list", [Tint]] where the identifier {e list} denotes a polymorphic ADT defined by the user with [t_adt]. *) - | Trecord of trecord - (** Record type. *) - and tvar = { v : int; (** Unique identifier *) @@ -74,20 +71,6 @@ and tvar = { hence distinct types should have disjoints sets of type variables (see function {!val:fresh}). *) -and trecord = { - mutable args : t list; - (** Arguments passed to the record constructor *) - name : Dolmen.Std.Expr.ty_cst; - (** Name of the record type *) - mutable lbs : (Dolmen.Std.Expr.term_cst * t) list; - (** List of fields of the record. Each field has a name, - and an associated type. *) - record_constr : Dolmen.Std.Expr.term_cst; - (** record constructor. Useful is case it's a specialization of an - algeberaic datatype. Default value is "\{__[name]" *) -} -(** Record types. *) - type adt_constr = { constr : Dolmen.Std.Expr.term_cst ; (** constructor of an ADT type *) @@ -168,6 +151,7 @@ val text : t list -> Dolmen.Std.Expr.ty_cst -> t given. *) val t_adt : + ?record:bool -> ?body:((Dolmen.Std.Expr.term_cst * (Dolmen.Std.Expr.term_cst * t) list) list) option -> Dolmen.Std.Expr.ty_cst -> @@ -180,17 +164,6 @@ val t_adt : argument is the name of the type. The third one provides its list of arguments. *) -val trecord : - record_constr:Dolmen.Std.Expr.term_cst -> - t list -> Dolmen.Std.Expr.ty_cst -> (Dolmen.Std.Expr.term_cst * t) list -> t -(** Create a record type. [trecord args name lbs] creates a record - type with name [name], arguments [args] and fields [lbs]. - - If [sort_fields] is true, the record fields are sorted according to - [Hstring.compare]. This is to preserve compatibility with the old - typechecker behavior and should not be used in new code. *) - - (** {2 Substitutions} *) module M : Map.S with type key = int diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index 168e7c8a0..5ee810575 100644 --- a/src/lib/structures/typed.ml +++ b/src/lib/structures/typed.ml @@ -83,8 +83,7 @@ and 'a tt_desc = | TTextract of 'a atterm * int * int | TTconcat of 'a atterm * 'a atterm - | TTdot of 'a atterm * Hstring.t - | TTrecord of (Hstring.t * 'a atterm) list + | TTrecord of Ty.t * (Hstring.t * 'a atterm) list | TTlet of (Symbols.t * 'a atterm) list * 'a atterm | TTnamed of Hstring.t * 'a atterm | TTite of 'a atform * @@ -220,9 +219,7 @@ let rec print_term = fprintf fmt "%a^{%d, %d}" print_term t1 i j | TTconcat (t1, t2) -> fprintf fmt "%a @@ %a" print_term t1 print_term t2 - | TTdot (t1, s) -> - fprintf fmt "%a.%s" print_term t1 (Hstring.view s) - | TTrecord l -> + | TTrecord (_, l) -> fprintf fmt "{ "; List.iter (fun (s, t) -> fprintf fmt "%s = %a" (Hstring.view s) print_term t) l; diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli index f23992689..343f2a668 100644 --- a/src/lib/structures/typed.mli +++ b/src/lib/structures/typed.mli @@ -118,9 +118,7 @@ and 'a tt_desc = (** Extract a sub-bitvector *) | TTconcat of 'a atterm * 'a atterm (* Concatenation of bitvectors *) - | TTdot of 'a atterm * Hstring.t - (** Field access on structs/records *) - | TTrecord of (Hstring.t * 'a atterm) list + | TTrecord of Ty.t * (Hstring.t * 'a atterm) list (** Record creation. *) | TTlet of (Symbols.t * 'a atterm) list * 'a atterm (** Let-bindings. Accept a list of mutually recursive le-bindings. *)