equal
deleted
inserted
replaced
9 val e_taci : taci |
9 val e_taci : taci |
10 datatype pblmet = Method of Celem.metID | Problem of Celem.pblID | Upblmet |
10 datatype pblmet = Method of Celem.metID | Problem of Celem.pblID | Upblmet |
11 datatype mout = |
11 datatype mout = |
12 EmptyMout |
12 EmptyMout |
13 | Error' of string |
13 | Error' of string |
14 | FormKF of UnparseC.cterm' |
14 | FormKF of TermC.as_string |
15 | PpcKF of pblmet * Model.item Model.ppc |
15 | PpcKF of pblmet * Model.item Model.ppc |
16 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list) |
16 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list) |
17 val generate1 : Tactic.T -> Istate_Def.T * Proof.context -> Calc.T |
17 val generate1 : Tactic.T -> Istate_Def.T * Proof.context -> Calc.T |
18 -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree |
18 -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree |
19 val init_istate : Tactic.input -> term -> Istate_Def.T |
19 val init_istate : Tactic.input -> term -> Istate_Def.T |
22 val embed_deriv : taci list -> Calc.T -> Pos.pos' list * (Calc.T) (* for inform.sml *) |
22 val embed_deriv : taci list -> Calc.T -> Pos.pos' list * (Calc.T) (* for inform.sml *) |
23 val generate_hard : (* for solve.sml *) |
23 val generate_hard : (* for solve.sml *) |
24 theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree |
24 theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree |
25 val generate : (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list -> |
25 val generate : (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list -> |
26 Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos' (* for mathengine.sml *) |
26 Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos' (* for mathengine.sml *) |
27 val generate_inconsistent_rew : Selem.subs option * ThmC.thm'' -> term -> Istate_Def.T * Proof.context -> |
27 val generate_inconsistent_rew : Selem.subs option * ThmC_Def.thm'' -> term -> Istate_Def.T * Proof.context -> |
28 Pos.pos' -> Ctree.ctree -> Calc.T (* for interface.sml *) |
28 Pos.pos' -> Ctree.ctree -> Calc.T (* for interface.sml *) |
29 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
29 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
30 val tacis2str : taci list -> string |
30 val tacis2str : taci list -> string |
31 val mout2str : mout -> string |
31 val mout2str : mout -> string |
32 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
32 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
94 | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x) |
94 | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x) |
95 |
95 |
96 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*) |
96 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*) |
97 datatype foppFK = (* in DG cases div 2 *) |
97 datatype foppFK = (* in DG cases div 2 *) |
98 EmptyFoppFK (*DG internal*) |
98 EmptyFoppFK (*DG internal*) |
99 | FormFK of UnparseC.cterm' |
99 | FormFK of TermC.as_string |
100 | PpcFK of UnparseC.cterm' Model.ppc |
100 | PpcFK of TermC.as_string Model.ppc |
101 fun foppFK2str (FormFK ct') ="FormFK " ^ ct' |
101 fun foppFK2str (FormFK ct') ="FormFK " ^ ct' |
102 | foppFK2str (PpcFK ppc) ="PpcFK " ^ Model.ppc2str ppc |
102 | foppFK2str (PpcFK ppc) ="PpcFK " ^ Model.ppc2str ppc |
103 | foppFK2str EmptyFoppFK ="EmptyFoppFK" |
103 | foppFK2str EmptyFoppFK ="EmptyFoppFK" |
104 |
104 |
105 datatype nest = Open | Closed | Nundef; |
105 datatype nest = Open | Closed | Nundef; |
116 | edit2str Write = "Write" |
116 | edit2str Write = "Write" |
117 | edit2str Protect = "Protect"; |
117 | edit2str Protect = "Protect"; |
118 |
118 |
119 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*) |
119 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*) |
120 Error_ of string (*<--*) |
120 Error_ of string (*<--*) |
121 | FormKF of cellID * edit * indent * nest * UnparseC.cterm' (*<--*) |
121 | FormKF of cellID * edit * indent * nest * TermC.as_string (*<--*) |
122 | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*) |
122 | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*) |
123 | RefineKF of Stool.match list (*<--*) |
123 | RefineKF of Stool.match list (*<--*) |
124 | RefinedKF of (Celem.pblID * ((Model.itm list) * ((bool * term) list))) (*<--*) |
124 | RefinedKF of (Celem.pblID * ((Model.itm list) * ((bool * term) list))) (*<--*) |
125 |
125 |
126 (* |
126 (* |
127 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout |
127 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout |
128 *) |
128 *) |
129 datatype mout = |
129 datatype mout = |
130 FormKF of UnparseC.cterm' |
130 FormKF of TermC.as_string |
131 | PpcKF of (pblmet * Model.item Model.ppc) |
131 | PpcKF of (pblmet * Model.item Model.ppc) |
132 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list) |
132 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list) |
133 | Error' of string |
133 | Error' of string |
134 | EmptyMout |
134 | EmptyMout |
135 |
135 |