From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- checker/votour.ml | 189 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 189 insertions(+) create mode 100644 checker/votour.ml (limited to 'checker/votour.ml') 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 *) +(* "?" + |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 -> "" + +(** 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, enters the -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]") -- cgit v1.2.3