Skip to content

Commit

Permalink
ADT destructors are delayed functions
Browse files Browse the repository at this point in the history
Before this PR, the ADT destructors worked as follow:
- Destructor applictions from the user input were guarded: there are
  considered as aliens by the ADT theory;
- If the domain of an ADT semantic values became a singleton or if the
  input contains a tester application on this value, the ADT destructor
  application on this semantic value became interpreted.

The reason of this contruction is because all the functions are total in
the SMT-LIB standard, even the destructors. So a destructor is partially
interpreted:

If `v` is an ADT value and `d` is a destructor of this ADT associated
with the constructor `c`, then:
- `d v` can be anything if the constructor of `v` isn't necessary `c`;
- `d v` is the field of `c` associated with `d` if the only possible
  constructor for `v` is `c`.

This PR uses the new mechanism `Rel_utils.Delayed` to delay the
computation of `d v` until we know that `v` is of the form `(c ...)`.
  • Loading branch information
Halbaroth committed Apr 2, 2024
1 parent 8d62c62 commit 0a1f35e
Show file tree
Hide file tree
Showing 17 changed files with 144 additions and 302 deletions.
4 changes: 2 additions & 2 deletions src/lib/frontend/cnf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -149,8 +149,8 @@ let rec make_term quant_basename t =
let t2 = mk_term t2 in
E.mk_ite cond t1 t2

| TTproject (b, t, s) ->
E.mk_term (Sy.destruct ~guarded:b (Hstring.view s)) [mk_term t] ty
| TTproject (t, s) ->
E.mk_term (Sy.destruct (Hstring.view s)) [mk_term t] ty

| TTmatch (e, pats) ->
let e = make_term quant_basename e in
Expand Down
2 changes: 1 addition & 1 deletion src/lib/frontend/d_cnf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1046,7 +1046,7 @@ let rec mk_expr
| Trecord _ ->
Sy.Op (Sy.Access (Hstring.make name))
| Tadt _ ->
Sy.destruct ~guarded:true name
Sy.destruct name
| _ -> assert false
in
E.mk_term sy [e] ty
Expand Down
5 changes: 2 additions & 3 deletions src/lib/frontend/models.ml
Original file line number Diff line number Diff line change
Expand Up @@ -185,9 +185,8 @@ module Pp_smtlib_term = struct
else
fprintf fmt "(%a %a %a)" print e1 Sy.print f print e2

| Sy.Op Sy.Destruct (hs, grded), [e] ->
fprintf fmt "%a#%s%a"
print e (if grded then "" else "!") Hstring.print hs
| Sy.Op Sy.Destruct hs, [e] ->
fprintf fmt "%a#%a" print e Hstring.print hs


| Sy.In(lb, rb), [t] ->
Expand Down
4 changes: 2 additions & 2 deletions src/lib/frontend/parsed_interface.ml
Original file line number Diff line number Diff line change
Expand Up @@ -337,5 +337,5 @@ let mk_match loc expr cases =
let mk_algebraic_test loc expr cstr =
mk_localized loc (PPisConstr (expr, cstr))

let mk_algebraic_project loc ~guarded expr cstr =
mk_localized loc (PPproject (guarded, expr, cstr))
let mk_algebraic_project loc expr cstr =
mk_localized loc (PPproject (expr, cstr))
2 changes: 1 addition & 1 deletion src/lib/frontend/parsed_interface.mli
Original file line number Diff line number Diff line change
Expand Up @@ -258,4 +258,4 @@ val mk_match : Loc.t -> lexpr -> (pattern * lexpr) list -> lexpr

val mk_algebraic_test : Loc.t -> lexpr -> string -> lexpr

val mk_algebraic_project : Loc.t -> guarded:bool -> lexpr -> string -> lexpr
val mk_algebraic_project : Loc.t -> lexpr -> string -> lexpr
18 changes: 9 additions & 9 deletions src/lib/frontend/typechecker.ml
Original file line number Diff line number Diff line change
Expand Up @@ -494,7 +494,7 @@ module Env = struct
let pp_profile = PFunction ([pur_ty], lbl_ty) in
let mk_sy s =
if record then (Symbols.Op (Access (Hstring.make s)))
else Symbols.destruct ~guarded:true s
else Symbols.destruct s
in
let kind = if record then RecordDestr else AdtDestr in
add_logics ~kind env mk_sy [destr, ""] pp_profile loc
Expand Down Expand Up @@ -621,7 +621,7 @@ let mk_adequate_app p s te_args ty logic_kind =

| Env.RecordDestr, [te], _ -> TTdot(te, hp)

