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.ml137
1 files changed, 70 insertions, 67 deletions
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index bace2d2..de6a8fb 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -27,7 +27,7 @@ open SmtCertif
let euf_checker_modules = [ ["SMTCoq";"Trace";"Euf_Checker"] ]
-let certif_ops = CoqTerms.make_certif_ops euf_checker_modules
+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"
@@ -66,11 +66,13 @@ let compute_roots roots last_root =
let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, roots, max_id, confl) =
- let (tres, last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in
- let certif =
- mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
- let ce4 = Structures.mkConst certif in
- let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in
+
+ let t_i' = make_t_i rt in
+ let t_func' = make_t_func ro t_i' in
+ let t_atom' = Atom.interp_tbl ra in
+ let t_form' = snd (Form.interp_tbl rf) in
+
+ let (tres, last_root, _) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|t_i'; t_func'; t_atom'; t_form'|])) confl false in
let used_roots = compute_roots roots last_root in
let roots =
let res = Array.make (List.length roots + 1) (mkInt 0) in
@@ -87,16 +89,18 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in
let ce3' = Structures.mkConst used_roots in
let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in
- let t_i' = make_t_i rt in
- let t_func' = make_t_func ro t_i' in
let ce5 = Structures.mkConst t_i' in
let _ = declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition) in
let ce6 = Structures.mkConst t_func' in
let _ = declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition) in
- let ce1 = Structures.mkConst (Atom.interp_tbl ra) in
+ let ce1 = Structures.mkConst t_atom' in
let _ = declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition) in
- let ce2 = Structures.mkConst (snd (Form.interp_tbl rf)) in
+ let ce2 = Structures.mkConst t_form' in
let _ = declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition) in
+ let certif =
+ mklApp cCertif [|t_i'; t_func'; t_atom'; t_form'; mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+ let ce4 = Structures.mkConst certif in
+ let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in
()
@@ -109,9 +113,12 @@ let interp_roots roots =
| f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots
let build_certif (rt, ro, ra, rf, roots, max_id, confl) =
- let (tres,last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in
- let certif =
- mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+ let t_atom = Atom.interp_tbl ra in
+ let t_form = snd (Form.interp_tbl rf) in
+ let t_i = make_t_i rt in
+ let t_func = make_t_func ro t_i in
+
+ let (tres,last_root,_) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|t_i; t_func; t_atom; t_form|])) confl false in
let used_roots = compute_roots roots last_root in
let used_rootsCstr =
let l = List.length used_roots in
@@ -125,10 +132,8 @@ let build_certif (rt, ro, ra, rf, roots, max_id, confl) =
List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
Structures.mkArray (Lazy.force cint, res) in
- let t_atom = Atom.interp_tbl ra in
- let t_form = snd (Form.interp_tbl rf) in
- let t_i = make_t_i rt in
- let t_func = make_t_func ro t_i in
+ let certif =
+ mklApp cCertif [|t_i; t_func; t_atom; t_form; mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
(rootsCstr, used_rootsCstr, certif, t_atom, t_form, t_i, t_func)
@@ -141,7 +146,7 @@ let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) =
Term.mkLetIn (mkName "t_atom", t_atom, mklApp carray [|Lazy.force catom|], (*6*)
Term.mkLetIn (mkName "t_form", t_form, mklApp carray [|Lazy.force cform|], (*5*)
Term.mkLetIn (mkName "d", rootsCstr, mklApp carray [|Lazy.force cint|], (*4*)
- Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, (*3*)
+ Term.mkLetIn (mkName "c", certif, mklApp ccertif [|t_i; t_func; t_atom; t_form|], (*3*)
Term.mkLetIn (mkName "t_i", t_i, mklApp carray [|Lazy.force ctyp_eqb|], (*2*)
Term.mkLetIn (mkName "t_func", t_func, mklApp carray [|mklApp ctval [|t_i|]|], (*1*)
mklApp cchecker_correct
@@ -169,67 +174,65 @@ let checker ((rt, ro, ra, rf, roots, max_id, confl) as p) =
(* Tactic *)
let build_body rt ro ra rf l b (max_id, confl) =
- let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in
- let certif =
- mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
-
- let t_atom = Atom.interp_tbl ra in
- let t_form = snd (Form.interp_tbl rf) in
- let t_i = make_t_i rt in
- let t_func = make_t_func ro t_i in
-
+ 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 = mkName "t_i" in
- let ntfunc = mkName "t_func" in
- let vtatom = Term.mkRel 5 in
- let vtform = Term.mkRel 4 in
- let vc = Term.mkRel 3 in
- let vti = Term.mkRel 2 in
- let vtfunc = Term.mkRel 1 in
+ let v = Term.mkRel in
- Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
- Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, Lazy.force ccertif,
- Term.mkLetIn (nti, Structures.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|],
- Term.mkLetIn (ntfunc, Structures.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|],
- mklApp cchecker_b_correct
- [|vti;vtfunc;vtatom; vtform; l; b; vc;
- vm_cast_true (mklApp cchecker_b [|vti;vtfunc;vtatom;vtform;l;b;vc|])|])))))
+ let t_i = make_t_i rt in
+ let t_func = Term.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 (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl true in
+ let certif =
+ 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 proof =
+ Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+ 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*)|],
+ mklApp cchecker_b_correct
+ [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*);
+ vm_cast_true (mklApp cchecker_b [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*)|])|])))))
+ in
-let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
- let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in
- let certif =
- mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+ (proof, cuts)
- let t_atom = Atom.interp_tbl ra in
- let t_form = snd (Form.interp_tbl rf) in
- let t_i = make_t_i rt in
- let t_func = make_t_func ro t_i in
+let build_body_eq rt ro ra rf l1 l2 l (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 nti = mkName "t_i" in
- let ntfunc = mkName "t_func" in
- let vtatom = Term.mkRel 5 in
- let vtform = Term.mkRel 4 in
- let vc = Term.mkRel 3 in
- let vti = Term.mkRel 2 in
- let vtfunc = Term.mkRel 1 in
+ let v = Term.mkRel in
+
+ let t_i = make_t_i rt in
+ let t_func = Term.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 (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl true in
+ let certif =
+ 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 proof =
+ Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+ 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*)|],
+ mklApp cchecker_eq_correct
+ [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*);
+ vm_cast_true (mklApp cchecker_eq [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*)|])|])))))
+ in
- Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
- Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, Lazy.force ccertif,
- Term.mkLetIn (nti, Structures.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|],
- Term.mkLetIn (ntfunc, Structures.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|],
- mklApp cchecker_eq_correct
- [|vti;vtfunc;vtatom; vtform; l1; l2; l; vc;
- vm_cast_true (mklApp cchecker_eq [|vti;vtfunc;vtatom;vtform;l1;l2;l;vc|])|])))))
+ (proof, cuts)
let get_arguments concl =
@@ -250,7 +253,7 @@ let tactic call_solver rt ro ra rf env sigma t =
let (forall_let, concl) = Term.decompose_prod_assum t in
let env = Environ.push_rel_context forall_let env in
let a, b = get_arguments concl in
- let body =
+ let (body, cuts) =
if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then
let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
@@ -265,7 +268,7 @@ let tactic call_solver rt ro ra rf env sigma t =
let compose_lam_assum forall_let body =
List.fold_left (fun t rd -> Term.mkLambda_or_LetIn rd t) body forall_let in
let res = compose_lam_assum forall_let body in
- let cuts = Btype.get_cuts rt in
+ let cuts = (Btype.get_cuts rt)@cuts in
List.fold_right (fun (eqn, eqt) tac ->
Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac
) cuts (Structures.vm_cast_no_check res)
generated by cgit (git 2.34.1) at 2024-07-03 05:23:29 +0000