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