(*  Title:      HOL/Tools/Lifting/lifting_info.ML

    Author:     Ondrej Kuncar

Context data for the lifting package.

*)

signature LIFTING_INFO =

sig

  type quot_map = {rel_quot_thm: thm}

  val lookup_quot_maps: Proof.context -> string -> quot_map option

  val print_quot_maps: Proof.context -> unit

  type pcr = {pcrel_def: thm, pcr_cr_eq: thm}

  type quotient = {quot_thm: thm, pcr_info: pcr option}

  val pcr_eq: pcr * pcr -> bool

  val quotient_eq: quotient * quotient -> bool

  val transform_quotient: morphism -> quotient -> quotient

  val lookup_quotients: Proof.context -> string -> quotient option

  val update_quotients: string -> quotient -> Context.generic -> Context.generic

  val delete_quotients: thm -> Context.generic -> Context.generic

  val print_quotients: Proof.context -> unit

  type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}

  val lookup_restore_data: Proof.context -> string -> restore_data option

  val init_restore_data: string -> quotient -> Context.generic -> Context.generic

  val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic  

  val get_invariant_commute_rules: Proof.context -> thm list

  val get_reflexivity_rules: Proof.context -> thm list

  val add_reflexivity_rule_raw_attribute: attribute

  val add_reflexivity_rule_attribute: attribute

  type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 

    pos_distr_rules: thm list, neg_distr_rules: thm list}

  val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option

  val get_quot_maps           : Proof.context -> quot_map Symtab.table

  val get_quotients           : Proof.context -> quotient Symtab.table

  val get_relator_distr_data  : Proof.context -> relator_distr_data Symtab.table

  val get_restore_data        : Proof.context -> restore_data Symtab.table

  val setup: theory -> theory

end

structure Lifting_Info: LIFTING_INFO =

struct

open Lifting_Util

(** data container **)

type quot_map = {rel_quot_thm: thm}

type pcr = {pcrel_def: thm, pcr_cr_eq: thm}

type quotient = {quot_thm: thm, pcr_info: pcr option}

type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 

  pos_distr_rules: thm list, neg_distr_rules: thm list}

type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}

structure Data = Generic_Data

(

  type T = 

    { quot_maps : quot_map Symtab.table,

      quotients : quotient Symtab.table,

      reflexivity_rules : thm Item_Net.T,

      relator_distr_data : relator_distr_data Symtab.table,

      restore_data : restore_data Symtab.table

    }

  val empty =

    { quot_maps = Symtab.empty,

      quotients = Symtab.empty,

      reflexivity_rules = Thm.full_rules,

      relator_distr_data = Symtab.empty,

      restore_data = Symtab.empty

    }

  val extend = I

  fun merge

    ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, 

        restore_data = rd1 },

      { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2,

        restore_data = rd2 } ) =

    { quot_maps = Symtab.merge (K true) (qm1, qm2),

      quotients = Symtab.merge (K true) (q1, q2),

      reflexivity_rules = Item_Net.merge (rr1, rr2),

      relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),

      restore_data = Symtab.merge (K true) (rd1, rd2) }

)

fun map_data f1 f2 f3 f4 f5

  { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data } =

  { quot_maps = f1 quot_maps,

    quotients = f2 quotients,

    reflexivity_rules = f3 reflexivity_rules,

    relator_distr_data = f4 relator_distr_data,

    restore_data = f5 restore_data }

fun map_quot_maps           f = map_data f I I I I

fun map_quotients           f = map_data I f I I I

fun map_reflexivity_rules   f = map_data I I f I I

fun map_relator_distr_data  f = map_data I I I f I

fun map_restore_data        f = map_data I I I I f

val get_quot_maps'           = #quot_maps o Data.get

val get_quotients'           = #quotients o Data.get

val get_reflexivity_rules'   = #reflexivity_rules o Data.get

val get_relator_distr_data'  = #relator_distr_data o Data.get

val get_restore_data'        = #restore_data o Data.get

fun get_quot_maps          ctxt = get_quot_maps' (Context.Proof ctxt)

fun get_quotients          ctxt = get_quotients' (Context.Proof ctxt)

fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)

fun get_restore_data       ctxt = get_restore_data' (Context.Proof ctxt)

(* info about Quotient map theorems *)

val lookup_quot_maps = Symtab.lookup o get_quot_maps

