diff options
| -rw-r--r-- | _CoqProject | 3 | ||||
| -rw-r--r-- | src/ltac2_plugin.mlpack | 1 | ||||
| -rw-r--r-- | src/tac2stdlib.ml | 166 | ||||
| -rw-r--r-- | src/tac2stdlib.mli | 9 | ||||
| -rw-r--r-- | theories/Ltac2.v | 1 | ||||
| -rw-r--r-- | theories/Std.v | 59 |
6 files changed, 239 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 90338abbfb..6d3470cfa7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -15,6 +15,8 @@ src/tac2entries.ml src/tac2entries.mli src/tac2core.ml src/tac2core.mli +src/tac2stdlib.ml +src/tac2stdlib.mli src/g_ltac2.ml4 src/ltac2_plugin.mlpack @@ -25,4 +27,5 @@ theories/Array.v theories/Control.v theories/Message.v theories/Constr.v +theories/Std.v theories/Ltac2.v diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack index 3d87a8cddb..dc78207291 100644 --- a/src/ltac2_plugin.mlpack +++ b/src/ltac2_plugin.mlpack @@ -4,4 +4,5 @@ Tac2intern Tac2interp Tac2entries Tac2core +Tac2stdlib G_ltac2 diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml new file mode 100644 index 0000000000..89a8d98693 --- /dev/null +++ b/src/tac2stdlib.ml @@ -0,0 +1,166 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +open Locus +open Misctypes +open Tac2expr +open Tac2core +open Proofview.Notations + +(** Standard tactics sharing their implementation with Ltac1 *) + +let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s } + +let return x = Proofview.tclUNIT x +let v_unit = Tac2core.Value.of_unit () + +let lift tac = tac <*> return v_unit + +let wrap f = + return () >>= fun () -> return (f ()) + +let wrap_unit f = + return () >>= fun () -> f (); return v_unit + +let define_prim0 name tac = + let tac = function + | [_] -> lift tac + | _ -> assert false + in + Tac2env.define_primitive (pname name) tac + +let define_prim1 name tac = + let tac = function + | [x] -> lift (tac x) + | _ -> assert false + in + Tac2env.define_primitive (pname name) tac + +let define_prim2 name tac = + let tac = function + | [x; y] -> lift (tac x y) + | _ -> assert false + in + Tac2env.define_primitive (pname name) tac + +(** Tactics from coretactics *) + +let () = define_prim0 "tac_reflexivity" Tactics.intros_reflexivity + +(* + +TACTIC EXTEND exact + [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] +END + +*) + +let () = define_prim0 "tac_assumption" Tactics.assumption + +let () = define_prim1 "tac_transitivity" begin fun c -> + let c = Value.to_constr c in + Tactics.intros_transitivity (Some c) +end + +let () = define_prim0 "tac_etransitivity" (Tactics.intros_transitivity None) + +let () = define_prim1 "tac_cut" begin fun c -> + let c = Value.to_constr c in + 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_exactnocheck" begin fun c -> + Tactics.exact_no_check (Value.to_constr c) +end + +let () = define_prim1 "tac_vmcastnocheck" begin fun c -> + Tactics.vm_cast_no_check (Value.to_constr c) +end + +let () = define_prim1 "tac_nativecastnocheck" begin fun c -> + Tactics.native_cast_no_check (Value.to_constr c) +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 n = Value.to_int n in + Tactics.constructor_tac false None n NoBindings +end + +let () = define_prim1 "tac_econstructorn" begin fun n -> + let n = Value.to_int n in + Tactics.constructor_tac true None n NoBindings +end + +let () = define_prim0 "tac_symmetry" (Tactics.intros_symmetry Locusops.onConcl) + +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_rename" begin fun ids -> + let ids = Value.to_list ids in + let map c = match Value.to_tuple c with + | [|x; y|] -> (Value.to_ident x, Value.to_ident y) + | _ -> assert false + in + let ids = List.map map ids in + Tactics.rename_hyp ids +end + +let () = define_prim1 "tac_revert" begin fun ids -> + let ids = List.map Value.to_ident (Value.to_list ids) in + Tactics.revert ids +end + +let () = define_prim0 "tac_admit" Proofview.give_up + +let () = define_prim2 "tac_fix" begin fun idopt n -> + let idopt = Option.map Value.to_ident (Value.to_option idopt) in + let n = Value.to_int n in + Tactics.fix idopt n +end + +let () = define_prim1 "tac_cofix" begin fun idopt -> + let idopt = Option.map Value.to_ident (Value.to_option idopt) in + Tactics.cofix idopt +end + +let () = define_prim1 "tac_clear" begin fun ids -> + let ids = List.map Value.to_ident (Value.to_list ids) in + Tactics.clear ids +end + +let () = define_prim1 "tac_keep" begin fun ids -> + let ids = List.map Value.to_ident (Value.to_list ids) in + Tactics.keep ids +end + +let () = define_prim1 "tac_clearbody" begin fun ids -> + let ids = List.map Value.to_ident (Value.to_list ids) in + Tactics.clear_body ids +end + +(** Tactics from extratactics *) + +let () = define_prim1 "tac_absurd" begin fun c -> + Contradiction.absurd (Value.to_constr c) +end + +let () = define_prim1 "tac_subst" begin fun ids -> + let ids = List.map Value.to_ident (Value.to_list ids) in + Equality.subst ids +end + +let () = define_prim0 "tac_substall" (return () >>= fun () -> Equality.subst_all ()) diff --git a/src/tac2stdlib.mli b/src/tac2stdlib.mli new file mode 100644 index 0000000000..927b57074d --- /dev/null +++ b/src/tac2stdlib.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Standard tactics sharing their implementation with Ltac1 *) diff --git a/theories/Ltac2.v b/theories/Ltac2.v index 221f7be424..4cd3fafcb2 100644 --- a/theories/Ltac2.v +++ b/theories/Ltac2.v @@ -14,3 +14,4 @@ Require Ltac2.Array. Require Ltac2.Message. Require Ltac2.Constr. Require Ltac2.Control. +Require Ltac2.Std. diff --git a/theories/Std.v b/theories/Std.v new file mode 100644 index 0000000000..5cc1622ba9 --- /dev/null +++ b/theories/Std.v @@ -0,0 +1,59 @@ +(************************************************************************) +(* 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. + +(** Standard, built-in tactics. See Ltac1 for documentation. *) + +Ltac2 @ external reflexivity : unit -> unit := "ltac2" "tac_reflexivity". + +Ltac2 @ external assumption : unit -> unit := "ltac2" "tac_assumption". + +Ltac2 @ external transitivity : constr -> unit := "ltac2" "tac_transitivity". + +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 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 constructor_n : int -> unit := "ltac2" "tac_constructorn". +Ltac2 @ external econstructor_n : int -> unit := "ltac2" "tac_econstructorn". + +Ltac2 @ external symmetry : unit -> unit := "ltac2" "tac_symmetry". + +Ltac2 @ external rename : (ident * ident) list -> unit := "ltac2" "tac_rename". + +Ltac2 @ external revert : ident list -> unit := "ltac2" "tac_revert". + +Ltac2 @ external admit : unit -> unit := "ltac2" "tac_admit". + +Ltac2 @ external fix_ : ident option -> int -> unit := "ltac2" "tac_fix". +Ltac2 @ external cofix_ : ident option -> unit := "ltac2" "tac_cofix". + +Ltac2 @ external clear : ident list -> unit := "ltac2" "tac_clear". +Ltac2 @ external keep : ident list -> unit := "ltac2" "tac_keep". + +Ltac2 @ external clearbody : ident list -> unit := "ltac2" "tac_clearbody". + +Ltac2 @ external exact_no_check : constr -> unit := "ltac2" "tac_exactnocheck". +Ltac2 @ external vm_cast_no_check : constr -> unit := "ltac2" "tac_vmcastnocheck". +Ltac2 @ external native_cast_no_check : constr -> unit := "ltac2" "tac_nativecastnocheck". + +Ltac2 @ external absurd : constr -> unit := "ltac2" "tac_absurd". + +Ltac2 @ external subst : ident list -> unit := "ltac2" "tac_subst". +Ltac2 @ external subst_all : unit -> unit := "ltac2" "tac_substall". |