diff options
author | ckeller <ckeller@users.noreply.github.com> | 2019-04-12 14:13:00 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-12 14:13:00 +0200 |
commit | 02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b (patch) | |
tree | ec18dc8768ea8ca45ed380ffda289fe204a822a5 /src/versions | |
parent | ad491f845f6fb3e88ff1169ac472f194d12306d2 (diff) | |
download | smtcoq-02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b.tar.gz smtcoq-02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b.zip |
Error message to state that tactics are not supported with native-coq (#47)
* Better error message for failing tactics with native-coq
Diffstat (limited to 'src/versions')
-rw-r--r-- | src/versions/native/Make | 2 | ||||
-rw-r--r-- | src/versions/native/Makefile | 2 | ||||
-rw-r--r-- | src/versions/native/Tactics_native.v | 55 | ||||
-rw-r--r-- | src/versions/native/smtcoq_plugin_native.ml4 | 10 | ||||
-rw-r--r-- | src/versions/standard/Tactics_standard.v | 65 | ||||
-rw-r--r-- | src/versions/standard/_CoqProject | 1 |
6 files changed, 129 insertions, 6 deletions
diff --git a/src/versions/native/Make b/src/versions/native/Make index 63c95b2..a9e60e4 100644 --- a/src/versions/native/Make +++ b/src/versions/native/Make @@ -51,7 +51,7 @@ CMXA = smtcoq.cmxa CMXS = smtcoq_plugin.cmxs -VCMXS = "versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.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_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.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_SMTCoq.cmi" +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 diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile index afc5523..4683956 100644 --- a/src/versions/native/Makefile +++ b/src/versions/native/Makefile @@ -73,7 +73,7 @@ COQDOCLIBS?=-R . SMTCoq CAMLYACC=$(CAMLBIN)ocamlyacc CAMLLEX=$(CAMLBIN)ocamllex -VCMXS=versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.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_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.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_SMTCoq.cmi +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 diff --git a/src/versions/native/Tactics_native.v b/src/versions/native/Tactics_native.v new file mode 100644 index 0000000..d2b2400 --- /dev/null +++ b/src/versions/native/Tactics_native.v @@ -0,0 +1,55 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* 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 index d6954b5..7d78731 100644 --- a/src/versions/native/smtcoq_plugin_native.ml4 +++ b/src/versions/native/smtcoq_plugin_native.ml4 @@ -86,12 +86,14 @@ VERNAC COMMAND EXTEND Add_lemma END +let error () = Structures.error "Tactics are not supported with native-coq" + TACTIC EXTEND Tactic_verit -| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic lpl !lemmas_list ] -| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check lpl !lemmas_list ] +| [ "verit_bool_base" constr_list(lpl) ] -> [ error () ] +| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ error () ] END TACTIC EXTEND Tactic_cvc4 -| [ "cvc4_bool" ] -> [ Lfsc.tactic () ] -| [ "cvc4_bool_no_check" ] -> [ Lfsc.tactic_no_check () ] +| [ "cvc4_bool" ] -> [ error () ] +| [ "cvc4_bool_no_check" ] -> [ error () ] END diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v new file mode 100644 index 0000000..95b92d6 --- /dev/null +++ b/src/versions/standard/Tactics_standard.v @@ -0,0 +1,65 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +Require Import PropToBool BoolToProp. (* Before SMTCoq.State *) +Require Import Int63 List PArray Bool ZArith. +Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances QInst. + +Declare ML Module "smtcoq_plugin". + + +Tactic Notation "verit_bool" constr_list(h) := + verit_bool_base h; vauto. + +Tactic Notation "verit_bool_no_check" constr_list(h) := + verit_bool_no_check_base h; vauto. + + +(** Tactics in Prop **) + +Ltac zchaff := prop2bool; zchaff_bool; bool2prop. +Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop. + +Tactic Notation "verit" constr_list(h) := prop2bool; verit_bool h; bool2prop. +Tactic Notation "verit_no_check" constr_list(h) := prop2bool; verit_bool_no_check h; bool2prop. + +Ltac cvc4 := prop2bool; cvc4_bool; bool2prop. +Ltac cvc4_no_check := prop2bool; cvc4_bool_no_check; bool2prop. + + +(* Ltac smt := prop2bool; *) +(* repeat *) +(* match goal with *) +(* | [ |- context[ CompDec ?t ] ] => try assumption *) +(* | [ |- _ : bool] => verit_bool *) +(* | [ |- _ : bool] => try (cvc4_bool; verit_bool) *) +(* end; *) +(* bool2prop. *) +(* Ltac smt_no_check := prop2bool; *) +(* repeat *) +(* match goal with *) +(* | [ |- context[ CompDec ?t ] ] => try assumption *) +(* | [ |- _ : bool] => verit_bool_no_check *) +(* | [ |- _ : bool] => try (cvc4_bool_no_check; verit_bool_no_check) *) +(* end; *) +(* bool2prop. *) + +Tactic Notation "smt" constr_list(h) := (prop2bool; try verit_bool h; cvc4_bool; try verit_bool h; bool2prop). +Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; bool2prop). + + + +(* + Local Variables: + coq-load-path: ((rec "." "SMTCoq")) + End: +*) diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject index a71f500..f283e00 100644 --- a/src/versions/standard/_CoqProject +++ b/src/versions/standard/_CoqProject @@ -146,6 +146,7 @@ SMTCoq.v ReflectFacts.v PropToBool.v BoolToProp.v +QInst.v Tactics.v SMT_terms.v State.v |