From ec41af7ac01cef7c30785e6dd704381f31e7c2d3 Mon Sep 17 00:00:00 2001 From: ckeller Date: Thu, 14 Feb 2019 20:09:40 +0100 Subject: V8.7 (#36) Port SMTCoq to Coq-8.7 --- .gitignore | 2 + INSTALL.md | 18 +- src/Misc.v | 9 +- src/SMT_terms.v | 17 +- src/State.v | 5 +- src/Tactics.v | 18 +- src/array/FArray.v | 335 +++--- src/bva/BVList.v | 2 +- src/bva/Bva_checker.v | 4 +- src/cnf/Cnf.v | 2 +- src/configure.sh | 2 + src/lfsc/ast.ml | 96 +- src/lfsc/builtin.ml | 15 +- src/lfsc/converter.ml | 20 +- src/lfsc/lfsc.ml | 8 +- src/lfsc/lfscLexer.mll | 2 +- src/lfsc/lfscParser.mly | 1 - src/lfsc/tosmtcoq.ml | 8 +- src/lia/Lia.v | 2 +- src/lia/lia.ml | 9 +- src/lia/lia.mli | 4 +- src/smtlib2/smtlib2_ast.ml | 124 +- src/smtlib2/smtlib2_genConstr.ml | 2 +- src/smtlib2/smtlib2_genConstr.mli | 1 + src/smtlib2/smtlib2_solver.ml | 2 +- src/spl/Syntactic.v | 4 +- src/trace/coqTerms.ml | 31 +- src/trace/coqTerms.mli | 1 + src/trace/satAtom.mli | 1 - src/trace/smtAtom.ml | 41 +- src/trace/smtBtype.ml | 4 +- src/trace/smtCertif.ml | 2 - src/trace/smtCommands.ml | 236 ++-- src/trace/smtForm.ml | 2 +- src/trace/smtTrace.ml | 4 +- src/verit/verit.ml | 61 +- src/verit/veritSyntax.ml | 28 +- src/versions/native/structures.ml | 17 +- src/versions/native/structures.mli | 14 +- src/versions/standard/Int63/Int63Axioms_standard.v | 31 +- src/versions/standard/Int63/Int63Op_standard.v | 2 +- .../standard/Int63/Int63Properties_standard.v | 131 +- src/versions/standard/Make | 12 +- src/versions/standard/Makefile | 1252 +++++++++++--------- src/versions/standard/Makefile.conf | 103 ++ src/versions/standard/Structures_standard.v | 9 + src/versions/standard/g_smtcoq_standard.ml4 | 11 +- src/versions/standard/structures.ml | 65 +- src/versions/standard/structures.mli | 25 +- src/zchaff/zchaff.ml | 1 - src/zchaff/zchaff.mli | 1 + src/zchaff/zchaffParser.ml | 3 +- unit-tests/Tests_lfsc.v | 2 + unit-tests/Tests_verit.v | 54 +- 54 files changed, 1597 insertions(+), 1259 deletions(-) create mode 100644 src/versions/standard/Makefile.conf diff --git a/.gitignore b/.gitignore index 3199ccb..b5aaccd 100644 --- a/.gitignore +++ b/.gitignore @@ -21,7 +21,9 @@ setup.log .nia.cache # cp targets of src/configure.sh: +src/Make src/Makefile +src/Makefile.conf src/smtcoq_plugin.ml4 src/versions/native/Structures.v src/g_smtcoq.ml4 diff --git a/INSTALL.md b/INSTALL.md index 59c40f7..73084c5 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -15,7 +15,7 @@ changes](#setting-up-environment-for-smtcoq). ## Requirements -You need to have OCaml version >= 4.04.0 and Coq version 8.6 or 8.6.1. +You need to have OCaml version >= 4.04.0 and Coq version 8.7.*. The easiest way to install these two pieces of software is through opam. > **Warning**: The version of Coq that you plan to use must have been compiled @@ -26,7 +26,7 @@ The easiest way to install these two pieces of software is through opam. If you want to use SMTCoq with high performance, you need to use the [version of Coq with native data-structures](https://github.com/smtcoq/native-coq) instead of -Coq-8.6. +Coq-8.7. ### Installation with Coq and OCaml opam packages @@ -63,16 +63,16 @@ opam switch 4.04.0 #### Install Coq -After OCaml is installed, you can install Coq through opam (we recommend 8.6.1). +After OCaml is installed, you can install Coq through opam (we recommend 8.7.2). ```bash -opam install coq.8.6.1 +opam install coq.8.7.2 ``` If you also want to install CoqIDE at the same time you can do ```bash -opam install coq.8.6.1 coqide.8.6.1 +opam install coq.8.7.2 coqide.8.7.2 ``` but you might need to install some extra packages and libraries for your system @@ -90,11 +90,11 @@ make install ``` -### Installation with official Coq 8.6 release +### Installation with official Coq 8.7 release -1. Download the last stable version of Coq 8.6: +1. Download the last stable version of Coq 8.7: ```bash -wget https://coq.inria.fr/distrib/8.6.1/files/coq-8.6.1.tar.gz +wget https://coq.inria.fr/distrib/8.7.2/files/coq-8.7.2.tar.gz ``` and compile it by following the instructions available in the repository (make sure you use OCaml 4.04.0 for that). We recommand @@ -107,7 +107,7 @@ make 2. Set an environment variable COQBIN to the directory where Coq's binaries are; for instance: ```bash -export COQBIN=/home/jdoe/coq-8.6.1/bin/ +export COQBIN=/home/jdoe/coq-8.7.2/bin/ ``` (the final slash is mandatory). diff --git a/src/Misc.v b/src/Misc.v index fe724f4..84feab4 100644 --- a/src/Misc.v +++ b/src/Misc.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import Bool List PArray Int63. +Require Import Bool List PArray Int63 ZArith. Local Open Scope int63_scope. Local Open Scope array_scope. @@ -1038,3 +1038,10 @@ Proof. destruct b; intuition. Qed. Lemma is_true_iff e : e = true <-> is_true e. Proof. now unfold is_true. Qed. + + +(* + Local Variables: + coq-load-path: ((rec "." "SMTCoq")) + End: +*) diff --git a/src/SMT_terms.v b/src/SMT_terms.v index c411c99..c627bc2 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import Bool Int63 PArray BinPos SMT_classes_instances. +Require Import Bool Int63 PArray BinNat BinPos ZArith SMT_classes_instances. Require Import Misc State BVList. (* FArray Equalities DecidableTypeEx. *) Require FArray. Require List . @@ -2452,10 +2452,10 @@ Qed. case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x + k2 interp_t y)%Z; auto. case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x - k2 interp_t y)%Z; auto. case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x * k2 interp_t y)%Z; auto. - case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x =? k2 interp_t y); auto. - case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x >? k2 interp_t y); auto. + case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x =? k2 interp_t y)%Z; auto. + case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x >? k2 interp_t y)%Z; auto. case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) A); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) A) as [k2| ]; simpl; try (exists true; reflexivity); exists (Typ.i_eqb t_i A (k1 interp_t x) (k2 interp_t y)); auto. (*BO_BVand*) @@ -2659,3 +2659,10 @@ Section PredefinedArrays. End PredefinedArrays. *) + + +(* + Local Variables: + coq-load-path: ((rec "." "SMTCoq")) + End: +*) diff --git a/src/State.v b/src/State.v index 3125b06..a3af611 100644 --- a/src/State.v +++ b/src/State.v @@ -10,10 +10,7 @@ (**************************************************************************) -Require Import List. -Require Import Bool. -Require Import Int63. -Require Import PArray. +Require Import List Bool Int63 PArray Omega. (* Require Import AxiomesInt. *) diff --git a/src/Tactics.v b/src/Tactics.v index 68c51dd..106e128 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -11,7 +11,7 @@ Require Import PropToBool BoolToProp. (* Before SMTCoq.State *) -Require Import Int63 List PArray Bool. +Require Import Int63 List PArray Bool ZArith. Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances. Declare ML Module "smtcoq_plugin". @@ -50,15 +50,15 @@ Qed. (* verit considers equality modulo its symmetry, so we have to recover the right direction in the instances of the theorems *) -Definition hidden_eq a b := a =? b. +Definition hidden_eq (a b : Z) := (a =? b)%Z. Ltac all_rew := repeat match goal with - | [ |- context [ ?A =? ?B]] => - change (A =? B) with (hidden_eq A B) + | [ |- context [ (?A =? ?B)%Z]] => + change (A =? B)%Z with (hidden_eq A B) end; repeat match goal with | [ |- context [ hidden_eq ?A ?B] ] => - replace (hidden_eq A B) with (B =? A); + replace (hidden_eq A B) with (B =? A)%Z; [ | now rewrite Z.eqb_sym] end. @@ -112,3 +112,11 @@ Ltac cvc4_no_check := prop2bool; cvc4_bool_no_check; bool2prop. Tactic Notation "smt" constr_list(h) := (prop2bool; try verit_bool h; cvc4_bool; try verit_bool h; bool2prop). Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; bool2prop). + + + +(* + Local Variables: + coq-load-path: ((rec "." "SMTCoq")) + End: +*) diff --git a/src/array/FArray.v b/src/array/FArray.v index 8b1701f..1f8c6b4 100644 --- a/src/array/FArray.v +++ b/src/array/FArray.v @@ -11,7 +11,7 @@ Require Import Bool OrderedType SMT_classes. -Require Import ProofIrrelevance. +Require Import ProofIrrelevance. (* TODO: REMOVE THIS AXIOM *) (** This file formalizes functional arrays with extensionality as specified in SMT-LIB 2. It gives realization to axioms that define the SMT-LIB theory of @@ -474,7 +474,7 @@ Module Raw. (** * [mem] *) - Function mem (k : key) (s : farray) {struct s} : bool := + Fixpoint mem (k : key) (s : farray) {struct s} : bool := match s with | nil => false | (k',_) :: l => @@ -488,30 +488,31 @@ Module Raw. Lemma mem_1 : forall m (Hm:Sort m) x, In x m -> mem x m = true. Proof. intros m Hm x; generalize Hm; clear Hm. - functional induction (mem x m);intros sorted belong1;trivial. - - inversion belong1. inversion H. - - absurd (In x ((k', _x) :: l));try assumption. - apply Sort_Inf_NotIn with _x;auto. - - apply IHb. - elim (sort_inv sorted);auto. - elim (In_inv belong1);auto. - intro abs. - absurd (eq x k'); auto. - symmetry in abs. - apply lt_not_eq in abs; auto. + induction m as [ |[k' _x] l IHb]; intros sorted belong1. + - inversion belong1. inversion H. + - simpl. case_eq (compare x k'); trivial. + + intros _x0 e0. + absurd (In x ((k', _x) :: l));try assumption. + apply Sort_Inf_NotIn with _x;auto. + + intros _x0 e0. + apply IHb. + elim (sort_inv sorted);auto. + elim (In_inv belong1);auto. + intro abs. + absurd (eq x k'); auto. + symmetry in abs. + apply lt_not_eq in abs; auto. Qed. Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m. Proof. intros m Hm x; generalize Hm; clear Hm; unfold In,MapsTo. - functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail). - exists _x; auto. - induction IHb; auto. - exists x0; auto. - inversion_clear sorted; auto. + induction m as [ |[k' _x] l IHb]; intros sorted hyp;try ((inversion hyp);fail). + revert hyp. simpl. case_eq (compare x k'); intros _x0 e0 hyp;try ((inversion hyp);fail). + - exists _x; auto. + - induction IHb; auto. + + exists x0; auto. + + inversion_clear sorted; auto. Qed. Lemma mem_3 : forall m (Hm:Sort m) x, mem x m = false -> ~ In x m. @@ -523,7 +524,7 @@ Module Raw. (** * [find] *) - Function find (k:key) (s: farray) {struct s} : option elt := + Fixpoint find (k:key) (s: farray) {struct s} : option elt := match s with | nil => None | (k',x)::s' => @@ -537,43 +538,40 @@ Module Raw. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m x. unfold MapsTo. - functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto. + induction m as [ |[k' _x] l IHb];simpl; intro e';try now (intro eqfind; inversion eqfind; auto). + case_eq (compare x k'); intros _x0 e0 eqfind; inversion eqfind; auto. Qed. Lemma find_1 : forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e. Proof. intros m Hm x e; generalize Hm; clear Hm; unfold MapsTo. - functional induction (find x m);simpl; subst; try clear H_eq_1. - - inversion 2. - - inversion_clear 2. - clear e1;compute in H0; destruct H0. - apply lt_not_eq in H; auto. now contradict H. - - clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. - (* order. *) - intros. - apply (lt_trans k') in _x; auto. - apply lt_not_eq in _x. - now contradict _x. - - clear e1;inversion_clear 2. - compute in H0; destruct H0; intuition congruence. - generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. - (* order. *) - intros. - apply lt_not_eq in H. now contradict H. - - clear e1; do 2 inversion_clear 1; auto. - compute in H2; destruct H2. - (* order. *) - subst. apply lt_not_eq in _x. now contradict _x. + induction m as [ |[k' _x] l IHb];simpl; subst; try clear H_eq_1. + - inversion 2. + - case_eq (compare x k'); intros _x0 e1; subst. + + inversion_clear 2. + * clear e1;compute in H0; destruct H0. + apply lt_not_eq in H; auto. now contradict H. + * clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. + (* order. *) + intros. + apply (lt_trans k') in _x0; auto. + apply lt_not_eq in _x0. + now contradict _x0. + + clear e1;inversion_clear 2. + * compute in H0; destruct H0; intuition congruence. + * generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. + (* order. *) + intros. + apply lt_not_eq in H. now contradict H. + + clear e1; do 2 inversion_clear 1; auto. + compute in H2; destruct H2. + (* order. *) + subst. apply lt_not_eq in _x0. now contradict _x0. Qed. (** * [add] *) - Function add (k : key) (x : elt) (s : farray) {struct s} : farray := + Fixpoint add (k : key) (x : elt) (s : farray) {struct s} : farray := match s with | nil => (k,x) :: nil | (k',y) :: l => @@ -588,7 +586,7 @@ Module Raw. Proof. intros m x y e; generalize y; clear y. unfold MapsTo. - functional induction (add x e m);simpl;auto. + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1]; simpl; auto. Qed. Lemma add_2 : forall m x y e e', @@ -596,7 +594,7 @@ Module Raw. Proof. intros m x y e e'. generalize y e; clear y e; unfold MapsTo. - functional induction (add x e' m) ;simpl;auto; clear e0. + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e0];simpl;auto; clear e0. subst;auto. intros y' e'' eqky'; inversion_clear 1; destruct H0; simpl in *. @@ -611,7 +609,7 @@ Module Raw. ~ eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. Proof. intros m x y e e'. generalize y e; clear y e; unfold MapsTo. - functional induction (add x e' m);simpl; intros. + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];simpl; intros. apply (In_inv_3 H0); compute; auto. apply (In_inv_3 H0); compute; auto. constructor 2; apply (In_inv_3 H0); compute; auto. @@ -644,7 +642,7 @@ Module Raw. (** * [remove] *) - Function remove (k : key) (s : farray) {struct s} : farray := + Fixpoint remove (k : key) (s : farray) {struct s} : farray := match s with | nil => nil | (k',x) :: l => @@ -658,7 +656,7 @@ Module Raw. Lemma remove_1 : forall m (Hm:Sort m) x y, eq x y -> ~ In y (remove x m). Proof. intros m Hm x y; generalize Hm; clear Hm. - functional induction (remove x m);simpl;intros;subst. + induction m as [ |[k' x0] l IHb]; simpl;intros; [ |case_eq (compare x k'); intros _x e0];simpl;intros;subst. red; inversion 1; inversion H0. @@ -685,7 +683,7 @@ Module Raw. ~ eq x y -> MapsTo y e m -> MapsTo y e (remove x m). Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo. - functional induction (remove x m);subst;auto; + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac @@ -701,7 +699,7 @@ Module Raw. MapsTo y e (remove x m) -> MapsTo y e m. Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo. - functional induction (remove x m);subst;auto. + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto. inversion_clear 1; inversion_clear 1; auto. Qed. @@ -709,7 +707,7 @@ Module Raw. ~ eq x y -> In y m -> In y (remove x m). Proof. intros m Hm x y; generalize Hm; clear Hm. - functional induction (remove x m);subst;auto; + induction m as [ |[k' x0] l IHf]; simpl; [ |case_eq (compare x k'); intros _x e1];subst;auto; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac @@ -719,7 +717,7 @@ Module Raw. inversion H2. unfold eqk in H3. simpl in H3. subst. now contradict H0. apply In_alt. - exists x1. auto. + exists x. auto. apply lt_not_eq in _x. intros. inversion_clear Hm. @@ -750,7 +748,7 @@ Module Raw. apply remove_4_aux; auto. revert H. generalize Hm; clear Hm. - functional induction (remove x m);subst;auto; + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac @@ -761,16 +759,16 @@ Module Raw. exists e. apply InA_cons_tl. auto. intros. - apply lt_not_eq in _x. + apply lt_not_eq in _x0. inversion_clear Hm. apply In_inv in H0. destruct H0. (* destruct (eq_dec k' y). *) - exists x0. + exists _x. apply InA_cons_hd. split; simpl; auto. - specialize (IHf H1 H H0). - inversion IHf. - exists x1. + specialize (IHb H1 H H0). + inversion IHb. + exists x0. apply InA_cons_tl. auto. Qed. @@ -828,7 +826,7 @@ Module Raw. (** * [fold] *) - Function fold (A:Type)(f:key->elt->A->A)(m:farray) (acc:A) {struct m} : A := + Fixpoint fold (A:Type)(f:key->elt->A->A)(m:farray) (acc:A) {struct m} : A := match m with | nil => acc | (k,e)::m' => fold f m' (f k e acc) @@ -837,12 +835,12 @@ Module Raw. Lemma fold_1 : forall m (A:Type)(i:A)(f:key->elt->A->A), fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. Proof. - intros; functional induction (fold f m i); auto. + intros; revert i; induction m as [ |[k e]]; simpl; auto. Qed. (** * [equal] *) - Function equal (cmp:elt->elt->bool)(m m' : farray) {struct m} : bool := + Fixpoint equal (cmp:elt->elt->bool)(m m' : farray) {struct m} : bool := match m, m' with | nil, nil => true | (x,e)::l, (x',e')::l' => @@ -861,121 +859,112 @@ Module Raw. Equivb cmp m m' -> equal cmp m m' = true. Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. - functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; + revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; auto; unfold Equivb; intuition; subst. + - destruct (H0 x') as [_ H3]. + assert (H2: In x' nil). + { + apply H3. exists e'. now constructor. + } + elim H2. intros x Hx. inversion Hx. + - destruct (H0 x) as [H3 _]. + assert (H2: In x nil). + { + apply H3. exists e. now constructor. + } + elim H2. intros x0 Hx0. inversion Hx0. + - case_eq (compare x x'); simpl; subst;auto; unfold Equivb; intuition; subst. - match goal with H: compare _ _ = _ |- _ => clear H end. - assert (cmp_e_e':cmp e e' = true). - apply H1 with x; auto. - rewrite cmp_e_e'; simpl. - apply IHb; auto. - inversion_clear Hm; auto. - inversion_clear Hm'; auto. - unfold Equivb; intuition. - destruct (H0 k). - assert (In k ((x,e) ::l)). - destruct H as (e'', hyp); exists e''; auto. - destruct (In_inv (H2 H4)); auto. - inversion_clear Hm. - elim (Sort_Inf_NotIn H6 H7). - destruct H as (e'', hyp); exists e''; auto. - apply MapsTo_eq with k; auto. - destruct (H0 k). - assert (In k ((x,e') ::l')). - destruct H as (e'', hyp); exists e''; auto. - destruct (In_inv (H3 H4)); auto. - subst. - inversion_clear Hm'. - now elim (Sort_Inf_NotIn H5 H6). - apply H1 with k; destruct (eq_dec x k); auto. - - - destruct (compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y. - destruct (H0 x). - assert (In x ((x',e')::l')). - apply H; auto. - exists e; auto. - destruct (In_inv H3). - (* order. *) - apply lt_not_eq in Hlt; now contradict Hlt. - inversion_clear Hm'. - assert (Inf (x,e) l'). - apply Inf_lt with (x',e'); auto. - elim (Sort_Inf_NotIn H5 H7 H4). - - destruct (H0 x'). - assert (In x' ((x,e)::l)). - apply H2; auto. - exists e'; auto. - destruct (In_inv H3). - (* order. *) - subst; apply lt_not_eq in Hlt; now contradict Hlt. - inversion_clear Hm. - assert (Inf (x',e') l). - apply Inf_lt with (x,e); auto. - elim (Sort_Inf_NotIn H5 H7 H4). - - destruct m; - destruct m';try contradiction. - - clear H1;destruct p as (k,e). - destruct (H0 k). - destruct H1. - exists e; auto. - inversion H1. - - destruct p as (x,e). - destruct (H0 x). - destruct H. - exists e; auto. - inversion H. - - destruct p;destruct p0;contradiction. + + destruct (H0 x). + assert (In x ((x',e')::l')). + apply H2; auto. + exists e; auto. + destruct (In_inv H4). + (* order. *) + clear H. apply lt_not_eq in l0; now contradict l0. + inversion_clear Hm'. + assert (Inf (x,e) l'). + apply Inf_lt with (x',e'); auto. + elim (Sort_Inf_NotIn H6 H8 H5). + + match goal with H: compare _ _ = _ |- _ => clear H end. + assert (cmp_e_e':cmp e e' = true). + apply H1 with x'; auto. + rewrite cmp_e_e'; simpl. + apply IHl; auto. + inversion_clear Hm; auto. + inversion_clear Hm'; auto. + unfold Equivb; intuition. + destruct (H0 k). + assert (In k ((x',e) ::l)). + destruct H as (e'', hyp); exists e''; auto. + destruct (In_inv (H2 H4)); auto. + inversion_clear Hm. + elim (Sort_Inf_NotIn H6 H7). + destruct H as (e'', hyp); exists e''; auto. + apply MapsTo_eq with k; auto. + destruct (H0 k). + assert (In k ((x',e') ::l')). + destruct H as (e'', hyp); exists e''; auto. + destruct (In_inv (H3 H4)); auto. + subst. + inversion_clear Hm'. + now elim (Sort_Inf_NotIn H5 H6). + apply H1 with k; destruct (eq_dec x' k); auto. + + destruct (H0 x'). + assert (In x' ((x,e)::l)). + apply H3; auto. + exists e'; auto. + destruct (In_inv H4). + (* order. *) + clear H; subst; apply lt_not_eq in l0; now contradict l0. + inversion_clear Hm. + assert (Inf (x',e') l). + apply Inf_lt with (x,e); auto. + elim (Sort_Inf_NotIn H6 H8 H5). Qed. Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, equal cmp m m' = true -> Equivb cmp m m'. Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. - functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; + revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; subst;auto; unfold Equivb; intuition; try discriminate; subst; try match goal with H: compare _ _ = _ |- _ => clear H end. - - inversion H0. - - inversion_clear Hm;inversion_clear Hm'. - destruct (andb_prop _ _ H); clear H. - destruct (IHb H1 H3 H6). - destruct (In_inv H0). - exists e'; constructor; split; trivial; apply eq_trans with x; auto. - destruct (H k). - destruct (H9 H8) as (e'',hyp). - exists e''; auto. - - inversion_clear Hm;inversion_clear Hm'. - destruct (andb_prop _ _ H); clear H. - destruct (IHb H1 H3 H6). - destruct (In_inv H0). - exists e; constructor; split; trivial; apply eq_trans with x'; auto. - destruct (H k). - destruct (H10 H8) as (e'',hyp). - exists e''; auto. - - inversion_clear Hm;inversion_clear Hm'. - destruct (andb_prop _ _ H); clear H. - destruct (IHb H2 H4 H7). - inversion_clear H0. - destruct H9; simpl in *; subst. - inversion_clear H1. - destruct H0; simpl in *; subst; auto. - elim (Sort_Inf_NotIn H4 H5). - exists e'0; apply MapsTo_eq with x; auto. + - inversion H0. + - revert H; case_eq (compare x x'); intros _x _ H; try inversion H. + inversion_clear Hm;inversion_clear Hm'. + destruct (andb_prop _ _ H); clear H. + destruct (IHl _ H1 H4 H7). + destruct (In_inv H0). + exists e'; constructor; split; trivial; apply eq_trans with x; auto. + destruct (H k). + destruct (H10 H9) as (e'',hyp). + exists e''; auto. + - revert H; case_eq (compare x x'); intros _x _ H; try inversion H. + inversion_clear Hm;inversion_clear Hm'. + destruct (andb_prop _ _ H); clear H. + destruct (IHl _ H1 H4 H7). + destruct (In_inv H0). + exists e; constructor; split; trivial; apply eq_trans with x'; auto. + destruct (H k). + destruct (H11 H9) as (e'',hyp). + exists e''; auto. + - revert H; case_eq (compare x x'); intros _x _ H; [inversion H| |inversion H]. + inversion_clear Hm;inversion_clear Hm'. + destruct (andb_prop _ _ H); clear H. + destruct (IHl _ H2 H4 H7). + inversion_clear H0. + + destruct H9; simpl in *; subst. + inversion_clear H1. + * destruct H0; simpl in *; subst; auto. + * elim (Sort_Inf_NotIn H4 H5). + exists e'0; apply MapsTo_eq with x'; auto. (* order. *) - inversion_clear H1. - destruct H0; simpl in *; subst; auto. - elim (Sort_Inf_NotIn H2 H3). - exists e0; apply MapsTo_eq with x; auto. - (* order. *) - apply H8 with k; auto. + + inversion_clear H1. + * destruct H0; simpl in *; subst; auto. + elim (Sort_Inf_NotIn H2 H3). + exists e0; apply MapsTo_eq with x'; auto. + (* order. *) + * apply H8 with k; auto. Qed. (** This lemma isn't part of the spec of [Equivb], but is used in [FMapAVL] *) diff --git a/src/bva/BVList.v b/src/bva/BVList.v index 48befd6..a53970b 100644 --- a/src/bva/BVList.v +++ b/src/bva/BVList.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import List Bool NArith Psatz Int63 Nnat. +Require Import List Bool NArith Psatz Int63 Nnat ZArith. Require Import Misc. Import ListNotations. Local Open Scope list_scope. diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 81e0a30..84df9bd 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -12,11 +12,9 @@ (** A small checker for bit-vectors bit-blasting *) -(*Add Rec LoadPath "." as SMTCoq.*) - Require Structures. -Require Import Int63 Int63Properties PArray SMT_classes. +Require Import Int63 Int63Properties PArray SMT_classes ZArith. Require Import Misc State SMT_terms BVList Psatz. Require Import Bool List BoolEq NZParity Nnat. diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v index 73f9f97..ec18c15 100644 --- a/src/cnf/Cnf.v +++ b/src/cnf/Cnf.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import PArray List Bool. +Require Import PArray List Bool ZArith. Require Import Misc State SMT_terms BVList. Import Form. diff --git a/src/configure.sh b/src/configure.sh index 52f21b3..cc2a1ca 100755 --- a/src/configure.sh +++ b/src/configure.sh @@ -21,7 +21,9 @@ if [ $@ -a $@ = -native ]; then cp ${pre}versions/native/smtcoq_plugin_native.ml4 ${pre}smtcoq_plugin.ml4 cp ${pre}versions/native/Structures_native.v ${pre}versions/native/Structures.v else + cp ${pre}versions/standard/Make ${pre}Make cp ${pre}versions/standard/Makefile ${pre}Makefile + cp ${pre}versions/standard/Makefile.conf ${pre}Makefile.conf cp ${pre}versions/standard/g_smtcoq_standard.ml4 ${pre}g_smtcoq.ml4 cp ${pre}versions/standard/smtcoq_plugin_standard.mlpack ${pre}smtcoq_plugin.mlpack cp ${pre}versions/standard/Int63/Int63_standard.v ${pre}versions/standard/Int63/Int63.v diff --git a/src/lfsc/ast.ml b/src/lfsc/ast.ml index 29a4afc..454bc0a 100644 --- a/src/lfsc/ast.ml +++ b/src/lfsc/ast.ml @@ -83,12 +83,12 @@ let value t = (deref t).value let ttype t = deref (deref t).ttype -let rec name c = match value c with +let name c = match value c with | Const {sname=Name n} -> Some n | _ -> None -let rec app_name r = match value r with +let app_name r = match value r with | App ({value=Const{sname=Name n}}, args) -> Some (n, args) | _ -> None @@ -298,36 +298,36 @@ end -let rec holes_address acc t = match t.value with - | Hole i -> (i, t) :: acc - | Type | Kind | Mpz | Mpq | Int _ | Rat _ -> acc - | SideCond (name, args, exp, t) -> acc - | Const _ -> acc - | App (f, args) -> - List.fold_left holes_address acc args - | Pi (s, x) -> holes_address acc x - | Lambda (s, x) -> holes_address acc x - | Ptr t -> holes_address acc t - -let holes_address = holes_address [] - - -let check_holes_integrity where h1 h2 = - List.iter (fun (i, a) -> - List.iter (fun (j, b) -> - if j = i && a != b then - ( - eprintf "\n%s: Hole _%d was at %nx, now at %nx\n@." where i - (address_of a) (address_of b); - (* eprintf "\n%s: Hole _%d has changed\n@." where i; *) - assert false) - ) h2 - ) h1 - -let check_term_integrity where t = - let h = holes_address t in - check_holes_integrity (where ^ "term has != _") h h - +(* let rec holes_address acc t = match t.value with + * | Hole i -> (i, t) :: acc + * | Type | Kind | Mpz | Mpq | Int _ | Rat _ -> acc + * | SideCond (name, args, exp, t) -> acc + * | Const _ -> acc + * | App (f, args) -> + * List.fold_left holes_address acc args + * | Pi (s, x) -> holes_address acc x + * | Lambda (s, x) -> holes_address acc x + * | Ptr t -> holes_address acc t *) + +(* let holes_address = holes_address [] *) + + +(* let check_holes_integrity where h1 h2 = + * List.iter (fun (i, a) -> + * List.iter (fun (j, b) -> + * if j = i && a != b then + * ( + * eprintf "\n%s: Hole _%d was at %nx, now at %nx\n@." where i + * (address_of a) (address_of b); + * (\* eprintf "\n%s: Hole _%d has changed\n@." where i; *\) + * assert false) + * ) h2 + * ) h1 *) + +(* let check_term_integrity where t = + * let h = holes_address t in + * check_holes_integrity (where ^ "term has != _") h h *) + let eq_name s1 s2 = match s1, s2 with @@ -471,10 +471,10 @@ module MSym = Map.Make (struct let empty_subst = MSym.empty -let fresh_alpha = - let cpt = ref 0 in - fun ty -> incr cpt; - mk_symbol ("'a"^string_of_int !cpt) ty +(* let fresh_alpha = + * let cpt = ref 0 in + * fun ty -> incr cpt; + * mk_symbol ("'a"^string_of_int !cpt) ty *) let get_t ?(gen=true) sigma s = @@ -834,20 +834,20 @@ let rec hole_nbs acc t = match value t with | _ -> acc -let rec min_hole acc t = match value t with - | Hole nb -> - (match acc with Some n when nb < n -> Some nb | None -> Some nb | _ -> acc) - | App (f, args) -> List.fold_left min_hole (min_hole acc f) args - | Pi (s, x) | Lambda (s, x) -> min_hole acc x - | Ptr t -> min_hole acc t - | _ -> acc +(* let rec min_hole acc t = match value t with + * | Hole nb -> + * (match acc with Some n when nb < n -> Some nb | None -> Some nb | _ -> acc) + * | App (f, args) -> List.fold_left min_hole (min_hole acc f) args + * | Pi (s, x) | Lambda (s, x) -> min_hole acc x + * | Ptr t -> min_hole acc t + * | _ -> acc *) -let compare_int_opt m1 m2 = match m1, m2 with - | None, None -> 0 - | Some _, None -> -1 - | None, Some _ -> 1 - | Some n1, Some n2 -> compare n1 n2 +(* let compare_int_opt m1 m2 = match m1, m2 with + * | None, None -> 0 + * | Some _, None -> -1 + * | None, Some _ -> 1 + * | Some n1, Some n2 -> compare n1 n2 *) let compare_sc_checks (_, args1, exp1) (_, args2, exp2) = diff --git a/src/lfsc/builtin.ml b/src/lfsc/builtin.ml index 7d0151b..86899df 100644 --- a/src/lfsc/builtin.ml +++ b/src/lfsc/builtin.ml @@ -11,7 +11,6 @@ open Ast -open Format module H = struct @@ -90,7 +89,7 @@ module H = struct let var_bv = Hstring.make "var_bv" - let a_var_bv = Hstring.make "a_var_bv" + (* let a_var_bv = Hstring.make "a_var_bv" *) let a_bv = Hstring.make "a_bv" let a_int = Hstring.make "a_int" @@ -98,7 +97,7 @@ module H = struct let bitof = Hstring.make "bitof" let bblast_term = Hstring.make "bblast_term" - let eq = Hstring.make "=" + (* let eq = Hstring.make "=" *) let bvand = Hstring.make "bvand" let bvor = Hstring.make "bvor" let bvxor = Hstring.make "bvxor" @@ -163,7 +162,7 @@ module H = struct let tfalse = Hstring.make "false" let a_var_bv = Hstring.make "a_var_bv" let eq = Hstring.make "=" - let trust_f = Hstring.make "trust_f" + (* let trust_f = Hstring.make "trust_f" *) let ext = Hstring.make "ext" let decl_atom = Hstring.make "decl_atom" let asf = Hstring.make "asf" @@ -179,7 +178,7 @@ module H = struct let or_elim_1 = Hstring.make "or_elim_1" let or_elim_2 = Hstring.make "or_elim_2" let iff_elim_1 = Hstring.make "iff_elim_1" - let iff_elim_2 = Hstring.make "iff_elim_2" + (* let iff_elim_2 = Hstring.make "iff_elim_2" *) let impl_elim = Hstring.make "impl_elim" let not_and_elim = Hstring.make "not_and_elim" let xor_elim_1 = Hstring.make "xor_elim_1" @@ -232,8 +231,8 @@ module H = struct let bv_bbl_bvneg = Hstring.make "bv_bbl_bvneg" let bv_bbl_bvadd = Hstring.make "bv_bbl_bvadd" let bv_bbl_bvmul = Hstring.make "bv_bbl_bvmul" - let bv_bbl_bvult = Hstring.make "bv_bbl_bvult" - let bv_bbl_bvslt = Hstring.make "bv_bbl_bvslt" + (* let bv_bbl_bvult = Hstring.make "bv_bbl_bvult" *) + (* let bv_bbl_bvslt = Hstring.make "bv_bbl_bvslt" *) let bv_bbl_concat = Hstring.make "bv_bbl_concat" let bv_bbl_extract = Hstring.make "bv_bbl_extract" let bv_bbl_zero_extend = Hstring.make "bv_bbl_zero_extend" @@ -1172,7 +1171,7 @@ let rec bblast_bvult x y n = | _ -> failwith "bblast_bvult" -let rec bblast_bvslt x y n = +let bblast_bvslt x y n = match value x with | App (ff, [xi; x']) when term_equal ff bbltc_s -> (match value y with diff --git a/src/lfsc/converter.ml b/src/lfsc/converter.ml index d586e37..2dfbed3 100644 --- a/src/lfsc/converter.ml +++ b/src/lfsc/converter.ml @@ -874,19 +874,19 @@ module Make (T : Translator_sig.S) = struct | _ -> raise Not_found - let rec reso_of_QR acc qr = match app_name qr with - | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r -> - reso_of_QR (reso_of_QR acc u1) u2 - | _ -> clause_qr qr :: acc + (* let rec reso_of_QR acc qr = match app_name qr with + * | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r -> + * reso_of_QR (reso_of_QR acc u1) u2 + * | _ -> clause_qr qr :: acc *) (** Returns clauses used in a linear resolution chain *) - let reso_of_QR qr = reso_of_QR [] qr |> List.rev + (* let reso_of_QR qr = reso_of_QR [] qr |> List.rev *) - let rec reso_of_QR qr = match app_name qr with - | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r -> - reso_of_QR u1 @ reso_of_QR u2 - | _ -> [clause_qr qr] + (* let rec reso_of_QR qr = match app_name qr with + * | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r -> + * reso_of_QR u1 @ reso_of_QR u2 + * | _ -> [clause_qr qr] *) let rec reso_of_QR depth acc qr = match app_name qr with | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r -> @@ -963,7 +963,7 @@ module Make (T : Translator_sig.S) = struct | None -> assert false - let rec bb_lem env p = + let bb_lem env p = let env, p = bb_trim_intro_unit env p in let id = bb_lem_res None p in { env with clauses = id :: env.clauses } diff --git a/src/lfsc/lfsc.ml b/src/lfsc/lfsc.ml index 0f9fd8d..a11139d 100644 --- a/src/lfsc/lfsc.ml +++ b/src/lfsc/lfsc.ml @@ -11,13 +11,9 @@ open Format -open Entries -open Declare -open Decl_kinds open SmtMisc open CoqTerms -open SmtForm open SmtCertif open SmtTrace open SmtAtom @@ -163,8 +159,8 @@ let checker_debug fsmt fproof = let theorem name fsmt fproof = SmtCommands.theorem name (import_all fsmt fproof) -let checker fsmt fproof = - SmtCommands.checker (import_all fsmt fproof) +(* let checker fsmt fproof = + * SmtCommands.checker (import_all fsmt fproof) *) (* Same but print runtime *) let checker fsmt fproof = diff --git a/src/lfsc/lfscLexer.mll b/src/lfsc/lfscLexer.mll index 3e8d5f9..242df00 100644 --- a/src/lfsc/lfscLexer.mll +++ b/src/lfsc/lfscLexer.mll @@ -245,7 +245,7 @@ and scan_string buf start = parse { let ofs = lexbuf.lex_start_pos in let len = lexbuf.lex_curr_pos - ofs in - Quoted_string_buffer.add_substring buf lexbuf.lex_buffer ofs len; + Quoted_string_buffer.add_substring buf (Bytes.to_string lexbuf.lex_buffer) ofs len; Quoted_string_buffer.add_lexeme buf lexbuf; scan_string buf start lexbuf } diff --git a/src/lfsc/lfscParser.mly b/src/lfsc/lfscParser.mly index 26de090..3d6749f 100644 --- a/src/lfsc/lfscParser.mly +++ b/src/lfsc/lfscParser.mly @@ -16,7 +16,6 @@ open Ast open Lexing open Format -open Builtin let parse_failure what = let pos = Parsing.symbol_start_pos () in diff --git a/src/lfsc/tosmtcoq.ml b/src/lfsc/tosmtcoq.ml index 0395244..f520ba7 100644 --- a/src/lfsc/tosmtcoq.ml +++ b/src/lfsc/tosmtcoq.ml @@ -12,8 +12,6 @@ open SmtAtom open SmtForm -open SmtCertif -open SmtTrace open VeritSyntax open Ast open Builtin @@ -42,7 +40,7 @@ module HT = struct let add h k v = h := M.add k v !h let find h k = M.find k !h let clear h = h := M.empty - let iter f h = M.iter f !h + (* let iter f h = M.iter f !h *) end @@ -499,8 +497,8 @@ let register_clause_id cl id = Hashtbl.add ids_clauses id cl -let register_termclause_id t id = - register_clause_id (to_clause t) id +(* let register_termclause_id t id = + * register_clause_id (to_clause t) id *) let new_clause_id ?(reuse=true) cl = diff --git a/src/lia/Lia.v b/src/lia/Lia.v index cafac1b..8c5a597 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import Bool List Int63 PArray. +Require Import Bool List Int63 PArray ZArith. Require Import Misc State SMT_terms Euf. Require Import RingMicromega ZMicromega Tauto Psatz. diff --git a/src/lia/lia.ml b/src/lia/lia.ml index adeed4e..d8ed560 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -11,11 +11,6 @@ (*** Linking SMT Terms to Micromega Terms ***) -open Term -open Coqlib -open Declare -open Decl_kinds -open Entries open Util open Structures.Micromega_plugin_Micromega open Structures.Micromega_plugin_Coq_micromega @@ -114,7 +109,7 @@ let smt_binop_to_micromega_formula tbl op ha hb = let rhs = smt_Atom_to_micromega_pExpr tbl hb in {flhs = lhs; fop = op; frhs = rhs } -let rec smt_Atom_to_micromega_formula tbl ha = +let smt_Atom_to_micromega_formula tbl ha = match Atom.atom ha with | Abop (op,ha,hb) -> smt_binop_to_micromega_formula tbl op ha hb | _ -> Structures.error @@ -122,7 +117,7 @@ let rec smt_Atom_to_micromega_formula tbl ha = (* specialized fold *) -let default_constr = mkInt 0 +let default_constr = Structures.econstr_of_constr (mkInt 0) let default_tag = Structures.Micromega_plugin_Mutils.Tag.from 0 (* morphism for general formulas *) diff --git a/src/lia/lia.mli b/src/lia/lia.mli index 93361f2..9d4ee6b 100644 --- a/src/lia/lia.mli +++ b/src/lia/lia.mli @@ -12,7 +12,7 @@ val pos_of_int : int -> Structures.Micromega_plugin_Micromega.positive val z_of_int : int -> Structures.Micromega_plugin_Micromega.z -type my_tbl = { tbl : (SmtAtom.hatom, int) Hashtbl.t; mutable count : int; } +type my_tbl val get_atom_var : my_tbl -> SmtAtom.hatom -> int val create_tbl : int -> my_tbl val smt_Atom_to_micromega_pos : @@ -36,8 +36,6 @@ val smt_Atom_to_micromega_formula : SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.z Structures.Micromega_plugin_Micromega.formula -val default_constr : Term.constr -val default_tag : Structures.Micromega_plugin_Mutils.Tag.t val binop_array : ('a -> 'b -> 'c) -> 'a -> ('c -> 'c -> 'c) -> 'c -> 'b array -> 'c val smt_Form_to_coq_micromega_formula : diff --git a/src/smtlib2/smtlib2_ast.ml b/src/smtlib2/smtlib2_ast.ml index 7317b60..65dc3e3 100644 --- a/src/smtlib2/smtlib2_ast.ml +++ b/src/smtlib2/smtlib2_ast.ml @@ -16,8 +16,6 @@ (**************************************************************************) -open Smtlib2_util - type loc = Lexing.position * Lexing.position type specconstant = @@ -191,65 +189,65 @@ let loc_of e = loc_commands e;; -let print_specconstant fmt = function - | SpecConstsDec (_, s) - | SpecConstNum (_, s) - | SpecConstString (_, s) - | SpecConstsHex (_, s) - | SpecConstsBinary (_, s) -> Format.pp_print_string fmt s - - -let print_symbol fmt = function - | Symbol (_, s) - | SymbolWithOr (_, s) -> Format.pp_print_string fmt s - - -let print_identifier fmt = function - | IdSymbol (_, s) -> print_symbol fmt s - | IdUnderscoreSymNum (_, s, (_, l)) -> - Format.fprintf fmt "(_ %a" print_symbol s; - List.iter (Format.fprintf fmt " %s") l; - Format.fprintf fmt ")" - -let rec print_sort fmt = function - | SortIdentifier (_, i) -> print_identifier fmt i - | SortIdSortMulti (_, i, (_, ls)) -> - Format.fprintf fmt "(%a" print_identifier i; - List.iter (Format.fprintf fmt " %a" print_sort) ls; - Format.fprintf fmt ")" - -let print_qualidentifier fmt = function - | QualIdentifierId (_, i) -> print_identifier fmt i - | QualIdentifierAs (_, i, s) -> - Format.fprintf fmt "(%a as %a)" - print_identifier i print_sort s - -let print_sortedvar fmt = function - | SortedVarSymSort (_, v, s) -> - Format.fprintf fmt "(%a %a)" print_symbol v print_sort s - -let rec print_varbinding fmt = function - | VarBindingSymTerm (_, s, t) -> - Format.fprintf fmt "(%a %a)" print_symbol s print_term t - -and print_term fmt = function - | TermSpecConst (_, c) -> print_specconstant fmt c - | TermQualIdentifier (_, i) -> print_qualidentifier fmt i - | TermQualIdTerm (_, i, (_, tl)) -> - Format.fprintf fmt "(%a" print_qualidentifier i; - List.iter (Format.fprintf fmt " %a" print_term) tl; - Format.fprintf fmt ")" - | TermLetTerm (_, (_, vb), t) -> - Format.fprintf fmt "(let ("; - List.iter (Format.fprintf fmt " %a" print_varbinding) vb; - Format.fprintf fmt ") %a)" print_term t - | TermForAllTerm (_, (_, sv), t) -> - Format.fprintf fmt "(forall ("; - List.iter (Format.fprintf fmt " %a" print_sortedvar) sv; - Format.fprintf fmt ") %a)" print_term t - | TermExistsTerm (_, (_, sv), t) -> - Format.fprintf fmt "(exists ("; - List.iter (Format.fprintf fmt " %a" print_sortedvar) sv; - Format.fprintf fmt ") %a)" print_term t - | TermExclimationPt (_, t, _) -> print_term fmt t +(* let print_specconstant fmt = function + * | SpecConstsDec (_, s) + * | SpecConstNum (_, s) + * | SpecConstString (_, s) + * | SpecConstsHex (_, s) + * | SpecConstsBinary (_, s) -> Format.pp_print_string fmt s *) + + +(* let print_symbol fmt = function + * | Symbol (_, s) + * | SymbolWithOr (_, s) -> Format.pp_print_string fmt s *) + + +(* let print_identifier fmt = function + * | IdSymbol (_, s) -> print_symbol fmt s + * | IdUnderscoreSymNum (_, s, (_, l)) -> + * Format.fprintf fmt "(_ %a" print_symbol s; + * List.iter (Format.fprintf fmt " %s") l; + * Format.fprintf fmt ")" *) + +(* let rec print_sort fmt = function + * | SortIdentifier (_, i) -> print_identifier fmt i + * | SortIdSortMulti (_, i, (_, ls)) -> + * Format.fprintf fmt "(%a" print_identifier i; + * List.iter (Format.fprintf fmt " %a" print_sort) ls; + * Format.fprintf fmt ")" *) + +(* let print_qualidentifier fmt = function + * | QualIdentifierId (_, i) -> print_identifier fmt i + * | QualIdentifierAs (_, i, s) -> + * Format.fprintf fmt "(%a as %a)" + * print_identifier i print_sort s *) + +(* let print_sortedvar fmt = function + * | SortedVarSymSort (_, v, s) -> + * Format.fprintf fmt "(%a %a)" print_symbol v print_sort s *) + +(* let rec print_varbinding fmt = function + * | VarBindingSymTerm (_, s, t) -> + * Format.fprintf fmt "(%a %a)" print_symbol s print_term t *) + +(* and print_term fmt = function + * | TermSpecConst (_, c) -> print_specconstant fmt c + * | TermQualIdentifier (_, i) -> print_qualidentifier fmt i + * | TermQualIdTerm (_, i, (_, tl)) -> + * Format.fprintf fmt "(%a" print_qualidentifier i; + * List.iter (Format.fprintf fmt " %a" print_term) tl; + * Format.fprintf fmt ")" + * | TermLetTerm (_, (_, vb), t) -> + * Format.fprintf fmt "(let ("; + * List.iter (Format.fprintf fmt " %a" print_varbinding) vb; + * Format.fprintf fmt ") %a)" print_term t + * | TermForAllTerm (_, (_, sv), t) -> + * Format.fprintf fmt "(forall ("; + * List.iter (Format.fprintf fmt " %a" print_sortedvar) sv; + * Format.fprintf fmt ") %a)" print_term t + * | TermExistsTerm (_, (_, sv), t) -> + * Format.fprintf fmt "(exists ("; + * List.iter (Format.fprintf fmt " %a" print_sortedvar) sv; + * Format.fprintf fmt ") %a)" print_term t + * | TermExclimationPt (_, t, _) -> print_term fmt t *) diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index 692294d..203077b 100644 --- a/src/smtlib2/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -50,7 +50,7 @@ let string_type s = let sort_of_string s = string_type s -let sort_of_symbol s = sort_of_string (string_of_symbol s) +(* let sort_of_symbol s = sort_of_string (string_of_symbol s) *) let rec bigint_binary_size acc i size = diff --git a/src/smtlib2/smtlib2_genConstr.mli b/src/smtlib2/smtlib2_genConstr.mli index 40f73c7..dabd99b 100644 --- a/src/smtlib2/smtlib2_genConstr.mli +++ b/src/smtlib2/smtlib2_genConstr.mli @@ -10,6 +10,7 @@ (**************************************************************************) +val pp_symbol : Smtlib2_ast.symbol -> string val parse_smt2bv : string -> bool list val bigint_bv : Big_int.big_int -> int -> string val import_smtlib2 : diff --git a/src/smtlib2/smtlib2_solver.ml b/src/smtlib2/smtlib2_solver.ml index 3ee8229..8ae7202 100644 --- a/src/smtlib2/smtlib2_solver.ml +++ b/src/smtlib2/smtlib2_solver.ml @@ -82,7 +82,7 @@ let read_success s = | r -> error s r -let no_response _ = () +(* let no_response _ = () *) let read_check_result s = diff --git a/src/spl/Syntactic.v b/src/spl/Syntactic.v index cc34522..6d66a43 100644 --- a/src/spl/Syntactic.v +++ b/src/spl/Syntactic.v @@ -11,7 +11,7 @@ (*** Spl -- a small checker for simplifications ***) -Require Import List PArray Bool Int63 ZMicromega. +Require Import List PArray Bool Int63 ZMicromega ZArith. Require Import Misc State SMT_terms BVList. Require Lia. @@ -214,7 +214,7 @@ Section CheckAtom. end. (* TODO : move this *) - Lemma Zge_is_ge_bool : forall x y, (x >= y) <-> (Zge_bool x y = true). + Lemma Zge_is_ge_bool : forall x y, (x >= y)%Z <-> (Zge_bool x y = true). Proof. intros x y;assert (W:=Zge_cases x y);destruct (Zge_bool x y). split;auto. diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 76f213b..895d217 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -12,8 +12,9 @@ open Coqlib -let gen_constant modules constant = - lazy (gen_constant_in_modules "SMT" modules constant) + +let gen_constant = Structures.gen_constant + (* Int63 *) let cint = Structures.cint @@ -65,7 +66,7 @@ let cleb = gen_constant z_modules "leb" let cgeb = gen_constant z_modules "geb" let cgtb = gen_constant z_modules "gtb" let ceqbZ = gen_constant z_modules "eqb" -let cZeqbsym = gen_constant z_modules "eqb_sym" +(* let cZeqbsym = gen_constant z_modules "eqb_sym" *) (* Booleans *) let bool_modules = [["Coq";"Bool";"Bool"]] @@ -100,12 +101,12 @@ let cprod = gen_constant init_modules "prod" (* Dependent pairs *) let csigT = gen_constant init_modules "sigT" -let cprojT1 = gen_constant init_modules "projT1" -let cprojT2 = gen_constant init_modules "projT2" -let cprojT3 = gen_constant init_modules "projT3" +(* let cprojT1 = gen_constant init_modules "projT1" *) +(* let cprojT2 = gen_constant init_modules "projT2" *) +(* let cprojT3 = gen_constant init_modules "projT3" *) -let csigT2 = gen_constant init_modules "sigT2" -let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2" +(* let csigT2 = gen_constant init_modules "sigT2" *) +(* let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2" *) (* Logical Operators *) let cnot = gen_constant init_modules "not" @@ -118,7 +119,7 @@ let cand = gen_constant init_modules "and" let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]] let cbitvector = gen_constant bv_modules "bitvector" let cof_bits = gen_constant bv_modules "of_bits" -let c_of_bits = gen_constant bv_modules "_of_bits" +(* let c_of_bits = gen_constant bv_modules "_of_bits" *) let cbitOf = gen_constant bv_modules "bitOf" let cbv_eq = gen_constant bv_modules "bv_eq" let cbv_not = gen_constant bv_modules "bv_not" @@ -147,8 +148,8 @@ let cdiff = gen_constant array_modules "diff" let cequalarray = gen_constant array_modules "FArray.equal" (* OrderedType *) -let cOrderedTypeCompare = - gen_constant [["Coq";"Structures";"OrderedType"]] "Compare" +(* let cOrderedTypeCompare = + * gen_constant [["Coq";"Structures";"OrderedType"]] "Compare" *) (* SMT_terms *) let smt_modules = [ ["SMTCoq";"Misc"]; @@ -172,7 +173,7 @@ let cTBV = gen_constant smt_modules "TBV" let cTFArray = gen_constant smt_modules "TFArray" let cTindex = gen_constant smt_modules "Tindex" -let ct_i = gen_constant smt_modules "t_i" +(* let ct_i = gen_constant smt_modules "t_i" *) let cinterp_t = gen_constant smt_modules "Typ.interp" let cdec_interp = gen_constant smt_modules "dec_interp" let cord_interp = gen_constant smt_modules "ord_interp" @@ -180,14 +181,14 @@ let ccomp_interp = gen_constant smt_modules "comp_interp" let cinh_interp = gen_constant smt_modules "inh_interp" let cinterp_eqb = gen_constant smt_modules "i_eqb" -let cinterp_eqb_eqb = gen_constant smt_modules "i_eqb_eqb" +(* let cinterp_eqb_eqb = gen_constant smt_modules "i_eqb_eqb" *) let classes_modules = [["SMTCoq";"classes";"SMT_classes"]; ["SMTCoq";"classes";"SMT_classes_instances"]] let ctyp_compdec = gen_constant classes_modules "typ_compdec" let cTyp_compdec = gen_constant classes_modules "Typ_compdec" -let ctyp_compdec_from = gen_constant classes_modules "typ_compdec_from" +(* let ctyp_compdec_from = gen_constant classes_modules "typ_compdec_from" *) let cunit_typ_compdec = gen_constant classes_modules "unit_typ_compdec" let cte_carrier = gen_constant classes_modules "te_carrier" let cte_compdec = gen_constant classes_modules "te_compdec" @@ -340,7 +341,7 @@ let mkN = function | i -> SmtMisc.mklApp cNpos [|mkPositive i|] (* Compute a Boolean *) -let rec mkBool = function +let mkBool = function | true -> Lazy.force ctrue | false -> Lazy.force cfalse diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index b21bef8..9aeddac 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -259,4 +259,5 @@ val mk_bool : Term.constr -> bool val mk_bool_list : Term.constr -> bool list val mk_nat : Term.constr -> int val mk_N : Term.constr -> int +val mk_Z : Term.constr -> int val mk_bvsize : Term.constr -> int diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli index b5fe759..4ecfae3 100644 --- a/src/trace/satAtom.mli +++ b/src/trace/satAtom.mli @@ -21,7 +21,6 @@ module Atom : sig val to_smt : Format.formatter -> t -> unit val logic : t -> SmtMisc.logic - val is_bool_type : t -> bool type reify_tbl = { mutable count : int; tbl : (Term.constr, t) Hashtbl.t; diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index fd9f2bd..330884b 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -12,9 +12,6 @@ open SmtMisc open CoqTerms -open Entries -open Declare -open Decl_kinds open SmtBtype @@ -229,8 +226,8 @@ module Op = | BO_diffarray (ti, te) -> (TFArray (ti, te), TFArray (ti, te)) - let interp_ieq t_i t = - mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] + (* let interp_ieq t_i t = + * mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] *) (* let veval_t te = let env = Global.env () in @@ -246,30 +243,30 @@ module Op = let interp_eqarray t_i ti te = mklApp cequalarray - SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; - SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; - SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; - SmtBtype.inh_interp t_i te |] + [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; + SmtBtype.inh_interp t_i te |] let interp_select t_i ti te = mklApp cselect - SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; - SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; - SmtBtype.inh_interp t_i te|] + [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.inh_interp t_i te|] let interp_diff t_i ti te = mklApp cdiff - SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; - SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; - SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; - SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |] + [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; + SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |] let interp_store t_i ti te = mklApp cstore - SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; - SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; - SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |] + [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |] let interp_eq t_i = function @@ -1022,7 +1019,7 @@ module Atom = else CCunknown_deps (gobble_of_coq_cst cc) with Not_found -> CCunknown in - let rec mk_hatom h = + let rec mk_hatom (h : Term.constr) = let c, args = Term.decompose_app h in match get_cst c with | CCxH -> mk_cop CCxH args @@ -1064,9 +1061,9 @@ module Atom = | CCselect -> mk_bop_select args | CCdiff -> mk_bop_diff args | CCstore -> mk_top_store args - | CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h) + | CCunknown -> mk_unknown c args (Structures.retyping_get_type_of env sigma h) | CCunknown_deps gobble -> - mk_unknown_deps c args (Retyping.get_type_of env sigma h) gobble + mk_unknown_deps c args (Structures.retyping_get_type_of env sigma h) gobble and mk_cop op args = match op, args with diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index 0ebb893..119c046 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -119,8 +119,8 @@ let to_list reify = let make_t_i rt = interp_tbl rt -let interp_t t_i t = - mklApp cinterp_t [|t_i ; to_coq t|] +(* let interp_t t_i t = + * mklApp cinterp_t [|t_i ; to_coq t|] *) let dec_interp t_i t = mklApp cdec_interp [|t_i ; to_coq t|] diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml index b1468e4..6ce6997 100644 --- a/src/trace/smtCertif.ml +++ b/src/trace/smtCertif.ml @@ -10,8 +10,6 @@ (**************************************************************************) -open SmtForm - type used = int type clause_id = int diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 43365ef..1a990f1 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -34,10 +34,10 @@ let cchecker_b = gen_constant euf_checker_modules "checker_b" let cchecker_eq_correct = gen_constant euf_checker_modules "checker_eq_correct" let cchecker_eq = gen_constant euf_checker_modules "checker_eq" -let csetup_checker_step_debug = - gen_constant euf_checker_modules "setup_checker_step_debug" -let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug" -let cstep = gen_constant euf_checker_modules "step" +(* let csetup_checker_step_debug = + * gen_constant euf_checker_modules "setup_checker_step_debug" *) +(* let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug" *) +(* let cstep = gen_constant euf_checker_modules "step" *) let cchecker_debug = gen_constant euf_checker_modules "checker_debug" let cname_step = gen_constant euf_checker_modules "name_step" @@ -315,7 +315,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) = Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in - let res = Vnorm.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in + let res = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in Format.eprintf " = %s\n : bool@." (if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then "true" else "false") @@ -389,7 +389,7 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = mklApp cchecker_debug [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in - let res = Vnorm.cbv_vm (Global.env ()) tm + let res = Structures.cbv_vm (Global.env ()) tm (mklApp coption [|mklApp cprod [|Lazy.force cnat; Lazy.force cname_step|]|]) in @@ -453,117 +453,117 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = -let rec of_coq_list cl = - match Term.decompose_app cl with - | c, _ when Term.eq_constr c (Lazy.force cnil) -> [] - | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) -> - x :: of_coq_list cr - | _ -> assert false - - -let checker_debug_step t_i t_func t_atom t_form root used_root trace - (rt, ro, ra, rf, roots, max_id, confl) = - - let t_i' = make_t_i rt in - let ce5 = Structures.mkUConst t_i' in - let ct_i = Term.mkConst (declare_constant t_i - (DefinitionEntry ce5, IsDefinition Definition)) in - - let t_func' = make_t_func ro ct_i in - let ce6 = Structures.mkUConst t_func' in - let ct_func = - Term.mkConst (declare_constant t_func - (DefinitionEntry ce6, IsDefinition Definition)) in - - let t_atom' = Atom.interp_tbl ra in - let ce1 = Structures.mkUConst t_atom' in - let ct_atom = - Term.mkConst (declare_constant t_atom - (DefinitionEntry ce1, IsDefinition Definition)) in - - let t_form' = snd (Form.interp_tbl rf) in - let ce2 = Structures.mkUConst t_form' in - let ct_form = - Term.mkConst (declare_constant t_form - (DefinitionEntry ce2, IsDefinition Definition)) in - - let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) - (interp_conseq_uf ct_i) - (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in - List.iter (fun (v,ty) -> - let _ = Structures.declare_new_variable v ty in - print_assm ty - ) cuts; - - let used_roots = compute_roots roots last_root in - let croots = - let res = Array.make (List.length roots + 1) (mkInt 0) in - let i = ref 0 in - List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - Structures.mkArray (Lazy.force cint, res) in - let cused_roots = - let l = List.length used_roots in - let res = Array.make (l + 1) (mkInt 0) in - let i = ref (l-1) in - List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; - Structures.mkArray (Lazy.force cint, res)|] in - let ce3 = Structures.mkUConst croots in - let _ = declare_constant root - (DefinitionEntry ce3, IsDefinition Definition) in - let ce3' = Structures.mkUConst cused_roots in - let _ = declare_constant used_root - (DefinitionEntry ce3', IsDefinition Definition) in - - let certif = - mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1); - tres;mkInt (get_pos confl)|] in - let ce4 = Structures.mkUConst certif in - let _ = declare_constant trace - (DefinitionEntry ce4, IsDefinition Definition) in - - let setup = - mklApp csetup_checker_step_debug - [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in - - let setup = Vnorm.cbv_vm (Global.env ()) setup - (mklApp cprod - [|Lazy.force cState_S_t; - mklApp clist [|mklApp cstep - [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in - - let s, steps = match Term.decompose_app setup with - | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) -> - s, of_coq_list csteps - | _ -> assert false - in - - let cpt = ref (List.length roots) in - let debug_step s step = - incr cpt; - Format.eprintf "%d@." !cpt; - let tm = - mklApp cchecker_step_debug - [| ct_i; ct_func; ct_atom; ct_form; s; step |] in - - let res = - Vnorm.cbv_vm (Global.env ()) tm - (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in - - match Term.decompose_app res with - | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) -> - if not (mk_bool cbad) then s - else Structures.error ("Step number " ^ string_of_int !cpt ^ - " (" ^ string_coq_constr - (fst (Term.decompose_app step)) ^ ")" ^ - " of the certificate likely failed." ) - | _ -> assert false - in - - List.fold_left debug_step s steps |> ignore; - - Structures.error ("Debug checker is only meant to be used for certificates \ - that fail to be checked by SMTCoq.") +(* let rec of_coq_list cl = + * match Term.decompose_app cl with + * | c, _ when Term.eq_constr c (Lazy.force cnil) -> [] + * | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) -> + * x :: of_coq_list cr + * | _ -> assert false *) + + +(* let checker_debug_step t_i t_func t_atom t_form root used_root trace + * (rt, ro, ra, rf, roots, max_id, confl) = + * + * let t_i' = make_t_i rt in + * let ce5 = Structures.mkUConst t_i' in + * let ct_i = Term.mkConst (declare_constant t_i + * (DefinitionEntry ce5, IsDefinition Definition)) in + * + * let t_func' = make_t_func ro ct_i in + * let ce6 = Structures.mkUConst t_func' in + * let ct_func = + * Term.mkConst (declare_constant t_func + * (DefinitionEntry ce6, IsDefinition Definition)) in + * + * let t_atom' = Atom.interp_tbl ra in + * let ce1 = Structures.mkUConst t_atom' in + * let ct_atom = + * Term.mkConst (declare_constant t_atom + * (DefinitionEntry ce1, IsDefinition Definition)) in + * + * let t_form' = snd (Form.interp_tbl rf) in + * let ce2 = Structures.mkUConst t_form' in + * let ct_form = + * Term.mkConst (declare_constant t_form + * (DefinitionEntry ce2, IsDefinition Definition)) in + * + * let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) + * (interp_conseq_uf ct_i) + * (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in + * List.iter (fun (v,ty) -> + * let _ = Structures.declare_new_variable v ty in + * print_assm ty + * ) cuts; + * + * let used_roots = compute_roots roots last_root in + * let croots = + * let res = Array.make (List.length roots + 1) (mkInt 0) in + * let i = ref 0 in + * List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; + * Structures.mkArray (Lazy.force cint, res) in + * let cused_roots = + * let l = List.length used_roots in + * let res = Array.make (l + 1) (mkInt 0) in + * let i = ref (l-1) in + * List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; + * mklApp cSome [|mklApp carray [|Lazy.force cint|]; + * Structures.mkArray (Lazy.force cint, res)|] in + * let ce3 = Structures.mkUConst croots in + * let _ = declare_constant root + * (DefinitionEntry ce3, IsDefinition Definition) in + * let ce3' = Structures.mkUConst cused_roots in + * let _ = declare_constant used_root + * (DefinitionEntry ce3', IsDefinition Definition) in + * + * let certif = + * mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1); + * tres;mkInt (get_pos confl)|] in + * let ce4 = Structures.mkUConst certif in + * let _ = declare_constant trace + * (DefinitionEntry ce4, IsDefinition Definition) in + * + * let setup = + * mklApp csetup_checker_step_debug + * [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in + * + * let setup = Structures.cbv_vm (Global.env ()) setup + * (mklApp cprod + * [|Lazy.force cState_S_t; + * mklApp clist [|mklApp cstep + * [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in + * + * let s, steps = match Term.decompose_app setup with + * | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) -> + * s, of_coq_list csteps + * | _ -> assert false + * in + * + * let cpt = ref (List.length roots) in + * let debug_step s step = + * incr cpt; + * Format.eprintf "%d@." !cpt; + * let tm = + * mklApp cchecker_step_debug + * [| ct_i; ct_func; ct_atom; ct_form; s; step |] in + * + * let res = + * Structures.cbv_vm (Global.env ()) tm + * (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in + * + * match Term.decompose_app res with + * | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) -> + * if not (mk_bool cbad) then s + * else Structures.error ("Step number " ^ string_of_int !cpt ^ + * " (" ^ string_coq_constr + * (fst (Term.decompose_app step)) ^ ")" ^ + * " of the certificate likely failed." ) + * | _ -> assert false + * in + * + * List.fold_left debug_step s steps |> ignore; + * + * Structures.error ("Debug checker is only meant to be used for certificates \ + * that fail to be checked by SMTCoq.") *) @@ -725,7 +725,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in let lcpl = lcpl @ tlcepl in - let lcl = List.map (Retyping.get_type_of env sigma) lcpl in + let lcl = List.map (Structures.retyping_get_type_of env sigma) lcpl in let lsmt = List.map (of_coq_lemma rt ro ra' rf' env sigma solver_logic) lcl in let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index 4138e7c..ad6a5a4 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -618,7 +618,7 @@ module Make (Atom:ATOM) = mklApp cifb (Array.map interp_form args) | Fnot2 n -> (let r = ref (interp_form args.(0)) in - for i = 1 to n do + for _ = 1 to n do r := mklApp cnegb [|!r|] done; !r) diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index b410f88..a9855a2 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -409,12 +409,12 @@ let to_coq to_lit interp (cstep, mklApp cEqCgrP [|out_c c; out_f f1; out_f f2; res|] | LiaMicromega (cl,d) -> let cl' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in - let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm; Structures.Micromega_plugin_Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm|]) in + let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.micromega_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Structures.micromega_coq_proofTerm|]) in mklApp cLiaMicromega [|out_c c; cl'; c'|] | LiaDiseq l -> mklApp cLiaDiseq [|out_c c; out_f l|] | SplArith (orig,res,l) -> let res' = out_f res in - let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm; Structures.Micromega_plugin_Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm|]) in + let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.micromega_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.micromega_coq_proofTerm|]) in mklApp cSplArith [|out_c c; out_c orig; res'; l'|] | SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|] | BBVar res -> mklApp cBBVar [|out_c c; out_f res|] diff --git a/src/verit/verit.ml b/src/verit/verit.ml index 32f76f1..2fd7d2d 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -10,55 +10,50 @@ (**************************************************************************) -open Entries -open Declare -open Decl_kinds - open SmtMisc open CoqTerms -open SmtForm open SmtTrace open SmtAtom open SmtBtype open SmtCertif -let debug = false +(* let debug = false *) (******************************************************************************) (* Given a verit trace build the corresponding certif and theorem *) (******************************************************************************) -exception Import_trace of int +(* exception Import_trace of int *) -let get_val = function - Some a -> a - | None -> assert false +(* let get_val = function + * Some a -> a + * | None -> assert false *) (* For debugging certif processing :