Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 81 insertions, 32 deletions

diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 4e256981fc..fe41b96cbb 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -46,7 +46,6 @@ let rec nb_prod_after n c=
     | _ -> 0
 
 let construct_nhyps ind gls =
-  let env=pf_env gls in
   let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
   let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in 
   let hyp = nb_prod_after nparams in	
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index 451ac33d8c..39ab02cc14 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -24,7 +24,7 @@ open Libnames
 
 (* declaring search depth as a global option *)
 
-let ground_depth=ref 5
+let ground_depth=ref 3
 
 let _=
   let gdopt=
@@ -34,13 +34,28 @@ let _=
       optread=(fun ()->Some !ground_depth); 
       optwrite=
    (function 
-	None->ground_depth:=5
+	None->ground_depth:=3
       |	Some i->ground_depth:=(max i 0))}
   in
     declare_int_option gdopt
-      
+
+let congruence_depth=ref 100
+
+let _=
+  let gdopt=
+    { optsync=true;
+      optname="Congruence Depth";
+      optkey=SecondaryTable("Congruence","Depth"); 
+      optread=(fun ()->Some !congruence_depth); 
+      optwrite=
+   (function 
+	None->congruence_depth:=0
+      |	Some i->congruence_depth:=(max i 0))}
+  in
+    declare_int_option gdopt
+
 let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
-    
+
 let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 		      
 type external_env=
@@ -94,3 +109,19 @@ TACTIC EXTEND gintuition
   [ "gintuition" tactic_opt(t) ] ->
      [ gen_ground_tac false (option_map eval_tactic t) Void ]
 END
+
+
+let default_declarative_automation gls = 
+  tclORELSE 
+    (Cctac.congruence_tac !congruence_depth []) 
+    (gen_ground_tac true 
+       (Some (tclTHEN
+		default_solver
+		(Cctac.congruence_tac !congruence_depth [])))
+       Void) gls
+
+
+
+let () = 
+  Decl_proof_instr.register_automation_tac default_declarative_automation
+
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 2877c19db9..ce775e0bee 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -72,10 +72,11 @@ let  rec mkevarmap_from_listex lex =
 		  let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in
 		  let _ = prstr "OF TYPE: " in
 		  let _ = prconstr typ in*)
