(* title: "/thy-hierarchy.sml"

     export theory-data "thehier" to xml

   author: Walther Neuper 0601

   (c) isac-team

*)

signature THEORY_HIERARCHY =

sig

  val collect_cals: string * ThyC.id -> (Celem.theID * Celem.thydata) list

  val collect_isab: string -> string * thm -> Celem.theID * Celem.thydata

  val collect_ords: 'a * ThyC.id -> (Celem.theID * Celem.thydata) list

  val collect_part: string -> theory -> theory list -> (Celem.theID * Celem.thydata) list

  val collect_rlss: string -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory list ->

    (Celem.theID * Celem.thydata) list

  val collect_thms: string -> theory -> (Celem.theID * Celem.thydata) list

  val hierarchy_guh: 'a Celem1.ptyp list -> string

  val insert_errpatIDs: 'a -> Celem.theID -> Error_Fill_Def.errpatID list ->

    Celem.thydata * Celem.theID

  val makeHcal: string * ThyC.id -> string * Rule_Def.calc -> Celem.theID * Celem.thydata

  val makeHord: string * ThyC.id -> string * ((term * term) list -> term * term -> bool) ->

    Celem.theID * Celem.thydata

  val makeHrls: string -> Rule_Set.id * (ThyC.id * Rule_Def.rule_set) ->

    Celem.theID * Celem.thydata

  val makeHthm: string * ThyC.id -> thm -> Celem.theID * Celem.thydata

  val make_cal: theory -> Rule_Def.calc -> Celem.authors -> Celem.thydata * Celem.theID

  val make_isa: theory -> ThyC.id * ThyC.id -> Celem.authors ->

    Celem.thydata * Celem.theID

  val make_ord: theory -> ((term * term) list -> term * term -> bool) -> Celem.authors ->

    Celem.thydata * Celem.theID

  val make_rls: theory -> Rule_Def.rule_set -> Celem.authors -> Celem.thydata * Celem.theID

  val make_thm: theory -> string -> string * thm -> Celem.authors -> Celem.thydata * Celem.theID

  val make_thy: theory -> Celem.authors -> Celem.thydata * Celem.theID

  val show_thes: unit -> unit

  val thes2file: Celem.filepath -> unit

  val thms_of: theory -> thm list

  val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Def.rule_set)) list ->

    (string * thm) list

  val thy_hierarchy2file: Celem.filepath -> unit

  val thydata2file: Celem.filepath -> Pos.pos -> Celem.theID -> Celem.thydata -> unit

  val thydata2xml: Celem.theID * Celem.thydata -> Celem.xml

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

  (*NONE*)

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

  val thenode: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos ->

    string list -> 'a -> 'b) -> 'a Celem1.ptyp -> unit

  val thenodes: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos ->

    string list -> 'a -> 'b) -> 'a Celem1.ptyp list -> unit

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

end

(**)

structure Thy_Hierarchy(**): THEORY_HIERARCHY(**) =

struct

(**)

open TermC (* allows contains_one_of to be infix *)

(* copy from mutabelle_extra.ML, fun thms_of *)

fun thms_of thy = (* das ist zu verbessern *)

  let

    val fun_ids = Specify.get_fun_ids thy

  in

    filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy

        andalso not (thm contains_one_of fun_ids)

        andalso not (ThmC.id_of_thm thm = "mono"))

        (* created in Biegelinie by partial_function ^^^^^^*)

      (map snd (Global_Theory.all_thms_of thy false))

  end

(* wrap theory-data into the uniform type thydata *)

fun makeHthm (part : string, thyID : ThyC.id) (thm : thm) =

    let val theID = [part, thyID, "Theorems"] @ [ThmC.id_of_thm thm] : Celem.theID

    in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [], 

		     mathauthors = ["isac-team"], fillpats = [], thm = thm})

    end;

fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, rls): ThyC.id * Rule_Set.T) =

    let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID

    in (theID, Celem.Hrls {guh = Celem.theID2guh theID, coursedesign = [], 

		     mathauthors = ["isac-team"], thy_rls = thy_rls})

    end;

fun makeHcal (part : string, thyID : ThyC.id) (calID, cal) =

    let val theID = [part, thyID,"Operations"] @ [calID] : Celem.theID

    in (theID, Celem.Hcal {guh = Celem.theID2guh theID, coursedesign=[], 

		     mathauthors = ["isac-team"], calc = cal})

    end;

