Exporting more internals from Coq implementation.

7 files changed, 185 insertions, 21 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index f28c5c5dcf..515cadc525 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -557,6 +557,14 @@ let prm_refine : ml_tactic = function
   end >>= fun () -> return v_unit
 | _ -> assert false
 
+let prm_with_holes : ml_tactic = function
+| [x; f] ->
+  Proofview.tclEVARMAP >>= fun sigma0 ->
+  thaw x >>= fun ans ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.Unsafe.tclEVARS sigma0 >>= fun () ->
+  Tacticals.New.tclWITHHOLES false (interp_app f [ans]) sigma
+| _ -> assert false
 
 (** Registering *)
 
@@ -615,6 +623,7 @@ let () = Tac2env.define_primitive (pname "goal") prm_goal
 let () = Tac2env.define_primitive (pname "hyp") prm_hyp
 let () = Tac2env.define_primitive (pname "hyps") prm_hyps
 let () = Tac2env.define_primitive (pname "refine") prm_refine
+let () = Tac2env.define_primitive (pname "with_holes") prm_with_holes
 
 (** ML types *)
 
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 2094898ced..a75500eae7 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -239,6 +239,9 @@ let interp_ml_object t = MLType.obj t
 let coq_prefix =
   MPfile (DirPath.make (List.map Id.of_string ["Init"; "Ltac2"]))
 
+let std_prefix =
+  MPfile (DirPath.make (List.map Id.of_string ["Std"; "Ltac2"]))
+
 (** Generic arguments *)
 
 let wit_ltac2 = Genarg.make0 "ltac2"
diff --git a/src/tac2env.mli b/src/tac2env.mli
index e26109b691..fea03c4285 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -106,6 +106,9 @@ val interp_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object
 val coq_prefix : ModPath.t
 (** Path where primitive datatypes are defined in Ltac2 plugin. *)
 
+val std_prefix : ModPath.t
+(** Path where Ltac-specific datatypes are defined in Ltac2 plugin. *)
+
 (** {5 Generic arguments} *)
 
 val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 0aeccbd9c6..7c7b539113 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
 open Locus
 open Misctypes
 open Tac2expr
@@ -14,6 +15,57 @@ open Proofview.Notations
 
 module Value = Tac2ffi
 
+let to_pair f g = function
+| ValBlk (0, [| x; y |]) -> (f x, g y)
+| _ -> assert false
+
+let to_name c = match Value.to_option Value.to_ident c with
+| None -> Anonymous
+| Some id -> Name id
+
+let to_qhyp = function
+| ValBlk (0, [| i |]) -> AnonHyp (Value.to_int i)
+| ValBlk (1, [| id |]) -> NamedHyp (Value.to_ident id)
+| _ -> assert false
+
+let to_bindings = function
+| ValInt 0 -> NoBindings
+| ValBlk (0, [| vl |]) ->
+  ImplicitBindings (Value.to_list Value.to_constr vl)
+| ValBlk (1, [| vl |]) ->
+  ExplicitBindings ((Value.to_list (fun p -> None, to_pair to_qhyp Value.to_constr p) vl))
+| _ -> assert false
+
+let to_constr_with_bindings = function
+| ValBlk (0, [| c; bnd |]) -> (Value.to_constr c, to_bindings bnd)
+| _ -> assert false
+
+let to_int_or_var i = ArgArg (Value.to_int i)
+
+let to_occurrences f = function
+| ValInt 0 -> AllOccurrences
+| ValBlk (0, [| vl |]) -> AllOccurrencesBut (Value.to_list f vl)
+| ValInt 1 -> NoOccurrences
+| ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list f vl)
+| _ -> assert false
+
+let to_hyp_location_flag = function
+| ValInt 0 -> InHyp
+| ValInt 1 -> InHypTypeOnly
+| ValInt 2 -> InHypValueOnly
+| _ -> assert false
+
+let to_clause = function
+| ValBlk (0, [| hyps; concl |]) ->
+  let cast = function
+  | ValBlk (0, [| hyp; occ; flag |]) ->
+    ((to_occurrences to_int_or_var occ, Value.to_ident hyp), to_hyp_location_flag flag)
+  | _ -> assert false
+  in
+  let hyps = Value.to_option (fun h -> Value.to_list cast h) hyps in
+  { onhyps = hyps; concl_occs = to_occurrences to_int_or_var concl; }
+| _ -> assert false
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -50,6 +102,29 @@ let define_prim2 name tac =
   in
   Tac2env.define_primitive (pname name) tac
 
