rewritten instantiate code

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 12227b4b190126414e97210547faf4625781db42..33677cb422c2e22191c259376a6e2e7450cd157a 100644 (file)
--- 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 -> "…"
@@ -207,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
@@ -225,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;