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

3 files changed, 38 insertions, 1 deletions

diff --git a/checker/validate.ml b/checker/validate.ml
index f1b3fbe42..6a1a26c31 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -56,6 +56,13 @@ let val_block ctx o =
       fail ctx o "block: found no scan tag")
   else fail ctx o "expected block obj"
 
+let val_dyn ctx o =
+  let fail () = fail ctx o "expected a Dyn.t" in
+  if not (Obj.is_block o) then fail ()
+  else if not (Obj.size o = 2) then fail ()
+  else if not (Obj.tag (Obj.field o 0) = Obj.string_tag) then fail ()
+  else ()
+
 open Values
 
 let rec val_gen v ctx o = match v with
@@ -71,6 +78,7 @@ let rec val_gen v ctx o = match v with
   | Any -> ()
   | Fail s -> fail ctx o ("unexpected object " ^ s)
   | Annot (s,v) -> val_gen v (ctx/s) o
+  | Dyn -> val_dyn ctx o
 
 (* Check that an object is a tuple (or a record). vs is an array of
    value representation for each field. Its size corresponds to the
diff --git a/checker/values.ml b/checker/values.ml
index eb43ec3e1..3d77339dc 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -42,6 +42,7 @@ type value =
   | Int
   | String
   | Annot of string * value
+  | Dyn
 
 (** Some pseudo-constructors *)
 
@@ -295,7 +296,7 @@ let v_compiled_lib =
 
 (** Library objects *)
 
-let v_obj = Tuple ("Dyn.t",[|String;Any|])
+let v_obj = Dyn
 let v_libobj = Tuple ("libobj", [|v_id;v_obj|])
 let v_libobjs = List v_libobj
 let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|])
@@ -306,3 +307,22 @@ let v_lib =
   Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
 
 let v_opaques = Array v_constr
+
+(** Registering dynamic values *)
+
+module StringOrd =
+struct
+  type t = string
+  let compare (x : t) (y : t) = compare x y
+end
+
+module StringMap = Map.Make(StringOrd)
+
+let dyn_table : value StringMap.t ref = ref StringMap.empty
+
+let register_dyn name t =
+  dyn_table := StringMap.add name t !dyn_table
+
+let find_dyn name =
+  try StringMap.find name !dyn_table
+  with Not_found -> Any
diff --git a/checker/votour.ml b/checker/votour.ml
index 11b95c93c..95f1ee85a 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 = {