Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: genprint.ml Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open Genarg
open Geninterp

(* We register printers at two levels:
   - generic arguments for general printers
   - generic values for printing ltac values *)

(* Printing generic values *)

type 'a with_level =
  { default_already_surrounded : Notation_gram.tolerability;
    default_ensure_surrounded : Notation_gram.tolerability;
    printer : 'a }

type printer_result =
| PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t)
| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level

type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t

type top_printer_result =
| TopPrinterBasic of (unit -> Pp.t)
| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level

type 'a printer = 'a -> printer_result

type 'a top_printer = 'a -> top_printer_result

module ValMap = ValTMap (struct type 'a t = 'a -> top_printer_result end)

let print0_val_map = ref ValMap.empty

let find_print_val_fun tag =
  try ValMap.find tag !print0_val_map
  with Not_found ->
    let msg s = Pp.(str "print function not found for a value interpreted as " ++ str s ++ str ".") in
    CErrors.anomaly (msg (Val.repr tag))

let generic_val_print v =
  let Val.Dyn (tag,v) = v in
  find_print_val_fun tag v

let register_val_print0 s pr =
  print0_val_map := ValMap.add s pr !print0_val_map

let combine_dont_needs pr_pair pr1 = function
  | TopPrinterBasic pr2 ->
     TopPrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ()))
  | TopPrinterNeedsContext pr2 ->
     TopPrinterNeedsContext (fun env sigma ->
         pr_pair (pr1 ()) (pr2 env sigma))
  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
     TopPrinterNeedsContext (fun env sigma ->
         pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded))

let combine_needs pr_pair pr1 = function
  | TopPrinterBasic pr2 ->
     TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ()))
  | TopPrinterNeedsContext pr2 ->
     TopPrinterNeedsContext (fun env sigma ->
         pr_pair (pr1 env sigma) (pr2 env sigma))
  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
     TopPrinterNeedsContext (fun env sigma ->
         pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded))

let combine pr_pair pr1 v2 =
  match pr1 with
  | TopPrinterBasic pr1 ->
     combine_dont_needs pr_pair pr1 (generic_val_print v2)
  | TopPrinterNeedsContext pr1 ->
     combine_needs pr_pair pr1 (generic_val_print v2)
  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
     combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded)
       (generic_val_print v2)

let _ =
  let pr_cons a b = Pp.(a ++ spc () ++ b) in
  register_val_print0 Val.typ_list
    (function
     | [] -> TopPrinterBasic mt
     | a::l ->
        List.fold_left (combine pr_cons) (generic_val_print a) l)

let _ =
  register_val_print0 Val.typ_opt
    (function
     | None -> TopPrinterBasic Pp.mt
     | Some v -> generic_val_print v)

let _ =
  let pr_pair a b = Pp.(a ++ spc () ++ b) in
  register_val_print0 Val.typ_pair
    (fun (v1,v2) -> combine pr_pair (generic_val_print v1) v2)

(* Printing generic arguments *)

type ('raw, 'glb, 'top) genprinter = {
  raw : 'raw -> printer_result;
  glb : 'glb -> printer_result;
  top : 'top -> top_printer_result;
}

module PrintObj =
struct
  type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) genprinter
  let name = "printer"
  let default wit = match wit with
  | ExtraArg tag ->
    let name = ArgT.repr tag in
    let printer = {
      raw = (fun _ -> PrinterBasic (fun env sigma -> str " ++ str name ++ str ">"));
      glb = (fun _ -> PrinterBasic (fun env sigma -> str " ++ str name ++ str ">"));
      top = (fun _ -> TopPrinterBasic (fun () -> str " ++ str name ++ str ">"));
    } in
    Some printer
  | _ -> assert false
end

module Print = Register (PrintObj)

let register_print0 wit raw glb top =
  let printer = { raw; glb; top; } in
  Print.register0 wit printer;
  match val_tag (Topwit wit), wit with
  | Val.Base t, ExtraArg t' when Geninterp.Val.repr t = ArgT.repr t' ->
     register_val_print0 t top
  | _ ->
     (* An alias, thus no primitive printer attached *)
     ()

let register_vernac_print0 wit raw =
  let glb _ = CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.") in
  let top _ = CErrors.anomaly (Pp.str "vernac argument needs not wit printer.") in
  let printer = { raw; glb; top; } in
  Print.register0 wit printer

let raw_print wit v = (Print.obj wit).raw v
let glb_print wit v = (Print.obj wit).glb v
let top_print wit v = (Print.obj wit).top v

let generic_raw_print (GenArg (Rawwit w, v)) = raw_print w v
let generic_glb_print (GenArg (Glbwit w, v)) = glb_print w v
let generic_top_print (GenArg (Topwit w, v)) = top_print w v

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.