Printer

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

5 files changed, 133 insertions, 3 deletions

diff --git a/dev/base_db b/dev/base_db
index 7f1822961..b540aed6c 100644
--- a/dev/base_db
+++ b/dev/base_db
@@ -2,5 +2,5 @@ load_printer "gramlib.cma"
 load_printer "top_printers.cmo"
 install_printer Top_printers.prid
 install_printer Top_printers.prsp
-install_printer Top_printers.constr_display
+install_printer Top_printers.print_pure_constr
 
diff --git a/dev/base_include b/dev/base_include
index b73f45206..7e233d171 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -30,6 +30,7 @@ Topdirs.dir_directory Coq_config.camlp4lib;;
 
 #install_printer  (* identifier *) prid;;
 #install_printer  (* section_path *)  prsp;;
+#install_printer  (* constr *)  print_pure_constr;;
 
 (* parsing of terms *)
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index d650ec03f..95c85866d 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -137,6 +137,124 @@ let constr_display csr =
   in
     mSG [<'sTR (term_display csr);'fNL>]
 
+open Format;;
+
+let print_pure_constr csr =
+  let rec term_display c = match kind_of_term c with
+  | IsRel n -> print_string "#"; print_int n
+  | IsMeta n -> print_string "Meta("; print_int n; print_string ")"
+  | IsVar id -> print_string (string_of_id id)
+  | IsSort s -> sort_display s
+  | IsXtra s -> print_string ("Xtra("^s^")")
+  | IsCast (c,t) -> open_hovbox 1;
+      print_string "("; (term_display c); print_cut();
+      print_string "::"; (term_display t); print_string ")"; close_box()
+  | IsProd (Name(id),t,c) ->
+      open_hovbox 1;
+      print_string"("; print_string (string_of_id id); 
+      print_string ":"; box_display t; 
+      print_string ")"; print_cut(); 
+      box_display c; close_box()
+  | IsProd (Anonymous,t,c) ->
+      print_string"("; box_display t; print_cut(); print_string "->";
+      box_display c; print_string ")"; 
+  | IsLambda (na,t,c) ->
+      print_string "["; name_display na;
+      print_string ":"; box_display t; print_string "]";
+      print_cut(); box_display c; 
+  | IsLetIn (na,b,t,c) ->
+      print_string "["; name_display na; print_string "="; 
+      box_display b; print_cut();
+      print_string ":"; box_display t; print_string "]";
+      print_cut(); box_display c; 
+  | IsApp (c,l) -> 
+      print_string "("; 
+      box_display c; 
+      Array.iter (fun x -> print_space (); box_display x) l;
+      print_string ")"
+  | IsEvar (e,l) -> print_string "Evar#"; print_int e; print_string "{";
+      Array.iter (fun x -> print_space (); box_display x) l;
+      print_string"}"
+  | IsConst (c,l) -> print_string "Cons(";
+      sp_display c;
+      print_string "){";
+      Array.iter (fun x -> print_space (); box_display x) l;
+      print_string"}"
+  | IsMutInd ((sp,i),l) ->
+      print_string "Ind(";
+      sp_display sp;
+      print_string ","; print_int i;
+      print_string "){";
+      Array.iter (fun x -> print_space (); box_display x) l;
+      print_string"}"
+  | IsMutConstruct (((sp,i),j),l) ->
+      print_string "Constr(";
+      sp_display sp;
+      print_string ",";
+      print_int i; print_string ","; print_int j; print_string ")";
+      Array.iter (fun x -> print_space (); box_display x) l;
+  | IsMutCase (ci,p,c,bl) ->
+      open_vbox 0;
+      print_string "<"; box_display p; print_string ">";
+      print_cut(); print_string "Case";
+      print_space(); box_display c; print_space (); print_string "of";
+      open_vbox 0;
+      Array.iter (fun x ->  print_cut();  box_display x) bl;
+      close_box();
+      print_cut(); 
+      print_string "end"; 
+      close_box()
+  | IsFix ((t,i),(tl,lna,bl)) ->
+      print_string "Fix("; print_int i; print_string ")"; 
+      print_cut();
+      open_vbox 0;
+      let rec print_fix lna k = 
+	match lna with [] ->  ()
+	  | nf::ln ->  open_vbox 0;
+	name_display nf; print_string "/"; 
+	print_int t.(k); print_cut(); print_string ":";
+	box_display tl.(k) ; print_cut(); print_string ":=";
+	box_display bl.(k); close_box ();
+	print_cut();
+	print_fix ln (k+1)
+      in print_string"{"; print_fix lna 0; print_string"}"
+  | IsCoFix(i,(tl,lna,bl)) ->
+      print_string "CoFix("; print_int i; print_string ")"; 
+      print_cut();
+      open_vbox 0;
+      let rec print_fix lna k = 
+	match lna with [] ->  ()
+	  | nf::ln ->  open_vbox 1;
+	name_display nf;  print_cut(); print_string ":";
+	box_display tl.(k) ; print_cut(); print_string ":=";
+	box_display bl.(k); close_box ();
+	print_cut();
+	print_fix ln (k+1)
+      in print_string"{"; print_fix lna 0; print_string"}"
+
+  and box_display c = open_hovbox 1; term_display c; close_box()
+
+  and sort_display = function
+    | Prop(Pos) -> print_string "Set"
+    | Prop(Null) -> print_string "Prop"
+    | Type u -> open_hbox();
+	print_string "Type("; pP (pr_uni u); print_string ")"; close_box()
+
+  and name_display = function
+    | Name id -> print_string (string_of_id id)
+    | Anonymous -> print_string "_"
+(* Remove the top names for library and Scratch to avoid long names *)
+  and sp_display sp = let ls = 
+    match (dirpath sp) with 
+        ("Scratch"::l)-> l
+      | ("Coq"::_::l) -> l 
+      | l             -> l
+  in  List.iter (fun x -> print_string x; print_string ".") ls;
+      print_string (string_of_id  (basename sp))
+
+  in
+     box_display csr; print_newline()
+
 let _ =
   Vernacentries.add "PrintConstr"
     (function
@@ -145,3 +263,12 @@ let _ =
               let (evmap,sign) = Command.get_current_context () in
   	      constr_display (Astterm.interp_constr evmap sign c))
        | _ -> bad_vernac_args "PrintConstr")
