File ‹zippy_instance_resolves_data.ML›

(*  Title:      Zippy/zippy_instance_resolves_data.ML
    Author:     Kevin Kappelmann
*)
@{parse_entries (sig) PARSE_ZIPPY_INSTANCE_RESOLVES_DATA_MODES [r, e, d, f]}

signature ZIPPY_INSTANCE_RESOLVES_DATA_ARGS =
sig
  structure PM : PARSE_ZIPPY_INSTANCE_RESOLVES_DATA_MODES
  type mode = PM.key
  val parse_mode : mode parser
end

structure Zippy_Instance_Resolves_Data_Args : ZIPPY_INSTANCE_RESOLVES_DATA_ARGS =
struct
@{parse_entries (struct) PM [r, e, d, f]}
type mode = PM.key
val parse_mode = PM.parse_key
end

functor Zippy_Instance_Resolves_Data(
    structure FI : FUNCTOR_INSTANCE_BASE
    structure Z : ZIPPY_INSTANCE_TACTIC
    structure TI : TERM_INDEX
    val init_args : (Z.Tac_AAM.mk_meta,
      int -> @{AllT_args} Z.Base_Data.PAction.action,
      Z.Base_Data.GCS.goal_pos -> (@{ParaT_args} @{AllT_args} Z.ZLPC.Z2.zipper) Z.emorph,
      @{AllT_args} Z.Result_Action.mk_copy_update_data,
      @{AllT_args} Z.PResults.presultsq,
      thm * (term * (thm,
        Z.Tac_AAM.mk_meta,
        int -> @{AllT_args} Z.Base_Data.PAction.action,
        (Z.Base_Data.GCS.goal_pos -> (@{ParaT_args} @{AllT_args} Z.ZLPC.Z2.zipper) Z.emorph) list,
        @{AllT_args} Z.Result_Action.mk_copy_update_data,
        @{AllT_args} Z.PResults.presultsq)
        Zippy_Instance_Hom_Changed_Goals_Data_Args.PD.entries) -> bool)
        Zippy_Instance_Hom_Changed_Goals_Data_Args.PDC.entries
    structure Log : ZIPPY_LOGGER_MIXIN_BASE
  ) =
struct
local structure FI =  Functor_Instance(FI)
in
structure Logging =
struct
  local structure Base = struct val parent_logger = Log.logger end
  in
  structure Resolve = Zippy_Logger_Mixin_Base(open Base; val name = "Resolve")
  structure EResolve = Zippy_Logger_Mixin_Base(open Base; val name = "EResolve")
  structure DResolve = Zippy_Logger_Mixin_Base(open Base; val name = "DResolve")
  structure FResolve = Zippy_Logger_Mixin_Base(open Base; val name = "FResolve")
  end
end

local open Z; open ZLPC
  structure Base = struct structure Z = Z; structure TI = TI; val init_args = init_args end
in
\<^functor_instance>‹struct_name: Resolve
  functor_name: Zippy_Instance_Hom_Changed_Goals_Data
  FI_struct_name: FI_Hom_Changed_Goals_Data
  id: ‹FI.prefix_id "resolve"›
  path: ‹FI.long_name›
  more_args: ‹open Base
    val key_of_thm = Thm.concl_of
    val num_new_goals = Thm.nprems_of
    structure Log = Logging.Resolve››
structure Resolve = Resolve.Hom_Changed_Goals_Data

\<^functor_instance>‹struct_name: EResolve
  functor_name: Zippy_Instance_Hom_Changed_Goals_Data
  FI_struct_name: FI_Hom_Changed_Goals_Data
  id: ‹FI.prefix_id "eresolve"›
  path: ‹FI.long_name›
  more_args: ‹open Base
    val key_of_thm = Thm.major_prem_of
    val num_new_goals = Thm.nprems_of #> General_Util.pred
    structure Log = Logging.EResolve››
structure EResolve = EResolve.Hom_Changed_Goals_Data

\<^functor_instance>‹struct_name: DResolve
  functor_name: Zippy_Instance_Hom_Changed_Goals_Data
  FI_struct_name: FI_Hom_Changed_Goals_Data
  id: ‹FI.prefix_id "dresolve"›
  path: ‹FI.long_name›
  more_args: ‹open Base
    val key_of_thm = Thm.major_prem_of
    val num_new_goals = Thm.nprems_of
    structure Log = Logging.DResolve››
structure DResolve = DResolve.Hom_Changed_Goals_Data

\<^functor_instance>‹struct_name: FResolve
  functor_name: Zippy_Instance_Hom_Changed_Goals_Data
  FI_struct_name: FI_Hom_Changed_Goals_Data
  id: ‹FI.prefix_id "fresolve"›
  path: ‹FI.long_name›
  more_args: ‹open Base
    val key_of_thm = Thm.major_prem_of
    val num_new_goals = Thm.nprems_of
    structure Log = Logging.FResolve››
structure FResolve = FResolve.Hom_Changed_Goals_Data

local open Zippy_Instance_Resolves_Data_Args
  val parse_mode_opt_default = Scan.optional (Args.parens (Parse.!!! PM.parse_key)) (PM.key PM.r)
in
val parse_attribute = parse_mode_opt_default
  :|-- (fn PM.r _ => Resolve.parse_attribute | PM.e _ => EResolve.parse_attribute
    | PM.d _ => DResolve.parse_attribute | PM.f _ => FResolve.parse_attribute)

val binding = Binding.make (FI.id, FI.pos)

val setup_attribute = Attrib.local_setup binding
  (Parse.!!! parse_attribute |> Scan.lift) o
  Either.cases I (fn what => "configure " ^ what ^ " data " ^ enclose "(" ")" FI.long_name)

val parse_method =
  let val parse = Scan.lift parse_mode_opt_default
    :|-- (fn PM.r _ => Resolve.parse_entry_context_update | PM.e _ => EResolve.parse_entry_context_update
      | PM.d _ => DResolve.parse_entry_context_update | PM.f _ => FResolve.parse_entry_context_update)
  in Parse.and_list1' parse >> K () end
end
end
end
end