Quelle  coq_micromega.ml   Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                                                                      *)
(* Micromega: A reflexive tactic using the Positivstellensatz           *)
(*                                                                      *)
(* ** Toplevel definition of tactics **                                 *)
(*                                                                      *)
(* - Modules Mc, Env, Cache, CacheZ                                  *)
(*                                                                      *)
(*  Frédéric Besson (Irisa/Inria) 2006-2019                             *)
(*                                                                      *)
(************************************************************************)

open Pp
open Names
open Goptions
open Mutils
open Constr
open Context
open Tactypes
open McPrinter

module ERelevance = EConstr.ERelevance

(**
  * Debug flag
  *)

let debug = false

(* Limit the proof search *)

let max_depth = max_int

let since_8_14 = Deprecation.make ~since:"8.14" ()

(* Search limit for provers over Q R *)
let { Goptions.get = lra_proof_depth } =
  declare_int_option_and_ref
    ~depr:since_8_14
    ~key:["Lra"; "Depth"]
    ~value:max_depth
    ()

let { Goptions.get = lia_proof_depth } =
  declare_int_option_and_ref
    ~depr:since_8_14
    ~key:["Lia"; "Depth"]
    ~value:max_depth
    ()

let get_lia_option () = lia_proof_depth ()

(* Enable/disable caches *)

let { Goptions.get = use_lia_cache } =
  declare_bool_option_and_ref
    ~key:["Lia"; "Cache"]
    ~value:true
    ()

let { Goptions.get = use_nia_cache } =
  declare_bool_option_and_ref
    ~key:["Nia"; "Cache"]
    ~value:true
    ()

let { Goptions.get = use_nra_cache } =
  declare_bool_option_and_ref
    ~key:["Nra"; "Cache"]
    ~value:true
    ()

let { Goptions.get = show_used_hyps } =
  declare_bool_option_and_ref
    ~key:["Info";"Micromega"]
    ~value:false
    ()

let use_csdp_cache () = true

(**
  * Initialize a tag type to the Tag module declaration (see Mutils).
  *)

type tag = Tag.t

module Mc = Micromega

(**
  * 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 Mc.formula

type 'cst formula =
  ('cst atom, EConstr.constr, tag * EConstr.constr, Names.Id.t) Mc.gFormula

type 'cst clause = ('cst Mc.nFormula, tag * EConstr.constr) Mc.clause
type 'cst cnf = ('cst Mc.nFormula, tag * EConstr.constr) Mc.cnf

let pp_kind o = function
  | Mc.IsProp -> output_string o "Prop"
  | Mc.IsBool -> output_string o "bool"

let kind_is_prop = function Mc.IsProp -> true | Mc.IsBool -> false

let rec pp_formula o (f : 'cst formula) =
  Mc.(
    match f with
    | TT k -> output_string o (if kind_is_prop k then "True" else "true")
    | FF k -> output_string o (if kind_is_prop k then "False" else "false")
    | X (k, c) -> Printf.fprintf o "X %a" pp_kind k
    | A (_, _, (t, _)) -> Printf.fprintf o "A(%a)" Tag.pp t
    | AND (_, f1, f2) ->
      Printf.fprintf o "AND(%a,%a)" pp_formula f1 pp_formula f2
    | OR (_, f1, f2) -> Printf.fprintf o "OR(%a,%a)" pp_formula f1 pp_formula f2
    | IMPL (_, f1, n, f2) ->
      Printf.fprintf o "IMPL(%a,%s,%a)" pp_formula f1
        (match n with Some id -> Names.Id.to_string id | None -> "")
        pp_formula f2
    | NOT (_, f) -> Printf.fprintf o "NOT(%a)" pp_formula f
    | IFF (_, f1, f2) ->
      Printf.fprintf o "IFF(%a,%a)" pp_formula f1 pp_formula f2
    | EQ (f1, f2) -> Printf.fprintf o "EQ(%a,%a)" pp_formula f1 pp_formula f2)

(**
  * 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 Rocq data-strustures into Caml and Caml extracted
  * code. This includes initializing Caml variables based on Rocq terms, parsing
  * various Rocq expressions into Caml, and dumping Caml expressions into Rocq.
  *
  * Opened here and in csdpcert.ml.
  *)

(**
    * Initialization : a large amount of Caml symbols are derived from
    * ZMicromega.v
    *)

let constr_of_ref str =
  EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Global.env ()) (Rocqlib.lib_ref str))

let rocq_and = lazy (constr_of_ref "core.and.type")
let rocq_or = lazy (constr_of_ref "core.or.type")
let rocq_not = lazy (constr_of_ref "core.not.type")
let rocq_iff = lazy (constr_of_ref "core.iff.type")
let rocq_True = lazy (constr_of_ref "core.True.type")
let rocq_False = lazy (constr_of_ref "core.False.type")
let rocq_bool = lazy (constr_of_ref "core.bool.type")
let rocq_true = lazy (constr_of_ref "core.bool.true")
let rocq_false = lazy (constr_of_ref "core.bool.false")
let rocq_andb = lazy (constr_of_ref "core.bool.andb")
let rocq_orb = lazy (constr_of_ref "core.bool.orb")
let rocq_implb = lazy (constr_of_ref "core.bool.implb")
let rocq_eqb = lazy (constr_of_ref "core.bool.eqb")
let rocq_negb = lazy (constr_of_ref "core.bool.negb")
let rocq_cons = lazy (constr_of_ref "core.list.cons")
let rocq_nil = lazy (constr_of_ref "core.list.nil")
let rocq_list = lazy (constr_of_ref "core.list.type")
let rocq_O = lazy (constr_of_ref "num.nat.O")
let rocq_S = lazy (constr_of_ref "num.nat.S")
let rocq_nat = lazy (constr_of_ref "num.nat.type")
let rocq_unit = lazy (constr_of_ref "core.unit.type")

