redeffect.mlg.cppo

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2020     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *            Mozilla Public License Version 2.0              *)
(************************************************************************)

{

open Stdarg
open Reductionops

}

DECLARE PLUGIN "coq-reduction-effects.plugin"

(** *******************************************************************)
(** Grammar entry for binding a constant to the printing hook         *)
(** *******************************************************************)

{
let check_ID_type env sigma typ =
#if COQ_VERSION >= (8, 21, 0)
  let decls,_ = whd_decompose_prod env sigma typ in
#elif COQ_VERSION >= (8, 18, 0)
  let decls,_ = hnf_decompose_prod env sigma typ in
#else
  let decls,_ = splay_prod env sigma typ in
#endif
  match List.rev decls with
  | (x,t)::(_,u)::_
    when
      EConstr.isType sigma (whd_all env sigma t) &&
      let xt = Context.Rel.Declaration.LocalAssum (x,t) in
      EConstr.isRelN sigma 1 (whd_all (EConstr.push_rel xt env) sigma u) -> ()
  | _ ->
    CErrors.user_err Pp.(
        strbrk ("Function printing its second argument should be of "^
                "type \"forall A:Type, A -> T\" for some T, instead of type")
        ++ spc() ++ Printer.pr_econstr_env env sigma typ)

(** Checks whether the candidate printing function
    both is a constant and has (at least) two arguments *)
let check_valid_print_ref = function
  | Names.GlobRef.ConstRef cst ->
    let env = Global.env () in
    let sigma = Evd.from_env env in
    let sigma, c = Evd.fresh_constant_instance env sigma cst in
    let t = Typeops.type_of_constant_in env c in
    check_ID_type env sigma (EConstr.of_constr t);
    cst
  | _ -> CErrors.user_err (Pp.strbrk "Printing function should be a constant.")

let printing_hook env sigma c =
#if COQ_VERSION >= (8, 18, 0)
  let (f,l) = Constr.decompose_app c in
#else
  let (f,l) = Constr.decompose_appvect c in
#endif
  if Array.length l >= 2 then
    Feedback.msg_notice (Printer.pr_constr_env env sigma (l.(1)))

let printing_name = "Printing"

let _ = declare_reduction_effect printing_name printing_hook

let declare_effect ref =
  let ref = Smartlocate.global_with_alias ref in
  let cst = check_valid_print_ref ref in
#if COQ_VERSION >= (8, 21, 0)
  set_reduction_effect Export cst printing_name
#else
  set_reduction_effect cst printing_name
#endif
}

VERNAC COMMAND EXTEND PrintingEffect CLASSIFIED AS SIDEFF
| [ "Declare" "Printing" "Effect" global(print_ref) ] ->
    { declare_effect print_ref }
END