From cd798e8cb6f2f5123d61de10172b9dbbcb46f86f Mon Sep 17 00:00:00 2001 From: notin Date: Mon, 8 Mar 2010 12:47:05 +0000 Subject: Application des patches envoyés par F. Besson pour micromega MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 85f007b7-540e-0410-9357-904b9bb8a0f7 --- config/coq_config.mli | 2 + configure | 86 +- plugins/micromega/Psatz.v | 37 +- plugins/micromega/coq_micromega.ml | 2122 +++++++++++++++++++----------------- 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 " + printf "\tSpecifies the path of the CSDP solver intallation\n" echo "-browser " printf "\tUse 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 *) -- cgit v1.2.3