fun quot_map_thm_sanity_check rel_quot_thm ctxt =

  let

    fun quot_term_absT ctxt quot_term = 

      let 

        val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term

          handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block

            [Pretty.str "The Quotient map theorem is not in the right form.",

             Pretty.brk 1,

             Pretty.str "The following term is not the Quotient predicate:",

             Pretty.brk 1,

             Syntax.pretty_term ctxt t]))

      in

        fastype_of abs

      end

    val ((_, [rel_quot_thm_fixed]), ctxt') = Variable.importT [rel_quot_thm] ctxt

    val rel_quot_thm_prop = prop_of rel_quot_thm_fixed

    val rel_quot_thm_concl = Logic.strip_imp_concl rel_quot_thm_prop

    val rel_quot_thm_prems = Logic.strip_imp_prems rel_quot_thm_prop;

    val concl_absT = quot_term_absT ctxt' rel_quot_thm_concl

    val concl_tfrees = Term.add_tfree_namesT (concl_absT) []

    val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list) 

                          rel_quot_thm_prems []

    val extra_prem_tfrees =

      case subtract (op =) concl_tfrees prems_tfrees of

        [] => []

      | extras => [Pretty.block ([Pretty.str "Extra type variables in the premises:",

                                 Pretty.brk 1] @ 

                                 ((Pretty.commas o map (Pretty.str o quote)) extras) @

                                 [Pretty.str "."])]

    val errs = extra_prem_tfrees 

  in

    if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""] 

                                                 @ (map Pretty.string_of errs)))

  end

fun add_quot_map rel_quot_thm ctxt = 

  let

    val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) ctxt

    val rel_quot_thm_concl = (Logic.strip_imp_concl o prop_of) rel_quot_thm

    val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl

    val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs

    val minfo = {rel_quot_thm = rel_quot_thm}

  in

    Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) ctxt

  end    

val quot_map_attribute_setup =

  Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map))

    "declaration of the Quotient map theorem"

fun print_quot_maps ctxt =

  let

    fun prt_map (ty_name, {rel_quot_thm}) =

      Pretty.block (separate (Pretty.brk 2)

         [Pretty.str "type:", 

          Pretty.str ty_name,

          Pretty.str "quot. theorem:", 

          Syntax.pretty_term ctxt (prop_of rel_quot_thm)])

  in

    map prt_map (Symtab.dest (get_quot_maps ctxt))

    |> Pretty.big_list "maps for type constructors:"

    |> Pretty.writeln

  end

(* info about quotient types *)

fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1},

           {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = 

           Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2)

fun option_eq _ (NONE,NONE) = true

  | option_eq _ (NONE,_) = false

  | option_eq _ (_,NONE) = false

  | option_eq cmp (SOME x, SOME y) = cmp (x,y);

fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1},

                {quot_thm = quot_thm2, pcr_info = pcr_info2}) =

                Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)

fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =

  {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}

fun transform_quotient phi {quot_thm, pcr_info} =

  {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info}

fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name

fun update_quotients type_name qinfo ctxt = 

  Data.map (map_quotients (Symtab.update (type_name, qinfo))) ctxt

fun delete_quotients quot_thm ctxt =

  let

    val (_, qtyp) = quot_thm_rty_qty quot_thm

    val qty_full_name = (fst o dest_Type) qtyp

    val symtab = get_quotients' ctxt

    fun compare_data (_, data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm)

  in

    if Symtab.member compare_data symtab (qty_full_name, quot_thm)

      then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt

      else ctxt

  end

fun print_quotients ctxt =

  let

    fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) =

      Pretty.block (separate (Pretty.brk 2)

       [Pretty.str "type:", 

        Pretty.str qty_name,

        Pretty.str "quot. thm:",

        Syntax.pretty_term ctxt (prop_of quot_thm),

        Pretty.str "pcrel_def thm:",

        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcr_info,

        Pretty.str "pcr_cr_eq thm:",

        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcr_info])

  in

    map prt_quot (Symtab.dest (get_quotients ctxt))

    |> Pretty.big_list "quotients:"

    |> Pretty.writeln

  end

val quot_del_attribute_setup =

  Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))

    "deletes the Quotient theorem"

(* data for restoring Transfer/Lifting context *)

fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name

fun update_restore_data bundle_name restore_data ctxt = 

  Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) ctxt

fun init_restore_data bundle_name qinfo ctxt = 

  update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } ctxt

