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
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
open Coqast
open Ast
open Pp
open Util
open Names
open Pcoq
open Extend
exception Non_closed_number
let get_r_sign loc =
let ast_of_id id = Astterm.globalize_constr (Nvar(loc,id)) in
((ast_of_id (id_of_string "R0"),
ast_of_id (id_of_string "R1"),
ast_of_id (id_of_string "Rplus"),
ast_of_id (id_of_string "NRplus")))
let r_of_int n dloc =
let (ast0,ast1,astp,_) = get_r_sign dloc in
let rec mk_r n =
if n <= 0 then
ast0
else if n = 1 then
ast1
else
Node(dloc,"APPLIST", [astp; ast1; mk_r (n-1)])
in
mk_r n
let r_of_string s dloc =
r_of_int (int_of_string s) dloc
let rnumber = create_constr_entry (get_univ "rnatural") "rnumber"
let _ =
Gram.extend rnumber None
[None, None,
[[Gramext.Stoken ("INT", "")],
Gramext.action r_of_string]]
(** pp **)
let rec int_of_r_rec ast1 astp p =
match p with
| Node (_,"APPLIST", [b; a; c]) when alpha_eq(b,astp) &&
alpha_eq(a,ast1) ->
(int_of_r_rec ast1 astp c)+1
| a when alpha_eq(a,ast1) -> 1
| _ -> raise Non_closed_number
let int_of_r p =
let (_,ast1,astp,_) = get_r_sign dummy_loc in
try
Some (int_of_r_rec ast1 astp p)
with
Non_closed_number -> None
let replace_plus p =
let (_,ast1,_,astnr) = get_r_sign dummy_loc in
ope ("REXPR",[ope("APPLIST", [astnr; ast1; p])])
let r_printer std_pr p =
let (_,ast1,astp,_) = get_r_sign dummy_loc in
match (int_of_r p) with
| Some i -> str (string_of_int (i+1))
| None -> std_pr (replace_plus p)
let r_printer_outside std_pr p =
let (_,ast1,astp,_) = get_r_sign dummy_loc in
match (int_of_r p) with
| Some i -> str "``" ++ str (string_of_int (i+1)) ++ str "``"
| None -> std_pr (replace_plus p)
let _ = Esyntax.Ppprim.add ("r_printer", r_printer)
let _ = Esyntax.Ppprim.add ("r_printer_outside", r_printer_outside)
|
