diff options
Diffstat (limited to 'src/versions/native')
-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 | 188 | ||||
-rw-r--r-- | src/versions/native/structures.mli | 119 |
7 files changed, 0 insertions, 1196 deletions
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 0738801..0000000 --- a/src/versions/native/structures.ml +++ /dev/null @@ -1,188 +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_Mutils = Mutils -module Micromega_plugin_Certificate = Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega - -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 d8071d9..0000000 --- a/src/versions/native/structures.mli +++ /dev/null @@ -1,119 +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_Mutils = Mutils -module Micromega_plugin_Certificate = Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega - -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 |