(*  Title:      HOL/Tools/ctr_sugar_code.ML

     Author:     Jasmin Blanchette, TU Muenchen

     Author:     Dmitriy Traytel, TU Muenchen

     Author:     Stefan Berghofer, TU Muenchen

     Author:     Florian Haftmann, TU Muenchen

     Copyright   2001-2013

 Code generation for freely generated types.

 *)

 signature CTR_SUGAR_CODE =

 sig

   val add_ctr_code: string -> typ list -> (string * typ) list -> thm list -> thm list -> thm list ->

     theory -> theory

 end;

 structure Ctr_Sugar_Code : CTR_SUGAR_CODE =

 struct

 open Ctr_Sugar_Util

 val eqN = "eq"

 val reflN = "refl"

 val simpsN = "simps"

 fun mk_case_certificate thy raw_thms =

   let

     val thms as thm1 :: _ = raw_thms

       |> Conjunction.intr_balanced

       |> Thm.unvarify_global

       |> Conjunction.elim_balanced (length raw_thms)

       |> map Simpdata.mk_meta_eq

       |> map Drule.zero_var_indexes;

     val params = Term.add_free_names (Thm.prop_of thm1) [];

     val rhs = thm1

       |> Thm.prop_of |> Logic.dest_equals |> fst |> Term.strip_comb

       ||> fst o split_last |> list_comb;

     val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);

     val assum = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs));

   in

     thms

     |> Conjunction.intr_balanced

     |> rewrite_rule [Thm.symmetric (Thm.assume assum)]

     |> Thm.implies_intr assum

     |> Thm.generalize ([], params) 0

     |> Axclass.unoverload thy

     |> Thm.varifyT_global

   end;

 fun mk_free_ctr_equations fcT ctrs inject_thms distinct_thms thy =

   let

     fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u;

     fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});

     fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});

     val monomorphic_prop_of = prop_of o Thm.unvarify_global o Drule.zero_var_indexes;

     fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);

     fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];

     val triv_inject_goals =

       map_filter (fn c as (_, T) =>

           if T = fcT then SOME (HOLogic.mk_Trueprop (true_eq (Const c, Const c))) else NONE)

         ctrs;

     val inject_goals = map (massage_inject o monomorphic_prop_of) inject_thms;

     val distinct_goals = maps (massage_distinct o monomorphic_prop_of) distinct_thms;

     val refl_goal = HOLogic.mk_Trueprop (true_eq (Free ("x", fcT), Free ("x", fcT)));

     val simp_ctxt =

       Simplifier.global_context thy HOL_basic_ss

         addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms));

     fun prove goal =

       Goal.prove_sorry_global thy [] [] goal (K (ALLGOALS (simp_tac simp_ctxt)))

       |> Simpdata.mk_eq;

   in

     (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)

   end;

 fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =

   let

     fun add_def lthy =

       let

         fun mk_side const_name =

           Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT);

         val spec =

           mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})

           |> Syntax.check_term lthy;

         val ((_, (_, raw_def)), lthy') =

           Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;

         val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)

         val def = singleton (Proof_Context.export lthy' ctxt_thy) raw_def;

       in

         (def, lthy')

       end;

     fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);

     val qualify =

       Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;

   in

     Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])

     #> add_def

     #-> Class.prove_instantiation_exit_result (map o Morphism.thm) (K tac) o single

     #-> fold Code.del_eqn

     #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)

     #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK

       [((qualify reflN, [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),

         ((qualify simpsN, [Code.add_default_eqn_attribute]), [(rev thms, [])])])

     #> snd

   end;

 fun add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy =

   let

     val fcT = Type (fcT_name, As);

     val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs;

   in

     if can (Code.constrset_of_consts thy) unover_ctrs then

       thy

       |> Code.add_datatype ctrs

       |> fold_rev Code.add_default_eqn case_thms

       |> Code.add_case (mk_case_certificate thy case_thms)

       |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])

         ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms

     else

       thy

   end;

 end;