Theory Anti_Unification

header {* Anti-Unification *}
theory Anti_Unification
imports Refine_Util
begin
  text {* We implement a simple anti-unification.
    Currently, we do not handle lambdas, nor sorts, and avoid
    higher-order variables, i.e., 
    f x and g x will be unified to ?v, not ?v x, and existing higher-order
    patterns will be collapsed, e.g.: ?f x and ?f x will become ?v.
    *}

ML {*
  signature ANTI_UNIFICATION = sig
    type typ_env
    type term_env
    type env = typ_env * term_env

    val empty_typ: typ_env
    val empty_term: term_env
    val empty: env

    val anti_unifyT: typ * typ -> typ_env -> typ * typ_env
    val anti_unify_env: term * term -> env -> term * env
    val anti_unify: term * term -> term
    val anti_unify_list: term list -> term

    val specialize_tac: thm list -> tactic'
    val specialize_net_tac: (int * thm) Net.net -> tactic'
  end


  structure Anti_Unification :ANTI_UNIFICATION = struct
    structure Term2tab = Table (
      type key = term * term 
      val ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord
    );

    structure Typ2tab = Table (
      type key = typ * typ 
      val ord = prod_ord Term_Ord.typ_ord Term_Ord.typ_ord
    );

    type typ_env = (typ Typ2tab.table * int)
    type term_env = (term Term2tab.table * int)
    type env = typ_env * term_env

    val empty_typ = (Typ2tab.empty,0)
    val empty_term = (Term2tab.empty,0)
    val empty = (empty_typ,empty_term)

    fun tvar_pair p (vtab,idx) = 
      case Typ2tab.lookup vtab p of
        NONE => let
          val tv = TVar (("T",idx),[])
          val vtab = Typ2tab.update (p,tv) vtab
        in
          (tv,(vtab,idx+1))
        end
      | SOME tv => (tv,(vtab,idx))

    fun anti_unifyT (TFree v1, TFree v2) dt =
        if v1 = v2 then (TFree v1,dt) 
        else tvar_pair (TFree v1, TFree v2) dt
      | anti_unifyT (p as (Type (n1,l1), Type (n2,l2))) dt =
        if n1 = n2 andalso (length l1 = length l2) then 
          let
            val (l,dt) = fold_map anti_unifyT (l1~~l2) dt
          in (Type (n1,l),dt) end
        else
          tvar_pair p dt
      | anti_unifyT p dt = tvar_pair p dt

    fun var_pair p (tdt,(vtab,idx)) = 
      case Term2tab.lookup vtab p of
        NONE => let
          val (T,tdt) = anti_unifyT (pairself fastype_of p) tdt
          val v = Var (("v",idx),T)
          val vtab = Term2tab.update (p,v) vtab
        in
          (v,(tdt,(vtab,idx+1)))
        end
      | SOME v => (v,(tdt,(vtab,idx)))

    fun anti_unify_env (p as (Free (n1,T1), Free (n2,T2))) (tdt,dt) = 
        if n1 = n2 then 
          let 
            val (T,tdt) = anti_unifyT (T1,T2) tdt 
          in (Free (n1,T),(tdt,dt)) end
        else
          var_pair p (tdt,dt)
      | anti_unify_env (p as (Const (n1,T1), Const (n2,T2))) (tdt,dt) =
        if n1 = n2 then 
          let 
            val (T,tdt) = anti_unifyT (T1,T2) tdt 
          in (Const (n1,T),(tdt,dt)) end
        else
          var_pair p (tdt,dt)
      | anti_unify_env (p as (f1$x1,f2$x2)) dtp = 
        let 
          val (f,dtp) = anti_unify_env (f1,f2) dtp
        in 
          if is_Var f then
            var_pair p dtp
          else let
            val (x,dtp) = anti_unify_env (x1,x2) dtp
          in (f$x,dtp) end
        end
      | anti_unify_env p dtp = var_pair p dtp

    fun anti_unify p = anti_unify_env p empty |> #1

    fun anti_unify_list l = let
      fun f [] _ = raise TERM ("anti_unify_list: Empty",[])
        | f [t] dt = (t,dt)
        | f (t1::t2::ts) dt = let
            val (t,dt) = anti_unify_env (t1,t2) dt
          in f (t::ts) dt end
    in
      f l empty |> #1
    end

    local
      fun specialize_aux_tac get_candidates i st = let
        val thy = theory_of_thm st
        val maxidx = Thm.maxidx_of st
        val concl = Logic.concl_of_goal (prop_of st) i
        val pre_candidates = get_candidates concl
          |> map (fn thm => 
               let
                 val tidx = Thm.maxidx_of thm
                 val t = Thm.incr_indexes maxidx thm |> concl_of
               in (maxidx + tidx,t) end)

        fun unifies (idx,t) 
          = can (Pattern.unify thy (t,concl)) (Envir.empty idx)

        val candidates = filter unifies pre_candidates |> map #2
      in
        case candidates of 
          [] => Seq.single st
        | _ => let
            val thy = theory_of_thm st
            val pattern = anti_unify_list candidates
              |> cterm_of thy |> Thm.trivial
            (*val _ = tracing (Display.string_of_thm_without_context pattern)*)
          in 
            rtac pattern i st
          end
      end
    in
      fun specialize_tac thms = let
        fun get_candidates concl = 
          filter (fn thm => Term.could_unify (concl_of thm,concl)) thms

      in 
        specialize_aux_tac get_candidates
      end

      fun specialize_net_tac net = let
        fun get_candidates concl = Net.unify_term net concl |> map #2
      in 
        specialize_aux_tac get_candidates
      end
    end



  end
*}



end