Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove the Typed module #1258

Merged
merged 2 commits into from
Nov 12, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion rsc/extra/subgraphs.dot
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,6 @@ subgraph cluster_lib {
"Expr";
"Xliteral";
"Ty";
"Typed";
"Commands";
"Errors";
"Fpa_rounding";
Expand Down
2 changes: 1 addition & 1 deletion src/lib/dune
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion src/lib/frontend/frontend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
158 changes: 110 additions & 48 deletions src/lib/frontend/translate.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down
1 change: 0 additions & 1 deletion src/lib/index.mld
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@ be sent to the SMT solver.

{!modules:
AltErgoLib.Ty
AltErgoLib.Typed
AltErgoLib.Expr
AltErgoLib.Commands
}
Expand Down
7 changes: 0 additions & 7 deletions src/lib/structures/commands.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
1 change: 0 additions & 1 deletion src/lib/structures/commands.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
115 changes: 17 additions & 98 deletions src/lib/structures/expr.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1300,26 +1300,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

Expand Down Expand Up @@ -2617,88 +2618,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
Expand Down
6 changes: 4 additions & 2 deletions src/lib/structures/expr.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -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
Expand Down
Loading
Loading