Remove the Typed module (#1258)

* Remove the Typed module

This AST was only used by the legacy typechecker and the match compilation. This PR removes the Typed AST and create a new type to store Dolmen patterns during match compilation.

rsc/extra/subgraphs.dot

@@ -187,7 +187,6 @@ subgraph cluster_lib {
                 "Expr";
                 "Xliteral";
                 "Ty";
-                "Typed";
                 "Commands";
                 "Errors";
                 "Fpa_rounding";

src/lib/dune

@@ -57,7 +57,7 @@
     ; structures
     Commands Errors Explanation Fpa_rounding
     Profiling Satml_types Symbols
-    Expr Var Ty Typed Xliteral ModelMap Id Objective Literal
+    Expr Var Ty Xliteral ModelMap Id Objective Literal
     ; util
     Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
     Options Timers Util Vec Version Steps Printer

src/lib/frontend/frontend.ml

@@ -452,7 +452,6 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         check_if_over (internal_assume ~loc:d.st_loc (n, f, mf)) env
       | PredDef (f, name) ->
         check_if_over (internal_pred_def ~loc:d.st_loc (name, f)) env
-      | RwtDef _ -> assert false
       | Query (n, f, sort) ->
         begin
           (* If we have reached an unknown state, we can return it right

src/lib/frontend/translate.ml

@@ -761,55 +761,117 @@ let handle_patt_var id (DE.{ term_descr; _ } as term)  =
       "Expected a variable in a case match but got %a"
       DE.Term.print term
 
-(** Helper function to translate patterns in a pattern-matching from a Dolmen
-    Term.t to an Alt-Ergo Expr.t *)
-let mk_pattern DE.{ term_descr; _ } =
-  match term_descr with
-  | App (
-      { term_descr =
-          Cst ({ builtin = B.Constructor { adt; case; }; _ } as cst); _
-      }, _, pargs
-    ) ->
-    let vnames =
-      begin match DT.definition adt with
-        | Some (Adt { cases; _ }) ->
-          let { DE.dstrs; _ } = cases.(case) in
-          Array.fold_right (
-            fun v acc ->
-              match v with
-              | Some dstr -> dstr :: acc
-              | _ -> assert false
-          ) dstrs []
-        | _ ->
-          Fmt.failwith
-            "Expected a constructor for an algebraic data type but got\
-             something else for the definition of: %a"
-            DE.Ty.Const.print adt
-      end
-    in
-    let rev_args =
-      List.fold_left2 (
-        fun acc rn arg ->
-          let v, n, ty = handle_patt_var rn arg in
-          (v, n, ty) :: acc
-      ) [] vnames pargs
-    in
-    let args = List.rev rev_args in
-    Typed.Constr {name = cst; args}
+module Match : sig
+  type pat
+  (** Type used as an intermediate description of patterns during the
+      match compilation. *)
+
+  val mk_pat : DE.term -> pat
+  (** Convert Dolmen pattern into the intermediate description. *)
+
+  val make : Expr.t -> (pat * Expr.t) list -> Expr.t
+  (** [make e l] compiles into ite expressions the match of the expression [e]
+      against the patterns of the branches [l]. *)
+end = struct
+  type pat =
+    | Var of Var.t
+    | Constr of DE.term_cst * (Var.t * DE.term_cst * Ty.t) list
+
+  (** Helper function to translate patterns in a pattern-matching from a Dolmen
+      Term.t to an Alt-Ergo Expr.t *)
+  let mk_pat DE.{ term_descr; _ } =
+    match term_descr with
+    | App (
+        { term_descr =
+            Cst ({ builtin = B.Constructor { adt; case; }; _ } as cst); _
+        }, _, pargs
+      ) ->
+      let vnames =
+        begin match DT.definition adt with
+          | Some (Adt { cases; _ }) ->
+            let { DE.dstrs; _ } = cases.(case) in
+            Array.fold_right (
+              fun v acc ->
+                match v with
+                | Some dstr -> dstr :: acc
+                | _ -> assert false
+            ) dstrs []
+          | _ ->
+            Fmt.failwith
+              "Expected a constructor for an algebraic data type but got\
+               something else for the definition of: %a"
+              DE.Ty.Const.print adt
+        end
+      in
+      let rev_args =
+        List.fold_left2 (
+          fun acc rn arg ->
+            let v, n, ty = handle_patt_var rn arg in
+            (v, n, ty) :: acc
+        ) [] vnames pargs
+      in
+      Constr (cst, List.rev rev_args)
 
-  | Cst ({ builtin = B.Constructor _; _ } as cst) ->
-    Typed.Constr {name = cst; args = []}
+    | Cst ({ builtin = B.Constructor _; _ } as cst) ->
+      Constr (cst, [])
 
-  | Var ({ builtin = B.Base; path; _ } as t_v) ->
-    (* Should the type be passed as an argument
-       instead of re-evaluating it here? *)
-    let v = Var.of_string (get_basename path) in
-    let sy = Sy.var v in
-    Cache.store_sy t_v sy;
-    (* Adding the matched variable to the store *)
-    Typed.Var v
+    | Var ({ builtin = B.Base; path; _ } as t_v) ->
+      (* Should the type be passed as an argument
+         instead of re-evaluating it here? *)
+      let v = Var.of_string (get_basename path) in
+      let sy = Sy.var v in
+      Cache.store_sy t_v sy;
+      (* Adding the matched variable to the store *)
+      Var v
 
-  | _ -> assert false
+    | _ -> assert false
+
+  let rec compile mk_destr mk_tester e cases accu =
+    match cases with
+    | [] -> accu
+
+    | (Var x, p) :: _ ->
+      E.apply_subst (Var.Map.singleton x e, Ty.esubst) p
+
+    | (Constr (name, args), p) :: l ->
+      let _then =
+        List.fold_left
+          (fun acc (var, destr, ty) ->
+             let destr = mk_destr destr in
+             let d = E.mk_term destr [e] ty in
+             E.mk_let var d acc
+          ) p args
+      in
+      match l with
+        [] -> _then
+      | _ ->
+        let _else = compile mk_destr mk_tester e l accu in
+        let cond = mk_tester name e in
+        E.mk_ite cond _then _else
+
+  let make e cases =
+    let ty = E.type_info e in
+    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 mk_tester =
+      match ty with
+      | Ty.Tadt _ -> E.mk_tester
+      | Ty.Trecord _ ->
+        (* no need to test for records *)
+        (fun _e _name -> assert false)
+      | _ -> assert false
+    in
+    let res = compile mk_destr mk_tester e cases e in
+    (*     debug_compile_match e cases res; *)
+    res
+    [@ocaml.ppwarning "TODO: introduce a let if e is a big expr"]
+    [@ocaml.ppwarning "TODO: add other elim schemes"]
+    [@ocaml.ppwarning "TODO: add a match construct in expr"]
+end
 
 let arith_ty = function
   | `Int -> Ty.Tint
@@ -1367,12 +1429,12 @@ let rec mk_expr
         let pats =
           List.rev_map (
             fun (p, t) ->
-              let patt = mk_pattern p in
+              let patt = Match.mk_pat p in
               let e = aux_mk_expr t in
               patt, e
           ) (List.rev pats)
         in
-        E.mk_match e pats
+        Match.make e pats
 
       | Binder ((Let_par ls | Let_seq ls) as let_binder, body) ->
         let lsbis =

src/lib/index.mld

@@ -35,7 +35,6 @@ be sent to the SMT solver.
 
 {!modules:
 AltErgoLib.Ty
-AltErgoLib.Typed
 AltErgoLib.Expr
 AltErgoLib.Commands
 }

src/lib/structures/commands.ml

@@ -34,7 +34,6 @@ type sat_decl_aux =
   | Decl of Id.typed
   | Assume of string * Expr.t * bool
   | PredDef of Expr.t * string (*name of the predicate*)
-  | RwtDef of (Expr.t Typed.rwt_rule) list
   | Optimize of Objective.Function.t
   | Query of string *  Expr.t * Ty.goal_sort
   | ThAssume of Expr.th_elt
@@ -57,12 +56,6 @@ let print_aux fmt = function
     Format.fprintf fmt "assume %s(%b): @[<hov>%a@]" name b Expr.print e
   | PredDef (e, name) ->
     Format.fprintf fmt "pred-def %s: @[<hov>%a@]" name Expr.print e
-  | RwtDef l ->
-    Format.fprintf fmt "rwrts: @[<v>%a@]"
-      (Util.print_list_pp
-         ~sep:Format.pp_print_space
-         ~pp:(Typed.print_rwt Expr.print)
-      ) l
   | Query (name, e, sort) ->
     Format.fprintf fmt "query %s(%a): @[<hov>%a@]"
       name Ty.print_goal_sort sort Expr.print e

src/lib/structures/commands.mli

@@ -31,7 +31,6 @@ type sat_decl_aux =
   | Decl of Id.typed
   | Assume of string * Expr.t * bool
   | PredDef of Expr.t * string (*name of the predicate*)
-  | RwtDef of (Expr.t Typed.rwt_rule) list
   | Optimize of Objective.Function.t
   | Query of string *  Expr.t * Ty.goal_sort
   | ThAssume of Expr.th_elt

src/lib/structures/expr.ml

@@ -1299,26 +1299,27 @@ let mk_builtin ~is_pos n l =
 
 (** smart constructors for datatypes. *)
 
-let is_constr DE.{ builtin; _ } =
-  match builtin with
-  | DStd.Builtin.Constructor _ -> true
-  | _ -> false
-
 let has_attached_order id =
   DE.Term.Const.get_tag id Nest.order_tag |> Option.is_some
 
 let mk_constr c xs ty =
-  if not @@ is_constr c then
-    Fmt.invalid_arg "expected a constructor, got %a" DE.Id.print c;
-  (* This assertion ensures that the API of the [Nest] module have been
-     correctly used, that is [Nest.attach_orders] have been called on
-     the nest of [id] if [id] is a constructor of ADT. *)
-  if not @@ has_attached_order c then
-    Fmt.invalid_arg "no order on constructor %a" DE.Id.print c;
-  mk_term (Sy.Op (Constr c)) xs ty
-
-let mk_tester cons t =
-  mk_builtin ~is_pos:true (Sy.IsConstr cons) [t]
+  match c.DE.builtin with
+  | DStd.Builtin.Constructor _ ->
+    (* This assertion ensures that the API of the [Nest] module have been
+       correctly used, that is [Nest.attach_orders] have been called on
+       the nest of [id] if [id] is a constructor of ADT. *)
+    if not @@ has_attached_order c then
+      Fmt.invalid_arg "no order on constructor %a" DE.Id.print c;
+    mk_term (Sy.Op (Constr c)) xs ty
+  | _ ->
+    Fmt.invalid_arg "expected a constructor, got %a" DE.Id.print c
+
+let mk_tester c t =
+  match c.DE.builtin with
+  | DStd.Builtin.Constructor _ ->
+    mk_builtin ~is_pos:true (Sy.IsConstr c) [t]
+  | _ ->
+    Fmt.invalid_arg "expected a constructor, got %a" DE.Id.print c
 
 let mk_record xs ty = mk_term (Sy.Op Record) xs ty
 
@@ -2616,88 +2617,6 @@ let mk_exists name loc binders trs f ~toplevel ~decl_kind =
     in
     mk_forall name loc Var.Map.empty trs tmp ~toplevel ~decl_kind
 
-
-let rec compile_match mk_destr mker e cases accu =
-  match cases with
-  | [] -> accu
-
-  | (Typed.Var x, p) :: _ ->
-    apply_subst ((Var.Map.singleton x e), Ty.esubst) p
-
-  | (Typed.Constr {name; args}, p) :: l ->
-    let _then =
-      List.fold_left
-        (fun acc (var, destr, ty) ->
-           let destr = mk_destr destr in
-           let d = mk_term destr [e] ty in
-           mk_let var d acc
-        )p args
-    in
-    match l with
-      [] -> _then
-    | _ ->
-      let _else = compile_match mk_destr mker e l accu in
-      let cond = mker e name in
-      mk_ite cond _then _else
-
-(* TO BE REMOVED *)
-let debug_compile_match e cases res =
-  if Options.get_debug_adt () then begin
-    Printer.print_dbg  ~flushed:false ~module_name:"Expr"
-      "compilation of: match %a with@ " print e;
-    let p_list_vars fmt l =
-      match l with
-        [] -> ()
-      | [e,_,_] -> Var.print fmt e
-      | (e,_,_) :: l ->
-        Format.fprintf fmt "(%a" Var.print e;
-        List.iter (fun (e,_,_) -> Format.fprintf fmt ", %a" Var.print e) l;
-        Format.fprintf fmt ")"
-    in
-    List.iter
-      (fun (p, v) ->
-         match p with
-         | Typed.Constr {name; args} ->
-           Printer.print_dbg  ~flushed:false ~header:false
-             "| %a %a -> %a@ "
-             DE.Term.Const.print name
-             p_list_vars args
-             print v;
-         | Typed.Var x ->
-           Printer.print_dbg  ~flushed:false ~header:false
-             "| %a -> %a@ " Var.print x print v;
-      )cases;
-    Printer.print_dbg ~header:false
-      "end@ result is: %a" print res;
-  end
-
-let mk_match e cases =
-  let ty = type_info e in
-  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 =
-    match ty with
-    | Ty.Tadt _ ->
-      (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
-  debug_compile_match e cases res;
-  res
-  [@ocaml.ppwarning "TODO: introduce a let if e is a big expr"]
-  [@ocaml.ppwarning "TODO: add other elim schemes"]
-  [@ocaml.ppwarning "TODO: add a match construct in expr"]
-
-
 let is_pure e = e.pure
 
 module Purification = struct

src/lib/structures/expr.mli

@@ -294,6 +294,10 @@ 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
+(** [mk_tester c e] produces the tester expression ((_ is c) e).
+
+    @raise Invalid_argument if [c] is not a Dolmen constructor. *)
+
 val mk_record : t list -> Ty.t -> t
 
 (** Substitutions *)
@@ -396,8 +400,6 @@ val mk_exists :
 
 val mk_let : Var.t -> t -> t -> t
 
-val mk_match : t -> (Typed.pattern * t) list -> t
-
 val skolemize : quantified -> t
 
 val elim_let : recursive:bool -> letin -> t