8 sig |
8 sig |
9 datatype iitem = Find of cterm' list | Given of cterm' list | Relate of cterm' list |
9 datatype iitem = Find of cterm' list | Given of cterm' list | Relate of cterm' list |
10 type imodel = iitem list |
10 type imodel = iitem list |
11 type icalhd = Ctree.pos' * cterm' * imodel * Ctree.pos_ * spec |
11 type icalhd = Ctree.pos' * cterm' * imodel * Ctree.pos_ * spec |
12 val fetchErrorpatterns : Ctree.tac -> errpatID list |
12 val fetchErrorpatterns : Ctree.tac -> errpatID list |
13 val input_icalhd : Ctree.ptree -> icalhd -> Ctree.ptree * Ctree.ocalhd |
13 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd |
14 val inform : Chead.calcstate' -> string -> string * Chead.calcstate' |
14 val inform : Chead.calcstate' -> string -> string * Chead.calcstate' |
15 val find_fillpatterns : Ctree.ptree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list |
15 val find_fillpatterns : Ctree.ctree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list |
16 val is_exactly_equal : Ctree.ptree * Ctree.pos' -> string -> string * Ctree.tac |
16 val is_exactly_equal : Ctree.ctree * Ctree.pos' -> string -> string * Ctree.tac |
17 |
17 |
18 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
18 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
19 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list |
19 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list |
20 val cas_input : term -> (Ctree.ptree * Ctree.ocalhd) option |
20 val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option |
21 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c) |
21 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c) |
22 val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos') -> term -> string * Chead.calcstate' |
22 val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos') -> term -> string * Chead.calcstate' |
23 val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option |
23 val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option |
24 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) -> |
24 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) -> |
25 rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list |
25 rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list |
26 val check_error_patterns : |
26 val check_error_patterns : |
27 term * term -> |
27 term * term -> |
93 val pre = check_preconds thy prls pre mits |
93 val pre = check_preconds thy prls pre mits |
94 val ctxt = Ctree.e_ctxt (*WN110515 cas_input_ DOESNT WORK*) |
94 val ctxt = Ctree.e_ctxt (*WN110515 cas_input_ DOESNT WORK*) |
95 in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end; |
95 in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end; |
96 |
96 |
97 |
97 |
98 (* check if the input term is a CAScmd and return a ptree with a _complete_ calchead *) |
98 (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *) |
99 fun cas_input hdt = |
99 fun cas_input hdt = |
100 let |
100 let |
101 val (h, argl) = strip_comb hdt |
101 val (h, argl) = strip_comb hdt |
102 in |
102 in |
103 case assoc_cas (assoc_thy "Isac") h of |
103 case assoc_cas (assoc_thy "Isac") h of |
106 let |
106 let |
107 val dtss = argl2dtss argl |
107 val dtss = argl2dtss argl |
108 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss |
108 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss |
109 val spec = (dI, pI, mI) |
109 val spec = (dI, pI, mI) |
110 val (pt,_) = |
110 val (pt,_) = |
111 Ctree.cappend_problem Ctree.e_ptree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt) |
111 Ctree.cappend_problem Ctree.e_ctree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt) |
112 val pt = Ctree.update_spec pt [] spec |
112 val pt = Ctree.update_spec pt [] spec |
113 val pt = Ctree.update_pbl pt [] pits |
113 val pt = Ctree.update_pbl pt [] pits |
114 val pt = Ctree.update_met pt [] mits |
114 val pt = Ctree.update_met pt [] mits |
115 val pt = Ctree.update_ctxt pt [] ctxt |
115 val pt = Ctree.update_ctxt pt [] ctxt |
116 in |
116 in |