added tests for path

bin/check.ml

@@ -13,7 +13,7 @@ open Tmodule
 open Parser_frontend
 module W = Gospel.Warnings
 
-type config = { verbose : bool; load_path : string list }
+type config = { verbose : bool; paths : bool; load_path : string list }
 
 let fmt = Format.std_formatter
 let pp = Format.fprintf
@@ -22,8 +22,8 @@ let path2module p =
   Filename.basename p |> Filename.chop_extension |> String.capitalize_ascii
 
 let type_check load_path name sigs =
-  let md = init_muc name in
   let mod_name = path2module name in 
+  let md = init_muc mod_name in
   let penv =
     Utils.Sstr.singleton mod_name |> Typing.penv load_path
   in
@@ -53,7 +53,8 @@ let run_file config file =
       pp fmt "@[********* Typed GOSPEL ********@]@.";
       pp fmt "@[*******************************@]@.";
       pp fmt "@[%a@]@." print_file file);
-    pp fmt "OK\n";
+    let () =
+      if config.paths then print_ids fmt else pp fmt "OK\n" in 
     true
   with W.Error e ->
     let bt = Printexc.get_backtrace () in

bin/check.mli

@@ -8,6 +8,6 @@
 (*  (as described in file LICENSE enclosed).                              *)
 (**************************************************************************)
 
-type config = { verbose : bool; load_path : string list }
+type config = { verbose : bool; paths : bool; load_path : string list }
 
 val run : config -> string list -> bool

bin/cli.ml

@@ -41,22 +41,26 @@ let verbose =
   let doc = "Print all intermediate forms." in
   Arg.(value & flag & info [ "v"; "verbose" ] ~doc)
 
+let paths =
+  let doc = "Print the fully qualified name of all top-level variables." in
+  Arg.(value & flag & info [ "p"; "paths" ] ~doc)
+
 let load_path =
   let doc = "Include directory in load path." in
   Arg.(value & opt_all dir [] & info [ "L"; "load-path" ] ~doc ~docv:"DIR")
 
 let intfs = Arg.(non_empty & pos_all ocaml_intf [] & info [] ~docv:"FILE")
 let files = Arg.(non_empty & pos_all ocaml_file [] & info [] ~docv:"FILE")
 
-let run_check verbose load_path file =
+let run_check verbose load_path paths file =
   let load_path =
     List.fold_left
       (fun acc f ->
         let dir = Filename.dirname f in
         if not (List.mem dir acc) then dir :: acc else acc)
       load_path file
   in
-  let b = Check.run { verbose; load_path } file in
+  let b = Check.run { verbose; paths; load_path } file in
   if not b then exit 125 else ()
 
 let run_dumpast load_path file =
@@ -79,7 +83,7 @@ let dumpast =
 let tc =
   let doc = "Gospel type-checker." in
   let info = Cmd.info "check" ~doc in
-  let term = Term.(const run_check $ verbose $ load_path $ intfs) in
+  let term = Term.(const run_check $ verbose $ load_path $ paths $ intfs) in
   Cmd.v info term
 
 let pps =

epic.txt

@@ -0,0 +1,16 @@
+Path_test
+Path_test
+Path_test
+Path_test
+Path_test
+Path_test.M
+Path_test.M
+Path_test.M
+Path_test.M
+Path_test.M.Nested
+Path_test.M.Nested
+Path_test.M
+Path_test
+Path_test.N
+Path_test.N
+Path_test

src/identifier.ml

@@ -33,6 +33,10 @@ module Ident = struct
     id_tag : int;
   }
 
+  let id_stack = Queue.create ()
+  (* only to be used for testing *)
+  let iter f = Queue.iter f id_stack
+
   let pp =
     let current = Hashtbl.create 0 in
     let output = Hashtbl.create 0 in
@@ -56,15 +60,21 @@ module Ident = struct
   let create =
     let tag = ref 0 in
     fun ?(attrs = []) ?(path=[]) ~loc str ->
-    if path <> [] then (List.iter (fun x -> print_string x; print_char '.') path; print_endline str);
       incr tag;
-      { id_str = str;
-        id_attrs = attrs;
-        id_path = path;
-        id_loc = loc;
-        id_tag = !tag;
-      }
-
+      let id =
+        { id_str = str;
+          id_attrs = attrs;
+          id_path = path;
+          id_loc = loc;
+          id_tag = !tag;
+        } in
+      let () =
+        if path <> [] && 
+          not (List.exists (fun suffix ->
+              String.ends_with ~suffix (List.hd path)) ["Stdlib"; "CamlinternalFormatBasics"; "Gospelstdlib"] )
+        then Queue.push id id_stack else () in
+      id
+
   let of_preid ?(path=[]) (pid : Preid.t) =
     create pid.pid_str ~path ~attrs:pid.pid_attrs ~loc:pid.pid_loc
 

src/identifier.mli

@@ -50,7 +50,8 @@ module Ident : sig
   val compare : t -> t -> int
   val equal : t -> t -> bool
   val hash : t -> int
-
+  val iter : (t -> unit) -> unit
+
   val pp : Format.formatter -> t -> unit
   (** Pretty printer for identifiers. *)
 

src/tast_printer.ml

@@ -378,3 +378,5 @@ and print_modyle_type1 f x =
     | Mod_typeof me -> pp f "@[<hov2>module@ type@ of@ %a@]" module_expr me
     | Mod_extension e -> extension reset_ctxt f e
     | _ -> paren true print_module_type f x
+
+

src/tmodule.ml

