Theory Automatic_Refinement.Autoref_Fix_Rel

section ‹Relator Fixing›
theory Autoref_Fix_Rel
imports Autoref_Id_Ops
begin

ML_val "2 upto 5"

subsubsection ‹Priority tags›
text ‹
  Priority tags are used to influence the ordering of refinement theorems.
  A priority tag defines two numeric priorities, a major and a minor priority.
  The major priority is considered first, the minor priority last, i.e., after
  the homogenity and relator-priority criteria.
  The default value for both priorities is 0.
›
definition PRIO_TAG :: "int ⇒ int ⇒ bool" 
  where [simp]: "PRIO_TAG ma mi ≡ True"
lemma PRIO_TAGI: "PRIO_TAG ma mi" by simp

abbreviation "MAJOR_PRIO_TAG i ≡ PRIO_TAG i 0"
abbreviation "MINOR_PRIO_TAG i ≡ PRIO_TAG 0 i"
abbreviation "DFLT_PRIO_TAG ≡ PRIO_TAG 0 0"

text ‹Some standard tags›
abbreviation "PRIO_TAG_OPTIMIZATION ≡ MINOR_PRIO_TAG 10"
  ― ‹Optimized version of an algorithm, with additional side-conditions›
abbreviation "PRIO_TAG_GEN_ALGO ≡ MINOR_PRIO_TAG (- 10)"
  ― ‹Generic algorithm, considered to be less efficient than default algorithm›


subsection ‹Solving Relator Constraints›
text ‹
  In this phase, we try to instantiate the annotated relators, using
  the available refinement rules.
›

definition CONSTRAINT :: "'a ⇒ ('c×'a) set ⇒ bool" 
  where [simp]: "CONSTRAINT f R ≡ True"

lemma CONSTRAINTI: "CONSTRAINT f R" by auto

ML ‹
  structure Autoref_Rules = Named_Thms ( 
    val name = @{binding autoref_rules_raw}
    val description = "Refinement Framework: " ^
        "Automatic refinement rules" 
  );
›
setup Autoref_Rules.setup


text ‹Generic algorithm tags have to be defined here, as we need them for
  relator fixing !›

definition PREFER_tag :: "bool ⇒ bool" 
  where [simp, autoref_tag_defs]: "PREFER_tag x ≡ x"
definition DEFER_tag :: "bool ⇒ bool" 
  where [simp, autoref_tag_defs]: "DEFER_tag x ≡ x"

lemma PREFER_tagI: "P ⟹ PREFER_tag P" by simp
lemma DEFER_tagI: "P ⟹ DEFER_tag P" by simp
lemmas SIDEI = PREFER_tagI DEFER_tagI

definition [simp, autoref_tag_defs]: "GEN_OP_tag P == P"
lemma GEN_OP_tagI: "P ==> GEN_OP_tag P" by simp
abbreviation "SIDE_GEN_OP P == PREFER_tag (GEN_OP_tag P)"
text ‹Shortcut for assuming an operation in a generic algorithm lemma›
abbreviation "GEN_OP c a R ≡ SIDE_GEN_OP ((c,OP a ::: R) ∈ R)"


definition TYREL :: "('a×'b) set ⇒ bool" 
  where [simp]: "TYREL R ≡ True"
definition TYREL_DOMAIN :: "'a itself ⇒ bool" 
  where [simp]: "TYREL_DOMAIN i ≡ True"

lemma TYREL_RES: "⟦ TYREL_DOMAIN TYPE('a); TYREL (R::(_×'a) set) ⟧ ⟹ TYREL R"
  .

