aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace
diff options
context:
space:
mode:
authorckeller <ckeller@users.noreply.github.com>2019-03-11 20:25:35 +0100
committerGitHub <noreply@github.com>2019-03-11 20:25:35 +0100
commita88e3b3b6ad01a9b85c828b9a1225732275affee (patch)
treeacc3768695698a80867b4ce941ab4cb7b4b99d7a /src/trace
parent33010bfa6345549d8b9b0c06f44150b60d0c86e5 (diff)
downloadsmtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.tar.gz
smtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.zip
V8.8 (#42)
* Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Organization structures * 8.8 ok with standard coq
Diffstat (limited to 'src/trace')
-rw-r--r--src/trace/coqTerms.ml73
-rw-r--r--src/trace/coqTerms.mli424
-rw-r--r--src/trace/satAtom.ml2
-rw-r--r--src/trace/satAtom.mli10
-rw-r--r--src/trace/smtAtom.ml32
-rw-r--r--src/trace/smtAtom.mli26
-rw-r--r--src/trace/smtBtype.ml38
-rw-r--r--src/trace/smtBtype.mli32
-rw-r--r--src/trace/smtCommands.ml340
-rw-r--r--src/trace/smtCommands.mli20
-rw-r--r--src/trace/smtForm.ml30
-rw-r--r--src/trace/smtForm.mli46
-rw-r--r--src/trace/smtMisc.ml16
-rw-r--r--src/trace/smtMisc.mli13
-rw-r--r--src/trace/smtTrace.ml8
-rw-r--r--src/trace/smtTrace.mli38
16 files changed, 560 insertions, 588 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 895d217..ad5ec1d 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -11,6 +11,7 @@
open Coqlib
+open SmtMisc
let gen_constant = Structures.gen_constant
@@ -274,7 +275,7 @@ let cinterp_var_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "i
let make_certif_ops modules args =
let gen_constant c =
match args with
- | Some args -> lazy (SmtMisc.mklApp (gen_constant modules c) args)
+ | Some args -> lazy (mklApp (gen_constant modules c) args)
| None -> gen_constant modules c in
(gen_constant "step",
gen_constant "Res", gen_constant "Weaken", gen_constant "ImmFlatten",
@@ -300,14 +301,14 @@ let make_certif_ops modules args =
(** Useful constructions *)
let ceq_refl_true =
- lazy (SmtMisc.mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|])
+ lazy (mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|])
let eq_refl_true () = Lazy.force ceq_refl_true
let vm_cast_true_no_check t =
- Term.mkCast(eq_refl_true (),
- Term.VMcast,
- SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|])
+ Structures.mkCast(eq_refl_true (),
+ Structures.vmcast,
+ mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|])
(* This version checks convertibility right away instead of delaying it at
Qed. This allows to report issues to the user as soon as he/she runs one of
@@ -315,9 +316,9 @@ let vm_cast_true_no_check t =
let vm_cast_true env t =
try
Structures.vm_conv Reduction.CUMUL env
- (SmtMisc.mklApp ceq
+ (mklApp ceq
[|Lazy.force cbool; Lazy.force ctrue; Lazy.force ctrue|])
- (SmtMisc.mklApp ceq [|Lazy.force cbool; t; 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.")
@@ -326,19 +327,19 @@ let vm_cast_true env t =
(* Compute a nat *)
let rec mkNat = function
| 0 -> Lazy.force cO
- | i -> SmtMisc.mklApp cS [|mkNat (i-1)|]
+ | i -> mklApp cS [|mkNat (i-1)|]
(* Compute a positive *)
let rec mkPositive = function
| 1 -> Lazy.force cxH
| i ->
let c = if (i mod 2) = 0 then cxO else cxI in
- SmtMisc.mklApp c [|mkPositive (i / 2)|]
+ mklApp c [|mkPositive (i / 2)|]
(* Compute a N *)
let mkN = function
| 0 -> Lazy.force cN0
- | i -> SmtMisc.mklApp cNpos [|mkPositive i|]
+ | i -> mklApp cNpos [|mkPositive i|]
(* Compute a Boolean *)
let mkBool = function
@@ -347,47 +348,47 @@ let mkBool = function
(* Compute a Boolean list *)
let rec mk_bv_list = function
- | [] -> SmtMisc.mklApp cnil [|Lazy.force cbool|]
+ | [] -> mklApp cnil [|Lazy.force cbool|]
| b :: bv ->
- SmtMisc.mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|]
+ mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|]
(* Reification *)
let mk_bool b =
- let c, args = Term.decompose_app b in
- if Term.eq_constr c (Lazy.force ctrue) then true
- else if Term.eq_constr c (Lazy.force cfalse) then false
+ 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
else assert false
let rec mk_bool_list bs =
- let c, args = Term.decompose_app bs in
- if Term.eq_constr c (Lazy.force cnil) then []
- else if Term.eq_constr c (Lazy.force ccons) then
+ 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
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 = Term.decompose_app n in
- if Term.eq_constr c (Lazy.force cO) then
+ let c, args = Structures.decompose_app n in
+ if Structures.eq_constr c (Lazy.force cO) then
0
- else if Term.eq_constr c (Lazy.force cS) then
+ else if Structures.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 = Term.decompose_app n in
- if Term.eq_constr c (Lazy.force cxH) then
+ let c, args = Structures.decompose_app n in
+ if Structures.eq_constr c (Lazy.force cxH) then
1
- else if Term.eq_constr c (Lazy.force cxO) then
+ else if Structures.eq_constr c (Lazy.force cxO) then
match args with
| [n] -> 2 * (mk_positive n)
| _ -> assert false
- else if Term.eq_constr c (Lazy.force cxI) then
+ else if Structures.eq_constr c (Lazy.force cxI) then
match args with
| [n] -> 2 * (mk_positive n) + 1
| _ -> assert false
@@ -395,10 +396,10 @@ let rec mk_positive n =
let mk_N n =
- let c, args = Term.decompose_app n in
- if Term.eq_constr c (Lazy.force cN0) then
+ let c, args = Structures.decompose_app n in
+ if Structures.eq_constr c (Lazy.force cN0) then
0
- else if Term.eq_constr c (Lazy.force cNpos) then
+ else if Structures.eq_constr c (Lazy.force cNpos) then
match args with
| [n] -> mk_positive n
| _ -> assert false
@@ -406,13 +407,13 @@ let mk_N n =
let mk_Z n =
- let c, args = Term.decompose_app n in
- if Term.eq_constr c (Lazy.force cZ0) then 0
- else if Term.eq_constr c (Lazy.force cZpos) then
+ 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
match args with
| [n] -> mk_positive n
| _ -> assert false
- else if Term.eq_constr c (Lazy.force cZneg) then
+ else if Structures.eq_constr c (Lazy.force cZneg) then
match args with
| [n] -> - mk_positive n
| _ -> assert false
@@ -421,12 +422,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 = Term.decompose_app n in
- if Term.eq_constr c (Lazy.force cof_nat) then
+ let c, args = Structures.decompose_app n in
+ if Structures.eq_constr c (Lazy.force cof_nat) then
match args with
| [nl] ->
- let c, args = Term.decompose_app nl in
- if Term.eq_constr c (Lazy.force clength) then
+ let c, args = Structures.decompose_app nl in
+ if Structures.eq_constr c (Lazy.force clength) then
match args with
| [_; l] -> List.length (mk_bool_list l)
| _ -> assert false
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
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
index 549462c..c91cee1 100644
--- a/src/trace/satAtom.ml
+++ b/src/trace/satAtom.ml
@@ -27,7 +27,7 @@ module Atom =
type reify_tbl =
{ mutable count : int;
- tbl : (Term.constr, int) Hashtbl.t
+ tbl : (Structures.constr, int) Hashtbl.t
}
let create () =
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index 4ecfae3..49bc590 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -23,13 +23,13 @@ module Atom : sig
type reify_tbl = {
mutable count : int;
- tbl : (Term.constr, t) Hashtbl.t;
+ tbl : (Structures.constr, t) Hashtbl.t;
}
val create : unit -> reify_tbl
- val declare : reify_tbl -> Term.constr -> t
- val get : reify_tbl -> Term.constr -> t
- val atom_tbl : reify_tbl -> Term.constr array
- val interp_tbl : reify_tbl -> Term.constr
+ 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
end
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 330884b..16d9bdb 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -68,7 +68,7 @@ type nop =
type op_def = {
tparams : btype array;
tres : btype;
- op_val : Term.constr }
+ op_val : Structures.constr }
type index = Index of int
| Rel_name of string
@@ -80,14 +80,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 = Term.mkProp})
+ (i, {tparams = dom; tres = codom; op_val = Structures.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 = Term.mkRel i})
+ (Index i, {tparams = [||]; tres = ty; op_val = Structures.mkRel i})
module Op =
struct
@@ -339,7 +339,7 @@ module Op =
(* reify table *)
type reify_tbl =
{ mutable count : int;
- tbl : (Term.constr, indexed_op) Hashtbl.t
+ tbl : (Structures.constr, indexed_op) Hashtbl.t
}
let create () =
@@ -692,7 +692,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 (Printer.pr_constr t))
+ Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Structures.pr_constr t))
and to_smt_bop op h1 h2 =
let s = match op with
@@ -1019,8 +1019,8 @@ module Atom =
else CCunknown_deps (gobble_of_coq_cst cc)
with Not_found -> CCunknown
in
- let rec mk_hatom (h : Term.constr) =
- let c, args = Term.decompose_app h in
+ let rec mk_hatom (h : Structures.constr) =
+ let c, args = Structures.decompose_app h in
match get_cst c with
| CCxH -> mk_cop CCxH args
| CCZ0 -> mk_cop CCZ0 args
@@ -1248,10 +1248,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 Term.isRel c then
- let i = Term.destRel c 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 (string_of_name n)
+ Some (Structures.string_of_name n)
else
None
in
@@ -1267,7 +1267,7 @@ module Atom =
[gobble] *)
and mk_unknown_deps c args ty gobble =
let deps, args = split_list_at gobble args in
- let c = Term.mkApp (c, Array.of_list deps) in
+ let c = Structures.mkApp (c, Array.of_list deps) in
mk_unknown c args ty
in
@@ -1320,12 +1320,12 @@ module Atom =
let pc =
match atom a with
| Acop c -> Op.interp_cop c
- | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|])
+ | Auop (op,h) -> Structures.mkApp (Op.interp_uop op, [|interp_atom h|])
| Abop (op,h1,h2) ->
- Term.mkApp (Op.interp_bop t_i op,
+ Structures.mkApp (Op.interp_bop t_i op,
[|interp_atom h1; interp_atom h2|])
| Atop (op,h1,h2,h3) ->
- Term.mkApp (Op.interp_top t_i op,
+ Structures.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
@@ -1333,9 +1333,9 @@ module Atom =
let cargs = Array.fold_right (fun h l ->
mklApp ccons [|typ; interp_atom h; l|])
ha (mklApp cnil [|typ|]) in
- Term.mkApp (cop,[|cargs|])
+ Structures.mkApp (cop,[|cargs|])
| Aapp (op,t) ->
- Term.mkApp ((snd op).op_val, Array.map interp_atom t) in
+ Structures.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 a542ad6..a6a1761 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 -> Term.constr -> btype array ->
+ val declare : reify_tbl -> Structures.constr -> btype array ->
btype -> string option -> indexed_op
- val of_coq : reify_tbl -> Term.constr -> indexed_op
+ val of_coq : reify_tbl -> Structures.constr -> indexed_op
- val interp_tbl : Term.constr ->
- (btype array -> btype -> Term.constr -> Term.constr) ->
- reify_tbl -> Term.constr
+ val interp_tbl : Structures.constr ->
+ (btype array -> btype -> Structures.constr -> Structures.constr) ->
+ reify_tbl -> Structures.constr
val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list
@@ -143,18 +143,18 @@ module Atom :
(** Given a coq term, build the corresponding atom *)
val of_coq : ?hash:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
- reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Term.constr -> t
+ reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t
- val get_coq_term_op : int -> Term.constr
+ val get_coq_term_op : int -> Structures.constr
- val to_coq : t -> Term.constr
+ val to_coq : t -> Structures.constr
val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array
- val interp_tbl : reify_tbl -> Term.constr
+ val interp_tbl : reify_tbl -> Structures.constr
- val interp_to_coq : Term.constr -> (int, Term.constr) Hashtbl.t ->
- t -> Term.constr
+ val interp_to_coq : Structures.constr -> (int, Structures.constr) Hashtbl.t ->
+ t -> Structures.constr
val logic : t -> SmtMisc.logic
@@ -202,5 +202,5 @@ module Trace : sig
end
-val make_t_i : SmtBtype.reify_tbl -> Term.constr
-val make_t_func : Op.reify_tbl -> Term.constr -> Term.constr
+val make_t_i : SmtBtype.reify_tbl -> Structures.constr
+val make_t_func : Op.reify_tbl -> Structures.constr -> Structures.constr
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 119c046..948acaa 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -15,9 +15,9 @@ open CoqTerms
(** Syntaxified version of Coq type *)
-type indexed_type = Term.constr gen_hashed
+type indexed_type = Structures.constr gen_hashed
-let dummy_indexed_type i = {index = i; hval = Term.mkProp}
+let dummy_indexed_type i = {index = i; hval = Structures.mkProp}
let indexed_type_index i = i.index
let indexed_type_hval i = i.hval
@@ -76,8 +76,8 @@ let rec logic = function
(* reify table *)
type reify_tbl =
{ mutable count : int;
- tbl : (Term.constr, btype) Hashtbl.t;
- mutable cuts : (Structures.names_id * Term.types) list;
+ tbl : (Structures.constr, btype) Hashtbl.t;
+ mutable cuts : (Structures.id * Structures.types) list;
unsup_tbl : (btype, btype) Hashtbl.t;
}
@@ -175,8 +175,8 @@ let rec compdec_btype reify = function
[|interp_to_coq reify ti; interp_to_coq reify te;
compdec_btype reify ti; compdec_btype reify te|]
| Tindex i ->
- let c, args = Term.decompose_app i.hval in
- if Term.eq_constr c (Lazy.force cTyp_compdec) then
+ let c, args = Structures.decompose_app i.hval in
+ if Structures.eq_constr c (Lazy.force cTyp_compdec) then
match args with
| [_; tic] -> tic
| _ -> assert false
@@ -195,22 +195,22 @@ let declare_and_compdec reify t ty =
let rec of_coq reify known_logic t =
try
- let c, args = Term.decompose_app t in
- if Term.eq_constr c (Lazy.force cbool) ||
- Term.eq_constr c (Lazy.force cTbool) then Tbool
- else if Term.eq_constr c (Lazy.force cZ) ||
- Term.eq_constr c (Lazy.force cTZ) then
+ 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
check_known TZ known_logic
- else if Term.eq_constr c (Lazy.force cpositive) ||
- Term.eq_constr c (Lazy.force cTpositive) then
+ else if Structures.eq_constr c (Lazy.force cpositive) ||
+ Structures.eq_constr c (Lazy.force cTpositive) then
check_known Tpositive known_logic
- else if Term.eq_constr c (Lazy.force cbitvector) ||
- Term.eq_constr c (Lazy.force cTBV) then
+ else if Structures.eq_constr c (Lazy.force cbitvector) ||
+ Structures.eq_constr c (Lazy.force cTBV) then
match args with
| [s] -> check_known (TBV (mk_bvsize s)) known_logic
| _ -> assert false
- else if Term.eq_constr c (Lazy.force cfarray) ||
- Term.eq_constr c (Lazy.force cTFArray) then
+ else if Structures.eq_constr c (Lazy.force cfarray) ||
+ Structures.eq_constr c (Lazy.force cTFArray) then
match args with
| ti :: te :: _ ->
let ty = TFArray (of_coq reify known_logic ti,
@@ -221,8 +221,8 @@ let rec of_coq reify known_logic t =
try Hashtbl.find reify.tbl t
with Not_found ->
let n = string_of_int (List.length reify.cuts) in
- let compdec_name = Names.id_of_string ("CompDec"^n) in
- let compdec_var = Term.mkVar compdec_name in
+ let compdec_name = Structures.mkId ("CompDec"^n) in
+ let compdec_var = Structures.mkVar compdec_name in
let compdec_type = mklApp cCompDec [| t |]in
reify.cuts <- (compdec_name, compdec_type) :: reify.cuts;
let ce = mklApp cTyp_compdec [|t; compdec_var|] in
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli
index 4f8d4ad..5d45ca4 100644
--- a/src/trace/smtBtype.mli
+++ b/src/trace/smtBtype.mli
@@ -13,11 +13,11 @@
open SmtMisc
-type indexed_type = Term.constr gen_hashed
+type indexed_type = Structures.constr gen_hashed
val dummy_indexed_type: int -> indexed_type
val indexed_type_index : indexed_type -> int
-val indexed_type_hval : indexed_type -> Term.constr
+val indexed_type_hval : indexed_type -> Structures.constr
type btype =
| TZ
@@ -27,11 +27,11 @@ type btype =
| TFArray of btype * btype
| Tindex of indexed_type
-val indexed_type_of_int : int -> Term.constr SmtMisc.gen_hashed
+val indexed_type_of_int : int -> Structures.constr SmtMisc.gen_hashed
val equal : btype -> btype -> bool
-val to_coq : btype -> Term.constr
+val to_coq : btype -> Structures.constr
val to_smt : Format.formatter -> btype -> unit
@@ -39,26 +39,26 @@ type reify_tbl
val create : unit -> reify_tbl
-val declare : reify_tbl -> Term.constr -> Term.constr -> btype
+val declare : reify_tbl -> Structures.constr -> Structures.constr -> btype
-val of_coq : reify_tbl -> logic -> Term.constr -> btype
+val of_coq : reify_tbl -> logic -> Structures.constr -> btype
-val get_coq_type_op : int -> Term.constr
+val get_coq_type_op : int -> Structures.constr
-val interp_tbl : reify_tbl -> Term.constr
+val interp_tbl : reify_tbl -> Structures.constr
val to_list : reify_tbl -> (int * indexed_type) list
-val make_t_i : reify_tbl -> Term.constr
+val make_t_i : reify_tbl -> Structures.constr
-val dec_interp : Term.constr -> btype -> Term.constr
-val ord_interp : Term.constr -> btype -> Term.constr
-val comp_interp : Term.constr -> btype -> Term.constr
-val inh_interp : Term.constr -> btype -> Term.constr
-val interp : Term.constr -> btype -> Term.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 interp_to_coq : reify_tbl -> btype -> Term.constr
+val interp_to_coq : reify_tbl -> btype -> Structures.constr
-val get_cuts : reify_tbl -> (Structures.names_id * Term.types) list
+val get_cuts : reify_tbl -> (Structures.id * Structures.types) list
val logic : btype -> logic
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 1a990f1..78c07b9 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -10,10 +10,6 @@
(**************************************************************************)
-open Entries
-open Declare
-open Decl_kinds
-
open SmtMisc
open CoqTerms
open SmtForm
@@ -132,19 +128,19 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
let t_i' = make_t_i rt in
let ce5 = Structures.mkUConst t_i' in
- let ct_i = Term.mkConst (declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition)) in
+ let ct_i = Structures.mkConst (Structures.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 = Term.mkConst (declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition)) in
+ let ct_func = Structures.mkConst (Structures.declare_constant t_func ce6) in
let t_atom' = Atom.interp_tbl ra in
let ce1 = Structures.mkUConst t_atom' in
- let ct_atom = Term.mkConst (declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition)) in
+ let ct_atom = Structures.mkConst (Structures.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 = Term.mkConst (declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition)) in
+ let ct_form = Structures.mkConst (Structures.declare_constant t_form ce2) in
(* EMPTY LEMMA LIST *)
let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
@@ -167,14 +163,14 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
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 _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in
+ let _ = Structures.declare_constant root ce3 in
let ce3' = Structures.mkUConst used_roots in
- let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in
+ let _ = Structures.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 _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in
+ let _ = Structures.declare_constant trace ce4 in
()
@@ -188,15 +184,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 = mkName "t_i" in
- let ntfunc = mkName "t_func" in
- let ntatom = mkName "t_atom" in
- let ntform = mkName "t_form" in
- let nc = mkName "c" in
- let nused_roots = mkName "used_roots" in
- let nd = mkName "d" in
+ 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 v = Term.mkRel in
+ let v = Structures.mkRel in
let t_i = make_t_i rt in
let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -230,50 +226,50 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in
let theorem_proof_cast =
- Term.mkCast (
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
- Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
- Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
- Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
- Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
- Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+ 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|],
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*)|])|]))))))),
- Term.VMcast,
+ Structures.vmcast,
theorem_concl)
in
let theorem_proof_nocast =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
- Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
- Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
- Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
- Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
- Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+ 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|],
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 _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
+ let _ = Structures.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 = mkName "t_i" in
- let ntfunc = mkName "t_func" in
- let ntatom = mkName "t_atom" in
- let ntform = mkName "t_form" in
- let nc = mkName "c" in
- let nused_roots = mkName "used_roots" in
- let nd = mkName "d" in
+ 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 v = Term.mkRel in
+ let v = Structures.mkRel in
let t_i = make_t_i rt in
let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -306,18 +302,18 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
Structures.mkArray (Lazy.force cint, res) in
let tm =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
- Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
- Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
- Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
- Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
- Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+ 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|],
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
Format.eprintf " = %s\n : bool@."
- (if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then
+ (if Structures.eq_constr res (Lazy.force CoqTerms.ctrue) then
"true" else "false")
let count_used confl =
@@ -333,15 +329,15 @@ let count_used confl =
let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
- let nti = mkName "t_i" in
- let ntfunc = mkName "t_func" in
- let ntatom = mkName "t_atom" in
- let ntform = mkName "t_form" in
- let nc = mkName "c" in
- let nused_roots = mkName "used_roots" in
- let nd = mkName "d" in
+ 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 v = Term.mkRel in
+ let v = Structures.mkRel in
let t_i = make_t_i rt in
let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -376,16 +372,16 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
Structures.mkArray (Lazy.force cint, res) in
let tm =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
- Term.mkLetIn (ntfunc, t_func,
+ Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+ Structures.mkLetIn (ntfunc, t_func,
mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
- Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
- Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*);
+ 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*)|],
- Term.mkLetIn (nused_roots, used_rootsCstr,
+ Structures.mkLetIn (nused_roots, used_rootsCstr,
mklApp coption [|mklApp carray [|Lazy.force cint|]|],
- Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+ Structures.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
@@ -394,54 +390,54 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
[|mklApp cprod
[|Lazy.force cnat; Lazy.force cname_step|]|]) in
- match Term.decompose_app res with
- | c, _ when Term.eq_constr c (Lazy.force cNone) ->
+ 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 \
that fail to be checked by SMTCoq.")
- | c, [_; n] when Term.eq_constr c (Lazy.force cSome) ->
- (match Term.decompose_app n with
- | c, [_; _; cnb; cn] when Term.eq_constr c (Lazy.force cpair) ->
- let n = fst (Term.decompose_app cn) in
+ | 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
let name =
- if Term.eq_constr n (Lazy.force cName_Res ) then "Res"
- else if Term.eq_constr n (Lazy.force cName_Weaken) then "Weaken"
- else if Term.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten"
- else if Term.eq_constr n (Lazy.force cName_CTrue) then "CTrue"
- else if Term.eq_constr n (Lazy.force cName_CFalse ) then "CFalse"
- else if Term.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef"
- else if Term.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2"
- else if Term.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj"
- else if Term.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef"
- else if Term.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2"
- else if Term.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj"
- else if Term.eq_constr n (Lazy.force cName_EqTr ) then "EqTr"
- else if Term.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr"
- else if Term.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP"
- else if Term.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega"
- else if Term.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq"
- else if Term.eq_constr n (Lazy.force cName_SplArith) then "SplArith"
- else if Term.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim"
- else if Term.eq_constr n (Lazy.force cName_BBVar) then "BBVar"
- else if Term.eq_constr n (Lazy.force cName_BBConst) then "BBConst"
- else if Term.eq_constr n (Lazy.force cName_BBOp) then "BBOp"
- else if Term.eq_constr n (Lazy.force cName_BBNot) then "BBNot"
- else if Term.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg"
- else if Term.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd"
- else if Term.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat"
- else if Term.eq_constr n (Lazy.force cName_BBMul) then "BBMul"
- else if Term.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt"
- else if Term.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt"
- else if Term.eq_constr n (Lazy.force cName_BBEq) then "BBEq"
- else if Term.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq"
- else if Term.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract"
- else if Term.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend"
- else if Term.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend"
- else if Term.eq_constr n (Lazy.force cName_BBShl) then "BBShl"
- else if Term.eq_constr n (Lazy.force cName_BBShr) then "BBShr"
- else if Term.eq_constr n (Lazy.force cName_RowEq) then "RowEq"
- else if Term.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq"
- else if Term.eq_constr n (Lazy.force cName_Ext) then "Ext"
- else if Term.eq_constr n (Lazy.force cName_Hole) then "Hole"
+ 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"
else string_coq_constr n
in
let nb = mk_nat cnb + List.length roots + (confl.id + 1 - count_used confl) in
@@ -454,9 +450,9 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
(* let rec of_coq_list cl =
- * match Term.decompose_app cl with
- * | c, _ when Term.eq_constr c (Lazy.force cnil) -> []
- * | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) ->
+ * 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) ->
* x :: of_coq_list cr
* | _ -> assert false *)
@@ -466,26 +462,22 @@ let checker_debug (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 = Term.mkConst (declare_constant t_i
- * (DefinitionEntry ce5, IsDefinition Definition)) in
+ * let ct_i = Structures.mkConst (Structures.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 =
- * Term.mkConst (declare_constant t_func
- * (DefinitionEntry ce6, IsDefinition Definition)) in
+ * Structures.mkConst (Structures.declare_constant t_func ce6) in
*
* let t_atom' = Atom.interp_tbl ra in
* let ce1 = Structures.mkUConst t_atom' in
* let ct_atom =
- * Term.mkConst (declare_constant t_atom
- * (DefinitionEntry ce1, IsDefinition Definition)) in
+ * Structures.mkConst (Structures.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 =
- * Term.mkConst (declare_constant t_form
- * (DefinitionEntry ce2, IsDefinition Definition)) in
+ * Structures.mkConst (Structures.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)
@@ -509,18 +501,15 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
* mklApp cSome [|mklApp carray [|Lazy.force cint|];
* Structures.mkArray (Lazy.force cint, res)|] in
* let ce3 = Structures.mkUConst croots in
- * let _ = declare_constant root
- * (DefinitionEntry ce3, IsDefinition Definition) in
+ * let _ = Structures.declare_constant root ce3 in
* let ce3' = Structures.mkUConst cused_roots in
- * let _ = declare_constant used_root
- * (DefinitionEntry ce3', IsDefinition Definition) in
+ * let _ = Structures.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 _ = declare_constant trace
- * (DefinitionEntry ce4, IsDefinition Definition) in
+ * let _ = Structures.declare_constant trace ce4 in
*
* let setup =
* mklApp csetup_checker_step_debug
@@ -532,8 +521,8 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
* mklApp clist [|mklApp cstep
* [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in
*
- * let s, steps = match Term.decompose_app setup with
- * | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) ->
+ * let s, steps = match Structures.decompose_app setup with
+ * | c, [_; _; s; csteps] when Structures.eq_constr c (Lazy.force cpair) ->
* s, of_coq_list csteps
* | _ -> assert false
* in
@@ -550,12 +539,12 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
* Structures.cbv_vm (Global.env ()) tm
* (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
*
- * match Term.decompose_app res with
- * | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) ->
+ * match Structures.decompose_app res with
+ * | c, [_; _; s; cbad] when Structures.eq_constr c (Lazy.force cpair) ->
* if not (mk_bool cbad) then s
* else Structures.error ("Step number " ^ string_of_int !cpt ^
* " (" ^ string_coq_constr
- * (fst (Term.decompose_app step)) ^ ")" ^
+ * (fst (Structures.decompose_app step)) ^ ")" ^
* " of the certificate likely failed." )
* | _ -> assert false
* in
@@ -570,13 +559,13 @@ 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 = mkName "t_i" in
- let ntfunc = mkName "t_func" in
- let ntatom = mkName "t_atom" in
- let ntform = mkName "t_form" in
- let nc = mkName "c" in
+ 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 v = Term.mkRel in
+ let v = Structures.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
@@ -594,11 +583,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 =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
- Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
- Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
- Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, mklApp ccertif
+ 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*)|],
t))))) in
@@ -625,13 +614,13 @@ 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 = mkName "t_i" in
- let ntfunc = mkName "t_func" in
- let ntatom = mkName "t_atom" in
- let ntform = mkName "t_form" in
- let nc = mkName "c" in
+ 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 v = Term.mkRel in
+ let v = Structures.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
@@ -644,11 +633,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 =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
- Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
- Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
- Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, mklApp ccertif
+ 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*)|],
t))))) in
@@ -676,10 +665,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 = Term.decompose_app concl in
+ let f, args = Structures.decompose_app concl in
match args with
- | [ty;a;b] when (Term.eq_constr f (Lazy.force ceq)) && (Term.eq_constr ty (Lazy.force cbool)) -> a, b
- | [a] when (Term.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue
+ | [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
| _ -> failwith ("Verit.tactic: can only deal with equality over bool")
@@ -699,18 +688,18 @@ let of_coq_lemma rt ro ra' rf' env sigma solver_logic clemma =
let env_lemma = List.fold_right Environ.push_rel rel_context env in
let forall_args =
let fmap r = let n, t = Structures.destruct_rel_decl r in
- string_of_name n, SmtBtype.of_coq rt solver_logic t in
+ Structures.string_of_name n, SmtBtype.of_coq rt solver_logic t in
List.map fmap rel_context in
- let f, args = Term.decompose_app qf_lemma in
+ let f, args = Structures.decompose_app qf_lemma in
let core_f =
- if Term.eq_constr f (Lazy.force cis_true) then
+ if Structures.eq_constr f (Lazy.force cis_true) then
match args with
| [a] -> a
| _ -> raise Axiom_form_unsupported
- else if Term.eq_constr f (Lazy.force ceq) then
+ else if Structures.eq_constr f (Lazy.force ceq) then
match args with
- | [ty; arg1; arg2] when Term.eq_constr ty (Lazy.force cbool) &&
- Term.eq_constr arg2 (Lazy.force ctrue) ->
+ | [ty; arg1; arg2] when Structures.eq_constr ty (Lazy.force cbool) &&
+ Structures.eq_constr arg2 (Lazy.force ctrue) ->
arg1
| _ -> raise Axiom_form_unsupported
else raise Axiom_form_unsupported in
@@ -730,7 +719,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
let lsmt = List.map (of_coq_lemma rt ro ra' rf' env sigma solver_logic) lcl in
let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in
- let lem_tbl : (int, Term.constr * Term.constr) Hashtbl.t =
+ let lem_tbl : (int, Structures.constr * Structures.constr) Hashtbl.t =
Hashtbl.create 100 in
let new_ref ((l, pl), ls) =
Hashtbl.add lem_tbl (Form.index ls) (l, pl) in
@@ -752,10 +741,10 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
| _ -> failwith "unexpected form of root" in
let (body_cast, body_nocast, cuts) =
- if ((Term.eq_constr b (Lazy.force ctrue)) ||
- (Term.eq_constr b (Lazy.force cfalse))) then
+ if ((Structures.eq_constr b (Lazy.force ctrue)) ||
+ (Structures.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 nl = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
+ let nl = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
let lsmt = Form.flatten rf nl :: lsmt in
let max_id_confl = make_proof call_solver env rt ro ra' rf' nl lsmt in
@@ -776,7 +765,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
List.fold_right (fun (eqn, eqt) tac ->
Structures.tclTHENLAST
- (Structures.assert_before (Names.Name eqn) eqt)
+ (Structures.assert_before (Structures.name_of_id eqn) eqt)
tac
) cuts
(Structures.tclTHEN
@@ -804,7 +793,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 (Names.id_of_string s) env in
+ let nd = Environ.lookup_named (Structures.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 -> ());
@@ -814,14 +803,13 @@ let string_index_of_constr env i cf =
let vstring_i env i =
let cf = SmtAtom.Atom.get_coq_term_op i in
- if Term.isRel cf then
- let dbi = Term.destRel cf in
+ if Structures.isRel cf then
+ let dbi = Structures.destRel cf in
let s =
Environ.lookup_rel dbi env
|> Structures.get_rel_dec_name
- |> function
- | Names.Name id -> Names.string_of_id id
- | Names.Anonymous -> "?" in
+ |> SmtMisc.string_of_name_def "?"
+ in
s, dbi
else
string_index_of_constr env i cf
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
index d7b6ae6..9a1b681 100644
--- a/src/trace/smtCommands.mli
+++ b/src/trace/smtCommands.mli
@@ -11,13 +11,13 @@
val parse_certif :
- Structures.names_id ->
- Structures.names_id ->
- Structures.names_id ->
- Structures.names_id ->
- Structures.names_id ->
- Structures.names_id ->
- Structures.names_id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.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.names_id ->
+ Structures.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 -> Term.constr -> Term.constr) ->
- Term.constr list ->
+ (Environ.env -> Structures.constr -> Structures.constr) ->
+ Structures.constr list ->
Structures.constr_expr list -> Structures.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 ad6a5a4..20b99ac 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -82,7 +82,7 @@ module type FORM =
val get : ?declare:bool -> reify -> pform -> t
(** Give a coq term, build the corresponding formula *)
- val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+ val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t
val hash_hform : (hatom -> hatom) -> reify -> t -> t
(** Flattening of [Fand] and [For], removing of [Fnot2] *)
@@ -94,20 +94,20 @@ module type FORM =
(** Producing Coq terms *)
- val to_coq : t -> Term.constr
+ val to_coq : t -> Structures.constr
val pform_tbl : reify -> pform array
val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
- val interp_tbl : reify -> Term.constr * Term.constr
+ val interp_tbl : reify -> Structures.constr * Structures.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. *)
val interp_to_coq :
- (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t ->
- t -> Term.constr
+ (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
+ t -> Structures.constr
end
module Make (Atom:ATOM) =
@@ -361,9 +361,9 @@ module Make (Atom:ATOM) =
| CCunknown
module ConstrHash = struct
- type t = Term.constr
- let equal = Term.eq_constr
- let hash = Term.hash_constr
+ type t = Structures.constr
+ let equal = Structures.eq_constr
+ let hash = Structures.hash_constr
end
module ConstrHashtbl = Hashtbl.Make(ConstrHash)
@@ -386,7 +386,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 = Term.decompose_app h in
+ let c, args = Structures.decompose_app h in
match get_cst c with
| CCtrue -> get reify (Fapp(Ftrue,empty_args))
| CCfalse -> get reify (Fapp(Ffalse,empty_args))
@@ -427,8 +427,8 @@ module Make (Atom:ATOM) =
and mk_fnot i args =
match args with
| [t] ->
- let c,args = Term.decompose_app t in
- if Term.eq_constr c (Lazy.force cnegb) then
+ let c,args = Structures.decompose_app t in
+ if Structures.eq_constr c (Lazy.force cnegb) then
mk_fnot (i+1) args
else
let q,r = i lsr 1 , i land 1 in
@@ -442,8 +442,8 @@ module Make (Atom:ATOM) =
match args with
| [t1;t2] ->
let l2 = mk_hform t2 in
- let c, args = Term.decompose_app t1 in
- if Term.eq_constr c (Lazy.force candb) then
+ let c, args = Structures.decompose_app t1 in
+ if Structures.eq_constr c (Lazy.force candb) then
mk_fand (l2::acc) args
else
let l1 = mk_hform t1 in
@@ -454,8 +454,8 @@ module Make (Atom:ATOM) =
match args with
| [t1;t2] ->
let l2 = mk_hform t2 in
- let c, args = Term.decompose_app t1 in
- if Term.eq_constr c (Lazy.force corb) then
+ let c, args = Structures.decompose_app t1 in
+ if Structures.eq_constr c (Lazy.force corb) then
mk_for (l2::acc) args
else
let l1 = mk_hform t1 in
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index c26e279..ba8c066 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -12,10 +12,10 @@
open SmtMisc
-module type ATOM =
- sig
+module type ATOM =
+ sig
- type t
+ type t
val index : t -> int
val equal : t -> t -> bool
@@ -25,7 +25,7 @@ module type ATOM =
val to_smt : Format.formatter -> t -> unit
val logic : t -> logic
- end
+ end
type fop =
@@ -38,16 +38,16 @@ type fop =
| Fiff
| Fite
| Fnot2 of int
- | Fforall of (string * SmtBtype.btype) list
-
-type ('a,'f) gen_pform =
+ | Fforall of (string * SmtBtype.btype) list
+
+type ('a,'f) gen_pform =
| Fatom of 'a
| Fapp of fop * 'f array
| FbbT of 'a * 'f list
module type FORM =
- sig
- type hatom
+ sig
+ type hatom
type t
type pform = (hatom, t) gen_pform
@@ -72,16 +72,16 @@ module type FORM =
(* Building formula from positive formula *)
exception NotWellTyped of pform
- type reify
+ type reify
val create : unit -> reify
val clear : reify -> unit
val get : ?declare:bool -> reify -> pform -> t
-
- (** Given a coq term, build the corresponding formula *)
- val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+
+ (** Given a coq term, build the corresponding formula *)
+ val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t
val hash_hform : (hatom -> hatom) -> reify -> t -> t
-
+
(** Flattening of [Fand] and [For], removing of [Fnot2] *)
val flatten : reify -> t -> t
@@ -89,24 +89,22 @@ module type FORM =
counter-parts *)
val right_assoc : reify -> t -> t
- (** Producing Coq terms *)
+ (** Producing Coq terms *)
- val to_coq : t -> Term.constr
+ val to_coq : t -> Structures.constr
val pform_tbl : reify -> pform array
val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
- val interp_tbl : reify -> Term.constr * Term.constr
- val nvars : reify -> int
- (** Producing a Coq term corresponding to the interpretation
+ val interp_tbl : reify -> Structures.constr * Structures.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. *)
- val interp_to_coq :
- (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t ->
- t -> Term.constr
+ val interp_to_coq :
+ (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
+ t -> Structures.constr
end
module Make (Atom:ATOM) : FORM with type hatom = Atom.t
-
-
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index f839869..92f0f09 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -25,16 +25,9 @@ type 'a gen_hashed = { index : int; hval : 'a }
(** Functions over constr *)
-let mklApp f args = Term.mkApp (Lazy.force f, args)
-
-(* TODO : Set -> Type *)
-let declare_new_type = Structures.declare_new_type
-let declare_new_variable = Structures.declare_new_variable
-
-let mkName s =
- let id = Names.id_of_string s in
- Names.Name id
+let mklApp f args = Structures.mkApp (Lazy.force f, args)
+let string_of_name_def d n = try Structures.string_of_name n with | _ -> d
let string_coq_constr t =
let rec fix rf x = rf (fix rf) x in
@@ -43,11 +36,6 @@ let string_coq_constr t =
Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr t))
-let string_of_name = function
- Names.Name id -> Names.string_of_id id
- | _ -> failwith "unnamed rel"
-
-
(** Logics *)
type logic_item =
diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli
index a9de935..f3bcf60 100644
--- a/src/trace/smtMisc.mli
+++ b/src/trace/smtMisc.mli
@@ -10,15 +10,12 @@
(**************************************************************************)
-val cInt_tbl : (int, Term.constr) Hashtbl.t
-val mkInt : int -> Term.constr
+val cInt_tbl : (int, Structures.constr) Hashtbl.t
+val mkInt : int -> Structures.constr
type 'a gen_hashed = { index : int; hval : 'a; }
-val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr
-val declare_new_type : Names.variable -> Term.constr
-val declare_new_variable : Names.variable -> Term.types -> Term.constr
-val mkName : string -> Names.name
-val string_coq_constr : Term.constr -> string
-val string_of_name : Names.name -> string
+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
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 a9855a2..5d9d82d 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -458,10 +458,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 = Names.id_of_string ("ass"^(string_of_int (Hashtbl.hash concl))) in
+ let ass_name = Structures.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 = Term.mkVar ass_name in
+ let ass_var = Structures.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
@@ -471,8 +471,8 @@ let to_coq to_lit interp (cstep,
| Some find -> find cl
| None -> assert false in
let concl' = out_cl [concl] in
- let app_name = Names.id_of_string ("app" ^ (string_of_int (Hashtbl.hash concl))) in
- let app_var = Term.mkVar app_name 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
cuts := (app_name, app_ty)::!cuts;
mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|]
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli
index f06ade4..5ded32a 100644
--- a/src/trace/smtTrace.mli
+++ b/src/trace/smtTrace.mli
@@ -47,26 +47,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 -> Term.constr) ->
- ('a list list * 'a list -> Term.types) ->
- 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 ->
+ ('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 SmtCertif.clause ->
- ('a SmtCertif.clause -> Term.types * Term.constr) option ->
- Term.constr * 'a SmtCertif.clause *
- (Names.identifier * Term.types) list
+ ('a SmtCertif.clause -> Structures.types * Structures.constr) option ->
+ Structures.constr * 'a SmtCertif.clause *
+ (Structures.id * Structures.types) list
module MakeOpt :
functor (Form : SmtForm.FORM) ->
sig
generated by cgit (git 2.34.1) at 2024-06-29 03:05:59 +0000