Print warnings when checking proofs with holes

5 files changed, 46 insertions, 24 deletions

diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 5e984a4..4c0ea6d 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -81,6 +81,13 @@ let interp_conseq_uf (prem, concl) =
   interp prem
 
 
+let print_assm ty =
+  let rec fix rf x = rf (fix rf) x in
+  let pr = fix Ppconstr.modular_constr_pr Pp.mt Structures.ppconstr_lsimpleconstr in
+  Printf.printf "WARNING: assuming the following hypothesis:\n%s\n\n" (Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr ty)));
+  flush stdout
+
+
 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
@@ -99,7 +106,12 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
   let ce2 = Structures.mkUConst t_form' in
   let ct_form = Term.mkConst (declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition)) in
 
-  let (tres, last_root, _) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl false in
+  let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl in
+  List.iter (fun (v,ty) ->
+    let _ = Structures.declare_new_variable v ty in
+    print_assm ty
+  ) cuts;
+
   let used_roots = compute_roots roots last_root in
   let roots =
     let res = Array.make (List.length roots + 1) (mkInt 0) in
@@ -149,7 +161,12 @@ let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) =
   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)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl false in
+  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl in
+  List.iter (fun (v,ty) ->
+    let _ = Structures.declare_new_variable v ty in
+    print_assm ty
+  ) cuts;
+
   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
 
@@ -203,7 +220,12 @@ let checker ((rt, ro, ra, rf, roots, max_id, confl) as p) =
   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)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl false in
+  let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl in
+  List.iter (fun (v,ty) ->
+    let _ = Structures.declare_new_variable v ty in
+    print_assm ty
+  ) cuts;
+
   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
 
@@ -251,7 +273,7 @@ let build_body rt ro ra rf l b (max_id, confl) =
   let t_func = Structures.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 interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl true in
+  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl 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
 
@@ -282,7 +304,7 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
   let t_func = Structures.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 interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl true in
+  let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl 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
 
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index b6f4295..b3248ef 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -274,15 +274,13 @@ let build_certif first_root confl =
   alloc first_root
 
 
-(* [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,
-    cHole) confl isCut =
+    cHole) confl =
 
   let cuts = ref [] in
 
@@ -336,18 +334,10 @@ let to_coq to_lit interp (cstep,
 	| SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|]
         | 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 (
-             if isCut then List.length !cuts else Hashtbl.hash concl
-           ))) in
+           let ass_name = Names.id_of_string ("ass"^(string_of_int (Hashtbl.hash concl))) in
            let ass_ty = interp (prem, concl) 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
+           cuts := (ass_name, ass_ty)::!cuts;
+           let ass_var = Term.mkVar ass_name in
            let out_cl cl = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) 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
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 51e14d6..a35d04b 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -89,3 +89,8 @@ let mk_smt_tactic tac gl =
   let sigma = Tacmach.project gl in
   let t = Tacmach.pf_concl gl in
   tac env sigma t gl
+
+let ppconstr_lsimpleconstr = Ppconstr.lsimple
+let constrextern_extern_constr =
+  let env = Global.env () in
+  Constrextern.extern_constr false env
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 26a8cc1..6921593 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -128,3 +128,8 @@ let mk_smt_tactic tac =
     let t = Proofview.Goal.concl gl in
     tac env sigma t
   )
+
+let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr
+let constrextern_extern_constr =
+  let env = Global.env () in
+  Constrextern.extern_constr false env (Evd.from_env env)
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 523bd1d..74ae918 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -204,7 +204,7 @@ let parse_certif dimacs trace fdimacs ftrace =
   let _ = declare_constant dimacs (DefinitionEntry ce1, IsDefinition Definition) in
 
   let max_id, confl = import_cnf_trace reloc ftrace first last in
-  let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl false in
+  let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in
   let certif = 
    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in 
   let ce2 = Structures.mkUConst certif in
@@ -223,7 +223,7 @@ let theorem name fdimacs ftrace =
 
   let max_id, confl = import_cnf_trace reloc ftrace first last in
   let (tres,_,_) =
-    SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl false in
+    SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in
   let certif =
    mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in 
 
@@ -252,7 +252,7 @@ let checker fdimacs ftrace =
 
   let max_id, confl = import_cnf_trace reloc ftrace first last in
   let (tres,_,_) =
-    SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl false in
+    SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in
   let certif =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
 
@@ -351,7 +351,7 @@ let build_body reify_atom reify_form l b (max_id, confl) =
   let tvar = Atom.interp_tbl reify_atom in
   let _, tform = Form.interp_tbl reify_form in
   let (tres,_,_) =
-    SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl false in
+    SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl in
   let certif =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
   let vtvar = Term.mkRel 3 in
@@ -372,7 +372,7 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) =
   let tvar = Atom.interp_tbl reify_atom in
   let _, tform = Form.interp_tbl reify_form in
   let (tres,_,_) =
-    SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl false in
+    SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl in
   let certif =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in 
   let vtvar = Term.mkRel 3 in