From 04e07924ddd8d0a95e01103103bd8c2a3e79c6c5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 27 Oct 2008 15:59:42 +0000 Subject: [PATCH] Implicit annotationas are now printed --- helm/software/components/ng_kernel/nCicPp.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index cebdaf0b2..2b0787a72 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -43,6 +43,14 @@ let r2s pp_fix_name r = with NCicLibrary.ObjectNotFound _ -> R.string_of_reference r ;; +let string_of_implicit_annotation = function + | `Closed -> "▪" + | `Type -> "" + | `Hole -> "□" + | `Term -> "Term" + | `Typeof x -> "Ty("^string_of_int x^")" +;; + let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t = let buff = Buffer.create 100 in let f = Format.formatter_of_buffer buff in @@ -121,7 +129,8 @@ let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t = List.iter (fun x -> F.fprintf f "@;";aux ctx x) (List.tl l); if not toplevel then F.fprintf f ")"; F.fprintf f "@]" - | C.Implicit _ -> F.fprintf f "?" + | C.Implicit annot -> + F.fprintf f "?%s" (string_of_implicit_annotation annot) | C.Meta (n,lc) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in aux ctx (NCicSubstitution.subst_meta lc t) @@ -196,7 +205,7 @@ let rec ppcontext ?(sep="\n") ~subst ~metasenv = function let rec ppmetasenv ~subst metasenv = function | [] -> "" | (i,(name, ctx, ty)) :: tl -> - let name = match name with Some n -> "("^n^")" | _ -> "" in + let name = match name with Some n -> "(\""^n^"\")" | _ -> "" in ppcontext ~sep:"; " ~subst ~metasenv ctx ^ " ⊢ ?"^string_of_int i^name^" : " ^ ppterm ~metasenv ~subst ~context:ctx ty ^ "\n" ^ -- 2.39.2