Skip to content

Commit

Permalink
Use type variables of Dolmen directly
Browse files Browse the repository at this point in the history
  • Loading branch information
@Halbaroth
Halbaroth committed Oct 25, 2024
1 parent 73949e9 commit 3aeec5d
Show file tree
Hide file tree
Showing 5 changed files with 70 additions and 105 deletions.
6 changes: 3 additions & 3 deletions src/lib/frontend/translate.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1687,7 +1687,7 @@ let make_form name_base f loc ~decl_kind =
in
assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
let ff = E.purify_form ff in
if Ty.Tvar.Set.is_empty (E.free_type_vars ff) then ff
if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
else
E.mk_forall name_base loc Var.Map.empty [] ff ~toplevel:true ~decl_kind

Expand Down Expand Up @@ -1943,7 +1943,7 @@ let make dloc_file acc stmt =
assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
let ff = E.purify_form ff in
let e =
if Ty.Tvar.Set.is_empty (E.free_type_vars ff) then ff
if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
else
E.mk_forall name_base loc
Var.Map.empty [] ff ~toplevel:true ~decl_kind
Expand All @@ -1964,7 +1964,7 @@ let make dloc_file acc stmt =
assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
let ff = E.purify_form ff in
let e =
if Ty.Tvar.Set.is_empty (E.free_type_vars ff) then ff
if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
else
E.mk_forall name_base loc
Var.Map.empty [] ff ~toplevel:true ~decl_kind
Expand Down
72 changes: 36 additions & 36 deletions src/lib/structures/expr.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ and term_view = {
bind : bind_kind;
tag: int;
vars : (Ty.t * int) Var.Map.t; (* vars to types and nb of occurences *)
vty : Ty.Tvar.Set.t;
vty : Ty.TvSet.t;
depth: int;
nb_nodes : int;
pure : bool;
Expand Down Expand Up @@ -337,9 +337,9 @@ module SmtPrinter = struct
pp_boxed ppf main

and pp_quantified bind ppf q =
if q.toplevel && not @@ Ty.Tvar.Set.is_empty q.main.vty then
if q.toplevel && not @@ Ty.TvSet.is_empty q.main.vty then
Fmt.pf ppf "@[<2>(par (%a)@, %a)@]"
Fmt.(box @@ iter ~sep:sp Ty.Tvar.Set.iter Ty.Tvar.pp) q.main.vty
Fmt.(box @@ iter ~sep:sp Ty.TvSet.iter DE.Ty.Var.print) q.main.vty
(pp_main bind) q
else
pp_main bind ppf q
Expand Down Expand Up @@ -791,7 +791,7 @@ let free_type_vars t = t.vty

let is_ground t =
Var.Map.is_empty (free_vars t Var.Map.empty) &&
Ty.Tvar.Set.is_empty (free_type_vars t)
Ty.TvSet.is_empty (free_type_vars t)

let size t = t.nb_nodes

Expand Down Expand Up @@ -865,7 +865,7 @@ let free_vars_non_form s l ty =
| _, e::r -> List.fold_left (fun s t -> merge_vars s t.vars) e.vars r

let free_type_vars_non_form l ty =
List.fold_left (fun acc t -> Ty.Tvar.Set.union acc t.vty) (Ty.vty_of ty) l
List.fold_left (fun acc t -> Ty.TvSet.union acc t.vty) (Ty.vty_of ty) l

let is_ite s = match s with
| Sy.Op Sy.Tite -> true
Expand Down Expand Up @@ -949,7 +949,7 @@ let vrai =
let res =
let nb_nodes = 0 in
let vars = Var.Map.empty in
let vty = Ty.Tvar.Set.empty in
let vty = Ty.TvSet.empty in
let faux =
HC.make
{f = Sy.False; xs = []; ty = Ty.Tbool; depth = -2; (*smallest depth*)
Expand Down Expand Up @@ -1029,7 +1029,7 @@ let mk_or f1 f2 is_impl =
let d = (max f1.depth f2.depth) in (* the +1 causes regression *)
let nb_nodes = f1.nb_nodes + f2.nb_nodes + 1 in
let vars = merge_vars f1.vars f2.vars in
let vty = Ty.Tvar.Set.union f1.vty f2.vty in
let vty = Ty.TvSet.union f1.vty f2.vty in
let pos =
HC.make {f=Sy.Form (Sy.F_Clause is_impl); xs=[f1; f2]; ty=Ty.Tbool;
depth=d; tag= -42; vars; vty; nb_nodes; neg = None;
Expand Down Expand Up @@ -1059,7 +1059,7 @@ let mk_iff f1 f2 =
let d = (max f1.depth f2.depth) in (* the +1 causes regression *)
let nb_nodes = f1.nb_nodes + f2.nb_nodes + 1 in
let vars = merge_vars f1.vars f2.vars in
let vty = Ty.Tvar.Set.union f1.vty f2.vty in
let vty = Ty.TvSet.union f1.vty f2.vty in
let pos =
HC.make {f=Sy.Form Sy.F_Iff; xs=[f1; f2]; ty=Ty.Tbool;
depth=d; tag= -42; vars; vty; nb_nodes; neg = None;
Expand Down Expand Up @@ -1146,7 +1146,7 @@ let mk_forall_ter =
lemma. Otherwise (if not toplevel), the free vtys of the lemma
are those of lem.main *)
let vty =
if new_q.toplevel then Ty.Tvar.Set.empty
if new_q.toplevel then Ty.TvSet.empty
else free_type_vars new_q.main
in
let vars =
Expand Down Expand Up @@ -1181,7 +1181,7 @@ let no_occur_check v e =
not (Var.Map.mem v e.vars)

let no_vtys l =
List.for_all (fun e -> Ty.Tvar.Set.is_empty e.vty) l
List.for_all (fun e -> Ty.TvSet.is_empty e.vty) l

(** smart constructors for literals *)

Expand Down Expand Up @@ -1490,7 +1490,7 @@ and mk_let_aux ({ let_v; let_e; in_e; _ } as x) =
let nb_nodes = let_e.nb_nodes + in_e.nb_nodes + 1 (* approx *) in
(* do not include free vars in let_sko that have been simplified *)
let vars = merge_vars let_e.vars (Var.Map.remove let_v in_e.vars) in
let vty = Ty.Tvar.Set.union let_e.vty in_e.vty in
let vty = Ty.TvSet.union let_e.vty in_e.vty in
let pos =
HC.make {f=Sy.Let; xs=[]; ty;
depth=d; tag= -42; vars; vty; nb_nodes; neg = None;
Expand All @@ -1513,7 +1513,7 @@ and mk_forall_bis (q : quantified) =
let binders = (* ignore binders that are not used in f *)
Var.Map.filter (fun v _ -> Var.Map.mem v q.main.vars) q.binders
in
if Var.Map.is_empty binders && Ty.Tvar.Set.is_empty q.main.vty then q.main
if Var.Map.is_empty binders && Ty.TvSet.is_empty q.main.vty then q.main
else
let q = {q with binders} in
(* Attempt to reduce the number of quantifiers. We try to find a
Expand Down Expand Up @@ -1571,7 +1571,7 @@ and find_particular_subst =
in
fun binders trs f ->
(* TODO: move the test for `trs` outside. *)
if not (Ty.Tvar.Set.is_empty f.vty) || has_hypotheses trs ||
if not (Ty.TvSet.is_empty f.vty) || has_hypotheses trs ||
has_semantic_triggers trs
then
None
Expand Down Expand Up @@ -1688,7 +1688,7 @@ let resolution_of_literal a binders free_vty acc =
match lit_view a with
| Pred(t, _) ->
let cond =
Ty.Tvar.Set.subset free_vty (free_type_vars t) &&
Ty.TvSet.subset free_vty (free_type_vars t) &&
let vars = free_vars t Var.Map.empty in
Var.Map.for_all (fun v _ -> Var.Map.mem v vars) binders
in
Expand Down Expand Up @@ -1770,7 +1770,7 @@ let resolution_triggers ~is_back { kind; main = f; binders; _ } =
)cand []

let free_type_vars_as_types e =
Ty.Tvar.Set.fold
Ty.TvSet.fold
(fun tv z -> Ty.Set.add (Ty.Tvar tv) z)
(free_type_vars e) Ty.Set.empty

Expand All @@ -1795,7 +1795,7 @@ let mk_let let_v let_e in_e =

let skolemize { main = f; binders; sko_v; sko_vty; _ } =
let print fmt ty =
assert (Ty.Tvar.Set.is_empty (Ty.vty_of ty));
assert (Ty.TvSet.is_empty (Ty.vty_of ty));
Format.fprintf fmt "<%a>" Ty.print ty
in
let pp_sep_nospace fmt () = Format.fprintf fmt "" in
Expand Down Expand Up @@ -1921,7 +1921,7 @@ module Triggers = struct
module STRS =
Set.Make(
struct
type t = expr * Var.Set.t * Ty.Tvar.Set.t
type t = expr * Var.Set.t * Ty.TvSet.t

let compare (t1,_,_) (t2,_,_) = compare t1 t2
end)
Expand Down Expand Up @@ -2092,7 +2092,7 @@ module Triggers = struct
fun l ->
unique (List.stable_sort cmp_trig_term_list l) []

let vty_of_term acc t = Ty.Tvar.Set.union acc t.vty
let vty_of_term acc t = Ty.TvSet.union acc t.vty

let not_pure t = not t.pure

Expand All @@ -2113,11 +2113,11 @@ module Triggers = struct
variables. *)
not (List.exists not_pure l) &&
let s1 = List.fold_left (vars_of_term bv) Var.Set.empty l in
let s2 = List.fold_left vty_of_term Ty.Tvar.Set.empty l in
let s2 = List.fold_left vty_of_term Ty.TvSet.empty l in
(* TODO: we can replace `Var.Set.subset bv s1`
by `Var.Seq.equal bv s1`. By construction `s1` is
a subset of `bv`. *)
Var.Set.subset bv s1 && Ty.Tvar.Set.subset vty s2 )
Var.Set.subset bv s1 && Ty.TvSet.subset vty s2 )
trs

(* unused
Expand All @@ -2129,8 +2129,8 @@ module Triggers = struct
if List.exists not_pure l then
failwith "If-Then-Else are not allowed in (theory triggers)";
let s1 = List.fold_left (vars_of_term bv) SSet.empty l in
let s2 = List.fold_left vty_of_term Ty.Tvar.Set.empty l in
if not (Ty.Tvar.Set.subset vty s2) || not (SSet.subset bv s1) then
let s2 = List.fold_left vty_of_term Ty.TvSet.empty l in
if not (Ty.TvSet.subset vty s2) || not (SSet.subset bv s1) then
failwith "Triggers of a theory should contain every quantified \
types and variables.")
trs;
Expand Down Expand Up @@ -2158,7 +2158,7 @@ module Triggers = struct
module SLLT =
Set.Make(
struct
type t = expr list * Var.Set.t * Ty.Tvar.Set.t
type t = expr list * Var.Set.t * Ty.TvSet.t
let compare (a, y1, _) (b, y2, _) =
let c = try compare_lists a b compare; 0 with Util.Cmp c -> c in
if c <> 0 then c else Var.Set.compare y1 y2
Expand Down Expand Up @@ -2209,14 +2209,14 @@ module Triggers = struct
let llt, llt_ok =
SLLT.fold
(fun (l, bv2, vty2) (llt, llt_ok) ->
if Var.Set.subset bv1 bv2 && Ty.Tvar.Set.subset vty1 vty2 then
if Var.Set.subset bv1 bv2 && Ty.TvSet.subset vty1 vty2 then
(* t doesn't bring new vars *)
llt, llt_ok
else
let bv3 = Var.Set.union bv2 bv1 in
let vty3 = Ty.Tvar.Set.union vty2 vty1 in
let vty3 = Ty.TvSet.union vty2 vty1 in
let e = t::l, bv3, vty3 in
if Var.Set.subset bv bv3 && Ty.Tvar.Set.subset vty vty3 then
if Var.Set.subset bv bv3 && Ty.TvSet.subset vty vty3 then
(* The multi-trigger [e] cover all the free variables [bv]
and [vty]. *)
llt, SLLT.add e llt_ok
Expand Down Expand Up @@ -2245,17 +2245,17 @@ module Triggers = struct
List.exists
(fun (_, bv',vty') ->
(Var.Set.subset bv bv' && not(Var.Set.equal bv bv')
&& Ty.Tvar.Set.subset vty vty')
|| (Ty.Tvar.Set.subset vty vty' && not(Ty.Tvar.Set.equal vty vty')
&& Ty.TvSet.subset vty vty')
|| (Ty.TvSet.subset vty vty' && not(Ty.TvSet.equal vty vty')
&& Var.Set.subset bv bv') ) l
in fun bv_a vty_a l ->
let rec simpl_rec acc = function
| [] -> acc
| ((_, bv, vty) as e)::l ->
if strict_subset bv vty l || strict_subset bv vty acc ||
(Var.Set.subset bv_a bv && Ty.Tvar.Set.subset vty_a vty) ||
(Var.Set.subset bv_a bv && Ty.TvSet.subset vty_a vty) ||
(Var.Set.equal (Var.Set.inter bv_a bv) Var.Set.empty &&
Ty.Tvar.Set.equal (Ty.Tvar.Set.inter vty_a vty) Ty.Tvar.Set.empty)
Ty.TvSet.equal (Ty.TvSet.inter vty_a vty) Ty.TvSet.empty)
then simpl_rec acc l
else simpl_rec (e::acc) l
in
Expand All @@ -2281,7 +2281,7 @@ module Triggers = struct
and [vtype]. *)
let mono = List.filter
(fun (_, bv_t, vty_t) ->
Var.Set.subset vterm bv_t && Ty.Tvar.Set.subset vtype vty_t) trs
Var.Set.subset vterm bv_t && Ty.TvSet.subset vtype vty_t) trs
in
let trs_v, trs_nv = List.partition (fun (t, _, _) -> is_var t) mono in
let base = if menv.Util.triggers_var then trs_nv @ trs_v else trs_nv in
Expand Down Expand Up @@ -2370,7 +2370,7 @@ module Triggers = struct
Var.Map.exists (fun e _ -> Var.Set.mem e bv) bv_lf
in
let has_tyvar vty vty_lf =
Ty.Tvar.Set.exists (fun e -> Ty.Tvar.Set.mem e vty) vty_lf
Ty.TvSet.exists (fun e -> Ty.TvSet.mem e vty) vty_lf
in
let args_of e lets =
match e.bind with
Expand Down Expand Up @@ -2466,9 +2466,9 @@ module Triggers = struct
)terms terms

let check_user_triggers f toplevel binders trs0 ~decl_kind =
if Var.Map.is_empty binders && Ty.Tvar.Set.is_empty f.vty then trs0
if Var.Map.is_empty binders && Ty.TvSet.is_empty f.vty then trs0
else
let vtype = if toplevel then f.vty else Ty.Tvar.Set.empty in
let vtype = if toplevel then f.vty else Ty.TvSet.empty in
let vterm =
Var.Map.fold (fun v _ s -> Var.Set.add v s) binders Var.Set.empty
in
Expand All @@ -2485,7 +2485,7 @@ module Triggers = struct
filter_good_triggers (vterm, vtype) trs0

let make f binders decl_kind mconf =
if Var.Map.is_empty binders && Ty.Tvar.Set.is_empty f.vty then []
if Var.Map.is_empty binders && Ty.TvSet.is_empty f.vty then []
else
let vtype = f.vty in
let vterm =
Expand Down Expand Up @@ -2591,7 +2591,7 @@ let mk_forall name loc binders trs f ~toplevel ~decl_kind =
user_trs = trs; main = f; sko_v; sko_vty; kind = decl_kind}

let mk_exists name loc binders trs f ~toplevel ~decl_kind =
if not toplevel || Ty.Tvar.Set.is_empty f.vty then
if not toplevel || Ty.TvSet.is_empty f.vty then
neg (mk_forall name loc binders trs (neg f) ~toplevel ~decl_kind)
else
(* If there are type variables in a toplevel exists: 1 - we add
Expand Down
4 changes: 2 additions & 2 deletions src/lib/structures/expr.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ type term_view = private {
(** Map of free term variables in the term to their type and
number of occurrences. *)

vty : Ty.Tvar.Set.t;
vty : Ty.TvSet.t;
(** Map of free type variables in the term. *)

depth: int;
Expand Down Expand Up @@ -222,7 +222,7 @@ val compare_let : letin -> letin -> int

(** Some auxiliary functions *)
val free_vars : t -> (Ty.t * int) Var.Map.t -> (Ty.t * int) Var.Map.t
val free_type_vars : t -> Ty.Tvar.Set.t
val free_type_vars : t -> Ty.TvSet.t
val is_ground : t -> bool
val size : t -> int
val depth : t -> int
Expand Down
Loading

0 comments on commit 3aeec5d

Please sign in to comment.