Adding environment-manipulating functions.

5 files changed, 87 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 5af42197ea..15e02a6484 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,5 +44,6 @@ theories/Constr.v
 theories/Pattern.v
 theories/Fresh.v
 theories/Std.v
+theories/Env.v
 theories/Notations.v
 theories/Ltac2.v
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 13265ee080..8a7d2034fc 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -494,6 +494,26 @@ let () = define3 "constr_closenl" (list ident) int constr begin fun ids k c ->
   return (Value.of_constr ans)
 end
 
+let () = define1 "constr_case" (repr_ext val_inductive) begin fun ind ->
+  Proofview.tclENV >>= fun env ->
+  try
+    let ans = Inductiveops.make_case_info env ind Constr.RegularStyle in
+    return (Value.of_ext Value.val_case ans)
+  with e when CErrors.noncritical e ->
+    throw err_notfound
+end
+
+let () = define2 "constr_constructor" (repr_ext val_inductive) int begin fun (ind, i) k ->
+  Proofview.tclENV >>= fun env ->
+  try
+    let open Declarations in
+    let ans = Environ.lookup_mind ind env in
+    let _ = ans.mind_packets.(i).mind_consnames.(k) in
+    return (Value.of_ext val_constructor ((ind, i), (k + 1)))
+  with e when CErrors.noncritical e ->
+    throw err_notfound
+end
+
 let () = define3 "constr_in_context" ident constr closure begin fun id t c ->
   Proofview.Goal.goals >>= function
   | [gl] ->
@@ -801,6 +821,42 @@ let () = define2 "fresh_fresh" (repr_ext val_free) ident begin fun avoid id ->
   return (Value.of_ident nid)
 end
 
+(** Env *)
+
+let () = define1 "env_get" (list ident) begin fun ids ->
+  let r = match ids with
+  | [] -> None
+  | _ :: _ as ids ->
+    let (id, path) = List.sep_last ids in
+    let path = DirPath.make (List.rev path) in
+    let fp = Libnames.make_path path id in
+    try Some (Nametab.global_of_path fp) with Not_found -> None
+  in
+  return (Value.of_option Value.of_reference r)
+end
+
+let () = define1 "env_expand" (list ident) begin fun ids ->
+  let r = match ids with
+  | [] -> []
+  | _ :: _ as ids ->
+    let (id, path) = List.sep_last ids in
+    let path = DirPath.make (List.rev path) in
+    let qid = Libnames.make_qualid path id in
+    Nametab.locate_all qid
+  in
+  return (Value.of_list Value.of_reference r)
+end
+
+let () = define1 "env_path" reference begin fun r ->
+  match Nametab.path_of_global r with
+  | fp ->
+    let (path, id) = Libnames.repr_path fp in
+    let path = DirPath.repr path in
+    return (Value.of_list Value.of_ident (List.rev_append path [id]))
+  | exception Not_found ->
+    throw err_notfound
+end
+
 (** ML types *)
 
 let constr_flags () =
diff --git a/theories/Constr.v b/theories/Constr.v
index 072c613920..d8d222730e 100644
--- a/theories/Constr.v
+++ b/theories/Constr.v
@@ -57,6 +57,13 @@ Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "con
 (** [closenl [x₁;...;xₙ] k c] abstracts over variables [x₁;...;xₙ] and replaces them with
     [Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *)
 
+Ltac2 @ external case : inductive -> case := "ltac2" "constr_case".
+(** Generate the case information for a given inductive type. *)
+
+Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "constr_constructor".
+(** Generate the i-th constructor for a given inductive type. Indexing starts
+    at 0. Panics if there is no such constructor. *)
+
 End Unsafe.
 
 Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context".
diff --git a/theories/Env.v b/theories/Env.v
new file mode 100644
index 0000000000..7e36aa7990
--- /dev/null
+++ b/theories/Env.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+Require Import Std.
+
+Ltac2 @ external get : ident list -> Std.reference option := "ltac2" "env_get".
+(** Returns the global reference corresponding to the absolute name given as
+    argument if it exists. *)
+
+Ltac2 @ external expand : ident list -> Std.reference list := "ltac2" "env_expand".
+(** Returns the list of all global references whose absolute name contains
+    the argument list as a prefix. *)
+
+Ltac2 @ external path : Std.reference -> ident list := "ltac2" "env_path".
+(** Returns the absolute name of the given reference. Panics if the reference
+    does not exist. *)
diff --git a/theories/Ltac2.v b/theories/Ltac2.v
index 7b2f592ac6..3fe71f4c65 100644
--- a/theories/Ltac2.v
+++ b/theories/Ltac2.v
@@ -18,4 +18,5 @@ Require Ltac2.Control.
 Require Ltac2.Fresh.
 Require Ltac2.Pattern.
 Require Ltac2.Std.
+Require Ltac2.Env.
 Require Export Ltac2.Notations.