aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_primnew.ml4
blob: d41055fb6675f7554894b3f3be66b54006c7e561 (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
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
(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(*i $Id$ i*)

open Coqast
open Pcoq
open Names
open Libnames
open Topconstr

let _ =
  if not !Options.v7 then
    Pcoq.reset_all_grammars()
let _ =
  if not !Options.v7 then
  let f = Gram.Unsafe.clear_entry in
  f Prim.bigint;
  f Prim.qualid;
  f Prim.ast;
  f Prim.reference

let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'"]
let _ = 
  if not !Options.v7 then
    List.iter (fun s -> Lexer.add_token("",s)) prim_kw

ifdef Quotify then
open Qast

open Prim

ifdef Quotify then
module Prelude = struct
let local_id_of_string s = Apply ("Names","id_of_string", [s])
let local_make_dirpath l = Qast.Apply ("Names","make_dirpath",[l])
let local_make_posint s = s
let local_make_negint s = Apply ("Pervasives","~-", [s])
let local_make_qualid l id' = 
  Qast.Apply ("Nametab","make_qualid", [local_make_dirpath l;id'])
let local_make_short_qualid id =
  Qast.Apply ("Nametab","make_short_qualid",[id])
let local_make_path l id' =
  Qast.Apply ("Libnames","encode_kn", [local_make_dirpath l;id'])
let local_make_binding loc a b =
  match a with
    | Qast.Node ("Nvar", [_;id]) ->
	Qast.Node ("Slam", [Qast.Loc; Qast.Option (Some id); b])
    | Qast.Node ("Nmeta", [_;s]) ->
	Qast.Node ("Smetalam", [Qast.Loc;s;b])
    | _ -> 
	Qast.Apply ("Pervasives", "failwith", [Qast.Str "Slam expects a var or a metavar"])
let local_append l id = Qast.Apply ("List","append", [l; Qast.List [id]])
end

else

module Prelude = struct
open Nametab
let local_id_of_string = id_of_string
let local_make_dirpath = make_dirpath
let local_make_qualid l id' = make_qualid (local_make_dirpath l) id'
let local_make_short_qualid id = make_short_qualid id
let local_make_posint = int_of_string
let local_make_negint n = - int_of_string n
let local_make_path l a = encode_kn (local_make_dirpath l) a
let local_make_binding loc a b =
  match a with
    | Nvar (_,id) -> Slam(loc,Some id,b)
    | Nmeta (_,s) -> Smetalam(loc,s,b)
    | _ -> failwith "Slam expects a var or a metavar"
let local_append l id = l@[id]
end

open Prelude

ifdef Quotify then
open Q

if not !Options.v7 then
GEXTEND Gram
  GLOBAL: ast bigint qualid reference;
  metaident:
    [ [ s = METAIDENT -> Nmeta (loc,s) ] ]
  ;
  field:
    [ [ s = FIELD -> local_id_of_string s ] ]
  ;
  fields:
    [ [ id = field; (l,id') = fields -> (local_append l id,id')
      | id = field -> ([],id)
      ] ]
  ;
  astpath:
    [ [ id = base_ident; (l,a) = fields ->
          Path(loc, local_make_path (local_append l id) a)
      | id = base_ident -> Nvar(loc, id)
      ] ]
  ;
  basequalid:
    [ [ id = base_ident; (l,id')=fields ->
          local_make_qualid (local_append l id) id'
      | id = base_ident -> local_make_short_qualid id
      ] ]
  ;
  reference:
    [ [ id = base_ident; (l,id') = fields ->
        Qualid (loc, local_make_qualid (local_append l id) id')
      | id = base_ident -> Ident (loc,id)
      ] ]
  ;
  qualid:
    [ [ qid = basequalid -> loc, qid ] ]
  ;
  ast:
    [ [ id = metaident -> id
      | p = astpath -> p
      | s = INT -> Num(loc, local_make_posint s)
      | s = STRING -> Str(loc, s)
      | "{"; s = METAIDENT; "}" -> Id(loc,s)
      | "("; nname = IDENT; l = LIST0 ast; ")" -> Node(loc,nname,l)
      | "("; METAIDENT "$LIST"; id = metaident; ")" -> Node(loc,"$LIST",[id])
      | "("; METAIDENT "$STR"; id = metaident; ")" -> Node(loc,"$STR",[id])
      | "("; METAIDENT "$VAR"; id = metaident; ")" -> Node(loc,"$VAR",[id])
      | "("; METAIDENT "$ID"; id = metaident; ")" -> Node(loc,"$ID",[id])
      | "("; METAIDENT "$ABSTRACT"; l = LIST0 ast;")"->Node(loc,"$ABSTRACT",l)
      | "("; METAIDENT "$PATH"; id = metaident; ")" -> Node(loc,"$PATH",[id])
      | "("; METAIDENT "$NUM"; id = metaident; ")" -> Node(loc,"$NUM",[id])
      | "["; "<>"; "]"; b = ast -> Slam(loc,None,b)
      | "["; a = ast; "]"; b = ast -> local_make_binding loc a b
      | "'"; a = ast -> Node(loc,"$QUOTE",[a]) ] ]
  ;
  bigint: (* Negative numbers are dealt with specially *)
    [ [ i = INT -> Bignat.POS (Bignat.of_string i) ] ]
  ;
END

(*
let constr_to_ast a =
  Termast.ast_of_rawconstr
    (Constrintern.interp_rawconstr Evd.empty (Global.env()) a)

let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr

let _ = define_ast_quotation true "constr" constr_parser_with_glob
*)