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=2f4b694deeb413620b37e2ede0d6fbd909aa802b;hpb=889815067d64e081eb90ea1a792890c2ad4e511c;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 2f4b694de..f608acc15 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -57,6 +57,7 @@ let string_of_implicit_annotation = function
   | `Closed -> "▪"
   | `Type -> ""
   | `Hole -> "□"
+  | `Tagged s -> "[\"" ^ s ^ "\"]"
   | `Term -> "Term"
   | `Typeof x -> "Ty("^string_of_int x^")"
   | `Vector -> "…"
@@ -173,16 +174,7 @@ 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
 ;;
@@ -216,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
@@ -234,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;
@@ -249,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;
@@ -257,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
@@ -268,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