Quelle  g_class.mlg   Sprache: unbekannt

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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 Class_tactics
open Stdarg
open Classes

}

DECLARE PLUGIN "rocq-runtime.plugins.ltac"

(** Options: depth, debug and transparency settings. *)

VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
| #[ locality = Attributes.hint_locality ]
  [ "Typeclasses" "Transparent" ne_reference_list(cl) ] -> {
    set_typeclass_transparency_com ~locality cl true
  }
END

VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF
| #[ locality = Attributes.hint_locality ]
  [ "Typeclasses" "Opaque" ne_reference_list(cl) ] -> {
    set_typeclass_transparency_com ~locality cl false
  }
END

{

let pr_debug _prc _prlc _prt b =
  if b then Pp.str "debug" else Pp.mt()

}

ARGUMENT EXTEND debug TYPED AS bool PRINTED BY { pr_debug }
| [ "debug" ] -> { true }
| [ ] -> { false }
END

{

let pr_search_strategy_name _prc _prlc _prt = function
  | Dfs -> Pp.str "dfs"
  | Bfs -> Pp.str "bfs"

let pr_search_strategy _prc _prlc _prt = function
  | Some s -> pr_search_strategy_name _prc _prlc _prt s
  | None -> Pp.mt ()

}

ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name }
| [ "bfs" ] -> { Bfs }
| [ "dfs" ] -> { Dfs }
END

ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy }
| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s }
| [ ] -> { None }
END

(* true = All transparent, false = Opaque if possible *)

VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
 | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> {
     set_typeclasses_debug d;
     Option.iter set_typeclasses_strategy s;
     set_typeclasses_depth depth
   }
END

TACTIC EXTEND typeclasses_eauto
 | [ "typeclasses" "eauto" "dfs" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
    { typeclasses_eauto ~depth:d ~strategy:Dfs l }
 | [ "typeclasses" "eauto" "bfs" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
    { typeclasses_eauto ~depth:d ~strategy:Bfs l }
 | [ "typeclasses" "eauto" "best_effort" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
    { typeclasses_eauto ~depth:d ~best_effort:true l }
 | [ "typeclasses" "eauto" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
    { typeclasses_eauto ~depth:d l }
 | [ "typeclasses" "eauto" "bfs" nat_or_var_opt(d) ] -> {
     typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] }
 | [ "typeclasses" "eauto" "dfs" nat_or_var_opt(d) ] -> {
     typeclasses_eauto ~depth:d ~strategy:Dfs ~only_classes:true [Class_tactics.typeclasses_db] }
 | [ "typeclasses" "eauto" "best_effort" nat_or_var_opt(d) ] -> {
      typeclasses_eauto ~depth:d ~only_classes:true ~best_effort:true [Class_tactics.typeclasses_db] }
 | [ "typeclasses" "eauto" nat_or_var_opt(d) ] -> {
     typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] }
END

TACTIC EXTEND head_of_constr
| [ "head_of_constr" ident(h) constr(c) ] -> { head_of_constr h c }
END

TACTIC EXTEND not_evar
| [ "not_evar" constr(ty) ] -> { not_evar ty }
END

TACTIC EXTEND is_ground
| [ "is_ground" constr(ty) ] -> { is_ground ty }
END

TACTIC EXTEND autoapply
| [ "autoapply" constr(c) "with" preident(i) ] -> { autoapply c i }
END