rewiring Czar printers that were disabled

Backported from trunk.

4 files changed, 128 insertions, 99 deletions

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 7467604a60..3c4cacbc54 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -46,23 +46,23 @@ type ('constr,'tac) casee =
     Real of 'constr
   | Virtual of ('constr statement,'constr,'tac) cut
 
-type ('hyp,'constr,'pat,'tac) bare_proof_instr =
-  | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr
-  | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr
-  | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr
+type ('var,'constr,'pat,'tac) bare_proof_instr =
+  | Pthen of ('var,'constr,'pat,'tac) bare_proof_instr
+  | Pthus of ('var,'constr,'pat,'tac) bare_proof_instr
+  | Phence of ('var,'constr,'pat,'tac) bare_proof_instr
   | Pcut of ('constr or_thesis statement,'constr,'tac) cut
   | Prew of side * ('constr statement,'constr,'tac) cut
-  | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
-  | Passume of ('hyp,'constr) hyp list
-  | Plet of ('hyp,'constr) hyp list
-  | Pgiven of ('hyp,'constr) hyp list
-  | Pconsider of 'constr*('hyp,'constr) hyp list
+  | Psuffices of ((('var,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
+  | Passume of ('var,'constr) hyp list
+  | Plet of ('var,'constr) hyp list
+  | Pgiven of ('var,'constr) hyp list
+  | Pconsider of 'constr*('var,'constr) hyp list
   | Pclaim of 'constr statement
   | Pfocus of 'constr statement
-  | Pdefine of Id.t * 'hyp list * 'constr
+  | Pdefine of Id.t * 'var list * 'constr
   | Pcast of Id.t or_thesis * 'constr
-  | Psuppose of ('hyp,'constr) hyp list
-  | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
+  | Psuppose of ('var,'constr) hyp list
+  | Pcase of 'var list*'pat*(('var,'constr or_thesis) hyp list)
   | Ptake of 'constr list
   | Pper of elim_type * ('constr,'tac) casee
   | Pend of block_type
@@ -70,19 +70,19 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr =
 
 type emphasis = int
 
-type ('hyp,'constr,'pat,'tac) gen_proof_instr=
+type ('var,'constr,'pat,'tac) gen_proof_instr=
     {emph: emphasis;
-     instr: ('hyp,'constr,'pat,'tac) bare_proof_instr }
+     instr: ('var,'constr,'pat,'tac) bare_proof_instr }
 
 
 type raw_proof_instr =
-    ((Id.t*(Constrexpr.constr_expr option)) Loc.located,
+    ((Id.t * (Constrexpr.constr_expr option)) Loc.located,
      Constrexpr.constr_expr,
      Constrexpr.cases_pattern_expr,
      raw_tactic_expr) gen_proof_instr
 
 type glob_proof_instr =
-    ((Id.t*(Tacexpr.glob_constr_and_expr option)) Loc.located,
+    ((Id.t * (Tacexpr.glob_constr_and_expr option)) Loc.located,
      Tacexpr.glob_constr_and_expr,
      Constrexpr.cases_pattern_expr,
      Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index acec8ba4e8..2bd88d5aea 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -19,6 +19,7 @@ open Tok (* necessary for camlp4 *)
 
 open Pcoq.Constr
 open Pcoq.Tactic
+open Ppdecl_proof
 
 let pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
@@ -43,15 +44,6 @@ let pr_open_subgoals () =
   pr_subgoals close_cmd sigma goals
 *)
 
-let pr_raw_proof_instr _ _ _ instr =
-  Errors.anomaly (Pp.str "Cannot print a proof_instr")
-    (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller
-                     dans cette direction
-       Ppdecl_proof.pr_proof_instr (Global.env()) instr
-    *)
-let pr_proof_instr _ _ _ instr = Empty.abort instr
-let pr_glob_proof_instr _ _ _ instr = Empty.abort instr
-
 let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
   Decl_interp.interp_proof_instr 
     (Decl_mode.get_info sigma gl)
@@ -87,7 +79,7 @@ let vernac_proof_instr instr =
 (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *)
 
 (* Only declared at raw level, because only used in vernac commands. *)
-let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type =
+let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
   Genarg.make0 None "proof_instr"
 
 (* We create a new parser entry [proof_mode]. The Declarative proof mode
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 27308666d2..b3198dbf24 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -12,41 +12,35 @@ open Decl_expr
 open Names
 open Nameops
 
-let pr_constr = Printer.pr_constr_env
-let pr_tac = Pptactic.pr_glob_tactic
-let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr
-
 let pr_label = function
     Anonymous -> mt ()
   | Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
 
-let pr_constr env c = pr_constr env Evd.empty c
-
-let pr_justification_items env = function
+let pr_justification_items pr_constr = function
     Some [] -> mt ()
   | Some (_::_ as l) ->
       spc () ++ str "by" ++ spc () ++
-	prlist_with_sep (fun () -> str ",") (pr_constr env) l
+	prlist_with_sep (fun () -> str ",") pr_constr l
   | None -> spc () ++ str "by *"
 
-let pr_justification_method env = function
+let pr_justification_method pr_tac = function
     None -> mt ()
   | Some tac ->
-      spc () ++ str "using" ++ spc () ++ pr_tac env tac
+      spc () ++ str "using" ++ spc () ++ pr_tac tac
 
-let pr_statement pr_it env st =
-  pr_label st.st_label ++ pr_it env st.st_it
+let pr_statement pr_constr st =
+  pr_label st.st_label ++ pr_constr st.st_it
 
-let pr_or_thesis pr_this env = function
+let pr_or_thesis pr_this = function
     Thesis Plain -> str "thesis"
   | Thesis (For id) ->
       str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
-  | This c -> pr_this env c
+  | This c -> pr_this c
 
-let pr_cut pr_it env c =
-  hov 1 (pr_it env c.cut_stat) ++
-    pr_justification_items env c.cut_by ++
-    pr_justification_method env c.cut_using
+let pr_cut pr_constr pr_tac pr_it c =
+  hov 1 (pr_it c.cut_stat) ++
+    pr_justification_items pr_constr c.cut_by ++
+    pr_justification_method pr_tac c.cut_using
 
 let type_or_thesis = function
     Thesis _ -> Term.mkProp
@@ -54,128 +48,127 @@ let type_or_thesis = function
 
 let _I x = x
 
-let rec print_hyps pconstr gtyp env sep _be _have hyps =
+let rec pr_hyps pr_var pr_constr gtyp sep _be _have hyps =
   let pr_sep = if sep then str "and" ++ spc () else mt () in
     match hyps with
 	(Hvar _ ::_) as rest ->
 	  spc () ++ pr_sep ++ str _have ++
-	    print_vars pconstr gtyp env false _be _have rest
+	    pr_vars pr_var pr_constr gtyp false _be _have rest
       | Hprop st :: rest ->
 	  begin
-	    let nenv =
-	      match st.st_label with
-		  Anonymous -> env
-		| Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
-	      spc() ++ pr_sep ++ pr_statement pconstr env st ++
-		print_hyps pconstr gtyp nenv true _be _have rest
+	(* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) 
+	      spc() ++ pr_sep ++ pr_statement pr_constr st ++
+		pr_hyps pr_var pr_constr gtyp true _be _have rest
 	  end
       | [] -> mt ()
 
-and print_vars pconstr gtyp env sep _be _have vars =
+and pr_vars pr_var pr_constr gtyp sep _be _have vars =
   match vars with
     Hvar st :: rest ->
       begin
-	let nenv =
-	  match st.st_label with
-	      Anonymous -> anomaly (Pp.str "anonymous variable")
-	    | Name id -> Environ.push_named (id,None,st.st_it) env in
+	(* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) 
 	let pr_sep = if sep then pr_comma () else mt () in
 		spc() ++ pr_sep ++
-		   pr_statement pr_constr env st ++
-		  print_vars pconstr gtyp nenv true _be _have rest
+		  pr_var st ++
+		  pr_vars pr_var pr_constr gtyp true _be _have rest
       end
    | (Hprop _ :: _) as rest ->
       let _st =  if _be then
 	str "be such that"
       else
 	str "such that" in
-	spc() ++ _st ++  print_hyps pconstr gtyp env false _be _have rest
+	spc() ++ _st ++  pr_hyps pr_var pr_constr gtyp false _be _have rest
   | [] -> mt ()
 
-let pr_suffices_clause env (hyps,c) =
-    print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++
-       str "to show" ++ spc () ++ pr_or_thesis pr_constr env c
+let pr_suffices_clause pr_var pr_constr (hyps,c) =
+    pr_hyps pr_var pr_constr _I false false "to have" hyps ++ spc () ++
+       str "to show" ++ spc () ++ pr_or_thesis pr_constr c
 
 let pr_elim_type = function
     ET_Case_analysis -> str "cases"
   | ET_Induction -> str "induction"
 
-let pr_casee env =function
-    Real c -> str "on" ++ spc () ++ pr_constr env c
-  | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut
+let pr_block_type = function
+    B_elim et -> pr_elim_type et
+  | B_proof -> str "proof"
+  | B_claim -> str "claim"
+  | B_focus -> str "focus"
+
+let pr_casee pr_constr pr_tac =function
+    Real c -> str "on" ++ spc () ++ pr_constr c
+  | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) cut
 
 let pr_side = function
     Lhs -> str "=~"
   | Rhs -> str "~="
 
-let rec pr_bare_proof_instr _then _thus env = function
+let rec pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then _thus = function
   | Pescape -> str "escape"
-  | Pthen i -> pr_bare_proof_instr true _thus env i
-  | Pthus i -> pr_bare_proof_instr _then true env i
-  | Phence i -> pr_bare_proof_instr true true env i
+  | Pthen i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac  true _thus i
+  | Pthus i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac  _then true i
+  | Phence i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true true i
   | Pcut c ->
       begin
 	match _then,_thus with
 	    false,false -> str "have" ++ spc () ++
-	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
 	  | false,true  -> str "thus" ++ spc () ++
-	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
 	  | true,false  -> str "then" ++ spc () ++
-	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
 	  | true,true   -> str "hence" ++ spc () ++
-	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	      pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
       end
   | Psuffices c ->
-      str "suffices" ++  pr_cut pr_suffices_clause env c
+      str "suffices" ++  pr_cut pr_constr pr_tac (pr_suffices_clause pr_var pr_constr) c
   | Prew (sid,c) ->
       (if _thus then str "thus" else str "    ") ++ spc () ++
-	pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c
+	pr_side sid ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) c
   | Passume hyps ->
-      str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps
+      str "assume" ++ pr_hyps pr_var pr_constr _I false false "we have" hyps
   | Plet hyps ->
-      str "let" ++ print_vars pr_constr _I env false true "let" hyps
+      str "let" ++ pr_vars pr_var pr_constr _I false true "let" hyps
   | Pclaim st ->
-      str "claim" ++ spc () ++ pr_statement pr_constr env st
+      str "claim" ++ spc () ++ pr_statement pr_constr st
   | Pfocus st ->
-      str "focus on" ++ spc () ++ pr_statement pr_constr env st
+      str "focus on" ++ spc () ++ pr_statement pr_constr st
   | Pconsider (id,hyps) ->
-      str "consider" ++ print_vars pr_constr _I env false false "consider" hyps
-      ++ spc () ++ str "from " ++ pr_constr env id
+      str "consider" ++ pr_vars pr_var pr_constr _I false false "consider" hyps
+      ++ spc () ++ str "from " ++ pr_constr id
   | Pgiven hyps ->
-      str "given" ++ print_vars pr_constr _I env false false "given" hyps
+      str "given" ++ pr_vars pr_var pr_constr _I false false "given" hyps
   | Ptake witl ->
       str "take" ++ spc () ++
-	prlist_with_sep pr_comma (pr_constr env) witl
+	prlist_with_sep pr_comma pr_constr witl
   | Pdefine (id,args,body) ->
       str "define" ++ spc () ++ pr_id id ++ spc () ++
 	prlist_with_sep spc
 	(fun st -> str "(" ++
-	   pr_statement pr_constr env st ++ str ")") args ++ spc () ++
-	str "as" ++ (pr_constr env body)
+	   pr_var st ++ str ")") args ++ spc () ++
+	str "as" ++ (pr_constr body)
   | Pcast (id,typ) ->
       str "reconsider" ++ spc () ++
-	pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++
-	str "as" ++ spc () ++ (pr_constr env typ)
+	pr_or_thesis pr_id id ++ spc () ++
+	str "as" ++ spc () ++ (pr_constr typ)
   | Psuppose hyps ->
       str "suppose" ++
-	print_hyps pr_constr _I env false false "we have" hyps
+	pr_hyps pr_var pr_constr _I false false "we have" hyps 
   | Pcase (params,pat,hyps) ->
       str "suppose it is" ++ spc () ++ pr_pat pat ++
 	(if params = [] then mt () else
 	   (spc () ++ str "with" ++ spc () ++
 	      prlist_with_sep spc
 	      (fun st -> str "(" ++
-		 pr_statement pr_constr env st ++ str ")") params ++ spc ()))
+		 pr_var st ++ str ")") params ++ spc ()))
       ++
 	(if hyps = [] then mt () else
 	   (spc () ++ str "and" ++
-	      print_hyps (pr_or_thesis pr_constr) type_or_thesis
-	      env false false "we have" hyps))
-  | Pper (et,c) ->
+	      pr_hyps pr_var (pr_or_thesis pr_constr) type_or_thesis
+	      false false "we have" hyps)) 
+  | Pper (et,c) -> 
       str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
