1 (* isac's rewriter |
1 (* isac's rewriter |
2 (c) Walther Neuper 2000 |
2 (c) Walther Neuper 2000 |
3 |
|
4 use"ProgLang/rewrite.sml"; |
|
5 use"rewrite.sml"; |
|
6 *) |
3 *) |
7 |
4 |
|
5 signature REWRITE = |
|
6 sig |
|
7 val assoc_thm': theory -> thm' -> thm |
|
8 val assoc_thm'': theory -> thmID -> thm |
|
9 val calculate_: theory -> string * eval_fn -> term -> (term * (string * thm)) option |
|
10 val eval__true: theory -> int -> term list -> (term * term) list -> rls -> term list * bool |
|
11 val eval_listexpr_: theory -> rls -> term -> term |
|
12 val eval_true: theory -> term list -> rls -> bool |
|
13 val eval_true_: theory' -> rls -> term -> bool |
|
14 val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) -> rls -> bool -> lrd list -> term -> term -> term * term list * lrd list * bool |
|
15 val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> rls -> bool -> thm -> term -> (term * term list) option |
|
16 val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> rls -> bool -> (term * term) list -> thm -> term -> (term * term list) option |
|
17 val rewrite_set_: theory -> bool -> rls -> term -> (term * term list) option |
|
18 val rewrite_set_inst_: theory -> bool -> (term * term) list -> rls -> term -> (term * term list) option |
|
19 val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> rls -> term list -> term -> (term * term list) option |
|
20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
|
21 (* NONE *) |
|
22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
|
23 (* NONE *) |
|
24 (* probably shift up --------------- |
|
25 exception NO_REWRITE |
|
26 exception STOP_REW_SUB |
|
27 val adhoc_thm': theory' -> string * eval_fn -> cterm' -> thm' option |
|
28 val app_rev: theory -> int -> rls -> term -> term * term list * bool |
|
29 val app_sub: theory -> int -> rls -> term -> term * term list * bool |
|
30 val calculate: theory' -> string * eval_fn -> cterm' -> (string * thm') option |
|
31 val convert: 'a -> string -> string |
|
32 val convert_metaview_to_thmid: theory -> string -> thm |
|
33 val eval_true': theory' -> rls' -> term -> bool |
|
34 val get_rls_scr: rls' -> scr |
|
35 val mk_thm: theory -> string -> thm |
|
36 val mk_thm'': theory -> term -> thm |
|
37 val parse': theory' -> cterm' -> cterm' option |
|
38 val rewrite: theory' -> rew_ord' -> rls' -> bool -> thm' -> cterm' -> (string * string) option |
|
39 val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) -> rls -> bool -> thm -> term -> (term * term list) option |
|
40 val rewrite__set_: theory -> int -> bool -> (term * term) list -> rls -> term -> (term * term list) option |
|
41 val rewrite_inst: theory' -> rew_ord' -> rls' -> bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) option |
|
42 val rewrite_set: theory' -> bool -> rls' -> cterm' -> (string * string) option |
|
43 val rewrite_set_inst: theory' -> bool -> subs' -> rls' -> cterm' -> (string * string) option |
|
44 val subs'2subst: theory -> subs' -> subst |
|
45 val trace: int -> string -> unit |
|
46 val trace1: int -> string -> unit |
|
47 --------------------------------------*) |
|
48 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
|
49 end |
|
50 |
|
51 (**) |
|
52 structure Rewrite(**): REWRITE(**) = |
|
53 struct |
|
54 (**) |
8 |
55 |
9 exception NO_REWRITE; |
56 exception NO_REWRITE; |
10 exception STOP_REW_SUB; (*WN050820 quick and dirty*) |
57 exception STOP_REW_SUB; (*WN050820 quick and dirty*) |
11 |
58 |
12 fun trace i str = |
59 fun trace i str = |
397 | "add_assoc" => "add.assoc" |
444 | "add_assoc" => "add.assoc" |
398 | "mult_assoc" => "mult.assoc" |
445 | "mult_assoc" => "mult.assoc" |
399 | _ => thmid |
446 | _ => thmid |
400 in (Global_Theory.get_thm thy) thmid' end; |
447 in (Global_Theory.get_thm thy) thmid' end; |
401 |
448 |
402 (* FIXME: the other direction below is probably concerned with this fun: *) |
449 (* FIXME: the other direction below is probably concerned with this fun: |
403 thmID_of_derivation_name' @{thm add.assoc} = "assoc" (* TODO: repair this fun *); |
450 thmID_of_derivation_name' @{thm add.assoc} = "assoc" TODO: repair this fun *); |
404 |
451 |
405 fun convert thmid_to_metaview thmid = |
452 fun convert thmid_to_metaview thmid = |
406 case thmid of |
453 case thmid of |
407 "add.commute" => "add_commute" |
454 "add.commute" => "add_commute" |
408 | "mult.commute" => "mult_commute" |
455 | "mult.commute" => "mult_commute" |