+(** Tactics from Tacexpr *)
+
+let () = define_prim2 "tac_eelim" begin fun c copt ->
+  let c = to_constr_with_bindings c in
+  let copt = Value.to_option to_constr_with_bindings copt in
+  Tactics.elim true None c copt
+end
+
+let () = define_prim1 "tac_ecase" begin fun c ->
+  let c = to_constr_with_bindings c in
+  Tactics.general_case_analysis true None c
+end
+
+let () = define_prim1 "tac_egeneralize" begin fun cl ->
+  let cast = function
+  | ValBlk (0, [| c; occs; na |]) ->
+    ((to_occurrences Value.to_int c, Value.to_constr c), to_name na)
+  | _ -> assert false
+  in
+  let cl = Value.to_list cast cl in
+  Tactics.new_generalize_gen cl
+end
+
 (** Tactics from coretactics *)
 
 let () = define_prim0 "tac_reflexivity" Tactics.intros_reflexivity
@@ -76,10 +151,26 @@ let () = define_prim1 "tac_cut" begin fun c ->
   Tactics.cut c
 end
 
-let () = define_prim0 "tac_left" (Tactics.left_with_bindings false NoBindings)
-let () = define_prim0 "tac_eleft" (Tactics.left_with_bindings true NoBindings)
-let () = define_prim0 "tac_right" (Tactics.right_with_bindings false NoBindings)
-let () = define_prim0 "tac_eright" (Tactics.right_with_bindings true NoBindings)
+let () = define_prim1 "tac_left" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.left_with_bindings false bnd
+end
+let () = define_prim1 "tac_eleft" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.left_with_bindings true bnd
+end
+let () = define_prim1 "tac_right" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.right_with_bindings false bnd
+end
+let () = define_prim1 "tac_eright" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.right_with_bindings true bnd
+end
+
+let () = define_prim1 "tac_introsuntil" begin fun h ->
+  Tactics.intros_until (to_qhyp h)
+end
 
 let () = define_prim1 "tac_exactnocheck" begin fun c ->
   Tactics.exact_no_check (Value.to_constr c)
@@ -96,20 +187,32 @@ end
 let () = define_prim0 "tac_constructor" (Tactics.any_constructor false None)
 let () = define_prim0 "tac_econstructor" (Tactics.any_constructor true None)
 
-let () = define_prim1 "tac_constructorn" begin fun n ->
+let () = define_prim2 "tac_constructorn" begin fun n bnd ->
   let n = Value.to_int n in
-  Tactics.constructor_tac false None n NoBindings
+  let bnd = to_bindings bnd in
+  Tactics.constructor_tac false None n bnd
 end
 
-let () = define_prim1 "tac_econstructorn" begin fun n ->
+let () = define_prim2 "tac_econstructorn" begin fun n bnd ->
   let n = Value.to_int n in
-  Tactics.constructor_tac true None n NoBindings
+  let bnd = to_bindings bnd in
+  Tactics.constructor_tac true None n bnd
 end
 
-let () = define_prim0 "tac_symmetry" (Tactics.intros_symmetry Locusops.onConcl)
+let () = define_prim1 "tac_symmetry" begin fun cl ->
+  let cl = to_clause cl in
+  Tactics.intros_symmetry cl
+end
 
-let () = define_prim0 "tac_split" (Tactics.split_with_bindings false [NoBindings])
-let () = define_prim0 "tac_esplit" (Tactics.split_with_bindings true [NoBindings])
+let () = define_prim1 "tac_split" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.split_with_bindings false [bnd]
+end
+
+let () = define_prim1 "tac_esplit" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.split_with_bindings true [bnd]
+end
 
 let () = define_prim1 "tac_rename" begin fun ids ->
   let map c = match Value.to_tuple c with
diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v
index 4950a20ec4..35546ef6c1 100644
--- a/tests/stuff/ltac2.v
+++ b/tests/stuff/ltac2.v
@@ -120,7 +120,6 @@ Abort.
 
 Goal True.
 Proof.
-
 let x () := plus (fun () => 0) (fun _ => 1) in
 match case x with
 | Val x =>
@@ -131,6 +130,13 @@ match case x with
 end.
 Abort.
 
