1.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Fri Apr 10 15:02:50 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Fri Apr 10 16:16:09 2020 +0200
1.3 @@ -7,9 +7,9 @@
1.4 signature RULE_SET =
1.5 sig
1.6 datatype T = datatype Rule_Def.rule_set
1.7 - eqtype identifier
1.8 + eqtype id
1.9
1.10 - val rls2str: T -> string
1.11 + val id: T -> string
1.12 val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
1.13 preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
1.14
1.15 @@ -40,8 +40,8 @@
1.16 structure Rule_Set(**): RULE_SET(**) =
1.17 struct
1.18 (**)
1.19 -datatype T = datatype Rule_Def.rule_set
1.20 -type identifier = string
1.21 +datatype T = datatype Rule_Def.rule_set;
1.22 +type id = string;
1.23
1.24 (*/------- this will disappear eventually ----------------------------------------------------\*)
1.25 fun dummy_ord (_: (term * term) list) (_: term, _: term) = true;
1.26 @@ -50,7 +50,7 @@
1.27 srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.EmptyScr}
1.28 (*\------- this will disappear eventually ----------------------------------------------------/*)
1.29
1.30 -fun rls2str xxx = Rule.id_rls xxx;
1.31 +val id = Rule.set_id;
1.32 fun rep Rule_Def.Empty = rep empty
1.33 | rep (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
1.34 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
1.35 @@ -94,7 +94,7 @@
1.36 erls = merge (merge_ids er1 er2) er1 er2,
1.37 srls = merge (merge_ids sr1 sr2) sr1 sr2,
1.38 calc = union Exec_Def.calc_eq ca1 ca2,
1.39 - rules = union Rule.eq_rule rs1 rs2,
1.40 + rules = union Rule.equal rs1 rs2,
1.41 errpatts = union (op =) eps1 eps2}
1.42 | merge id
1.43 (Rule_Def.Seqence {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
1.44 @@ -107,16 +107,16 @@
1.45 erls = merge (merge_ids er1 er2) er1 er2,
1.46 srls = merge (merge_ids sr1 sr2) sr1 sr2,
1.47 calc = union Exec_Def.calc_eq ca1 ca2,
1.48 - rules = union Rule.eq_rule rs1 rs2,
1.49 + rules = union Rule.equal rs1 rs2,
1.50 errpatts = union (op =) eps1 eps2}
1.51 | merge id _ _ = error ("merge: \"" ^ id ^
1.52 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Seqence");
1.53
1.54 (* datastructure for KEStore_Elems, intermediate for thehier *)
1.55 type for_kestore =
1.56 - (identifier * (* identifier unique within Isac *)
1.57 + (id * (* id unique within Isac *)
1.58 (ThyC.theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
1.59 - T)) (* ((#id o rep) T) = identifier by coding discipline *)
1.60 + T)) (* ((#id o rep) T) = id by coding discipline *)
1.61 fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
1.62
1.63 fun insert_merge (re as (id, (thyID, r1))) ys =
1.64 @@ -133,18 +133,18 @@
1.65 (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.66 rules = rs, errpatts = eps, scr = sc}) r =
1.67 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.68 - rules = gen_rems Rule.eq_rule (rs, r),
1.69 + rules = gen_rems Rule.equal (rs, r),
1.70 errpatts = eps,
1.71 scr = sc}
1.72 | keep_unique_rules id
1.73 (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.74 rules = rs, errpatts = eps, scr = sc}) r =
1.75 Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.76 - rules = gen_rems Rule.eq_rule (rs, r),
1.77 + rules = gen_rems Rule.equal (rs, r),
1.78 errpatts = eps,
1.79 scr = sc}
1.80 | keep_unique_rules id (Rule_Def.Rrls _) _ = raise ERROR ("keep_unique_rules: not for reverse-rewrite-rule-set "^id)
1.81 - | keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ rls2str rls);
1.82 + | keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ id rls);
1.83
1.84 fun get_rules Rule_Def.Empty = []
1.85 | get_rules (Rule_Def.Repeat {rules, ...}) = rules