diff -r 75a9d629ea53 -r 3b194392ea71 src/Tools/isac/BaseDefinitions/rule-set.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Fri Apr 10 15:02:50 2020 +0200
@@ -0,0 +1,174 @@
+(* Title:  BaseDefinitions/rule-set.sml
+   Author: Walther Neuper
+   (c) due to copyright terms
+
+In ISAC a Rule_Set serves rewriting. KEStore holds all rule-sets for ubiquitous access.
+*)
+signature RULE_SET =
+sig
+  datatype T = datatype Rule_Def.rule_set
+  eqtype identifier
+
+  val rls2str: T -> string
+  val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
+    preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
+
+  val append_rules: string -> T -> Rule_Def.rule list -> T
+  val keep_unique_rules: string -> T ->  Rule_Def.rule list -> T
+  val merge: string -> T -> T -> T
+  val get_rules: T -> Rule_Def.rule list
+
+  type for_kestore
+  val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
+  val to_kestore: for_kestore list * for_kestore list -> for_kestore list
+
+(*/------- this will disappear eventually -----------\*)
+  val empty: T
+  type rrlsstate = term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list
+  val e_rrlsstate: rrlsstate
+  val e_rrls: T
+(*\------- this will disappear eventually -----------/*)
+
+(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
+  (*NONE*)
+(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
+  val insert_merge: for_kestore -> for_kestore list -> for_kestore list
+( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
+end
+
+(**)
+structure Rule_Set(**): RULE_SET(**) =
+struct
+(**)
+datatype T = datatype Rule_Def.rule_set
+type identifier = string
+
+(*/------- this will disappear eventually ----------------------------------------------------\*)
+fun dummy_ord (_: (term * term) list) (_: term, _: term) = true;
+val empty =
+  Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
+    srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.EmptyScr}
+(*\------- this will disappear eventually ----------------------------------------------------/*)
+
+fun rls2str xxx = Rule.id_rls xxx;
+fun rep Rule_Def.Empty = rep empty
+  | rep (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
+    {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
+      calc = calc, rules = rules, scr = scr}
+  | rep (Rule_Def.Seqence {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
+    {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
+      calc = calc, rules = rules, scr = scr}
+  | rep (Rule_Def.Rrls _)  = rep empty
+
+fun append_rules id Rule_Def.Empty _ = raise ERROR ("append_rules: with \"" ^ id ^ "\" not for Rule_Def.Empty")
+  | append_rules id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
+			rules = rs, errpatts = errpatts, scr = sc}) r =
+    Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
+      rules = rs @ r, errpatts = errpatts, scr = sc}
+  | append_rules id (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
+			rules = rs, errpatts = errpatts, scr = sc}) r =
+    Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
+      rules = rs @ r, errpatts = errpatts, scr = sc}
+  | append_rules id (Rule_Def.Rrls _) _ = raise ERROR ("append_rules: not for reverse-rewrite-rule-set " ^ id);
+
+fun merge_ids rls1 rls2 =
+  let 
+    val id1 = (#id o rep) rls1
+    val id2 = (#id o rep) rls2
+  in
+    if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
+  end
+
+fun merge _ Rule_Def.Empty rls = rls
+  | merge _ rls Rule_Def.Empty = rls
+  | merge _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
+  | merge _ _ (Rrls x) = Rrls x
+  | merge id
+	  (Rule_Def.Repeat {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
+	    rules = rs1, errpatts = eps1, scr = sc1, ...})
+	  (Rule_Def.Repeat {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
+	    rules = rs2, errpatts = eps2, ...})
+    =
+	  Rule_Def.Repeat {id = id, rew_ord = ro1, scr = sc1,
+	    preconds = union (op =) pc1 pc2,	    
+	    erls = merge (merge_ids er1 er2) er1 er2,
+	    srls = merge (merge_ids sr1 sr2) sr1 sr2,
+	    calc = union Exec_Def.calc_eq ca1 ca2,
+		  rules = union Rule.eq_rule rs1 rs2,
+      errpatts = union (op =) eps1 eps2}
+  | merge id
+	  (Rule_Def.Seqence {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
+	    rules = rs1, errpatts = eps1, scr = sc1, ...})
+	  (Rule_Def.Seqence {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
+	    rules = rs2, errpatts = eps2, ...})
+    =
+	  Rule_Def.Seqence {id = id, rew_ord = ro1, scr = sc1,
+	    preconds = union (op =) pc1 pc2,	    
+	    erls = merge (merge_ids er1 er2) er1 er2,
+	    srls = merge (merge_ids sr1 sr2) sr1 sr2,
+	    calc = union Exec_Def.calc_eq ca1 ca2,
+		  rules = union Rule.eq_rule rs1 rs2,
+      errpatts = union (op =) eps1 eps2}
+  | merge id _ _ = error ("merge: \"" ^ id ^ 
+    "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Seqence");
+
+(* datastructure for KEStore_Elems, intermediate for thehier *)
+type for_kestore = 
+  (identifier *     (* identifier unique within Isac *)
+  (ThyC.theory' *  (* just for assignment in thehier, not appropriate for parsing etc *)
+    T))     (* ((#id o rep) T) = identifier   by coding discipline *)
+fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
+
+fun insert_merge (re as (id, (thyID, r1))) ys = 
+    case get_index (fn y => if curry equal re y then SOME y else NONE) ys of
+      NONE => re :: ys
+    | SOME (i, (_, (_, r2))) => 
+      let
+        val r12 = merge id r1 r2
+      in list_update ys i (id, (thyID, r12)) end
+fun to_kestore (s1, s2) = fold insert_merge s1 s2;
+
+(* used only for one hack *)
+fun keep_unique_rules id 
+     (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
+  		  rules = rs, errpatts = eps, scr = sc}) r =
+      Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
+  	    rules = gen_rems Rule.eq_rule (rs, r),
+  	    errpatts = eps,
+  	    scr = sc}
+  | keep_unique_rules id
+     (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
+  		  rules = rs, errpatts = eps, scr = sc}) r =
+      Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
+  	    rules = gen_rems Rule.eq_rule (rs, r),
+  	    errpatts = eps,
+  	    scr = sc}
+  | keep_unique_rules id (Rule_Def.Rrls _) _ = raise ERROR ("keep_unique_rules: not for reverse-rewrite-rule-set "^id)
+  | keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ rls2str rls);
+
+fun get_rules Rule_Def.Empty = []
+  | get_rules (Rule_Def.Repeat {rules, ...}) = rules
+  | get_rules (Rule_Def.Seqence {rules, ...}) = rules
+  | get_rules (Rule_Def.Rrls _) = [];
+
+(*/------- this will disappear eventually -----------\*)
+type rrlsstate =  (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
+  (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
+val e_rrlsstate = (UnparseC.e_term, UnparseC.e_term, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.e_term, []))]) : rrlsstate;
+local
+    fun ii (_: term) = e_rrlsstate;
+    fun no (_: term) = SOME (UnparseC.e_term, [UnparseC.e_term]);
+    fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
+    fun ne (_: Rule_Def.rule list list) (_: term) = SOME Rule_Def.Erule;
+    fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
+in
+val e_rfuns = Rule_Def.Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
+		  next_rule = ne, attach_form = fo};
+end;
+val e_rrls =
+  Rule_Def.Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
+    calc = [], errpatts = [], scr = e_rfuns}
+(*\------- this will disappear eventually -----------/*)
+
+
+(**)end(**)