(*  let rocq_option = lazy (init_constant "option")*)
let rocq_None = lazy (constr_of_ref "core.option.None")
let rocq_tt = lazy (constr_of_ref "core.unit.tt")
let rocq_Inl = lazy (constr_of_ref "core.sum.inl")
let rocq_Inr = lazy (constr_of_ref "core.sum.inr")
let rocq_N0 = lazy (constr_of_ref "num.N.N0")
let rocq_Npos = lazy (constr_of_ref "num.N.Npos")
let rocq_xH = lazy (constr_of_ref "num.pos.xH")
let rocq_xO = lazy (constr_of_ref "num.pos.xO")
let rocq_xI = lazy (constr_of_ref "num.pos.xI")
let rocq_Z = lazy (constr_of_ref "num.Z.type")
let rocq_ZERO = lazy (constr_of_ref "num.Z.Z0")
let rocq_POS = lazy (constr_of_ref "num.Z.Zpos")
let rocq_NEG = lazy (constr_of_ref "num.Z.Zneg")
let rocq_Q = lazy (constr_of_ref "rat.Q.type")
let rocq_Qmake = lazy (constr_of_ref "rat.Q.Qmake")
let rocq_R = lazy (constr_of_ref "reals.R.type")
let rocq_Rcst = lazy (constr_of_ref "micromega.Rcst.type")
let rocq_C0 = lazy (constr_of_ref "micromega.Rcst.C0")
let rocq_C1 = lazy (constr_of_ref "micromega.Rcst.C1")
let rocq_CQ = lazy (constr_of_ref "micromega.Rcst.CQ")
let rocq_CZ = lazy (constr_of_ref "micromega.Rcst.CZ")
let rocq_CPlus = lazy (constr_of_ref "micromega.Rcst.CPlus")
let rocq_CMinus = lazy (constr_of_ref "micromega.Rcst.CMinus")
let rocq_CMult = lazy (constr_of_ref "micromega.Rcst.CMult")
let rocq_CPow = lazy (constr_of_ref "micromega.Rcst.CPow")
let rocq_CInv = lazy (constr_of_ref "micromega.Rcst.CInv")
let rocq_COpp = lazy (constr_of_ref "micromega.Rcst.COpp")
let rocq_R0 = lazy (constr_of_ref "reals.R.R0")
let rocq_R1 = lazy (constr_of_ref "reals.R.R1")
let rocq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type")
let rocq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof")
let rocq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof")
let rocq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof")
let rocq_splitProof = lazy (constr_of_ref "micromega.ZArithProof.SplitProof")
let rocq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof")
let rocq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof")
let rocq_IsProp = lazy (constr_of_ref "micromega.kind.isProp")
let rocq_IsBool = lazy (constr_of_ref "micromega.kind.isBool")
let rocq_Zgt = lazy (constr_of_ref "num.Z.gt")
let rocq_Zge = lazy (constr_of_ref "num.Z.ge")
let rocq_Zle = lazy (constr_of_ref "num.Z.le")
let rocq_Zlt = lazy (constr_of_ref "num.Z.lt")
let rocq_Zgtb = lazy (constr_of_ref "num.Z.gtb")
let rocq_Zgeb = lazy (constr_of_ref "num.Z.geb")
let rocq_Zleb = lazy (constr_of_ref "num.Z.leb")
let rocq_Zltb = lazy (constr_of_ref "num.Z.ltb")
let rocq_Zeqb = lazy (constr_of_ref "num.Z.eqb")
let rocq_eq = lazy (constr_of_ref "core.eq.type")
let rocq_Zplus = lazy (constr_of_ref "num.Z.add")
let rocq_Zminus = lazy (constr_of_ref "num.Z.sub")
let rocq_Zopp = lazy (constr_of_ref "num.Z.opp")
let rocq_Zmult = lazy (constr_of_ref "num.Z.mul")
let rocq_Zpower = lazy (constr_of_ref "num.Z.pow")
let rocq_Qle = lazy (constr_of_ref "rat.Q.Qle")
let rocq_Qlt = lazy (constr_of_ref "rat.Q.Qlt")
let rocq_Qeq = lazy (constr_of_ref "rat.Q.Qeq")
let rocq_Qplus = lazy (constr_of_ref "rat.Q.Qplus")
let rocq_Qminus = lazy (constr_of_ref "rat.Q.Qminus")
let rocq_Qopp = lazy (constr_of_ref "rat.Q.Qopp")
let rocq_Qmult = lazy (constr_of_ref "rat.Q.Qmult")
let rocq_Qpower = lazy (constr_of_ref "rat.Q.Qpower")
let rocq_Rgt = lazy (constr_of_ref "reals.R.Rgt")
let rocq_Rge = lazy (constr_of_ref "reals.R.Rge")
let rocq_Rle = lazy (constr_of_ref "reals.R.Rle")
let rocq_Rlt = lazy (constr_of_ref "reals.R.Rlt")
let rocq_Rplus = lazy (constr_of_ref "reals.R.Rplus")
let rocq_Rminus = lazy (constr_of_ref "reals.R.Rminus")
let rocq_Ropp = lazy (constr_of_ref "reals.R.Ropp")
let rocq_Rmult = lazy (constr_of_ref "reals.R.Rmult")
let rocq_Rinv = lazy (constr_of_ref "reals.R.Rinv")
let rocq_Rpower = lazy (constr_of_ref "reals.R.pow")
let rocq_powerZR = lazy (constr_of_ref "reals.R.powerRZ")
let rocq_IZR = lazy (constr_of_ref "reals.R.IZR")
let rocq_IQR = lazy (constr_of_ref "reals.R.Q2R")
let rocq_PEX = lazy (constr_of_ref "micromega.PExpr.PEX")
let rocq_PEc = lazy (constr_of_ref "micromega.PExpr.PEc")
let rocq_PEadd = lazy (constr_of_ref "micromega.PExpr.PEadd")
let rocq_PEopp = lazy (constr_of_ref "micromega.PExpr.PEopp")
let rocq_PEmul = lazy (constr_of_ref "micromega.PExpr.PEmul")
let rocq_PEsub = lazy (constr_of_ref "micromega.PExpr.PEsub")
let rocq_PEpow = lazy (constr_of_ref "micromega.PExpr.PEpow")
let rocq_PX = lazy (constr_of_ref "micromega.Pol.PX")
let rocq_Pc = lazy (constr_of_ref "micromega.Pol.Pc")
let rocq_Pinj = lazy (constr_of_ref "micromega.Pol.Pinj")
let rocq_OpEq = lazy (constr_of_ref "micromega.Op2.OpEq")
let rocq_OpNEq = lazy (constr_of_ref "micromega.Op2.OpNEq")
let rocq_OpLe = lazy (constr_of_ref "micromega.Op2.OpLe")
let rocq_OpLt = lazy (constr_of_ref "micromega.Op2.OpLt")
let rocq_OpGe = lazy (constr_of_ref "micromega.Op2.OpGe")
let rocq_OpGt = lazy (constr_of_ref "micromega.Op2.OpGt")
let rocq_PsatzLet = lazy (constr_of_ref "micromega.Psatz.PsatzLet")
let rocq_PsatzIn = lazy (constr_of_ref "micromega.Psatz.PsatzIn")
let rocq_PsatzSquare = lazy (constr_of_ref "micromega.Psatz.PsatzSquare")
let rocq_PsatzMulE = lazy (constr_of_ref "micromega.Psatz.PsatzMulE")
let rocq_PsatzMultC = lazy (constr_of_ref "micromega.Psatz.PsatzMulC")
let rocq_PsatzAdd = lazy (constr_of_ref "micromega.Psatz.PsatzAdd")
let rocq_PsatzC = lazy (constr_of_ref "micromega.Psatz.PsatzC")
let rocq_PsatzZ = lazy (constr_of_ref "micromega.Psatz.PsatzZ")

(*  let rocq_GT     = lazy (m_constant "GT")*)

let rocq_DeclaredConstant =
  lazy (constr_of_ref "micromega.DeclaredConstant.type")

let rocq_TT = lazy (constr_of_ref "micromega.GFormula.TT")
let rocq_FF = lazy (constr_of_ref "micromega.GFormula.FF")
let rocq_AND = lazy (constr_of_ref "micromega.GFormula.AND")
let rocq_OR = lazy (constr_of_ref "micromega.GFormula.OR")
let rocq_NOT = lazy (constr_of_ref "micromega.GFormula.NOT")
let rocq_Atom = lazy (constr_of_ref "micromega.GFormula.A")
let rocq_X = lazy (constr_of_ref "micromega.GFormula.X")
let rocq_IMPL = lazy (constr_of_ref "micromega.GFormula.IMPL")
let rocq_IFF = lazy (constr_of_ref "micromega.GFormula.IFF")
let rocq_EQ = lazy (constr_of_ref "micromega.GFormula.EQ")
let rocq_Formula = lazy (constr_of_ref "micromega.BFormula.type")
let rocq_eKind = lazy (constr_of_ref "micromega.eKind")

(**
    * Initialization : a few Caml symbols are derived from other libraries;
    * QMicromega, ZArithRing, RingMicromega.
    *)

let rocq_QWitness = lazy (constr_of_ref "micromega.QWitness.type")
let rocq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula")
let rocq_Cstr = lazy (constr_of_ref "micromega.Formula.type")

