aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtCommands.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace/smtCommands.ml')
-rw-r--r--src/trace/smtCommands.ml542
1 files changed, 267 insertions, 275 deletions
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index d15ae68..2108da4 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -18,65 +18,57 @@ open SmtTrace
open SmtCertif
-let euf_checker_modules = [ ["SMTCoq";"Trace";"Euf_Checker"] ]
-let certif_ops args = CoqTerms.make_certif_ops euf_checker_modules args
-let cCertif = gen_constant euf_checker_modules "Certif"
-let ccertif = gen_constant euf_checker_modules "certif"
-let cchecker = gen_constant euf_checker_modules "checker"
-let cchecker_correct = gen_constant euf_checker_modules "checker_correct"
-let cchecker_b_correct =
- gen_constant euf_checker_modules "checker_b_correct"
-let cchecker_b = gen_constant euf_checker_modules "checker_b"
-let cchecker_eq_correct =
- gen_constant euf_checker_modules "checker_eq_correct"
-let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
-(* let csetup_checker_step_debug =
- * gen_constant euf_checker_modules "setup_checker_step_debug" *)
-(* let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug" *)
-(* let cstep = gen_constant euf_checker_modules "step" *)
-let cchecker_debug = gen_constant euf_checker_modules "checker_debug"
-
-let cname_step = gen_constant euf_checker_modules "name_step"
-
-let cName_Res = gen_constant euf_checker_modules "Name_Res"
-let cName_Weaken= gen_constant euf_checker_modules "Name_Weaken"
-let cName_ImmFlatten= gen_constant euf_checker_modules "Name_ImmFlatten"
-let cName_CTrue= gen_constant euf_checker_modules "Name_CTrue"
-let cName_CFalse = gen_constant euf_checker_modules "Name_CFalse"
-let cName_BuildDef= gen_constant euf_checker_modules "Name_BuildDef"
-let cName_BuildDef2= gen_constant euf_checker_modules "Name_BuildDef2"
-let cName_BuildProj = gen_constant euf_checker_modules "Name_BuildProj"
-let cName_ImmBuildDef= gen_constant euf_checker_modules "Name_ImmBuildDef"
-let cName_ImmBuildDef2= gen_constant euf_checker_modules "Name_ImmBuildDef2"
-let cName_ImmBuildProj = gen_constant euf_checker_modules "Name_ImmBuildProj"
-let cName_EqTr = gen_constant euf_checker_modules "Name_EqTr"
-let cName_EqCgr = gen_constant euf_checker_modules "Name_EqCgr"
-let cName_EqCgrP= gen_constant euf_checker_modules "Name_EqCgrP"
-let cName_LiaMicromega = gen_constant euf_checker_modules "Name_LiaMicromega"
-let cName_LiaDiseq= gen_constant euf_checker_modules "Name_LiaDiseq"
-let cName_SplArith= gen_constant euf_checker_modules "Name_SplArith"
-let cName_SplDistinctElim = gen_constant euf_checker_modules "Name_SplDistinctElim"
-let cName_BBVar= gen_constant euf_checker_modules "Name_BBVar"
-let cName_BBConst= gen_constant euf_checker_modules "Name_BBConst"
-let cName_BBOp= gen_constant euf_checker_modules "Name_BBOp"
-let cName_BBNot= gen_constant euf_checker_modules "Name_BBNot"
-let cName_BBNeg= gen_constant euf_checker_modules "Name_BBNeg"
-let cName_BBAdd= gen_constant euf_checker_modules "Name_BBAdd"
-let cName_BBConcat= gen_constant euf_checker_modules "Name_BBConcat"
-let cName_BBMul= gen_constant euf_checker_modules "Name_BBMul"
-let cName_BBUlt= gen_constant euf_checker_modules "Name_BBUlt"
-let cName_BBSlt= gen_constant euf_checker_modules "Name_BBSlt"
-let cName_BBEq= gen_constant euf_checker_modules "Name_BBEq"
-let cName_BBDiseq= gen_constant euf_checker_modules "Name_BBDiseq"
-let cName_BBExtract= gen_constant euf_checker_modules "Name_BBExtract"
-let cName_BBZextend= gen_constant euf_checker_modules "Name_BBZextend"
-let cName_BBSextend= gen_constant euf_checker_modules "Name_BBSextend"
-let cName_BBShl= gen_constant euf_checker_modules "Name_BBShl"
-let cName_BBShr= gen_constant euf_checker_modules "Name_BBShr"
-let cName_RowEq= gen_constant euf_checker_modules "Name_RowEq"
-let cName_RowNeq= gen_constant euf_checker_modules "Name_RowNeq"
-let cName_Ext= gen_constant euf_checker_modules "Name_Ext"
-let cName_Hole= gen_constant euf_checker_modules "Name_Hole"
+let certif_ops = CoqTerms.ceuf_checker_certif_ops
+let cCertif = CoqTerms.ceuf_checker_Certif
+let ccertif = CoqTerms.ceuf_checker_certif
+let cchecker = CoqTerms.ceuf_checker_checker
+let cchecker_correct = CoqTerms.ceuf_checker_checker_correct
+let cchecker_b_correct = CoqTerms.ceuf_checker_checker_b_correct
+let cchecker_b = CoqTerms.ceuf_checker_checker_b
+let cchecker_eq_correct = CoqTerms.ceuf_checker_checker_eq_correct
+let cchecker_eq = CoqTerms.ceuf_checker_checker_eq
+let cchecker_debug = CoqTerms.ceuf_checker_checker_debug
+let cname_step = CoqTerms.ceuf_checker_name_step
+let cName_Res = CoqTerms.ceuf_checker_Name_Res
+let cName_Weaken = CoqTerms.ceuf_checker_Name_Weaken
+let cName_ImmFlatten = CoqTerms.ceuf_checker_Name_ImmFlatten
+let cName_CTrue = CoqTerms.ceuf_checker_Name_CTrue
+let cName_CFalse = CoqTerms.ceuf_checker_Name_CFalse
+let cName_BuildDef = CoqTerms.ceuf_checker_Name_BuildDef
+let cName_BuildDef2 = CoqTerms.ceuf_checker_Name_BuildDef2
+let cName_BuildProj = CoqTerms.ceuf_checker_Name_BuildProj
+let cName_ImmBuildDef = CoqTerms.ceuf_checker_Name_ImmBuildDef
+let cName_ImmBuildDef2 = CoqTerms.ceuf_checker_Name_ImmBuildDef2
+let cName_ImmBuildProj = CoqTerms.ceuf_checker_Name_ImmBuildProj
+let cName_EqTr = CoqTerms.ceuf_checker_Name_EqTr
+let cName_EqCgr = CoqTerms.ceuf_checker_Name_EqCgr
+let cName_EqCgrP = CoqTerms.ceuf_checker_Name_EqCgrP
+let cName_LiaMicromega = CoqTerms.ceuf_checker_Name_LiaMicromega
+let cName_LiaDiseq = CoqTerms.ceuf_checker_Name_LiaDiseq
+let cName_SplArith = CoqTerms.ceuf_checker_Name_SplArith
+let cName_SplDistinctElim = CoqTerms.ceuf_checker_Name_SplDistinctElim
+let cName_BBVar = CoqTerms.ceuf_checker_Name_BBVar
+let cName_BBConst = CoqTerms.ceuf_checker_Name_BBConst
+let cName_BBOp = CoqTerms.ceuf_checker_Name_BBOp
+let cName_BBNot = CoqTerms.ceuf_checker_Name_BBNot
+let cName_BBNeg = CoqTerms.ceuf_checker_Name_BBNeg
+let cName_BBAdd = CoqTerms.ceuf_checker_Name_BBAdd
+let cName_BBConcat = CoqTerms.ceuf_checker_Name_BBConcat
+let cName_BBMul = CoqTerms.ceuf_checker_Name_BBMul
+let cName_BBUlt = CoqTerms.ceuf_checker_Name_BBUlt
+let cName_BBSlt = CoqTerms.ceuf_checker_Name_BBSlt
+let cName_BBEq = CoqTerms.ceuf_checker_Name_BBEq
+let cName_BBDiseq = CoqTerms.ceuf_checker_Name_BBDiseq
+let cName_BBExtract = CoqTerms.ceuf_checker_Name_BBExtract
+let cName_BBZextend = CoqTerms.ceuf_checker_Name_BBZextend
+let cName_BBSextend = CoqTerms.ceuf_checker_Name_BBSextend
+let cName_BBShl = CoqTerms.ceuf_checker_Name_BBShl
+let cName_BBShr = CoqTerms.ceuf_checker_Name_BBShr
+let cName_RowEq = CoqTerms.ceuf_checker_Name_RowEq
+let cName_RowNeq = CoqTerms.ceuf_checker_Name_RowNeq
+let cName_Ext = CoqTerms.ceuf_checker_Name_Ext
+let cName_Hole = CoqTerms.ceuf_checker_Name_Hole
+
(* Given an SMT-LIB2 file and a certif, build the corresponding objects *)
@@ -115,7 +107,7 @@ let interp_conseq_uf t_i (prem, concl) =
let tf = Hashtbl.create 17 in
let rec interp = function
| [] -> mklApp cis_true [|interp_uf t_i ta tf concl|]
- | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
+ | c::prem -> CoqInterface.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
interp prem
@@ -127,26 +119,26 @@ let print_assm ty =
let parse_certif t_i t_func t_atom t_form root used_root trace (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 = Structures.mkConst (Structures.declare_constant t_i ce5) in
+ let ce5 = CoqInterface.mkUConst t_i' in
+ let ct_i = CoqInterface.mkConst (CoqInterface.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 = Structures.mkConst (Structures.declare_constant t_func ce6) in
+ let ce6 = CoqInterface.mkUConst t_func' in
+ let ct_func = CoqInterface.mkConst (CoqInterface.declare_constant t_func ce6) in
let t_atom' = Atom.interp_tbl ra in
- let ce1 = Structures.mkUConst t_atom' in
- let ct_atom = Structures.mkConst (Structures.declare_constant t_atom ce1) in
+ let ce1 = CoqInterface.mkUConst t_atom' in
+ let ct_atom = CoqInterface.mkConst (CoqInterface.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 = Structures.mkConst (Structures.declare_constant t_form ce2) in
+ let ce2 = CoqInterface.mkUConst t_form' in
+ let ct_form = CoqInterface.mkConst (CoqInterface.declare_constant t_form ce2) in
(* EMPTY LEMMA LIST *)
let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
(interp_conseq_uf ct_i) (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
List.iter (fun (v,ty) ->
- let _ = Structures.declare_new_variable v ty in
+ let _ = CoqInterface.declare_new_variable v ty in
print_assm ty
) cuts;
@@ -155,22 +147,22 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
let res = Array.make (List.length roots + 1) (mkInt 0) in
let i = ref 0 in
List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
- Structures.mkArray (Lazy.force cint, res) in
+ CoqTerms.mkArray (Lazy.force cint, res) in
let used_roots =
let l = List.length used_roots in
let res = Array.make (l + 1) (mkInt 0) in
let i = ref (l-1) in
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 _ = Structures.declare_constant root ce3 in
- let ce3' = Structures.mkUConst used_roots in
- let _ = Structures.declare_constant used_root ce3' in
+ mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in
+ let ce3 = CoqInterface.mkUConst roots in
+ let _ = CoqInterface.declare_constant root ce3 in
+ let ce3' = CoqInterface.mkUConst used_roots in
+ let _ = CoqInterface.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 _ = Structures.declare_constant trace ce4 in
+ let ce4 = CoqInterface.mkUConst certif in
+ let _ = CoqInterface.declare_constant trace ce4 in
()
@@ -184,15 +176,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 = 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 nti = CoqInterface.mkName "t_i" in
+ let ntfunc = CoqInterface.mkName "t_func" in
+ let ntatom = CoqInterface.mkName "t_atom" in
+ let ntform = CoqInterface.mkName "t_form" in
+ let nc = CoqInterface.mkName "c" in
+ let nused_roots = CoqInterface.mkName "used_roots" in
+ let nd = CoqInterface.mkName "d" in
- let v = Structures.mkRel in
+ let v = CoqInterface.mkRel in
let t_i = make_t_i rt in
let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -204,7 +196,7 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
(interp_conseq_uf t_i)
(certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
List.iter (fun (v,ty) ->
- let _ = Structures.declare_new_variable v ty in
+ let _ = CoqInterface.declare_new_variable v ty in
print_assm ty
) cuts;
@@ -217,59 +209,59 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
let res = Array.make (l + 1) (mkInt 0) in
let i = ref (l-1) in
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
+ mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in
let rootsCstr =
let res = Array.make (List.length roots + 1) (mkInt 0) in
let i = ref 0 in
List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
- Structures.mkArray (Lazy.force cint, res) in
+ CoqTerms.mkArray (Lazy.force cint, res) in
let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in
let theorem_proof_cast =
- 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|],
+ CoqInterface.mkCast (
+ CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+ CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+ CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+ CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+ CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+ CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+ CoqInterface.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*)|])|]))))))),
- Structures.vmcast,
+ CoqInterface.vmcast,
theorem_concl)
in
let theorem_proof_nocast =
- 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|],
+ CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+ CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+ CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+ CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+ CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+ CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+ CoqInterface.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 _ = Structures.declare_constant name ce in
+ let ce = CoqInterface.mkTConst theorem_proof_cast theorem_proof_nocast theorem_concl in
+ let _ = CoqInterface.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 = 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 nti = CoqInterface.mkName "t_i" in
+ let ntfunc = CoqInterface.mkName "t_func" in
+ let ntatom = CoqInterface.mkName "t_atom" in
+ let ntform = CoqInterface.mkName "t_form" in
+ let nc = CoqInterface.mkName "c" in
+ let nused_roots = CoqInterface.mkName "used_roots" in
+ let nd = CoqInterface.mkName "d" in
- let v = Structures.mkRel in
+ let v = CoqInterface.mkRel in
let t_i = make_t_i rt in
let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -281,7 +273,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
(interp_conseq_uf t_i)
(certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
List.iter (fun (v,ty) ->
- let _ = Structures.declare_new_variable v ty in
+ let _ = CoqInterface.declare_new_variable v ty in
print_assm ty
) cuts;
@@ -294,26 +286,26 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
let res = Array.make (l + 1) (mkInt 0) in
let i = ref (l-1) in
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
+ mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in
let rootsCstr =
let res = Array.make (List.length roots + 1) (mkInt 0) in
let i = ref 0 in
List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
- Structures.mkArray (Lazy.force cint, res) in
+ CoqTerms.mkArray (Lazy.force cint, res) in
let tm =
- 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|],
+ CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+ CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+ CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+ CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+ CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+ CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+ CoqInterface.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
+ let res = CoqInterface.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
Format.eprintf " = %s\n : bool@."
- (if Structures.eq_constr res (Lazy.force CoqTerms.ctrue) then
+ (if CoqInterface.eq_constr res (Lazy.force CoqTerms.ctrue) then
"true" else "false")
let count_used confl =
@@ -329,15 +321,15 @@ let count_used confl =
let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
- 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 nti = CoqInterface.mkName "t_i" in
+ let ntfunc = CoqInterface.mkName "t_func" in
+ let ntatom = CoqInterface.mkName "t_atom" in
+ let ntform = CoqInterface.mkName "t_form" in
+ let nc = CoqInterface.mkName "c" in
+ let nused_roots = CoqInterface.mkName "used_roots" in
+ let nd = CoqInterface.mkName "d" in
- let v = Structures.mkRel in
+ let v = CoqInterface.mkRel in
let t_i = make_t_i rt in
let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -349,7 +341,7 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
(certif_ops (Some [|v 4(*t_i*); v 3(*t_func*);
v 2(*t_atom*); v 1(* t_form *)|])) confl None in
List.iter (fun (v,ty) ->
- let _ = Structures.declare_new_variable v ty in
+ let _ = CoqInterface.declare_new_variable v ty in
print_assm ty
) cuts;
@@ -364,84 +356,84 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
let i = ref (l-1) in
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
+ CoqTerms.mkArray (Lazy.force cint, res)|] in
let rootsCstr =
let res = Array.make (List.length roots + 1) (mkInt 0) in
let i = ref 0 in
List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
- Structures.mkArray (Lazy.force cint, res) in
+ CoqTerms.mkArray (Lazy.force cint, res) in
let tm =
- Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
- Structures.mkLetIn (ntfunc, t_func,
+ CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+ CoqInterface.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*);
+ CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+ CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+ CoqInterface.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,
+ CoqInterface.mkLetIn (nused_roots, used_rootsCstr,
mklApp coption [|mklApp carray [|Lazy.force cint|]|],
- Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+ CoqInterface.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
- let res = Structures.cbv_vm (Global.env ()) tm
+ let res = CoqInterface.cbv_vm (Global.env ()) tm
(mklApp coption
[|mklApp cprod
[|Lazy.force cnat; Lazy.force cname_step|]|]) in
- 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 \
+ match CoqInterface.decompose_app res with
+ | c, _ when CoqInterface.eq_constr c (Lazy.force cNone) ->
+ CoqInterface.error ("Debug checker is only meant to be used for certificates \
that fail to be checked by SMTCoq.")
- | 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
+ | c, [_; n] when CoqInterface.eq_constr c (Lazy.force cSome) ->
+ (match CoqInterface.decompose_app n with
+ | c, [_; _; cnb; cn] when CoqInterface.eq_constr c (Lazy.force cpair) ->
+ let n = fst (CoqInterface.decompose_app cn) in
let name =
- 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"
+ if CoqInterface.eq_constr n (Lazy.force cName_Res ) then "Res"
+ else if CoqInterface.eq_constr n (Lazy.force cName_Weaken) then "Weaken"
+ else if CoqInterface.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten"
+ else if CoqInterface.eq_constr n (Lazy.force cName_CTrue) then "CTrue"
+ else if CoqInterface.eq_constr n (Lazy.force cName_CFalse ) then "CFalse"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj"
+ else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef"
+ else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2"
+ else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj"
+ else if CoqInterface.eq_constr n (Lazy.force cName_EqTr ) then "EqTr"
+ else if CoqInterface.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr"
+ else if CoqInterface.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP"
+ else if CoqInterface.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega"
+ else if CoqInterface.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq"
+ else if CoqInterface.eq_constr n (Lazy.force cName_SplArith) then "SplArith"
+ else if CoqInterface.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBVar) then "BBVar"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBConst) then "BBConst"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBOp) then "BBOp"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBNot) then "BBNot"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBMul) then "BBMul"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBEq) then "BBEq"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBShl) then "BBShl"
+ else if CoqInterface.eq_constr n (Lazy.force cName_BBShr) then "BBShr"
+ else if CoqInterface.eq_constr n (Lazy.force cName_RowEq) then "RowEq"
+ else if CoqInterface.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq"
+ else if CoqInterface.eq_constr n (Lazy.force cName_Ext) then "Ext"
+ else if CoqInterface.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
- Structures.error ("Step number " ^ string_of_int nb ^
+ CoqInterface.error ("Step number " ^ string_of_int nb ^
" (" ^ name ^ ") of the certificate likely failed.")
| _ -> assert false
)
@@ -450,9 +442,9 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
(* let rec of_coq_list cl =
- * 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) ->
+ * match CoqInterface.decompose_app cl with
+ * | c, _ when CoqInterface.eq_constr c (Lazy.force cnil) -> []
+ * | c, [_; x; cr] when CoqInterface.eq_constr c (Lazy.force ccons) ->
* x :: of_coq_list cr
* | _ -> assert false *)
@@ -461,29 +453,29 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
* (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 = Structures.mkConst (Structures.declare_constant t_i ce5) in
+ * let ce5 = CoqInterface.mkUConst t_i' in
+ * let ct_i = CoqInterface.mkConst (CoqInterface.declare_constant t_i ce5) in
*
* let t_func' = make_t_func ro ct_i in
- * let ce6 = Structures.mkUConst t_func' in
+ * let ce6 = CoqInterface.mkUConst t_func' in
* let ct_func =
- * Structures.mkConst (Structures.declare_constant t_func ce6) in
+ * CoqInterface.mkConst (CoqInterface.declare_constant t_func ce6) in
*
* let t_atom' = Atom.interp_tbl ra in
- * let ce1 = Structures.mkUConst t_atom' in
+ * let ce1 = CoqInterface.mkUConst t_atom' in
* let ct_atom =
- * Structures.mkConst (Structures.declare_constant t_atom ce1) in
+ * CoqInterface.mkConst (CoqInterface.declare_constant t_atom ce1) in
*
* let t_form' = snd (Form.interp_tbl rf) in
- * let ce2 = Structures.mkUConst t_form' in
+ * let ce2 = CoqInterface.mkUConst t_form' in
* let ct_form =
- * Structures.mkConst (Structures.declare_constant t_form ce2) in
+ * CoqInterface.mkConst (CoqInterface.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)
* (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
* List.iter (fun (v,ty) ->
- * let _ = Structures.declare_new_variable v ty in
+ * let _ = CoqInterface.declare_new_variable v ty in
* print_assm ty
* ) cuts;
*
@@ -492,37 +484,37 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
* let res = Array.make (List.length roots + 1) (mkInt 0) in
* let i = ref 0 in
* List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
- * Structures.mkArray (Lazy.force cint, res) in
+ * CoqTerms.mkArray (Lazy.force cint, res) in
* let cused_roots =
* let l = List.length used_roots in
* let res = Array.make (l + 1) (mkInt 0) in
* let i = ref (l-1) in
* 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 croots in
- * let _ = Structures.declare_constant root ce3 in
- * let ce3' = Structures.mkUConst cused_roots in
- * let _ = Structures.declare_constant used_root ce3' in
+ * CoqTerms.mkArray (Lazy.force cint, res)|] in
+ * let ce3 = CoqInterface.mkUConst croots in
+ * let _ = CoqInterface.declare_constant root ce3 in
+ * let ce3' = CoqInterface.mkUConst cused_roots in
+ * let _ = CoqInterface.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 _ = Structures.declare_constant trace ce4 in
+ * let ce4 = CoqInterface.mkUConst certif in
+ * let _ = CoqInterface.declare_constant trace ce4 in
*
* let setup =
* mklApp csetup_checker_step_debug
* [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in
*
- * let setup = Structures.cbv_vm (Global.env ()) setup
+ * let setup = CoqInterface.cbv_vm (Global.env ()) setup
* (mklApp cprod
* [|Lazy.force cState_S_t;
* mklApp clist [|mklApp cstep
* [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in
*
- * let s, steps = match Structures.decompose_app setup with
- * | c, [_; _; s; csteps] when Structures.eq_constr c (Lazy.force cpair) ->
+ * let s, steps = match CoqInterface.decompose_app setup with
+ * | c, [_; _; s; csteps] when CoqInterface.eq_constr c (Lazy.force cpair) ->
* s, of_coq_list csteps
* | _ -> assert false
* in
@@ -536,22 +528,22 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
* [| ct_i; ct_func; ct_atom; ct_form; s; step |] in
*
* let res =
- * Structures.cbv_vm (Global.env ()) tm
+ * CoqInterface.cbv_vm (Global.env ()) tm
* (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
*
- * match Structures.decompose_app res with
- * | c, [_; _; s; cbad] when Structures.eq_constr c (Lazy.force cpair) ->
+ * match CoqInterface.decompose_app res with
+ * | c, [_; _; s; cbad] when CoqInterface.eq_constr c (Lazy.force cpair) ->
* if not (mk_bool cbad) then s
- * else Structures.error ("Step number " ^ string_of_int !cpt ^
+ * else CoqInterface.error ("Step number " ^ string_of_int !cpt ^
* " (" ^ string_coq_constr
- * (fst (Structures.decompose_app step)) ^ ")" ^
+ * (fst (CoqInterface.decompose_app step)) ^ ")" ^
* " of the certificate likely failed." )
* | _ -> assert false
* in
*
* List.fold_left debug_step s steps |> ignore;
*
- * Structures.error ("Debug checker is only meant to be used for certificates \
+ * CoqInterface.error ("Debug checker is only meant to be used for certificates \
* that fail to be checked by SMTCoq.") *)
@@ -559,16 +551,16 @@ 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 = 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 nti = CoqInterface.mkName "t_i" in
+ let ntfunc = CoqInterface.mkName "t_func" in
+ let ntatom = CoqInterface.mkName "t_atom" in
+ let ntform = CoqInterface.mkName "t_form" in
+ let nc = CoqInterface.mkName "c" in
- let v = Structures.mkRel in
+ let v = CoqInterface.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
+ let t_func = CoqInterface.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in
let t_atom = Atom.interp_tbl ra in
let t_form = snd (Form.interp_tbl rf) in
let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq
@@ -583,11 +575,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 =
- 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
+ CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+ CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
+ CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+ CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+ CoqInterface.mkLetIn (nc, certif, mklApp ccertif
[|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
t))))) in
@@ -614,16 +606,16 @@ 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 = 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 nti = CoqInterface.mkName "t_i" in
+ let ntfunc = CoqInterface.mkName "t_func" in
+ let ntatom = CoqInterface.mkName "t_atom" in
+ let ntform = CoqInterface.mkName "t_form" in
+ let nc = CoqInterface.mkName "c" in
- let v = Structures.mkRel in
+ let v = CoqInterface.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
+ let t_func = CoqInterface.lift 1 (make_t_func ro (v 0 (*t_i*))) in
let t_atom = Atom.interp_tbl ra in
let t_form = snd (Form.interp_tbl rf) in
let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq
@@ -633,11 +625,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 =
- 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
+ CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+ CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
+ CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+ CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+ CoqInterface.mkLetIn (nc, certif, mklApp ccertif
[|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
t))))) in
@@ -665,10 +657,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 = Structures.decompose_app concl in
+ let f, args = CoqInterface.decompose_app concl in
match args with
- | [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
+ | [ty;a;b] when (CoqInterface.eq_constr f (Lazy.force ceq)) && (CoqInterface.eq_constr ty (Lazy.force cbool)) -> a, b
+ | [a] when (CoqInterface.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue
| _ -> failwith ("Verit.tactic: can only deal with equality over bool")
@@ -689,7 +681,7 @@ let gen_rel_name =
let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
let warn () =
- Structures.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr (Structures.extern_constr clemma))));
+ CoqInterface.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (CoqInterface.extern_constr clemma))));
None
in
@@ -698,16 +690,16 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
let rel_context = List.map (fun rel -> Context.Rel.Declaration.set_name (Names.Name.mk_name (Names.Id.of_string (gen_rel_name ()))) rel) rel_context in
let env_lemma = Environ.push_rel_context rel_context env in
- let f, args = Structures.decompose_app qf_lemma in
+ let f, args = CoqInterface.decompose_app qf_lemma in
let core_f =
- if Structures.eq_constr f (Lazy.force cis_true) then
+ if CoqInterface.eq_constr f (Lazy.force cis_true) then
match args with
| [a] -> Some a
| _ -> warn ()
- else if Structures.eq_constr f (Lazy.force ceq) then
+ else if CoqInterface.eq_constr f (Lazy.force ceq) then
match args with
- | [ty; arg1; arg2] when Structures.eq_constr ty (Lazy.force cbool) &&
- Structures.eq_constr arg2 (Lazy.force ctrue) ->
+ | [ty; arg1; arg2] when CoqInterface.eq_constr ty (Lazy.force cbool) &&
+ CoqInterface.eq_constr arg2 (Lazy.force ctrue) ->
Some arg1
| _ -> warn ()
else warn () in
@@ -722,8 +714,8 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
| None -> None
in
let forall_args =
- let fmap r = let n, t = Structures.destruct_rel_decl r in
- Structures.string_of_name n, SmtBtype.of_coq rt solver_logic t in
+ let fmap r = let n, t = CoqInterface.destruct_rel_decl r in
+ CoqInterface.string_of_name n, SmtBtype.of_coq rt solver_logic t in
List.map fmap rel_context
in
match forall_args with
@@ -736,11 +728,11 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl env sigma concl =
let a, b = get_arguments concl in
- let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in
+ let tlcepl = List.map (CoqInterface.interp_constr env sigma) lcepl in
let lcpl = lcpl @ tlcepl in
let create_lemma l =
- let cl = Structures.retyping_get_type_of env sigma l in
+ let cl = CoqInterface.retyping_get_type_of env sigma l in
match of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic cl with
| Some smt -> Some ((cl, l), smt)
| None -> None
@@ -748,7 +740,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l
let l_pl_ls = SmtMisc.filter_map create_lemma lcpl in
let lsmt = List.map snd l_pl_ls in
- let lem_tbl : (int, Structures.constr * Structures.constr) Hashtbl.t =
+ let lem_tbl : (int, CoqInterface.constr * CoqInterface.constr) Hashtbl.t =
Hashtbl.create 100 in
let new_ref ((l, pl), ls) =
Hashtbl.add lem_tbl (Form.index ls) (l, pl) in
@@ -770,11 +762,11 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l
| _ -> failwith "unexpected form of root" in
let (body_cast, body_nocast, cuts) =
- if ((Structures.eq_constr b (Lazy.force ctrue)) ||
- (Structures.eq_constr b (Lazy.force cfalse))) then (
+ if ((CoqInterface.eq_constr b (Lazy.force ctrue)) ||
+ (CoqInterface.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 _ = Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env sigma) rf_quant a in
- let nl = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
+ let nl = if (CoqInterface.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
let lsmt = Form.flatten rf nl :: lsmt in
let max_id_confl = make_proof call_solver env rt ro ra_quant rf_quant nl lsmt in
build_body rt ro ra rf (Form.to_coq l) b max_id_confl (vm_cast env) (Some find_lemma)
@@ -793,19 +785,19 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l
let cuts = (SmtBtype.get_cuts rt) @ cuts in
List.fold_right (fun (eqn, eqt) tac ->
- Structures.tclTHENLAST
- (Structures.assert_before (Structures.name_of_id eqn) eqt)
+ CoqInterface.tclTHENLAST
+ (CoqInterface.assert_before (CoqInterface.name_of_id eqn) eqt)
tac
) cuts
- (Structures.tclTHEN
- (Structures.set_evars_tac body_nocast)
- (Structures.vm_cast_no_check body_cast))
+ (CoqInterface.tclTHEN
+ (CoqInterface.set_evars_tac body_nocast)
+ (CoqInterface.vm_cast_no_check body_cast))
let tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl =
- Structures.tclTHEN
+ CoqInterface.tclTHEN
Tactics.intros
- (Structures.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl))
+ (CoqInterface.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl))
(**********************************************)
@@ -822,7 +814,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 (Structures.mkId s) env in
+ let nd = Environ.lookup_named (CoqInterface.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 -> ());
@@ -832,11 +824,11 @@ let string_index_of_constr env i cf =
let vstring_i env i =
let cf = SmtAtom.Atom.get_coq_term_op i in
- if Structures.isRel cf then
- let dbi = Structures.destRel cf in
+ if CoqInterface.isRel cf then
+ let dbi = CoqInterface.destRel cf in
let s =
Environ.lookup_rel dbi env
- |> Structures.get_rel_dec_name
+ |> CoqInterface.get_rel_dec_name
|> SmtMisc.string_of_name_def "?"
in
s, dbi
@@ -977,14 +969,14 @@ let model_item env rt ro ra rf =
* let outf = Format.formatter_of_out_channel out in
* SExpr.print outf l; pp_print_flush outf ();
* close_out out; *)
- Structures.error ("Could not reconstruct model")
+ CoqInterface.error ("Could not reconstruct model")
let model env rt ro ra rf = function
| List (Atom "model" :: l) ->
List.fold_left (fun acc m -> match model_item env rt ro ra rf m with Fun m -> m::acc | Sort -> acc) [] l
|> List.sort (fun ((_ ,i1), _) ((_, i2), _) -> i2 - i1)
- | _ -> Structures.error ("No model")
+ | _ -> CoqInterface.error ("No model")
let model_string env rt ro ra rf s =
generated by cgit (git 2.34.1) at 2024-06-02 02:42:54 +0000