module Pretty (partiellement)

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

3 files changed, 718 insertions, 0 deletions

diff --git a/parsing/pretty.ml b/parsing/pretty.ml
new file mode 100644
index 000000000..59d93aaa0
--- /dev/null
+++ b/parsing/pretty.ml
@@ -0,0 +1,664 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Inductive
+open Sign
+open Printer
+open Reduction
+open Impargs
+open Libobject
+open Printer
+
+let print_basename sp =
+  let (_,id,k) = repr_path sp in
+  try 
+    if sp = Nametab.sp_of_id k id then 
+      string_of_id id
+    else 
+      (string_of_id id)^"."^(string_of_kind k)
+  with Not_found -> 
+    warning "Undeclared constants in print_name";
+    string_of_path sp
+
+let print_basename_mind sp mindid =
+  let (_,id,k) = repr_path sp in
+  try 
+    if sp = Nametab.sp_of_id k id then  
+      string_of_id mindid
+    else 
+      (string_of_id mindid)^"."^(string_of_kind k)
+  with Not_found ->
+    warning "Undeclared constants in print_name";
+    string_of_path_mind sp mindid
+
+let print_closed_sections = ref false
+
+let print_typed_value_in_sign sign (trm,typ) =
+  [< term0 (gLOB sign) trm ; 'fNL ;
+     'sTR "     : "; term0 (gLOB sign) typ ; 'fNL >]
+
+let print_typed_value = print_typed_value_in_sign nil_sign
+			  		  
+let print_recipe = function
+  | Some c -> prterm c
+  | None -> [< 'sTR"<uncookable>" >]
+
+let fprint_recipe = function
+  | Some c -> fprterm c
+  | None -> [< 'sTR"<uncookable>" >]
+
+let print_typed_recipe (val_0,typ) =
+  [< print_recipe val_0 ; 'fNL ; 'sTR "     : "; prtype typ ; 'fNL >]
+
+let print_impl_args = function
+  | []  -> [<>]
+  | [i] -> [< 'sTR"Position ["; 'iNT i; 'sTR"] is implicit" >]
+  | l   -> 
+      [< 'sTR"Positions ["; 
+         prlist_with_sep (fun () -> [< 'sTR";" >]) (fun i -> [< 'iNT i >]) l;
+         'sTR"] are implicit" >]
+
+(* To be improved; the type should be used to provide the types in the
+   abstractions. This should be done recursively inside prterm, so that
+   the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
+   synthesizes the type nat of the abstraction on u *)
+
+let print_var name typ =
+  [< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >]
+
+let print_env pk = 
+  let pterminenv = if pk = FW then fterm0 else term0 in
+  let pr_binder env (na,c) =
+    match na with
+      | Name id as name ->
+          let pc = pterminenv env c in [< print_id id; 'sTR":"; pc >]
+      | Anonymous -> anomaly "Anonymous variables in inductives" 
+  in
+  let rec prec env = function
+    | [] -> [<>] 
+    | [b] -> pr_binder env b
+    | b::rest ->
+        let pb = pr_binder env b in
+        let penvtl = prec (add_rel b env) rest in
+        [< pb; 'sTR";"; 'sPC; penvtl >]
+  in 
+  prec (gLOB nil_sign)
+
+let assumptions_for_print lna =
+  ENVIRON(([],[]),List.map (fun na -> (na,())) lna)
+
+let print_constructors_with_sep pk fsep mip = 
+  let pterm,pterminenv =
+    if pk = FW then (fprterm,fterm0) else (prterm,term0) in
+  let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
+  let ass_name = assumptions_for_print lna in
+  let lidC = Array.to_list 
+               (array_map2 (fun id c -> (id,c)) mip.mind_consnames lC) in
+  let prass (id,c) =
+    let pc = pterminenv ass_name c in [< print_id id; 'sTR " : "; pc >]
+  in
+  prlist_with_sep fsep prass lidC
+
+let implicit_args_id id l = 
+  if l = [] then 
+    [<>]
+  else 
+    [< 'sTR"For "; print_id id; 'sTR": "; print_impl_args l ; 'fNL >]
+
+let implicit_args_msg sp mipv = 
+  [< prvecti
+       (fun i mip -> 
+	  let imps = inductive_implicits (sp,i) in
+          [< (implicit_args_id mip.mind_typename (list_of_implicits imps));
+             prvecti 
+	       (fun j idc ->
+		  let imps = constructor_implicits ((sp,i),j) in
+                  (implicit_args_id idc (list_of_implicits imps)))
+               mip.mind_consnames 
+          >])
+       mipv >]
+
+let print_mutual pk sp mib = 
+  let pterm,pterminenv =
+    if pk = FW then (fprterm,fterm0) else (prterm,term0) in
+  let env = Global.unsafe_env () in
+  let evd = Evd.empty in
+  let {mind_packets=mipv; mind_nparams=nparams} = mib in 
+  let (lpars,_) = decomp_n_prod env evd nparams mipv.(0).mind_arity.body in
+  let lparsname = List.map fst lpars in
+  let lparsprint = assumptions_for_print lparsname in
+  let prass ass_name (id,c) =
+    let pc = pterminenv ass_name c in [< print_id id; 'sTR " : "; pc >] 
+  in
+  let print_constructors mip = 
+    let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
+    let ass_name = assumptions_for_print (lparsname@lna) in
+    let lidC =
+      Array.to_list 
+        (array_map2 (fun id c -> (id,snd (decomp_n_prod env evd nparams c)))
+           mip.mind_consnames lC) in
+    let plidC = prlist_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >])
+                  (prass ass_name) lidC in
+    (hV 0 [< 'sTR "  "; plidC >]) 
+  in
+  let print_oneind mip = 
+    let (_,arity) = decomp_n_prod env evd nparams mip.mind_arity.body in
+      (hOV 0
+         [< (hOV 0
+	       [< print_id mip.mind_typename ; 'bRK(1,2);
+		  if nparams = 0 then 
+		    [<>] 
+		  else
+		    [< 'sTR "["; print_env pk (List.rev lpars); 
+		       'sTR "]"; 'bRK(1,2) >]; 
+	          'sTR ": "; pterminenv lparsprint arity; 'sTR " :=" >]);
+            'bRK(1,2); print_constructors mip >]) 
+  in 
+  let mip = mipv.(0) in
+  (* Case one [co]inductive *)
+  if Array.length mipv = 1 then 
+    let (_,arity) = decomp_n_prod env evd nparams mip.mind_arity.body in 
+    let sfinite = if mip.mind_finite then "Inductive " else "CoInductive " in
+    (hOV 0 [< 'sTR sfinite ; print_id mip.mind_typename ;
+              if nparams = 0 then 
+		[<>] 
+              else 
+		[< 'sTR" ["; print_env pk (List.rev lpars); 'sTR "]">];
+              'bRK(1,5); 'sTR": "; pterminenv lparsprint arity; 'sTR" :=";
+              'bRK(0,4); print_constructors mip; 'fNL;
+              implicit_args_msg sp mipv  >] )
+  (* Mutual [co]inductive definitions *)
+  else
+    let (mipli,miplc) =
+      List.fold_left 
+        (fun (li,lc) mi ->
+           if mi.mind_finite then (mi::li,lc) else (li,mi::lc))
+        ([],[]) (Array.to_list mipv) 
+    in 
+    let strind =
+      if mipli = [] then [<>] 
+      else [< 'sTR "Inductive"; 'bRK(1,4);
+              (prlist_with_sep
+                 (fun () -> [< 'fNL; 'sTR"  with"; 'bRK(1,4) >])
+                 print_oneind
+                 (List.rev mipli)); 'fNL >]
+    and strcoind =
+      if miplc = [] then [<>] 
+      else [< 'sTR "CoInductive"; 'bRK(1,4);
+              (prlist_with_sep
+                 (fun () -> [<'fNL; 'sTR "  with"; 'bRK(1,4) >]) 
+                 print_oneind (List.rev miplc)); 'fNL >] 
+    in
+    (hV 0 [< 'sTR"Mutual " ; 
+             if mip.mind_finite then 
+	       [< strind; strcoind >] 
+             else 
+	       [<strcoind; strind>];
+             implicit_args_msg sp mipv >])
+
+let print_extracted_mutual sp = 
+  let mib = Global.lookup_mind (ccisp_of sp) in
+  match mib.mind_singl with 
+    | None -> 
+	let fwsp = fwsp_of sp in
+	print_mutual FW fwsp (Global.lookup_mind fwsp)
+    | Some a -> fprterm a
+
+let print_leaf_entry with_values sep (spopt,lobj) =
+  let tag = object_tag lobj in
+  match (spopt,tag) with
+    | (_,"VARIABLE") ->
+	let (name,(typ,_),_,l,_,_) = outVariable lobj in
+	[< print_var (string_of_id name) typ; 
+	   print_impl_args (list_of_implicits l); 'fNL >]
+ 
+    | (sp,"CONSTANT") ->
+	let (cmap,_,_) = outConstant lobj in
+	if Listmap.in_dom cmap CCI then
+	  let {cONSTBODY=val_0;cONSTTYPE=typ;cONSTIMPARGS=l} = 
+	    Listmap.map cmap CCI
+	  in 
+	  hOV 0 [< (match val_0 with 
+		      | None -> 
+			  [< 'sTR"*** [ "; 
+			     'sTR (print_basename (ccisp_of sp));  
+			     'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >]
+		      | _ -> 
+			  [< 'sTR(print_basename (ccisp_of sp)) ; 
+			     'sTR sep; 'cUT ;
+			     if with_values then 
+			       print_typed_recipe (val_0,typ) 
+			     else 
+			       [< prtype typ ; 'fNL >] >]); 
+		   print_impl_args (list_of_implicits l); 'fNL >]
+	else
+	  hOV 0 [< 'sTR"Fw constant " ; 
+		   'sTR (print_basename (fwsp_of sp)) ; 'fNL>]
+
+    | (sp,"MUTUALINDUCTIVE") ->
+	let (cmap,_) = outMutualInductive lobj in
+	if Listmap.in_dom cmap CCI then
+	  [< print_mutual CCI (Listmap.map cmap CCI); 'fNL >]
+	else
+	  hOV 0 [< 'sTR"Fw inductive definition " ; 
+		   'sTR (print_basename (fwsp_of sp)) ; 'fNL >]
+
+    | (_,"UNIVERSES") -> [< print_universes_object (outUniverses lobj); 'fNL >]
+
+    | (_,"AUTOHINT") -> [< 'sTR" Add Auto Marker" ; 'fNL >]
+
+    | (_,"GRAMMAR") -> [< 'sTR" Grammar Marker" ; 'fNL >]
+
+    | (sp,"SYNTAXCONSTANT") -> 
+        [< 'sTR" Syntax Macro " ; 
+      	   'sTR(string_of_id(basename sp)) ; 'sTR sep;  
+           if with_values then 
+             let cmap = outSyntaxConstant lobj in 
+      	     [< prterm (Listmap.map cmap CCI) >]
+           else [<>]; 'fNL >]
+	
+    | (_,"PPSYNTAX") -> [< 'sTR" Syntax Marker" ; 'fNL >]
+
+    | (_,"TOKEN") -> [< 'sTR" Token Marker" ; 'fNL >]
+
+    | (_,"CLASS") -> [< 'sTR" Class Marker" ; 'fNL >]
+    | (_,"COERCION") -> [< 'sTR" Coercion Marker" ; 'fNL >]
+    | (sp,s) -> [< 'sTR(string_of_path sp) ; 'sTR" : " ;
+                   'sTR"Unrecognized object " ; 'sTR s ; 'fNL >]
+
+let rec print_library_entry with_values ent = 
+  let sep = if with_values then " = " else " : " in 
+  match ent with
+    | (sp,Lib.LEAF lobj) -> [< print_leaf_entry with_values sep (sp,lobj) >]
+    | (s,Lib.ClosedDir(_,_,_,ctxt)) ->
+	[< 'sTR"Closed Section " ; 'sTR (string_of_path s) ; 'fNL ;
+	   if !print_closed_sections then
+             [< 'sTR " " ; hOV 0 [< print_context with_values ctxt >] >]
+	   else 
+	     [< >] >]
+    | (sp,Lib.OpenDir(str,_)) -> 
+        [< 'sTR(" >>>>>>> Section " ^ str) ; 'fNL >]
+    | (_,Lib.Import(s,_,true)) ->
+	[< 'sTR" >>>>>>> Import " ; 'sTR s ; 'fNL >]
+    | (_,Lib.Import(s,_,false)) ->
+	[< 'sTR" >>>>>>> Export " ; 'sTR s ; 'fNL >]
+
+and print_context with_values = 
+  let rec prec = function
+    | h::rest -> [< prec rest ; print_library_entry with_values h >]
+    | [] -> [< >]
+  in 
+  prec
+
+let print_full_context () = print_context true (Lib.contents_after None)
+
+let print_full_context_typ () = print_context false (Lib.contents_after None)
+
+(* For printing an inductive definition with
+   its constructors and elimination,
+   assume that the declaration of constructors and eliminations
+   follows the definition of the inductive type *)
+
+let rec head_const c = match strip_outer_cast c with
+  | DOP2(Prod,_,DLAM(_,c)) -> head_const c
+  | DOPN(AppL,cl)    -> head_const (hd_vect cl)
+  | def         -> def
+
+let list_filter_vec f vec = 
+  let rec frec n lf = 
+    if n < 0 then lf 
+    else if f vec.(n) then 
+      frec (n-1) (vec.(n)::lf)
+    else 
+      frec (n-1) lf
+  in 
+  frec (Array.length vec -1) []
+
+ (* The four functions print_constructors_head, print_all_constructors_head,
+   print_constructors_rel and crible implement the behavior needed for the
+   Coq Search command.  These functions take as first argument the procedure
+   that will be called to treat each entry.  This procedure receives the name
+   of the object, the assumptions that will make it possible to print its type,
+   and the constr term that represent its type. *)
+
+let print_constructors_head 
+  (fn:string -> unit assumptions -> constr -> unit) c mip = 
+  let (lna,lC) = decomp_all_DLAMV_name mip.mINDLC in
+  let ass_name = assumptions_for_print lna in
+  let lidC = map2_vect (fun id c_0 -> (id,c_0)) mip.mINDCONSNAMES lC in
+  let flid = list_filter_vec (fun (_,c_0) -> head_const c_0 = c) lidC in
+  List.iter
+    (function (id,c_0) -> fn (string_of_id id) ass_name c_0) flid
+    
+let print_all_constructors_head fn c mib = 
+  let mipvec = mib.mINDPACKETS 
+  and n = mib.mINDNTYPES in 
+  let rec prec i = 
+    if i = n then 
+      mSG([< >])
+    else begin
+      print_constructors_head fn c mipvec.(i); 
+      prec (i+1)
+    end
+  in 
+  prec 0 
+
+let print_constructors_rel fn mip = 
+  let (lna,lC) = decomp_all_DLAMV_name mip.mINDLC in
+  let ass_name = assumptions_for_print lna in
+  let lidC = map2_vect (fun id c -> (id,c)) mip.mINDCONSNAMES lC in
+  let flid = list_filter_vec (fun (_,c) -> isRel (head_const c)) lidC in
+  List.iter (function (id,c) -> fn (string_of_id id) ass_name c) flid
+
+let crible (fn:string -> unit assumptions -> constr -> unit) name =
+  let imported = Library.search_imports() in
+  let const = Machops.global (gLOB(initial_sign())) name in 
+  let rec crible_rec = function
+    | (spopt,Lib.LEAF lobj)::rest ->
+	(match (spopt,object_tag lobj) with
+	   | (_,"VARIABLE") ->
+	       let (namec,(typ,_),_,_,_,_) = outVariable lobj in 
+               (if (head_const typ.body)=const then  
+                  fn (string_of_id namec) (gLOB(initial_sign())) typ.body);
+               crible_rec rest
+	   | (sp,"CONSTANT") ->
+	       let (_,{cONSTTYPE=typ}) = const_of_path (ccisp_of sp) in
+               (if (head_const typ.body)=const then
+                  fn (print_basename sp) (gLOB(initial_sign())) typ.body);
+               crible_rec rest
+	   | (sp,"MUTUALINDUCTIVE") -> 
+               let (_,mib) = mind_of_path (ccisp_of sp) in 
+               (match const with (DOPN(MutInd(sp',tyi),_)) 
+                    -> if sp = objsp_of sp' then print_constructors_rel fn
+                      (mind_nth_type_packet mib tyi) 
+		  | _ -> print_all_constructors_head fn const mib); 
+               crible_rec rest
+	   | _ -> crible_rec rest)
+
+    | (spopt,Lib.OpenDir _)::rest -> crible_rec rest
+    | (spopt,Lib.ClosedDir (_,_,_,libseg))::rest -> 
+        (if List.mem spopt imported then crible_rec libseg);
+        crible_rec rest
+    | (spopt,Lib.Import _)::rest -> crible_rec rest
+    | []      -> ()
+  in 
+  try 
+    crible_rec (Lib.contents_after None)
+  with Not_found -> 
+    error ((string_of_id name) ^ " not declared")
+
+let print_crible name =
+  crible (fun str ass_name constr -> 
+            let pc = term0 ass_name constr in
+            mSG[<'sTR str; 'sTR":"; pc; 'fNL >]) name
+
+let read_sec_context sec =
+  let rec get_cxt in_cxt = function
+    | ((sp,Lib.OpenDir(str,_)) as hd)::rest ->
+        if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+    | [] -> []
+    | hd::rest -> get_cxt (hd::in_cxt) rest 
+  in
+  let cxt = (Lib.contents_after None) in
+  List.rev (get_cxt [] cxt)
+
+let print_sec_context sec = print_context true (read_sec_context sec)
+
+let print_sec_context_typ sec = print_context false (read_sec_context sec)
+
+let print_val sign {_VAL=trm;_TYPE=typ} =
+  print_typed_value_in_sign sign (trm,typ)
+    
+let print_type sign {_VAL=trm;_TYPE=typ} =
+  print_typed_value_in_sign sign (trm, nf_betaiota typ)
+    
+let print_eval red_fun sign {_VAL=trm;_TYPE=typ} =
+  let ntrm = red_fun trm
+  and ntyp = nf_betaiota typ in
+  [< 'sTR "     = "; print_typed_value_in_sign sign (ntrm, ntyp) >]
+
+let print_name name = 
+  let str = string_of_id name in 
+  try 
+    let sp = Nametab.sp_of_id CCI name in  
+    let lobj = Lib.map_leaf (objsp_of sp) in
+    print_leaf_entry true " = " (sp,lobj)
+  with 
+    | Not_found -> 
+	(try 
+	   let typ = snd(lookup_glob name (gLOB (initial_sign ()))) in 
+	   ([< print_var str typ;
+               try print_impl_args (Vartab.implicits_of_var CCI name)
+               with _ -> [<>] >]) 
+	 with Not_found | Invalid_argument _ -> 
+	   error (str ^ " not a defined object"))
+    | Invalid_argument _ -> error (str ^ " not a defined object")
+
+let print_opaque_name name = 
+  let (sigma,sign) = initial_sigma_sign() in
+  try 
+    match (Machops.global (gLOB sign) name) with
+      | DOPN(Const sp,_) as x ->
+          if evaluable_const sigma x then
+            print_typed_value(const_value sigma x,const_type sigma x)
+          else begin
+            Constants.set_transparent_sp sp;
+            let valu = const_value sigma x in 
+	    Constants.set_opaque_sp sp;
+            print_typed_value(valu,const_type sigma x)
+	  end
+      | DOPN(MutInd (sp,_),_) as x ->
+          print_mutual CCI (snd (mind_of_path sp))
+      | DOPN(MutConstruct _,_) as x -> 
+          print_typed_value(x, type_of sigma sign x)
+      | VAR id ->
+          let a = snd(lookup_sign id sign) in 
+	  print_var (string_of_id id) a
+      | _ -> failwith "print_name"
+  with Not_found -> 
+    error ((string_of_id name) ^ " not declared")
+
+let print_local_context () =
+  let env = Lib.contents_after None in
+  let rec print_var_rec = function 
+    | [] -> [< >]
+    | ((_,Lib.LEAF lobj))::rest ->
+	if "VARIABLE" = object_tag lobj then
+          let (name,(typ,_),_,_,_,_) = outVariable lobj in 
+	  [< print_var_rec rest;
+             print_var (string_of_id name) typ >]
+	else 
+	  print_var_rec rest
+    | _::rest -> print_var_rec rest
+
+  and print_last_const = function
+    | (sp,Lib.LEAF lobj)::rest -> 
+        (match object_tag lobj with
+           | "CONSTANT" -> 
+               let (_,{cONSTBODY=val_0;cONSTTYPE=typ}) = 
+		 const_of_path (ccisp_of sp) in
+               [< print_last_const rest;
+                  'sTR(print_basename sp) ;'sTR" = ";
+                  print_typed_recipe (val_0,typ) >]
+           | "MUTUALINDUCTIVE" -> 
+               let (_,mib) = mind_of_path (ccisp_of sp) in 
+               [< print_last_const rest;print_mutual CCI mib; 'fNL >]
+           |  "VARIABLE" ->  [< >]
+           |  _          ->  print_last_const rest)
+    | (sp,Lib.ClosedDir _)::rest -> print_last_const rest
+    | _ -> [< >]
+  in 
+  [< print_var_rec env;  print_last_const env >]
+
+let fprint_var name typ =
+  [< 'sTR ("*** [" ^ name ^ " :"); fprtype typ; 'sTR "]"; 'fNL >]
+
+let fprint_judge {_VAL=trm;_TYPE=typ} = 
+  [< fprterm trm; 'sTR" : " ; fprterm typ >]
+
+let unfold_head_fconst sigma = 
+  let rec unfrec = function
+    | DOPN(Const _,_) as k -> const_value sigma k 
+    | DOP2(Lambda,t,DLAM(na,b)) -> DOP2(Lambda,t,DLAM(na,unfrec b))
+    | DOPN(AppL,v) -> DOPN(AppL,cons_vect (unfrec (hd_vect v)) (tl_vect v))
+    | x -> x
+  in 
+  unfrec
+
+let print_extracted_name name =
+  let (sigma,(sign,fsign)) = initial_sigma_assumptions() in
+  try
+    match (Machops.global (gLOB sign) name) with
+      | DOPN(Const _,_) as x ->
+          let cont = snd(infexecute sigma (sign,fsign) x) in 
+          (match cont with
+             | Inf {_VAL=trm; _TYPE=typ} ->
+                 (hOV 0
+                    [< 'sTR (string_of_id name); 
+                       if defined_const sigma x then 
+                         begin
+			   Constants.set_transparent_extraction name;
+			   [< 'sTR " ==>";'bRK(1,4); 
+                              fprterm (unfold_head_fconst sigma trm); 'fNL>]
+			 end
+                       else 
+			 [< >]; 
+		       'sTR " :  "; fprterm typ; 'fNL >])
+             | _ -> error "Non informative term")
+      | VAR id ->
+	  (* Pourquoi on n'utilise pas fsign ? *)
+          let a = snd(lookup_sign id sign) in
+          let cont = snd(infexecute sigma (sign,fsign) a.body) in 
+	  (match cont with  (* Cradingue *)
+             | Inf {_VAL=t;_TYPE=k} -> 
+		 (match whd_betadeltaiota sigma k with
+		    | DOP0 (Sort s) ->
+			fprint_var (string_of_id name) {body=t;typ=s})
+             | _  -> error "Non informative term")
+	  
+      | DOPN(MutInd (sp,_),_) as x ->
+          let cont = snd(infexecute sigma (sign,fsign) x) in 
+	  (match cont with
+             | Inf _ ->
+                 (hOV 0 [< 'sTR (string_of_id name); 'sTR " ==>"; 'bRK(1,4);
+                           print_extracted_mutual sp >])
+             | _ -> error "Non informative term")
+      | DOPN(MutConstruct _ ,_) as x ->
+          let cont = snd(infexecute sigma (sign,fsign) x) in 
+	  (match cont with
+             | Inf d ->
+                 [< 'sTR ((string_of_id name) ^" ==> ");
+		    fprint_judge d ; 'fNL >]
+             | _  -> error "Non informative term")
+      | _ -> anomaly "should be a variable or constant"
+  with Not_found -> 
+    error ((string_of_id name) ^ " not declared")
+
+let print_extraction () = 
+  let rec print_rec = function
+    | (sp,Lib.LEAF lobj)::rest ->
+	(match (sp,object_tag lobj) with
+	   | (sp,"CONSTANT") ->
+	       (try 
+		  let (_,{cONSTBODY=d}) = const_of_path (fwsp_of sp) in 
+		  [< print_rec rest;
+		     'sTR(print_basename sp) ; 'sTR" ==> ";  
+		     fprint_recipe d; 'fNL >]
+		with Not_found -> 
+		  print_rec rest)
+	   | (_,"VARIABLE") ->
+	       let (name,(_,cont),_,_,_,_) = outVariable lobj in
+               [< print_rec rest;
+		  (match cont with 
+		     | Some(t,_) -> fprint_var (string_of_id name) t
+                     | _         -> [< >]) >]
+	   | (sp,"MUTUALINDUCTIVE") ->
+	       [< print_rec rest; 
+		  (try 
+		     [< print_extracted_mutual sp ; 'fNL >] 
+		   with Not_found -> [<>]) >]
+	   | _ -> print_rec rest)
+	
+    | (sp,Lib.ClosedDir _)::rest -> print_rec rest
+	  
+    | _::rest -> print_rec rest
+	  
+    | [] -> [< 'fNL >]
+  in 
+  [< print_rec (Lib.contents_after None); 'fNL >]
+ 
+let print_extracted_context () =
+  let env = Lib.contents_after None in 
+  let rec print_var_rec = function 
+    | ((_,Lib.LEAF lobj))::rest ->
+	if "VARIABLE" = object_tag lobj then
+          let (name,(typ,cont),_,_,_,_) = outVariable lobj in
+          [< print_var_rec rest ; 'fNL;
+             match cont with
+	       | Some(t,_) -> fprint_var (string_of_id name) t
+               | _         -> [< >] >]
+	else 
+	  print_var_rec rest
+    |  _::rest -> print_var_rec rest
+    | [] -> [< 'fNL >]
+
+  and print_last_constants = function 
+    | (sp,Lib.LEAF lobj)::rest ->
+	(match object_tag lobj with 
+	   | "CONSTANT" -> 
+	       let (_,{cONSTBODY=c;cONSTTYPE=typ}) = 
+		 const_of_path (fwsp_of sp) in
+               [< print_last_constants rest;
+		  let s=print_basename sp	in 
+		  (try 
+		     let (_,{cONSTBODY = d}) = const_of_path (fwsp_of sp) in 
+		     [< 'sTR (s ^" ==> "); fprint_recipe d; 'fNL >]
+		   with Not_found -> 
+		     [< >]) >]
+	   | "MUTUALINDUCTIVE" -> 
+	       [< print_last_constants rest; 
+		  try print_extracted_mutual sp with Not_found -> [<>] >]
+	   | "VARIABLE" -> 
+	       let (_,(_,cont),_,_,_,_) = outVariable lobj in
+               (match cont with 
+		  | Some _ -> [<>]
+                  | None -> print_last_constants rest)
+	   | _ ->  print_last_constants rest)
+	
+    |  (_,Lib.ClosedDir _)::rest -> print_last_constants rest
+    | _ -> [< >]
+  in 
+  [< print_var_rec env; print_last_constants env >]
+
+let print_extracted_vars () =
+  let env = Lib.contents_after None in 
+  let rec print_var_rec = function
+    | ((_,Lib.LEAF lobj))::rest ->
+	if "VARIABLE" = object_tag lobj then
+          let (name,(_,cont),_,_,_,_) = outVariable lobj in
+          [< print_var_rec rest ; 'fNL;
+             match cont with
+	       | Some (t,_) -> fprint_var (string_of_id name) t
+               | _          -> [< >] >]
+	else 
+	  print_var_rec rest
+    |  _::rest -> print_var_rec rest
+    | [] -> [< 'fNL >]
+  in 
+  print_var_rec env
+
+(* for debug *)
+let inspect depth = 
+  let rec inspectrec n res env = 
+    if n=0 or env=[] then 
+      res
+    else 
+      inspectrec (n-1) (List.hd env::res) (List.tl env)
+  in 
+  let items = List.rev (inspectrec depth [] (Lib.contents_after None)) in
+  print_context false items
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
new file mode 100644
index 000000000..2b4c378c2
--- /dev/null
+++ b/parsing/pretty.mli
@@ -0,0 +1,44 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Names
+open Sign
+open Term
+open Inductive
+open Reduction
+open Environ
+(*i*)
+
+(* A Pretty-Printer for the Calculus of Inductive Constructions. *)
+
+val assumptions_for_print : name list -> unit assumptions
+
+val print_basename : section_path -> string
+val print_basename_mind : section_path -> identifier -> string
+val print_closed_sections : bool ref
+val print_impl_args : int list -> std_ppcmds
+val print_env : path_kind -> (name * constr) list -> std_ppcmds
+val print_context : bool -> Lib.library_segment -> std_ppcmds
+val print_library_entry : bool -> (section_path * Lib.node) -> std_ppcmds
+val print_full_context : unit -> std_ppcmds
+val print_full_context_typ : unit -> std_ppcmds
+val print_crible : identifier -> unit
+val print_sec_context : string -> std_ppcmds
+val print_sec_context_typ : string -> std_ppcmds
+val print_val : context -> unsafe_judgment -> std_ppcmds
+val print_type : context -> unsafe_judgment -> std_ppcmds
+val print_eval :
+  'a reduction_function -> context -> unsafe_judgment -> std_ppcmds
+val implicit_args_msg : mutual_inductive_packet array -> std_ppcmds
+val print_mutual : path_kind -> mutual_inductive_body -> std_ppcmds
+val print_name : identifier -> std_ppcmds
+val print_opaque_name : identifier -> std_ppcmds
+val print_local_context : unit -> std_ppcmds
+val print_extracted_name : identifier -> std_ppcmds
+val print_extraction : unit -> std_ppcmds
+val print_extracted_vars : unit -> std_ppcmds
+val crible : (string -> unit assumptions -> constr -> unit) -> identifier ->
+  unit
+val inspect : int -> std_ppcmds
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 9bf72b660..438c338b8 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -12,6 +12,16 @@ val gencompr  : path_kind -> Coqast.t -> std_ppcmds
 val gentermpr : path_kind -> 'a assumptions -> constr -> std_ppcmds
 val gentacpr  : Coqast.t -> std_ppcmds
 
+val prterm          : constr -> std_ppcmds
+val prtype_env      : 'a assumptions -> typed_type -> std_ppcmds
+val prtype          : typed_type -> std_ppcmds
+val fprterm         : constr -> std_ppcmds
+val fprtype_env     : 'a assumptions -> typed_type -> std_ppcmds
+val fprtype         : typed_type -> std_ppcmds
+val fterm0          : 'a assumptions -> constr -> std_ppcmds
+val term0           : 'a assumptions -> constr -> std_ppcmds
+val term0_at_top    : 'a assumptions -> constr -> std_ppcmds
+
 val print_arguments : bool ref
 val print_casts     : bool ref
 val print_emacs     : bool ref