Possibility to embed any Coq proof in certificates (not tested yet)

4 files changed, 113 insertions, 81 deletions

diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index d405894..f2c24b8 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -163,16 +163,21 @@ let cFite = gen_constant smt_modules "Fite"
 
 let cis_true = gen_constant smt_modules "is_true"
 
-let make_certif_ops modules = 
- (gen_constant modules "step", 
-  gen_constant modules "Res", gen_constant modules "ImmFlatten", 
-  gen_constant modules "CTrue", gen_constant modules "CFalse", 
-  gen_constant modules "BuildDef", gen_constant modules "BuildDef2", 
-  gen_constant modules "BuildProj", 
-  gen_constant modules "ImmBuildProj", gen_constant modules"ImmBuildDef", 
-  gen_constant modules"ImmBuildDef2",
-  gen_constant modules "EqTr", gen_constant modules "EqCgr", gen_constant modules "EqCgrP", 
-  gen_constant modules "LiaMicromega", gen_constant modules "LiaDiseq", gen_constant modules "SplArith", gen_constant modules "SplDistinctElim")
+let make_certif_ops modules args =
+  let gen_constant c =
+    match args with
+      | Some args -> lazy (SmtMisc.mklApp (gen_constant modules c) args)
+      | None -> gen_constant modules c in
+ (gen_constant "step", 
+  gen_constant "Res", gen_constant "ImmFlatten", 
+  gen_constant "CTrue", gen_constant "CFalse", 
+  gen_constant "BuildDef", gen_constant "BuildDef2", 
+  gen_constant "BuildProj", 
+  gen_constant "ImmBuildProj", gen_constant"ImmBuildDef", 
+  gen_constant"ImmBuildDef2",
+  gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP", 
+  gen_constant "LiaMicromega", gen_constant "LiaDiseq", gen_constant "SplArith", gen_constant "SplDistinctElim",
+  gen_constant "Hole")
   
 
 (** Useful construction *)
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index 6a56c43..8ed87e4 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -108,6 +108,9 @@ type 'hform rule =
   (* Elimination of operators *)
   | SplDistinctElim of 'hform clause * 'hform
 
+  (* Possibility to introduce "holes" in proofs (that should be filled in Coq) *)
+  | Hole of 'hform
+
 and 'hform clause = {
             id    : clause_id;
     mutable kind  : 'hform clause_kind;
@@ -137,4 +140,5 @@ let used_clauses r =
   | ImmFlatten (c,_)  | SplArith (c,_,_) | SplDistinctElim (c,_) -> [c]
   | True | False | BuildDef _ | BuildDef2 _ | BuildProj _
   | EqTr _ | EqCgr _ | EqCgrP _
-  | LiaMicromega _ | LiaDiseq _ -> []
+  | LiaMicromega _ | LiaDiseq _
+  | Hole _ -> []
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)
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index e2a9b1d..83b8779 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -274,12 +274,18 @@ let build_certif first_root confl =
   alloc first_root
 
 
-let to_coq to_lit (cstep,
+(* [isCut]: true if we handle holes by adding cuts inside a tactic,
+   false otherwise (then, by adding a section variable) *)
+let to_coq to_lit interp (cstep,
     cRes, cImmFlatten,
     cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj,
     cImmBuildProj,cImmBuildDef,cImmBuildDef2,  
     cEqTr, cEqCgr, cEqCgrP, 
-    cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim) confl =
+    cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim,
+    cHole) confl isCut =
+
+  let cuts = ref [] in
+
   let out_f f = to_lit f in
   let out_c c = mkInt (get_pos c) in
   let step_to_coq c =
@@ -328,6 +334,20 @@ let to_coq to_lit (cstep,
           let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in
           mklApp cSplArith [|out_c c; out_c orig; res'; l'|]
 	| SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|]
+        | Hole res ->
+           let ass_name = Names.id_of_string ("ass"^(string_of_int (
+             if isCut then List.length !cuts else Hashtbl.hash res
+           ))) in
+           let ass_ty = interp res in
+           let ass_var =
+             if isCut then (
+               let ass_var = Term.mkVar ass_name in
+               cuts := (ass_name, ass_ty)::!cuts;
+               ass_var
+             ) else (
+               declare_new_variable ass_name ass_ty
+             ) in
+           mklApp cHole [|out_c c; out_f res; ass_var|]
 	end
     | _ -> assert false in
   let step = Lazy.force cstep in
@@ -361,7 +381,7 @@ let to_coq to_lit (cstep,
     trace.(q) <- Structures.mkArray (step, traceq)
   end;
 
-  (Structures.mkArray (mklApp carray [|step|], trace), last_root)
+  (Structures.mkArray (mklApp carray [|step|], trace), last_root, !cuts)