wneuper/isa: comparison src/Tools/isac/CalcElements/calcelems.sml

equal deleted inserted replaced

-:f3cac3053e7b
+:4dd533681fef
 type fillpat
 datatype thydata
 = Hcal of {calc: Rule_Set.calc, coursedesign: authors, guh: guh, mathauthors: authors}
 | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: Rule.subst -> term * term -> bool}
-| Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule_Set.rls}
+| Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule_Set.T}
 | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm}
 | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}
 type theID
 type spec
 val cas_eq: cas_elem * cas_elem -> bool
 val e_pbt: pbt
 val e_met: met
 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
-val overwritelthy: theory -> (Rule_Set.rls' * (string * Rule_Set.rls)) list * (Rule_Set.rls' * Rule_Set.rls) list ->
+val overwritelthy: theory -> (Rule_Set.rls' * (string * Rule_Set.T)) list * (Rule_Set.rls' * Rule_Set.T) list ->
-(Rule_Set.rls' * (string * Rule_Set.rls)) list  end
+(Rule_Set.rls' * (string * Rule_Set.T)) list  end
 (**)
 structure Celem(**): CALC_ELEMENT(**) =
 struct
 (**)
 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
 datatype thydata =
 Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string}
 | Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: fillpat list,
 thm: thm} (* here no sym_thm, thus no thmID required *)
-| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (Rule.thyID * Rule_Set.rls)}
+| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (Rule.thyID * Rule_Set.T)}
 | Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule_Set.calc}
 | Hord of {guh: guh, coursedesign: authors, mathauthors: authors,
 ord: (Rule.subst -> (term * term) -> bool)};
 fun the2str (Html {guh, ...}) = guh
 | the2str (Hthm {guh, ...}) = guh
 they do NOT handle overlays by re-using an identifier in different thys;
 "thyID.rlsID" would be a good solution, if the "." would be possible
 in scripts...
 actually a hack to get alltogether run again with minimal effort *)
 fun insthy thy' (rls', rls) = (rls', (thy', rls));
-fun overwritelthy thy (al, bl: (Rule_Set.rls' * Rule_Set.rls) list) =
+fun overwritelthy thy (al, bl: (Rule_Set.rls' * Rule_Set.T) list) =
 let val bl' = map (insthy ((get_thy o Rule.theory2theory') thy)) bl
 in overwritel (al, bl') end;
 fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
 because applied terms may be from 'subthy' as well as from super;
 thus we take 'maxthy'; see match_ags !                           *)
 cas : term option,  (* 'CAS-command'                                                   *)
 met : metID list,   (* methods solving the pbt                                         *)
 (*TODO: abstract to ?pre_model?...*)
-prls : Rule_Set.rls,    (* for preds in where_                                             *)
+prls : Rule_Set.T,    (* for preds in where_                                             *)
 where_ : term list, (* where - predicates                                              *)
 ppc : pat list      (* this is the model-pattern;
 it contains "#Given","#Where","#Find","#Relate"-patterns
 for constraints on identifiers see "fun cpy_nam"                *)
 }
 val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure",
-cas = NONE, prls = Rule_Set.Erls, where_ = [], ppc = [], met = []} : pbt
+cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : pbt
 fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
 prls = prls', thy = thy', where_ = w'} : pbt)
 = "{cas = " ^ (Rule.termopt2str cas') ^  ", guh = \"" ^ guh'  ^ "\", init = "
 ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
 ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = "
 {guh        : guh,             (* unique within this isac-knowledge             *)
 mathauthors: string list,     (* copyright                                     *)
 init       : pblID,           (* WN060721 introduced mistakenly--TODO.REMOVE!  *)
 rew_ord'   : Rule_Def.rew_ord',  (* for rules in Detail
 			                                 TODO.WN0509 store fun itself, see 'type pbt'  *)
-erls       : Rule_Set.rls,        (* the eval_rls for cond. in rules FIXME "rls'
+erls       : Rule_Set.T,        (* the eval_rls for cond. in rules FIXME "rls'
 				                               instead erls in "fun prep_met"                *)
-srls       : Rule_Set.rls,        (* for evaluating list expressions in scr        *)
+srls       : Rule_Set.T,        (* for evaluating list expressions in scr        *)
-crls       : Rule_Set.rls,        (* for check_elementwise, ie. formulae in calc.  *)
+crls       : Rule_Set.T,        (* for check_elementwise, ie. formulae in calc.  *)
-nrls       : Rule_Set.rls,        (* canonical simplifier specific for this met    *)
+nrls       : Rule_Set.T,        (* canonical simplifier specific for this met    *)
 errpats    : Rule.errpat list,(* error patterns expected in this method        *)
 calc       : Rule_Set.calc list, (* Theory_Data in fun prep_met                   *)
 (*branch   : TransitiveB set in append_problem at generation ob pblobj         *)
 scr        : Rule.program,    (* progam, empty as @{thm refl} or Rfuns         *)
 (*TODO: abstract to ?pre_model?...*)
-prls       : Rule_Set.rls,        (* for evaluating predicates in modelpattern     *)
+prls       : Rule_Set.T,        (* for evaluating predicates in modelpattern     *)
 ppc        : pat list,        (* items in given, find, relate;
 	      items (in "#Find") which need not occur in the arg-list of a SubProblem
 are 'copy-named' with an identifier "*'.'".
 copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
 see ME/calchead.sml 'fun is_copy_named'.                                     *)
 (* for dialog-authoring *)
 fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
 let
 val rls' =
 case rls of
-Rule_Set.Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
+Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
-=> Rule_Set.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
+=> 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.Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
+| Rule_Set.Seqence {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
-=> Rule_Set.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
+=> Rule_Set.Seqence {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

changeset 59851	4dd533681fef
parent 59850	f3cac3053e7b
child 59852	ea7e6679080e