1 (* Title: "BridgeLibisabelle/thy-hierarchy.sml"
2 Author: Walther Neuper 0601
3 (c) due to copyright terms
5 Tools for Build_Thydata of theorems and rule-sets defined in Knowledge/ and ProgLang/
8 signature THEORY_HIERARCHY =
10 val collect_cals: string * ThyC.id -> (Thy_Write.theID * Thy_Write.thydata) list
11 val collect_isab: string -> string * thm -> Thy_Write.theID * Thy_Write.thydata
12 val collect_ords: 'a * ThyC.id -> (Thy_Write.theID * Thy_Write.thydata) list
13 val collect_part: string -> theory -> theory list -> (Thy_Write.theID * Thy_Write.thydata) list
14 val collect_rlss: string -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory list ->
15 (Thy_Write.theID * Thy_Write.thydata) list
16 val collect_thms: string -> theory -> (Thy_Write.theID * Thy_Write.thydata) list
18 val hierarchy_guh: 'a Store.T -> string
19 val insert_errpatIDs: 'a -> Thy_Write.theID -> Error_Pattern_Def.id list ->
20 Thy_Write.thydata * Thy_Write.theID
21 val update_hrls: Thy_Write.thydata -> Error_Pattern_Def.id list -> Thy_Write.thydata
23 val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Def.rule_set)) list ->
27 val get_fun_ids: theory -> (string * typ) list
32 structure Thy_Hierarchy(**): THEORY_HIERARCHY(**) =
35 open TermC (* allows contains_one_of to be infix *)
37 fun fun_id_of ({scr = prog, ...} : MethodC.T) =
39 Rule.Empty_Prog => NONE
42 Const ("HOL.eq", _) $ Free ("t", _) $ Free ("t", _) (*=@{thm refl}*) => NONE
43 | _ => SOME (Program.get_fun_id t))
44 | Rule.Rfuns _ => NONE
47 val mets = Store.get_all (KEStore_Elems.get_mets thy)
48 (* all mets of the respective theory PLUS of all ancestor theories*)
49 val fun_ids = mets |> map fun_id_of |> filter is_some |> map the
51 filter (fn (str, _) => ThyC.cut_id str = Context.theory_name thy) fun_ids
54 (* copy from mutabelle_extra.ML, fun thms_of *)
55 fun thms_of thy = (* das ist zu verbessern *)
57 val fun_ids = get_fun_ids thy
59 filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy
60 andalso not (thm contains_one_of fun_ids)
61 andalso not (ThmC.id_of_thm thm = "mono"))
62 (* created in Biegelinie by partial_function ^^^^^^*)
63 (map snd (Global_Theory.all_thms_of thy false))
66 (* wrap theory-data into the uniform type thydata *)
68 fun makeHthm (part : string, thyID : ThyC.id) (thm : thm) =
69 let val theID = [part, thyID, "Theorems"] @ [ThmC.id_of_thm thm] : Thy_Write.theID
70 in (theID, Thy_Write.Hthm {guh = Thy_Write.theID2guh theID, coursedesign = [],
71 mathauthors = ["isac-team"], fillpats = [], thm = thm})
73 fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, rls): ThyC.id * Rule_Set.T) =
74 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Thy_Write.theID
75 in (theID, Thy_Write.Hrls {guh = Thy_Write.theID2guh theID, coursedesign = [],
76 mathauthors = ["isac-team"], thy_rls = thy_rls})
78 fun makeHcal (part : string, thyID : ThyC.id) (calID, cal) =
79 let val theID = [part, thyID,"Operations"] @ [calID] : Thy_Write.theID
80 in (theID, Thy_Write.Hcal {guh = Thy_Write.theID2guh theID, coursedesign=[],
81 mathauthors = ["isac-team"], calc = cal})
83 fun makeHord (part : string, thyID : ThyC.id) (ordID, ord) =
84 let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : Thy_Write.theID
85 in (theID, Thy_Write.Hord {guh = Thy_Write.theID2guh theID, coursedesign=[],
86 mathauthors = ["isac-team"], ord = ord})
89 (* get all theorems from the list of rule-sets (defined in Knowledge) *)
90 fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
91 |> map (Thy_Present.thms_of_rls o #2 o #2)
93 |> map (ThmC.revert_sym_rule thy)
94 |> map (fn Rule.Thm (thmID, thm) => (thmID, thm))
95 |> distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2)
98 (* collect all thydata defined in in a theory *)
100 fun collect_thms part thy =
101 map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy))
102 fun collect_rlss part rlss thys = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
103 |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)
104 |> map (makeHrls part)
105 fun collect_cals (part, thy') =
106 let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)
107 in map (makeHcal (part, thy')) cals end;
108 fun collect_ords (part, thy') =
109 let val thy = ThyC.get_theory thy'
110 in [(*TODO.WN060120 rew_ord, Eval*)]:(Thy_Write.theID * Thy_Write.thydata) list end;
112 (* parts are: Isabelle | IsacKnowledge | IsacScripts, see Know_Store.thy *)
113 fun collect_part part parent thys =
114 (flat (map (collect_thms part) thys)) @
115 (collect_rlss part (KEStore_Elems.get_rlss parent) thys) @
116 [(*TODO: collect_cals, collect_ords*)]
118 (* collect theorems defined in Isabelle *)
119 fun collect_isab isa (thmDeriv, thm) =
121 [isa, ThyC.cut_id thmDeriv, "Theorems", ThmC.cut_id thmDeriv]
123 (theID: Thy_Write.theID, Thy_Write.Hthm {guh = Thy_Write.theID2guh theID,
124 mathauthors = ["Isabelle team, TU Munich"],
131 (** create an xml representation for thehier: hierarchy of entries + files per entry **)
133 (* create an xml-hierarchy where the filname is created from the guh;
134 ad DTD: a NODE contains an ID and zero or more NODEs*)
135 fun hierarchy_guh h =
139 fun node i p theID (Store.Node (id, _, ns)) =
141 val p' = Pos.lev_on p
142 val theID' = theID @ [id]
144 (indt i) ^ "<NODE>\n" ^
145 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
146 (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^
147 (indt (i+j)) ^ "<CONTENTREF> " ^ Thy_Write.theID2guh theID' ^ " </CONTENTREF>\n" ^
148 (nodes (i+j) (Pos.lev_dn p') theID' ns) ^
149 (indt i) ^ "</NODE>\n"
151 and nodes _ _ _ [] = ""
152 | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Pos.lev_on p) theID ns);
153 in nodes j [0] [] h end;
155 fun thy_hierarchy2file (path: Pbl_Met_Hierarchy.filepath) =
156 Pbl_Met_Hierarchy.str2file (path ^ "thy_hierarchy.xml")
158 " <ID> theory hierarchy </ID>\n" ^
160 " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
161 (hierarchy_guh (get_thes ())) ^
164 (* for dialog-authoring *)
165 fun update_hrls (Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
169 Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
170 => Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
171 calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
172 | Rule_Set.Sequence {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
173 => Rule_Set.Sequence {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
174 calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
175 | Rule_Set.Rrls {id, prepat, rew_ord, erls, calc, scr, ...}
176 => Rule_Set.Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
177 scr = scr, errpatts = errpatIDs}
180 Thy_Write.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
181 thy_rls = (thyID, rls')}
183 | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
185 fun insert_errpatIDs thy theID errpatIDs = (* TODO: redo like insert_fillpatts *)
187 val hrls = Thy_Read.from_store theID
188 val hrls' = update_hrls hrls errpatIDs
189 handle ERROR _ => raise ERROR ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
190 in (hrls', theID) end