1.1 --- a/src/Tools/isac/BaseDefinitions/KEStore.thy Fri Apr 10 15:02:50 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/KEStore.thy Fri Apr 10 16:16:09 2020 +0200
1.3 @@ -6,14 +6,14 @@
1.4
1.5 begin
1.6 ML_file libraryC.sml
1.7 -ML_file theoryC.sml
1.8 -ML_file unparseC.sml
1.9 -ML_file "rule-def.sml"
1.10 -ML_file "thmC-def.sml"
1.11 -ML_file "exec-def.sml"
1.12 -ML_file "rewrite-order.sml"
1.13 +ML_file theoryC.sml (*rename identifiers by use of struct.id*)
1.14 +ML_file unparseC.sml (*rename identifiers by use of struct.id*)
1.15 +ML_file "rule-def.sml" (*rename identifiers by use of struct.id*)
1.16 +ML_file "thmC-def.sml" (*rename identifiers by use of struct.id*)
1.17 +ML_file "exec-def.sml" (*rename identifiers by use of struct.id*)
1.18 +ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*)
1.19 ML_file rule.sml
1.20 -ML_file "error-fill-def.sml"
1.21 +ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
1.22 ML_file "rule-set.sml"
1.23 ML_file calcelems.sml
1.24 ML \<open>
1.25 @@ -37,8 +37,8 @@
1.26 *)
1.27 signature KESTORE_ELEMS =
1.28 sig
1.29 - val get_rlss: theory -> (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list
1.30 - val add_rlss: (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list -> theory -> theory
1.31 + val get_rlss: theory -> (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list
1.32 + val add_rlss: (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list -> theory -> theory
1.33 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
1.34 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
1.35 val get_cas: theory -> Celem.cas_elem list
1.36 @@ -59,7 +59,7 @@
1.37 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
1.38
1.39 structure Data = Theory_Data (
1.40 - type T = (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list;
1.41 + type T = (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list;
1.42 val empty = [];
1.43 val extend = I;
1.44 val merge = Rule_Set.to_kestore;
1.45 @@ -147,13 +147,13 @@
1.46 ML \<open>
1.47 val get_ref_thy = KEStore_Elems.get_ref_thy;
1.48
1.49 -fun assoc_rls (rls' : Rule_Set.identifier) =
1.50 +fun assoc_rls (rls' : Rule_Set.id) =
1.51 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.Thy_Info_get_theory "Isac_Knowledge")) rls' of
1.52 SOME (_, rls) => rls
1.53 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
1.54 "TODO exception hierarchy needs to be established.")
1.55
1.56 -fun assoc_rls' thy (rls' : Rule_Set.identifier) =
1.57 +fun assoc_rls' thy (rls' : Rule_Set.id) =
1.58 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
1.59 SOME (_, rls) => rls
1.60 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Fri Apr 10 15:02:50 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Fri Apr 10 16:16:09 2020 +0200
2.3 @@ -72,7 +72,7 @@
2.4 val isabthys: unit -> theory list
2.5 val partID': ThyC.theory' -> string
2.6 val thm2guh: string * ThyC.thyID -> ThmC_Def.thmID -> guh
2.7 - val rls2guh: string * ThyC.thyID -> Rule_Set.identifier -> guh
2.8 + val rls2guh: string * ThyC.thyID -> Rule_Set.id -> guh
2.9 val theID2guh: theID -> guh
2.10 type pbt_ = string * (term * term)
2.11 eqtype xml
2.12 @@ -99,8 +99,8 @@
2.13 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.14
2.15 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
2.16 -val overwritelthy: theory -> (Rule_Set.identifier * (string * Rule_Set.T)) list * (Rule_Set.identifier * Rule_Set.T) list ->
2.17 - (Rule_Set.identifier * (string * Rule_Set.T)) list end
2.18 +val overwritelthy: theory -> (Rule_Set.id * (string * Rule_Set.T)) list * (Rule_Set.id * Rule_Set.T) list ->
2.19 + (Rule_Set.id * (string * Rule_Set.T)) list end
2.20
2.21 (**)
2.22 structure Celem(**): CALC_ELEMENT(**) =
2.23 @@ -339,7 +339,7 @@
2.24 in scripts...
2.25 actually a hack to get alltogether run again with minimal effort *)
2.26 fun insthy thy' (rls', rls) = (rls', (thy', rls));
2.27 -fun overwritelthy thy (al, bl: (Rule_Set.identifier * Rule_Set.T) list) =
2.28 +fun overwritelthy thy (al, bl: (Rule_Set.id * Rule_Set.T) list) =
2.29 let val bl' = map (insthy ((get_thy o ThyC.theory2theory') thy)) bl
2.30 in overwritel (al, bl') end;
2.31
2.32 @@ -402,7 +402,7 @@
2.33 = "{cas = " ^ (UnparseC.termopt2str cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
2.34 ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
2.35 ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = "
2.36 - ^ (Rule_Set.rls2str prls' |> quote) ^ ", thy = {" ^ (ThyC.theory2str thy') ^ "}, where_ = "
2.37 + ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ (ThyC.theory2str thy') ^ "}, where_ = "
2.38 ^ (UnparseC.terms2str w') ^ "}" |> linefeed;
2.39 fun pbts2str pbts = map pbt2str pbts |> list2str;
2.40
3.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Fri Apr 10 15:02:50 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Fri Apr 10 16:16:09 2020 +0200
3.3 @@ -7,9 +7,9 @@
3.4 signature RULE_SET =
3.5 sig
3.6 datatype T = datatype Rule_Def.rule_set
3.7 - eqtype identifier
3.8 + eqtype id
3.9
3.10 - val rls2str: T -> string
3.11 + val id: T -> string
3.12 val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
3.13 preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
3.14
3.15 @@ -40,8 +40,8 @@
3.16 structure Rule_Set(**): RULE_SET(**) =
3.17 struct
3.18 (**)
3.19 -datatype T = datatype Rule_Def.rule_set
3.20 -type identifier = string
3.21 +datatype T = datatype Rule_Def.rule_set;
3.22 +type id = string;
3.23
3.24 (*/------- this will disappear eventually ----------------------------------------------------\*)
3.25 fun dummy_ord (_: (term * term) list) (_: term, _: term) = true;
3.26 @@ -50,7 +50,7 @@
3.27 srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.EmptyScr}
3.28 (*\------- this will disappear eventually ----------------------------------------------------/*)
3.29
3.30 -fun rls2str xxx = Rule.id_rls xxx;
3.31 +val id = Rule.set_id;
3.32 fun rep Rule_Def.Empty = rep empty
3.33 | rep (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
3.34 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
3.35 @@ -94,7 +94,7 @@
3.36 erls = merge (merge_ids er1 er2) er1 er2,
3.37 srls = merge (merge_ids sr1 sr2) sr1 sr2,
3.38 calc = union Exec_Def.calc_eq ca1 ca2,
3.39 - rules = union Rule.eq_rule rs1 rs2,
3.40 + rules = union Rule.equal rs1 rs2,
3.41 errpatts = union (op =) eps1 eps2}
3.42 | merge id
3.43 (Rule_Def.Seqence {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
3.44 @@ -107,16 +107,16 @@
3.45 erls = merge (merge_ids er1 er2) er1 er2,
3.46 srls = merge (merge_ids sr1 sr2) sr1 sr2,
3.47 calc = union Exec_Def.calc_eq ca1 ca2,
3.48 - rules = union Rule.eq_rule rs1 rs2,
3.49 + rules = union Rule.equal rs1 rs2,
3.50 errpatts = union (op =) eps1 eps2}
3.51 | merge id _ _ = error ("merge: \"" ^ id ^
3.52 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Seqence");
3.53
3.54 (* datastructure for KEStore_Elems, intermediate for thehier *)
3.55 type for_kestore =
3.56 - (identifier * (* identifier unique within Isac *)
3.57 + (id * (* id unique within Isac *)
3.58 (ThyC.theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
3.59 - T)) (* ((#id o rep) T) = identifier by coding discipline *)
3.60 + T)) (* ((#id o rep) T) = id by coding discipline *)
3.61 fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
3.62
3.63 fun insert_merge (re as (id, (thyID, r1))) ys =
3.64 @@ -133,18 +133,18 @@
3.65 (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
3.66 rules = rs, errpatts = eps, scr = sc}) r =
3.67 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
3.68 - rules = gen_rems Rule.eq_rule (rs, r),
3.69 + rules = gen_rems Rule.equal (rs, r),
3.70 errpatts = eps,
3.71 scr = sc}
3.72 | keep_unique_rules id
3.73 (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
3.74 rules = rs, errpatts = eps, scr = sc}) r =
3.75 Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
3.76 - rules = gen_rems Rule.eq_rule (rs, r),
3.77 + rules = gen_rems Rule.equal (rs, r),
3.78 errpatts = eps,
3.79 scr = sc}
3.80 | keep_unique_rules id (Rule_Def.Rrls _) _ = raise ERROR ("keep_unique_rules: not for reverse-rewrite-rule-set "^id)
3.81 - | keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ rls2str rls);
3.82 + | keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ id rls);
3.83
3.84 fun get_rules Rule_Def.Empty = []
3.85 | get_rules (Rule_Def.Repeat {rules, ...}) = rules
4.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Fri Apr 10 15:02:50 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Fri Apr 10 16:16:09 2020 +0200
4.3 @@ -11,11 +11,11 @@
4.4 datatype rule = datatype Rule_Def.rule
4.5 datatype program = datatype Rule_Def.program
4.6
4.7 - val id_rls: Rule_Def.rule_set -> string
4.8 - val id_rule: Rule_Def.rule -> string
4.9 - val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool
4.10 - val rule2str: Rule_Def.rule -> string
4.11 - val rule2str': Rule_Def.rule -> string
4.12 + val set_id: Rule_Def.rule_set -> string
4.13 + val id: Rule_Def.rule -> string
4.14 + val equal: Rule_Def.rule * Rule_Def.rule -> bool
4.15 + val to_string: Rule_Def.rule -> string
4.16 + val to_string_short: Rule_Def.rule -> string
4.17
4.18 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.19 (*NONE*)
4.20 @@ -28,43 +28,37 @@
4.21 struct
4.22 (**)
4.23
4.24 -datatype rule = datatype Rule_Def.rule
4.25 -datatype program = datatype Rule_Def.program
4.26 +datatype rule = datatype Rule_Def.rule;
4.27 +datatype program = datatype Rule_Def.program;
4.28
4.29 -type calc = Rule_Def.calc (*..from Rule_Def*)
4.30 -type calID = Rule_Def.calID; (*..from Rule_Def*)
4.31 -(* eval function calling sml code during rewriting.
4.32 -Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,
4.33 - see "fun rule2stac": instead of
4.34 - Num_Calc: calID * eval_fn -> rule
4.35 - would be better
4.36 - Num_Calc: prog_calcID * (calID * eval_fn)) -> rule*)
4.37 -type eval_fn = Rule_Def.eval_fn (*..from Rule_Def*)
4.38 +type calc = Rule_Def.calc
4.39 +type calID = Rule_Def.calID;
4.40 +type eval_fn = Rule_Def.eval_fn;
4.41
4.42 -fun id_rls Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)
4.43 - | id_rls (Rule_Def.Repeat {id, ...}) = id
4.44 - | id_rls (Rule_Def.Seqence {id, ...}) = id
4.45 - | id_rls (Rule_Def.Rrls {id, ...}) = id;
4.46 +fun set_id Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)
4.47 + | set_id (Rule_Def.Repeat {id, ...}) = id
4.48 + | set_id (Rule_Def.Seqence {id, ...}) = id
4.49 + | set_id (Rule_Def.Rrls {id, ...}) = id;
4.50
4.51 -fun id_rule (Rule_Def.Thm (id, _)) = id
4.52 - | id_rule (Rule_Def.Num_Calc (id, _)) = id
4.53 - | id_rule (Rule_Def.Cal1 (id, _)) = id
4.54 - | id_rule (Rule_Def.Rls_ rls) = id_rls rls
4.55 - | id_rule Rule_Def.Erule = "Erule";
4.56 -fun eq_rule (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2
4.57 - | eq_rule (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2
4.58 - | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2
4.59 - | eq_rule _ = false;
4.60 +fun id (Rule_Def.Thm (id, _)) = id
4.61 + | id (Rule_Def.Num_Calc (id, _)) = id
4.62 + | id (Rule_Def.Cal1 (id, _)) = id
4.63 + | id (Rule_Def.Rls_ rls) = set_id rls
4.64 + | id Rule_Def.Erule = "Erule";
4.65 +fun equal (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2
4.66 + | equal (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2
4.67 + | equal (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = set_id rls1 = set_id rls2
4.68 + | equal _ = false;
4.69
4.70 -fun rule2str Rule_Def.Erule = "Erule"
4.71 - | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thmI thm ^ ")"
4.72 - | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
4.73 - | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
4.74 - | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";
4.75 -fun rule2str' Rule_Def.Erule = "Erule"
4.76 - | rule2str' (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
4.77 - | rule2str' (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
4.78 - | rule2str' (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
4.79 - | rule2str' (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";
4.80 +fun to_string Rule_Def.Erule = "Erule"
4.81 + | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thmI thm ^ ")"
4.82 + | to_string (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
4.83 + | to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
4.84 + | to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
4.85 +fun to_string_short Rule_Def.Erule = "Erule"
4.86 + | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
4.87 + | to_string_short (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
4.88 + | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
4.89 + | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
4.90
4.91 (**)end(**)
5.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml Fri Apr 10 15:02:50 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml Fri Apr 10 16:16:09 2020 +0200
5.3 @@ -84,13 +84,13 @@
5.4 | _ => str
5.5 end
5.6
5.7 -fun id_of_thm (Rule_Def.Thm (id, _)) = id (* TODO re-arrange code for rule2str *)
5.8 - | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
5.9 +fun id_of_thm (Rule_Def.Thm (id, _)) = id (* TODO re-arrange code for to_string *)
5.10 + | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ to_string r *))
5.11
5.12 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
5.13 fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
5.14 -fun thm_of_thm (Rule_Def.Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *)
5.15 - | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))
5.16 +fun thm_of_thm (Rule_Def.Thm (_, thm)) = thm (* TODO re-arrange code for to_string *)
5.17 + | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ to_string r *))
5.18 fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
5.19
5.20 (**)end(**)
6.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 10 15:02:50 2020 +0200
6.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 10 16:16:09 2020 +0200
6.3 @@ -244,15 +244,15 @@
6.4 indt (j+i) ^"</ORDER>\n" ^
6.5 indt (j+i) ^"<ERLS>\n" ^
6.6 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
6.7 - indt (j+2*i) ^ "<STRING> " ^ Rule_Set.rls2str erls ^ " </STRING>\n" ^
6.8 + indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
6.9 indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID)
6.10 - (Rule_Set.rls2str erls) ^ " </GUH>\n" ^
6.11 + (Rule_Set.id erls) ^ " </GUH>\n" ^
6.12 indt (j+i) ^"</ERLS>\n" ^
6.13 indt (j+i) ^"<SRLS>\n" ^
6.14 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
6.15 - indt (j+2*i) ^ "<STRING> " ^ Rule_Set.rls2str erls ^ " </STRING>\n" ^
6.16 + indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
6.17 indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID)
6.18 - (Rule_Set.rls2str srls) ^ " </GUH>\n" ^
6.19 + (Rule_Set.id srls) ^ " </GUH>\n" ^
6.20 indt (j+i) ^"</SRLS>\n" ^
6.21 calcrefs2xml (j+i) (thyID, calc) ^
6.22 scr2xml (j+i) scr ^
6.23 @@ -275,8 +275,8 @@
6.24 indt (j+i) ^"</ORDER>\n" ^
6.25 indt (j+i) ^"<ERLS> " ^
6.26 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
6.27 - indt (j+2*i) ^ "<STRING> " ^ Rule_Set.rls2str erls ^ " </STRING>\n" ^
6.28 - indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID) (Rule_Set.rls2str erls) ^ " </GUH>\n" ^
6.29 + indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
6.30 + indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID) (Rule_Set.id erls) ^ " </GUH>\n" ^
6.31 indt (j+i) ^"</ERLS>\n" ^
6.32 calcrefs2xml (j+i) (thyID, calc) ^
6.33 indt (j+i) ^"<SCRIPT>\n"^
7.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Apr 10 15:02:50 2020 +0200
7.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Apr 10 16:16:09 2020 +0200
7.3 @@ -25,7 +25,7 @@
7.4 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [],
7.5 mathauthors = ["isac-team"], fillpats = [], thm = thm})
7.6 end;
7.7 -fun makeHrls (part : string) (rls' : Rule_Set.identifier, thy_rls as (thyID, rls): ThyC.thyID * Rule_Set.T) =
7.8 +fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, rls): ThyC.thyID * Rule_Set.T) =
7.9 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID
7.10 in (theID, Celem.Hrls {guh = Celem.theID2guh theID, coursedesign = [],
7.11 mathauthors = ["isac-team"], thy_rls = thy_rls})
7.12 @@ -52,7 +52,7 @@
7.13 else Rule.Thm (Thm.get_name_hint thm, thm)
7.14
7.15 (* get all theorems from the list of rule-sets (defined in Knowledge) *)
7.16 -fun thms_of_rlss thy rlss = (rlss : (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list)
7.17 +fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list)
7.18 |> map (Rtools.thms_of_rls o #2 o #2)
7.19 |> flat
7.20 |> map (revert_sym thy)
7.21 @@ -64,7 +64,7 @@
7.22
7.23 fun collect_thms part thy =
7.24 map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy))
7.25 -fun collect_rlss part rlss thys = (rlss : (Rule_Set.identifier * (ThyC.thyID * Rule_Set.T)) list)
7.26 +fun collect_rlss part rlss thys = (rlss : (Rule_Set.id * (ThyC.thyID * Rule_Set.T)) list)
7.27 |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)
7.28 |> map (makeHrls part)
7.29 fun collect_cals (part, thy') =
8.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Fri Apr 10 15:02:50 2020 +0200
8.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Fri Apr 10 16:16:09 2020 +0200
8.3 @@ -44,9 +44,9 @@
8.4 type errpatID = Rule_Def.errpatID
8.5
8.6 fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
8.7 - | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.rule2str r);
8.8 -fun rule2rls' (Rule.Rls_ rls) = Rule_Set.rls2str rls
8.9 - | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.rule2str r);
8.10 + | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.to_string r);
8.11 +fun rule2rls' (Rule.Rls_ rls) = Rule_Set.id rls
8.12 + | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.to_string r);
8.13
8.14 (*the lists contain eq-al elem-pairs at the beginning;
8.15 return first list reverted (again) - ie. in order as required subsequently*)
8.16 @@ -76,7 +76,7 @@
8.17 (Tactic.Rewrite_Set (rule2rls' r),
8.18 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
8.19 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
8.20 - | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ UnparseC.term2str t)
8.21 + | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term2str t)
8.22
8.23 (* fo = ifo excluded already in inform *)
8.24 fun concat_deriv rew_ord erls rules fo ifo =
9.1 --- a/src/Tools/isac/Interpret/li-tool.sml Fri Apr 10 15:02:50 2020 +0200
9.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Fri Apr 10 16:16:09 2020 +0200
9.3 @@ -144,28 +144,28 @@
9.4 | _ => Not_Associated)
9.5 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
9.6 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
9.7 - if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
9.8 + if Rule_Set.id rls = HOLogic.dest_string rls_ then
9.9 if f = f_ then
9.10 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
9.11 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
9.12 else Not_Associated
9.13 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
9.14 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
9.15 - if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
9.16 + if Rule_Set.id rls = HOLogic.dest_string rls_ then
9.17 if f = f_ then
9.18 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
9.19 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
9.20 else Not_Associated
9.21 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
9.22 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
9.23 - if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
9.24 + if Rule_Set.id rls = HOLogic.dest_string rls_ then
9.25 if f = f_ then
9.26 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
9.27 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
9.28 else Not_Associated
9.29 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
9.30 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
9.31 - if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then
9.32 + if Rule_Set.id rls = HOLogic.dest_string rls_ then
9.33 if f = f_ then
9.34 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
9.35 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
10.1 --- a/src/Tools/isac/Interpret/rewtools.sml Fri Apr 10 15:02:50 2020 +0200
10.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Fri Apr 10 16:16:09 2020 +0200
10.3 @@ -10,17 +10,17 @@
10.4 type deriv
10.5 val contains_rule : Rule.rule -> Rule_Set.T -> bool
10.6 val atomic_appl_tacs : theory -> string -> Rule_Set.T -> term -> Tactic.input -> Tactic.input list
10.7 - val thy_containing_rls : ThyC.theory' -> Rule_Set.identifier -> string * ThyC.theory'
10.8 + val thy_containing_rls : ThyC.theory' -> Rule_Set.id -> string * ThyC.theory'
10.9 val thy_containing_cal : ThyC.theory' -> Exec_Def.prog_calcID -> string * string
10.10 datatype contthy
10.11 = ContNOrew of {applto: term, thm_rls: Celem.guh, thyID: ThyC.thyID}
10.12 | ContNOrewInst of {applto: term, bdvs: UnparseC.subst, thm_rls: Celem.guh, thminst: term, thyID: ThyC.thyID}
10.13 | ContRls of {applto: term, asms: term list, result: term, rls: Celem.guh, thyID: ThyC.thyID}
10.14 | ContRlsInst of {applto: term, asms: term list, bdvs: UnparseC.subst, result: term, rls: Celem.guh, thyID: ThyC.thyID}
10.15 - | ContThm of {applat: term, applto: term, asmrls: Rule_Set.identifier, asms: (term * term) list,
10.16 + | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
10.17 lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
10.18 thm: Celem.guh, thyID: ThyC.thyID}
10.19 - | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.identifier, asms: (term * term) list,
10.20 + | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
10.21 bdvs: UnparseC.subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
10.22 rhs: term * term, thm: Celem.guh, thminst: term, thyID: ThyC.thyID}
10.23 | EContThy
10.24 @@ -90,11 +90,11 @@
10.25 list
10.26
10.27 fun trta2str (t, r, (t', a)) =
10.28 - "\n(" ^ UnparseC.term2str t ^ ", " ^ Rule.rule2str' r ^ ", (" ^ UnparseC.term2str t' ^ ", " ^ UnparseC.terms2str a ^ "))"
10.29 + "\n(" ^ UnparseC.term2str t ^ ", " ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term2str t' ^ ", " ^ UnparseC.terms2str a ^ "))"
10.30 fun trtas2str trtas = (strs2str o (map trta2str)) trtas
10.31 val deriv2str = trtas2str
10.32 fun rta2str (r, (t, a)) =
10.33 - "\n(" ^ Rule.rule2str' r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))"
10.34 + "\n(" ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))"
10.35 fun rtas2str rtas = (strs2str o (map rta2str)) rtas
10.36 val deri2str = rtas2str
10.37
10.38 @@ -186,7 +186,7 @@
10.39 (case Rewrite.rewrite_set_ thy true rls t of
10.40 NONE => rew_once lim rts t apno rs'
10.41 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
10.42 - | rule => error ("rew_once: uncovered case " ^ Rule.rule2str rule))
10.43 + | rule => error ("rew_once: uncovered case " ^ Rule.to_string rule))
10.44 | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
10.45 in rew_once (! Celem.lim_deriv) [] tt Noap rs end
10.46
10.47 @@ -222,7 +222,7 @@
10.48 | _ => "sym_" ^ thmID
10.49 in Rule.Thm (thmID', thm') end
10.50 | sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
10.51 -| sym_rule r = error ("sym_rule: not for " ^ Rule.rule2str r)
10.52 +| sym_rule r = error ("sym_rule: not for " ^ Rule.to_string r)
10.53
10.54 (*version for reverse rewrite used before 040214*)
10.55 fun rev_deriv (t, r, (_, a)) = (sym_rule r, (t, a));
10.56 @@ -231,9 +231,9 @@
10.57
10.58 fun eq_Thm (Rule.Thm (id1, _), Rule.Thm (id2,_)) = id1 = id2
10.59 | eq_Thm (Rule.Thm (_, _), _) = false
10.60 - | eq_Thm (Rule.Rls_ r1, Rule.Rls_ r2) = Rule_Set.rls2str r1 = Rule_Set.rls2str r2
10.61 + | eq_Thm (Rule.Rls_ r1, Rule.Rls_ r2) = Rule_Set.id r1 = Rule_Set.id r2
10.62 | eq_Thm (Rule.Rls_ _, _) = false
10.63 - | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule.rule2str r1 ^ "' '" ^ Rule.rule2str r2 ^ "'")
10.64 + | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule.to_string r1 ^ "' '" ^ Rule.to_string r2 ^ "'")
10.65 fun distinct_Thm r = gen_distinct eq_Thm r
10.66
10.67 fun eq_Thms thmIDs thm = (member op = thmIDs (ThmC_Def.id_of_thm thm))
10.68 @@ -285,7 +285,7 @@
10.69 * term, (* ... instantiated .*)
10.70 result : term, (* resulting from the rewrite .*)
10.71 resasms : term list, (* ... with asms stored .*)
10.72 - asmrls : Rule_Set.identifier (* ruleset for evaluating asms .*)
10.73 + asmrls : Rule_Set.id (* ruleset for evaluating asms .*)
10.74 }
10.75 | ContThmInst of (* a theorem with bdvs in contex ============ *)
10.76 {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
10.77 @@ -303,7 +303,7 @@
10.78 * term, (*... instantiated .*)
10.79 result : term, (*resulting from the rewrite .*)
10.80 resasms : term list, (*... with asms stored .*)
10.81 - asmrls : Rule_Set.identifier (*ruleset for evaluating asms .*)
10.82 + asmrls : Rule_Set.id (*ruleset for evaluating asms .*)
10.83 }
10.84 | ContRls of (* a rule set in contex ========================= *)
10.85 {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
10.86 @@ -352,7 +352,7 @@
10.87 thm = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv),
10.88 applto = f, applat = TermC.empty, reword = ord',
10.89 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
10.90 - result = res, resasms = asm, asmrls = Rule_Set.rls2str erls}
10.91 + result = res, resasms = asm, asmrls = Rule_Set.id erls}
10.92 | Applicable.Notappl _ =>
10.93 let
10.94 val pp = Ctree.par_pblobj pt p
10.95 @@ -385,7 +385,7 @@
10.96 Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv),
10.97 bdvs = subst, thminst = thminst, applto = f, applat = TermC.empty, reword = ord',
10.98 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
10.99 - result = res, resasms = asm, asmrls = Rule_Set.rls2str erls}
10.100 + result = res, resasms = asm, asmrls = Rule_Set.id erls}
10.101 end
10.102 | Applicable.Notappl _ =>
10.103 let
10.104 @@ -442,9 +442,9 @@
10.105 fun contains_rule r rls =
10.106 let
10.107 fun (*find (_, Rls_ rls) = finds (get_rules rls)
10.108 - | find r12 = eq_rule r12
10.109 + | find r12 = equal r12
10.110 and*) finds [] = false
10.111 - | finds (r1 :: rs) = if Rule.eq_rule (r, r1) then true else finds rs
10.112 + | finds (r1 :: rs) = if Rule.equal (r, r1) then true else finds rs
10.113 in
10.114 finds (Rule_Set.get_rules rls)
10.115 end
11.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml Fri Apr 10 15:02:50 2020 +0200
11.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Fri Apr 10 16:16:09 2020 +0200
11.3 @@ -59,11 +59,11 @@
11.4 fun topt2str NONE = "NONE"
11.5 | topt2str (SOME t) = "SOME " ^ UnparseC.term2str t;
11.6 fun pstate2str {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *)
11.7 - "(" ^ Env.env2str env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.rls2str eval ^ ", " ^
11.8 + "(" ^ Env.env2str env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id eval ^ ", " ^
11.9 topt2str form_arg ^ ", \n" ^ UnparseC.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
11.10 bool2str found_accept ^ ", " ^ bool2str assoc ^ ")";
11.11 fun pstate2str' {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *)
11.12 - "(" ^ Env.env2str' env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.rls2str eval ^ ", " ^
11.13 + "(" ^ Env.env2str' env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id eval ^ ", " ^
11.14 topt2str form_arg ^ ", " ^ UnparseC.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
11.15 bool2str found_accept ^ ", " ^ bool2str assoc ^ ")";
11.16
11.17 @@ -74,13 +74,13 @@
11.18 | RrlsState of Rule_Set.rrlsstate; (*for reverse rewriting*)
11.19 val empty = Pstate e_pstate;
11.20
11.21 -fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))";
11.22 +fun rta2str (r, (t, a)) = "\n(" ^ Rule.to_string r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))";
11.23 fun string_of Uistate = "Uistate"
11.24 | string_of (Pstate pst) =
11.25 "Pstate " ^ pstate2str pst
11.26 | string_of (RrlsState (t, t1, rss, rtas)) =
11.27 "RrlsState (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.term2str t1 ^ ", " ^
11.28 - (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^
11.29 + (strs2str o (map (strs2str o (map Rule.to_string)))) rss ^ ", " ^
11.30 (strs2str o (map rta2str)) rtas ^ ")";
11.31 fun string_of' Uistate = "Uistate"
11.32 | string_of' (Pstate pst) =
12.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 10 15:02:50 2020 +0200
12.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 10 16:16:09 2020 +0200
12.3 @@ -127,7 +127,7 @@
12.4 error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.t2str thy t ^ "'")
12.5 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *)
12.6 let
12.7 - val _= trace i (" rls: " ^ Rule_Set.rls2str rrls ^ " on: " ^ UnparseC.t2str thy t)
12.8 + val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.t2str thy t)
12.9 val (t', asm, rew) = app_rev thy (i + 1) rrls t
12.10 in if rew then SOME (t', distinct asm) else NONE end
12.11 | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Num_Calc, Cal1 *)
12.12 @@ -138,7 +138,7 @@
12.13 | rew_once ruls asm ct Appl [] =
12.14 (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
12.15 | Rule_Set.Seqence _ => (ct, asm)
12.16 - | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.rls2str rls ^ "\""))
12.17 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
12.18 | rew_once ruls asm ct apno (rul :: thms) =
12.19 case rul of
12.20 Rule.Thm (thmid, thm) =>
12.21 @@ -182,9 +182,9 @@
12.22 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
12.23 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
12.24 | NONE => rew_once ruls asm ct apno thms)
12.25 - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
12.26 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
12.27 val ruls = (#rules o Rule_Set.rep) rls;
12.28 - val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)
12.29 + val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.t2str thy ct)
12.30 val (ct', asm') = rew_once ruls [] ct Noap ruls;
12.31 in if ct = ct' then NONE else SOME (ct', distinct asm') end
12.32 (*-------------------------------------------------------------*)
12.33 @@ -207,7 +207,7 @@
12.34 (* apply the normal_form of a rev-set *)
12.35 fun app_rev' thy (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
12.36 if chk_prepat thy erls prepat t then normal_form t else NONE
12.37 - | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.rls2str r ^ "\"");
12.38 + | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.id r ^ "\"");
12.39 val opt = app_rev' thy rrls t
12.40 in
12.41 case opt of
13.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 10 15:02:50 2020 +0200
13.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 10 16:16:09 2020 +0200
13.3 @@ -77,9 +77,9 @@
13.4 | Check_elementwise of TermC.as_string
13.5 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
13.6
13.7 - | Derive of Rule_Set.identifier
13.8 - | Detail_Set of Rule_Set.identifier
13.9 - | Detail_Set_Inst of Selem.subs * Rule_Set.identifier
13.10 + | Derive of Rule_Set.id
13.11 + | Detail_Set of Rule_Set.id
13.12 + | Detail_Set_Inst of Selem.subs * Rule_Set.id
13.13 | End_Detail
13.14
13.15 | Empty_Tac
13.16 @@ -93,8 +93,8 @@
13.17
13.18 | Rewrite of ThmC_Def.thm''
13.19 | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
13.20 - | Rewrite_Set of Rule_Set.identifier
13.21 - | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
13.22 + | Rewrite_Set of Rule_Set.id
13.23 + | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
13.24
13.25 | Specify_Method of Celem.metID
13.26 | Specify_Problem of Celem.pblID
13.27 @@ -111,7 +111,7 @@
13.28 val eq_tac : input * input -> bool
13.29 val is_rewtac : input -> bool
13.30 val is_rewset : input -> bool
13.31 - val rls_of : input -> Rule_Set.identifier
13.32 + val rls_of : input -> Rule_Set.id
13.33 val rule2tac : theory -> (term * term) list -> Rule.rule -> input
13.34 val input_from_T : T -> input
13.35 val result : T -> term
13.36 @@ -165,9 +165,9 @@
13.37 | Check_elementwise of TermC.as_string
13.38 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
13.39
13.40 - | Derive of Rule_Set.identifier (* WN0509 drop *)
13.41 - | Detail_Set of Rule_Set.identifier (* WN0509 drop *)
13.42 - | Detail_Set_Inst of Selem.subs * Rule_Set.identifier (* WN0509 drop *)
13.43 + | Derive of Rule_Set.id (* WN0509 drop *)
13.44 + | Detail_Set of Rule_Set.id (* WN0509 drop *)
13.45 + | Detail_Set_Inst of Selem.subs * Rule_Set.id (* WN0509 drop *)
13.46 | End_Detail (* WN0509 drop *)
13.47
13.48 | Empty_Tac
13.49 @@ -185,8 +185,8 @@
13.50 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
13.51 | Rewrite of ThmC_Def.thm''
13.52 | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
13.53 - | Rewrite_Set of Rule_Set.identifier
13.54 - | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
13.55 + | Rewrite_Set of Rule_Set.id
13.56 + | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
13.57
13.58 | Specify_Method of Celem.metID
13.59 | Specify_Problem of Celem.pblID
13.60 @@ -315,11 +315,11 @@
13.61 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
13.62 | rule2tac _ subst (Rule.Thm thm'') =
13.63 Rewrite_Inst (Selem.subst2subs subst, thm'')
13.64 - | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.rls2str rls)
13.65 + | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
13.66 | rule2tac _ subst (Rule.Rls_ rls) =
13.67 - Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.rls2str rls))
13.68 + Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.id rls))
13.69 | rule2tac _ _ rule =
13.70 - error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
13.71 + error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
13.72
13.73 (* tactics for for internal use, compare "input" for user at the front-end.
13.74 tac_ contains results from check in 'fun applicable_in'.
13.75 @@ -437,12 +437,12 @@
13.76 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
13.77 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
13.78 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
13.79 - "," ^ Rule_Set.rls2str rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
13.80 + "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
13.81 | End_Detail' _ => "End_Detail' xxx"
13.82 | Detail_Set' _ => "Detail_Set' xxx"
13.83 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
13.84
13.85 - | Derive' rls => "Derive' " ^ Rule_Set.rls2str rls
13.86 + | Derive' rls => "Derive' " ^ Rule_Set.id rls
13.87 | Calculate' _ => "Calculate' "
13.88 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
13.89
13.90 @@ -468,13 +468,13 @@
13.91 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
13.92 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
13.93
13.94 - | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.rls2str rls)
13.95 - | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.rls2str rls)
13.96 + | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
13.97 + | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls)
13.98
13.99 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
13.100 - Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.rls2str rls)
13.101 + Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.id rls)
13.102 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
13.103 - Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.rls2str rls)
13.104 + Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.id rls)
13.105
13.106 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
13.107 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
14.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Fri Apr 10 15:02:50 2020 +0200
14.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Fri Apr 10 16:16:09 2020 +0200
14.3 @@ -133,8 +133,8 @@
14.4 fun rule2stac _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ HOLogic.mk_string thmID))
14.5 | rule2stac thy (Rule.Num_Calc (c, _)) = Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
14.6 | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string (assoc_calc thy c)))
14.7 - | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.rls2str rls))
14.8 - | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.rule2str r ^ "\"");
14.9 + | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.id rls))
14.10 + | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.to_string r ^ "\"");
14.11 fun rule2stac_inst _ (Rule.Thm (thmID, _)) =
14.12 Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID))
14.13 | rule2stac_inst thy (Rule.Num_Calc (c, _)) =
14.14 @@ -142,8 +142,8 @@
14.15 | rule2stac_inst thy (Rule.Cal1 (c, _)) =
14.16 Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
14.17 | rule2stac_inst _ (Rule.Rls_ rls) =
14.18 - Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.rls2str rls))
14.19 - | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.rule2str r ^ "\"");
14.20 + Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.id rls))
14.21 + | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.to_string r ^ "\"");
14.22
14.23 (*for appropriate nesting take stacs in _reverse_ order*)
14.24 fun op #>@ sts [s] = SEq $ s $ sts
14.25 @@ -169,7 +169,7 @@
14.26 | contain_bdv (Rule.Rls_ rls :: rs) =
14.27 contain_bdv (Rule_Set.get_rules rls) orelse contain_bdv rs
14.28 | contain_bdv (r :: _) =
14.29 - error ("contain_bdv called with [" ^ Rule.id_rule r ^ ",...]");
14.30 + error ("contain_bdv called with [" ^ Rule.id r ^ ",...]");
14.31
14.32 (* filter Frees for free_str and pair their respective types with typ *)
14.33 fun subst_typ free_str typ frees =
14.34 @@ -237,7 +237,7 @@
14.35 val prog = case rls of
14.36 Rule_Def.Repeat {rules, ...} => rules2scr_Rls thy rules
14.37 | Rule_Set.Seqence {rules, ...} => rules2scr_Seq thy rules
14.38 - | _ => raise ERROR ("Auto_Prog.gen: not for rule-set \"" ^ Rule_Set.rls2str rls ^ "\"")
14.39 + | _ => raise ERROR ("Auto_Prog.gen: not for rule-set \"" ^ Rule_Set.id rls ^ "\"")
14.40 in
14.41 subst_typs prog (type_of t) (TermC.guess_bdv_typ t)
14.42 end
15.1 --- a/src/Tools/isac/Specify/appl.sml Fri Apr 10 15:02:50 2020 +0200
15.2 +++ b/src/Tools/isac/Specify/appl.sml Fri Apr 10 16:16:09 2020 +0200
15.3 @@ -29,7 +29,7 @@
15.4 (rew_ord', erls, ca)
15.5 | rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
15.6 (rew_ord', erls, ca)
15.7 - | rew_info rls = error ("rew_info called with '" ^ Rule_Set.rls2str rls ^ "'");
15.8 + | rew_info rls = error ("rew_info called with '" ^ Rule_Set.id rls ^ "'");
15.9
15.10 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
15.11 fun from_pblobj_or_detail_thm _ p pt =
16.1 --- a/src/Tools/isac/Specify/generate.sml Fri Apr 10 15:02:50 2020 +0200
16.2 +++ b/src/Tools/isac/Specify/generate.sml Fri Apr 10 16:16:09 2020 +0200
16.3 @@ -264,7 +264,7 @@
16.4 | generate1 (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
16.5 let
16.6 val (pt, c) = cappend_atomic pt p (is, ctxt) f
16.7 - (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs', Rule_Set.rls2str rls')) (f', asm) Complete
16.8 + (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs', Rule_Set.id rls')) (f', asm) Complete
16.9 val pt = update_branch pt p TransitiveB
16.10 in
16.11 ((p, Res), c, FormKF (UnparseC.term2str f'), pt)
16.12 @@ -273,7 +273,7 @@
16.13 let
16.14 val (pt, _) = cappend_form pt p (is, ctxt) f
16.15 val pt = update_branch pt p TransitiveB
16.16 - val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule_Set.rls2str rls)) f
16.17 + val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule_Set.id rls)) f
16.18 val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
16.19 val pos' = ((lev_on o lev_dn) p, Frm)
16.20 in
16.21 @@ -282,7 +282,7 @@
16.22 | generate1 (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
16.23 let
16.24 val (pt, c) = cappend_atomic pt p (is, ctxt) f
16.25 - (Tactic.Rewrite_Set (Rule_Set.rls2str rls')) (f', asm) Complete
16.26 + (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Complete
16.27 val pt = update_branch pt p TransitiveB
16.28 in
16.29 ((p, Res), c, FormKF (UnparseC.term2str f'), pt)
16.30 @@ -291,7 +291,7 @@
16.31 let
16.32 val (pt, _) = cappend_form pt p (is, ctxt) f
16.33 val pt = update_branch pt p TransitiveB
16.34 - val is = init_istate (Tactic.Rewrite_Set (Rule_Set.rls2str rls)) f
16.35 + val is = init_istate (Tactic.Rewrite_Set (Rule_Set.id rls)) f
16.36 val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
16.37 val pos' = ((lev_on o lev_dn) p, Frm)
16.38 in
16.39 @@ -401,7 +401,7 @@
16.40 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
16.41 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
16.42 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
16.43 - val pt = update_tac pt p (Tactic.Derive (Rule_Set.rls2str nrls))
16.44 + val pt = update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
16.45 val pt = update_branch pt p TransitiveB
16.46 in (c, (pt, pos: pos')) end
16.47 | embed_deriv tacis (pt, (p, Res)) =
16.48 @@ -418,7 +418,7 @@
16.49 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
16.50 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
16.51 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
16.52 - val pt = update_tac pt p (Tactic.Derive (Rule_Set.rls2str nrls))
16.53 + val pt = update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
16.54 val pt = update_branch pt p TransitiveB
16.55 in (c, (pt, pos)) end
16.56 | embed_deriv _ _ = error "embed_deriv: uncovered definition"
17.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy Fri Apr 10 15:02:50 2020 +0200
17.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy Fri Apr 10 16:16:09 2020 +0200
17.3 @@ -4,6 +4,6 @@
17.4
17.5 ML_file "lucas_interpreter.sml"
17.6 ML \<open>
17.7 -(*val test_ruleset' = Unsynchronized.ref ([] : (Rule_Set.identifier * (theory' * rls)) list)*)
17.8 +(*val test_ruleset' = Unsynchronized.ref ([] : (Rule_Set.id * (theory' * rls)) list)*)
17.9 \<close>
17.10 end
18.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Fri Apr 10 15:02:50 2020 +0200
18.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Fri Apr 10 16:16:09 2020 +0200
18.3 @@ -22,7 +22,7 @@
18.4 case rules of
18.5 [Rule.Thm ("not_def", _)] => ()
18.6 | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
18.7 - (* merge rules of rls with the same Rule_Set.identifier must be done one level higher:
18.8 + (* merge rules of rls with the same Rule_Set.id must be done one level higher:
18.9 Test_KEStore_Elems.add_rlss does *add* or *overwrite* *)
18.10 \<close>
18.11
19.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Fri Apr 10 15:02:50 2020 +0200
19.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Fri Apr 10 16:16:09 2020 +0200
19.3 @@ -7,8 +7,8 @@
19.4 *)
19.5 signature KESTORE_ELEMS =
19.6 sig
19.7 - val get_rlss: theory -> (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list
19.8 - val add_rlss: (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list -> theory -> theory
19.9 + val get_rlss: theory -> (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list
19.10 + val add_rlss: (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list -> theory -> theory
19.11 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
19.12 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
19.13 (*etc*)
19.14 @@ -20,7 +20,7 @@
19.15
19.16 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
19.17 structure Data = Theory_Data (
19.18 - type T = (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list;
19.19 + type T = (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list;
19.20 val empty = [];
19.21 val extend = I;
19.22 val merge = merge rls_eq;
20.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 10 15:02:50 2020 +0200
20.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 10 16:16:09 2020 +0200
20.3 @@ -189,13 +189,13 @@
20.4 ". (/THEOREM)\n" ^
20.5 "(/REWRITEINSTTACTIC)\n" then () else error "xml_of_tac Rewrite_Inst CHANGED";
20.6
20.7 -Rewrite_Set: Rule_Set.identifier -> Tactic.input;
20.8 +Rewrite_Set: Rule_Set.id -> Tactic.input;
20.9 val tac = Rewrite_Set("simplify");
20.10 if xmlstr 0 (xml_of_tac tac) = "(REWRITESETTACTIC name=Rewrite_Set)\n" ^
20.11 ". simplify\n" ^
20.12 "(/REWRITESETTACTIC)\n" then () else error "xml_of_tac Rewrite_Set CHANGED";
20.13
20.14 -Rewrite_Set_Inst: subs * Rule_Set.identifier -> Tactic.input;
20.15 +Rewrite_Set_Inst: subs * Rule_Set.id -> Tactic.input;
20.16 val tac = Rewrite_Set_Inst(["(''bdv'', x)"], "simplify");
20.17 if xmlstr 0 (xml_of_tac tac) =
20.18 "(REWRITESETINSTTACTIC name=Rewrite_Set_Inst)\n" ^
21.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Apr 10 15:02:50 2020 +0200
21.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Apr 10 16:16:09 2020 +0200
21.3 @@ -188,8 +188,8 @@
21.4 "----------- fun thms_of_rlss ------------------------------------";
21.5 "----------- fun thms_of_rlss ------------------------------------";
21.6 val rlss =
21.7 - [("empty" : Rule_Set.identifier, ("KEStore": theory', Rule_Set.empty)),
21.8 - ("discard_minus" : Rule_Set.identifier, ("Poly": theory', discard_minus))]
21.9 + [("empty" : Rule_Set.id, ("KEStore": theory', Rule_Set.empty)),
21.10 + ("discard_minus" : Rule_Set.id, ("Poly": theory', discard_minus))]
21.11 ;
21.12 val [_, (thmID, term)] = thms_of_rlss thy rlss;
21.13 (*
21.14 @@ -198,7 +198,7 @@
21.15 *)
21.16 ;
21.17 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
21.18 -val rlss' = (rlss : (Rule_Set.identifier * (theory' * Rule_Set.T)) list)
21.19 +val rlss' = (rlss : (Rule_Set.id * (theory' * Rule_Set.T)) list)
21.20 |> map (thms_of_rls o #2 o #2)
21.21 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
21.22 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
22.1 --- a/test/Tools/isac/Knowledge/rational.sml Fri Apr 10 15:02:50 2020 +0200
22.2 +++ b/test/Tools/isac/Knowledge/rational.sml Fri Apr 10 16:16:09 2020 +0200
22.3 @@ -809,15 +809,15 @@
22.4 (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC_Def.thmID_of_derivation_name)
22.5 then () else error "first element of revset changed";
22.6 if
22.7 -(revsets |> nth 1 |> nth 1 |> rule2str) = "Thm (\"realpow_twoI\",?r1 ^^^ 2 = ?r1 * ?r1)" andalso
22.8 -(revsets |> nth 1 |> nth 2 |> rule2str) = "Thm (\"#: 9 = 3 ^^^ 2\",9 = 3 ^^^ 2)" andalso
22.9 -(revsets |> nth 1 |> nth 3 |> rule2str) = "Thm (\"#: 6 * x = 2 * (3 * x)\",6 * x = 2 * (3 * x))"
22.10 +(revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\",?r1 ^^^ 2 = ?r1 * ?r1)" andalso
22.11 +(revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 ^^^ 2\",9 = 3 ^^^ 2)" andalso
22.12 +(revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\",6 * x = 2 * (3 * x))"
22.13 andalso
22.14 -(revsets |> nth 1 |> nth 4 |> rule2str) = "Thm (\"#: -3 * x = -1 * (3 * x)\",-3 * x = -1 * (3 * x))"
22.15 +(revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: -3 * x = -1 * (3 * x)\",-3 * x = -1 * (3 * x))"
22.16 andalso
22.17 -(revsets |> nth 1 |> nth 5 |> rule2str) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso
22.18 -(revsets |> nth 1 |> nth 6 |> rule2str) = "Rls_ (\"sym_order_mult_rls_\")" andalso
22.19 -(revsets |> nth 1 |> nth 7 |> rule2str) =
22.20 +(revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso
22.21 +(revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso
22.22 +(revsets |> nth 1 |> nth 7 |> Rule.to_string) =
22.23 "Thm (\"sym_mult_assoc\",?a * (?b * ?c) = ?a * ?b * ?c)"
22.24 then () else error "first 7 elements in revset changed"
22.25
22.26 @@ -1706,7 +1706,7 @@
22.27
22.28 (*default_print_depth 99;*) map (UnparseC.term2str o #1) der; (*default_print_depth 3;*)
22.29 "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]";
22.30 -(*default_print_depth 99;*) map (rule2str o #2) der; (*default_print_depth 3;*)
22.31 +(*default_print_depth 99;*) map (Rule.to_string o #2) der; (*default_print_depth 3;*)
22.32 (*default_print_depth 99;*) map (UnparseC.term2str o #1 o #3) der; (*default_print_depth 3;*)
22.33
22.34 val der = make_deriv thy Atools_erls rules ro NONE
23.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 10 15:02:50 2020 +0200
23.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 10 16:16:09 2020 +0200
23.3 @@ -532,7 +532,7 @@
23.4 | rew_once ruls asm ct Appl [] =
23.5 (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
23.6 | Rule_Set.Seqence _ => (ct, asm)
23.7 - | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
23.8 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
23.9 | rew_once ruls asm ct apno (rul :: thms) =
23.10 case rul of
23.11 Rule.Thm (thmid, thm) =>
23.12 @@ -576,9 +576,9 @@
23.13 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
23.14 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
23.15 | NONE => rew_once ruls asm ct apno thms)
23.16 - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
23.17 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
23.18 val ruls = (#rules o Rule.Rule_Set.rep) rls;
23.19 -(* val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)*)
23.20 +(* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.t2str thy ct)*)
23.21 val (ct', asm') = rew_once ruls [] ct Noap ruls;
23.22 "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
23.23 = (ruls, []:term list, ct, Noap, ruls);
24.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Fri Apr 10 15:02:50 2020 +0200
24.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Fri Apr 10 16:16:09 2020 +0200
24.3 @@ -162,8 +162,8 @@
24.4 "~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
24.5 val fT = type_of f;
24.6 val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, fT] ---> fT)
24.7 - $ HOLogic.mk_string (Rule_Set.rls2str rls) $ f;
24.8 -(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule_Set.rls2str rls, idT) *)
24.9 + $ HOLogic.mk_string (Rule_Set.id rls) $ f;
24.10 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule_Set.id rls, idT) *)
24.11
24.12 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
24.13 case nxt of (Rewrite_Set _) => ()
25.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Fri Apr 10 15:02:50 2020 +0200
25.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Fri Apr 10 16:16:09 2020 +0200
25.3 @@ -83,7 +83,7 @@
25.4 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))),
25.5 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = (pt, d, m, stac);
25.6
25.7 -(*+*)if Rule_Set.rls2str rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
25.8 +(*+*)if Rule_Set.id rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
25.9
25.10 "~~~~~ continue me[1] after Step.by_tactic";
25.11 val (pt, p) = ptp''''';
26.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Fri Apr 10 15:02:50 2020 +0200
26.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Fri Apr 10 16:16:09 2020 +0200
26.3 @@ -68,10 +68,10 @@
26.4
26.5 (** )val (pt, c) =( **)
26.6 cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
26.7 - (Tactic.Rewrite_Set (Rule_Set.rls2str rls')) (f',asm) Complete;
26.8 + (Tactic.Rewrite_Set (Rule_Set.id rls')) (f',asm) Complete;
26.9 "~~~~~ fun cappend_atomic , args:"; val (pt, p: pos, ic_res, f, r, f', s)
26.10 = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,
26.11 - (Tactic.Rewrite_Set (Rule_Set.rls2str rls')), (f',asm), Complete);
26.12 + (Tactic.Rewrite_Set (Rule_Set.id rls')), (f',asm), Complete);
26.13 (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*then*);
26.14 val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
26.15 val (pt, cs) = cut_tree(*!*)pt (p, Frm);