diff options
Diffstat (limited to 'checker/votour.ml')
-rw-r--r-- | checker/votour.ml | 104 |
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"^ |