9 type calcstate' |
9 type calcstate' |
10 datatype appl = Appl of Ctree.tac_ | Notappl of string |
10 datatype appl = Appl of Ctree.tac_ | Notappl of string |
11 val nxt_specify_init_calc : Ctree.fmz -> calcstate |
11 val nxt_specify_init_calc : Ctree.fmz -> calcstate |
12 val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree -> |
12 val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree -> |
13 Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ctree |
13 Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ctree |
14 val nxt_specif : Ctree.tac -> Ctree.ctree * Ctree.pos' -> calcstate' |
14 val nxt_specif : Ctree.tac -> Ctree.state -> calcstate' |
15 val nxt_spec : Ctree.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 -> Ctree.pos_ * Ctree.tac |
16 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac |
17 |
17 |
18 val reset_calchead : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' |
18 val reset_calchead : Ctree.state -> Ctree.state |
19 val get_ocalhd : Ctree.ctree * Ctree.pos' -> Ctree.ocalhd |
19 val get_ocalhd : Ctree.state -> 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 : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' |
21 val all_modspec : Ctree.state -> Ctree.state |
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 : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' |
26 val complete_mod : Ctree.state -> Ctree.state |
27 val is_complete_mod : Ctree.ctree * Ctree.pos' -> bool |
27 val is_complete_mod : Ctree.state -> bool |
28 val complete_spec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' |
28 val complete_spec : Ctree.state -> Ctree.state |
29 val is_complete_spec : Ctree.ctree * Ctree.pos' -> bool |
29 val is_complete_spec : Ctree.state -> 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 : Ctree.ctree -> unit |
32 val show_pt : Ctree.ctree -> unit |
33 val pt_extract : Ctree.ctree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list |
33 val pt_extract : Ctree.state -> Ctree.ptform * Ctree.tac option * term list |
34 val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term) list |
34 val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (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 |