aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/coqTerms.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace/coqTerms.ml')
-rw-r--r--src/trace/coqTerms.ml187
1 files changed, 187 insertions, 0 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
new file mode 100644
index 0000000..1ee6448
--- /dev/null
+++ b/src/trace/coqTerms.ml
@@ -0,0 +1,187 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2015 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - MSR-Inria Joint Lab *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+open Coqlib
+
+let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
+
+(* Int63 *)
+let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]]
+
+let cint = gen_constant int63_modules "int"
+let ceq63 = gen_constant int63_modules "eqb"
+
+(* PArray *)
+let parray_modules = [["Coq";"Array";"PArray"]]
+
+let carray = gen_constant parray_modules "array"
+
+(* 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"
+
+(* 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"
+(* Je ne comprends pas pourquoi ça fonctionne avec Zeq_bool et pas avec
+ Z.eqb *)
+(* let ceqbZ = gen_constant z_modules "eqb" *)
+let ceqbZ = gen_constant [["Coq";"ZArith";"Zbool"]] "Zeq_bool"
+
+(* 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 creflect = gen_constant bool_modules "reflect"
+
+(* Lists *)
+let clist = gen_constant init_modules "list"
+let cnil = gen_constant init_modules "nil"
+let ccons = gen_constant init_modules "cons"
+
+
+(* Option *)
+let coption = gen_constant init_modules "option"
+let cSome = gen_constant init_modules "Some"
+let cNone = gen_constant init_modules "None"
+
+(* Pairs *)
+let cpair = gen_constant init_modules "pair"
+
+(* 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"
+
+(* 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 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 cTindex = gen_constant smt_modules "Tindex"
+
+let ctyp_eqb = gen_constant smt_modules "typ_eqb"
+let cTyp_eqb = gen_constant smt_modules "Typ_eqb"
+let cte_carrier = gen_constant smt_modules "te_carrier"
+let cte_eqb = gen_constant smt_modules "te_eqb"
+let cunit_typ_eqb = gen_constant smt_modules "unit_typ_eqb"
+
+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 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 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 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 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 cis_true = gen_constant smt_modules "is_true"
+
+let make_certif_ops modules =
+ (gen_constant modules "step",
+ gen_constant modules "Res", gen_constant modules "ImmFlatten",
+ gen_constant modules "CTrue", gen_constant modules "CFalse",
+ gen_constant modules "BuildDef", gen_constant modules "BuildDef2",
+ gen_constant modules "BuildProj",
+ gen_constant modules "ImmBuildProj", gen_constant modules"ImmBuildDef",
+ gen_constant modules"ImmBuildDef2",
+ gen_constant modules "EqTr", gen_constant modules "EqCgr", gen_constant modules "EqCgrP",
+ gen_constant modules "LiaMicromega", gen_constant modules "LiaDiseq", gen_constant modules "SplArith", gen_constant modules "SplDistinctElim")
+
+
+(** Usefull construction *)
+
+let ceq_refl_true =
+ lazy (SmtMisc.mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|])
+
+let eq_refl_true () = Lazy.force ceq_refl_true
+
+let vm_cast_true t =
+ Term.mkCast(eq_refl_true (),
+ Term.VMcast,
+ SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|])
generated by cgit (git 2.34.1) at 2024-06-11 18:43:57 +0000