diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-21 21:04:00 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-21 21:04:00 +0000 |
commit | bd7da353ea503423206e329af7a56174cb39f435 (patch) | |
tree | 275cce39ed6fb899660155a43ab0987c4f83025b /printing/genprint.ml | |
parent | 9024a91b59b9ecfb94e68b3748f2a9a66adcf515 (diff) |
Splitted up Genarg in four different levels:
1. Genarg itself which only defines the abstract datatypes needed.
2. Genintern, first file of interp/, defining the intern and subst
functions.
3. Geninterp, first file of tactics/, defining the interp function.
4. Genprint, first file of printing/, dealing with the printers.
The Genarg file has no dependency and is in lib/, so that we can put
generic arguments everywhere, and in particular in ASTs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing/genprint.ml')
-rw-r--r-- | printing/genprint.ml | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml new file mode 100644 index 000000000..5a1da2fd7 --- /dev/null +++ b/printing/genprint.ml @@ -0,0 +1,53 @@ +(************************************************************************) +(* 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 Util +open Genarg + +type printer = { + raw : Obj.t -> std_ppcmds; + glb : Obj.t -> std_ppcmds; + top : Obj.t -> std_ppcmds; +} + +let default_printer name = (); fun _ -> str "<genarg:" ++ str name ++ str ">" + +let default_printer name = + let pr = default_printer name in + { raw = pr; glb = pr; top = pr; } + +let (arg0_printer_map : printer String.Map.t ref) = ref String.Map.empty + +let get_printer0 name = + try String.Map.find name !arg0_printer_map + with Not_found -> default_printer name + +let obj_printer t = match t with +| ExtraArgType s -> get_printer0 s +| _ -> assert false + +let raw_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).raw +let glb_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).glb +let top_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).top + +let generic_raw_print v = + (obj_printer (genarg_tag v)).raw (Unsafe.prj v) +let generic_glb_print v = + (obj_printer (genarg_tag v)).glb (Unsafe.prj v) +let generic_top_print v = + (obj_printer (genarg_tag v)).top (Unsafe.prj v) + +let register_print0 arg rpr gpr tpr = match unquote (rawwit arg) with +| ExtraArgType s -> + if String.Map.mem s !arg0_printer_map then + Errors.anomaly (str "interp0 function already registered: " ++ str s) + else + let pr = { raw = Obj.magic rpr; glb = Obj.magic gpr; top = Obj.magic tpr; } in + arg0_printer_map := String.Map.add s pr !arg0_printer_map +| _ -> assert false |