Exporting more internals from Coq implementation.

1 files changed, 114 insertions, 11 deletions

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