21 struct |
21 struct |
22 (**) |
22 (**) |
23 open Ctree |
23 open Ctree |
24 open Pos |
24 open Pos |
25 |
25 |
26 fun rew_info (Rule.Rls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
26 fun rew_info (Rule_Set.Rls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
27 (rew_ord', erls, ca) |
27 (rew_ord', erls, ca) |
28 | rew_info (Rule.Seq {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
28 | rew_info (Rule_Set.Seq {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
29 (rew_ord', erls, ca) |
29 (rew_ord', erls, ca) |
30 | rew_info (Rule.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
30 | rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
31 (rew_ord', erls, ca) |
31 (rew_ord', erls, ca) |
32 | rew_info rls = error ("rew_info called with '" ^ Rule.rls2str rls ^ "'"); |
32 | rew_info rls = error ("rew_info called with '" ^ Rule_Set.rls2str rls ^ "'"); |
33 |
33 |
34 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*) |
34 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*) |
35 fun from_pblobj_or_detail_thm _ p pt = |
35 fun from_pblobj_or_detail_thm _ p pt = |
36 let |
36 let |
37 val (pbl, p', rls') = parent_node pt p |
37 val (pbl, p', rls') = parent_node pt p |
60 val {calc = scr_isa_fns, ...} = Specify.get_met (get_obj g_metID pt p') |
60 val {calc = scr_isa_fns, ...} = Specify.get_met (get_obj g_metID pt p') |
61 val opt = assoc (scr_isa_fns, scrop) |
61 val opt = assoc (scr_isa_fns, scrop) |
62 in |
62 in |
63 case opt of |
63 case opt of |
64 SOME isa_fn => ("OK", thy', isa_fn) |
64 SOME isa_fn => ("OK", thy', isa_fn) |
65 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Rule.e_evalfn)) |
65 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Rule_Set.e_evalfn)) |
66 end |
66 end |
67 else |
67 else |
68 let |
68 let |
69 val thy' = get_obj g_domID pt (par_pblobj pt p); |
69 val thy' = get_obj g_domID pt (par_pblobj pt p); |
70 val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*) |
70 val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*) |
71 in |
71 in |
72 case assoc (scr_isa_fns, scrop) of |
72 case assoc (scr_isa_fns, scrop) of |
73 SOME isa_fn => ("OK",thy',isa_fn) |
73 SOME isa_fn => ("OK",thy',isa_fn) |
74 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Rule.e_evalfn)) |
74 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Rule_Set.e_evalfn)) |
75 end |
75 end |
76 end; |
76 end; |
77 |
77 |
78 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*) |
78 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*) |
79 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (Rule.e_term, []) |
79 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (Rule.e_term, []) |