From ae455fa3aa29c872c9c5b2736fff861afebcd051 Mon Sep 17 00:00:00 2001 From: ckeller Date: Fri, 15 Mar 2019 11:23:55 +0100 Subject: V8.9 (#43) * New syntax for implicit arguments * Towards 8.9: problems with Micromega plugin * Move to _CoqProject * Back to name Makefile * Switch to Makefile.local instead of -extra * The compilation issue is a Coq bug * Ok with 8.9 * INSTALL with 8.9 * Everything ok with 8.9 --- src/versions/native/structures.ml | 4 +- src/versions/native/structures.mli | 6 +- src/versions/standard/Make | 169 -- src/versions/standard/Makefile.local | 33 + src/versions/standard/_CoqProject | 155 ++ src/versions/standard/coq_micromega_full.ml | 2215 ++++++++++++++++++++ src/versions/standard/mutils_full.ml | 358 ++++ src/versions/standard/mutils_full.mli | 77 + .../standard/smtcoq_plugin_standard.mlpack | 2 + src/versions/standard/structures.ml | 16 +- src/versions/standard/structures.mli | 14 +- 11 files changed, 2860 insertions(+), 189 deletions(-) delete mode 100644 src/versions/standard/Make create mode 100644 src/versions/standard/Makefile.local create mode 100644 src/versions/standard/_CoqProject create mode 100644 src/versions/standard/coq_micromega_full.ml create mode 100644 src/versions/standard/mutils_full.ml create mode 100644 src/versions/standard/mutils_full.mli (limited to 'src/versions') diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index e11697e..ee4bf96 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -139,10 +139,10 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r = (* Micromega *) -module Micromega_plugin_Certificate = Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega module Micromega_plugin_Micromega = Micromega module Micromega_plugin_Mutils = Mutils +module Micromega_plugin_Certificate = Certificate +module Micromega_plugin_Coq_micromega = Coq_micromega let micromega_coq_proofTerm = Coq_micromega.M.coq_proofTerm diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli index cae581e..939ffc7 100644 --- a/src/versions/native/structures.mli +++ b/src/versions/native/structures.mli @@ -81,10 +81,10 @@ val mkTrace : (* Micromega *) -module Micromega_plugin_Certificate = Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega module Micromega_plugin_Micromega = Micromega module Micromega_plugin_Mutils = Mutils +module Micromega_plugin_Certificate = Certificate +module Micromega_plugin_Coq_micromega = Coq_micromega val micromega_coq_proofTerm : constr lazy_t val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr @@ -107,7 +107,7 @@ val set_evars_tac : 'a -> Proof_type.tactic type constr_expr = Topconstr.constr_expr val error : string -> 'a val extern_constr : constr -> Topconstr.constr_expr -val destruct_rel_decl : Term.rel_declaration -> name * constr +val destruct_rel_decl : Term.rel_declaration -> name * types val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> constr val ppconstr_lsimpleconstr : Ppconstr.precedence val constrextern_extern_constr : constr -> Topconstr.constr_expr diff --git a/src/versions/standard/Make b/src/versions/standard/Make deleted file mode 100644 index e275b8f..0000000 --- a/src/versions/standard/Make +++ /dev/null @@ -1,169 +0,0 @@ -######################################################################## -## This file is intended to developers: please do not use it ## -## directly, rather use the "configure.sh" script. ## -######################################################################## - - - - -######################################################################## -## To generate the Makefile: ## -## coq_makefile -f Make -o Makefile ## -## In the Makefile : ## -## 1) Add "-native" to the CAMLDEP command (ocamldep -native ...) ## -## 2) remove "post-all" from the targets "all" and "all.timing.diff" ## -######################################################################## - - --R . SMTCoq - --I . --I bva --I classes --I array --I cnf --I euf --I lfsc --I lia --I smtlib2 --I trace --I verit --I zchaff --I versions/standard --I versions/standard/Int63 --I versions/standard/Array - -# -I "$(shell $(COQBIN)coqc -where)/plugins/micromega" - --extra "test" "" "cd ../unit-tests; make" --extra "ztest" "" "cd ../unit-tests; make zchaff" --extra "vtest" "" "cd ../unit-tests; make verit" --extra "lfsctest" "" "cd ../unit-tests; make lfsc" - --extra "%.ml" "%.mll" "$(CAMLLEX) $<" --extra "%.ml %.mli" "%.mly" "$(CAMLYACC) $<" --extra-phony "smtcoq_plugin.mlpack.d" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml" "" - -CAMLLEX = $(CAMLBIN)ocamllex -CAMLYACC = $(CAMLBIN)ocamlyacc - -versions/standard/Int63/Int63.v -versions/standard/Int63/Int63Native.v -versions/standard/Int63/Int63Op.v -versions/standard/Int63/Int63Axioms.v -versions/standard/Int63/Int63Properties.v -versions/standard/Array/PArray.v - -versions/standard/Structures.v -versions/standard/structures.ml -versions/standard/structures.mli - -bva/BVList.v -bva/Bva_checker.v - -classes/SMT_classes.v -classes/SMT_classes_instances.v - -array/FArray.v -array/Array_checker.v - -trace/coqTerms.ml -trace/coqTerms.mli -trace/smtBtype.ml -trace/smtBtype.mli -trace/satAtom.ml -trace/satAtom.mli -trace/smtAtom.ml -trace/smtAtom.mli -trace/smtCertif.ml -trace/smtCertif.mli -trace/smtCnf.ml -trace/smtCnf.mli -trace/smtCommands.ml -trace/smtCommands.mli -trace/smtForm.ml -trace/smtForm.mli -trace/smtMisc.ml -trace/smtMisc.mli -trace/smtTrace.ml -trace/smtTrace.mli - -smtlib2/smtlib2_parse.ml -smtlib2/smtlib2_parse.mli -smtlib2/smtlib2_lex.ml -smtlib2/smtlib2_lex.mli -smtlib2/smtlib2_ast.ml -smtlib2/smtlib2_ast.mli -smtlib2/smtlib2_genConstr.ml -smtlib2/smtlib2_genConstr.mli -smtlib2/smtlib2_util.ml -smtlib2/smtlib2_util.mli -smtlib2/sExpr.ml -smtlib2/sExpr.mli -smtlib2/smtlib2_solver.ml -smtlib2/smtlib2_solver.mli -smtlib2/sExprParser.ml -smtlib2/sExprParser.mli -smtlib2/sExprLexer.ml - -verit/veritParser.ml -verit/veritParser.mli -verit/veritLexer.ml -verit/veritLexer.mli -verit/verit.ml -verit/verit.mli -verit/veritSyntax.ml -verit/veritSyntax.mli - -lfsc/shashcons.mli -lfsc/shashcons.ml -lfsc/hstring.mli -lfsc/hstring.ml -lfsc/lfscParser.ml -lfsc/lfscParser.mli -lfsc/type.ml -lfsc/ast.ml -lfsc/ast.mli -lfsc/translator_sig.mli -lfsc/builtin.ml -lfsc/tosmtcoq.ml -lfsc/tosmtcoq.mli -lfsc/converter.ml -lfsc/lfsc.ml -lfsc/lfscLexer.ml - -zchaff/cnfParser.ml -zchaff/cnfParser.mli -zchaff/satParser.ml -zchaff/satParser.mli -zchaff/zchaff.ml -zchaff/zchaff.mli -zchaff/zchaffParser.ml -zchaff/zchaffParser.mli - -cnf/Cnf.v - -euf/Euf.v - -lia/lia.ml -lia/lia.mli -lia/Lia.v - -spl/Assumptions.v -spl/Syntactic.v -spl/Arithmetic.v -spl/Operators.v - -Conversion_tactics.v -Misc.v -SMTCoq.v -ReflectFacts.v -PropToBool.v -BoolToProp.v -Tactics.v -SMT_terms.v -State.v -Trace.v - -g_smtcoq.ml4 -smtcoq_plugin.mlpack diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local new file mode 100644 index 0000000..67b0b8e --- /dev/null +++ b/src/versions/standard/Makefile.local @@ -0,0 +1,33 @@ +######################################################################## +## This file is intended to developers: please do not use it ## +## directly, rather use the "configure.sh" script. ## +######################################################################## + + +test : + cd ../unit-tests; make + +ztest : + cd ../unit-tests; make zchaff + +vtest : + cd ../unit-tests; make verit + +lfsctest : + cd ../unit-tests; make lfsc + +clean:: + cd ../unit-tests; make clean; rm *vo *glob + + +CAMLLEX = $(CAMLBIN)ocamllex +CAMLYACC = $(CAMLBIN)ocamlyacc + +%.ml : %.mll + $(CAMLLEX) $< + +%.ml %.mli : %.mly + $(CAMLYACC) $< + +.PHONY: smtcoq_plugin.mlpack.d +smtcoq_plugin.mlpack.d : verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject new file mode 100644 index 0000000..a71f500 --- /dev/null +++ b/src/versions/standard/_CoqProject @@ -0,0 +1,155 @@ +######################################################################## +## This file is intended to developers: please do not use it ## +## directly, rather use the "configure.sh" script. ## +######################################################################## + + + + +######################################################################## +## To generate the Makefile: ## +## coq_makefile -f Make -o Makefile ## +######################################################################## + + +-R . SMTCoq + +-I . +-I bva +-I classes +-I array +-I cnf +-I euf +-I lfsc +-I lia +-I smtlib2 +-I trace +-I verit +-I zchaff +-I versions/standard +-I versions/standard/Int63 +-I versions/standard/Array + +versions/standard/Int63/Int63.v +versions/standard/Int63/Int63Native.v +versions/standard/Int63/Int63Op.v +versions/standard/Int63/Int63Axioms.v +versions/standard/Int63/Int63Properties.v +versions/standard/Array/PArray.v + +versions/standard/mutils_full.ml +versions/standard/mutils_full.mli +versions/standard/coq_micromega_full.ml +versions/standard/Structures.v +versions/standard/structures.ml +versions/standard/structures.mli + +bva/BVList.v +bva/Bva_checker.v + +classes/SMT_classes.v +classes/SMT_classes_instances.v + +array/FArray.v +array/Array_checker.v + +trace/coqTerms.ml +trace/coqTerms.mli +trace/smtBtype.ml +trace/smtBtype.mli +trace/satAtom.ml +trace/satAtom.mli +trace/smtAtom.ml +trace/smtAtom.mli +trace/smtCertif.ml +trace/smtCertif.mli +trace/smtCnf.ml +trace/smtCnf.mli +trace/smtCommands.ml +trace/smtCommands.mli +trace/smtForm.ml +trace/smtForm.mli +trace/smtMisc.ml +trace/smtMisc.mli +trace/smtTrace.ml +trace/smtTrace.mli + +smtlib2/smtlib2_parse.ml +smtlib2/smtlib2_parse.mli +smtlib2/smtlib2_lex.ml +smtlib2/smtlib2_lex.mli +smtlib2/smtlib2_ast.ml +smtlib2/smtlib2_ast.mli +smtlib2/smtlib2_genConstr.ml +smtlib2/smtlib2_genConstr.mli +smtlib2/smtlib2_util.ml +smtlib2/smtlib2_util.mli +smtlib2/sExpr.ml +smtlib2/sExpr.mli +smtlib2/smtlib2_solver.ml +smtlib2/smtlib2_solver.mli +smtlib2/sExprParser.ml +smtlib2/sExprParser.mli +smtlib2/sExprLexer.ml + +verit/veritParser.ml +verit/veritParser.mli +verit/veritLexer.ml +verit/veritLexer.mli +verit/verit.ml +verit/verit.mli +verit/veritSyntax.ml +verit/veritSyntax.mli + +lfsc/shashcons.mli +lfsc/shashcons.ml +lfsc/hstring.mli +lfsc/hstring.ml +lfsc/lfscParser.ml +lfsc/lfscParser.mli +lfsc/type.ml +lfsc/ast.ml +lfsc/ast.mli +lfsc/translator_sig.mli +lfsc/builtin.ml +lfsc/tosmtcoq.ml +lfsc/tosmtcoq.mli +lfsc/converter.ml +lfsc/lfsc.ml +lfsc/lfscLexer.ml + +zchaff/cnfParser.ml +zchaff/cnfParser.mli +zchaff/satParser.ml +zchaff/satParser.mli +zchaff/zchaff.ml +zchaff/zchaff.mli +zchaff/zchaffParser.ml +zchaff/zchaffParser.mli + +cnf/Cnf.v + +euf/Euf.v + +lia/lia.ml +lia/lia.mli +lia/Lia.v + +spl/Assumptions.v +spl/Syntactic.v +spl/Arithmetic.v +spl/Operators.v + +Conversion_tactics.v +Misc.v +SMTCoq.v +ReflectFacts.v +PropToBool.v +BoolToProp.v +Tactics.v +SMT_terms.v +State.v +Trace.v + +g_smtcoq.ml4 +smtcoq_plugin.mlpack diff --git a/src/versions/standard/coq_micromega_full.ml b/src/versions/standard/coq_micromega_full.ml new file mode 100644 index 0000000..d957110 --- /dev/null +++ b/src/versions/standard/coq_micromega_full.ml @@ -0,0 +1,2215 @@ +(*** 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 *) +(* 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: *) diff --git a/src/versions/standard/mutils_full.ml b/src/versions/standard/mutils_full.ml new file mode 100644 index 0000000..efa2e4d --- /dev/null +++ b/src/versions/standard/mutils_full.ml @@ -0,0 +1,358 @@ +(*** This file is taken from Coq-8.9.0 to solve a compilation issue due + to a wrong order in dependencies. + See https://github.com/coq/coq/issues/9768 . ***) + + +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* () + | e::l -> f o e ; output_string o ";" ; pp_list f o l + + +let finally f rst = + try + let res = f () in + rst () ; res + with reraise -> + (try rst () + with any -> raise reraise + ); raise reraise + +let rec try_any l x = + match l with + | [] -> None + | (f,s)::l -> match f x with + | None -> try_any l x + | x -> x + +let all_sym_pairs f l = + let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in + + let rec xpairs acc l = + match l with + | [] -> acc + | e::l -> xpairs (pair_with acc e l) l in + xpairs [] l + +let all_pairs f l = + let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in + + let rec xpairs acc l = + match l with + | [] -> acc + | e::lx -> xpairs (pair_with acc e l) lx in + xpairs [] l + +let rec is_sublist f l1 l2 = + match l1 ,l2 with + | [] ,_ -> true + | e::l1', [] -> false + | e::l1' , e'::l2' -> + if f e e' then is_sublist f l1' l2' + else is_sublist f l1 l2' + +let extract pred l = + List.fold_left (fun (fd,sys) e -> + match fd with + | None -> + begin + match pred e with + | None -> fd, e::sys + | Some v -> Some(v,e) , sys + end + | _ -> (fd, e::sys) + ) (None,[]) l + +open Num +open Big_int + +let ppcm x y = + let g = gcd_big_int x y in + let x' = div_big_int x g in + let y' = div_big_int y g in + mult_big_int g (mult_big_int x' y') + +let denominator = function + | Int _ | Big_int _ -> unit_big_int + | Ratio r -> Ratio.denominator_ratio r + +let numerator = function + | Ratio r -> Ratio.numerator_ratio r + | Int i -> Big_int.big_int_of_int i + | Big_int i -> i + +let rec ppcm_list c l = + match l with + | [] -> c + | e::l -> ppcm_list (ppcm c (denominator e)) l + +let rec rec_gcd_list c l = + match l with + | [] -> c + | e::l -> rec_gcd_list (gcd_big_int c (numerator e)) l + +let gcd_list l = + let res = rec_gcd_list zero_big_int l in + if Int.equal (compare_big_int res zero_big_int) 0 + then unit_big_int else res + +let rats_to_ints l = + let c = ppcm_list unit_big_int l in + List.map (fun x -> (div_big_int (mult_big_int (numerator x) c) + (denominator x))) l + +(* assoc_pos j [a0...an] = [j,a0....an,j+n],j+n+1 *) +(** + * MODULE: Coq to Caml data-structure mappings + *) + +module CoqToCaml = +struct + open Micromega + + let rec nat = function + | O -> 0 + | S n -> (nat n) + 1 + + + let rec positive p = + match p with + | XH -> 1 + | XI p -> 1+ 2*(positive p) + | XO p -> 2*(positive p) + + let n nt = + match nt with + | N0 -> 0 + | Npos p -> positive p + + let rec index i = (* Swap left-right ? *) + match i with + | XH -> 1 + | XI i -> 1+(2*(index i)) + | XO i -> 2*(index i) + + open Big_int + + let rec positive_big_int p = + match p with + | XH -> unit_big_int + | XI p -> add_int_big_int 1 (mult_int_big_int 2 (positive_big_int p)) + | XO p -> (mult_int_big_int 2 (positive_big_int p)) + + let z_big_int x = + match x with + | Z0 -> zero_big_int + | Zpos p -> (positive_big_int p) + | Zneg p -> minus_big_int (positive_big_int p) + + let q_to_num {qnum = x ; qden = y} = + Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y))) + +end + + +(** + * MODULE: Caml to Coq data-structure mappings + *) + +module CamlToCoq = +struct + open Micromega + + let rec nat = function + | 0 -> O + | n -> S (nat (n-1)) + + + let rec positive n = + if Int.equal n 1 then XH + else if Int.equal (n land 1) 1 then XI (positive (n lsr 1)) + else XO (positive (n lsr 1)) + + let n nt = + if nt < 0 + then assert false + else if Int.equal nt 0 then N0 + else Npos (positive nt) + + let rec index n = + if Int.equal n 1 then XH + else if Int.equal (n land 1) 1 then XI (index (n lsr 1)) + else XO (index (n lsr 1)) + + + let z x = + match compare x 0 with + | 0 -> Z0 + | 1 -> Zpos (positive x) + | _ -> (* this should be -1 *) + Zneg (positive (-x)) + + open Big_int + + let positive_big_int n = + let two = big_int_of_int 2 in + let rec _pos n = + if eq_big_int n unit_big_int then XH + else + let (q,m) = quomod_big_int n two in + if eq_big_int unit_big_int m + then XI (_pos q) + else XO (_pos q) in + _pos n + + let bigint x = + match sign_big_int x with + | 0 -> Z0 + | 1 -> Zpos (positive_big_int x) + | _ -> Zneg (positive_big_int (minus_big_int x)) + + let q n = + {Micromega.qnum = bigint (numerator n) ; + Micromega.qden = positive_big_int (denominator n)} + +end + +(** + * MODULE: Comparisons on lists: by evaluating the elements in a single list, + * between two lists given an ordering, and using a hash computation + *) + +module Cmp = +struct + + let rec compare_lexical l = + match l with + | [] -> 0 (* Equal *) + | f::l -> + let cmp = f () in + if Int.equal cmp 0 then compare_lexical l else cmp + + let rec compare_list cmp l1 l2 = + match l1 , l2 with + | [] , [] -> 0 + | [] , _ -> -1 + | _ , [] -> 1 + | e1::l1 , e2::l2 -> + let c = cmp e1 e2 in + if Int.equal c 0 then compare_list cmp l1 l2 else c + +end + +(** + * MODULE: Labels for atoms in propositional formulas. + * Tags are used to identify unused atoms in CNFs, and propagate them back to + * the original formula. The translation back to Coq then ignores these + * superfluous items, which speeds the translation up a bit. + *) + +module type Tag = +sig + + type t + + val from : int -> t + val next : t -> t + val pp : out_channel -> t -> unit + val compare : t -> t -> int + +end + +module Tag : Tag = +struct + + type t = int + + let from i = i + let next i = i + 1 + let pp o i = output_string o (string_of_int i) + let compare : int -> int -> int = Int.compare + +end + +(** + * MODULE: Ordered sets of tags. + *) + +module TagSet = Set.Make(Tag) + +(** As for Unix.close_process, our Unix.waipid will ignore all EINTR *) + +let rec waitpid_non_intr pid = + try snd (Unix.waitpid [] pid) + with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid + +(** + * Forking routine, plumbing the appropriate pipes where needed. + *) + +let command exe_path args vl = + (* creating pipes for stdin, stdout, stderr *) + let (stdin_read,stdin_write) = Unix.pipe () + and (stdout_read,stdout_write) = Unix.pipe () + and (stderr_read,stderr_write) = Unix.pipe () in + + (* Create the process *) + let pid = Unix.create_process exe_path args stdin_read stdout_write stderr_write in + + (* Write the data on the stdin of the created process *) + let outch = Unix.out_channel_of_descr stdin_write in + output_value outch vl ; + flush outch ; + + (* Wait for its completion *) + let status = waitpid_non_intr pid in + + finally + (* Recover the result *) + (fun () -> + match status with + | Unix.WEXITED 0 -> + let inch = Unix.in_channel_of_descr stdout_read in + begin + try Marshal.from_channel inch + with any -> + failwith + (Printf.sprintf "command \"%s\" exited %s" exe_path + (Printexc.to_string any)) + end + | Unix.WEXITED i -> + failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i) + | Unix.WSIGNALED i -> + failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i) + | Unix.WSTOPPED i -> + failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i)) + (* Cleanup *) + (fun () -> + List.iter (fun x -> try Unix.close x with any -> ()) + [stdin_read; stdin_write; + stdout_read; stdout_write; + stderr_read; stderr_write]) + +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) diff --git a/src/versions/standard/mutils_full.mli b/src/versions/standard/mutils_full.mli new file mode 100644 index 0000000..d506485 --- /dev/null +++ b/src/versions/standard/mutils_full.mli @@ -0,0 +1,77 @@ +(*** This file is taken from Coq-8.9.0 to solve a compilation issue due + to a wrong order in dependencies. + See https://github.com/coq/coq/issues/9768 . ***) + + +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Big_int.big_int +val denominator : Num.num -> Big_int.big_int + +module Cmp : sig + + val compare_list : ('a -> 'b -> int) -> 'a list -> 'b list -> int + val compare_lexical : (unit -> int) list -> int + +end + +module Tag : sig + + type t + + val pp : out_channel -> t -> unit + val next : t -> t + val from : int -> t + +end + +module TagSet : CSig.SetS with type elt = Tag.t + +val pp_list : (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit + +module CamlToCoq : sig + + val positive : int -> Micromega.positive + val bigint : Big_int.big_int -> Micromega.z + val n : int -> Micromega.n + val nat : int -> Micromega.nat + val q : Num.num -> Micromega.q + val index : int -> Micromega.positive + val z : int -> Micromega.z + val positive_big_int : Big_int.big_int -> Micromega.positive + +end + +module CoqToCaml : sig + + val z_big_int : Micromega.z -> Big_int.big_int + val q_to_num : Micromega.q -> Num.num + val positive : Micromega.positive -> int + val n : Micromega.n -> int + val nat : Micromega.nat -> int + val index : Micromega.positive -> int + +end + +val rats_to_ints : Num.num list -> Big_int.big_int list + +val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list +val all_sym_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list +val try_any : (('a -> 'b option) * 'c) list -> 'a -> 'b option +val is_sublist : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool + +val gcd_list : Num.num list -> Big_int.big_int + +val extract : ('a -> 'b option) -> 'a list -> ('b * 'a) option * 'a list + +val command : string -> string array -> 'a -> 'b diff --git a/src/versions/standard/smtcoq_plugin_standard.mlpack b/src/versions/standard/smtcoq_plugin_standard.mlpack index 68ce13a..0101147 100644 --- a/src/versions/standard/smtcoq_plugin_standard.mlpack +++ b/src/versions/standard/smtcoq_plugin_standard.mlpack @@ -1,3 +1,5 @@ +Mutils_full +Coq_micromega_full Structures SmtMisc diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index f259a70..ea35a35 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -77,14 +77,14 @@ let mkTConst c noc ty = (* TODO : Set -> Type *) let declare_new_type t = - let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) Universes.empty_binders [] false Vernacexpr.NoInline (CAst.make t) in + let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in Constr.mkVar t let declare_new_variable v constr_t = let env = Global.env () in let evd = Evd.from_env env in let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in - let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) Universes.empty_binders [] false Vernacexpr.NoInline (CAst.make v) in + let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in Constr.mkVar v let declare_constant n c = @@ -103,7 +103,7 @@ let econstr_of_constr = EConstr.of_constr (* Modules *) -let gen_constant_in_modules s m n = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n +let gen_constant_in_modules s m n = UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) @@ -165,18 +165,18 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = (* Micromega *) -module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Micromega_plugin.Mutils +module Micromega_plugin_Mutils = Mutils_full +module Micromega_plugin_Certificate = Micromega_plugin.Certificate +module Micromega_plugin_Coq_micromega = Coq_micromega_full let micromega_coq_proofTerm = (* Cannot contain evars *) - lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin.Coq_micromega.M.coq_proofTerm))) + lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin_Coq_micromega.M.coq_proofTerm))) let micromega_dump_proof_term p = (* Cannot contain evars *) - EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p) + EConstr.Unsafe.to_constr (Micromega_plugin_Coq_micromega.dump_proof_term p) (* Tactics *) diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index 3d6f6b2..3aa8b3b 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -87,13 +87,13 @@ val mkTrace : (* Micromega *) -module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Micromega_plugin.Mutils +module Micromega_plugin_Mutils = Mutils_full +module Micromega_plugin_Certificate = Micromega_plugin.Certificate +module Micromega_plugin_Coq_micromega = Coq_micromega_full val micromega_coq_proofTerm : constr lazy_t -val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr +val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr (* Tactics *) @@ -110,11 +110,11 @@ val set_evars_tac : constr -> tactic type constr_expr = Constrexpr.constr_expr val error : string -> 'a val extern_constr : constr -> constr_expr -val destruct_rel_decl : Context.Rel.Declaration.t -> name * constr +val destruct_rel_decl : (constr, types) Context.Rel.Declaration.pt -> name * types val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr -val ppconstr_lsimpleconstr : Notation_term.tolerability +val ppconstr_lsimpleconstr : Notation_gram.tolerability val constrextern_extern_constr : constr -> constr_expr -val get_rel_dec_name : Context.Rel.Declaration.t -> name +val get_rel_dec_name : (constr, types) Context.Rel.Declaration.pt -> name val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr val vm_conv : Reduction.conv_pb -> types Reduction.kernel_conversion_function -- cgit