-		  let info ={
+		  let info = {
 			 evar_concl = typ;
 			 evar_hyps = empty_named_context_val;
-			 evar_body = Evar_empty} in
+			 evar_body = Evar_empty;
+		         evar_extra = None} in
 		  Evd.add (mkevarmap_from_listex lex') ex info
 
 let mkEq typ c1 c2 = 
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index ce2ee1e7da..bec24af1be 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -156,16 +156,16 @@ let seq_to_lnhyp sign sign' cl =
 
 let rule_is_complex r =
    match r with
-      Tactic (TacArg (Tacexp t),_) -> true  
-   |  Tactic (TacAtom (_,TacAuto _), _) -> true
-   |  Tactic (TacAtom (_,TacSymmetry _), _) -> true 
+       Nested (Tactic 
+		 (TacArg (Tacexp _)
+		 |TacAtom (_,(TacAuto _|TacSymmetry _))),_) -> true
    |_ -> false
 ;;
 
 let rule_to_ntactic r =
    let rt =
      (match r with
-       Tactic (t,_) -> t
+       Nested(Tactic t,_) -> t
      | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h)
      | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in
    if rule_is_complex r
@@ -234,17 +234,17 @@ let  to_nproof sigma osign pf =
               (List.map (fun x -> (to_nproof_rec sigma sign x).t_proof)
 		 spfl) in
 	  (match r with
-	    Tactic (TacAtom (_, TacAuto _),_) ->
-	      if spfl=[]
-	      then
-	      	{t_info="to_prove";
-	    	  t_goal= {newhyp=[];
-			    t_concl=concl ntree;
-			    t_full_concl=ntree.t_goal.t_full_concl;
-			    t_full_env=ntree.t_goal.t_full_env};
-		  t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])}
-	      else ntree
-	  | _ -> ntree))
+	       Nested(Tactic (TacAtom (_, TacAuto _)),_) ->
+		 if spfl=[]
+		 then
+	      	   {t_info="to_prove";
+	    	    t_goal= {newhyp=[];
+			     t_concl=concl ntree;
+			     t_full_concl=ntree.t_goal.t_full_concl;
+			     t_full_env=ntree.t_goal.t_full_env};
+		    t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])}
+		 else ntree
+	     | _ -> ntree))
       	else
 	  {t_info="to_prove";
 	    t_goal=(seq_to_lnhyp oldsign nsign cl);
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 88a9014eec..292a428739 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1641,6 +1641,15 @@ let rec xlate_vernac =
 	CT_solve (CT_int n, xlate_tactic tac,
 		  if b then CT_dotdot
                   else CT_coerce_NONE_to_DOTDOT_OPT CT_none)
+
+(* MMode *)
+
+    | (VernacDeclProof | VernacReturn | VernacProofInstr _) -> 
+	anomaly "No MMode in CTcoq"
+
+
+(* /MMode *)
+
     | VernacFocus nopt -> CT_focus (xlate_int_opt nopt)
     | VernacUnfocus -> CT_unfocus
     |VernacExtend("Extraction", [f;l]) ->
@@ -1784,6 +1793,7 @@ let rec xlate_vernac =
   | VernacShow ShowExistentials -> CT_show_existentials
   | VernacShow ShowScript -> CT_show_script
   | VernacShow(ShowMatch _) -> xlate_error "TODO: VernacShow(ShowMatch _)"
+  | VernacShow(ShowThesis) -> xlate_error "TODO: VernacShow(ShowThesis _)"
   | VernacGo arg -> CT_go (xlate_locn arg)
   | VernacShow (ExplainProof l) -> CT_explain_proof (nums_to_int_list l)
   | VernacShow (ExplainTree l) ->
diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml
index 801122476e..b0e6b6ecff 100644
--- a/contrib/rtauto/refl_tauto.ml
+++ b/contrib/rtauto/refl_tauto.ml
@@ -303,7 +303,6 @@ let rtauto_tac gls=
     end in
   let build_start_time=System.get_time () in
   let _ = step_count := 0; node_count := 0 in
-  let nhyps = List.length hyps in
   let main = mkApp (force node_count l_Reflect,
 		    [|build_env gamma;
 		      build_form formula;
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 678b650cc8..92cbf6df52 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -63,21 +63,24 @@ let nf_evar sigma ~preserve =
 (* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *)
 let rec unshare_proof_tree =
  let module PT = Proof_type in
-  function {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = ref} ->
+  function {PT.open_subgoals = status ; 
+	    PT.goal = goal ; 
+	    PT.ref = ref} ->
    let unshared_ref =
     match ref with
        None -> None
      | Some (rule,pfs) ->
         let unshared_rule =
          match rule with
-            PT.Prim prim -> PT.Prim prim
-          | PT.Change_evars -> PT.Change_evars
-          | PT.Tactic (tactic_expr, pf) ->
-             PT.Tactic (tactic_expr, unshare_proof_tree pf)
-        in
+             PT.Nested (cmpd, pf) ->
+               PT.Nested (cmpd, unshare_proof_tree pf)
+	   | other -> other
+	in
          Some (unshared_rule, List.map unshare_proof_tree pfs)
    in
-    {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = unshared_ref}
+    {PT.open_subgoals = status ; 
+     PT.goal = goal ; 
+     PT.ref = unshared_ref}
 ;;
 
 module ProofTreeHash =
@@ -103,7 +106,7 @@ let extract_open_proof sigma pf =
        {PT.ref=Some(PT.Prim _,_)} as pf ->
         L.prim_extractor proof_extractor vl pf
 	  
-     | {PT.ref=Some(PT.Tactic (_,hidden_proof),spfl)} ->
+     | {PT.ref=Some(PT.Nested (_,hidden_proof),spfl)} ->
 	 let sgl,v = Refiner.frontier hidden_proof in
 	 let flat_proof = v spfl in
          ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ;
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 578c1ed2f3..d382ef955c 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -141,7 +141,7 @@ Pp.ppnl (Pp.(++) (Pp.str
               (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
 
      | {PT.goal=goal;
-        PT.ref=Some(PT.Tactic (tactic_expr,hidden_proof),nodes)} ->
+        PT.ref=Some(PT.Nested (PT.Tactic tactic_expr,hidden_proof),nodes)} ->
          (* [hidden_proof] is the proof of the tactic;                     *)
          (* [nodes] are the proof of the subgoals generated by the tactic; *)
          (* [flat_proof] if the proof-tree obtained substituting [nodes]   *)
@@ -194,6 +194,12 @@ Pp.ppnl (Pp.(++) (Pp.str
           (List.fold_left
             (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
 
+     | {PT.ref=Some((PT.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} ->
+         Util.anomaly "Not Implemented" 
+
+     | {PT.ref=Some(PT.Daimon,_)} ->
+         X.xml_empty "Hidden_open_goal" of_attribute
+
      | {PT.ref=None;PT.goal=goal} ->
          X.xml_empty "Open_goal" of_attribute
   in