-      pr_casee env c
-  | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
-  | _ -> anomaly (Pp.str "unprintable instruction")
+	pr_casee pr_constr pr_tac c  
+  | Pend blk -> str "end" ++ spc () ++ pr_block_type blk
 
 let pr_emph = function
     0 -> str "    "
@@ -184,7 +177,39 @@ let pr_emph = function
   | 3 -> str "*** "
   | _ -> anomaly (Pp.str "unknown emphasis")
 
-let pr_proof_instr env instr =
+let pr_gen_proof_instr pr_var pr_constr pr_pat pr_tac instr =
   pr_emph instr.emph ++ spc () ++
-    pr_bare_proof_instr false false env instr.instr
+    pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac false false instr.instr
+
+
+let pr_raw_proof_instr pconstr1 pconstr2 ptac (instr : raw_proof_instr) =
+   pr_gen_proof_instr
+     (fun (_,(id,otyp)) -> 
+       match otyp with
+	 None -> pr_id id
+       | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")"
+     )
+     pconstr2
+     Ppconstr.pr_cases_pattern_expr
+     (ptac Pptactic.ltop)
+     instr
+
+let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) =
+    pr_gen_proof_instr
+      (fun (_,(id,otyp)) -> 
+	match otyp with
+	  None -> pr_id id
+	| Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")")
+     pconstr2
+     Ppconstr.pr_cases_pattern_expr
+     (ptac Pptactic.ltop)
+     instr
+
+let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) =
+  pr_gen_proof_instr
+    (fun st -> pr_statement pconstr1 st)
+    pconstr2
+    (fun mpat -> Ppconstr.pr_cases_pattern_expr mpat.pat_expr)
+    (ptac Pptactic.ltop)
+    instr
 
diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli
index fd6fb66376..678fc07688 100644
--- a/plugins/decl_mode/ppdecl_proof.mli
+++ b/plugins/decl_mode/ppdecl_proof.mli
@@ -1,2 +1,14 @@
 
-val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds
+open Decl_expr
+open Pptactic
+
+val pr_gen_proof_instr : 
+  ('var -> Pp.std_ppcmds) ->
+  ('constr -> Pp.std_ppcmds) ->
+  ('pat -> Pp.std_ppcmds) ->
+  ('tac -> Pp.std_ppcmds) ->  
+  ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds
+
+val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer
+val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer
+val pr_proof_instr : proof_instr extra_genarg_printer