diff options
Diffstat (limited to 'dev/objects.el')
| -rw-r--r-- | dev/objects.el | 153 |
1 files changed, 153 insertions, 0 deletions
diff --git a/dev/objects.el b/dev/objects.el new file mode 100644 index 00000000..b3a2694d --- /dev/null +++ b/dev/objects.el @@ -0,0 +1,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)) + + + |