(************************************************************************)
(*         *   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 Ltac_plugin
open Pp
open Util
open Libnames
open Printer
open Newring_ast
open Newring
open Stdarg
open Tacarg
open Pcoq.Constr
open Pltac

}

DECLARE PLUGIN "newring_plugin"

TACTIC EXTEND protect_fv
| [ "protect_fv" string(map) "in" ident(id) ] ->
    { protect_tac_in map id }
| [ "protect_fv" string(map) ] ->
    { protect_tac map }
END

{

open Pptactic
open Ppconstr

let pr_ring_mod env sigma = function
  | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg (pr_constr_expr env sigma) eq_test
  | Ring_kind Abstract ->  str "abstract"
  | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg (pr_constr_expr env sigma) morph
  | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]"
  | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
  | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]"
  | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]"
  | Setoid(sth,ext) -> str "setoid" ++ pr_arg (pr_constr_expr env sigma) sth ++ pr_arg (pr_constr_expr env sigma) ext
  | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
  | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]"
  | Sign_spec t -> str "sign" ++ pr_arg (pr_constr_expr env sigma) t
  | Div_spec t -> str "div" ++ pr_arg (pr_constr_expr env sigma) t

}

VERNAC ARGUMENT EXTEND ring_mod
  PRINTED BY { pr_ring_mod env sigma }
  | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) }
  | [ "abstract" ] -> { Ring_kind Abstract }
  | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) }
  | [ "constants" "[" tactic(cst_tac) "]" ] -> { Const_tac(CstTac cst_tac) }
  | [ "closed" "[" ne_global_list(l) "]" ] -> { Const_tac(Closed l) }
  | [ "preprocess" "[" tactic(pre) "]" ] -> { Pre_tac pre }
  | [ "postprocess" "[" tactic(post) "]" ] -> { Post_tac post }
  | [ "setoid" constr(sth) constr(ext) ] -> { Setoid(sth,ext) }
  | [ "sign" constr(sign_spec) ] -> { Sign_spec sign_spec }
  | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] ->
           { Pow_spec (Closed l, pow_spec) }
  | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] ->
           { Pow_spec (CstTac cst_tac, pow_spec) }
  | [ "div" constr(div_spec) ] -> { Div_spec div_spec }
END

{

let pr_ring_mods env sigma l = surround (prlist_with_sep pr_comma (pr_ring_mod env sigma) l)

}

VERNAC ARGUMENT EXTEND ring_mods
  PRINTED BY { pr_ring_mods env sigma }
  | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods }
END

VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
  | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] ->
    { let l = match l with None -> [] | Some l -> l in add_theory id t l }
  | ![proof] [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> {
    fun ~pstate ->
    Feedback.msg_notice (strbrk "The following ring structures have been declared:");
    Spmap.iter (fun fn fi ->
      (* We should use the global env here as this shouldn't contain proof
         data, however preserving behavior as requested in review. *)
      let sigma, env = Option.cata Pfedit.get_current_context
          (let e = Global.env () in Evd.from_env e, e) pstate in
      Feedback.msg_notice (hov 2
        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
          str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
          str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
    ) !from_name;
    pstate }
END

TACTIC EXTEND ring_lookup
| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
    { let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t }
END

{

let pr_field_mod env sigma = function
  | Ring_mod m -> pr_ring_mod env sigma m
  | Inject inj -> str "completeness" ++ pr_arg (pr_constr_expr env sigma) inj

}

VERNAC ARGUMENT EXTEND field_mod
  PRINTED BY { pr_field_mod env sigma }
  | [ ring_mod(m) ] -> { Ring_mod m }
  | [ "completeness" constr(inj) ] -> { Inject inj }
END

{

let pr_field_mods env sigma l = surround (prlist_with_sep pr_comma (pr_field_mod env sigma) l)

}

VERNAC ARGUMENT EXTEND field_mods
  PRINTED BY { pr_field_mods env sigma }
  | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods }
END

VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
| [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] ->
  { let l = match l with None -> [] | Some l -> l in add_field_theory id t l }
| ![proof] [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> {
    fun ~pstate ->
    Feedback.msg_notice (strbrk "The following field structures have been declared:");
    Spmap.iter (fun fn fi ->
      (* We should use the global env here as this shouldn't
         contain proof data. *)
      let sigma, env = Option.cata Pfedit.get_current_context
          (let e = Global.env () in Evd.from_env e, e) pstate in
      Feedback.msg_notice (hov 2
        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
          str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
          str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
    ) !field_from_name;
    pstate }
END

TACTIC EXTEND field_lookup
| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
      { let (t,l) = List.sep_last lt in field_lookup f lH l t }
END