signature QUOTIENT_DEF =

sig

  datatype flag = absF | repF

  val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term

  val make_def: binding -> typ -> mixfix -> Attrib.binding -> term ->

    Proof.context -> (term * thm) * local_theory

  val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) ->

    local_theory -> (term * thm) * local_theory

  val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->

    local_theory -> local_theory

  val diff: (typ * typ) -> (typ * typ) list -> (typ * typ) list

end;

structure Quotient_Def: QUOTIENT_DEF =

struct

(* wrapper for define *)

fun define name mx attr rhs lthy =

let

  val ((rhs, (_ , thm)), lthy') =

in

  ((rhs, thm), lthy')

end

(* calculates the aggregate abs and rep functions for a given type; 

   repF is for constants' arguments; absF is for constants;

   function types need to be treated specially, since repF and absF

   change *)

datatype flag = absF | repF

fun negF absF = repF

  | negF repF = absF

fun get_fun flag qenv lthy ty =

let

  fun get_fun_aux s fs =

   (case (maps_lookup (ProofContext.theory_of lthy) s) of

      SOME info => list_comb (Const (#mapfun info, dummyT), fs)

    | NONE      => error ("no map association for type " ^ s))

  fun get_const flag qty =

  let 

    val thy = ProofContext.theory_of lthy

    val qty_name = Long_Name.base_name (fst (dest_Type qty))

  in

    case flag of

      absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)

    | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)

  end

  fun mk_identity ty = Abs ("", ty, Bound 0)

in

  if (AList.defined (op=) qenv ty)

  then (get_const flag ty)

  else (case ty of

          TFree _ => mk_identity ty

        | Type (_, []) => mk_identity ty 

        | Type ("fun" , [ty1, ty2]) => 

            let

              val fs_ty1 = get_fun (negF flag) qenv lthy ty1

              val fs_ty2 = get_fun flag qenv lthy ty2

            in  

              get_fun_aux "fun" [fs_ty1, fs_ty2]

            end 

        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)

        | _ => error ("no type variables allowed"))

end

(* returns all subterms where two types differ *)

fun diff (T, S) Ds =

  case (T, S) of

    (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds 

  | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds

  | (Type (a, Ts), Type (b, Us)) => 

      if a = b then diffs (Ts, Us) Ds else (T, S)::Ds

  | _ => (T, S)::Ds

and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)

  | diffs ([], []) Ds = Ds

  | diffs _ _ = error "Unequal length of type arguments"

(* sanity check that the calculated quotient environment

   matches with the stored quotient environment. *)

fun sanity_chk qenv lthy =

let

  val global_qenv = Quotient_Info.mk_qenv lthy

  val thy = ProofContext.theory_of lthy

  fun error_msg lthy (qty, rty) =

  let 

    val qtystr = quote (Syntax.string_of_typ lthy qty)

    val rtystr = quote (Syntax.string_of_typ lthy rty)

  in

    error (implode ["Quotient type ", qtystr, " does not match with ", rtystr])

  end

  fun is_inst (qty, rty) (qty', rty') =

    if Sign.typ_instance thy (qty, qty')

    then let

           val inst = Sign.typ_match thy (qty', qty) Vartab.empty

         in

           rty = Envir.subst_type inst rty'       

         end

    else false

  fun chk_inst (qty, rty) = 

    if exists (is_inst (qty, rty)) global_qenv 

    then true

    else error_msg lthy (qty, rty)

in

  map chk_inst qenv

end

fun make_def nconst_bname qty mx attr rhs lthy =

let

  val (arg_tys, res_ty) = strip_type qty

  val rty = fastype_of rhs

  val qenv = distinct (op=) (diff (qty, rty) [])   

  val _ = sanity_chk qenv lthy

  val rep_fns = map (get_fun repF qenv lthy) arg_tys

  val abs_fn  = (get_fun absF qenv lthy) res_ty

  fun mk_fun_map t s =  

        Const (@{const_name "fun_map"}, dummyT) $ t $ s

  val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs)

                   |> Syntax.check_term lthy 

  val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy

  val nconst_str = Binding.name_of nconst_bname

  val qcinfo = {qconst = trm, rconst = rhs}

                (fn phi => qconsts_update_generic nconst_str 

                             (qconsts_transfer phi qcinfo)) lthy'

in

  ((trm, thm), lthy'')

end

(* interface and syntax setup *)

(* the ML-interface takes a 5-tuple consisting of  *)

(*                                                 *)

(* - the name of the constant to be lifted         *)

(* - its type                                      *)

(* - its mixfix annotation                         *)

(* - a meta-equation defining the constant,        *)

(*   and the attributes of for this meta-equality  *)

fun quotdef ((bind, qty, mx), (attr, prop)) lthy =

let   

  val (_, rhs) = Primitive_Defs.abs_def prop'

in

  make_def bind qty mx attr rhs lthy 

end

fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = 

let

  val qty  = Syntax.read_typ lthy qtystr

  val prop = Syntax.read_prop lthy propstr

in

  quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd

end

val quotdef_parser =

  (OuterParse.binding --

    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- 

      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- 

       (SpecParse.opt_thm_name ":" -- OuterParse.prop)

val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"

  OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)

end; (* structure *)

open Quotient_Def;