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
152
153
|
(defun add-survive-module nil
(interactive)
(query-replace-regexp
"
\\([ ]*\\)\\(Summary\.\\)?survive_section"
"
\\1\\2survive_module = false;
\\1\\2survive_section")
)
(global-set-key [f2] 'add-survive-module)
; functions to change old style object declaration to new style
(defun repl-open nil
(interactive)
(query-replace-regexp
"open_function\\([ ]*\\)=\\([ ]*\\)cache_\\([a-zA-Z0-9'_]*\\)\\( *\\);"
"open_function\\1=\\2(fun i o -> if i=1 then cache_\\3 o)\\4;")
)
(global-set-key [f6] 'repl-open)
(defun repl-load nil
(interactive)
(query-replace-regexp
"load_function\\([ ]*\\)=\\([ ]*\\)cache_\\([a-zA-Z0-9'_]*\\)\\( *\\);"
"load_function\\1=\\2(fun _ -> cache_\\3)\\4;")
)
(global-set-key [f7] 'repl-load)
(defun repl-decl nil
(interactive)
(query-replace-regexp
"\\(Libobject\.\\)?declare_object[
]*([ ]*\\(.*\\)[
]*,[ ]*
\\([ ]*\\){\\([ ]*\\)\\([^ ][^}]*\\)}[ ]*)"
"\\1declare_object {(\\1default_object \\2) with
\\3 \\4\\5}")
; "|$1=\\1|$2=\\2|$3=\\3|$4=\\4|")
)
(global-set-key [f9] 'repl-decl)
; eval the above and try f9 f6 f7 on the following:
let (inThing,outThing) =
declare_object
("THING",
{ load_function = cache_thing;
cache_function = cache_thing;
open_function = cache_thing;
export_function = (function x -> Some x)
})
;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
; functions helping writing non-copying substitutions
(defun make-subst (name)
(interactive "s")
(defun f (l)
(save-excursion
(query-replace-regexp
(concat "\\([a-zA-z_0-9]*\\)[ ]*:[ ]*"
(car l)
"\\([ ]*;\\|[
]*\}\\)")
(concat "let \\1\' = " (cdr l) " " name "\\1 in"))
)
)
(mapcar 'f '(("constr"."subst_mps subst")
("Coqast.t"."subst_ast subst")
("Coqast.t list"."list_smartmap (subst_ast subst)")
("'pat"."subst_pat subst")
("'pat unparsing_hunk"."subst_hunk subst_pat subst")
("'pat unparsing_hunk list"."list_smartmap (subst_hunk subst_pat subst)")
("'pat syntax_entry"."subst_syntax_entry subst_pat subst")
("'pat syntax_entry list"."list_smartmap (subst_syntax_entry subst_pat subst)")
("constr option"."option_smartmap (subst_mps subst)")
("constr list"."list_smartmap (subst_mps subst)")
("constr array"."array_smartmap (subst_mps subst)")
("constr_pattern"."subst_pattern subst")
("constr_pattern option"."option_smartmap (subst_pattern subst)")
("constr_pattern array"."array_smartmap (subst_pattern subst)")
("constr_pattern list"."list_smartmap (subst_pattern subst)")
("global_reference"."subst_global subst")
("extended_global_reference"."subst_ext subst")
("obj_typ"."subst_obj subst")
)
)
)
(global-set-key [f2] 'make-subst)
(defun make-if (name)
(interactive "s")
(save-excursion
(query-replace-regexp
"\\([a-zA-z_0-9]*\\)[ ]*:[ ]*['a-zA-z_. ]*\\(;\\|[
]*\}\\)"
(concat "&& \\1\' == " name "\\1")
)
)
)
(global-set-key [f4] 'make-if)
(defun make-record nil
(interactive)
(save-excursion
(query-replace-regexp
"\\([a-zA-z_0-9]*\\)[ ]*:[ ]*['a-zA-z_. ]*\\(;\\|[
]*\}\\)"
(concat "\\1 = \\1\' ;")
)
)
)
(global-set-key [f5] 'make-record)
(defun make-prim nil
(interactive)
(save-excursion (query-replace-regexp "\\<[a-zA-Z'_0-9]*\\>" "\\&'"))
)
(global-set-key [f6] 'make-prim)
; eval the above, yank the text below and do
; paste f2 morph.
; paste f4 morph.
; paste f5
lem : constr;
profil : bool list;
arg_types : constr list;
lem2 : constr option }
; and you almost get Setoid_replace.subst_morph :)
; and now f5 on this:
(ref,(c1,c2))
|
