diff options
Diffstat (limited to 'src/trace/coqTerms.mli')
| -rw-r--r-- | src/trace/coqTerms.mli | 487 |
1 files changed, 280 insertions, 207 deletions
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index 92acbb6..b5b1a0b 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -10,249 +10,322 @@ (**************************************************************************) -val gen_constant : string list list -> string -> CoqInterface.constr lazy_t +type coqTerm = CoqInterface.constr lazy_t (* Int63 *) -val cint : CoqInterface.constr lazy_t -val ceq63 : CoqInterface.constr lazy_t +val cint : coqTerm +val ceq63 : coqTerm (* PArray *) -val carray : CoqInterface.constr lazy_t +val carray : coqTerm +val cmake : coqTerm +val cset : coqTerm + +(* is_true *) +val cis_true : coqTerm (* nat *) -val cnat : CoqInterface.constr lazy_t -val cO : CoqInterface.constr lazy_t -val cS : CoqInterface.constr lazy_t +val cnat : coqTerm +val cO : coqTerm +val cS : coqTerm (* Positive *) -val cpositive : CoqInterface.constr lazy_t -val cxI : CoqInterface.constr lazy_t -val cxO : CoqInterface.constr lazy_t -val cxH : CoqInterface.constr lazy_t -val ceqbP : CoqInterface.constr lazy_t +val cpositive : coqTerm +val cxI : coqTerm +val cxO : coqTerm +val cxH : coqTerm +val ceqbP : coqTerm (* N *) -val cN : CoqInterface.constr lazy_t -val cN0 : CoqInterface.constr lazy_t -val cNpos : CoqInterface.constr lazy_t -val cof_nat : CoqInterface.constr lazy_t +val cN : coqTerm +val cN0 : coqTerm +val cNpos : coqTerm +val cof_nat : coqTerm (* Z *) -val cZ : CoqInterface.constr lazy_t -val cZ0 : CoqInterface.constr lazy_t -val cZpos : CoqInterface.constr lazy_t -val cZneg : CoqInterface.constr lazy_t -val copp : CoqInterface.constr lazy_t -val cadd : CoqInterface.constr lazy_t -val csub : CoqInterface.constr lazy_t -val cmul : CoqInterface.constr lazy_t -val cltb : CoqInterface.constr lazy_t -val cleb : CoqInterface.constr lazy_t -val cgeb : CoqInterface.constr lazy_t -val cgtb : CoqInterface.constr lazy_t -val ceqbZ : CoqInterface.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 : CoqInterface.constr lazy_t -val ctrue : CoqInterface.constr lazy_t -val cfalse : CoqInterface.constr lazy_t -val candb : CoqInterface.constr lazy_t -val corb : CoqInterface.constr lazy_t -val cxorb : CoqInterface.constr lazy_t -val cnegb : CoqInterface.constr lazy_t -val cimplb : CoqInterface.constr lazy_t -val ceqb : CoqInterface.constr lazy_t -val cifb : CoqInterface.constr lazy_t -val ciff : CoqInterface.constr lazy_t -val creflect : CoqInterface.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 : CoqInterface.constr lazy_t -val cnil : CoqInterface.constr lazy_t -val ccons : CoqInterface.constr lazy_t -val clength : CoqInterface.constr lazy_t +val clist : coqTerm +val cnil : coqTerm +val ccons : coqTerm +val clength : coqTerm (* Option *) -val coption : CoqInterface.constr lazy_t -val cSome : CoqInterface.constr lazy_t -val cNone : CoqInterface.constr lazy_t +val coption : coqTerm +val cSome : coqTerm +val cNone : coqTerm (* Pairs *) -val cpair : CoqInterface.constr lazy_t -val cprod : CoqInterface.constr lazy_t +val cpair : coqTerm +val cprod : coqTerm (* Dependent pairs *) -val csigT : CoqInterface.constr lazy_t +val csigT : coqTerm (* Logical Operators *) -val cnot : CoqInterface.constr lazy_t -val ceq : CoqInterface.constr lazy_t -val crefl_equal : CoqInterface.constr lazy_t -val cconj : CoqInterface.constr lazy_t -val cand : CoqInterface.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 : CoqInterface.constr lazy_t -val cof_bits : CoqInterface.constr lazy_t -val cbitOf : CoqInterface.constr lazy_t -val cbv_eq : CoqInterface.constr lazy_t -val cbv_not : CoqInterface.constr lazy_t -val cbv_neg : CoqInterface.constr lazy_t -val cbv_and : CoqInterface.constr lazy_t -val cbv_or : CoqInterface.constr lazy_t -val cbv_xor : CoqInterface.constr lazy_t -val cbv_add : CoqInterface.constr lazy_t -val cbv_mult : CoqInterface.constr lazy_t -val cbv_ult : CoqInterface.constr lazy_t -val cbv_slt : CoqInterface.constr lazy_t -val cbv_concat : CoqInterface.constr lazy_t -val cbv_extr : CoqInterface.constr lazy_t -val cbv_zextn : CoqInterface.constr lazy_t -val cbv_sextn : CoqInterface.constr lazy_t -val cbv_shl : CoqInterface.constr lazy_t -val cbv_shr : CoqInterface.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 : CoqInterface.constr lazy_t -val cselect : CoqInterface.constr lazy_t -val cstore : CoqInterface.constr lazy_t -val cdiff : CoqInterface.constr lazy_t -val cequalarray : CoqInterface.constr lazy_t - -(* OrderedType *) - -(* SMT_terms *) -val cState_C_t : CoqInterface.constr lazy_t -val cState_S_t : CoqInterface.constr lazy_t - -val cdistinct : CoqInterface.constr lazy_t - -val ctype : CoqInterface.constr lazy_t -val cTZ : CoqInterface.constr lazy_t -val cTbool : CoqInterface.constr lazy_t -val cTpositive : CoqInterface.constr lazy_t -val cTBV : CoqInterface.constr lazy_t -val cTFArray : CoqInterface.constr lazy_t -val cTindex : CoqInterface.constr lazy_t - -val cinterp_t : CoqInterface.constr lazy_t -val cdec_interp : CoqInterface.constr lazy_t -val cord_interp : CoqInterface.constr lazy_t -val ccomp_interp : CoqInterface.constr lazy_t -val cinh_interp : CoqInterface.constr lazy_t - -val cinterp_eqb : CoqInterface.constr lazy_t - -val ctyp_compdec : CoqInterface.constr lazy_t -val cTyp_compdec : CoqInterface.constr lazy_t -val cunit_typ_compdec : CoqInterface.constr lazy_t -val cte_carrier : CoqInterface.constr lazy_t -val cte_compdec : CoqInterface.constr lazy_t -val ceqb_of_compdec : CoqInterface.constr lazy_t -val cCompDec : CoqInterface.constr lazy_t - -val cbool_compdec : CoqInterface.constr lazy_t -val cZ_compdec : CoqInterface.constr lazy_t -val cPositive_compdec : CoqInterface.constr lazy_t -val cBV_compdec : CoqInterface.constr lazy_t -val cFArray_compdec : CoqInterface.constr lazy_t - -val ctval : CoqInterface.constr lazy_t -val cTval : CoqInterface.constr lazy_t - -val cCO_xH : CoqInterface.constr lazy_t -val cCO_Z0 : CoqInterface.constr lazy_t -val cCO_BV : CoqInterface.constr lazy_t - -val cUO_xO : CoqInterface.constr lazy_t -val cUO_xI : CoqInterface.constr lazy_t -val cUO_Zpos : CoqInterface.constr lazy_t -val cUO_Zneg : CoqInterface.constr lazy_t -val cUO_Zopp : CoqInterface.constr lazy_t -val cUO_BVbitOf : CoqInterface.constr lazy_t -val cUO_BVnot : CoqInterface.constr lazy_t -val cUO_BVneg : CoqInterface.constr lazy_t -val cUO_BVextr : CoqInterface.constr lazy_t -val cUO_BVzextn : CoqInterface.constr lazy_t -val cUO_BVsextn : CoqInterface.constr lazy_t - -val cBO_Zplus : CoqInterface.constr lazy_t -val cBO_Zminus : CoqInterface.constr lazy_t -val cBO_Zmult : CoqInterface.constr lazy_t -val cBO_Zlt : CoqInterface.constr lazy_t -val cBO_Zle : CoqInterface.constr lazy_t -val cBO_Zge : CoqInterface.constr lazy_t -val cBO_Zgt : CoqInterface.constr lazy_t -val cBO_eq : CoqInterface.constr lazy_t -val cBO_BVand : CoqInterface.constr lazy_t -val cBO_BVor : CoqInterface.constr lazy_t -val cBO_BVxor : CoqInterface.constr lazy_t -val cBO_BVadd : CoqInterface.constr lazy_t -val cBO_BVmult : CoqInterface.constr lazy_t -val cBO_BVult : CoqInterface.constr lazy_t -val cBO_BVslt : CoqInterface.constr lazy_t -val cBO_BVconcat : CoqInterface.constr lazy_t -val cBO_BVshl : CoqInterface.constr lazy_t -val cBO_BVshr : CoqInterface.constr lazy_t -val cBO_select : CoqInterface.constr lazy_t -val cBO_diffarray : CoqInterface.constr lazy_t - -val cTO_store : CoqInterface.constr lazy_t - -val cNO_distinct : CoqInterface.constr lazy_t - -val catom : CoqInterface.constr lazy_t -val cAcop : CoqInterface.constr lazy_t -val cAuop : CoqInterface.constr lazy_t -val cAbop : CoqInterface.constr lazy_t -val cAtop : CoqInterface.constr lazy_t -val cAnop : CoqInterface.constr lazy_t -val cAapp : CoqInterface.constr lazy_t - -val cform : CoqInterface.constr lazy_t -val cFatom : CoqInterface.constr lazy_t -val cFtrue : CoqInterface.constr lazy_t -val cFfalse : CoqInterface.constr lazy_t -val cFnot2 : CoqInterface.constr lazy_t -val cFand : CoqInterface.constr lazy_t -val cFor : CoqInterface.constr lazy_t -val cFxor : CoqInterface.constr lazy_t -val cFimp : CoqInterface.constr lazy_t -val cFiff : CoqInterface.constr lazy_t -val cFite : CoqInterface.constr lazy_t -val cFbbT : CoqInterface.constr lazy_t - -val cis_true : CoqInterface.constr lazy_t - -val cvalid_sat_checker : CoqInterface.constr lazy_t -val cinterp_var_sat_checker : CoqInterface.constr lazy_t - -val make_certif_ops : - string list list -> - CoqInterface.constr array option -> - 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 +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 : CoqInterface.constr lazy_t +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 : CoqInterface.constr -> bool |