lemma DOMAIN_OF_TYREL: "TYREL (R::(_×'a) set) 
  ⟹ TYREL_DOMAIN TYPE('a)" by simp

lemma TYRELI: "TYREL (R::(_×'a) set)" by simp

lemma ty_REL: "TYREL (R::(_×'a) set)" by simp


ML ‹
  
  signature AUTOREF_FIX_REL = sig
    
    type constraint = (term * term) list * (term * term)
    type thm_pairs = (constraint option * thm) list 
    type hom_net = (int * thm) Net.net

    val thm_pairsD_init: Proof.context -> Proof.context
    val thm_pairsD_get: Proof.context -> thm_pairs

    val constraints_of_term: term -> (term * term) list
    val constraints_of_goal: int -> thm -> (term * term) list

    val mk_CONSTRAINT: term * term -> term 
    val mk_CONSTRAINT_rl: Proof.context -> constraint -> thm

    val insert_CONSTRAINTS_tac: Proof.context -> tactic'

    val constraint_of_thm: Proof.context -> thm -> constraint

    datatype prio_relpos = 
      PR_FIRST 
    | PR_LAST 
    | PR_BEFORE of string 
    | PR_AFTER of string

    val declare_prio: string -> term -> prio_relpos -> local_theory -> local_theory
    val delete_prio: string -> local_theory -> local_theory

    val print_prios: Proof.context -> unit

    val compute_hom_net: thm_pairs -> Proof.context -> hom_net

    val add_hom_rule: thm -> Context.generic -> Context.generic
    val del_hom_rule: thm -> Context.generic -> Context.generic
    val get_hom_rules: Proof.context -> thm list

    val add_tyrel_rule: thm -> Context.generic -> Context.generic
    val del_tyrel_rule: thm -> Context.generic -> Context.generic
    val get_tyrel_rules: Proof.context -> thm list


    val insert_tyrel_tac : Proof.context -> int -> int -> tactic'
    val solve_tyrel_tac : Proof.context -> tactic'
    val tyrel_tac : Proof.context -> itactic


    val internal_hom_tac: Proof.context -> itactic
    val internal_spec_tac: Proof.context -> itactic
    val internal_solve_tac: Proof.context -> itactic

    val guess_relators_tac: Proof.context -> itactic
  
    val pretty_constraint: Proof.context -> constraint -> Pretty.T
    val pretty_constraints: Proof.context -> constraint list -> Pretty.T

    val pretty_thm_pair: Proof.context -> (constraint option * thm) -> Pretty.T
    val pretty_thm_pairs: Proof.context -> thm_pairs -> Pretty.T

    val analyze: Proof.context -> int -> int -> thm -> bool
    val pretty_failure: Proof.context -> int -> int -> thm -> Pretty.T

    val try_solve_tac: Proof.context -> tactic'
    val solve_step_tac: Proof.context -> tactic'
    val phase: Autoref_Phases.phase

    val setup: theory -> theory
  end

  structure Autoref_Fix_Rel :AUTOREF_FIX_REL = struct

    type constraint = (term * term) list * (term * term)
    type thm_pairs = (constraint option * thm) list 
    type hom_net = (int * thm) Net.net


    (*********************)
    (*    Constraints    *)
    (*********************)
    local
      fun fix_loose_bvars env t = 
        if Term.is_open t then 
          let
            val frees = tag_list 0 env 
              |> map (fn (i,(n,T)) => Free (":"^string_of_int i ^ "_" ^ n,T)) 
          in
            subst_bounds (frees, t)
          end
        else t

      fun constraints env @{mpat "OP ?f ::: ?R"} = 
          ( Term.is_open R andalso raise TERM ("Loose bvar in relator",[R]);
            [(fix_loose_bvars env f,R)]
          )
        | constraints _ (Free _) = []
        | constraints _ (Bound _) = []
        | constraints env @{mpat "?f ::: _"} = constraints env f
        | constraints env @{mpat "?f$?x"} 
          = constraints env x @ constraints env f
        | constraints env @{mpat "PROTECT (λx. PROTECT ?t)"} 
          = constraints ((x,x_T)::env) t
        | constraints _ @{mpat "PROTECT PROTECT"} = []
        | constraints _ t = raise TERM ("constraints_of_term",[t])
    in 
      val constraints_of_term = constraints [] 
    end

    fun constraints_of_goal i st =
      case Logic.concl_of_goal (Thm.prop_of st) i of
        @{mpat "Trueprop ((_,?a)∈_)"} => constraints_of_term a
      | _ => raise THM ("constraints_of_goal",i,[st])


    fun mk_CONSTRAINT (f,R) = let
      val fT = fastype_of f
      val RT = fastype_of R
      val res = Const (@{const_name CONSTRAINT},fT --> RT --> HOLogic.boolT)
        $f$R
    in 
      res
    end;

    (* Types of f and R must match! *)
    fun mk_CONSTRAINT_rl ctxt (ps,c) = let
      val ps = map (mk_CONSTRAINT #> HOLogic.mk_Trueprop) ps
      val c = mk_CONSTRAINT c |> HOLogic.mk_Trueprop
      val g = Logic.list_implies (ps,c)
    in
      Goal.prove ctxt [] [] g
        (fn {context = goal_ctxt, ...} => resolve_tac goal_ctxt @{thms CONSTRAINTI} 1)
    end;

    (* Internal use for hom-patterns, f and R are unified *)
    fun mk_CONSTRAINT_rl_atom ctxt (f,R) = let
      val ts = map (SOME o Thm.cterm_of ctxt) [f,R]
      val idx = Term.maxidx_term f (Term.maxidx_of_term R) + 1
    in 
      infer_instantiate' ctxt ts (Thm.incr_indexes idx @{thm CONSTRAINTI})
    end;

    fun insert_CONSTRAINTS_tac ctxt i st = let
      val cs = constraints_of_goal i st 
      |> map (mk_CONSTRAINT #> HOLogic.mk_Trueprop #> Thm.cterm_of ctxt)
    in
      Refine_Util.insert_subgoals_tac cs i st
    end

    fun constraint_of_thm ctxt thm = let 
      exception NO_REL of term
      open Autoref_Tagging

      fun extract_entry t = 
        case Logic.strip_imp_concl (strip_all_body t) of
          @{mpat "Trueprop ((_,?f)∈_)"} => SOME (fst (strip_app f),t)
        | _ => NONE

      fun relator_of t = let
        (*val _ = tracing (Syntax.string_of_term @{context} t)*)

        val t = strip_all_body t
        val prems = Logic.strip_imp_prems t
        val concl = Logic.strip_imp_concl t
      in
        case concl of 
          @{mpat "Trueprop ((_,?t)∈?R)"} => let
            val (f,args) = strip_app t
          in
            case f of 
              @{mpat "OP ?f:::?rel"} => (f,rel)
            | _ => let
                val rels = map_filter extract_entry prems
                fun find_rel t = case filter (fn (t',_) => t=t') rels of
                  [(_,t)] => snd (relator_of t)
                | _ => raise NO_REL t

                val argrels = map find_rel args
                val rel = fold Relators.mk_fun_rel (rev argrels) R
              in
                (f,rel)
              end
          end
        | _ => raise THM ("constraint_of_thm: Invalid concl",~1,[thm])
      end

      val (f,rel) = relator_of (Thm.prop_of thm) 
        handle exc as (NO_REL t) => (
          warning (
            "Could not infer unique higher-order relator for "
            ^ "refinement rule: \n"
            ^ Thm.string_of_thm ctxt thm
            ^ "\n for argument: " 
            ^ Syntax.string_of_term ctxt t
          ); 
          Exn.reraise exc)

      (* Extract GEN_OP-tags *)
      fun 
        genop_cs @{mpat "Trueprop (SIDE_GEN_OP ((_,OP ?f ::: _) ∈ ?R))"} = 
          if has_Var f then NONE else SOME (f,R)
      | genop_cs _ = NONE

      val gen_ops = Thm.prems_of thm
        |> map_filter genop_cs

    in
      (gen_ops,(f,rel))
    end

    (*********************)
    (*    Priorities     *)
    (*********************)
    structure Rel_Prio_List = Prio_List (
      type item = string * term
      val eq = (op =) o apply2 fst 
    )

    structure Rel_Prio = Generic_Data (
      type T = Rel_Prio_List.T
      val empty = Rel_Prio_List.empty
      val merge = Rel_Prio_List.merge
    )

    fun pretty_rel_prio ctxt (s,t) = Pretty.block [
      Pretty.str s, Pretty.str ":", Pretty.brk 1,
      Syntax.pretty_term ctxt t
    ]

    fun print_prios ctxt = let
      val rpl = Rel_Prio.get (Context.Proof ctxt)
    in
      (map (pretty_rel_prio ctxt) rpl)
      |> Pretty.big_list "Relator Priorities"
      |> Pretty.string_of
      |> warning
    end


    datatype prio_relpos = 
      PR_FIRST 
    | PR_LAST 
    | PR_BEFORE of string 
    | PR_AFTER of string

    fun declare_prio name pat0 relpos lthy = 
      let
        val pat1 = Proof_Context.cert_term lthy pat0
        val pat2 = singleton (Variable.export_terms (Proof_Context.augment pat1 lthy) lthy) pat1
      in
        lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = ⌂}
          (fn phi =>
            let val item = (name, Morphism.term phi pat2) in
              Rel_Prio.map (fn rpl =>
                case relpos of
                  PR_FIRST => Rel_Prio_List.add_first rpl item
                | PR_LAST => Rel_Prio_List.add_last rpl item
                | PR_BEFORE n => Rel_Prio_List.add_before rpl item (n,Term.dummy)
                | PR_AFTER n => Rel_Prio_List.add_after rpl item (n,Term.dummy)
              )
            end)
      end

    fun delete_prio name = Local_Theory.declaration {syntax = false, pervasive = false, pos = ⌂}
      (fn phi => Rel_Prio.map (Rel_Prio_List.delete (name, Term.dummy)))

    local
      fun relators_of R = let
        fun f @{mpat "?R1.0→?R2.0"} = f R1 @ f R2
          | f R = [R]
      in
        f R |> map Refine_Util.anorm_term |> distinct (op =)
      end

      fun dest_prio_tag @{mpat "Trueprop (PRIO_TAG ?ma ?mi)"} = 
            apply2 (#2 o HOLogic.dest_number) (ma,mi)
        | dest_prio_tag t = raise TERM ("dest_prio_tag",[t])

      fun get_tagged_prios thm = let
        val prems = Thm.prems_of thm
        fun r [] = (0,0)
          | r (prem::prems) = (
              case try dest_prio_tag prem of
                NONE => r prems
              | SOME p => p
            ) 

      in
        r prems
      end

      fun prio_order_of ctxt (SOME (_,(_,R)),thm) = 
        let
          val rels = relators_of R
          val hom = length rels
          val (major_prio,minor_prio) = get_tagged_prios thm

          val rpl = Rel_Prio.get (Context.Proof ctxt)
          val matches = Pattern.matches (Proof_Context.theory_of ctxt)
          fun prefer ((_,p1),(_,p2)) = matches (p2,p1)
          fun prio_of R 
            = Rel_Prio_List.prio_of (fn (_,pat) => matches (pat,R)) prefer rpl 
              + 1
          val prio = fold (fn R => fn s => prio_of R + s) rels 0
        in
          (major_prio, (hom,(prio,minor_prio)))
        end
      | prio_order_of _ _ = raise Match

      val prio_order = 
        prod_ord
          (rev_order o int_ord)
          (prod_ord 
            int_ord
            (prod_ord (rev_order o int_ord) (rev_order o int_ord)))

      fun annotate_thm_pair ctxt (SOME (ps,(f,R)),thm) = 
        let
          open Autoref_Tagging  Conv

          fun warn () = warning ("Error annotating refinement theorem: "
            ^ Thm.string_of_thm ctxt thm
          )

          val R_cert = Thm.cterm_of ctxt R

          fun cnv ctxt ct = (case Thm.term_of ct of
            @{mpat "OP _ ::: _"} => all_conv
          | @{mpat "OP _"} => mk_rel_ANNOT_conv ctxt R_cert
          | @{mpat "_ $ _"} => arg1_conv (cnv ctxt)
          | _ => mk_OP_conv then_conv mk_rel_ANNOT_conv ctxt R_cert

          ) ct

          (*val _ = tracing ("ANNOT: " ^ @{make_string} thm)*)
          val thm = (fconv_rule (rhs_conv cnv ctxt)) thm
          val thm = case try (fconv_rule (rhs_conv cnv ctxt)) thm of
            NONE => (warn (); thm)
          | SOME thm => thm
          (*val _ = tracing ("RES: " ^ @{make_string} thm)*)

        in
          (SOME (ps,(f,R)),thm)
        end
      | annotate_thm_pair _ p = p

    in
      fun compute_thm_pairs ctxt = let
        val rules = Autoref_Rules.get ctxt
        fun add_o p = (prio_order_of ctxt p,p)

        val pairs = rules
          |> map (fn thm => (try (constraint_of_thm ctxt) thm,thm))
        val spairs = filter (is_some o #1) pairs
          |> map add_o 
          |> sort (prio_order o apply2 #1)
          |> map #2
        val npairs = filter (is_none o #1) pairs
      in
        spairs@npairs |> map (annotate_thm_pair ctxt)
      end
    end

    structure thm_pairsD = Autoref_Data (
      type T = thm_pairs
      val compute = compute_thm_pairs
      val prereq = []
    )

    val thm_pairsD_init = thm_pairsD.init
    val thm_pairsD_get = thm_pairsD.get

    structure hom_rules = Named_Sorted_Thms (
      val name = @{binding autoref_hom}
      val description = "Autoref: Homogenity rules"
      val sort = K I
      val transform = K (
        fn thm => case Thm.concl_of thm of 
          @{mpat "Trueprop (CONSTRAINT _ _)"} => [thm]
        | _ => raise THM ("Invalid homogenity rule",~1,[thm])
      )
    )
  
    val add_hom_rule = hom_rules.add_thm
    val del_hom_rule = hom_rules.del_thm
    val get_hom_rules = hom_rules.get

    local
      open Relators
      fun 
        repl @{mpat "?R→?S"} ctab = let
          val (R,ctab) = repl R ctab
          val (S,ctab) = repl S ctab
        in (mk_fun_rel R S,ctab) end
      | repl R ctab = let
          val (args,R) = strip_relAPP R
          val (args,ctab) = fold_map repl args ctab 
          val (ctxt,tab) = ctab

          val (R,(ctxt,tab)) = case Termtab.lookup tab R of
            SOME R => (R,(ctxt,tab))
          | NONE => let
              val aT = fastype_of R |> strip_type |> #2 
                |> HOLogic.dest_setT |> HOLogic.dest_prodT |> #2
              val (cT,ctxt) = yield_singleton Variable.invent_types @{sort type} ctxt
              val cT = TFree cT
              val T = map fastype_of args ---> HOLogic.mk_setT (HOLogic.mk_prodT (cT,aT))
              val (R',ctxt) = yield_singleton Variable.variant_fixes "R" ctxt
              val R' = list_relAPP args (Free (R',T))
              val tab = Termtab.update (R,R') tab
            in (R',(ctxt,tab)) end
        in 
          (R,(ctxt,tab))   
        end

      fun hom_pat_of_rel ctxt R = let
        val (R,(ctxt',_)) = repl R (ctxt,Termtab.empty)
        val R = singleton (Variable.export_terms ctxt' ctxt) R
      in
        Refine_Util.anorm_term R
      end

    in
      fun compute_hom_net pairs ctxt = let
        val cs = map_filter #1 pairs
        val cs' = map (fn (_,(f,R)) => (f,hom_pat_of_rel ctxt R)) cs
        val thms = get_hom_rules ctxt @ map (mk_CONSTRAINT_rl_atom ctxt) cs'
        val thms = map (Thm.cprop_of #> Thm.trivial) thms
        val net = Tactic.build_net thms
      in
        net
      end
    end

    structure hom_netD = Autoref_Data (
      type T = hom_net
      fun compute ctxt = compute_hom_net (thm_pairsD.get ctxt) ctxt
      val prereq = [ thm_pairsD.init ]
    )

    structure tyrel_rules = Named_Sorted_Thms (
      val name = @{binding autoref_tyrel}
      val description = "Autoref: Type-based relator fixing rules"
      val sort = K I

      val transform = K (
        fn thm => case Thm.prop_of thm of 
          @{mpat "Trueprop (TYREL _)"} => [thm]
        | _ => raise THM ("Invalid tyrel-rule",~1,[thm])
      )
    )

    val add_tyrel_rule = tyrel_rules.add_thm
    val del_tyrel_rule = tyrel_rules.del_thm
    val get_tyrel_rules = tyrel_rules.get

    local
      (*fun rel_annots @{mpat "_ ::: ?R"} = [R]
        | rel_annots @{mpat "?f$?x"} = rel_annots f @ rel_annots x
        | rel_annots @{mpat "PROTECT (λ_. PROTECT ?t)"} = rel_annots t
        | rel_annots @{mpat "PROTECT PROTECT"} = []
        | rel_annots (Free _) = []
        | rel_annots (Bound _) = []
        | rel_annots t = raise TERM ("rel_annots",[t])
      *)

      fun add_relators t acc = let
        open Relators
        val (args,_) = strip_relAPP t
        val res = fold add_relators args acc
        val res = insert (op =) t res
      in
        res
      end
  
      fun add_relators_of_subgoal st i acc = 
        case Logic.concl_of_goal (Thm.prop_of st) i of
          @{mpat "Trueprop (CONSTRAINT _ ?R)"} => add_relators R acc
        | _ => acc
  
    in

      fun insert_tyrel_tac ctxt i j k st = let
        fun get_constraint t = let
          val T = fastype_of t
          val res = Const (@{const_name TYREL}, T --> HOLogic.boolT) $ t
        in
          res |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt
        end
        
        val relators = fold (add_relators_of_subgoal st) (i upto j) []
        val tyrels = map get_constraint relators
      in
        Refine_Util.insert_subgoals_tac tyrels k st
      end
    end

    fun solve_tyrel_tac ctxt = let
      fun mk_tac rl = resolve_tac ctxt @{thms TYREL_RES} 
        THEN' match_tac ctxt [rl RS @{thm DOMAIN_OF_TYREL}]
        THEN' resolve_tac ctxt [rl]

      val tac = FIRST' (map mk_tac (tyrel_rules.get ctxt))
    in
      DETERM o tac ORELSE' (TRY o resolve_tac ctxt @{thms TYRELI})
    end
    
    fun tyrel_tac ctxt i j =
      (insert_tyrel_tac ctxt i j
      THEN_ALL_NEW_FWD solve_tyrel_tac ctxt) i



    fun internal_hom_tac ctxt = let
      val hom_net = hom_netD.get ctxt
    in
      Seq.INTERVAL (TRY o DETERM o resolve_from_net_tac ctxt hom_net)    
    end

    fun internal_spec_tac ctxt = let
      val pairs = thm_pairsD.get ctxt
      val net = pairs
        |> map_filter (fst #> map_option (snd #> mk_CONSTRAINT_rl_atom ctxt))
        |> Tactic.build_net
    in 
      fn i => fn j => REPEAT (CHANGED 
        (Seq.INTERVAL (DETERM o Anti_Unification.specialize_net_tac ctxt net) i j)
      )
    end

    fun apply_to_constraints tac = let
      fun no_CONSTRAINT_tac i st = 
        case Logic.concl_of_goal (Thm.prop_of st) i of
          @{mpat "Trueprop (CONSTRAINT _ _)"} => Seq.empty
        | _ => Seq.single st  

    in
      Seq.INTERVAL (no_CONSTRAINT_tac ORELSE' tac)
    end

    fun internal_solve_tac ctxt = let
      val pairs = thm_pairsD.get ctxt
      val net = pairs
        |> map_filter (fst #> map_option (mk_CONSTRAINT_rl ctxt))
        |> Tactic.build_net

      val s_tac = SOLVED' (REPEAT_ALL_NEW (resolve_from_net_tac ctxt net))
    in 
      apply_to_constraints s_tac
      ORELSE_INTERVAL 
      apply_to_constraints (TRY o DETERM o s_tac)
    end

    fun guess_relators_tac ctxt = let
      val pairs = thm_pairsD.get ctxt
      val net = pairs
        |> map_filter (fst #> map_option (mk_CONSTRAINT_rl ctxt))
        |> Tactic.build_net

      val hom_net = hom_netD.get ctxt

      fun hom_tac i j = Seq.INTERVAL 
        (TRY o DETERM o resolve_from_net_tac ctxt hom_net) i j

      fun spec_tac i j = 
        REPEAT (CHANGED 
          (Seq.INTERVAL (DETERM o Anti_Unification.specialize_net_tac ctxt net) i j)
        )

      val solve_tac = let 
        val s_tac = SOLVED' (REPEAT_ALL_NEW (resolve_from_net_tac ctxt net))
      in   
        apply_to_constraints s_tac
        ORELSE_INTERVAL 
        apply_to_constraints (TRY o DETERM o s_tac)
      end
    in
      Seq.INTERVAL (insert_CONSTRAINTS_tac ctxt)
      THEN_INTERVAL hom_tac
      THEN_INTERVAL spec_tac
      THEN_INTERVAL (tyrel_tac ctxt)
      THEN_INTERVAL solve_tac
    end


    (*********************)
    (*  Pretty Printing  *)
    (*********************)

    fun pretty_constraint_atom ctxt (f,R) = Pretty.block 
      [ Syntax.pretty_term ctxt f,
        Pretty.str " :: ",
        Syntax.pretty_typ ctxt (fastype_of f),
        Pretty.str " ::: ",
        Syntax.pretty_term ctxt R]

    fun pretty_constraint ctxt (ps,(f,R)) = 
      case ps of 
        [] => pretty_constraint_atom ctxt (f,R)
      | _ => Pretty.block [
               map (pretty_constraint_atom ctxt) ps 
               |> Pretty.separate "; " 
               |> Pretty.enclose "⟦" "⟧",
               Pretty.brk 1, Pretty.str "⟹", Pretty.brk 1,
               pretty_constraint_atom ctxt (f,R)
             ]


    fun pretty_constraints ctxt l = Pretty.big_list "Constraints" 
      (map (pretty_constraint ctxt) l)

    fun pretty_thm_pair ctxt (c,thm) = Pretty.block [
      case c of 
        NONE => Pretty.str "NONE"
      | SOME c => pretty_constraint ctxt c,
      Pretty.brk 2, Pretty.str "---", Pretty.brk 2,
      Thm.pretty_thm ctxt thm
    ]

    fun pretty_thm_pairs ctxt pairs = Pretty.big_list "Thm-Pairs"
      (map (pretty_thm_pair ctxt) pairs)

    local
      fun unifies ctxt (t1, t2) = Term.could_unify (t1, t2) andalso
        let
          val idx1 = Term.maxidx_of_term t1
          val t2 = Logic.incr_indexes ([], idx1 + 1) t2
          val idx2 = Term.maxidx_of_term t2
        in
          can (Pattern.unify (Context.Proof ctxt) (t1,t2)) (Envir.empty idx2)
        end

      fun analyze_possible_problems ctxt (f,R) = let

        fun strange_aux sf R = 
        ( 
          if sf then 
            let
              val T = fastype_of R
            in 
              case try (HOLogic.dest_prodT o HOLogic.dest_setT) T of
                SOME _ => []
              | NONE => [Pretty.block [
                  Pretty.str "Strange relator type, expected plain relation: ",
                  Syntax.pretty_term (Config.put show_types true ctxt) R
                ]]
            end
          else []
        ) @ ( 
          case R of
            @{mpat "⟨?R⟩?S"} => strange_aux true R @ strange_aux false S
          | Var (_,T) => (
              case 
                try (HOLogic.dest_prodT o HOLogic.dest_setT) (#2 (strip_type T))
              of
                SOME (TFree _,_) => [Pretty.block [
                  Pretty.str "Fixed concrete type on schematic relator: ",
                  Syntax.pretty_term (Config.put show_types true ctxt) R
                ]]
              | _ => []
            )
          | _ => []
        )

        val strange = case strange_aux true R of 
          [] => NONE
        | l => SOME (Pretty.block l)

        val folded_relator = let
          fun 
            match (Type (name,args)) R = 
              let
                val (Rargs,Rhd) = Relators.strip_relAPP R
              in 
                if is_Var Rhd then []
                else if length args <> length Rargs then
                  [Pretty.block [ 
                    Pretty.str "Type/relator arity mismatch:",
                    Pretty.brk 1,
                    Pretty.block [
                      Pretty.str name, Pretty.str "/", 
                      Pretty.str (string_of_int (length args))
                    ],
                    Pretty.brk 1,Pretty.str "vs.",Pretty.brk 1,
                    Pretty.block [
                      Syntax.pretty_term ctxt Rhd, Pretty.str "/", 
                      Pretty.str (string_of_int (length Rargs))
                    ]
                  ]]
                else
                  args ~~ Rargs |> map (uncurry match) |> flat

              end
          | match _ _ = []   

        in 
          case match (fastype_of f) R of
            [] => NONE 
          | l => SOME (Pretty.block (Pretty.fbreaks l @ [Pretty.fbrk,
              Pretty.str ("Explanation: This may be due to using polymorphic "
              ^ "relators like Id on non-terminal types." 
              ^ "A problem usually occurs when "
              ^ "this relator has to be matched against a fully unfolded one."
              ^ "This warning is also issued on partially parametric relators "
              ^ "like br. However, the refinement rules are usually set up to "
              ^ "compensate for this, so this is probably not the cause for an "
              ^ "unsolved constraint")
            ]))
        end


        val issues = [strange, folded_relator]
          |> map_filter I
      in
        case issues of
          [] => NONE
        | l => SOME (Pretty.big_list "Possible problems" l)

      end

      fun pretty_try_candidates ctxt i st = if i > Thm.nprems_of st then
        Pretty.str "Goal number out of range"
      else
        case Logic.concl_of_goal (Thm.prop_of st) i of
          @{mpat "Trueprop (CONSTRAINT ?f ?R)"} =>
            let
              val pairs = thm_pairsD.get ctxt
              val st = Drule.zero_var_indexes st

              val pt_hd = Pretty.block [
                Pretty.str "Head: ", Pretty.fbrk,
                pretty_constraint_atom ctxt (f,R)
              ]

              fun isc (SOME (ps,(fp,R)),_) = 
                    if unifies ctxt (f,fp) then SOME (ps,(fp,R)) else NONE
                | isc _ = NONE

              val candidates = pairs |> map_filter isc

              fun try_c c = let
                val pt1 = Pretty.block [
                  Pretty.str "Trying ",
                  pretty_constraint ctxt c
                ]

                val rl = mk_CONSTRAINT_rl ctxt c 
                   |> Drule.zero_var_indexes
                val res = (SOLVED' (resolve_tac ctxt [rl])) i st
                  |> Seq.pull |> is_some

                val pt2 = (if res then Pretty.str "OK" else Pretty.str "ERR")
                  
              in
                Pretty.block [pt1,Pretty.fbrk,pt2]
              end

              val res = Pretty.block (
                Pretty.fbreaks [pt_hd,
                  Pretty.big_list "Solving Attempts" 
                    (map try_c candidates)]
              )

            in 
              res
            end
        | _ => Pretty.str "Unexpected goal format"


      exception ERR of Pretty.T
      fun analyze' ctxt i j st = let
        val As = Logic.strip_horn (Thm.prop_of st) |> #1 
          |> drop (i-1) |> take (j-i+1)
          |> map (strip_all_body #> Logic.strip_imp_concl)
        val Cs = map_filter (
            fn @{mpat "Trueprop (CONSTRAINT ?f ?R)"} => SOME (f,R)
             | @{mpat "Trueprop ((_,_)∈_)"} => NONE
             | t => raise ERR (Pretty.block [
                 Pretty.str "Internal: Unexpected goal format: ",
                 Syntax.pretty_term ctxt t
               ])
          ) As

        val Cs_problems = map (fn c => 
          case analyze_possible_problems ctxt c of
            NONE => pretty_constraint_atom ctxt c
          | SOME p => Pretty.block [pretty_constraint_atom ctxt c,Pretty.fbrk,p]
        ) Cs
 
        val Cs_pretty = Pretty.big_list "Constraints" Cs_problems
      in
        case Cs of [] => ()
        | _ => raise ERR (Pretty.block [
            Pretty.str 
              "Could not infer all relators, some constraints remaining",
            Pretty.fbrk,
            Cs_pretty,
            Pretty.fbrk,
            Pretty.block [
              Pretty.str "Trying to solve first constraint",
              Pretty.fbrk,
              pretty_try_candidates ctxt i st
            ]
          ])
      end

    in
      fun analyze ctxt i j st = can (analyze' ctxt i j) st

      fun pretty_failure ctxt i j st = 
        (analyze' ctxt i j st; Pretty.str "No failure") handle ERR p => p

      fun try_solve_tac ctxt i st =  
        if i > Thm.nprems_of st then
          (tracing "Goal number out of range"; Seq.empty)
        else
          case Logic.concl_of_goal (Thm.prop_of st) i of
            @{mpat "Trueprop (CONSTRAINT ?f ?R)"} =>
              let
                val pairs = thm_pairsD.get ctxt
                val st = Drule.zero_var_indexes st

                val pt = Pretty.block [
                  Pretty.str "Head: ", Pretty.fbrk,
                  pretty_constraint_atom ctxt (f,R)
                ]
                val _ = tracing (Pretty.string_of pt)

                val _ = case analyze_possible_problems ctxt (f,R) of
                  NONE => ()
                | SOME p => tracing (Pretty.string_of p)
            
                fun isc (SOME (ps,(fp,R)),_) = 
                      if unifies ctxt (f,fp) then SOME (ps,(fp,R)) else NONE
                  | isc _ = NONE

                val net = pairs
                  |> map_filter (fst #> map_option (mk_CONSTRAINT_rl ctxt))
                  |> Tactic.build_net


                val candidates = pairs |> map_filter isc

                fun try_c c = let
                  val _ = Pretty.block [
                    Pretty.str "Trying ",
                    pretty_constraint ctxt c
                  ] |> Pretty.string_of |> tracing

                  val rl = mk_CONSTRAINT_rl ctxt c 
                     |> Drule.zero_var_indexes
                  val res = (SOLVED' (resolve_tac ctxt [rl] 
                      THEN_ALL_NEW (REPEAT_ALL_NEW (resolve_from_net_tac ctxt net)))
                    ) i st
                    |> Seq.pull |> is_some

                  val _ = (if res then Pretty.str "OK" else Pretty.str "ERR")
                    |> Pretty.string_of |> tracing
                in
                  ()
                end

                val _ = map try_c candidates
              in 
                Seq.single st
              end

          | _ => Seq.empty


    end


    fun solve_step_tac ctxt = let
      val pairs = thm_pairsD.get ctxt
      val net = pairs
        |> map_filter (fst #> map_option (mk_CONSTRAINT_rl ctxt))
        |> Tactic.build_net
    in 
      resolve_from_net_tac ctxt net
    end

    val phase = {
      init = thm_pairsD.init #> hom_netD.init,
      tac = guess_relators_tac,
      analyze = analyze,
      pretty_failure = pretty_failure
    }


    val setup = hom_rules.setup #> tyrel_rules.setup
  end

›

setup Autoref_Fix_Rel.setup

end