Extending the Coq API in Ltac2.

4 files changed, 91 insertions, 1 deletions

diff --git a/Constr.v b/Constr.v
index 994f9bf3ac..9e5833a778 100644
--- a/Constr.v
+++ b/Constr.v
@@ -7,3 +7,37 @@
 (************************************************************************)
 
 Require Import Coq.ltac2.Init.
+
+Ltac2 @ external type : constr -> constr := "ltac2" "constr_type".
+(** Return the type of a term *)
+
+Ltac2 @ external equal : constr -> constr -> bool := "ltac2" "constr_equal".
+(** Strict syntactic equality: only up to α-conversion and evar expansion *)
+
+Module Unsafe.
+
+(** Low-level access to kernel term. Use with care! *)
+
+Ltac2 Type kind := [
+| Rel (int)
+| Var (ident)
+| Meta (meta)
+| Evar (evar, constr list)
+| Sort (sort)
+| Cast (constr, cast, constr)
+| Prod (ident option, constr, constr)
+| Lambda (ident option, constr, constr)
+| LetIn (ident option, constr, constr, constr)
+| App (constr, constr list)
+| Constant (constant, instance)
+| Ind (inductive, instance)
+| Constructor (inductive, instance)
+(*
+  | Case      of case_info * 'constr * 'constr * 'constr array
+  | Fix       of ('constr, 'types) pfixpoint
+  | CoFix     of ('constr, 'types) pcofixpoint
+*)
+| Proj (projection, constr)
+].
+
+End Unsafe.
diff --git a/Control.v b/Control.v
index a476513ede..6b3b360abb 100644
--- a/Control.v
+++ b/Control.v
@@ -28,6 +28,11 @@ Ltac2 @ external focus : int -> int -> (unit -> 'a) -> 'a := "ltac2" "focus".
 Ltac2 @ external shelve : unit -> unit := "ltac2" "shelve".
 Ltac2 @ external shelve_unifiable : unit -> unit := "ltac2" "shelve_unifiable".
 
+Ltac2 @ external new_goal : evar -> unit := "ltac2" "new_goal".
+(** Adds the given evar to the list of goals as the last one. If it is
+    already defined in the current state, don't do anything. Panics if the
+    evar is not in the current state. *)
+
 (** Goal inspection *)
 
 Ltac2 @ external goal : unit -> constr := "ltac2" "goal".
diff --git a/Init.v b/Init.v
index 8ff5837bb4..1d2d40f5c0 100644
--- a/Init.v
+++ b/Init.v
@@ -15,10 +15,20 @@ Global Set Default Proof Mode "Ltac2".
 Ltac2 Type int.
 Ltac2 Type string.
 Ltac2 Type char.
+Ltac2 Type ident.
 
+(** Constr-specific built-in types *)
+Ltac2 Type meta.
 Ltac2 Type evar.
+Ltac2 Type sort.
+Ltac2 Type cast.
+Ltac2 Type instance.
+Ltac2 Type constant.
+Ltac2 Type inductive.
+Ltac2 Type constructor.
+Ltac2 Type projection.
 Ltac2 Type constr.
-Ltac2 Type ident.
+
 Ltac2 Type message.
 Ltac2 Type exn := [ .. ].
 Ltac2 Type 'a array.
diff --git a/tac2core.ml b/tac2core.ml
index 13395c87b3..94758eb217 100644
--- a/tac2core.ml
+++ b/tac2core.ml
@@ -136,6 +136,9 @@ let err_notfocussed =
 let err_outofbounds =
   LtacError (coq_core "Out_of_bounds", [||])
 
+let err_notfound =
+  LtacError (coq_core "Not_found", [||])
+
 (** Helper functions *)
 
 let thaw f = interp_app f [v_unit]
@@ -270,6 +273,31 @@ let prm_string_get : ml_tactic = function
   else wrap (fun () -> Value.of_char (Bytes.get s n))
 | _ -> assert false
 
+(** Terms *)
+
+(** constr -> constr *)
+let prm_constr_type : ml_tactic = function
+| [c] ->
+  let c = Value.to_constr c in
+  let get_type env sigma =
+  Proofview.V82.wrap_exceptions begin fun () ->
+    let (sigma, t) = Typing.type_of env sigma c in
+    let t = Value.of_constr t in
+    Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t
+  end in
+  pf_apply get_type
+| _ -> assert false
+
+(** constr -> constr *)
+let prm_constr_equal : ml_tactic = function
+| [c1; c2] ->
+  let c1 = Value.to_constr c1 in
+  let c2 = Value.to_constr c2 in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let b = EConstr.eq_constr sigma c1 c2 in
+  Proofview.tclUNIT (Value.of_bool b)
+| _ -> assert false
+
 (** Error *)
 
 let prm_throw : ml_tactic = function
@@ -342,6 +370,15 @@ let prm_shelve_unifiable : ml_tactic = function
 | [_] -> Proofview.shelve_unifiable >>= fun () -> return v_unit
 | _ -> assert false
 
+let prm_new_goal : ml_tactic = function
+| [ev] ->
+  let ev = Evar.unsafe_of_int (Value.to_int ev) in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  if Evd.mem sigma ev then
+    Proofview.Unsafe.tclNEWGOALS [ev] <*> Proofview.tclUNIT v_unit
+  else throw err_notfound
+| _ -> assert false
+
 (** unit -> constr *)
 let prm_goal : ml_tactic = function
 | [_] ->
@@ -391,6 +428,9 @@ let () = Tac2env.define_primitive (pname "string_length") prm_string_length
 let () = Tac2env.define_primitive (pname "string_get") prm_string_get
 let () = Tac2env.define_primitive (pname "string_set") prm_string_set
 
+let () = Tac2env.define_primitive (pname "constr_type") prm_constr_type
+let () = Tac2env.define_primitive (pname "constr_equal") prm_constr_equal
+
 let () = Tac2env.define_primitive (pname "int_equal") prm_int_equal
 let () = Tac2env.define_primitive (pname "int_compare") prm_int_compare
 let () = Tac2env.define_primitive (pname "int_neg") prm_int_neg
@@ -410,6 +450,7 @@ let () = Tac2env.define_primitive (pname "enter") prm_enter
 let () = Tac2env.define_primitive (pname "focus") prm_focus
 let () = Tac2env.define_primitive (pname "shelve") prm_shelve
 let () = Tac2env.define_primitive (pname "shelve_unifiable") prm_shelve_unifiable
+let () = Tac2env.define_primitive (pname "new_goal") prm_new_goal
 let () = Tac2env.define_primitive (pname "goal") prm_goal
 let () = Tac2env.define_primitive (pname "hyp") prm_hyp
 let () = Tac2env.define_primitive (pname "refine") prm_refine