diff options
-rw-r--r-- | .gitignore | 17 | ||||
-rw-r--r-- | INSTALL.md | 41 | ||||
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | ci/manifest-sources-8.11 | 2 | ||||
-rw-r--r-- | doc/sources.md | 32 | ||||
-rw-r--r-- | src/Array/PArray.v (renamed from src/versions/standard/Array/PArray_standard.v) | 0 | ||||
-rw-r--r-- | src/Int63/Int63.v (renamed from src/versions/standard/Int63/Int63_standard.v) | 0 | ||||
-rw-r--r-- | src/Int63/Int63Axioms.v (renamed from src/versions/standard/Int63/Int63Axioms_standard.v) | 0 | ||||
-rw-r--r-- | src/Int63/Int63Native.v (renamed from src/versions/standard/Int63/Int63Native_standard.v) | 0 | ||||
-rw-r--r-- | src/Int63/Int63Op.v (renamed from src/versions/standard/Int63/Int63Op_standard.v) | 0 | ||||
-rw-r--r-- | src/Int63/Int63Properties.v (renamed from src/versions/standard/Int63/Int63Properties_standard.v) | 0 | ||||
-rw-r--r-- | src/Makefile.local (renamed from src/versions/standard/Makefile.local) | 0 | ||||
-rw-r--r-- | src/Tactics.v (renamed from src/versions/standard/Tactics_standard.v) | 0 | ||||
-rw-r--r-- | src/Trace.v | 17 | ||||
-rw-r--r-- | src/_CoqProject (renamed from src/versions/standard/_CoqProject) | 23 | ||||
-rw-r--r-- | src/bva/Bva_checker.v | 26 | ||||
-rw-r--r-- | src/classes/SMT_classes_instances.v | 3 | ||||
-rwxr-xr-x | src/configure.sh | 42 | ||||
-rw-r--r-- | src/extraction/Makefile | 2 | ||||
-rw-r--r-- | src/extraction/verit_checker.mli | 6 | ||||
-rw-r--r-- | src/g_smtcoq.mlg (renamed from src/versions/standard/g_smtcoq_standard.mlg) | 2 | ||||
-rw-r--r-- | src/lfsc/lfsc.ml | 22 | ||||
-rw-r--r-- | src/lia/lia.ml | 12 | ||||
-rw-r--r-- | src/lia/lia.mli | 2 | ||||
-rw-r--r-- | src/smtcoq_plugin.mlpack (renamed from src/versions/standard/smtcoq_plugin_standard.mlpack) | 2 | ||||
-rw-r--r-- | src/smtlib2/smtlib2_genConstr.ml | 8 | ||||
-rw-r--r-- | src/smtlib2/smtlib2_solver.ml | 6 | ||||
-rw-r--r-- | src/trace/coqInterface.ml (renamed from src/versions/standard/structures.ml) | 4 | ||||
-rw-r--r-- | src/trace/coqInterface.mli (renamed from src/versions/standard/structures.mli) | 0 | ||||
-rw-r--r-- | src/trace/coqTerms.ml | 134 | ||||
-rw-r--r-- | src/trace/coqTerms.mli | 428 | ||||
-rw-r--r-- | src/trace/satAtom.ml | 4 | ||||
-rw-r--r-- | src/trace/satAtom.mli | 10 | ||||
-rw-r--r-- | src/trace/smtAtom.ml | 50 | ||||
-rw-r--r-- | src/trace/smtAtom.mli | 26 | ||||
-rw-r--r-- | src/trace/smtBtype.ml | 42 | ||||
-rw-r--r-- | src/trace/smtBtype.mli | 28 | ||||
-rw-r--r-- | src/trace/smtCertif.ml | 4 | ||||
-rw-r--r-- | src/trace/smtCertif.mli | 4 | ||||
-rw-r--r-- | src/trace/smtCommands.ml | 432 | ||||
-rw-r--r-- | src/trace/smtCommands.mli | 22 | ||||
-rw-r--r-- | src/trace/smtForm.ml | 46 | ||||
-rw-r--r-- | src/trace/smtForm.mli | 10 | ||||
-rw-r--r-- | src/trace/smtMisc.ml | 10 | ||||
-rw-r--r-- | src/trace/smtMisc.mli | 10 | ||||
-rw-r--r-- | src/trace/smtTrace.ml | 20 | ||||
-rw-r--r-- | src/trace/smtTrace.mli | 38 | ||||
-rw-r--r-- | src/verit/verit.ml | 14 | ||||
-rw-r--r-- | src/verit/verit.mli | 16 | ||||
-rw-r--r-- | src/verit/veritSyntax.ml | 2 | ||||
-rw-r--r-- | src/versions/native/Make | 171 | ||||
-rw-r--r-- | src/versions/native/Makefile | 505 | ||||
-rw-r--r-- | src/versions/native/Structures_native.v | 59 | ||||
-rw-r--r-- | src/versions/native/Tactics_native.v | 55 | ||||
-rw-r--r-- | src/versions/native/smtcoq_plugin_native.ml4 | 99 | ||||
-rw-r--r-- | src/versions/native/structures.ml | 186 | ||||
-rw-r--r-- | src/versions/native/structures.mli | 117 | ||||
-rw-r--r-- | src/versions/standard/Structures_standard.v | 64 | ||||
-rw-r--r-- | src/zchaff/zchaff.ml | 116 | ||||
-rw-r--r-- | src/zchaff/zchaff.mli | 10 |
60 files changed, 809 insertions, 2194 deletions
@@ -21,23 +21,10 @@ setup.log .lia.cache .nia.cache -# cp targets of src/configure.sh: -src/_CoqProject +# targets of coq_makefile: src/Makefile src/Makefile.conf -src/Makefile.local -src/smtcoq_plugin.ml4 -src/versions/native/Structures.v -src/g_smtcoq.mlg -src/smtcoq_plugin.mlpack -src/Tactics.v -src/versions/standard/Int63/Int63.v -src/versions/standard/Int63/Int63Native.v -src/versions/standard/Int63/Int63Op.v -src/versions/standard/Int63/Int63Axioms.v -src/versions/standard/Int63/Int63Properties.v -src/versions/standard/Array/PArray.v -src/versions/standard/Structures.v +src/g_smtcoq.ml # generated by the Makefile src/uninstall_me.sh @@ -81,12 +81,6 @@ You need to have OCaml version >= 4.08 and < 4.10 and Coq version 8.10.*. > SMTCoq. In particular this means you want a version of Coq that was compiled > with OCaml version >= 4.08. -If you want to use SMTCoq with high performance to check large proof -certificates, you need to use the [version of Coq with native -data-structures](https://github.com/smtcoq/native-coq) instead of -Coq-8.10 (warning: this allows one to use the vernacular commands but not -the tactics). - ### Install opam We recommended to install the required packages from @@ -139,44 +133,11 @@ but you might need to install some extra packages and libraries for your system Compile and install SMTCoq by using the following commands in the src directory. ```bash -./configure.sh -make -make install -``` - -## Installation with native-coq (not recommended except for high performances) - -> **Warning**: this installation procedure is recommended only to use -> the vernacular commands efficiently (in particular, to check very -> large proof certificates). It does not allow one to use the tactics. - -1. Download the git version of Coq with native compilation: -```bash -git clone https://github.com/smtcoq/native-coq.git -``` - and compile it by following the instructions available in the - repository. We recommand that you do not install it, but only compile - it in local: -```bash -./configure -local -make -``` - -2. Set an environment variable COQBIN to the directory where Coq's - binaries are; for instance: -```bash -export COQBIN=/home/jdoe/native-coq/bin/ -``` - (the final slash is mandatory). - -3. Compile and install SMTCoq by using the following commands in the src directory. -``` -./configure.sh -native +coq_makefile -f _CoqProject -o Makefile make make install ``` - ## Installation of the provers To use SMTCoq, we recommend installing the following two SMT solvers: @@ -1,5 +1,5 @@ all: - cd src && ./configure.sh && $(MAKE) + cd src && coq_makefile -f _CoqProject -o Makefile && $(MAKE) install: all cd src && $(MAKE) install diff --git a/ci/manifest-sources-8.11 b/ci/manifest-sources-8.11 index b93f959..795a34f 100644 --- a/ci/manifest-sources-8.11 +++ b/ci/manifest-sources-8.11 @@ -27,7 +27,7 @@ tasks: cd smtcoq git checkout coq-8.11 cd src - ./configure.sh + coq_makefile -f _CoqProject -o Makefile make make install cd ../.. diff --git a/doc/sources.md b/doc/sources.md index 55d2cec..045150d 100644 --- a/doc/sources.md +++ b/doc/sources.md @@ -17,14 +17,6 @@ The rest of the document describes the organization of `src`. SMTCoq sources are contained in this directory. A few Coq files can be found at top-level. -### [configure.sh](../src/configure.sh) - -This script is meant to be run when compiling SMTCoq for the first time. It -should also be run every time the Makefile is modified. It takes as argument an -optional flag `-native` which, when present, will set up the sources to use the -*native Coq* libraries. Otherwise the standard version 8.5 of Coq is used. See -section [versions](#versions). - ### [SMTCoq.v](../src/SMTCoq.v) This is the main SMTCoq entry point, it is meant to be imported by users that @@ -142,30 +134,6 @@ This module contains miscellaneous general lemmas that are used in several places throughout the development of SMTCoq. -### [versions](../src/versions) - -This directory contains everything that is dependent on the version of Coq that -one wants to use. `standard` contains libraries for the standard version of Coq -and `native` contains everything related to native Coq. Note that some -libraries are already present in the default libraries of native Coq, in this -case they have a counterpart in `standard` that replicates the functionality -(without using native integers or native arrays). - -A particular point of interest is the files -[smtcoq_plugin_standard.ml4](../src/versions/standard/smtcoq_plugin_standard.ml4) -and -[smtcoq_plugin_native.ml4](../src/versions/native/smtcoq_plugin_native.ml4). They -provide extension points for Coq by defining new vernacular commands and new -tactics. For instance the tactic `verit` tells Coq to call the OCaml function -`verit.tactic` (which in turns uses the Coq API to manipulate the goals and -call the certified checkers). - -```ocaml -TACTIC EXTEND Tactic_verit -| [ "verit" ] -> [ Verit.tactic () ] -END -``` - ### [spl](../src/spl) diff --git a/src/versions/standard/Array/PArray_standard.v b/src/Array/PArray.v index 25da052..25da052 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/Array/PArray.v diff --git a/src/versions/standard/Int63/Int63_standard.v b/src/Int63/Int63.v index acee305..acee305 100644 --- a/src/versions/standard/Int63/Int63_standard.v +++ b/src/Int63/Int63.v diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/Int63/Int63Axioms.v index 9625bce..9625bce 100644 --- a/src/versions/standard/Int63/Int63Axioms_standard.v +++ b/src/Int63/Int63Axioms.v diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/Int63/Int63Native.v index 0f9d6b7..0f9d6b7 100644 --- a/src/versions/standard/Int63/Int63Native_standard.v +++ b/src/Int63/Int63Native.v diff --git a/src/versions/standard/Int63/Int63Op_standard.v b/src/Int63/Int63Op.v index bb7d9a1..bb7d9a1 100644 --- a/src/versions/standard/Int63/Int63Op_standard.v +++ b/src/Int63/Int63Op.v diff --git a/src/versions/standard/Int63/Int63Properties_standard.v b/src/Int63/Int63Properties.v index feb19b8..feb19b8 100644 --- a/src/versions/standard/Int63/Int63Properties_standard.v +++ b/src/Int63/Int63Properties.v diff --git a/src/versions/standard/Makefile.local b/src/Makefile.local index 8abc72c..8abc72c 100644 --- a/src/versions/standard/Makefile.local +++ b/src/Makefile.local diff --git a/src/versions/standard/Tactics_standard.v b/src/Tactics.v index f79b253..f79b253 100644 --- a/src/versions/standard/Tactics_standard.v +++ b/src/Tactics.v diff --git a/src/Trace.v b/src/Trace.v index f9731f8..b6715ab 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -11,7 +11,6 @@ Require Import Bool Int63 PArray. -Require Structures. Require Import Misc State SMT_terms. Require Import Syntactic Arithmetic Operators Assumptions. Require Import Cnf Euf Lia BVList Bva_checker Array_checker. @@ -34,7 +33,7 @@ Section trace. Variable rho : Valuation.t. - Definition _trace_ := Structures.trace step. + Definition _trace_ := ((list step) * step)%type. (* A checker for such a trace *) @@ -42,7 +41,7 @@ Section trace. Hypothesis is_false_correct : forall c, is_false c -> ~ C.interp rho c. Definition _checker_ (s: S.t) (t: _trace_) (confl:clause_id) : bool := - let s' := Structures.trace_fold check_step s t in + let s' := List.fold_left check_step (fst t) s in (* let s' := PArray.fold_left (fun s a => PArray.fold_left check_step s a) s t in *) is_false (S.get s' confl). (* Register _checker_ as PrimInline. *) @@ -78,7 +77,11 @@ Section trace. intros s t' cid Hf Hv. apply (is_false_correct Hf). apply S.valid_get. - apply Structures.trace_fold_ind; auto. + clear Hf. + rewrite <- List.fold_left_rev_right in *. + induction (List.rev (fst t')); [ apply Hv | ]. + apply valid_check_step. + apply IHl. (* apply PArray.fold_left_ind; auto. *) (* intros a i _ Ha;apply PArray.fold_left_ind;trivial. *) (* intros a0 i0 _ H1;auto. *) @@ -534,7 +537,7 @@ Inductive step := Definition setup_checker_step_debug d used_roots (c:certif) := let (nclauses, t, confl) := c in let s := add_roots (S.make nclauses) d used_roots in - (s, Structures.trace_to_list t). + (s, fst t). Definition position_of_step (st:step) := @@ -686,7 +689,7 @@ Inductive step := let (nclauses, t, confl) := c in let s := add_roots (S.make nclauses) d used_roots in let '(_, nb, failure) := - Structures.trace_fold + List.fold_left (fun acc step => match acc with | (s, nb, None) => @@ -698,7 +701,7 @@ Inductive step := else (s, nb, None) | _ => acc end - ) (s, O, None) t + ) (fst t) (s, O, None) in match failure with | Some st => Some (nb, name_of_step st) diff --git a/src/versions/standard/_CoqProject b/src/_CoqProject index 133565d..f7862e1 100644 --- a/src/versions/standard/_CoqProject +++ b/src/_CoqProject @@ -26,21 +26,16 @@ -I trace -I verit -I zchaff --I versions/standard --I versions/standard/Int63 --I versions/standard/Array +-I Int63 +-I Array -I ../3rdparty/alt-ergo -versions/standard/Int63/Int63.v -versions/standard/Int63/Int63Native.v -versions/standard/Int63/Int63Op.v -versions/standard/Int63/Int63Axioms.v -versions/standard/Int63/Int63Properties.v -versions/standard/Array/PArray.v - -versions/standard/Structures.v -versions/standard/structures.ml -versions/standard/structures.mli +Int63/Int63.v +Int63/Int63Native.v +Int63/Int63Op.v +Int63/Int63Axioms.v +Int63/Int63Properties.v +Array/PArray.v bva/BVList.v bva/Bva_checker.v @@ -73,6 +68,8 @@ trace/smtMisc.ml trace/smtMisc.mli trace/smtTrace.ml trace/smtTrace.mli +trace/coqInterface.ml +trace/coqInterface.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_parse.mli diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 7a47c70..1487453 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -12,8 +12,6 @@ (** A small checker for bit-vectors bit-blasting *) -Require Structures. - Require Import Int63 Int63Properties PArray SMT_classes ZArith. Require Import Misc State SMT_terms BVList Psatz. @@ -925,7 +923,7 @@ Definition shl_lit_be (a: list _lit) (b: list bool): list _lit := Definition check_shl (bs1: list _lit) (bs2: list bool) (bsres: list _lit) : bool := - if (Structures.nat_eqb (length bs1) (length bs2)) then + if (Nat.eqb (length bs1) (length bs2)) then if (forallb2 eq_carry_lit (lit_to_carry (shl_lit_be bs1 bs2)) bsres) then true else false else false. @@ -976,7 +974,7 @@ Definition shr_lit_be (a: list _lit) (b: list bool): list _lit := Definition check_shr (bs1: list _lit) (bs2: list bool) (bsres: list _lit) : bool := - if (Structures.nat_eqb (length bs1) (length bs2)) then + if (Nat.eqb (length bs1) (length bs2)) then if (forallb2 eq_carry_lit (lit_to_carry (shr_lit_be bs1 bs2)) bsres) then true else false else false. @@ -7946,7 +7944,7 @@ Proof. intro bs1. - simpl in *. unfold check_shl in H. simpl in H. case_eq bs2; simpl; intros; subst. simpl in H. now contradict H. - simpl in *. inversion H0. rewrite H2, Structures.nat_eqb_refl in H. + simpl in *. inversion H0. rewrite H2, Nat.eqb_refl in H. case_eq (forallb2 eq_carry_lit (lit_to_carry (shl_lit_be (a :: bs1) (b :: l))) bsres); intros. + apply prop_eq_carry_lit2 in H1. rewrite prop_interp_carry3 in H1. @@ -8016,8 +8014,8 @@ Proof. intro bs1. induction bs1 as [ | xbs1 xsbs1 IHbs1 ]. - intros. simpl. unfold check_shl, shl_lit_be in H. - case_eq (Structures.nat_eqb (@length int []) (length bs2)); intros. - rewrite Structures.nat_eqb_eq in H0. + case_eq (Nat.eqb (@length int []) (length bs2)); intros. + rewrite Nat.eqb_eq in H0. rewrite <- H0 in H. simpl in H. rewrite nshl_lit_empty in H. case_eq bsres; intros. simpl. @@ -8025,7 +8023,7 @@ Proof. intro bs1. subst; now contradict H. rewrite H0 in H; now contradict H. - intros. unfold check_shl in H. - case_eq (Structures.nat_eqb (Datatypes.length (xbs1 :: xsbs1)) (Datatypes.length bs2)); intros. + case_eq (Nat.eqb (Datatypes.length (xbs1 :: xsbs1)) (Datatypes.length bs2)); intros. rewrite H0 in H. case_eq ( forallb2 eq_carry_lit (lit_to_carry (shl_lit_be (xbs1 :: xsbs1) bs2)) bsres); intros. @@ -8033,7 +8031,7 @@ Proof. intro bs1. rewrite prop_interp_carry3 in H1. unfold RAWBITVECTOR_LIST.bv_shl. - rewrite Structures.nat_eqb_eq in H0. + rewrite Nat.eqb_eq in H0. unfold RAWBITVECTOR_LIST.size. rewrite !map_length. rewrite H0, N.eqb_refl. now rewrite <- H1, shl_interp. @@ -8287,7 +8285,7 @@ Proof. intro bs1. - simpl in *. unfold check_shr in H. simpl in H. case_eq bs2; simpl; intros; subst. simpl in H. now contradict H. - simpl in *. inversion H0. rewrite H2, Structures.nat_eqb_refl in H. + simpl in *. inversion H0. rewrite H2, Nat.eqb_refl in H. case_eq (forallb2 eq_carry_lit (lit_to_carry (shr_lit_be (a :: bs1) (b :: l))) bsres); intros. + apply prop_eq_carry_lit2 in H1. rewrite prop_interp_carry3 in H1. @@ -8345,8 +8343,8 @@ Proof. intro bs1. induction bs1 as [ | xbs1 xsbs1 IHbs1 ]. - intros. simpl. unfold check_shr, shr_lit_be in H. - case_eq (Structures.nat_eqb (@length int []) (length bs2)); intros. - rewrite Structures.nat_eqb_eq in H0. + case_eq (Nat.eqb (@length int []) (length bs2)); intros. + rewrite Nat.eqb_eq in H0. rewrite <- H0 in H. simpl in H. rewrite nshr_lit_empty in H. case_eq bsres; intros. simpl. @@ -8354,7 +8352,7 @@ Proof. intro bs1. subst; now contradict H. rewrite H0 in H; now contradict H. - intros. unfold check_shr in H. - case_eq (Structures.nat_eqb (Datatypes.length (xbs1 :: xsbs1)) (Datatypes.length bs2)); intros. + case_eq (Nat.eqb (Datatypes.length (xbs1 :: xsbs1)) (Datatypes.length bs2)); intros. rewrite H0 in H. case_eq ( forallb2 eq_carry_lit (lit_to_carry (shr_lit_be (xbs1 :: xsbs1) bs2)) bsres); intros. @@ -8362,7 +8360,7 @@ Proof. intro bs1. rewrite prop_interp_carry3 in H1. unfold RAWBITVECTOR_LIST.bv_shr. - rewrite Structures.nat_eqb_eq in H0. + rewrite Nat.eqb_eq in H0. unfold RAWBITVECTOR_LIST.size. rewrite !map_length. rewrite H0, N.eqb_refl. now rewrite <- H1, shr_interp. diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v index aa2082e..a2831cf 100644 --- a/src/classes/SMT_classes_instances.v +++ b/src/classes/SMT_classes_instances.v @@ -13,7 +13,6 @@ Require Import Bool OrderedType BinPos ZArith OrderedTypeEx. Require Import Int63. Require Import State BVList FArray. -Require Structures. Require Export SMT_classes. @@ -253,7 +252,7 @@ Section Nat. Defined. Global Instance Nat_eqbtype : EqbType nat := - {| eqb := Structures.nat_eqb; eqb_spec := Structures.nat_eqb_eq |}. + {| eqb := Nat.eqb; eqb_spec := Nat.eqb_eq |}. Global Instance Nat_dec : DecType nat := EqbToDecType. diff --git a/src/configure.sh b/src/configure.sh deleted file mode 100755 index fb265e0..0000000 --- a/src/configure.sh +++ /dev/null @@ -1,42 +0,0 @@ -#!/bin/sh - -pre=$(echo $0 | sed "s,\(\([^/]*/\)*\)[^/]*,\1,") - -rm -f ${pre}_CoqProject -rm -f ${pre}Makefile -rm -f ${pre}Makefile.conf -rm -f ${pre}Makefile.local -rm -f ${pre}smtcoq_plugin.ml4 -rm -f ${pre}versions/native/Structures.v -rm -f ${pre}g_smtcoq.mlg -rm -f ${pre}smtcoq_plugin.mlpack -rm -f ${pre}Tactics.v -rm -f ${pre}versions/standard/Int63/Int63.v -rm -f ${pre}versions/standard/Int63/Int63Native.v -rm -f ${pre}versions/standard/Int63/Int63Op.v -rm -f ${pre}versions/standard/Int63/Int63Axioms.v -rm -f ${pre}versions/standard/Int63/Int63Properties.v -rm -f ${pre}versions/standard/Array/PArray.v -rm -f ${pre}versions/standard/Structures.v - -set -e -if [ $@ -a $@ = -native ]; then - cp ${pre}versions/native/Makefile ${pre}Makefile - cp ${pre}versions/native/smtcoq_plugin_native.ml4 ${pre}smtcoq_plugin.ml4 - cp ${pre}versions/native/Structures_native.v ${pre}versions/native/Structures.v - cp ${pre}versions/native/Tactics_native.v ${pre}Tactics.v -else - cp ${pre}versions/standard/_CoqProject ${pre}_CoqProject - cp ${pre}versions/standard/Makefile.local ${pre}Makefile.local - cp ${pre}versions/standard/g_smtcoq_standard.mlg ${pre}g_smtcoq.mlg - 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 - cp ${pre}versions/standard/Int63/Int63Native_standard.v ${pre}versions/standard/Int63/Int63Native.v - cp ${pre}versions/standard/Int63/Int63Op_standard.v ${pre}versions/standard/Int63/Int63Op.v - cp ${pre}versions/standard/Int63/Int63Axioms_standard.v ${pre}versions/standard/Int63/Int63Axioms.v - cp ${pre}versions/standard/Int63/Int63Properties_standard.v ${pre}versions/standard/Int63/Int63Properties.v - cp ${pre}versions/standard/Array/PArray_standard.v ${pre}versions/standard/Array/PArray.v - cp ${pre}versions/standard/Structures_standard.v ${pre}versions/standard/Structures.v - cp ${pre}versions/standard/Tactics_standard.v ${pre}Tactics.v - coq_makefile -f _CoqProject -o Makefile -fi diff --git a/src/extraction/Makefile b/src/extraction/Makefile index 73b0ae4..354dd53 100644 --- a/src/extraction/Makefile +++ b/src/extraction/Makefile @@ -15,7 +15,7 @@ COQTOP=$(COQBIN)../ FLAGS=-rectypes COMPILEFLAGS=-cclib -lunix -SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../euf -I ../cnf -I ../versions/native/ +SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../euf -I ../cnf -I ../../3rdparty/alt-ergo COQLIB=-I ${COQTOP}kernel -I ${COQTOP}lib -I ${COQTOP}library -I ${COQTOP}parsing -I ${COQTOP}pretyping -I ${COQTOP}interp -I ${COQTOP}proofs -I ${COQTOP}tactics -I ${COQTOP}toplevel -I ${COQTOP}plugins/btauto -I ${COQTOP}plugins/cc -I ${COQTOP}plugins/decl_mode -I ${COQTOP}plugins/extraction -I ${COQTOP}plugins/field -I ${COQTOP}plugins/firstorder -I ${COQTOP}plugins/fourier -I ${COQTOP}plugins/funind -I ${COQTOP}plugins/micromega -I ${COQTOP}plugins/nsatz -I ${COQTOP}plugins/omega -I ${COQTOP}plugins/quote -I ${COQTOP}plugins/ring -I ${COQTOP}plugins/romega -I ${COQTOP}plugins/rtauto -I ${COQTOP}plugins/setoid_ring -I ${COQTOP}plugins/syntax -I ${COQTOP}plugins/xml -I /usr/lib/ocaml/camlp5 CMXA=nums.cmxa str.cmxa unix.cmxa gramlib.cmxa dynlink.cmxa ${COQTOP}kernel/byterun/coq_fix_code.o ${COQTOP}kernel/byterun/coq_interp.o ${COQTOP}kernel/byterun/coq_memory.o ${COQTOP}kernel/byterun/coq_values.o clib.cmxa lib.cmxa kernel.cmxa library.cmxa pretyping.cmxa interp.cmxa proofs.cmxa parsing.cmxa tactics.cmxa toplevel.cmxa micromega_plugin.cmxa smtcoq.cmxa diff --git a/src/extraction/verit_checker.mli b/src/extraction/verit_checker.mli index 4491410..7b8b882 100644 --- a/src/extraction/verit_checker.mli +++ b/src/extraction/verit_checker.mli @@ -10,7 +10,7 @@ (**************************************************************************) -module Mc = Structures.Micromega_plugin_Certificate.Mc +module Mc = CoqInterface.Micromega_plugin_Certificate.Mc val mkInt : int -> ExtrNative.uint val mkArray : 'a array -> 'a ExtrNative.parray val dump_nat : Mc.nat -> Smt_checker.nat @@ -25,7 +25,7 @@ val to_coq : 'a SmtCertif.clause -> Smt_checker.Euf_Checker.step ExtrNative.parray ExtrNative.parray * 'a SmtCertif.clause -val btype_to_coq : SmtAtom.btype -> Smt_checker.Typ.coq_type +val btype_to_coq : SmtBtype.btype -> Smt_checker.Typ.coq_type val c_to_coq : SmtAtom.cop -> Smt_checker.Atom.cop val u_to_coq : SmtAtom.uop -> Smt_checker.Atom.unop val b_to_coq : SmtAtom.bop -> Smt_checker.Atom.binop @@ -42,7 +42,7 @@ val form_interp_tbl : SmtAtom.Form.reify -> Smt_checker.Form.form ExtrNative.parray val count_btype : int ref val count_op : int ref -val declare_sort : Smtlib2_ast.symbol -> SmtAtom.btype +val declare_sort : Smtlib2_ast.symbol -> SmtBtype.btype val declare_fun : Smtlib2_ast.symbol -> Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op diff --git a/src/versions/standard/g_smtcoq_standard.mlg b/src/g_smtcoq.mlg index 5cfb287..c8d38db 100644 --- a/src/versions/standard/g_smtcoq_standard.mlg +++ b/src/g_smtcoq.mlg @@ -87,7 +87,7 @@ let lemmas_list = Summary.ref ~name:"Selected lemmas" [] let cache_lemmas (_, lems) = lemmas_list := lems -let declare_lemmas : Structures.constr_expr list -> Libobject.obj = +let declare_lemmas : CoqInterface.constr_expr list -> Libobject.obj = let open Libobject in declare_object { diff --git a/src/lfsc/lfsc.ml b/src/lfsc/lfsc.ml index f17eb04..f2157a4 100644 --- a/src/lfsc/lfsc.ml +++ b/src/lfsc/lfsc.ml @@ -57,7 +57,7 @@ let process_signatures_once = ) signatures with | Ast.TypingError (t1, t2) -> - Structures.error + CoqInterface.error (asprintf "@[<hov>LFSC typing error: expected %a, got %a@]@." Ast.print_term t1 Ast.print_term t2) @@ -116,7 +116,7 @@ let import_trace first parse lexbuf = with | Ast.TypingError (t1, t2) -> - Structures.error + CoqInterface.error (asprintf "@[<hov>LFSC typing error: expected %a, got %a@]@." Ast.print_term t1 Ast.print_term t2) @@ -386,13 +386,13 @@ let call_cvc4 env rt ro ra rf root _ = begin try get_proof cvc4 (import_trace (Some root) lfsc_parse_one) with - | Ast.CVC4Sat -> Structures.error "CVC4 returned SAT" - | No_proof -> Structures.error "CVC4 did not generate a proof" - | Failure s -> Structures.error ("Importing of proof failed: " ^ s) + | Ast.CVC4Sat -> CoqInterface.error "CVC4 returned SAT" + | No_proof -> CoqInterface.error "CVC4 did not generate a proof" + | Failure s -> CoqInterface.error ("Importing of proof failed: " ^ s) end | Sat -> let smodel = get_model cvc4 in - Structures.error + CoqInterface.error ("CVC4 returned sat. Here is the model:\n\n" ^ SmtCommands.model_string env rt ro ra rf smodel) (* (asprintf "CVC4 returned sat. Here is the model:\n%a" SExpr.print smodel) *) @@ -435,7 +435,7 @@ let get_model_from_file filename = let lexbuf = Lexing.from_channel chan in match SExprParser.sexps SExprLexer.main lexbuf with | [SExpr.Atom "sat"; m] -> m - | _ -> Structures.error "CVC4 returned SAT but no model" + | _ -> CoqInterface.error "CVC4 returned SAT but no model" let call_cvc4_file env rt ro ra rf root = @@ -467,17 +467,17 @@ let call_cvc4_file env rt ro ra rf root = eprintf "CVC4 = %.5f@." (t1-.t0); if exit_code <> 0 then - Structures.error ("CVC4 crashed: return code "^string_of_int exit_code); + CoqInterface.error ("CVC4 crashed: return code "^string_of_int exit_code); (* ignore (Sys.command clean_cmd); *) try import_trace_from_file (Some root) prooffilename with - | No_proof -> Structures.error "CVC4 did not generate a proof" - | Failure s -> Structures.error ("Importing of proof failed: " ^ s) + | No_proof -> CoqInterface.error "CVC4 did not generate a proof" + | Failure s -> CoqInterface.error ("Importing of proof failed: " ^ s) | Ast.CVC4Sat -> let smodel = get_model_from_file prooffilename in - Structures.error + CoqInterface.error ("CVC4 returned sat. Here is the model:\n\n" ^ SmtCommands.model_string env rt ro ra rf smodel) diff --git a/src/lia/lia.ml b/src/lia/lia.ml index 53dbf6d..e00092e 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -12,7 +12,7 @@ (*** Linking SMT Terms to Micromega Terms ***) open Util -open Structures.Micromega_plugin_Micromega +open CoqInterface.Micromega_plugin_Micromega open SmtForm open SmtAtom @@ -92,7 +92,7 @@ let smt_binop_to_micromega_formula tbl op ha hb = | BO_Zge -> OpGe | BO_Zgt -> OpGt | BO_eq _ -> OpEq - | _ -> Structures.error + | _ -> CoqInterface.error "lia.ml: smt_binop_to_micromega_formula expecting a formula" in let lhs = smt_Atom_to_micromega_pExpr tbl ha in @@ -102,7 +102,7 @@ let smt_binop_to_micromega_formula tbl op ha hb = 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 + | _ -> CoqInterface.error "lia.ml: smt_Atom_to_micromega_formula was expecting an LIA formula" (* specialized fold *) @@ -152,7 +152,7 @@ let smt_clause_to_coq_micromega_formula tbl cl = binop_list tbl (fun x y -> Cj (x,y)) TT (List.map Form.neg cl) let tauto_lia ff = - let cnf_ff,_ = Structures.Micromega_plugin_Micromega.cnfZ ff in + let cnf_ff,_ = CoqInterface.Micromega_plugin_Micromega.cnfZ ff in let rec xwitness_list l = match l with | [] -> Some [] @@ -160,8 +160,8 @@ let tauto_lia ff = match xwitness_list l with | None -> None | Some l -> - match Structures.Micromega_plugin_Certificate.lia true max_int (List.map (fun ((e, o), _) -> Structures.Micromega_plugin_Micromega.denorm e, o) e) with - | Structures.Micromega_plugin_Certificate.Prf w -> Some (w::l) + match CoqInterface.Micromega_plugin_Certificate.lia true max_int (List.map (fun ((e, o), _) -> CoqInterface.Micromega_plugin_Micromega.denorm e, o) e) with + | CoqInterface.Micromega_plugin_Certificate.Prf w -> Some (w::l) | _ -> None in xwitness_list cnf_ff diff --git a/src/lia/lia.mli b/src/lia/lia.mli index 7b4c6c8..f996ac0 100644 --- a/src/lia/lia.mli +++ b/src/lia/lia.mli @@ -12,4 +12,4 @@ val build_lia_certif : SmtAtom.Form.t list -> - Structures.Micromega_plugin_Certificate.Mc.zArithProof list option + CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list option diff --git a/src/versions/standard/smtcoq_plugin_standard.mlpack b/src/smtcoq_plugin.mlpack index f210db1..0907551 100644 --- a/src/versions/standard/smtcoq_plugin_standard.mlpack +++ b/src/smtcoq_plugin.mlpack @@ -1,4 +1,4 @@ -Structures +CoqInterface SmtMisc CoqTerms diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index eb1c5b7..0c6e2ac 100644 --- a/src/smtlib2/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -97,10 +97,10 @@ let rec sort_of_sort = function let declare_sort_from_name rt s = - let cons_t = Structures.declare_new_type (Structures.mkId ("Smt_sort_"^s)) in + let cons_t = CoqInterface.declare_new_type (CoqInterface.mkId ("Smt_sort_"^s)) in let compdec_type = mklApp cCompDec [| cons_t |] in let compdec_var = - Structures.declare_new_variable (Structures.mkId ("CompDec_"^s)) compdec_type in + CoqInterface.declare_new_variable (CoqInterface.mkId ("CompDec_"^s)) compdec_type in let res = SmtBtype.of_coq_compdec rt cons_t compdec_var in SmtMaps.add_btype s res; res @@ -110,9 +110,9 @@ let declare_sort rt sym = declare_sort_from_name rt (string_of_symbol sym) let declare_fun_from_name rt ro s tyl ty = let coqTy = List.fold_right (fun typ c -> - Structures.mkArrow (interp_to_coq rt typ) c) + CoqInterface.mkArrow (interp_to_coq rt typ) c) tyl (interp_to_coq rt ty) in - let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in + let cons_v = CoqInterface.declare_new_variable (CoqInterface.mkId ("Smt_var_"^s)) coqTy in let op = Op.declare ro cons_v (Array.of_list tyl) ty None in SmtMaps.add_fun s op; op diff --git a/src/smtlib2/smtlib2_solver.ml b/src/smtlib2/smtlib2_solver.ml index 99538ce..efab1c1 100644 --- a/src/smtlib2/smtlib2_solver.ml +++ b/src/smtlib2/smtlib2_solver.ml @@ -73,7 +73,7 @@ let read_response { lexbuf } = let error s sexp = kill s; - Structures.error (asprintf "Solver error: %a." SExpr.print sexp) + CoqInterface.error (asprintf "Solver error: %a." SExpr.print sexp) let read_success s = @@ -89,7 +89,7 @@ let read_check_result s = match SExprParser.sexp SExprLexer.main s.lexbuf with | SExpr.Atom "sat" -> Sat | SExpr.Atom "unsat" -> Unsat - | SExpr.Atom "unknown" -> Structures.error ("Solver returned uknown.") + | SExpr.Atom "unknown" -> CoqInterface.error ("Solver returned uknown.") | r -> error s r @@ -111,7 +111,7 @@ let send_command s cmd read = * let buf = Bytes.create err_p2 in * Unix.read s.stderr buf 0 err_p2 |> ignore; * let err_msg = Bytes.sub_string buf err_p1 len in - * Structures.error ("Solver error: "^err_msg); + * CoqInterface.error ("Solver error: "^err_msg); * end * else (kill s; raise e) *) kill s; raise e diff --git a/src/versions/standard/structures.ml b/src/trace/coqInterface.ml index 863c921..36f4337 100644 --- a/src/versions/standard/structures.ml +++ b/src/trace/coqInterface.ml @@ -112,7 +112,7 @@ let init_modules = Coqlib.init_modules (* Int63 *) -let int63_modules = [["SMTCoq";"versions";"standard";"Int63";"Int63Native"]] +let int63_modules = [["SMTCoq";"Int63";"Int63Native"]] (* 31-bits integers are "called" 63 bits (this is sound) *) let int31_module = [["Coq";"Numbers";"Cyclic";"Int31";"Int31"]] @@ -135,7 +135,7 @@ let cint = gen_constant int31_module "int31" (* PArray *) -let parray_modules = [["SMTCoq";"versions";"standard";"Array";"PArray"]] +let parray_modules = [["SMTCoq";"Array";"PArray"]] let cmake = gen_constant parray_modules "make" let cset = gen_constant parray_modules "set" diff --git a/src/versions/standard/structures.mli b/src/trace/coqInterface.mli index 104f3f9..104f3f9 100644 --- a/src/versions/standard/structures.mli +++ b/src/trace/coqInterface.mli diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index c6188b8..1c4ee81 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -13,23 +13,23 @@ open SmtMisc -let gen_constant = Structures.gen_constant +let gen_constant = CoqInterface.gen_constant (* Int63 *) -let cint = Structures.cint -let ceq63 = gen_constant Structures.int63_modules "eqb" +let cint = CoqInterface.cint +let ceq63 = gen_constant CoqInterface.int63_modules "eqb" (* PArray *) -let carray = gen_constant Structures.parray_modules "array" +let carray = gen_constant CoqInterface.parray_modules "array" (* is_true *) -let cis_true = gen_constant Structures.init_modules "is_true" +let cis_true = gen_constant CoqInterface.init_modules "is_true" (* nat *) -let cnat = gen_constant Structures.init_modules "nat" -let cO = gen_constant Structures.init_modules "O" -let cS = gen_constant Structures.init_modules "S" +let cnat = gen_constant CoqInterface.init_modules "nat" +let cO = gen_constant CoqInterface.init_modules "O" +let cS = gen_constant CoqInterface.init_modules "S" (* Positive *) let positive_modules = [["Coq";"Numbers";"BinNums"]; @@ -74,49 +74,49 @@ let ceqbZ = gen_constant z_modules "eqb" (* Booleans *) let bool_modules = [["Coq";"Bool";"Bool"]] -let cbool = gen_constant Structures.init_modules "bool" -let ctrue = gen_constant Structures.init_modules "true" -let cfalse = gen_constant Structures.init_modules "false" -let candb = gen_constant Structures.init_modules "andb" -let corb = gen_constant Structures.init_modules "orb" -let cxorb = gen_constant Structures.init_modules "xorb" -let cnegb = gen_constant Structures.init_modules "negb" -let cimplb = gen_constant Structures.init_modules "implb" +let cbool = gen_constant CoqInterface.init_modules "bool" +let ctrue = gen_constant CoqInterface.init_modules "true" +let cfalse = gen_constant CoqInterface.init_modules "false" +let candb = gen_constant CoqInterface.init_modules "andb" +let corb = gen_constant CoqInterface.init_modules "orb" +let cxorb = gen_constant CoqInterface.init_modules "xorb" +let cnegb = gen_constant CoqInterface.init_modules "negb" +let cimplb = gen_constant CoqInterface.init_modules "implb" let ceqb = gen_constant bool_modules "eqb" let cifb = gen_constant bool_modules "ifb" -let ciff = gen_constant Structures.init_modules "iff" +let ciff = gen_constant CoqInterface.init_modules "iff" let creflect = gen_constant bool_modules "reflect" (* Lists *) -let clist = gen_constant Structures.init_modules "list" -let cnil = gen_constant Structures.init_modules "nil" -let ccons = gen_constant Structures.init_modules "cons" -let clength = gen_constant Structures.init_modules "length" +let clist = gen_constant CoqInterface.init_modules "list" +let cnil = gen_constant CoqInterface.init_modules "nil" +let ccons = gen_constant CoqInterface.init_modules "cons" +let clength = gen_constant CoqInterface.init_modules "length" (* Option *) -let coption = gen_constant Structures.init_modules "option" -let cSome = gen_constant Structures.init_modules "Some" -let cNone = gen_constant Structures.init_modules "None" +let coption = gen_constant CoqInterface.init_modules "option" +let cSome = gen_constant CoqInterface.init_modules "Some" +let cNone = gen_constant CoqInterface.init_modules "None" (* Pairs *) -let cpair = gen_constant Structures.init_modules "pair" -let cprod = gen_constant Structures.init_modules "prod" +let cpair = gen_constant CoqInterface.init_modules "pair" +let cprod = gen_constant CoqInterface.init_modules "prod" (* Dependent pairs *) -let csigT = gen_constant Structures.init_modules "sigT" -(* let cprojT1 = gen_constant Structures.init_modules "projT1" *) -(* let cprojT2 = gen_constant Structures.init_modules "projT2" *) -(* let cprojT3 = gen_constant Structures.init_modules "projT3" *) +let csigT = gen_constant CoqInterface.init_modules "sigT" +(* let cprojT1 = gen_constant CoqInterface.init_modules "projT1" *) +(* let cprojT2 = gen_constant CoqInterface.init_modules "projT2" *) +(* let cprojT3 = gen_constant CoqInterface.init_modules "projT3" *) -(* let csigT2 = gen_constant Structures.init_modules "sigT2" *) -(* let csigT_of_sigT2 = gen_constant Structures.init_modules "sigT_of_sigT2" *) +(* let csigT2 = gen_constant CoqInterface.init_modules "sigT2" *) +(* let csigT_of_sigT2 = gen_constant CoqInterface.init_modules "sigT_of_sigT2" *) (* Logical Operators *) -let cnot = gen_constant Structures.init_modules "not" -let ceq = gen_constant Structures.init_modules "eq" -let crefl_equal = gen_constant Structures.init_modules "eq_refl" -let cconj = gen_constant Structures.init_modules "conj" -let cand = gen_constant Structures.init_modules "and" +let cnot = gen_constant CoqInterface.init_modules "not" +let ceq = gen_constant CoqInterface.init_modules "eq" +let crefl_equal = gen_constant CoqInterface.init_modules "eq_refl" +let cconj = gen_constant CoqInterface.init_modules "conj" +let cand = gen_constant CoqInterface.init_modules "and" (* Bit vectors *) let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]] @@ -306,8 +306,8 @@ let ceq_refl_true = let eq_refl_true () = Lazy.force ceq_refl_true let vm_cast_true_no_check t = - Structures.mkCast(eq_refl_true (), - Structures.vmcast, + CoqInterface.mkCast(eq_refl_true (), + CoqInterface.vmcast, mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]) (* This version checks convertibility right away instead of delaying it at @@ -315,13 +315,13 @@ let vm_cast_true_no_check t = SMTCoq's tactics. *) let vm_cast_true env t = try - Structures.vm_conv Reduction.CUMUL env + CoqInterface.vm_conv Reduction.CUMUL env (mklApp ceq [|Lazy.force cbool; Lazy.force ctrue; Lazy.force ctrue|]) (mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]); vm_cast_true_no_check t with Reduction.NotConvertible -> - Structures.error ("SMTCoq was not able to check the proof certificate.") + CoqInterface.error ("SMTCoq was not able to check the proof certificate.") (* Compute a nat *) @@ -355,39 +355,39 @@ let rec mk_bv_list = function (* Reification *) let mk_bool b = - let c, args = Structures.decompose_app b in - if Structures.eq_constr c (Lazy.force ctrue) then true - else if Structures.eq_constr c (Lazy.force cfalse) then false + let c, args = CoqInterface.decompose_app b in + if CoqInterface.eq_constr c (Lazy.force ctrue) then true + else if CoqInterface.eq_constr c (Lazy.force cfalse) then false else assert false let rec mk_bool_list bs = - let c, args = Structures.decompose_app bs in - if Structures.eq_constr c (Lazy.force cnil) then [] - else if Structures.eq_constr c (Lazy.force ccons) then + let c, args = CoqInterface.decompose_app bs in + if CoqInterface.eq_constr c (Lazy.force cnil) then [] + else if CoqInterface.eq_constr c (Lazy.force ccons) then match args with | [_; b; bs] -> mk_bool b :: mk_bool_list bs | _ -> assert false else assert false let rec mk_nat n = - let c, args = Structures.decompose_app n in - if Structures.eq_constr c (Lazy.force cO) then + let c, args = CoqInterface.decompose_app n in + if CoqInterface.eq_constr c (Lazy.force cO) then 0 - else if Structures.eq_constr c (Lazy.force cS) then + else if CoqInterface.eq_constr c (Lazy.force cS) then match args with | [n] -> (mk_nat n) + 1 | _ -> assert false else assert false let rec mk_positive n = - let c, args = Structures.decompose_app n in - if Structures.eq_constr c (Lazy.force cxH) then + let c, args = CoqInterface.decompose_app n in + if CoqInterface.eq_constr c (Lazy.force cxH) then 1 - else if Structures.eq_constr c (Lazy.force cxO) then + else if CoqInterface.eq_constr c (Lazy.force cxO) then match args with | [n] -> 2 * (mk_positive n) | _ -> assert false - else if Structures.eq_constr c (Lazy.force cxI) then + else if CoqInterface.eq_constr c (Lazy.force cxI) then match args with | [n] -> 2 * (mk_positive n) + 1 | _ -> assert false @@ -395,10 +395,10 @@ let rec mk_positive n = let mk_N n = - let c, args = Structures.decompose_app n in - if Structures.eq_constr c (Lazy.force cN0) then + let c, args = CoqInterface.decompose_app n in + if CoqInterface.eq_constr c (Lazy.force cN0) then 0 - else if Structures.eq_constr c (Lazy.force cNpos) then + else if CoqInterface.eq_constr c (Lazy.force cNpos) then match args with | [n] -> mk_positive n | _ -> assert false @@ -406,13 +406,13 @@ let mk_N n = let mk_Z n = - let c, args = Structures.decompose_app n in - if Structures.eq_constr c (Lazy.force cZ0) then 0 - else if Structures.eq_constr c (Lazy.force cZpos) then + let c, args = CoqInterface.decompose_app n in + if CoqInterface.eq_constr c (Lazy.force cZ0) then 0 + else if CoqInterface.eq_constr c (Lazy.force cZpos) then match args with | [n] -> mk_positive n | _ -> assert false - else if Structures.eq_constr c (Lazy.force cZneg) then + else if CoqInterface.eq_constr c (Lazy.force cZneg) then match args with | [n] -> - mk_positive n | _ -> assert false @@ -421,12 +421,12 @@ let mk_Z n = (* size of bivectors are either N.of_nat (length l) or an N *) let mk_bvsize n = - let c, args = Structures.decompose_app n in - if Structures.eq_constr c (Lazy.force cof_nat) then + let c, args = CoqInterface.decompose_app n in + if CoqInterface.eq_constr c (Lazy.force cof_nat) then match args with | [nl] -> - let c, args = Structures.decompose_app nl in - if Structures.eq_constr c (Lazy.force clength) then + let c, args = CoqInterface.decompose_app nl in + if CoqInterface.eq_constr c (Lazy.force clength) then match args with | [_; l] -> List.length (mk_bool_list l) | _ -> assert false @@ -437,7 +437,7 @@ let mk_bvsize n = (** Switches between constr and OCaml *) (* Transform a option constr into a constr option *) let option_of_constr_option co = - let c, args = Structures.decompose_app co in + let c, args = CoqInterface.decompose_app co in if c = Lazy.force cSome then match args with | [_;c] -> Some c @@ -448,7 +448,7 @@ let option_of_constr_option co = (* Transform a tuple of constr into a (reversed) list of constr *) let list_of_constr_tuple = let rec list_of_constr_tuple acc t = - let c, args = Structures.decompose_app t in + let c, args = CoqInterface.decompose_app t in if c = Lazy.force cpair then match args with | [_;_;t1;t2] -> diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index 282f8f6..92acbb6 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -10,258 +10,258 @@ (**************************************************************************) -val gen_constant : string list list -> string -> Structures.constr lazy_t +val gen_constant : string list list -> string -> CoqInterface.constr lazy_t (* Int63 *) -val cint : Structures.constr lazy_t -val ceq63 : Structures.constr lazy_t +val cint : CoqInterface.constr lazy_t +val ceq63 : CoqInterface.constr lazy_t (* PArray *) -val carray : Structures.constr lazy_t +val carray : CoqInterface.constr lazy_t (* nat *) -val cnat : Structures.constr lazy_t -val cO : Structures.constr lazy_t -val cS : Structures.constr lazy_t +val cnat : CoqInterface.constr lazy_t +val cO : CoqInterface.constr lazy_t +val cS : CoqInterface.constr lazy_t (* Positive *) -val cpositive : Structures.constr lazy_t -val cxI : Structures.constr lazy_t -val cxO : Structures.constr lazy_t -val cxH : Structures.constr lazy_t -val ceqbP : Structures.constr lazy_t +val cpositive : CoqInterface.constr lazy_t +val cxI : CoqInterface.constr lazy_t +val cxO : CoqInterface.constr lazy_t +val cxH : CoqInterface.constr lazy_t +val ceqbP : CoqInterface.constr lazy_t (* N *) -val cN : Structures.constr lazy_t -val cN0 : Structures.constr lazy_t -val cNpos : Structures.constr lazy_t -val cof_nat : Structures.constr lazy_t +val cN : CoqInterface.constr lazy_t +val cN0 : CoqInterface.constr lazy_t +val cNpos : CoqInterface.constr lazy_t +val cof_nat : CoqInterface.constr lazy_t (* Z *) -val cZ : Structures.constr lazy_t -val cZ0 : Structures.constr lazy_t -val cZpos : Structures.constr lazy_t -val cZneg : Structures.constr lazy_t -val copp : Structures.constr lazy_t -val cadd : Structures.constr lazy_t -val csub : Structures.constr lazy_t -val cmul : Structures.constr lazy_t -val cltb : Structures.constr lazy_t -val cleb : Structures.constr lazy_t -val cgeb : Structures.constr lazy_t -val cgtb : Structures.constr lazy_t -val ceqbZ : Structures.constr lazy_t +val cZ : CoqInterface.constr lazy_t +val cZ0 : CoqInterface.constr lazy_t +val cZpos : CoqInterface.constr lazy_t +val cZneg : CoqInterface.constr lazy_t +val copp : CoqInterface.constr lazy_t +val cadd : CoqInterface.constr lazy_t +val csub : CoqInterface.constr lazy_t +val cmul : CoqInterface.constr lazy_t +val cltb : CoqInterface.constr lazy_t +val cleb : CoqInterface.constr lazy_t +val cgeb : CoqInterface.constr lazy_t +val cgtb : CoqInterface.constr lazy_t +val ceqbZ : CoqInterface.constr lazy_t (* Booleans *) -val cbool : Structures.constr lazy_t -val ctrue : Structures.constr lazy_t -val cfalse : Structures.constr lazy_t -val candb : Structures.constr lazy_t -val corb : Structures.constr lazy_t -val cxorb : Structures.constr lazy_t -val cnegb : Structures.constr lazy_t -val cimplb : Structures.constr lazy_t -val ceqb : Structures.constr lazy_t -val cifb : Structures.constr lazy_t -val ciff : Structures.constr lazy_t -val creflect : Structures.constr lazy_t +val cbool : CoqInterface.constr lazy_t +val ctrue : CoqInterface.constr lazy_t +val cfalse : CoqInterface.constr lazy_t +val candb : CoqInterface.constr lazy_t +val corb : CoqInterface.constr lazy_t +val cxorb : CoqInterface.constr lazy_t +val cnegb : CoqInterface.constr lazy_t +val cimplb : CoqInterface.constr lazy_t +val ceqb : CoqInterface.constr lazy_t +val cifb : CoqInterface.constr lazy_t +val ciff : CoqInterface.constr lazy_t +val creflect : CoqInterface.constr lazy_t (* Lists *) -val clist : Structures.constr lazy_t -val cnil : Structures.constr lazy_t -val ccons : Structures.constr lazy_t -val clength : Structures.constr lazy_t +val clist : CoqInterface.constr lazy_t +val cnil : CoqInterface.constr lazy_t +val ccons : CoqInterface.constr lazy_t +val clength : CoqInterface.constr lazy_t (* Option *) -val coption : Structures.constr lazy_t -val cSome : Structures.constr lazy_t -val cNone : Structures.constr lazy_t +val coption : CoqInterface.constr lazy_t +val cSome : CoqInterface.constr lazy_t +val cNone : CoqInterface.constr lazy_t (* Pairs *) -val cpair : Structures.constr lazy_t -val cprod : Structures.constr lazy_t +val cpair : CoqInterface.constr lazy_t +val cprod : CoqInterface.constr lazy_t (* Dependent pairs *) -val csigT : Structures.constr lazy_t +val csigT : CoqInterface.constr lazy_t (* Logical Operators *) -val cnot : Structures.constr lazy_t -val ceq : Structures.constr lazy_t -val crefl_equal : Structures.constr lazy_t -val cconj : Structures.constr lazy_t -val cand : Structures.constr lazy_t +val cnot : CoqInterface.constr lazy_t +val ceq : CoqInterface.constr lazy_t +val crefl_equal : CoqInterface.constr lazy_t +val cconj : CoqInterface.constr lazy_t +val cand : CoqInterface.constr lazy_t (* Bit vectors *) -val cbitvector : Structures.constr lazy_t -val cof_bits : Structures.constr lazy_t -val cbitOf : Structures.constr lazy_t -val cbv_eq : Structures.constr lazy_t -val cbv_not : Structures.constr lazy_t -val cbv_neg : Structures.constr lazy_t -val cbv_and : Structures.constr lazy_t -val cbv_or : Structures.constr lazy_t -val cbv_xor : Structures.constr lazy_t -val cbv_add : Structures.constr lazy_t -val cbv_mult : Structures.constr lazy_t -val cbv_ult : Structures.constr lazy_t -val cbv_slt : Structures.constr lazy_t -val cbv_concat : Structures.constr lazy_t -val cbv_extr : Structures.constr lazy_t -val cbv_zextn : Structures.constr lazy_t -val cbv_sextn : Structures.constr lazy_t -val cbv_shl : Structures.constr lazy_t -val cbv_shr : Structures.constr lazy_t +val cbitvector : CoqInterface.constr lazy_t +val cof_bits : CoqInterface.constr lazy_t +val cbitOf : CoqInterface.constr lazy_t +val cbv_eq : CoqInterface.constr lazy_t +val cbv_not : CoqInterface.constr lazy_t +val cbv_neg : CoqInterface.constr lazy_t +val cbv_and : CoqInterface.constr lazy_t +val cbv_or : CoqInterface.constr lazy_t +val cbv_xor : CoqInterface.constr lazy_t +val cbv_add : CoqInterface.constr lazy_t +val cbv_mult : CoqInterface.constr lazy_t +val cbv_ult : CoqInterface.constr lazy_t +val cbv_slt : CoqInterface.constr lazy_t +val cbv_concat : CoqInterface.constr lazy_t +val cbv_extr : CoqInterface.constr lazy_t +val cbv_zextn : CoqInterface.constr lazy_t +val cbv_sextn : CoqInterface.constr lazy_t +val cbv_shl : CoqInterface.constr lazy_t +val cbv_shr : CoqInterface.constr lazy_t (* Arrays *) -val cfarray : Structures.constr lazy_t -val cselect : Structures.constr lazy_t -val cstore : Structures.constr lazy_t -val cdiff : Structures.constr lazy_t -val cequalarray : Structures.constr lazy_t +val cfarray : CoqInterface.constr lazy_t +val cselect : CoqInterface.constr lazy_t +val cstore : CoqInterface.constr lazy_t +val cdiff : CoqInterface.constr lazy_t +val cequalarray : CoqInterface.constr lazy_t (* OrderedType *) (* SMT_terms *) -val cState_C_t : Structures.constr lazy_t -val cState_S_t : Structures.constr lazy_t - -val cdistinct : Structures.constr lazy_t - -val ctype : Structures.constr lazy_t -val cTZ : Structures.constr lazy_t -val cTbool : Structures.constr lazy_t -val cTpositive : Structures.constr lazy_t -val cTBV : Structures.constr lazy_t -val cTFArray : Structures.constr lazy_t -val cTindex : Structures.constr lazy_t - -val cinterp_t : Structures.constr lazy_t -val cdec_interp : Structures.constr lazy_t -val cord_interp : Structures.constr lazy_t -val ccomp_interp : Structures.constr lazy_t -val cinh_interp : Structures.constr lazy_t - -val cinterp_eqb : Structures.constr lazy_t - -val ctyp_compdec : Structures.constr lazy_t -val cTyp_compdec : Structures.constr lazy_t -val cunit_typ_compdec : Structures.constr lazy_t -val cte_carrier : Structures.constr lazy_t -val cte_compdec : Structures.constr lazy_t -val ceqb_of_compdec : Structures.constr lazy_t -val cCompDec : Structures.constr lazy_t - -val cbool_compdec : Structures.constr lazy_t -val cZ_compdec : Structures.constr lazy_t -val cPositive_compdec : Structures.constr lazy_t -val cBV_compdec : Structures.constr lazy_t -val cFArray_compdec : Structures.constr lazy_t - -val ctval : Structures.constr lazy_t -val cTval : Structures.constr lazy_t - -val cCO_xH : Structures.constr lazy_t -val cCO_Z0 : Structures.constr lazy_t -val cCO_BV : Structures.constr lazy_t - -val cUO_xO : Structures.constr lazy_t -val cUO_xI : Structures.constr lazy_t -val cUO_Zpos : Structures.constr lazy_t -val cUO_Zneg : Structures.constr lazy_t -val cUO_Zopp : Structures.constr lazy_t -val cUO_BVbitOf : Structures.constr lazy_t -val cUO_BVnot : Structures.constr lazy_t -val cUO_BVneg : Structures.constr lazy_t -val cUO_BVextr : Structures.constr lazy_t -val cUO_BVzextn : Structures.constr lazy_t -val cUO_BVsextn : Structures.constr lazy_t - -val cBO_Zplus : Structures.constr lazy_t -val cBO_Zminus : Structures.constr lazy_t -val cBO_Zmult : Structures.constr lazy_t -val cBO_Zlt : Structures.constr lazy_t -val cBO_Zle : Structures.constr lazy_t -val cBO_Zge : Structures.constr lazy_t -val cBO_Zgt : Structures.constr lazy_t -val cBO_eq : Structures.constr lazy_t -val cBO_BVand : Structures.constr lazy_t -val cBO_BVor : Structures.constr lazy_t -val cBO_BVxor : Structures.constr lazy_t -val cBO_BVadd : Structures.constr lazy_t -val cBO_BVmult : Structures.constr lazy_t -val cBO_BVult : Structures.constr lazy_t -val cBO_BVslt : Structures.constr lazy_t -val cBO_BVconcat : Structures.constr lazy_t -val cBO_BVshl : Structures.constr lazy_t -val cBO_BVshr : Structures.constr lazy_t -val cBO_select : Structures.constr lazy_t -val cBO_diffarray : Structures.constr lazy_t - -val cTO_store : Structures.constr lazy_t - -val cNO_distinct : Structures.constr lazy_t - -val catom : Structures.constr lazy_t -val cAcop : Structures.constr lazy_t -val cAuop : Structures.constr lazy_t -val cAbop : Structures.constr lazy_t -val cAtop : Structures.constr lazy_t -val cAnop : Structures.constr lazy_t -val cAapp : Structures.constr lazy_t - -val cform : Structures.constr lazy_t -val cFatom : Structures.constr lazy_t -val cFtrue : Structures.constr lazy_t -val cFfalse : Structures.constr lazy_t -val cFnot2 : Structures.constr lazy_t -val cFand : Structures.constr lazy_t -val cFor : Structures.constr lazy_t -val cFxor : Structures.constr lazy_t -val cFimp : Structures.constr lazy_t -val cFiff : Structures.constr lazy_t -val cFite : Structures.constr lazy_t -val cFbbT : Structures.constr lazy_t - -val cis_true : Structures.constr lazy_t - -val cvalid_sat_checker : Structures.constr lazy_t -val cinterp_var_sat_checker : Structures.constr lazy_t +val cState_C_t : CoqInterface.constr lazy_t +val cState_S_t : CoqInterface.constr lazy_t + +val cdistinct : CoqInterface.constr lazy_t + +val ctype : CoqInterface.constr lazy_t +val cTZ : CoqInterface.constr lazy_t +val cTbool : CoqInterface.constr lazy_t +val cTpositive : CoqInterface.constr lazy_t +val cTBV : CoqInterface.constr lazy_t +val cTFArray : CoqInterface.constr lazy_t +val cTindex : CoqInterface.constr lazy_t + +val cinterp_t : CoqInterface.constr lazy_t +val cdec_interp : CoqInterface.constr lazy_t +val cord_interp : CoqInterface.constr lazy_t +val ccomp_interp : CoqInterface.constr lazy_t +val cinh_interp : CoqInterface.constr lazy_t + +val cinterp_eqb : CoqInterface.constr lazy_t + +val ctyp_compdec : CoqInterface.constr lazy_t +val cTyp_compdec : CoqInterface.constr lazy_t +val cunit_typ_compdec : CoqInterface.constr lazy_t +val cte_carrier : CoqInterface.constr lazy_t +val cte_compdec : CoqInterface.constr lazy_t +val ceqb_of_compdec : CoqInterface.constr lazy_t +val cCompDec : CoqInterface.constr lazy_t + +val cbool_compdec : CoqInterface.constr lazy_t +val cZ_compdec : CoqInterface.constr lazy_t +val cPositive_compdec : CoqInterface.constr lazy_t +val cBV_compdec : CoqInterface.constr lazy_t +val cFArray_compdec : CoqInterface.constr lazy_t + +val ctval : CoqInterface.constr lazy_t +val cTval : CoqInterface.constr lazy_t + +val cCO_xH : CoqInterface.constr lazy_t +val cCO_Z0 : CoqInterface.constr lazy_t +val cCO_BV : CoqInterface.constr lazy_t + +val cUO_xO : CoqInterface.constr lazy_t +val cUO_xI : CoqInterface.constr lazy_t +val cUO_Zpos : CoqInterface.constr lazy_t +val cUO_Zneg : CoqInterface.constr lazy_t +val cUO_Zopp : CoqInterface.constr lazy_t +val cUO_BVbitOf : CoqInterface.constr lazy_t +val cUO_BVnot : CoqInterface.constr lazy_t +val cUO_BVneg : CoqInterface.constr lazy_t +val cUO_BVextr : CoqInterface.constr lazy_t +val cUO_BVzextn : CoqInterface.constr lazy_t +val cUO_BVsextn : CoqInterface.constr lazy_t + +val cBO_Zplus : CoqInterface.constr lazy_t +val cBO_Zminus : CoqInterface.constr lazy_t +val cBO_Zmult : CoqInterface.constr lazy_t +val cBO_Zlt : CoqInterface.constr lazy_t +val cBO_Zle : CoqInterface.constr lazy_t +val cBO_Zge : CoqInterface.constr lazy_t +val cBO_Zgt : CoqInterface.constr lazy_t +val cBO_eq : CoqInterface.constr lazy_t +val cBO_BVand : CoqInterface.constr lazy_t +val cBO_BVor : CoqInterface.constr lazy_t +val cBO_BVxor : CoqInterface.constr lazy_t +val cBO_BVadd : CoqInterface.constr lazy_t +val cBO_BVmult : CoqInterface.constr lazy_t +val cBO_BVult : CoqInterface.constr lazy_t +val cBO_BVslt : CoqInterface.constr lazy_t +val cBO_BVconcat : CoqInterface.constr lazy_t +val cBO_BVshl : CoqInterface.constr lazy_t +val cBO_BVshr : CoqInterface.constr lazy_t +val cBO_select : CoqInterface.constr lazy_t +val cBO_diffarray : CoqInterface.constr lazy_t + +val cTO_store : CoqInterface.constr lazy_t + +val cNO_distinct : CoqInterface.constr lazy_t + +val catom : CoqInterface.constr lazy_t +val cAcop : CoqInterface.constr lazy_t +val cAuop : CoqInterface.constr lazy_t +val cAbop : CoqInterface.constr lazy_t +val cAtop : CoqInterface.constr lazy_t +val cAnop : CoqInterface.constr lazy_t +val cAapp : CoqInterface.constr lazy_t + +val cform : CoqInterface.constr lazy_t +val cFatom : CoqInterface.constr lazy_t +val cFtrue : CoqInterface.constr lazy_t +val cFfalse : CoqInterface.constr lazy_t +val cFnot2 : CoqInterface.constr lazy_t +val cFand : CoqInterface.constr lazy_t +val cFor : CoqInterface.constr lazy_t +val cFxor : CoqInterface.constr lazy_t +val cFimp : CoqInterface.constr lazy_t +val cFiff : CoqInterface.constr lazy_t +val cFite : CoqInterface.constr lazy_t +val cFbbT : CoqInterface.constr lazy_t + +val cis_true : CoqInterface.constr lazy_t + +val cvalid_sat_checker : CoqInterface.constr lazy_t +val cinterp_var_sat_checker : CoqInterface.constr lazy_t val make_certif_ops : string list list -> - Structures.constr array option -> - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t + CoqInterface.constr array option -> + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * + CoqInterface.constr lazy_t * CoqInterface.constr lazy_t (* Some constructions *) -val ceq_refl_true : Structures.constr lazy_t -val eq_refl_true : unit -> Structures.constr -val vm_cast_true_no_check : Structures.constr -> Structures.constr -val vm_cast_true : Environ.env -> Structures.constr -> Structures.constr -val mkNat : int -> Structures.constr -val mkN : int -> Structures.constr -val mk_bv_list : bool list -> Structures.constr +val ceq_refl_true : CoqInterface.constr lazy_t +val eq_refl_true : unit -> CoqInterface.constr +val vm_cast_true_no_check : CoqInterface.constr -> CoqInterface.constr +val vm_cast_true : Environ.env -> CoqInterface.constr -> CoqInterface.constr +val mkNat : int -> CoqInterface.constr +val mkN : int -> CoqInterface.constr +val mk_bv_list : bool list -> CoqInterface.constr (* Reification *) -val mk_bool : Structures.constr -> bool -val mk_bool_list : Structures.constr -> bool list -val mk_nat : Structures.constr -> int -val mk_N : Structures.constr -> int -val mk_Z : Structures.constr -> int -val mk_bvsize : Structures.constr -> int +val mk_bool : CoqInterface.constr -> bool +val mk_bool_list : CoqInterface.constr -> bool list +val mk_nat : CoqInterface.constr -> int +val mk_N : CoqInterface.constr -> int +val mk_Z : CoqInterface.constr -> int +val mk_bvsize : CoqInterface.constr -> int (* Switches between constr and OCaml *) -val option_of_constr_option : Structures.constr -> Structures.constr option -val list_of_constr_tuple : Structures.constr -> Structures.constr list +val option_of_constr_option : CoqInterface.constr -> CoqInterface.constr option +val list_of_constr_tuple : CoqInterface.constr -> CoqInterface.constr list diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml index 6ffd752..0296c88 100644 --- a/src/trace/satAtom.ml +++ b/src/trace/satAtom.ml @@ -27,7 +27,7 @@ module Atom = type reify_tbl = { mutable count : int; - tbl : (Structures.constr, int) Hashtbl.t + tbl : (CoqInterface.constr, int) Hashtbl.t } let create () = @@ -51,7 +51,7 @@ module Atom = t let interp_tbl reify = - Structures.mkArray (Lazy.force cbool, atom_tbl reify) + CoqInterface.mkArray (Lazy.force cbool, atom_tbl reify) let logic _ = SL.empty diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli index b6a8dea..311b147 100644 --- a/src/trace/satAtom.mli +++ b/src/trace/satAtom.mli @@ -23,13 +23,13 @@ module Atom : sig type reify_tbl = { mutable count : int; - tbl : (Structures.constr, t) Hashtbl.t; + tbl : (CoqInterface.constr, t) Hashtbl.t; } val create : unit -> reify_tbl - val declare : reify_tbl -> Structures.constr -> t - val get : reify_tbl -> Structures.constr -> t - val atom_tbl : reify_tbl -> Structures.constr array - val interp_tbl : reify_tbl -> Structures.constr + val declare : reify_tbl -> CoqInterface.constr -> t + val get : reify_tbl -> CoqInterface.constr -> t + val atom_tbl : reify_tbl -> CoqInterface.constr array + val interp_tbl : reify_tbl -> CoqInterface.constr end diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 2710eb2..78f2eee 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -85,7 +85,7 @@ type nop = type op_def = { tparams : SmtBtype.btype array; tres : SmtBtype.btype; - op_val : Structures.constr } + op_val : CoqInterface.constr } type index = Index of int | Rel_name of string @@ -97,14 +97,14 @@ let destruct s (i, hval) = match i with | Rel_name _ -> failwith s let dummy_indexed_op i dom codom = - (i, {tparams = dom; tres = codom; op_val = Structures.mkProp}) + (i, {tparams = dom; tres = codom; op_val = CoqInterface.mkProp}) let indexed_op_index i = let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in index let debruijn_indexed_op i ty = - (Index i, {tparams = [||]; tres = ty; op_val = Structures.mkRel i}) + (Index i, {tparams = [||]; tres = ty; op_val = CoqInterface.mkRel i}) module Op = struct @@ -357,7 +357,7 @@ module Op = (* reify table *) type reify_tbl = { mutable count : int; - tbl : (Structures.constr, indexed_op) Hashtbl.t + tbl : (CoqInterface.constr, indexed_op) Hashtbl.t } let create () = @@ -385,7 +385,7 @@ module Op = let index, hval = destruct "destruct on a Rel: called by set in interp_tbl" op in t.(index) <- mk_Tval hval.tparams hval.tres hval.op_val in Hashtbl.iter set reify.tbl; - Structures.mkArray (tval, t) + CoqInterface.mkArray (tval, t) let to_list reify = let set _ op acc = @@ -713,7 +713,7 @@ module Atom = to_smt_atom (atom h) and to_smt_atom = function - | Acop (CO_BV bv) -> if List.length bv = 0 then Structures.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv + | Acop (CO_BV bv) -> if List.length bv = 0 then CoqInterface.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv | Acop _ as a -> to_smt_int fmt (compute_int a) | Auop (op,h) -> to_smt_uop op h | Abop (op,h1,h2) -> to_smt_bop op h1 h2 @@ -740,7 +740,7 @@ module Atom = Array.iter (fun bt -> SmtBtype.to_smt fmt bt; Format.fprintf fmt " ") bta; Format.fprintf fmt ") ( "; SmtBtype.to_smt fmt bt; - Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Structures.pr_constr t)) + Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (CoqInterface.pr_constr t)) and to_smt_uop op h = match op with @@ -1107,8 +1107,8 @@ module Atom = else CCunknown_deps (gobble_of_coq_cst cc) with Not_found -> CCunknown in - let rec mk_hatom (h : Structures.constr) = - let c, args = Structures.decompose_app h in + let rec mk_hatom (h : CoqInterface.constr) = + let c, args = CoqInterface.decompose_app h in match get_cst c with | CCxH -> mk_cop CCxH args | CCZ0 -> mk_cop CCZ0 args @@ -1150,9 +1150,9 @@ module Atom = | CCselect -> mk_bop_select args | CCdiff -> mk_bop_diff args | CCstore -> mk_top_store args - | CCunknown -> mk_unknown c args (Structures.retyping_get_type_of env sigma h) + | CCunknown -> mk_unknown c args (CoqInterface.retyping_get_type_of env sigma h) | CCunknown_deps gobble -> - mk_unknown_deps c args (Structures.retyping_get_type_of env sigma h) gobble + mk_unknown_deps c args (CoqInterface.retyping_get_type_of env sigma h) gobble and mk_cop op args = match op, args with @@ -1343,10 +1343,10 @@ module Atom = let rec collect_types = function | [] -> ([],[]) | x::xs as l -> - let ty = Structures.retyping_get_type_of env sigma x in + let ty = CoqInterface.retyping_get_type_of env sigma x in if Constr.iskind ty || - let c, _ = Structures.decompose_app ty in - Structures.eq_constr c (Lazy.force cCompDec) + let c, _ = CoqInterface.decompose_app ty in + CoqInterface.eq_constr c (Lazy.force cCompDec) then let (l1, l2) = collect_types xs in (x::l1, l2) @@ -1365,10 +1365,10 @@ module Atom = with | Not_found -> let targs = Array.map type_of hargs in let tres = SmtBtype.of_coq rt known_logic ty in - let os = if Structures.isRel c then - let i = Structures.destRel c in - let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in - Some (Structures.string_of_name n) + let os = if CoqInterface.isRel c then + let i = CoqInterface.destRel c in + let n, _ = CoqInterface.destruct_rel_decl (Environ.lookup_rel i env) in + Some (CoqInterface.string_of_name n) else if Vars.closed0 c then None else @@ -1391,7 +1391,7 @@ module Atom = [gobble] *) and mk_unknown_deps c args ty gobble = let deps, args = split_list_at gobble args in - let c = Structures.mkApp (c, Array.of_list deps) in + let c = CoqInterface.mkApp (c, Array.of_list deps) in mk_unknown c args ty in @@ -1432,7 +1432,7 @@ module Atom = let interp_tbl reify = let t = to_array reify (Lazy.force dft_atom) a_to_coq in - Structures.mkArray (Lazy.force catom, t) + CoqInterface.mkArray (Lazy.force catom, t) (** Producing a Coq term corresponding to the interpretation of an atom *) @@ -1444,12 +1444,12 @@ module Atom = let pc = match atom a with | Acop c -> Op.interp_cop c - | Auop (op,h) -> Structures.mkApp (Op.interp_uop op, [|interp_atom h|]) + | Auop (op,h) -> CoqInterface.mkApp (Op.interp_uop op, [|interp_atom h|]) | Abop (op,h1,h2) -> - Structures.mkApp (Op.interp_bop t_i op, + CoqInterface.mkApp (Op.interp_bop t_i op, [|interp_atom h1; interp_atom h2|]) | Atop (op,h1,h2,h3) -> - Structures.mkApp (Op.interp_top t_i op, + CoqInterface.mkApp (Op.interp_top t_i op, [|interp_atom h1; interp_atom h2; interp_atom h3|]) | Anop (NO_distinct ty as op,ha) -> let cop = Op.interp_nop t_i op in @@ -1457,9 +1457,9 @@ module Atom = let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in - Structures.mkApp (cop,[|cargs|]) + CoqInterface.mkApp (cop,[|cargs|]) | Aapp (op,t) -> - Structures.mkApp ((snd op).op_val, Array.map interp_atom t) in + CoqInterface.mkApp ((snd op).op_val, Array.map interp_atom t) in Hashtbl.add atom_tbl l pc; pc in interp_atom a diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index 645a638..27737ff 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -76,14 +76,14 @@ module Op : val create : unit -> reify_tbl - val declare : reify_tbl -> Structures.constr -> btype array -> + val declare : reify_tbl -> CoqInterface.constr -> btype array -> btype -> string option -> indexed_op - val of_coq : reify_tbl -> Structures.constr -> indexed_op + val of_coq : reify_tbl -> CoqInterface.constr -> indexed_op - val interp_tbl : Structures.constr -> - (btype array -> btype -> Structures.constr -> Structures.constr) -> - reify_tbl -> Structures.constr + val interp_tbl : CoqInterface.constr -> + (btype array -> btype -> CoqInterface.constr -> CoqInterface.constr) -> + reify_tbl -> CoqInterface.constr val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list @@ -142,18 +142,18 @@ module Atom : (** Given a coq term, build the corresponding atom *) exception UnknownUnderForall val of_coq : ?eqsym:bool -> SmtBtype.reify_tbl -> Op.reify_tbl -> - reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t + reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> CoqInterface.constr -> t - val get_coq_term_op : int -> Structures.constr + val get_coq_term_op : int -> CoqInterface.constr - val to_coq : t -> Structures.constr + val to_coq : t -> CoqInterface.constr val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array - val interp_tbl : reify_tbl -> Structures.constr + val interp_tbl : reify_tbl -> CoqInterface.constr - val interp_to_coq : Structures.constr -> (int, Structures.constr) Hashtbl.t -> - t -> Structures.constr + val interp_to_coq : CoqInterface.constr -> (int, CoqInterface.constr) Hashtbl.t -> + t -> CoqInterface.constr val logic : t -> SmtMisc.logic @@ -201,5 +201,5 @@ module Trace : sig end -val make_t_i : SmtBtype.reify_tbl -> Structures.constr -val make_t_func : Op.reify_tbl -> Structures.constr -> Structures.constr +val make_t_i : SmtBtype.reify_tbl -> CoqInterface.constr +val make_t_func : Op.reify_tbl -> CoqInterface.constr -> CoqInterface.constr diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index 3b6d107..c9aad70 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -19,7 +19,7 @@ type uninterpreted_type = (* Uninterpreted type for which a CompDec is already known The constr is of type typ_compdec *) - | CompDec of Structures.constr + | CompDec of CoqInterface.constr (* Uninterpreted type for which the knowledge of a CompDec is delayed until either: - one is used @@ -27,11 +27,11 @@ type uninterpreted_type = via a cut The constr is of type Type *) - | Delayed of Structures.constr + | Delayed of CoqInterface.constr type indexed_type = uninterpreted_type gen_hashed -let dummy_indexed_type i = {index = i; hval = Delayed (Structures.mkProp)} +let dummy_indexed_type i = {index = i; hval = Delayed (CoqInterface.mkProp)} let indexed_type_index i = i.index let indexed_type_compdec i = match i.hval with @@ -105,8 +105,8 @@ let rec logic = function (* reify table *) type reify_tbl = { mutable count : int; - tbl : (Structures.constr, btype) Hashtbl.t; - mutable cuts : (Structures.id * Structures.types) list; + tbl : (CoqInterface.constr, btype) Hashtbl.t; + mutable cuts : (CoqInterface.id * CoqInterface.types) list; unsup_tbl : (btype, btype) Hashtbl.t; } @@ -145,8 +145,8 @@ let interp_tbl reify = | CompDec compdec -> t.(it.index) <- compdec; Some bt | Delayed ty -> let n = string_of_int (List.length reify.cuts) in - let compdec_name = Structures.mkId ("CompDec"^n) in - let compdec_var = Structures.mkVar compdec_name in + let compdec_name = CoqInterface.mkId ("CompDec"^n) in + let compdec_var = CoqInterface.mkVar compdec_name in let compdec_type = mklApp cCompDec [| ty |] in reify.cuts <- (compdec_name, compdec_type) :: reify.cuts; let ce = mklApp cTyp_compdec [|ty; compdec_var|] in @@ -156,7 +156,7 @@ let interp_tbl reify = | _ -> Some bt in Hashtbl.filter_map_inplace set reify.tbl; - Structures.mkArray (Lazy.force ctyp_compdec, t) + CoqInterface.mkArray (Lazy.force ctyp_compdec, t) let to_list reify = @@ -241,8 +241,8 @@ let rec compdec_btype reify = function | Tindex i -> (match i.hval with | CompDec compdec -> - let c, args = Structures.decompose_app compdec in - if Structures.eq_constr c (Lazy.force cTyp_compdec) then + let c, args = CoqInterface.decompose_app compdec in + if CoqInterface.eq_constr c (Lazy.force cTyp_compdec) then match args with | [_; tic] -> tic | _ -> assert false @@ -264,22 +264,22 @@ let declare_and_compdec reify t ty = let rec of_coq reify known_logic t = try - let c, args = Structures.decompose_app t in - if Structures.eq_constr c (Lazy.force cbool) || - Structures.eq_constr c (Lazy.force cTbool) then Tbool - else if Structures.eq_constr c (Lazy.force cZ) || - Structures.eq_constr c (Lazy.force cTZ) then + let c, args = CoqInterface.decompose_app t in + if CoqInterface.eq_constr c (Lazy.force cbool) || + CoqInterface.eq_constr c (Lazy.force cTbool) then Tbool + else if CoqInterface.eq_constr c (Lazy.force cZ) || + CoqInterface.eq_constr c (Lazy.force cTZ) then check_known TZ known_logic - else if Structures.eq_constr c (Lazy.force cpositive) || - Structures.eq_constr c (Lazy.force cTpositive) then + else if CoqInterface.eq_constr c (Lazy.force cpositive) || + CoqInterface.eq_constr c (Lazy.force cTpositive) then check_known Tpositive known_logic - else if Structures.eq_constr c (Lazy.force cbitvector) || - Structures.eq_constr c (Lazy.force cTBV) then + else if CoqInterface.eq_constr c (Lazy.force cbitvector) || + CoqInterface.eq_constr c (Lazy.force cTBV) then match args with | [s] -> check_known (TBV (mk_bvsize s)) known_logic | _ -> assert false - else if Structures.eq_constr c (Lazy.force cfarray) || - Structures.eq_constr c (Lazy.force cTFArray) then + else if CoqInterface.eq_constr c (Lazy.force cfarray) || + CoqInterface.eq_constr c (Lazy.force cTFArray) then match args with | ti :: te :: _ -> let ty = TFArray (of_coq reify known_logic ti, diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli index ec73d21..7060ab6 100644 --- a/src/trace/smtBtype.mli +++ b/src/trace/smtBtype.mli @@ -17,7 +17,7 @@ type indexed_type val dummy_indexed_type: int -> indexed_type val indexed_type_index : indexed_type -> int -val indexed_type_compdec : indexed_type -> Structures.constr +val indexed_type_compdec : indexed_type -> CoqInterface.constr type btype = | TZ @@ -31,7 +31,7 @@ val indexed_type_of_int : int -> indexed_type module HashedBtype : Hashtbl.HashedType with type t = btype -val to_coq : btype -> Structures.constr +val to_coq : btype -> CoqInterface.constr val to_smt : Format.formatter -> btype -> unit @@ -40,25 +40,25 @@ type reify_tbl val create : unit -> reify_tbl val copy : reify_tbl -> reify_tbl -val of_coq : reify_tbl -> logic -> Structures.constr -> btype -val of_coq_compdec : reify_tbl -> Structures.constr -> Structures.constr -> btype +val of_coq : reify_tbl -> logic -> CoqInterface.constr -> btype +val of_coq_compdec : reify_tbl -> CoqInterface.constr -> CoqInterface.constr -> btype -val get_coq_type_op : int -> Structures.constr +val get_coq_type_op : int -> CoqInterface.constr -val interp_tbl : reify_tbl -> Structures.constr +val interp_tbl : reify_tbl -> CoqInterface.constr val to_list : reify_tbl -> (int * indexed_type) list -val make_t_i : reify_tbl -> Structures.constr +val make_t_i : reify_tbl -> CoqInterface.constr -val dec_interp : Structures.constr -> btype -> Structures.constr -val ord_interp : Structures.constr -> btype -> Structures.constr -val comp_interp : Structures.constr -> btype -> Structures.constr -val inh_interp : Structures.constr -> btype -> Structures.constr -val interp : Structures.constr -> btype -> Structures.constr +val dec_interp : CoqInterface.constr -> btype -> CoqInterface.constr +val ord_interp : CoqInterface.constr -> btype -> CoqInterface.constr +val comp_interp : CoqInterface.constr -> btype -> CoqInterface.constr +val inh_interp : CoqInterface.constr -> btype -> CoqInterface.constr +val interp : CoqInterface.constr -> btype -> CoqInterface.constr -val interp_to_coq : reify_tbl -> btype -> Structures.constr +val interp_to_coq : reify_tbl -> btype -> CoqInterface.constr -val get_cuts : reify_tbl -> (Structures.id * Structures.types) list +val get_cuts : reify_tbl -> (CoqInterface.id * CoqInterface.types) list val logic : btype -> logic diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml index 2ea4ca8..24cdf78 100644 --- a/src/trace/smtCertif.ml +++ b/src/trace/smtCertif.ml @@ -98,11 +98,11 @@ type 'hform rule = *) (* Linear arithmetic *) - | LiaMicromega of 'hform list * Structures.Micromega_plugin_Certificate.Mc.zArithProof list + | LiaMicromega of 'hform list * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list | LiaDiseq of 'hform (* Arithmetic simplifications *) - | SplArith of 'hform clause * 'hform * Structures.Micromega_plugin_Certificate.Mc.zArithProof list + | SplArith of 'hform clause * 'hform * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list (* Elimination of operators *) | SplDistinctElim of 'hform clause * 'hform diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli index 7da3097..bc2da38 100644 --- a/src/trace/smtCertif.mli +++ b/src/trace/smtCertif.mli @@ -96,11 +96,11 @@ type 'hform rule = *) (* Linear arithmetic *) - | LiaMicromega of 'hform list * Structures.Micromega_plugin_Certificate.Mc.zArithProof list + | LiaMicromega of 'hform list * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list | LiaDiseq of 'hform (* Arithmetic simplifications *) - | SplArith of 'hform clause * 'hform * Structures.Micromega_plugin_Certificate.Mc.zArithProof list + | SplArith of 'hform clause * 'hform * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list (* Elimination of operators *) | SplDistinctElim of 'hform clause * 'hform diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index fa2a56b..e655a9d 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -115,7 +115,7 @@ let interp_conseq_uf t_i (prem, concl) = let tf = Hashtbl.create 17 in let rec interp = function | [] -> mklApp cis_true [|interp_uf t_i ta tf concl|] - | c::prem -> Structures.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in + | c::prem -> CoqInterface.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in interp prem @@ -127,26 +127,26 @@ let print_assm ty = let parse_certif 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 = Structures.mkConst (Structures.declare_constant t_i ce5) in + let ce5 = CoqInterface.mkUConst t_i' in + let ct_i = CoqInterface.mkConst (CoqInterface.declare_constant t_i ce5) in let t_func' = make_t_func ro ct_i in - let ce6 = Structures.mkUConst t_func' in - let ct_func = Structures.mkConst (Structures.declare_constant t_func ce6) in + let ce6 = CoqInterface.mkUConst t_func' in + let ct_func = CoqInterface.mkConst (CoqInterface.declare_constant t_func ce6) in let t_atom' = Atom.interp_tbl ra in - let ce1 = Structures.mkUConst t_atom' in - let ct_atom = Structures.mkConst (Structures.declare_constant t_atom ce1) in + let ce1 = CoqInterface.mkUConst t_atom' in + let ct_atom = CoqInterface.mkConst (CoqInterface.declare_constant t_atom ce1) in let t_form' = snd (Form.interp_tbl rf) in - let ce2 = Structures.mkUConst t_form' in - let ct_form = Structures.mkConst (Structures.declare_constant t_form ce2) in + let ce2 = CoqInterface.mkUConst t_form' in + let ct_form = CoqInterface.mkConst (CoqInterface.declare_constant t_form ce2) in (* EMPTY LEMMA LIST *) 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 + let _ = CoqInterface.declare_new_variable v ty in print_assm ty ) cuts; @@ -155,22 +155,22 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, 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 + CoqInterface.mkArray (Lazy.force cint, res) in let used_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 roots in - let _ = Structures.declare_constant root ce3 in - let ce3' = Structures.mkUConst used_roots in - let _ = Structures.declare_constant used_root ce3' in + mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.mkArray (Lazy.force cint, res)|] in + let ce3 = CoqInterface.mkUConst roots in + let _ = CoqInterface.declare_constant root ce3 in + let ce3' = CoqInterface.mkUConst used_roots in + let _ = CoqInterface.declare_constant used_root ce3' 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 _ = Structures.declare_constant trace ce4 in + let ce4 = CoqInterface.mkUConst certif in + let _ = CoqInterface.declare_constant trace ce4 in () @@ -184,15 +184,15 @@ let interp_roots t_i roots = | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots let theorem name (rt, ro, ra, rf, roots, max_id, confl) = - let nti = Structures.mkName "t_i" in - let ntfunc = Structures.mkName "t_func" in - let ntatom = Structures.mkName "t_atom" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in - let nused_roots = Structures.mkName "used_roots" in - let nd = Structures.mkName "d" in + let nti = CoqInterface.mkName "t_i" in + let ntfunc = CoqInterface.mkName "t_func" in + let ntatom = CoqInterface.mkName "t_atom" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in + let nused_roots = CoqInterface.mkName "used_roots" in + let nd = CoqInterface.mkName "d" in - let v = Structures.mkRel in + let v = CoqInterface.mkRel in let t_i = make_t_i rt in let t_func = make_t_func ro (v 1 (*t_i*)) in @@ -204,7 +204,7 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) = (interp_conseq_uf t_i) (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in List.iter (fun (v,ty) -> - let _ = Structures.declare_new_variable v ty in + let _ = CoqInterface.declare_new_variable v ty in print_assm ty ) cuts; @@ -217,59 +217,59 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) = 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 + mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.mkArray (Lazy.force cint, res)|] in let rootsCstr = 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 + CoqInterface.mkArray (Lazy.force cint, res) in let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in let theorem_proof_cast = - Structures.mkCast ( - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + CoqInterface.mkCast ( + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], + CoqInterface.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker_correct [|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*); vm_cast_true_no_check (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*)|])|]))))))), - Structures.vmcast, + CoqInterface.vmcast, theorem_concl) in let theorem_proof_nocast = - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], + CoqInterface.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker_correct [|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 ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_concl in - let _ = Structures.declare_constant name ce in + let ce = CoqInterface.mkTConst theorem_proof_cast theorem_proof_nocast theorem_concl in + let _ = CoqInterface.declare_constant name ce in () (* Given an SMT-LIB2 file and a certif, call the checker *) let checker (rt, ro, ra, rf, roots, max_id, confl) = - let nti = Structures.mkName "t_i" in - let ntfunc = Structures.mkName "t_func" in - let ntatom = Structures.mkName "t_atom" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in - let nused_roots = Structures.mkName "used_roots" in - let nd = Structures.mkName "d" in + let nti = CoqInterface.mkName "t_i" in + let ntfunc = CoqInterface.mkName "t_func" in + let ntatom = CoqInterface.mkName "t_atom" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in + let nused_roots = CoqInterface.mkName "used_roots" in + let nd = CoqInterface.mkName "d" in - let v = Structures.mkRel in + let v = CoqInterface.mkRel in let t_i = make_t_i rt in let t_func = make_t_func ro (v 1 (*t_i*)) in @@ -281,7 +281,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) = (interp_conseq_uf t_i) (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in List.iter (fun (v,ty) -> - let _ = Structures.declare_new_variable v ty in + let _ = CoqInterface.declare_new_variable v ty in print_assm ty ) cuts; @@ -294,26 +294,26 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) = 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 + mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.mkArray (Lazy.force cint, res)|] in let rootsCstr = 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 + CoqInterface.mkArray (Lazy.force cint, res) in let tm = - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], + CoqInterface.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 = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in + let res = CoqInterface.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in Format.eprintf " = %s\n : bool@." - (if Structures.eq_constr res (Lazy.force CoqTerms.ctrue) then + (if CoqInterface.eq_constr res (Lazy.force CoqTerms.ctrue) then "true" else "false") let count_used confl = @@ -329,15 +329,15 @@ let count_used confl = let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = - let nti = Structures.mkName "t_i" in - let ntfunc = Structures.mkName "t_func" in - let ntatom = Structures.mkName "t_atom" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in - let nused_roots = Structures.mkName "used_roots" in - let nd = Structures.mkName "d" in + let nti = CoqInterface.mkName "t_i" in + let ntfunc = CoqInterface.mkName "t_func" in + let ntatom = CoqInterface.mkName "t_atom" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in + let nused_roots = CoqInterface.mkName "used_roots" in + let nd = CoqInterface.mkName "d" in - let v = Structures.mkRel in + let v = CoqInterface.mkRel in let t_i = make_t_i rt in let t_func = make_t_func ro (v 1 (*t_i*)) in @@ -349,7 +349,7 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in List.iter (fun (v,ty) -> - let _ = Structures.declare_new_variable v ty in + let _ = CoqInterface.declare_new_variable v ty in print_assm ty ) cuts; @@ -364,84 +364,84 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = 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 + CoqInterface.mkArray (Lazy.force cint, res)|] in let rootsCstr = 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 + CoqInterface.mkArray (Lazy.force cint, res) in let tm = - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Structures.mkLetIn (nused_roots, used_rootsCstr, + CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + CoqInterface.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], 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 = Structures.cbv_vm (Global.env ()) tm + let res = CoqInterface.cbv_vm (Global.env ()) tm (mklApp coption [|mklApp cprod [|Lazy.force cnat; Lazy.force cname_step|]|]) in - match Structures.decompose_app res with - | c, _ when Structures.eq_constr c (Lazy.force cNone) -> - Structures.error ("Debug checker is only meant to be used for certificates \ + match CoqInterface.decompose_app res with + | c, _ when CoqInterface.eq_constr c (Lazy.force cNone) -> + CoqInterface.error ("Debug checker is only meant to be used for certificates \ that fail to be checked by SMTCoq.") - | c, [_; n] when Structures.eq_constr c (Lazy.force cSome) -> - (match Structures.decompose_app n with - | c, [_; _; cnb; cn] when Structures.eq_constr c (Lazy.force cpair) -> - let n = fst (Structures.decompose_app cn) in + | c, [_; n] when CoqInterface.eq_constr c (Lazy.force cSome) -> + (match CoqInterface.decompose_app n with + | c, [_; _; cnb; cn] when CoqInterface.eq_constr c (Lazy.force cpair) -> + let n = fst (CoqInterface.decompose_app cn) in let name = - if Structures.eq_constr n (Lazy.force cName_Res ) then "Res" - else if Structures.eq_constr n (Lazy.force cName_Weaken) then "Weaken" - else if Structures.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten" - else if Structures.eq_constr n (Lazy.force cName_CTrue) then "CTrue" - else if Structures.eq_constr n (Lazy.force cName_CFalse ) then "CFalse" - else if Structures.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef" - else if Structures.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2" - else if Structures.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj" - else if Structures.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef" - else if Structures.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2" - else if Structures.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj" - else if Structures.eq_constr n (Lazy.force cName_EqTr ) then "EqTr" - else if Structures.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr" - else if Structures.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP" - else if Structures.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega" - else if Structures.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq" - else if Structures.eq_constr n (Lazy.force cName_SplArith) then "SplArith" - else if Structures.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim" - else if Structures.eq_constr n (Lazy.force cName_BBVar) then "BBVar" - else if Structures.eq_constr n (Lazy.force cName_BBConst) then "BBConst" - else if Structures.eq_constr n (Lazy.force cName_BBOp) then "BBOp" - else if Structures.eq_constr n (Lazy.force cName_BBNot) then "BBNot" - else if Structures.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg" - else if Structures.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd" - else if Structures.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat" - else if Structures.eq_constr n (Lazy.force cName_BBMul) then "BBMul" - else if Structures.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt" - else if Structures.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt" - else if Structures.eq_constr n (Lazy.force cName_BBEq) then "BBEq" - else if Structures.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq" - else if Structures.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract" - else if Structures.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend" - else if Structures.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend" - else if Structures.eq_constr n (Lazy.force cName_BBShl) then "BBShl" - else if Structures.eq_constr n (Lazy.force cName_BBShr) then "BBShr" - else if Structures.eq_constr n (Lazy.force cName_RowEq) then "RowEq" - else if Structures.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq" - else if Structures.eq_constr n (Lazy.force cName_Ext) then "Ext" - else if Structures.eq_constr n (Lazy.force cName_Hole) then "Hole" + if CoqInterface.eq_constr n (Lazy.force cName_Res ) then "Res" + else if CoqInterface.eq_constr n (Lazy.force cName_Weaken) then "Weaken" + else if CoqInterface.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten" + else if CoqInterface.eq_constr n (Lazy.force cName_CTrue) then "CTrue" + else if CoqInterface.eq_constr n (Lazy.force cName_CFalse ) then "CFalse" + else if CoqInterface.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef" + else if CoqInterface.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2" + else if CoqInterface.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj" + else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef" + else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2" + else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj" + else if CoqInterface.eq_constr n (Lazy.force cName_EqTr ) then "EqTr" + else if CoqInterface.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr" + else if CoqInterface.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP" + else if CoqInterface.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega" + else if CoqInterface.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq" + else if CoqInterface.eq_constr n (Lazy.force cName_SplArith) then "SplArith" + else if CoqInterface.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim" + else if CoqInterface.eq_constr n (Lazy.force cName_BBVar) then "BBVar" + else if CoqInterface.eq_constr n (Lazy.force cName_BBConst) then "BBConst" + else if CoqInterface.eq_constr n (Lazy.force cName_BBOp) then "BBOp" + else if CoqInterface.eq_constr n (Lazy.force cName_BBNot) then "BBNot" + else if CoqInterface.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg" + else if CoqInterface.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd" + else if CoqInterface.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat" + else if CoqInterface.eq_constr n (Lazy.force cName_BBMul) then "BBMul" + else if CoqInterface.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt" + else if CoqInterface.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt" + else if CoqInterface.eq_constr n (Lazy.force cName_BBEq) then "BBEq" + else if CoqInterface.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq" + else if CoqInterface.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract" + else if CoqInterface.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend" + else if CoqInterface.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend" + else if CoqInterface.eq_constr n (Lazy.force cName_BBShl) then "BBShl" + else if CoqInterface.eq_constr n (Lazy.force cName_BBShr) then "BBShr" + else if CoqInterface.eq_constr n (Lazy.force cName_RowEq) then "RowEq" + else if CoqInterface.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq" + else if CoqInterface.eq_constr n (Lazy.force cName_Ext) then "Ext" + else if CoqInterface.eq_constr n (Lazy.force cName_Hole) then "Hole" else string_coq_constr n in let nb = mk_nat cnb + List.length roots + (confl.id + 1 - count_used confl) in - Structures.error ("Step number " ^ string_of_int nb ^ + CoqInterface.error ("Step number " ^ string_of_int nb ^ " (" ^ name ^ ") of the certificate likely failed.") | _ -> assert false ) @@ -450,9 +450,9 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = (* let rec of_coq_list cl = - * match Structures.decompose_app cl with - * | c, _ when Structures.eq_constr c (Lazy.force cnil) -> [] - * | c, [_; x; cr] when Structures.eq_constr c (Lazy.force ccons) -> + * match CoqInterface.decompose_app cl with + * | c, _ when CoqInterface.eq_constr c (Lazy.force cnil) -> [] + * | c, [_; x; cr] when CoqInterface.eq_constr c (Lazy.force ccons) -> * x :: of_coq_list cr * | _ -> assert false *) @@ -461,29 +461,29 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * (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 = Structures.mkConst (Structures.declare_constant t_i ce5) in + * let ce5 = CoqInterface.mkUConst t_i' in + * let ct_i = CoqInterface.mkConst (CoqInterface.declare_constant t_i ce5) in * * let t_func' = make_t_func ro ct_i in - * let ce6 = Structures.mkUConst t_func' in + * let ce6 = CoqInterface.mkUConst t_func' in * let ct_func = - * Structures.mkConst (Structures.declare_constant t_func ce6) in + * CoqInterface.mkConst (CoqInterface.declare_constant t_func ce6) in * * let t_atom' = Atom.interp_tbl ra in - * let ce1 = Structures.mkUConst t_atom' in + * let ce1 = CoqInterface.mkUConst t_atom' in * let ct_atom = - * Structures.mkConst (Structures.declare_constant t_atom ce1) in + * CoqInterface.mkConst (CoqInterface.declare_constant t_atom ce1) in * * let t_form' = snd (Form.interp_tbl rf) in - * let ce2 = Structures.mkUConst t_form' in + * let ce2 = CoqInterface.mkUConst t_form' in * let ct_form = - * Structures.mkConst (Structures.declare_constant t_form ce2) in + * CoqInterface.mkConst (CoqInterface.declare_constant t_form ce2) 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 + * let _ = CoqInterface.declare_new_variable v ty in * print_assm ty * ) cuts; * @@ -492,37 +492,37 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * 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 + * CoqInterface.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 _ = Structures.declare_constant root ce3 in - * let ce3' = Structures.mkUConst cused_roots in - * let _ = Structures.declare_constant used_root ce3' in + * CoqInterface.mkArray (Lazy.force cint, res)|] in + * let ce3 = CoqInterface.mkUConst croots in + * let _ = CoqInterface.declare_constant root ce3 in + * let ce3' = CoqInterface.mkUConst cused_roots in + * let _ = CoqInterface.declare_constant used_root ce3' 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 _ = Structures.declare_constant trace ce4 in + * let ce4 = CoqInterface.mkUConst certif in + * let _ = CoqInterface.declare_constant trace ce4 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 + * let setup = CoqInterface.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 Structures.decompose_app setup with - * | c, [_; _; s; csteps] when Structures.eq_constr c (Lazy.force cpair) -> + * let s, steps = match CoqInterface.decompose_app setup with + * | c, [_; _; s; csteps] when CoqInterface.eq_constr c (Lazy.force cpair) -> * s, of_coq_list csteps * | _ -> assert false * in @@ -536,22 +536,22 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * [| ct_i; ct_func; ct_atom; ct_form; s; step |] in * * let res = - * Structures.cbv_vm (Global.env ()) tm + * CoqInterface.cbv_vm (Global.env ()) tm * (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in * - * match Structures.decompose_app res with - * | c, [_; _; s; cbad] when Structures.eq_constr c (Lazy.force cpair) -> + * match CoqInterface.decompose_app res with + * | c, [_; _; s; cbad] when CoqInterface.eq_constr c (Lazy.force cpair) -> * if not (mk_bool cbad) then s - * else Structures.error ("Step number " ^ string_of_int !cpt ^ + * else CoqInterface.error ("Step number " ^ string_of_int !cpt ^ * " (" ^ string_coq_constr - * (fst (Structures.decompose_app step)) ^ ")" ^ + * (fst (CoqInterface.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 \ + * CoqInterface.error ("Debug checker is only meant to be used for certificates \ * that fail to be checked by SMTCoq.") *) @@ -559,16 +559,16 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = (* Tactic *) let build_body rt ro ra rf l b (max_id, confl) vm_cast find = - let nti = Structures.mkName "t_i" in - let ntfunc = Structures.mkName "t_func" in - let ntatom = Structures.mkName "t_atom" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in + let nti = CoqInterface.mkName "t_i" in + let ntfunc = CoqInterface.mkName "t_func" in + let ntatom = CoqInterface.mkName "t_atom" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in - let v = Structures.mkRel in + let v = CoqInterface.mkRel in let t_i = make_t_i rt in - let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in + let t_func = CoqInterface.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in let t_atom = Atom.interp_tbl ra in let t_form = snd (Form.interp_tbl rf) in let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq @@ -583,11 +583,11 @@ let build_body rt ro ra rf l b (max_id, confl) vm_cast find = mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let add_lets t = - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], t))))) in @@ -614,16 +614,16 @@ let build_body rt ro ra rf l b (max_id, confl) vm_cast find = let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find = - let nti = Structures.mkName "t_i" in - let ntfunc = Structures.mkName "t_func" in - let ntatom = Structures.mkName "t_atom" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in + let nti = CoqInterface.mkName "t_i" in + let ntfunc = CoqInterface.mkName "t_func" in + let ntatom = CoqInterface.mkName "t_atom" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in - let v = Structures.mkRel in + let v = CoqInterface.mkRel in let t_i = make_t_i rt in - let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i*))) in + let t_func = CoqInterface.lift 1 (make_t_func ro (v 0 (*t_i*))) in let t_atom = Atom.interp_tbl ra in let t_form = snd (Form.interp_tbl rf) in let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq @@ -633,11 +633,11 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find = mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let add_lets t = - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], t))))) in @@ -665,10 +665,10 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find = let get_arguments concl = - let f, args = Structures.decompose_app concl in + let f, args = CoqInterface.decompose_app concl in match args with - | [ty;a;b] when (Structures.eq_constr f (Lazy.force ceq)) && (Structures.eq_constr ty (Lazy.force cbool)) -> a, b - | [a] when (Structures.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue + | [ty;a;b] when (CoqInterface.eq_constr f (Lazy.force ceq)) && (CoqInterface.eq_constr ty (Lazy.force cbool)) -> a, b + | [a] when (CoqInterface.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue | _ -> failwith ("Verit.tactic: can only deal with equality over bool") @@ -689,7 +689,7 @@ let gen_rel_name = let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = let warn () = - Structures.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (Structures.extern_constr clemma)))); + CoqInterface.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (CoqInterface.extern_constr clemma)))); None in @@ -698,16 +698,16 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = let rel_context = List.map (fun rel -> Context.Rel.Declaration.set_name (Names.Name.mk_name (Names.Id.of_string (gen_rel_name ()))) rel) rel_context in let env_lemma = Environ.push_rel_context rel_context env in - let f, args = Structures.decompose_app qf_lemma in + let f, args = CoqInterface.decompose_app qf_lemma in let core_f = - if Structures.eq_constr f (Lazy.force cis_true) then + if CoqInterface.eq_constr f (Lazy.force cis_true) then match args with | [a] -> Some a | _ -> warn () - else if Structures.eq_constr f (Lazy.force ceq) then + else if CoqInterface.eq_constr f (Lazy.force ceq) then match args with - | [ty; arg1; arg2] when Structures.eq_constr ty (Lazy.force cbool) && - Structures.eq_constr arg2 (Lazy.force ctrue) -> + | [ty; arg1; arg2] when CoqInterface.eq_constr ty (Lazy.force cbool) && + CoqInterface.eq_constr arg2 (Lazy.force ctrue) -> Some arg1 | _ -> warn () else warn () in @@ -722,8 +722,8 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = | None -> None in let forall_args = - let fmap r = let n, t = Structures.destruct_rel_decl r in - Structures.string_of_name n, SmtBtype.of_coq rt solver_logic t in + let fmap r = let n, t = CoqInterface.destruct_rel_decl r in + CoqInterface.string_of_name n, SmtBtype.of_coq rt solver_logic t in List.map fmap rel_context in match forall_args with @@ -736,11 +736,11 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl env sigma concl = let a, b = get_arguments concl in - let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in + let tlcepl = List.map (CoqInterface.interp_constr env sigma) lcepl in let lcpl = lcpl @ tlcepl in let create_lemma l = - let cl = Structures.retyping_get_type_of env sigma l in + let cl = CoqInterface.retyping_get_type_of env sigma l in match of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic cl with | Some smt -> Some ((cl, l), smt) | None -> None @@ -748,7 +748,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l let l_pl_ls = SmtMisc.filter_map create_lemma lcpl in let lsmt = List.map snd l_pl_ls in - let lem_tbl : (int, Structures.constr * Structures.constr) Hashtbl.t = + let lem_tbl : (int, CoqInterface.constr * CoqInterface.constr) Hashtbl.t = Hashtbl.create 100 in let new_ref ((l, pl), ls) = Hashtbl.add lem_tbl (Form.index ls) (l, pl) in @@ -770,11 +770,11 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l | _ -> failwith "unexpected form of root" in let (body_cast, body_nocast, cuts) = - if ((Structures.eq_constr b (Lazy.force ctrue)) || - (Structures.eq_constr b (Lazy.force cfalse))) then ( + if ((CoqInterface.eq_constr b (Lazy.force ctrue)) || + (CoqInterface.eq_constr b (Lazy.force cfalse))) then ( let l = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in let _ = Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env sigma) rf_quant a in - let nl = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in + let nl = if (CoqInterface.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in let lsmt = Form.flatten rf nl :: lsmt in let max_id_confl = make_proof call_solver env rt ro ra_quant rf_quant nl lsmt in build_body rt ro ra rf (Form.to_coq l) b max_id_confl (vm_cast env) (Some find_lemma) @@ -793,19 +793,19 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l let cuts = (SmtBtype.get_cuts rt) @ cuts in List.fold_right (fun (eqn, eqt) tac -> - Structures.tclTHENLAST - (Structures.assert_before (Structures.name_of_id eqn) eqt) + CoqInterface.tclTHENLAST + (CoqInterface.assert_before (CoqInterface.name_of_id eqn) eqt) tac ) cuts - (Structures.tclTHEN - (Structures.set_evars_tac body_nocast) - (Structures.vm_cast_no_check body_cast)) + (CoqInterface.tclTHEN + (CoqInterface.set_evars_tac body_nocast) + (CoqInterface.vm_cast_no_check body_cast)) let tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl = - Structures.tclTHEN + CoqInterface.tclTHEN Tactics.intros - (Structures.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl)) + (CoqInterface.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl)) (**********************************************) @@ -822,7 +822,7 @@ let string_index_of_constr env i cf = try let s = string_coq_constr cf in let nc = Environ.named_context env in - let nd = Environ.lookup_named (Structures.mkId s) env in + let nd = Environ.lookup_named (CoqInterface.mkId s) env in let cpt = ref 0 in (try List.iter (fun n -> incr cpt; if n == nd then raise Exit) nc with Exit -> ()); @@ -832,11 +832,11 @@ let string_index_of_constr env i cf = let vstring_i env i = let cf = SmtAtom.Atom.get_coq_term_op i in - if Structures.isRel cf then - let dbi = Structures.destRel cf in + if CoqInterface.isRel cf then + let dbi = CoqInterface.destRel cf in let s = Environ.lookup_rel dbi env - |> Structures.get_rel_dec_name + |> CoqInterface.get_rel_dec_name |> SmtMisc.string_of_name_def "?" in s, dbi @@ -977,14 +977,14 @@ let model_item env rt ro ra rf = * let outf = Format.formatter_of_out_channel out in * SExpr.print outf l; pp_print_flush outf (); * close_out out; *) - Structures.error ("Could not reconstruct model") + CoqInterface.error ("Could not reconstruct model") let model env rt ro ra rf = function | List (Atom "model" :: l) -> List.fold_left (fun acc m -> match model_item env rt ro ra rf m with Fun m -> m::acc | Sort -> acc) [] l |> List.sort (fun ((_ ,i1), _) ((_, i2), _) -> i2 - i1) - | _ -> Structures.error ("No model") + | _ -> CoqInterface.error ("No model") let model_string env rt ro ra rf s = diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli index b643594..e885028 100644 --- a/src/trace/smtCommands.mli +++ b/src/trace/smtCommands.mli @@ -11,13 +11,13 @@ val parse_certif : - Structures.id -> - Structures.id -> - Structures.id -> - Structures.id -> - Structures.id -> - Structures.id -> - Structures.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify * SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> @@ -29,7 +29,7 @@ val checker_debug : SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> 'a val theorem : - Structures.id -> + CoqInterface.id -> SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify * SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> @@ -56,8 +56,8 @@ val tactic : SmtAtom.Form.reify -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> - (Environ.env -> Structures.constr -> Structures.constr) -> - Structures.constr list -> - Structures.constr_expr list -> Structures.tactic + (Environ.env -> CoqInterface.constr -> CoqInterface.constr) -> + CoqInterface.constr list -> + CoqInterface.constr_expr list -> CoqInterface.tactic val model_string : Environ.env -> SmtBtype.reify_tbl -> 'a -> 'b -> 'c -> SExpr.t -> string diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index 7f2ebd8..0a7d859 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -81,7 +81,7 @@ module type FORM = val get : ?declare:bool -> reify -> pform -> t (** Given a coq term, build the corresponding formula *) - val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t + val of_coq : (CoqInterface.constr -> hatom) -> reify -> CoqInterface.constr -> t val hash_hform : (hatom -> hatom) -> reify -> t -> t (* Flattening of [Fand] and [For], removing of [Fnot2] *) @@ -93,20 +93,20 @@ module type FORM = (** Producing Coq terms *) - val to_coq : t -> Structures.constr + val to_coq : t -> CoqInterface.constr val pform_tbl : reify -> pform array val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array - val interp_tbl : reify -> Structures.constr * Structures.constr + val interp_tbl : reify -> CoqInterface.constr * CoqInterface.constr val nvars : reify -> int (* Producing a Coq term corresponding to the interpretation of a formula *) (* [interp_atom] map [hatom] to coq term, it is better if it produce shared terms. *) val interp_to_coq : - (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t -> - t -> Structures.constr + (hatom -> CoqInterface.constr) -> (int, CoqInterface.constr) Hashtbl.t -> + t -> CoqInterface.constr (* Unstratified terms *) type atom_form_lit = @@ -368,9 +368,9 @@ module Make (Atom:ATOM) = | CCunknown module ConstrHash = struct - type t = Structures.constr - let equal = Structures.eq_constr - let hash = Structures.hash_constr + type t = CoqInterface.constr + let equal = CoqInterface.eq_constr + let hash = CoqInterface.hash_constr end module ConstrHashtbl = Hashtbl.Make(ConstrHash) @@ -393,7 +393,7 @@ module Make (Atom:ATOM) = let get_cst c = try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in let rec mk_hform h = - let c, args = Structures.decompose_app h in + let c, args = CoqInterface.decompose_app h in match get_cst c with | CCtrue -> get reify (Fapp(Ftrue,empty_args)) | CCfalse -> get reify (Fapp(Ffalse,empty_args)) @@ -408,7 +408,7 @@ module Make (Atom:ATOM) = let l1 = mk_hform b1 in let l2 = mk_hform b2 in get reify (Fapp (Fimp, [|l1;l2|])) - | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb") + | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments for implb") | CCifb -> (* We should also be able to reify if then else *) begin match args with @@ -417,7 +417,7 @@ module Make (Atom:ATOM) = let l2 = mk_hform b2 in let l3 = mk_hform b3 in get reify (Fapp (Fite, [|l1;l2;l3|])) - | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb" + | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments for ifb" end | _ -> let a = atom_of_coq h in @@ -429,13 +429,13 @@ module Make (Atom:ATOM) = let l1 = mk_hform b1 in let l2 = mk_hform b2 in get reify (f [|l1; l2|]) - | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments" + | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments" and mk_fnot i args = match args with | [t] -> - let c,args = Structures.decompose_app t in - if Structures.eq_constr c (Lazy.force cnegb) then + let c,args = CoqInterface.decompose_app t in + if CoqInterface.eq_constr c (Lazy.force cnegb) then mk_fnot (i+1) args else let q,r = i lsr 1 , i land 1 in @@ -443,31 +443,31 @@ module Make (Atom:ATOM) = let l = if r = 0 then l else neg l in if q = 0 then l else get reify (Fapp(Fnot2 q, [|l|])) - | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb" + | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for negb" and mk_fand acc args = match args with | [t1;t2] -> let l2 = mk_hform t2 in - let c, args = Structures.decompose_app t1 in - if Structures.eq_constr c (Lazy.force candb) then + let c, args = CoqInterface.decompose_app t1 in + if CoqInterface.eq_constr c (Lazy.force candb) then mk_fand (l2::acc) args else let l1 = mk_hform t1 in get reify (Fapp(Fand, Array.of_list (l1::l2::acc))) - | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb" + | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for andb" and mk_for acc args = match args with | [t1;t2] -> let l2 = mk_hform t2 in - let c, args = Structures.decompose_app t1 in - if Structures.eq_constr c (Lazy.force corb) then + let c, args = CoqInterface.decompose_app t1 in + if CoqInterface.eq_constr c (Lazy.force corb) then mk_for (l2::acc) args else let l1 = mk_hform t1 in get reify (Fapp(For, Array.of_list (l1::l2::acc))) - | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in + | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in mk_hform c @@ -546,7 +546,7 @@ module Make (Atom:ATOM) = let args_to_coq args = let cargs = Array.make (Array.length args + 1) (mkInt 0) in Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args; - Structures.mkArray (Lazy.force cint, cargs) + CoqInterface.mkArray (Lazy.force cint, cargs) let pf_to_coq = function | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|] @@ -586,7 +586,7 @@ module Make (Atom:ATOM) = let interp_tbl reify = let (i,t) = to_array reify (Lazy.force cFtrue) pf_to_coq in - (mkInt i, Structures.mkArray (Lazy.force cform, t)) + (mkInt i, CoqInterface.mkArray (Lazy.force cform, t)) let nvars reify = reify.count (* Producing a Coq term corresponding to the interpretation of a formula *) diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index 06a867f..47b4123 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -77,7 +77,7 @@ module type FORM = val get : ?declare:bool -> reify -> pform -> t (** Given a coq term, build the corresponding formula *) - val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t + val of_coq : (CoqInterface.constr -> hatom) -> reify -> CoqInterface.constr -> t val hash_hform : (hatom -> hatom) -> reify -> t -> t @@ -90,20 +90,20 @@ module type FORM = (** Producing Coq terms *) - val to_coq : t -> Structures.constr + val to_coq : t -> CoqInterface.constr val pform_tbl : reify -> pform array val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array - val interp_tbl : reify -> Structures.constr * Structures.constr + val interp_tbl : reify -> CoqInterface.constr * CoqInterface.constr val nvars : reify -> int (* Producing a Coq term corresponding to the interpretation of a formula *) (* [interp_atom] map [hatom] to coq term, it is better if it produce shared terms. *) val interp_to_coq : - (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t -> - t -> Structures.constr + (hatom -> CoqInterface.constr) -> (int, CoqInterface.constr) Hashtbl.t -> + t -> CoqInterface.constr (* Unstratified terms *) type atom_form_lit = diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index d750550..165814b 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -16,7 +16,7 @@ let cInt_tbl = Hashtbl.create 17 let mkInt i = try Hashtbl.find cInt_tbl i with Not_found -> - let ci = Structures.mkInt i in + let ci = CoqInterface.mkInt i in Hashtbl.add cInt_tbl i ci; ci @@ -25,15 +25,15 @@ type 'a gen_hashed = { index : int; hval : 'a } (** Functions over constr *) -let mklApp f args = Structures.mkApp (Lazy.force f, args) +let mklApp f args = CoqInterface.mkApp (Lazy.force f, args) -let string_of_name_def d n = try Structures.string_of_name n with | _ -> d +let string_of_name_def d n = try CoqInterface.string_of_name n with | _ -> d let string_coq_constr t = let rec fix rf x = rf (fix rf) x in let pr = fix - Ppconstr.modular_constr_pr Pp.mt Structures.ppconstr_lsimpleconstr in - Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr t)) + Ppconstr.modular_constr_pr Pp.mt CoqInterface.ppconstr_lsimpleconstr in + Pp.string_of_ppcmds (pr (CoqInterface.constrextern_extern_constr t)) (** Logics *) diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli index a6f5db8..5359c15 100644 --- a/src/trace/smtMisc.mli +++ b/src/trace/smtMisc.mli @@ -10,12 +10,12 @@ (**************************************************************************) -val cInt_tbl : (int, Structures.constr) Hashtbl.t -val mkInt : int -> Structures.constr +val cInt_tbl : (int, CoqInterface.constr) Hashtbl.t +val mkInt : int -> CoqInterface.constr type 'a gen_hashed = { index : int; hval : 'a; } -val mklApp : Structures.constr Lazy.t -> Structures.constr array -> Structures.constr -val string_of_name_def : string -> Structures.name -> string -val string_coq_constr : Structures.constr -> string +val mklApp : CoqInterface.constr Lazy.t -> CoqInterface.constr array -> CoqInterface.constr +val string_of_name_def : string -> CoqInterface.name -> string +val string_coq_constr : CoqInterface.constr -> string type logic_item = LUF | LLia | LBitvectors | LArrays module SL : Set.S with type elt = logic_item type logic = SL.t diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index 65994f9..7b68a26 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -383,7 +383,7 @@ let to_coq to_lit interp (cstep, l := tl | _ -> assert false done; - mklApp cRes [|mkInt (get_pos c); Structures.mkArray (Lazy.force cint, args)|] + mklApp cRes [|mkInt (get_pos c); CoqInterface.mkArray (Lazy.force cint, args)|] | Other other -> begin match other with | Weaken (c',l') -> @@ -412,12 +412,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_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Structures.micromega_coq_proofTerm|]) in + let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force CoqInterface.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force CoqInterface.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_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.micromega_coq_proofTerm|]) in + let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force CoqInterface.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force CoqInterface.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|] @@ -461,10 +461,10 @@ let to_coq to_lit interp (cstep, | Ext (res) -> mklApp cExt [|out_c c; out_f res|] | Hole (prem_id, concl) -> let prem = List.map (fun cl -> match cl.value with Some l -> l | None -> assert false) prem_id in - let ass_name = Structures.mkId ("ass"^(string_of_int (Hashtbl.hash concl))) in + let ass_name = CoqInterface.mkId ("ass"^(string_of_int (Hashtbl.hash concl))) in let ass_ty = interp (prem, concl) in cuts := (ass_name, ass_ty)::!cuts; - let ass_var = Structures.mkVar ass_name in + let ass_var = CoqInterface.mkVar ass_name in let prem_id' = List.fold_right (fun c l -> mklApp ccons [|Lazy.force cint; out_c c; l|]) prem_id (mklApp cnil [|Lazy.force cint|]) in let prem' = List.fold_right (fun cl l -> mklApp ccons [|Lazy.force cState_C_t; out_cl cl; l|]) prem (mklApp cnil [|Lazy.force cState_C_t|]) in let concl' = out_cl concl in @@ -474,23 +474,23 @@ let to_coq to_lit interp (cstep, | Some find -> find cl | None -> assert false in let concl' = out_cl [concl] in - let app_name = Structures.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in - let app_var = Structures.mkVar app_name in - let app_ty = Structures.mkArrow clemma (interp ([], [concl])) in + let app_name = CoqInterface.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in + let app_var = CoqInterface.mkVar app_name in + let app_ty = CoqInterface.mkArrow clemma (interp ([], [concl])) in cuts := (app_name, app_ty)::!cuts; mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|] end | _ -> assert false in let step = Lazy.force cstep in let def_step = - mklApp cRes [|mkInt 0; Structures.mkArray (Lazy.force cint, [|mkInt 0|]) |] in + mklApp cRes [|mkInt 0; CoqInterface.mkArray (Lazy.force cint, [|mkInt 0|]) |] in let r = ref confl in let nc = ref 0 in while not (isRoot !r.kind) do r := prev !r; incr nc done; let last_root = !r in (* Be careful, step_to_coq makes a side effect on cuts so it needs to be called first *) let res = - Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r + CoqInterface.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r in (res, last_root, !cuts) diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli index 2c70bbc..e79ce20 100644 --- a/src/trace/smtTrace.mli +++ b/src/trace/smtTrace.mli @@ -48,26 +48,26 @@ val alloc : 'a SmtCertif.clause -> int val naive_alloc : 'a SmtCertif.clause -> int val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int val to_coq : - ('a -> Structures.constr) -> - ('a list list * 'a list -> Structures.types) -> - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t -> + ('a -> CoqInterface.constr) -> + ('a list list * 'a list -> CoqInterface.types) -> + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t -> 'a SmtCertif.clause -> - ('a SmtCertif.clause -> Structures.types * Structures.constr) option -> - Structures.constr * 'a SmtCertif.clause * - (Structures.id * Structures.types) list + ('a SmtCertif.clause -> CoqInterface.types * CoqInterface.constr) option -> + CoqInterface.constr * 'a SmtCertif.clause * + (CoqInterface.id * CoqInterface.types) list module MakeOpt : diff --git a/src/verit/verit.ml b/src/verit/verit.ml index eed1dca..7f89943 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -193,25 +193,25 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt = if l = "warning : proof_done: status is still open" then raise Unknown else if l = "Invalid memory reference" then - Structures.warning "verit-warning" ("veriT outputted the warning: " ^ l) + CoqInterface.warning "verit-warning" ("veriT outputted the warning: " ^ l) else if n >= 7 && String.sub l 0 7 = "warning" then - Structures.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7))) + CoqInterface.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7))) else if n >= 8 && String.sub l 0 8 = "error : " then - Structures.error ("veriT failed with the error: " ^ (String.sub l 8 (n-8))) + CoqInterface.error ("veriT failed with the error: " ^ (String.sub l 8 (n-8))) else - Structures.error ("veriT failed with the error: " ^ l) + CoqInterface.error ("veriT failed with the error: " ^ l) done with End_of_file -> () in try - if exit_code <> 0 then Structures.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); + if exit_code <> 0 then CoqInterface.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); raise_warnings_errors (); let res = import_trace ra_quant rf_quant logfilename (Some first) lsmt in close_in win; Sys.remove wname; res with x -> close_in win; Sys.remove wname; match x with - | Unknown -> Structures.error "veriT returns 'unknown'" - | VeritSyntax.Sat -> Structures.error "veriT found a counter-example" + | Unknown -> CoqInterface.error "veriT returns 'unknown'" + | VeritSyntax.Sat -> CoqInterface.error "veriT found a counter-example" | _ -> raise x let verit_logic = diff --git a/src/verit/verit.mli b/src/verit/verit.mli index 0560d77..f0acd0c 100644 --- a/src/verit/verit.mli +++ b/src/verit/verit.mli @@ -11,13 +11,13 @@ val parse_certif : - Structures.id -> - Structures.id -> - Structures.id -> - Structures.id -> - Structures.id -> Structures.id -> Structures.id -> string -> string -> unit + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> CoqInterface.id -> CoqInterface.id -> string -> string -> unit val checker : string -> string -> unit val checker_debug : string -> string -> unit -val theorem : Structures.id -> string -> string -> unit -val tactic : EConstr.t -> Structures.constr_expr list -> Structures.tactic -val tactic_no_check : EConstr.t -> Structures.constr_expr list -> Structures.tactic +val theorem : CoqInterface.id -> string -> string -> unit +val tactic : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic +val tactic_no_check : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index 21c10e8..c5db594 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -493,7 +493,7 @@ let mk_clause (id,typ,value,ids_params) = let mk_clause cl = try mk_clause cl with Failure f -> - Structures.error ("SMTCoq was not able to check the certificate \ + CoqInterface.error ("SMTCoq was not able to check the certificate \ for the following reason.\n"^f) let apply_dec f (decl, a) = decl, f a diff --git a/src/versions/native/Make b/src/versions/native/Make deleted file mode 100644 index e278c82..0000000 --- a/src/versions/native/Make +++ /dev/null @@ -1,171 +0,0 @@ -######################################################################## -## This file is intended to developers, please do not use it to ## -## generate a Makefile, rather use the provided Makefile. ## -######################################################################## - - - - -######################################################################## -## To generate the Makefile: ## -## coq_makefile -f Make -o Makefile ## -## In the Makefile : ## -## 1) Suppress the "Makefile" target ## -## 2) Change the "all" target into: ## -## all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) ## -## 3) Change the "install-natdynlink" target: ## -## change CMXSFILES into CMXS and add the same block for CMXA and VCMXS. ## -## 4) Change the "install" target: change CMOFILES into CMXFILES. ## -## 5) Add to the "clean" target: ## -## - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a ## -######################################################################## - - --R . SMTCoq - --I bva --I classes --I array --I cnf --I euf --I lfsc --I lia --I smtlib2 --I trace --I verit --I zchaff --I versions/native --I ../3rdparty/alt-ergo - - --custom "cd ../unit-tests; make vernac" "" "test" --custom "cd ../unit-tests; make zchaffv" "" "ztest" --custom "cd ../unit-tests; make veritv" "" "vtest" - --custom "$(CAMLLEX) $<" "%.mll" "%.ml" --custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli" --custom "" "verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml" "ml" - --custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx trace/smtMaps.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx" "$(CMXA)" --custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)" - -CMXA = smtcoq.cmxa -CMXS = smtcoq_plugin.cmxs -VCMXS = "versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs classes/NSMTCoq_SMT_classes.cmxs classes/NSMTCoq_SMT_classes_instances.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_Tactics.cmxs NSMTCoq_Conversion_tactics.cmxs NSMTCoq_PropToBool.cmxs NSMTCoq_BoolToProp.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi classes/NSMTCoq_SMT_classes.cmi classes/NSMTCoq_SMT_classes_instances.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_Tactics.cmi NSMTCoq_Conversion_tactics.cmi NSMTCoq_PropToBool.cmi NSMTCoq_BoolToProp.cmi NSMTCoq_SMTCoq.cmi" -CAMLLEX = $(CAMLBIN)ocamllex -CAMLYACC = $(CAMLBIN)ocamlyacc - -bva/BVList.v -bva/Bva_checker.v - -classes/SMT_classes.v -classes/SMT_classes_instances.v - -array/FArray.v -array/Array_checker.v - -versions/native/Structures.v -versions/native/structures.ml -versions/native/structures.mli - -trace/coqTerms.ml -trace/coqTerms.mli -trace/satAtom.ml -trace/satAtom.mli -trace/smtAtom.ml -trace/smtAtom.mli -trace/smtBtype.ml -trace/smtBtype.mli -trace/smtCertif.ml -trace/smtCertif.mli -trace/smtCnf.ml -trace/smtCnf.mli -trace/smtCommands.ml -trace/smtCommands.mli -trace/smtForm.ml -trace/smtForm.mli -trace/smtMaps.ml -trace/smtMaps.mli -trace/smtMisc.ml -trace/smtMisc.mli -trace/smtTrace.ml -trace/smtTrace.mli - -../3rdparty/alt-ergo/smtlib2_parse.ml -../3rdparty/alt-ergo/smtlib2_parse.mli -../3rdparty/alt-ergo/smtlib2_lex.ml -../3rdparty/alt-ergo/smtlib2_lex.mli -../3rdparty/alt-ergo/smtlib2_ast.ml -../3rdparty/alt-ergo/smtlib2_ast.mli -../3rdparty/alt-ergo/smtlib2_util.ml -../3rdparty/alt-ergo/smtlib2_util.mli - -smtlib2/smtlib2_genConstr.ml -smtlib2/smtlib2_genConstr.mli -smtlib2/sExprParser.ml -smtlib2/sExprParser.mli -smtlib2/sExprLexer.ml -smtlib2/sExpr.ml -smtlib2/sExpr.mli -smtlib2/smtlib2_solver.ml -smtlib2/smtlib2_solver.mli - -verit/veritParser.ml -verit/veritParser.mli -verit/veritLexer.ml -verit/veritLexer.mli -verit/verit.ml -verit/verit.mli -verit/veritSyntax.ml -verit/veritSyntax.mli - -lfsc/shashcons.mli -lfsc/shashcons.ml -lfsc/hstring.mli -lfsc/hstring.ml -lfsc/lfscParser.ml -lfsc/lfscLexer.ml -lfsc/type.ml -lfsc/ast.ml -lfsc/ast.mli -lfsc/translator_sig.mli -lfsc/builtin.ml -lfsc/tosmtcoq.ml -lfsc/tosmtcoq.mli -lfsc/converter.ml -lfsc/lfsc.ml - -zchaff/cnfParser.ml -zchaff/cnfParser.mli -zchaff/satParser.ml -zchaff/satParser.mli -zchaff/zchaff.ml -zchaff/zchaff.mli -zchaff/zchaffParser.ml -zchaff/zchaffParser.mli - -cnf/Cnf.v - -euf/Euf.v - -lia/lia.ml -lia/lia.mli -lia/Lia.v - -spl/Assumptions.v -spl/Syntactic.v -spl/Arithmetic.v -spl/Operators.v - -Conversion_tactics.v -Misc.v -SMTCoq.v -ReflectFacts.v -PropToBool.v -BoolToProp.v -Tactics.v -SMT_terms.v -State.v -Trace.v - -smtcoq_plugin.ml4 diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile deleted file mode 100644 index aaaab9e..0000000 --- a/src/versions/native/Makefile +++ /dev/null @@ -1,505 +0,0 @@ -############################################################################# -## v # The Coq Proof Assistant ## -## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## -## \VV/ # ## -## // # Makefile automagically generated by coq_makefile Vtrunk ## -############################################################################# - -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING - -# -# This Makefile was generated by the command line : -# coq_makefile -f Make -o Makefile -# - -.DEFAULT_GOAL := all - -# -# This Makefile may take arguments passed as environment variables: -# COQBIN to specify the directory where Coq binaries resides; -# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc; -# DSTROOT to specify a prefix to install path. - -# Here is a hack to make $(eval $(shell works: -define donewline - - -endef -includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr '\n' '@'; }))) -$(call includecmdwithout@,$(COQBIN)coqtop -config) - -########################## -# # -# Libraries definitions. # -# # -########################## - -OCAMLLIBS?=-I ../3rdparty/alt-ergo\ - -I versions/native\ - -I zchaff\ - -I verit\ - -I trace\ - -I smtlib2\ - -I lia\ - -I lfsc\ - -I euf\ - -I cnf\ - -I array\ - -I classes\ - -I bva -COQLIBS?=-I ../3rdparty/alt-ergo\ - -I versions/native\ - -I zchaff\ - -I verit\ - -I trace\ - -I smtlib2\ - -I lia\ - -I lfsc\ - -I euf\ - -I cnf\ - -I array\ - -I classes\ - -I bva -R . SMTCoq -COQDOCLIBS?=-R . SMTCoq - -########################## -# # -# Variables definitions. # -# # -########################## - -CAMLYACC=$(CAMLBIN)ocamlyacc -CAMLLEX=$(CAMLBIN)ocamllex -VCMXS=versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs classes/NSMTCoq_SMT_classes.cmxs classes/NSMTCoq_SMT_classes_instances.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_Tactics.cmxs NSMTCoq_Conversion_tactics.cmxs NSMTCoq_PropToBool.cmxs NSMTCoq_BoolToProp.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi classes/NSMTCoq_SMT_classes.cmi classes/NSMTCoq_SMT_classes_instances.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_Tactics.cmi NSMTCoq_Conversion_tactics.cmi NSMTCoq_PropToBool.cmi NSMTCoq_BoolToProp.cmi NSMTCoq_SMTCoq.cmi -CMXS=smtcoq_plugin.cmxs -CMXA=smtcoq.cmxa - -OPT?= -COQDEP?=$(COQBIN)coqdep -c -COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) -COQCHKFLAGS?=-silent -o -COQDOCFLAGS?=-interpolate -utf8 -COQC?=$(COQBIN)coqc -GALLINA?=$(COQBIN)gallina -COQDOC?=$(COQBIN)coqdoc -COQCHK?=$(COQBIN)coqchk - -COQSRCLIBS?=-I $(COQLIB)kernel -I $(COQLIB)lib \ - -I $(COQLIB)library -I $(COQLIB)parsing \ - -I $(COQLIB)pretyping -I $(COQLIB)interp \ - -I $(COQLIB)proofs -I $(COQLIB)tactics \ - -I $(COQLIB)toplevel \ - -I $(COQLIB)plugins/btauto \ - -I $(COQLIB)plugins/cc \ - -I $(COQLIB)plugins/decl_mode \ - -I $(COQLIB)plugins/extraction \ - -I $(COQLIB)plugins/field \ - -I $(COQLIB)plugins/firstorder \ - -I $(COQLIB)plugins/fourier \ - -I $(COQLIB)plugins/funind \ - -I $(COQLIB)plugins/micromega \ - -I $(COQLIB)plugins/nsatz \ - -I $(COQLIB)plugins/omega \ - -I $(COQLIB)plugins/quote \ - -I $(COQLIB)plugins/ring \ - -I $(COQLIB)plugins/romega \ - -I $(COQLIB)plugins/rtauto \ - -I $(COQLIB)plugins/setoid_ring \ - -I $(COQLIB)plugins/syntax \ - -I $(COQLIB)plugins/xml -ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) - -CAMLC?=$(OCAMLC) -c -rectypes -CAMLOPTC?=$(OCAMLOPT) -c -rectypes -CAMLLINK?=$(OCAMLC) -rectypes -CAMLOPTLINK?=$(OCAMLOPT) -rectypes -GRAMMARS?=grammar.cma -CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo -CAMLP4OPTIONS?=-loc loc -PP?=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl" - -################## -# # -# Install Paths. # -# # -################## - -ifdef USERINSTALL -XDG_DATA_HOME?=$(HOME)/.local/share -COQLIBINSTALL=$(XDG_DATA_HOME)/coq -COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq -else -COQLIBINSTALL=${COQLIB}user-contrib -COQDOCINSTALL=${DOCDIR}user-contrib -endif - -###################### -# # -# Files dispatching. # -# # -###################### - -VFILES:=Trace.v\ - State.v\ - SMT_terms.v\ - Tactics.v\ - BoolToProp.v\ - PropToBool.v\ - ReflectFacts.v\ - SMTCoq.v\ - Misc.v\ - Conversion_tactics.v\ - spl/Operators.v\ - spl/Arithmetic.v\ - spl/Syntactic.v\ - spl/Assumptions.v\ - lia/Lia.v\ - euf/Euf.v\ - cnf/Cnf.v\ - versions/native/Structures.v\ - array/Array_checker.v\ - array/FArray.v\ - classes/SMT_classes_instances.v\ - classes/SMT_classes.v\ - bva/Bva_checker.v\ - bva/BVList.v - --include $(addsuffix .d,$(VFILES)) -.SECONDARY: $(addsuffix .d,$(VFILES)) - -vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),$(addprefix $(dir $(vo)),$(filter-out Warning: Error:,$(firstword $(shell $(COQBIN)coqtop -batch -quiet -print-mod-uid $(vo:.vo=))))))) -VOFILES:=$(foreach vo,$(VFILES:.v=.vo),$(dir $(vo))$(notdir $(vo))) -GLOBFILES:=$(VFILES:.v=.glob) -VIFILES:=$(VFILES:.v=.vi) -GFILES:=$(VFILES:.v=.g) -HTMLFILES:=$(VFILES:.v=.html) -GHTMLFILES:=$(VFILES:.v=.g.html) -OBJFILES:=$(call vo_to_obj,$(VOFILES)) -ML4FILES:=smtcoq_plugin.ml4 - --include $(addsuffix .d,$(ML4FILES)) -.SECONDARY: $(addsuffix .d,$(ML4FILES)) - -MLFILES:=lia/lia.ml\ - zchaff/zchaffParser.ml\ - zchaff/zchaff.ml\ - zchaff/satParser.ml\ - zchaff/cnfParser.ml\ - lfsc/lfsc.ml\ - lfsc/converter.ml\ - lfsc/tosmtcoq.ml\ - lfsc/builtin.ml\ - lfsc/ast.ml\ - lfsc/type.ml\ - lfsc/lfscLexer.ml\ - lfsc/lfscParser.ml\ - lfsc/hstring.ml\ - lfsc/shashcons.ml\ - verit/veritSyntax.ml\ - verit/verit.ml\ - verit/veritLexer.ml\ - verit/veritParser.ml\ - smtlib2/smtlib2_solver.ml\ - smtlib2/sExpr.ml\ - smtlib2/sExprLexer.ml\ - smtlib2/sExprParser.ml\ - smtlib2/smtlib2_genConstr.ml\ - ../3rdparty/alt-ergo/smtlib2_util.ml\ - ../3rdparty/alt-ergo/smtlib2_ast.ml\ - ../3rdparty/alt-ergo/smtlib2_lex.ml\ - ../3rdparty/alt-ergo/smtlib2_parse.ml\ - trace/smtTrace.ml\ - trace/smtMisc.ml\ - trace/smtMaps.ml\ - trace/smtForm.ml\ - trace/smtCommands.ml\ - trace/smtCnf.ml\ - trace/smtCertif.ml\ - trace/smtBtype.ml\ - trace/smtAtom.ml\ - trace/satAtom.ml\ - trace/coqTerms.ml\ - versions/native/structures.ml - --include $(addsuffix .d,$(MLFILES)) -.SECONDARY: $(addsuffix .d,$(MLFILES)) - -MLIFILES:=lia/lia.mli\ - zchaff/zchaffParser.mli\ - zchaff/zchaff.mli\ - zchaff/satParser.mli\ - zchaff/cnfParser.mli\ - lfsc/tosmtcoq.mli\ - lfsc/translator_sig.mli\ - lfsc/ast.mli\ - lfsc/hstring.mli\ - lfsc/shashcons.mli\ - verit/veritSyntax.mli\ - verit/verit.mli\ - verit/veritLexer.mli\ - verit/veritParser.mli\ - smtlib2/smtlib2_solver.mli\ - smtlib2/sExpr.mli\ - smtlib2/sExprParser.mli\ - smtlib2/smtlib2_genConstr.mli\ - ../3rdparty/alt-ergo/smtlib2_util.mli\ - ../3rdparty/alt-ergo/smtlib2_ast.mli\ - ../3rdparty/alt-ergo/smtlib2_lex.mli\ - ../3rdparty/alt-ergo/smtlib2_parse.mli\ - trace/smtTrace.mli\ - trace/smtMisc.mli\ - trace/smtMaps.mli\ - trace/smtForm.mli\ - trace/smtCommands.mli\ - trace/smtCnf.mli\ - trace/smtCertif.mli\ - trace/smtBtype.mli\ - trace/smtAtom.mli\ - trace/satAtom.mli\ - trace/coqTerms.mli\ - versions/native/structures.mli - --include $(addsuffix .d,$(MLIFILES)) -.SECONDARY: $(addsuffix .d,$(MLIFILES)) - -ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) -CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES)) -CMXFILES=$(CMOFILES:.cmo=.cmx) -CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi)) -CMXSFILES=$(CMXFILES:.cmx=.cmxs) - -####################################### -# # -# Definition of the toplevel targets. # -# # -####################################### - -all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) - -mlihtml: $(MLIFILES:.mli=.cmi) - mkdir $@ || rm -rf $@/* - $(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) - -all-mli.tex: $(MLIFILES:.mli=.cmi) - $(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) - -spec: $(VIFILES) - -gallina: $(GFILES) - -html: $(GLOBFILES) $(VFILES) - - mkdir -p html - $(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES) - -gallinahtml: $(GLOBFILES) $(VFILES) - - mkdir -p html - $(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES) - -all.ps: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -all-gal.ps: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -all.pdf: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -all-gal.pdf: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -validate: $(VOFILES) - $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=)) - -beautify: $(VFILES:=.beautified) - for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done - @echo 'Do not do "make clean" until you are sure that everything went well!' - @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' - -.PHONY: all opt byte archclean clean install userinstall depend html validate - -################### -# # -# Custom targets. # -# # -################### - -$(CMXS): $(CMXA) - $(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^ - -$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx trace/smtMaps.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx - $(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^ - -ml: verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml - - -%.ml %.mli: %.mly - $(CAMLYACC) $< - -%.ml: %.mll - $(CAMLLEX) $< - -vtest: - cd ../unit-tests; make veritv - -ztest: - cd ../unit-tests; make zchaffv - -test: - cd ../unit-tests; make vernac - -#################### -# # -# Special targets. # -# # -#################### - -byte: - $(MAKE) all "OPT:=-byte" - -opt: - $(MAKE) all "OPT:=-opt" - -userinstall: - +$(MAKE) USERINSTALL=true install - -install-natdynlink: - for i in $(CMXS); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - for i in $(CMXA); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - for i in $(VCMXS); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - -install:$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink) - for i in $(VOFILES) $(OBJFILES) $(OBJFILES:.o=.cm*); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - for i in $(CMXFILES); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - for i in $(CMIFILES); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - -install-doc: - install -d $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/html - for i in html/*; do \ - install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/$$i;\ - done - install -d $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/mlihtml - for i in mlihtml/*; do \ - install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/$$i;\ - done - -clean: - rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES) - rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a) - rm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES)) - rm -f $(OBJFILES) $(OBJFILES:.o=.native) - rm -f $(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) - rm -f $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs) - rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) - rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex - - rm -rf html mlihtml - - rm -rf $(CMXS) - - rm -rf $(CMXA) - - rm -rf ml - - rm -rf vtest - - rm -rf ztest - - rm -rf test - - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a - -archclean: - rm -f *.cmx *.o - -printenv: - @$(COQBIN)coqtop -config - @echo CAMLC = $(CAMLC) - @echo CAMLOPTC = $(CAMLOPTC) - @echo PP = $(PP) - @echo COQFLAGS = $(COQFLAGS) - @echo COQLIBINSTALL = $(COQLIBINSTALL) - @echo COQDOCINSTALL = $(COQDOCINSTALL) - - -################### -# # -# Implicit rules. # -# # -################### - -%.cmi: %.mli - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -%.mli.d: %.mli - $(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.cmo: %.ml4 - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -%.cmx: %.ml4 - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -%.ml4.d: %.ml4 - $(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.cmo: %.ml - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -%.cmx: %.ml - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $< - -%.ml.d: %.ml - $(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.cmxs: %.cmx - $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $< - -%.vo %.glob: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $* - -%.vi: %.v - $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* - -%.g: %.v - $(GALLINA) $< - -%.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ - -%.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ - -%.g.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ - -%.g.html: %.v %.glob - $(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@ - -%.v.d: %.v - $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.v.beautified: - $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $* - -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING - diff --git a/src/versions/native/Structures_native.v b/src/versions/native/Structures_native.v deleted file mode 100644 index 47ae21f..0000000 --- a/src/versions/native/Structures_native.v +++ /dev/null @@ -1,59 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -Require Import PArray. - - -Section Trace. - - (* We use [array array step] to allow bigger trace *) - Definition trace (step:Type) := array (array step). - - Definition trace_to_list {step:Type} (t:trace step) : list step := - PArray.fold_left (fun res a => List.app res (PArray.to_list a)) nil t. - - Definition trace_length {step:Type} (t:trace step) : int := - PArray.fold_left (fun l a => (l + (length a))%int63) 0%int63 t. - - Definition trace_get {step:Type} (t:trace step) (i:int) : step := - snd (PArray.fold_left (fun (jres:(option int) * step) a => - let (j,res) := jres in - match j with - | Some j' => - let l := length a in - if (j' < l)%int63 then - (None, get a j') - else - ((Some ((j' - l)%int63)),res) - | None => (None,res) - end - ) (Some i, (get (get t 0) 0)) t). - - Definition trace_fold {state step:Type} (transition: state -> step -> state) (s0:state) (t:trace step) := - PArray.fold_left (PArray.fold_left transition) s0 t. - - Lemma trace_fold_ind (state step : Type) (P : state -> Prop) (transition : state -> step -> state) (t : trace step) - (IH: forall (s0 : state) (i : int), (i < trace_length t)%int63 = true -> P s0 -> P (transition s0 (trace_get t i))) : - forall s0 : state, P s0 -> P (trace_fold transition s0 t). - Proof. - apply PArray.fold_left_ind. - intros a i Hi Ha. - apply PArray.fold_left_ind;trivial. - intros a0 i0 Hi0 Ha0. (* IH applied to a0 and (sum of the lengths of the first i arrays + i0) *) - Admitted. - -End Trace. - - -Definition nat_eqb := beq_nat. -Definition nat_eqb_eq := beq_nat_true_iff. -Definition nat_eqb_refl := NPeano.Nat.eqb_refl. diff --git a/src/versions/native/Tactics_native.v b/src/versions/native/Tactics_native.v deleted file mode 100644 index 45d3603..0000000 --- a/src/versions/native/Tactics_native.v +++ /dev/null @@ -1,55 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -Require Import Psatz. - -Declare ML Module "smtcoq_plugin". - - - -Tactic Notation "verit_bool" constr_list(h) := - fail "Tactics are not supported with native-coq". - -Tactic Notation "verit_bool_no_check" constr_list(h) := - fail "Tactics are not supported with native-coq". - - -(** Tactics in Prop **) - -Ltac zchaff := - fail "Tactics are not supported with native-coq". -Ltac zchaff_no_check := - fail "Tactics are not supported with native-coq". - -Tactic Notation "verit" constr_list(h) := - fail "Tactics are not supported with native-coq". -Tactic Notation "verit_no_check" constr_list(h) := - fail "Tactics are not supported with native-coq". - -Ltac cvc4 := - fail "Tactics are not supported with native-coq". -Ltac cvc4_no_check := - fail "Tactics are not supported with native-coq". - - -Tactic Notation "smt" constr_list(h) := - fail "Tactics are not supported with native-coq". -Tactic Notation "smt_no_check" constr_list(h) := - fail "Tactics are not supported with native-coq". - - - -(* - Local Variables: - coq-load-path: ((rec "../.." "SMTCoq")) - End: -*) diff --git a/src/versions/native/smtcoq_plugin_native.ml4 b/src/versions/native/smtcoq_plugin_native.ml4 deleted file mode 100644 index ebf8511..0000000 --- a/src/versions/native/smtcoq_plugin_native.ml4 +++ /dev/null @@ -1,99 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -VERNAC COMMAND EXTEND Vernac_zchaff -| [ "Parse_certif_zchaff" - ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] -> - [ - Zchaff.parse_certif dimacs trace fdimacs fproof - ] -| [ "Zchaff_Checker" string(fdimacs) string(fproof) ] -> - [ - Zchaff.checker fdimacs fproof - ] -| [ "Zchaff_Theorem" ident(name) string(fdimacs) string(fproof) ] -> - [ - Zchaff.theorem name fdimacs fproof - ] -END - -VERNAC COMMAND EXTEND Vernac_zchaff_abs -| [ "Zchaff_Theorem_Abs" ident(name) string(fdimacs) string(fproof) ] -> - [ - Zchaff.theorem_abs name fdimacs fproof - ] -END - -VERNAC COMMAND EXTEND Vernac_verit -| [ "Parse_certif_verit" - ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] -> - [ - Verit.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof - ] -| [ "Verit_Checker" string(fsmt) string(fproof) ] -> - [ - Verit.checker fsmt fproof - ] -| [ "Verit_Checker_Debug" string(fsmt) string(fproof) ] -> - [ - Verit.checker_debug fsmt fproof - ] -| [ "Verit_Theorem" ident(name) string(fsmt) string(fproof) ] -> - [ - Verit.theorem name fsmt fproof - ] -END - -VERNAC COMMAND EXTEND Vernac_lfsc -| [ "Parse_certif_lfsc" - ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] -> - [ - Lfsc.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof - ] -| [ "Lfsc_Checker" string(fsmt) string(fproof) ] -> - [ - Lfsc.checker fsmt fproof - ] -| [ "Lfsc_Checker_Debug" string(fsmt) string(fproof) ] -> - [ - Lfsc.checker_debug fsmt fproof - ] -| [ "Lfsc_Theorem" ident(name) string(fsmt) string(fproof) ] -> - [ - Lfsc.theorem name fsmt fproof - ] -END - -TACTIC EXTEND Tactic_zchaff -| [ "zchaff_bool" ] -> [ Zchaff.tactic () ] -| [ "zchaff_bool_no_check" ] -> [ Zchaff.tactic_no_check () ] -END - -let lemmas_list = ref [] - -VERNAC COMMAND EXTEND Add_lemma -| [ "Add_lemmas" constr_list(lems) ] -> [ lemmas_list := lems @ !lemmas_list ] -| [ "Clear_lemmas" ] -> [ lemmas_list := [] ] -END - - -let error () = Structures.error "Tactics are not supported with native-coq" - -TACTIC EXTEND Tactic_verit -| [ "verit_bool_base" constr_list(lpl) ] -> [ error () ] -| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ error () ] -END - -TACTIC EXTEND Tactic_cvc4 -| [ "cvc4_bool" ] -> [ error () ] -| [ "cvc4_bool_no_check" ] -> [ error () ] -END diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml deleted file mode 100644 index 435a1a1..0000000 --- a/src/versions/native/structures.ml +++ /dev/null @@ -1,186 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -open Entries -open Coqlib - - -(* Constr generation and manipulation *) -type id = Names.identifier -let mkId = Names.id_of_string - - -type name = Names.name -let name_of_id i = Names.Name i -let mkName s = - let id = mkId s in - name_of_id id -let string_of_name = function - Names.Name id -> Names.string_of_id id - | _ -> failwith "unnamed rel" - - -type constr = Term.constr -type types = Term.types -let eq_constr = Term.eq_constr -let hash_constr = Term.hash_constr -let mkProp = Term.mkProp -let mkConst = Term.mkConst -let mkVar = Term.mkVar -let mkRel = Term.mkRel -let isRel = Term.isRel -let destRel = Term.destRel -let lift = Term.lift -let mkApp = Term.mkApp -let decompose_app = Term.decompose_app -let mkLambda = Term.mkLambda -let mkProd = Term.mkProd -let mkLetIn = Term.mkLetIn - -let pr_constr_env = Printer.pr_constr_env -let pr_constr = Printer.pr_constr - - -let dummy_loc = Pp.dummy_loc - -let mkUConst c = - { const_entry_body = c; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} - -let mkTConst c _ ty = - { const_entry_body = c; - const_entry_type = Some ty; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} - -(* TODO : Set -> Type *) -let declare_new_type t = - Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) Term.mkSet [] false None (dummy_loc, t); - Term.mkVar t - -let declare_new_variable v constr_t = - Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (dummy_loc, v); - Term.mkVar v - -let declare_constant n c = - Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition) - - -type cast_kind = Term.cast_kind -let vmcast = Term.VMcast -let mkCast = Term.mkCast - - -(* EConstr *) -type econstr = Term.constr -let econstr_of_constr e = e - - -(* Modules *) -let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) - - -(* Int63 *) -let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]] - -let mkInt : int -> Term.constr = - fun i -> Term.mkInt (Uint63.of_int i) - -let cint = gen_constant int63_modules "int" - - -(* PArray *) -let parray_modules = [["Coq";"Array";"PArray"]] - -let max_array_size : int = - Parray.trunc_size (Uint63.of_int 4194303) -let mkArray : Term.types * Term.constr array -> Term.constr = - Term.mkArray - - -(* Traces *) -(* WARNING: side effect on r! *) -let mkTrace step_to_coq next carray _ _ _ _ size step def_step r = - let max = max_array_size - 1 in - let q,r1 = size / max, size mod max in - let trace = - let len = if r1 = 0 then q + 1 else q + 2 in - Array.make len (mkArray (step, [|def_step|])) in - for j = 0 to q - 1 do - let tracej = Array.make max_array_size def_step in - for i = 0 to max - 1 do - r := next !r; - tracej.(i) <- step_to_coq !r; - done; - trace.(j) <- mkArray (step, tracej) - done; - if r1 <> 0 then ( - let traceq = Array.make (r1 + 1) def_step in - for i = 0 to r1-1 do - r := next !r; - traceq.(i) <- step_to_coq !r; - done; - trace.(q) <- mkArray (step, traceq) - ); - mkArray (Term.mkApp (Lazy.force carray, [|step|]), trace) - - -(* Micromega *) -module Micromega_plugin_Micromega = Micromega -module Micromega_plugin_Certificate = Certificate - -let micromega_coq_proofTerm = - Coq_micromega.M.coq_proofTerm - -let micromega_dump_proof_term p = - Coq_micromega.dump_proof_term p - - -(* Tactics *) -type tactic = Proof_type.tactic -let tclTHEN = Tacticals.tclTHEN -let tclTHENLAST = Tacticals.tclTHENLAST -let assert_before = Tactics.assert_tac -let vm_cast_no_check = Tactics.vm_cast_no_check -let mk_tactic tac gl = - let env = Tacmach.pf_env gl in - let sigma = Tacmach.project gl in - let t = Tacmach.pf_concl gl in - tac env sigma t gl -let set_evars_tac _ = Tacticals.tclIDTAC - - -(* Other differences between the two versions of Coq *) -type constr_expr = Topconstr.constr_expr -let error = Errors.error -let warning _ s = Pp.warning s -let extern_constr = Constrextern.extern_constr true Environ.empty_env -let destruct_rel_decl (n, _, t) = n, t -let interp_constr env sigma = Constrintern.interp_constr sigma env -let ppconstr_lsimpleconstr = Ppconstr.lsimple -let constrextern_extern_constr = - let env = Global.env () in - Constrextern.extern_constr false env - -let get_rel_dec_name = fun _ -> Names.Anonymous - -(* Eta-expanded to get rid of optional arguments *) -let retyping_get_type_of env = Retyping.get_type_of env - -let vm_conv = Reduction.vm_conv -let cbv_vm = Vnorm.cbv_vm - - diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli deleted file mode 100644 index f2775a6..0000000 --- a/src/versions/native/structures.mli +++ /dev/null @@ -1,117 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -(* Constr generation and manipulation *) -type id = Names.variable -val mkId : string -> id - -type name -val name_of_id : id -> name -val mkName : string -> name -val string_of_name : name -> string - -type constr = Term.constr -type types = constr -val eq_constr : constr -> constr -> bool -val hash_constr : constr -> int -val mkProp : types -val mkConst : Names.constant -> constr -val mkVar : id -> constr -val mkRel : int -> constr -val isRel : constr -> bool -val destRel : constr -> int -val lift : int -> constr -> constr -val mkApp : constr * constr array -> constr -val decompose_app : constr -> constr * constr list -val mkLambda : name * types * constr -> constr -val mkProd : name * types * types -> types -val mkLetIn : name * constr * types * constr -> constr - -val pr_constr_env : Environ.env -> constr -> Pp.std_ppcmds -val pr_constr : constr -> Pp.std_ppcmds - -val mkUConst : constr -> Entries.definition_entry -val mkTConst : constr -> 'a -> types -> Entries.definition_entry -val declare_new_type : id -> types -val declare_new_variable : id -> types -> constr -val declare_constant : id -> Entries.definition_entry -> Names.constant - -type cast_kind -val vmcast : cast_kind -val mkCast : constr * cast_kind * constr -> constr - - -(* EConstr *) -type econstr = constr -val econstr_of_constr : constr -> econstr - - -(* Modules *) -val gen_constant : string list list -> string -> constr lazy_t - - -(* Int63 *) -val int63_modules : string list list -val mkInt : int -> constr -val cint : constr lazy_t - - -(* PArray *) -val parray_modules : string list list -val max_array_size : int -val mkArray : types * constr array -> constr - - -(* Traces *) -val mkTrace : - ('a -> constr) -> - ('a -> 'a) -> - constr Lazy.t -> - 'b -> - 'c -> 'd -> 'e -> int -> types -> constr -> 'a ref -> constr - - -(* Micromega *) -module Micromega_plugin_Micromega = Micromega -module Micromega_plugin_Certificate = Certificate - -val micromega_coq_proofTerm : constr lazy_t -val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr - - -(* Tactics *) -type tactic = Proof_type.tactic -val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic -val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic -val assert_before : name -> types -> Proof_type.tactic -val vm_cast_no_check : constr -> Proof_type.tactic -val mk_tactic : - (Environ.env -> - Evd.evar_map -> types -> Proof_type.goal Tacmach.sigma -> 'a) -> - Proof_type.goal Tacmach.sigma -> 'a -val set_evars_tac : 'a -> Proof_type.tactic - - -(* Other differences between the two versions of Coq *) -type constr_expr = Topconstr.constr_expr -val error : string -> 'a -val warning : string -> string -> unit -val extern_constr : constr -> Topconstr.constr_expr -val destruct_rel_decl : Term.rel_declaration -> name * types -val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> constr -val ppconstr_lsimpleconstr : Ppconstr.precedence -val constrextern_extern_constr : constr -> Topconstr.constr_expr -val get_rel_dec_name : 'a -> name -val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr - -val vm_conv : Reduction.conv_pb -> types Reduction.conversion_function -val cbv_vm : Environ.env -> constr -> types -> constr diff --git a/src/versions/standard/Structures_standard.v b/src/versions/standard/Structures_standard.v deleted file mode 100644 index 1a0abf5..0000000 --- a/src/versions/standard/Structures_standard.v +++ /dev/null @@ -1,64 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -Require Import Int63. - -Require Import List. - - -Section Trace. - - Definition trace (step:Type) := ((list step) * step)%type. - - Definition trace_to_list {step:Type} (t:trace step) : list step := - let (t, _) := t in t. - - Definition trace_length {step:Type} (t:trace step) : int := - let (t,_) := t in - List.fold_left (fun i _ => (i+1)%int) t 0%int. - - Fixpoint trace_get_aux {step:Type} (t:list step) (def:step) (i:int) : step := - match t with - | nil => def - | s::ss => - if (i == 0)%int then - s - else - trace_get_aux ss def (i-1) - end. - Definition trace_get {step:Type} (t:trace step) : int -> step := - let (t,def) := t in trace_get_aux t def. - - Definition trace_fold {state step:Type} (transition: state -> step -> state) (s0:state) (t:trace step) := - let (t,_) := t in - List.fold_left transition t s0. - - Lemma trace_fold_ind (state step : Type) (P : state -> Prop) (transition : state -> step -> state) (t : trace step) - (IH: forall (s0 : state) (i : int), (i < trace_length t)%int = true -> P s0 -> P (transition s0 (trace_get t i))) : - forall s0 : state, P s0 -> P (trace_fold transition s0 t). - Admitted. - -End Trace. - - -Require Import PeanoNat. - -Definition nat_eqb := Nat.eqb. -Definition nat_eqb_eq := Nat.eqb_eq. -Definition nat_eqb_refl := Nat.eqb_refl. - - -(* - Local Variables: - coq-load-path: ((rec "../.." "SMTCoq")) - End: -*) diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index c6bdc64..1f5110b 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -133,7 +133,7 @@ let import_cnf_trace reloc filename first last = let make_roots first last = let cint = Lazy.force cint in - let roots = Array.make (last.id + 2) (Structures.mkArray (cint, Array.make 1 (mkInt 0))) in + let roots = Array.make (last.id + 2) (CoqInterface.mkArray (cint, Array.make 1 (mkInt 0))) in let mk_elem l = let x = match Form.pform l with | Fatom x -> x + 2 @@ -144,15 +144,15 @@ let make_roots first last = let root = Array.of_list (get_val !r) in let croot = Array.make (Array.length root + 1) (mkInt 0) in Array.iteri (fun i l -> croot.(i) <- mk_elem l) root; - roots.(!r.id) <- Structures.mkArray (cint, croot); + roots.(!r.id) <- CoqInterface.mkArray (cint, croot); r := next !r done; let root = Array.of_list (get_val !r) in let croot = Array.make (Array.length root + 1) (mkInt 0) in Array.iteri (fun i l -> croot.(i) <- mk_elem l) root; - roots.(!r.id) <- Structures.mkArray (cint, croot); + roots.(!r.id) <- CoqInterface.mkArray (cint, croot); - Structures.mkArray (mklApp carray [|cint|], roots) + CoqInterface.mkArray (mklApp carray [|cint|], roots) let interp_roots first last = let tbl = Hashtbl.create 17 in @@ -164,7 +164,7 @@ let interp_roots first last = let h = if Form.is_pos l then ph else ph lxor 1 in try Hashtbl.find tbl h with Not_found -> - let p = Structures.mkApp (Structures.mkRel 1, [|mkInt (x+1)|]) in + let p = CoqInterface.mkApp (CoqInterface.mkRel 1, [|mkInt (x+1)|]) in let np = mklApp cnegb [|p|] in Hashtbl.add tbl ph p; Hashtbl.add tbl (ph lxor 1) np; @@ -194,15 +194,15 @@ let parse_certif dimacs trace fdimacs ftrace = SmtTrace.clear (); let _,first,last,reloc = import_cnf fdimacs in let d = make_roots first last in - let ce1 = Structures.mkUConst d in - let _ = Structures.declare_constant dimacs ce1 in + let ce1 = CoqInterface.mkUConst d in + let _ = CoqInterface.declare_constant dimacs ce1 in let max_id, confl = import_cnf_trace reloc ftrace first last in let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl None in let certif = mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - let ce2 = Structures.mkUConst certif in - let _ = Structures.declare_constant trace ce2 in + let ce2 = CoqInterface.mkUConst certif in + let _ = CoqInterface.declare_constant trace ce2 in () let cdimacs = gen_constant sat_checker_modules "dimacs" @@ -222,36 +222,36 @@ let theorems interp name fdimacs ftrace = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in let theorem_concl = mklApp cnot [|mklApp cis_true [|interp d first last|] |] in - let vtype = Structures.mkArrow (Lazy.force cint) (Lazy.force cbool) in + let vtype = CoqInterface.mkArrow (Lazy.force cint) (Lazy.force cbool) in let theorem_type = - Structures.mkProd (Structures.mkName "v", vtype, theorem_concl) in + CoqInterface.mkProd (CoqInterface.mkName "v", vtype, theorem_concl) in let theorem_proof_cast = - Structures.mkCast ( - Structures.mkLetIn (Structures.mkName "d", d, Lazy.force cdimacs, - Structures.mkLetIn (Structures.mkName "c", certif, Lazy.force ccertif, - Structures.mkLambda (Structures.mkName "v", vtype, + CoqInterface.mkCast ( + CoqInterface.mkLetIn (CoqInterface.mkName "d", d, Lazy.force cdimacs, + CoqInterface.mkLetIn (CoqInterface.mkName "c", certif, Lazy.force ccertif, + CoqInterface.mkLambda (CoqInterface.mkName "v", vtype, mklApp ctheorem_checker - [| Structures.mkRel 3(*d*); Structures.mkRel 2(*c*); + [| CoqInterface.mkRel 3(*d*); CoqInterface.mkRel 2(*c*); vm_cast_true_no_check - (mklApp cchecker [|Structures.mkRel 3(*d*); Structures.mkRel 2(*c*)|]); - Structures.mkRel 1(*v*)|]))), - Structures.vmcast, + (mklApp cchecker [|CoqInterface.mkRel 3(*d*); CoqInterface.mkRel 2(*c*)|]); + CoqInterface.mkRel 1(*v*)|]))), + CoqInterface.vmcast, theorem_type) in let theorem_proof_nocast = - Structures.mkLetIn (Structures.mkName "d", d, Lazy.force cdimacs, - Structures.mkLetIn (Structures.mkName "c", certif, Lazy.force ccertif, - Structures.mkLambda (Structures.mkName "v", vtype, + CoqInterface.mkLetIn (CoqInterface.mkName "d", d, Lazy.force cdimacs, + CoqInterface.mkLetIn (CoqInterface.mkName "c", certif, Lazy.force ccertif, + CoqInterface.mkLambda (CoqInterface.mkName "v", vtype, mklApp ctheorem_checker - [| Structures.mkRel 3(*d*); Structures.mkRel 2(*c*)|]))) + [| CoqInterface.mkRel 3(*d*); CoqInterface.mkRel 2(*c*)|]))) in - let ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_type in - let _ = Structures.declare_constant name ce in + let ce = CoqInterface.mkTConst theorem_proof_cast theorem_proof_nocast theorem_type in + let _ = CoqInterface.declare_constant name ce in () let theorem = theorems (fun _ -> interp_roots) let theorem_abs = - theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|Structures.mkRel 1(*v*)|]; d|]) + theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|CoqInterface.mkRel 1(*v*)|]; d|]) let checker fdimacs ftrace = @@ -267,9 +267,9 @@ let checker fdimacs ftrace = let tm = mklApp cchecker [|d; certif|] in - let res = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in + let res = CoqInterface.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in Format.eprintf " = %s\n : bool@." - (if Structures.eq_constr res (Lazy.force CoqTerms.ctrue) then + (if CoqInterface.eq_constr res (Lazy.force CoqTerms.ctrue) then "true" else "false") @@ -358,22 +358,22 @@ let cchecker_eq_correct = let cchecker_eq = gen_constant cnf_checker_modules "checker_eq" let build_body reify_atom reify_form l b (max_id, confl) vm_cast = - let ntvar = Structures.mkName "t_var" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in + let ntvar = CoqInterface.mkName "t_var" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in let tvar = Atom.interp_tbl reify_atom in let _, tform = Form.interp_tbl reify_form in let (tres,_,_) = SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in - let vtvar = Structures.mkRel 3 in - let vtform = Structures.mkRel 2 in - let vc = Structures.mkRel 1 in + let vtvar = CoqInterface.mkRel 3 in + let vtform = CoqInterface.mkRel 2 in + let vc = CoqInterface.mkRel 1 in let add_lets t = - Structures.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], - Structures.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, Lazy.force ccertif, + CoqInterface.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], + CoqInterface.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, Lazy.force ccertif, t))) in let cbc = @@ -391,22 +391,22 @@ let build_body reify_atom reify_form l b (max_id, confl) vm_cast = let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) vm_cast = - let ntvar = Structures.mkName "t_var" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in + let ntvar = CoqInterface.mkName "t_var" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in let tvar = Atom.interp_tbl reify_atom in let _, tform = Form.interp_tbl reify_form in let (tres,_,_) = SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in - let vtvar = Structures.mkRel 3 in - let vtform = Structures.mkRel 2 in - let vc = Structures.mkRel 1 in + let vtvar = CoqInterface.mkRel 3 in + let vtform = CoqInterface.mkRel 2 in + let vc = CoqInterface.mkRel 1 in let add_lets t = - Structures.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], - Structures.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, Lazy.force ccertif, + CoqInterface.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], + CoqInterface.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, Lazy.force ccertif, t))) in let ceqc = add_lets (mklApp cchecker_eq [|vtform;l1;l2;l;vc|]) @@ -421,10 +421,10 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) vm_cast = (proof_cast, proof_nocast) let get_arguments concl = - let f, args = Structures.decompose_app concl in + let f, args = CoqInterface.decompose_app concl in match args with - | [ty;a;b] when (Structures.eq_constr f (Lazy.force ceq)) && (Structures.eq_constr ty (Lazy.force cbool)) -> a, b - | [a] when (Structures.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue + | [ty;a;b] when (CoqInterface.eq_constr f (Lazy.force ceq)) && (CoqInterface.eq_constr ty (Lazy.force cbool)) -> a, b + | [a] when (CoqInterface.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue | _ -> failwith ("Zchaff.get_arguments :can only deal with equality over bool") @@ -499,7 +499,7 @@ let make_proof pform_tbl atom_tbl env reify_form l = let (reloc, resfilename, logfilename, last) = call_zchaff (Form.nvars reify_form) root in (try check_unsat resfilename with - | Sat model -> Structures.error (List.fold_left (fun acc i -> + | Sat model -> CoqInterface.error (List.fold_left (fun acc i -> let index = if i > 0 then i-1 else -i-1 in let ispos = i > 0 in try ( @@ -508,7 +508,7 @@ let make_proof pform_tbl atom_tbl env reify_form l = | Fatom a -> let t = atom_tbl.(a) in let value = if ispos then " = true" else " = false" in - acc^" "^(Pp.string_of_ppcmds (Structures.pr_constr_env env t))^value + acc^" "^(Pp.string_of_ppcmds (CoqInterface.pr_constr_env env t))^value | Fapp _ -> acc (* Nothing to do with ZChaff *) | FbbT _ -> assert false @@ -528,9 +528,9 @@ let core_tactic vm_cast env sigma concl = let reify_atom = Atom.create () in let reify_form = Form.create () in let (body_cast, body_nocast) = - if ((Structures.eq_constr b (Lazy.force ctrue)) || (Structures.eq_constr b (Lazy.force cfalse))) then + if ((CoqInterface.eq_constr b (Lazy.force ctrue)) || (CoqInterface.eq_constr b (Lazy.force cfalse))) then let l = Form.of_coq (Atom.get reify_atom) reify_form a in - let l' = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in + let l' = if (CoqInterface.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in let atom_tbl = Atom.atom_tbl reify_atom in let pform_tbl = Form.pform_tbl reify_form in let max_id_confl = make_proof pform_tbl atom_tbl (Environ.push_rel_context forall_let env) reify_form l' in @@ -551,10 +551,10 @@ let core_tactic vm_cast env sigma concl = let res_cast = compose_lam_assum forall_let body_cast in let res_nocast = compose_lam_assum forall_let body_nocast in - (Structures.tclTHEN - (Structures.set_evars_tac res_nocast) - (Structures.vm_cast_no_check res_cast)) + (CoqInterface.tclTHEN + (CoqInterface.set_evars_tac res_nocast) + (CoqInterface.vm_cast_no_check res_cast)) -let tactic () = Structures.tclTHEN Tactics.intros (Structures.mk_tactic (core_tactic vm_cast_true)) -let tactic_no_check () = Structures.tclTHEN Tactics.intros (Structures.mk_tactic (core_tactic (fun _ -> vm_cast_true_no_check))) +let tactic () = CoqInterface.tclTHEN Tactics.intros (CoqInterface.mk_tactic (core_tactic vm_cast_true)) +let tactic_no_check () = CoqInterface.tclTHEN Tactics.intros (CoqInterface.mk_tactic (core_tactic (fun _ -> vm_cast_true_no_check))) diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli index 3f458d3..1e472fc 100644 --- a/src/zchaff/zchaff.mli +++ b/src/zchaff/zchaff.mli @@ -11,9 +11,9 @@ val pp_trace : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit -val parse_certif : Structures.id -> Structures.id -> string -> string -> unit +val parse_certif : CoqInterface.id -> CoqInterface.id -> string -> string -> unit val checker : string -> string -> unit -val theorem : Structures.id -> string -> string -> unit -val theorem_abs : Structures.id -> string -> string -> unit -val tactic : unit -> Structures.tactic -val tactic_no_check : unit -> Structures.tactic +val theorem : CoqInterface.id -> string -> string -> unit +val theorem_abs : CoqInterface.id -> string -> string -> unit +val tactic : unit -> CoqInterface.tactic +val tactic_no_check : unit -> CoqInterface.tactic |