src/tac2stdlib.ml


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
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 ())