+
+let _ =
+  Vernacentries.add "PrintPureConstr"
+    (function
+       | [VARG_CONSTR c] -> 
+	   (fun () ->
+              let (evmap,sign) = Command.get_current_context () in
+  	      print_pure_constr (Astterm.interp_constr evmap sign c))
+       | _ -> bad_vernac_args "PrintPureConstr")
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index fbf9b3477..a3051fea8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -633,6 +633,7 @@ let one_step_reduce env sigma c =
              | None      -> error "Not reducible 1"
              | Some (a,rest) -> (subst1 a c, rest))
       | IsApp (f,cl) -> redrec (f, append_stack cl largs)
+      | IsLetIn (_,f,_,cl) -> (subst1 f cl,largs)
       | IsMutCase (ci,p,c,lf) ->
           (try
 	     (special_red_case env (whd_betadeltaiota_state env sigma)
@@ -681,3 +682,4 @@ let reduce_to_mind env sigma t =
 let reduce_to_ind env sigma t =
   let ((ind_sp,_),redt,c) = reduce_to_mind env sigma t in 
   (Declare.path_of_inductive_path ind_sp, redt, c)
+
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b90f7e493..23528e3f4 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -358,8 +358,8 @@ let close_section _ s =
   Global.pop_named_decls ids;
   Summary.unfreeze_lost_summaries fs;
   let mc = segment_contents decls in
-  add_anonymous_leaf (in_end_section (sec_sp,mc));
-  List.iter process_operation (List.rev ops)
+  add_anonymous_leaf (in_end_section (sec_sp,mc)); 
+  List.iter process_operation (List.rev ops) 
 
 let save_module_to s f =
   Library.save_module_to segment_contents s f