(*  Nominal Function Common
    Author: Christian Urban

    heavily based on the code of Alexander Krauss
    (code forked on 5 June 2011)

Redefinition of config datatype 
*)

signature NOMINAL_FUNCTION_DATA =
sig

type nominal_info =
 {is_partial : bool,
  defname : string,
    (* contains no logical entities: invariant under morphisms: *)
  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
  case_names : string list,
  fs : term list,
  R : term,
  psimps: thm list,
  pinducts: thm list,
  simps : thm list option,
  inducts : thm list option,
  termination: thm,
  eqvts: thm list}

end


structure Nominal_Function_Common =
struct

type nominal_info =
 {is_partial : bool,
  defname : string,
    (* contains no logical entities: invariant under morphisms: *)
  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
  case_names : string list,
  fs : term list,
  R : term,
  psimps: thm list,
  pinducts: thm list,
  simps : thm list option,
  inducts : thm list option,
  termination: thm,
  eqvts: thm list}

fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
  simps, inducts, termination, defname, is_partial, eqvts} : nominal_info) phi =
    let
      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
      val name = Binding.name_of o Morphism.binding phi o Binding.name
    in
      { add_simps = add_simps, case_names = case_names,
        fs = map term fs, R = term R, psimps = fact psimps,
        pinducts = fact pinducts, simps = Option.map fact simps,
        inducts = Option.map fact inducts, termination = thm termination,
        defname = name defname, is_partial=is_partial, eqvts = fact eqvts }
    end

structure NominalFunctionData = Generic_Data
(
  type T = (term * nominal_info) Item_Net.T;
  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
  val extend = I;
  fun merge tabs : T = Item_Net.merge tabs;
)

val get_function = NominalFunctionData.get o Context.Proof;


fun lift_morphism thy f =
  let
    fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
  in
    Morphism.thm_morphism f $> Morphism.term_morphism term
    $> Morphism.typ_morphism (Logic.type_map term)
  end

fun import_function_data t ctxt =
  let
    val thy = Proof_Context.theory_of ctxt
    val ct = cterm_of thy t
    val inst_morph = lift_morphism thy o Thm.instantiate

    fun match (trm, data) =
      SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
      handle Pattern.MATCH => NONE
  in
    get_first match (Item_Net.retrieve (get_function ctxt) t)
  end

fun import_last_function ctxt =
  case Item_Net.content (get_function ctxt) of
    [] => NONE
  | (t, data) :: _ =>
    let
      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
    in
      import_function_data t' ctxt'
    end

val all_function_data = Item_Net.content o get_function

fun add_function_data (data : nominal_info as {fs, termination, ...}) =
  NominalFunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
  #> Function_Common.store_termination_rule termination




(* Configuration management *)
datatype nominal_function_opt
  = Sequential
  | Default of string
  | DomIntros
  | No_Partials
  | Invariant of string

datatype nominal_function_config = NominalFunctionConfig of
 {sequential: bool,
  default: string option,
  domintros: bool,
  partials: bool,
  inv: string option}

fun apply_opt Sequential (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
    NominalFunctionConfig 
      {sequential=true, default=default, domintros=domintros, partials=partials, inv=inv}
  | apply_opt (Default d) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
    NominalFunctionConfig 
      {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, inv=inv}
  | apply_opt DomIntros (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
    NominalFunctionConfig 
      {sequential=sequential, default=default, domintros=true, partials=partials, inv=inv}
  | apply_opt No_Partials (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
    NominalFunctionConfig 
      {sequential=sequential, default=default, domintros=domintros, partials=false, inv=inv}
  | apply_opt (Invariant s) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
    NominalFunctionConfig 
      {sequential=sequential, default=default, domintros=domintros, partials=partials, inv = SOME s}

val nominal_default_config =
  NominalFunctionConfig { sequential=false, default=NONE,
    domintros=false, partials=true, inv=NONE}

datatype nominal_function_result = NominalFunctionResult of
 {fs: term list,
  G: term,
  R: term,
  psimps : thm list,
  simple_pinducts : thm list,
  cases : thm,
  termination : thm,
  domintros : thm list option,
  eqvts : thm list}

end