| Env.AdtDestr, [te], _ -> TTproject (true, te, hp)
| Env.AdtDestr, [te], _ -> TTproject (te, hp)

| Env.RecordDestr, _, _ -> assert false
| Env.RecordConstr, _, _ -> assert false
Expand Down Expand Up @@ -951,14 +951,14 @@ let rec type_term ?(call_from_type_form=false) env f =
| Ty.TypeClash(t1,t2) -> Errors.typing_error (Unification(t1,t2)) loc
end

| PPproject (grded, t, lbl) ->
| PPproject (t, lbl) ->
let te = type_term env t in
begin
try
match Env.fresh_type env lbl loc with
| _, {Env.args = [arg] ; result}, Env.AdtDestr ->
Ty.unify te.c.tt_ty arg;
TTproject (grded, te, Hstring.make lbl), Ty.shorten result
TTproject (te, Hstring.make lbl), Ty.shorten result

| _, {Env.args = [arg] ; result}, Env.RecordDestr ->
Ty.unify te.c.tt_ty arg;
Expand Down Expand Up @@ -1675,7 +1675,7 @@ let rec no_alpha_renaming_b ((up, m) as s) f =
| PPisConstr (e, _) ->
no_alpha_renaming_b s e

| PPproject (_, e, _) ->
| PPproject (e, _) ->
no_alpha_renaming_b s e

let rec alpha_renaming_b ((up, m) as s) f =
Expand Down Expand Up @@ -1925,10 +1925,10 @@ let rec alpha_renaming_b ((up, m) as s) f =
let cases' = if !same_cases then cases else cases' in
{ f with pp_desc = PPmatch(e', cases') }

| PPproject(grded, f1, a) ->
| PPproject(f1, a) ->
let ff1 = alpha_renaming_b s f1 in
if f1 == ff1 then f
else {f with pp_desc = PPproject(grded, ff1, a)}
else {f with pp_desc = PPproject(ff1, a)}

| PPisConstr(f1, a) ->
let ff1 = alpha_renaming_b s f1 in
Expand Down Expand Up @@ -2089,8 +2089,8 @@ let rec mono_term {c = {tt_ty=tt_ty; tt_desc=tt_desc}; annot = id} =
| TTite (cond, t1, t2) ->
TTite (monomorphize_form cond, mono_term t1, mono_term t2)

| TTproject (grded, t, lbl) ->
TTproject (grded, mono_term t, lbl)
| TTproject (t, lbl) ->
TTproject (mono_term t, lbl)
| TTmatch (e, pats) ->
let e = mono_term e in
let pats = List.rev_map (fun (p, f) -> p, mono_term f) (List.rev pats) in
Expand Down
16 changes: 5 additions & 11 deletions src/lib/reasoners/adt.ml
Original file line number Diff line number Diff line change
Expand Up @@ -88,12 +88,12 @@ module Shostak (X : ALIEN) = struct
not (Options.get_disable_adts ()) &&
match sy, ty with
| Sy.Op (Sy.Constr _), Ty.Tadt _ -> true
| Sy.Op Sy.Destruct (_, guarded), _ ->
(* A guarded destructor isn't interpreted by the ADT theory.
| Sy.Op Sy.Destruct _, Ty.Tadt _ ->
(* A destructor is partially interpreted by the ADT theory.
If we assume the tester of the constructor associated with
this destructor, we propagate the non-guarded version of the
destructor. See the documentation of [env.selectors] in [Adt_rel]. *)
not guarded
false
| _ -> false

let embed r =
Expand Down Expand Up @@ -192,12 +192,7 @@ module Shostak (X : ALIEN) = struct
in
is_mine @@ Constr {c_name = hs; c_ty = ty; c_args}, ctx

| Sy.Op Sy.Destruct (hs, guarded), [e], _ ->
if not guarded then
let sel = Select {d_name = hs ; d_arg = e ; d_ty = ty} in
is_mine sel, ctx
else
X.term_embed t, ctx
| Sy.Op Sy.Destruct _, [_], _ -> X.term_embed t, ctx
(* No risk !
if equal sel (embed sel_x) then X.term_embed t, ctx
else sel_x, ctx (* canonization OK *)
Expand Down Expand Up @@ -236,8 +231,7 @@ module Shostak (X : ALIEN) = struct
| Alien r | Select { d_arg = r; _ } ->
X.is_constant r

| Constr { c_args; _ } ->
List.for_all (fun (_, r) -> X.is_constant r) c_args
| Constr _ -> true

[@@ocaml.ppwarning "TODO: not sure"]
let fully_interpreted _ =
Expand Down
Loading

0 comments on commit 0a1f35e

Please sign in to comment.