Skip to content

Commit 22f29ed

Browse files
bclement-ocpbclement-ocp
committed
Upgrade dolmen version
Use the current development version of Dolmen, as preparation for its next release. This patch does the minimal amount of work needed to make Alt-Ergo support this version of Dolmen ; in particular, it does not exploit Dolmen's new organization of builtins by theories or implement new operators from the SMT-LIB 2.7 standard (except for `ubv_to_int` and `int_to_bv`, which are now new names for `bv2nat` and `int2bv` respectively).
1 parent 5e6f31a commit 22f29ed

File tree

17 files changed

+240
-180
lines changed

17 files changed

+240
-180
lines changed

‎alt-ergo-lib.opam‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,3 +60,18 @@ license: [
6060
"LicenseRef-OCamlpro-Non-Commercial"
6161
"Apache-2.0"
6262
]
63+
64+
pin-depends: [
65+
[
66+
"dolmen.0.11"
67+
"git+https://github.com/Gbury/dolmen.git#a0f1bc66e7256fff1068ac0df525a2d23c1f3ea7"
68+
]
69+
[
70+
"dolmen_loop.0.11"
71+
"git+https://github.com/Gbury/dolmen.git#a0f1bc66e7256fff1068ac0df525a2d23c1f3ea7"
72+
]
73+
[
74+
"dolmen_type.0.11"
75+
"git+https://github.com/Gbury/dolmen.git#a0f1bc66e7256fff1068ac0df525a2d23c1f3ea7"
76+
]
77+
]

‎alt-ergo-lib.opam.template‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,18 @@ license: [
66
"LicenseRef-OCamlpro-Non-Commercial"
77
"Apache-2.0"
88
]
9+
10+
pin-depends: [
11+
[
12+
"dolmen.0.11"
13+
"git+https://github.com/Gbury/dolmen.git#a0f1bc66e7256fff1068ac0df525a2d23c1f3ea7"
14+
]
15+
[
16+
"dolmen_loop.0.11"
17+
"git+https://github.com/Gbury/dolmen.git#a0f1bc66e7256fff1068ac0df525a2d23c1f3ea7"
18+
]
19+
[
20+
"dolmen_type.0.11"
21+
"git+https://github.com/Gbury/dolmen.git#a0f1bc66e7256fff1068ac0df525a2d23c1f3ea7"
22+
]
23+
]

‎nix/default.nix‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,14 @@ import sources.nixpkgs {
55
(_: pkgs: { inherit sources; })
66
(_: pkgs: {
77
ocamlPackages = pkgs.ocaml-ng.ocamlPackages_4_14.overrideScope (self: super: {
8-
pp_loc = pkgs.callPackage ./pp_loc.nix { };
9-
ocplib-simplex = pkgs.callPackage ./ocplib-simplex.nix { };
10-
dolmen = pkgs.callPackage ./dolmen.nix { };
11-
dolmen_type = pkgs.callPackage ./dolmen_type.nix { };
12-
dolmen_loop = pkgs.callPackage ./dolmen_loop.nix { };
13-
landmarks = pkgs.callPackage ./landmarks.nix { };
14-
landmarks-ppx = pkgs.callPackage ./landmarks-ppx.nix { };
15-
zarith_stubs_js = pkgs.callPackage ./zarith_stubs_js.nix { };
8+
pp_loc = self.callPackage ./pp_loc.nix { };
9+
ocplib-simplex = self.callPackage ./ocplib-simplex.nix { };
10+
dolmen = self.callPackage ./dolmen.nix { };
11+
dolmen_type = self.callPackage ./dolmen_type.nix { };
12+
dolmen_loop = self.callPackage ./dolmen_loop.nix { };
13+
landmarks = self.callPackage ./landmarks.nix { };
14+
landmarks-ppx = self.callPackage ./landmarks-ppx.nix { };
15+
zarith_stubs_js = self.callPackage ./zarith_stubs_js.nix { };
1616
});
1717
})
1818
];

‎nix/dolmen.nix‎

Lines changed: 8 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,20 @@
1-
{ sources, lib, ocamlPackages }:
1+
{ sources, lib, buildDunePackage
2+
, menhir, hmap, menhirLib, fmt, uutf, dune-site }:
23