fun add_transfer_rules_in_restore_data bundle_name transfer_rules ctxt =

  case Symtab.lookup (get_restore_data' ctxt) bundle_name of

    SOME restore_data => update_restore_data bundle_name { quotient = #quotient restore_data, 

      transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt

    | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")

(* theorems that a relator of an invariant is an invariant of the corresponding predicate *)

structure Invariant_Commute = Named_Thms

(

  val name = @{binding invariant_commute}

  val description = "theorems that a relator of an invariant is an invariant of the corresponding predicate"

)

fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt)

(* info about reflexivity rules *)

fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt))

(* Conversion to create a reflp' variant of a reflexivity rule  *)

fun safe_reflp_conv ct =

  Conv.try_conv (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm reflp'_def}))) ct

fun prep_reflp_conv ct = (

      Conv.implies_conv safe_reflp_conv prep_reflp_conv

      else_conv

      safe_reflp_conv

      else_conv

      Conv.all_conv) ct

fun add_reflexivity_rule_raw thm = Data.map (map_reflexivity_rules (Item_Net.update thm))

val add_reflexivity_rule_raw_attribute = Thm.declaration_attribute add_reflexivity_rule_raw

fun add_reflexivity_rule thm = add_reflexivity_rule_raw thm #>

  add_reflexivity_rule_raw (Conv.fconv_rule prep_reflp_conv thm)

val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule

val relfexivity_rule_setup =

  let

    val name = @{binding reflexivity_rule}

    fun del_thm_raw thm = Data.map (map_reflexivity_rules (Item_Net.remove thm))

    fun del_thm thm = del_thm_raw thm #>

      del_thm_raw (Conv.fconv_rule prep_reflp_conv thm)

    val del = Thm.declaration_attribute del_thm

    val text = "rules that are used to prove that a relation is reflexive"

    val content = Item_Net.content o get_reflexivity_rules'

  in

    Attrib.setup name (Attrib.add_del add_reflexivity_rule_attribute del) text

    #> Global_Theory.add_thms_dynamic (name, content)

  end

(* info about relator distributivity theorems *)

fun map_relator_distr_data' f1 f2 f3 f4

  {pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} =

  {pos_mono_rule   = f1 pos_mono_rule, 

   neg_mono_rule   = f2 neg_mono_rule,

   pos_distr_rules = f3 pos_distr_rules, 

   neg_distr_rules = f4 neg_distr_rules}

fun map_pos_mono_rule f = map_relator_distr_data' f I I I

fun map_neg_mono_rule f = map_relator_distr_data' I f I I

fun map_pos_distr_rules f = map_relator_distr_data' I I f I 

fun map_neg_distr_rules f = map_relator_distr_data' I I I f

fun introduce_polarities rule =

  let

    val dest_less_eq = HOLogic.dest_bin @{const_name "less_eq"} dummyT

    val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (prems_of rule)

    val equal_prems = filter op= prems_pairs

    val _ = if null equal_prems then () 

      else error "The rule contains reflexive assumptions."

    val concl_pairs = rule 

      |> concl_of

      |> HOLogic.dest_Trueprop

      |> dest_less_eq

      |> pairself (snd o strip_comb)

      |> op~~

      |> filter_out op=

    val _ = if has_duplicates op= concl_pairs 

      then error "The rule contains duplicated variables in the conlusion." else ()

    fun rewrite_prem prem_pair = 

      if member op= concl_pairs prem_pair

      then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))

      else if member op= concl_pairs (swap prem_pair)

        then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def}))

      else error "The rule contains a non-relevant assumption."

    fun rewrite_prems [] = Conv.all_conv

      | rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs)

    val rewrite_prems_conv = rewrite_prems prems_pairs

    val rewrite_concl_conv = 

      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})))

  in

    (Conv.fconv_rule (rewrite_prems_conv then_conv rewrite_concl_conv)) rule

  end

  handle 

    TERM _ => error "The rule has a wrong format."

    | CTERM _ => error "The rule has a wrong format."

fun negate_mono_rule mono_rule = 

  let

    val rewr_conv = HOLogic.Trueprop_conv (Conv.rewrs_conv [@{thm POS_NEG}, @{thm NEG_POS}])

  in

    Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule

  end;

fun add_mono_rule mono_rule ctxt = 

  let

    val mono_rule = introduce_polarities mono_rule

    val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 

      dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule

    val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name 

      then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")

      else ()

    val neg_mono_rule = negate_mono_rule mono_rule

    val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule, 

      pos_distr_rules = [], neg_distr_rules = []}

  in

    Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) ctxt

  end;

