diff options
Diffstat (limited to 'src/trace')
| -rw-r--r-- | src/trace/coqInterface.ml | 191 | ||||
| -rw-r--r-- | src/trace/coqInterface.mli | 111 | ||||
| -rw-r--r-- | src/trace/coqTerms.ml | 636 | ||||
| -rw-r--r-- | src/trace/coqTerms.mli | 515 | ||||
| -rw-r--r-- | src/trace/satAtom.ml | 6 | ||||
| -rw-r--r-- | src/trace/satAtom.mli | 12 | ||||
| -rw-r--r-- | src/trace/smtAtom.ml | 64 | ||||
| -rw-r--r-- | src/trace/smtAtom.mli | 28 | ||||
| -rw-r--r-- | src/trace/smtBtype.ml | 44 | ||||
| -rw-r--r-- | src/trace/smtBtype.mli | 28 | ||||
| -rw-r--r-- | src/trace/smtCertif.ml | 4 | ||||
| -rw-r--r-- | src/trace/smtCertif.mli | 4 | ||||
| -rw-r--r-- | src/trace/smtCommands.ml | 542 | ||||
| -rw-r--r-- | src/trace/smtCommands.mli | 22 | ||||
| -rw-r--r-- | src/trace/smtForm.ml | 84 | ||||
| -rw-r--r-- | src/trace/smtForm.mli | 20 | ||||
| -rw-r--r-- | src/trace/smtMisc.ml | 12 | ||||
| -rw-r--r-- | src/trace/smtMisc.mli | 10 | ||||
| -rw-r--r-- | src/trace/smtTrace.ml | 22 | ||||
| -rw-r--r-- | src/trace/smtTrace.mli | 38 |
20 files changed, 1436 insertions, 957 deletions
diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml new file mode 100644 index 0000000..9b2c72c --- /dev/null +++ b/src/trace/coqInterface.ml @@ -0,0 +1,191 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2022 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +open Entries + + +(* Constr generation and manipulation *) +type id = Names.variable +let mkId = Names.Id.of_string + + +type name = Names.Name.t +let name_of_id i = Names.Name i +let mkName s = + let id = mkId s in + name_of_id id +let string_of_name = function + Names.Name id -> Names.Id.to_string id + | _ -> failwith "unnamed rel" + + +type constr = Constr.t +type types = Constr.types +let eq_constr = Constr.equal +let hash_constr = Constr.hash +let mkProp = Constr.mkProp +let mkConst = Constr.mkConst +let mkVar = Constr.mkVar +let mkRel = Constr.mkRel +let isRel = Constr.isRel +let destRel = Constr.destRel +let lift = Vars.lift +let mkApp = Constr.mkApp +let decompose_app = Constr.decompose_app +let mkLambda (n, t, c) = Constr.mkLambda (Context.make_annot n Sorts.Relevant, t, c) +let mkProd (n, t, c) = Constr.mkProd (Context.make_annot n Sorts.Relevant, t, c) +let mkLetIn (n, c1, t, c2) = Constr.mkLetIn (Context.make_annot n Sorts.Relevant, c1, t, c2) +let mkArrow a b = Term.mkArrow a Sorts.Relevant b + +let pr_constr_env env = Printer.pr_constr_env env Evd.empty +let pr_constr = pr_constr_env Environ.empty_env + + +let mkUConst : Constr.t -> Safe_typing.private_constants Entries.definition_entry = fun c -> + let env = Global.env () in + let evd = Evd.from_env env in + let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in + { Entries.const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), + Safe_typing.empty_private_constants); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *) + const_entry_universes = Evd.univ_entry ~poly:false evd; + const_entry_opaque = false; + const_entry_inline_code = false } + +let mkTConst c noc ty = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in + { const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), + Safe_typing.empty_private_constants); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = Some ty; + const_entry_universes = Evd.univ_entry ~poly:false evd; + const_entry_opaque = false; + const_entry_inline_code = false } + +(* TODO : Set -> Type *) +let declare_new_type t = + let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_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 ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in + Constr.mkVar v + +let declare_constant n c = + Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition) + + + +type cast_kind = Constr.cast_kind +let vmcast = Constr.VMcast +let mkCast = Constr.mkCast + + +(* EConstr *) +type econstr = EConstr.t +let econstr_of_constr = EConstr.of_constr + + +(* Int63 *) +let mkInt : int -> Constr.constr = + fun i -> Constr.mkInt (Uint63.of_int i) + + +(* PArray *) +let max_array_size : int = 4194302 + + +(* Traces *) +(* WARNING: side effect on r! *) +let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = + let rec mkTrace s = + if s = size then + mkApp (Lazy.force cnil, [|step|]) + else ( + r := next !r; + let st = step_to_coq !r in + mkApp (Lazy.force ccons, [|step; st; mkTrace (s+1)|]) + ) in + mkApp (Lazy.force cpair, [|mkApp (Lazy.force clist, [|step|]); step; mkTrace 0; def_step|]) + + +(* Micromega *) +module Micromega_plugin_Micromega = Micromega_plugin.Micromega +module Micromega_plugin_Certificate = Micromega_plugin.Certificate + +let micromega_dump_proof_term p = + (* Cannot contain evars *) + EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p) + + +(* Tactics *) +type tactic = unit Proofview.tactic +let tclTHEN = Tacticals.New.tclTHEN +let tclTHENLAST = Tacticals.New.tclTHENLAST +let assert_before n c = Tactics.assert_before n (EConstr.of_constr c) + +let vm_cast_no_check c = Tactics.vm_cast_no_check (EConstr.of_constr c) + +let mk_tactic tac = + Proofview.Goal.enter (fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let t = Proofview.Goal.concl gl in + let t = EConstr.to_constr sigma t in (* The goal should not contain uninstanciated evars *) + tac env sigma t + ) +let set_evars_tac noc = + mk_tactic ( + fun env sigma _ -> + let sigma, _ = Typing.type_of env sigma (EConstr.of_constr noc) in + Proofview.Unsafe.tclEVARS sigma) + + +(* Other differences between the two versions of Coq *) +type constr_expr = Constrexpr.constr_expr +let error s = CErrors.user_err (Pp.str s) +let warning n s = CWarnings.create ~name:n ~category:"SMTCoq plugin" Pp.str s + +let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c) + +let destruct_rel_decl r = Context.Rel.Declaration.get_name r, + Context.Rel.Declaration.get_type r + +(* Cannot contain evars since it comes from a Constr.t *) +let interp_constr env sigma t = Constrintern.interp_constr env sigma t |> fst |> EConstr.Unsafe.to_constr + +let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr + +let constrextern_extern_constr c = + let env = Global.env () in + Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c) + +let get_rel_dec_name = function + | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> + Context.binder_name n + +let retyping_get_type_of env sigma c = + (* Cannot contain evars since it comes from a Constr.t *) + EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)) + +let vm_conv = Vconv.vm_conv + +(* Cannot contain evars since it comes from a Constr.t *) +let cbv_vm env c t = EConstr.Unsafe.to_constr (Vnorm.cbv_vm env Evd.empty (EConstr.of_constr c) (EConstr.of_constr t)) diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli new file mode 100644 index 0000000..0536ef1 --- /dev/null +++ b/src/trace/coqInterface.mli @@ -0,0 +1,111 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2022 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +(* WARNING: currently, we map all the econstr into constr: we suppose + that the goal does not contain existencial variables *) + +(* Constr generation and manipulation *) +type id = Names.variable +val mkId : string -> id + +type name +val name_of_id : id -> name +val mkName : string -> name +val string_of_name : name -> string + +type constr = Constr.t +type types = constr +val eq_constr : constr -> constr -> bool +val hash_constr : constr -> int +val mkProp : types +val mkConst : Names.Constant.t -> constr +val mkVar : id -> constr +val mkRel : int -> constr +val isRel : constr -> bool +val destRel : constr -> int +val lift : int -> constr -> constr +val mkApp : constr * constr array -> constr +val decompose_app : constr -> constr * constr list +val mkLambda : name * types * constr -> constr +val mkProd : name * types * types -> types +val mkLetIn : name * constr * types * constr -> constr +val mkArrow : types -> types -> constr + +val pr_constr_env : Environ.env -> constr -> Pp.t +val pr_constr : constr -> Pp.t + +val mkUConst : constr -> Safe_typing.private_constants Entries.definition_entry +val mkTConst : constr -> constr -> types -> Safe_typing.private_constants Entries.definition_entry +val declare_new_type : id -> types +val declare_new_variable : id -> types -> constr +val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t + +type cast_kind +val vmcast : cast_kind +val mkCast : constr * cast_kind * constr -> constr + + +(* EConstr *) +type econstr = EConstr.t +val econstr_of_constr : constr -> econstr + + +(* Int63 *) +val mkInt : int -> constr + + +(* PArray *) +val max_array_size : int + + +(* Traces *) +val mkTrace : + ('a -> constr) -> + ('a -> 'a) -> + 'b -> + constr Lazy.t -> + constr Lazy.t -> + constr Lazy.t -> + constr Lazy.t -> + int -> constr -> constr -> 'a ref -> constr + + +(* Micromega *) +module Micromega_plugin_Micromega = Micromega_plugin.Micromega +module Micromega_plugin_Certificate = Micromega_plugin.Certificate +val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr + + +(* Tactics *) +type tactic = unit Proofview.tactic +val tclTHEN : tactic -> tactic -> tactic +val tclTHENLAST : tactic -> tactic -> tactic +val assert_before : name -> types -> tactic +val vm_cast_no_check : constr -> tactic +val mk_tactic : (Environ.env -> Evd.evar_map -> constr -> tactic) -> tactic +val set_evars_tac : constr -> tactic + + +(* Other differences between the two versions of Coq *) +type constr_expr = Constrexpr.constr_expr +val error : string -> 'a +val warning : string -> string -> unit +val extern_constr : constr -> constr_expr +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_gram.tolerability +val constrextern_extern_constr : constr -> constr_expr +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 +val cbv_vm : Environ.env -> constr -> types -> constr diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index dcacd4b..87a21b8 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -10,280 +10,374 @@ (**************************************************************************) -open Coqlib open SmtMisc -let gen_constant = Structures.gen_constant +type coqTerm = CoqInterface.constr lazy_t + +let gc prefix constant = + lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref (prefix ^ "." ^ constant))) (* Int63 *) -let cint = Structures.cint -let ceq63 = gen_constant Structures.int63_modules "eqb" +let int63_prefix = "num.int63" +let int63_gc = gc int63_prefix +let cint = int63_gc "type" +let ceq63 = int63_gc "eqb" (* PArray *) -let carray = gen_constant Structures.parray_modules "array" +let array_prefix = "array.array" +let array_gc = gc array_prefix +let carray = array_gc "type" +let cmake = array_gc "make" +let cset = array_gc "set" (* is_true *) -let cis_true = gen_constant init_modules "is_true" +let cis_true = gc "core.is_true" "is_true" (* nat *) -let cnat = gen_constant init_modules "nat" -let cO = gen_constant init_modules "O" -let cS = gen_constant init_modules "S" +let nat_prefix = "num.nat" +let nat_gc = gc nat_prefix +let cnat = nat_gc "type" +let cO = nat_gc "O" +let cS = nat_gc "S" (* Positive *) -let positive_modules = [["Coq";"Numbers";"BinNums"]; - ["Coq";"PArith";"BinPosDef";"Pos"]] - -let cpositive = gen_constant positive_modules "positive" -let cxI = gen_constant positive_modules "xI" -let cxO = gen_constant positive_modules "xO" -let cxH = gen_constant positive_modules "xH" -let ceqbP = gen_constant positive_modules "eqb" +let positive_prefix = "num.pos" +let positive_gc = gc positive_prefix +let cpositive = positive_gc "type" +let cxI = positive_gc "xI" +let cxO = positive_gc "xO" +let cxH = positive_gc "xH" +let ceqbP = positive_gc "eqb" (* N *) -let n_modules = [["Coq";"NArith";"BinNat";"N"]] - -let cN = gen_constant positive_modules "N" -let cN0 = gen_constant positive_modules "N0" -let cNpos = gen_constant positive_modules "Npos" - -let cof_nat = gen_constant n_modules "of_nat" - +let n_prefix = "num.N" +let n_gc = gc n_prefix +let cN = n_gc "type" +let cN0 = n_gc "N0" +let cNpos = n_gc "Npos" +let cof_nat = n_gc "of_nat" (* Z *) -let z_modules = [["Coq";"Numbers";"BinNums"]; - ["Coq";"ZArith";"BinInt"]; - ["Coq";"ZArith";"BinInt";"Z"]] - -let cZ = gen_constant z_modules "Z" -let cZ0 = gen_constant z_modules "Z0" -let cZpos = gen_constant z_modules "Zpos" -let cZneg = gen_constant z_modules "Zneg" -let copp = gen_constant z_modules "opp" -let cadd = gen_constant z_modules "add" -let csub = gen_constant z_modules "sub" -let cmul = gen_constant z_modules "mul" -let cltb = gen_constant z_modules "ltb" -let cleb = gen_constant z_modules "leb" -let cgeb = gen_constant z_modules "geb" -let cgtb = gen_constant z_modules "gtb" -let ceqbZ = gen_constant z_modules "eqb" -(* let cZeqbsym = gen_constant z_modules "eqb_sym" *) +let z_prefix = "num.Z" +let z_gc = gc z_prefix +let cZ = z_gc "type" +let cZ0 = z_gc "Z0" +let cZpos = z_gc "Zpos" +let cZneg = z_gc "Zneg" +let copp = z_gc "opp" +let cadd = z_gc "add" +let csub = z_gc "sub" +let cmul = z_gc "mul" +let cltb = z_gc "ltb" +let cleb = z_gc "leb" +let cgeb = z_gc "geb" +let cgtb = z_gc "gtb" +let ceqbZ = z_gc "eqb" (* Booleans *) -let bool_modules = [["Coq";"Bool";"Bool"]] - -let cbool = gen_constant init_modules "bool" -let ctrue = gen_constant init_modules "true" -let cfalse = gen_constant init_modules "false" -let candb = gen_constant init_modules "andb" -let corb = gen_constant init_modules "orb" -let cxorb = gen_constant init_modules "xorb" -let cnegb = gen_constant init_modules "negb" -let cimplb = gen_constant init_modules "implb" -let ceqb = gen_constant bool_modules "eqb" -let cifb = gen_constant bool_modules "ifb" -let ciff = gen_constant init_modules "iff" -let creflect = gen_constant bool_modules "reflect" +let bool_prefix = "core.bool" +let bool_gc = gc bool_prefix +let cbool = bool_gc "type" +let ctrue = bool_gc "true" +let cfalse = bool_gc "false" +let candb = bool_gc "andb" +let corb = bool_gc "orb" +let cxorb = bool_gc "xorb" +let cnegb = bool_gc "negb" +let cimplb = bool_gc "implb" +let ceqb = bool_gc "eqb" +let cifb = bool_gc "ifb" +let creflect = bool_gc "reflect" (* Lists *) -let clist = gen_constant init_modules "list" -let cnil = gen_constant init_modules "nil" -let ccons = gen_constant init_modules "cons" -let clength = gen_constant init_modules "length" +let list_prefix = "core.list" +let list_gc = gc list_prefix +let clist = list_gc "type" +let cnil = list_gc "nil" +let ccons = list_gc "cons" +let clength = list_gc "length" (* Option *) -let coption = gen_constant init_modules "option" -let cSome = gen_constant init_modules "Some" -let cNone = gen_constant init_modules "None" +let option_prefix = "core.option" +let option_gc = gc option_prefix +let coption = option_gc "type" +let cSome = option_gc "Some" +let cNone = option_gc "None" (* Pairs *) -let cpair = gen_constant init_modules "pair" -let cprod = gen_constant init_modules "prod" +let pair_prefix = "core.prod" +let pair_gc = gc pair_prefix +let cpair = pair_gc "intro" +let cprod = pair_gc "type" (* Dependent pairs *) -let csigT = gen_constant init_modules "sigT" -(* let cprojT1 = gen_constant init_modules "projT1" *) -(* let cprojT2 = gen_constant init_modules "projT2" *) -(* let cprojT3 = gen_constant init_modules "projT3" *) - -(* let csigT2 = gen_constant init_modules "sigT2" *) -(* let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2" *) +let sigT_prefix = "core.sigT" +let sigT_gc = gc sigT_prefix +let csigT = sigT_gc "type" (* Logical Operators *) -let cnot = gen_constant init_modules "not" -let ceq = gen_constant init_modules "eq" -let crefl_equal = gen_constant init_modules "eq_refl" -let cconj = gen_constant init_modules "conj" -let cand = gen_constant init_modules "and" +let cnot = gc "core.not" "type" +let cconj = gc "core.and" "conj" +let cand = gc "core.and" "type" +let ciff = gc "core.iff" "type" + +(* Equality *) +let eq_prefix = "core.eq" +let eq_gc = gc eq_prefix +let ceq = eq_gc "type" +let crefl_equal = eq_gc "refl" + +(* Micromega *) +let micromega_prefix = "micromega.ZMicromega" +let micromega_gc = gc micromega_prefix +let micromega_coq_proofTerm = micromega_gc "ZArithProof" (* Bit vectors *) -let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]] -let cbitvector = gen_constant bv_modules "bitvector" -let cof_bits = gen_constant bv_modules "of_bits" -(* let c_of_bits = gen_constant bv_modules "_of_bits" *) -let cbitOf = gen_constant bv_modules "bitOf" -let cbv_eq = gen_constant bv_modules "bv_eq" -let cbv_not = gen_constant bv_modules "bv_not" -let cbv_neg = gen_constant bv_modules "bv_neg" -let cbv_and = gen_constant bv_modules "bv_and" -let cbv_or = gen_constant bv_modules "bv_or" -let cbv_xor = gen_constant bv_modules "bv_xor" -let cbv_add = gen_constant bv_modules "bv_add" -let cbv_mult = gen_constant bv_modules "bv_mult" -let cbv_ult = gen_constant bv_modules "bv_ult" -let cbv_slt = gen_constant bv_modules "bv_slt" -let cbv_concat = gen_constant bv_modules "bv_concat" -let cbv_extr = gen_constant bv_modules "bv_extr" -let cbv_zextn = gen_constant bv_modules "bv_zextn" -let cbv_sextn = gen_constant bv_modules "bv_sextn" -let cbv_shl = gen_constant bv_modules "bv_shl" -let cbv_shr = gen_constant bv_modules "bv_shr" - +let bv_prefix = "SMTCoq.bva.BVList.BITVECTOR_LIST" +let bv_gc = gc bv_prefix +let cbitvector = bv_gc "bitvector" +let cof_bits = bv_gc "of_bits" +let cbitOf = bv_gc "bitOf" +let cbv_eq = bv_gc "bv_eq" +let cbv_not = bv_gc "bv_not" +let cbv_neg = bv_gc "bv_neg" +let cbv_and = bv_gc "bv_and" +let cbv_or = bv_gc "bv_or" +let cbv_xor = bv_gc "bv_xor" +let cbv_add = bv_gc "bv_add" +let cbv_mult = bv_gc "bv_mult" +let cbv_ult = bv_gc "bv_ult" +let cbv_slt = bv_gc "bv_slt" +let cbv_concat = bv_gc "bv_concat" +let cbv_extr = bv_gc "bv_extr" +let cbv_zextn = bv_gc "bv_zextn" +let cbv_sextn = bv_gc "bv_sextn" +let cbv_shl = bv_gc "bv_shl" +let cbv_shr = bv_gc "bv_shr" (* Arrays *) -let array_modules = [["SMTCoq";"array";"FArray"]] -let cfarray = gen_constant array_modules "FArray.farray" -let cselect = gen_constant array_modules "select" -let cstore = gen_constant array_modules "store" -let cdiff = gen_constant array_modules "diff" -let cequalarray = gen_constant array_modules "FArray.equal" - -(* OrderedType *) -(* let cOrderedTypeCompare = - * gen_constant [["Coq";"Structures";"OrderedType"]] "Compare" *) - -(* SMT_terms *) -let smt_modules = [ ["SMTCoq";"Misc"]; - ["SMTCoq";"State"]; - ["SMTCoq";"SMT_terms"]; - ["SMTCoq";"SMT_terms";"Typ"]; - ["SMTCoq";"SMT_terms";"Form"]; - ["SMTCoq";"SMT_terms";"Atom"] - ] - -let cState_C_t = gen_constant [["SMTCoq";"State";"C"]] "t" -let cState_S_t = gen_constant [["SMTCoq";"State";"S"]] "t" - -let cdistinct = gen_constant smt_modules "distinct" - -let ctype = gen_constant smt_modules "type" -let cTZ = gen_constant smt_modules "TZ" -let cTbool = gen_constant smt_modules "Tbool" -let cTpositive = gen_constant smt_modules "Tpositive" -let cTBV = gen_constant smt_modules "TBV" -let cTFArray = gen_constant smt_modules "TFArray" -let cTindex = gen_constant smt_modules "Tindex" - -(* let ct_i = gen_constant smt_modules "t_i" *) -let cinterp_t = gen_constant smt_modules "Typ.interp" -let cdec_interp = gen_constant smt_modules "dec_interp" -let cord_interp = gen_constant smt_modules "ord_interp" -let ccomp_interp = gen_constant smt_modules "comp_interp" -let cinh_interp = gen_constant smt_modules "inh_interp" - -let cinterp_eqb = gen_constant smt_modules "i_eqb" -(* let cinterp_eqb_eqb = gen_constant smt_modules "i_eqb_eqb" *) - -let classes_modules = [["SMTCoq";"classes";"SMT_classes"]; - ["SMTCoq";"classes";"SMT_classes_instances"]] - -let ctyp_compdec = gen_constant classes_modules "typ_compdec" -let cTyp_compdec = gen_constant classes_modules "Typ_compdec" -(* let ctyp_compdec_from = gen_constant classes_modules "typ_compdec_from" *) -let cunit_typ_compdec = gen_constant classes_modules "unit_typ_compdec" -let cte_carrier = gen_constant classes_modules "te_carrier" -let cte_compdec = gen_constant classes_modules "te_compdec" -let ceqb_of_compdec = gen_constant classes_modules "eqb_of_compdec" -let cCompDec = gen_constant classes_modules "CompDec" - -let cbool_compdec = gen_constant classes_modules "bool_compdec" -let cZ_compdec = gen_constant classes_modules "Z_compdec" -let cPositive_compdec = gen_constant classes_modules "Positive_compdec" -let cBV_compdec = gen_constant classes_modules "BV_compdec" -let cFArray_compdec = gen_constant classes_modules "FArray_compdec" - -let ctval = gen_constant smt_modules "tval" -let cTval = gen_constant smt_modules "Tval" - -let cCO_xH = gen_constant smt_modules "CO_xH" -let cCO_Z0 = gen_constant smt_modules "CO_Z0" -let cCO_BV = gen_constant smt_modules "CO_BV" - -let cUO_xO = gen_constant smt_modules "UO_xO" -let cUO_xI = gen_constant smt_modules "UO_xI" -let cUO_Zpos = gen_constant smt_modules "UO_Zpos" -let cUO_Zneg = gen_constant smt_modules "UO_Zneg" -let cUO_Zopp = gen_constant smt_modules "UO_Zopp" -let cUO_BVbitOf = gen_constant smt_modules "UO_BVbitOf" -let cUO_BVnot = gen_constant smt_modules "UO_BVnot" -let cUO_BVneg = gen_constant smt_modules "UO_BVneg" -let cUO_BVextr = gen_constant smt_modules "UO_BVextr" -let cUO_BVzextn = gen_constant smt_modules "UO_BVzextn" -let cUO_BVsextn = gen_constant smt_modules "UO_BVsextn" - -let cBO_Zplus = gen_constant smt_modules "BO_Zplus" -let cBO_Zminus = gen_constant smt_modules "BO_Zminus" -let cBO_Zmult = gen_constant smt_modules "BO_Zmult" -let cBO_Zlt = gen_constant smt_modules "BO_Zlt" -let cBO_Zle = gen_constant smt_modules "BO_Zle" -let cBO_Zge = gen_constant smt_modules "BO_Zge" -let cBO_Zgt = gen_constant smt_modules "BO_Zgt" -let cBO_eq = gen_constant smt_modules "BO_eq" -let cBO_BVand = gen_constant smt_modules "BO_BVand" -let cBO_BVor = gen_constant smt_modules "BO_BVor" -let cBO_BVxor = gen_constant smt_modules "BO_BVxor" -let cBO_BVadd = gen_constant smt_modules "BO_BVadd" -let cBO_BVmult = gen_constant smt_modules "BO_BVmult" -let cBO_BVult = gen_constant smt_modules "BO_BVult" -let cBO_BVslt = gen_constant smt_modules "BO_BVslt" -let cBO_BVconcat = gen_constant smt_modules "BO_BVconcat" -let cBO_BVshl = gen_constant smt_modules "BO_BVshl" -let cBO_BVshr = gen_constant smt_modules "BO_BVshr" -let cBO_select = gen_constant smt_modules "BO_select" -let cBO_diffarray = gen_constant smt_modules "BO_diffarray" - -let cTO_store = gen_constant smt_modules "TO_store" - -let cNO_distinct = gen_constant smt_modules "NO_distinct" - -let catom = gen_constant smt_modules "atom" -let cAcop = gen_constant smt_modules "Acop" -let cAuop = gen_constant smt_modules "Auop" -let cAbop = gen_constant smt_modules "Abop" -let cAtop = gen_constant smt_modules "Atop" -let cAnop = gen_constant smt_modules "Anop" -let cAapp = gen_constant smt_modules "Aapp" - -let cform = gen_constant smt_modules "form" -let cFatom = gen_constant smt_modules "Fatom" -let cFtrue = gen_constant smt_modules "Ftrue" -let cFfalse = gen_constant smt_modules "Ffalse" -let cFnot2 = gen_constant smt_modules "Fnot2" -let cFand = gen_constant smt_modules "Fand" -let cFor = gen_constant smt_modules "For" -let cFxor = gen_constant smt_modules "Fxor" -let cFimp = gen_constant smt_modules "Fimp" -let cFiff = gen_constant smt_modules "Fiff" -let cFite = gen_constant smt_modules "Fite" -let cFbbT = gen_constant smt_modules "FbbT" - -let cvalid_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "valid" -let cinterp_var_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "interp_var" - -let make_certif_ops modules args = +let array_prefix = "SMTCoq.array.FArray" +let array_gc = gc array_prefix +let cfarray = array_gc "farray" +let cselect = array_gc "select" +let cstore = array_gc "store" +let cdiff = array_gc "diff" +let cequalarray = array_gc "equal" + +(* SMTCoq terms *) +let state_prefix = "SMTCoq.State" +let state_gc = gc state_prefix +let cState_C_t = state_gc "C.t" +let cState_S_t = state_gc "S.t" + +let misc_prefix = "SMTCoq.Misc" +let misc_gc = gc misc_prefix +let cdistinct = misc_gc "distinct" + +let terms_prefix = "SMTCoq.SMT_terms" +let terms_gc = gc terms_prefix + +let ctype = terms_gc "Typ.type" +let cTZ = terms_gc "Typ.TZ" +let cTbool = terms_gc "Typ.Tbool" +let cTpositive = terms_gc "Typ.Tpositive" +let cTBV = terms_gc "Typ.TBV" +let cTFArray = terms_gc "Typ.TFArray" +let cTindex = terms_gc "Typ.Tindex" + +let cinterp_t = terms_gc "Typ.interp" +let cdec_interp = terms_gc "Typ.dec_interp" +let cord_interp = terms_gc "Typ.ord_interp" +let ccomp_interp = terms_gc "Typ.comp_interp" +let cinh_interp = terms_gc "Typ.inh_interp" + +let cinterp_eqb = terms_gc "Typ.i_eqb" + +let ctval = terms_gc "Atom.tval" +let cTval = terms_gc "Atom.Tval" + +let cCO_xH = terms_gc "Atom.CO_xH" +let cCO_Z0 = terms_gc "Atom.CO_Z0" +let cCO_BV = terms_gc "Atom.CO_BV" + +let cUO_xO = terms_gc "Atom.UO_xO" +let cUO_xI = terms_gc "Atom.UO_xI" +let cUO_Zpos = terms_gc "Atom.UO_Zpos" +let cUO_Zneg = terms_gc "Atom.UO_Zneg" +let cUO_Zopp = terms_gc "Atom.UO_Zopp" +let cUO_BVbitOf = terms_gc "Atom.UO_BVbitOf" +let cUO_BVnot = terms_gc "Atom.UO_BVnot" +let cUO_BVneg = terms_gc "Atom.UO_BVneg" +let cUO_BVextr = terms_gc "Atom.UO_BVextr" +let cUO_BVzextn = terms_gc "Atom.UO_BVzextn" +let cUO_BVsextn = terms_gc "Atom.UO_BVsextn" + +let cBO_Zplus = terms_gc "Atom.BO_Zplus" +let cBO_Zminus = terms_gc "Atom.BO_Zminus" +let cBO_Zmult = terms_gc "Atom.BO_Zmult" +let cBO_Zlt = terms_gc "Atom.BO_Zlt" +let cBO_Zle = terms_gc "Atom.BO_Zle" +let cBO_Zge = terms_gc "Atom.BO_Zge" +let cBO_Zgt = terms_gc "Atom.BO_Zgt" +let cBO_eq = terms_gc "Atom.BO_eq" +let cBO_BVand = terms_gc "Atom.BO_BVand" +let cBO_BVor = terms_gc "Atom.BO_BVor" +let cBO_BVxor = terms_gc "Atom.BO_BVxor" +let cBO_BVadd = terms_gc "Atom.BO_BVadd" +let cBO_BVmult = terms_gc "Atom.BO_BVmult" +let cBO_BVult = terms_gc "Atom.BO_BVult" +let cBO_BVslt = terms_gc "Atom.BO_BVslt" +let cBO_BVconcat = terms_gc "Atom.BO_BVconcat" +let cBO_BVshl = terms_gc "Atom.BO_BVshl" +let cBO_BVshr = terms_gc "Atom.BO_BVshr" +let cBO_select = terms_gc "Atom.BO_select" +let cBO_diffarray = terms_gc "Atom.BO_diffarray" + +let cTO_store = terms_gc "Atom.TO_store" + +let cNO_distinct = terms_gc "Atom.NO_distinct" + +let catom = terms_gc "Atom.atom" +let cAcop = terms_gc "Atom.Acop" +let cAuop = terms_gc "Atom.Auop" +let cAbop = terms_gc "Atom.Abop" +let cAtop = terms_gc "Atom.Atop" +let cAnop = terms_gc "Atom.Anop" +let cAapp = terms_gc "Atom.Aapp" + +let cform = terms_gc "Form.form" +let cFatom = terms_gc "Form.Fatom" +let cFtrue = terms_gc "Form.Ftrue" +let cFfalse = terms_gc "Form.Ffalse" +let cFnot2 = terms_gc "Form.Fnot2" +let cFand = terms_gc "Form.Fand" +let cFor = terms_gc "Form.For" +let cFxor = terms_gc "Form.Fxor" +let cFimp = terms_gc "Form.Fimp" +let cFiff = terms_gc "Form.Fiff" +let cFite = terms_gc "Form.Fite" +let cFbbT = terms_gc "Form.FbbT" + +(* SMTCoq Classes *) +let classes_prefix = "SMTCoq.classes.SMT_classes" +let classes_gc = gc classes_prefix +let ctyp_compdec = classes_gc "typ_compdec" +let cTyp_compdec = classes_gc "Typ_compdec" +let cte_carrier = classes_gc "te_carrier" +let cte_compdec = classes_gc "te_compdec" +let ceqb_of_compdec = classes_gc "eqb_of_compdec" +let cCompDec = classes_gc "CompDec" + +let classesi_prefix = "SMTCoq.classes.SMT_classes_instances" +let classesi_gc = gc classesi_prefix +let cunit_typ_compdec = classesi_gc "unit_typ_compdec" +let cbool_compdec = classesi_gc "bool_compdec" +let cZ_compdec = classesi_gc "Z_compdec" +let cPositive_compdec = classesi_gc "Positive_compdec" +let cBV_compdec = classesi_gc "BV_compdec" +let cFArray_compdec = classesi_gc "FArray_compdec" + +(* SMTCoq Trace *) +let sat_checker_prefix = "SMTCoq.Trace.Sat_Checker" +let sat_checker_gc = gc sat_checker_prefix +let csat_checker_valid = sat_checker_gc "valid" +let csat_checker_interp_var = sat_checker_gc "interp_var" +let csat_checker_Certif = sat_checker_gc "Certif" +let csat_checker_dimacs = sat_checker_gc "dimacs" +let csat_checker_certif = sat_checker_gc "certif" +let csat_checker_theorem_checker = sat_checker_gc "theorem_checker" +let csat_checker_checker = sat_checker_gc "checker" + +let cnf_checker_prefix = "SMTCoq.Trace.Cnf_Checker" +let cnf_checker_gc = gc cnf_checker_prefix +let ccnf_checker_certif = cnf_checker_gc "certif" +let ccnf_checker_Certif = cnf_checker_gc "Certif" +let ccnf_checker_checker_b_correct = cnf_checker_gc "checker_b_correct" +let ccnf_checker_checker_b = cnf_checker_gc "checker_b" +let ccnf_checker_checker_eq_correct = cnf_checker_gc "checker_eq_correct" +let ccnf_checker_checker_eq = cnf_checker_gc "checker_eq" + +let euf_checker_prefix = "SMTCoq.Trace.Euf_Checker" +let euf_checker_gc = gc euf_checker_prefix +let ceuf_checker_Certif = euf_checker_gc "Certif" +let ceuf_checker_certif = euf_checker_gc "certif" +let ceuf_checker_checker = euf_checker_gc "checker" +let ceuf_checker_checker_correct = euf_checker_gc "checker_correct" +let ceuf_checker_checker_b_correct = euf_checker_gc "checker_b_correct" +let ceuf_checker_checker_b = euf_checker_gc "checker_b" +let ceuf_checker_checker_eq_correct = euf_checker_gc "checker_eq_correct" +let ceuf_checker_checker_eq = euf_checker_gc "checker_eq" +let ceuf_checker_checker_debug = euf_checker_gc "checker_debug" +let ceuf_checker_name_step = euf_checker_gc "name_step" +let ceuf_checker_Name_Res = euf_checker_gc "Name_Res" +let ceuf_checker_Name_Weaken = euf_checker_gc "Name_Weaken" +let ceuf_checker_Name_ImmFlatten = euf_checker_gc "Name_ImmFlatten" +let ceuf_checker_Name_CTrue = euf_checker_gc "Name_CTrue" +let ceuf_checker_Name_CFalse = euf_checker_gc "Name_CFalse" +let ceuf_checker_Name_BuildDef = euf_checker_gc "Name_BuildDef" +let ceuf_checker_Name_BuildDef2 = euf_checker_gc "Name_BuildDef2" +let ceuf_checker_Name_BuildProj = euf_checker_gc "Name_BuildProj" +let ceuf_checker_Name_ImmBuildDef = euf_checker_gc "Name_ImmBuildDef" +let ceuf_checker_Name_ImmBuildDef2 = euf_checker_gc "Name_ImmBuildDef2" +let ceuf_checker_Name_ImmBuildProj = euf_checker_gc "Name_ImmBuildProj" +let ceuf_checker_Name_EqTr = euf_checker_gc "Name_EqTr" +let ceuf_checker_Name_EqCgr = euf_checker_gc "Name_EqCgr" +let ceuf_checker_Name_EqCgrP = euf_checker_gc "Name_EqCgrP" +let ceuf_checker_Name_LiaMicromega = euf_checker_gc "Name_LiaMicromega" +let ceuf_checker_Name_LiaDiseq = euf_checker_gc "Name_LiaDiseq" +let ceuf_checker_Name_SplArith = euf_checker_gc "Name_SplArith" +let ceuf_checker_Name_SplDistinctElim = euf_checker_gc "Name_SplDistinctElim" +let ceuf_checker_Name_BBVar = euf_checker_gc "Name_BBVar" +let ceuf_checker_Name_BBConst = euf_checker_gc "Name_BBConst" +let ceuf_checker_Name_BBOp = euf_checker_gc "Name_BBOp" +let ceuf_checker_Name_BBNot = euf_checker_gc "Name_BBNot" +let ceuf_checker_Name_BBNeg = euf_checker_gc "Name_BBNeg" +let ceuf_checker_Name_BBAdd = euf_checker_gc "Name_BBAdd" +let ceuf_checker_Name_BBConcat = euf_checker_gc "Name_BBConcat" +let ceuf_checker_Name_BBMul = euf_checker_gc "Name_BBMul" +let ceuf_checker_Name_BBUlt = euf_checker_gc "Name_BBUlt" +let ceuf_checker_Name_BBSlt = euf_checker_gc "Name_BBSlt" +let ceuf_checker_Name_BBEq = euf_checker_gc "Name_BBEq" +let ceuf_checker_Name_BBDiseq = euf_checker_gc "Name_BBDiseq" +let ceuf_checker_Name_BBExtract = euf_checker_gc "Name_BBExtract" +let ceuf_checker_Name_BBZextend = euf_checker_gc "Name_BBZextend" +let ceuf_checker_Name_BBSextend = euf_checker_gc "Name_BBSextend" +let ceuf_checker_Name_BBShl = euf_checker_gc "Name_BBShl" +let ceuf_checker_Name_BBShr = euf_checker_gc "Name_BBShr" +let ceuf_checker_Name_RowEq = euf_checker_gc "Name_RowEq" +let ceuf_checker_Name_RowNeq = euf_checker_gc "Name_RowNeq" +let ceuf_checker_Name_Ext = euf_checker_gc "Name_Ext" +let ceuf_checker_Name_Hole = euf_checker_gc "Name_Hole" + +type certif_ops = + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm +let make_certif_ops prefix args = + let gc = gc prefix in let gen_constant c = match args with - | Some args -> lazy (mklApp (gen_constant modules c) args) - | None -> gen_constant modules c in + | Some args -> lazy (mklApp (gc c) args) + | None -> gc c in (gen_constant "step", gen_constant "Res", gen_constant "Weaken", gen_constant "ImmFlatten", gen_constant "CTrue", gen_constant "CFalse", gen_constant "BuildDef", gen_constant "BuildDef2", gen_constant "BuildProj", - gen_constant "ImmBuildProj", gen_constant"ImmBuildDef", + gen_constant "ImmBuildProj", gen_constant "ImmBuildDef", gen_constant"ImmBuildDef2", gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP", gen_constant "LiaMicromega", gen_constant "LiaDiseq", @@ -297,6 +391,9 @@ let make_certif_ops modules args = gen_constant "BBShl", gen_constant "BBShr", gen_constant "RowEq", gen_constant "RowNeq", gen_constant "Ext", gen_constant "Hole", gen_constant "ForallInst") +let csat_checker_certif_ops = make_certif_ops sat_checker_prefix None +let ccnf_checker_certif_ops = make_certif_ops cnf_checker_prefix None +let ceuf_checker_certif_ops = make_certif_ops euf_checker_prefix (** Useful constructions *) @@ -307,8 +404,8 @@ let ceq_refl_true = let eq_refl_true () = Lazy.force ceq_refl_true let vm_cast_true_no_check t = - Structures.mkCast(eq_refl_true (), - Structures.vmcast, + CoqInterface.mkCast(eq_refl_true (), + CoqInterface.vmcast, mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]) (* This version checks convertibility right away instead of delaying it at @@ -316,13 +413,13 @@ let vm_cast_true_no_check t = SMTCoq's tactics. *) let vm_cast_true env t = try - Structures.vm_conv Reduction.CUMUL env + CoqInterface.vm_conv Reduction.CUMUL env (mklApp ceq [|Lazy.force cbool; Lazy.force ctrue; Lazy.force ctrue|]) (mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]); vm_cast_true_no_check t with Reduction.NotConvertible -> - Structures.error ("SMTCoq was not able to check the proof certificate.") + CoqInterface.error ("SMTCoq was not able to check the proof certificate.") (* Compute a nat *) @@ -353,42 +450,55 @@ let rec mk_bv_list = function | b :: bv -> mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|] +(* Compute an array *) +let mkArray : Constr.types * Constr.t array -> Constr.t = + fun (ty, a) -> + let l = (Array.length a) - 1 in + snd (Array.fold_left (fun (i,acc) c -> + let acc' = + if i = l then + acc + else + mklApp cset [|ty; acc; mkInt i; c|] in + (i+1,acc') + ) (0, mklApp cmake [|ty; mkInt l; a.(l)|]) a) + (* Reification *) let mk_bool b = - let c, args = Structures.decompose_app b in - if Structures.eq_constr c (Lazy.force ctrue) then true - else if Structures.eq_constr c (Lazy.force cfalse) then false + let c, args = CoqInterface.decompose_app b in + if CoqInterface.eq_constr c (Lazy.force ctrue) then true + else if CoqInterface.eq_constr c (Lazy.force cfalse) then false else assert false let rec mk_bool_list bs = - let c, args = Structures.decompose_app bs in - if Structures.eq_constr c (Lazy.force cnil) then [] - else if Structures.eq_constr c (Lazy.force ccons) then + let c, args = CoqInterface.decompose_app bs in + if CoqInterface.eq_constr c (Lazy.force cnil) then [] + else if CoqInterface.eq_constr c (Lazy.force ccons) then match args with | [_; b; bs] -> mk_bool b :: mk_bool_list bs | _ -> assert false else assert false let rec mk_nat n = - let c, args = Structures.decompose_app n in - if Structures.eq_constr c (Lazy.force cO) then + let c, args = CoqInterface.decompose_app n in + if CoqInterface.eq_constr c (Lazy.force cO) then 0 - else if Structures.eq_constr c (Lazy.force cS) then + else if CoqInterface.eq_constr c (Lazy.force cS) then match args with | [n] -> (mk_nat n) + 1 | _ -> assert false else assert false let rec mk_positive n = - let c, args = Structures.decompose_app n in - if Structures.eq_constr c (Lazy.force cxH) then + let c, args = CoqInterface.decompose_app n in + if CoqInterface.eq_constr c (Lazy.force cxH) then 1 - else if Structures.eq_constr c (Lazy.force cxO) then + else if CoqInterface.eq_constr c (Lazy.force cxO) then match args with | [n] -> 2 * (mk_positive n) | _ -> assert false - else if Structures.eq_constr c (Lazy.force cxI) then + else if CoqInterface.eq_constr c (Lazy.force cxI) then match args with | [n] -> 2 * (mk_positive n) + 1 | _ -> assert false @@ -396,10 +506,10 @@ let rec mk_positive n = let mk_N n = - let c, args = Structures.decompose_app n in - if Structures.eq_constr c (Lazy.force cN0) then + let c, args = CoqInterface.decompose_app n in + if CoqInterface.eq_constr c (Lazy.force cN0) then 0 - else if Structures.eq_constr c (Lazy.force cNpos) then + else if CoqInterface.eq_constr c (Lazy.force cNpos) then match args with | [n] -> mk_positive n | _ -> assert false @@ -407,13 +517,13 @@ let mk_N n = let mk_Z n = - let c, args = Structures.decompose_app n in - if Structures.eq_constr c (Lazy.force cZ0) then 0 - else if Structures.eq_constr c (Lazy.force cZpos) then + let c, args = CoqInterface.decompose_app n in + if CoqInterface.eq_constr c (Lazy.force cZ0) then 0 + else if CoqInterface.eq_constr c (Lazy.force cZpos) then match args with | [n] -> mk_positive n | _ -> assert false - else if Structures.eq_constr c (Lazy.force cZneg) then + else if CoqInterface.eq_constr c (Lazy.force cZneg) then match args with | [n] -> - mk_positive n | _ -> assert false @@ -422,12 +532,12 @@ let mk_Z n = (* size of bivectors are either N.of_nat (length l) or an N *) let mk_bvsize n = - let c, args = Structures.decompose_app n in - if Structures.eq_constr c (Lazy.force cof_nat) then + let c, args = CoqInterface.decompose_app n in + if CoqInterface.eq_constr c (Lazy.force cof_nat) then match args with | [nl] -> - let c, args = Structures.decompose_app nl in - if Structures.eq_constr c (Lazy.force clength) then + let c, args = CoqInterface.decompose_app nl in + if CoqInterface.eq_constr c (Lazy.force clength) then match args with | [_; l] -> List.length (mk_bool_list l) | _ -> assert false @@ -438,7 +548,7 @@ let mk_bvsize n = (** Switches between constr and OCaml *) (* Transform a option constr into a constr option *) let option_of_constr_option co = - let c, args = Structures.decompose_app co in + let c, args = CoqInterface.decompose_app co in if c = Lazy.force cSome then match args with | [_;c] -> Some c @@ -449,7 +559,7 @@ let option_of_constr_option co = (* Transform a tuple of constr into a (reversed) list of constr *) let list_of_constr_tuple = let rec list_of_constr_tuple acc t = - let c, args = Structures.decompose_app t in + let c, args = CoqInterface.decompose_app t in if c = Lazy.force cpair then match args with | [_;_;t1;t2] -> diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index f62f01a..53622ac 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -10,258 +10,331 @@ (**************************************************************************) -val gen_constant : string list list -> string -> Structures.constr lazy_t +type coqTerm = CoqInterface.constr lazy_t (* Int63 *) -val cint : Structures.constr lazy_t -val ceq63 : Structures.constr lazy_t +val cint : coqTerm +val ceq63 : coqTerm (* PArray *) -val carray : Structures.constr lazy_t +val carray : coqTerm +val cmake : coqTerm +val cset : coqTerm + +(* is_true *) +val cis_true : coqTerm (* nat *) -val cnat : Structures.constr lazy_t -val cO : Structures.constr lazy_t -val cS : Structures.constr lazy_t +val cnat : coqTerm +val cO : coqTerm +val cS : coqTerm (* Positive *) -val cpositive : Structures.constr lazy_t -val cxI : Structures.constr lazy_t -val cxO : Structures.constr lazy_t -val cxH : Structures.constr lazy_t -val ceqbP : Structures.constr lazy_t +val cpositive : coqTerm +val cxI : coqTerm +val cxO : coqTerm +val cxH : coqTerm +val ceqbP : coqTerm (* N *) -val cN : Structures.constr lazy_t -val cN0 : Structures.constr lazy_t -val cNpos : Structures.constr lazy_t -val cof_nat : Structures.constr lazy_t +val cN : coqTerm +val cN0 : coqTerm +val cNpos : coqTerm +val cof_nat : coqTerm (* Z *) -val cZ : Structures.constr lazy_t -val cZ0 : Structures.constr lazy_t -val cZpos : Structures.constr lazy_t -val cZneg : Structures.constr lazy_t -val copp : Structures.constr lazy_t -val cadd : Structures.constr lazy_t -val csub : Structures.constr lazy_t -val cmul : Structures.constr lazy_t -val cltb : Structures.constr lazy_t -val cleb : Structures.constr lazy_t -val cgeb : Structures.constr lazy_t -val cgtb : Structures.constr lazy_t -val ceqbZ : Structures.constr lazy_t +val cZ : coqTerm +val cZ0 : coqTerm +val cZpos : coqTerm +val cZneg : coqTerm +val copp : coqTerm +val cadd : coqTerm +val csub : coqTerm +val cmul : coqTerm +val cltb : coqTerm +val cleb : coqTerm +val cgeb : coqTerm +val cgtb : coqTerm +val ceqbZ : coqTerm (* Booleans *) -val cbool : Structures.constr lazy_t -val ctrue : Structures.constr lazy_t -val cfalse : Structures.constr lazy_t -val candb : Structures.constr lazy_t -val corb : Structures.constr lazy_t -val cxorb : Structures.constr lazy_t -val cnegb : Structures.constr lazy_t -val cimplb : Structures.constr lazy_t -val ceqb : Structures.constr lazy_t -val cifb : Structures.constr lazy_t -val ciff : Structures.constr lazy_t -val creflect : Structures.constr lazy_t +val cbool : coqTerm +val ctrue : coqTerm +val cfalse : coqTerm +val candb : coqTerm +val corb : coqTerm +val cxorb : coqTerm +val cnegb : coqTerm +val cimplb : coqTerm +val ceqb : coqTerm +val cifb : coqTerm +val creflect : coqTerm (* Lists *) -val clist : Structures.constr lazy_t -val cnil : Structures.constr lazy_t -val ccons : Structures.constr lazy_t -val clength : Structures.constr lazy_t +val clist : coqTerm +val cnil : coqTerm +val ccons : coqTerm +val clength : coqTerm (* Option *) -val coption : Structures.constr lazy_t -val cSome : Structures.constr lazy_t -val cNone : Structures.constr lazy_t +val coption : coqTerm +val cSome : coqTerm +val cNone : coqTerm (* Pairs *) -val cpair : Structures.constr lazy_t -val cprod : Structures.constr lazy_t +val cpair : coqTerm +val cprod : coqTerm (* Dependent pairs *) -val csigT : Structures.constr lazy_t +val csigT : coqTerm (* Logical Operators *) -val cnot : Structures.constr lazy_t -val ceq : Structures.constr lazy_t -val crefl_equal : Structures.constr lazy_t -val cconj : Structures.constr lazy_t -val cand : Structures.constr lazy_t +val cnot : coqTerm +val cconj : coqTerm +val cand : coqTerm +val ciff : coqTerm + +(* Equality *) +val ceq : coqTerm +val crefl_equal : coqTerm + +(* Micromega *) +val micromega_coq_proofTerm : coqTerm (* Bit vectors *) -val cbitvector : Structures.constr lazy_t -val cof_bits : Structures.constr lazy_t -val cbitOf : Structures.constr lazy_t -val cbv_eq : Structures.constr lazy_t -val cbv_not : Structures.constr lazy_t -val cbv_neg : Structures.constr lazy_t -val cbv_and : Structures.constr lazy_t -val cbv_or : Structures.constr lazy_t -val cbv_xor : Structures.constr lazy_t -val cbv_add : Structures.constr lazy_t -val cbv_mult : Structures.constr lazy_t -val cbv_ult : Structures.constr lazy_t -val cbv_slt : Structures.constr lazy_t -val cbv_concat : Structures.constr lazy_t -val cbv_extr : Structures.constr lazy_t -val cbv_zextn : Structures.constr lazy_t -val cbv_sextn : Structures.constr lazy_t -val cbv_shl : Structures.constr lazy_t -val cbv_shr : Structures.constr lazy_t +val cbitvector : coqTerm +val cof_bits : coqTerm +val cbitOf : coqTerm +val cbv_eq : coqTerm +val cbv_not : coqTerm +val cbv_neg : coqTerm +val cbv_and : coqTerm +val cbv_or : coqTerm +val cbv_xor : coqTerm +val cbv_add : coqTerm +val cbv_mult : coqTerm +val cbv_ult : coqTerm +val cbv_slt : coqTerm +val cbv_concat : coqTerm +val cbv_extr : coqTerm +val cbv_zextn : coqTerm +val cbv_sextn : coqTerm +val cbv_shl : coqTerm +val cbv_shr : coqTerm (* Arrays *) -val cfarray : Structures.constr lazy_t -val cselect : Structures.constr lazy_t -val cstore : Structures.constr lazy_t -val cdiff : Structures.constr lazy_t -val cequalarray : Structures.constr lazy_t - -(* OrderedType *) - -(* SMT_terms *) -val cState_C_t : Structures.constr lazy_t -val cState_S_t : Structures.constr lazy_t - -val cdistinct : Structures.constr lazy_t - -val ctype : Structures.constr lazy_t -val cTZ : Structures.constr lazy_t -val cTbool : Structures.constr lazy_t -val cTpositive : Structures.constr lazy_t -val cTBV : Structures.constr lazy_t -val cTFArray : Structures.constr lazy_t -val cTindex : Structures.constr lazy_t - -val cinterp_t : Structures.constr lazy_t -val cdec_interp : Structures.constr lazy_t -val cord_interp : Structures.constr lazy_t -val ccomp_interp : Structures.constr lazy_t -val cinh_interp : Structures.constr lazy_t - -val cinterp_eqb : Structures.constr lazy_t - -val ctyp_compdec : Structures.constr lazy_t -val cTyp_compdec : Structures.constr lazy_t -val cunit_typ_compdec : Structures.constr lazy_t -val cte_carrier : Structures.constr lazy_t -val cte_compdec : Structures.constr lazy_t -val ceqb_of_compdec : Structures.constr lazy_t -val cCompDec : Structures.constr lazy_t - -val cbool_compdec : Structures.constr lazy_t -val cZ_compdec : Structures.constr lazy_t -val cPositive_compdec : Structures.constr lazy_t -val cBV_compdec : Structures.constr lazy_t -val cFArray_compdec : Structures.constr lazy_t - -val ctval : Structures.constr lazy_t -val cTval : Structures.constr lazy_t - -val cCO_xH : Structures.constr lazy_t -val cCO_Z0 : Structures.constr lazy_t -val cCO_BV : Structures.constr lazy_t - -val cUO_xO : Structures.constr lazy_t -val cUO_xI : Structures.constr lazy_t -val cUO_Zpos : Structures.constr lazy_t -val cUO_Zneg : Structures.constr lazy_t -val cUO_Zopp : Structures.constr lazy_t -val cUO_BVbitOf : Structures.constr lazy_t -val cUO_BVnot : Structures.constr lazy_t -val cUO_BVneg : Structures.constr lazy_t -val cUO_BVextr : Structures.constr lazy_t -val cUO_BVzextn : Structures.constr lazy_t -val cUO_BVsextn : Structures.constr lazy_t - -val cBO_Zplus : Structures.constr lazy_t -val cBO_Zminus : Structures.constr lazy_t -val cBO_Zmult : Structures.constr lazy_t -val cBO_Zlt : Structures.constr lazy_t -val cBO_Zle : Structures.constr lazy_t -val cBO_Zge : Structures.constr lazy_t -val cBO_Zgt : Structures.constr lazy_t -val cBO_eq : Structures.constr lazy_t -val cBO_BVand : Structures.constr lazy_t -val cBO_BVor : Structures.constr lazy_t -val cBO_BVxor : Structures.constr lazy_t -val cBO_BVadd : Structures.constr lazy_t -val cBO_BVmult : Structures.constr lazy_t -val cBO_BVult : Structures.constr lazy_t -val cBO_BVslt : Structures.constr lazy_t -val cBO_BVconcat : Structures.constr lazy_t -val cBO_BVshl : Structures.constr lazy_t -val cBO_BVshr : Structures.constr lazy_t -val cBO_select : Structures.constr lazy_t -val cBO_diffarray : Structures.constr lazy_t - -val cTO_store : Structures.constr lazy_t - -val cNO_distinct : Structures.constr lazy_t - -val catom : Structures.constr lazy_t -val cAcop : Structures.constr lazy_t -val cAuop : Structures.constr lazy_t -val cAbop : Structures.constr lazy_t -val cAtop : Structures.constr lazy_t -val cAnop : Structures.constr lazy_t -val cAapp : Structures.constr lazy_t - -val cform : Structures.constr lazy_t -val cFatom : Structures.constr lazy_t -val cFtrue : Structures.constr lazy_t -val cFfalse : Structures.constr lazy_t -val cFnot2 : Structures.constr lazy_t -val cFand : Structures.constr lazy_t -val cFor : Structures.constr lazy_t -val cFxor : Structures.constr lazy_t -val cFimp : Structures.constr lazy_t -val cFiff : Structures.constr lazy_t -val cFite : Structures.constr lazy_t -val cFbbT : Structures.constr lazy_t - -val cis_true : Structures.constr lazy_t - -val cvalid_sat_checker : Structures.constr lazy_t -val cinterp_var_sat_checker : Structures.constr lazy_t - -val make_certif_ops : - string list list -> - Structures.constr array option -> - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * - Structures.constr lazy_t * Structures.constr lazy_t +val cfarray : coqTerm +val cselect : coqTerm +val cstore : coqTerm +val cdiff : coqTerm +val cequalarray : coqTerm + +(* SMTCoq terms *) +val cState_C_t : coqTerm +val cState_S_t : coqTerm + +val cdistinct : coqTerm + +val ctype : coqTerm +val cTZ : coqTerm +val cTbool : coqTerm +val cTpositive : coqTerm +val cTBV : coqTerm +val cTFArray : coqTerm +val cTindex : coqTerm + +val cinterp_t : coqTerm +val cdec_interp : coqTerm +val cord_interp : coqTerm +val ccomp_interp : coqTerm +val cinh_interp : coqTerm + +val cinterp_eqb : coqTerm + +val ctval : coqTerm +val cTval : coqTerm + +val cCO_xH : coqTerm +val cCO_Z0 : coqTerm +val cCO_BV : coqTerm + +val cUO_xO : coqTerm +val cUO_xI : coqTerm +val cUO_Zpos : coqTerm +val cUO_Zneg : coqTerm +val cUO_Zopp : coqTerm +val cUO_BVbitOf : coqTerm +val cUO_BVnot : coqTerm +val cUO_BVneg : coqTerm +val cUO_BVextr : coqTerm +val cUO_BVzextn : coqTerm +val cUO_BVsextn : coqTerm + +val cBO_Zplus : coqTerm +val cBO_Zminus : coqTerm +val cBO_Zmult : coqTerm +val cBO_Zlt : coqTerm +val cBO_Zle : coqTerm +val cBO_Zge : coqTerm +val cBO_Zgt : coqTerm +val cBO_eq : coqTerm +val cBO_BVand : coqTerm +val cBO_BVor : coqTerm +val cBO_BVxor : coqTerm +val cBO_BVadd : coqTerm +val cBO_BVmult : coqTerm +val cBO_BVult : coqTerm +val cBO_BVslt : coqTerm +val cBO_BVconcat : coqTerm +val cBO_BVshl : coqTerm +val cBO_BVshr : coqTerm +val cBO_select : coqTerm +val cBO_diffarray : coqTerm + +val cTO_store : coqTerm + +val cNO_distinct : coqTerm + +val catom : coqTerm +val cAcop : coqTerm +val cAuop : coqTerm +val cAbop : coqTerm +val cAtop : coqTerm +val cAnop : coqTerm +val cAapp : coqTerm + +val cform : coqTerm +val cFatom : coqTerm +val cFtrue : coqTerm +val cFfalse : coqTerm +val cFnot2 : coqTerm +val cFand : coqTerm +val cFor : coqTerm +val cFxor : coqTerm +val cFimp : coqTerm +val cFiff : coqTerm +val cFite : coqTerm +val cFbbT : coqTerm + +(* SMTCoq Classes *) +val ctyp_compdec : coqTerm +val cTyp_compdec : coqTerm +val cte_carrier : coqTerm +val cte_compdec : coqTerm +val ceqb_of_compdec : coqTerm +val cCompDec : coqTerm + +val cunit_typ_compdec : coqTerm +val cbool_compdec : coqTerm +val cZ_compdec : coqTerm +val cPositive_compdec : coqTerm +val cBV_compdec : coqTerm +val cFArray_compdec : coqTerm + +(* SMTCoq Trace *) +type certif_ops = + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm + +val csat_checker_valid : coqTerm +val csat_checker_interp_var : coqTerm +val csat_checker_Certif : coqTerm +val csat_checker_dimacs : coqTerm +val csat_checker_certif : coqTerm +val csat_checker_theorem_checker : coqTerm +val csat_checker_checker : coqTerm +val csat_checker_certif_ops : certif_ops + +val ccnf_checker_certif : coqTerm +val ccnf_checker_Certif : coqTerm +val ccnf_checker_checker_b_correct : coqTerm +val ccnf_checker_checker_b : coqTerm +val ccnf_checker_checker_eq_correct : coqTerm +val ccnf_checker_checker_eq : coqTerm +val ccnf_checker_certif_ops : certif_ops + +val ceuf_checker_Certif : coqTerm +val ceuf_checker_certif : coqTerm +val ceuf_checker_checker : coqTerm +val ceuf_checker_checker_correct : coqTerm +val ceuf_checker_checker_b_correct : coqTerm +val ceuf_checker_checker_b : coqTerm +val ceuf_checker_checker_eq_correct : coqTerm +val ceuf_checker_checker_eq : coqTerm +val ceuf_checker_checker_debug : coqTerm +val ceuf_checker_name_step : coqTerm +val ceuf_checker_Name_Res : coqTerm +val ceuf_checker_Name_Weaken : coqTerm +val ceuf_checker_Name_ImmFlatten : coqTerm +val ceuf_checker_Name_CTrue : coqTerm +val ceuf_checker_Name_CFalse : coqTerm +val ceuf_checker_Name_BuildDef : coqTerm +val ceuf_checker_Name_BuildDef2 : coqTerm +val ceuf_checker_Name_BuildProj : coqTerm +val ceuf_checker_Name_ImmBuildDef : coqTerm +val ceuf_checker_Name_ImmBuildDef2 : coqTerm +val ceuf_checker_Name_ImmBuildProj : coqTerm +val ceuf_checker_Name_EqTr : coqTerm +val ceuf_checker_Name_EqCgr : coqTerm +val ceuf_checker_Name_EqCgrP : coqTerm +val ceuf_checker_Name_LiaMicromega : coqTerm +val ceuf_checker_Name_LiaDiseq : coqTerm +val ceuf_checker_Name_SplArith : coqTerm +val ceuf_checker_Name_SplDistinctElim : coqTerm +val ceuf_checker_Name_BBVar : coqTerm +val ceuf_checker_Name_BBConst : coqTerm +val ceuf_checker_Name_BBOp : coqTerm +val ceuf_checker_Name_BBNot : coqTerm +val ceuf_checker_Name_BBNeg : coqTerm +val ceuf_checker_Name_BBAdd : coqTerm +val ceuf_checker_Name_BBConcat : coqTerm +val ceuf_checker_Name_BBMul : coqTerm +val ceuf_checker_Name_BBUlt : coqTerm +val ceuf_checker_Name_BBSlt : coqTerm +val ceuf_checker_Name_BBEq : coqTerm +val ceuf_checker_Name_BBDiseq : coqTerm +val ceuf_checker_Name_BBExtract : coqTerm +val ceuf_checker_Name_BBZextend : coqTerm +val ceuf_checker_Name_BBSextend : coqTerm +val ceuf_checker_Name_BBShl : coqTerm +val ceuf_checker_Name_BBShr : coqTerm +val ceuf_checker_Name_RowEq : coqTerm +val ceuf_checker_Name_RowNeq : coqTerm +val ceuf_checker_Name_Ext : coqTerm +val ceuf_checker_Name_Hole : coqTerm +val ceuf_checker_certif_ops : CoqInterface.constr array option -> certif_ops + (* Some constructions *) -val ceq_refl_true : Structures.constr lazy_t -val eq_refl_true : unit -> Structures.constr -val vm_cast_true_no_check : Structures.constr -> Structures.constr -val vm_cast_true : Environ.env -> Structures.constr -> Structures.constr -val mkNat : int -> Structures.constr -val mkN : int -> Structures.constr -val mk_bv_list : bool list -> Structures.constr +val ceq_refl_true : coqTerm +val eq_refl_true : unit -> CoqInterface.constr +val vm_cast_true_no_check : CoqInterface.constr -> CoqInterface.constr +val vm_cast_true : Environ.env -> CoqInterface.constr -> CoqInterface.constr +val mkNat : int -> CoqInterface.constr +val mkN : int -> CoqInterface.constr +val mk_bv_list : bool list -> CoqInterface.constr +val mkArray : Constr.types * Constr.t array -> Constr.t (* Reification *) -val mk_bool : Structures.constr -> bool -val mk_bool_list : Structures.constr -> bool list -val mk_nat : Structures.constr -> int -val mk_N : Structures.constr -> int -val mk_Z : Structures.constr -> int -val mk_bvsize : Structures.constr -> int +val mk_bool : CoqInterface.constr -> bool +val mk_bool_list : CoqInterface.constr -> bool list +val mk_nat : CoqInterface.constr -> int +val mk_N : CoqInterface.constr -> int +val mk_Z : CoqInterface.constr -> int +val mk_bvsize : CoqInterface.constr -> int (* Switches between constr and OCaml *) -val option_of_constr_option : Structures.constr -> Structures.constr option -val list_of_constr_tuple : Structures.constr -> Structures.constr list +val option_of_constr_option : CoqInterface.constr -> CoqInterface.constr option +val list_of_constr_tuple : CoqInterface.constr -> CoqInterface.constr list diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml index 4a3a62d..37e6a8c 100644 --- a/src/trace/satAtom.ml +++ b/src/trace/satAtom.ml @@ -27,7 +27,7 @@ module Atom = type reify_tbl = { mutable count : int; - tbl : (Structures.constr, int) Hashtbl.t + tbl : (CoqInterface.constr, int) Hashtbl.t } let create () = @@ -51,11 +51,11 @@ module Atom = t let interp_tbl reify = - Structures.mkArray (Lazy.force cbool, atom_tbl reify) + CoqTerms.mkArray (Lazy.force cbool, atom_tbl reify) let logic _ = SL.empty - let to_smt = Format.pp_print_int + let to_smt ?(debug=false) = Format.pp_print_int end diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli index 1e14cbb..9f4272c 100644 --- a/src/trace/satAtom.mli +++ b/src/trace/satAtom.mli @@ -18,18 +18,18 @@ module Atom : sig val is_bool_type : t -> bool val is_bv_type : t -> bool - val to_smt : Format.formatter -> t -> unit + val to_smt : ?debug:bool -> Format.formatter -> t -> unit val logic : t -> SmtMisc.logic type reify_tbl = { mutable count : int; - tbl : (Structures.constr, t) Hashtbl.t; + tbl : (CoqInterface.constr, t) Hashtbl.t; } val create : unit -> reify_tbl - val declare : reify_tbl -> Structures.constr -> t - val get : reify_tbl -> Structures.constr -> t - val atom_tbl : reify_tbl -> Structures.constr array - val interp_tbl : reify_tbl -> Structures.constr + val declare : reify_tbl -> CoqInterface.constr -> t + val get : reify_tbl -> CoqInterface.constr -> t + val atom_tbl : reify_tbl -> CoqInterface.constr array + val interp_tbl : reify_tbl -> CoqInterface.constr end diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 1befbf7..ccd9629 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -85,7 +85,7 @@ type nop = type op_def = { tparams : SmtBtype.btype array; tres : SmtBtype.btype; - op_val : Structures.constr } + op_val : CoqInterface.constr } type index = Index of int | Rel_name of string @@ -97,14 +97,14 @@ let destruct s (i, hval) = match i with | Rel_name _ -> failwith s let dummy_indexed_op i dom codom = - (i, {tparams = dom; tres = codom; op_val = Structures.mkProp}) + (i, {tparams = dom; tres = codom; op_val = CoqInterface.mkProp}) let indexed_op_index i = let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in index let debruijn_indexed_op i ty = - (Index i, {tparams = [||]; tres = ty; op_val = Structures.mkRel i}) + (Index i, {tparams = [||]; tres = ty; op_val = CoqInterface.mkRel i}) module Op = struct @@ -357,7 +357,7 @@ module Op = (* reify table *) type reify_tbl = { mutable count : int; - tbl : (Structures.constr, indexed_op) Hashtbl.t + tbl : (CoqInterface.constr, indexed_op) Hashtbl.t } let create () = @@ -385,7 +385,7 @@ module Op = let index, hval = destruct "destruct on a Rel: called by set in interp_tbl" op in t.(index) <- mk_Tval hval.tparams hval.tres hval.op_val in Hashtbl.iter set reify.tbl; - Structures.mkArray (tval, t) + CoqTerms.mkArray (tval, t) let to_list reify = let set _ op acc = @@ -707,13 +707,13 @@ module Atom = | [] -> () - let to_smt_named ?pi:(pi=false) (fmt:Format.formatter) h = + let to_smt_named ?(debug=false) ?pi:(pi=false) (fmt:Format.formatter) h = let rec to_smt fmt h = if pi then Format.fprintf fmt "%d:" (index h); - to_smt_atom (atom h) + to_smt_atom ~debug:debug (atom h) - and to_smt_atom = function - | Acop (CO_BV bv) -> if List.length bv = 0 then Structures.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv + and to_smt_atom ?(debug=false) = function + | Acop (CO_BV bv) -> if List.length bv = 0 then CoqInterface.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv | Acop _ as a -> to_smt_int fmt (compute_int a) | Auop (op,h) -> to_smt_uop op h | Abop (op,h1,h2) -> to_smt_bop op h1 h2 @@ -722,7 +722,9 @@ module Atom = | Aapp ((i,op),a) -> let op_smt () = (match i with - | Index index -> Format.fprintf fmt "op_%i" index + | Index index -> + (Format.fprintf fmt "op_%i" index; + if debug then Format.fprintf fmt " (aka %s)" (Pp.string_of_ppcmds (CoqInterface.pr_constr op.op_val));) | Rel_name name -> Format.fprintf fmt "%s" name); if pi then to_smt_op op in @@ -740,7 +742,7 @@ module Atom = Array.iter (fun bt -> SmtBtype.to_smt fmt bt; Format.fprintf fmt " ") bta; Format.fprintf fmt ") ( "; SmtBtype.to_smt fmt bt; - Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Structures.pr_constr t)) + Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (CoqInterface.pr_constr t)) and to_smt_uop op h = match op with @@ -805,7 +807,7 @@ module Atom = in to_smt fmt h - let to_smt (fmt:Format.formatter) h = to_smt_named fmt h + let to_smt ?(debug=false) (fmt:Format.formatter) h = to_smt_named ~debug:debug fmt h type reify_tbl = @@ -855,7 +857,7 @@ module Atom = else ( Format.eprintf "Incorrect type: wanted %a, got %a@." SmtBtype.to_smt t SmtBtype.to_smt th; - failwith (Format.asprintf "Atom %a is not of the expected type" to_smt h) + failwith (Format.asprintf "Atom %a is not of the expected type" (to_smt ~debug:true) h) ) in @@ -1107,8 +1109,8 @@ module Atom = else CCunknown_deps (gobble_of_coq_cst cc) with Not_found -> CCunknown in - let rec mk_hatom (h : Structures.constr) = - let c, args = Structures.decompose_app h in + let rec mk_hatom (h : CoqInterface.constr) = + let c, args = CoqInterface.decompose_app h in match get_cst c with | CCxH -> mk_cop CCxH args | CCZ0 -> mk_cop CCZ0 args @@ -1150,9 +1152,9 @@ module Atom = | CCselect -> mk_bop_select args | CCdiff -> mk_bop_diff args | CCstore -> mk_top_store args - | CCunknown -> mk_unknown c args (Structures.retyping_get_type_of env sigma h) + | CCunknown -> mk_unknown c args (CoqInterface.retyping_get_type_of env sigma h) | CCunknown_deps gobble -> - mk_unknown_deps c args (Structures.retyping_get_type_of env sigma h) gobble + mk_unknown_deps c args (CoqInterface.retyping_get_type_of env sigma h) gobble and mk_cop op args = match op, args with @@ -1346,10 +1348,10 @@ module Atom = let (l1, l2) = collect_types xs in match l1 with | [] -> - let ty = Structures.retyping_get_type_of env sigma x in + let ty = CoqInterface.retyping_get_type_of env sigma x in if Constr.iskind ty || - let c, _ = Structures.decompose_app ty in - Structures.eq_constr c (Lazy.force cCompDec) + let c, _ = CoqInterface.decompose_app ty in + CoqInterface.eq_constr c (Lazy.force cCompDec) then ([x], xs) else @@ -1368,10 +1370,10 @@ module Atom = with | Not_found -> let targs = Array.map type_of hargs in let tres = SmtBtype.of_coq rt known_logic ty in - let os = if Structures.isRel c then - let i = Structures.destRel c in - let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in - Some (Structures.string_of_name n) + let os = if CoqInterface.isRel c then + let i = CoqInterface.destRel c in + let n, _ = CoqInterface.destruct_rel_decl (Environ.lookup_rel i env) in + Some (CoqInterface.string_of_name n) else if Vars.closed0 c then None else @@ -1394,7 +1396,7 @@ module Atom = [gobble] *) and mk_unknown_deps c args ty gobble = let deps, args = split_list_at gobble args in - let c = Structures.mkApp (c, Array.of_list deps) in + let c = CoqInterface.mkApp (c, Array.of_list deps) in mk_unknown c args ty in @@ -1435,7 +1437,7 @@ module Atom = let interp_tbl reify = let t = to_array reify (Lazy.force dft_atom) a_to_coq in - Structures.mkArray (Lazy.force catom, t) + CoqTerms.mkArray (Lazy.force catom, t) (** Producing a Coq term corresponding to the interpretation of an atom *) @@ -1447,12 +1449,12 @@ module Atom = let pc = match atom a with | Acop c -> Op.interp_cop c - | Auop (op,h) -> Structures.mkApp (Op.interp_uop op, [|interp_atom h|]) + | Auop (op,h) -> CoqInterface.mkApp (Op.interp_uop op, [|interp_atom h|]) | Abop (op,h1,h2) -> - Structures.mkApp (Op.interp_bop t_i op, + CoqInterface.mkApp (Op.interp_bop t_i op, [|interp_atom h1; interp_atom h2|]) | Atop (op,h1,h2,h3) -> - Structures.mkApp (Op.interp_top t_i op, + CoqInterface.mkApp (Op.interp_top t_i op, [|interp_atom h1; interp_atom h2; interp_atom h3|]) | Anop (NO_distinct ty as op,ha) -> let cop = Op.interp_nop t_i op in @@ -1460,9 +1462,9 @@ module Atom = let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in - Structures.mkApp (cop,[|cargs|]) + CoqInterface.mkApp (cop,[|cargs|]) | Aapp (op,t) -> - Structures.mkApp ((snd op).op_val, Array.map interp_atom t) in + CoqInterface.mkApp ((snd op).op_val, Array.map interp_atom t) in Hashtbl.add atom_tbl l pc; pc in interp_atom a diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index b430d6f..57992d2 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -76,14 +76,14 @@ module Op : val create : unit -> reify_tbl - val declare : reify_tbl -> Structures.constr -> btype array -> + val declare : reify_tbl -> CoqInterface.constr -> btype array -> btype -> string option -> indexed_op - val of_coq : reify_tbl -> Structures.constr -> indexed_op + val of_coq : reify_tbl -> CoqInterface.constr -> indexed_op - val interp_tbl : Structures.constr -> - (btype array -> btype -> Structures.constr -> Structures.constr) -> - reify_tbl -> Structures.constr + val interp_tbl : CoqInterface.constr -> + (btype array -> btype -> CoqInterface.constr -> CoqInterface.constr) -> + reify_tbl -> CoqInterface.constr val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list @@ -119,7 +119,7 @@ module Atom : val type_of : t -> btype - val to_smt : Format.formatter -> t -> unit + val to_smt : ?debug:bool -> Format.formatter -> t -> unit type reify_tbl @@ -142,18 +142,18 @@ module Atom : (** Given a coq term, build the corresponding atom *) exception UnknownUnderForall val of_coq : ?eqsym:bool -> SmtBtype.reify_tbl -> Op.reify_tbl -> - reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t + reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> CoqInterface.constr -> t - val get_coq_term_op : int -> Structures.constr + val get_coq_term_op : int -> CoqInterface.constr - val to_coq : t -> Structures.constr + val to_coq : t -> CoqInterface.constr val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array - val interp_tbl : reify_tbl -> Structures.constr + val interp_tbl : reify_tbl -> CoqInterface.constr - val interp_to_coq : Structures.constr -> (int, Structures.constr) Hashtbl.t -> - t -> Structures.constr + val interp_to_coq : CoqInterface.constr -> (int, CoqInterface.constr) Hashtbl.t -> + t -> CoqInterface.constr val logic : t -> SmtMisc.logic @@ -201,5 +201,5 @@ module Trace : sig end -val make_t_i : SmtBtype.reify_tbl -> Structures.constr -val make_t_func : Op.reify_tbl -> Structures.constr -> Structures.constr +val make_t_i : SmtBtype.reify_tbl -> CoqInterface.constr +val make_t_func : Op.reify_tbl -> CoqInterface.constr -> CoqInterface.constr diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index 71f7c14..fa3ed5f 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -19,7 +19,7 @@ type uninterpreted_type = (* Uninterpreted type for which a CompDec is already known The constr is of type typ_compdec *) - | CompDec of Structures.constr + | CompDec of CoqInterface.constr (* Uninterpreted type for which the knowledge of a CompDec is delayed until either: - one is used @@ -27,11 +27,11 @@ type uninterpreted_type = via a cut The constr is of type Type *) - | Delayed of Structures.constr + | Delayed of CoqInterface.constr type indexed_type = uninterpreted_type gen_hashed -let dummy_indexed_type i = {index = i; hval = Delayed (Structures.mkProp)} +let dummy_indexed_type i = {index = i; hval = Delayed (CoqInterface.mkProp)} let indexed_type_index i = i.index let indexed_type_compdec i = match i.hval with @@ -51,7 +51,7 @@ let index_tbl = Hashtbl.create 17 let index_to_coq i = try Hashtbl.find index_tbl i with Not_found -> - let interp = mklApp cTindex [|mkInt i|] in + let interp = mklApp cTindex [|mkN i|] in Hashtbl.add index_tbl i interp; interp @@ -105,8 +105,8 @@ let rec logic = function (* reify table *) type reify_tbl = { mutable count : int; - tbl : (Structures.constr, btype) Hashtbl.t; - mutable cuts : (Structures.id * Structures.types) list; + tbl : (CoqInterface.constr, btype) Hashtbl.t; + mutable cuts : (CoqInterface.id * CoqInterface.types) list; unsup_tbl : (btype, btype) Hashtbl.t; } @@ -145,8 +145,8 @@ let interp_tbl reify = | CompDec compdec -> t.(it.index) <- compdec; Some bt | Delayed ty -> let n = string_of_int (List.length reify.cuts) in - let compdec_name = Structures.mkId ("CompDec"^n) in - let compdec_var = Structures.mkVar compdec_name in + let compdec_name = CoqInterface.mkId ("CompDec"^n) in + let compdec_var = CoqInterface.mkVar compdec_name in let compdec_type = mklApp cCompDec [| ty |] in reify.cuts <- (compdec_name, compdec_type) :: reify.cuts; let ce = mklApp cTyp_compdec [|ty; compdec_var|] in @@ -156,7 +156,7 @@ let interp_tbl reify = | _ -> Some bt in Hashtbl.filter_map_inplace set reify.tbl; - Structures.mkArray (Lazy.force ctyp_compdec, t) + CoqTerms.mkArray (Lazy.force ctyp_compdec, t) let to_list reify = @@ -241,8 +241,8 @@ let rec compdec_btype reify = function | Tindex i -> (match i.hval with | CompDec compdec -> - let c, args = Structures.decompose_app compdec in - if Structures.eq_constr c (Lazy.force cTyp_compdec) then + let c, args = CoqInterface.decompose_app compdec in + if CoqInterface.eq_constr c (Lazy.force cTyp_compdec) then match args with | [_; tic] -> tic | _ -> assert false @@ -264,22 +264,22 @@ let declare_and_compdec reify t ty = let rec of_coq reify known_logic t = try - let c, args = Structures.decompose_app t in - if Structures.eq_constr c (Lazy.force cbool) || - Structures.eq_constr c (Lazy.force cTbool) then Tbool - else if Structures.eq_constr c (Lazy.force cZ) || - Structures.eq_constr c (Lazy.force cTZ) then + let c, args = CoqInterface.decompose_app t in + if CoqInterface.eq_constr c (Lazy.force cbool) || + CoqInterface.eq_constr c (Lazy.force cTbool) then Tbool + else if CoqInterface.eq_constr c (Lazy.force cZ) || + CoqInterface.eq_constr c (Lazy.force cTZ) then check_known TZ known_logic - else if Structures.eq_constr c (Lazy.force cpositive) || - Structures.eq_constr c (Lazy.force cTpositive) then + else if CoqInterface.eq_constr c (Lazy.force cpositive) || + CoqInterface.eq_constr c (Lazy.force cTpositive) then check_known Tpositive known_logic - else if Structures.eq_constr c (Lazy.force cbitvector) || - Structures.eq_constr c (Lazy.force cTBV) then + else if CoqInterface.eq_constr c (Lazy.force cbitvector) || + CoqInterface.eq_constr c (Lazy.force cTBV) then match args with | [s] -> check_known (TBV (mk_bvsize s)) known_logic | _ -> assert false - else if Structures.eq_constr c (Lazy.force cfarray) || - Structures.eq_constr c (Lazy.force cTFArray) then + else if CoqInterface.eq_constr c (Lazy.force cfarray) || + CoqInterface.eq_constr c (Lazy.force cTFArray) then match args with | ti :: te :: _ -> let ty = TFArray (of_coq reify known_logic ti, diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli index 05a8486..9503645 100644 --- a/src/trace/smtBtype.mli +++ b/src/trace/smtBtype.mli @@ -17,7 +17,7 @@ type indexed_type val dummy_indexed_type: int -> indexed_type val indexed_type_index : indexed_type -> int -val indexed_type_compdec : indexed_type -> Structures.constr +val indexed_type_compdec : indexed_type -> CoqInterface.constr type btype = | TZ @@ -31,7 +31,7 @@ val indexed_type_of_int : int -> indexed_type module HashedBtype : Hashtbl.HashedType with type t = btype -val to_coq : btype -> Structures.constr +val to_coq : btype -> CoqInterface.constr val to_smt : Format.formatter -> btype -> unit @@ -40,25 +40,25 @@ type reify_tbl val create : unit -> reify_tbl val copy : reify_tbl -> reify_tbl -val of_coq : reify_tbl -> logic -> Structures.constr -> btype -val of_coq_compdec : reify_tbl -> Structures.constr -> Structures.constr -> btype +val of_coq : reify_tbl -> logic -> CoqInterface.constr -> btype +val of_coq_compdec : reify_tbl -> CoqInterface.constr -> CoqInterface.constr -> btype -val get_coq_type_op : int -> Structures.constr +val get_coq_type_op : int -> CoqInterface.constr -val interp_tbl : reify_tbl -> Structures.constr +val interp_tbl : reify_tbl -> CoqInterface.constr val to_list : reify_tbl -> (int * indexed_type) list -val make_t_i : reify_tbl -> Structures.constr +val make_t_i : reify_tbl -> CoqInterface.constr -val dec_interp : Structures.constr -> btype -> Structures.constr -val ord_interp : Structures.constr -> btype -> Structures.constr -val comp_interp : Structures.constr -> btype -> Structures.constr -val inh_interp : Structures.constr -> btype -> Structures.constr -val interp : Structures.constr -> btype -> Structures.constr +val dec_interp : CoqInterface.constr -> btype -> CoqInterface.constr +val ord_interp : CoqInterface.constr -> btype -> CoqInterface.constr +val comp_interp : CoqInterface.constr -> btype -> CoqInterface.constr +val inh_interp : CoqInterface.constr -> btype -> CoqInterface.constr +val interp : CoqInterface.constr -> btype -> CoqInterface.constr -val interp_to_coq : reify_tbl -> btype -> Structures.constr +val interp_to_coq : reify_tbl -> btype -> CoqInterface.constr -val get_cuts : reify_tbl -> (Structures.id * Structures.types) list +val get_cuts : reify_tbl -> (CoqInterface.id * CoqInterface.types) list val logic : btype -> logic diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml index 33437bf..3264d9e 100644 --- a/src/trace/smtCertif.ml +++ b/src/trace/smtCertif.ml @@ -98,11 +98,11 @@ type 'hform rule = *) (* Linear arithmetic *) - | LiaMicromega of 'hform list * Structures.Micromega_plugin_Certificate.Mc.zArithProof list + | LiaMicromega of 'hform list * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list | LiaDiseq of 'hform (* Arithmetic simplifications *) - | SplArith of 'hform clause * 'hform * Structures.Micromega_plugin_Certificate.Mc.zArithProof list + | SplArith of 'hform clause * 'hform * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list (* Elimination of operators *) | SplDistinctElim of 'hform clause * 'hform diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli index ef25b1f..999131c 100644 --- a/src/trace/smtCertif.mli +++ b/src/trace/smtCertif.mli @@ -96,11 +96,11 @@ type 'hform rule = *) (* Linear arithmetic *) - | LiaMicromega of 'hform list * Structures.Micromega_plugin_Certificate.Mc.zArithProof list + | LiaMicromega of 'hform list * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list | LiaDiseq of 'hform (* Arithmetic simplifications *) - | SplArith of 'hform clause * 'hform * Structures.Micromega_plugin_Certificate.Mc.zArithProof list + | SplArith of 'hform clause * 'hform * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list (* Elimination of operators *) | SplDistinctElim of 'hform clause * 'hform diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index d15ae68..2108da4 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -18,65 +18,57 @@ open SmtTrace open SmtCertif -let euf_checker_modules = [ ["SMTCoq";"Trace";"Euf_Checker"] ] -let certif_ops args = CoqTerms.make_certif_ops euf_checker_modules args -let cCertif = gen_constant euf_checker_modules "Certif" -let ccertif = gen_constant euf_checker_modules "certif" -let cchecker = gen_constant euf_checker_modules "checker" -let cchecker_correct = gen_constant euf_checker_modules "checker_correct" -let cchecker_b_correct = - gen_constant euf_checker_modules "checker_b_correct" -let cchecker_b = gen_constant euf_checker_modules "checker_b" -let cchecker_eq_correct = - gen_constant euf_checker_modules "checker_eq_correct" -let cchecker_eq = gen_constant euf_checker_modules "checker_eq" -(* let csetup_checker_step_debug = - * gen_constant euf_checker_modules "setup_checker_step_debug" *) -(* let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug" *) -(* let cstep = gen_constant euf_checker_modules "step" *) -let cchecker_debug = gen_constant euf_checker_modules "checker_debug" - -let cname_step = gen_constant euf_checker_modules "name_step" - -let cName_Res = gen_constant euf_checker_modules "Name_Res" -let cName_Weaken= gen_constant euf_checker_modules "Name_Weaken" -let cName_ImmFlatten= gen_constant euf_checker_modules "Name_ImmFlatten" -let cName_CTrue= gen_constant euf_checker_modules "Name_CTrue" -let cName_CFalse = gen_constant euf_checker_modules "Name_CFalse" -let cName_BuildDef= gen_constant euf_checker_modules "Name_BuildDef" -let cName_BuildDef2= gen_constant euf_checker_modules "Name_BuildDef2" -let cName_BuildProj = gen_constant euf_checker_modules "Name_BuildProj" -let cName_ImmBuildDef= gen_constant euf_checker_modules "Name_ImmBuildDef" -let cName_ImmBuildDef2= gen_constant euf_checker_modules "Name_ImmBuildDef2" -let cName_ImmBuildProj = gen_constant euf_checker_modules "Name_ImmBuildProj" -let cName_EqTr = gen_constant euf_checker_modules "Name_EqTr" -let cName_EqCgr = gen_constant euf_checker_modules "Name_EqCgr" -let cName_EqCgrP= gen_constant euf_checker_modules "Name_EqCgrP" -let cName_LiaMicromega = gen_constant euf_checker_modules "Name_LiaMicromega" -let cName_LiaDiseq= gen_constant euf_checker_modules "Name_LiaDiseq" -let cName_SplArith= gen_constant euf_checker_modules "Name_SplArith" -let cName_SplDistinctElim = gen_constant euf_checker_modules "Name_SplDistinctElim" -let cName_BBVar= gen_constant euf_checker_modules "Name_BBVar" -let cName_BBConst= gen_constant euf_checker_modules "Name_BBConst" -let cName_BBOp= gen_constant euf_checker_modules "Name_BBOp" -let cName_BBNot= gen_constant euf_checker_modules "Name_BBNot" -let cName_BBNeg= gen_constant euf_checker_modules "Name_BBNeg" -let cName_BBAdd= gen_constant euf_checker_modules "Name_BBAdd" -let cName_BBConcat= gen_constant euf_checker_modules "Name_BBConcat" -let cName_BBMul= gen_constant euf_checker_modules "Name_BBMul" -let cName_BBUlt= gen_constant euf_checker_modules "Name_BBUlt" -let cName_BBSlt= gen_constant euf_checker_modules "Name_BBSlt" -let cName_BBEq= gen_constant euf_checker_modules "Name_BBEq" -let cName_BBDiseq= gen_constant euf_checker_modules "Name_BBDiseq" -let cName_BBExtract= gen_constant euf_checker_modules "Name_BBExtract" -let cName_BBZextend= gen_constant euf_checker_modules "Name_BBZextend" -let cName_BBSextend= gen_constant euf_checker_modules "Name_BBSextend" -let cName_BBShl= gen_constant euf_checker_modules "Name_BBShl" -let cName_BBShr= gen_constant euf_checker_modules "Name_BBShr" -let cName_RowEq= gen_constant euf_checker_modules "Name_RowEq" -let cName_RowNeq= gen_constant euf_checker_modules "Name_RowNeq" -let cName_Ext= gen_constant euf_checker_modules "Name_Ext" -let cName_Hole= gen_constant euf_checker_modules "Name_Hole" +let certif_ops = CoqTerms.ceuf_checker_certif_ops +let cCertif = CoqTerms.ceuf_checker_Certif +let ccertif = CoqTerms.ceuf_checker_certif +let cchecker = CoqTerms.ceuf_checker_checker +let cchecker_correct = CoqTerms.ceuf_checker_checker_correct +let cchecker_b_correct = CoqTerms.ceuf_checker_checker_b_correct +let cchecker_b = CoqTerms.ceuf_checker_checker_b +let cchecker_eq_correct = CoqTerms.ceuf_checker_checker_eq_correct +let cchecker_eq = CoqTerms.ceuf_checker_checker_eq +let cchecker_debug = CoqTerms.ceuf_checker_checker_debug +let cname_step = CoqTerms.ceuf_checker_name_step +let cName_Res = CoqTerms.ceuf_checker_Name_Res +let cName_Weaken = CoqTerms.ceuf_checker_Name_Weaken +let cName_ImmFlatten = CoqTerms.ceuf_checker_Name_ImmFlatten +let cName_CTrue = CoqTerms.ceuf_checker_Name_CTrue +let cName_CFalse = CoqTerms.ceuf_checker_Name_CFalse +let cName_BuildDef = CoqTerms.ceuf_checker_Name_BuildDef +let cName_BuildDef2 = CoqTerms.ceuf_checker_Name_BuildDef2 +let cName_BuildProj = CoqTerms.ceuf_checker_Name_BuildProj +let cName_ImmBuildDef = CoqTerms.ceuf_checker_Name_ImmBuildDef +let cName_ImmBuildDef2 = CoqTerms.ceuf_checker_Name_ImmBuildDef2 +let cName_ImmBuildProj = CoqTerms.ceuf_checker_Name_ImmBuildProj +let cName_EqTr = CoqTerms.ceuf_checker_Name_EqTr +let cName_EqCgr = CoqTerms.ceuf_checker_Name_EqCgr +let cName_EqCgrP = CoqTerms.ceuf_checker_Name_EqCgrP +let cName_LiaMicromega = CoqTerms.ceuf_checker_Name_LiaMicromega +let cName_LiaDiseq = CoqTerms.ceuf_checker_Name_LiaDiseq +let cName_SplArith = CoqTerms.ceuf_checker_Name_SplArith +let cName_SplDistinctElim = CoqTerms.ceuf_checker_Name_SplDistinctElim +let cName_BBVar = CoqTerms.ceuf_checker_Name_BBVar +let cName_BBConst = CoqTerms.ceuf_checker_Name_BBConst +let cName_BBOp = CoqTerms.ceuf_checker_Name_BBOp +let cName_BBNot = CoqTerms.ceuf_checker_Name_BBNot +let cName_BBNeg = CoqTerms.ceuf_checker_Name_BBNeg +let cName_BBAdd = CoqTerms.ceuf_checker_Name_BBAdd +let cName_BBConcat = CoqTerms.ceuf_checker_Name_BBConcat +let cName_BBMul = CoqTerms.ceuf_checker_Name_BBMul +let cName_BBUlt = CoqTerms.ceuf_checker_Name_BBUlt +let cName_BBSlt = CoqTerms.ceuf_checker_Name_BBSlt +let cName_BBEq = CoqTerms.ceuf_checker_Name_BBEq +let cName_BBDiseq = CoqTerms.ceuf_checker_Name_BBDiseq +let cName_BBExtract = CoqTerms.ceuf_checker_Name_BBExtract +let cName_BBZextend = CoqTerms.ceuf_checker_Name_BBZextend +let cName_BBSextend = CoqTerms.ceuf_checker_Name_BBSextend +let cName_BBShl = CoqTerms.ceuf_checker_Name_BBShl +let cName_BBShr = CoqTerms.ceuf_checker_Name_BBShr +let cName_RowEq = CoqTerms.ceuf_checker_Name_RowEq +let cName_RowNeq = CoqTerms.ceuf_checker_Name_RowNeq +let cName_Ext = CoqTerms.ceuf_checker_Name_Ext +let cName_Hole = CoqTerms.ceuf_checker_Name_Hole + (* Given an SMT-LIB2 file and a certif, build the corresponding objects *) @@ -115,7 +107,7 @@ let interp_conseq_uf t_i (prem, concl) = let tf = Hashtbl.create 17 in let rec interp = function | [] -> mklApp cis_true [|interp_uf t_i ta tf concl|] - | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in + | c::prem -> CoqInterface.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in interp prem @@ -127,26 +119,26 @@ let print_assm ty = let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, roots, max_id, confl) = let t_i' = make_t_i rt in - let ce5 = Structures.mkUConst t_i' in - let ct_i = Structures.mkConst (Structures.declare_constant t_i ce5) in + let ce5 = CoqInterface.mkUConst t_i' in + let ct_i = CoqInterface.mkConst (CoqInterface.declare_constant t_i ce5) in let t_func' = make_t_func ro ct_i in - let ce6 = Structures.mkUConst t_func' in - let ct_func = Structures.mkConst (Structures.declare_constant t_func ce6) in + let ce6 = CoqInterface.mkUConst t_func' in + let ct_func = CoqInterface.mkConst (CoqInterface.declare_constant t_func ce6) in let t_atom' = Atom.interp_tbl ra in - let ce1 = Structures.mkUConst t_atom' in - let ct_atom = Structures.mkConst (Structures.declare_constant t_atom ce1) in + let ce1 = CoqInterface.mkUConst t_atom' in + let ct_atom = CoqInterface.mkConst (CoqInterface.declare_constant t_atom ce1) in let t_form' = snd (Form.interp_tbl rf) in - let ce2 = Structures.mkUConst t_form' in - let ct_form = Structures.mkConst (Structures.declare_constant t_form ce2) in + let ce2 = CoqInterface.mkUConst t_form' in + let ct_form = CoqInterface.mkConst (CoqInterface.declare_constant t_form ce2) in (* EMPTY LEMMA LIST *) let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) (interp_conseq_uf ct_i) (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in List.iter (fun (v,ty) -> - let _ = Structures.declare_new_variable v ty in + let _ = CoqInterface.declare_new_variable v ty in print_assm ty ) cuts; @@ -155,22 +147,22 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - Structures.mkArray (Lazy.force cint, res) in + CoqTerms.mkArray (Lazy.force cint, res) in let used_roots = let l = List.length used_roots in let res = Array.make (l + 1) (mkInt 0) in let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in - let ce3 = Structures.mkUConst roots in - let _ = Structures.declare_constant root ce3 in - let ce3' = Structures.mkUConst used_roots in - let _ = Structures.declare_constant used_root ce3' in + mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in + let ce3 = CoqInterface.mkUConst roots in + let _ = CoqInterface.declare_constant root ce3 in + let ce3' = CoqInterface.mkUConst used_roots in + let _ = CoqInterface.declare_constant used_root ce3' in let certif = mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - let ce4 = Structures.mkUConst certif in - let _ = Structures.declare_constant trace ce4 in + let ce4 = CoqInterface.mkUConst certif in + let _ = CoqInterface.declare_constant trace ce4 in () @@ -184,15 +176,15 @@ let interp_roots t_i roots = | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots let theorem name (rt, ro, ra, rf, roots, max_id, confl) = - let nti = Structures.mkName "t_i" in - let ntfunc = Structures.mkName "t_func" in - let ntatom = Structures.mkName "t_atom" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in - let nused_roots = Structures.mkName "used_roots" in - let nd = Structures.mkName "d" in + let nti = CoqInterface.mkName "t_i" in + let ntfunc = CoqInterface.mkName "t_func" in + let ntatom = CoqInterface.mkName "t_atom" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in + let nused_roots = CoqInterface.mkName "used_roots" in + let nd = CoqInterface.mkName "d" in - let v = Structures.mkRel in + let v = CoqInterface.mkRel in let t_i = make_t_i rt in let t_func = make_t_func ro (v 1 (*t_i*)) in @@ -204,7 +196,7 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) = (interp_conseq_uf t_i) (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in List.iter (fun (v,ty) -> - let _ = Structures.declare_new_variable v ty in + let _ = CoqInterface.declare_new_variable v ty in print_assm ty ) cuts; @@ -217,59 +209,59 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) = let res = Array.make (l + 1) (mkInt 0) in let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in + mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in let rootsCstr = let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - Structures.mkArray (Lazy.force cint, res) in + CoqTerms.mkArray (Lazy.force cint, res) in let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in let theorem_proof_cast = - Structures.mkCast ( - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + CoqInterface.mkCast ( + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], + CoqInterface.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker_correct [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*); vm_cast_true_no_check (mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|])|]))))))), - Structures.vmcast, + CoqInterface.vmcast, theorem_concl) in let theorem_proof_nocast = - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], + CoqInterface.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker_correct [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in - let ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_concl in - let _ = Structures.declare_constant name ce in + let ce = CoqInterface.mkTConst theorem_proof_cast theorem_proof_nocast theorem_concl in + let _ = CoqInterface.declare_constant name ce in () (* Given an SMT-LIB2 file and a certif, call the checker *) let checker (rt, ro, ra, rf, roots, max_id, confl) = - let nti = Structures.mkName "t_i" in - let ntfunc = Structures.mkName "t_func" in - let ntatom = Structures.mkName "t_atom" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in - let nused_roots = Structures.mkName "used_roots" in - let nd = Structures.mkName "d" in + let nti = CoqInterface.mkName "t_i" in + let ntfunc = CoqInterface.mkName "t_func" in + let ntatom = CoqInterface.mkName "t_atom" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in + let nused_roots = CoqInterface.mkName "used_roots" in + let nd = CoqInterface.mkName "d" in - let v = Structures.mkRel in + let v = CoqInterface.mkRel in let t_i = make_t_i rt in let t_func = make_t_func ro (v 1 (*t_i*)) in @@ -281,7 +273,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) = (interp_conseq_uf t_i) (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in List.iter (fun (v,ty) -> - let _ = Structures.declare_new_variable v ty in + let _ = CoqInterface.declare_new_variable v ty in print_assm ty ) cuts; @@ -294,26 +286,26 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) = let res = Array.make (l + 1) (mkInt 0) in let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in + mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in let rootsCstr = let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - Structures.mkArray (Lazy.force cint, res) in + CoqTerms.mkArray (Lazy.force cint, res) in let tm = - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], + CoqInterface.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in - let res = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in + let res = CoqInterface.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in Format.eprintf " = %s\n : bool@." - (if Structures.eq_constr res (Lazy.force CoqTerms.ctrue) then + (if CoqInterface.eq_constr res (Lazy.force CoqTerms.ctrue) then "true" else "false") let count_used confl = @@ -329,15 +321,15 @@ let count_used confl = let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = - let nti = Structures.mkName "t_i" in - let ntfunc = Structures.mkName "t_func" in - let ntatom = Structures.mkName "t_atom" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in - let nused_roots = Structures.mkName "used_roots" in - let nd = Structures.mkName "d" in + let nti = CoqInterface.mkName "t_i" in + let ntfunc = CoqInterface.mkName "t_func" in + let ntatom = CoqInterface.mkName "t_atom" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in + let nused_roots = CoqInterface.mkName "used_roots" in + let nd = CoqInterface.mkName "d" in - let v = Structures.mkRel in + let v = CoqInterface.mkRel in let t_i = make_t_i rt in let t_func = make_t_func ro (v 1 (*t_i*)) in @@ -349,7 +341,7 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in List.iter (fun (v,ty) -> - let _ = Structures.declare_new_variable v ty in + let _ = CoqInterface.declare_new_variable v ty in print_assm ty ) cuts; @@ -364,84 +356,84 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; mklApp cSome [|mklApp carray [|Lazy.force cint|]; - Structures.mkArray (Lazy.force cint, res)|] in + CoqTerms.mkArray (Lazy.force cint, res)|] in let rootsCstr = let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - Structures.mkArray (Lazy.force cint, res) in + CoqTerms.mkArray (Lazy.force cint, res) in let tm = - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Structures.mkLetIn (nused_roots, used_rootsCstr, + CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + CoqInterface.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker_debug [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in - let res = Structures.cbv_vm (Global.env ()) tm + let res = CoqInterface.cbv_vm (Global.env ()) tm (mklApp coption [|mklApp cprod [|Lazy.force cnat; Lazy.force cname_step|]|]) in - match Structures.decompose_app res with - | c, _ when Structures.eq_constr c (Lazy.force cNone) -> - Structures.error ("Debug checker is only meant to be used for certificates \ + match CoqInterface.decompose_app res with + | c, _ when CoqInterface.eq_constr c (Lazy.force cNone) -> + CoqInterface.error ("Debug checker is only meant to be used for certificates \ that fail to be checked by SMTCoq.") - | c, [_; n] when Structures.eq_constr c (Lazy.force cSome) -> - (match Structures.decompose_app n with - | c, [_; _; cnb; cn] when Structures.eq_constr c (Lazy.force cpair) -> - let n = fst (Structures.decompose_app cn) in + | c, [_; n] when CoqInterface.eq_constr c (Lazy.force cSome) -> + (match CoqInterface.decompose_app n with + | c, [_; _; cnb; cn] when CoqInterface.eq_constr c (Lazy.force cpair) -> + let n = fst (CoqInterface.decompose_app cn) in let name = - if Structures.eq_constr n (Lazy.force cName_Res ) then "Res" - else if Structures.eq_constr n (Lazy.force cName_Weaken) then "Weaken" - else if Structures.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten" - else if Structures.eq_constr n (Lazy.force cName_CTrue) then "CTrue" - else if Structures.eq_constr n (Lazy.force cName_CFalse ) then "CFalse" - else if Structures.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef" - else if Structures.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2" - else if Structures.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj" - else if Structures.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef" - else if Structures.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2" - else if Structures.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj" - else if Structures.eq_constr n (Lazy.force cName_EqTr ) then "EqTr" - else if Structures.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr" - else if Structures.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP" - else if Structures.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega" - else if Structures.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq" - else if Structures.eq_constr n (Lazy.force cName_SplArith) then "SplArith" - else if Structures.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim" - else if Structures.eq_constr n (Lazy.force cName_BBVar) then "BBVar" - else if Structures.eq_constr n (Lazy.force cName_BBConst) then "BBConst" - else if Structures.eq_constr n (Lazy.force cName_BBOp) then "BBOp" - else if Structures.eq_constr n (Lazy.force cName_BBNot) then "BBNot" - else if Structures.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg" - else if Structures.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd" - else if Structures.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat" - else if Structures.eq_constr n (Lazy.force cName_BBMul) then "BBMul" - else if Structures.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt" - else if Structures.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt" - else if Structures.eq_constr n (Lazy.force cName_BBEq) then "BBEq" - else if Structures.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq" - else if Structures.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract" - else if Structures.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend" - else if Structures.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend" - else if Structures.eq_constr n (Lazy.force cName_BBShl) then "BBShl" - else if Structures.eq_constr n (Lazy.force cName_BBShr) then "BBShr" - else if Structures.eq_constr n (Lazy.force cName_RowEq) then "RowEq" - else if Structures.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq" - else if Structures.eq_constr n (Lazy.force cName_Ext) then "Ext" - else if Structures.eq_constr n (Lazy.force cName_Hole) then "Hole" + if CoqInterface.eq_constr n (Lazy.force cName_Res ) then "Res" + else if CoqInterface.eq_constr n (Lazy.force cName_Weaken) then "Weaken" + else if CoqInterface.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten" + else if CoqInterface.eq_constr n (Lazy.force cName_CTrue) then "CTrue" + else if CoqInterface.eq_constr n (Lazy.force cName_CFalse ) then "CFalse" + else if CoqInterface.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef" + else if CoqInterface.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2" + else if CoqInterface.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj" + else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef" + else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2" + else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj" + else if CoqInterface.eq_constr n (Lazy.force cName_EqTr ) then "EqTr" + else if CoqInterface.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr" + else if CoqInterface.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP" + else if CoqInterface.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega" + else if CoqInterface.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq" + else if CoqInterface.eq_constr n (Lazy.force cName_SplArith) then "SplArith" + else if CoqInterface.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim" + else if CoqInterface.eq_constr n (Lazy.force cName_BBVar) then "BBVar" + else if CoqInterface.eq_constr n (Lazy.force cName_BBConst) then "BBConst" + else if CoqInterface.eq_constr n (Lazy.force cName_BBOp) then "BBOp" + else if CoqInterface.eq_constr n (Lazy.force cName_BBNot) then "BBNot" + else if CoqInterface.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg" + else if CoqInterface.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd" + else if CoqInterface.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat" + else if CoqInterface.eq_constr n (Lazy.force cName_BBMul) then "BBMul" + else if CoqInterface.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt" + else if CoqInterface.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt" + else if CoqInterface.eq_constr n (Lazy.force cName_BBEq) then "BBEq" + else if CoqInterface.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq" + else if CoqInterface.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract" + else if CoqInterface.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend" + else if CoqInterface.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend" + else if CoqInterface.eq_constr n (Lazy.force cName_BBShl) then "BBShl" + else if CoqInterface.eq_constr n (Lazy.force cName_BBShr) then "BBShr" + else if CoqInterface.eq_constr n (Lazy.force cName_RowEq) then "RowEq" + else if CoqInterface.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq" + else if CoqInterface.eq_constr n (Lazy.force cName_Ext) then "Ext" + else if CoqInterface.eq_constr n (Lazy.force cName_Hole) then "Hole" else string_coq_constr n in let nb = mk_nat cnb + List.length roots + (confl.id + 1 - count_used confl) in - Structures.error ("Step number " ^ string_of_int nb ^ + CoqInterface.error ("Step number " ^ string_of_int nb ^ " (" ^ name ^ ") of the certificate likely failed.") | _ -> assert false ) @@ -450,9 +442,9 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = (* let rec of_coq_list cl = - * match Structures.decompose_app cl with - * | c, _ when Structures.eq_constr c (Lazy.force cnil) -> [] - * | c, [_; x; cr] when Structures.eq_constr c (Lazy.force ccons) -> + * match CoqInterface.decompose_app cl with + * | c, _ when CoqInterface.eq_constr c (Lazy.force cnil) -> [] + * | c, [_; x; cr] when CoqInterface.eq_constr c (Lazy.force ccons) -> * x :: of_coq_list cr * | _ -> assert false *) @@ -461,29 +453,29 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * (rt, ro, ra, rf, roots, max_id, confl) = * * let t_i' = make_t_i rt in - * let ce5 = Structures.mkUConst t_i' in - * let ct_i = Structures.mkConst (Structures.declare_constant t_i ce5) in + * let ce5 = CoqInterface.mkUConst t_i' in + * let ct_i = CoqInterface.mkConst (CoqInterface.declare_constant t_i ce5) in * * let t_func' = make_t_func ro ct_i in - * let ce6 = Structures.mkUConst t_func' in + * let ce6 = CoqInterface.mkUConst t_func' in * let ct_func = - * Structures.mkConst (Structures.declare_constant t_func ce6) in + * CoqInterface.mkConst (CoqInterface.declare_constant t_func ce6) in * * let t_atom' = Atom.interp_tbl ra in - * let ce1 = Structures.mkUConst t_atom' in + * let ce1 = CoqInterface.mkUConst t_atom' in * let ct_atom = - * Structures.mkConst (Structures.declare_constant t_atom ce1) in + * CoqInterface.mkConst (CoqInterface.declare_constant t_atom ce1) in * * let t_form' = snd (Form.interp_tbl rf) in - * let ce2 = Structures.mkUConst t_form' in + * let ce2 = CoqInterface.mkUConst t_form' in * let ct_form = - * Structures.mkConst (Structures.declare_constant t_form ce2) in + * CoqInterface.mkConst (CoqInterface.declare_constant t_form ce2) in * * let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) * (interp_conseq_uf ct_i) * (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in * List.iter (fun (v,ty) -> - * let _ = Structures.declare_new_variable v ty in + * let _ = CoqInterface.declare_new_variable v ty in * print_assm ty * ) cuts; * @@ -492,37 +484,37 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * let res = Array.make (List.length roots + 1) (mkInt 0) in * let i = ref 0 in * List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - * Structures.mkArray (Lazy.force cint, res) in + * CoqTerms.mkArray (Lazy.force cint, res) in * let cused_roots = * let l = List.length used_roots in * let res = Array.make (l + 1) (mkInt 0) in * let i = ref (l-1) in * List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; * mklApp cSome [|mklApp carray [|Lazy.force cint|]; - * Structures.mkArray (Lazy.force cint, res)|] in - * let ce3 = Structures.mkUConst croots in - * let _ = Structures.declare_constant root ce3 in - * let ce3' = Structures.mkUConst cused_roots in - * let _ = Structures.declare_constant used_root ce3' in + * CoqTerms.mkArray (Lazy.force cint, res)|] in + * let ce3 = CoqInterface.mkUConst croots in + * let _ = CoqInterface.declare_constant root ce3 in + * let ce3' = CoqInterface.mkUConst cused_roots in + * let _ = CoqInterface.declare_constant used_root ce3' in * * let certif = * mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1); * tres;mkInt (get_pos confl)|] in - * let ce4 = Structures.mkUConst certif in - * let _ = Structures.declare_constant trace ce4 in + * let ce4 = CoqInterface.mkUConst certif in + * let _ = CoqInterface.declare_constant trace ce4 in * * let setup = * mklApp csetup_checker_step_debug * [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in * - * let setup = Structures.cbv_vm (Global.env ()) setup + * let setup = CoqInterface.cbv_vm (Global.env ()) setup * (mklApp cprod * [|Lazy.force cState_S_t; * mklApp clist [|mklApp cstep * [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in * - * let s, steps = match Structures.decompose_app setup with - * | c, [_; _; s; csteps] when Structures.eq_constr c (Lazy.force cpair) -> + * let s, steps = match CoqInterface.decompose_app setup with + * | c, [_; _; s; csteps] when CoqInterface.eq_constr c (Lazy.force cpair) -> * s, of_coq_list csteps * | _ -> assert false * in @@ -536,22 +528,22 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * [| ct_i; ct_func; ct_atom; ct_form; s; step |] in * * let res = - * Structures.cbv_vm (Global.env ()) tm + * CoqInterface.cbv_vm (Global.env ()) tm * (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in * - * match Structures.decompose_app res with - * | c, [_; _; s; cbad] when Structures.eq_constr c (Lazy.force cpair) -> + * match CoqInterface.decompose_app res with + * | c, [_; _; s; cbad] when CoqInterface.eq_constr c (Lazy.force cpair) -> * if not (mk_bool cbad) then s - * else Structures.error ("Step number " ^ string_of_int !cpt ^ + * else CoqInterface.error ("Step number " ^ string_of_int !cpt ^ * " (" ^ string_coq_constr - * (fst (Structures.decompose_app step)) ^ ")" ^ + * (fst (CoqInterface.decompose_app step)) ^ ")" ^ * " of the certificate likely failed." ) * | _ -> assert false * in * * List.fold_left debug_step s steps |> ignore; * - * Structures.error ("Debug checker is only meant to be used for certificates \ + * CoqInterface.error ("Debug checker is only meant to be used for certificates \ * that fail to be checked by SMTCoq.") *) @@ -559,16 +551,16 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = (* Tactic *) let build_body rt ro ra rf l b (max_id, confl) vm_cast find = - let nti = Structures.mkName "t_i" in - let ntfunc = Structures.mkName "t_func" in - let ntatom = Structures.mkName "t_atom" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in + let nti = CoqInterface.mkName "t_i" in + let ntfunc = CoqInterface.mkName "t_func" in + let ntatom = CoqInterface.mkName "t_atom" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in - let v = Structures.mkRel in + let v = CoqInterface.mkRel in let t_i = make_t_i rt in - let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in + let t_func = CoqInterface.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in let t_atom = Atom.interp_tbl ra in let t_form = snd (Form.interp_tbl rf) in let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq @@ -583,11 +575,11 @@ let build_body rt ro ra rf l b (max_id, confl) vm_cast find = mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let add_lets t = - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], t))))) in @@ -614,16 +606,16 @@ let build_body rt ro ra rf l b (max_id, confl) vm_cast find = let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find = - let nti = Structures.mkName "t_i" in - let ntfunc = Structures.mkName "t_func" in - let ntatom = Structures.mkName "t_atom" in - let ntform = Structures.mkName "t_form" in - let nc = Structures.mkName "c" in + let nti = CoqInterface.mkName "t_i" in + let ntfunc = CoqInterface.mkName "t_func" in + let ntatom = CoqInterface.mkName "t_atom" in + let ntform = CoqInterface.mkName "t_form" in + let nc = CoqInterface.mkName "c" in - let v = Structures.mkRel in + let v = CoqInterface.mkRel in let t_i = make_t_i rt in - let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i*))) in + let t_func = CoqInterface.lift 1 (make_t_func ro (v 0 (*t_i*))) in let t_atom = Atom.interp_tbl ra in let t_form = snd (Form.interp_tbl rf) in let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq @@ -633,11 +625,11 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find = mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let add_lets t = - Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], - Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Structures.mkLetIn (nc, certif, mklApp ccertif + CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], + CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], t))))) in @@ -665,10 +657,10 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find = let get_arguments concl = - let f, args = Structures.decompose_app concl in + let f, args = CoqInterface.decompose_app concl in match args with - | [ty;a;b] when (Structures.eq_constr f (Lazy.force ceq)) && (Structures.eq_constr ty (Lazy.force cbool)) -> a, b - | [a] when (Structures.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue + | [ty;a;b] when (CoqInterface.eq_constr f (Lazy.force ceq)) && (CoqInterface.eq_constr ty (Lazy.force cbool)) -> a, b + | [a] when (CoqInterface.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue | _ -> failwith ("Verit.tactic: can only deal with equality over bool") @@ -689,7 +681,7 @@ let gen_rel_name = let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = let warn () = - Structures.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr (Structures.extern_constr clemma)))); + CoqInterface.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (CoqInterface.extern_constr clemma)))); None in @@ -698,16 +690,16 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = let rel_context = List.map (fun rel -> Context.Rel.Declaration.set_name (Names.Name.mk_name (Names.Id.of_string (gen_rel_name ()))) rel) rel_context in let env_lemma = Environ.push_rel_context rel_context env in - let f, args = Structures.decompose_app qf_lemma in + let f, args = CoqInterface.decompose_app qf_lemma in let core_f = - if Structures.eq_constr f (Lazy.force cis_true) then + if CoqInterface.eq_constr f (Lazy.force cis_true) then match args with | [a] -> Some a | _ -> warn () - else if Structures.eq_constr f (Lazy.force ceq) then + else if CoqInterface.eq_constr f (Lazy.force ceq) then match args with - | [ty; arg1; arg2] when Structures.eq_constr ty (Lazy.force cbool) && - Structures.eq_constr arg2 (Lazy.force ctrue) -> + | [ty; arg1; arg2] when CoqInterface.eq_constr ty (Lazy.force cbool) && + CoqInterface.eq_constr arg2 (Lazy.force ctrue) -> Some arg1 | _ -> warn () else warn () in @@ -722,8 +714,8 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = | None -> None in let forall_args = - let fmap r = let n, t = Structures.destruct_rel_decl r in - Structures.string_of_name n, SmtBtype.of_coq rt solver_logic t in + let fmap r = let n, t = CoqInterface.destruct_rel_decl r in + CoqInterface.string_of_name n, SmtBtype.of_coq rt solver_logic t in List.map fmap rel_context in match forall_args with @@ -736,11 +728,11 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl env sigma concl = let a, b = get_arguments concl in - let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in + let tlcepl = List.map (CoqInterface.interp_constr env sigma) lcepl in let lcpl = lcpl @ tlcepl in let create_lemma l = - let cl = Structures.retyping_get_type_of env sigma l in + let cl = CoqInterface.retyping_get_type_of env sigma l in match of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic cl with | Some smt -> Some ((cl, l), smt) | None -> None @@ -748,7 +740,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l let l_pl_ls = SmtMisc.filter_map create_lemma lcpl in let lsmt = List.map snd l_pl_ls in - let lem_tbl : (int, Structures.constr * Structures.constr) Hashtbl.t = + let lem_tbl : (int, CoqInterface.constr * CoqInterface.constr) Hashtbl.t = Hashtbl.create 100 in let new_ref ((l, pl), ls) = Hashtbl.add lem_tbl (Form.index ls) (l, pl) in @@ -770,11 +762,11 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l | _ -> failwith "unexpected form of root" in let (body_cast, body_nocast, cuts) = - if ((Structures.eq_constr b (Lazy.force ctrue)) || - (Structures.eq_constr b (Lazy.force cfalse))) then ( + if ((CoqInterface.eq_constr b (Lazy.force ctrue)) || + (CoqInterface.eq_constr b (Lazy.force cfalse))) then ( let l = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in let _ = Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env sigma) rf_quant a in - let nl = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in + let nl = if (CoqInterface.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in let lsmt = Form.flatten rf nl :: lsmt in let max_id_confl = make_proof call_solver env rt ro ra_quant rf_quant nl lsmt in build_body rt ro ra rf (Form.to_coq l) b max_id_confl (vm_cast env) (Some find_lemma) @@ -793,19 +785,19 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l let cuts = (SmtBtype.get_cuts rt) @ cuts in List.fold_right (fun (eqn, eqt) tac -> - Structures.tclTHENLAST - (Structures.assert_before (Structures.name_of_id eqn) eqt) + CoqInterface.tclTHENLAST + (CoqInterface.assert_before (CoqInterface.name_of_id eqn) eqt) tac ) cuts - (Structures.tclTHEN - (Structures.set_evars_tac body_nocast) - (Structures.vm_cast_no_check body_cast)) + (CoqInterface.tclTHEN + (CoqInterface.set_evars_tac body_nocast) + (CoqInterface.vm_cast_no_check body_cast)) let tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl = - Structures.tclTHEN + CoqInterface.tclTHEN Tactics.intros - (Structures.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl)) + (CoqInterface.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl)) (**********************************************) @@ -822,7 +814,7 @@ let string_index_of_constr env i cf = try let s = string_coq_constr cf in let nc = Environ.named_context env in - let nd = Environ.lookup_named (Structures.mkId s) env in + let nd = Environ.lookup_named (CoqInterface.mkId s) env in let cpt = ref 0 in (try List.iter (fun n -> incr cpt; if n == nd then raise Exit) nc with Exit -> ()); @@ -832,11 +824,11 @@ let string_index_of_constr env i cf = let vstring_i env i = let cf = SmtAtom.Atom.get_coq_term_op i in - if Structures.isRel cf then - let dbi = Structures.destRel cf in + if CoqInterface.isRel cf then + let dbi = CoqInterface.destRel cf in let s = Environ.lookup_rel dbi env - |> Structures.get_rel_dec_name + |> CoqInterface.get_rel_dec_name |> SmtMisc.string_of_name_def "?" in s, dbi @@ -977,14 +969,14 @@ let model_item env rt ro ra rf = * let outf = Format.formatter_of_out_channel out in * SExpr.print outf l; pp_print_flush outf (); * close_out out; *) - Structures.error ("Could not reconstruct model") + CoqInterface.error ("Could not reconstruct model") let model env rt ro ra rf = function | List (Atom "model" :: l) -> List.fold_left (fun acc m -> match model_item env rt ro ra rf m with Fun m -> m::acc | Sort -> acc) [] l |> List.sort (fun ((_ ,i1), _) ((_, i2), _) -> i2 - i1) - | _ -> Structures.error ("No model") + | _ -> CoqInterface.error ("No model") let model_string env rt ro ra rf s = diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli index eddf576..d0ebb61 100644 --- a/src/trace/smtCommands.mli +++ b/src/trace/smtCommands.mli @@ -11,13 +11,13 @@ val parse_certif : - Structures.id -> - Structures.id -> - Structures.id -> - Structures.id -> - Structures.id -> - Structures.id -> - Structures.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> + CoqInterface.id -> SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify * SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> @@ -29,7 +29,7 @@ val checker_debug : SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> 'a val theorem : - Structures.id -> + CoqInterface.id -> SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify * SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> @@ -56,8 +56,8 @@ val tactic : SmtAtom.Form.reify -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> - (Environ.env -> Structures.constr -> Structures.constr) -> - Structures.constr list -> - Structures.constr_expr list -> Structures.tactic + (Environ.env -> CoqInterface.constr -> CoqInterface.constr) -> + CoqInterface.constr list -> + CoqInterface.constr_expr list -> CoqInterface.tactic val model_string : Environ.env -> SmtBtype.reify_tbl -> 'a -> 'b -> 'c -> SExpr.t -> string diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index 6f26f24..2d68252 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -25,7 +25,7 @@ module type ATOM = val is_bool_type : t -> bool val is_bv_type : t -> bool - val to_smt : Format.formatter -> t -> unit + val to_smt : ?debug:bool -> Format.formatter -> t -> unit val logic : t -> logic end @@ -80,11 +80,11 @@ module type FORM = val clear : reify -> unit val get : ?declare:bool -> reify -> pform -> t - (** Give a coq term, build the corresponding formula *) - val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t + (** Given a coq term, build the corresponding formula *) + val of_coq : (CoqInterface.constr -> hatom) -> reify -> CoqInterface.constr -> t val hash_hform : (hatom -> hatom) -> reify -> t -> t - (** Flattening of [Fand] and [For], removing of [Fnot2] *) + (* Flattening of [Fand] and [For], removing of [Fnot2] *) val flatten : reify -> t -> t (** Turn n-ary [Fand] and [For] into their right-associative @@ -93,20 +93,20 @@ module type FORM = (** Producing Coq terms *) - val to_coq : t -> Structures.constr + val to_coq : t -> CoqInterface.constr val pform_tbl : reify -> pform array val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array - val interp_tbl : reify -> Structures.constr * Structures.constr + val interp_tbl : reify -> CoqInterface.constr * CoqInterface.constr val nvars : reify -> int - (** Producing a Coq term corresponding to the interpretation - of a formula *) - (** [interp_atom] map [hatom] to coq term, it is better if it produce - shared terms. *) + (* Producing a Coq term corresponding to the interpretation + of a formula *) + (* [interp_atom] map [hatom] to coq term, it is better if it produce + shared terms. *) val interp_to_coq : - (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t -> - t -> Structures.constr + (hatom -> CoqInterface.constr) -> (int, CoqInterface.constr) Hashtbl.t -> + t -> CoqInterface.constr (* Unstratified terms *) type atom_form_lit = @@ -173,12 +173,12 @@ module Make (Atom:ATOM) = to_smt_pform fmt hp.hval; Format.fprintf fmt ")" - and to_smt_pform fmt = function - | Fatom a -> Atom.to_smt fmt a + and to_smt_pform ?(debug=false) fmt = function + | Fatom a -> Atom.to_smt ~debug:debug fmt a | Fapp (op,args) -> to_smt_op fmt op args (* This is an intermediate object of proofs, it correspond to nothing in SMT *) | FbbT (a, l) -> - Format.fprintf fmt "(bbT %a [" Atom.to_smt a; + Format.fprintf fmt "(bbT %a [" (Atom.to_smt ~debug:debug) a; let fi = ref true in List.iter (fun f -> Format.fprintf fmt "%s%a" (if !fi then "" else "; ") @@ -296,34 +296,34 @@ module Make (Atom:ATOM) = let check pf = match pf with | Fatom ha -> if not (Atom.is_bool_type ha) then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) | Fapp (op, args) -> (match op with | Ftrue | Ffalse -> if Array.length args <> 0 then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) | Fnot2 _ -> if Array.length args <> 1 then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) | Fand | For -> () | Fxor | Fimp | Fiff -> if Array.length args <> 2 then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) | Fite -> if Array.length args <> 3 then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) | Fforall l -> () ) | FbbT (ha, l) -> if not (Atom.is_bv_type ha) then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) let declare reify pf = @@ -368,9 +368,9 @@ module Make (Atom:ATOM) = | CCunknown module ConstrHash = struct - type t = Structures.constr - let equal = Structures.eq_constr - let hash = Structures.hash_constr + type t = CoqInterface.constr + let equal = CoqInterface.eq_constr + let hash = CoqInterface.hash_constr end module ConstrHashtbl = Hashtbl.Make(ConstrHash) @@ -393,7 +393,7 @@ module Make (Atom:ATOM) = let get_cst c = try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in let rec mk_hform h = - let c, args = Structures.decompose_app h in + let c, args = CoqInterface.decompose_app h in match get_cst c with | CCtrue -> get reify (Fapp(Ftrue,empty_args)) | CCfalse -> get reify (Fapp(Ffalse,empty_args)) @@ -408,7 +408,7 @@ module Make (Atom:ATOM) = let l1 = mk_hform b1 in let l2 = mk_hform b2 in get reify (Fapp (Fimp, [|l1;l2|])) - | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb") + | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments for implb") | CCifb -> (* We should also be able to reify if then else *) begin match args with @@ -417,7 +417,7 @@ module Make (Atom:ATOM) = let l2 = mk_hform b2 in let l3 = mk_hform b3 in get reify (Fapp (Fite, [|l1;l2;l3|])) - | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb" + | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments for ifb" end | _ -> let a = atom_of_coq h in @@ -429,13 +429,13 @@ module Make (Atom:ATOM) = let l1 = mk_hform b1 in let l2 = mk_hform b2 in get reify (f [|l1; l2|]) - | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments" + | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments" and mk_fnot i args = match args with | [t] -> - let c,args = Structures.decompose_app t in - if Structures.eq_constr c (Lazy.force cnegb) then + let c,args = CoqInterface.decompose_app t in + if CoqInterface.eq_constr c (Lazy.force cnegb) then mk_fnot (i+1) args else let q,r = i lsr 1 , i land 1 in @@ -443,31 +443,31 @@ module Make (Atom:ATOM) = let l = if r = 0 then l else neg l in if q = 0 then l else get reify (Fapp(Fnot2 q, [|l|])) - | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb" + | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for negb" and mk_fand acc args = match args with | [t1;t2] -> let l2 = mk_hform t2 in - let c, args = Structures.decompose_app t1 in - if Structures.eq_constr c (Lazy.force candb) then + let c, args = CoqInterface.decompose_app t1 in + if CoqInterface.eq_constr c (Lazy.force candb) then mk_fand (l2::acc) args else let l1 = mk_hform t1 in get reify (Fapp(Fand, Array.of_list (l1::l2::acc))) - | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb" + | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for andb" and mk_for acc args = match args with | [t1;t2] -> let l2 = mk_hform t2 in - let c, args = Structures.decompose_app t1 in - if Structures.eq_constr c (Lazy.force corb) then + let c, args = CoqInterface.decompose_app t1 in + if CoqInterface.eq_constr c (Lazy.force corb) then mk_for (l2::acc) args else let l1 = mk_hform t1 in get reify (Fapp(For, Array.of_list (l1::l2::acc))) - | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in + | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in mk_hform c @@ -546,7 +546,7 @@ module Make (Atom:ATOM) = let args_to_coq args = let cargs = Array.make (Array.length args + 1) (mkInt 0) in Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args; - Structures.mkArray (Lazy.force cint, cargs) + CoqTerms.mkArray (Lazy.force cint, cargs) let pf_to_coq = function | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|] @@ -586,12 +586,12 @@ module Make (Atom:ATOM) = let interp_tbl reify = let (i,t) = to_array reify (Lazy.force cFtrue) pf_to_coq in - (mkInt i, Structures.mkArray (Lazy.force cform, t)) + (mkInt i, CoqTerms.mkArray (Lazy.force cform, t)) let nvars reify = reify.count - (** Producing a Coq term corresponding to the interpretation of a formula *) - (** [interp_atom] map [Atom.t] to coq term, it is better if it produce - shared terms. *) + (* Producing a Coq term corresponding to the interpretation of a formula *) + (* [interp_atom] map [Atom.t] to coq term, it is better if it produce + shared terms. *) let interp_to_coq interp_atom form_tbl f = let rec interp_form f = let l = to_lit f in diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index 9678b4c..6a5fca8 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -22,7 +22,7 @@ module type ATOM = val is_bool_type : t -> bool val is_bv_type : t -> bool - val to_smt : Format.formatter -> t -> unit + val to_smt : ?debug:bool -> Format.formatter -> t -> unit val logic : t -> logic end @@ -77,7 +77,7 @@ module type FORM = val get : ?declare:bool -> reify -> pform -> t (** Given a coq term, build the corresponding formula *) - val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t + val of_coq : (CoqInterface.constr -> hatom) -> reify -> CoqInterface.constr -> t val hash_hform : (hatom -> hatom) -> reify -> t -> t @@ -90,20 +90,20 @@ module type FORM = (** Producing Coq terms *) - val to_coq : t -> Structures.constr + val to_coq : t -> CoqInterface.constr val pform_tbl : reify -> pform array val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array - val interp_tbl : reify -> Structures.constr * Structures.constr + val interp_tbl : reify -> CoqInterface.constr * CoqInterface.constr val nvars : reify -> int - (** Producing a Coq term corresponding to the interpretation - of a formula *) - (** [interp_atom] map [hatom] to coq term, it is better if it produce - shared terms. *) + (* Producing a Coq term corresponding to the interpretation + of a formula *) + (* [interp_atom] map [hatom] to coq term, it is better if it produce + shared terms. *) val interp_to_coq : - (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t -> - t -> Structures.constr + (hatom -> CoqInterface.constr) -> (int, CoqInterface.constr) Hashtbl.t -> + t -> CoqInterface.constr (* Unstratified terms *) type atom_form_lit = diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index 227f2ff..e82001c 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -16,7 +16,7 @@ let cInt_tbl = Hashtbl.create 17 let mkInt i = try Hashtbl.find cInt_tbl i with Not_found -> - let ci = Structures.mkInt i in + let ci = CoqInterface.mkInt i in Hashtbl.add cInt_tbl i ci; ci @@ -25,15 +25,15 @@ type 'a gen_hashed = { index : int; mutable hval : 'a } (** Functions over constr *) -let mklApp f args = Structures.mkApp (Lazy.force f, args) +let mklApp f args = CoqInterface.mkApp (Lazy.force f, args) -let string_of_name_def d n = try Structures.string_of_name n with | _ -> d +let string_of_name_def d n = try CoqInterface.string_of_name n with | _ -> d let string_coq_constr t = let rec fix rf x = rf (fix rf) x in let pr = fix - Ppconstr.modular_constr_pr Pp.mt Structures.ppconstr_lsimpleconstr in - Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr t)) + Ppconstr.modular_constr_pr Pp.mt CoqInterface.ppconstr_lsimpleconstr in + Pp.string_of_ppcmds (pr (CoqInterface.constrextern_extern_constr t)) (** Logics *) @@ -46,7 +46,7 @@ type logic_item = module SL = Set.Make (struct type t = logic_item - let compare = Pervasives.compare + let compare = Stdlib.compare end) type logic = SL.t diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli index 149e377..3517018 100644 --- a/src/trace/smtMisc.mli +++ b/src/trace/smtMisc.mli @@ -10,12 +10,12 @@ (**************************************************************************) -val cInt_tbl : (int, Structures.constr) Hashtbl.t -val mkInt : int -> Structures.constr +val cInt_tbl : (int, CoqInterface.constr) Hashtbl.t +val mkInt : int -> CoqInterface.constr type 'a gen_hashed = { index : int; mutable hval : 'a; } -val mklApp : Structures.constr Lazy.t -> Structures.constr array -> Structures.constr -val string_of_name_def : string -> Structures.name -> string -val string_coq_constr : Structures.constr -> string +val mklApp : CoqInterface.constr Lazy.t -> CoqInterface.constr array -> CoqInterface.constr +val string_of_name_def : string -> CoqInterface.name -> string +val string_coq_constr : CoqInterface.constr -> string type logic_item = LUF | LLia | LBitvectors | LArrays module SL : Set.S with type elt = logic_item type logic = SL.t diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index e637b5c..650424f 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -159,7 +159,7 @@ let order_roots init_index first = r := n | _ -> failwith "root value has unexpected form" end done; - let _, lr = List.sort (fun (i1, _) (i2, _) -> Pervasives.compare i1 i2) !acc + let _, lr = List.sort (fun (i1, _) (i2, _) -> Stdlib.compare i1 i2) !acc |> List.split in let link_to c1 c2 = let curr_id = c2.id -1 in @@ -383,7 +383,7 @@ let to_coq to_lit interp (cstep, l := tl | _ -> assert false done; - mklApp cRes [|mkInt (get_pos c); Structures.mkArray (Lazy.force cint, args)|] + mklApp cRes [|mkInt (get_pos c); CoqTerms.mkArray (Lazy.force cint, args)|] | Other other -> begin match other with | Weaken (c',l') -> @@ -412,12 +412,12 @@ let to_coq to_lit interp (cstep, mklApp cEqCgrP [|out_c c; out_f f1; out_f f2; res|] | LiaMicromega (cl,d) -> let cl' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in - let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.micromega_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Structures.micromega_coq_proofTerm|]) in + let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force CoqTerms.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force CoqTerms.micromega_coq_proofTerm|]) in mklApp cLiaMicromega [|out_c c; cl'; c'|] | LiaDiseq l -> mklApp cLiaDiseq [|out_c c; out_f l|] | SplArith (orig,res,l) -> let res' = out_f res in - let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.micromega_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.micromega_coq_proofTerm|]) in + let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force CoqTerms.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force CoqTerms.micromega_coq_proofTerm|]) in mklApp cSplArith [|out_c c; out_c orig; res'; l'|] | SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|] | BBVar res -> mklApp cBBVar [|out_c c; out_f res|] @@ -461,10 +461,10 @@ let to_coq to_lit interp (cstep, | Ext (res) -> mklApp cExt [|out_c c; out_f res|] | Hole (prem_id, concl) -> let prem = List.map (fun cl -> match cl.value with Some l -> l | None -> assert false) prem_id in - let ass_name = Structures.mkId ("ass"^(string_of_int (Hashtbl.hash concl))) in + let ass_name = CoqInterface.mkId ("ass"^(string_of_int (Hashtbl.hash concl))) in let ass_ty = interp (prem, concl) in cuts := (ass_name, ass_ty)::!cuts; - let ass_var = Structures.mkVar ass_name in + let ass_var = CoqInterface.mkVar ass_name in let prem_id' = List.fold_right (fun c l -> mklApp ccons [|Lazy.force cint; out_c c; l|]) prem_id (mklApp cnil [|Lazy.force cint|]) in let prem' = List.fold_right (fun cl l -> mklApp ccons [|Lazy.force cState_C_t; out_cl cl; l|]) prem (mklApp cnil [|Lazy.force cState_C_t|]) in let concl' = out_cl concl in @@ -474,23 +474,23 @@ let to_coq to_lit interp (cstep, | Some find -> find cl | None -> assert false in let concl' = out_cl [concl] in - let app_name = Structures.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in - let app_var = Structures.mkVar app_name in - let app_ty = Term.mkArrow clemma (interp ([], [concl])) in + let app_name = CoqInterface.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in + let app_var = CoqInterface.mkVar app_name in + let app_ty = CoqInterface.mkArrow clemma (interp ([], [concl])) in cuts := (app_name, app_ty)::!cuts; mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|] end | _ -> assert false in let step = Lazy.force cstep in let def_step = - mklApp cRes [|mkInt 0; Structures.mkArray (Lazy.force cint, [|mkInt 0|]) |] in + mklApp cRes [|mkInt 0; CoqTerms.mkArray (Lazy.force cint, [|mkInt 0|]) |] in let r = ref confl in let nc = ref 0 in while not (isRoot !r.kind) do r := prev !r; incr nc done; let last_root = !r in (* Be careful, step_to_coq makes a side effect on cuts so it needs to be called first *) let res = - Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r + CoqInterface.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r in (res, last_root, !cuts) diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli index 06dc6a3..895cdc9 100644 --- a/src/trace/smtTrace.mli +++ b/src/trace/smtTrace.mli @@ -48,26 +48,26 @@ val alloc : 'a SmtCertif.clause -> int val naive_alloc : 'a SmtCertif.clause -> int val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int val to_coq : - ('a -> Structures.constr) -> - ('a list list * 'a list -> Structures.types) -> - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * - Structures.constr Lazy.t * Structures.constr Lazy.t -> + ('a -> CoqInterface.constr) -> + ('a list list * 'a list -> CoqInterface.types) -> + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t * + CoqInterface.constr Lazy.t * CoqInterface.constr Lazy.t -> 'a SmtCertif.clause -> - ('a SmtCertif.clause -> Structures.types * Structures.constr) option -> - Structures.constr * 'a SmtCertif.clause * - (Structures.id * Structures.types) list + ('a SmtCertif.clause -> CoqInterface.types * CoqInterface.constr) option -> + CoqInterface.constr * 'a SmtCertif.clause * + (CoqInterface.id * CoqInterface.types) list module MakeOpt : |