(*  Title:      quotient_def.thy
    Author:     Cezary Kaliszyk and Christian Urban

    Definitions for constants on quotient types.

*)

signature QUOTIENT_DEF =
sig
  val quotient_def: (binding * mixfix) option * (Attrib.binding * (term * term)) ->
    local_theory -> (term * thm) * local_theory

  val quotdef_cmd: (binding * mixfix) option * (Attrib.binding * (string * string)) ->
    local_theory -> (term * thm) * local_theory
end;

structure Quotient_Def: QUOTIENT_DEF =
struct

open Quotient_Info;
open Quotient_Term;

(** Interface and Syntax Setup **)

(* The ML-interface for a quotient definition takes
   as argument:

    - the mixfix annotation
    - name and attributes
    - the new constant as term
    - the rhs of the definition as term

   It returns the defined constant and its definition
   theorem; stores the data in the qconsts data slot.

   Restriction: At the moment the right-hand side must
   be a terms composed of constant. Similarly the
   left-hand side must be a single constant.
*)
fun quotient_def (bindmx, (attr, (lhs, rhs))) lthy =
let
  val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
  val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
  val der_bname = Binding.name lhs_str
  val (qconst_bname, mx) =
    case bindmx of
      SOME (bname, mx) =>
        let
          val _ = (Name.of_binding bname = lhs_str) orelse error ("Head of quotient_definition " ^ 
            (quote lhs_str) ^ " differs from declaration " ^ (Binding.name_of bname) ^
            Position.str_of (Binding.pos_of bname))
        in
          (der_bname, mx)
        end
      | NONE => (der_bname, NoSyn)
  val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
  val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
  val (_, prop') = LocalDefs.cert_def lthy prop
  val (_, newrhs) = Primitive_Defs.abs_def prop'

  val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy

  (* data storage *)
  fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
  fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
  val lthy'' = Local_Theory.declaration true
                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
in
  ((trm, thm), lthy'')
end

fun quotdef_cmd (bindmx, (attr, (lhs_str, rhs_str))) lthy =
let
  val lhs = Syntax.read_term lthy lhs_str
  val rhs = Syntax.read_term lthy rhs_str
  val lthy' = Variable.declare_term lhs lthy
  val lthy'' = Variable.declare_term rhs lthy'
in
  quotient_def (bindmx, (attr, (lhs, rhs))) lthy''
end

val binding_mixfix_parser = OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where"
val quotdef_parser =
  (Scan.option binding_mixfix_parser) --
    OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term))

val _ =
  OuterSyntax.local_theory "quotient_definition"
    "definition for constants over the quotient type"
      OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))

end; (* structure *)