(**
    * Parsing and dumping : transformation functions between Caml and Rocq
    * data-structures.
    *
    * dump_*    functions go from Micromega to Rocq terms
    * undump_*  functions go from Rocq to Micromega terms (reverse of dump_)
    * parse_*   functions go from Rocq to Micromega terms
    * pp_*      functions pretty-print Rocq 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 rec dump_nat x =
  match x with
  | Mc.O -> Lazy.force rocq_O
  | Mc.S p -> EConstr.mkApp (Lazy.force rocq_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 rocq_xH
  | Mc.XO p -> EConstr.mkApp (Lazy.force rocq_xO, [|dump_positive p|])
  | Mc.XI p -> EConstr.mkApp (Lazy.force rocq_xI, [|dump_positive p|])

let parse_n sigma term =
  let i, c = get_left_construct sigma term in
  match i with
  | 1 -> Mc.N0
  | 2 -> Mc.Npos (parse_positive sigma c.(0))
  | i -> raise ParseError

let dump_n x =
  match x with
  | Mc.N0 -> Lazy.force rocq_N0
  | Mc.Npos p -> EConstr.mkApp (Lazy.force rocq_Npos, [|dump_positive p|])

(** [is_ground_term env sigma term] holds if the term [term]
      is an instance of the typeclass [DeclConstant.GT term]
      i.e. built from user-defined constants and functions.
      NB: This mechanism can be used to customise the reification process to decide
      what to consider as a constant (see [parse_constant])
   *)

let is_declared_term env evd t =
  match EConstr.kind evd t with
  | Const _ | Construct _ -> (
    (* Restrict typeclass resolution to trivial cases *)
    let typ = Retyping.get_type_of env evd t in
    try
      ignore
        (Class_tactics.resolve_one_typeclass env evd
           (EConstr.mkApp (Lazy.force rocq_DeclaredConstant, [|typ; t|])));
      true
    with Not_found -> false )
  | _ -> false

let rec is_ground_term env evd term =
  match EConstr.kind evd term with
  | App (c, args) ->
    is_declared_term env evd c && Array.for_all (is_ground_term env evd) args
  | Const _ | Construct _ -> is_declared_term env evd term
  | _ -> false

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 rocq_ZERO
  | Mc.Zpos p -> EConstr.mkApp (Lazy.force rocq_POS, [|dump_positive p|])
  | Mc.Zneg p -> EConstr.mkApp (Lazy.force rocq_NEG, [|dump_positive p|])


let dump_q q =
  EConstr.mkApp
    ( Lazy.force rocq_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 rocq_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.CPow (x, y) -> Printf.fprintf o "(%a ^ _)" pp_Rcst x
  | 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 rocq_C0
  | Mc.C1 -> Lazy.force rocq_C1
  | Mc.CQ q -> EConstr.mkApp (Lazy.force rocq_CQ, [|dump_q q|])
  | Mc.CZ z -> EConstr.mkApp (Lazy.force rocq_CZ, [|dump_z z|])
  | Mc.CPlus (x, y) ->
    EConstr.mkApp (Lazy.force rocq_CPlus, [|dump_Rcst x; dump_Rcst y|])
  | Mc.CMinus (x, y) ->
    EConstr.mkApp (Lazy.force rocq_CMinus, [|dump_Rcst x; dump_Rcst y|])
  | Mc.CMult (x, y) ->
    EConstr.mkApp (Lazy.force rocq_CMult, [|dump_Rcst x; dump_Rcst y|])
  | Mc.CPow (x, y) ->
    EConstr.mkApp
      ( Lazy.force rocq_CPow
      , [| dump_Rcst x
         ; ( match y with
           | Mc.Inl z ->
             EConstr.mkApp
               ( Lazy.force rocq_Inl
               , [|Lazy.force rocq_Z; Lazy.force rocq_nat; dump_z z|] )
           | Mc.Inr n ->
             EConstr.mkApp
               ( Lazy.force rocq_Inr
               , [|Lazy.force rocq_Z; Lazy.force rocq_nat; dump_nat n|] ) ) |] )
  | Mc.CInv t -> EConstr.mkApp (Lazy.force rocq_CInv, [|dump_Rcst t|])
  | Mc.COpp t -> EConstr.mkApp (Lazy.force rocq_COpp, [|dump_Rcst t|])

let rec dump_list typ dump_elt l =
  match l with
  | [] -> EConstr.mkApp (Lazy.force rocq_nil, [|typ|])
  | e :: l ->
    EConstr.mkApp
      (Lazy.force rocq_cons, [|typ; dump_elt e; dump_list typ dump_elt l|])


let undump_var = parse_positive

let dump_var = dump_positive

let undump_expr undump_constant sigma e =
  let is c c' = EConstr.eq_constr sigma c (Lazy.force c') in
  let rec xundump e =
    match EConstr.kind sigma e with
    | App (c, [|_; n|]) when is c rocq_PEX -> Mc.PEX (undump_var sigma n)
    | App (c, [|_; z|]) when is c rocq_PEc -> Mc.PEc (undump_constant sigma z)
    | App (c, [|_; e1; e2|]) when is c rocq_PEadd ->
      Mc.PEadd (xundump e1, xundump e2)
    | App (c, [|_; e1; e2|]) when is c rocq_PEsub ->
      Mc.PEsub (xundump e1, xundump e2)
    | App (c, [|_; e|]) when is c rocq_PEopp -> Mc.PEopp (xundump e)
    | App (c, [|_; e1; e2|]) when is c rocq_PEmul ->
      Mc.PEmul (xundump e1, xundump e2)
    | App (c, [|_; e; n|]) when is c rocq_PEpow ->
      Mc.PEpow (xundump e, parse_n sigma n)
    | _ -> raise ParseError
  in
  xundump e

let dump_expr typ dump_z e =
  let rec dump_expr e =
    match e with
    | Mc.PEX n -> EConstr.mkApp (Lazy.force rocq_PEX, [|typ; dump_var n|])
    | Mc.PEc z -> EConstr.mkApp (Lazy.force rocq_PEc, [|typ; dump_z z|])
    | Mc.PEadd (e1, e2) ->
      EConstr.mkApp (Lazy.force rocq_PEadd, [|typ; dump_expr e1; dump_expr e2|])
    | Mc.PEsub (e1, e2) ->
      EConstr.mkApp (Lazy.force rocq_PEsub, [|typ; dump_expr e1; dump_expr e2|])
    | Mc.PEopp e -> EConstr.mkApp (Lazy.force rocq_PEopp, [|typ; dump_expr e|])
    | Mc.PEmul (e1, e2) ->
      EConstr.mkApp (Lazy.force rocq_PEmul, [|typ; dump_expr e1; dump_expr e2|])
    | Mc.PEpow (e, n) ->
      EConstr.mkApp (Lazy.force rocq_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 rocq_Pc, [|typ; dump_c n|])
    | Mc.Pinj (p, pol) ->
      EConstr.mkApp (Lazy.force rocq_Pinj, [|typ; dump_positive p; dump_pol pol|])
    | Mc.PX (pol1, p, pol2) ->
      EConstr.mkApp
        ( Lazy.force rocq_PX
        , [|typ; dump_pol pol1; dump_positive p; dump_pol pol2|] )
  in
  dump_pol e


(* let pp_clause pp_c o (f: 'cst clause) =
   List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c)  p Tag.pp t) f *)

let pp_clause_tag o (f : 'cst clause) =
  List.iter (fun ((p, _), (t, _)) -> Printf.fprintf o "(_ @%a)" Tag.pp t) f

(* let pp_cnf pp_c o (f:'cst cnf) =
   List.iter (fun l -> Printf.fprintf o "[%a]" (pp_clause pp_c) l) f *)

let pp_cnf_tag o (f : 'cst cnf) =
  List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause_tag l) f

let dump_psatz typ dump_z e =
  let z = Lazy.force typ in
  let rec dump_cone e =
    match e with
    | Mc.PsatzLet (e1, e2) ->
      EConstr.mkApp (Lazy.force rocq_PsatzLet, [|z; dump_cone e1; dump_cone e2|])
    | Mc.PsatzIn n -> EConstr.mkApp (Lazy.force rocq_PsatzIn, [|z; dump_nat n|])
    | Mc.PsatzMulC (e, c) ->
      EConstr.mkApp
        (Lazy.force rocq_PsatzMultC, [|z; dump_pol z dump_z e; dump_cone c|])
    | Mc.PsatzSquare e ->
      EConstr.mkApp (Lazy.force rocq_PsatzSquare, [|z; dump_pol z dump_z e|])
    | Mc.PsatzAdd (e1, e2) ->
      EConstr.mkApp (Lazy.force rocq_PsatzAdd, [|z; dump_cone e1; dump_cone e2|])
    | Mc.PsatzMulE (e1, e2) ->
      EConstr.mkApp (Lazy.force rocq_PsatzMulE, [|z; dump_cone e1; dump_cone e2|])
    | Mc.PsatzC p -> EConstr.mkApp (Lazy.force rocq_PsatzC, [|z; dump_z p|])
    | Mc.PsatzZ -> EConstr.mkApp (Lazy.force rocq_PsatzZ, [|z|])
  in
  dump_cone e

let undump_op sigma c =
  let i, c = get_left_construct sigma c in
  match i with
  | 1 -> Mc.OpEq
  | 2 -> Mc.OpNEq
  | 3 -> Mc.OpLe
  | 4 -> Mc.OpGe
  | 5 -> Mc.OpLt
  | 6 -> Mc.OpGt
  | _ -> raise ParseError

let dump_op = function
  | Mc.OpEq -> Lazy.force rocq_OpEq
  | Mc.OpNEq -> Lazy.force rocq_OpNEq
  | Mc.OpLe -> Lazy.force rocq_OpLe
  | Mc.OpGe -> Lazy.force rocq_OpGe
  | Mc.OpGt -> Lazy.force rocq_OpGt
  | Mc.OpLt -> Lazy.force rocq_OpLt

let undump_cstr undump_constant sigma c =
  let is c c' = EConstr.eq_constr sigma c (Lazy.force c') in
  match EConstr.kind sigma c with
  | App (c, [|_; e1; o; e2|]) when is c rocq_Build ->
    {Mc.flhs = undump_expr undump_constant sigma e1;
     Mc.fop = undump_op sigma o;
     Mc.frhs = undump_expr undump_constant sigma e2}
  | _ -> raise ParseError

let dump_cstr typ dump_constant {Mc.flhs = e1; Mc.fop = o; Mc.frhs = e2} =
  EConstr.mkApp
    ( Lazy.force rocq_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_prop =
  [ (rocq_Zgt, Mc.OpGt)
  ; (rocq_Zge, Mc.OpGe)
  ; (rocq_Zlt, Mc.OpLt)
  ; (rocq_Zle, Mc.OpLe) ]

let zop_table_bool =
  [ (rocq_Zgtb, Mc.OpGt)
  ; (rocq_Zgeb, Mc.OpGe)
  ; (rocq_Zltb, Mc.OpLt)
  ; (rocq_Zleb, Mc.OpLe)
  ; (rocq_Zeqb, Mc.OpEq) ]

let rop_table_prop =
  [ (rocq_Rgt, Mc.OpGt)
  ; (rocq_Rge, Mc.OpGe)
  ; (rocq_Rlt, Mc.OpLt)
  ; (rocq_Rle, Mc.OpLe) ]

let rop_table_bool = []
let qop_table_prop = [(rocq_Qlt, Mc.OpLt); (rocq_Qle, Mc.OpLe); (rocq_Qeq, Mc.OpEq)]
let qop_table_bool = []

type gl = Environ.env * Evd.evar_map

let is_convertible env sigma t1 t2 = Reductionops.is_conv env sigma t1 t2

let parse_operator table_prop table_bool has_equality typ (env, sigma) k
    (op, args) =
  match args with
  | [|a1; a2|] ->
    ( assoc_const sigma op
        (match k with Mc.IsProp -> table_prop | Mc.IsBool -> table_bool)
    , a1
    , a2 )
  | [|ty; a1; a2|] ->
    if
      has_equality
      && EConstr.eq_constr sigma op (Lazy.force rocq_eq)
      && is_convertible env sigma ty (Lazy.force typ)
    then (Mc.OpEq, args.(1), args.(2))
    else raise ParseError
  | _ -> raise ParseError

let parse_zop = parse_operator zop_table_prop zop_table_bool true rocq_Z
let parse_rop = parse_operator rop_table_prop [] true rocq_R
let parse_qop = parse_operator qop_table_prop [] false rocq_R

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
  type t =
    { vars : (EConstr.t * Mc.kind) list
    ; (* The list represents a mapping from EConstr.t to indexes. *)
      gl : gl (* The evar_map may be updated due to unification of universes *)
    }

  let empty gl = {vars = []; gl}

  (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *)
  let eq_constr (env, sigma) x y =
    match EConstr.eq_constr_universes_proj env sigma x y with
    | Some csts -> (
      let csts = UnivProblem.Set.force csts in
      match Evd.add_universe_constraints sigma csts with
      | sigma -> Some (env, sigma)
      | exception UGraph.UniverseInconsistency _ -> None )
    | None -> None

  let compute_rank_add env v is_prop =
    let rec add gl vars n v =
      match vars with
      | [] -> (gl, [(v, is_prop)], n)
      | (e, b) :: l -> (
        match eq_constr gl e v with
        | Some gl' -> (gl', vars, n)
        | None ->
          let gl, l', n = add gl l (n + 1) v in
          (gl, (e, b) :: l', n) )
    in
    let gl', vars', n = add env.gl env.vars 1 v in
    ({vars = vars'; gl = gl'}, CamlToCoq.positive n)

  let get_rank env v =
    let gl = env.gl in
    let rec get_rank env n =
      match env with
      | [] -> raise (Invalid_argument "get_rank")
      | (e, _) :: l -> (
        match eq_constr gl e v with Some _ -> n | None -> get_rank l (n + 1) )
    in
    get_rank env.vars 1

  let elements env = env.vars

  (* let string_of_env gl env =
     let rec string_of_env i env acc =
       match env with
       | [] -> acc
       | e::env -> string_of_env (i+1) env
                     (IMap.add i
                             (Pp.string_of_ppcmds
                                   (Printer.pr_econstr_env gl.env gl.sigma e)) acc) in
     string_of_env 1 env IMap.empty
  *)
  let pp (genv, sigma) env =
    let ppl =
      List.mapi
        (fun i (e, _) ->
          Pp.str "x"
          ++ Pp.int (i + 1)
          ++ Pp.str ":"
          ++ Printer.pr_econstr_env genv sigma e)
        env
    in
    List.fold_right (fun e p -> e ++ Pp.str " ; " ++ p) ppl (Pp.str "\n")
end

(* MODULE END: Env *)

(**
    * This is the big generic function for expression parsers.
    *)

let parse_expr (genv, sigma) parse_constant parse_exp ops_spec env term =
  if debug then
    Feedback.msg_debug
      (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env genv sigma term);
  let parse_variable env term =
    let env, n = Env.compute_rank_add env term Mc.IsBool 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 (genv, sigma) 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 -> (
            try
              let expr, env = parse_expr env args.(0) in
              let power = parse_exp expr args.(1) in
              (power, env)
            with ParseError ->
              (* if the exponent is a variable *)
              let env, n = Env.compute_rank_add env term Mc.IsBool in
              (Mc.PEX n, env) )
          | Ukn s ->
            if debug then (
              Printf.printf "unknown op: %s\n" s;
              flush stdout );
            let env, n = Env.compute_rank_add env term Mc.IsBool in
            (Mc.PEX n, env) )
        | _ -> parse_variable env term )
      | _ -> parse_variable env term )
  in
  parse_expr env term

let zop_spec =
  [ (rocq_Zplus, Binop (fun x y -> Mc.PEadd (x, y)))
  ; (rocq_Zminus, Binop (fun x y -> Mc.PEsub (x, y)))
  ; (rocq_Zmult, Binop (fun x y -> Mc.PEmul (x, y)))
  ; (rocq_Zopp, Opp)
  ; (rocq_Zpower, Power) ]

let qop_spec =
  [ (rocq_Qplus, Binop (fun x y -> Mc.PEadd (x, y)))
  ; (rocq_Qminus, Binop (fun x y -> Mc.PEsub (x, y)))
  ; (rocq_Qmult, Binop (fun x y -> Mc.PEmul (x, y)))
  ; (rocq_Qopp, Opp)
  ; (rocq_Qpower, Power) ]

let rop_spec =
  [ (rocq_Rplus, Binop (fun x y -> Mc.PEadd (x, y)))
  ; (rocq_Rminus, Binop (fun x y -> Mc.PEsub (x, y)))
  ; (rocq_Rmult, Binop (fun x y -> Mc.PEmul (x, y)))
  ; (rocq_Ropp, Opp)
  ; (rocq_Rpower, Power) ]

let parse_constant parse ((genv : Environ.env), sigma) t = parse sigma t

(** [parse_more_constant parse gl t] returns the reification of term [t].
      If [t] is a ground term, then it is first reduced to normal form
      before using a 'syntactic' parser *)
let parse_more_constant parse (genv, sigma) t =
  try parse (genv, sigma) t
  with ParseError ->
    if debug then Feedback.msg_debug Pp.(str "try harder");
    if is_ground_term genv sigma t then
      parse (genv, sigma) (Redexpr.cbv_vm genv sigma t)
    else raise ParseError

let zconstant = parse_constant parse_z
let qconstant = parse_constant parse_q
let nconstant = parse_constant parse_nat

(** [parse_more_zexpr parse_constant gl] improves the parsing of exponent
      which can be arithmetic expressions (without variables).
      [parse_constant_expr] returns a constant if the argument is an expression without variables. *)

let rec parse_zexpr gl =
  parse_expr gl zconstant
    (fun expr (x : EConstr.t) ->
      let z = parse_zconstant gl x in
      match z with
      | Mc.Zneg _ -> Mc.PEc Mc.Z0
      | _ -> Mc.PEpow (expr, Mc.Z.to_N z))
    zop_spec

and parse_zconstant gl e =
  let e, _ = parse_zexpr gl (Env.empty gl) e in
  match Mc.zeval_const e with None -> raise ParseError | Some z -> z

(* NB: R is a different story.
   Because it is axiomatised, reducing would not be effective.
   Therefore, there is a specific parser for constant over R
*)

let rconst_assoc =
  [ (rocq_Rplus, fun x y -> Mc.CPlus (x, y))
  ; (rocq_Rminus, fun x y -> Mc.CMinus (x, y))
  ; (rocq_Rmult, fun x y -> Mc.CMult (x, y))
    (*      rocq_Rdiv   , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*) ]

let rconstant (genv, sigma) term =
  let rec rconstant term =
    match EConstr.kind sigma term with
    | Const x ->
      if EConstr.eq_constr sigma term (Lazy.force rocq_R0) then Mc.C0
      else if EConstr.eq_constr sigma term (Lazy.force rocq_R1) then Mc.C1
      else raise ParseError
    | App (op, args) -> (
      try
        (* the evaluation order is important in the following *)
        let f = assoc_const sigma op rconst_assoc in
        let a = rconstant args.(0) in
        let b = rconstant args.(1) in
        f a b
      with ParseError -> (
        match op with
        | op when EConstr.eq_constr sigma op (Lazy.force rocq_Rinv) ->
          let arg = rconstant 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 rocq_Rpower) ->
          Mc.CPow
            ( rconstant args.(0)
            , Mc.Inr (parse_more_constant nconstant (genv, sigma) args.(1)) )
        | op when EConstr.eq_constr sigma op (Lazy.force rocq_IQR) ->
          Mc.CQ (qconstant (genv, sigma) args.(0))
        | op when EConstr.eq_constr sigma op (Lazy.force rocq_IZR) ->
          Mc.CZ (parse_more_constant zconstant (genv, sigma) args.(0))
        | _ -> raise ParseError ) )
    | _ -> raise ParseError
  in
  rconstant term

