summaryrefslogtreecommitdiff
path: root/checker/votour.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/votour.ml')
-rw-r--r--checker/votour.ml189
1 files changed, 189 insertions, 0 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
new file mode 100644
index 00000000..29593cb7
--- /dev/null
+++ b/checker/votour.ml
@@ -0,0 +1,189 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Values
+
+(** {6 Interactive visit of a vo} *)
+
+(** 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 s -> "Invalid node: "^s
+ |Tuple (name,_) -> name
+ |Sum (name,_,_) -> name
+ |Array v -> "array"^(if extra then "/"^get_name ~extra v else "")
+ |List v -> "list"^(if extra then "/"^get_name ~extra v else "")
+ |Opt v -> "option"^(if extra then "/"^get_name ~extra v else "")
+ |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 *)
+
+let get_string_in_tuple v o =
+ try
+ for i = 0 to Array.length v - 1 do
+ if v.(i) = String then
+ failwith (" [.."^(Obj.magic (Obj.field o i) : string)^"..]");
+ done;
+ ""
+ with Failure s -> s
+
+(** Some details : tags, integer value for non-block, etc etc *)
+
+let rec get_details v o = match v with
+ |String | Any when (Obj.is_block o && Obj.tag o = Obj.string_tag) ->
+ " [" ^ String.escaped (Obj.magic o : string) ^"]"
+ |Tuple (_,v) -> get_string_in_tuple v o
+ |(Sum _|Any) when Obj.is_block o ->
+ " [tag=" ^ string_of_int (Obj.tag o) ^"]"
+ |(Sum _|Any) ->
+ " [imm=" ^ string_of_int (Obj.magic o : int) ^"]"
+ |Int -> " [" ^ string_of_int (Obj.magic o : int) ^"]"
+ |Annot (s,v) -> get_details v o
+ |_ -> ""
+
+let node_info (v,o,p) =
+ get_name ~extra:true v ^ get_details v o ^
+ " (size "^ string_of_int (CObj.shared_size_of_pos p)^"w)"
+
+(** Children of a block : type, object, position.
+ For lists, we collect all elements of the list at once *)
+
+let access_children vs o pos =
+ Array.mapi (fun i v -> v, Obj.field o i, i::pos) vs
+
+let rec get_children v o pos = match v with
+ |Tuple (_,v) -> access_children v o pos
+ |Sum (_,_,vv) ->
+ if Obj.is_block o then access_children vv.(Obj.tag o) o pos
+ else [||]
+ |Array v -> access_children (Array.make (Obj.size o) v) o pos
+ |List v ->
+ let rec loop pos = function
+ | [] -> []
+ | o :: ol -> (v,o,0::pos) :: loop (1::pos) ol
+ in
+ Array.of_list (loop pos (Obj.magic o : Obj.t list))
+ |Opt v ->
+ if Obj.is_block o then [|v,Obj.field o 0,0::pos|] else [||]
+ |String | Int -> [||]
+ |Annot (s,v) -> get_children v o pos
+ |Any ->
+ 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 s -> failwith "forbidden"
+
+type info = {
+ nam : string;
+ typ : value;
+ obj : Obj.t;
+ pos : int list
+}
+
+let stk = ref ([] : info list)
+
+let init () = stk := []
+
+let push name v o p = stk := { nam = name; typ = v; obj = o; pos = p } :: !stk
+
+let pop () = match !stk with
+ | i::s -> stk := s; i
+ | _ -> failwith "empty stack"
+
+let rec visit v o pos =
+ Printf.printf "\nDepth %d Pos %s Context %s\n"
+ (List.length !stk)
+ (String.concat "." (List.rev_map string_of_int pos))
+ (String.concat "/" (List.rev_map (fun i -> i.nam) !stk));
+ Printf.printf "-------------\n";
+ let children = get_children v o pos in
+ let nchild = Array.length children in
+ Printf.printf "Here: %s, %d child%s\n"
+ (node_info (v,o,pos)) nchild (if nchild = 0 then "" else "ren:");
+ Array.iteri
+ (fun i vop -> Printf.printf " %d: %s\n" i (node_info vop))
+ children;
+ Printf.printf "-------------\n";
+ Printf.printf ("# %!");
+ let l = read_line () in
+ try
+ if l = "u" then let info = pop () in visit info.typ info.obj info.pos
+ else if l = "x" then (Printf.printf "\nGoodbye!\n\n";exit 0)
+ else
+ let v',o',pos' = children.(int_of_string l) in
+ 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
+ | Failure _ | Invalid_argument _ -> visit v o pos
+
+(** Loading the vo *)
+
+type segment = {
+ name : string;
+ mutable pos : int;
+ typ : Values.value;
+}
+
+let visit_vo f =
+ Printf.printf "\nWelcome to votour !\n";
+ Printf.printf "Enjoy your guided tour of a Coq .vo or .vi file\n";
+ Printf.printf "Object sizes are in words (%d bits)\n" Sys.word_size;
+ Printf.printf
+ "At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
+ let segments = [|
+ {name="library"; pos=0; typ=Values.v_lib};
+ {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques};
+ {name="discharging info"; pos=0; typ=Opt Any};
+ {name="STM tasks"; pos=0; typ=Opt Any};
+ {name="opaque proofs"; pos=0; typ=Values.v_opaques};
+ |] in
+ while true do
+ let ch = open_in_bin f in
+ let magic = input_binary_int ch in
+ Printf.printf "File format: %d\n%!" magic;
+ for i=0 to Array.length segments - 1 do
+ let pos = input_binary_int ch in
+ segments.(i).pos <- pos_in ch;
+ seek_in ch pos;
+ ignore(Digest.input ch);
+ done;
+ Printf.printf "The file has %d segments, choose the one to visit:\n"
+ (Array.length segments);
+ Array.iteri (fun i { name; pos } ->
+ Printf.printf " %d: %s, starting at byte %d\n" i name pos)
+ segments;
+ Printf.printf "# %!";
+ let l = read_line () in
+ let seg = int_of_string l in
+ seek_in ch segments.(seg).pos;
+ let o = (input_value ch : Obj.t) in
+ let () = CObj.register_shared_size o in
+ let () = init () in
+ visit segments.(seg).typ o []
+ done
+
+let main =
+ if not !Sys.interactive then
+ Arg.parse [] visit_vo
+ ("votour: guided tour of a Coq .vo or .vi file\n"^
+ "Usage: votour file.v[oi]")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 01:35:16 +0000