From 0bfad3f438ba29135f2c18d1bf3cb0c8f462a205 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Apr 2008 16:40:05 +0000 Subject: [PATCH] added ppobj --- helm/software/components/ng_kernel/check.ml | 2 +- helm/software/components/ng_kernel/nCicPp.ml | 13 +++++++++++++ helm/software/components/ng_kernel/nCicPp.mli | 2 ++ 3 files changed, 16 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index a1d2a7ccb..908493cbe 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -12,7 +12,7 @@ let _ = let l = OCic2NCic.convert_obj u o in List.iter (fun (u,_,_,_,_ as o) -> - prerr_endline ("CHECK: " ^ NUri.string_of_uri u); + prerr_endline ("CHECK: " ^ NUri.string_of_uri u ^"\n"^NCicPp.ppobj o); try NCicTypeChecker.typecheck_obj o with | NCicTypeChecker.AssertFailure s diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 087e58c98..7af5d17a6 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -33,4 +33,17 @@ let trivial_pp_term ~context ~subst ~metasenv = | C.Sort (C.Type n) -> "Type"^string_of_int n in aux (List.map fst context) +;; + +let ppobj = function + | (u,_,_,_,NCic.Fixpoint (b, fl, _)) -> + "let rec "^NUri.string_of_uri u^"\n"^ + String.concat "\nand " + (List.map (fun (_,name,n,ty,bo) -> + name ^ " on " ^ string_of_int n ^ " : " ^ ppterm ty ^ " :=\n"^ + ppterm bo) fl) + | _ -> "todo" +;; + + diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli index ef535cee8..19b754eea 100644 --- a/helm/software/components/ng_kernel/nCicPp.mli +++ b/helm/software/components/ng_kernel/nCicPp.mli @@ -15,3 +15,5 @@ val trivial_pp_term: subst:NCic.substitution -> metasenv:NCic.metasenv -> NCic.term -> string + +val ppobj: NCic.obj -> string -- 2.39.2