From bd7da353ea503423206e329af7a56174cb39f435 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 21 Jun 2013 21:04:00 +0000 Subject: 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 --- printing/genprint.ml | 53 +++++++++++++++++++++++++++++++++++++++++++++++++ printing/genprint.mli | 28 ++++++++++++++++++++++++++ printing/pptactic.ml | 6 +++--- printing/printing.mllib | 1 + 4 files changed, 85 insertions(+), 3 deletions(-) create mode 100644 printing/genprint.ml create mode 100644 printing/genprint.mli (limited to 'printing') diff --git a/printing/genprint.ml b/printing/genprint.ml new file mode 100644 index 0000000000..5a1da2fd7d --- /dev/null +++ b/printing/genprint.ml @@ -0,0 +1,53 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds; + glb : Obj.t -> std_ppcmds; + top : Obj.t -> std_ppcmds; +} + +let default_printer name = (); fun _ -> 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 diff --git a/printing/genprint.mli b/printing/genprint.mli new file mode 100644 index 0000000000..8300f12bfc --- /dev/null +++ b/printing/genprint.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'raw -> std_ppcmds +(** Printer for raw level generic arguments. *) + +val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds +(** Printer for glob level generic arguments. *) + +val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds +(** Printer for top level generic arguments. *) + +val generic_raw_print : rlevel generic_argument -> std_ppcmds +val generic_glb_print : glevel generic_argument -> std_ppcmds +val generic_top_print : tlevel generic_argument -> std_ppcmds + +val register_print0 : ('raw, 'glb, 'top) genarg_type -> + ('raw -> std_ppcmds) -> ('glb -> std_ppcmds) -> ('top -> std_ppcmds) -> unit diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 2ff19c9601..47bc200361 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -177,7 +177,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi x) | ExtraArgType s -> try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genarg.raw_print x + with Not_found -> Genprint.generic_raw_print x let rec pr_glb_generic prc prlc prtac prpat x = @@ -219,7 +219,7 @@ let rec pr_glb_generic prc prlc prtac prpat x = x) | ExtraArgType s -> try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genarg.glb_print x + with Not_found -> Genprint.generic_glb_print x let rec pr_top_generic prc prlc prtac prpat x = match Genarg.genarg_tag x with @@ -256,7 +256,7 @@ let rec pr_top_generic prc prlc prtac prpat x = x) | ExtraArgType s -> try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genarg.top_print x + with Not_found -> Genprint.generic_top_print x let rec tacarg_using_rule_token pr_gen = function | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al) diff --git a/printing/printing.mllib b/printing/printing.mllib index f5840bc3ea..9b3bffc8d6 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,3 +1,4 @@ +Genprint Pputils Ppconstr Printer -- cgit v1.2.3