walther@59866: (* Title: BaseDefinitions/rule-set.sml walther@59850: Author: Walther Neuper walther@59850: (c) due to copyright terms walther@59850: walther@59887: In ISAC a Rule_Set serves rewriting. Know_Store holds all rule-sets for ubiquitous access. walther@60384: *) 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@60509: preconds: term list, rew_ord: Rewrite_Ord.T, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T} Walther@60436: val to_string: T -> string walther@59852: walther@59852: val append_rules: string -> T -> Rule_Def.rule list -> T walther@60384: val append_erls_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@59914: val id_from_rule: Rule.rule -> string walther@59914: val contains: Rule.rule -> T -> bool 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 ----------------------------------------------------/*) wenzelm@60223: \<^isac_test>\ walther@59852: val insert_merge: for_kestore -> for_kestore list -> for_kestore list wenzelm@60223: \ 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@60477: fun dummy_ord (_: LibraryC.subst) (_: 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@60436: fun to_string Rule_Def.Empty = "Rule_Set.Empty" Walther@60436: | to_string (Rule_Def.Repeat {id, preconds, rew_ord, erls = _, srls = _, calc = _, errpatts = _, rules, scr}) = Walther@60436: "(Rule_Def.Repeat {id = " ^ id ^ ", preconds = " ^ UnparseC.terms preconds ^ ", rew_ord = " ^ Rewrite_Ord.to_string rew_ord Walther@60436: ^ ",\n erls = _, srls = _, calc = _, errpatts = _, " Walther@60436: ^ ",\n rules = " ^ Rule.s_to_string rules Walther@60440: ^ ",\n rules = " ^ Rule_Def.program_to_string scr ^ "})" Walther@60436: | to_string (Rule_Def.Sequence {id, preconds, rew_ord, erls = _, srls = _, calc = _, errpatts = _, rules, scr}) = Walther@60436: "(Rule_Def.Repeat {id = " ^ id ^ ", preconds = " ^ UnparseC.terms preconds ^ ", rew_ord = " ^ Rewrite_Ord.to_string rew_ord Walther@60436: ^ ",\n erls = _, srls = _, calc = _, errpatts = _, " Walther@60436: ^ ",\n rules = " ^ Rule.s_to_string rules Walther@60440: ^ ",\n rules = " ^ Rule_Def.program_to_string scr ^ "})" Walther@60436: | to_string (Rule_Def.Rrls _) = "Rule_Def.Rrls _" walther@59850: walther@60384: fun append_rules id Rule_Def.Empty r = (*.. required for append_erls_rules *) walther@60384: Rule_Def.Repeat {id = id, preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty, walther@60384: srls = Rule_Def.Empty, calc = [], rules = r, errpatts = [], scr = Rule_Def.Empty_Prog} 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@60384: fun append_erls_rules id_erls Rule_Def.Empty _ = walther@60384: raise ERROR ("append_erls_rules: with \"" ^ id_erls ^ "\" not for Rule_Def.Empty") walther@60384: | append_erls_rules id_erls (Rule_Def.Repeat walther@60384: {id = id, preconds = pc, rew_ord = ro, erls = erls, srls = sr, calc = ca, walther@60384: rules = rules, errpatts = errpatts, scr = sc}) rs = walther@60384: Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = append_rules id_erls erls rs, walther@60384: srls = sr, calc = ca, rules = rules, errpatts = errpatts, scr = sc} walther@60384: | append_erls_rules id_erls (Rule_Def.Sequence walther@60384: {id = id, preconds = pc, rew_ord = ro, erls = erls, srls = sr, calc = ca, walther@60384: rules = rules, errpatts = errpatts, scr = sc}) rs = walther@60384: Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, erls = append_rules id_erls erls rs, walther@60384: srls = sr, calc = ca, rules = rules, errpatts = errpatts, scr = sc} walther@60384: | append_erls_rules id_erls (Rule_Def.Rrls _) _ = walther@60384: raise ERROR ("append_erls_rules: not for reverse-rewrite-rule-set " ^ id_erls); walther@60384: 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@59919: calc = union Eval_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@59919: calc = union Eval_Def.calc_eq ca1 ca2, walther@59867: rules = union Rule.equal rs1 rs2, walther@59852: errpatts = union (op =) eps1 eps2} walther@59962: | merge id _ _ = raise 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@59879: (ThyC.id * (* 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@59907: fun id_from_rule (Rule.Rls_ rls) = id rls walther@59907: | id_from_rule r = raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string r); walther@59907: walther@59914: (* check if a rule is contained in a rule-set (recursivley down in Rls_); walther@59914: this rule can even be a rule-set itself *) walther@59914: fun contains r rls = walther@59914: let walther@59914: fun (*find (_, Rls_ rls) = finds (get_rules rls) walther@59914: | find r12 = equal r12 walther@59914: and*) finds [] = false walther@59914: | finds (r1 :: rs) = if Rule.equal (r, r1) then true else finds rs walther@59914: in walther@59914: finds (get_rules rls) walther@59914: end walther@59914: 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@59907: 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(**)