From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- plugins/micromega/coq_micromega.ml | 1710 ++++++++++++++++++++++++++++++++++++ 1 file changed, 1710 insertions(+) create mode 100644 plugins/micromega/coq_micromega.ml (limited to 'plugins/micromega/coq_micromega.ml') diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml new file mode 100644 index 00000000..abe4b368 --- /dev/null +++ b/plugins/micromega/coq_micromega.ml @@ -0,0 +1,1710 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ,=,<>,<=,>=} 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 + | 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 + | 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.string_of_id id + | 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) + | _ -> [] + +(** + * 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 + + 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' = + match f with + | [] -> tt + | e :: rst -> (or_cnf rst f') @ (or_clause_cnf e f') 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) -> + (if polarity then and_cnf else or_cnf) (xcnf polarity e1) (xcnf polarity e2) + | D(e1,e2) -> + (if polarity then or_cnf else and_cnf) (xcnf polarity e1) (xcnf polarity e2) + | I(e1,_,e2) -> + (if polarity then or_cnf else and_cnf) (xcnf (not polarity) e1) (xcnf polarity e2) in + + xcnf true f + +(** + * MODULE: Ordered set of integers. + *) + +module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end) + +(** + * 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 + + 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 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 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 = + 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) = + 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 + 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_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 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 = 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 + + (** + * 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) + | _ -> [] + +let same_proof sg cl1 cl2 = + let rec xsame_proof sg = + match sg with + | [] -> true + | n::sg -> (try List.nth cl1 n = List.nth cl2 n with _ -> false) + && (xsame_proof sg ) in + xsame_proof sg + +let tags_of_clause tgs wit clause = + let rec xtags tgs = function + | Mc.PsatzIn n -> Names.Idset.union tgs + (snd (List.nth clause (CoqToCaml.nat n) )) + | Mc.PsatzMulC(e,w) -> xtags tgs w + | Mc.PsatzMulE (w1,w2) | Mc.PsatzAdd(w1,w2) -> xtags (xtags tgs w1) w2 + | _ -> tgs in + xtags tgs wit + +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 = + match l2 with + | [] -> Some [] + | e :: l2 -> + match find_witness prover (e::l1) with + | None -> None + | Some w -> + (match witness prover l1 l2 with + | None -> None + | 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") +let coq_Leaf = lazy + (Coqlib.gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf") +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 + let node = Lazy.force coq_Node + and leaf = Lazy.force coq_Leaf + and empty = Term.mkApp (Lazy.force coq_Empty, [| typ |]) in + let rec aux n = + if n > size_of_a + then empty + else if n > semi_size_of_a + then Term.mkApp (leaf, [| typ; a.(n-1) |]) + else Term.mkApp (node, [| typ; aux (2*n); a.(n-1); aux (2*n+1) |]) + in + aux 1 + +let btree_of_array typ a = + try + btree_of_array typ a + with x -> + failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x)) + +let dump_varmap typ env = + btree_of_array typ (Array.of_list env) + + +let rec pp_varmap o vm = + match vm with + | Mc.Empty -> output_string o "[]" + | Mc.Leaf z -> Printf.fprintf o "[%a]" pp_z z + | Mc.Node(l,z,r) -> Printf.fprintf o "[%a, %a, %a]" pp_varmap l pp_z z pp_varmap r + + + +let rec dump_proof_term = function + | Micromega.DoneProof -> Lazy.force coq_doneProof + | Micromega.RatProof(cone,rst) -> + Term.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|]) + | Micromega.CutProof(cone,prf) -> + Term.mkApp(Lazy.force coq_cutProof, + [| dump_psatz coq_Z dump_z cone ; + dump_proof_term prf|]) + | Micromega.EnumProof(c1,c2,prfs) -> + Term.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 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 parse_arith env tg hyps = + match hyps with + | [] -> ([],env,tg) + | (i,t)::l -> + let (lhyps,env,tg) = parse_hyps parse_arith env tg l in + try + let (c,env,tg) = parse_formula parse_arith env tg t in + ((i,c)::lhyps, env,tg) + with _ -> (lhyps,env,tg) + (*(if debug then Printf.printf "parse_arith : %s\n" x);*) + + +(*exception ParseError*) + +let parse_goal parse_arith env hyps term = + (* try*) + let (f,env,tg) = parse_formula parse_arith env (Tag.from 0) term in + let (lhyps,env,tg) = parse_hyps parse_arith env tg hyps in + (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 *) + coeff : Term.constr ; (* Z, Q *) + dump_coeff : 'd -> Term.constr ; + proof_typ : Term.constr ; + dump_proof : 'prf -> Term.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 +} + +let rz_domain_spec = lazy { + typ = Lazy.force coq_R; + coeff = Lazy.force coq_Z; + dump_coeff = dump_z; + proof_typ = Lazy.force coq_ZWitness ; + dump_proof = dump_psatz coq_Z dump_z +} + +(** + * Instanciate the current Coq goal with a Micromega formula, a varmap, and a + * witness. + *) + +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 + Tactics.change_in_concl None + (set + [ + ("__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) + ] + (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 *) + 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 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 + +(* *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 + + 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 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 (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 + +(** + * 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) -> + 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 "\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 + +(** + * 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 = + let concl = Tacmach.pf_concl gl in + let hyps = Tacmach.pf_hyps_types gl in + try + let (hyps,concl,env) = parse_goal parse_arith Env.empty hyps concl in + let env = Env.elements env in + micromega_tauto negate normalise spec prover env hyps concl gl + with + | 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 + | None -> None + | Some c -> Some (Mc.RatProof( c,Mc.DoneProof)) + +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 + type t = (provername * micromega_polys) + let equal = (=) + 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 a Coq isn't aware of any csdp executable. + *) + +let require_csdp = + match System.search_exe_in_path "csdp" with + | Some _ -> lazy () + | _ -> 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" ; 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 + | 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) + +let linear_prover_Z = { + name = "linear prover" ; + prover = lift_ratproof (lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec)) ; + 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_prover_Q = { + name = "linear prover"; + prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ; + 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"; + prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec) ; + hyps = hyps_of_cone ; + compact = compact_cone ; + pp_prf = pp_psatz pp_z ; + pp_f = fun o x -> pp_pol pp_z o (fst x) +} + +let non_linear_prover_Q str o = { + name = "real nonlinear prover"; + prover = call_csdpcert_q (str, o); + 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"; + prover = call_csdpcert_z (str, o); + hyps = hyps_of_cone; + compact = compact_cone; + pp_prf = pp_psatz pp_z; + pp_f = fun o x -> pp_pol pp_z o (fst x) +} + +let non_linear_prover_Z str o = { + name = "real nonlinear prover"; + prover = lift_ratproof (call_csdpcert_z (str, o)); + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) +} + +module CacheZ = PHashtable(struct + type t = (Mc.z Mc.pol * Mc.op1) list + let equal = (=) + let hash = Hashtbl.hash +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; + 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 psatzl_Z gl = + micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec + [ linear_prover_Z ] gl + +let psatzl_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 + +let psatzl_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 + +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 + +let sos_Z gl = + micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec + [ 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 + +let sos_R gl = + micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec + [ 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 + +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) -- cgit v1.2.3