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
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
open Genarg
open Geninterp
open Ltac2_plugin
open Tac2ffi
open Tac2expr
open Proofview.Notations
open Tac2externals
let ltac2_ltac1_plugin = "rocq-runtime.plugins.ltac2_ltac1"
let pname ?(plugin=ltac2_ltac1_plugin) s = { mltac_plugin = plugin; mltac_tactic = s }
let define ?plugin s = define (pname ?plugin s)
let val_tag wit = match val_tag wit with
| Base t -> t
| _ -> assert false
let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
let Val.Dyn (t', x) = v in
match Val.eq t t' with
| None -> None
| Some Refl -> Some x
let in_gen wit v = Val.Dyn (val_tag wit, v)
let out_gen wit v = prj (val_tag wit) v
let () =
define "ltac1_of_intro_pattern" (Tac2stdlib.intro_pattern @-> ret Tac2quote_ltac1.ltac1) @@ fun v ->
let v = Tac2tactics.mk_intro_pattern v in
in_gen (topwit Ltac_plugin.Tacarg.wit_simple_intropattern) v
let rec to_intro_pattern (v : Tactypes.intro_pattern) : Tac2types.intro_pattern =
match v.CAst.v with
| IntroForthcoming b -> IntroForthcoming b
| IntroNaming pat -> IntroNaming (to_intro_pattern_naming pat)
| IntroAction act -> IntroAction (to_intro_pattern_action act)
(* these types have the same definition but aren't equal *)
and to_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Tac2types.intro_pattern_naming = function
| IntroIdentifier id -> IntroIdentifier id
| IntroFresh id -> IntroFresh id
| IntroAnonymous -> IntroAnonymous
and to_intro_pattern_action : Tactypes.delayed_open_constr Tactypes.intro_pattern_action_expr -> Tac2types.intro_pattern_action = function
| IntroWildcard -> IntroWildcard
| IntroOrAndPattern op -> IntroOrAndPattern (to_or_and_intro_pattern op)
| IntroInjection inj -> IntroInjection (to_intro_patterns inj)
| IntroApplyOn ({loc;v=c}, ipat) ->
let c =
let open Proofview in
Goal.enter_one ~__LOC__ @@ fun gl ->
let sigma, c = c (Goal.env gl) (Goal.sigma gl) in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
tclUNIT c
in
let c () = c in
IntroApplyOn (c, to_intro_pattern ipat)
| IntroRewrite b -> IntroRewrite b
and to_or_and_intro_pattern : Tactypes.delayed_open_constr Tactypes.or_and_intro_pattern_expr -> Tac2types.or_and_intro_pattern = function
| IntroOrPattern ill -> IntroOrPattern (List.map to_intro_patterns ill)
| IntroAndPattern il -> IntroAndPattern (to_intro_patterns il)
and to_intro_patterns v = List.map to_intro_pattern v
let () =
define "ltac1_to_intro_pattern" (Tac2quote_ltac1.ltac1 @-> ret (option Tac2stdlib.intro_pattern)) @@ fun v ->
(* should we be using Taccoerce.coerce_to_intro_pattern instead?
semantics are different: it also handles wit_hyp and Var constr *)
match out_gen (topwit Ltac_plugin.Tacarg.wit_simple_intropattern) v with
| None -> None
| Some v ->
let v = to_intro_pattern v in
Some v
|
