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.

Sign up for GitHub

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

WIP: get rid of module rec and functors by moving many types into types.ml #576

Draft
wants to merge 3 commits into
base: next
Choose a base branch
from
Draft

WIP: get rid of module rec and functors by moving many types into types.ml #576

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
460e7c4
Rename X* in shostak.ml
lefessan Apr 14, 2023
87d2b0f
'make deps' should call 'opam', 'make dune-deps' calls 'dune-deps'
lefessan Apr 14, 2023
982962a
Move Symbols, Expr and Theory types in types.ml, get rid of module rec
lefessan Apr 15, 2023
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
3 changes: 3 additions & 0 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -348,6 +348,9 @@ archi: $(EXTRA_DIR)/ocamldot/ocamldot
dot -Tpdf archi.dot > archi.pdf

deps:
opam install --deps-only .

dune-deps:
dune-deps . | dot -Tpng -o docs/deps.png

.PHONY: archi deps
Expand Down
2 changes: 1 addition & 1 deletion src/bin/gui/annoted_ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ and at_desc =
| ATrecord of (Hstring.t * aterm) list
| ATnamed of Hstring.t * aterm
| ATmapsTo of Var.t * aterm
| ATinInterval of aterm * Symbols.bound * Symbols.bound
| ATinInterval of aterm * Types.bound * Types.bound
(* bool = true <-> interval is_open *)
| ATite of aform annoted * aterm * aterm

Expand Down
2 changes: 1 addition & 1 deletion src/bin/gui/annoted_ast.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ and at_desc =
| ATrecord of (Hstring.t * aterm) list
| ATnamed of Hstring.t * aterm
| ATmapsTo of Var.t * aterm
| ATinInterval of aterm * Symbols.bound * Symbols.bound
| ATinInterval of aterm * Types.bound * Types.bound
(* bool = true <-> interval is_open *)
| ATite of aform annoted * aterm * aterm

Expand Down
6 changes: 3 additions & 3 deletions src/bin/gui/main_gui.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -451,9 +451,9 @@ let add_inst ({ h; _ } as inst_model) orig =
let id = Expr.id orig in
let name =
match Expr.form_view orig with
| Expr.Lemma { Expr.name = n ; _ } when Stdlib.(<>) n "" -> n
| Expr.Lemma _ | Expr.Unit _ | Expr.Clause _ | Expr.Literal _
| Expr.Skolem _ | Expr.Let _ | Expr.Iff _ | Expr.Xor _ ->
| Lemma { name = n ; _ } when Stdlib.(<>) n "" -> n
| Lemma _ | Types.Unit _ | Types.Clause _ | Types.Literal _
| Types.Skolem _ | Types.Let _ | Types.Iff _ | Types.Xor _ ->
string_of_int id
in
let r, n, limit, to_add =
Expand Down
3 changes: 2 additions & 1 deletion src/lib/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,11 +56,12 @@
Commands Errors Explanation Fpa_rounding
Parsed Profiling Satml_types Symbols
Expr Var Ty Typed Xliteral ModelMap
Types
; util
Config Emap Gc_debug Hconsing Hstring Iheap Lists Loc
MyDynlink MyUnix Numbers NumsNumbers NumbersInterface
Options Timers Util Vec Version ZarithNumbers Steps Printer Format_shims
My_zip
My_zip CMap CSet Shostak_pre
)