fun makeHord (part : string, thyID : ThyC.id) (ordID, ord) =

    let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : Celem.theID

    in (theID, Celem.Hord  {guh = Celem.theID2guh theID, coursedesign=[], 

		      mathauthors = ["isac-team"], ord = ord})

    end;

(* get all theorems from the list of rule-sets (defined in Knowledge) *)

fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)

  |> map (Rtools.thms_of_rls o #2 o #2)

  |> flat

  |> map (ThmC.revert_sym_rule thy)

  |> map (fn Rule.Thm (thmID, thm) => (thmID, thm))

  |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2) 

  : ThmC.T list                              

(* collect all thydata defined in in a theory *)

fun collect_thms part thy =

  map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy))

fun collect_rlss part rlss thys = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)

  |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)

  |> map (makeHrls part)

fun collect_cals (part, thy') =

  let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)

  in map (makeHcal (part, thy')) cals end;

fun collect_ords (part, thy') =

    let val thy = ThyC.get_theory thy'

    in [(*TODO.WN060120 rew_ord, Eval*)]:(Celem.theID * Celem.thydata) list end;

(* parts are: Isabelle | IsacKnowledge | IsacScripts, see Know_Store.thy *)

fun collect_part part parent thys =

  (flat (map (collect_thms part) thys)) @

  (collect_rlss part (KEStore_Elems.get_rlss parent) thys) @ 

  [(*TODO: collect_cals, collect_ords*)]

(* collect theorems defined in Isabelle *)

fun collect_isab isa (thmDeriv, thm) =

  let val theID =

    [isa, ThyC.cut_id thmDeriv, "Theorems", ThmC.cut_id thmDeriv]

  in 

    (theID: Celem.theID, Celem.Hthm {guh = Celem.theID2guh theID, 

      mathauthors = ["Isabelle team, TU Munich"],

      coursedesign = [],

      fillpats = [],

      thm = thm}) 

  end

fun show_thes () = (writeln o Specify.format_pblIDl o (Specify.scan [])) (get_thes ());

(** create an xml representation for thehier: hierarchy of entries + files per entry **)

(* create an xml-hierarchy where the filname is created from the guh; 

  ad DTD: a NODE contains an ID and zero or more NODEs*)

fun hierarchy_guh h =

  let

    val i = indentation

    val j = indentation

    fun node i p theID (Celem1.Ptyp (id, _, ns)) = 

        let

          val p' = Pos.lev_on p

          val theID' = theID @ [id]

        in

        (indt i) ^ "<NODE>\n" ^ 

        (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ 

        (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^ 

        (indt (i+j)) ^ "<CONTENTREF> " ^ Celem.theID2guh theID' ^ " </CONTENTREF>\n" ^

        (nodes (i+j) (Pos.lev_dn p') theID' ns) ^ 

        (indt i) ^ "</NODE>\n"

        end

    and nodes _ _ _ [] = ""

      | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Pos.lev_on p) theID ns);

  in nodes j [0] [] h end;

fun thy_hierarchy2file (path: Celem.filepath) = 

  str2file (path ^ "thy_hierarchy.xml") 

    ("<NODE>\n" ^

    "  <ID> theory hierarchy </ID>\n" ^

    "  <NO> 1 </NO>\n" ^

    "  <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^

    (hierarchy_guh (get_thes ())) ^

    "</NODE>");

(* create the xml-files for the thydata in the hierarchy *)

val i = indentation;

(* analoguous to 'fun met2xml' *)

fun thydata2xml (theID: Celem.theID, Celem.Html {guh, coursedesign, mathauthors, html}) =

      "<HTMLDATA>\n" ^

      indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^

      id2xml i theID ^

      indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^

      authors2xml i "MATHAUTHORS" mathauthors ^

      authors2xml i "COURSEDESIGNS" coursedesign ^

      "</HTMLDATA>\n" : Celem.xml

  | thydata2xml (theID, Celem.Hthm {guh, coursedesign, mathauthors, fillpats(*TODO?*), thm}) =

      "<THEOREMDATA>\n" ^

      indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^

      id2xml i theID ^

      thm''2xml i thm ^

      indt i ^ "<PROOF>\n" ^

      extref2xml (i+i) "Proof of the theorem" (* TODO "Unsorted"vvv: distinguish Isabelle | Isac *)

	      ("http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^

	        nth 2 theID ^ ".html") ^

	    indt i ^  "</PROOF>\n" ^

	    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^

	    authors2xml i "MATHAUTHORS" mathauthors ^

	    authors2xml i "COURSEDESIGNS" coursedesign ^

	    "</THEOREMDATA>\n"

  | thydata2xml (theID, Celem.Hrls {guh, coursedesign, mathauthors, thy_rls}) =

      "<RULESETDATA>\n" ^

      indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^

      id2xml i theID ^

      rls2xml i thy_rls ^

      indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^

      authors2xml i "MATHAUTHORS" mathauthors ^

    authors2xml i "COURSEDESIGNS" coursedesign ^

      "</RULESETDATA>\n"

  | thydata2xml (theID, Celem.Hcal {guh, coursedesign, mathauthors, calc}) =

      "<RULESETDATA>\n" ^

      indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^

      id2xml i theID ^

      calc2xml i (Celem.theID2thyID theID, calc) ^

      indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^

      authors2xml i "MATHAUTHORS" mathauthors ^

      authors2xml i "COURSEDESIGNS" coursedesign ^

      "</RULESETDATA>\n"

  | thydata2xml (theID, _) =

      error ("thydata2xml: not implemented for "^ strs2str' theID);

(* analoguous to 'fun met2file' *)

fun thydata2file (path : Celem.filepath) (pos : Pos.pos) (theID : Celem.theID) thydata =

  (writeln ("### thes2file: id = " ^ strs2str theID);

    str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata)));

(* analoguous to 'fun node' *)

fun thenode (pa : Celem.filepath) ids po wfn (Celem1.Ptyp (id, [n], ns)) = 

    let val po' = Pos.lev_on po

    in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Pos.lev_dn po') wfn ns end

and thenodes _ _ _ _ [] = ()

  | thenodes pa ids po wfn (n::ns) =

      (thenode pa ids po wfn n; thenodes pa ids (Pos.lev_on po) wfn ns);

(* analoguous to 'fun mets2file' *)

fun thes2file (p : Celem.filepath) = thenodes p [] [0] thydata2file (get_thes ());

(***.store a single theory element in the hierarchy.***)

(*.for mathauthors only, other html is added to xml exported from here.*)

fun make_isa thy (part, thypart) (mathauthors : Celem.authors) =

  let 

    val theID = [part, Context.theory_name thy, thypart]

    val guh = case theID of

        [part] => Celem.part2guh theID

      | [part, thyID, thypart] => Celem.thypart2guh theID

    val theID = Rtools.guh2theID guh

    val the = Celem.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}

  in (the, theID) end

fun make_thy thy (mathauthors : Celem.authors) =

  let 

    val guh = Celem.thy2guh ["IsacKnowledge", Context.theory_name thy]

    val theID = Rtools.guh2theID guh

    val the = Celem.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}

  in (the, theID) end

fun make_thm thy part (thmID : ThmC.id, thm) (mathauthors : Celem.authors) =

  let

    val guh = Celem.thm2guh (part, Context.theory_name thy) thmID

    val theID = Rtools.guh2theID guh

    val the = Celem.Hthm {guh = guh, coursedesign = [(*inserted in xml after export*)], 

			mathauthors = mathauthors, fillpats = [], thm = thm}

  in (the, theID) end

fun make_rls thy rls (mathauthors : Celem.authors) =

  let 

    val guh = Celem.rls2guh ("IsacKnowledge", Context.theory_name thy) ((#id o Rule_Set.rep) rls)

    val theID = Rtools.guh2theID guh

    val the = Celem.Hrls {guh = guh, coursedesign = [], mathauthors = mathauthors,

			thy_rls = (Context.theory_name thy, rls)}

	  (*needs no (!check_guhs_unique) because guh is generated automatically*)

  in (the, theID) end

fun make_cal thy cal (mathauthors : Celem.authors) =

  let

    val guh = Celem.cal2guh ("IsacKnowledge", Context.theory_name thy) ("TODO store_cal")

    val theID = Rtools.guh2theID guh

    val the = Celem.Hcal {guh = guh, coursedesign = [], mathauthors = mathauthors, calc = cal}

  in (the, theID) end

fun make_ord thy ord (mathauthors : Celem.authors) =

  let 

    val guh = Celem.ord2guh ("IsacKnowledge", Context.theory_name thy) ("TODO store_ord")

    val theID = Rtools.guh2theID guh

    val the = Celem.Hord {guh = guh, coursedesign = [], mathauthors = mathauthors, ord = ord}

  in (the, theID) end

fun insert_errpatIDs thy theID errpatIDs = (* TODO: redo like insert_fillpatts *)

  let

    val hrls = Specify.get_the theID

    val hrls' = Celem.update_hrls hrls errpatIDs

      handle ERROR _ => error ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")

  in (hrls', theID) end

(**)end(**)

open Thy_Hierarchy