let rconstant (genv, sigma) term =
  if debug then
    Feedback.msg_debug
      (Pp.str "rconstant: " ++ Printer.pr_leconstr_env genv sigma term ++ fnl ());
  let res = rconstant (genv, sigma) term in
  if debug then (
    Printf.printf "rconstant -> %a\n" pp_Rcst res;
    flush stdout );
  res

let parse_qexpr gl =
  parse_expr gl qconstant
    (fun expr x ->
      let exp = zconstant gl x in
      match exp with
      | Mc.Zneg _ -> (
        match expr with
        | Mc.PEc q -> Mc.PEc (Mc.qpower q exp)
        | _ -> raise ParseError )
      | _ ->
        let exp = Mc.Z.to_N exp in
        Mc.PEpow (expr, exp))
    qop_spec

let parse_rexpr (genv, sigma) =
  parse_expr (genv, sigma) rconstant
    (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 (k : Mc.kind) env cstr (genv, sigma) =
  if debug then
    Feedback.msg_debug
      ( Pp.str "parse_arith: "
      ++ Printer.pr_leconstr_env genv sigma cstr
      ++ fnl () );
  match EConstr.kind sigma cstr with
  | App (op, args) ->
    let op, lhs, rhs = parse_op (genv, sigma) k (op, args) in
    let e1, env = parse_expr (genv, sigma) env lhs in
    let e2, env = parse_expr (genv, 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 mkAND b f1 f2 = Mc.AND (b, f1, f2)
let mkOR b f1 f2 = Mc.OR (b, f1, f2)
let mkIff b f1 f2 = Mc.IFF (b, f1, f2)
let mkIMPL b f1 f2 = Mc.IMPL (b, f1, None, f2)
let mkEQ f1 f2 = Mc.EQ (f1, f2)

let mkformula_binary b g term f1 f2 =
  match (f1, f2) with
  | Mc.X (b1, _), Mc.X (b2, _) -> Mc.X (b, term)
  | _ -> g f1 f2

(**
    * This is the big generic function for formula parsers.
    *)

let is_prop env sigma term =
  let sort = Retyping.get_sort_of env sigma term in
  EConstr.ESorts.is_prop sigma sort

type formula_op =
  { op_impl : EConstr.t option (* only for booleans *)
  ; op_and : EConstr.t
  ; op_or : EConstr.t
  ; op_iff : EConstr.t
  ; op_not : EConstr.t
  ; op_tt : EConstr.t
  ; op_ff : EConstr.t }

let prop_op =
  lazy
    { op_impl = None (* implication is Prod *)
    ; op_and = Lazy.force rocq_and
    ; op_or = Lazy.force rocq_or
    ; op_iff = Lazy.force rocq_iff
    ; op_not = Lazy.force rocq_not
    ; op_tt = Lazy.force rocq_True
    ; op_ff = Lazy.force rocq_False }

let bool_op =
  lazy
    { op_impl = Some (Lazy.force rocq_implb)
    ; op_and = Lazy.force rocq_andb
    ; op_or = Lazy.force rocq_orb
    ; op_iff = Lazy.force rocq_eqb
    ; op_not = Lazy.force rocq_negb
    ; op_tt = Lazy.force rocq_true
    ; op_ff = Lazy.force rocq_false }

let is_implb sigma l o =
  match o with None -> false | Some c -> EConstr.eq_constr sigma l c

let parse_formula (genv, sigma) parse_atom env tg term =
  let parse_atom b env tg t =
    try
      let at, env = parse_atom b env t (genv, sigma) in
      (Mc.A (b, at, (tg, t)), env, Tag.next tg)
    with ParseError -> (Mc.X (b, t), env, tg)
  in
  let prop_op = Lazy.force prop_op in
  let bool_op = Lazy.force bool_op in
  let eq = Lazy.force rocq_eq in
  let bool = Lazy.force rocq_bool in
  let rec xparse_formula op k env tg term =
    match EConstr.kind sigma term with
    | App (l, rst) -> (
      match rst with
      | [|a; b|] when is_implb sigma l op.op_impl ->
        let f, env, tg = xparse_formula op k env tg a in
        let g, env, tg = xparse_formula op k env tg b in
        (mkformula_binary k (mkIMPL k) term f g, env, tg)
      | [|a; b|] when EConstr.eq_constr sigma l op.op_and ->
        let f, env, tg = xparse_formula op k env tg a in
        let g, env, tg = xparse_formula op k env tg b in
        (mkformula_binary k (mkAND k) term f g, env, tg)
      | [|a; b|] when EConstr.eq_constr sigma l op.op_or ->
        let f, env, tg = xparse_formula op k env tg a in
        let g, env, tg = xparse_formula op k env tg b in
        (mkformula_binary k (mkOR k) term f g, env, tg)
      | [|a; b|] when EConstr.eq_constr sigma l op.op_iff ->
        let f, env, tg = xparse_formula op k env tg a in
        let g, env, tg = xparse_formula op k env tg b in
        (mkformula_binary k (mkIff k) term f g, env, tg)
      | [|ty; a; b|]
        when EConstr.eq_constr sigma l eq && is_convertible genv sigma ty bool
        ->
        let f, env, tg = xparse_formula bool_op Mc.IsBool env tg a in
        let g, env, tg = xparse_formula bool_op Mc.IsBool env tg b in
        (mkformula_binary Mc.IsProp mkEQ term f g, env, tg)
      | [|a|] when EConstr.eq_constr sigma l op.op_not ->
        let f, env, tg = xparse_formula op k env tg a in
        (Mc.NOT (k, f), env, tg)
      | _ -> parse_atom k env tg term )
    | Prod (typ, a, b)
      when kind_is_prop k
           && (typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b) ->
      let f, env, tg = xparse_formula op k env tg a in
      let g, env, tg = xparse_formula op k env tg b in
      (mkformula_binary Mc.IsProp (mkIMPL Mc.IsProp) term f g, env, tg)
    | _ ->
      if EConstr.eq_constr sigma term op.op_tt then (Mc.TT k, env, tg)
      else if EConstr.eq_constr sigma term op.op_ff then Mc.(FF k, env, tg)
      else (Mc.X (k, term), env, tg)
  in
  xparse_formula prop_op Mc.IsProp env tg (*Reductionops.whd_zeta*) term

(*  let dump_bool b = Lazy.force (if b then rocq_true else rocq_false)*)

let undump_kind sigma k =
  if EConstr.eq_constr sigma k (Lazy.force rocq_IsProp) then Mc.IsProp
  else Mc.IsBool

let dump_kind k =
  Lazy.force (match k with Mc.IsProp -> rocq_IsProp | Mc.IsBool -> rocq_IsBool)

let undump_formula undump_atom tg sigma f =
  let is c c' = EConstr.eq_constr sigma c (Lazy.force c') in
  let kind k = undump_kind sigma k in
  let rec xundump f =
    match EConstr.kind sigma f with
    | App (c, [|_; _; _; _; k|]) when is c rocq_TT -> Mc.TT (kind k)
    | App (c, [|_; _; _; _; k|]) when is c rocq_FF -> Mc.FF (kind k)
    | App (c, [|_; _; _; _; k; f1; f2|]) when is c rocq_AND ->
      Mc.AND (kind k, xundump f1, xundump f2)
    | App (c, [|_; _; _; _; k; f1; f2|]) when is c rocq_OR ->
      Mc.OR (kind k, xundump f1, xundump f2)
    | App (c, [|_; _; _; _; k; f1; _; f2|]) when is c rocq_IMPL ->
      Mc.IMPL (kind k, xundump f1, None, xundump f2)
    | App (c, [|_; _; _; _; k; f|]) when is c rocq_NOT ->
      Mc.NOT (kind k, xundump f)
    | App (c, [|_; _; _; _; k; f1; f2|]) when is c rocq_IFF ->
      Mc.IFF (kind k, xundump f1, xundump f2)
    | App (c, [|_; _; _; _; f1; f2|]) when is c rocq_EQ ->
      Mc.EQ (xundump f1, xundump f2)
    | App (c, [|_; _; _; _; k; x; _|]) when is c rocq_Atom ->
      Mc.A (kind k, undump_atom sigma x, tg)
    | App (c, [|_; _; _; _; k; x|]) when is c rocq_X ->
      Mc.X (kind k, x)
    | _ -> raise ParseError
  in
  xundump f

let dump_formula typ dump_atom f =
  let app_ctor c args =
    EConstr.mkApp
      ( Lazy.force c
      , Array.of_list
          ( typ :: Lazy.force rocq_eKind :: Lazy.force rocq_unit
          :: Lazy.force rocq_unit :: args ) )
  in
  let rec xdump f =
    match f with
    | Mc.TT k -> app_ctor rocq_TT [dump_kind k]
    | Mc.FF k -> app_ctor rocq_FF [dump_kind k]
    | Mc.AND (k, x, y) -> app_ctor rocq_AND [dump_kind k; xdump x; xdump y]
    | Mc.OR (k, x, y) -> app_ctor rocq_OR [dump_kind k; xdump x; xdump y]
    | Mc.IMPL (k, x, _, y) ->
      app_ctor rocq_IMPL
        [ dump_kind k
        ; xdump x
        ; EConstr.mkApp (Lazy.force rocq_None, [|Lazy.force rocq_unit|])
        ; xdump y ]
    | Mc.NOT (k, x) -> app_ctor rocq_NOT [dump_kind k; xdump x]
    | Mc.IFF (k, x, y) -> app_ctor rocq_IFF [dump_kind k; xdump x; xdump y]
    | Mc.EQ (x, y) -> app_ctor rocq_EQ [xdump x; xdump y]
    | Mc.A (k, x, _) ->
      app_ctor rocq_Atom [dump_kind k; dump_atom x; Lazy.force rocq_tt]
    | Mc.X (k, t) -> app_ctor rocq_X [dump_kind k; t]
  in
  xdump f

let prop_env_of_formula gl form =
  Mc.(
    let rec doit env = function
      | TT _ | FF _ | A (_, _, _) -> env
      | X (b, t) -> fst (Env.compute_rank_add env t b)
      | AND (b, f1, f2) | OR (b, f1, f2) | IMPL (b, f1, _, f2) | IFF (b, f1, f2)
        ->
        doit (doit env f1) f2
      | NOT (b, f) -> doit env f
      | EQ (f1, f2) -> doit (doit env f1) f2
    in
    doit (Env.empty gl) 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
  Mc.(
    let rec doit = function
      | TT _ | FF _ | X _ -> ISet.empty
      | A (_, a, (t, c)) -> vars_of_atom a
      | AND (_, f1, f2)
       |OR (_, f1, f2)
       |IMPL (_, f1, _, f2)
       |IFF (_, f1, f2)
       |EQ (f1, f2) ->
        ISet.union (doit f1) (doit f2)
      | NOT (_, 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_prop : (Mc.op2 * EConstr.constr) list
  ; dump_op_bool : (Mc.op2 * EConstr.constr) list }

let dump_zexpr =
  lazy
    { interp_typ = Lazy.force rocq_Z
    ; dump_cst = dump_z
    ; dump_add = Lazy.force rocq_Zplus
    ; dump_sub = Lazy.force rocq_Zminus
    ; dump_opp = Lazy.force rocq_Zopp
    ; dump_mul = Lazy.force rocq_Zmult
    ; dump_pow = Lazy.force rocq_Zpower
    ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)))
    ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_prop
    ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_bool
    }

