Adding dynamic value printing to votour through a registering mechanism.

TODO: register the desired dynamic types.

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

1 files changed, 9 insertions, 0 deletions

diff --git a/checker/votour.ml b/checker/votour.ml
index 11b95c93c9..95f1ee85a9 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -12,6 +12,10 @@ open Values
 
 (** Name of a value *)
 
+type dyn = { dyn_tag : string; dyn_obj : Obj.t; }
+
+let to_dyn obj = (Obj.magic obj : dyn)
+
 let rec get_name ?(extra=false) = function
   |Any -> "?"
   |Fail _ -> assert false
@@ -23,6 +27,7 @@ let rec get_name ?(extra=false) = function
   |Int -> "int"
   |String -> "string"
   |Annot (s,v) -> s^"/"^get_name ~extra v
+  |Dyn -> "<dynamic>"
 
 (** For tuples, its quite handy to display the inner 1st string (if any).
     Cf. [structure_body] for instance *)
@@ -80,6 +85,10 @@ let rec get_children v o pos = match v with
     if Obj.is_block o && Obj.tag o < Obj.no_scan_tag then
       Array.init (Obj.size o) (fun i -> (Any,Obj.field o i,i::pos))
     else [||]
+  |Dyn ->
+    let t = to_dyn o in
+    let tpe = find_dyn t.dyn_tag in
+    [|(String, Obj.repr t.dyn_tag, 0 :: pos); (tpe, t.dyn_obj, 1 :: pos)|]
   |Fail _ -> assert false
 
 type info = {