aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-03-08 12:47:05 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-03-08 12:47:05 +0000
commitcd798e8cb6f2f5123d61de10172b9dbbcb46f86f (patch)
treee5c7297ae741f6f4cdfe690004165c17f2385675
parent042a9e9156c183e705a5d5dddd4f2842fa57b943 (diff)
Application des patches envoyés par F. Besson pour micromega
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--config/coq_config.mli2
-rwxr-xr-xconfigure86
-rw-r--r--plugins/micromega/Psatz.v37
-rw-r--r--plugins/micromega/coq_micromega.ml2122
4 files changed, 1211 insertions, 1036 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 2cd1e4543..5feb96303 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -55,6 +55,8 @@ val plugins_dirs : string list
val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *)
+val csdp : string option (* the path to CSDP, for the Micromega plugin *)
+
val browser : string
(** default web browser to use, may be overriden by environment
variable COQREMOTEBROWSER *)
diff --git a/configure b/configure
index 8e3780c02..82abb5150 100755
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
##################################
#
@@ -69,6 +69,8 @@ usage () {
printf "\tSpecifies whether or not to compile Coqide\n"
echo "-uim-script-path"
printf "\tSpecifies where uim's .scm files are installed\n"
+ echo "-csdpdir <dir>"
+ printf "\tSpecifies the path of the CSDP solver intallation\n"
echo "-browser <command>"
printf "\tUse <command> to open URL %%s\n"
echo "-with-doc (yes|no)"
@@ -117,6 +119,8 @@ gcc_exec=gcc
ar_exec=ar
ranlib_exec=ranlib
+csdpexec=
+
local=false
coqrunbyteflags_spec=no
coqtoolsbyteflags_spec=no
@@ -213,6 +217,9 @@ while : ; do
*) COQIDE=no
esac
shift;;
+ -csdpdir|--csdpdir)
+ csdpdir="$2"
+ shift;;
-browser|--browser) browser_spec=yes
BROWSER=$2
shift;;
@@ -261,7 +268,7 @@ while : ; do
done
if [ $prefix_spec = yes -a $local = true ] ; then
- echo "Options -prefix and -local are incompatible"
+ echo "Options -prefix and -local are incompatible."
echo "Configure script failed!"
exit 1
fi
@@ -295,7 +302,7 @@ case $arch_spec in
elif test -x /usr/bin/uname ; then
ARCH=`/usr/bin/uname -s`
else
- echo "I can not automatically find the name of your architecture"
+ echo "I can not automatically find the name of your architecture."
printf "%s"\
"Give me a name, please [win32 for Win95, Win98 or WinNT]: "
read ARCH
@@ -341,7 +348,7 @@ if [ "$MAKE" != "" ]; then
if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
fi
if [ $OK = "no" ]; then
- echo "GNU Make >= 3.81 is needed"
+ echo "GNU Make >= 3.81 is needed."
echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz"
echo "then locally installed on a Unix-style system by issuing:"
echo " tar xzvf make-3.81.tar.gz"
@@ -350,14 +357,14 @@ if [ "$MAKE" != "" ]; then
echo " make"
echo " mv make .."
echo " cd .."
- echo "Restart then the configure script and later use ./make instead of make"
+ echo "Restart then the configure script and later use ./make instead of make."
exit 1
else
echo "You have locally installed GNU Make 3.81. Good!"
fi
esac
else
- echo "Cannot find GNU Make 3.81"
+ echo "Cannot find GNU Make 3.81."
fi
# Browser command
@@ -407,7 +414,7 @@ case $camldir_spec in
esac
if test ! -f "$CAMLC" ; then
- echo "I can not find the executable '$CAMLC'! (Have you installed it?)"
+ echo "I can not find the executable '$CAMLC'. Have you installed it?"
echo "Configuration script failed!"
exit 1
fi
@@ -423,10 +430,10 @@ case $CAMLVERSION in
1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09.[012])
echo "Your version of Objective-Caml is $CAMLVERSION."
if [ "$force_caml_version" = "yes" ]; then
- echo "WARNING: you are compiling Coq with an outdated version of Objective-Caml"
+ echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml."
else
- echo "You need Objective-Caml 3.09.3 or later"
- echo "Configuration script failed!"
+ echo " You need Objective-Caml 3.09.3 or later."
+ echo " Configuration script failed!"
exit 1
fi;;
?*)
@@ -487,7 +494,7 @@ if [ "$camlp5dir" != "" ]; then
CAMLP4=camlp5
CAMLP4LIB=$camlp5dir
if [ ! -f $camlp5dir/camlp5.cma ]; then
- echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)"
+ echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
echo "Configuration script failed!"
exit 1
fi
@@ -651,6 +658,51 @@ if which uim-fep; then
done
fi
+# Borcher's C library for semidefinite programming (CSDP) is required for the
+# micromega plugin to be fully functional.
+#
+# We test for its presence; when not found we
+# - fail if the path was explicitely provided via the "-csdpdir" option,
+# - issue a warning else.
+
+if [ "$csdpdir" != "" ]; then
+ if [ ! -f "$csdpdir/csdp" ]; then
+ echo "Cannot find the csdp binary in $csdpdir ($csdpdir/csdp not found)."
+ echo "Configuration script failed!"
+ exit 1
+ else
+ if [ ! -x "$csdpdir/csdp" ]; then
+ echo "The csdp binary in $csdpdir is not executable: check your permissions."
+ echo "Configuration script failed!"
+ exit 1
+ fi
+ fi
+ USE_CSDP="yes"
+ CSDP=$csdpdir/csdp
+else
+ CSDP=`which csdp`
+ if [ ! -f "$CSDP" ]; then
+ echo "*Warning* Cannot find the csdp executable. Have you installed it?"
+ echo " CSDP can be found pre-packaged as part of your software distribution,"
+ echo " or at https://projects.coin-or.org/csdp."
+ USE_CSDP="no"
+ else
+ if [ ! -x "$CSDP" ]; then
+ echo "*Warning* The csdp binary at $CSDP is not executable: check your permissions."
+ USE_CSDP="noexec"
+ else
+ USE_CSDP="yes"
+ fi
+ fi
+fi
+
+# Finally, set the ML configuration variable to reflect the state of the CSDP
+# installation.
+case $USE_CSDP in
+ yes) csdpexec="Some \"$CSDP\"";;
+ no|noexec) csdpexec="None";;
+esac
+
# strip command
case $ARCH in
@@ -865,6 +917,13 @@ else
echo " Documentation : None"
fi
echo " CoqIde : $COQIDE"
+if test "$USE_CSDP" = "yes"; then
+echo " CSDP for Micromega : $CSDP"
+else if test "$USE_CSDP" = "no"; then
+echo " CSDP for Micromega : None"
+else if test "$USE_CSDP" = "noexec"; then
+echo " CSDP for Micromega : $CSDP found, but is not executable"
+fi fi fi
echo " Web browser : $BROWSER"
echo " Coq web site : $WWWCOQ"
echo ""
@@ -1008,6 +1067,7 @@ let vo_magic_number = $VOMAGIC
let state_magic_number = $STATEMAGIC
let exec_extension = "$EXE"
let with_geoproof = ref $with_geoproof
+let csdp = $csdpexec
let browser = "$BROWSER"
let wwwcoq = "$WWWCOQ"
let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
@@ -1099,9 +1159,9 @@ chmod a-w "$config_file"
# The end
####################################################
-echo "If anything in the above is wrong, please restart './configure'"
+echo "If anything in the above is wrong, please restart './configure'."
echo
echo "*Warning* To compile the system for a new architecture"
echo " don't forget to do a 'make archclean' before './configure'."
-# $Id$
+# $Id: configure 12689 2010-01-26 13:41:56Z glondu $
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index a2b10ebaa..444a590a1 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -33,14 +33,18 @@ Ltac xpsatz dom d :=
apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
| R =>
(sos_R || psatz_R d) ;
- intros __wit __varmap __ff ;
- change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
- apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity
+ (* If csdp is not installed, the previous step might not produce any
+ progress: the rest of the tactical will then fail. Hence the 'try'. *)
+ try (intros __wit __varmap __ff ;
+ change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
+ apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
| Q =>
- (sos_Q || psatz_Q d) ;
- intros __wit __varmap __ff ;
- change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
- apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity
+ (sos_Q || psatz_Q d) ;
+ (* If csdp is not installed, the previous step might not produce any
+ progress: the rest of the tactical will then fail. Hence the 'try'. *)
+ try (intros __wit __varmap __ff ;
+ change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
+ apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
| _ => fail "Unsupported domain"
end in tac.
@@ -56,26 +60,27 @@ Ltac psatzl dom :=
apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
| Q =>
psatzl_Q ;
- intros __wit __varmap __ff ;
- change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
- apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity
+ (* If csdp is not installed, the previous step might not produce any
+ progress: the rest of the tactical will then fail. Hence the 'try'. *)
+ try (intros __wit __varmap __ff ;
+ change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
+ apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
| R =>
psatzl_R ;
- intros __wit __varmap __ff ;
- change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
- apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity
+ (* If csdp is not installed, the previous step might not produce any
+ progress: the rest of the tactical will then fail. Hence the 'try'. *)
+ try (intros __wit __varmap __ff ;
+ change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
+ apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
| _ => fail "Unsupported domain"
end in tac.
-
-
Ltac lia :=
xlia ;
intros __wit __varmap __ff ;
change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
-
(* Local Variables: *)
(* coding: utf-8 *)
(* End: *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 10cde3c56..88b4f90e6 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -8,13 +8,26 @@
(* *)
(* Micromega: A reflexive tactic using the Positivstellensatz *)
(* *)
+(* ** Toplevel definition of tactics ** *)
+(* *)
+(* - Modules ISet, M, Mc, Env, Cache, CacheZ *)
+(* *)
(* Frédéric Besson (Irisa/Inria) 2006-2009 *)
(* *)
(************************************************************************)
open Mutils
+
+(**
+ * Debug flag
+ *)
+
let debug = false
+(**
+ * Time function
+ *)
+
let time str f x =
let t0 = (Unix.times()).Unix.tms_utime in
let res = f x in
@@ -23,20 +36,40 @@ let time str f x =
flush stdout);
res
+(**
+ * Initialize a tag type to the Tag module declaration (see Mutils).
+ *)
type tag = Tag.t
+
+(**
+ * An atom is of the form:
+ * pExpr1 {<,>,=,<>,<=,>=} pExpr2
+ * where pExpr1, pExpr2 are polynomial expressions (see Micromega). pExprs are
+ * parametrized by 'cst, which is used as the type of constants.
+ *)
+
type 'cst atom = 'cst Micromega.formula
+(**
+ * Micromega's encoding of formulas.
+ * By order of appearance: boolean constants, variables, atoms, conjunctions,
+ * disjunctions, negation, implication.
+ *)
+
type 'cst formula =
| TT
| FF
| X of Term.constr
| A of 'cst atom * tag * Term.constr
- | C of 'cst formula * 'cst formula
+ | C of 'cst formula * 'cst formula
| D of 'cst formula * 'cst formula
| N of 'cst formula
| I of 'cst formula * Names.identifier option * 'cst formula
+(**
+ * Formula pretty-printer.
+ *)
let rec pp_formula o f =
match f with
@@ -53,891 +86,925 @@ let rec pp_formula o f =
| None -> "") pp_formula f2
| N(f) -> Printf.fprintf o "N(%a)" pp_formula f
+(**
+ * Collect the identifiers of a (string of) implications. Implication labels
+ * are inherited from Coq/CoC's higher order dependent type constructor (Pi).
+ *)
+
let rec ids_of_formula f =
match f with
| I(f1,Some id,f2) -> id::(ids_of_formula f2)
| _ -> []
-module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end)
-
-let selecti s m =
- let rec xselect i m =
- match m with
- | [] -> []
- | e::m -> if ISet.mem i s then e:: (xselect (i+1) m) else xselect (i+1) m in
- xselect 0 m
-
+(**
+ * A clause is a list of (tagged) nFormulas.
+ * nFormulas are normalized formulas, i.e., of the form:
+ * cPol {=,<>,>,>=} 0
+ * with cPol compact polynomials (see the Pol inductive type in EnvRing.v).
+ *)
type 'cst clause = ('cst Micromega.nFormula * tag) list
+(**
+ * A CNF is a list of clauses.
+ *)
+
type 'cst cnf = ('cst clause) list
+(**
+ * True and False are empty cnfs and clauses.
+ *)
+
let tt : 'cst cnf = []
+
let ff : 'cst cnf = [ [] ]
+(**
+ * A refinement of cnf with tags left out. This is an intermediary form
+ * between the cnf tagged list representation ('cst cnf) used to solve psatz,
+ * and the freeform formulas ('cst formula) that is retrieved from Coq.
+ *)
type 'cst mc_cnf = ('cst Micromega.nFormula) list list
+(**
+ * From a freeform formula, build a cnf.
+ * The parametric functions negate and normalize are theory-dependent, and
+ * originate in micromega.ml (extracted, e.g. for rnegate, from RMicromega.v
+ * and RingMicromega.v).
+ *)
+
let cnf (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) (f:'cst formula) =
let negate a t =
List.map (fun cl -> List.map (fun x -> (x,t)) cl) (negate a) in
let normalise a t =
- List.map (fun cl -> List.map (fun x -> (x,t)) cl) (normalise a) in
+ List.map (fun cl -> List.map (fun x -> (x,t)) cl) (normalise a) in
let and_cnf x y = x @ y in
let or_clause_cnf t f = List.map (fun x -> t@x) f in
- let rec or_cnf f f' =
+ let rec or_cnf f f' =
match f with
| [] -> tt
| e :: rst -> (or_cnf rst f') @ (or_clause_cnf e f') in
- let rec xcnf (pol : bool) f =
+ let rec xcnf (polarity : bool) f =
match f with
- | TT -> if pol then tt else ff (* ?? *)
- | FF -> if pol then ff else tt (* ?? *)
- | X p -> if pol then ff else ff (* ?? *)
- | A(x,t,_) -> if pol then normalise x t else negate x t
- | N(e) -> xcnf (not pol) e
+ | TT -> if polarity then tt else ff
+ | FF -> if polarity then ff else tt
+ | X p -> if polarity then ff else ff
+ | A(x,t,_) -> if polarity then normalise x t else negate x t
+ | N(e) -> xcnf (not polarity) e
| C(e1,e2) ->
- (if pol then and_cnf else or_cnf) (xcnf pol e1) (xcnf pol e2)
+ (if polarity then and_cnf else or_cnf) (xcnf polarity e1) (xcnf polarity e2)
| D(e1,e2) ->
- (if pol then or_cnf else and_cnf) (xcnf pol e1) (xcnf pol e2)
+ (if polarity then or_cnf else and_cnf) (xcnf polarity e1) (xcnf polarity e2)
| I(e1,_,e2) ->
- (if pol then or_cnf else and_cnf) (xcnf (not pol) e1) (xcnf pol e2) in
-
- xcnf true f
-
-
-module M =
-struct
- open Coqlib
- open Term
- (* let constant = gen_constant_in_modules "Omicron" coq_modules*)
-
-
- let logic_dir = ["Coq";"Logic";"Decidable"]
- let coq_modules =
- init_modules @
- [logic_dir] @ arith_modules @ zarith_base_modules @
- [ ["Coq";"Lists";"List"];
- ["ZMicromega"];
- ["Tauto"];
- ["RingMicromega"];
- ["EnvRing"];
- ["Coq"; "micromega"; "ZMicromega"];
- ["Coq" ; "micromega" ; "Tauto"];
- ["Coq" ; "micromega" ; "RingMicromega"];
- ["Coq" ; "micromega" ; "EnvRing"];
- ["Coq";"QArith"; "QArith_base"];
- ["Coq";"Reals" ; "Rdefinitions"];
- ["Coq";"Reals" ; "Rpow_def"];
- ["LRing_normalise"]]
-
- let init_constant = gen_constant_in_modules "ZMicromega" init_modules
- let constant = gen_constant_in_modules "ZMicromega" coq_modules
-
- let coq_and = lazy (init_constant "and")
- let coq_or = lazy (init_constant "or")
- let coq_not = lazy (init_constant "not")
- let coq_iff = lazy (init_constant "iff")
- let coq_True = lazy (init_constant "True")
- let coq_False = lazy (init_constant "False")
-
- let coq_cons = lazy (constant "cons")
- let coq_nil = lazy (constant "nil")
- let coq_list = lazy (constant "list")
-
- let coq_O = lazy (init_constant "O")
- let coq_S = lazy (init_constant "S")
- let coq_nat = lazy (init_constant "nat")
-
- let coq_NO = lazy
- (gen_constant_in_modules "N" [ ["Coq";"NArith";"BinNat" ]] "N0")
- let coq_Npos = lazy
- (gen_constant_in_modules "N" [ ["Coq";"NArith"; "BinNat"]] "Npos")
- (* let coq_n = lazy (constant "N")*)
-
- let coq_pair = lazy (constant "pair")
- let coq_None = lazy (constant "None")
- let coq_option = lazy (constant "option")
- let coq_positive = lazy (constant "positive")
- let coq_xH = lazy (constant "xH")
- let coq_xO = lazy (constant "xO")
- let coq_xI = lazy (constant "xI")
-
- let coq_N0 = lazy (constant "N0")
- let coq_N0 = lazy (constant "Npos")
-
-
- let coq_Z = lazy (constant "Z")
- let coq_Q = lazy (constant "Q")
- let coq_R = lazy (constant "R")
-
- let coq_ZERO = lazy (constant "Z0")
- let coq_POS = lazy (constant "Zpos")
- let coq_NEG = lazy (constant "Zneg")
-
- let coq_QWitness = lazy
- (gen_constant_in_modules "QMicromega"
- [["Coq"; "micromega"; "QMicromega"]] "QWitness")
- let coq_ZWitness = lazy
- (gen_constant_in_modules "QMicromega"
- [["Coq"; "micromega"; "ZMicromega"]] "ZWitness")
-
-
- let coq_Build_Witness = lazy (constant "Build_Witness")
-
-
- let coq_Qmake = lazy (constant "Qmake")
- let coq_R0 = lazy (constant "R0")
- let coq_R1 = lazy (constant "R1")
-
-
- let coq_proofTerm = lazy (constant "ZArithProof")
- let coq_doneProof = lazy (constant "DoneProof")
- let coq_ratProof = lazy (constant "RatProof")
- let coq_cutProof = lazy (constant "CutProof")
- let coq_enumProof = lazy (constant "EnumProof")
-
- let coq_Zgt = lazy (constant "Zgt")
- let coq_Zge = lazy (constant "Zge")
- let coq_Zle = lazy (constant "Zle")
- let coq_Zlt = lazy (constant "Zlt")
- let coq_Eq = lazy (init_constant "eq")
-
- let coq_Zplus = lazy (constant "Zplus")
- let coq_Zminus = lazy (constant "Zminus")
- let coq_Zopp = lazy (constant "Zopp")
- let coq_Zmult = lazy (constant "Zmult")
- let coq_Zpower = lazy (constant "Zpower")
- let coq_N_of_Z = lazy
- (gen_constant_in_modules "ZArithRing"
- [["Coq";"setoid_ring";"ZArithRing"]] "N_of_Z")
-
- let coq_Qgt = lazy (constant "Qgt")
- let coq_Qge = lazy (constant "Qge")
- let coq_Qle = lazy (constant "Qle")
- let coq_Qlt = lazy (constant "Qlt")
- let coq_Qeq = lazy (constant "Qeq")
-
-
- let coq_Qplus = lazy (constant "Qplus")
- let coq_Qminus = lazy (constant "Qminus")
- let coq_Qopp = lazy (constant "Qopp")
- let coq_Qmult = lazy (constant "Qmult")
- let coq_Qpower = lazy (constant "Qpower")
-
-
- let coq_Rgt = lazy (constant "Rgt")
- let coq_Rge = lazy (constant "Rge")
- let coq_Rle = lazy (constant "Rle")
- let coq_Rlt = lazy (constant "Rlt")
-
- let coq_Rplus = lazy (constant "Rplus")
- let coq_Rminus = lazy (constant "Rminus")
- let coq_Ropp = lazy (constant "Ropp")
- let coq_Rmult = lazy (constant "Rmult")
- let coq_Rpower = lazy (constant "pow")
-
-
- let coq_PEX = lazy (constant "PEX" )
- let coq_PEc = lazy (constant"PEc")
- let coq_PEadd = lazy (constant "PEadd")
- let coq_PEopp = lazy (constant "PEopp")
- let coq_PEmul = lazy (constant "PEmul")
- let coq_PEsub = lazy (constant "PEsub")
- let coq_PEpow = lazy (constant "PEpow")
-
- let coq_PX = lazy (constant "PX" )
- let coq_Pc = lazy (constant"Pc")
- let coq_Pinj = lazy (constant "Pinj")
-
-
- let coq_OpEq = lazy (constant "OpEq")
- let coq_OpNEq = lazy (constant "OpNEq")
- let coq_OpLe = lazy (constant "OpLe")
- let coq_OpLt = lazy (constant "OpLt")
- let coq_OpGe = lazy (constant "OpGe")
- let coq_OpGt = lazy (constant "OpGt")
-
-
- let coq_PsatzIn = lazy (constant "PsatzIn")
- let coq_PsatzSquare = lazy (constant "PsatzSquare")
- let coq_PsatzMulE = lazy (constant "PsatzMulE")
- let coq_PsatzMultC = lazy (constant "PsatzMulC")
- let coq_PsatzAdd = lazy (constant "PsatzAdd")
- let coq_PsatzC = lazy (constant "PsatzC")
- let coq_PsatzZ = lazy (constant "PsatzZ")
- let coq_coneMember = lazy (constant "coneMember")
-
-
- let coq_make_impl = lazy
- (gen_constant_in_modules "Zmicromega" [["Refl"]] "make_impl")
- let coq_make_conj = lazy
- (gen_constant_in_modules "Zmicromega" [["Refl"]] "make_conj")
-
- let coq_Build = lazy
- (gen_constant_in_modules "RingMicromega"
- [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ]
- "Build_Formula")
- let coq_Cstr = lazy
- (gen_constant_in_modules "RingMicromega"
- [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] "Formula")
-
-
- type parse_error =
- | Ukn
- | BadStr of string
- | BadNum of int
- | BadTerm of Term.constr
- | Msg of string
- | Goal of (Term.constr list ) * Term.constr * parse_error
-
- let string_of_error = function
- | Ukn -> "ukn"
- | BadStr s -> s
- | BadNum i -> string_of_int i
- | BadTerm _ -> "BadTerm"
- | Msg s -> s
- | Goal _ -> "Goal"
-
-
- exception ParseError
-
-
-
-
- let get_left_construct term =
- match Term.kind_of_term term with
- | Term.Construct(_,i) -> (i,[| |])
- | Term.App(l,rst) ->
- (match Term.kind_of_term l with
- | Term.Construct(_,i) -> (i,rst)
- | _ -> raise ParseError
- )
- | _ -> raise ParseError
-
- module Mc = Micromega
-
- let rec parse_nat term =
- let (i,c) = get_left_construct term in
- match i with
- | 1 -> Mc.O
- | 2 -> Mc.S (parse_nat (c.(0)))
- | i -> raise ParseError
-
-
- let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n)
-
-
- let rec dump_nat x =
- match x with
- | Mc.O -> Lazy.force coq_O
- | Mc.S p -> Term.mkApp(Lazy.force coq_S,[| dump_nat p |])
-
-
- let rec parse_positive term =
- let (i,c) = get_left_construct term in
- match i with
- | 1 -> Mc.XI (parse_positive c.(0))
- | 2 -> Mc.XO (parse_positive c.(0))
- | 3 -> Mc.XH
- | i -> raise ParseError
-
-
- let rec dump_positive x =
- match x with
- | Mc.XH -> Lazy.force coq_xH
- | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_positive p |])
- | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_positive p |])
-
- let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x)
-
-
- let rec dump_n x =
- match x with
- | Mc.N0 -> Lazy.force coq_N0
- | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|])
-
- let rec dump_index x =
- match x with
- | Mc.XH -> Lazy.force coq_xH
- | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_index p |])
- | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_index p |])
+ (if polarity then or_cnf else and_cnf) (xcnf (not polarity) e1) (xcnf polarity e2) in
+ xcnf true f
- let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x)
+(**
+ * MODULE: Ordered set of integers.
+ *)
- let rec dump_n x =
- match x with
- | Mc.N0 -> Lazy.force coq_NO
- | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p |])
-
- let rec pp_n o x = output_string o (string_of_int (CoqToCaml.n x))
-
- let dump_pair t1 t2 dump_t1 dump_t2 (x,y) =
- Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|])
-
-
- let rec parse_z term =
- let (i,c) = get_left_construct term in
- match i with
- | 1 -> Mc.Z0
- | 2 -> Mc.Zpos (parse_positive c.(0))
- | 3 -> Mc.Zneg (parse_positive c.(0))
- | i -> raise ParseError
-
- let dump_z x =
- match x with
- | Mc.Z0 ->Lazy.force coq_ZERO
- | Mc.Zpos p -> Term.mkApp(Lazy.force coq_POS,[| dump_positive p|])
- | Mc.Zneg p -> Term.mkApp(Lazy.force coq_NEG,[| dump_positive p|])
+module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end)
- let pp_z o x = Printf.fprintf o "%i" (CoqToCaml.z x)
+(**
+ * Given a set of integers s={i0,...,iN} and a list m, return the list of
+ * elements of m that are at position i0,...,iN.
+ *)
-let dump_num bd1 =
- Term.mkApp(Lazy.force coq_Qmake,
- [|dump_z (CamlToCoq.bigint (numerator bd1)) ;
- dump_positive (CamlToCoq.positive_big_int (denominator bd1)) |])
+let selecti s m =
+ let rec xselecti i m =
+ match m with
+ | [] -> []
+ | e::m -> if ISet.mem i s then e::(xselecti (i+1) m) else xselecti (i+1) m in
+ xselecti 0 m
+(**
+ * MODULE: Mapping of the Coq data-strustures into Caml and Caml extracted
+ * code. This includes initializing Caml variables based on Coq terms, parsing
+ * various Coq expressions into Caml, and dumping Caml expressions into Coq.
+ *
+ * Opened here and in csdpcert.ml.
+ *)
-let dump_q q =
- Term.mkApp(Lazy.force coq_Qmake,
- [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|])
+module M =
+struct
-let parse_q term =
- match Term.kind_of_term term with
- | Term.App(c, args) -> if c = Lazy.force coq_Qmake then
- {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
- else raise ParseError
- | _ -> raise ParseError
+ open Coqlib
+ open Term
+
+ (**
+ * Location of the Coq libraries.
+ *)
+
+ let logic_dir = ["Coq";"Logic";"Decidable"]
+ let coq_modules =
+ init_modules @
+ [logic_dir] @ arith_modules @ zarith_base_modules @
+ [ ["Coq";"Lists";"List"];
+ ["ZMicromega"];
+ ["Tauto"];
+ ["RingMicromega"];
+ ["EnvRing"];
+ ["Coq"; "micromega"; "ZMicromega"];
+ ["Coq" ; "micromega" ; "Tauto"];
+ ["Coq" ; "micromega" ; "RingMicromega"];
+ ["Coq" ; "micromega" ; "EnvRing"];
+ ["Coq";"QArith"; "QArith_base"];
+ ["Coq";"Reals" ; "Rdefinitions"];
+ ["Coq";"Reals" ; "Rpow_def"];
+ ["LRing_normalise"]]
+
+ (**
+ * Initialization : a large amount of Caml symbols are derived from
+ * ZMicromega.v
+ *)
+
+ let init_constant = gen_constant_in_modules "ZMicromega" init_modules
+ let constant = gen_constant_in_modules "ZMicromega" coq_modules
+ (* let constant = gen_constant_in_modules "Omicron" coq_modules *)
+
+ let coq_and = lazy (init_constant "and")
+ let coq_or = lazy (init_constant "or")
+ let coq_not = lazy (init_constant "not")
+ let coq_iff = lazy (init_constant "iff")
+ let coq_True = lazy (init_constant "True")
+ let coq_False = lazy (init_constant "False")
+
+ let coq_cons = lazy (constant "cons")
+ let coq_nil = lazy (constant "nil")
+ let coq_list = lazy (constant "list")
+
+ let coq_O = lazy (init_constant "O")
+ let coq_S = lazy (init_constant "S")
+ let coq_nat = lazy (init_constant "nat")
+
+ let coq_NO = lazy
+ (gen_constant_in_modules "N" [ ["Coq";"NArith";"BinNat" ]] "N0")
+ let coq_Npos = lazy
+ (gen_constant_in_modules "N" [ ["Coq";"NArith"; "BinNat"]] "Npos")
+ (* let coq_n = lazy (constant "N")*)
+
+ let coq_pair = lazy (constant "pair")
+ let coq_None = lazy (constant "None")
+ let coq_option = lazy (constant "option")
+ let coq_positive = lazy (constant "positive")
+ let coq_xH = lazy (constant "xH")
+ let coq_xO = lazy (constant "xO")
+ let coq_xI = lazy (constant "xI")
+
+ let coq_N0 = lazy (constant "N0")
+ let coq_N0 = lazy (constant "Npos")
+
+ let coq_Z = lazy (constant "Z")
+ let coq_Q = lazy (constant "Q")
+ let coq_R = lazy (constant "R")
+
+ let coq_ZERO = lazy (constant "Z0")
+ let coq_POS = lazy (constant "Zpos")
+ let coq_NEG = lazy (constant "Zneg")
+
+ let coq_Build_Witness = lazy (constant "Build_Witness")
+
+ let coq_Qmake = lazy (constant "Qmake")
+ let coq_R0 = lazy (constant "R0")
+ let coq_R1 = lazy (constant "R1")
+
+ let coq_proofTerm = lazy (constant "ZArithProof")
+ let coq_doneProof = lazy (constant "DoneProof")
+ let coq_ratProof = lazy (constant "RatProof")
+ let coq_cutProof = lazy (constant "CutProof")
+ let coq_enumProof = lazy (constant "EnumProof")
+
+ let coq_Zgt = lazy (constant "Zgt")
+ let coq_Zge = lazy (constant "Zge")
+ let coq_Zle = lazy (constant "Zle")
+ let coq_Zlt = lazy (constant "Zlt")
+ let coq_Eq = lazy (init_constant "eq")
+
+ let coq_Zplus = lazy (constant "Zplus")
+ let coq_Zminus = lazy (constant "Zminus")
+ let coq_Zopp = lazy (constant "Zopp")
+ let coq_Zmult = lazy (constant "Zmult")
+ let coq_Zpower = lazy (constant "Zpower")
+
+ let coq_Qgt = lazy (constant "Qgt")
+ let coq_Qge = lazy (constant "Qge")
+ let coq_Qle = lazy (constant "Qle")
+ let coq_Qlt = lazy (constant "Qlt")
+ let coq_Qeq = lazy (constant "Qeq")
+
+ let coq_Qplus = lazy (constant "Qplus")
+ let coq_Qminus = lazy (constant "Qminus")
+ let coq_Qopp = lazy (constant "Qopp")
+ let coq_Qmult = lazy (constant "Qmult")
+ let coq_Qpower = lazy (constant "Qpower")
+
+ let coq_Rgt = lazy (constant "Rgt")
+ let coq_Rge = lazy (constant "Rge")
+ let coq_Rle = lazy (constant "Rle")
+ let coq_Rlt = lazy (constant "Rlt")
+
+ let coq_Rplus = lazy (constant "Rplus")
+ let coq_Rminus = lazy (constant "Rminus")
+ let coq_Ropp = lazy (constant "Ropp")
+ let coq_Rmult = lazy (constant "Rmult")
+ let coq_Rpower = lazy (constant "pow")
+
+ let coq_PEX = lazy (constant "PEX" )
+ let coq_PEc = lazy (constant"PEc")
+ let coq_PEadd = lazy (constant "PEadd")
+ let coq_PEopp = lazy (constant "PEopp")
+ let coq_PEmul = lazy (constant "PEmul")
+ let coq_PEsub = lazy (constant "PEsub")
+ let coq_PEpow = lazy (constant "PEpow")
+
+ let coq_PX = lazy (constant "PX" )
+ let coq_Pc = lazy (constant"Pc")
+ let coq_Pinj = lazy (constant "Pinj")
+
+ let coq_OpEq = lazy (constant "OpEq")
+ let coq_OpNEq = lazy (constant "OpNEq")
+ let coq_OpLe = lazy (constant "OpLe")
+ let coq_OpLt = lazy (constant "OpLt")
+ let coq_OpGe = lazy (constant "OpGe")
+ let coq_OpGt = lazy (constant "OpGt")
+
+ let coq_PsatzIn = lazy (constant "PsatzIn")
+ let coq_PsatzSquare = lazy (constant "PsatzSquare")
+ let coq_PsatzMulE = lazy (constant "PsatzMulE")
+ let coq_PsatzMultC = lazy (constant "PsatzMulC")
+ let coq_PsatzAdd = lazy (constant "PsatzAdd")
+ let coq_PsatzC = lazy (constant "PsatzC")
+ let coq_PsatzZ = lazy (constant "PsatzZ")
+ let coq_coneMember = lazy (constant "coneMember")
+
+ let coq_make_impl = lazy
+ (gen_constant_in_modules "Zmicromega" [["Refl"]] "make_impl")
+ let coq_make_conj = lazy
+ (gen_constant_in_modules "Zmicromega" [["Refl"]] "make_conj")
+
+ let coq_TT = lazy
+ (gen_constant_in_modules "ZMicromega"
+ [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "TT")
+ let coq_FF = lazy
+ (gen_constant_in_modules "ZMicromega"
+ [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "FF")
+ let coq_And = lazy
+ (gen_constant_in_modules "ZMicromega"
+ [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "Cj")
+ let coq_Or = lazy
+ (gen_constant_in_modules "ZMicromega"
+ [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "D")
+ let coq_Neg = lazy
+ (gen_constant_in_modules "ZMicromega"
+ [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "N")
+ let coq_Atom = lazy
+ (gen_constant_in_modules "ZMicromega"
+ [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "A")
+ let coq_X = lazy
+ (gen_constant_in_modules "ZMicromega"
+ [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "X")
+ let coq_Impl = lazy
+ (gen_constant_in_modules "ZMicromega"
+ [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "I")
+ let coq_Formula = lazy
+ (gen_constant_in_modules "ZMicromega"
+ [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "BFormula")
+
+ (**
+ * Initialization : a few Caml symbols are derived from other libraries;
+ * QMicromega, ZArithRing, RingMicromega.
+ *)
+
+ let coq_QWitness = lazy
+ (gen_constant_in_modules "QMicromega"
+ [["Coq"; "micromega"; "QMicromega"]] "QWitness")
+ let coq_ZWitness = lazy
+ (gen_constant_in_modules "QMicromega"
+ [["Coq"; "micromega"; "ZMicromega"]] "ZWitness")
+
+ let coq_N_of_Z = lazy
+ (gen_constant_in_modules "ZArithRing"
+ [["Coq";"setoid_ring";"ZArithRing"]] "N_of_Z")
+
+ let coq_Build = lazy
+ (gen_constant_in_modules "RingMicromega"
+ [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ]
+ "Build_Formula")
+ let coq_Cstr = lazy
+ (gen_constant_in_modules "RingMicromega"
+ [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] "Formula")
+
+ (**
+ * Parsing and dumping : transformation functions between Caml and Coq
+ * data-structures.
+ *
+ * dump_* functions go from Micromega to Coq terms
+ * parse_* functions go from Coq to Micromega terms
+ * pp_* functions pretty-print Coq terms.
+ *)
+
+ (* Error datastructures *)
+
+ type parse_error =
+ | Ukn
+ | BadStr of string
+ | BadNum of int
+ | BadTerm of Term.constr
+ | Msg of string
+ | Goal of (Term.constr list ) * Term.constr * parse_error
+
+ let string_of_error = function
+ | Ukn -> "ukn"
+ | BadStr s -> s
+ | BadNum i -> string_of_int i
+ | BadTerm _ -> "BadTerm"
+ | Msg s -> s
+ | Goal _ -> "Goal"
+
+ exception ParseError
+
+ (* A simple but useful getter function *)
+
+ let get_left_construct term =
+ match Term.kind_of_term term with
+ | Term.Construct(_,i) -> (i,[| |])
+ | Term.App(l,rst) ->
+ (match Term.kind_of_term l with
+ | Term.Construct(_,i) -> (i,rst)
+ | _ -> raise ParseError
+ )
+ | _ -> raise ParseError
+
+ (* Access the Micromega module *)
+
+ module Mc = Micromega
+
+ (* parse/dump/print from numbers up to expressions and formulas *)
+
+ let rec parse_nat term =
+ let (i,c) = get_left_construct term in
+ match i with
+ | 1 -> Mc.O
+ | 2 -> Mc.S (parse_nat (c.(0)))
+ | i -> raise ParseError
+
+ let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n)
+
+ let rec dump_nat x =
+ match x with
+ | Mc.O -> Lazy.force coq_O
+ | Mc.S p -> Term.mkApp(Lazy.force coq_S,[| dump_nat p |])
+
+ let rec parse_positive term =
+ let (i,c) = get_left_construct term in
+ match i with
+ | 1 -> Mc.XI (parse_positive c.(0))
+ | 2 -> Mc.XO (parse_positive c.(0))
+ | 3 -> Mc.XH
+ | i -> raise ParseError
+
+ let rec dump_positive x =
+ match x with
+ | Mc.XH -> Lazy.force coq_xH
+ | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_positive p |])
+ | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_positive p |])
+
+ let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x)
+
+ let rec dump_n x =
+ match x with
+ | Mc.N0 -> Lazy.force coq_N0
+ | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|])
+
+ let rec dump_index x =
+ match x with
+ | Mc.XH -> Lazy.force coq_xH
+ | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_index p |])
+ | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_index p |])
+
+ let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x)
+
+ let rec dump_n x =
+ match x with
+ | Mc.N0 -> Lazy.force coq_NO
+ | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p |])
+
+ let rec pp_n o x = output_string o (string_of_int (CoqToCaml.n x))
+
+ let dump_pair t1 t2 dump_t1 dump_t2 (x,y) =
+ Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|])
+
+ let rec parse_z term =
+ let (i,c) = get_left_construct term in
+ match i with
+ | 1 -> Mc.Z0
+ | 2 -> Mc.Zpos (parse_positive c.(0))
+ | 3 -> Mc.Zneg (parse_positive c.(0))
+ | i -> raise ParseError
+
+ let dump_z x =
+ match x with
+ | Mc.Z0 ->Lazy.force coq_ZERO
+ | Mc.Zpos p -> Term.mkApp(Lazy.force coq_POS,[| dump_positive p|])
+ | Mc.Zneg p -> Term.mkApp(Lazy.force coq_NEG,[| dump_positive p|])
+
+ let pp_z o x = Printf.fprintf o "%i" (CoqToCaml.z x)
+
+ let dump_num bd1 =
+ Term.mkApp(Lazy.force coq_Qmake,
+ [|dump_z (CamlToCoq.bigint (numerator bd1)) ;
+ dump_positive (CamlToCoq.positive_big_int (denominator bd1)) |])
+
+ let dump_q q =
+ Term.mkApp(Lazy.force coq_Qmake,
+ [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|])
+
+ let parse_q term =
+ match Term.kind_of_term term with
+ | Term.App(c, args) -> if c = Lazy.force coq_Qmake then
+ {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
+ else raise ParseError
+ | _ -> raise ParseError
+ let rec parse_list parse_elt term =
+ let (i,c) = get_left_construct term in
+ match i with
+ | 1 -> []
+ | 2 -> parse_elt c.(1) :: parse_list parse_elt c.(2)
+ | i -> raise ParseError
- let rec parse_list parse_elt term =
- let (i,c) = get_left_construct term in
- match i with
- | 1 -> []
- | 2 -> parse_elt c.(1) :: parse_list parse_elt c.(2)
- | i -> raise ParseError
+ let rec dump_list typ dump_elt l =
+ match l with
+ | [] -> Term.mkApp(Lazy.force coq_nil,[| typ |])
+ | e :: l -> Term.mkApp(Lazy.force coq_cons,
+ [| typ; dump_elt e;dump_list typ dump_elt l|])
+ let pp_list op cl elt o l =
+ let rec _pp o l =
+ match l with
+ | [] -> ()
+ | [e] -> Printf.fprintf o "%a" elt e
+ | e::l -> Printf.fprintf o "%a ,%a" elt e _pp l in
+ Printf.fprintf o "%s%a%s" op _pp l cl
- let rec dump_list typ dump_elt l =
- match l with
- | [] -> Term.mkApp(Lazy.force coq_nil,[| typ |])
- | e :: l -> Term.mkApp(Lazy.force coq_cons,
- [| typ; dump_elt e;dump_list typ dump_elt l|])
+ let pp_var = pp_positive
+ let dump_var = dump_positive
- let pp_list op cl elt o l =
- let rec _pp o l =
- match l with
- | [] -> ()
- | [e] -> Printf.fprintf o "%a" elt e
- | e::l -> Printf.fprintf o "%a ,%a" elt e _pp l in
- Printf.fprintf o "%s%a%s" op _pp l cl
-
-
- let pp_var = pp_positive
- let dump_var = dump_positive
-
- let pp_expr pp_z o e =
- let rec pp_expr o e =
- match e with
- | Mc.PEX n -> Printf.fprintf o "V %a" pp_var n
- | Mc.PEc z -> pp_z o z
- | Mc.PEadd(e1,e2) -> Printf.fprintf o "(%a)+(%a)" pp_expr e1 pp_expr e2
- | Mc.PEmul(e1,e2) -> Printf.fprintf o "%a*(%a)" pp_expr e1 pp_expr e2
- | Mc.PEopp e -> Printf.fprintf o "-(%a)" pp_expr e
- | Mc.PEsub(e1,e2) -> Printf.fprintf o "(%a)-(%a)" pp_expr e1 pp_expr e2
- | Mc.PEpow(e,n) -> Printf.fprintf o "(%a)^(%a)" pp_expr e pp_n n in
- pp_expr o e
-
-
- let dump_expr typ dump_z e =
- let rec dump_expr e =
- match e with
- | Mc.PEX n -> mkApp(Lazy.force coq_PEX,[| typ; dump_var n |])
- | Mc.PEc z -> mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |])
- | Mc.PEadd(e1,e2) -> mkApp(Lazy.force coq_PEadd,
- [| typ; dump_expr e1;dump_expr e2|])
- | Mc.PEsub(e1,e2) -> mkApp(Lazy.force coq_PEsub,
- [| typ; dump_expr e1;dump_expr e2|])
- | Mc.PEopp e -> mkApp(Lazy.force coq_PEopp,
- [| typ; dump_expr e|])
- | Mc.PEmul(e1,e2) -> mkApp(Lazy.force coq_PEmul,
- [| typ; dump_expr e1;dump_expr e2|])
- | Mc.PEpow(e,n) -> mkApp(Lazy.force coq_PEpow,
- [| typ; dump_expr e; dump_n n|])
- in
- dump_expr e
-
-
- let dump_pol typ dump_c e =
- let rec dump_pol e =
- match e with
- | Mc.Pc n -> mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|])
- | Mc.Pinj(p,pol) -> mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|])
- | Mc.PX(pol1,p,pol2) -> mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in
- dump_pol e
-
- let pp_pol pp_c o e =
- let rec pp_pol o e =
- match e with
- | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n
- | Mc.Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol
- | Mc.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in
- pp_pol o e
-
-
- let pp_cnf pp_c o f =
- let pp_clause o l = List.iter (fun ((p,_),t) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) l in
- List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause l) f
-
-
- let dump_psatz typ dump_z e =
- let z = Lazy.force typ in
- let rec dump_cone e =
- match e with
- | Mc.PsatzIn n -> mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |])
- | Mc.PsatzMulC(e,c) -> mkApp(Lazy.force coq_PsatzMultC,
- [| z; dump_pol z dump_z e ; dump_cone c |])
- | Mc.PsatzSquare e -> mkApp(Lazy.force coq_PsatzSquare,
- [| z;dump_pol z dump_z e|])
- | Mc.PsatzAdd(e1,e2) -> mkApp(Lazy.force coq_PsatzAdd,
- [| z; dump_cone e1; dump_cone e2|])
- | Mc.PsatzMulE(e1,e2) -> mkApp(Lazy.force coq_PsatzMulE,
- [| z; dump_cone e1; dump_cone e2|])
- | Mc.PsatzC p -> mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|])
- | Mc.PsatzZ -> mkApp( Lazy.force coq_PsatzZ,[| z|]) in
- dump_cone e
-
-
- let pp_psatz pp_z o e =
- let rec pp_cone o e =
+ let pp_expr pp_z o e =
+ let rec pp_expr o e =
match e with
- | Mc.PsatzIn n ->
- Printf.fprintf o "(In %a)%%nat" pp_nat n
- | Mc.PsatzMulC(e,c) ->
- Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c
- | Mc.PsatzSquare e ->
- Printf.fprintf o "(%a^2)" (pp_pol pp_z) e
- | Mc.PsatzAdd(e1,e2) ->
- Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2
- | Mc.PsatzMulE(e1,e2) ->
- Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2
- | Mc.PsatzC p ->
- Printf.fprintf o "(%a)%%positive" pp_z p
- | Mc.PsatzZ ->
- Printf.fprintf o "0" in
- pp_cone o e
-
-
- let rec dump_op = function
- | Mc.OpEq-> Lazy.force coq_OpEq
- | Mc.OpNEq-> Lazy.force coq_OpNEq
- | Mc.OpLe -> Lazy.force coq_OpLe
- | Mc.OpGe -> Lazy.force coq_OpGe
- | Mc.OpGt-> Lazy.force coq_OpGt
- | Mc.OpLt-> Lazy.force coq_OpLt
-
-
-
- let pp_op o e=
- match e with
- | Mc.OpEq-> Printf.fprintf o "="
- | Mc.OpNEq-> Printf.fprintf o "<>"
- | Mc.OpLe -> Printf.fprintf o "=<"
- | Mc.OpGe -> Printf.fprintf o ">="
- | Mc.OpGt-> Printf.fprintf o ">"
- | Mc.OpLt-> Printf.fprintf o "<"
-
-
-
-
- let pp_cstr pp_z o {Mc.flhs = l ; Mc.fop = op ; Mc.frhs = r } =
- Printf.fprintf o"(%a %a %a)" (pp_expr pp_z) l pp_op op (pp_expr pp_z) r
-
- let dump_cstr typ dump_constant {Mc.flhs = e1 ; Mc.fop = o ; Mc.frhs = e2} =
- Term.mkApp(Lazy.force coq_Build,
- [| typ; dump_expr typ dump_constant e1 ;
- dump_op o ;
- dump_expr typ dump_constant e2|])
-
- let assoc_const x l =
- try
- snd (List.find (fun (x',y) -> x = Lazy.force x') l)
- with
- Not_found -> raise ParseError
-
- let zop_table = [
- coq_Zgt, Mc.OpGt ;
- coq_Zge, Mc.OpGe ;
- coq_Zlt, Mc.OpLt ;
- coq_Zle, Mc.OpLe ]
-
- let rop_table = [
- coq_Rgt, Mc.OpGt ;
- coq_Rge, Mc.OpGe ;
- coq_Rlt, Mc.OpLt ;
- coq_Rle, Mc.OpLe ]
-
- let qop_table = [
- coq_Qlt, Mc.OpLt ;
- coq_Qle, Mc.OpLe ;
- coq_Qeq, Mc.OpEq
- ]
-
-
- let parse_zop (op,args) =
- match kind_of_term op with
- | Const x -> (assoc_const op zop_table, args.(0) , args.(1))
- | Ind(n,0) ->
- if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_Z
- then (Mc.OpEq, args.(1), args.(2))
- else raise ParseError
- | _ -> failwith "parse_zop"
-
-
- let parse_rop (op,args) =
+ | Mc.PEX n -> Printf.fprintf o "V %a" pp_var n
+ | Mc.PEc z -> pp_z o z
+ | Mc.PEadd(e1,e2) -> Printf.fprintf o "(%a)+(%a)" pp_expr e1 pp_expr e2
+ | Mc.PEmul(e1,e2) -> Printf.fprintf o "%a*(%a)" pp_expr e1 pp_expr e2
+ | Mc.PEopp e -> Printf.fprintf o "-(%a)" pp_expr e
+ | Mc.PEsub(e1,e2) -> Printf.fprintf o "(%a)-(%a)" pp_expr e1 pp_expr e2
+ | Mc.PEpow(e,n) -> Printf.fprintf o "(%a)^(%a)" pp_expr e pp_n n in
+ pp_expr o e
+
+ let dump_expr typ dump_z e =
+ let rec dump_expr e =
+ match e with
+ | Mc.PEX n -> mkApp(Lazy.force coq_PEX,[| typ; dump_var n |])
+ | Mc.PEc z -> mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |])
+ | Mc.PEadd(e1,e2) -> mkApp(Lazy.force coq_PEadd,
+ [| typ; dump_expr e1;dump_expr e2|])
+ | Mc.PEsub(e1,e2) -> mkApp(Lazy.force coq_PEsub,
+ [| typ; dump_expr e1;dump_expr e2|])
+ | Mc.PEopp e -> mkApp(Lazy.force coq_PEopp,
+ [| typ; dump_expr e|])
+ | Mc.PEmul(e1,e2) -> mkApp(Lazy.force coq_PEmul,
+ [| typ; dump_expr e1;dump_expr e2|])
+ | Mc.PEpow(e,n) -> mkApp(Lazy.force coq_PEpow,
+ [| typ; dump_expr e; dump_n n|])
+ in
+ dump_expr e
+
+ let dump_pol typ dump_c e =
+ let rec dump_pol e =
+ match e with
+ | Mc.Pc n -> mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|])
+ | Mc.Pinj(p,pol) -> mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|])
+ | Mc.PX(pol1,p,pol2) -> mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in
+ dump_pol e
+
+ let pp_pol pp_c o e =
+ let rec pp_pol o e =
+ match e with
+ | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n
+ | Mc.Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol
+ | Mc.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in
+ pp_pol o e
+
+ let pp_cnf pp_c o f =
+ let pp_clause o l = List.iter (fun ((p,_),t) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) l in
+ List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause l) f
+
+ let dump_psatz typ dump_z e =
+ let z = Lazy.force typ in
+ let rec dump_cone e =
+ match e with
+ | Mc.PsatzIn n -> mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |])
+ | Mc.PsatzMulC(e,c) -> mkApp(Lazy.force coq_PsatzMultC,
+ [| z; dump_pol z dump_z e ; dump_cone c |])
+ | Mc.PsatzSquare e -> mkApp(Lazy.force coq_PsatzSquare,
+ [| z;dump_pol z dump_z e|])
+ | Mc.PsatzAdd(e1,e2) -> mkApp(Lazy.force coq_PsatzAdd,
+ [| z; dump_cone e1; dump_cone e2|])
+ | Mc.PsatzMulE(e1,e2) -> mkApp(Lazy.force coq_PsatzMulE,
+ [| z; dump_cone e1; dump_cone e2|])
+ | Mc.PsatzC p -> mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|])
+ | Mc.PsatzZ -> mkApp( Lazy.force coq_PsatzZ,[| z|]) in
+ dump_cone e
+
+ let pp_psatz pp_z o e =
+ let rec pp_cone o e =
+ match e with
+ | Mc.PsatzIn n ->
+ Printf.fprintf o "(In %a)%%nat" pp_nat n
+ | Mc.PsatzMulC(e,c) ->
+ Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c
+ | Mc.PsatzSquare e ->
+ Printf.fprintf o "(%a^2)" (pp_pol pp_z) e
+ | Mc.PsatzAdd(e1,e2) ->
+ Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2
+ | Mc.PsatzMulE(e1,e2) ->
+ Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2
+ | Mc.PsatzC p ->
+ Printf.fprintf o "(%a)%%positive" pp_z p
+ | Mc.PsatzZ ->
+ Printf.fprintf o "0" in
+ pp_cone o e
+
+ let rec dump_op = function
+ | Mc.OpEq-> Lazy.force coq_OpEq
+ | Mc.OpNEq-> Lazy.force coq_OpNEq
+ | Mc.OpLe -> Lazy.force coq_OpLe
+ | Mc.OpGe -> Lazy.force coq_OpGe
+ | Mc.OpGt-> Lazy.force coq_OpGt
+ | Mc.OpLt-> Lazy.force coq_OpLt
+
+ let pp_op o e=
+ match e with
+ | Mc.OpEq-> Printf.fprintf o "="
+ | Mc.OpNEq-> Printf.fprintf o "<>"
+ | Mc.OpLe -> Printf.fprintf o "=<"
+ | Mc.OpGe -> Printf.fprintf o ">="
+ | Mc.OpGt-> Printf.fprintf o ">"
+ | Mc.OpLt-> Printf.fprintf o "<"
+
+ let pp_cstr pp_z o {Mc.flhs = l ; Mc.fop = op ; Mc.frhs = r } =
+ Printf.fprintf o"(%a %a %a)" (pp_expr pp_z) l pp_op op (pp_expr pp_z) r
+
+ let dump_cstr typ dump_constant {Mc.flhs = e1 ; Mc.fop = o ; Mc.frhs = e2} =
+ Term.mkApp(Lazy.force coq_Build,
+ [| typ; dump_expr typ dump_constant e1 ;
+ dump_op o ;
+ dump_expr typ dump_constant e2|])
+
+ let assoc_const x l =
+ try
+ snd (List.find (fun (x',y) -> x = Lazy.force x') l)
+ with
+ Not_found -> raise ParseError
+
+ let zop_table = [
+ coq_Zgt, Mc.OpGt ;
+ coq_Zge, Mc.OpGe ;
+ coq_Zlt, Mc.OpLt ;
+ coq_Zle, Mc.OpLe ]
+
+ let rop_table = [
+ coq_Rgt, Mc.OpGt ;
+ coq_Rge, Mc.OpGe ;
+ coq_Rlt, Mc.OpLt ;
+ coq_Rle, Mc.OpLe ]
+
+ let qop_table = [
+ coq_Qlt, Mc.OpLt ;
+ coq_Qle, Mc.OpLe ;
+ coq_Qeq, Mc.OpEq
+ ]
+
+ let parse_zop (op,args) =
match kind_of_term op with
- | Const x -> (assoc_const op rop_table, args.(0) , args.(1))
+ | Const x -> (assoc_const op zop_table, args.(0) , args.(1))
| Ind(n,0) ->
- if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_R
- then (Mc.OpEq, args.(1), args.(2))
- else raise ParseError
- | _ -> failwith "parse_zop"
-
- let parse_qop (op,args) =
- (assoc_const op qop_table, args.(0) , args.(1))
-
-
- module Env =
- struct
- type t = constr list
-
- let compute_rank_add env v =
- let rec _add env n v =
- match env with
- | [] -> ([v],n)
- | e::l ->
- if eq_constr e v
- then (env,n)
- else
- let (env,n) = _add l ( n+1) v in
- (e::env,n) in
- let (env, n) = _add env 1 v in
- (env, CamlToCoq.idx n)
-
-
- let empty = []
-
- let elements env = env
-
- end
-
-
- let is_constant t = (* This is an approx *)
- match kind_of_term t with
- | Construct(i,_) -> true
- | _ -> false
-
-
- type 'a op =
- | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr)
- | Opp
- | Power
- | Ukn of string
-
-
- let assoc_ops x l =
- try
- snd (List.find (fun (x',y) -> x = Lazy.force x') l)
- with
- Not_found -> Ukn "Oups"
-
-
-
- let parse_expr parse_constant parse_exp ops_spec env term =
- if debug
- then (Pp.pp (Pp.str "parse_expr: ");
- Pp.pp_flush ();Pp.pp (Printer.prterm term); Pp.pp_flush ());
-
- let constant_or_variable env term =
+ if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_Z
+ then (Mc.OpEq, args.(1), args.(2))
+ else raise ParseError
+ | _ -> failwith "parse_zop"
+
+ let parse_rop (op,args) =
+ match kind_of_term op with
+ | Const x -> (assoc_const op rop_table, args.(0) , args.(1))
+ | Ind(n,0) ->
+ if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_R
+ then (Mc.OpEq, args.(1), args.(2))
+ else raise ParseError
+ | _ -> failwith "parse_zop"
+
+ let parse_qop (op,args) =
+ (assoc_const op qop_table, args.(0) , args.(1))
+
+ let is_constant t = (* This is an approx *)
+ match kind_of_term t with
+ | Construct(i,_) -> true
+ | _ -> false
+
+ type 'a op =
+ | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr)
+ | Opp
+ | Power
+ | Ukn of string
+
+ let assoc_ops x l =
try
- ( Mc.PEc (parse_constant term) , env)
- with ParseError ->
- let (env,n) = Env.compute_rank_add env term in
- (Mc.PEX n , env) in
-
- let rec parse_expr env term =
- let combine env op (t1,t2) =
- let (expr1,env) = parse_expr env t1 in
- let (expr2,env) = parse_expr env t2 in
- (op expr1 expr2,env) in
-
- match kind_of_term term with
- | App(t,args) ->
- (
- match kind_of_term t with
- | Const c ->
- ( match assoc_ops t ops_spec with
- | Binop f -> combine env f (args.(0),args.(1))
- | Opp -> let (expr,env) = parse_expr env args.(0) in
- (Mc.PEopp expr, env)
- | Power ->
- begin
- try
- let (expr,env) = parse_expr env args.(0) in
- let power = (parse_exp expr args.(1)) in
- (power , env)
- with _ -> (* if the exponent is a variable *)
- let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
- end
- | Ukn s ->
- if debug
- then (Printf.printf "unknown op: %s\n" s; flush stdout;);
- let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
- )
- | _ -> constant_or_variable env term
- )
- | _ -> constant_or_variable env term in
- parse_expr env term
-
-
- let zop_spec =
+ snd (List.find (fun (x',y) -> x = Lazy.force x') l)
+ with
+ Not_found -> Ukn "Oups"
+
+ (**
+ * MODULE: Env is for environment.
+ *)
+
+ module Env =
+ struct
+ type t = constr list
+
+ let compute_rank_add env v =
+ let rec _add env n v =
+ match env with
+ | [] -> ([v],n)
+ | e::l ->
+ if eq_constr e v
+ then (env,n)
+ else
+ let (env,n) = _add l ( n+1) v in
+ (e::env,n) in
+ let (env, n) = _add env 1 v in
+ (env, CamlToCoq.idx n)
+
+ let empty = []
+
+ let elements env = env
+
+ end (* MODULE END: Env *)
+
+ (**
+ * This is the big generic function for expression parsers.
+ *)
+
+ let parse_expr parse_constant parse_exp ops_spec env term =
+ if debug
+ then (Pp.pp (Pp.str "parse_expr: ");
+ Pp.pp_flush ();Pp.pp (Printer.prterm term); Pp.pp_flush ());
+
+ let constant_or_variable env term =
+ try
+ ( Mc.PEc (parse_constant term) , env)
+ with ParseError ->
+ let (env,n) = Env.compute_rank_add env term in
+ (Mc.PEX n , env) in
+
+ let rec parse_expr env term =
+ let combine env op (t1,t2) =
+ let (expr1,env) = parse_expr env t1 in
+ let (expr2,env) = parse_expr env t2 in
+ (op expr1 expr2,env) in
+
+ match kind_of_term term with
+ | App(t,args) ->
+ (
+ match kind_of_term t with
+ | Const c ->
+ ( match assoc_ops t ops_spec with
+ | Binop f -> combine env f (args.(0),args.(1))
+ | Opp -> let (expr,env) = parse_expr env args.(0) in
+ (Mc.PEopp expr, env)
+ | Power ->
+ begin
+ try
+ let (expr,env) = parse_expr env args.(0) in
+ let power = (parse_exp expr args.(1)) in
+ (power , env)
+ with _ -> (* if the exponent is a variable *)
+ let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
+ end
+ | Ukn s ->
+ if debug
+ then (Printf.printf "unknown op: %s\n" s; flush stdout;);
+ let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
+ )
+ | _ -> constant_or_variable env term
+ )
+ | _ -> constant_or_variable env term in
+ parse_expr env term
+
+ let zop_spec =
+ [
+ coq_Zplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+ coq_Zminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+ coq_Zmult , Binop (fun x y -> Mc.PEmul (x,y)) ;
+ coq_Zopp , Opp ;
+ coq_Zpower , Power]
+
+ let qop_spec =
[
- coq_Zplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
- coq_Zminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
- coq_Zmult , Binop (fun x y -> Mc.PEmul (x,y)) ;
- coq_Zopp , Opp ;
- coq_Zpower , Power]
-
-let qop_spec =
- [
- coq_Qplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
- coq_Qminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
- coq_Qmult , Binop (fun x y -> Mc.PEmul (x,y)) ;
- coq_Qopp , Opp ;
- coq_Qpower , Power]
-
-let rop_spec =
- [
- coq_Rplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
- coq_Rminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
- coq_Rmult , Binop (fun x y -> Mc.PEmul (x,y)) ;
- coq_Ropp , Opp ;
- coq_Rpower , Power]
-
-
-
-
-
-let zconstant = parse_z
-let qconstant = parse_q
-
+ coq_Qplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+ coq_Qminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+ coq_Qmult , Binop (fun x y -> Mc.PEmul (x,y)) ;
+ coq_Qopp , Opp ;
+ coq_Qpower , Power]
-let rconstant term =
- if debug
- then (Pp.pp_flush ();
- Pp.pp (Pp.str "rconstant: ");
- Pp.pp (Printer.prterm term); Pp.pp_flush ());
- match Term.kind_of_term term with
- | Const x ->
- if term = Lazy.force coq_R0
- then Mc.Z0
- else if term = Lazy.force coq_R1
- then Mc.Zpos Mc.XH
- else raise ParseError
- | _ -> raise ParseError
-
-
-let parse_zexpr = parse_expr
- zconstant
- (fun expr x ->
- let exp = (parse_z x) in
- match exp with
- | Mc.Zneg _ -> Mc.PEc Mc.Z0
- | _ -> Mc.PEpow(expr, Mc.n_of_Z exp))
- zop_spec
-
-let parse_qexpr = parse_expr
- qconstant
+ let rop_spec =
+ [
+ coq_Rplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+ coq_Rminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+ coq_Rmult , Binop (fun x y -> Mc.PEmul (x,y)) ;
+ coq_Ropp , Opp ;
+ coq_Rpower , Power]
+
+ let zconstant = parse_z
+ let qconstant = parse_q
+
+ let rconstant term =
+ if debug
+ then (Pp.pp_flush ();
+ Pp.pp (Pp.str "rconstant: ");
+ Pp.pp (Printer.prterm term); Pp.pp_flush ());
+ match Term.kind_of_term term with
+ | Const x ->
+ if term = Lazy.force coq_R0
+ then Mc.Z0
+ else if term = Lazy.force coq_R1
+ then Mc.Zpos Mc.XH
+ else raise ParseError
+ | _ -> raise ParseError
+
+ let parse_zexpr = parse_expr
+ zconstant
+ (fun expr x ->
+ let exp = (parse_z x) in
+ match exp with
+ | Mc.Zneg _ -> Mc.PEc Mc.Z0
+ | _ -> Mc.PEpow(expr, Mc.n_of_Z exp))
+ zop_spec
+
+ let parse_qexpr = parse_expr
+ qconstant
+ (fun expr x ->
+ let exp = parse_z x in
+ match exp with
+ | Mc.Zneg _ ->
+ begin
+ match expr with
+ | Mc.PEc q -> Mc.PEc (Mc.qpower q exp)
+ | _ -> print_string "parse_qexpr parse error" ; flush stdout ; raise ParseError
+ end
+ | _ -> let exp = Mc.n_of_Z exp in
+ Mc.PEpow(expr,exp))
+ qop_spec
+
+ let parse_rexpr = parse_expr
+ rconstant
(fun expr x ->
- let exp = parse_z x in
- match exp with
- | Mc.Zneg _ ->
- begin
- match expr with
- | Mc.PEc q -> Mc.PEc (Mc.qpower q exp)
- | _ -> print_string "parse_qexpr parse error" ; flush stdout ; raise ParseError
- end
- | _ -> let exp = Mc.n_of_Z exp in
- Mc.PEpow(expr,exp))
- qop_spec
-
-let parse_rexpr = parse_expr
- rconstant
- (fun expr x ->
- let exp = Mc.n_of_nat (parse_nat x) in
- Mc.PEpow(expr,exp))
- rop_spec
-
-
- let parse_arith parse_op parse_expr env cstr =
- if debug
- then (Pp.pp_flush ();
- Pp.pp (Pp.str "parse_arith: ");
- Pp.pp (Printer.prterm cstr);
- Pp.pp_flush ());
- match kind_of_term cstr with
- | App(op,args) ->
- let (op,lhs,rhs) = parse_op (op,args) in
- let (e1,env) = parse_expr env lhs in
- let (e2,env) = parse_expr env rhs in
- ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env)
- | _ -> failwith "error : parse_arith(2)"
-
- let parse_zarith = parse_arith parse_zop parse_zexpr
-
- let parse_qarith = parse_arith parse_qop parse_qexpr
-
- let parse_rarith = parse_arith parse_rop parse_rexpr
-
-
- (* generic parsing of arithmetic expressions *)
-
-
-
-
- let rec f2f = function
- | TT -> Mc.TT
- | FF -> Mc.FF
- | X _ -> Mc.X
- | A (x,_,_) -> Mc.A x
- | C (a,b) -> Mc.Cj(f2f a,f2f b)
- | D (a,b) -> Mc.D(f2f a,f2f b)
- | N (a) -> Mc.N(f2f a)
- | I(a,_,b) -> Mc.I(f2f a,f2f b)
-
- let is_prop t =
- match t with
- | Names.Anonymous -> true (* Not quite right *)
- | Names.Name x -> false
-
- let mkC f1 f2 = C(f1,f2)
- let mkD f1 f2 = D(f1,f2)
- let mkIff f1 f2 = C(I(f1,None,f2),I(f2,None,f1))
- let mkI f1 f2 = I(f1,None,f2)
-
- let mkformula_binary g term f1 f2 =
- match f1 , f2 with
- | X _ , X _ -> X(term)
- | _ -> g f1 f2
-
- let parse_formula parse_atom env term =
-
- let parse_atom env tg t = try let (at,env) = parse_atom env t in
- (A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in
-
- let rec xparse_formula env tg term =
- match kind_of_term term with
- | App(l,rst) ->
- (match rst with
- | [|a;b|] when l = Lazy.force coq_and ->
- let f,env,tg = xparse_formula env tg a in
- let g,env, tg = xparse_formula env tg b in
- mkformula_binary mkC term f g,env,tg
- | [|a;b|] when l = Lazy.force coq_or ->
- let f,env,tg = xparse_formula env tg a in
- let g,env,tg = xparse_formula env tg b in
- mkformula_binary mkD term f g,env,tg
- | [|a|] when l = Lazy.force coq_not ->
- let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg)
- | [|a;b|] when l = Lazy.force coq_iff ->
- let f,env,tg = xparse_formula env tg a in
- let g,env,tg = xparse_formula env tg b in
- mkformula_binary mkIff term f g,env,tg
- | _ -> parse_atom env tg term)
- | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b) ->
- let f,env,tg = xparse_formula env tg a in
- let g,env,tg = xparse_formula env tg b in
- mkformula_binary mkI term f g,env,tg
- | _ when term = Lazy.force coq_True -> (TT,env,tg)
- | _ when term = Lazy.force coq_False -> (FF,env,tg)
- | _ -> X(term),env,tg in
- xparse_formula env term
-
- let coq_TT = lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "TT")
- let coq_FF = lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "FF")
- let coq_And = lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "Cj")
- let coq_Or = lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "D")
- let coq_Neg = lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "N")
- let coq_Atom = lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "A")
- let coq_X = lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "X")
- let coq_Impl = lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "I")
- let coq_Formula = lazy
- (gen_constant_in_modules "ZMicromega"
- [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "BFormula")
-
- let dump_formula typ dump_atom f =
- let rec xdump f =
- match f with
- | TT -> mkApp(Lazy.force coq_TT,[| typ|])
- | FF -> mkApp(Lazy.force coq_FF,[| typ|])
- | C(x,y) -> mkApp(Lazy.force coq_And,[| typ ; xdump x ; xdump y|])
- | D(x,y) -> mkApp(Lazy.force coq_Or,[| typ ; xdump x ; xdump y|])
- | I(x,_,y) -> mkApp(Lazy.force coq_Impl,[| typ ; xdump x ; xdump y|])
- | N(x) -> mkApp(Lazy.force coq_Neg,[| typ ; xdump x|])
- | A(x,_,_) -> mkApp(Lazy.force coq_Atom,[| typ ; dump_atom x|])
- | X(t) -> mkApp(Lazy.force coq_X,[| typ ; t|]) in
-
+ let exp = Mc.n_of_nat (parse_nat x) in
+ Mc.PEpow(expr,exp))
+ rop_spec
+
+ let parse_arith parse_op parse_expr env cstr =
+ if debug
+ then (Pp.pp_flush ();
+ Pp.pp (Pp.str "parse_arith: ");
+ Pp.pp (Printer.prterm cstr);
+ Pp.pp_flush ());
+ match kind_of_term cstr with
+ | App(op,args) ->
+ let (op,lhs,rhs) = parse_op (op,args) in
+ let (e1,env) = parse_expr env lhs in
+ let (e2,env) = parse_expr env rhs in
+ ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env)
+ | _ -> failwith "error : parse_arith(2)"
+
+ let parse_zarith = parse_arith parse_zop parse_zexpr
+
+ let parse_qarith = parse_arith parse_qop parse_qexpr
+
+ let parse_rarith = parse_arith parse_rop parse_rexpr
+
+ (* generic parsing of arithmetic expressions *)
+
+ let rec f2f = function
+ | TT -> Mc.TT
+ | FF -> Mc.FF
+ | X _ -> Mc.X
+ | A (x,_,_) -> Mc.A x
+ | C (a,b) -> Mc.Cj(f2f a,f2f b)
+ | D (a,b) -> Mc.D(f2f a,f2f b)
+ | N (a) -> Mc.N(f2f a)
+ | I(a,_,b) -> Mc.I(f2f a,f2f b)
+
+ let is_prop t =
+ match t with
+ | Names.Anonymous -> true (* Not quite right *)
+ | Names.Name x -> false
+
+ let mkC f1 f2 = C(f1,f2)
+ let mkD f1 f2 = D(f1,f2)
+ let mkIff f1 f2 = C(I(f1,None,f2),I(f2,None,f1))
+ let mkI f1 f2 = I(f1,None,f2)
+
+ let mkformula_binary g term f1 f2 =
+ match f1 , f2 with
+ | X _ , X _ -> X(term)
+ | _ -> g f1 f2
+
+ (**
+ * This is the big generic function for formula parsers.
+ *)
+
+ let parse_formula parse_atom env term =
+
+ let parse_atom env tg t = try let (at,env) = parse_atom env t in
+ (A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in
+
+ let rec xparse_formula env tg term =
+ match kind_of_term term with
+ | App(l,rst) ->
+ (match rst with
+ | [|a;b|] when l = Lazy.force coq_and ->
+ let f,env,tg = xparse_formula env tg a in
+ let g,env, tg = xparse_formula env tg b in
+ mkformula_binary mkC term f g,env,tg
+ | [|a;b|] when l = Lazy.force coq_or ->
+ let f,env,tg = xparse_formula env tg a in
+ let g,env,tg = xparse_formula env tg b in
+ mkformula_binary mkD term f g,env,tg
+ | [|a|] when l = Lazy.force coq_not ->
+ let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg)
+ | [|a;b|] when l = Lazy.force coq_iff ->
+ let f,env,tg = xparse_formula env tg a in
+ let g,env,tg = xparse_formula env tg b in
+ mkformula_binary mkIff term f g,env,tg
+ | _ -> parse_atom env tg term)
+ | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b) ->
+ let f,env,tg = xparse_formula env tg a in
+ let g,env,tg = xparse_formula env tg b in
+ mkformula_binary mkI term f g,env,tg
+ | _ when term = Lazy.force coq_True -> (TT,env,tg)
+ | _ when term = Lazy.force coq_False -> (FF,env,tg)
+ | _ -> X(term),env,tg in
+ xparse_formula env term
+
+ let dump_formula typ dump_atom f =
+ let rec xdump f =
+ match f with
+ | TT -> mkApp(Lazy.force coq_TT,[|typ|])
+ | FF -> mkApp(Lazy.force coq_FF,[|typ|])
+ | C(x,y) -> mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|])
+ | D(x,y) -> mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|])
+ | I(x,_,y) -> mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|])
+ | N(x) -> mkApp(Lazy.force coq_Neg,[|typ ; xdump x|])
+ | A(x,_,_) -> mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|])
+ | X(t) -> mkApp(Lazy.force coq_X,[|typ ; t|]) in
xdump f
-
-
-
- (* ! reverse the list of bindings *)
- let set l concl =
- let rec _set acc = function
- | [] -> acc
- | (e::l) ->
- let (name,expr,typ) = e in
- _set (Term.mkNamedLetIn
- (Names.id_of_string name)
- expr typ acc) l in
- _set concl l
-
-
-end
+ (**
+ * Given a conclusion and a list of affectations, rebuild a term prefixed by
+ * the appropriate letins.
+ * TODO: reverse the list of bindings!
+ *)
+
+ let set l concl =
+ let rec xset acc = function
+ | [] -> acc
+ | (e::l) ->
+ let (name,expr,typ) = e in
+ xset (Term.mkNamedLetIn
+ (Names.id_of_string name)
+ expr typ acc) l in
+ xset concl l
+
+end (**
+ * MODULE END: M
+ *)
open M
-
let rec sig_of_cone = function
- | Mc.PsatzIn n -> [CoqToCaml.nat n]
- | Mc.PsatzMulE(w1,w2) ->
- (sig_of_cone w1)@(sig_of_cone w2)
- | Mc.PsatzMulC(w1,w2) -> (sig_of_cone w2)
- | Mc.PsatzAdd(w1,w2) -> (sig_of_cone w1)@(sig_of_cone w2)
+ | Mc.PsatzIn n -> [CoqToCaml.nat n]
+ | Mc.PsatzMulE(w1,w2) -> (sig_of_cone w1)@(sig_of_cone w2)
+ | Mc.PsatzMulC(w1,w2) -> (sig_of_cone w2)
+ | Mc.PsatzAdd(w1,w2) -> (sig_of_cone w1)@(sig_of_cone w2)
| _ -> []
let same_proof sg cl1 cl2 =
@@ -961,7 +1028,6 @@ let tags_of_cnf wits cnf =
List.fold_left2 (fun acc w cl -> tags_of_clause acc w cl)
Names.Idset.empty wits cnf
-
let find_witness prover polys1 = try_any prover polys1
let rec witness prover l1 l2 =
@@ -976,13 +1042,11 @@ let rec witness prover l1 l2 =
| Some l -> Some (w::l)
)
-
let rec apply_ids t ids =
match ids with
| [] -> t
| i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
-
let coq_Node = lazy
(Coqlib.gen_constant_in_modules "VarMap"
[["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")
@@ -993,7 +1057,6 @@ let coq_Empty = lazy
(Coqlib.gen_constant_in_modules "VarMap"
[["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
-
let btree_of_array typ a =
let size_of_a = Array.length a in
let semi_size_of_a = size_of_a lsr 1 in
@@ -1064,7 +1127,7 @@ let rec parse_hyps parse_arith env tg hyps =
(*(if debug then Printf.printf "parse_arith : %s\n" x);*)
-exception ParseError
+(*exception ParseError*)
let parse_goal parse_arith env hyps term =
(* try*)
@@ -1073,6 +1136,9 @@ let parse_goal parse_arith env hyps term =
(lhyps,f,env)
(* with Failure x -> raise ParseError*)
+(**
+ * The datastructures that aggregate theory-dependent proof values.
+ *)
type ('d, 'prf) domain_spec = {
typ : Term.constr; (* Z, Q , R *)
@@ -1098,7 +1164,7 @@ let qq_domain_spec = lazy {
dump_proof = dump_psatz coq_Q dump_q
}
-let rz_domain_spec = lazy {
+let rz_domain_spec = lazy {
typ = Lazy.force coq_R;
coeff = Lazy.force coq_Z;
dump_coeff = dump_z;
@@ -1106,76 +1172,59 @@ let rz_domain_spec = lazy {
dump_proof = dump_psatz coq_Z dump_z
}
+(**
+ * Instanciate the current Coq goal with a Micromega formula, a varmap, and a
+ * witness.
+ *)
-let abstract_formula hyps f =
-
- let rec xabs f =
- match f with
- | X c -> X c
- | A(a,t,term) -> if TagSet.mem t hyps then A(a,t,term) else X(term)
- | C(f1,f2) ->
- (match xabs f1 , xabs f2 with
- | X a1 , X a2 -> X (Term.mkApp(Lazy.force coq_and, [|a1;a2|]))
- | f1 , f2 -> C(f1,f2) )
- | D(f1,f2) ->
- (match xabs f1 , xabs f2 with
- | X a1 , X a2 -> X (Term.mkApp(Lazy.force coq_or, [|a1;a2|]))
- | f1 , f2 -> D(f1,f2) )
- | N(f) ->
- (match xabs f with
- | X a -> X (Term.mkApp(Lazy.force coq_not, [|a|]))
- | f -> N f)
- | I(f1,hyp,f2) ->
- (match xabs f1 , hyp, xabs f2 with
- | X a1 , Some _ , af2 -> af2
- | X a1 , None , X a2 -> X (Term.mkArrow a1 a2)
- | af1 , _ , af2 -> I(af1,hyp,af2)
- )
- | FF -> FF
- | TT -> TT
-
- in xabs f
-
-
-let micromega_order_change spec cert cert_typ env ff gl =
- let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
-
+let micromega_order_change spec cert cert_typ env ff gl =
+ let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in
let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
- let vm = dump_varmap ( spec.typ) env in
+ let vm = dump_varmap (spec.typ) env in
Tactics.change_in_concl None
(set
[
- ("__ff", ff, Term.mkApp(Lazy.force coq_Formula ,[| formula_typ |]));
- ("__varmap", vm , Term.mkApp
+ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
+ ("__varmap", vm, Term.mkApp
(Coqlib.gen_constant_in_modules "VarMap"
- [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "t", [| spec.typ|]));
- ("__wit", cert,cert_typ)
+ [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|]));
+ ("__wit", cert, cert_typ)
]
- (Tacmach.pf_concl gl )
-
- )
+ (Tacmach.pf_concl gl)
+ )
gl
+(**
+ * The datastructures that aggregate prover attributes.
+ *)
type ('a,'prf) prover = {
name : string ; (* name of the prover *)
- prover : 'a list -> 'prf option; (* the prover itself *)
- hyps : 'prf -> ISet.t; (* extract the indexes of the hypotheses really used in the proof *)
- compact : 'prf -> (int -> int) -> 'prf; (* remap the hyp indexes according to function *)
+ prover : 'a list -> 'prf option ; (* the prover itself *)
+ hyps : 'prf -> ISet.t ; (* extract the indexes of the hypotheses really used in the proof *)
+ compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *)
pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *)
- pp_f : out_channel -> 'a -> unit
+ pp_f : out_channel -> 'a -> unit (* pretty printing of the formulas (polynomials)*)
}
-let find_witness provers polys1 =
+(**
+ * Given a list of provers and a disjunction of atoms, find a proof of any of
+ * the atoms. Returns an (optional) pair of a proof and a prover
+ * datastructure.
+ *)
+let find_witness provers polys1 =
let provers = List.map (fun p ->
(fun l ->
match p.prover l with
| None -> None
| Some prf -> Some(prf,p)) , p.name) provers in
+ try_any provers (List.map fst polys1)
- try_any provers (List.map fst polys1)
-
+(**
+ * Given a list of provers and a CNF, find a proof for each of the clauses.
+ * Return the proofs as a list.
+ *)
let witness_list prover l =
let rec xwitness_list l =
@@ -1191,49 +1240,48 @@ let witness_list prover l =
) in
xwitness_list l
-
let witness_list_tags = witness_list
-let is_singleton = function [] -> true | [e] -> true | _ -> false
+(* *Deprecated* let is_singleton = function [] -> true | [e] -> true | _ -> false *)
let pp_ml_list pp_elt o l =
output_string o "[" ;
List.iter (fun x -> Printf.fprintf o "%a ;" pp_elt x) l ;
output_string o "]"
+(**
+ * Prune the proof object, according to the 'diff' between two cnf formulas.
+ *)
+
let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
let compact_proof (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
let new_cl = Mutils.mapi (fun (f,_) i -> (f,i)) new_cl in
let remap i =
let formula = try fst (List.nth old_cl i) with Failure _ -> failwith "bad old index" in
- List.assoc formula new_cl in
-
- if debug then
- begin
- Printf.printf "\ncompact_proof : %a %a %a"
- (pp_ml_list prover.pp_f) (List.map fst old_cl)
- prover.pp_prf prf
- (pp_ml_list prover.pp_f) (List.map fst new_cl) ;
- flush stdout
- end ;
- let res = try prover.compact prf remap with x ->
- if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
- (* This should not happen -- this is the recovery plan... *)
- match prover.prover (List.map fst new_cl) with
- | None -> failwith "proof compaction error"
- | Some p -> p
- in
- if debug then
- begin
- Printf.printf " -> %a\n"
- prover.pp_prf res ;
- flush stdout
- end
- ;
- res in
-
-
+ List.assoc formula new_cl in
+ if debug then
+ begin
+ Printf.printf "\ncompact_proof : %a %a %a"
+ (pp_ml_list prover.pp_f) (List.map fst old_cl)
+ prover.pp_prf prf
+ (pp_ml_list prover.pp_f) (List.map fst new_cl) ;
+ flush stdout
+ end ;
+ let res = try prover.compact prf remap with x ->
+ if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
+ (* This should not happen -- this is the recovery plan... *)
+ match prover.prover (List.map fst new_cl) with
+ | None -> failwith "proof compaction error"
+ | Some p -> p
+ in
+ if debug then
+ begin
+ Printf.printf " -> %a\n"
+ prover.pp_prf res ;
+ flush stdout
+ end ;
+ res in
let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
let hyps_idx = prover.hyps prf in
@@ -1242,89 +1290,135 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
let cnf_res = List.combine cnf_ff res in (* we get pairs clause * proof *)
- List.map (fun x ->
- let (o,p) = List.find (fun (l,p) -> is_proof_compatible l p x) cnf_res
- in compact_proof o p x) cnf_ff'
+ List.map (fun x ->
+ let (o,p) = List.find (fun (l,p) -> is_proof_compatible l p x) cnf_res
+ in compact_proof o p x) cnf_ff'
+
+
+(**
+ * "Hide out" tagged atoms of a formula by transforming them into generic
+ * variables. See the Tag module in mutils.ml for more.
+ *)
+let abstract_formula hyps f =
+ let rec xabs f =
+ match f with
+ | X c -> X c
+ | A(a,t,term) -> if TagSet.mem t hyps then A(a,t,term) else X(term)
+ | C(f1,f2) ->
+ (match xabs f1 , xabs f2 with
+ | X a1 , X a2 -> X (Term.mkApp(Lazy.force coq_and, [|a1;a2|]))
+ | f1 , f2 -> C(f1,f2) )
+ | D(f1,f2) ->
+ (match xabs f1 , xabs f2 with
+ | X a1 , X a2 -> X (Term.mkApp(Lazy.force coq_or, [|a1;a2|]))
+ | f1 , f2 -> D(f1,f2) )
+ | N(f) ->
+ (match xabs f with
+ | X a -> X (Term.mkApp(Lazy.force coq_not, [|a|]))
+ | f -> N f)
+ | I(f1,hyp,f2) ->
+ (match xabs f1 , hyp, xabs f2 with
+ | X a1 , Some _ , af2 -> af2
+ | X a1 , None , X a2 -> X (Term.mkArrow a1 a2)
+ | af1 , _ , af2 -> I(af1,hyp,af2)
+ )
+ | FF -> FF
+ | TT -> TT
+ in xabs f
+(**
+ * This exception is raised by really_call_csdpcert if Coq's configure didn't
+ * find a CSDP executable.
+ *)
+exception CsdpNotFound
-let micromega_tauto negate normalise spec prover env polys1 polys2 gl =
+(**
+ * This is the core of Micromega: apply the prover, analyze the result and
+ * prune unused fomulas, and finally modify the proof state.
+ *)
+
+let micromega_tauto negate normalise spec prover env polys1 polys2 gl =
let spec = Lazy.force spec in
+
+ (* Express the goal as one big implication *)
let (ff,ids) =
List.fold_right
- (fun (id,f) (cc,ids) ->
+ (fun (id,f) (cc,ids) ->
match f with
X _ -> (cc,ids)
| _ -> (I(f,Some id,cc), id::ids))
polys1 (polys2,[]) in
+ (* Convert the aplpication into a (mc_)cnf (a list of lists of formulas) *)
let cnf_ff = cnf negate normalise ff in
+ if debug then
+ begin
+ Pp.pp (Pp.str "Formula....\n") ;
+ let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
+ let ff = dump_formula formula_typ
+ (dump_cstr spec.typ spec.dump_coeff) ff in
+ Pp.pp (Printer.prterm ff) ; Pp.pp_flush ();
+ Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
+ end;
+
+ match witness_list_tags prover cnf_ff with
+ | None -> Tacticals.tclFAIL 0 (Pp.str " Cannot find witness") gl
+ | Some res -> (*Printf.printf "\nList %i" (List.length `res); *)
+ let hyps = List.fold_left (fun s (cl,(prf,p)) ->
+ let tags = ISet.fold (fun i s -> let t = snd (List.nth cl i) in
+ if debug then (Printf.fprintf stdout "T : %i -> %a" i Tag.pp t) ;
+ (*try*) TagSet.add t s (* with Invalid_argument _ -> s*)) (p.hyps prf) TagSet.empty in
+ TagSet.union s tags) TagSet.empty (List.combine cnf_ff res) in
+
+ if debug then (Printf.printf "TForm : %a\n" pp_formula ff ; flush stdout;
+ Printf.printf "Hyps : %a\n" (fun o s -> TagSet.fold (fun i _ -> Printf.fprintf o "%a " Tag.pp i) s ()) hyps) ;
+
+ let ff' = abstract_formula hyps ff in
+ let cnf_ff' = cnf negate normalise ff' in
+
if debug then
begin
- Pp.pp (Pp.str "Formula....\n") ;
+ Pp.pp (Pp.str "\nAFormula\n") ;
let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
- let ff = dump_formula formula_typ
- (dump_cstr spec.typ spec.dump_coeff) ff in
- Pp.pp (Printer.prterm ff) ; Pp.pp_flush ();
- Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
+ let ff' = dump_formula formula_typ
+ (dump_cstr spec.typ spec.dump_coeff) ff' in
+ Pp.pp (Printer.prterm ff') ; Pp.pp_flush ();
+ Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
end;
- match witness_list_tags prover cnf_ff with
- | None -> Tacticals.tclFAIL 0 (Pp.str "Cannot find witness") gl
- | Some res -> (*Printf.printf "\nList %i" (List.length `res); *)
-
- let hyps = List.fold_left (fun s (cl,(prf,p)) ->
- let tags = ISet.fold (fun i s -> let t = snd (List.nth cl i) in
- if debug then (Printf.fprintf stdout "T : %i -> %a" i Tag.pp t) ;
- (*try*) TagSet.add t s (* with Invalid_argument _ -> s*)) (p.hyps prf) TagSet.empty in
- TagSet.union s tags) TagSet.empty (List.combine cnf_ff res) in
-
- if debug then (Printf.printf "TForm : %a\n" pp_formula ff ; flush stdout;
- Printf.printf "Hyps : %a\n" (fun o s -> TagSet.fold (fun i _ -> Printf.fprintf o "%a " Tag.pp i) s ()) hyps) ;
-
- let ff' = abstract_formula hyps ff in
-
- let cnf_ff' = cnf negate normalise ff' in
-
- if debug then
- begin
- Pp.pp (Pp.str "\nAFormula\n") ;
- let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
- let ff' = dump_formula formula_typ
- (dump_cstr spec.typ spec.dump_coeff) ff' in
- Pp.pp (Printer.prterm ff') ; Pp.pp_flush ();
- Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
- end;
-
- (* Even if it does not work, this does not mean it is not provable
- -- the prover is REALLY incomplete *)
-(* if debug then
- begin
- (* recompute the proofs *)
- match witness_list_tags prover cnf_ff' with
- | None -> failwith "abstraction is wrong"
- | Some res -> ()
- end ; *)
- let res' = compact_proofs cnf_ff res cnf_ff' in
-
- let (ff',res',ids) = (ff',res',List.map Term.mkVar (ids_of_formula ff')) in
-
- let res' = dump_list (spec.proof_typ) spec.dump_proof res' in
- (Tacticals.tclTHENSEQ
- [
- Tactics.generalize ids;
- micromega_order_change spec res'
- (Term.mkApp(Lazy.force coq_list,[| spec.proof_typ|])) env ff' ;
- ]) gl
-
+ (* Even if it does not work, this does not mean it is not provable
+ -- the prover is REALLY incomplete *)
+ (* if debug then
+ begin
+ (* recompute the proofs *)
+ match witness_list_tags prover cnf_ff' with
+ | None -> failwith "abstraction is wrong"
+ | Some res -> ()
+ end ; *)
+ let res' = compact_proofs cnf_ff res cnf_ff' in
+
+ let (ff',res',ids) = (ff',res',List.map Term.mkVar (ids_of_formula ff')) in
+
+ let res' = dump_list (spec.proof_typ) spec.dump_proof res' in
+ (Tacticals.tclTHENSEQ
+ [
+ Tactics.generalize ids ;
+ micromega_order_change spec res'
+ (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
+ ]) gl
+
+(**
+ * Parse the proof environment, and call micromega_tauto
+ *)
let micromega_gen
parse_arith
(negate:'cst atom -> 'cst mc_cnf)
(normalise:'cst atom -> 'cst mc_cnf)
- spec prover gl =
+ spec prover gl =
let concl = Tacmach.pf_concl gl in
let hyps = Tacmach.pf_hyps_types gl in
try
@@ -1335,7 +1429,12 @@ let micromega_gen
| Failure x -> flush stdout ; Pp.pp_flush () ;
Tacticals.tclFAIL 0 (Pp.str x) gl
| ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
-
+ | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+ Tacticals.tclFAIL 0 (Pp.str
+ (" Skipping what remains of this tactic: the complexity of the goal requires "
+ ^ "the use of a specialized external tool called csdp. \n\n"
+ ^ "Unfortunately this instance of Coq isn't aware of the presence of any \"csdp\" executable. \n\n"
+ ^ "You may need to specify the location during Coq's pre-compilation configuration step")) gl
let lift_ratproof prover l =
match prover l with
@@ -1346,6 +1445,10 @@ type micromega_polys = (Micromega.q Mc.pol * Mc.op1) list
type csdp_certificate = S of Sos_types.positivstellensatz option | F of string
type provername = string * int option
+(**
+ * The caching mechanism.
+ *)
+
open Persistent_cache
module Cache = PHashtable(struct
@@ -1356,22 +1459,37 @@ end)
let csdp_cache = "csdp.cache"
+(**
+ * Build the command to call csdpcert, and launch it. This in turn will call
+ * the sos driver to the csdp executable.
+ * Throw CsdpNotFound if a Coq isn't aware of any csdp executable.
+ *)
+
let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivstellensatz option =
fun provername poly ->
+ match Coq_config.csdp with
+ | None -> raise CsdpNotFound (* caugth in micromega_gen *)
+ | Some _ -> () ;
+
let cmdname =
List.fold_left Filename.concat (Envars.coqlib ())
["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
- match ((command cmdname [| cmdname |] (provername,poly)) : csdp_certificate) with
+ match ((command cmdname [|cmdname|] (provername,poly)) : csdp_certificate) with
| F str -> failwith str
| S res -> res
-
+(**
+ * Check the cache before calling the prover.
+ *)
let xcall_csdpcert =
Cache.memo csdp_cache (fun (prover,pb) -> really_call_csdpcert prover pb)
+(**
+ * Prover callback functions.
+ *)
let call_csdpcert prover pb = xcall_csdpcert (prover,pb)
@@ -1381,7 +1499,6 @@ let rec z_to_q_pol e =
| Mc.Pinj(p,pol) -> Mc.Pinj(p,z_to_q_pol pol)
| Mc.PX(pol1,p,pol2) -> Mc.PX(z_to_q_pol pol1, p, z_to_q_pol pol2)
-
let call_csdpcert_q provername poly =
match call_csdpcert provername poly with
| None -> None
@@ -1391,7 +1508,6 @@ let call_csdpcert_q provername poly =
then Some cert
else ((print_string "buggy certificate" ; flush stdout) ;None)
-
let call_csdpcert_z provername poly =
let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in
match call_csdpcert provername l with
@@ -1402,8 +1518,7 @@ let call_csdpcert_z provername poly =
then Some cert
else ((print_string "buggy certificate" ; flush stdout) ;None)
-
-let xhyps_of_cone base acc prf =
+let xhyps_of_cone base acc prf =
let rec xtract e acc =
match e with
| Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> acc
@@ -1432,6 +1547,7 @@ let compact_cone prf f =
xinterp prf
let hyps_of_pt pt =
+
let rec xhyps base pt acc =
match pt with
| Mc.DoneProof -> acc
@@ -1449,11 +1565,10 @@ let hyps_of_pt pt =
then (Printf.fprintf stdout "\nhyps_of_pt : %a -> " pp_proof_term pt ; ISet.iter (fun i -> Printf.printf "%i " i) res);
res
-
let compact_pt pt f =
let translate ofset x =
if x < ofset then x
- else (f (x-ofset) + ofset) in
+ else (f (x-ofset) + ofset) in
let rec compact_pt ofset pt =
match pt with
@@ -1464,9 +1579,10 @@ let compact_pt pt f =
Mc.map (fun x -> compact_pt (ofset+1) x) l) in
compact_pt 0 pt
-
-
-(** Definition of provers *)
+(**
+ * Definition of provers.
+ * Instantiates the type ('a,'prf) prover defined above.
+ *)
let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Mc.denorm e , o) l)
@@ -1532,67 +1648,59 @@ end)
let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.zlinear_prover)
-
let linear_Z = {
- name = "lia";
- prover = memo_zlinear_prover ;
- hyps = hyps_of_pt;
+ name = "lia";
+ prover = memo_zlinear_prover ;
+ hyps = hyps_of_pt;
compact = compact_pt;
- pp_prf = pp_proof_term;
+ pp_prf = pp_proof_term;
pp_f = fun o x -> pp_pol pp_z o (fst x)
}
-
-
-(** Instantiation of the tactics *)
+(**
+ * Functions instantiating micromega_gen with the appropriate theories and
+ * solvers
+ *)
let psatzl_Z gl =
micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
- [linear_prover_Z ] gl
-
+ [ linear_prover_Z ] gl
let psatzl_Q gl =
- micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec
- [ linear_prover_Q ] gl
-
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec
+ [ linear_prover_Q ] gl
let psatz_Q i gl =
micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec
- [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] gl
-
+ [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] gl
let psatzl_R gl =
- micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec
- [ linear_prover_R ] gl
+ micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec
+ [ linear_prover_R ] gl
let psatz_R i gl =
micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec
- [ non_linear_prover_R "real_nonlinear_prover" (Some i)] gl
-
+ [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] gl
let psatz_Z i gl =
micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
- [non_linear_prover_Z "real_nonlinear_prover" (Some i) ] gl
-
+ [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] gl
let sos_Z gl =
micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
- [non_linear_prover_Z "pure_sos" None] gl
+ [ non_linear_prover_Z "pure_sos" None ] gl
let sos_Q gl =
micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec
- [non_linear_prover_Q "pure_sos" None] gl
-
+ [ non_linear_prover_Q "pure_sos" None ] gl
let sos_R gl =
micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec
- [non_linear_prover_R "pure_sos" None] gl
-
-
+ [ non_linear_prover_R "pure_sos" None ] gl
let xlia gl =
micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
- [linear_Z] gl
+ [ linear_Z ] gl
(* Local Variables: *)
(* coding: utf-8 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 17:50:39 +0000