1.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed Dec 21 11:27:22 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Thu Dec 22 10:25:49 2016 +0100
1.3 @@ -9,30 +9,32 @@
1.4 signature MATH_ENGINE =
1.5 sig
1.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
1.7 - val me : Solve.tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Generate.mout * Solve.tac'_ * safe * ptree
1.8 + val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ptree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ptree
1.9 val autocalc :
1.10 - pos' list -> pos' -> (ptree * pos') * Generate.taci list -> Solve.auto -> string * pos' list * (ptree * pos')
1.11 + Ctree.pos' list -> Ctree.pos' -> (Ctree.ptree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ptree * Ctree.pos')
1.12 val locatetac :
1.13 - tac -> ptree * (posel list * pos_) -> string * (Generate.taci list * pos' list * (ptree * pos'))
1.14 - val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
1.15 + Ctree.tac -> Ctree.ptree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos'))
1.16 + val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
1.17 val detailstep :
1.18 - ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
1.19 + Ctree.ptree -> Ctree.pos' -> string * Ctree.ptree * Ctree.pos'
1.20 + val get_pblID : Ctree.ptree * Ctree.pos' -> pblID option
1.21
1.22 - val initcontext_met : ptree -> pos' -> bool * string list * scr * itm list * (bool * term) list
1.23 - val initcontext_pbl : ptree -> pos' -> bool * string list * term * itm list * (bool * term) list
1.24 - val context_met : metID -> ptree -> pos -> bool * metID * scr * itm list * (bool * term) list
1.25 - val context_pbl : pblID -> ptree -> pos -> bool * pblID * term * itm list * (bool * term) list
1.26 - val set_method : metID -> ptree * pos' -> ptree * ocalhd
1.27 - val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
1.28 - val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
1.29 - val tryrefine : pblID -> ptree -> pos' -> bool * pblID * term * itm list * (bool * term) list
1.30 + val initcontext_met : Ctree.ptree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list
1.31 + val initcontext_pbl : Ctree.ptree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list
1.32 + val context_met : metID -> Ctree.ptree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list
1.33 + val context_pbl : pblID -> Ctree.ptree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list
1.34 + val set_method : metID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
1.35 + val set_problem : pblID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
1.36 + val set_theory : thyID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
1.37 + val tryrefine : pblID -> Ctree.ptree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list
1.38
1.39 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.40 type nxt_
1.41 type lOc_
1.42 - val CalcTreeTEST : fmz list -> pos' * NEW * Generate.mout * (string * tac) * safe * ptree
1.43 + val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ptree
1.44 val f2str : Generate.mout -> cterm'
1.45 - val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_
1.46 + val loc_solve_ : string * Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_
1.47 + val loc_specify_ : Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_
1.48 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.49 end
1.50
1.51 @@ -41,10 +43,10 @@
1.52 struct
1.53 (**)
1.54
1.55 -fun get_pblID (pt, (p, _):pos') =
1.56 - let val p' = par_pblobj pt p
1.57 - val (_, pI, _) = get_obj g_spec pt p'
1.58 - val (_, (_, oI, _), _) = get_obj g_origin pt p'
1.59 +fun get_pblID (pt, (p, _): Ctree.pos') =
1.60 + let val p' = Ctree.par_pblobj pt p
1.61 + val (_, pI, _) = Ctree.get_obj Ctree.g_spec pt p'
1.62 + val (_, (_, oI, _), _) = Ctree.get_obj Ctree.g_origin pt p'
1.63 in
1.64 if pI <> e_pblID
1.65 then SOME pI
1.66 @@ -52,7 +54,7 @@
1.67 if oI <> e_pblID then SOME oI else NONE end;
1.68
1.69 (* introduced for test only *)
1.70 -val e_tac_ = Tac_ (Pure.thy, "", "", "");
1.71 +val e_tac_ = Ctree.Tac_ (Pure.thy, "", "", "");
1.72 datatype lOc_ =
1.73 ERror of string (*after loc_specify, loc_solve*)
1.74 | UNsafe of Chead.calcstate' (*after loc_specify, loc_solve*)
1.75 @@ -96,7 +98,7 @@
1.76 (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
1.77 | UNsafe cs' => ("unsafe-ok", cs')
1.78 | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
1.79 - (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
1.80 + (if p' = ([], Ctree.Res) then "end-of-calculation" else "ok", cs')
1.81 (*for SEVER.tacs user to ask ? *)
1.82 end
1.83 end
1.84 @@ -106,16 +108,16 @@
1.85 fun nxt_specify_ (ptp as (pt, (p, p_))) =
1.86 let
1.87 val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
1.88 - case get_obj I pt p of
1.89 - pblobj as (PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
1.90 + case Ctree.get_obj I pt p of
1.91 + pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
1.92 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
1.93 - | PrfObj _ => error "nxt_specify_: not on PrfObj"
1.94 + | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj"
1.95 in
1.96 - if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
1.97 + if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin
1.98 then
1.99 case mI' of
1.100 - ["no_met"] => Chead.nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
1.101 - | _ => Chead.nxt_specif Model_Problem (pt, (p,Pbl))
1.102 + ["no_met"] => Chead.nxt_specif (Ctree.Refine_Tacitly pI') (pt, (p, Ctree.Pbl))
1.103 + | _ => Chead.nxt_specif Ctree.Model_Problem (pt, (p, Ctree.Pbl))
1.104 else
1.105 let
1.106 val cpI = if pI = e_pblID then pI' else pI;
1.107 @@ -128,67 +130,67 @@
1.108 Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
1.109 in
1.110 case tac of
1.111 - Apply_Method mI =>
1.112 - Solve.nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.113 + Ctree.Apply_Method mI =>
1.114 + Solve.nxt_solv (Ctree.Apply_Method' (mI, NONE, Ctree.e_istate, Ctree.e_ctxt)) (Ctree.e_istate, Ctree.e_ctxt) ptp
1.115 | _ => Chead.nxt_specif tac ptp
1.116 end
1.117 end
1.118
1.119 (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
1.120 -fun set_method (mI:metID) ptp =
1.121 +fun set_method mI ptp =
1.122 let
1.123 val (mits, pt, p) =
1.124 - case Chead.nxt_specif (Specify_Method mI) ptp of
1.125 - ([(_, Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p)
1.126 + case Chead.nxt_specif (Ctree.Specify_Method mI) ptp of
1.127 + ([(_, Ctree.Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p)
1.128 | _ => error "set_method: case 1 uncovered"
1.129 val pre = [] (*...from Specify_Method'*)
1.130 val complete = true (*...from Specify_Method'*)
1.131 (*from Specify_Method' ? vvv, vvv ?*)
1.132 val (hdf, spec) =
1.133 - case get_obj I pt p of
1.134 - PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
1.135 - | PrfObj _ => error "set_method: case 2 uncovered"
1.136 + case Ctree.get_obj I pt p of
1.137 + Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
1.138 + | Ctree.PrfObj _ => error "set_method: case 2 uncovered"
1.139 in
1.140 - (pt, (complete, Met, hdf, mits, pre, spec) : ocalhd)
1.141 + (pt, (complete, Ctree.Met, hdf, mits, pre, spec) : Ctree.ocalhd)
1.142 end
1.143
1.144 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
1.145 -fun set_problem pI (ptp: ptree * pos') =
1.146 +fun set_problem pI ptp =
1.147 let
1.148 val (complete, pits, pre, pt, p) =
1.149 - case Chead.nxt_specif (Specify_Problem pI) ptp of
1.150 - ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
1.151 + case Chead.nxt_specif (Ctree.Specify_Problem pI) ptp of
1.152 + ([(_, Ctree.Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
1.153 => (complete, pits, pre, pt, p)
1.154 | _ => error "set_problem: case 1 uncovered"
1.155 (*from Specify_Problem' ? vvv, vvv ?*)
1.156 val (hdf, spec) =
1.157 - case get_obj I pt p of
1.158 - PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
1.159 - | PrfObj _ => error "set_problem: case 2 uncovered"
1.160 + case Ctree.get_obj I pt p of
1.161 + Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
1.162 + | Ctree.PrfObj _ => error "set_problem: case 2 uncovered"
1.163 in
1.164 - (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd)
1.165 + (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd)
1.166 end
1.167
1.168 -fun set_theory (tI:thyID) (ptp: ptree * pos') =
1.169 +fun set_theory tI ptp =
1.170 let
1.171 val (complete, pits, pre, pt, p) =
1.172 - case Chead.nxt_specif (Specify_Theory tI) ptp of
1.173 - ([(_, Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
1.174 + case Chead.nxt_specif (Ctree.Specify_Theory tI) ptp of
1.175 + ([(_, Ctree.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
1.176 => (complete, pits, pre, pt, p)
1.177 | _ => error "set_theory: case 1 uncovered"
1.178 (*from Specify_Theory' ? vvv, vvv ?*)
1.179 val (hdf, spec) =
1.180 - case get_obj I pt p of
1.181 - PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
1.182 - | PrfObj _ => error "set_theory: case 2 uncovered"
1.183 - in (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd) end;
1.184 + case Ctree.get_obj I pt p of
1.185 + Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
1.186 + | Ctree.PrfObj _ => error "set_theory: case 2 uncovered"
1.187 + in (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd) end;
1.188
1.189 (* does a step forward; returns tactic used, ctree updated.
1.190 TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
1.191 -fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis): Chead.calcstate) =
1.192 +fun step (ip as (_, p_)) (ptp as (pt,p), tacis) =
1.193 let val pIopt = get_pblID (pt,ip);
1.194 in
1.195 - if ip = ([],Res)
1.196 + if ip = ([], Ctree.Res)
1.197 then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate')
1.198 else
1.199 case tacis of
1.200 @@ -197,7 +199,7 @@
1.201 then
1.202 let val (pt',c',p') = Generate.generate tacis (pt,[],p)
1.203 in ("ok", (tacis, c', (pt', p'))) end
1.204 - else (case (if member op = [Pbl, Met] p_
1.205 + else (case (if member op = [Ctree.Pbl, Ctree.Met] p_
1.206 then nxt_specify_ (pt, ip) else Solve.nxt_solve_ (pt, ip))
1.207 handle ERROR msg => (writeln ("*** " ^ msg);
1.208 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
1.209 @@ -206,7 +208,7 @@
1.210 | _ => (case pIopt of
1.211 NONE => ("no-fmz-spec", ([], [], ptp))
1.212 | SOME _ => (*vvvvvv: Apply_Method without init_form*)
1.213 - (case if member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
1.214 + (case if member op = [Ctree.Pbl, Ctree.Met] p_ andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p))
1.215 then nxt_specify_ (pt, ip)
1.216 else (Solve.nxt_solve_ (pt,ip))
1.217 handle ERROR msg => (writeln ("*** " ^ msg);
1.218 @@ -234,12 +236,12 @@
1.219 else (str, c@c', ptp) end
1.220 (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
1.221 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
1.222 - if Solve.autoord auto > 3 andalso just_created (pt, pos)
1.223 + if Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos)
1.224 then
1.225 let val ptp = Chead.all_modspec (pt, pos);
1.226 in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
1.227 else
1.228 - if member op = [Pbl, Met] p_
1.229 + if member op = [Ctree.Pbl, Ctree.Met] p_
1.230 then
1.231 if not (Chead.is_complete_mod (pt, pos))
1.232 then
1.233 @@ -271,10 +273,10 @@
1.234 fun initcontext_pbl pt (p, _) =
1.235 let
1.236 val (probl, os, pI, hdl, pI') =
1.237 - case get_obj I pt p of
1.238 - PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
1.239 + case Ctree.get_obj I pt p of
1.240 + Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
1.241 => (probl, os, pI, hdl, pI')
1.242 - | PrfObj _ => error "initcontext_pbl: uncovered case"
1.243 + | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case"
1.244 val pblID =
1.245 if pI' = e_pblID
1.246 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
1.247 @@ -288,9 +290,9 @@
1.248 fun initcontext_met pt (p,_) =
1.249 let
1.250 val (meth, os, mI, mI') =
1.251 - case get_obj I pt p of
1.252 - PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
1.253 - | PrfObj _ => error "initcontext_met: uncovered case"
1.254 + case Ctree.get_obj I pt p of
1.255 + Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
1.256 + | Ctree.PrfObj _ => error "initcontext_met: uncovered case"
1.257 val metID = if mI' = e_metID
1.258 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
1.259 else mI'
1.260 @@ -301,24 +303,24 @@
1.261 end
1.262
1.263 (* match the model of a problem at pos p with the model-pattern of the problem with pblID *)
1.264 -fun context_pbl pI pt (p:pos) =
1.265 +fun context_pbl pI pt p =
1.266 let
1.267 val (probl, os, hdl) =
1.268 - case get_obj I pt p of
1.269 - PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
1.270 - | PrfObj _ => error "context_pbl: uncovered case"
1.271 + case Ctree.get_obj I pt p of
1.272 + Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
1.273 + | Ctree.PrfObj _ => error "context_pbl: uncovered case"
1.274 val {ppc,where_,prls,...} = Specify.get_pbt pI
1.275 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
1.276 in
1.277 (model_ok, pI, hdl, pbl, pre)
1.278 end
1.279
1.280 -fun context_met mI pt (p:pos) =
1.281 +fun context_met mI pt p =
1.282 let
1.283 val (meth, os) =
1.284 - case get_obj I pt p of
1.285 - PblObj {meth, origin = (os, _, _),...} => (meth, os)
1.286 - | PrfObj _ => error "context_met: uncovered case"
1.287 + case Ctree.get_obj I pt p of
1.288 + Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
1.289 + | Ctree.PrfObj _ => error "context_met: uncovered case"
1.290 val {ppc,pre,prls,scr,...} = Specify.get_met mI
1.291 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
1.292 in
1.293 @@ -328,9 +330,9 @@
1.294 fun tryrefine pI pt (p,_) =
1.295 let
1.296 val (probl, os, hdl) =
1.297 - case get_obj I pt p of
1.298 - PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
1.299 - | PrfObj _ => error "context_met: uncovered case"
1.300 + case Ctree.get_obj I pt p of
1.301 + Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
1.302 + | Ctree.PrfObj _ => error "context_met: uncovered case"
1.303 in
1.304 case Specify.refine_pbl (assoc_thy "Isac") pI probl of
1.305 NONE => (*copy from context_pbl*)
1.306 @@ -343,17 +345,17 @@
1.307 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)
1.308 end
1.309
1.310 -fun detailstep pt (pos as (p, _):pos') =
1.311 +fun detailstep pt (pos as (p, _)) =
1.312 let
1.313 - val nd = get_nd pt p
1.314 - val cn = children nd
1.315 + val nd = Ctree.get_nd pt p
1.316 + val cn = Ctree.children nd
1.317 in
1.318 if null cn
1.319 then
1.320 - if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
1.321 + if (Ctree.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)]
1.322 then Solve.detailrls pt pos
1.323 - else ("no-Rewrite_Set...", EmptyPtree, e_pos')
1.324 - else ("donesteps", pt, (p @ [length (children (get_nd pt p))], Res))
1.325 + else ("no-Rewrite_Set...", Ctree.EmptyPtree, Ctree.e_pos')
1.326 + else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res))
1.327 end;
1.328
1.329
1.330 @@ -368,8 +370,8 @@
1.331 val (form, _, _) = Chead.pt_extract ptp
1.332 in
1.333 case form of
1.334 - Form t => Generate.FormKF (term2str t)
1.335 - | ModSpec (_, p_, _, gfr, pre, _) =>
1.336 + Ctree.Form t => Generate.FormKF (term2str t)
1.337 + | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
1.338 Generate.PpcKF (
1.339 (case p_ of Pbl => Generate.Problem [] | Met => Generate.Method []
1.340 | _ => error "TESTg_form: uncovered case",
1.341 @@ -381,9 +383,9 @@
1.342 fun CalcTreeTEST [(fmz, sp)] =
1.343 let
1.344 val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
1.345 - val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
1.346 + val tac = case tacis of [] => Ctree.Empty_Tac | _ => (#1 o hd) tacis
1.347 val f = TESTg_form (pt,p)
1.348 - in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end
1.349 + in (p, []:NEW, f, (Ctree.tac2IDstr tac, tac), Ctree.Sundef, pt) end
1.350 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
1.351
1.352 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
1.353 @@ -406,7 +408,7 @@
1.354 | ("failure", _) => error "sys-error"
1.355 | _ => error "me: uncovered case"
1.356 val (_, ts) =
1.357 - (case step p ((pt, e_pos'),[]) of
1.358 + (case step p ((pt, Ctree.e_pos'),[]) of
1.359 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
1.360 | ("helpless", _) => ("helpless: cannot propose tac", [])
1.361 | ("no-fmz-spec", _) => error "no-fmz-spec"
1.362 @@ -416,9 +418,9 @@
1.363 val tac =
1.364 case ts of
1.365 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
1.366 - | _ => if p = ([], Res) then End_Proof' else Empty_Tac;
1.367 + | _ => if p = ([], Ctree.Res) then Ctree.End_Proof' else Ctree.Empty_Tac;
1.368 in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
1.369 - (tac2IDstr tac, tac): Solve.tac'_, Sundef, pt)
1.370 + (Ctree.tac2IDstr tac, tac), Ctree.Sundef, pt)
1.371 end
1.372
1.373 (* for quick test-print-out, until 'type inout' is removed *)