(* Title:  BaseDefinitions/celem-8.sml

   Author: Walther Neuper

   (c) due to copyright terms

Here is a minimum of code required for Know_Store.thy.

For main code see structure Thy_Write and structure Thy_Present.

The latter is legacy for HTML representation of theory data in Isac's Java front end.

*)

signature THEORY_DATA_STORE_WRITE =

sig

  type authors

  datatype thydata

    = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}

    | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rule_Def.rew_ord_}

    | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}

    | Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}

    | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}

  type theID

  val theID2str: string list -> string

  val the2str: thydata -> string

  val thes2str: thydata list -> string

  val theID2thyID: theID -> ThyC.id

  val part2guh: theID -> Check_Unique.id

  val thy2guh: theID -> Check_Unique.id

  val thypart2guh: theID -> Check_Unique.id

  val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.id

  val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.id

  val cal2guh: string * ThyC.id -> string -> Check_Unique.id

  val ord2guh: string * ThyC.id -> string -> Check_Unique.id

  val theID2guh: theID -> Check_Unique.id

  val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T

  val update_hthm: thydata -> Error_Pattern_Def.fill_in list -> thydata

(* ---- 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 Thy_Write(**): THEORY_DATA_STORE_WRITE(**) =

struct

(**)

(*the key into the hierarchy ob theory elements*)

type theID = string list;

val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)

fun theID2thyID theID =

  if length theID >= 3 then (last_elem o (drop_last_n 2)) theID

  else error ("theID2thyID called with " ^ theID2str theID);

type authors = string list;

(* datatype for collecting thydata for hierarchy *)

(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)

datatype thydata =

  Html of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, html: string}

| Hthm of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, fillpats: Error_Pattern_Def.fill_in list,

   thm: thm} (* here no sym_thm, thus no thmID required *)

| Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}

| Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}

| Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors,

    ord: (subst -> (term * term) -> bool)};

fun the2str (Html {guh, ...}) = guh

  | the2str (Hthm {guh, ...}) = guh

  | the2str (Hrls {guh, ...}) = guh

  | the2str (Hcal {guh, ...}) = guh

  | the2str (Hord {guh, ...}) = guh

fun thes2str thes = map the2str thes |> list2str;

(* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)

     (a): thehier does not contain sym_thmID theorems

     (b): lookup for sym_thmID directly from Isabelle using sym_thm

          (within math-engine NO lookup in thehier -- within java in *.xml only!)

TODO (c): export from thehier to xml

TODO (c1)   creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy

TODO (c2)   creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"

TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)

          stands for both, "thmID" and "sym_thmID" 

TODO (d1)   lookup from calctxt          

TODO (d1)   lookup from from rule set in MiniBrowser *)

type thehier = (thydata Store.node) list;

(* required to determine sequence of main nodes of thehier in Know_Store.thy *)

fun part2guh [str] = (case str of

	  "Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.id

      | "IsacScripts" => "thy_scri_" ^ str ^ "-part"

      | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"

      | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))

  | part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");

fun thy2guh [part, thyID] = (case part of

      "Isabelle" => "thy_isab_" ^ thyID

    | "IsacScripts" => "thy_scri_" ^ thyID

    | "IsacKnowledge" => "thy_isac_" ^ thyID

    | str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))

  | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");

fun thypart2guh ([part, thyID, thypart] : theID) = (case part of

      "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.id

    | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart

    | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart

    | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))

  | thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");

(* convert the data got via contextToThy to a globally unique handle.

   there is another way to get the guh: get out of the 'theID' in the hierarchy *)

fun thm2guh (isa, thyID) thmID = case isa of

    "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.id

  | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID

  | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID

  | _ => raise ERROR

    ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");

fun rls2guh (isa, thyID) rls' = case isa of

    "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.id

  | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'

  | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'

  | _ => raise ERROR

    ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");

fun cal2guh (isa, thyID) calID = case isa of

    "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.id

  | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID

  | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID

  | _ => raise ERROR

    ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");

fun ord2guh (isa, thyID) rew_ord' = case isa of

    "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Check_Unique.id

  | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'

  | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'

  | _ => raise ERROR

    ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");

(* TODO

fun theID2guh theID = case length theID of

    0 => error ("theID2guh: called with theID = " ^ strs2str' theID)

  | 1 => part2guh theID

  | 2 => thy2guh theID

  | 3 => thypart2guh theID

  | 4 => 

    let val [isa, thyID, typ, elemID] = theID

    in case typ of

        "Theorems" => thm2guh (isa, thyID) elemID

      | "Rulesets" => rls2guh (isa, thyID) elemID

      | "Calculations" => cal2guh (isa, thyID) elemID

      | "Orders" => ord2guh (isa, thyID) elemID

      | "Theorems" => thy2guh [isa, thyID]

      | str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)

    end

  | n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID);

*)

(* not only for thydata, but also for thy's etc *)

fun theID2guh [] = raise ERROR ("theID2guh: called with []")

  | theID2guh [str] = part2guh [str]

  | theID2guh [s1, s2] = thy2guh [s1, s2]

  | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]

  | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of

      "Theorems" => thm2guh (isa, thyID) elemID

    | "Rulesets" => rls2guh (isa, thyID) elemID

    | "Calculations" => cal2guh (isa, thyID) elemID

    | "Orders" => ord2guh (isa, thyID) elemID

    | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))

  | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);

(* not only for thydata, but also for thy's etc *)

fun theID2guh [] = raise ERROR ("theID2guh: called with []")

  | theID2guh [str] = part2guh [str]

  | theID2guh [s1, s2] = thy2guh [s1, s2]

  | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]

  | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of

      "Theorems" => thm2guh (isa, thyID) elemID

    | "Rulesets" => rls2guh (isa, thyID) elemID

    | "Calculations" => cal2guh (isa, thyID) elemID

    | "Orders" => ord2guh (isa, thyID) elemID

    | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))

  | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);

fun Html_default exist = (Html {guh = theID2guh exist, 

  coursedesign = ["isac team 2006"], mathauthors = [], html = ""})

fun fill_parents (_, [i]) thydata = Store.Node (i, [thydata], [])

  | fill_parents (exist, i :: is) thydata =

    Store.Node (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])

  | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"

fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]

  | add_thydata (exist, [i]) data (pys as (py as Store.Node (key, _, _)) :: pyss) = 

    if i = key

    then pys (* preserve existing thydata *) 

    else py :: add_thydata (exist, [i]) data pyss

  | add_thydata (exist, iss as (i :: is)) data ((py as Store.Node (key, d, pys)) :: pyss) = 

    if i = key

    then       

      if length pys = 0

      then Store.Node (key, d, [fill_parents (exist @ [i], is) data]) :: pyss

      else Store.Node (key, d, add_thydata (exist @ [i], is) data pys) :: pyss

    else py :: add_thydata (exist, iss) data pyss

  | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"

fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =

  Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,

    fillpats = fillpats', thm = thm}

  | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";

(**)end(**)