X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=1058a48cca4a0faaa09ee2609d4f10a9dc522b08;hb=d40ad33ad3d075c5dd74b6a67131683b0ebe32d6;hp=006a8a7a5f4fec44529d2e623c7852ea0a6858f4;hpb=72a3999ca5a4a2168753c272063ea6530dc963bd;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 006a8a7a5..1058a48cc 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -51,13 +51,13 @@ let r2s pp_fix_name r =
   | NCicEnvironment.ObjectNotFound _ 
   | Failure "nth" 
   | Invalid_argument "List.nth" -> R.string_of_reference r
-
 ;;
 
 let string_of_implicit_annotation = function
   | `Closed -> "▪"
   | `Type -> ""
   | `Hole -> "□"
+  | `Tagged s -> "[\"" ^ s ^ "\"]"
   | `Term -> "Term"
   | `Typeof x -> "Ty("^string_of_int x^")"
   | `Vector -> "…"
@@ -174,26 +174,20 @@ let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
             (List.map (NCicSubstitution.lift shift) (List.tl l));
          end;
        F.fprintf f "])"
-  | C.Sort C.Prop -> F.fprintf f "Prop"
-  | C.Sort (C.Type []) -> F.fprintf f "Type0"
-  | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
-  | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
-  | C.Sort (C.Type l) -> 
-      F.fprintf f "Max(";
-      aux ctx (C.Sort (C.Type [List.hd l]));
-      List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x])))
-       (List.tl l);
-      F.fprintf f ")"
+  | C.Sort s -> NCicEnvironment.ppsort f s
  in 
   aux ~toplevel:true (List.map fst context) 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 = 
@@ -201,29 +195,49 @@ 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 =
+ 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
@@ -235,10 +249,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;
@@ -250,6 +263,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;
@@ -258,7 +300,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
@@ -269,7 +311,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