[why3doc] fixed links to use and def points

Makefile.in

@@ -1667,6 +1667,13 @@ stdlibdoc: $(STDLIBFILES) $(STDMODFILES) bin/why3doc.@OCAMLBEST@
 	WHY3CONFIG="" bin/why3doc.@OCAMLBEST@ -L theories -L modules \
           -o doc/stdlibdoc --title "Why3 Standard Library" \
 	  $(STDLIBFILES) $(STDMODFILES) $(STDMACFILES)
+	cd doc/stdlibdoc; \
+	  for f in theories.*.html; \
+	    do mv "$$f" "$${f#theories.}"; done; \
+	  for f in modules.*.html; \
+	    do mv "$$f" "$${f#modules.}"; done
+	sed -i -e "s#theories.##g" -e "s#modules.##g" doc/stdlibdoc/index.html
+
 
 clean::
 	rm -f doc/stdlibdoc/*

src/core/theory.ml

@@ -346,7 +346,7 @@ let add_tdecl uc td = match td.td_node with
 
 (** Declarations *)
 
-let store_path, restore_path =
+let store_path, store_theory, restore_path =
   let id_to_path = Wid.create 17 in
   let store_path uc path id =
     (* this symbol already belongs to some theory *)
@@ -354,8 +354,18 @@ let store_path, restore_path =
     let prefix = List.rev (id.id_string :: path @ uc.uc_prefix) in
     Wid.set id_to_path id (uc.uc_path, uc.uc_name.id_string, prefix)
   in
+  let store_theory th =
+    let id = th.th_name in
+    (* this symbol is already a theory *)
+    if Wid.mem id_to_path id then () else
+    Wid.set id_to_path id (th.th_path, id.id_string, []) in
   let restore_path id = Wid.find id_to_path id in
-  store_path, restore_path
+  store_path, store_theory, restore_path
+
+let close_theory uc =
+  let th = close_theory uc in
+  store_theory th;
+  th
 
 let add_symbol add id v uc =
   store_path uc [] id;

src/core/theory.mli

@@ -133,7 +133,8 @@ val restore_path : ident -> string list * string * string list
    qualified symbol name) if the ident was ever introduced in
    a theory declaration. If the ident was declared in several
    different theories, the first association is retained.
-   Raises Not_found if the ident was never declared in a theory. *)
+   If [id] is a theory name, the third component is an empty list.
+   Raises [Not_found] if the ident was never declared in/as a theory. *)
 
 (** {2 Declaration constructors} *)
 

src/parser/glob.ml

@@ -18,20 +18,25 @@ let () = Debug.unset_flag flag (* make sure it is unset by default *)
 
 let dummy_id = id_register (id_fresh "dummy")
 
+type def_use = Def | Use
+
 let glob = Hashtbl.create 5003
   (* could be improved with nested hash tables *)
 
-(* dead code
-let with_loc f = function
-  | None -> ()
-  | Some loc when loc = Loc.dummy_position -> ()
-  | Some loc -> f loc
-*)
+let key loc = let f, l, c, _ = Loc.get loc in f, l, c
+
+let add loc idk =
+  let k = key loc in
+  if not (Hashtbl.mem glob k) then Hashtbl.add glob k idk
+
+let def id =
+  Opt.iter (fun loc -> add loc (id, Def)) id.id_loc
 
 let use loc id =
-  let f, l, c, _ = Loc.get loc in
-(* Format.eprintf "GLOB USE: id=%s at %s/%d/%d@." id.id_string f l c; *)
-  Hashtbl.add glob (f, l, c) id
+  add loc (id, Use)
+
+let find loc =
+  Hashtbl.find glob (key loc)
 
-let locate pos =
-  Hashtbl.find glob pos
+(* FIXME allow several entries for the same loc, find returns all of them,
+         and why3doc inserts several anchors *)

src/parser/glob.mli

@@ -15,9 +15,14 @@ val flag: Debug.flag
 
 val dummy_id: ident
 
+val def: ident -> unit
+  (** [def id] registers that [id] is defined at position [id.id_loc] *)
+
 val use: Loc.position -> ident -> unit
-  (** [add loc id] registers that [id] was used at position [loc] *)
+  (** [use loc id] registers that [id] is used at position [loc] *)
+
+type def_use = Def | Use
 
-val locate: string * int * int -> ident
-  (** [locate pos] returns the ident used at position [pos], if any,
+val find: Loc.position -> ident * def_use
+  (** [find pos] returns the ident used/defined at position [pos], if any,
       or raises [Not_found] *)

src/parser/typing.ml

@@ -35,6 +35,10 @@ exception ClashTheory of string
 
 (** lazy declaration of tuples *)
 
+let add_decl_with_tuples uc d =
+  if Debug.test_flag Glob.flag then Sid.iter Glob.def d.d_news;
+  add_decl_with_tuples uc d
+
 let add_ty_decl uc ts      = add_decl_with_tuples uc (create_ty_decl ts)
 let add_data_decl uc dl    = add_decl_with_tuples uc (create_data_decl dl)
 let add_param_decl uc ls   = add_decl_with_tuples uc (create_param_decl ls)
@@ -48,6 +52,9 @@ let rec qloc = function
   | Qdot (p, id) -> Loc.join (qloc p) id.id_loc
   | Qident id    -> id.id_loc
 
+let qloc_last = function
+  | Qdot (_, id) | Qident id -> id.id_loc
+
 let rec print_qualid fmt = function
   | Qdot (p, id) -> Format.fprintf fmt "%a.%s" print_qualid p id.id
   | Qident id    -> Format.fprintf fmt "%s" id.id
@@ -64,7 +71,7 @@ let find_qualid get_id find ns q =
   let sl = string_list_of_qualid q in
   let r = try find ns sl with Not_found ->
     Loc.error ~loc:(qloc q) (UnboundSymbol q) in
-  if Debug.test_flag Glob.flag then Glob.use (qloc q) (get_id r);
+  if Debug.test_flag Glob.flag then Glob.use (qloc_last q) (get_id r);
   r
 
 let find_prop_ns     ns q = find_qualid (fun pr -> pr.pr_name) ns_find_pr ns q
@@ -800,7 +807,8 @@ let add_use_clone env lenv th loc (use, subst) =
   if Debug.test_flag debug_parse_only then th else
   let use_or_clone th =
     let t = find_theory env lenv use.use_theory in
-    if Debug.test_flag Glob.flag then Glob.use (qloc use.use_theory) t.th_name;
+    if Debug.test_flag Glob.flag then
+      Glob.use (qloc_last use.use_theory) t.th_name;
     match subst with
     | None -> use_export th t
     | Some s ->
@@ -821,6 +829,7 @@ let add_use_clone env lenv th loc (use, subst) =
 let close_theory lenv th =
   if Debug.test_flag debug_parse_only then lenv else
   let th = close_theory th in
+  if Debug.test_flag Glob.flag then Glob.def th.th_name;
   let id = th.th_name.id_string in
   let loc = th.th_name.Ident.id_loc in
   if Mstr.mem id lenv then Loc.error ?loc (ClashTheory id);

src/why3doc/doc_def.ml

@@ -12,11 +12,6 @@
 open Why3
 open Ident
 
-let loadpath = ref []
-let set_loadpath l = loadpath := l
-let is_in_path fname =
-  List.mem (Filename.dirname fname) !loadpath
-
 let stdlib_url = ref None
 let set_stdlib_url u = stdlib_url := Some u
 
@@ -24,10 +19,10 @@ let output_dir = ref None
 let set_output_dir d = output_dir := d
 
 let dir_sep = Str.regexp_string Filename.dir_sep
-let html_filename fn = Str.global_replace dir_sep "." fn
 
 let output_file fname =
-  let f = html_filename fname in
+  let fname = Filename.chop_extension fname in
+  let f = Str.global_replace dir_sep "." fname in
   let base = match !output_dir with
     | None -> f
     | Some dir -> Filename.concat dir f
@@ -35,28 +30,7 @@ let output_file fname =
   base ^ ".html"
 
 type url = string
-type tag = string
-
-type file_kind = Local | Loadpath | Unknown
-
-type file = {
-  tags: (int * int, tag) Hashtbl.t; (* line, column -> tag *)
-  kind: file_kind;
-}
-
-let files = Hashtbl.create 17
-
-let add_file fname =
-  Hashtbl.add files fname { tags = Hashtbl.create 17; kind = Local }
-
-let get_file fname =
-  try
-    Hashtbl.find files fname
-  with Not_found ->
-    let k = if is_in_path fname then Loadpath else Unknown in
-    let f = { tags = Hashtbl.create 17; kind = k } in
-    Hashtbl.add files fname f;
-    f
+type anchor = string
 
 let tag_allowed_char =
   let tbl = Array.make 256 false in
@@ -97,30 +71,19 @@ let tag_escape s =
 let make_tag s l =
   tag_escape s ^ "_" ^ string_of_int l
 
-let add_ident id = match id.id_loc with
-  | None ->
-      ()
-  | Some loc ->
-      let f, l, c, _ = Loc.get loc in
-      let f = get_file f in
-      let t = make_tag id.id_string l in
-      Hashtbl.add f.tags (l, c) t
-
-let is_def (fn, l, c) =
-  let f = get_file fn in
-  Hashtbl.find f.tags (l, c)
-
 let make_url fn =
-  let url = html_filename fn ^ ".html" in
-  match (get_file fn).kind, !stdlib_url with
-    | Local, _ -> url
-    | Loadpath, Some www -> www ^ "/" ^ url
-    | _ -> raise Not_found
-
-let locate id = match id.id_loc with
-  | None ->
-      raise Not_found
-  | Some loc ->
-      let fn, l, _, _ = Loc.get loc in
-      fn, make_url fn, make_tag id.id_string l
+  let url = fn ^ ".html" in
+  match !stdlib_url with
+  | None -> url
+  | Some www -> www ^ "/" ^ url
+
+let anchor id = match id.id_loc with
+  | None -> raise Not_found
+  | Some loc -> let _, l, _, _ = Loc.get loc in make_tag id.id_string l
+
+let locate id =
+  let lp, _, _ =
+    try Mlw_module.restore_path id with Not_found -> Theory.restore_path id in
+  let url = if lp = [] then "" else make_url (String.concat "." lp) in
+  url ^ "#" ^ anchor id
 

src/why3doc/doc_def.mli

@@ -14,24 +14,17 @@ open Ident
 
 (* records definition locations *)
 
-val set_loadpath: string list -> unit
 val set_output_dir: string option -> unit
 val set_stdlib_url: string -> unit
 
 val output_file: string -> string
 
-val add_file: string -> unit
+type anchor = string
 
-val add_ident: ident -> unit
-
-type tag = string
-
-val is_def: string * int * int -> tag
-  (* if [loc] is a definition point, returns the corresponding tag,
-     otrherwise raises [Not_found] *)
+val anchor: ident -> string
 
 type url = string
 
-val locate: ident -> string * url * tag
-  (* returns (filename, url, tag) or raises [Not_found] *)
+val locate: ident -> url
+  (* or raises [Not_found] *)
 

src/why3doc/doc_lexer.mll

@@ -45,8 +45,7 @@
     "returns"; "variant"; "writes"; ]
 
   let get_loc lb =
-    let p = Lexing.lexeme_start_p lb in
-    p.pos_fname, p.pos_lnum, p.pos_cnum - p.pos_bol
+    Loc.extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)
 
   let html_char fmt c =
     pp_print_string fmt (match c with
@@ -91,15 +90,13 @@
       (* is this a def point? *)
       let s = html_escape s in
       try
-        let t = Doc_def.is_def loc in
-        fprintf fmt "<a name=\"%s\">%s</a>" t s
-      with Not_found ->
-      (* is this a use point? *)
-      try
-        let id = Glob.locate loc in
-        let fn, url, t = Doc_def.locate id in
-        let url = if fn = !current_file then "" else url in
-        fprintf fmt "<a href=\"%s#%s\">%s</a>" url t s
+        match Glob.find loc with
+        | id, Glob.Def ->
+          let t = Doc_def.anchor id in
+          fprintf fmt "<a name=\"%s\">%s</a>" t s
+        | id, Glob.Use ->
+          let url = Doc_def.locate id in
+          fprintf fmt "<a href=\"%s\">%s</a>" url s
       with Not_found ->
         (* otherwise, just print it *)
         pp_print_string fmt s

src/why3doc/doc_main.ml

@@ -11,8 +11,6 @@
 
 open Format
 open Why3
-open Stdlib
-open Theory
 
 let () = Debug.set_flag Glob.flag
 
@@ -55,7 +53,7 @@ let () =
   let config = Whyconf.read_config None in
   let main = Whyconf.get_main config in
   opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
-  Doc_def.set_loadpath !opt_loadpath;
+  (* Doc_def.set_loadpath !opt_loadpath; *)
   Doc_def.set_output_dir !opt_output
 
 let index = match !opt_index with
@@ -78,11 +76,7 @@ let css =
 
 let do_file env fname =
   try
-    let m = Env.read_file env fname in
-    let add _s th =
-      Doc_def.add_ident th.th_name;
-      Ident.Sid.iter Doc_def.add_ident th.th_local in
-    Mstr.iter add m
+    ignore (Env.read_file env fname)
   with e ->
     eprintf "warning: could not read file '%s'@." fname;
     eprintf "(%a)@." Exn_printer.exn_printer e
@@ -100,7 +94,7 @@ let print_file fname =
   close_out c
 
 let () =
-  Queue.iter Doc_def.add_file opt_queue;
+  (* Queue.iter Doc_def.add_file opt_queue; *)
   try
     let env = Env.create_env !opt_loadpath in
     (* process files *)
@@ -108,7 +102,7 @@ let () =
     Queue.iter print_file opt_queue;
     (* then generate the index *)
     if index then begin
-      let fhtml = Doc_def.output_file "index" in
+      let fhtml = Doc_def.output_file "index.why" in
       let c = open_out fhtml in
       let fmt = formatter_of_out_channel c in
       if not !opt_body then Doc_html.print_header fmt ~title ~css ();
@@ -121,7 +115,7 @@ let () =
         let fhtml = Doc_def.output_file fn in
         let basename = Filename.basename fhtml in
         fprintf fmt "<li> <a href=\"%s\">%s</a> %s </li>@\n"
-          basename fn header
+          basename (Filename.chop_extension basename) header
       in
       Queue.iter add opt_queue;
       fprintf fmt "</ul>@\n";

src/whyml/mlw_module.ml

@@ -241,7 +241,7 @@ let use_export uc m =
 
 let add_to_theory f uc x = { uc with muc_theory = f uc.muc_theory x }
 
-let store_path, restore_path =
+let store_path, store_module, restore_path =
   let id_to_path = Wid.create 17 in
   let store_path uc path id =
     (* this symbol already belongs to some theory *)
@@ -249,8 +249,18 @@ let store_path, restore_path =
     let prefix = List.rev (id.id_string :: path @ uc.muc_prefix) in
     Wid.set id_to_path id (uc.muc_path, uc.muc_name, prefix)
   in
+  let store_module m =
+    let id = m.mod_theory.th_name in
+    (* this symbol is already a module *)
+    if Wid.mem id_to_path id then () else
+    Wid.set id_to_path id (m.mod_theory.th_path, id.id_string, []) in
   let restore_path id = Wid.find id_to_path id in
-  store_path, restore_path
+  store_path, store_module, restore_path
+
+let close_module uc =
+  let m = close_module uc in
+  store_module m;
+  m
 
 let add_symbol add id v uc =
   store_path uc [] id;

src/whyml/mlw_module.mli

@@ -82,7 +82,8 @@ val restore_path : ident -> string list * string * string list
    qualified symbol name) if the ident was ever introduced in
    a module declaration. If the ident was declared in several
    different modules, the first association is retained.
-   Raises Not_found if the ident was never declared in a module. *)
+   If [id] is a module name, the third component is an empty list.
+   Raises Not_found if the ident was never declared in/as a module. *)
 
 val restore_module : theory -> modul
 (** retrieves a module from its underlying theory

src/whyml/mlw_typing.ml

@@ -53,8 +53,13 @@ let flush_tuples uc =
   Hint.clear ht_tuple;
   uc
 
-let add_pdecl_with_tuples ~wp uc pd = add_pdecl ~wp (flush_tuples uc) pd
-let add_decl_with_tuples uc d = add_decl (flush_tuples uc) d
+let add_pdecl_with_tuples ~wp uc pd =
+  if Debug.test_flag Glob.flag then Sid.iter Glob.def pd.pd_news;
+  add_pdecl ~wp (flush_tuples uc) pd
+
+let add_decl_with_tuples uc d =
+  if Debug.test_flag Glob.flag then Sid.iter Glob.def d.d_news;
+  add_decl (flush_tuples uc) d
 
 (** symbol lookup *)
 
@@ -1206,9 +1211,10 @@ let add_pdecl ~wp loc uc d =
 
 let use_clone_pure lib mth uc loc (use,inst) =
   let path, s = match use.use_theory with
-    | Qdot (p,id) -> Typing.string_list_of_qualid p, id.id
-    | Qident id -> [], id.id in
-  let th = find_theory loc lib mth path s in
+    | Qdot (p,id) -> Typing.string_list_of_qualid p, id
+    | Qident id -> [], id in
+  let th = find_theory loc lib mth path s.id in
+  if Debug.test_flag Glob.flag then Glob.use s.id_loc th.th_name;
   (* open namespace, if any *)
   let uc = match use.use_import with
     | Some (_, use_as) -> Theory.open_namespace uc use_as
@@ -1230,9 +1236,11 @@ let use_clone_pure lib mth uc loc use =
 
 let use_clone lib mmd mth uc loc (use,inst) =
   let path, s = match use.use_theory with
-    | Qdot (p,id) -> Typing.string_list_of_qualid p, id.id
-    | Qident id -> [], id.id in
-  let mth = find_module loc lib mmd mth path s in
+    | Qdot (p,id) -> Typing.string_list_of_qualid p, id
+    | Qident id -> [], id in
+  let mth = find_module loc lib mmd mth path s.id in
+  if Debug.test_flag Glob.flag then Glob.use s.id_loc
+    (match mth with Module m -> m.mod_theory.th_name | Theory th -> th.th_name);
   (* open namespace, if any *)
   let uc = match use.use_import with
     | Some (_, use_as) -> open_namespace uc use_as
@@ -1268,6 +1276,7 @@ let close_theory (mmd,mth) uc =
 let close_module (mmd,mth) uc =
   if Debug.test_flag Typing.debug_parse_only then (mmd,mth) else
   let m = close_module uc in
+  if Debug.test_flag Glob.flag then Glob.def m.mod_theory.th_name;
   let id = m.mod_theory.th_name.id_string in
   let loc = m.mod_theory.th_name.Ident.id_loc in
   if Mstr.mem id mmd then Loc.errorm ?loc "clash with previous module %s" id;