diff options
Diffstat (limited to 'src/versions/standard/coq_micromega_full.ml')
| -rw-r--r-- | src/versions/standard/coq_micromega_full.ml | 2215 |
1 files changed, 0 insertions, 2215 deletions
diff --git a/src/versions/standard/coq_micromega_full.ml b/src/versions/standard/coq_micromega_full.ml deleted file mode 100644 index d957110..0000000 --- a/src/versions/standard/coq_micromega_full.ml +++ /dev/null @@ -1,2215 +0,0 @@ -(*** This file is taken from Coq-8.9.0 to expose more functions than - coq_micromega.mli does. - See https://github.com/coq/coq/issues/9749 . ***) - - -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(* *) -(* 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-20011 *) -(* *) -(************************************************************************) - -open Pp -open Names -open Goptions -open Mutils_full -open Constr -open Tactypes - -module Micromega = Micromega_plugin.Micromega -module Certificate = Micromega_plugin.Certificate -module Sos_types = Micromega_plugin.Sos_types -module Mfourier = Micromega_plugin.Mfourier - -(** - * Debug flag - *) - -let debug = false - -(* Limit the proof search *) - -let max_depth = max_int - -(* Search limit for provers over Q R *) -let lra_proof_depth = ref max_depth - - -(* Search limit for provers over Z *) -let lia_enum = ref true -let lia_proof_depth = ref max_depth - -let get_lia_option () = - (!lia_enum,!lia_proof_depth) - -let get_lra_option () = - !lra_proof_depth - - - -let _ = - - let int_opt l vref = - { - optdepr = false; - optname = List.fold_right (^) l ""; - optkey = l ; - optread = (fun () -> Some !vref); - optwrite = (fun x -> vref := (match x with None -> max_depth | Some v -> v)) - } in - - let lia_enum_opt = - { - optdepr = false; - optname = "Lia Enum"; - optkey = ["Lia2";"Enum"]; - optread = (fun () -> !lia_enum); - optwrite = (fun x -> lia_enum := x) - } in - let _ = declare_int_option (int_opt ["Lra2"; "Depth"] lra_proof_depth) in - let _ = declare_int_option (int_opt ["Lia2"; "Depth"] lia_proof_depth) in - let _ = declare_bool_option lia_enum_opt in - () - -(** - * 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 EConstr.constr - | A of 'cst atom * tag * EConstr.constr - | C of 'cst formula * 'cst formula - | D of 'cst formula * 'cst formula - | N of 'cst formula - | I of 'cst formula * Names.Id.t option * 'cst formula - -(** - * Formula pretty-printer. - *) - -let rec pp_formula o f = - match f with - | TT -> output_string o "tt" - | FF -> output_string o "ff" - | X c -> output_string o "X " - | A(_,t,_) -> Printf.fprintf o "A(%a)" Tag.pp t - | C(f1,f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2 - | D(f1,f2) -> Printf.fprintf o "D(%a,%a)" pp_formula f1 pp_formula f2 - | I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)" - pp_formula f1 - (match n with - | Some id -> Names.Id.to_string id - | None -> "") pp_formula f2 - | N(f) -> Printf.fprintf o "N(%a)" pp_formula f - - -let rec map_atoms fct f = - match f with - | TT -> TT - | FF -> FF - | X x -> X x - | A (at,tg,cstr) -> A(fct at,tg,cstr) - | C (f1,f2) -> C(map_atoms fct f1, map_atoms fct f2) - | D (f1,f2) -> D(map_atoms fct f1, map_atoms fct f2) - | N f -> N(map_atoms fct f) - | I(f1,o,f2) -> I(map_atoms fct f1, o , map_atoms fct f2) - -let rec map_prop fct f = - match f with - | TT -> TT - | FF -> FF - | X x -> X (fct x) - | A (at,tg,cstr) -> A(at,tg,cstr) - | C (f1,f2) -> C(map_prop fct f1, map_prop fct f2) - | D (f1,f2) -> D(map_prop fct f1, map_prop fct f2) - | N f -> N(map_prop fct f) - | I(f1,o,f2) -> I(map_prop fct f1, o , map_prop fct f2) - -(** - * 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) - | _ -> [] - -(** - * 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. - *) - -module Mc = Micromega - -type 'cst mc_cnf = ('cst Mc.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). - *) - -type 'a tagged_option = T of tag list | S of 'a - -let cnf - (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) - (unsat : 'cst Mc.nFormula -> bool) (deduce : 'cst Mc.nFormula -> 'cst Mc.nFormula -> 'cst Mc.nFormula option) (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 - - let and_cnf x y = x @ y in - -let rec add_term t0 = function - | [] -> - (match deduce (fst t0) (fst t0) with - | Some u -> if unsat u then T [snd t0] else S (t0::[]) - | None -> S (t0::[])) - | t'::cl0 -> - (match deduce (fst t0) (fst t') with - | Some u -> - if unsat u - then T [snd t0 ; snd t'] - else (match add_term t0 cl0 with - | S cl' -> S (t'::cl') - | T l -> T l) - | None -> - (match add_term t0 cl0 with - | S cl' -> S (t'::cl') - | T l -> T l)) in - - - let rec or_clause cl1 cl2 = - match cl1 with - | [] -> S cl2 - | t0::cl -> - (match add_term t0 cl2 with - | S cl' -> or_clause cl cl' - | T l -> T l) in - - - - let or_clause_cnf t f = - List.fold_right (fun e (acc,tg) -> - match or_clause t e with - | S cl -> (cl :: acc,tg) - | T l -> (acc,tg@l)) f ([],[]) in - - - let rec or_cnf f f' = - match f with - | [] -> tt,[] - | e :: rst -> - let (rst_f',t) = or_cnf rst f' in - let (e_f', t') = or_clause_cnf e f' in - (rst_f' @ e_f', t @ t') in - - - let rec xcnf (polarity : bool) f = - match f with - | 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) -> - let e1,t1 = xcnf polarity e1 in - let e2,t2 = xcnf polarity e2 in - if polarity - then and_cnf e1 e2, t1 @ t2 - else let f',t' = or_cnf e1 e2 in - (f', t1 @ t2 @ t') - | D(e1,e2) -> - let e1,t1 = xcnf polarity e1 in - let e2,t2 = xcnf polarity e2 in - if polarity - then let f',t' = or_cnf e1 e2 in - (f', t1 @ t2 @ t') - else and_cnf e1 e2, t1 @ t2 - | I(e1,_,e2) -> - let e1 , t1 = (xcnf (not polarity) e1) in - let e2 , t2 = (xcnf polarity e2) in - if polarity - then let f',t' = or_cnf e1 e2 in - (f', t1 @ t2 @ t') - else and_cnf e1 e2, t1 @ t2 in - - xcnf true f - -(** - * MODULE: Ordered set of integers. - *) - -module ISet = Set.Make(Int) - -(** - * 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 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. - *) - -module M = -struct - - (** - * Location of the Coq libraries. - *) - - let logic_dir = ["Coq";"Logic";"Decidable"] - - let mic_modules = - [ - ["Coq";"Lists";"List"]; - ["ZMicromega"]; - ["Tauto"]; - ["RingMicromega"]; - ["EnvRing"]; - ["Coq"; "micromega"; "ZMicromega"]; - ["Coq"; "micromega"; "RMicromega"]; - ["Coq" ; "micromega" ; "Tauto"]; - ["Coq" ; "micromega" ; "RingMicromega"]; - ["Coq" ; "micromega" ; "EnvRing"]; - ["Coq";"QArith"; "QArith_base"]; - ["Coq";"Reals" ; "Rdefinitions"]; - ["Coq";"Reals" ; "Rpow_def"]; - ["LRing_normalise"]] - - let coq_modules = - Coqlib.(init_modules @ - [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules) - - let bin_module = [["Coq";"Numbers";"BinNums"]] - - let r_modules = - [["Coq";"Reals" ; "Rdefinitions"]; - ["Coq";"Reals" ; "Rpow_def"] ; - ["Coq";"Reals" ; "Raxioms"] ; - ["Coq";"QArith"; "Qreals"] ; - ] - - let z_modules = [["Coq";"ZArith";"BinInt"]] - - (** - * Initialization : a large amount of Caml symbols are derived from - * ZMicromega.v - *) - - let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n) - let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules - let constant = gen_constant_in_modules "ZMicromega" coq_modules - let bin_constant = gen_constant_in_modules "ZMicromega" bin_module - let r_constant = gen_constant_in_modules "ZMicromega" r_modules - let z_constant = gen_constant_in_modules "ZMicromega" z_modules - let m_constant = gen_constant_in_modules "ZMicromega" mic_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_N0 = lazy (bin_constant "N0") - let coq_Npos = lazy (bin_constant "Npos") - - let coq_xH = lazy (bin_constant "xH") - let coq_xO = lazy (bin_constant "xO") - let coq_xI = lazy (bin_constant "xI") - - let coq_Z = lazy (bin_constant "Z") - let coq_ZERO = lazy (bin_constant "Z0") - let coq_POS = lazy (bin_constant "Zpos") - let coq_NEG = lazy (bin_constant "Zneg") - - let coq_Q = lazy (constant "Q") - let coq_R = lazy (constant "R") - - let coq_Qmake = lazy (constant "Qmake") - - let coq_Rcst = lazy (constant "Rcst") - - let coq_C0 = lazy (m_constant "C0") - let coq_C1 = lazy (m_constant "C1") - let coq_CQ = lazy (m_constant "CQ") - let coq_CZ = lazy (m_constant "CZ") - let coq_CPlus = lazy (m_constant "CPlus") - let coq_CMinus = lazy (m_constant "CMinus") - let coq_CMult = lazy (m_constant "CMult") - let coq_CInv = lazy (m_constant "CInv") - let coq_COpp = lazy (m_constant "COpp") - - - 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 (z_constant "Z.gt") - let coq_Zge = lazy (z_constant "Z.ge") - let coq_Zle = lazy (z_constant "Z.le") - let coq_Zlt = lazy (z_constant "Z.lt") - let coq_Eq = lazy (init_constant "eq") - - let coq_Zplus = lazy (z_constant "Z.add") - let coq_Zminus = lazy (z_constant "Z.sub") - let coq_Zopp = lazy (z_constant "Z.opp") - let coq_Zmult = lazy (z_constant "Z.mul") - let coq_Zpower = lazy (z_constant "Z.pow") - - 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 (r_constant "Rgt") - let coq_Rge = lazy (r_constant "Rge") - let coq_Rle = lazy (r_constant "Rle") - let coq_Rlt = lazy (r_constant "Rlt") - - let coq_Rplus = lazy (r_constant "Rplus") - let coq_Rminus = lazy (r_constant "Rminus") - let coq_Ropp = lazy (r_constant "Ropp") - let coq_Rmult = lazy (r_constant "Rmult") - let coq_Rinv = lazy (r_constant "Rinv") - let coq_Rpower = lazy (r_constant "pow") - let coq_IZR = lazy (r_constant "IZR") - let coq_IQR = lazy (r_constant "Q2R") - - - 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_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_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. - *) - - exception ParseError - - (* A simple but useful getter function *) - - let get_left_construct sigma term = - match EConstr.kind sigma term with - | Construct((_,i),_) -> (i,[| |]) - | App(l,rst) -> - (match EConstr.kind sigma l with - | Construct((_,i),_) -> (i,rst) - | _ -> raise ParseError - ) - | _ -> raise ParseError - - (* Access the Micromega module *) - - (* parse/dump/print from numbers up to expressions and formulas *) - - let rec parse_nat sigma term = - let (i,c) = get_left_construct sigma term in - match i with - | 1 -> Mc.O - | 2 -> Mc.S (parse_nat sigma (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 -> EConstr.mkApp(Lazy.force coq_S,[| dump_nat p |]) - - let rec parse_positive sigma term = - let (i,c) = get_left_construct sigma term in - match i with - | 1 -> Mc.XI (parse_positive sigma c.(0)) - | 2 -> Mc.XO (parse_positive sigma 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 -> EConstr.mkApp(Lazy.force coq_xO,[| dump_positive p |]) - | Mc.XI p -> EConstr.mkApp(Lazy.force coq_xI,[| dump_positive p |]) - - let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) - - let dump_n x = - match x with - | Mc.N0 -> Lazy.force coq_N0 - | Mc.Npos p -> EConstr.mkApp(Lazy.force coq_Npos,[| dump_positive p|]) - - let parse_z sigma term = - let (i,c) = get_left_construct sigma term in - match i with - | 1 -> Mc.Z0 - | 2 -> Mc.Zpos (parse_positive sigma c.(0)) - | 3 -> Mc.Zneg (parse_positive sigma c.(0)) - | i -> raise ParseError - - let dump_z x = - match x with - | Mc.Z0 ->Lazy.force coq_ZERO - | Mc.Zpos p -> EConstr.mkApp(Lazy.force coq_POS,[| dump_positive p|]) - | Mc.Zneg p -> EConstr.mkApp(Lazy.force coq_NEG,[| dump_positive p|]) - - let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (CoqToCaml.z_big_int x)) - - let dump_q q = - EConstr.mkApp(Lazy.force coq_Qmake, - [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|]) - - let parse_q sigma term = - match EConstr.kind sigma term with - | App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then - {Mc.qnum = parse_z sigma args.(0) ; Mc.qden = parse_positive sigma args.(1) } - else raise ParseError - | _ -> raise ParseError - - - let rec pp_Rcst o cst = - match cst with - | Mc.C0 -> output_string o "C0" - | Mc.C1 -> output_string o "C1" - | Mc.CQ q -> output_string o "CQ _" - | Mc.CZ z -> pp_z o z - | Mc.CPlus(x,y) -> Printf.fprintf o "(%a + %a)" pp_Rcst x pp_Rcst y - | Mc.CMinus(x,y) -> Printf.fprintf o "(%a - %a)" pp_Rcst x pp_Rcst y - | Mc.CMult(x,y) -> Printf.fprintf o "(%a * %a)" pp_Rcst x pp_Rcst y - | Mc.CInv t -> Printf.fprintf o "(/ %a)" pp_Rcst t - | Mc.COpp t -> Printf.fprintf o "(- %a)" pp_Rcst t - - - let rec dump_Rcst cst = - match cst with - | Mc.C0 -> Lazy.force coq_C0 - | Mc.C1 -> Lazy.force coq_C1 - | Mc.CQ q -> EConstr.mkApp(Lazy.force coq_CQ, [| dump_q q |]) - | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_CZ, [| dump_z z |]) - | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |]) - | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |]) - - let rec dump_list typ dump_elt l = - match l with - | [] -> EConstr.mkApp(Lazy.force coq_nil,[| typ |]) - | e :: l -> EConstr.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 dump_var = dump_positive - - let dump_expr typ dump_z e = - let rec dump_expr e = - match e with - | Mc.PEX n -> EConstr.mkApp(Lazy.force coq_PEX,[| typ; dump_var n |]) - | Mc.PEc z -> EConstr.mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |]) - | Mc.PEadd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEadd, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEsub(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEsub, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEopp e -> EConstr.mkApp(Lazy.force coq_PEopp, - [| typ; dump_expr e|]) - | Mc.PEmul(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEmul, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEpow(e,n) -> EConstr.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 -> EConstr.mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|]) - | Mc.Pinj(p,pol) -> EConstr.mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|]) - | Mc.PX(pol1,p,pol2) -> EConstr.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 -> EConstr.mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |]) - | Mc.PsatzMulC(e,c) -> EConstr.mkApp(Lazy.force coq_PsatzMultC, - [| z; dump_pol z dump_z e ; dump_cone c |]) - | Mc.PsatzSquare e -> EConstr.mkApp(Lazy.force coq_PsatzSquare, - [| z;dump_pol z dump_z e|]) - | Mc.PsatzAdd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzAdd, - [| z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzMulE(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzMulE, - [| z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzC p -> EConstr.mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|]) - | Mc.PsatzZ -> EConstr.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 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 dump_cstr typ dump_constant {Mc.flhs = e1 ; Mc.fop = o ; Mc.frhs = e2} = - EConstr.mkApp(Lazy.force coq_Build, - [| typ; dump_expr typ dump_constant e1 ; - dump_op o ; - dump_expr typ dump_constant e2|]) - - let assoc_const sigma x l = - try - snd (List.find (fun (x',y) -> EConstr.eq_constr sigma 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 - ] - - type gl = { env : Environ.env; sigma : Evd.evar_map } - - let is_convertible gl t1 t2 = - Reductionops.is_conv gl.env gl.sigma t1 t2 - - let parse_zop gl (op,args) = - let sigma = gl.sigma in - match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> - if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z) - then (Mc.OpEq, args.(1), args.(2)) - else raise ParseError - | _ -> failwith "parse_zop" - - let parse_rop gl (op,args) = - let sigma = gl.sigma in - match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> - if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R) - then (Mc.OpEq, args.(1), args.(2)) - else raise ParseError - | _ -> failwith "parse_zop" - - let parse_qop gl (op,args) = - (assoc_const gl.sigma op qop_table, args.(0) , args.(1)) - - type 'a op = - | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) - | Opp - | Power - | Ukn of string - - let assoc_ops sigma x l = - try - snd (List.find (fun (x',y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) - with - Not_found -> Ukn "Oups" - - (** - * MODULE: Env is for environment. - *) - - module Env = - struct - let compute_rank_add env sigma v = - let rec _add env n v = - match env with - | [] -> ([v],n) - | e::l -> - if EConstr.eq_constr sigma 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.positive n) - - let get_rank env sigma v = - - let rec _get_rank env n = - match env with - | [] -> raise (Invalid_argument "get_rank") - | e::l -> - if EConstr.eq_constr sigma e v - then n - else _get_rank l (n+1) in - _get_rank env 1 - - - let empty = [] - - let elements env = env - - end (* MODULE END: Env *) - - (** - * This is the big generic function for expression parsers. - *) - - let parse_expr sigma parse_constant parse_exp ops_spec env term = - if debug - then ( - let _, env = Pfedit.get_current_context () in - Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term)); - -(* - 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 parse_variable env term = - let (env,n) = Env.compute_rank_add env sigma 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 - - try (Mc.PEc (parse_constant term) , env) - with ParseError -> - match EConstr.kind sigma term with - | App(t,args) -> - ( - match EConstr.kind sigma t with - | Const c -> - ( match assoc_ops sigma 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 e when CErrors.noncritical e -> - (* if the exponent is a variable *) - let (env,n) = Env.compute_rank_add env sigma 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 sigma term in (Mc.PEX n, env) - ) - | _ -> parse_variable env term - ) - | _ -> parse_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_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 - - - let rconst_assoc = - [ - coq_Rplus , (fun x y -> Mc.CPlus(x,y)) ; - coq_Rminus , (fun x y -> Mc.CMinus(x,y)) ; - coq_Rmult , (fun x y -> Mc.CMult(x,y)) ; - (* coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*) - ] - - let rec rconstant sigma term = - match EConstr.kind sigma term with - | Const x -> - if EConstr.eq_constr sigma term (Lazy.force coq_R0) - then Mc.C0 - else if EConstr.eq_constr sigma term (Lazy.force coq_R1) - then Mc.C1 - else raise ParseError - | App(op,args) -> - begin - try - (* the evaluation order is important in the following *) - let f = assoc_const sigma op rconst_assoc in - let a = rconstant sigma args.(0) in - let b = rconstant sigma args.(1) in - f a b - with - ParseError -> - match op with - | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> - let arg = rconstant sigma args.(0) in - if Mc.qeq_bool (Mc.q_of_Rcst arg) {Mc.qnum = Mc.Z0 ; Mc.qden = Mc.XH} - then raise ParseError (* This is a division by zero -- no semantics *) - else Mc.CInv(arg) - | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> Mc.CQ (parse_q sigma args.(0)) - | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> Mc.CZ (parse_z sigma args.(0)) - | _ -> raise ParseError - end - - | _ -> raise ParseError - - - let rconstant sigma term = - let _, env = Pfedit.get_current_context () in - if debug - then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); - let res = rconstant sigma term in - if debug then - (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; - res - - - let parse_zexpr sigma = parse_expr sigma - (zconstant sigma) - (fun expr x -> - let exp = (parse_z sigma x) in - match exp with - | Mc.Zneg _ -> Mc.PEc Mc.Z0 - | _ -> Mc.PEpow(expr, Mc.Z.to_N exp)) - zop_spec - - let parse_qexpr sigma = parse_expr sigma - (qconstant sigma) - (fun expr x -> - let exp = parse_z sigma 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.Z.to_N exp in - Mc.PEpow(expr,exp)) - qop_spec - - let parse_rexpr sigma = parse_expr sigma - (rconstant sigma) - (fun expr x -> - let exp = Mc.N.of_nat (parse_nat sigma x) in - Mc.PEpow(expr,exp)) - rop_spec - - let parse_arith parse_op parse_expr env cstr gl = - let sigma = gl.sigma in - if debug - then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ()); - match EConstr.kind sigma cstr with - | App(op,args) -> - let (op,lhs,rhs) = parse_op gl (op,args) in - let (e1,env) = parse_expr sigma env lhs in - let (e2,env) = parse_expr sigma 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 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 gl parse_atom env tg term = - let sigma = gl.sigma in - - let parse_atom env tg t = - try - let (at,env) = parse_atom env t gl in - (A(at,tg,t), env,Tag.next tg) - with e when CErrors.noncritical e -> (X(t),env,tg) in - - let is_prop term = - let sort = Retyping.get_sort_of gl.env gl.sigma term in - Sorts.is_prop sort in - - let rec xparse_formula env tg term = - match EConstr.kind sigma term with - | App(l,rst) -> - (match rst with - | [|a;b|] when EConstr.eq_constr sigma 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 EConstr.eq_constr sigma 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 EConstr.eq_constr sigma l (Lazy.force coq_not) -> - let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg) - | [|a;b|] when EConstr.eq_constr sigma 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 EConstr.Vars.noccurn sigma 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 EConstr.eq_constr sigma term (Lazy.force coq_True) -> (TT,env,tg) - | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> (FF,env,tg) - | _ when is_prop term -> X(term),env,tg - | _ -> raise ParseError - in - xparse_formula env tg ((*Reductionops.whd_zeta*) term) - - let dump_formula typ dump_atom f = - let rec xdump f = - match f with - | TT -> EConstr.mkApp(Lazy.force coq_TT,[|typ|]) - | FF -> EConstr.mkApp(Lazy.force coq_FF,[|typ|]) - | C(x,y) -> EConstr.mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|]) - | D(x,y) -> EConstr.mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|]) - | I(x,_,y) -> EConstr.mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|]) - | N(x) -> EConstr.mkApp(Lazy.force coq_Neg,[|typ ; xdump x|]) - | A(x,_,_) -> EConstr.mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|]) - | X(t) -> EConstr.mkApp(Lazy.force coq_X,[|typ ; t|]) in - xdump f - - - let prop_env_of_formula sigma form = - let rec doit env = function - | TT | FF | A(_,_,_) -> env - | X t -> fst (Env.compute_rank_add env sigma t) - | C(f1,f2) | D(f1,f2) | I(f1,_,f2) -> - doit (doit env f1) f2 - | N f -> doit env f in - - doit [] form - - let var_env_of_formula form = - - let rec vars_of_expr = function - | Mc.PEX n -> ISet.singleton (CoqToCaml.positive n) - | Mc.PEc z -> ISet.empty - | Mc.PEadd(e1,e2) | Mc.PEmul(e1,e2) | Mc.PEsub(e1,e2) -> - ISet.union (vars_of_expr e1) (vars_of_expr e2) - | Mc.PEopp e | Mc.PEpow(e,_)-> vars_of_expr e - in - - let vars_of_atom {Mc.flhs ; Mc.fop; Mc.frhs} = - ISet.union (vars_of_expr flhs) (vars_of_expr frhs) in - - let rec doit = function - | TT | FF | X _ -> ISet.empty - | A (a,t,c) -> vars_of_atom a - | C(f1,f2) | D(f1,f2) |I (f1,_,f2) -> ISet.union (doit f1) (doit f2) - | N f -> doit f in - - doit form - - - - - type 'cst dump_expr = (* 'cst is the type of the syntactic constants *) - { - interp_typ : EConstr.constr; - dump_cst : 'cst -> EConstr.constr; - dump_add : EConstr.constr; - dump_sub : EConstr.constr; - dump_opp : EConstr.constr; - dump_mul : EConstr.constr; - dump_pow : EConstr.constr; - dump_pow_arg : Mc.n -> EConstr.constr; - dump_op : (Mc.op2 * EConstr.constr) list - } - -let dump_zexpr = lazy - { - interp_typ = Lazy.force coq_Z; - dump_cst = dump_z; - dump_add = Lazy.force coq_Zplus; - dump_sub = Lazy.force coq_Zminus; - dump_opp = Lazy.force coq_Zopp; - dump_mul = Lazy.force coq_Zmult; - dump_pow = Lazy.force coq_Zpower; - dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))); - dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) zop_table - } - -let dump_qexpr = lazy - { - interp_typ = Lazy.force coq_Q; - dump_cst = dump_q; - dump_add = Lazy.force coq_Qplus; - dump_sub = Lazy.force coq_Qminus; - dump_opp = Lazy.force coq_Qopp; - dump_mul = Lazy.force coq_Qmult; - dump_pow = Lazy.force coq_Qpower; - dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))); - dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) qop_table - } - -let rec dump_Rcst_as_R cst = - match cst with - | Mc.C0 -> Lazy.force coq_R0 - | Mc.C1 -> Lazy.force coq_R1 - | Mc.CQ q -> EConstr.mkApp(Lazy.force coq_IQR, [| dump_q q |]) - | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_IZR, [| dump_z z |]) - | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |]) - | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |]) - - -let dump_rexpr = lazy - { - interp_typ = Lazy.force coq_R; - dump_cst = dump_Rcst_as_R; - dump_add = Lazy.force coq_Rplus; - dump_sub = Lazy.force coq_Rminus; - dump_opp = Lazy.force coq_Ropp; - dump_mul = Lazy.force coq_Rmult; - dump_pow = Lazy.force coq_Rpower; - dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n))); - dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) rop_table - } - - - - -(** [make_goal_of_formula depxr vars props form] where - - vars is an environment for the arithmetic variables occuring in form - - props is an environment for the propositions occuring in form - @return a goal where all the variables and propositions of the formula are quantified - -*) - -let prodn n env b = - let rec prodrec = function - | (0, env, b) -> b - | (n, ((v,t)::l), b) -> prodrec (n-1, l, EConstr.mkProd (v,t,b)) - | _ -> assert false - in - prodrec (n,env,b) - -let make_goal_of_formula sigma dexpr form = - - let vars_idx = - List.mapi (fun i v -> (v, i+1)) (ISet.elements (var_env_of_formula form)) in - - (* List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*) - - let props = prop_env_of_formula sigma form in - - let vars_n = List.map (fun (_,i) -> (Names.Id.of_string (Printf.sprintf "__x%i" i)) , dexpr.interp_typ) vars_idx in - let props_n = List.mapi (fun i _ -> (Names.Id.of_string (Printf.sprintf "__p%i" (i+1))) , EConstr.mkProp) props in - - let var_name_pos = List.map2 (fun (idx,_) (id,_) -> id,idx) vars_idx vars_n in - - let dump_expr i e = - let rec dump_expr = function - | Mc.PEX n -> EConstr.mkRel (i+(List.assoc (CoqToCaml.positive n) vars_idx)) - | Mc.PEc z -> dexpr.dump_cst z - | Mc.PEadd(e1,e2) -> EConstr.mkApp(dexpr.dump_add, - [| dump_expr e1;dump_expr e2|]) - | Mc.PEsub(e1,e2) -> EConstr.mkApp(dexpr.dump_sub, - [| dump_expr e1;dump_expr e2|]) - | Mc.PEopp e -> EConstr.mkApp(dexpr.dump_opp, - [| dump_expr e|]) - | Mc.PEmul(e1,e2) -> EConstr.mkApp(dexpr.dump_mul, - [| dump_expr e1;dump_expr e2|]) - | Mc.PEpow(e,n) -> EConstr.mkApp(dexpr.dump_pow, - [| dump_expr e; dexpr.dump_pow_arg n|]) - in dump_expr e in - - let mkop op e1 e2 = - try - EConstr.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|]) - with Not_found -> - EConstr.mkApp(Lazy.force coq_Eq,[|dexpr.interp_typ ; e1 ;e2|]) in - - let dump_cstr i { Mc.flhs ; Mc.fop ; Mc.frhs } = - mkop fop (dump_expr i flhs) (dump_expr i frhs) in - - let rec xdump pi xi f = - match f with - | TT -> Lazy.force coq_True - | FF -> Lazy.force coq_False - | C(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) - | D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) - | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y) - | N(x) -> EConstr.mkArrow (xdump pi xi x) (Lazy.force coq_False) - | A(x,_,_) -> dump_cstr xi x - | X(t) -> let idx = Env.get_rank props sigma t in - EConstr.mkRel (pi+idx) in - - let nb_vars = List.length vars_n in - let nb_props = List.length props_n in - - (* Printf.fprintf stdout "NBProps : %i\n" nb_props ;*) - - let subst_prop p = - let idx = Env.get_rank props sigma p in - EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) in - - let form' = map_prop subst_prop form in - - (prodn nb_props (List.map (fun (x,y) -> Name.Name x,y) props_n) - (prodn nb_vars (List.map (fun (x,y) -> Name.Name x,y) vars_n) - (xdump (List.length vars_n) 0 form)), - List.rev props_n, List.rev var_name_pos,form') - - (** - * 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 (EConstr.mkNamedLetIn - (Names.Id.of_string name) - expr typ acc) l in - xset concl l - -end (** - * MODULE END: M - *) - -open M - -let coq_Node = - lazy (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node") -let coq_Leaf = - lazy (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf") -let coq_Empty = - lazy (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty") - -let coq_VarMap = - lazy (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t") - - -let rec dump_varmap typ m = - match m with - | Mc.Empty -> EConstr.mkApp(Lazy.force coq_Empty,[| typ |]) - | Mc.Leaf v -> EConstr.mkApp(Lazy.force coq_Leaf,[| typ; v|]) - | Mc.Node(l,o,r) -> - EConstr.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) - - -let vm_of_list env = - match env with - | [] -> Mc.Empty - | (d,_)::_ -> - List.fold_left (fun vm (c,i) -> - Mc.vm_add d (CamlToCoq.positive i) c vm) Mc.Empty env - -let rec dump_proof_term = function - | Micromega.DoneProof -> Lazy.force coq_doneProof - | Micromega.RatProof(cone,rst) -> - EConstr.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|]) - | Micromega.CutProof(cone,prf) -> - EConstr.mkApp(Lazy.force coq_cutProof, - [| dump_psatz coq_Z dump_z cone ; - dump_proof_term prf|]) - | Micromega.EnumProof(c1,c2,prfs) -> - EConstr.mkApp (Lazy.force coq_enumProof, - [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; - dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |]) - - -let rec size_of_psatz = function - | Micromega.PsatzIn _ -> 1 - | Micromega.PsatzSquare _ -> 1 - | Micromega.PsatzMulC(_,p) -> 1 + (size_of_psatz p) - | Micromega.PsatzMulE(p1,p2) | Micromega.PsatzAdd(p1,p2) -> size_of_psatz p1 + size_of_psatz p2 - | Micromega.PsatzC _ -> 1 - | Micromega.PsatzZ -> 1 - -let rec size_of_pf = function - | Micromega.DoneProof -> 1 - | Micromega.RatProof(p,a) -> (size_of_pf a) + (size_of_psatz p) - | Micromega.CutProof(p,a) -> (size_of_pf a) + (size_of_psatz p) - | Micromega.EnumProof(p1,p2,l) -> (size_of_psatz p1) + (size_of_psatz p2) + (List.fold_left (fun acc p -> size_of_pf p + acc) 0 l) - -let dump_proof_term t = - if debug then Printf.printf "dump_proof_term %i\n" (size_of_pf t) ; - dump_proof_term t - - - -let pp_q o q = Printf.fprintf o "%a/%a" pp_z q.Micromega.qnum pp_positive q.Micromega.qden - - -let rec pp_proof_term o = function - | Micromega.DoneProof -> Printf.fprintf o "D" - | Micromega.RatProof(cone,rst) -> Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst - | Micromega.CutProof(cone,rst) -> Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst - | Micromega.EnumProof(c1,c2,rst) -> - Printf.fprintf o "EP[%a,%a,%a]" - (pp_psatz pp_z) c1 (pp_psatz pp_z) c2 - (pp_list "[" "]" pp_proof_term) rst - -let rec parse_hyps gl parse_arith env tg hyps = - match hyps with - | [] -> ([],env,tg) - | (i,t)::l -> - let (lhyps,env,tg) = parse_hyps gl parse_arith env tg l in - try - let (c,env,tg) = parse_formula gl parse_arith env tg t in - ((i,c)::lhyps, env,tg) - with e when CErrors.noncritical e -> (lhyps,env,tg) - (*(if debug then Printf.printf "parse_arith : %s\n" x);*) - - -(*exception ParseError*) - -let parse_goal gl parse_arith env hyps term = - (* try*) - let (f,env,tg) = parse_formula gl parse_arith env (Tag.from 0) term in - let (lhyps,env,tg) = parse_hyps gl parse_arith env tg hyps in - (lhyps,f,env) - (* with Failure x -> raise ParseError*) - -(** - * The datastructures that aggregate theory-dependent proof values. - *) -type ('synt_c, 'prf) domain_spec = { - typ : EConstr.constr; (* is the type of the interpretation domain - Z, Q, R*) - coeff : EConstr.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *) - dump_coeff : 'synt_c -> EConstr.constr ; - proof_typ : EConstr.constr ; - dump_proof : 'prf -> EConstr.constr -} - -let zz_domain_spec = lazy { - typ = Lazy.force coq_Z; - coeff = Lazy.force coq_Z; - dump_coeff = dump_z ; - proof_typ = Lazy.force coq_proofTerm ; - dump_proof = dump_proof_term -} - -let qq_domain_spec = lazy { - typ = Lazy.force coq_Q; - coeff = Lazy.force coq_Q; - dump_coeff = dump_q ; - proof_typ = Lazy.force coq_QWitness ; - dump_proof = dump_psatz coq_Q dump_q -} - -(** Naive topological sort of constr according to the subterm-ordering *) - -(* An element is minimal x is minimal w.r.t y if - x <= y or (x and y are incomparable) *) - -(** - * Instanciate the current Coq goal with a Micromega formula, a varmap, and a - * witness. - *) - -let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*) = - (* let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *) - let formula_typ = (EConstr.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) (vm_of_list env) in - (* todo : directly generate the proof term - or generalize before conversion? *) - Proofview.Goal.nf_enter begin fun gl -> - Tacticals.New.tclTHENLIST - [ - Tactics.change_concl - (set - [ - ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, EConstr.mkApp(Lazy.force coq_VarMap, [|spec.typ|])); - ("__wit", cert, cert_typ) - ] - (Tacmach.New.pf_concl gl)) - ] - end - - -(** - * The datastructures that aggregate prover attributes. - *) - -type ('option,'a,'prf) prover = { - name : string ; (* name of the prover *) - get_option : unit ->'option ; (* find the options of the prover *) - prover : 'option * '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 (* pretty printing of the formulas (polynomials)*) -} - - - -(** - * 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 (p.get_option (),l) with - | None -> None - | Some prf -> Some(prf,p)) , p.name) provers in - 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 = - match l with - | [] -> Some [] - | e :: l -> - match find_witness prover e with - | None -> None - | Some w -> - (match xwitness_list l with - | None -> None - | Some l -> Some (w :: l) - ) in - xwitness_list l - -let witness_list_tags = witness_list - -(** - * 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 = List.mapi (fun i (f,_) -> (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 when CErrors.noncritical 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 (prover.get_option () ,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 - let hyps = selecti hyps_idx old_cl in - is_sublist Pervasives.(=) hyps new_cl in - - 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' - - -(** - * "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 (EConstr.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 (EConstr.mkApp(Lazy.force coq_or, [|a1;a2|])) - | f1 , f2 -> D(f1,f2) ) - | N(f) -> - (match xabs f with - | X a -> X (EConstr.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 (EConstr.mkArrow a1 a2) - | af1 , _ , af2 -> I(af1,hyp,af2) - ) - | FF -> FF - | TT -> TT - in xabs f - - -(* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2 *) -let rec abstract_wrt_formula f1 f2 = - match f1 , f2 with - | X c , _ -> X c - | A _ , A _ -> f2 - | C(a,b) , C(a',b') -> C(abstract_wrt_formula a a', abstract_wrt_formula b b') - | D(a,b) , D(a',b') -> D(abstract_wrt_formula a a', abstract_wrt_formula b b') - | I(a,_,b) , I(a',x,b') -> I(abstract_wrt_formula a a',x, abstract_wrt_formula b b') - | FF , FF -> FF - | TT , TT -> TT - | N x , N y -> N(abstract_wrt_formula x y) - | _ -> failwith "abstract_wrt_formula" - -(** - * This exception is raised by really_call_csdpcert if Coq's configure didn't - * find a CSDP executable. - *) - -exception CsdpNotFound - - -(** - * This is the core of Micromega: apply the prover, analyze the result and - * prune unused fomulas, and finally modify the proof state. - *) - -let formula_hyps_concl hyps concl = - List.fold_right - (fun (id,f) (cc,ids) -> - match f with - X _ -> (cc,ids) - | _ -> (I(f,Some id,cc), id::ids)) - hyps (concl,[]) - - -let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 gl = - - (* Express the goal as one big implication *) - let (ff,ids) = formula_hyps_concl polys1 polys2 in - - (* Convert the aplpication into a (mc_)cnf (a list of lists of formulas) *) - let cnf_ff,cnf_ff_tags = cnf negate normalise unsat deduce ff in - - if debug then - begin - Feedback.msg_notice (Pp.str "Formula....\n") ; - let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in - let ff = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff in - Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff - end; - - match witness_list_tags prover cnf_ff with - | None -> None - | 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) (List.fold_left (fun s i -> TagSet.add i s) TagSet.empty cnf_ff_tags) (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 unsat deduce ff' in - - if debug then - begin - Feedback.msg_notice (Pp.str "\nAFormula\n") ; - let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in - let ff' = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff' in - Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff'); - 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', ids_of_formula ff') in - - let res' = dump_list (spec.proof_typ) spec.dump_proof res' in - Some (ids,ff',res') - - -(** - * Parse the proof environment, and call micromega_tauto - *) - -let fresh_id avoid id gl = - Tactics.fresh_id_in_env avoid id (Proofview.Goal.env gl) - -let micromega_gen - parse_arith - (negate:'cst atom -> 'cst mc_cnf) - (normalise:'cst atom -> 'cst mc_cnf) - unsat deduce - spec dumpexpr prover tac = - Proofview.Goal.nf_enter begin fun gl -> - let sigma = Tacmach.New.project gl in - let concl = Tacmach.New.pf_concl gl in - let hyps = Tacmach.New.pf_hyps_types gl in - try - let gl0 = { env = Tacmach.New.pf_env gl; sigma } in - let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in - let env = Env.elements env in - let spec = Lazy.force spec in - let dumpexpr = Lazy.force dumpexpr in - - match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl0 with - | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") - | Some (ids,ff',res') -> - let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma dumpexpr ff' in - let intro (id,_) = Tactics.introduction id in - - let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in - let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in - let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in - let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in - - let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; - micromega_order_change spec res' - (EConstr.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in - - let goal_props = List.rev (prop_env_of_formula sigma ff') in - - let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in - - let arith_args = goal_props @ goal_vars in - - let kill_arith = - Tacticals.New.tclTHEN - (Tactics.keep []) - ((*Tactics.tclABSTRACT None*) - (Tacticals.New.tclTHEN tac_arith tac)) in - - Tacticals.New.tclTHENS - (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal) - [ - kill_arith; - (Tacticals.New.tclTHENLIST - [(Tactics.generalize (List.map EConstr.mkVar ids)); - Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args)) - ] ) - ] - with - | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") - | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") - | CsdpNotFound -> flush stdout ; - Tacticals.New.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 Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" - ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) - end - -let micromega_gen parse_arith - (negate:'cst atom -> 'cst mc_cnf) - (normalise:'cst atom -> 'cst mc_cnf) - unsat deduce - spec prover = - (micromega_gen parse_arith negate normalise unsat deduce spec prover) - - - -let micromega_order_changer cert env ff = - (*let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *) - let coeff = Lazy.force coq_Rcst in - let dump_coeff = dump_Rcst in - let typ = Lazy.force coq_R in - let cert_typ = (EConstr.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in - - let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in - let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in - let vm = dump_varmap (typ) (vm_of_list env) in - Proofview.Goal.nf_enter begin fun gl -> - Tacticals.New.tclTHENLIST - [ - (Tactics.change_concl - (set - [ - ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, EConstr.mkApp - (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); - ("__wit", cert, cert_typ) - ] - (Tacmach.New.pf_concl gl))); - (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) - ] - end - -let micromega_genr prover tac = - let parse_arith = parse_rarith in - let negate = Mc.rnegate in - let normalise = Mc.rnormalise in - let unsat = Mc.runsat in - let deduce = Mc.rdeduce in - let spec = lazy { - typ = Lazy.force coq_R; - coeff = Lazy.force coq_Rcst; - dump_coeff = dump_q; - proof_typ = Lazy.force coq_QWitness ; - dump_proof = dump_psatz coq_Q dump_q - } in - Proofview.Goal.nf_enter begin fun gl -> - let sigma = Tacmach.New.project gl in - let concl = Tacmach.New.pf_concl gl in - let hyps = Tacmach.New.pf_hyps_types gl in - - try - let gl0 = { env = Tacmach.New.pf_env gl; sigma } in - let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in - let env = Env.elements env in - let spec = Lazy.force spec in - - let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in - let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in - - match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl0 with - | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") - | Some (ids,ff',res') -> - let (ff,ids) = formula_hyps_concl - (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in - let ff' = abstract_wrt_formula ff' ff in - - let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma (Lazy.force dump_rexpr) ff' in - let intro (id,_) = Tactics.introduction id in - - let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in - let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in - let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in - let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in - - let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; - micromega_order_changer res' env' ff_arith ] in - - let goal_props = List.rev (prop_env_of_formula sigma ff') in - - let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in - - let arith_args = goal_props @ goal_vars in - - let kill_arith = - Tacticals.New.tclTHEN - (Tactics.keep []) - ((*Tactics.tclABSTRACT None*) - (Tacticals.New.tclTHEN tac_arith tac)) in - - Tacticals.New.tclTHENS - (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal) - [ - kill_arith; - (Tacticals.New.tclTHENLIST - [(Tactics.generalize (List.map EConstr.mkVar ids)); - Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args)) - ] ) - ] - - with - | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") - | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") - | CsdpNotFound -> flush stdout ; - Tacticals.New.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 Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" - ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) - end - - - - -let micromega_genr prover = (micromega_genr prover) - - -let lift_ratproof prover l = - match prover l with - | None -> None - | Some c -> Some (Mc.RatProof( c,Mc.DoneProof)) - -type micromega_polys = (Micromega.q Mc.pol * Mc.op1) list - -[@@@ocaml.warning "-37"] -type csdp_certificate = S of Sos_types.positivstellensatz option | F of string -(* Used to read the result of the execution of csdpcert *) - -type provername = string * int option - -(** - * The caching mechanism. - *) - -open Micromega_plugin.Persistent_cache - -module Cache = PHashtable(struct - type t = (provername * micromega_polys) - let equal = Pervasives.(=) - let hash = Hashtbl.hash -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 Coq isn't aware of any csdp executable. - *) - -let require_csdp = - if System.is_in_system_path "csdp" - then lazy () - else lazy (raise CsdpNotFound) - -let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivstellensatz option = - fun provername poly -> - - Lazy.force require_csdp; - - 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 - | 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) - -let rec z_to_q_pol e = - match e with - | Mc.Pc z -> Mc.Pc {Mc.qnum = z ; Mc.qden = Mc.XH} - | 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 - | Some cert -> - let cert = Certificate.q_cert_of_pos cert in - if Mc.qWeakChecker poly cert - then Some cert - else ((print_string "buggy certificate") ;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 - | None -> None - | Some cert -> - let cert = Certificate.z_cert_of_pos cert in - if Mc.zWeakChecker poly cert - then Some cert - else ((print_string "buggy certificate" ; flush stdout) ;None) - -let xhyps_of_cone base acc prf = - let rec xtract e acc = - match e with - | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> acc - | Mc.PsatzIn n -> let n = (CoqToCaml.nat n) in - if n >= base - then ISet.add (n-base) acc - else acc - | Mc.PsatzMulC(_,c) -> xtract c acc - | Mc.PsatzAdd(e1,e2) | Mc.PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in - - xtract prf acc - -let hyps_of_cone prf = xhyps_of_cone 0 ISet.empty prf - -let compact_cone prf f = - let np n = CamlToCoq.nat (f (CoqToCaml.nat n)) in - - let rec xinterp prf = - match prf with - | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> prf - | Mc.PsatzIn n -> Mc.PsatzIn (np n) - | Mc.PsatzMulC(e,c) -> Mc.PsatzMulC(e,xinterp c) - | Mc.PsatzAdd(e1,e2) -> Mc.PsatzAdd(xinterp e1,xinterp e2) - | Mc.PsatzMulE(e1,e2) -> Mc.PsatzMulE(xinterp e1,xinterp e2) in - - xinterp prf - -let hyps_of_pt pt = - - let rec xhyps base pt acc = - match pt with - | Mc.DoneProof -> acc - | Mc.RatProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c) - | Mc.CutProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c) - | Mc.EnumProof(c1,c2,l) -> - let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in - List.fold_left (fun s x -> xhyps (base + 1) x s) s l in - - xhyps 0 pt ISet.empty - -let hyps_of_pt pt = - let res = hyps_of_pt pt in - if debug - 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 - - let rec compact_pt ofset pt = - match pt with - | Mc.DoneProof -> Mc.DoneProof - | Mc.RatProof(c,pt) -> Mc.RatProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt ) - | Mc.CutProof(c,pt) -> Mc.CutProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt ) - | Mc.EnumProof(c1,c2,l) -> Mc.EnumProof(compact_cone c1 (translate (ofset)), compact_cone c2 (translate (ofset)), - Mc.map (fun x -> compact_pt (ofset+1) x) l) in - compact_pt 0 pt - -(** - * 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) - -module CacheZ = PHashtable(struct - type prover_option = bool * int - - type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) - -module CacheQ = PHashtable(struct - type t = int * ((Mc.q Mc.pol * Mc.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) - -let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) -let memo_nlia = CacheZ.memo ".nia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) -let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) - - - -let linear_prover_Q = { - name = "linear prover"; - get_option = get_lra_option ; - prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ; - hyps = hyps_of_cone ; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) -} - - -let linear_prover_R = { - name = "linear prover"; - get_option = get_lra_option ; - prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ; - hyps = hyps_of_cone ; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) -} - -let nlinear_prover_R = { - name = "nra"; - get_option = get_lra_option; - prover = memo_nra ; - hyps = hyps_of_cone ; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) -} - -let non_linear_prover_Q str o = { - name = "real nonlinear prover"; - get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> call_csdpcert_q o l); - hyps = hyps_of_cone; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) -} - -let non_linear_prover_R str o = { - name = "real nonlinear prover"; - get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> call_csdpcert_q o l); - hyps = hyps_of_cone; - compact = compact_cone; - pp_prf = pp_psatz pp_q; - pp_f = fun o x -> pp_pol pp_q o (fst x) -} - -let non_linear_prover_Z str o = { - name = "real nonlinear prover"; - get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) -} - -let linear_Z = { - name = "lia"; - get_option = get_lia_option; - prover = memo_zlinear_prover ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) -} - -let nlinear_Z = { - name = "nlia"; - get_option = get_lia_option; - prover = memo_nlia ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) -} - -(** - * Functions instantiating micromega_gen with the appropriate theories and - * solvers - *) - -let lra_Q = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ linear_prover_Q ] - -let psatz_Q i = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] - -let lra_R = - micromega_genr [ linear_prover_R ] - -let psatz_R i = - micromega_genr [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] - - -let psatz_Z i = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] - -let sos_Z = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ non_linear_prover_Z "pure_sos" None ] - -let sos_Q = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ non_linear_prover_Q "pure_sos" None ] - - -let sos_R = - micromega_genr [ non_linear_prover_R "pure_sos" None ] - - -let xlia = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ linear_Z ] - -let xnlia = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ nlinear_Z ] - -let nra = - micromega_genr [ nlinear_prover_R ] - -let nqa = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ nlinear_prover_R ] - - - -(* Local Variables: *) -(* coding: utf-8 *) -(* End: *) |