X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=f608acc15109f913c4f92a428a8d0cc5452887e9;hb=dc7c02d8d8678d250a99dd6d012adcd69da63b75;hp=ddecb4dfb9ba75c299211307787ce68e27363de3;hpb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index ddecb4dfb..f608acc15 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -208,13 +208,28 @@ let rec ppcontext ~formatter ?(sep="\n") ~subst ~metasenv = function
       F.fprintf formatter "%s" sep
 ;;
 
+let ppmetaattrs =
+ function
+    [] -> ""
+  | attrs ->
+   "(" ^
+    String.concat ","
+     (List.map
+       (function
+           `IsSort -> "sort"
+         | `Name n -> "name=" ^ n
+         | `InScope -> "in_scope"
+         | `OutScope n -> "out_scope:" ^ string_of_int n
+       ) attrs) ^
+    ")"
+;;
+
 let rec ppmetasenv ~formatter ~subst metasenv = function
   | [] -> ()
-  | (i,(name, ctx, ty)) :: tl ->
+  | (i,(attrs, ctx, ty)) :: tl ->
       F.fprintf formatter "@[<hov 2>";
-      let name = match name with Some n -> "("^n^")" | _ -> "" in
       ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx;
-      F.fprintf formatter "@;⊢@;?%d%s :@;" i name;
+      F.fprintf formatter "@;⊢@;?%d%s :@;" i (ppmetaattrs attrs);
       ppterm ~formatter ~metasenv ~subst ~context:ctx ty;
       F.fprintf formatter "@]@\n";
       ppmetasenv ~formatter ~subst metasenv tl
@@ -226,10 +241,9 @@ let ppmetasenv ~formatter ~subst metasenv =
 
 let rec ppsubst ~formatter ~subst ~metasenv = function
   | [] -> ()
-  | (i,(name, ctx, t, ty)) :: tl ->
-      let name = match name with Some n -> "("^n^")" | _ -> "" in
+  | (i,(attrs, ctx, t, ty)) :: tl ->
       ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx;
-      F.fprintf formatter " ⊢ ?%d%s := " i name;
+      F.fprintf formatter " ⊢ ?%d%s := " i (ppmetaattrs attrs);
       ppterm ~formatter ~metasenv ~subst ~context:ctx t;
       F.fprintf formatter " : ";
       ppterm ~formatter ~metasenv ~subst ~context:ctx ty;
@@ -241,6 +255,35 @@ let ppsubst ~formatter ~metasenv subst =
  ppsubst ~formatter ~metasenv ~subst 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) = 
   F.fprintf formatter "metasenv:\n";
   ppmetasenv ~formatter ~subst metasenv;
@@ -249,7 +292,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
@@ -260,7 +303,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