(* 

   authors: Walther Neuper 2002, 2006

  (c) due to copyright terms

tools for rewriting, reverse rewriting, context to thy concerning rewriting

*)

signature THEORY_DATA_PRESENTATION =

sig

  eqtype filename

  val guh2filename : Check_Unique.id -> filename

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

end 

(**)

structure Thy_Present(**): THEORY_DATA_PRESENTATION(**) =

struct

(**)

type filename = string;

(* 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 _) = []

fun guh2filename guh = guh ^ ".xml";

(**)end(**)