let dump_qexpr =
  lazy
    { interp_typ = Lazy.force rocq_Q
    ; dump_cst = dump_q
    ; dump_add = Lazy.force rocq_Qplus
    ; dump_sub = Lazy.force rocq_Qminus
    ; dump_opp = Lazy.force rocq_Qopp
    ; dump_mul = Lazy.force rocq_Qmult
    ; dump_pow = Lazy.force rocq_Qpower
    ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)))
    ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_prop
    ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_bool
    }

let rec dump_Rcst_as_R cst =
  match cst with
  | Mc.C0 -> Lazy.force rocq_R0
  | Mc.C1 -> Lazy.force rocq_R1
  | Mc.CQ q -> EConstr.mkApp (Lazy.force rocq_IQR, [|dump_q q|])
  | Mc.CZ z -> EConstr.mkApp (Lazy.force rocq_IZR, [|dump_z z|])
  | Mc.CPlus (x, y) ->
    EConstr.mkApp (Lazy.force rocq_Rplus, [|dump_Rcst_as_R x; dump_Rcst_as_R y|])
  | Mc.CMinus (x, y) ->
    EConstr.mkApp (Lazy.force rocq_Rminus, [|dump_Rcst_as_R x; dump_Rcst_as_R y|])
  | Mc.CMult (x, y) ->
    EConstr.mkApp (Lazy.force rocq_Rmult, [|dump_Rcst_as_R x; dump_Rcst_as_R y|])
  | Mc.CPow (x, y) -> (
    match y with
    | Mc.Inl z ->
      EConstr.mkApp (Lazy.force rocq_powerZR, [|dump_Rcst_as_R x; dump_z z|])
    | Mc.Inr n ->
      EConstr.mkApp (Lazy.force rocq_Rpower, [|dump_Rcst_as_R x; dump_nat n|]) )
  | Mc.CInv t -> EConstr.mkApp (Lazy.force rocq_Rinv, [|dump_Rcst_as_R t|])
  | Mc.COpp t -> EConstr.mkApp (Lazy.force rocq_Ropp, [|dump_Rcst_as_R t|])

