1 files changed, 61 insertions, 43 deletions

diff --git a/checker/votour.ml b/checker/votour.ml
index 48f9f45e..bc820e23 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -1,15 +1,19 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Values
 
 (** {6 Interactive visit of a vo} *)
 
+let max_string_length = 1024
+
 let rec read_num max =
   let quit () =
     Printf.printf "\nGoodbye!\n%!";
@@ -19,14 +23,14 @@ let rec read_num max =
   if l = "u" then None
   else if l = "x" then quit ()
   else
-    try
-      let v = int_of_string l in
+    match int_of_string l with
+    | v ->
       if v < 0 || v >= max then
         let () =
           Printf.printf "Out-of-range input! (only %d children)\n%!" max in
         read_num max
       else Some v
-    with Failure "int_of_string" ->
+    | exception Failure _ ->
       Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!";
       read_num max
 
@@ -75,48 +79,51 @@ struct
 
   type obj = data
 
-  let memory = ref [||]
-  let sizes = ref [||]
+  let memory = ref LargeArray.empty
+  let sizes = ref LargeArray.empty
   (** size, in words *)
 
   let ws = Sys.word_size / 8
 
-  let rec init_size seen = function
-  | Int _ | Atm _ | Fun _ -> 0
+  let rec init_size seen k = function
+  | Int _ | Atm _ | Fun _ -> k 0
   | Ptr p ->
-    if seen.(p) then 0
+    if LargeArray.get seen p then k 0
     else
-      let () = seen.(p) <- true in
-      match (!memory).(p) with
+      let () = LargeArray.set seen p true in
+      match LargeArray.get !memory p with
       | Struct (tag, os) ->
-        let fold accu o = accu + 1 + init_size seen o in
-        let size = Array.fold_left fold 1 os in
-        let () = (!sizes).(p) <- size in
-        size
+        let len = Array.length os in
+        let rec fold i accu k =
+          if i == len then k accu
+          else
+            init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
+        in
+        fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size)
       | String s ->
         let size = 2 + (String.length s / ws) in
-        let () = (!sizes).(p) <- size in
-        size
+        let () = LargeArray.set !sizes p size in
+        k size
 
   let size = function
   | Int _ | Atm _ | Fun _ -> 0
-  | Ptr p -> (!sizes).(p)
+  | Ptr p -> LargeArray.get !sizes p
 
   let repr = function
   | Int i -> INT i
   | Atm t -> BLOCK (t, [||])
   | Fun _ -> OTHER
   | Ptr p ->
-    match (!memory).(p) with
+    match LargeArray.get !memory p with
     | Struct (tag, os) -> BLOCK (tag, os)
     | String s -> STRING s
 
   let input ch =
     let obj, mem = parse_channel ch in
     let () = memory := mem in
-    let () = sizes := Array.make (Array.length mem) (-1) in
-    let seen = Array.make (Array.length mem) false in
-    let _ = init_size seen obj in
+    let () = sizes := LargeArray.make (LargeArray.length mem) (-1) in
+    let seen = LargeArray.make (LargeArray.length mem) false in
+    let () = init_size seen ignore obj in
     obj
 
   let oid = function
@@ -149,22 +156,25 @@ let rec get_name ?(extra=false) = function
 (** For tuples, its quite handy to display the inner 1st string (if any).
     Cf. [structure_body] for instance *)
 
+exception TupleString of string
 let get_string_in_tuple o =
   try
     for i = 0 to Array.length o - 1 do
       match Repr.repr o.(i) with
       | STRING s ->
-        failwith (Printf.sprintf " [..%s..]" s)
+        let len = min max_string_length (String.length s) in
+        raise (TupleString (Printf.sprintf " [..%s..]" (String.sub s 0 len)))
       | _ -> ()
     done;
     ""
-  with Failure s -> s
+  with TupleString s -> s
 
 (** Some details : tags, integer value for non-block, etc etc *)
 
 let rec get_details v o = match v, Repr.repr o with
   | (String | Any), STRING s ->
-    Printf.sprintf " [%s]" (String.escaped s)
+    let len = min max_string_length (String.length s) in
+    Printf.sprintf " [%s]" (String.escaped (String.sub s 0 len))
   |Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o
   |(Sum _|Any), BLOCK (tag, _) ->
     Printf.sprintf " [tag=%i]" tag
@@ -191,20 +201,20 @@ let access_children vs os pos =
   else raise Exit
 
 let access_list v o pos =
-  let rec loop o pos = match Repr.repr o with
-  | INT 0 -> []
+  let rec loop o pos accu = match Repr.repr o with
+  | INT 0 -> List.rev accu
   | BLOCK (0, [|hd; tl|]) ->
-    (v, hd, 0 :: pos) :: loop tl (1 :: pos)
+    loop tl (1 :: pos) ((v, hd, 0 :: pos) :: accu)
   | _ -> raise Exit
   in
-  Array.of_list (loop o pos)
+  Array.of_list (loop o pos [])
 
 let access_block o = match Repr.repr o with
 | BLOCK (tag, os) -> (tag, os)
 | _ -> raise Exit
-let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit
 
 (** raises Exit if the object has not the expected structure *)
+exception Forbidden
 let rec get_children v o pos = match v with
   |Tuple (_, v) ->
     let (_, os) = access_block o in
@@ -225,18 +235,26 @@ let rec get_children v o pos = match v with
     | BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|]
     | _ -> raise Exit
     end
-  |String | Int -> [||]
+  | String ->
+    begin match Repr.repr o with
+    | STRING _ -> [||]
+    | _ -> raise Exit
+    end
+  | Int ->
+    begin match Repr.repr o with
+    | INT _ -> [||]
+    | _ -> raise Exit
+    end
   |Annot (s,v) -> get_children v o pos
   |Any -> raise Exit
   |Dyn ->
     begin match Repr.repr o with
     | BLOCK (0, [|id; o|]) ->
-      let n = access_int id in
-      let tpe = find_dyn n in
+      let tpe = Any in
       [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|]
     | _ -> raise Exit
     end
-  |Fail s -> failwith "forbidden"
+  |Fail s -> raise Forbidden
 
 let get_children v o pos =
   try get_children v o pos
@@ -257,9 +275,10 @@ let init () = stk := []
 
 let push name v o p = stk := { nam = name; typ = v; obj = o; pos = p } :: !stk
 
+exception EmptyStack
 let pop () = match !stk with
   | i::s -> stk := s; i
-  | _ -> failwith "empty stack"
+  | _ -> raise EmptyStack
 
 let rec visit v o pos =
   Printf.printf "\nDepth %d Pos %s Context %s\n"
@@ -283,8 +302,8 @@ let rec visit v o pos =
        push (get_name v) v o pos;
        visit v' o' pos'
   with
-  | Failure "empty stack" -> ()
-  | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos
+  | EmptyStack -> ()
+  | Forbidden -> let info = pop () in visit info.typ info.obj info.pos
   | Failure _ | Invalid_argument _ -> visit v o pos
 
 end
@@ -313,8 +332,7 @@ let dummy_header = {
 }
 
 let parse_header chan =
-  let magic = String.create 4 in
-  let () = for i = 0 to 3 do magic.[i] <- input_char chan done in
+  let magic = really_input_string chan 4 in
   let length = input_binary_int chan in
   let objects = input_binary_int chan in
   let size32 = input_binary_int chan in
@@ -377,7 +395,7 @@ let visit_vo f =
     | None -> ()
   done
 
-let main =
+let () =
   if not !Sys.interactive then
     Arg.parse [] visit_vo
       ("votour: guided tour of a Coq .vo or .vi file\n"^