3-
let
4-
dolmen = sources.dolmen;
5-
in
6-
7-
ocamlPackages.buildDunePackage {
4+
buildDunePackage {
85
strictDeps = true;
96
pname = "dolmen";
10-
inherit (dolmen) version;
7+
inherit (sources.dolmen) version;
118

129
minimalOCamlVersion = "4.08";
1310
duneVersion = "3";
1411

15-
src = dolmen;
12+
src = sources.dolmen;
1613

17-
nativeBuildInputs = [ ocamlPackages.menhir ];
18-
propagatedBuildInputs = with ocamlPackages; [ hmap menhirLib fmt ];
14+
nativeBuildInputs = [ menhir ];
15+
propagatedBuildInputs = [ hmap menhirLib fmt uutf dune-site ];
1916

2017
meta = with lib; {
21-
inherit (dolmen) homepage description;
18+
inherit (sources.dolmen) homepage description;
2219
};
2320
}

‎nix/dolmen_loop.nix‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,14 @@
1-
{ sources, lib, ocamlPackages }:
1+
{ sources, lib, buildDunePackage
2+
, gen, zarith, dolmen, dolmen_type }:
23

3-
ocamlPackages.buildDunePackage {
4+
buildDunePackage {
45
pname = "dolmen_loop";
5-
inherit (ocamlPackages.dolmen) version src strictDeps;
6+
inherit (dolmen) version src strictDeps;
67

78
minimalOCamlVersion = "4.08";
89
duneVersion = "3";
910

10-
propagatedBuildInputs = [ ocamlPackages.gen ocamlPackages.dolmen_type ];
11+
propagatedBuildInputs = [ gen dolmen_type zarith ];
1112

12-
meta = ocamlPackages.dolmen.meta;
13+
meta = dolmen.meta;
1314
}

‎nix/sources.json‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
{
22
"dolmen": {
3-
"branch": "v0.10",
3+
"branch": "master",
44
"description": "Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction",
55
"homepage": "",
66
"owner": "Gbury",
77
"repo": "dolmen",
8-
"rev": "c33632daab31fb3bb719031169baa6c984bb860f",
9-
"sha256": "1vvlg72sbwmpnh0kvwkbvnxxgwrdqcy5adqp26n3hpq3mix4sp7d",
8+
"rev": "3c77a22b2aac2eb85aca76f198797d40ca3ec4a3",
9+
"sha256": "0qsl5f0mh4azmqvq99l24cna8brvw00x9703wyd98gm0pbmsc3pm",
1010
"type": "tarball",
11-
"url": "https://github.com/Gbury/dolmen/archive/c33632daab31fb3bb719031169baa6c984bb860f.tar.gz",
11+
"url": "https://github.com/Gbury/dolmen/archive/3c77a22b2aac2eb85aca76f198797d40ca3ec4a3.tar.gz",
1212
"url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
1313
"version": "0.10"
1414
},

‎src/bin/common/parse_command.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,7 @@ let format_parser s =
7878
let format_to_string = function
7979
| Native -> "native"
8080
| Smtlib2 `V2_6 -> "smtlib2-v2.6"
81+
| Smtlib2 `V2_7 -> "smtlib2-v2.7"
8182
| Smtlib2 `Poly -> "psmt2"
8283
| Smtlib2 `Latest -> "smtlib2"
8384
| Why3 -> "why3"

‎src/bin/common/solving_loop.ml‎

Lines changed: 61 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ let add_if_named
138138
~(acc : DStd.Expr.term Util.MS.t)
139139
(stmt : Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt) =
140140
match stmt.contents with
141-
| `Defs [`Term_def ({name = Simple n; _}, id, _, _, t)] ->
141+
| `Defs (_recursive, [`Term_def ({name = Simple n; _}, id, _, _, t)]) ->
142142
begin
143143
match DStd.Expr.Id.get_tag id DStd.Expr.Tags.named with
144144
| None -> acc
@@ -404,7 +404,7 @@ let process_source ?selector_inst ~print_status src =
404404
~interactive_prompt
405405
|> Typer.init
406406
~additional_builtins:Translate.builtins
407-
~extension_builtins:[Typer.Ext.bv2nat]
407+
~extension_builtins:[Dolmen_loop.Typer.Ext.bvconv]
408408
|> Typer_Pipe.init ~type_check
409409
in
410410

