X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=1a793b92fde5db51b370c46eac38a5343f188058;hb=40ebec98f53ac1a9a1e7a462cbf0dd3e3d8d42fd;hp=33677cb422c2e22191c259376a6e2e7450cd157a;hpb=2007402c996678701798d71124a1a255529061ee;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 33677cb42..1a793b92f 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -180,11 +180,14 @@ let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
 ;;
 
 let on_buffer f t = 
+ try
   let buff = Buffer.create 100 in
   let formatter = F.formatter_of_buffer buff in
   f ~formatter:formatter t;
   F.fprintf formatter "@?";
   Buffer.contents buff
+ with Failure m ->
+  "[[Unprintable: " ^ m ^ "]]"
 ;;
 
 let ppterm ~formatter ~context ~subst ~metasenv ?(margin=80) ?inside_fix t = 
@@ -192,20 +195,25 @@ let ppterm ~formatter ~context ~subst ~metasenv ?(margin=80) ?inside_fix t =
   ppterm ~formatter ~context ~subst ~metasenv ?inside_fix t
 ;;
 
-let rec ppcontext ~formatter ?(sep="\n") ~subst ~metasenv = function
+let rec ppcontext ~formatter ?(sep="; ") ~subst ~metasenv = function
   | [] -> ()
   | (name, NCic.Decl t) :: tl -> 
       ppcontext ~formatter ~sep ~subst ~metasenv tl;
       F.fprintf formatter "%s: " name;
       ppterm ~formatter ~subst ~metasenv ~context:tl t;
-      F.fprintf formatter "%s" sep
+      F.fprintf formatter "%s@;" sep
   | (name, NCic.Def (bo,ty)) :: tl->
       ppcontext ~formatter ~sep ~subst ~metasenv tl;
       F.fprintf formatter "%s: " name;
       ppterm ~formatter ~subst ~metasenv ~context:tl ty;
       F.fprintf formatter " := ";
       ppterm ~formatter ~subst ~metasenv ~context:tl bo;
-      F.fprintf formatter "%s" sep
+      F.fprintf formatter "%s@;" sep
+;;
+let ppcontext ~formatter ?sep ~subst ~metasenv c =
+  F.fprintf formatter "@[<hov>";
+  ppcontext ~formatter ?sep ~subst ~metasenv c;
+  F.fprintf formatter "@]";
 ;;
 
 let ppmetaattrs =
@@ -216,7 +224,9 @@ let ppmetaattrs =
     String.concat ","
      (List.map
        (function
-           `IsSort -> "sort"
+         | `IsTerm -> "term"
+         | `IsType -> "type"
+         | `IsSort -> "sort"
          | `Name n -> "name=" ^ n
          | `InScope -> "in_scope"
          | `OutScope n -> "out_scope:" ^ string_of_int n
@@ -251,8 +261,38 @@ let rec ppsubst ~formatter ~subst ~metasenv = function
       ppsubst ~formatter ~subst ~metasenv tl
 ;;
 
-let ppsubst ~formatter ~metasenv subst =
- ppsubst ~formatter ~metasenv ~subst subst
+let ppsubst ~formatter ~metasenv ?(use_subst=true) subst =
+ let ssubst = if use_subst then subst else [] in
+  ppsubst ~formatter ~metasenv ~subst:ssubst subst
+;;
+
+let string_of_generated = function
+  | `Generated -> "Generated"
+  | `Provided -> "Provided"
+;;
+
+let string_of_flavour = function
+  | `Definition -> "Definition"
+  | `Fact -> "Fact"
+  | `Lemma -> "Lemma"
+  | `Theorem -> "Theorem"
+  | `Corollary -> "Corollary"
+  | `Example -> "Example"
+;;
+        
+let string_of_pragma = function
+  | `Coercion _arity -> "Coercion _"
+  | `Elim _sort -> "Elim _"
+  | `Projection -> "Projection"
+  | `InversionPrinciple -> "InversionPrinciple"
+  | `Variant -> "Variant"
+  | `Local -> "Local"
+  | `Regular -> "Regular"
+;;
+
+let string_of_fattrs (g,f,p) = 
+  String.concat ","
+   [ string_of_generated g; string_of_flavour f; string_of_pragma p ]
 ;;
 
 let ppobj ~formatter (u,_,metasenv, subst, o) = 
@@ -263,7 +303,7 @@ let ppobj ~formatter (u,_,metasenv, subst, o) =
   (*ppsubst subst ~formatter ~metasenv;*) F.fprintf formatter "...";
   F.fprintf formatter "\n";
   match o with 
-  | NCic.Fixpoint (b, fl, _) -> 
+  | NCic.Fixpoint (b, fl, attrs) -> 
       F.fprintf formatter "{%s}@\n@[<hov 0>" (NUri.string_of_uri u);
       F.fprintf formatter "@[<hov 2>%s"(if b then "let rec " else "let corec ");
       HExtlib.list_iter_sep
@@ -274,7 +314,8 @@ let ppobj ~formatter (u,_,metasenv, subst, o) =
         F.fprintf formatter "@]@;@[<hov 2>:=@;";
         ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo;
         F.fprintf formatter "@]") fl;
-        F.fprintf formatter "@]"
+      F.fprintf formatter "@; %s" (string_of_fattrs attrs);
+      F.fprintf formatter "@]"
   | NCic.Inductive (b, leftno,tyl, _) -> 
       F.fprintf formatter "{%s} with %d fixed params@\n@[<hov 0>@[<hov 2>%s"
        (NUri.string_of_uri u) leftno
@@ -315,7 +356,9 @@ let ppcontext ?sep ~subst ~metasenv ctx =
 
 let ppmetasenv ~subst metasenv = on_buffer (ppmetasenv ~subst) metasenv;;
 
-let ppsubst ~metasenv subst = on_buffer (ppsubst ~metasenv) subst;;
+let ppsubst ~metasenv ?use_subst subst =
+ on_buffer (ppsubst ~metasenv ?use_subst) subst
+;;
 
 let ppobj obj = on_buffer ppobj obj;;