(js_of_ocaml
Expand Down
64 changes: 33 additions & 31 deletions src/lib/frontend/cnf.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@
(* *)
(******************************************************************************)

open Types

module E = Expr
module Sy = Symbols
module SE = E.Set
Expand Down Expand Up @@ -79,46 +81,46 @@ let rec make_term up_qv quant_basename t =
let t2 = mk_term t2 in (*keep old mk_term order -> avoid regression*)
let t1 = mk_term t1 in
match s, ty with
| Sy.Op Sy.Plus, (Ty.Tint | Ty.Treal) ->
| Types.Op Types.Plus, (Ty.Tint | Ty.Treal) ->
let args = E.concat_chainable s ty t2 [] in
let args = E.concat_chainable s ty t1 args in
let args = List.fast_sort E.compare args in
E.mk_term s args ty
| _ -> E.mk_term s [t1; t2] ty
end

| TTprefix ((Sy.Op Sy.Minus) as s, n) ->
| TTprefix ((Types.Op Types.Minus) as s, n) ->
let t1 = if ty == Ty.Tint then E.int "0" else E.real "0" in
E.mk_term s [t1; mk_term n] ty
| TTprefix _ ->
assert false

| TTget (t1, t2) ->
E.mk_term (Sy.Op Sy.Get)
E.mk_term (Types.Op Types.Get)
[mk_term t1; mk_term t2] ty

| TTset (t1, t2, t3) ->
let t1 = mk_term t1 in
let t2 = mk_term t2 in
let t3 = mk_term t3 in
E.mk_term (Sy.Op Sy.Set) [t1; t2; t3] ty
E.mk_term (Types.Op Types.Set) [t1; t2; t3] ty

| TTextract (t1, t2, t3) ->
let t1 = mk_term t1 in
let t2 = mk_term t2 in
let t3 = mk_term t3 in
E.mk_term (Sy.Op Sy.Extract) [t1; t2; t3] ty
E.mk_term (Types.Op Types.Extract) [t1; t2; t3] ty

| TTconcat (t1, t2) ->
E.mk_term (Sy.Op Sy.Concat)
E.mk_term (Types.Op Types.Concat)
[mk_term t1; mk_term t2] ty

| TTdot (t, s) ->
E.mk_term (Sy.Op (Sy.Access s)) [mk_term t] ty
E.mk_term (Types.Op (Types.Access s)) [mk_term t] ty

| TTrecord lbs ->
let lbs = List.map (fun (_, t) -> mk_term t) lbs in
E.mk_term (Sy.Op Sy.Record) lbs ty
E.mk_term (Types.Op Types.Record) lbs ty

| TTlet (binders, t2) ->
let binders =
Expand All @@ -140,7 +142,7 @@ let rec make_term up_qv quant_basename t =
let cond =
make_form
up_qv quant_basename cond Loc.dummy
~decl_kind:E.Daxiom (* not correct, but not a problem *)
~decl_kind:Daxiom (* not correct, but not a problem *)
~toplevel:false
in
let t1 = mk_term t1 in
Expand All @@ -161,7 +163,7 @@ let rec make_term up_qv quant_basename t =
| TTform e ->
make_form
up_qv quant_basename e Loc.dummy
~decl_kind:E.Daxiom (* not correct, but not a problem *)
~decl_kind:Daxiom (* not correct, but not a problem *)
~toplevel:false
in
mk_term t
Expand Down Expand Up @@ -197,7 +199,7 @@ and make_trigger ~in_theory name up_qv quant_basename hyp (e, from_user) =
let trs = List.filter (fun t -> not (List.mem t l)) [t1; t2] in
let trs = List.map (make_term up_qv quant_basename) trs in
let lit =
E.mk_builtin ~is_pos:true Sy.LE
E.mk_builtin ~is_pos:true Types.LE
[make_term up_qv quant_basename t1;
make_term up_qv quant_basename t2]
in
Expand All @@ -208,7 +210,7 @@ and make_trigger ~in_theory name up_qv quant_basename hyp (e, from_user) =
let trs = List.filter (fun t -> not (List.mem t l)) [t1; t2] in
let trs = List.map (make_term up_qv quant_basename) trs in
let lit =
E.mk_builtin ~is_pos:true Sy.LT
E.mk_builtin ~is_pos:true Types.LT
[make_term up_qv quant_basename t1;
make_term up_qv quant_basename t2]
in
Expand All @@ -221,7 +223,7 @@ and make_trigger ~in_theory name up_qv quant_basename hyp (e, from_user) =
(* clean trigger:
remove useless terms in multi-triggers after inlining of lets*)
let trigger =
{ E.content ; guard ; t_depth; semantic = []; (* will be set by theories *)
{ content ; guard ; t_depth; semantic = []; (* will be set by theories *)
hyp; from_user;
}
in
Expand Down Expand Up @@ -249,7 +251,7 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
let lt = List.map (make_term up_qv name_base) lt in
E.mk_distinct ~iff:true lt
| TAle [t1;t2] ->
E.mk_builtin ~is_pos:true Sy.LE
E.mk_builtin ~is_pos:true Types.LE
[make_term up_qv name_base t1;
make_term up_qv name_base t2]
| TAlt [t1;t2] ->
Expand All @@ -259,20 +261,20 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
{c = {tt_ty = Ty.Tint;
tt_desc = TTconst(Tint "1")}; annot = t1.annot} in
let tt2 =
E.mk_term (Sy.Op Sy.Minus)
E.mk_term (Types.Op Types.Minus)
[make_term up_qv name_base t2;
make_term up_qv name_base one]
Ty.Tint
in
E.mk_builtin ~is_pos:true Sy.LE
E.mk_builtin ~is_pos:true Types.LE
[make_term up_qv name_base t1; tt2]
| _ ->
E.mk_builtin ~is_pos:true Sy.LT
E.mk_builtin ~is_pos:true Types.LT
[make_term up_qv name_base t1;
make_term up_qv name_base t2]
end
| TTisConstr (t, lbl) ->
E.mk_builtin ~is_pos:true (Sy.IsConstr lbl)
E.mk_builtin ~is_pos:true (Types.IsConstr lbl)
[make_term up_qv name_base t]

| _ -> assert false
Expand Down Expand Up @@ -309,7 +311,7 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
in
incr name_tag;
let up_qv =
List.fold_left (fun z (sy,ty) -> Sy.Map.add sy ty z) up_qv qf.qf_bvars
List.fold_left (fun z (sy,ty) -> Types.SYMBOL.Map.add sy ty z) up_qv qf.qf_bvars
in
let qvars = varset_of_list qf.qf_bvars in
let binders = E.mk_binders qvars in
Expand All @@ -332,7 +334,7 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
List.map (fun (f : _ Typed.annoted) ->
mk_form up_qv ~toplevel:false f.c f.annot) qf.qf_hyp
in
let in_theory = decl_kind == E.Dtheory in
let in_theory = decl_kind == Dtheory in
let trs =
List.map
(make_trigger ~in_theory name up_qv name_base hyp) qf.qf_triggers in
Expand Down Expand Up @@ -381,17 +383,17 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
(* wrapper of function make_form *)
let make_form name f loc ~decl_kind =
let ff =
make_form Sy.Map.empty name f loc ~decl_kind ~toplevel:true
make_form Symbols.Map.empty name f loc ~decl_kind ~toplevel:true
in
assert (Sy.Map.is_empty (E.free_vars ff Sy.Map.empty));
assert (Symbols.Map.is_empty (E.free_vars ff Symbols.Map.empty));
let ff = E.purify_form ff in
if Ty.Svty.is_empty (E.free_type_vars ff) then ff
else
let id = E.id ff in
E.mk_forall name loc Symbols.Map.empty [] ff id ~toplevel:true ~decl_kind

let mk_assume acc f name loc =
let ff = make_form name f loc ~decl_kind:E.Daxiom in
let ff = make_form name f loc ~decl_kind:Daxiom in
Commands.{st_decl=Assume(name, ff, true) ; st_loc=loc} :: acc


Expand All @@ -418,24 +420,24 @@ let defining_term f =

let mk_function acc f name loc =
let defn = defining_term f in
let defn = make_term Sy.Map.empty "" defn in
let ff = make_form name f loc ~decl_kind:(E.Dfunction defn) in
let defn = make_term Types.SYMBOL.Map.empty "" defn in
let ff = make_form name f loc ~decl_kind:(Dfunction defn) in
Commands.{st_decl=Assume(name, ff, true) ; st_loc=loc} :: acc

let mk_preddef acc f name loc =
let defn = defining_term f in
let defn = make_term Sy.Map.empty "" defn in
let ff = make_form name f loc ~decl_kind: (E.Dpredicate defn) in
let defn = make_term Types.SYMBOL.Map.empty "" defn in
let ff = make_form name f loc ~decl_kind: (Dpredicate defn) in
Commands.{st_decl=PredDef (ff, name) ; st_loc=loc} :: acc

let mk_query acc n f loc sort =
let ff = make_form "" f loc ~decl_kind:E.Dgoal in
let ff = make_form "" f loc ~decl_kind:Dgoal in
Commands.{st_decl=Query(n, ff, sort) ; st_loc=loc} :: acc

let make_rule (({rwt_left = t1; rwt_right = t2; rwt_vars} as r)
: _ Typed.rwt_rule) =
let up_qv =
List.fold_left (fun z (sy, ty) -> Sy.Map.add sy ty z) Sy.Map.empty rwt_vars
List.fold_left (fun z (sy, ty) -> Types.SYMBOL.Map.add sy ty z) Types.SYMBOL.Map.empty rwt_vars
in
let s1 = make_term up_qv "" t1 in
let s2 = make_term up_qv "" t2 in
Expand All @@ -451,8 +453,8 @@ let mk_theory acc l th_name extends _loc =
| TAxiom (loc, name, ax_kd, f) -> loc, name, f, ax_kd
| _ -> assert false
in
let ax_form = make_form ax_name f loc ~decl_kind:E.Dtheory in
let th_elt = {Expr.th_name; axiom_kind; extends; ax_form; ax_name} in
let ax_form = make_form ax_name f loc ~decl_kind:Dtheory in
let th_elt = {th_name; axiom_kind; extends; ax_form; ax_name} in
Commands.{st_decl=ThAssume th_elt ; st_loc=loc} :: acc
)acc l

Expand Down
Loading