From ec41af7ac01cef7c30785e6dd704381f31e7c2d3 Mon Sep 17 00:00:00 2001 From: ckeller Date: Thu, 14 Feb 2019 20:09:40 +0100 Subject: V8.7 (#36) Port SMTCoq to Coq-8.7 --- src/versions/native/structures.ml | 17 +- src/versions/native/structures.mli | 14 +- src/versions/standard/Int63/Int63Axioms_standard.v | 31 +- src/versions/standard/Int63/Int63Op_standard.v | 2 +- .../standard/Int63/Int63Properties_standard.v | 131 +- src/versions/standard/Make | 12 +- src/versions/standard/Makefile | 1252 +++++++++++--------- src/versions/standard/Makefile.conf | 103 ++ src/versions/standard/Structures_standard.v | 9 + src/versions/standard/g_smtcoq_standard.ml4 | 11 +- src/versions/standard/structures.ml | 65 +- src/versions/standard/structures.mli | 25 +- 12 files changed, 1025 insertions(+), 647 deletions(-) create mode 100644 src/versions/standard/Makefile.conf (limited to 'src/versions') diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index c286f56..dbf3d62 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -114,6 +114,8 @@ let assert_before = Tactics.assert_tac let vm_conv = Reduction.vm_conv let vm_cast_no_check = Tactics.vm_cast_no_check +let cbv_vm = Vnorm.cbv_vm + let mk_tactic tac gl = let env = Tacmach.pf_env gl in let sigma = Tacmach.project gl in @@ -128,15 +130,28 @@ let constrextern_extern_constr = 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 + -(* Old packaging of plugins *) +(* Micromega *) module Micromega_plugin_Certificate = Certificate module Micromega_plugin_Coq_micromega = Coq_micromega module Micromega_plugin_Micromega = Micromega module Micromega_plugin_Mutils = Mutils +let micromega_coq_proofTerm = + Coq_micromega.M.coq_proofTerm + +let micromega_dump_proof_term p = + Coq_micromega.dump_proof_term p + (* Types in the Coq source code *) type tactic = Proof_type.tactic type names_id = Names.identifier type constr_expr = Topconstr.constr_expr + +(* EConstr *) +type econstr = Term.constr +let econstr_of_constr e = e diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli index b4d9731..9ec21d2 100644 --- a/src/versions/native/structures.mli +++ b/src/versions/native/structures.mli @@ -24,7 +24,6 @@ val mkTrace : 'b -> 'c -> 'd -> 'e -> int -> Term.types -> Term.constr -> 'a ref -> Term.constr type names_id_t = Names.identifier -val dummy_loc : Pp.loc val mkUConst : Term.constr -> Entries.definition_entry val mkTConst : Term.constr -> 'a -> Term.types -> Entries.definition_entry val error : string -> 'a @@ -40,8 +39,11 @@ val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> Term 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 : Names.name -> Term.types -> Proof_type.tactic + val vm_conv : Reduction.conv_pb -> Term.types Reduction.conversion_function val vm_cast_no_check : Term.constr -> Proof_type.tactic +val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr + val mk_tactic : (Environ.env -> Evd.evar_map -> Term.types -> Proof_type.goal Tacmach.sigma -> 'a) -> @@ -50,16 +52,24 @@ val set_evars_tac : 'a -> Proof_type.tactic val ppconstr_lsimpleconstr : Ppconstr.precedence val constrextern_extern_constr : Term.constr -> Topconstr.constr_expr val get_rel_dec_name : 'a -> Names.name +val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr -(* Old packaging of plugins *) +(* Micromega *) module Micromega_plugin_Certificate = Certificate module Micromega_plugin_Coq_micromega = Coq_micromega module Micromega_plugin_Micromega = Micromega module Micromega_plugin_Mutils = Mutils +val micromega_coq_proofTerm : Term.constr lazy_t +val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr + (* Types in the Coq source code *) type tactic = Proof_type.tactic type names_id = Names.identifier type constr_expr = Topconstr.constr_expr + +(* EConstr *) +type econstr = Term.constr +val econstr_of_constr : Term.constr -> econstr diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v index d4e45fc..9a90d39 100644 --- a/src/versions/standard/Int63/Int63Axioms_standard.v +++ b/src/versions/standard/Int63/Int63Axioms_standard.v @@ -11,12 +11,41 @@ Require Import Bvector. -Require Export BigNumPrelude. +(* Require Export BigNumPrelude. *) Require Import Int31 Cyclic31. Require Export Int63Native. Require Export Int63Op. Require Import Psatz. +Local Open Scope Z_scope. + + +(* Taken from BigNumPrelude *) + + Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p. + Proof. + intros p x Hle;destruct (Z_le_gt_dec 0 p). + apply Zdiv_le_lower_bound;auto with zarith. + replace (2^p) with 0. + destruct x;compute;intro;discriminate. + destruct p;trivial;discriminate. + Qed. + + Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y. + Proof. + intros p x y H;destruct (Z_le_gt_dec 0 p). + apply Zdiv_lt_upper_bound;auto with zarith. + apply Z.lt_le_trans with y;auto with zarith. + rewrite <- (Z.mul_1_r y);apply Z.mul_le_mono_nonneg;auto with zarith. + assert (0 < 2^p);auto with zarith. + replace (2^p) with 0. + destruct x;change (0 n<>0. +Proof. + auto with zarith. +Qed. + +Definition Z_div_plus_l a b c H := Zdiv.Z_div_plus_full_l a b c (Zlt0_not_eq _ H). + +Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a. + Proof. + intros a b H H1;case (Z_mod_lt a b);auto with zarith;intros H2 H3;split;auto. + case (Z.le_gt_cases b a); intros H4; auto with zarith. + rewrite Zmod_small; auto with zarith. + Qed. + + (** Trivial lemmas without axiom *) Lemma wB_diff_0 : wB <> 0. @@ -406,7 +430,18 @@ Proof. case_eq ((i / j < j)%int);[ | rewrite <- Bool.not_true_iff_false]; rewrite ltb_spec, div_spec;intros. assert ([| j + (i / j)%int|] = [|j|] + [|i|]/[|j|]). - rewrite add_spec, Zmod_small;rewrite div_spec;auto with zarith. + { + rewrite add_spec, Zmod_small;rewrite div_spec; auto with zarith. + split. + - apply Z.add_nonneg_nonneg. + + apply Z.lt_le_incl; apply Z.le_lt_trans with (2 := H). apply Z_div_pos. + * apply Z.lt_gt. abstract omega. + * abstract omega. + + apply Z_div_pos. + * apply Z.lt_gt. assumption. + * abstract omega. + - abstract omega. + } apply Hrec;rewrite lsr_spec, H0, to_Z_1;change (2^1) with 2. split; [ | apply sqrt_test_false;auto with zarith]. replace ([|j|] + [|i|]/[|j|]) with @@ -414,9 +449,22 @@ Proof. rewrite Z_div_plus_full_l; auto with zarith. assert (0 <= [|i|]/ [|j|]) by (apply Z_div_pos; auto with zarith). assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / 2) ; auto with zarith. - case (Zle_lt_or_eq 1 [|j|]); auto with zarith; intros Hj1. + case (Zle_lt_or_eq 1 [|j|]); auto with zarith. + { + intro. apply Z_div_pos. + - apply Zgt_pos_0. + - apply Z.add_nonneg_nonneg. + + abstract omega. + + assumption. + } + intros Hj1. rewrite <- Hj1, Zdiv_1_r. assert (0 <= ([|i|] - 1) /2)%Z;[ |apply Z_div_pos]; auto with zarith. + { + apply Z_div_pos. + - apply Zgt_pos_0. + - abstract omega. + } apply sqrt_main;auto with zarith. split;[apply sqrt_test_true | ];auto with zarith. Qed. @@ -562,7 +610,16 @@ Proof. replace [|(1 << (digits - 1))|] with (wB/2); auto. rewrite lsr_spec; auto. replace (2^[|1|]) with 2%Z; auto. - split; auto with zarith. + split. + { + apply Z.add_nonneg_nonneg. + - apply Z_div_pos. + + apply Zgt_pos_0. + + assumption. + - apply Z_div_pos. + + apply Zgt_pos_0. + + abstract omega. + } assert ([|i|]/2 < wB/2); auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. apply Hrec; rewrite H; clear u H. @@ -574,6 +631,13 @@ Proof. (1 * 2 + (([|j|] - 2) + [||WW ih il||] / [|j|])); try ring. rewrite Z_div_plus_full_l; auto with zarith. assert (0 <= ([|j|] - 2 + [||WW ih il||] / [|j|]) / 2) ; auto with zarith. + { + apply Z_div_pos. + - apply Zgt_pos_0. + - apply Z.add_nonneg_nonneg. + + abstract omega. + + assumption. + } apply sqrt_test_false; auto with zarith. apply sqrt_main; auto with zarith. contradict Hij; apply Zle_not_lt. @@ -1091,7 +1155,8 @@ Proof. replace [|j|] with (d2 + [|i|])%Z. 2: unfold d2; ring. rewrite Zpower_exp; auto with zarith. - rewrite Zdiv_mult_cancel_r; auto with zarith. + rewrite Zdiv_mult_cancel_r. + 2: (apply Zlt0_not_eq; apply Z.pow_pos_nonneg; [apply Pos2Z.is_pos|assumption]). 2: unfold d2; auto with zarith. rewrite (Z_div_mod_eq [|x|] (2^d1)) at 2; auto with zarith. 2: apply Zlt_gt; apply Zpower_gt_0; unfold d1; lia. @@ -1404,7 +1469,12 @@ Proof. case (to_Z_bounded x); intros H1x H2x. case (to_Z_bounded (bit x 0)); intros H1b H2b. assert (F1: 0 <= [|x >> 1|] < wB/2). - rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith. + rewrite lsr_spec, to_Z_1, Zpower_1_r; split. + { + apply Z_div_pos. + - apply Zgt_pos_0. + - assumption. + } apply Zdiv_lt_upper_bound; auto with zarith. rewrite (bit_split x) at 1. rewrite add_spec, Zmod_small, lsl_spec, to_Z_1, Zpower_1_r, Zmod_small; @@ -1435,9 +1505,19 @@ Proof. rewrite (to_Z_split y) at 1; rewrite (to_Z_split (x lor y)). assert ([|y>>1|] <= [|(x lor y) >> 1|]). rewrite lor_lsr, <-leb_spec; apply IH. - rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith. + rewrite lsr_spec, to_Z_1, Zpower_1_r; split. + { + apply Z_div_pos. + - apply Zgt_pos_0. + - abstract omega. + } apply Zdiv_lt_upper_bound; auto with zarith. - rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith. + rewrite lsr_spec, to_Z_1, Zpower_1_r; split. + { + apply Z_div_pos. + - apply Zgt_pos_0. + - abstract omega. + } apply Zdiv_lt_upper_bound; auto with zarith. assert ([|bit y 0|] <= [|bit (x lor y) 0|]); auto with zarith. rewrite lor_spec; do 2 case bit; try discriminate. @@ -1462,9 +1542,19 @@ Proof. intros Hn. assert (F1: ((x >> 1) + (y >> 1))%int = (x >> 1) lor (y >> 1)). apply IH. - rewrite lsr_spec, Zpower_1_r; split; auto with zarith. + rewrite lsr_spec, Zpower_1_r; split. + { + apply Z_div_pos. + - apply Zgt_pos_0. + - abstract omega. + } apply Zdiv_lt_upper_bound; auto with zarith. - rewrite lsr_spec, Zpower_1_r; split; auto with zarith. + rewrite lsr_spec, Zpower_1_r; split. + { + apply Z_div_pos. + - apply Zgt_pos_0. + - abstract omega. + } apply Zdiv_lt_upper_bound; auto with zarith. intros m H1 H2. case_eq (digits <= m)%int; [idtac | rewrite <- not_true_iff_false]; @@ -1501,9 +1591,19 @@ Proof. rewrite Zpower_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith. generalize F3; do 2 case bit; try discriminate; auto. case (IH (x >> 1) (y >> 1)). - rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith. + rewrite lsr_spec, to_Z_1, Zpower_1_r; split. + { + apply Z_div_pos. + - apply Zgt_pos_0. + - abstract omega. + } apply Zdiv_lt_upper_bound; auto with zarith. - rewrite lsr_spec, to_Z_1, Zpower_1_r; split; auto with zarith. + rewrite lsr_spec, to_Z_1, Zpower_1_r; split. + { + apply Z_div_pos. + - apply Zgt_pos_0. + - abstract omega. + } apply Zdiv_lt_upper_bound; auto with zarith. intros _ HH m; case (to_Z_bounded m); intros H1m H2m. case_eq (digits <= m)%int. @@ -1521,7 +1621,14 @@ Proof. rewrite lsl_spec, to_Z_1, Zpower_1_r, Zmod_small; auto with zarith. case (to_Z_bounded (x lor y)); intros H1xy H2xy. rewrite lsr_spec, to_Z_1, Zpower_1_r; auto with zarith. - change wB with ((wB/2)*2); split; auto with zarith. + change wB with ((wB/2)*2); split. + { + apply Z.mul_nonneg_nonneg. + - apply Z_div_pos. + + apply Zgt_pos_0. + + assumption. + - apply Pos2Z.is_nonneg. + } assert ([|x lor y|] / 2 < wB / 2); auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. split. diff --git a/src/versions/standard/Make b/src/versions/standard/Make index ee7f119..e47c530 100644 --- a/src/versions/standard/Make +++ b/src/versions/standard/Make @@ -10,14 +10,8 @@ ## To generate the Makefile: ## ## coq_makefile -f Make -o Makefile ## ## In the Makefile : ## -## 1) Suppress the "Makefile" target ## -## 2) Change the "all" target: ## -## remove the "test", "ztest", "vtest", "lfsctest" and "./" ## -## dependencies ## -## 3) Change the "install" and "clean" targets: ## -## Suppress the "+" lines ## -## 4) Add to the "clean" target: ## -## - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml ## +## 1) Add "-native" to the CAMLDEP command (ocamldep -native ...) ## +## 2) remove "post-all" from the targets "all" and "all.timing.diff" ## ######################################################################## @@ -41,7 +35,7 @@ -I "$(shell $(COQBIN)coqc -where)/plugins/micromega" --extra "test" "" "cd ../unit-tests; make" "" +-extra "test" "" "cd ../unit-tests; make" -extra "ztest" "" "cd ../unit-tests; make zchaff" -extra "vtest" "" "cd ../unit-tests; make verit" -extra "lfsctest" "" "cd ../unit-tests; make lfsc" diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile index f71b0c8..2337ad7 100644 --- a/src/versions/standard/Makefile +++ b/src/versions/standard/Makefile @@ -1,712 +1,782 @@ -############################################################################# -## v # The Coq Proof Assistant ## -## /dev/null 2>/dev/null; echo $$?)) +STDTIME?=/usr/bin/env time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=time +endif +endif +else +STDTIME?=/usr/bin/env time -f $(TIMEFMT) +endif +# Coq binaries +COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" +COQCHK ?= "$(COQBIN)coqchk" +COQDEP ?= "$(COQBIN)coqdep" +GALLINA ?= "$(COQBIN)gallina" +COQDOC ?= "$(COQBIN)coqdoc" +COQMKTOP ?= "$(COQBIN)coqmktop" +COQMKFILE ?= "$(COQBIN)coq_makefile" + +# Timing scripts +COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" +BEFORE ?= +AFTER ?= + +# FIXME this should be generated by Coq (modules already linked by Coq) +CAMLDONTLINK=camlp5.gramlib,unix,str + +# OCaml binaries +CAMLC ?= "$(OCAMLFIND)" ocamlc -c +CAMLOPTC ?= "$(OCAMLFIND)" opt -c +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK) +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK) +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -native -slash -ml-synonym .ml4 -ml-synonym .mlpack + +# DESTDIR is prepended to all installation paths +DESTDIR ?= + +# Debug builds, typically -g to OCaml, -debug to Coq. +CAMLDEBUG ?= +COQDEBUG ?= + +# Extra packages to be linked in (as in findlib -package) +CAMLPKGS ?= + +# Option for making timing files +TIMING?= +# Output file names for timed builds +TIME_OF_BUILD_FILE ?= time-of-build.log +TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log +TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log +TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log +TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log +TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line + +########## End of parameters ################################################## +# What follows may be relevant to you only if you need to +# extend this Makefile. If so, look for 'Extension point' here and +# put in Makefile.local double colon rules accordingly. +# E.g. to perform some work after the all target completes you can write +# +# post-all:: +# echo "All done!" # -# This Makefile was generated by the command line : -# coq_makefile -f Make -o Makefile +# in Makefile.local # +############################################################################### + -.DEFAULT_GOAL := all -# This Makefile may take arguments passed as environment variables: -# COQBIN to specify the directory where Coq binaries resides; -# TIMECMD set a command to log .v compilation time; -# TIMED if non empty, use the default time command as TIMECMD; -# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc; -# DSTROOT to specify a prefix to install path. -# VERBOSE to disable the short display of compilation rules. -VERBOSE?= +# Flags ####################################################################### +# +# We define a bunch of variables combining the parameters + SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) -# Here is a hack to make $(eval $(shell works: -define donewline +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) +OPT?= -endef -includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; }))) -$(call includecmdwithout@,$(COQBIN)coqtop -config) +# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d +ifeq '$(OPT)' '-byte' +USEBYTE:=true +DYNOBJ:=.cma +DYNLIB:=.cma +else +USEBYTE:= +DYNOBJ:=.cmxs +DYNLIB:=.cmxs +endif -TIMED?= -TIMECMD?= -STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" -TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) +COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) +COQCHKFLAGS?=-silent -o $(COQLIBS) +COQDOCFLAGS?=-interpolate -utf8 +COQDOCLIBS?=$(COQLIBS_NOML) -vo_to_obj = $(addsuffix .o,\ - $(filter-out Warning: Error:,\ - $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1)))) - -########################## -# # -# Libraries definitions. # -# # -########################## - -OCAMLLIBS?=-I "."\ - -I "bva"\ - -I "classes"\ - -I "array"\ - -I "cnf"\ - -I "euf"\ - -I "lfsc"\ - -I "lia"\ - -I "smtlib2"\ - -I "trace"\ - -I "verit"\ - -I "zchaff"\ - -I "versions/standard"\ - -I "versions/standard/Int63"\ - -I "versions/standard/Array"\ - -I "$(shell $(COQBIN)coqc -where)/plugins/micromega" -COQLIBS?=\ - -R "." SMTCoq\ - -I "."\ - -I "bva"\ - -I "classes"\ - -I "array"\ - -I "cnf"\ - -I "euf"\ - -I "lfsc"\ - -I "lia"\ - -I "smtlib2"\ - -I "trace"\ - -I "verit"\ - -I "zchaff"\ - -I "versions/standard"\ - -I "versions/standard/Int63"\ - -I "versions/standard/Array"\ - -I "$(shell $(COQBIN)coqc -where)/plugins/micromega" -COQCHKLIBS?=\ - -R "." SMTCoq -COQDOCLIBS?=\ - -R "." SMTCoq - -########################## -# # -# Variables definitions. # -# # -########################## - -CAMLLEX=$(CAMLBIN)ocamllex -CAMLYACC=$(CAMLBIN)ocamlyacc +# The version of Coq being run and the version of coq_makefile that +# generated this makefile +COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) +COQMAKEFILE_VERSION:=8.7.2 -OPT?= -COQDEP?="$(COQBIN)coqdep" -c -COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) -COQCHKFLAGS?=-silent -o -COQDOCFLAGS?=-interpolate -utf8 -COQC?=$(TIMER) "$(COQBIN)coqc" -GALLINA?="$(COQBIN)gallina" -COQDOC?="$(COQBIN)coqdoc" -COQCHK?="$(COQBIN)coqchk" -COQMKTOP?="$(COQBIN)coqmktop" - -COQSRCLIBS?=-I "$(COQLIB)kernel" \ --I "$(COQLIB)lib" \ --I "$(COQLIB)library" \ --I "$(COQLIB)parsing" \ --I "$(COQLIB)pretyping" \ --I "$(COQLIB)interp" \ --I "$(COQLIB)printing" \ --I "$(COQLIB)intf" \ --I "$(COQLIB)proofs" \ --I "$(COQLIB)tactics" \ --I "$(COQLIB)tools" \ --I "$(COQLIB)ltacprof" \ --I "$(COQLIB)toplevel" \ --I "$(COQLIB)stm" \ --I "$(COQLIB)grammar" \ --I "$(COQLIB)config" \ --I "$(COQLIB)ltac" \ --I "$(COQLIB)engine" \ - \ - -I "$(COQLIB)/plugins/btauto" \ - -I "$(COQLIB)/plugins/cc" \ - -I "$(COQLIB)/plugins/decl_mode" \ - -I "$(COQLIB)/plugins/derive" \ - -I "$(COQLIB)/plugins/extraction" \ - -I "$(COQLIB)/plugins/firstorder" \ - -I "$(COQLIB)/plugins/fourier" \ - -I "$(COQLIB)/plugins/funind" \ - -I "$(COQLIB)/plugins/ltac" \ - -I "$(COQLIB)/plugins/micromega" \ - -I "$(COQLIB)/plugins/nsatz" \ - -I "$(COQLIB)/plugins/omega" \ - -I "$(COQLIB)/plugins/quote" \ - -I "$(COQLIB)/plugins/romega" \ - -I "$(COQLIB)/plugins/rtauto" \ - -I "$(COQLIB)/plugins/setoid_ring" \ - -I "$(COQLIB)/plugins/ssrmatching" \ - -I "$(COQLIB)/plugins/syntax" \ - -I "$(COQLIB)/plugins/xml" -ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) - -CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread -CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread -CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack -CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib) -GRAMMARS?=grammar.cma +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") + +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) + +# ocamldoc fails with unknown argument otherwise +CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) + +# FIXME This should be generated by Coq +GRAMMARS:=grammar.cma ifeq ($(CAMLP4),camlp5) CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo else CAMLP4EXTEND= endif -PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \ - $(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" -COQTOPINSTALL="${COQLIB}toploop" -endif -###################### -# # -# Files dispatching. # -# # -###################### - -VFILES:=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\ - bva/BVList.v\ - bva/Bva_checker.v\ - classes/SMT_classes.v\ - classes/SMT_classes_instances.v\ - array/FArray.v\ - array/Array_checker.v\ - cnf/Cnf.v\ - euf/Euf.v\ - 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 - -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(VFILES)) +CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) +ifeq (,$(CAMLLIB)) +PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") else -ifeq ($(MAKECMDGOALS),) --include $(addsuffix .d,$(VFILES)) -endif +PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' endif -.SECONDARY: $(addsuffix .d,$(VFILES)) - -VO=vo -VOFILES:=$(VFILES:.v=.$(VO)) -GLOBFILES:=$(VFILES:.v=.glob) -GFILES:=$(VFILES:.v=.g) -HTMLFILES:=$(VFILES:.v=.html) -GHTMLFILES:=$(VFILES:.v=.g.html) -OBJFILES=$(call vo_to_obj,$(VOFILES)) -ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs) -NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) -ML4FILES:=g_smtcoq.ml4 - -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(ML4FILES)) +ifneq (,$(TIMING)) +TIMING_ARG=-time +ifeq (after,$(TIMING)) +TIMING_EXT=after-timing +else +ifeq (before,$(TIMING)) +TIMING_EXT=before-timing else -ifeq ($(MAKECMDGOALS),) --include $(addsuffix .d,$(ML4FILES)) +TIMING_EXT=timing endif endif - -.SECONDARY: $(addsuffix .d,$(ML4FILES)) - -MLFILES:=versions/standard/structures.ml\ - trace/coqTerms.ml\ - trace/smtBtype.ml\ - trace/satAtom.ml\ - trace/smtAtom.ml\ - trace/smtCertif.ml\ - trace/smtCnf.ml\ - trace/smtCommands.ml\ - trace/smtForm.ml\ - trace/smtMisc.ml\ - trace/smtTrace.ml\ - smtlib2/smtlib2_parse.ml\ - smtlib2/smtlib2_lex.ml\ - smtlib2/smtlib2_ast.ml\ - smtlib2/smtlib2_genConstr.ml\ - smtlib2/smtlib2_util.ml\ - smtlib2/sExpr.ml\ - smtlib2/smtlib2_solver.ml\ - smtlib2/sExprParser.ml\ - smtlib2/sExprLexer.ml\ - verit/veritParser.ml\ - verit/veritLexer.ml\ - verit/verit.ml\ - verit/veritSyntax.ml\ - lfsc/shashcons.ml\ - lfsc/hstring.ml\ - lfsc/lfscParser.ml\ - lfsc/type.ml\ - lfsc/ast.ml\ - lfsc/builtin.ml\ - lfsc/tosmtcoq.ml\ - lfsc/converter.ml\ - lfsc/lfsc.ml\ - lfsc/lfscLexer.ml\ - zchaff/cnfParser.ml\ - zchaff/satParser.ml\ - zchaff/zchaff.ml\ - zchaff/zchaffParser.ml\ - lia/lia.ml - -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(MLFILES)) else -ifeq ($(MAKECMDGOALS),) --include $(addsuffix .d,$(MLFILES)) +TIMING_ARG= endif + +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) endif -.SECONDARY: $(addsuffix .d,$(MLFILES)) +concat_path = $(if $(1),$(1)/$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)) -MLPACKFILES:=smtcoq_plugin.mlpack +COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib) +COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib) +COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(MLPACKFILES)) +# Files ####################################################################### +# +# We here define a bunch of variables about the files being part of the +# Coq project in order to ease the writing of build target and build rules + +ALLSRCFILES := \ + $(VFILES) \ + $(ML4FILES) \ + $(MLFILES) \ + $(MLPACKFILES) \ + $(MLLIBFILES) \ + $(MLIFILES) + +# helpers +vo_to_obj = $(addsuffix .o,\ + $(filter-out Warning: Error:,\ + $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) +strip_dotslash = $(patsubst ./%,%,$(1)) +VO = vo + +VOFILES = $(VFILES:.v=.$(VO)) +GLOBFILES = $(VFILES:.v=.glob) +GFILES = $(VFILES:.v=.g) +HTMLFILES = $(VFILES:.v=.html) +GHTMLFILES = $(VFILES:.v=.g.html) +BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) +TEXFILES = $(VFILES:.v=.tex) +GTEXFILES = $(VFILES:.v=.g.tex) +CMOFILES = \ + $(ML4FILES:.ml4=.cmo) \ + $(MLFILES:.ml=.cmo) \ + $(MLPACKFILES:.mlpack=.cmo) +CMXFILES = $(CMOFILES:.cmo=.cmx) +OFILES = $(CMXFILES:.cmx=.o) +CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) +CMXAFILES = $(CMAFILES:.cma=.cmxa) +CMIFILES = \ + $(CMOFILES:.cmo=.cmi) \ + $(MLIFILES:.mli=.cmi) +# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just +# a .ml4 file +CMXSFILES = \ + $(MLPACKFILES:.mlpack=.cmxs) \ + $(CMXAFILES:.cmxa=.cmxs) \ + $(if $(MLPACKFILES)$(CMXAFILES),,\ + $(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs)) + +# files that are packed into a plugin (no extension) +PACKEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib)))) +# files that are archived into a .cma (mllib) +LIBEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib)))) +CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) +CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) +OBJFILES = $(call vo_to_obj,$(VOFILES)) +ALLNATIVEFILES = \ + $(OBJFILES:.o=.cmi) \ + $(OBJFILES:.o=.cmx) \ + $(OBJFILES:.o=.cmxs) +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) +FILESTOINSTALL = \ + $(VOFILES) \ + $(VFILES) \ + $(GLOBFILES) \ + $(NATIVEFILES) \ + $(CMIFILESTOINSTALL) +BYTEFILESTOINSTALL = \ + $(CMOFILESTOINSTALL) \ + $(CMAFILES) +ifeq '$(HASNATDYNLINK)' 'true' +DO_NATDYNLINK = yes +FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) else -ifeq ($(MAKECMDGOALS),) --include $(addsuffix .d,$(MLPACKFILES)) -endif +DO_NATDYNLINK = endif -.SECONDARY: $(addsuffix .d,$(MLPACKFILES)) - -MLIFILES:=versions/standard/structures.mli\ - trace/coqTerms.mli\ - trace/smtBtype.mli\ - trace/satAtom.mli\ - trace/smtAtom.mli\ - trace/smtCertif.mli\ - trace/smtCnf.mli\ - trace/smtCommands.mli\ - trace/smtForm.mli\ - trace/smtMisc.mli\ - trace/smtTrace.mli\ - smtlib2/smtlib2_parse.mli\ - smtlib2/smtlib2_lex.mli\ - smtlib2/smtlib2_ast.mli\ - smtlib2/smtlib2_genConstr.mli\ - smtlib2/smtlib2_util.mli\ - smtlib2/sExpr.mli\ - smtlib2/smtlib2_solver.mli\ - smtlib2/sExprParser.mli\ - verit/veritParser.mli\ - verit/veritLexer.mli\ - verit/verit.mli\ - verit/veritSyntax.mli\ - lfsc/shashcons.mli\ - lfsc/hstring.mli\ - lfsc/lfscParser.mli\ - lfsc/ast.mli\ - lfsc/translator_sig.mli\ - lfsc/tosmtcoq.mli\ - zchaff/cnfParser.mli\ - zchaff/satParser.mli\ - zchaff/zchaff.mli\ - zchaff/zchaffParser.mli\ - lia/lia.mli - -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(MLIFILES)) +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) + +# Compilation targets ######################################################### + +all: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all +.PHONY: all + +all.timing.diff: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" +.PHONY: all.timing.diff + +make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) +make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) +make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) + $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed +print-pretty-timed:: + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +print-pretty-timed-diff:: + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +ifeq (,$(BEFORE)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + $(HIDE)false else -ifeq ($(MAKECMDGOALS),) --include $(addsuffix .d,$(MLIFILES)) +ifeq (,$(AFTER)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + $(HIDE)false +else +print-pretty-single-time-diff:: + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif +pretty-timed: + $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed +.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff -.SECONDARY: $(addsuffix .d,$(MLIFILES)) +# Extension points for actions to be performed before/after the all target +pre-all:: + @# Extension point + $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ + echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ + echo "W: while the current Coq version is $(COQ_VERSION)";\ + fi +.PHONY: pre-all -ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo) -CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES)) -CMXFILES=$(CMOFILES:.cmo=.cmx) -OFILES=$(CMXFILES:.cmx=.o) -CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi)) -CMXSFILES=$(CMXFILES:.cmx=.cmxs) -ifeq '$(HASNATDYNLINK)' 'true' -HASNATDYNLINK_OR_EMPTY := yes -else -HASNATDYNLINK_OR_EMPTY := -endif +post-all:: + @# Extension point +.PHONY: post-all -####################################### -# # -# Definition of the toplevel targets. # -# # -####################################### +real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) +.PHONY: real-all -all: $(VOFILES) $(CMOFILES) $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) +real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) +.PHONE: real-all.timing.diff -mlihtml: $(MLIFILES:.mli=.cmi) - mkdir $@ || rm -rf $@/* - $(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) +bytefiles: $(CMOFILES) $(CMAFILES) +.PHONY: bytefiles -all-mli.tex: $(MLIFILES:.mli=.cmi) - $(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) +optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) +.PHONY: optfiles +# FIXME, see Ralph's bugreport quick: $(VOFILES:.vo=.vio) +.PHONY: quick vio2vo: - $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -checkproofs: - $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -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) + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ + -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +.PHONY: vio2vo -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 $^` +checkproofs: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ + -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) +.PHONY: checkproofs validate: $(VOFILES) - $(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=)) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=)) +.PHONY: validate -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/' +only: $(TGTS) +.PHONY: only -.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo ./ smtcoq_plugin.mlpack.d +# Documentation targets ####################################################### -################### -# # -# Custom targets. # -# # -################### - -test: - cd ../unit-tests; make - -ztest: - cd ../unit-tests; make zchaff - -vtest: - cd ../unit-tests; make verit - -lfsctest: - cd ../unit-tests; make lfsc - -%.ml: %.mll - $(CAMLLEX) $< - -%.ml %.mli: %.mly - $(CAMLYACC) $< - -smtcoq_plugin.mlpack.d: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml +html: $(GLOBFILES) $(VFILES) + $(SHOW)'COQDOC -d html $(GAL)' + $(HIDE)mkdir -p html + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) -################### -# # -# Subdirectories. # -# # -################### +mlihtml: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -d $@' + $(HIDE)mkdir $@ || rm -rf $@/* + $(HIDE)$(CAMLDOC) -html \ + -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) -./: - +cd "./" && $(MAKE) all +all-mli.tex: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -latex $@' + $(HIDE)$(CAMLDOC) -latex \ + -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) -##################################### -# # -# Ad-hoc implicit rules for mlpack. # -# # -##################################### +gallina: $(GFILES) -$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(smtcoq_plugin_MLPACK_DEPENDENCIES))): %.cmx: %.ml - $(SHOW)'CAMLOPT -c -for-pack Smtcoq_plugin $<' - $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack Smtcoq_plugin $< +all.ps: $(VFILES) + $(SHOW)'COQDOC -ps $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` -$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(smtcoq_plugin_MLPACK_DEPENDENCIES))): %.cmx: %.ml4 - $(SHOW)'CAMLOPT -c -pp -for-pack Smtcoq_plugin $<' - $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack Smtcoq_plugin $(PP) -impl $< +all.pdf: $(VFILES) + $(SHOW)'COQDOC -pdf $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` -#################### -# # -# Special targets. # -# # -#################### +# FIXME: not quite right, since the output name is different +gallinahtml: GAL=-g +gallinahtml: html -byte: - $(MAKE) all "OPT:=-byte" +all-gal.ps: GAL=-g +all-gal.ps: all.ps -opt: - $(MAKE) all "OPT:=-opt" +all-gal.pdf: GAL=-g +all-gal.pdf: all.pdf -userinstall: - +$(MAKE) USERINSTALL=true install +# ? +beautify: $(BEAUTYFILES) + 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: beautify -install-natdynlink: - cd "." && for i in $(CMXSFILES); do \ - install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \ - install -m 0755 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \ +# Installation targets ######################################################## +# +# There rules can be extended in Makefile.local +# Extensions can't assume when they run. + +install: + $(HIDE)for f in $(FILESTOINSTALL); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ done - -install-toploop: $(MLLIBFILES:.mllib=.cmxs) - install -d "$(DSTROOT)"$(COQTOPINSTALL)/ - install -m 0755 $? "$(DSTROOT)"$(COQTOPINSTALL)/ - -install:$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink) - cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \ - install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \ - install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \ + $(HIDE)$(MAKE) install-extra -f "$(SELF)" +install-extra:: + @# Extension point +.PHONY: install install-extra + +install-byte: + $(HIDE)for f in $(BYTEFILESTOINSTALL); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ done -install-doc: - install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/html - for i in html/*; do \ - install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/$$i;\ +install-doc:: html mlihtml + @# Extension point + $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(HIDE)for i in html/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ done - install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/mlihtml - for i in mlihtml/*; do \ - install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/$$i;\ + $(HIDE)install -d \ + "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE)for i in mlihtml/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ done - -uninstall_me.sh: Makefile - echo '#!/bin/sh' > $@ - printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/SMTCoq && rm -f $(CMXSFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "SMTCoq" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/SMTCoq && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "SMTCoq" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/SMTCoq \\\n' >> "$@" - printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find SMTCoq/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/SMTCoq \\\n' >> "$@" - printf '&& rm -f $(shell find "mlihtml" -maxdepth 1 -and -type f -print)\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find SMTCoq/mlihtml -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - chmod +x $@ - -uninstall: uninstall_me.sh - sh $< - -.merlin: - @echo 'FLG -rectypes' > .merlin - @echo "B $(COQLIB)kernel" >> .merlin - @echo "B $(COQLIB)lib" >> .merlin - @echo "B $(COQLIB)library" >> .merlin - @echo "B $(COQLIB)parsing" >> .merlin - @echo "B $(COQLIB)pretyping" >> .merlin - @echo "B $(COQLIB)interp" >> .merlin - @echo "B $(COQLIB)printing" >> .merlin - @echo "B $(COQLIB)intf" >> .merlin - @echo "B $(COQLIB)proofs" >> .merlin - @echo "B $(COQLIB)tactics" >> .merlin - @echo "B $(COQLIB)tools" >> .merlin - @echo "B $(COQLIB)ltacprof" >> .merlin - @echo "B $(COQLIB)toplevel" >> .merlin - @echo "B $(COQLIB)stm" >> .merlin - @echo "B $(COQLIB)grammar" >> .merlin - @echo "B $(COQLIB)config" >> .merlin - @echo "B $(COQLIB)ltac" >> .merlin - @echo "B $(COQLIB)engine" >> .merlin - @echo "B /home/artemis/Recherche/github.com/ckeller/smtcoq-lfsc/src/versions/standard" >> .merlin - @echo "S /home/artemis/Recherche/github.com/ckeller/smtcoq-lfsc/src/versions/standard" >> .merlin - @echo "B bva" >> .merlin - @echo "S bva" >> .merlin - @echo "B classes" >> .merlin - @echo "S classes" >> .merlin - @echo "B array" >> .merlin - @echo "S array" >> .merlin - @echo "B cnf" >> .merlin - @echo "S cnf" >> .merlin - @echo "B euf" >> .merlin - @echo "S euf" >> .merlin - @echo "B lfsc" >> .merlin - @echo "S lfsc" >> .merlin - @echo "B lia" >> .merlin - @echo "S lia" >> .merlin - @echo "B smtlib2" >> .merlin - @echo "S smtlib2" >> .merlin - @echo "B trace" >> .merlin - @echo "S trace" >> .merlin - @echo "B verit" >> .merlin - @echo "S verit" >> .merlin - @echo "B zchaff" >> .merlin - @echo "S zchaff" >> .merlin - @echo "B versions/standard" >> .merlin - @echo "S versions/standard" >> .merlin - @echo "B versions/standard/Int63" >> .merlin - @echo "S versions/standard/Int63" >> .merlin - @echo "B versions/standard/Array" >> .merlin - @echo "S versions/standard/Array" >> .merlin - @echo "B $(shell $(COQBIN)coqc -where)/plugins/micromega" >> .merlin - @echo "S $(shell $(COQBIN)coqc -where)/plugins/micromega" >> .merlin +.PHONY: install-doc + +uninstall:: + @# Extension point + $(HIDE)for f in $(FILESTOINSTALL); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" &&\ + (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ + done +.PHONY: uninstall + +uninstall-doc:: + @# Extension point + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true +.PHONY: uninstall-doc + +# Cleaning #################################################################### +# +# There rules can be extended in Makefile.local +# Extensions can't assume when they run. 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) $(NATIVEFILES) - find . -name .coq-native -type d -empty -delete - rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(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 uninstall_me.sh - - rm -rf test - - rm -rf ztest - - rm -rf vtest - - rm -rf lfsctest - - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml + @# Extension point + $(SHOW)'CLEAN' + $(HIDE)rm -f $(CMOFILES) + $(HIDE)rm -f $(CMIFILES) + $(HIDE)rm -f $(CMAFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.cmx) + $(HIDE)rm -f $(CMXAFILES) + $(HIDE)rm -f $(CMXSFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.o) + $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(ALLDFILES) + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)find . -name .coq-native -type d -empty -delete + $(HIDE)rm -f $(VOFILES) + $(HIDE)rm -f $(VOFILES:.vo=.vio) + $(HIDE)rm -f $(GFILES) + $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) + $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex + $(HIDE)rm -f $(VFILES:.v=.glob) + $(HIDE)rm -f $(VFILES:.v=.tex) + $(HIDE)rm -f $(VFILES:.v=.g.tex) + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)rm -rf html mlihtml +.PHONY: clean cleanall:: clean - rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + @# Extension point + $(SHOW)'CLEAN *.aux *.timing' + $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) +.PHONY: cleanall archclean:: - rm -f *.cmx *.o - +cd ./ && $(MAKE) archclean + @# Extension point + $(SHOW)'CLEAN *.cmx *.o' + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) +.PHONY: archclean -printenv: - @"$(COQBIN)coqtop" -config - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'PP = $(PP)' - @echo 'COQFLAGS = $(COQFLAGS)' - @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' - @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' - -################### -# # -# Implicit rules. # -# # -################### +# Compilation rules ########################################################### $(MLIFILES:.mli=.cmi): %.cmi: %.mli $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< $(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 $(SHOW)'CAMLC -pp -c $<' - $(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $< -$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4 - $(SHOW)'CAMLOPT -pp -c $<' - $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 - $(SHOW)'CAMLDEP -pp $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) +$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 + $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< $(MLFILES:.ml=.cmo): %.cmo: %.ml $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $< + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< -$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml - $(SHOW)'CAMLOPT -c $<' - $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $< +$(MLFILES:.ml=.cmx): %.cmx: %.ml + $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< -$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) -$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx +$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -linkall -shared -o $@ $< -$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa +$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + +$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + + +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -linkall -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< + +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^ + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack $(SHOW)'CAMLOPT -pack -o $@' - $(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^ + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ -$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) +# This rule is for _CoqProject with no .mllib nor .mlpack +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx + $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -o $@ $< + +ifneq (,$(TIMING)) +TIMING_EXTRA = > $<.$(TIMING_EXT) +else +TIMING_EXTRA = +endif $(VOFILES): %.vo: %.v $(SHOW)COQC $< - $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA) +# FIXME ?merge with .vo / .vio ? $(GLOBFILES): %.glob: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $< + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< $(VFILES:.v=.vio): %.vio: %.v - $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< + $(SHOW)COQC -quick $< + $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< + +$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing + $(SHOW)PYTHON TIMING-DIFF $< + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" + +$(BEAUTYFILES): %.v.beautified: %.v + $(SHOW)'BEAUTIFY $<' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $< $(GFILES): %.g: %.v - $(GALLINA) $< + $(SHOW)'GALLINA $<' + $(HIDE)$(GALLINA) $< -$(VFILES:.v=.tex): %.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ +$(TEXFILES): %.tex: %.v + $(SHOW)'COQDOC -latex $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ -$(HTMLFILES): %.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ +$(GTEXFILES): %.g.tex: %.v + $(SHOW)'COQDOC -latex -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ -$(VFILES:.v=.g.tex): %.g.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ +$(HTMLFILES): %.html: %.v %.glob + $(SHOW)'COQDOC -html $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ $(GHTMLFILES): %.g.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ + $(SHOW)'COQDOC -html -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ + +# Dependency files ############################################################ + +ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) +else + ifeq ($(MAKECMDGOALS),) + -include $(ALLDFILES) + endif +endif + +.SECONDARY: $(ALLDFILES) + +redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) + +$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 + $(SHOW)'CAMLDEP -pp $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) $(addsuffix .d,$(VFILES)): %.v.d: %.v $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(redir_if_ok) -$(addsuffix .beautified,$(VFILES)): %.v.beautified: - $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v +# Misc ######################################################################## -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING +byte: + $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" +.PHONY: byte +opt: + $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" +.PHONY: opt + +# This is deprecated. To extend this makefile use +# extension points and Makefile.local +printenv:: + $(warning printenv is deprecated) + $(warning write extensions in Makefile.local or include Makefile.conf) + @echo 'LOCAL = $(LOCAL)' + @echo 'COQLIB = $(COQLIB)' + @echo 'DOCDIR = $(DOCDIR)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'CAMLP4 = $(CAMLP4)' + @echo 'CAMLP4O = $(CAMLP4O)' + @echo 'CAMLP4BIN = $(CAMLP4BIN)' + @echo 'CAMLP4LIB = $(CAMLP4LIB)' + @echo 'CAMLP4OPTIONS = $(CAMLP4OPTIONS)' + @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' + @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' + @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'PP = $(PP)' + @echo 'COQFLAGS = $(COQFLAGS)' + @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' + @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' +.PHONY: printenv + +# Generate a .merlin file. If you need to append directives to this +# file you can extend the merlin-hook target in Makefile.local +.merlin: + $(SHOW)'FILL .merlin' + $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin + $(HIDE)echo 'B $(COQLIB)' >> .merlin + $(HIDE)echo 'S $(COQLIB)' >> .merlin + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo 'B $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo 'S $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) + $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" +.PHONY: merlin + +merlin-hook:: + @# Extension point +.PHONY: merlin-hook + +# prints all variables +debug: + $(foreach v,\ + $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ + $(.VARIABLES))),\ + $(info $(v) = $($(v)))) +.PHONY: debug + +.DEFAULT_GOAL := all diff --git a/src/versions/standard/Makefile.conf b/src/versions/standard/Makefile.conf new file mode 100644 index 0000000..928db7d --- /dev/null +++ b/src/versions/standard/Makefile.conf @@ -0,0 +1,103 @@ +# This configuration file was generated by running: +# coq_makefile -f Make -o Makefile + + +############################################################################### +# # +# Project files. # +# # +############################################################################### + +COQMF_VFILES = 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 bva/BVList.v bva/Bva_checker.v classes/SMT_classes.v classes/SMT_classes_instances.v array/FArray.v array/Array_checker.v cnf/Cnf.v euf/Euf.v 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 +COQMF_MLIFILES = versions/standard/structures.mli trace/coqTerms.mli trace/smtBtype.mli trace/satAtom.mli trace/smtAtom.mli trace/smtCertif.mli trace/smtCnf.mli trace/smtCommands.mli trace/smtForm.mli trace/smtMisc.mli trace/smtTrace.mli smtlib2/smtlib2_parse.mli smtlib2/smtlib2_lex.mli smtlib2/smtlib2_ast.mli smtlib2/smtlib2_genConstr.mli smtlib2/smtlib2_util.mli smtlib2/sExpr.mli smtlib2/smtlib2_solver.mli smtlib2/sExprParser.mli verit/veritParser.mli verit/veritLexer.mli verit/verit.mli verit/veritSyntax.mli lfsc/shashcons.mli lfsc/hstring.mli lfsc/lfscParser.mli lfsc/ast.mli lfsc/translator_sig.mli lfsc/tosmtcoq.mli zchaff/cnfParser.mli zchaff/satParser.mli zchaff/zchaff.mli zchaff/zchaffParser.mli lia/lia.mli +COQMF_MLFILES = versions/standard/structures.ml trace/coqTerms.ml trace/smtBtype.ml trace/satAtom.ml trace/smtAtom.ml trace/smtCertif.ml trace/smtCnf.ml trace/smtCommands.ml trace/smtForm.ml trace/smtMisc.ml trace/smtTrace.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/smtlib2_ast.ml smtlib2/smtlib2_genConstr.ml smtlib2/smtlib2_util.ml smtlib2/sExpr.ml smtlib2/smtlib2_solver.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml verit/veritParser.ml verit/veritLexer.ml verit/verit.ml verit/veritSyntax.ml lfsc/shashcons.ml lfsc/hstring.ml lfsc/lfscParser.ml lfsc/type.ml lfsc/ast.ml lfsc/builtin.ml lfsc/tosmtcoq.ml lfsc/converter.ml lfsc/lfsc.ml lfsc/lfscLexer.ml zchaff/cnfParser.ml zchaff/satParser.ml zchaff/zchaff.ml zchaff/zchaffParser.ml lia/lia.ml +COQMF_ML4FILES = g_smtcoq.ml4 +COQMF_MLPACKFILES = smtcoq_plugin.mlpack +COQMF_MLLIBFILES = + +############################################################################### +# # +# Path directives (-I, -R, -Q). # +# # +############################################################################### + +COQMF_OCAMLLIBS = -I . -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/standard -I versions/standard/Int63 -I versions/standard/Array -I '$(shell $(COQBIN)coqc -where)/plugins/micromega' +COQMF_SRC_SUBDIRS = . bva classes array cnf euf lfsc lia smtlib2 trace verit zchaff versions/standard versions/standard/Int63 versions/standard/Array '$(shell $(COQBIN)coqc -where)/plugins/micromega' +COQMF_COQLIBS = -I . -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/standard -I versions/standard/Int63 -I versions/standard/Array -I '$(shell $(COQBIN)coqc -where)/plugins/micromega' -R . SMTCoq +COQMF_COQLIBS_NOML = -R . SMTCoq + +############################################################################### +# # +# Coq configuration. # +# # +############################################################################### + +COQMF_LOCAL=1 +COQMF_COQLIB=/home/artemis/Autres/coq-8.7.2// +COQMF_DOCDIR=/home/artemis/Autres/coq-8.7.2/doc/ +COQMF_OCAMLFIND=/usr/bin/ocamlfind +COQMF_CAMLP4=camlp5 +COQMF_CAMLP4O=/usr/bin/camlp5o +COQMF_CAMLP4BIN=/usr/bin/ +COQMF_CAMLP4LIB=/usr/lib/ocaml/camlp5 +COQMF_CAMLP4OPTIONS=-loc loc +COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50 -safe-string +COQMF_HASNATDYNLINK=true +COQMF_COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml +COQMF_WINDRIVE=/home/artemis/Autres/coq-8.7.2 + +############################################################################### +# # +# Extra variables. # +# # +############################################################################### + +CAMLLEX = $(CAMLBIN)ocamllex +CAMLYACC = $(CAMLBIN)ocamlyacc +COQMF_OTHERFLAGS = +COQMF_INSTALLCOQDOCROOT = SMTCoq + +############################################################################### +# # +# Extra targets. (-extra and -extra-phony, DEPRECATED) # +# # +############################################################################### + +post-all:: + $(MAKE) -f $(SELF) test +clean:: + rm -f test +test : + cd ../unit-tests; make + +post-all:: + $(MAKE) -f $(SELF) ztest +clean:: + rm -f ztest +ztest : + cd ../unit-tests; make zchaff + +post-all:: + $(MAKE) -f $(SELF) vtest +clean:: + rm -f vtest +vtest : + cd ../unit-tests; make verit + +post-all:: + $(MAKE) -f $(SELF) lfsctest +clean:: + rm -f lfsctest +lfsctest : + cd ../unit-tests; make lfsc + +%.ml : %.mll + $(CAMLLEX) $< + +%.ml %.mli : %.mly + $(CAMLYACC) $< + +.PHONY: smtcoq_plugin.mlpack.d +smtcoq_plugin.mlpack.d : verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml + + diff --git a/src/versions/standard/Structures_standard.v b/src/versions/standard/Structures_standard.v index 4894ebd..d6c4435 100644 --- a/src/versions/standard/Structures_standard.v +++ b/src/versions/standard/Structures_standard.v @@ -50,6 +50,15 @@ Section Trace. 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/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4 index 2cc4415..bf923cc 100644 --- a/src/versions/standard/g_smtcoq_standard.ml4 +++ b/src/versions/standard/g_smtcoq_standard.ml4 @@ -12,9 +12,12 @@ DECLARE PLUGIN "smtcoq_plugin" -open Genarg open Stdarg -open Constrarg + +(* This is requires since Coq 8.7 because the Ltac machinery became a + plugin + see: https://lists.gforge.inria.fr/pipermail/coq-commits/2017-February/021276.html *) +open Ltac_plugin VERNAC COMMAND EXTEND Vernac_zchaff CLASSIFIED AS QUERY | [ "Parse_certif_zchaff" @@ -86,8 +89,8 @@ END 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) ] -> [ Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) !lemmas_list ] +| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) !lemmas_list ] END TACTIC EXTEND Tactic_cvc4 diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index cf5a272..74caf8b 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -11,10 +11,12 @@ open Entries -open Coqlib +(* Constr generation and manipulation *) + let mklApp f args = Term.mkApp (Lazy.force f, args) +let gen_constant_in_modules s m n = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) @@ -75,17 +77,15 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = (* Differences between the two versions of Coq *) -let dummy_loc = Loc.ghost - -let mkUConst c = +let mkUConst : Term.constr -> Safe_typing.private_constants Entries.definition_entry = fun c -> let env = Global.env () in let evd = Evd.from_env env in - let evd, ty = Typing.type_of env evd c in - { const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), + let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in + { Entries.const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants); const_entry_secctx = None; const_entry_feedback = None; - const_entry_type = Some ty; + const_entry_type = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Term.constr *) const_entry_polymorphic = false; const_entry_universes = snd (Evd.universe_context evd); const_entry_opaque = false; @@ -94,7 +94,7 @@ let mkUConst c = let mkTConst c noc ty = let env = Global.env () in let evd = Evd.from_env env in - let evd, _ = Typing.type_of env evd noc in + let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in { const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants); const_entry_secctx = None; @@ -105,25 +105,25 @@ let mkTConst c noc ty = const_entry_opaque = false; const_entry_inline_code = false } -let error = CErrors.error +let error s = CErrors.user_err (Pp.str s) let coqtype = Future.from_val Term.mkSet let declare_new_type t = - let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Future.force coqtype, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, t) in + let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Future.force coqtype, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (None, t) in Term.mkVar t let declare_new_variable v constr_t = let env = Global.env () in let evd = Evd.from_env env in - let evd, _ = Typing.type_of env evd constr_t in - let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.universe_context_set evd) [] [] false Vernacexpr.NoInline (dummy_loc, v) in + let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in + let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.universe_context_set evd) [] [] false Vernacexpr.NoInline (None, v) in Term.mkVar v -let extern_constr = Constrextern.extern_constr true Environ.empty_env Evd.empty +let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c) let vernacentries_interp expr = - Vernacentries.interp (dummy_loc, Vernacexpr.VernacCheckMayEval (Some (Genredexpr.CbvVm None), None, expr)) + Vernacentries.interp (None, Vernacexpr.VernacCheckMayEval (Some (Genredexpr.CbvVm None), None, expr)) let pr_constr_env env = Printer.pr_constr_env env Evd.empty @@ -136,43 +136,60 @@ let interp_constr env sigma t = Constrintern.interp_constr env sigma t |> fst let tclTHEN = Tacticals.New.tclTHEN let tclTHENLAST = Tacticals.New.tclTHENLAST -let assert_before = Tactics.assert_before +let assert_before n c = Tactics.assert_before n (EConstr.of_constr c) let vm_conv = Vconv.vm_conv -let vm_cast_no_check t = Tactics.vm_cast_no_check t +let vm_cast_no_check c = Tactics.vm_cast_no_check (EConstr.of_constr c) +(* Cannot contain evars since it comes from a Term.constr *) +let cbv_vm env c t = EConstr.Unsafe.to_constr (Vnorm.cbv_vm env Evd.empty (EConstr.of_constr c) (EConstr.of_constr t)) -(* Warning 40: this record of type Proofview.Goal.enter contains fields - that are not visible in the current scope: enter. *) let mk_tactic tac = - Proofview.Goal.nf_enter {Proofview.Goal.enter = (fun gl -> + Proofview.Goal.nf_enter (fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let t = Proofview.Goal.concl gl in + let t = EConstr.to_constr sigma t in (* The goal should not contain uninstanciated evars *) tac env sigma t - )} + ) let set_evars_tac noc = mk_tactic ( fun env sigma _ -> - let sigma, _ = Typing.type_of env sigma noc in + let sigma, _ = Typing.type_of env sigma (EConstr.of_constr noc) in Proofview.Unsafe.tclEVARS sigma) let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr -let constrextern_extern_constr = +let constrextern_extern_constr c = let env = Global.env () in - Constrextern.extern_constr false env (Evd.from_env env) + Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c) let get_rel_dec_name = function | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> n +let retyping_get_type_of env sigma c = + (* Cannot contain evars since it comes from a Term.constr *) + EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)) -(* New packaging of plugins *) + +(* Micromega *) module Micromega_plugin_Certificate = Micromega_plugin.Certificate module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega module Micromega_plugin_Micromega = Micromega_plugin.Micromega module Micromega_plugin_Mutils = Micromega_plugin.Mutils +let micromega_coq_proofTerm = + (* Cannot contain evars *) + lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin.Coq_micromega.M.coq_proofTerm))) + +let micromega_dump_proof_term p = + (* Cannot contain evars *) + EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p) + (* Types in the Coq source code *) type tactic = unit Proofview.tactic type names_id = Names.Id.t type constr_expr = Constrexpr.constr_expr + +(* EConstr *) +type econstr = EConstr.t +let econstr_of_constr = EConstr.of_constr diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index b17aa3c..3d17203 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -10,8 +10,13 @@ (**************************************************************************) +(* Constr generation and manipulation *) +(* WARNING: currently, we map all the econstr into constr: we suppose + that the goal does not contain existencial variables *) val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr val gen_constant : string list list -> string -> Term.constr lazy_t + +(* Int63 *) val int63_modules : string list list val int31_module : string list list val cD0 : Term.constr lazy_t @@ -19,11 +24,15 @@ val cD1 : Term.constr lazy_t val cI31 : Term.constr lazy_t val mkInt : int -> Term.constr val cint : Term.constr lazy_t + +(* PArray *) val parray_modules : string list list val cmake : Term.constr lazy_t val cset : Term.constr lazy_t val max_array_size : int val mkArray : Term.types * Term.constr array -> Term.constr + +(* Traces *) val mkTrace : ('a -> Term.constr) -> ('a -> 'a) -> @@ -33,7 +42,8 @@ val mkTrace : Term.constr Lazy.t -> Term.constr Lazy.t -> int -> Term.constr -> Term.constr -> 'a ref -> Term.constr -val dummy_loc : Loc.t + +(* Differences between the two versions of Coq *) val mkUConst : Term.constr -> Safe_typing.private_constants Entries.definition_entry val mkTConst : @@ -55,8 +65,11 @@ val tclTHEN : val tclTHENLAST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic val assert_before : Names.Name.t -> Term.types -> unit Proofview.tactic + val vm_conv : Reduction.conv_pb -> Term.types Reduction.kernel_conversion_function val vm_cast_no_check : Term.constr -> unit Proofview.tactic +val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr + val mk_tactic : (Environ.env -> Evd.evar_map -> Term.constr -> unit Proofview.tactic) -> unit Proofview.tactic @@ -64,16 +77,24 @@ val set_evars_tac : Term.constr -> unit Proofview.tactic val ppconstr_lsimpleconstr : Ppconstr.precedence val constrextern_extern_constr : Term.constr -> Constrexpr.constr_expr val get_rel_dec_name : Context.Rel.Declaration.t -> Names.Name.t +val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr -(* New packaging of plugins *) +(* Micromega *) module Micromega_plugin_Certificate = Micromega_plugin.Certificate module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega module Micromega_plugin_Micromega = Micromega_plugin.Micromega module Micromega_plugin_Mutils = Micromega_plugin.Mutils +val micromega_coq_proofTerm : Term.constr lazy_t +val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr + (* Types in the Coq source code *) type tactic = unit Proofview.tactic type names_id = Names.Id.t type constr_expr = Constrexpr.constr_expr + +(* EConstr *) +type econstr = EConstr.t +val econstr_of_constr : Term.constr -> econstr -- cgit