diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-18 19:48:50 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-18 19:48:50 +0000 |
commit | a3b4bde65a350bf3dc54ccec8f7608355c6a008a (patch) | |
tree | 46107f5a916af73f9c0051097ce73f2bdd3455b8 /interp/stdarg.ml | |
parent | 7a2701e6741fcf1e800e35b7721fc89abe40cbba (diff) |
Proof-of-concept: moved four easy-to-handle generic arguments to
their own file, Stdarg.
This required a little trick to correctly handle wit_* naming. We
use a dynamic table to remember exactly where those arguments come
from.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16587 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/stdarg.ml')
-rw-r--r-- | interp/stdarg.ml | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml new file mode 100644 index 000000000..cfc65bde8 --- /dev/null +++ b/interp/stdarg.ml @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Genarg + +let def_uniform name pr = { (default_uniform_arg0 name) with + arg0_rprint = pr; + arg0_gprint = pr; + arg0_tprint = pr; +} + +let wit_bool : bool uniform_genarg_type = + let pr_bool b = str (if b then "true" else "false") in + let arg = def_uniform "bool" pr_bool in + make0 None "bool" arg + +let () = register_name0 wit_bool "Stdarg.wit_bool" + +let wit_int : int uniform_genarg_type = + let pr_int = int in + let arg = def_uniform "int" pr_int in + make0 None "int" arg + +let () = register_name0 wit_int "Stdarg.wit_int" + +let wit_string : string uniform_genarg_type = + let pr_string s = str "\"" ++ str s ++ str "\"" in + let arg = def_uniform "string" pr_string in + make0 None "string" arg + +let () = register_name0 wit_string "Stdarg.wit_string" + +let wit_pre_ident : string uniform_genarg_type = + let pr_pre_ident = str in + let arg = def_uniform "preident" pr_pre_ident in + make0 None "preident" arg + +let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident" |