package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/src/ltac2_ltac1_plugin/g_ltac2_ltac1.ml.html

Source file g_ltac2_ltac1.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
let _ = Mltop.add_known_module "rocq-runtime.plugins.ltac2_ltac1"

# 13 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg"
 

open Procq.Prim
open Ltac2_plugin
open Tac2expr
open Ltac_plugin
open Ltac2_plugin.G_ltac2

let ltac_expr = Pltac.ltac_expr

let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)

let inj_ltac1 loc e = inj_wit Tac2quote_ltac1.wit_ltac1 loc e
let inj_ltac1val loc e = inj_wit Tac2quote_ltac1.wit_ltac1val loc e


# 21 "plugins/ltac2_ltac1/g_ltac2_ltac1.ml"

let _ =
  let ltac1_expr_in_env = Procq.Entry.make "ltac1_expr_in_env"
  in
  let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ltac2_ltac1", "g_ltac2_ltac1.mlg:0")
  ltac2_atom
  (Procq.Reuse (None, [Procq.Production.make
                       (Procq.Rule.next
                        (Procq.Rule.next
                         (Procq.Rule.next
                          (Procq.Rule.next
                           (Procq.Rule.next (Procq.Rule.stop)
                            ((Procq.Symbol.token (Tok.PIDENT (Some
                            ("ltac1val"))))))
                           ((Procq.Symbol.token (Tok.PKEYWORD (":")))))
                          ((Procq.Symbol.token (Tok.PKEYWORD ("(")))))
                         ((Procq.Symbol.nterm ltac1_expr_in_env)))
                        ((Procq.Symbol.token (Tok.PKEYWORD (")")))))
                       (fun _ qid _ _ _ loc -> 
# 34 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg"
                                                                    inj_ltac1val loc qid 
# 44 "plugins/ltac2_ltac1/g_ltac2_ltac1.ml"
);
                      Procq.Production.make
                      (Procq.Rule.next
                       (Procq.Rule.next
                        (Procq.Rule.next
                         (Procq.Rule.next
                          (Procq.Rule.next (Procq.Rule.stop)
                           ((Procq.Symbol.token (Tok.PIDENT (Some
                           ("ltac1"))))))
                          ((Procq.Symbol.token (Tok.PKEYWORD (":")))))
                         ((Procq.Symbol.token (Tok.PKEYWORD ("(")))))
                        ((Procq.Symbol.nterm ltac1_expr_in_env)))
                       ((Procq.Symbol.token (Tok.PKEYWORD (")")))))
                      (fun _ qid _ _ _ loc -> 
# 33 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg"
                                                                 inj_ltac1 loc qid 
# 61 "plugins/ltac2_ltac1/g_ltac2_ltac1.ml"
)]))
  in let () = assert (Procq.Entry.is_empty ltac1_expr_in_env) in
  let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ltac2_ltac1", "g_ltac2_ltac1.mlg:1")
  ltac1_expr_in_env
  (Procq.Fresh
  (Gramlib.Gramext.First, [(None, None,
                           [Procq.Production.make
                            (Procq.Rule.next (Procq.Rule.stop)
                             ((Procq.Symbol.nterm ltac_expr)))
                            (fun e loc -> 
# 38 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg"
                           [], e 
# 75 "plugins/ltac2_ltac1/g_ltac2_ltac1.ml"
);
                           Procq.Production.make
                           (Procq.Rule.next
                            (Procq.Rule.next
                             (Procq.Rule.next
                              (Procq.Rule.next (Procq.Rule.stop)
                               ((Procq.Symbol.nterm test_ltac1_env)))
                              ((Procq.Symbol.list0 (Procq.Symbol.nterm identref))))
                             ((Procq.Symbol.token (Tok.PKEYWORD ("|-")))))
                            ((Procq.Symbol.nterm ltac_expr)))
                           (fun e _ ids _ loc -> 
# 37 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg"
                                                                       ids, e 
# 89 "plugins/ltac2_ltac1/g_ltac2_ltac1.ml"
)])]))
  in ()