@@ -606,3 +606,11 @@ and print_ns nm fmt { ns_ts; ns_ls; ns_fd; ns_xs; ns_ns; ns_tns } =
 let print_file fmt { fl_nm; fl_sigs; fl_export } =
   pp fmt "@[module %a@\n@[<h2>@\n%a@\n@[<hv2>Signatures@\n%a@]@]@]@." Ident.pp
     fl_nm (print_ns fl_nm.id_str) fl_export print_signature fl_sigs
+
+let print_ids fmt =
+    Ident.iter (fun x ->
+          pp fmt "@[%a@]@\n"
+            (list ~sep:(fun fmt () -> pp fmt ".")
+             (fun fmt -> pp fmt "%s")
+            ) x.Ident.id_path
+        ) 

src/typing.ml

@@ -1309,7 +1309,7 @@ and process_mod path penv loc m muc =
   let muc, mty = process_modtype (path@[nm]) penv muc m.mdtype in
   let decl =
     {
-      md_name = Ident.create ~loc:m.mdname.loc nm;
+      md_name = Ident.create ~loc:m.mdname.loc ~path nm;
       md_type = mty;
       md_attrs = m.mdattributes;
       md_loc = m.mdloc;
@@ -1326,7 +1326,7 @@ and process_modtype_decl path penv loc decl muc =
   in
   let decl =
     {
-      mtd_name = Ident.create ~loc:decl.mtdname.loc nm;
+      mtd_name = Ident.create ~path ~loc:decl.mtdname.loc nm;
       mtd_type = mty;
       mtd_attrs = decl.mtdattributes;
       mtd_loc = decl.mtdloc;

test/path/dune

@@ -0,0 +1,3 @@
+(include ../utils/dune.common)
+
+(include dune.inc)

test/path/dune.inc

@@ -0,0 +1,20 @@
+(rule
+ (deps
+  %{bin:gospel}
+  (:checker %{project_root}/test/utils/testchecker.exe))
+ (action
+  (with-outputs-to path_test.mli.output
+   (run %{checker} %{dep:path_test.mli} --p))))
+
+(rule
+ (alias runtest)
+ (action
+  (diff path_test.mli path_test.mli.output)))
+
+(rule
+ (alias test-cmis)
+ (action
+  (chdir %{project_root}
+   ; Syntax sanity check
+   (run ocamlc -c %{dep:path_test.mli}))))
+

test/path/path_test.mli

@@ -0,0 +1,51 @@
+val x : int
+val y : int -> int
+
+type t
+
+val w : t
+
+val z : t -> t
+(*@ r = z arg
+    ensures arg = r *)
+
+module M : sig
+
+  val x : int
+  val y : int -> int
+
+ (*@ function f (n : int) : int *)
+ (*@ axiom a : forall n. f n = n + 1 *)
+
+  module Nested : sig
+    val x : int
+    val y : int -> int
+  end
+end
+
+module N : sig
+
+  val x : int
+  val y : int -> int
+
+end
+
+
+(* {gospel_expected|
+   Path_test
+   Path_test
+   Path_test
+   Path_test
+   Path_test
+   Path_test.M
+   Path_test.M
+   Path_test.M
+   Path_test.M
+   Path_test.M.Nested
+   Path_test.M.Nested
+   Path_test.M
+   Path_test
+   Path_test.N
+   Path_test.N
+   Path_test
+   |gospel_expected} *)

test/utils/dune_gen.ml

@@ -45,14 +45,17 @@ let print_rule file =
       | None -> ("", "")
       | Some prd -> ("(with-accepted-exit-codes " ^ prd ^ "\n    ", ")")
     in
+    let flag =
+      if file = "path_test.mli" then " --p" else "" in
+
     Printf.printf
       {|(rule
  (deps
   %%{bin:gospel}
   (:checker %%{project_root}/test/utils/testchecker.exe)%s)
  (action
   (with-outputs-to %s.output
-   (run %%{checker} %%{dep:%s}))))
+   (run %%{checker} %%{dep:%s}%s))))
 
 (rule
  (alias runtest)
@@ -67,7 +70,7 @@ let print_rule file =
    %s(run ocamlc -c %%{dep:%s})%s)))
 
 |}
-      deps file file file file exit_code_open file exit_code_close
+      deps file file flag file file exit_code_open file exit_code_close
 
 let () =
   let files = Filename.current_dir_name |> Sys.readdir in

test/utils/testchecker.ml

@@ -2,6 +2,8 @@ open Fmt
 
 let result_start = "(* {gospel_expected|"
 
+
+
 let print ppf file =
   let ch = open_in file in
   let rec aux ?(first = false) () =
@@ -15,15 +17,24 @@ let print ppf file =
   aux ~first:true ();
   close_in ch
 
-let test_file file =
+let test_file file flags =
   let stderr = str "%s_stderr" file in
-  let command = str "gospel check %s > %s 2> %s" file Filename.null stderr in
+  let stdout = str "%s_stdout" file in 
+  let command = str "gospel check %s %s > %s 2> %s" flags file stdout stderr in
   let status = Sys.command command in
   pr "%a@\n" print file;
   if status <> 0 then
     pr "(* @[{gospel_expected|@\n[%d] @[%a@]@\n|gospel_expected}@] *)@\n" status
       print stderr
+  else if flags = "--p" then
+    pr "(* @[{gospel_expected|@\n@[%a@]@\n|gospel_expected}@] *)@\n"
+      print stdout
 
 let () =
   let file = Sys.argv.(1) in
-  test_file file
+  let flags =
+    if Array.length Sys.argv > 2 then
+      begin Sys.argv.(2) end
+    else
+      "" in
+  test_file file flags