aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/tacextend.mlp
blob: 525be643252fa80b349a9490479c84286f0975d3 (plain)
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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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)         *)
(************************************************************************)

(** Implementation of the TACTIC EXTEND macro. *)

open Q_util
open Argextend

let plugin_name = <:expr< __coq_plugin_name >>

let mlexpr_of_ident id =
  (** Workaround for badly-designed generic arguments lacking a closure *)
  let id = "$" ^ id in
  <:expr< Names.Id.of_string_soft $str:id$ >>

let rec mlexpr_of_symbol = function
| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
| Uentry e ->
  let wit = <:expr< $lid:"wit_"^e$ >> in
  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
| Uentryl (e, l) ->
  assert (e = "tactic");
  let wit = <:expr< $lid:"wit_"^e$ >> in
  <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>

let rec mlexpr_of_clause = function
| [] -> <:expr< TyNil >>
| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
| ExtNonTerminal(g,None) :: cl ->
  <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >>
| ExtNonTerminal(g,Some id) :: cl ->
  <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >>

let rec binders_of_clause e = function
| [] -> <:expr< fun ist -> $e$ >>
| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl
| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >>
| _ :: cl -> binders_of_clause e cl

open Pcaml

EXTEND
  GLOBAL: str_item;
  str_item:
    [ [ "TACTIC"; "EXTEND"; s = tac_name;
        level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
        OPT "|"; l = LIST1 tacrule SEP "|";
        "END" ->
        let level = match level with Some i -> int_of_string i | None -> 0 in
        let level = mlexpr_of_int level in
        let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
        declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ]
  ;
  tacrule:
    [ [ "["; l = LIST1 tacargs; "]";
        "->"; "["; e = Pcaml.expr; "]" ->
         <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >>
    ] ]
  ;

  tacargs:
    [ [ e = LIDENT; "("; s = LIDENT; ")" ->
        let e = parse_user_entry e "" in
        ExtNonTerminal (e, Some s)
      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
        let e = parse_user_entry e sep in
        ExtNonTerminal (e, Some s)
      | e = LIDENT ->
        let e = parse_user_entry e "" in
        ExtNonTerminal (e, None)
      | s = STRING ->
	let () = if s = "" then failwith "Empty terminal." in
        ExtTerminal s
    ] ]
  ;
  tac_name:
    [ [ s = LIDENT -> s
      | s = UIDENT -> s
    ] ]
  ;
  END