ADT destructors are delayed functions

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 ...)`.

src/lib/frontend/cnf.ml

@@ -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

src/lib/frontend/d_cnf.ml

@@ -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

src/lib/frontend/models.ml

@@ -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] ->

src/lib/frontend/parsed_interface.ml

@@ -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))

src/lib/frontend/parsed_interface.mli

@@ -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

src/lib/frontend/typechecker.ml

@@ -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
@@ -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
@@ -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;
@@ -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 =
@@ -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
@@ -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

src/lib/reasoners/adt.ml

@@ -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 =
@@ -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 *)
@@ -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 _ =