Processor integers + Print assumption (see coqdev mailing list for the

details).




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 46 insertions, 0 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 6a0fe60f61..3386f45f51 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1182,3 +1182,49 @@ type values
 
 
 
+(* spiwack : internal representation printing *)
+let string_of_sorts =
+  function 
+  | Prop Pos -> "Prop Pos"
+  | Prop Null -> "Prop Null"
+  | Type u -> "Type "^string_of_universe u
+
+let string_of_cast_kind = 
+  function
+  |VMcast -> "VMcast"
+  | DEFAULTcast -> "DEFAULTcast"
+
+let rec string_of_constr = 
+  let string_of_term string_of_expr string_of_type = function
+  | Rel i -> "Rel "^string_of_int i
+  | Var id -> "Var "^string_of_identifier id
+  | Meta mv -> "Meta "^"mv?" (* need a function for printing metavariables *)
+  | Evar ev -> "Evar "^"ev?" (* ??     of 'constr pexistential *)
+  | Sort s -> "Sort "^string_of_sorts s
+  | Cast (e,ck,t) -> 
+         "Cast ("^string_of_expr e^", "^string_of_cast_kind ck^", "^
+                 string_of_type t^")" 
+  | Prod (n, t1, t2) -> 
+          "Prod ("^string_of_name n^", "^string_of_type t1^", "^
+                   string_of_type t2^")"  
+  | Lambda (n,t,e) ->
+          "Lambda ("^string_of_name n^", "^string_of_type t^", "^
+                    string_of_expr e^")"
+  | LetIn (n, e1, t, e2) -> 
+           "LetIn ("^string_of_name n^", "^string_of_expr e1^", "^
+           string_of_type t^", "^string_of_expr e2^")"
+  | App   (e, args) ->  "App ("^string_of_expr e^", [|"^
+          String.concat "; " (Array.to_list (Array.map string_of_expr args)) ^
+          "|])"
+  | Const c ->  "Const "^string_of_constant c
+  | Ind   ind ->  "Ind "^string_of_inductive ind
+  | Construct ctr -> "Construct "^string_of_constructor ctr
+  | Case(_,_,_,_)  -> "Case ..."    
+             (*    of case_info * 'constr * 'constr * 'constr array   *)
+  | Fix _  -> "Fix ..."  (*    of ('constr, 'types) pfixpoint *)
+  | CoFix _ -> "CoFix ..."  (*     of ('constr, 'types) pcofixpoint *)
+in 
+fun x -> string_of_term string_of_constr string_of_constr x
+
+
+(* /spiwack *)