let dump_rexpr =
  lazy
    { interp_typ = Lazy.force rocq_R
    ; dump_cst = dump_Rcst_as_R
    ; dump_add = Lazy.force rocq_Rplus
    ; dump_sub = Lazy.force rocq_Rminus
    ; dump_opp = Lazy.force rocq_Ropp
    ; dump_mul = Lazy.force rocq_Rmult
    ; dump_pow = Lazy.force rocq_Rpower
    ; dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n)))
    ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_prop
    ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_bool
    }

let prodn n env b =
  let rec prodrec = function
    | 0, env, b -> b
    | n, (v, t) :: l, b ->
      prodrec (n - 1, l, EConstr.mkProd (make_annot v ERelevance.relevant, t, b))
    | _ -> assert false
  in
  prodrec (n, env, b)

(** [make_goal_of_formula depxr vars props form] where
     - vars is an environment for the arithmetic variables occurring in form
     - props is an environment for the propositions occurring in form
    @return a goal where all the variables and propositions of the formula are quantified

*)

let eKind = function
  | Mc.IsProp -> EConstr.mkProp
  | Mc.IsBool -> Lazy.force rocq_bool

let make_goal_of_formula gl 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 gl form in
  let fresh_var str i = Names.Id.of_string (str ^ string_of_int i) in
  let fresh_prop str i = Names.Id.of_string (str ^ string_of_int i) in
  let vars_n =
    List.map (fun (_, i) -> (fresh_var "__x" i, dexpr.interp_typ)) vars_idx
  in
  let props_n =
    List.mapi
      (fun i (_, k) -> (fresh_prop "__p" (i + 1), eKind k))
      (Env.elements props)
  in
  let var_name_pos =
    List.fold_left2 (fun acc (idx, _) (id, _) -> (id, idx) :: acc) [] 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_prop op e1 e2 =
    try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|])
    with Not_found ->
      EConstr.mkApp (Lazy.force rocq_eq, [|dexpr.interp_typ; e1; e2|])
  in
  let dump_cstr_prop i {Mc.flhs; Mc.fop; Mc.frhs} =
    mkop_prop fop (dump_expr i flhs) (dump_expr i frhs)
  in
  let mkop_bool op e1 e2 =
    try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|])
    with Not_found ->
      EConstr.mkApp (Lazy.force rocq_eq, [|dexpr.interp_typ; e1; e2|])
  in
  let dump_cstr_bool i {Mc.flhs; Mc.fop; Mc.frhs} =
    mkop_bool fop (dump_expr i flhs) (dump_expr i frhs)
  in
  let rec xdump_prop pi xi f =
    match f with
    | Mc.TT _ -> Lazy.force rocq_True
    | Mc.FF _ -> Lazy.force rocq_False
    | Mc.AND (_, x, y) ->
      EConstr.mkApp
        (Lazy.force rocq_and, [|xdump_prop pi xi x; xdump_prop pi xi y|])
    | Mc.OR (_, x, y) ->
      EConstr.mkApp
        (Lazy.force rocq_or, [|xdump_prop pi xi x; xdump_prop pi xi y|])
    | Mc.IFF (_, x, y) ->
      EConstr.mkApp
        (Lazy.force rocq_iff, [|xdump_prop pi xi x; xdump_prop pi xi y|])
    | Mc.IMPL (_, x, _, y) ->
      EConstr.mkArrow (xdump_prop pi xi x) ERelevance.relevant
        (xdump_prop (pi + 1) (xi + 1) y)
    | Mc.NOT (_, x) ->
      EConstr.mkArrow (xdump_prop pi xi x) ERelevance.relevant (Lazy.force rocq_False)
    | Mc.EQ (x, y) ->
      EConstr.mkApp
        ( Lazy.force rocq_eq
        , [|Lazy.force rocq_bool; xdump_bool pi xi x; xdump_bool pi xi y|] )
    | Mc.A (_, x, _) -> dump_cstr_prop xi x
    | Mc.X (_, t) ->
      let idx = Env.get_rank props t in
      EConstr.mkRel (pi + idx)
  and xdump_bool pi xi f =
    match f with
    | Mc.TT _ -> Lazy.force rocq_true
    | Mc.FF _ -> Lazy.force rocq_false
    | Mc.AND (_, x, y) ->
      EConstr.mkApp
        (Lazy.force rocq_andb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
    | Mc.OR (_, x, y) ->
      EConstr.mkApp
        (Lazy.force rocq_orb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
    | Mc.IFF (_, x, y) ->
      EConstr.mkApp
        (Lazy.force rocq_eqb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
    | Mc.IMPL (_, x, _, y) ->
      EConstr.mkApp
        (Lazy.force rocq_implb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
    | Mc.NOT (_, x) ->
      EConstr.mkApp (Lazy.force rocq_negb, [|xdump_bool pi xi x|])
    | Mc.EQ (x, y) -> assert false
    | Mc.A (_, x, _) -> dump_cstr_bool xi x
    | Mc.X (_, t) ->
      let idx = Env.get_rank props 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 p in
    EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx))
  in
  let form' = Mc.mapX (fun _ p -> subst_prop p) Mc.IsProp 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_prop (List.length vars_n) 0 form))
  , List.rev props_n
  , 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 sigma l concl =
  let rec xset acc = function
    | [] -> acc
    | e :: l ->
      let name, expr, typ = e in
      xset
        (EConstr.mkNamedLetIn sigma
           (make_annot (Names.Id.of_string name) ERelevance.relevant)
           expr typ acc)
        l
  in
  xset concl l

let rocq_Branch = lazy (constr_of_ref "micromega.VarMap.Branch")
let rocq_Elt = lazy (constr_of_ref "micromega.VarMap.Elt")
let rocq_Empty = lazy (constr_of_ref "micromega.VarMap.Empty")
let rocq_VarMap = lazy (constr_of_ref "micromega.VarMap.type")

let rec dump_varmap typ m =
  match m with
  | Mc.Empty -> EConstr.mkApp (Lazy.force rocq_Empty, [|typ|])
  | Mc.Elt v -> EConstr.mkApp (Lazy.force rocq_Elt, [|typ; v|])
  | Mc.Branch (l, o, r) ->
    EConstr.mkApp
      (Lazy.force rocq_Branch, [|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 rocq_doneProof
  | Micromega.RatProof (cone, rst) ->
    EConstr.mkApp
      ( Lazy.force rocq_ratProof
      , [|dump_psatz rocq_Z dump_z cone; dump_proof_term rst|] )
  | Micromega.CutProof (cone, prf) ->
    EConstr.mkApp
      ( Lazy.force rocq_cutProof
      , [|dump_psatz rocq_Z dump_z cone; dump_proof_term prf|] )
  | Micromega.SplitProof (p, prf1, prf2) ->
    EConstr.mkApp
      ( Lazy.force rocq_splitProof
      , [| dump_pol (Lazy.force rocq_Z) dump_z p
         ; dump_proof_term prf1
         ; dump_proof_term prf2 |] )
  | Micromega.EnumProof (c1, c2, prfs) ->
    EConstr.mkApp
      ( Lazy.force rocq_enumProof
      , [| dump_psatz rocq_Z dump_z c1
         ; dump_psatz rocq_Z dump_z c2
         ; dump_list (Lazy.force rocq_proofTerm) dump_proof_term prfs |] )
  | Micromega.ExProof (p, prf) ->
    EConstr.mkApp
      (Lazy.force rocq_ExProof, [|dump_positive p; dump_proof_term prf|])

let rec size_of_psatz = function
  | Micromega.PsatzIn _ -> 1
  | Micromega.PsatzSquare _ -> 1
  | Micromega.PsatzMulC (_, p) -> 1 + size_of_psatz p
  | Micromega.PsatzLet (p1, p2)
   |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.SplitProof (_, p1, p2) -> size_of_pf p1 + size_of_pf p2
  | 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
  | Micromega.ExProof (_, a) -> size_of_pf a + 1

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 parse_hyps (genv, sigma) parse_arith env tg (hyps:(Names.Id.t * EConstr.types) list) =
  match hyps with
  | [] -> ([], env, tg)
  | (i, t) :: l ->
    let lhyps, env, tg = parse_hyps (genv, sigma) parse_arith env tg l in
    if is_prop genv sigma t then
      try
        let c, env, tg = parse_formula (genv, sigma) parse_arith env tg t in
        ((i, c) :: lhyps, env, tg)
      with ParseError -> (lhyps, env, tg)
    else (lhyps, env, tg)

let parse_goal gl parse_arith (env : Env.t) (hyps:(Names.Id.t * EConstr.types) list) term =
  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)

(**
  * 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
  ; undump_coeff : Evd.evar_map -> EConstr.constr -> 'synt_c
  ; proof_typ : EConstr.constr
  ; dump_proof : 'prf -> EConstr.constr
  ; coeff_eq : 'synt_c -> 'synt_c -> bool }

let zz_domain_spec =
  lazy
    { typ = Lazy.force rocq_Z
    ; coeff = Lazy.force rocq_Z
    ; dump_coeff = dump_z
    ; undump_coeff = parse_z
    ; proof_typ = Lazy.force rocq_proofTerm
    ; dump_proof = dump_proof_term
    ; coeff_eq = Mc.Z.eqb }

let qq_domain_spec =
  lazy
    { typ = Lazy.force rocq_Q
    ; coeff = Lazy.force rocq_Q
    ; dump_coeff = dump_q
    ; undump_coeff = parse_q
    ; proof_typ = Lazy.force rocq_QWitness
    ; dump_proof = dump_psatz rocq_Q dump_q
    ; coeff_eq = Mc.qeq_bool }

let max_tag f =
  1
  + Tag.to_int
      (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) Mc.IsProp f (Tag.from 0))

(** 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) *)

(**
  * Instantiate the current Rocq 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 rocq_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.enter (fun gl ->
    let sigma = Proofview.Goal.sigma gl in
      Tacticals.tclTHENLIST
        [ Tactics.change_concl
            (set sigma
               [ ( "__ff"
                 , ff
                 , EConstr.mkApp
                     ( Lazy.force rocq_Formula
                     , [|formula_typ; Lazy.force rocq_IsProp|] ) )
               ; ( "__varmap"
                 , vm
                 , EConstr.mkApp (Lazy.force rocq_VarMap, [|spec.typ|]) )
               ; ("__wit", cert, cert_typ) ]
               (Tacmach.pf_concl gl)) ])

(**
  * The datastructures that aggregate prover attributes.
  *)

open Certificate

type ('option, 'a, 'prf, 'model) prover =
  { name : string
  ; (* name of the prover *)
    get_option : unit -> 'option
  ; (* find the options of the prover *)
    prover : 'option * 'a list -> ('prf, 'model) Certificate.res
  ; (* 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  prover 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 p polys1 =
  let polys1 = List.map fst polys1 in
  p.prover (p.get_option (), polys1)

(**
  * Given a prover 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 stack l =
    match stack with
    | [] -> Prf l
    | e :: stack ->
      match find_witness prover e with
      | Model m -> (Model (m, e))
      | Unknown -> Unknown
      | Prf w -> xwitness_list stack (w :: l)
  in
  xwitness_list (List.rev l) []

(*  let t1 = System.get_time () in
  let res = witness_list p g in
  let t2 = System.get_time () in
  Feedback.msg_info Pp.(str "Witness generation "++int (List.length g) ++ str " "++System.fmt_time_difference t1 t2) ;
  res
 *)

(**
  * Prune the proof object, according to the 'diff' between two cnf formulas.
  *)

let compact_proofs prover (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) res
    (cnf_ff' : 'cst cnf) =
  let eq_formula (p1, o1) (p2, o2) =
    let open Mutils.Hash in
    eq_pol eq_cst p1 p2 && eq_op1 o1 o2
  in
  let compact_proof (old_cl : 'cst clause) prf (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
      CList.assoc_f eq_formula 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
        | Unknown | Model _ -> failwith "proof compaction error"
        | Prf p -> p )
    in
    if debug then begin
      Printf.printf " -> %a\n" prover.pp_prf res;
      flush stdout
    end;
    res
  in
  let is_proof_compatible (hyps, (old_cl : 'cst clause), prf) (new_cl : 'cst clause) =
    let eq (f1, (t1, e1)) (f2, (t2, e2)) =
      Int.equal (Tag.compare t1 t2) 0
      && eq_formula f1 f2
      (* We do not have to compare [e1] with [e2] because [t1 = t2] ensures
         by uid generation that they must be the same *)
    in
    is_sublist eq (Lazy.force hyps) new_cl
  in
  let map acc cl prf =
    let hyps = lazy (selecti (prover.hyps prf) cl) in
    (hyps, cl, prf) :: acc
  in
  let cnf_res = List.rev (List.fold_left2 map [] cnf_ff res) in
  (* we get pairs clause * proof *)
  if debug then begin
    Printf.printf "CNFRES\n";
    flush stdout;
    Printf.printf "CNFOLD %a\n" pp_cnf_tag cnf_ff;
    List.iter
      (fun (lazy hyps, cl, prf) ->
        Printf.printf "\nProver %a -> %a\n" pp_clause_tag cl pp_clause_tag hyps;
        flush stdout)
      cnf_res;
    Printf.printf "CNFNEW %a\n" pp_cnf_tag cnf_ff'
  end;
  List.map
    (fun x ->
      let _, o, p =
        try List.find (fun p -> is_proof_compatible p x) cnf_res
        with Not_found ->
          Printf.printf "ERROR: no compatible proof";
          flush stdout;
          failwith "Cannot find compatible proof"
      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 : TagSet.t -> 'a formula -> 'a formula =
 fun hyps f ->
  let to_constr =
    Mc.
      { mkTT =
          (let rocq_True = Lazy.force rocq_True in
           let rocq_true = Lazy.force rocq_true in
           function Mc.IsProp -> rocq_True | Mc.IsBool -> rocq_true)
      ; mkFF =
          (let rocq_False = Lazy.force rocq_False in
           let rocq_false = Lazy.force rocq_false in
           function Mc.IsProp -> rocq_False | Mc.IsBool -> rocq_false)
      ; mkA = (fun k a (tg, t) -> t)
      ; mkAND =
          (let rocq_and = Lazy.force rocq_and in
           let rocq_andb = Lazy.force rocq_andb in
           fun k x y ->
             EConstr.mkApp
               ( (match k with Mc.IsProp -> rocq_and | Mc.IsBool -> rocq_andb)
               , [|x; y|] ))
      ; mkOR =
          (let rocq_or = Lazy.force rocq_or in
           let rocq_orb = Lazy.force rocq_orb in
           fun k x y ->
             EConstr.mkApp
               ( (match k with Mc.IsProp -> rocq_or | Mc.IsBool -> rocq_orb)
               , [|x; y|] ))
      ; mkIMPL =
          (fun k x y ->
            match k with
            | Mc.IsProp -> EConstr.mkArrow x ERelevance.relevant y
            | Mc.IsBool -> EConstr.mkApp (Lazy.force rocq_implb, [|x; y|]))
      ; mkIFF =
          (let rocq_iff = Lazy.force rocq_iff in
           let rocq_eqb = Lazy.force rocq_eqb in
           fun k x y ->
             EConstr.mkApp
               ( (match k with Mc.IsProp -> rocq_iff | Mc.IsBool -> rocq_eqb)
               , [|x; y|] ))
      ; mkNOT =
          (let rocq_not = Lazy.force rocq_not in
           let rocq_negb = Lazy.force rocq_negb in
           fun k x ->
             EConstr.mkApp
               ( (match k with Mc.IsProp -> rocq_not | Mc.IsBool -> rocq_negb)
               , [|x|] ))
      ; mkEQ =
          (let rocq_eq = Lazy.force rocq_eq in
           fun x y -> EConstr.mkApp (rocq_eq, [|Lazy.force rocq_bool; x; y|])) }
  in
  Mc.abst_form to_constr (fun (t, _) -> TagSet.mem t hyps) true Mc.IsProp f

(* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2   *)
let rec abstract_wrt_formula f1 f2 =
  Mc.(
    match (f1, f2) with
    | X (b, c), _ -> X (b, c)
    | A _, A _ -> f2
    | AND (b, f1, f2), AND (_, f1', f2') ->
      AND (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
    | OR (b, f1, f2), OR (_, f1', f2') ->
      OR (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
    | IMPL (b, f1, _, f2), IMPL (_, f1', x, f2') ->
      IMPL (b, abstract_wrt_formula f1 f1', x, abstract_wrt_formula f2 f2')
    | IFF (b, f1, f2), IFF (_, f1', f2') ->
      IFF (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
    | EQ (f1, f2), EQ (f1', f2') ->
      EQ (abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
    | FF b, FF _ -> FF b
    | TT b, TT _ -> TT b
    | NOT (b, x), NOT (_, y) -> NOT (b, abstract_wrt_formula x y)
    | _ -> failwith "abstract_wrt_formula")

(**
  * This exception is raised by really_call_csdpcert if Rocq's configure didn't
  * find a CSDP executable.
  *)

exception CsdpNotFound

let fail_csdp_not_found () =
  flush stdout;
  let s =
    "Skipping the rest of this tactic: the complexity of the \
     goal requires the use of an external tool called CSDP. \n\n\
     However, the \"csdp\" binary is not present in the search path. \n\n\
     Some OS distributions include CSDP (package \"coinor-csdp\" on Debian \
     for instance). You can download binaries \
     and source code from <https://github.com/coin-or/csdp>." in
  Tacticals.tclFAIL (Pp.str s)

(**
  * 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
      | Mc.X _ -> (cc, ids)
      | _ -> (Mc.IMPL (Mc.IsProp, f, Some id, cc), id :: ids))
    hyps (concl, [])

(* let time str f x =
  let t1 = System.get_time () in
  let res = f x in
  let t2 = System.get_time () in
  Feedback.msg_info (Pp.str str ++ Pp.str " " ++ System.fmt_time_difference t1 t2) ;
  res
 *)

let rec fold_trace f accu tr =
  let open Micromega in
  match tr with
  | Null -> accu
  | Push (x, t) -> fold_trace f (f accu x) t
  | Merge (Null, t2) -> fold_trace f accu t2
  | Merge (Push (x, t1), t2) -> fold_trace f (f accu x) (Merge (t1, t2))
  | Merge (Merge (t1, t2), t3) -> fold_trace f accu (Merge (t1, Merge (t2, t3)))

let micromega_tauto ?(abstract=true) pre_process cnf spec prover
    (polys1 : (Names.Id.t * 'cst formula) list) (polys2 : 'cst formula) =
  (* Express the goal as one big implication *)
  let ff, ids = formula_hyps_concl polys1 polys2 in
  let mt = CamlToCoq.positive (max_tag ff) in
  (* Construction of cnf *)
  let pre_ff = pre_process mt (ff : 'a formula) in
  let cnf_ff, cnf_ff_tags = cnf Mc.IsProp pre_ff in
  match witness_list prover cnf_ff with
  | Model m -> Model m
  | Unknown -> Unknown
  | Prf res ->
--> --------------------

--> maximum size reached

--> --------------------