Adding files for the production of textual explanations as used in pcoq.

dependence files are updated accordingly.

Modifications in other files to cope with a few errors in the translation for
the parser (mostly around records, coercions, and the search-pattern command).


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

1 files changed, 185 insertions, 0 deletions

diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml
new file mode 100644
index 000000000..e3bca2243
--- /dev/null
+++ b/contrib/interface/showproof_ct.ml
@@ -0,0 +1,185 @@
+(*****************************************************************************)
+(*
+   Vers Ctcoq
+*)
+
+open Esyntax
+open Metasyntax
+open Printer
+open Pp
+open Translate
+open Ascent
+open Vtp
+open Xlate
+
+let ct_text x = CT_coerce_ID_to_TEXT (CT_ident x);;
+
+let sps s =
+  ct_text s
+    ;;
+
+
+let sphs s =
+  ct_text s
+    ;;
+
+let spe = sphs "";;
+let spb = sps " ";;
+let spr = sps "Retour chariot pour Show proof";;
+
+let spnb n = 
+   let s = ref "" in
+   for i=1 to n do s:=(!s)^" "; done; sps !s
+;;
+
+
+let rec spclean l =
+  match l with 
+    [] -> []
+   |x::l -> if x=spe then (spclean l) else x::(spclean l)
+;;
+
+
+let spnb n = 
+   let s = ref "" in
+   for i=1 to n do s:=(!s)^" "; done; sps !s
+;;
+
+let ct_FORMULA_constr = Hashtbl.create 50;;
+
+let stde()  = (Global.env())
+
+;;
+
+let spt t =
+   let f = (translate_constr (stde()) t) in
+   Hashtbl.add ct_FORMULA_constr f t;
+   CT_text_formula f
+;;
+
+
+
+let root_of_text_proof t=
+  CT_text_op [ct_text "root_of_text_proof";
+              t]
+    ;;
+    
+let spshrink info t =
+  CT_text_op [ct_text "shrink";
+	      CT_text_op [ct_text info;
+                          t]]
+;;
+			 
+let spuselemma intro x y =
+  CT_text_op [ct_text "uselemma";
+              ct_text intro;
+	      x;y]
+;;
+
+let sptoprove p t =
+  CT_text_op [ct_text "to_prove";
+	      CT_text_path p;
+              ct_text "goal";
+	      (spt t)]
+;;
+let sphyp p h t =
+  CT_text_op [ct_text "hyp";
+	      CT_text_path p;
+	      ct_text h;
+              (spt t)]
+;;
+let sphypt p h t =
+  CT_text_op [ct_text "hyp_with_type";
+	      CT_text_path p;
+	      ct_text h;
+              (spt t)]
+;;
+
+let spwithtac x t =
+    CT_text_op [ct_text "with_tactic";
+                ct_text t;
+                x]
+;;
+
+
+let spv l =
+   let l= spclean l in
+   CT_text_v l
+;;
+     
+let sph l =
+   let l= spclean l in
+   CT_text_h l
+;;
+
+
+let sphv l =
+   let l= spclean l in
+   CT_text_hv l
+;;
+
+let rec prlist_with_sep f g l =
+    match l with 
+      [] -> hOV 0 [< >]
+     |x::l1 -> hOV 0 [< (g x); (f ()); (prlist_with_sep f g l1)>]
+;;
+   
+let rec sp_print x = 
+   match x with
+     CT_coerce_ID_to_TEXT (CT_ident s)
+     -> (match s with
+       "\n" -> [< 'fNL >]
+     | "Retour chariot pour Show proof" -> [< 'fNL >]
+     |_ -> [< 'sTR s >])
+   | CT_text_formula  f -> [< prterm (Hashtbl.find ct_FORMULA_constr f) >]
+  |  CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove");
+	      CT_text_path (CT_signed_int_list p);
+              CT_coerce_ID_to_TEXT (CT_ident "goal");
+	      g] ->
+      let p=(List.map (fun y -> match y with
+	                 (CT_coerce_INT_to_SIGNED_INT
+			      (CT_int x)) -> x
+		       | _ -> raise (Failure "sp_print")) p) in
+      h 0 [<  'sTR "<b>"; sp_print g; 'sTR "</b>">]
+ |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "uselemma");
+              CT_coerce_ID_to_TEXT (CT_ident intro);
+	      l;g] ->
+      h 0 [< 'sTR ("<i>("^intro^" "); sp_print l; 'sTR ")</i>"; sp_print g>]
+ |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "hyp");
+	      CT_text_path (CT_signed_int_list p);
+	      CT_coerce_ID_to_TEXT (CT_ident hyp);
+              g]  ->
+      let p=(List.map (fun y -> match y with
+	                  (CT_coerce_INT_to_SIGNED_INT
+			      (CT_int x)) -> x
+		       | _ -> raise (Failure "sp_print")) p) in
+            h 0 [< 'sTR hyp>]
+
+  |   CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "hyp_with_type");
+	      CT_text_path (CT_signed_int_list p);
+	      CT_coerce_ID_to_TEXT (CT_ident hyp);
+              g]  ->
+      let p=(List.map (fun y -> match y with
+                         (CT_coerce_INT_to_SIGNED_INT
+			      (CT_int x)) -> x
+		       | _ -> raise (Failure "sp_print")) p) in
+      h 0 [< sp_print g; 'sPC; 'sTR "<i>("; 'sTR hyp;'sTR ")</i>">]   
+
+  | CT_text_h l ->
+      h 0 [< prlist_with_sep (fun () -> [< >])
+		(fun y -> sp_print y) l>]
+  | CT_text_v l ->
+      v 0 [< prlist_with_sep (fun () -> [< >])
+		(fun y -> sp_print y) l>]
+  | CT_text_hv l ->
+      h 0 [< prlist_with_sep (fun () -> [<>])
+		(fun y -> sp_print y) l>]
+  | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "shrink");
+	      CT_text_op [CT_coerce_ID_to_TEXT (CT_ident info); t]]  ->
+                   h 0 [< 'sTR ("("^info^": "); sp_print t ;'sTR ")" >]
+  | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "root_of_text_proof");
+              t]->
+                    sp_print t 
+  | _ -> [< 'sTR "..." >]
+;;
+