1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Fri Apr 10 15:02:50 2020 +0200
1.3 @@ -0,0 +1,174 @@
1.4 +(* Title: BaseDefinitions/rule-set.sml
1.5 + Author: Walther Neuper
1.6 + (c) due to copyright terms
1.7 +
1.8 +In ISAC a Rule_Set serves rewriting. KEStore holds all rule-sets for ubiquitous access.
1.9 +*)
1.10 +signature RULE_SET =
1.11 +sig
1.12 + datatype T = datatype Rule_Def.rule_set
1.13 + eqtype identifier
1.14 +
1.15 + val rls2str: T -> string
1.16 + val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
1.17 + preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
1.18 +
1.19 + val append_rules: string -> T -> Rule_Def.rule list -> T
1.20 + val keep_unique_rules: string -> T -> Rule_Def.rule list -> T
1.21 + val merge: string -> T -> T -> T
1.22 + val get_rules: T -> Rule_Def.rule list
1.23 +
1.24 + type for_kestore
1.25 + val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
1.26 + val to_kestore: for_kestore list * for_kestore list -> for_kestore list
1.27 +
1.28 +(*/------- this will disappear eventually -----------\*)
1.29 + val empty: T
1.30 + type rrlsstate = term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list
1.31 + val e_rrlsstate: rrlsstate
1.32 + val e_rrls: T
1.33 +(*\------- this will disappear eventually -----------/*)
1.34 +
1.35 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.36 + (*NONE*)
1.37 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.38 + val insert_merge: for_kestore -> for_kestore list -> for_kestore list
1.39 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.40 +end
1.41 +
1.42 +(**)
1.43 +structure Rule_Set(**): RULE_SET(**) =
1.44 +struct
1.45 +(**)
1.46 +datatype T = datatype Rule_Def.rule_set
1.47 +type identifier = string
1.48 +
1.49 +(*/------- this will disappear eventually ----------------------------------------------------\*)
1.50 +fun dummy_ord (_: (term * term) list) (_: term, _: term) = true;
1.51 +val empty =
1.52 + Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
1.53 + srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.EmptyScr}
1.54 +(*\------- this will disappear eventually ----------------------------------------------------/*)
1.55 +
1.56 +fun rls2str xxx = Rule.id_rls xxx;
1.57 +fun rep Rule_Def.Empty = rep empty
1.58 + | rep (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
1.59 + {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
1.60 + calc = calc, rules = rules, scr = scr}
1.61 + | rep (Rule_Def.Seqence {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
1.62 + {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
1.63 + calc = calc, rules = rules, scr = scr}
1.64 + | rep (Rule_Def.Rrls _) = rep empty
1.65 +
1.66 +fun append_rules id Rule_Def.Empty _ = raise ERROR ("append_rules: with \"" ^ id ^ "\" not for Rule_Def.Empty")
1.67 + | append_rules id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.68 + rules = rs, errpatts = errpatts, scr = sc}) r =
1.69 + Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.70 + rules = rs @ r, errpatts = errpatts, scr = sc}
1.71 + | append_rules id (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.72 + rules = rs, errpatts = errpatts, scr = sc}) r =
1.73 + Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.74 + rules = rs @ r, errpatts = errpatts, scr = sc}
1.75 + | append_rules id (Rule_Def.Rrls _) _ = raise ERROR ("append_rules: not for reverse-rewrite-rule-set " ^ id);
1.76 +
1.77 +fun merge_ids rls1 rls2 =
1.78 + let
1.79 + val id1 = (#id o rep) rls1
1.80 + val id2 = (#id o rep) rls2
1.81 + in
1.82 + if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
1.83 + end
1.84 +
1.85 +fun merge _ Rule_Def.Empty rls = rls
1.86 + | merge _ rls Rule_Def.Empty = rls
1.87 + | merge _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
1.88 + | merge _ _ (Rrls x) = Rrls x
1.89 + | merge id
1.90 + (Rule_Def.Repeat {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
1.91 + rules = rs1, errpatts = eps1, scr = sc1, ...})
1.92 + (Rule_Def.Repeat {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
1.93 + rules = rs2, errpatts = eps2, ...})
1.94 + =
1.95 + Rule_Def.Repeat {id = id, rew_ord = ro1, scr = sc1,
1.96 + preconds = union (op =) pc1 pc2,
1.97 + erls = merge (merge_ids er1 er2) er1 er2,
1.98 + srls = merge (merge_ids sr1 sr2) sr1 sr2,
1.99 + calc = union Exec_Def.calc_eq ca1 ca2,
1.100 + rules = union Rule.eq_rule rs1 rs2,
1.101 + errpatts = union (op =) eps1 eps2}
1.102 + | merge id
1.103 + (Rule_Def.Seqence {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
1.104 + rules = rs1, errpatts = eps1, scr = sc1, ...})
1.105 + (Rule_Def.Seqence {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
1.106 + rules = rs2, errpatts = eps2, ...})
1.107 + =
1.108 + Rule_Def.Seqence {id = id, rew_ord = ro1, scr = sc1,
1.109 + preconds = union (op =) pc1 pc2,
1.110 + erls = merge (merge_ids er1 er2) er1 er2,
1.111 + srls = merge (merge_ids sr1 sr2) sr1 sr2,
1.112 + calc = union Exec_Def.calc_eq ca1 ca2,
1.113 + rules = union Rule.eq_rule rs1 rs2,
1.114 + errpatts = union (op =) eps1 eps2}
1.115 + | merge id _ _ = error ("merge: \"" ^ id ^
1.116 + "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Seqence");
1.117 +
1.118 +(* datastructure for KEStore_Elems, intermediate for thehier *)
1.119 +type for_kestore =
1.120 + (identifier * (* identifier unique within Isac *)
1.121 + (ThyC.theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
1.122 + T)) (* ((#id o rep) T) = identifier by coding discipline *)
1.123 +fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
1.124 +
1.125 +fun insert_merge (re as (id, (thyID, r1))) ys =
1.126 + case get_index (fn y => if curry equal re y then SOME y else NONE) ys of
1.127 + NONE => re :: ys
1.128 + | SOME (i, (_, (_, r2))) =>
1.129 + let
1.130 + val r12 = merge id r1 r2
1.131 + in list_update ys i (id, (thyID, r12)) end
1.132 +fun to_kestore (s1, s2) = fold insert_merge s1 s2;
1.133 +
1.134 +(* used only for one hack *)
1.135 +fun keep_unique_rules id
1.136 + (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.137 + rules = rs, errpatts = eps, scr = sc}) r =
1.138 + Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.139 + rules = gen_rems Rule.eq_rule (rs, r),
1.140 + errpatts = eps,
1.141 + scr = sc}
1.142 + | keep_unique_rules id
1.143 + (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.144 + rules = rs, errpatts = eps, scr = sc}) r =
1.145 + Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.146 + rules = gen_rems Rule.eq_rule (rs, r),
1.147 + errpatts = eps,
1.148 + scr = sc}
1.149 + | keep_unique_rules id (Rule_Def.Rrls _) _ = raise ERROR ("keep_unique_rules: not for reverse-rewrite-rule-set "^id)
1.150 + | keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ rls2str rls);
1.151 +
1.152 +fun get_rules Rule_Def.Empty = []
1.153 + | get_rules (Rule_Def.Repeat {rules, ...}) = rules
1.154 + | get_rules (Rule_Def.Seqence {rules, ...}) = rules
1.155 + | get_rules (Rule_Def.Rrls _) = [];
1.156 +
1.157 +(*/------- this will disappear eventually -----------\*)
1.158 +type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
1.159 + (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
1.160 +val e_rrlsstate = (UnparseC.e_term, UnparseC.e_term, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.e_term, []))]) : rrlsstate;
1.161 +local
1.162 + fun ii (_: term) = e_rrlsstate;
1.163 + fun no (_: term) = SOME (UnparseC.e_term, [UnparseC.e_term]);
1.164 + fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
1.165 + fun ne (_: Rule_Def.rule list list) (_: term) = SOME Rule_Def.Erule;
1.166 + fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
1.167 +in
1.168 +val e_rfuns = Rule_Def.Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
1.169 + next_rule = ne, attach_form = fo};
1.170 +end;
1.171 +val e_rrls =
1.172 + Rule_Def.Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
1.173 + calc = [], errpatts = [], scr = e_rfuns}
1.174 +(*\------- this will disappear eventually -----------/*)
1.175 +
1.176 +
1.177 +(**)end(**)