@@ -608,7 +608,9 @@ let process_source ?selector_inst ~print_status src =
608608
issue in Dolmen, we can replace the [loc] argument by the [st_loc]
609609
value built in [handle_stmt]. *)
610610
let handle_custom_statement ~loc id args st =
611-
let args = List.map Dolmen_type.Core.Smtlib2.sexpr_as_term args in
611+
let args =
612+
List.map (Dolmen_type.Core.Smtlib2.sexpr_as_term (`Script `Poly)) args
613+
in
612614
let logic_file = State.get State.logic_file st in
613615
let st, terms = Typer.terms st ~input:(`Logic logic_file) ~loc args in
614616
match id, terms.ret with
@@ -638,46 +640,53 @@ let process_source ?selector_inst ~print_status src =
638640
st
639641
in
640642

641-
let handle_get_info ~loc (st : State.t) (name: string) =
642-
let print_std =
643-
fun (type a) (pp :a Fmt.t) (a : a) ->
644-
Printer.print_std "(%s %a)" name pp a
645-
in
646-
let pp_reason_unknown st =
647-
let err () =
648-
recoverable_error ~loc "Invalid (get-info :reason-unknown)"
643+
let handle_get_info ~loc (st : State.t) (info : DStd.Term.t) =
644+
match info with
645+
| { term = Builtin _ | App _ | Binder _ | Match _ | Colon _; _ }
646+
| { term = Symbol { ns = (Var | Sort | Term | Decl | Track | Value _); _ }
647+
; _ }
648+
| { term = Symbol { name = Indexed _ | Qualified _; ns = Attr }; _ } ->
649+
unsupported_opt "get-info"
650+
| { term = Symbol { name = Simple name; ns = Attr }; _ } ->
651+
let print_std =
652+
fun (type a) (pp :a Fmt.t) (a : a) ->
653+
Printer.print_std "(%s %a)" name pp a
649654
in
650-
match State.get partial_model_key st with
651-
| None -> err ()
652-
| Some Model ((module SAT), sat) ->
653-
match SAT.get_unknown_reason sat with
655+
let pp_reason_unknown st =
656+
let err () =
657+
recoverable_error ~loc "Invalid (get-info :reason-unknown)"
658+
in
659+
match State.get partial_model_key st with
654660
| None -> err ()
655-
| Some ur ->
656-
print_std Sat_solver_sig.pp_smt_unknown_reason ur
657-
in
658-
match name with
659-
| ":authors" ->
660-
print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo developers"
661-
| ":error-behavior" ->
662-
let behavior =
663-
if Options.get_exit_on_error () then
664-
"immediate-exit"
665-
else
666-
"continued-execution"
661+
| Some Model ((module SAT), sat) ->
662+
match SAT.get_unknown_reason sat with
663+
| None -> err ()
664+
| Some ur ->
665+
print_std Sat_solver_sig.pp_smt_unknown_reason ur
667666
in
668-
print_std Fmt.string behavior
669-
| ":name" ->
670-
print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo"
671-
| ":reason-unknown" ->
672-
pp_reason_unknown st
673-
| ":version" ->
674-
print_std Fmt.string Version._version
675-
| ":all-statistics" ->
676-
Printer.print_std "%t" Profiling.print_statistics
677-
| ":assertion-stack-levels" ->
678-
unsupported_opt name
679-
| _ ->
680-
unsupported_opt name
667+
match name with
668+
| ":authors" ->
669+
print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo developers"
670+
| ":error-behavior" ->
671+
let behavior =
672+
if Options.get_exit_on_error () then
673+
"immediate-exit"
674+
else
675+
"continued-execution"
676+
in
677+
print_std Fmt.string behavior
678+
| ":name" ->
679+
print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo"
680+
| ":reason-unknown" ->
681+
pp_reason_unknown st
682+
| ":version" ->
683+
print_std Fmt.string Version._version
684+
| ":all-statistics" ->
685+
Printer.print_std "%t" Profiling.print_statistics
686+
| ":assertion-stack-levels" ->
687+
unsupported_opt name
688+
| _ ->
689+
unsupported_opt name
681690
in
682691

683692
(* Fetches the term value in the current model. *)
@@ -921,7 +930,18 @@ let process_source ?selector_inst ~print_status src =
921930
let preludes =
922931
theory_preludes @
923932
List.map (fun path ->
924-
let dir, source = State.split_input (`File path) in
933+
(* Using [`File] sources with preludes is currently broken,
934+
see https://github.com/Gbury/dolmen/issues/248
935+
and https://github.com/OCamlPro/alt-ergo/issues/1330 *)
936+
let dir, source =
937+
let content =
938+
let ch = open_in_bin path in
939+
let s = really_input_string ch (in_channel_length ch) in
940+
close_in ch;
941+
s
942+
in
943+
Filename.dirname path, (`Raw (Filename.basename path, content))
944+
in
925945
State.mk_file dir source) (Options.get_preludes ())
926946
in
927947
let g =

0 commit comments

Comments
 (0)