signature QUOTIENT_TERM =
sig
    val regularize_trm: Proof.context -> term -> term -> term
    val inj_repabs_trm: Proof.context -> (term * term) -> term
end;

structure Quotient_Term: QUOTIENT_TERM =
struct

(*
Regularizing an rtrm means:
 
 - Quantifiers over types that need lifting are replaced 
   by bounded quantifiers, for example:

      All P  ----> All (Respects R) P

   where the aggregate relation R is given by the rty and qty;
 
 - Abstractions over types that need lifting are replaced
   by bounded abstractions, for example:
      
      %x. P  ----> Ball (Respects R) %x. P

 - Equalities over types that need lifting are replaced by
   corresponding equivalence relations, for example:

      A = B  ----> R A B

   or 

      A = B  ----> (R ===> R) A B
 
   for more complicated types of A and B
*)

(* builds the aggregate equivalence relation *)
(* that will be the argument of Respects     *)
fun mk_resp_arg lthy (rty, qty) =
let
  val thy = ProofContext.theory_of lthy
in  
  if rty = qty
  then HOLogic.eq_const rty
  else
    case (rty, qty) of
      (Type (s, tys), Type (s', tys')) =>
       if s = s' 
       then let
              val map_info = maps_lookup thy s
                             handle NotFound => 
                               raise LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) 
              val args = map (mk_resp_arg lthy) (tys ~~ tys')
            in
              list_comb (Const (#relfun map_info, dummyT), args) 
            end  
       else let  
              val SOME qinfo = quotdata_lookup_thy thy s'
              (* FIXME: check in this case that the rty and qty *)
              (* FIXME: correspond to each other *)
              val (s, _) = dest_Const (#rel qinfo)
              (* FIXME: the relation should only be the string        *)
              (* FIXME: and the type needs to be calculated as below; *)
              (* FIXME: maybe one should actually have a term         *)
              (* FIXME: and one needs to force it to have this type   *)
            in
              Const (s, rty --> rty --> @{typ bool})
            end
      | _ => HOLogic.eq_const dummyT 
             (* FIXME: check that the types correspond to each other? *)
end

val mk_babs = Const (@{const_name Babs}, dummyT)
val mk_ball = Const (@{const_name Ball}, dummyT)
val mk_bex  = Const (@{const_name Bex}, dummyT)
val mk_resp = Const (@{const_name Respects}, dummyT)

(* - applies f to the subterm of an abstraction,   *)
(*   otherwise to the given term,                  *)
(* - used by regularize, therefore abstracted      *)
(*   variables do not have to be treated specially *)
fun apply_subt f trm1 trm2 =
  case (trm1, trm2) of
    (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f t t')
  | _ => f trm1 trm2

(* the major type of All and Ex quantifiers *)
fun qnt_typ ty = domain_type (domain_type ty)  


(* produces a regularized version of rtrm       *)
(*                                              *)
(* - the result still contains dummyTs          *)
(*                                              *)
(* - for regularisation we do not need any      *)
(*   special treatment of bound variables       *)

fun regularize_trm lthy rtrm qtrm =
  case (rtrm, qtrm) of
    (Abs (x, ty, t), Abs (_, ty', t')) =>
       let
         val subtrm = Abs(x, ty, regularize_trm lthy t t')
       in
         if ty = ty' then subtrm
         else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
       end

  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
       let
         val subtrm = apply_subt (regularize_trm lthy) t t'
       in
         if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
         else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
       end

  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
       let
         val subtrm = apply_subt (regularize_trm lthy) t t'
       in
         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
         else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
       end

  | (* equalities need to be replaced by appropriate equivalence relations *) 
    (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
         if ty = ty' then rtrm
         else mk_resp_arg lthy (domain_type ty, domain_type ty') 

  | (* in this case we just check whether the given equivalence relation is correct *) 
    (rel, Const (@{const_name "op ="}, ty')) =>
       let 
         val exc = LIFT_MATCH "regularise (relation mismatch)"
         val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
         val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 
       in 
         if rel' aconv rel then rtrm else raise exc
       end  

  | (_, Const _) =>
       let 
         fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*)
           | same_name _ _ = false
          (* TODO/FIXME: This test is not enough. *) 
          (*             Why?                     *)
          (* Because constants can have the same name but not be the same
             constant.  All overloaded constants have the same name but because
             of different types they do differ.
        
             This code will let one write a theorem where plus on nat is
             matched to plus on int, even if the latter is defined differently.
    
             This would result in hard to understand failures in injection and
             cleaning. *)
           (* cu: if I also test the type, then something else breaks *)
       in
         if same_name rtrm qtrm then rtrm
         else 
           let 
             val thy = ProofContext.theory_of lthy
             val qtrm_str = Syntax.string_of_term lthy qtrm
             val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
             val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
             val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
           in 
             if Pattern.matches thy (rtrm', rtrm) 
             then rtrm else raise exc2
           end
       end 

  | (t1 $ t2, t1' $ t2') =>
       (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')

  | (Bound i, Bound i') =>
       if i = i' then rtrm 
       else raise (LIFT_MATCH "regularize (bounds mismatch)")

  | _ =>
       let 
         val rtrm_str = Syntax.string_of_term lthy rtrm
         val qtrm_str = Syntax.string_of_term lthy qtrm
       in
         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
       end



(*
Injection of Rep/Abs means:

  For abstractions
:
  * If the type of the abstraction needs lifting, then we add Rep/Abs 
    around the abstraction; otherwise we leave it unchanged.
 
  For applications:
  
  * If the application involves a bounded quantifier, we recurse on 
    the second argument. If the application is a bounded abstraction,
    we always put an Re/Abs around it (since bounded abstractions
    always need lifting). Otherwise we recurse on both arguments.

  For constants:

  * If the constant is (op =), we leave it always unchanged. 
    Otherwise the type of the constant needs lifting, we put
    and Rep/Abs around it. 

  For free variables:

  * We put aRep/Abs around it if the type needs lifting.

  Vars case cannot occur.
*)

fun mk_repabs lthy (T, T') trm = 
  Quotient_Def.get_fun repF lthy (T, T') 
    $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)


(* bound variables need to be treated properly,     *)
(* as the type of subterms needs to be calculated   *)

fun inj_repabs_trm lthy (rtrm, qtrm) =
 case (rtrm, qtrm) of
    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

  | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
      let
        val rty = fastype_of rtrm
        val qty = fastype_of qtrm
      in
        mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))
      end

  | (Abs (x, T, t), Abs (x', T', t')) =>
      let
        val rty = fastype_of rtrm
        val qty = fastype_of qtrm
        val (y, s) = Term.dest_abs (x, T, t)
        val (_, s') = Term.dest_abs (x', T', t')
        val yvar = Free (y, T)
        val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
      in
        if rty = qty then result
        else mk_repabs lthy (rty, qty) result
      end

  | (t $ s, t' $ s') =>  
       (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))

  | (Free (_, T), Free (_, T')) => 
        if T = T' then rtrm 
        else mk_repabs lthy (T, T') rtrm

  | (_, Const (@{const_name "op ="}, _)) => rtrm

  | (_, Const (_, T')) =>
      let
        val rty = fastype_of rtrm
      in 
        if rty = T' then rtrm
        else mk_repabs lthy (rty, T') rtrm
      end   
  
  | _ => raise (LIFT_MATCH "injection (default)")

end; (* structure *)

open Quotient_Term;