(* Title:  BaseDefinitions/celem-0.sml

    Author: Walther Neuper

    (c) due to copyright terms

           *)

 signature CALCELEMENT_0 =

 (*/------- to Celem0 -------\*)

 (*\------- to Celem0 -------/*)

 sig

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (*NONE*)

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   (*NONE*)

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 end

 (**)

 structure Celem0(**): CALCELEMENT_0(**) =

 struct

 (**)

 (*

 val get_cas: theory -> Celem.cas_elem list

   val add_cas: Celem.cas_elem list -> theory -> theory

   val get_ptyps: theory -> Celem.ptyps

   val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory

   val get_mets: theory -> Celem.mets

   val add_mets: (Celem.met * Celem.metID) list -> theory -> theory

   val get_thes: theory -> (Celem.thydata Celem.ptyp) list

   val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)

   val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 

     type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;

     val merge = merge Celem.cas_eq;

   fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)

     type T = Celem.ptyps;

     val empty = [Celem.e_Ptyp];

     val merge = Celem.merge_ptyps;

                 (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();

                   rev pblID |> Celem.insrt pblID pbt);

     type T = Celem.mets;

     val empty = [Celem.e_Mets];

     val merge = Celem.merge_ptyps;

                 (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();

                   Celem.insrt metID met metID);

     type T = (Celem.thydata Celem.ptyp) list;

     val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)

     fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata

           val hthm = Celem.get_py (Data.get thy) theID theID

           val hthm' = Celem.update_hthm hthm fillpats

         in Celem.update_ptyps theID theID hthm' end

   [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",

   (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",

   (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",

 fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =

   (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";

   | count_kestore_ptyps ((Celem.Ptyp (_, _, ps)) :: ps') =

 fun check_kestore_ptyp' strfun (Celem.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^

       (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;

 val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;

 fun ptyp_ord ((Celem.Ptyp (s1, _, _)), (Celem.Ptyp (s2, _, _))) = string_ord (s1, s2);

 fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);

   | sort_kestore_ptyp' ordfun ((Celem.Ptyp (key, pbts, ps)) :: ps') =

      ((Celem.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))

 fun metguh2str ({guh,...} : Celem.met) = guh : string;

 fun check_kestore_met (mp: Celem.met Celem.ptyp) =

 fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);

 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes

     |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))

 *)

 (*/------- to Celem0 -------\*)

 (*\------- to Celem0 -------/*)

 (**)end(**)