(* Title: "BridgeLibisabelle/thy-hierarchy.sml"

   Author: Walther Neuper 0601

   (c) due to copyright terms

Tools to Build_Thydata of theorems and rule-sets defined in Knowledge/ and ProgLang/

*)

signature THEORY_HIERARCHY =

sig

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

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

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

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

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

    (Thy_Write.theID * Thy_Write.thydata) list

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

  val insert_errpatIDs: 'a -> Thy_Write.theID -> Error_Pattern_Def.id list ->

    Thy_Write.thydata * Thy_Write.theID

  val thms_of_rls : Rule_Set.T -> Rule.rule list

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

    (string * thm) list

\<^isac_test>\<open>

  val hierarchy_guh: 'a Store.T -> string

  val get_fun_ids: theory -> (string * typ) list

\<close>

end

(**)

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

struct

(**)

open TermC (* allows contains_one_of to be infix *)

fun fun_id_of ({scr = prog, ...} : MethodC.T) = 

  case prog of

    Rule.Empty_Prog => NONE

  | Rule.Prog t => 

    (case t of

      Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("t", _) $ Free ("t", _) (*=@{thm refl}*) => NONE

    | _ => SOME (Program.get_fun_id t))

  | Rule.Rfuns _ => NONE

fun get_fun_ids thy =

  let 

    val mets = Store.get_all (KEStore_Elems.get_mets thy)

    (* all mets of the respective theory PLUS of all ancestor theories*)

    val fun_ids = mets |> map fun_id_of |> filter is_some |> map the

  in 

    filter (fn (str, _) => ThyC.cut_id str = Context.theory_name thy) fun_ids 

  end

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

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

  let

    val fun_ids = 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] : Thy_Write.theID

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

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

    end;

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

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

    in (theID, Thy_Write.Hrls {guh = Thy_Write.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] : Thy_Write.theID

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

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

    end;

(* get all theorems in a rule set (recursivley containing rule sets) *)

fun thm_of_rule Rule.Erule = []

  | thm_of_rule (thm as Rule.Thm _) = [thm]

  | thm_of_rule (Rule.Eval _) = []

  | thm_of_rule (Rule.Cal1 _) = []

  | thm_of_rule (Rule.Rls_ rls) = thms_of_rls rls

and thms_of_rls Rule_Set.Empty = []

  | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map  thm_of_rule)) rules

  | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map  thm_of_rule)) rules

  | thms_of_rls (Rule_Set.Rrls _) = []

(* 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 (thms_of_rls o #2 o #2)

  |> flat

  |> map (ThmC.revert_sym_rule thy)

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

           | _ => raise ERROR "thms_of_rlss: uncovered case")

  |> 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 (_, _) =

    [(*TODO.WN060120 rew_ord, Eval*)]:(Thy_Write.theID * Thy_Write.thydata) list

(* 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: Thy_Write.theID, Thy_Write.Hthm {guh = Thy_Write.theID2guh theID, 

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

      coursedesign = [],

      fillpats = [],

      thm = thm}) 

  end

(* for dialog-authoring *)

fun update_hrls (Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =

    let

      val rls' = 

        case rls of

          Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}

          => Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

               calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}

        | Rule_Set.Sequence {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}

          => Rule_Set.Sequence {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

               calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}

        | Rule_Set.Rrls {id, prepat, rew_ord, erls, calc, scr, ...}

          => Rule_Set.Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,

               scr = scr, errpatts = errpatIDs}

        | Erls => Erls

    in

      Thy_Write.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,

        thy_rls = (thyID, rls')}

    end

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

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

  let

    val hrls = Thy_Read.for_thy_hierarchy theID

    val hrls' = update_hrls hrls errpatIDs

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

  in (hrls', theID) end

(*keep tests of interaction Java-frontend <-> Kernel running*)

\<^isac_test>\<open>

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

val indentation = 2;

fun hierarchy_guh h =

  let

    val j = indentation

    fun node i p theID (Store.Node (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> " ^ Thy_Write.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;

\<close>

(**)end(**)