22 type authors |
22 type authors |
23 type guh |
23 type guh |
24 |
24 |
25 type fillpat |
25 type fillpat |
26 datatype thydata |
26 datatype thydata |
27 = Hcal of {calc: Rule_Set.calc, coursedesign: authors, guh: guh, mathauthors: authors} |
27 = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: guh, mathauthors: authors} |
28 | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: Rule.subst -> term * term -> bool} |
28 | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: Rule.subst -> term * term -> bool} |
29 | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule_Set.T} |
29 | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule_Set.T} |
30 | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm} |
30 | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm} |
31 | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors} |
31 | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors} |
32 type theID |
32 type theID |
77 val isabthys: unit -> theory list |
77 val isabthys: unit -> theory list |
78 val thyID_of_derivation_name: string -> string |
78 val thyID_of_derivation_name: string -> string |
79 val partID': Rule.theory' -> string |
79 val partID': Rule.theory' -> string |
80 val thm2guh: string * Rule.thyID -> thmID -> guh |
80 val thm2guh: string * Rule.thyID -> thmID -> guh |
81 val thmID_of_derivation_name: string -> string |
81 val thmID_of_derivation_name: string -> string |
82 val rls2guh: string * Rule.thyID -> Rule_Set.rls' -> guh |
82 val rls2guh: string * Rule.thyID -> Rule_Set.identifier -> guh |
83 val theID2guh: theID -> guh |
83 val theID2guh: theID -> guh |
84 eqtype fillpatID |
84 eqtype fillpatID |
85 type pbt_ = string * (term * term) |
85 type pbt_ = string * (term * term) |
86 eqtype xml |
86 eqtype xml |
87 val cal2guh: string * Rule.thyID -> string -> guh |
87 val cal2guh: string * Rule.thyID -> string -> guh |
107 val e_pbt: pbt |
107 val e_pbt: pbt |
108 val e_met: met |
108 val e_met: met |
109 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
109 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
110 |
110 |
111 (*----- unused code, kept as hints to design ideas ---------------------------------------------*) |
111 (*----- unused code, kept as hints to design ideas ---------------------------------------------*) |
112 val overwritelthy: theory -> (Rule_Set.rls' * (string * Rule_Set.T)) list * (Rule_Set.rls' * Rule_Set.T) list -> |
112 val overwritelthy: theory -> (Rule_Set.identifier * (string * Rule_Set.T)) list * (Rule_Set.identifier * Rule_Set.T) list -> |
113 (Rule_Set.rls' * (string * Rule_Set.T)) list end |
113 (Rule_Set.identifier * (string * Rule_Set.T)) list end |
114 |
114 |
115 (**) |
115 (**) |
116 structure Celem(**): CALC_ELEMENT(**) = |
116 structure Celem(**): CALC_ELEMENT(**) = |
117 struct |
117 struct |
118 (**) |
118 (**) |
284 datatype thydata = |
284 datatype thydata = |
285 Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string} |
285 Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string} |
286 | Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: fillpat list, |
286 | Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: fillpat list, |
287 thm: thm} (* here no sym_thm, thus no thmID required *) |
287 thm: thm} (* here no sym_thm, thus no thmID required *) |
288 | Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (Rule.thyID * Rule_Set.T)} |
288 | Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (Rule.thyID * Rule_Set.T)} |
289 | Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule_Set.calc} |
289 | Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc} |
290 | Hord of {guh: guh, coursedesign: authors, mathauthors: authors, |
290 | Hord of {guh: guh, coursedesign: authors, mathauthors: authors, |
291 ord: (Rule.subst -> (term * term) -> bool)}; |
291 ord: (Rule.subst -> (term * term) -> bool)}; |
292 fun the2str (Html {guh, ...}) = guh |
292 fun the2str (Html {guh, ...}) = guh |
293 | the2str (Hthm {guh, ...}) = guh |
293 | the2str (Hthm {guh, ...}) = guh |
294 | the2str (Hrls {guh, ...}) = guh |
294 | the2str (Hrls {guh, ...}) = guh |
409 they do NOT handle overlays by re-using an identifier in different thys; |
409 they do NOT handle overlays by re-using an identifier in different thys; |
410 "thyID.rlsID" would be a good solution, if the "." would be possible |
410 "thyID.rlsID" would be a good solution, if the "." would be possible |
411 in scripts... |
411 in scripts... |
412 actually a hack to get alltogether run again with minimal effort *) |
412 actually a hack to get alltogether run again with minimal effort *) |
413 fun insthy thy' (rls', rls) = (rls', (thy', rls)); |
413 fun insthy thy' (rls', rls) = (rls', (thy', rls)); |
414 fun overwritelthy thy (al, bl: (Rule_Set.rls' * Rule_Set.T) list) = |
414 fun overwritelthy thy (al, bl: (Rule_Set.identifier * Rule_Set.T) list) = |
415 let val bl' = map (insthy ((get_thy o Rule.theory2theory') thy)) bl |
415 let val bl' = map (insthy ((get_thy o Rule.theory2theory') thy)) bl |
416 in overwritel (al, bl') end; |
416 in overwritel (al, bl') end; |
417 |
417 |
418 fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1; |
418 fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1; |
419 |
419 |
548 instead erls in "fun prep_met" *) |
548 instead erls in "fun prep_met" *) |
549 srls : Rule_Set.T, (* for evaluating list expressions in scr *) |
549 srls : Rule_Set.T, (* for evaluating list expressions in scr *) |
550 crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *) |
550 crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *) |
551 nrls : Rule_Set.T, (* canonical simplifier specific for this met *) |
551 nrls : Rule_Set.T, (* canonical simplifier specific for this met *) |
552 errpats : Rule.errpat list,(* error patterns expected in this method *) |
552 errpats : Rule.errpat list,(* error patterns expected in this method *) |
553 calc : Rule_Set.calc list, (* Theory_Data in fun prep_met *) |
553 calc : Rule_Def.calc list, (* Theory_Data in fun prep_met *) |
554 (*branch : TransitiveB set in append_problem at generation ob pblobj *) |
554 (*branch : TransitiveB set in append_problem at generation ob pblobj *) |
555 scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *) |
555 scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *) |
556 (*TODO: abstract to ?pre_model?...*) |
556 (*TODO: abstract to ?pre_model?...*) |
557 prls : Rule_Set.T, (* for evaluating predicates in modelpattern *) |
557 prls : Rule_Set.T, (* for evaluating predicates in modelpattern *) |
558 ppc : pat list, (* items in given, find, relate; |
558 ppc : pat list, (* items in given, find, relate; |
561 copy-named items are 'generating' if they are NOT "*'''" ?WN120516?? |
561 copy-named items are 'generating' if they are NOT "*'''" ?WN120516?? |
562 see ME/calchead.sml 'fun is_copy_named'. *) |
562 see ME/calchead.sml 'fun is_copy_named'. *) |
563 pre : term list (* preconditions in where *) |
563 pre : term list (* preconditions in where *) |
564 }; |
564 }; |
565 val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'", |
565 val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'", |
566 erls = Rule_Set.e_rls, srls = Rule_Set.e_rls, prls = Rule_Set.e_rls, calc = [], crls = Rule_Set.e_rls, |
566 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty, |
567 errpats = [], nrls = Rule_Set.e_rls, ppc = [], pre = [], scr = Rule.EmptyScr}; |
567 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.EmptyScr}; |
568 val e_Mets = Ptyp ("e_metID", [e_met],[]); |
568 val e_Mets = Ptyp ("e_metID", [e_met],[]); |
569 |
569 |
570 type mets = (met ptyp) list; |
570 type mets = (met ptyp) list; |
571 fun coll_metguhs mets = |
571 fun coll_metguhs mets = |
572 let |
572 let |