local 

  fun add_distr_rule update_entry distr_rule ctxt =

    let

      val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 

        dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) distr_rule

    in

      if Symtab.defined (get_relator_distr_data' ctxt) distr_ruleT_name then 

        Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule))) 

          ctxt

      else error "The monoticity rule is not defined."

    end

    fun rewrite_concl_conv thm ctm = 

      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm

      handle CTERM _ => error "The rule has a wrong format."

in

  fun add_pos_distr_rule distr_rule ctxt = 

    let

      val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule

      fun update_entry distr_rule data = 

        map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data

    in

      add_distr_rule update_entry distr_rule ctxt

    end

    handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."

  fun add_neg_distr_rule distr_rule ctxt = 

    let

      val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule

      fun update_entry distr_rule data = 

        map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data

    in

      add_distr_rule update_entry distr_rule ctxt

    end

    handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."

end

local 

  val eq_refl2 = sym RS @{thm eq_refl}

in

  fun add_eq_distr_rule distr_rule ctxt =

    let 

      val pos_distr_rule = @{thm eq_refl} OF [distr_rule]

      val neg_distr_rule = eq_refl2 OF [distr_rule]

    in

      ctxt 

      |> add_pos_distr_rule pos_distr_rule

      |> add_neg_distr_rule neg_distr_rule

    end

end;

local

  fun sanity_check rule =

    let

      val assms = map (perhaps (try HOLogic.dest_Trueprop)) (prems_of rule)

      val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of rule);

      val (lhs, rhs) = case concl of

        Const ("Orderings.ord_class.less_eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => 

          (lhs, rhs)

        | Const ("Orderings.ord_class.less_eq", _) $ rhs $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) => 

          (lhs, rhs)

        | Const ("HOL.eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => (lhs, rhs)

        | _ => error "The rule has a wrong format."

      val lhs_vars = Term.add_vars lhs []

      val rhs_vars = Term.add_vars rhs []

      val assms_vars = fold Term.add_vars assms [];

      val _ = if has_duplicates op= lhs_vars then error "Left-hand side has variable duplicates" else ()

      val _ = if subset op= (rhs_vars, lhs_vars) then () 

        else error "Extra variables in the right-hand side of the rule"

      val _ = if subset op= (assms_vars, lhs_vars) then () 

        else error "Extra variables in the assumptions of the rule"

      val rhs_args = (snd o strip_comb) rhs;

      fun check_comp t = case t of 

        Const ("Relation.relcompp", _) $ Var (_, _) $ Var (_,_) => ()

        | _ => error "There is an argument on the rhs that is not a composition."

      val _ = map check_comp rhs_args

    in

      ()

    end

in

  fun add_distr_rule distr_rule ctxt = 

    let

      val _ = sanity_check distr_rule

      val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of distr_rule)

    in

      case concl of

        Const ("Orderings.ord_class.less_eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ => 

          add_pos_distr_rule distr_rule ctxt

        | Const ("Orderings.ord_class.less_eq", _) $ _ $ (Const ("Relation.relcompp",_) $ _ $ _) => 

          add_neg_distr_rule distr_rule ctxt

        | Const ("HOL.eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ =>

          add_eq_distr_rule distr_rule ctxt

    end

end

fun get_distr_rules_raw ctxt = Symtab.fold 

  (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) 

    (get_relator_distr_data' ctxt) []

fun get_mono_rules_raw ctxt = Symtab.fold 

  (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) 

    (get_relator_distr_data' ctxt) []

val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data

val relator_distr_attribute_setup =

  Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule))

    "declaration of relator's monoticity"

  #> Attrib.setup @{binding relator_distr} (Scan.succeed (Thm.declaration_attribute add_distr_rule))

    "declaration of relator's distributivity over OO"

  #> Global_Theory.add_thms_dynamic

     (@{binding relator_distr_raw}, get_distr_rules_raw)

  #> Global_Theory.add_thms_dynamic

     (@{binding relator_mono_raw}, get_mono_rules_raw)

(* theory setup *)

val setup =

  quot_map_attribute_setup

  #> quot_del_attribute_setup

  #> Invariant_Commute.setup

  #> relfexivity_rule_setup

  #> relator_distr_attribute_setup

(* outer syntax commands *)

val _ =

  Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions"

    (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))

val _ =

  Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"

    (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))

end