7 (*Celem*) |
7 (*Celem*) |
8 type T |
8 type T |
9 val env2str: Rule.subst -> string |
9 val env2str: Rule.subst -> string |
10 val subst2str: Rule.subst -> string |
10 val subst2str: Rule.subst -> string |
11 val subst2str': Rule.subst -> string |
11 val subst2str': Rule.subst -> string |
12 val upd_env: T -> term * term -> T |
12 val update: T -> term * term -> T |
13 val upd_env': term -> term * T -> T |
13 val update': term -> term * T -> T |
14 val upd_env_opt: T -> term option * term -> T |
14 val update_opt: T -> term option * term -> T |
15 val upd_env_opt': T * (term option * term) -> T |
15 val update_opt': T * (term option * term) -> T |
16 val upd_env_opt'': ((term * T) * term option) -> T |
16 val update_opt'': ((term * T) * term option) -> T |
17 |
17 |
18 end |
18 end |
19 |
19 |
20 (**) |
20 (**) |
21 structure Env(**): ENVIRONMENT(**) = |
21 structure Env(**): ENVIRONMENT(**) = |
32 (map ( |
32 (map ( |
33 pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s; |
33 pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s; |
34 val env2str = subst2str; |
34 val env2str = subst2str; |
35 |
35 |
36 (* update environment; t <> empty if coming from listexpr *) |
36 (* update environment; t <> empty if coming from listexpr *) |
37 fun upd_env env (id, vl) = |
37 fun update env (id, vl) = |
38 let val env' = if vl = Rule.e_term then env else overwrite (env, (id, vl)); |
38 let val env' = if vl = Rule.e_term then env else overwrite (env, (id, vl)); |
39 in env' end; |
39 in env' end; |
40 fun upd_env' id (vl, env) = upd_env env (id, vl) |
40 fun update' id (vl, env) = update env (id, vl) |
41 |
41 |
42 (*WN020526: not clear, when a is available in scan_up1 for eval_true*) |
42 (*WN020526: not clear, when a is available in scan_up1 for eval_true*) |
43 (*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS |
43 (*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS |
44 curried Rewrite) for CURRENT value (which may be different from PREVIOUS); |
44 curried Rewrite) for CURRENT value (which may be different from PREVIOUS); |
45 thus "NONE" must be set at the end of currying (ill designed anyway)*) |
45 thus "NONE" must be set at the end of currying (ill designed anyway)*) |
46 fun upd_env_opt env (SOME id, vl) = upd_env env (id, vl) |
46 fun update_opt env (SOME id, vl) = update env (id, vl) |
47 | upd_env_opt env (NONE, vl) = |
47 | update_opt env (NONE, vl) = |
48 ((**)tracing ("*** upd_env_opt: (NONE," ^ Rule.term2str vl ^ ")");(**) env); |
48 ((**)tracing ("*** update_opt: (NONE," ^ Rule.term2str vl ^ ")");(**) env); |
49 fun upd_env_opt' (env, (id, vl)) = upd_env_opt env (id, vl) |
49 fun update_opt' (env, (id, vl)) = update_opt env (id, vl) |
50 fun upd_env_opt'' ((vl, env), id) = upd_env_opt env (id, vl) |
50 fun update_opt'' ((vl, env), id) = update_opt env (id, vl) |
51 |
51 |
52 |
52 |
53 (**)end(**) |
53 (**)end(**) |