1.1 --- a/src/Tools/isac/calcelems.sml Sun Sep 29 18:48:35 2013 +0200
1.2 +++ b/src/Tools/isac/calcelems.sml Mon Sep 30 11:50:13 2013 +0200
1.3 @@ -50,6 +50,15 @@
1.4 (*. fun calculate_ fetches the evaluation-function via this list. *)
1.5 type prog_calcID = string;
1.6 type calc = (prog_calcID * cal);
1.7 +type calc_elem =
1.8 + prog_calcID * (* a simple identifier used in programs *)
1.9 + (calID * (* a long identifier used in Const *)
1.10 + eval_fn) (* an ML function *)
1.11 +fun calc_eq ((pi1, (ci1, _)) : calc_elem, (pi2, (ci2, _)) : calc_elem) =
1.12 + if pi1 = pi2
1.13 + then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
1.14 + else false
1.15 +
1.16
1.17 type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*)
1.18 type subst = (term * term) list; (*here for ets2str*)
1.19 @@ -526,37 +535,46 @@
1.20 (*id_rls checks for Rls, Seq, Rrls*)
1.21 | eq_rule _ = false;
1.22
1.23 +fun merge_ids rls1 rls2 =
1.24 + let
1.25 + val id1 = (#id o rep_rls) rls1
1.26 + val id2 = (#id o rep_rls) rls2
1.27 + in
1.28 + if id1 = id2 then id1
1.29 + else "merged_" ^ id1 ^ "_" ^ id2
1.30 + end
1.31 fun merge_rls _ Erls rls = rls
1.32 | merge_rls _ rls Erls = rls
1.33 + | merge_rls _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
1.34 + | merge_rls _ _ (Rrls x) = Rrls x
1.35 | merge_rls id
1.36 - (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.37 - rules =rs1, errpatts=eps1, scr=sc1})
1.38 - (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.39 - rules =rs2, errpatts=eps2, scr=sc2}) =
1.40 - (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.41 - rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.42 - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.43 - ((#srls o rep_rls) r2),
1.44 - calc=ca1 @ ((#calc o rep_rls) r2),
1.45 - rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.46 - errpatts = gen_union (op=) 0 (eps1, eps2),
1.47 - scr=sc1}:rls)
1.48 + (Rls {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
1.49 + rules = rs1, errpatts = eps1, scr = sc1, ...})
1.50 + (Rls {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
1.51 + rules = rs2, errpatts = eps2, ...})
1.52 + =
1.53 + (Rls {id = id, rew_ord = ro1, scr = sc1,
1.54 + preconds = union (op =) pc1 pc2,
1.55 + erls = merge_rls (merge_ids er1 er2) er1 er2,
1.56 + srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
1.57 + calc = union calc_eq ca1 ca2,
1.58 + rules = union eq_rule rs1 rs2,
1.59 + errpatts = union (op =) eps1 eps2} : rls)
1.60 | merge_rls id
1.61 - (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.62 - rules =rs1, errpatts=eps1, scr=sc1})
1.63 - (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.64 - rules =rs2, errpatts=eps2, scr=sc2}) =
1.65 - (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.66 - rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.67 - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.68 - ((#srls o rep_rls) r2),
1.69 - calc=ca1 @ ((#calc o rep_rls) r2),
1.70 - (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.71 - rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.72 - errpatts = gen_union (op=) 0 (eps1, eps2),
1.73 - scr=sc1}:rls)
1.74 - | merge_rls _ _ _ =
1.75 - error "merge_rls: not for reverse-rewrite-rule-sets and not for mixed Rls -- Seq";
1.76 + (Seq {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
1.77 + rules = rs1, errpatts = eps1, scr = sc1, ...})
1.78 + (Seq {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
1.79 + rules = rs2, errpatts = eps2, ...})
1.80 + =
1.81 + (Seq {id = id, rew_ord = ro1, scr = sc1,
1.82 + preconds = union (op =) pc1 pc2,
1.83 + erls = merge_rls (merge_ids er1 er2) er1 er2,
1.84 + srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
1.85 + calc = union calc_eq ca1 ca2,
1.86 + rules = union eq_rule rs1 rs2,
1.87 + errpatts = union (op =) eps1 eps2} : rls)
1.88 + | merge_rls id _ _ = error ("merge_rls: \"" ^ id ^
1.89 + "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Seq");
1.90
1.91 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.92 rules=rs, errpatts=eps, scr=sc}) r =
1.93 @@ -573,13 +591,24 @@
1.94 | remove_rls id (Rrls _) _ = error
1.95 ("remove_rls: not for reverse-rewrite-rule-set "^id);
1.96
1.97 -(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
1.98 -val it = [1, 2] : int list*)
1.99 +(* datastructure for KEStore_Elems, intermediate for thehier *)
1.100 +type rlss_elem =
1.101 + (rls' * (* identifier unique within Isac *)
1.102 + (theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
1.103 + rls)) (* ((#id o rep_rls) rls) = rls' by coding discipline *)
1.104 +fun rls_eq ((id1, (_, _)), (id2, (_, _))) = id1 = id2
1.105
1.106 -(*elder version: migrated 3 calls in smtest to memrls
1.107 -fun mem_rls id rls =
1.108 - case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
1.109 - SOME _ => true | NONE => false;*)
1.110 +fun insert_merge_rls (re as (id, (thyID, r1)) : rlss_elem) ys =
1.111 + case get_index (fn y => if curry rls_eq re y then SOME y else NONE) ys of
1.112 + NONE => re :: ys
1.113 + | SOME (i, (_, (_, r2))) =>
1.114 + let
1.115 + val r12 = merge_rls id r1 r2
1.116 + in list_update ys i (id, (thyID, r12)) end
1.117 +
1.118 +fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2;
1.119 +
1.120 +
1.121 fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
1.122 | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
1.123 | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));