5 *) |
5 *) |
6 signature CALC_HEAD = |
6 signature CALC_HEAD = |
7 sig |
7 sig |
8 type calcstate |
8 type calcstate |
9 type calcstate' |
9 type calcstate' |
10 datatype appl = Appl of tac_ | Notappl of string |
10 datatype appl = Appl of Ctree.tac_ | Notappl of string |
11 val nxt_specify_init_calc : fmz -> calcstate |
11 val nxt_specify_init_calc : Ctree.fmz -> calcstate |
12 val specify : tac_ -> pos' -> cid -> ptree -> |
12 val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ptree -> |
13 (posel list * pos_) * ((posel list * pos_) * istate) * Generate.mout * tac * safe * ptree |
13 Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ptree |
14 val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate' |
14 val nxt_specif : Ctree.tac -> Ctree.ptree * Ctree.pos' -> calcstate' |
15 val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list -> |
15 val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list -> |
16 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac |
16 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac |
17 |
17 |
18 val reset_calchead : ptree * pos' -> ptree * pos' |
18 val reset_calchead : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' |
19 val get_ocalhd : ptree * pos' -> ocalhd |
19 val get_ocalhd : Ctree.ptree * Ctree.pos' -> Ctree.ocalhd |
20 val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool |
20 val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool |
21 val all_modspec : ptree * pos' -> ptree * pos' |
21 val all_modspec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' |
22 |
22 |
23 val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list |
23 val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list |
24 val insert_ppc' : itm -> itm list -> itm list |
24 val insert_ppc' : itm -> itm list -> itm list |
25 |
25 |
26 val complete_mod : ptree * pos' -> ptree * pos' |
26 val complete_mod : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' |
27 val is_complete_mod : ptree * pos' -> bool |
27 val is_complete_mod : Ctree.ptree * Ctree.pos' -> bool |
28 val complete_spec : ptree * pos' -> ptree * pos' |
28 val complete_spec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' |
29 val is_complete_spec : ptree * pos' -> bool |
29 val is_complete_spec : Ctree.ptree * Ctree.pos' -> bool |
30 val some_spec : spec -> spec -> spec |
30 val some_spec : spec -> spec -> spec |
31 (* these could go to Ctree ..*) |
31 (* these could go to Ctree ..*) |
32 val show_pt : ptree -> unit |
32 val show_pt : Ctree.ptree -> unit |
33 val pt_extract : ptree * (posel list * pos_) -> ptform * tac option * term list |
33 val pt_extract : Ctree.ptree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list |
34 val get_interval : int list * pos_ -> pos' -> int -> ptree -> (pos' * term) list |
34 val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ptree -> (Ctree.pos' * term) list |
35 |
35 |
36 val match_ags : theory -> pat list -> term list -> ori list |
36 val match_ags : theory -> pat list -> term list -> ori list |
37 val match_ags_msg : pblID -> term -> term list -> unit |
37 val match_ags_msg : pblID -> term -> term list -> unit |
38 val oris2fmz_vals : ori list -> string list * term list |
38 val oris2fmz_vals : ori list -> string list * term list |
39 val vars_of_pbl_' : ('a * ('b * term)) list -> term list |
39 val vars_of_pbl_' : ('a * ('b * term)) list -> term list |
54 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
54 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
55 end |
55 end |
56 |
56 |
57 structure Chead(**): CALC_HEAD(**) = |
57 structure Chead(**): CALC_HEAD(**) = |
58 struct |
58 struct |
59 |
59 open Ctree |
60 (* datatypes *) |
60 (* datatypes *) |
61 |
61 |
62 (* the state wich is stored after each step of calculation; it contains |
62 (* the state wich is stored after each step of calculation; it contains |
63 the calc-state and a list of [tac,istate](="tacis") to be applied next. |
63 the calc-state and a list of [tac,istate](="tacis") to be applied next. |
64 the last_elem tacis is the first to apply to the calc-state and |
64 the last_elem tacis is the first to apply to the calc-state and |