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