diff options
Diffstat (limited to 'src/trace/coqTerms.mli')
| -rw-r--r-- | src/trace/coqTerms.mli | 428 |
1 files changed, 214 insertions, 214 deletions
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index 282f8f6..92acbb6 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -10,258 +10,258 @@ (**************************************************************************) -val gen_constant : string list list -> string -> Structures.constr lazy_t +val gen_constant : string list list -> string -> CoqInterface.constr lazy_t (* Int63 *) -val cint : Structures.constr lazy_t -val ceq63 : Structures.constr lazy_t +val cint : CoqInterface.constr lazy_t +val ceq63 : CoqInterface.constr lazy_t (* PArray *) -val carray : Structures.constr lazy_t +val carray : CoqInterface.constr lazy_t (* nat *) -val cnat : Structures.constr lazy_t -val cO : Structures.constr lazy_t -val cS : Structures.constr lazy_t +val cnat : CoqInterface.constr lazy_t +val cO : CoqInterface.constr lazy_t +val cS : CoqInterface.constr lazy_t (* 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 : 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 (* 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 : CoqInterface.constr lazy_t +val cN0 : CoqInterface.constr lazy_t +val cNpos : CoqInterface.constr lazy_t +val cof_nat : CoqInterface.constr lazy_t (* 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 : 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 (* 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 : 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 (* 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 : CoqInterface.constr lazy_t +val cnil : CoqInterface.constr lazy_t +val ccons : CoqInterface.constr lazy_t +val clength : CoqInterface.constr lazy_t (* Option *) -val coption : Structures.constr lazy_t -val cSome : Structures.constr lazy_t -val cNone : Structures.constr lazy_t +val coption : CoqInterface.constr lazy_t +val cSome : CoqInterface.constr lazy_t +val cNone : CoqInterface.constr lazy_t (* Pairs *) -val cpair : Structures.constr lazy_t -val cprod : Structures.constr lazy_t +val cpair : CoqInterface.constr lazy_t +val cprod : CoqInterface.constr lazy_t (* Dependent pairs *) -val csigT : Structures.constr lazy_t +val csigT : CoqInterface.constr lazy_t (* 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 : 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 (* 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 : 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 (* 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 +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 : 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 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 -> - 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 + 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 (* 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 : CoqInterface.constr lazy_t +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 (* 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 |