Improve locate API

Author: Gustavo2622

src/ecCommands.ml

@@ -120,8 +120,9 @@ module Loader : sig
 
   val addidir : ?namespace:namespace -> ?recursive:bool -> string -> loader -> unit
   val aslist  : loader -> ((namespace option * string) * idx_t) list
-  val locate  : ?namespaces:namespace option list -> string ->
-                  loader -> (namespace option * string * kind) option
+  val locate  : ?namespaces:namespace option list -> 
+                ?kinds:(EcLoader.kind list) -> string ->
+                 loader -> (namespace option * string * kind) option
 
   val push      : string -> loader -> unit
   val pop       : loader -> string option
@@ -170,8 +171,8 @@ end = struct
   let aslist (ld : loader) =
     EcLoader.aslist ld.ld_core
 
-  let locate ?namespaces (path : string) (ld : loader) =
-    EcLoader.locate ?namespaces path ld.ld_core
+  let locate ?namespaces ?kinds (path : string) (ld : loader) =
+    EcLoader.locate ?namespaces ?kinds path ld.ld_core
 
   let push (p : string) (ld : loader) =
     ld.ld_stack <- norm p :: ld.ld_stack
@@ -522,7 +523,7 @@ and process_th_require1 ld scope (nm, (sysname, thname), io) =
     then [Loader.namespace ld; None]
     else [nm] in
 
-  match Loader.locate ~namespaces:nm sysname ld with
+  match Loader.locate ~kinds:[`Ec; `EcA] ~namespaces:nm sysname ld with
   | None ->
       EcScope.hierror "cannot locate theory `%s'" sysname
 
@@ -557,7 +558,10 @@ and process_th_require1 ld scope (nm, (sysname, thname), io) =
         (fun () -> Pragma.set i_pragma)
       in
 
-      let kind = match kind with `Ec -> `Concrete | `EcA -> `Abstract in
+      let kind = match kind with 
+      | `Ec -> `Concrete | `EcA -> `Abstract 
+      | _ -> assert false 
+      in
 
       let scope = EcScope.Theory.require scope (name, kind) loader in
           match io with

src/ecDoc.ml

@@ -26,8 +26,9 @@ let c_filename ?(ext : string option) (nms : string list) =
 (* -------------------------------------------------------------------- *)
 let thkind_str (kind : EcLoader.kind) : string =
   match kind with
-  | `Ec -> "Theory"
-  | `EcA -> "Abstract Theory"
+  | `Ec   -> "Theory"
+  | `EcA  -> "Abstract Theory"
+  | `Spec -> "Spec File" (* FIXME *)
 
 (* -------------------------------------------------------------------- *)
 let itemkind_str_pl (ik : itemkind) : string =

src/ecEco.ml

@@ -64,13 +64,15 @@ let list_of_json (tx : Json.t -> 'a) (data : Json.t) : 'a list =
 (* -------------------------------------------------------------------- *)
 let kind_to_json (k : EcLoader.kind) =
   match k with
-  | `Ec  -> `String "ec"
-  | `EcA -> `String "eca"
+  | `Ec   -> `String "ec"
+  | `EcA  -> `String "eca"
+  | `Spec -> `String "spec"
 
 let kind_of_json (data : Json.t) =
   match data with
-  | `String "ec"  -> `Ec
-  | `String "eca" -> `EcA
+  | `String "ec"   -> `Ec
+  | `String "eca"  -> `EcA
+  | `String "spec" -> `Spec
   | _ -> raise InvalidEco
 
 (* -------------------------------------------------------------------- *)

src/ecLoader.ml

@@ -114,7 +114,7 @@ let check_case idir name (dev, ino) =
     with Unix.Unix_error _ -> None
 
 (* -------------------------------------------------------------------- *)
-let locate ?(namespaces = [None]) (name : string) (ecl : ecloader) =
+let locate ?(namespaces = [None]) ?(kinds = [`Ec; `EcA]) (name : string) (ecl : ecloader) =
   if not (EcRegexp.match_ (`S "^[a-zA-Z0-9_]+$") name) then
     None
   else
@@ -157,7 +157,7 @@ let locate ?(namespaces = [None]) (name : string) (ecl : ecloader) =
     match
       List.rev_pmap
         (fun kind -> List.opick (locate kind) ecl.ecl_idirs)
-        [`Ec; `EcA; `Spec]
+        kinds
     with
     | [x] -> Some x
     | _   -> None

src/ecLoader.mli

@@ -18,4 +18,4 @@ val aslist  : ecloader -> ((namespace option * string) * idx_t) list
 val dup     : ecloader -> ecloader
 val forsys  : ecloader -> ecloader
 val addidir : ?namespace:namespace -> ?recursive:bool -> string -> ecloader -> unit
-val locate  : ?namespaces:(namespace option) list -> string -> ecloader -> (namespace option * string * kind) option
+val locate  : ?namespaces:(namespace option) list -> ?kinds:(kind list) -> string -> ecloader -> (namespace option * string * kind) option