From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Apr 2008 16:40:05 +0000 (+0000)
Subject: added ppobj
X-Git-Tag: make_still_working~5446
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=0bfad3f438ba29135f2c18d1bf3cb0c8f462a205;hp=3ec1830d5251709ed6c4899c74903498a6cd2744;p=helm.git

added ppobj
---

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