+Goal (forall n : nat, n = 0 -> False) -> True.
+Proof.
+refine (fun () => '(fun H => _)).
+Std.ecase (hyp @H, Std.ExplicitBindings [Std.NamedHyp @n, '0]).
+refine (fun () => 'eq_refl).
+Qed.
+
 Ltac2 rec do n tac := match Int.equal n 0 with
 | true => ()
 | false => tac (); do (Int.sub n 1) tac
diff --git a/theories/Control.v b/theories/Control.v
index a6d46a89a8..a8b92aced2 100644
--- a/theories/Control.v
+++ b/theories/Control.v
@@ -54,3 +54,10 @@ Ltac2 @ external hyps : unit -> (ident * constr option * constr) list := "ltac2"
 (** Refinement *)
 
 Ltac2 @ external refine : (unit -> constr) -> unit := "ltac2" "refine".
+
+(** Evars *)
+
+Ltac2 @ external with_holes : (unit -> 'a) -> ('a -> 'b) -> 'b := "ltac2" "with_holes".
+(** [with_holes x f] evaluates [x], then apply [f] to the result, and fails if
+    all evars generated by the call to [x] have not been solved when [f]
+    returns. *)
diff --git a/theories/Std.v b/theories/Std.v
index 5cc1622ba9..a9eced6cbb 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -8,8 +8,39 @@
 
 Require Import Ltac2.Init.
 
+(** ML-facing types *)
+
+Ltac2 Type hypothesis := [ AnonHyp (int) | NamedHyp (ident) ].
+
+Ltac2 Type bindings := [
+| NoBindings
+| ImplicitBindings (constr list)
+| ExplicitBindings ((hypothesis * constr) list)
+].
+
+Ltac2 Type constr_with_bindings := constr * bindings.
+
+Ltac2 Type occurrences := [
+| AllOccurrences
+| AllOccurrencesBut (int list)
+| NoOccurrences
+| OnlyOccurrences (int list)
+].
+
+Ltac2 Type hyp_location_flag := [ InHyp | InHypTypeOnly | InHypValueOnly ].
+
+Ltac2 Type clause := {
+  on_hyps : (ident * occurrences * hyp_location_flag) list option;
+  on_concl : occurrences;
+}.
+
 (** Standard, built-in tactics. See Ltac1 for documentation. *)
 
+Ltac2 @ external eelim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_eelim".
+Ltac2 @ external ecase : constr_with_bindings -> unit := "ltac2" "tac_ecase".
+
+Ltac2 @ external egeneralize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_egeneralize".
+
 Ltac2 @ external reflexivity : unit -> unit := "ltac2" "tac_reflexivity".
 
 Ltac2 @ external assumption : unit -> unit := "ltac2" "tac_assumption".
@@ -20,20 +51,22 @@ Ltac2 @ external etransitivity : unit -> unit := "ltac2" "tac_etransitivity".
 
 Ltac2 @ external cut : constr -> unit := "ltac2" "tac_cut".
 
-Ltac2 @ external left : unit -> unit := "ltac2" "tac_left".
-Ltac2 @ external eleft : unit -> unit := "ltac2" "tac_eleft".
-Ltac2 @ external right : unit -> unit := "ltac2" "tac_right".
-Ltac2 @ external eright : unit -> unit := "ltac2" "tac_eright".
+Ltac2 @ external left : bindings -> unit := "ltac2" "tac_left".
+Ltac2 @ external eleft : bindings -> unit := "ltac2" "tac_eleft".
+Ltac2 @ external right : bindings -> unit := "ltac2" "tac_right".
+Ltac2 @ external eright : bindings -> unit := "ltac2" "tac_eright".
 
 Ltac2 @ external constructor : unit -> unit := "ltac2" "tac_constructor".
 Ltac2 @ external econstructor : unit -> unit := "ltac2" "tac_econstructor".
-Ltac2 @ external split : unit -> unit := "ltac2" "tac_split".
-Ltac2 @ external esplit : unit -> unit := "ltac2" "tac_esplit".
+Ltac2 @ external split : bindings -> unit := "ltac2" "tac_split".
+Ltac2 @ external esplit : bindings -> unit := "ltac2" "tac_esplit".
+
+Ltac2 @ external constructor_n : int -> bindings -> unit := "ltac2" "tac_constructorn".
+Ltac2 @ external econstructor_n : int -> bindings -> unit := "ltac2" "tac_econstructorn".
 
-Ltac2 @ external constructor_n : int -> unit := "ltac2" "tac_constructorn".
-Ltac2 @ external econstructor_n : int -> unit := "ltac2" "tac_econstructorn".
+Ltac2 @ external intros_until : hypothesis -> unit := "ltac2" "tac_introsuntil".
 
-Ltac2 @ external symmetry : unit -> unit := "ltac2" "tac_symmetry".
+Ltac2 @ external symmetry : clause -> unit := "ltac2" "tac_symmetry".
 
 Ltac2 @ external rename : (ident * ident) list -> unit := "ltac2" "tac_rename".