1.1 --- a/src/Tools/isac/Frontend/interface.sml Wed Nov 30 13:05:08 2016 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon Dec 12 18:08:13 2016 +0100
1.3 @@ -98,7 +98,7 @@
1.4 compare "fun CalcTreeTEST" which does NOT decode.*)
1.5 fun CalcTree [(fmz, sp) : fmz] (*for several variants lateron*) =
1.6 ((let
1.7 - val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))
1.8 + val cs = Chead.nxt_specify_init_calc (encode_fmz (fmz, sp))
1.9 val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)
1.10 in calctreeOK2xml cI end)
1.11 handle _ => sysERROR2xml 0 "error in kernel 2")
1.12 @@ -188,7 +188,7 @@
1.13 fun getTactic cI (p:pos') =
1.14 (let
1.15 val ((pt, _), _) = get_calc cI
1.16 - val (_, tac, _) = pt_extract (pt, p)
1.17 + val (_, tac, _) = Chead.pt_extract (pt, p)
1.18 in
1.19 case tac of
1.20 SOME ta => gettacticOK2xml cI ta
1.21 @@ -213,7 +213,7 @@
1.22 fun getAssumptions cI (p:pos') =
1.23 (let
1.24 val ((pt, _), _) = get_calc cI
1.25 - val (_, _, asms) = pt_extract (pt, p)
1.26 + val (_, _, asms) = Chead.pt_extract (pt, p)
1.27 in getasmsOK2xml cI asms end)
1.28 handle _ => sysERROR2xml cI "syserror in getAssumptions"
1.29
1.30 @@ -228,7 +228,7 @@
1.31 fun refFormula cI (p: pos') = (*WN0501 rename to "fun getElement" !*)
1.32 (let
1.33 val ((pt, _), _) = get_calc cI
1.34 - val (form, _, _) = pt_extract (pt, p)
1.35 + val (form, _, _) = Chead.pt_extract (pt, p)
1.36 in refformulaOK2xml cI p form end)
1.37 handle _ => sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^ " " ^ pos'2str p)
1.38
1.39 @@ -239,7 +239,7 @@
1.40 fun getFormulaeFromTo cI (([], Pbl) : pos') (to as ([], Pbl) : pos') _ false =
1.41 ((let
1.42 val ((pt,_),_) = get_calc cI
1.43 - val (ModSpec (_, _, headline, _, _, _), _, _) = pt_extract (pt, to)
1.44 + val (ModSpec (_, _, headline, _, _, _), _, _) = Chead.pt_extract (pt, to)
1.45 in getintervalOK cI [(to, headline)] end)
1.46 handle _ => sysERROR2xml cI "error in kernel 7")
1.47 | getFormulaeFromTo cI ([], Pbl) ([], Met) _ false =
1.48 @@ -258,7 +258,7 @@
1.49 val f = move_dn [] pt from
1.50 fun max (a,b) = if a < b then b else a
1.51 val lev = max (level, max (lev_of from, lev_of to)) (*... must reach margins *)
1.52 - in getintervalOK cI (get_interval f to lev pt) end)
1.53 + in getintervalOK cI (Chead.get_interval f to lev pt) end)
1.54 handle _ => sysERROR2xml cI "error in getFormulaeFromTo")
1.55 | getFormulaeFromTo cI from to level true =
1.56 sysERROR2xml cI ("getFormulaeFromTo impl.for formulae only, " ^
1.57 @@ -293,17 +293,17 @@
1.58 fun resetCalcHead cI =
1.59 (let
1.60 val (ptp,_) = get_calc cI
1.61 - val ptp = reset_calchead ptp
1.62 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
1.63 + val ptp = Chead.reset_calchead ptp
1.64 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Chead.get_ocalhd ptp)) end)
1.65 handle _ => sysERROR2xml cI "error in kernel 10";
1.66
1.67 (* at the activeFormula insert all the Descriptions in the Model and return a CalcHead;
1.68 the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)
1.69 fun modelProblem cI =
1.70 (let val (ptp, _) = get_calc cI
1.71 - val ptp = reset_calchead ptp
1.72 - val (_, _, ptp) = nxt_specif Model_Problem ptp
1.73 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
1.74 + val ptp = Chead.reset_calchead ptp
1.75 + val (_, _, ptp) = Chead.nxt_specif Model_Problem ptp
1.76 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Chead.get_ocalhd ptp)) end)
1.77 handle _ => sysERROR2xml cI "error in kernel 11";
1.78
1.79 (* set the UContext determined on a knowledgebrowser to the current calc
1.80 @@ -338,8 +338,8 @@
1.81 | ("failure", _) => sysERROR2xml cI "failure"
1.82 | ("not-applicable", _) => (*the rule comes from anywhere..*)
1.83 (case applicable_in ip pt tac of
1.84 - Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")
1.85 - | Appl m =>
1.86 + Chead.Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")
1.87 + | Chead.Appl m =>
1.88 let
1.89 val ctxt = get_ctxt pt pold
1.90 val (p, c, _, pt) =
1.91 @@ -459,7 +459,7 @@
1.92 val ((pt, _), _) = get_calc cI
1.93 val p = get_pos cI 1
1.94 in
1.95 - case Inform.inform (([], [], (pt, p)): calcstate') (encode ifo) of
1.96 + case Inform.inform (([], [], (pt, p)): Chead.calcstate') (encode ifo) of
1.97 ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
1.98 let
1.99 val unc = if null (fst p) then p else move_up [] pt p
2.1 --- a/src/Tools/isac/Frontend/states.sml Wed Nov 30 13:05:08 2016 +0100
2.2 +++ b/src/Tools/isac/Frontend/states.sml Mon Dec 12 18:08:13 2016 +0100
2.3 @@ -141,7 +141,7 @@
2.4 (* holds calculations; these are read/updated from the java-frontend at each interaction*)
2.5 val states = Synchronized.var "isac_states" ([] :
2.6 (calcID * (* the id unique for a calculation *)
2.7 - (calcstate * (* the interpreter state *)
2.8 + (Chead.calcstate * (* the interpreter state *)
2.9 (iterID * (* 1 sets the 'active formula': a calc. can have several visitors*)
2.10 pos' (* for iterator of a user *)
2.11 (* TODO iterID * pos' should go to java-frontend *)
2.12 @@ -184,7 +184,7 @@
2.13 *)
2.14 (* add users to a calcstate *)
2.15 fun get_iterID (cI:calcID)
2.16 - (p:(calcID * (calcstate * (iterID * pos') list)) list) =
2.17 + (p:(calcID * (Chead.calcstate * (iterID * pos') list)) list) =
2.18 case assoc (p, cI) of
2.19 NONE => error ("get_iterID: no iterID " ^ (string_of_int cI))
2.20 | SOME (_, us) => (new_key us 1):iterID;
2.21 @@ -363,7 +363,7 @@
2.22
2.23 (* here is the _only_ critical section on states,
2.24 because a single calculation (with _one_ cI) is sequential *)
2.25 -fun add_calc (cs:calcstate) = Synchronized.change_result states
2.26 +fun add_calc (cs: Chead.calcstate) = Synchronized.change_result states
2.27 (fn s =>
2.28 let val new_cI = new_key s 1
2.29 in (new_cI:calcID, s @ [(new_cI, (cs, []))]) end);
3.1 --- a/src/Tools/isac/Interpret/appl.sml Wed Nov 30 13:05:08 2016 +0100
3.2 +++ b/src/Tools/isac/Interpret/appl.sml Mon Dec 12 18:08:13 2016 +0100
3.3 @@ -216,35 +216,35 @@
3.4 tests for applicability are so expensive, that results (rewrites!)
3.5 are kept in the return-value of 'type tac_'.
3.6 .*)
3.7 -fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = Appl (Init_Proof' (ct', spec))
3.8 +fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = Chead.Appl (Init_Proof' (ct', spec))
3.9
3.10 | applicable_in (p,p_) pt Model_Problem =
3.11 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.12 - then Notappl ((tac2str Model_Problem) ^ " not for pos " ^ (pos'2str (p,p_)))
3.13 + then Chead.Notappl ((tac2str Model_Problem) ^ " not for pos " ^ (pos'2str (p,p_)))
3.14 else
3.15 let
3.16 val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
3.17 val {ppc,...} = get_pbt pI'
3.18 val pbl = init_pbl ppc
3.19 - in Appl (Model_Problem' (pI', pbl, [])) end
3.20 + in Chead.Appl (Model_Problem' (pI', pbl, [])) end
3.21
3.22 | applicable_in (p,p_) pt (Refine_Tacitly pI) =
3.23 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.24 - then Notappl ((tac2str (Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p,p_)))
3.25 + then Chead.Notappl ((tac2str (Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p,p_)))
3.26 else
3.27 let
3.28 val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
3.29 val opt = refine_ori oris pI;
3.30 in case opt of
3.31 SOME pblID =>
3.32 - Appl (Refine_Tacitly' (pI, pblID,
3.33 + Chead.Appl (Refine_Tacitly' (pI, pblID,
3.34 e_domID, e_metID, [](*filled in specify*)))
3.35 - | NONE => Notappl ((tac2str (Refine_Tacitly pI)) ^ " not applicable")
3.36 + | NONE => Chead.Notappl ((tac2str (Refine_Tacitly pI)) ^ " not applicable")
3.37 end
3.38
3.39 | applicable_in (p,p_) pt (Refine_Problem pI) =
3.40 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.41 - then Notappl ((tac2str (Refine_Problem pI))^
3.42 + then Chead.Notappl ((tac2str (Refine_Problem pI))^
3.43 " not for pos "^(pos'2str (p,p_)))
3.44 else
3.45 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
3.46 @@ -252,65 +252,65 @@
3.47 val thy = if dI' = e_domID then dI else dI';
3.48 val rfopt = refine_pbl (assoc_thy thy) pI itms;
3.49 in case rfopt of
3.50 - NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable")
3.51 + NONE => Chead.Notappl ((tac2str (Refine_Problem pI))^" not applicable")
3.52 | SOME (rf as (pI',_)) =>
3.53 (* val SOME (rf as (pI',_)) = rfopt;
3.54 *)
3.55 if pI' = pI
3.56 - then Notappl ((tac2str (Refine_Problem pI))^" not applicable")
3.57 - else Appl (Refine_Problem' rf)
3.58 + then Chead.Notappl ((tac2str (Refine_Problem pI))^" not applicable")
3.59 + else Chead.Appl (Refine_Problem' rf)
3.60 end
3.61
3.62 (*the specify-tacs have cterm' instead term:
3.63 parse+error here!!!: see appl_add*)
3.64 | applicable_in (p,p_) pt (Add_Given ct') =
3.65 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.66 - then Notappl ((tac2str (Add_Given ct'))^
3.67 + then Chead.Notappl ((tac2str (Add_Given ct'))^
3.68 " not for pos "^(pos'2str (p,p_)))
3.69 - else Appl (Add_Given' (ct', [(*filled in specify_additem*)]))
3.70 + else Chead.Appl (Add_Given' (ct', [(*filled in specify_additem*)]))
3.71 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
3.72
3.73 | applicable_in (p,p_) pt (Del_Given ct') =
3.74 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.75 - then Notappl ((tac2str (Del_Given ct'))^
3.76 + then Chead.Notappl ((tac2str (Del_Given ct'))^
3.77 " not for pos "^(pos'2str (p,p_)))
3.78 - else Appl (Del_Given' ct')
3.79 + else Chead.Appl (Del_Given' ct')
3.80
3.81 | applicable_in (p,p_) pt (Add_Find ct') =
3.82 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.83 - then Notappl ((tac2str (Add_Find ct'))^
3.84 + then Chead.Notappl ((tac2str (Add_Find ct'))^
3.85 " not for pos "^(pos'2str (p,p_)))
3.86 - else Appl (Add_Find' (ct', [(*filled in specify_additem*)]))
3.87 + else Chead.Appl (Add_Find' (ct', [(*filled in specify_additem*)]))
3.88
3.89 | applicable_in (p,p_) pt (Del_Find ct') =
3.90 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.91 - then Notappl ((tac2str (Del_Find ct'))^
3.92 + then Chead.Notappl ((tac2str (Del_Find ct'))^
3.93 " not for pos "^(pos'2str (p,p_)))
3.94 - else Appl (Del_Find' ct')
3.95 + else Chead.Appl (Del_Find' ct')
3.96
3.97 | applicable_in (p,p_) pt (Add_Relation ct') =
3.98 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.99 - then Notappl ((tac2str (Add_Relation ct'))^
3.100 + then Chead.Notappl ((tac2str (Add_Relation ct'))^
3.101 " not for pos "^(pos'2str (p,p_)))
3.102 - else Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))
3.103 + else Chead.Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))
3.104
3.105 | applicable_in (p,p_) pt (Del_Relation ct') =
3.106 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.107 - then Notappl ((tac2str (Del_Relation ct'))^
3.108 + then Chead.Notappl ((tac2str (Del_Relation ct'))^
3.109 " not for pos "^(pos'2str (p,p_)))
3.110 - else Appl (Del_Relation' ct')
3.111 + else Chead.Appl (Del_Relation' ct')
3.112
3.113 | applicable_in (p,p_) pt (Specify_Theory dI) =
3.114 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.115 - then Notappl ((tac2str (Specify_Theory dI))^
3.116 + then Chead.Notappl ((tac2str (Specify_Theory dI))^
3.117 " not for pos "^(pos'2str (p,p_)))
3.118 - else Appl (Specify_Theory' dI)
3.119 + else Chead.Appl (Specify_Theory' dI)
3.120 (* val (p,p_) = p; val Specify_Problem pID = m;
3.121 val Specify_Problem pID = m;
3.122 *)
3.123 | applicable_in (p,p_) pt (Specify_Problem pID) =
3.124 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.125 - then Notappl ((tac2str (Specify_Problem pID))^
3.126 + then Chead.Notappl ((tac2str (Specify_Problem pID))^
3.127 " not for pos "^(pos'2str (p,p_)))
3.128 else
3.129 let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_),
3.130 @@ -320,19 +320,19 @@
3.131 val pbl = if pI'=e_pblID andalso pI=e_pblID
3.132 then (false, (init_pbl ppc, []))
3.133 else match_itms_oris thy itms (ppc,where_,prls) oris;
3.134 - in Appl (Specify_Problem' (pID, pbl)) end
3.135 + in Chead.Appl (Specify_Problem' (pID, pbl)) end
3.136 (* val Specify_Method mID = nxt; val (p,p_) = p;
3.137 *)
3.138 | applicable_in (p,p_) pt (Specify_Method mID) =
3.139 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.140 - then Notappl ((tac2str (Specify_Method mID))^
3.141 + then Chead.Notappl ((tac2str (Specify_Method mID))^
3.142 " not for pos "^(pos'2str (p,p_)))
3.143 - else Appl (Specify_Method' (mID,[(*filled in specify*)],
3.144 + else Chead.Appl (Specify_Method' (mID,[(*filled in specify*)],
3.145 [(*filled in specify*)]))
3.146
3.147 | applicable_in (p,p_) pt (Apply_Method mI) =
3.148 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
3.149 - then Notappl ((tac2str (Apply_Method mI)) ^ " not for pos " ^ (pos'2str (p,p_)))
3.150 + then Chead.Notappl ((tac2str (Apply_Method mI)) ^ " not for pos " ^ (pos'2str (p,p_)))
3.151 else
3.152 let
3.153 val (PblObj{origin = (_, (dI, pI, _), _), probl, ctxt, ...}) = get_obj I pt p;
3.154 @@ -343,23 +343,23 @@
3.155 then assoc_thy dI |> Proof_Context.init_global |> insert_assumptions pres
3.156 else ctxt
3.157 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
3.158 - and then decide on Notappl/Appl accordingly once more.
3.159 + and then decide on Chead.Notappl/Appl accordingly once more.
3.160 Implement after all tests are running, since this changes
3.161 overall system behavior*)
3.162 - in Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
3.163 + in Chead.Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
3.164
3.165 | applicable_in (p,p_) pt (Check_Postcond pI) =
3.166 if member op = [Pbl,Met] p_
3.167 - then Notappl ((tac2str (Check_Postcond pI)) ^ " not for pos "^(pos'2str (p,p_)))
3.168 - else Appl (Check_Postcond' (pI, (e_term, [(*fun solve assignes the returnvalue of scr*)])))
3.169 + then Chead.Notappl ((tac2str (Check_Postcond pI)) ^ " not for pos "^(pos'2str (p,p_)))
3.170 + else Chead.Appl (Check_Postcond' (pI, (e_term, [(*fun solve assignes the returnvalue of scr*)])))
3.171
3.172 (*these are always applicable*)
3.173 - | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
3.174 - | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
3.175 + | applicable_in (p,p_) _ (Take str) = Chead.Appl (Take' (str2term str))
3.176 + | applicable_in (p,p_) _ (Free_Solve) = Chead.Appl (Free_Solve')
3.177
3.178 | applicable_in (p, p_) pt (m as Rewrite_Inst (subs, thm'')) =
3.179 if member op = [Pbl, Met] p_
3.180 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.181 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.182 else
3.183 let
3.184 val pp = par_pblobj pt p;
3.185 @@ -376,15 +376,15 @@
3.186 val subs' = subst2subs' subst;
3.187 in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (snd thm'') f of
3.188 SOME (f',asm) =>
3.189 - Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
3.190 - | NONE => Notappl ((fst thm'')^" not applicable")
3.191 + Chead.Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
3.192 + | NONE => Chead.Notappl ((fst thm'')^" not applicable")
3.193 end
3.194 - handle _ => Notappl ("syntax error in "^(subs2str subs))
3.195 + handle _ => Chead.Notappl ("syntax error in "^(subs2str subs))
3.196 end
3.197
3.198 | applicable_in (p,p_) pt (m as Rewrite thm'') =
3.199 if member op = [Pbl,Met] p_
3.200 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.201 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.202 else
3.203 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm'' p pt;
3.204 val thy = assoc_thy thy';
3.205 @@ -396,14 +396,14 @@
3.206 in if msg = "OK"
3.207 then
3.208 case rewrite_ thy (assoc_rew_ord ro) rls' false (snd thm'') f of
3.209 - SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
3.210 - | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable")
3.211 - else Notappl msg
3.212 + SOME (f',asm) => Chead.Appl (Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
3.213 + | NONE => Chead.Notappl ("'" ^ fst thm'' ^"' not applicable")
3.214 + else Chead.Notappl msg
3.215 end
3.216
3.217 | applicable_in (p,p_) pt (m as Rewrite_Asm thm'') =
3.218 if member op = [Pbl,Met] p_
3.219 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.220 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.221 else
3.222 let
3.223 val pp = par_pblobj pt p;
3.224 @@ -418,13 +418,13 @@
3.225 | _ => error ("applicable_in: call by "^
3.226 (pos'2str (p,p_)));
3.227 in case rewrite_ thy (assoc_rew_ord ro') erls false (snd thm'') f of
3.228 - SOME (f',asm) => Appl (
3.229 + SOME (f',asm) => Chead.Appl (
3.230 Rewrite' (thy', ro', erls, false, thm'', f, (f', asm)))
3.231 - | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end
3.232 + | NONE => Chead.Notappl ("'" ^ fst thm'' ^ "' not applicable") end
3.233
3.234 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
3.235 if member op = [Pbl,Met] p_
3.236 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.237 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.238 else
3.239 let
3.240 val pp = par_pblobj pt p;
3.241 @@ -439,14 +439,14 @@
3.242 let val subst = subs2subst thy subs
3.243 val subs' = subst2subs' subst
3.244 in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of
3.245 - SOME (f',asm) => Appl (
3.246 + SOME (f',asm) => Chead.Appl (
3.247 Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm)))
3.248 - | NONE => Notappl (rls^" not applicable") end
3.249 - handle _ => Notappl ("syntax error in "^(subs2str subs)) end
3.250 + | NONE => Chead.Notappl (rls^" not applicable") end
3.251 + handle _ => Chead.Notappl ("syntax error in "^(subs2str subs)) end
3.252
3.253 | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) =
3.254 if member op = [Pbl,Met] p_
3.255 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.256 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.257 else
3.258 let
3.259 val pp = par_pblobj pt p;
3.260 @@ -463,14 +463,14 @@
3.261 let val subst = subs2subst thy subs;
3.262 val subs' = subst2subs' subst;
3.263 in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
3.264 - SOME (f',asm) => Appl (
3.265 + SOME (f',asm) => Chead.Appl (
3.266 Rewrite_Set_Inst' (thy',(*put_asm*)false,subst,assoc_rls rls, f, (f', asm)))
3.267 - | NONE => Notappl (rls^" not applicable") end
3.268 - handle _ => Notappl ("syntax error in "^(subs2str subs)) end
3.269 + | NONE => Chead.Notappl (rls^" not applicable") end
3.270 + handle _ => Chead.Notappl ("syntax error in "^(subs2str subs)) end
3.271
3.272 | applicable_in (p,p_) pt (m as Rewrite_Set rls) =
3.273 if member op = [Pbl,Met] p_
3.274 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.275 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.276 else
3.277 let
3.278 val pp = par_pblobj pt p;
3.279 @@ -483,13 +483,13 @@
3.280 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
3.281 SOME (f',asm) =>
3.282 ((*tracing("#.# applicable_in Rewrite_Set,2f'= "^f');*)
3.283 - Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
3.284 + Chead.Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
3.285 )
3.286 - | NONE => Notappl (rls^" not applicable") end
3.287 + | NONE => Chead.Notappl (rls^" not applicable") end
3.288
3.289 | applicable_in (p,p_) pt (m as Detail_Set rls) =
3.290 if member op = [Pbl,Met] p_
3.291 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.292 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.293 else
3.294 let val pp = par_pblobj pt p
3.295 val thy' = (get_obj g_domID pt pp):theory'
3.296 @@ -500,8 +500,8 @@
3.297 (pos'2str (p,p_)));
3.298 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
3.299 SOME (f',asm) =>
3.300 - Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
3.301 - | NONE => Notappl (rls^" not applicable") end
3.302 + Chead.Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
3.303 + | NONE => Chead.Notappl (rls^" not applicable") end
3.304
3.305
3.306 | applicable_in p pt (End_Ruleset) =
3.307 @@ -512,7 +512,7 @@
3.308 *)
3.309 | applicable_in (p,p_) pt (m as Calculate op_) =
3.310 if member op = [Pbl,Met] p_
3.311 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.312 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.313 else
3.314 let
3.315 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
3.316 @@ -522,9 +522,9 @@
3.317 in if msg = "OK" then
3.318 case calculate_ (assoc_thy thy') isa_fn f of
3.319 SOME (f', (id, thm)) =>
3.320 - Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
3.321 - | NONE => Notappl ("'calculate "^op_^"' not applicable")
3.322 - else Notappl msg
3.323 + Chead.Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
3.324 + | NONE => Chead.Notappl ("'calculate "^op_^"' not applicable")
3.325 + else Chead.Notappl msg
3.326 end
3.327
3.328 (*Substitute combines two different kind of "substitution":
3.329 @@ -533,7 +533,7 @@
3.330 (which raises exn for ?a..?z)*)
3.331 | applicable_in (p,p_) pt (m as Substitute sube) =
3.332 if member op = [Pbl,Met] p_
3.333 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.334 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.335 else
3.336 let
3.337 val pp = par_pblobj pt p
3.338 @@ -550,14 +550,14 @@
3.339 (*1*)
3.340 then
3.341 let val f' = subst_atomic subst f
3.342 - in if f = f' then Notappl (sube2str sube^" not applicable")
3.343 - else Appl (Substitute' (ro, erls, subte, f, f'))
3.344 + in if f = f' then Chead.Notappl (sube2str sube^" not applicable")
3.345 + else Chead.Appl (Substitute' (ro, erls, subte, f, f'))
3.346 end
3.347 (*2*)
3.348 else
3.349 case rewrite_terms_ thy ro erls subte f of
3.350 - SOME (f', _) => Appl (Substitute' (ro, erls, subte, f, f'))
3.351 - | NONE => Notappl (sube2str sube^" not applicable")
3.352 + SOME (f', _) => Chead.Appl (Substitute' (ro, erls, subte, f, f'))
3.353 + | NONE => Chead.Notappl (sube2str sube^" not applicable")
3.354 end
3.355
3.356 | applicable_in p pt (Apply_Assumption cts') =
3.357 @@ -566,12 +566,12 @@
3.358 (*'logical' applicability wrt. script in locate: Inconsistent?*)
3.359 | applicable_in (p,p_) pt (m as Take ct') =
3.360 if member op = [Pbl,Met] p_
3.361 - then Notappl (tac2str m ^ " not for pos " ^ pos'2str (p,p_))
3.362 + then Chead.Notappl (tac2str m ^ " not for pos " ^ pos'2str (p,p_))
3.363 else
3.364 let val thy' = get_obj g_domID pt (par_pblobj pt p);
3.365 in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of
3.366 - SOME ct => Appl (Take' ct)
3.367 - | NONE => Notappl ("syntax error in " ^ ct'))
3.368 + SOME ct => Chead.Appl (Take' ct)
3.369 + | NONE => Chead.Notappl ("syntax error in " ^ ct'))
3.370 end
3.371
3.372 | applicable_in p pt (Take_Inst ct') =
3.373 @@ -584,11 +584,11 @@
3.374 then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*)
3.375 case get_obj g_env pt p of
3.376 SOME is =>
3.377 - Appl (Subproblem' ((domID, pblID, e_metID), [],
3.378 + Chead.Appl (Subproblem' ((domID, pblID, e_metID), [],
3.379 e_term, [], e_ctxt(*FIXME.WN150511*), subpbl domID pblID))
3.380 - | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.381 + | NONE => Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.382 else (*somewhere later in the script*)
3.383 - Appl (Subproblem' ((domID, pblID, e_metID), [],
3.384 + Chead.Appl (Subproblem' ((domID, pblID, e_metID), [],
3.385 e_term, [], e_ctxt, subpbl domID pblID))
3.386
3.387 | applicable_in p pt (End_Subproblem) =
3.388 @@ -613,7 +613,7 @@
3.389 | _ => error ("applicable_in: call by "^
3.390 (pos'2str (p,p_)));
3.391 val thy' = get_obj g_domID pt (par_pblobj pt p);
3.392 - in (Appl (Begin_Trans' f))
3.393 + in (Chead.Appl (Begin_Trans' f))
3.394 handle _ => error ("applicable_in: Begin_Trans finds \
3.395 \syntaxerror in '"^(term2str f)^"'") end
3.396
3.397 @@ -621,8 +621,8 @@
3.398 | applicable_in (p,p_) pt (End_Trans) =
3.399 let val thy' = get_obj g_domID pt (par_pblobj pt p);
3.400 in if p_ = Res
3.401 - then Appl (End_Trans' (get_obj g_result pt p))
3.402 - else Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
3.403 + then Chead.Appl (End_Trans' (get_obj g_result pt p))
3.404 + else Chead.Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
3.405 (*TODO: check parent branches*)
3.406 end
3.407 | applicable_in p pt (Begin_Sequ) =
3.408 @@ -636,7 +636,7 @@
3.409
3.410 | applicable_in (p,p_) pt (m as Check_elementwise pred) =
3.411 if member op = [Pbl,Met] p_
3.412 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.413 + then Chead.Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.414 else
3.415 let
3.416 val pp = par_pblobj pt p;
3.417 @@ -649,17 +649,17 @@
3.418 val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
3.419 in case f of
3.420 Const ("List.list.Cons",_) $ _ $ _ =>
3.421 - Appl (Check_elementwise' (f, pred, check_elementwise thy crls f vp))
3.422 + Chead.Appl (Check_elementwise' (f, pred, check_elementwise thy crls f vp))
3.423 | Const ("Tools.UniversalList",_) =>
3.424 - Appl (Check_elementwise' (f, pred, (f,asm)))
3.425 + Chead.Appl (Check_elementwise' (f, pred, (f,asm)))
3.426 | Const ("List.list.Nil",_) =>
3.427 - Appl (Check_elementwise' (f, pred, (f, asm)))
3.428 - | _ => Notappl ("Check_elementwise not applicable: "^(term2str f)^" should be constants")
3.429 + Chead.Appl (Check_elementwise' (f, pred, (f, asm)))
3.430 + | _ => Chead.Notappl ("Check_elementwise not applicable: "^(term2str f)^" should be constants")
3.431 end
3.432
3.433 | applicable_in (p,p_) pt Or_to_List =
3.434 if member op = [Pbl,Met] p_
3.435 - then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
3.436 + then Chead.Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
3.437 else
3.438 let
3.439 val pp = par_pblobj pt p;
3.440 @@ -669,8 +669,8 @@
3.441 Frm => get_obj g_form pt p
3.442 | Res => (fst o (get_obj g_result pt)) p;
3.443 in (let val ls = or2list f
3.444 - in Appl (Or_to_List' (f, ls)) end)
3.445 - handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f))
3.446 + in Chead.Appl (Or_to_List' (f, ls)) end)
3.447 + handle _ => Chead.Notappl ("'Or_to_List' not applicable to "^(term2str f))
3.448 end
3.449
3.450 | applicable_in p pt (Collect_Trues) =
3.451 @@ -678,7 +678,7 @@
3.452 (tac2str (Collect_Trues)))
3.453
3.454 | applicable_in p pt (Empty_Tac) =
3.455 - Notappl "Empty_Tac is not applicable"
3.456 + Chead.Notappl "Empty_Tac is not applicable"
3.457
3.458 | applicable_in (p,p_) pt (Tac id) =
3.459 let
3.460 @@ -692,9 +692,9 @@
3.461 in case id of
3.462 "subproblem_equation_dummy" =>
3.463 if is_expliceq f
3.464 - then Appl (Tac_ (thy, term2str f, id,
3.465 + then Chead.Appl (Tac_ (thy, term2str f, id,
3.466 "subproblem_equation_dummy ("^(term2str f)^")"))
3.467 - else Notappl "applicable only to equations made explicit"
3.468 + else Chead.Notappl "applicable only to equations made explicit"
3.469 | "solve_equation_dummy" =>
3.470 let (*val _= tracing("### applicable_in: solve_equation_dummy: f= "
3.471 ^f);*)
3.472 @@ -702,13 +702,13 @@
3.473 (*val _= tracing("### applicable_in: f'= "^f');*)
3.474 (*val _= (Thm.term_of o the o (parse thy)) f';*)
3.475 (*val _= tracing"### applicable_in: solve_equation_dummy";*)
3.476 - in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
3.477 + in if id' <> "subproblem_equation_dummy" then Chead.Notappl "no subproblem"
3.478 else if (thy2ctxt thy, f') |-> parseNEW |> the |> is_expliceq
3.479 - then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
3.480 + then Chead.Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
3.481 else error ("applicable_in: f= " ^ f') end
3.482 - | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end
3.483 + | _ => Chead.Appl (Tac_ (thy, term2str f, id, term2str f)) end
3.484
3.485 - | applicable_in p pt End_Proof' = Appl End_Proof''
3.486 + | applicable_in p pt End_Proof' = Chead.Appl End_Proof''
3.487
3.488 | applicable_in _ _ m =
3.489 error ("applicable_in called for "^(tac2str m));
3.490 @@ -716,7 +716,7 @@
3.491 (*WN060614 unused*)
3.492 fun tac2tac_ pt p m =
3.493 case applicable_in p pt m of
3.494 - Appl (m') => m'
3.495 - | Notappl _ => error ("tac2mstp': fails with"^
3.496 + Chead.Appl (m') => m'
3.497 + | Chead.Notappl _ => error ("tac2mstp': fails with"^
3.498 (tac2str m));
3.499
4.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed Nov 30 13:05:08 2016 +0100
4.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Dec 12 18:08:13 2016 +0100
4.3 @@ -2,228 +2,76 @@
4.4 most important types are declared in mstools.sml.
4.5 Author: Walther Neuper 991122, Mathias Lehnfeld
4.6 (c) due to copyright terms
4.7 +*)
4.8 +signature CALC_HEAD =
4.9 +sig
4.10 + type calcstate
4.11 + type calcstate'
4.12 + datatype appl = Appl of tac_ | Notappl of string
4.13 + val nxt_specify_init_calc : fmz -> calcstate
4.14 + val specify : tac_ -> pos' -> cid -> ptree ->
4.15 + (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac * safe * ptree
4.16 + val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate'
4.17 + val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list ->
4.18 + (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac
4.19
4.20 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
4.21 - 10 20 30 40 50 60 70 80
4.22 -*)
4.23 + val reset_calchead : ptree * pos' -> ptree * pos'
4.24 + val get_ocalhd : ptree * pos' -> ocalhd
4.25 + val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool
4.26 + val all_modspec : ptree * pos' -> ptree * pos'
4.27
4.28 -(* TODO interne Funktionen aus sig entfernen *)
4.29 -signature CALC_HEAD =
4.30 - sig
4.31 - datatype additm = Add of SpecifyTools.itm | Err of string
4.32 - val all_dsc_in : SpecifyTools.itm_ list -> Term.term list
4.33 - val all_modspec : ptree * pos' -> ptree * pos'
4.34 - datatype appl = Appl of tac_ | Notappl of string
4.35 - val appl_add :
4.36 - Proof.context ->
4.37 - string ->
4.38 - SpecifyTools.ori list ->
4.39 - SpecifyTools.itm list ->
4.40 - (string * (Term.term * Term.term)) list -> cterm' -> additm
4.41 - type calcstate
4.42 - type calcstate'
4.43 - val chk_vars : term ppc -> string * Term.term list
4.44 - val chktyp :
4.45 - theory -> int * term list * term list -> term
4.46 - val chktyps :
4.47 - theory -> term list * term list -> term list
4.48 - val complete_metitms :
4.49 - SpecifyTools.ori list ->
4.50 - SpecifyTools.itm list ->
4.51 - SpecifyTools.itm list -> pat list -> SpecifyTools.itm list
4.52 - val complete_mod_ : ori list * pat list * pat list * itm list ->
4.53 - itm list * itm list
4.54 - val complete_mod : ptree * pos' -> ptree * (pos * pos_)
4.55 - val complete_spec : ptree * pos' -> ptree * pos'
4.56 - val cpy_nam :
4.57 - pat list -> preori list -> pat -> preori
4.58 - val e_calcstate : calcstate
4.59 - val e_calcstate' : calcstate'
4.60 - val eq1 : ''a -> 'b * (''a * 'c) -> bool
4.61 - val eq3 :
4.62 - ''a -> Term.term -> 'b * 'c * 'd * ''a * SpecifyTools.itm_ -> bool
4.63 - val eq4 : ''a -> 'b * ''a list * 'c * 'd * 'e -> bool
4.64 - val eq5 :
4.65 - 'a * 'b * 'c * 'd * SpecifyTools.itm_ ->
4.66 - 'e * 'f * 'g * Term.term * 'h -> bool
4.67 - val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool
4.68 - val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool
4.69 - val f_mout : theory -> mout -> Term.term
4.70 - val filter_outs :
4.71 - SpecifyTools.ori list ->
4.72 - SpecifyTools.itm list -> SpecifyTools.ori list
4.73 - val filter_pbt :
4.74 - SpecifyTools.ori list ->
4.75 - ('a * (Term.term * 'b)) list -> SpecifyTools.ori list
4.76 - val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
4.77 - val foldr1 : ('a * 'a -> 'a) -> 'a list -> 'a
4.78 - val form : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
4.79 - val formres : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
4.80 - val gen_ins' : ('a * 'a -> bool) -> 'a * 'a list -> 'a list
4.81 - val get_formress :
4.82 - (string * (pos * pos_) * Term.term) list list ->
4.83 - pos -> ptree list -> (string * (pos * pos_) * Term.term) list
4.84 - val get_forms :
4.85 - (string * (pos * pos_) * Term.term) list list ->
4.86 - posel list -> ptree list -> (string * (pos * pos_) * Term.term) list
4.87 - val get_interval : pos' -> pos' -> int -> ptree -> (pos' * term) list
4.88 - val get_ocalhd : ptree * pos' -> ocalhd
4.89 - val get_spec_form : tac_ -> pos' -> ptree -> mout
4.90 - val geti_ct :
4.91 - theory ->
4.92 - SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'
4.93 - val getr_ct : theory -> SpecifyTools.ori -> string * cterm'
4.94 - val has_list_type : Term.term -> bool
4.95 - val header : pos_ -> pblID -> metID -> pblmet
4.96 - val insert_ppc :
4.97 - theory ->
4.98 - int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
4.99 - SpecifyTools.itm list -> SpecifyTools.itm list
4.100 - val insert_ppc' :
4.101 - SpecifyTools.itm -> SpecifyTools.itm list -> SpecifyTools.itm list
4.102 - val is_complete_mod : ptree * pos' -> bool
4.103 - val is_complete_mod_ : SpecifyTools.itm list -> bool
4.104 - val is_complete_modspec : ptree * pos' -> bool
4.105 - val is_complete_spec : ptree * pos' -> bool
4.106 - val is_copy_named : 'a * ('b * Term.term) -> bool
4.107 - val is_copy_named_idstr : string -> bool
4.108 - val is_error : SpecifyTools.itm_ -> bool
4.109 - val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
4.110 - val is_known :
4.111 - Proof.context ->
4.112 - string ->
4.113 - SpecifyTools.ori list ->
4.114 - Term.term -> string * SpecifyTools.ori * Term.term list
4.115 - val is_list_type : Term.typ -> bool
4.116 - val is_notyet_input :
4.117 - Proof.context ->
4.118 - SpecifyTools.itm list ->
4.119 - Term.term list ->
4.120 - SpecifyTools.ori ->
4.121 - ('a * (Term.term * Term.term)) list -> string * SpecifyTools.itm
4.122 - val is_parsed : SpecifyTools.itm_ -> bool
4.123 - val is_untouched : SpecifyTools.itm -> bool
4.124 - val matc :
4.125 - theory ->
4.126 - pat list ->
4.127 - Term.term list ->
4.128 - (int list * string * Term.term * Term.term list) list ->
4.129 - (int list * string * Term.term * Term.term list) list
4.130 - val match_ags :
4.131 - theory -> pat list -> Term.term list -> SpecifyTools.ori list
4.132 - val oris2fmz_vals : ori list -> string list * term list
4.133 - val maxl : int list -> int
4.134 - val match_ags_msg : string list -> Term.term -> Term.term list -> unit
4.135 - val memI : ''a list -> ''a -> bool
4.136 - val mk_additem : string -> cterm' -> tac
4.137 - val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
4.138 - val mtc :
4.139 - theory -> pat -> Term.term -> SpecifyTools.preori option
4.140 - val nxt_add :
4.141 - theory ->
4.142 - SpecifyTools.ori list ->
4.143 - (string * (Term.term * 'a)) list ->
4.144 - SpecifyTools.itm list -> (string * cterm') option
4.145 - val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
4.146 - val nxt_spec :
4.147 - pos_ ->
4.148 - bool ->
4.149 - SpecifyTools.ori list ->
4.150 - spec ->
4.151 - SpecifyTools.itm list * SpecifyTools.itm list ->
4.152 - (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->
4.153 - spec -> pos_ * tac
4.154 - val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'
4.155 - val nxt_specif_additem :
4.156 - string -> cterm' -> ptree * (int list * pos_) -> calcstate'
4.157 - val nxt_specify_init_calc : fmz -> calcstate
4.158 - val ocalhd_complete :
4.159 - SpecifyTools.itm list ->
4.160 - (bool * Term.term) list -> domID * pblID * metID -> bool
4.161 - val ori2Coritm :
4.162 - pat list -> ori -> itm
4.163 - val ori_2itm :
4.164 - SpecifyTools.itm_ ->
4.165 - Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
4.166 - val overwrite_ppc :
4.167 - theory ->
4.168 - int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
4.169 - SpecifyTools.itm list ->
4.170 - (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
4.171 - val parse_ok : SpecifyTools.itm_ list -> bool
4.172 - val posform2str : pos' * ptform -> string
4.173 - val posforms2str : (pos' * ptform) list -> string
4.174 - val posterms2str : (pos' * term) list -> string (*tests only*)
4.175 - val ppc135list : 'a SpecifyTools.ppc -> 'a list
4.176 - val ppc2list : 'a SpecifyTools.ppc -> 'a list
4.177 - val pt_extract :
4.178 - ptree * (int list * pos_) ->
4.179 - ptform * tac option * Term.term list
4.180 - val pt_form : ppobj -> ptform
4.181 - val pt_model : ppobj -> pos_ -> ptform
4.182 - val reset_calchead : ptree * pos' -> ptree * pos'
4.183 - val seek_oridts :
4.184 - Proof.context ->
4.185 - string ->
4.186 - Term.term * Term.term list ->
4.187 - (int * SpecifyTools.vats * string * Term.term * Term.term list) list
4.188 - -> string * SpecifyTools.ori * Term.term list
4.189 - val seek_orits :
4.190 - Proof.context ->
4.191 - string ->
4.192 - Term.term list ->
4.193 - (int * SpecifyTools.vats * string * Term.term * Term.term list) list
4.194 - -> string * SpecifyTools.ori * Term.term list
4.195 - val seek_ppc :
4.196 - int -> SpecifyTools.itm list -> SpecifyTools.itm option
4.197 - val show_pt : ptree -> unit
4.198 - val some_spec : spec -> spec -> spec
4.199 - val specify :
4.200 - tac_ ->
4.201 - pos' ->
4.202 - cid ->
4.203 - ptree ->
4.204 - (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *
4.205 - safe * ptree
4.206 - val specify_additem :
4.207 - string ->
4.208 - cterm' * 'a ->
4.209 - int list * pos_ ->
4.210 - 'b ->
4.211 - ptree ->
4.212 - (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
4.213 - val tag_form : theory -> term * term -> term
4.214 - val test_types : Proof.context -> Term.term * Term.term list -> string
4.215 - val typeless : Term.term -> Term.term
4.216 - val unbound_ppc : term SpecifyTools.ppc -> Term.term list
4.217 - val vals_of_oris : SpecifyTools.ori list -> Term.term list
4.218 - val variants_in : Term.term list -> int
4.219 - val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
4.220 - val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
4.221 - end
4.222 -
4.223 + val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list
4.224 + val insert_ppc' : itm -> itm list -> itm list
4.225
4.226 + val complete_mod : ptree * pos' -> ptree * pos'
4.227 + val is_complete_mod : ptree * pos' -> bool
4.228 + val complete_spec : ptree * pos' -> ptree * pos'
4.229 + val is_complete_spec : ptree * pos' -> bool
4.230 + val some_spec : spec -> spec -> spec
4.231 + (* these could go to Ctree ..*)
4.232 + val show_pt : ptree -> unit
4.233 + val pt_extract : ptree * (posel list * pos_) -> ptform * tac option * term list
4.234 + val get_interval : int list * pos_ -> pos' -> int -> ptree -> (pos' * term) list
4.235
4.236 + val match_ags : theory -> pat list -> term list -> ori list
4.237 + val match_ags_msg : pblID -> term -> term list -> unit
4.238 + val oris2fmz_vals : ori list -> string list * term list
4.239 + val vars_of_pbl_' : ('a * ('b * term)) list -> term list
4.240 + val is_known : Proof.context -> string -> ori list -> term -> string * ori * term list
4.241 + val is_notyet_input : Proof.context -> itm list -> term list -> ori -> ('a * (term * term)) list
4.242 + -> string * itm
4.243 + val e_calcstate' : calcstate'
4.244 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.245 + val vals_of_oris : ori list -> term list
4.246 + val is_error : itm_ -> bool
4.247 + val is_copy_named : 'a * ('b * term) -> bool
4.248 + val ori2Coritm : pat list -> ori -> itm
4.249 + val ppc2list : 'a ppc -> 'a list
4.250 + val is_copy_named_idstr : string -> bool
4.251 + val matc : theory -> (string * (term * term)) list -> term list -> preori list -> preori list
4.252 + val mtc : theory -> pat -> term -> preori option
4.253 + val cpy_nam : pat list -> preori list -> pat -> preori
4.254 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.255 +end
4.256
4.257 -
4.258 -structure CalcHead (**): CALC_HEAD(**) =
4.259 -
4.260 +structure Chead(**): CALC_HEAD(**) =
4.261 struct
4.262
4.263 (* datatypes *)
4.264
4.265 -(*.the state wich is stored after each step of calculation; it contains
4.266 +(* the state wich is stored after each step of calculation; it contains
4.267 the calc-state and a list of [tac,istate](="tacis") to be applied next.
4.268 the last_elem tacis is the first to apply to the calc-state and
4.269 the (only) one shown to the front-end as the 'proposed tac'.
4.270 the calc-state resulting from the application of tacis is not stored,
4.271 because the tacis hold enough information for efficiently rebuilding
4.272 - this state just by "fun generate ".*)
4.273 + this state just by "fun generate "
4.274 +*)
4.275 type calcstate =
4.276 - (ptree * pos') * (*the calc-state to which the tacis could be applied*)
4.277 - (taci list); (*ev. several (hidden) steps;
4.278 - in REVERSE order: first tac_ to apply is last_elem*)
4.279 -val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
4.280 + (ptree * pos') * (* the calc-state to which the tacis could be applied *)
4.281 + (taci list) (* ev. several (hidden) steps;
4.282 + in REVERSE order: first tac_ to apply is last_elem *)
4.283 +val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]) : calcstate;
4.284
4.285 (*the state used during one calculation within the mathengine; it contains
4.286 a list of [tac,istate](="tacis") which generated the the calc-state;
4.287 @@ -235,240 +83,122 @@
4.288 because the tacis hold enought information for efficiently rebuilding
4.289 this state just by "fun generate ".*)
4.290 type calcstate' =
4.291 - taci list * (*cas. several (hidden) steps;
4.292 - in REVERSE order: first tac_ to apply is last_elem*)
4.293 - pos' list * (*a "continuous" sequence of pos',
4.294 - deleted by application of taci list*)
4.295 - (ptree * pos'); (*the calc-state resulting from the application of tacis*)
4.296 + taci list * (* cas. several (hidden) steps;
4.297 + in REVERSE order: first tac_ to apply is last_elem*)
4.298 + pos' list * (* a "continuous" sequence of pos', deleted by application of taci list*)
4.299 + (ptree * pos') (* the calc-state resulting from the application of tacis*)
4.300 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
4.301
4.302 -(*FIXXXME.WN020430 intermediate hack for fun ass_up*)
4.303 -fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (Thm.term_of o the o (parse thy)) f
4.304 - | f_mout thy _ = error "f_mout: not called with formula";
4.305 +(* FIXXXME.WN020430 intermediate hack for fun ass_up *)
4.306 +fun f_mout thy (Form' (FormKF (_, _, _, _, f))) = (Thm.term_of o the o (parse thy)) f
4.307 + | f_mout _ _ = error "f_mout: not called with formula";
4.308
4.309 +(* is the calchead complete ? *)
4.310 +fun ocalhd_complete its pre (dI, pI, mI) =
4.311 + foldl and_ (true, map #3 its) andalso
4.312 + foldl and_ (true, map #1 pre) andalso
4.313 + dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID
4.314
4.315 -(*.is the calchead complete ?.*)
4.316 -fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
4.317 - foldl and_ (true, map #3 its) andalso
4.318 - foldl and_ (true, map #1 pre) andalso
4.319 - dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
4.320 -
4.321 -(*["BOOL (1+x=2)","REAL x"] --match_ags--> oris
4.322 - --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"]*)
4.323 +(* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
4.324 + --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
4.325 fun oris2fmz_vals oris =
4.326 - let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) =
4.327 - ((term2str o comp_dts') (dsc, ts), last_elem ts)
4.328 - handle _ => error ("ori2fmz_env called with "^terms2str ts)
4.329 - in (split_list o (map ori2fmz_vals)) oris end;
4.330 + let fun ori2fmz_vals ((_, _, _, dsc, ts): ori) =
4.331 + ((term2str o comp_dts') (dsc, ts), last_elem ts)
4.332 + handle _ => error ("ori2fmz_env called with " ^ terms2str ts)
4.333 + in (split_list o (map ori2fmz_vals)) oris end
4.334
4.335 (* make a term 'typeless' for comparing with another 'typeless' term;
4.336 'type-less' usually is illtyped *)
4.337 -fun typeless (Const(s,_)) = (Const(s,e_type))
4.338 - | typeless (Free(s,_)) = (Free(s,e_type))
4.339 - | typeless (Var(n,_)) = (Var(n,e_type))
4.340 +fun typeless (Const (s, _)) = (Const (s, e_type))
4.341 + | typeless (Free (s, _)) = (Free (s, e_type))
4.342 + | typeless (Var (n, _)) = (Var (n, e_type))
4.343 | typeless (Bound i) = (Bound i)
4.344 - | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
4.345 - | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
4.346 -(*
4.347 -> val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
4.348 -> val (_,t1) = split_dsc_t hs (Thm.term_of ct);
4.349 -> val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
4.350 -> val (_,t2) = split_dsc_t hs (Thm.term_of ct);
4.351 -> typeless t1 = typeless t2;
4.352 -val it = true : bool
4.353 -*)
4.354 + | typeless (Abs (s, _,t)) = Abs(s, e_type, typeless t)
4.355 + | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
4.356
4.357 -
4.358 -
4.359 -(*.to an input (d,ts) find the according ori and insert the ts.*)
4.360 -(*WN.11.03: + dont take first inter<>[]*)
4.361 -fun seek_oridts ctxt sel (d,ts) [] =
4.362 +(* to an input (d,ts) find the according ori and insert the ts)
4.363 + WN.11.03: + dont take first inter<>[] *)
4.364 +fun seek_oridts ctxt sel (d, ts) [] =
4.365 ("seek_oridts: input ('" ^
4.366 - (term_to_string' ctxt (comp_dts (d,ts))) ^ "') not found in oris (typed)",
4.367 + (term_to_string' ctxt (comp_dts (d, ts))) ^ "') not found in oris (typed)",
4.368 (0, [], sel, d, ts),
4.369 [])
4.370 - | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =
4.371 - if sel = sel' andalso d = d' andalso (inter op = ts ts') <> [] then
4.372 - ("", (id, vat, sel, d, inter op = ts ts'), ts') else
4.373 - seek_oridts ctxt sel (d, ts) oris;
4.374 + | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
4.375 + if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
4.376 + then ("", (id, vat, sel, d, inter op = ts ts'), ts')
4.377 + else seek_oridts ctxt sel (d, ts) oris
4.378
4.379 -(*.to an input (_,ts) find the according ori and insert the ts.*)
4.380 -fun seek_orits ctxt sel ts [] =
4.381 +(* to an input (_,ts) find the according ori and insert the ts *)
4.382 +fun seek_orits ctxt _ ts [] =
4.383 ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^
4.384 "') not found in oris (typed)", e_ori_, [])
4.385 - | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
4.386 + | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: (oris: ori list)) =
4.387 if sel = sel' andalso (inter op = ts ts') <> []
4.388 - then if sel = sel'
4.389 - then ("", (id,vat,sel,d, inter op = ts ts'):ori, ts')
4.390 - else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])
4.391 - else seek_orits ctxt sel ts oris;
4.392 -(* false
4.393 -> val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
4.394 -> seek_orits thy sel ts [(id,vat,sel',d,ts')];
4.395 -uncaught exception TYPE
4.396 -> seek_orits thy sel ts [];
4.397 -uncaught exception TYPE
4.398 -*)
4.399 + then
4.400 + if sel = sel'
4.401 + then ("", (id, vat, sel, d, inter op = ts ts'): ori, ts')
4.402 + else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])
4.403 + else seek_orits ctxt sel ts oris
4.404
4.405 -(*find_first item with #1 equal to id*)
4.406 -fun seek_ppc id [] = NONE
4.407 - | seek_ppc id (p::(ppc:itm list)) =
4.408 - if id = #1 p then SOME p else seek_ppc id ppc;
4.409 +(* find_first item with #1 equal to id *)
4.410 +fun seek_ppc _ [] = NONE
4.411 + | seek_ppc id (p :: (ppc: itm list)) = if id = #1 p then SOME p else seek_ppc id ppc
4.412
4.413 +datatype appl =
4.414 + Appl of tac_ (* tactic is applicable at a certain position in the Ctree *)
4.415 +| Notappl of string (* tactic is NOT applicable *)
4.416
4.417 -datatype appl = Appl of tac_ | Notappl of string;
4.418 -
4.419 -fun ppc2list ({Given=gis,Where=whs,Find=fis,
4.420 - With=wis,Relate=res}: 'a ppc) =
4.421 - gis @ whs @ fis @ wis @ res;
4.422 -fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
4.423 - gis @ fis @ res;
4.424 -
4.425 -
4.426 -
4.427 +fun ppc2list ({Given = gis, Where = whs, Find = fis, With = wis, Relate = res}: 'a ppc) =
4.428 + gis @ whs @ fis @ wis @ res
4.429 +fun ppc135list ({Given = gis, Find = fis, Relate = res, ...}: 'a ppc) = gis @ fis @ res
4.430
4.431 (* get the number of variants in a problem in 'original',
4.432 assumes equal descriptions in immediate sequence *)
4.433 fun variants_in ts =
4.434 - let fun eq(x,y) = head_of x = head_of y;
4.435 - fun cnt eq [] y n = ([n],[])
4.436 - | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
4.437 - else ([n], x::xs);
4.438 - fun coll eq xs [] = xs
4.439 - | coll eq xs (y::ys) =
4.440 - let val (n,ys') = cnt eq (y::ys) y 0;
4.441 - in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
4.442 - val vts = subtract op = [1] (distinct (coll eq [] ts));
4.443 - in case vts of [] => 1 | [n] => n
4.444 - | _ => error "different variants in formalization" end;
4.445 -(*
4.446 -> cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
4.447 -val it = ([3],[4,5,5,5,5,5]) : int list * int list
4.448 -> coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
4.449 -val it = [1,3,1,5] : int list
4.450 -*)
4.451 + let
4.452 + fun eq (x, y) = head_of x = head_of y
4.453 + fun cnt _ [] _ n = ([n], [])
4.454 + | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
4.455 + fun coll _ xs [] = xs
4.456 + | coll eq xs (y :: ys) =
4.457 + let val (n, ys') = cnt eq (y :: ys) y 0
4.458 + in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
4.459 + val vts = subtract op = [1] (distinct (coll eq [] ts))
4.460 + in
4.461 + case vts of
4.462 + [] => 1
4.463 + | [n] => n
4.464 + | _ => error "different variants in formalization"
4.465 + end
4.466
4.467 -fun is_list_type (Type("List.list",_)) = true
4.468 - | is_list_type _ = false;
4.469 -(* fun destr (Type(str,sort)) = (str,sort);
4.470 -> val (SOME ct) = parse thy "lll::real list";
4.471 -> val ty = (#T o rep_cterm) ct;
4.472 -> is_list_type ty;
4.473 -val it = true : bool
4.474 -> destr ty;
4.475 -val it = ("List.list",["RealDef.real"]) : string * typ list
4.476 -> atomty ((#t o rep_cterm) ct);
4.477 -*** -------------
4.478 -*** Free ( lll, real list)
4.479 -val it = () : unit
4.480 -
4.481 -> val (SOME ct) = parse thy "[lll::real]";
4.482 -> val ty = (#T o rep_cterm) ct;
4.483 -> is_list_type ty;
4.484 -val it = true : bool
4.485 -> destr ty;
4.486 -val it = ("List.list",["'a"]) : string * typ list
4.487 -> atomty ((#t o rep_cterm) ct);
4.488 -*** -------------
4.489 -*** Const ( List.list.Cons, [real, real list] => real list)
4.490 -*** Free ( lll, real)
4.491 -*** Const ( List.list.Nil, real list)
4.492 -
4.493 -> val (SOME ct) = parse thy "lll";
4.494 -> val ty = (#T o rep_cterm) ct;
4.495 -> is_list_type ty;
4.496 -val it = false : bool *)
4.497 -
4.498 -
4.499 -fun has_list_type (Free(_,T)) = is_list_type T
4.500 - | has_list_type _ = false;
4.501 -(*
4.502 -> val (SOME ct) = parse thy "lll::real list";
4.503 -> has_list_type (Thm.term_of ct);
4.504 -val it = true : bool
4.505 -> val (SOME ct) = parse thy "[lll::real]";
4.506 -> has_list_type (Thm.term_of ct);
4.507 -val it = false : bool *)
4.508 -
4.509 +fun is_list_type (Type ("List.list", _)) = true
4.510 + | is_list_type _ = false
4.511 +fun has_list_type (Free (_, T)) = is_list_type T
4.512 + | has_list_type _ = false
4.513 fun is_parsed (Syn _) = false
4.514 - | is_parsed _ = true;
4.515 -fun parse_ok its = foldl and_ (true, map is_parsed its);
4.516 + | is_parsed _ = true
4.517 +fun parse_ok its = foldl and_ (true, map is_parsed its)
4.518
4.519 fun all_dsc_in itm_s =
4.520 let
4.521 - fun d_in (Cor ((d,_),_)) = [d]
4.522 - | d_in (Syn c) = []
4.523 - | d_in (Typ c) = []
4.524 + fun d_in (Cor ((d, _), _)) = [d]
4.525 + | d_in (Syn _) = []
4.526 + | d_in (Typ _) = []
4.527 | d_in (Inc ((d,_),_)) = [d]
4.528 | d_in (Sup (d,_)) = [d]
4.529 - | d_in (Mis (d,_)) = [d];
4.530 - in (flat o (map d_in)) itm_s end;
4.531 + | d_in (Mis (d,_)) = [d]
4.532 + | d_in i = error ("all_dsc_in: uncovered case with " ^ itm_2str i)
4.533 + in (flat o (map d_in)) itm_s end;
4.534
4.535 -(* 30.1.00 ---
4.536 -fun is_Syn (Syn _) = true
4.537 - | is_Syn (Typ _) = true
4.538 - | is_Syn _ = false;
4.539 - --- *)
4.540 -fun is_error (Cor (_,ts)) = false
4.541 - | is_error (Sup (_,ts)) = false
4.542 - | is_error (Inc (_,ts)) = false
4.543 - | is_error (Mis (_,ts)) = false
4.544 - | is_error _ = true;
4.545 +fun is_error (Cor _) = false
4.546 + | is_error (Sup _) = false
4.547 + | is_error (Inc _) = false
4.548 + | is_error (Mis _) = false
4.549 + | is_error _ = true
4.550
4.551 -(* 30.1.00 ---
4.552 -fun ct_in (Syn (c)) = c
4.553 - | ct_in (Typ (c)) = c
4.554 - | ct_in _ = error "ct_in called for Cor .. Sup";
4.555 - --- *)
4.556 -
4.557 -(*#############################################################*)
4.558 -(*#############################################################*)
4.559 -(* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
4.560 -
4.561 -
4.562 -(* testdaten besorgen:
4.563 - use"test-coil-kernel.sml";
4.564 - val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
4.565 - get_obj I pt p;
4.566 - *)
4.567 -
4.568 -(* given oris, ppc,
4.569 - variant V: oris union ppc => int, id ID: oris union ppc => int
4.570 -
4.571 - ppc is_complete ==
4.572 - EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
4.573 -
4.574 - and
4.575 - @vt = max sum(i : ppc) V i
4.576 -*)
4.577 -
4.578 -
4.579 -
4.580 -(*
4.581 -> ((vts_cnt (vts_in itms))) itms;
4.582 -
4.583 -
4.584 -
4.585 ----^^--test 10.3.
4.586 -> val vts = vts_in itms;
4.587 -val vts = [1,2,3] : int list
4.588 -> val nvts = vts_cnt vts itms;
4.589 -val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
4.590 -> val mx = max2 nvts;
4.591 -val mx = (3,7) : int * int
4.592 -> val v = max_vt itms;
4.593 -val v = 3 : int
4.594 ---------------------------
4.595 ->
4.596 -*)
4.597 -
4.598 -(*.get the first term in ts from ori.*)
4.599 -(* val (_,_,fd,d,ts) = hd miss;
4.600 - *)
4.601 +(* get the first term in ts from ori *)
4.602 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
4.603 - (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm');
4.604 -(* val t = comp_dts (d,[hd ts]);
4.605 - *)
4.606 + (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm')
4.607
4.608 (* get a term from ori, notyet input in itm.
4.609 the term from ori is thrown back to a string in order to reuse
4.610 @@ -477,16 +207,11 @@
4.611 (fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm')
4.612
4.613 (* in FE dsc, not dat: this is in itms ...*)
4.614 -fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
4.615 - | is_untouched _ = false;
4.616 -
4.617 +fun is_untouched ((_, _, false, _, Inc ((_, []), _)): itm) = true
4.618 + | is_untouched _ = false
4.619
4.620 (* select an item in oris, notyet input in itms
4.621 (precondition: in itms are only Cor, Sup, Inc) *)
4.622 -local infix mem;
4.623 -fun x mem [] = false
4.624 - | x mem (y :: ys) = x = y orelse x mem ys;
4.625 -in
4.626 (*args of nxt_add
4.627 thy : for?
4.628 oris: from formalization 'type fmz', structured for efficient access
4.629 @@ -494,65 +219,51 @@
4.630 itms: already input items
4.631 *)
4.632 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
4.633 - let
4.634 - fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
4.635 - fun is_elem itms (f,(d,t)) =
4.636 - case find_first (test_d d) itms of
4.637 - SOME _ => true | NONE => false;
4.638 - in case filter_out (is_elem itms) pbt of
4.639 -(* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
4.640 - *)
4.641 - (f,(d,_))::itms =>
4.642 - SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')
4.643 - | _ => NONE end
4.644 + let
4.645 + fun test_d d ((i, _, _, _, itm_): itm) = (d = (d_in itm_)) andalso i <> 0
4.646 + fun is_elem itms (_, (d, _)) =
4.647 + case find_first (test_d d) itms of SOME _ => true | NONE => false
4.648 + in
4.649 + case filter_out (is_elem itms) pbt of
4.650 + (f, (d, _)) :: _ => SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')
4.651 + | _ => NONE
4.652 + end
4.653 + | nxt_add thy oris _ itms =
4.654 + let
4.655 + fun testr_vt v ori = member op= (#2 (ori:ori)) v andalso (#3 ori) <> "#undef"
4.656 + fun testi_vt v itm =member op= (#2 (itm:itm)) v
4.657 + fun test_id ids r = member op= ids (#1 (r:ori))
4.658 + fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
4.659 + (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts)
4.660 + fun false_and_not_Sup ((_, _, false, _, Sup _): itm) = false
4.661 + | false_and_not_Sup (_, _, false, _, _) = true
4.662 + | false_and_not_Sup _ = false
4.663 + val v = if itms = [] then 1 else max_vt itms
4.664 + val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
4.665 + val vits =
4.666 + if v = 0
4.667 + then itms (* because of dsc without dat *)
4.668 + else filter (testi_vt v) itms; (* itms..vat *)
4.669 + val icl = filter false_and_not_Sup vits; (* incomplete *)
4.670 + in
4.671 + if icl = []
4.672 + then case filter_out (test_id (map #1 vits)) vors of
4.673 + [] => NONE
4.674 + | miss => SOME (getr_ct thy (hd miss))
4.675 + else
4.676 + case find_first (test_subset (hd icl)) vors of
4.677 + NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
4.678 + | SOME ori => SOME (geti_ct thy ori (hd icl))
4.679 + end
4.680
4.681 -(* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
4.682 - *)
4.683 - | nxt_add thy oris pbt itms =
4.684 - let
4.685 - fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
4.686 - andalso (#3 ori) <>"#undef";
4.687 - fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
4.688 - fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
4.689 - fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
4.690 - (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
4.691 - fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
4.692 - | false_and_not_Sup (i,v,false,f, _) = true
4.693 - | false_and_not_Sup _ = false;
4.694 -
4.695 - val v = if itms = [] then 1 else max_vt itms;
4.696 - val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
4.697 - val vits = if v = 0 then itms (*because of dsc without dat*)
4.698 - else filter (testi_vt v) itms; (*itms..vat*)
4.699 - val icl = filter false_and_not_Sup vits; (* incomplete *)
4.700 - in if icl = []
4.701 - then case filter_out (test_id (map #1 vits)) vors of
4.702 - [] => NONE
4.703 - (* val miss = filter_out (test_id (map #1 vits)) vors;
4.704 - *)
4.705 - | miss => SOME (getr_ct thy (hd miss))
4.706 - else
4.707 - case find_first (test_subset (hd icl)) vors of
4.708 - (* val SOME ori = find_first (test_subset (hd icl)) vors;
4.709 - *)
4.710 - NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
4.711 - | SOME ori => SOME (geti_ct thy ori (hd icl))
4.712 - end
4.713 -end;
4.714 -
4.715 -
4.716 -
4.717 -fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
4.718 - | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
4.719 +fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
4.720 + | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
4.721 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
4.722 - | mk_delete thy str _ =
4.723 - error ("mk_delete: called with field '"^str^"'");
4.724 + | mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"")
4.725 fun mk_additem "#Given" ct = Add_Given ct
4.726 - | mk_additem "#Find" ct = Add_Find ct
4.727 + | mk_additem "#Find" ct = Add_Find ct
4.728 | mk_additem "#Relate"ct = Add_Relation ct
4.729 - | mk_additem str _ =
4.730 - error ("mk_additem: called with field '"^str^"'");
4.731 -
4.732 + | mk_additem str _ = error ("mk_additem: called with field \"" ^ str ^ "\"")
4.733
4.734 (* determine the next step of specification;
4.735 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
4.736 @@ -567,95 +278,77 @@
4.737 (pbt, mpc) problem type, guard of method
4.738 *)
4.739 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
4.740 - ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
4.741 - ((*tracing"### nxt_spec Pbl";*)
4.742 - if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
4.743 + ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
4.744 + (if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
4.745 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
4.746 - else case find_first (is_error o #5) (pbl:itm list) of
4.747 - SOME (_, _, _, fd, itm_) =>
4.748 - (Pbl, mk_delete
4.749 - (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
4.750 - | NONE =>
4.751 - ((*tracing"### nxt_spec is_error NONE";*)
4.752 - case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
4.753 - oris pbt pbl of
4.754 - SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
4.755 - (Pbl, mk_additem fd ct'))
4.756 - | NONE => (*pbl-items complete*)
4.757 - if not preok then (Pbl, Refine_Problem pI')
4.758 - else
4.759 - if dI = e_domID then (Pbl, Specify_Theory dI')
4.760 - else if pI = e_pblID then (Pbl, Specify_Problem pI')
4.761 - else if mI = e_metID then (Pbl, Specify_Method mI')
4.762 - else
4.763 - case find_first (is_error o #5) met of
4.764 - SOME (_,_,_,fd,itm_) =>
4.765 - (Met, mk_delete (assoc_thy dI) fd itm_)
4.766 - | NONE =>
4.767 - (case nxt_add (assoc_thy dI) oris mpc met of
4.768 - SOME (fd,ct') => (*30.8.01: pre?!?*)
4.769 - (Met, mk_additem fd ct')
4.770 - | NONE =>
4.771 - ((*Solv 3.4.00*)Met, Apply_Method mI))))
4.772 -
4.773 - | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
4.774 - ((*tracing"### nxt_spec Met"; *)
4.775 - case find_first (is_error o #5) met of
4.776 - SOME (_,_,_,fd,itm_) =>
4.777 - (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
4.778 - | NONE =>
4.779 - case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
4.780 - SOME (fd,ct') => (Met, mk_additem fd ct')
4.781 - | NONE =>
4.782 - ((*tracing"### nxt_spec Met: nxt_add NONE";*)
4.783 - if dI = e_domID then (Met, Specify_Theory dI')
4.784 - else if pI = e_pblID then (Met, Specify_Problem pI')
4.785 - else if not preok then (Met, Specify_Method mI)
4.786 - else (Met, Apply_Method mI)));
4.787 -
4.788 -(* di_ pI_ mI_ pos_
4.789 -val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
4.790 - (2,[2],true,"#Find",Syn("empty"))];
4.791 -*)
4.792 + else
4.793 + case find_first (is_error o #5) (pbl:itm list) of
4.794 + SOME (_, _, _, fd, itm_) =>
4.795 + (Pbl, mk_delete (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
4.796 + | NONE =>
4.797 + (case nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl of
4.798 + SOME (fd,ct') => (Pbl, mk_additem fd ct')
4.799 + | NONE => (*pbl-items complete*)
4.800 + if not preok then (Pbl, Refine_Problem pI')
4.801 + else if dI = e_domID then (Pbl, Specify_Theory dI')
4.802 + else if pI = e_pblID then (Pbl, Specify_Problem pI')
4.803 + else if mI = e_metID then (Pbl, Specify_Method mI')
4.804 + else
4.805 + case find_first (is_error o #5) met of
4.806 + SOME (_, _, _, fd, itm_) => (Met, mk_delete (assoc_thy dI) fd itm_)
4.807 + | NONE =>
4.808 + (case nxt_add (assoc_thy dI) oris mpc met of
4.809 + SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*)
4.810 + | NONE => (Met, Apply_Method mI))))
4.811 + | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
4.812 + (case find_first (is_error o #5) met of
4.813 + SOME (_,_,_,fd,itm_) => (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
4.814 + | NONE =>
4.815 + case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
4.816 + SOME (fd,ct') => (Met, mk_additem fd ct')
4.817 + | NONE =>
4.818 + (if dI = e_domID then (Met, Specify_Theory dI')
4.819 + else if pI = e_pblID then (Met, Specify_Problem pI')
4.820 + else if not preok then (Met, Specify_Method mI)
4.821 + else (Met, Apply_Method mI)))
4.822 + | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)
4.823
4.824 fun is_field_correct sel d dscpbt =
4.825 case assoc (dscpbt, sel) of
4.826 NONE => false
4.827 - | SOME ds => member op = ds d;
4.828 + | SOME ds => member op = ds d
4.829
4.830 -(*. update the itm_ already input, all..from ori .*)
4.831 -(* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
4.832 - *)
4.833 -fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
4.834 +(* update the itm_ already input, all..from ori *)
4.835 +fun ori_2itm itm_ pid all ((id, vt, fd, d, ts): ori) =
4.836 let
4.837 val ts' = union op = (ts_in itm_) ts;
4.838 val pval = pbl_ids' d ts'
4.839 - (*WN.9.5.03: FIXXXME [#0, epsilon]
4.840 - here would upd_penv be called for [#0, epsilon] etc. *)
4.841 - val complete = if eq_set op = (ts', all) then true else false;
4.842 - in case itm_ of
4.843 - (Cor _) =>
4.844 - (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
4.845 - else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
4.846 - | (Syn c) => error ("ori_2itm wants to overwrite "^c)
4.847 - | (Typ c) => error ("ori_2itm wants to overwrite "^c)
4.848 - | (Inc _) => if complete
4.849 - then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
4.850 - else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
4.851 - | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
4.852 - (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
4.853 - (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
4.854 -(* 28.1.00: not completely clear ---^^^ etc.*)
4.855 -(* 4.9.01: Mis just copied---vvv *)
4.856 - | (Mis _) => if complete
4.857 - then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
4.858 - else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
4.859 - end;
4.860 + (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
4.861 + val complete = if eq_set op = (ts', all) then true else false
4.862 + in
4.863 + case itm_ of
4.864 + (Cor _) =>
4.865 + (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
4.866 + else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval)))): itm
4.867 + | (Syn c) => error ("ori_2itm wants to overwrite " ^ c)
4.868 + | (Typ c) => error ("ori_2itm wants to overwrite " ^ c)
4.869 + | (Inc _) =>
4.870 + if complete
4.871 + then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
4.872 + else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
4.873 + | (Sup (d,ts')) => (*4.9.01 lost env*)
4.874 + (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
4.875 + (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
4.876 + (* 28.1.00: not completely clear ---^^^ etc.*)
4.877 + | (Mis _) => (* 4.9.01: Mis just copied *)
4.878 + if complete
4.879 + then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
4.880 + else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
4.881 + | i => error ("ori_2itm: uncovered case of "^ itm_2str i)
4.882 + end
4.883
4.884 -
4.885 -fun eq1 d (_,(d',_)) = (d = d');
4.886 -fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
4.887 -
4.888 +fun eq1 d (_, (d', _)) = (d = d')
4.889 +fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (d_in itm_)
4.890
4.891 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
4.892 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
4.893 @@ -667,675 +360,609 @@
4.894 (2) ori(ts) subset itm(ts) --- Err "already input"
4.895 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
4.896 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
4.897 -(* val(itms,(i,v,f,d,ts)) = (ppc,ori');
4.898 - *)
4.899 -fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
4.900 +fun is_notyet_input ctxt (itms: itm list) all ((i, v, f, d, ts): ori) pbt =
4.901 case find_first (eq1 d) pbt of
4.902 - SOME (_,(_,pid)) =>
4.903 + SOME (_, (_, pid)) =>
4.904 (case find_first (eq3 f d) itms of
4.905 SOME (_,_,_,_,itm_) =>
4.906 - let
4.907 - val ts' = inter op = (ts_in itm_) ts;
4.908 - in
4.909 - if subset op = (ts, ts')
4.910 - then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm)(*2*)
4.911 - else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
4.912 + let val ts' = inter op = (ts_in itm_) ts
4.913 + in
4.914 + if subset op = (ts, ts')
4.915 + then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm) (*2*)
4.916 + else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
4.917 end
4.918 - | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[]))) pid all (i,v,f,d,ts))) (*1*)
4.919 - | NONE => ("", ori_2itm (Sup (d,ts)) e_term all (i,v,f,d,ts));
4.920 + | NONE => ("", ori_2itm (Inc ((e_term, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
4.921 + | NONE => ("", ori_2itm (Sup (d, ts)) e_term all (i, v, f, d, ts))
4.922
4.923 fun test_types ctxt (d,ts) =
4.924 let
4.925 - val opt = (try comp_dts) (d,ts);
4.926 + val opt = (try comp_dts) (d, ts)
4.927 val msg = case opt of
4.928 SOME _ => ""
4.929 | NONE => (term_to_string' ctxt d ^ " " ^
4.930 - (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped");
4.931 - in msg end;
4.932 + (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped")
4.933 + in msg end
4.934
4.935 -fun maxl [] = error "maxl of []"
4.936 - | maxl (y::ys) =
4.937 - let fun mx x [] = x
4.938 - | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
4.939 - in mx y ys end;
4.940 -
4.941 -
4.942 -(*. is the input term t known in oris ?
4.943 - give feedback on all(?) strange input;
4.944 - return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
4.945 +(* is the input term t known in oris ?
4.946 + give feedback on all(?) strange input;
4.947 + return _all_ terms already input to this item (e.g. valuesFor a,b) *)
4.948 fun is_known ctxt sel ori t =
4.949 let
4.950 - val _ = tracing ("RM is_known: t=" ^ term2str t);
4.951 - val ots = (distinct o flat o (map #5)) (ori:ori list);
4.952 - val oids = ((map (fst o dest_Free)) o distinct o
4.953 - flat o (map vars)) ots;
4.954 - val (d, ts) = split_dts t;
4.955 - val ids = map (fst o dest_Free)
4.956 - ((distinct o (flat o (map vars))) ts);
4.957 - in if (subtract op = oids ids) <> []
4.958 - then (("identifiers "^(strs2str' (subtract op = oids ids)) ^
4.959 - " not in example"), e_ori_, [])
4.960 - else
4.961 - if d = e_term
4.962 - then
4.963 - if not (subset op = (map typeless ts, map typeless ots))
4.964 - then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
4.965 - "' not in example (typeless)", e_ori_, [])
4.966 - else
4.967 - (case seek_orits ctxt sel ts ori of
4.968 - ("", ori_ as (_,_,_,d,ts), all) =>
4.969 - (case test_types ctxt (d,ts) of
4.970 - "" => ("", ori_, all)
4.971 - | msg => (msg, e_ori_, []))
4.972 - | (msg,_,_) => (msg, e_ori_, []))
4.973 - else
4.974 - if member op = (map #4 ori) d
4.975 - then seek_oridts ctxt sel (d,ts) ori
4.976 - else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
4.977 - end;
4.978 + val _ = tracing ("RM is_known: t=" ^ term2str t)
4.979 + val ots = (distinct o flat o (map #5)) (ori:ori list)
4.980 + val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots
4.981 + val (d, ts) = split_dts t
4.982 + val ids = map (fst o dest_Free) ((distinct o (flat o (map vars))) ts)
4.983 + in
4.984 + if (subtract op = oids ids) <> []
4.985 + then (("identifiers "^(strs2str' (subtract op = oids ids)) ^ " not in example"), e_ori_, [])
4.986 + else
4.987 + if d = e_term
4.988 + then
4.989 + if not (subset op = (map typeless ts, map typeless ots))
4.990 + then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
4.991 + "' not in example (typeless)", e_ori_, [])
4.992 + else
4.993 + (case seek_orits ctxt sel ts ori of
4.994 + ("", ori_ as (_,_,_,d,ts), all) =>
4.995 + (case test_types ctxt (d,ts) of
4.996 + "" => ("", ori_, all)
4.997 + | msg => (msg, e_ori_, []))
4.998 + | (msg,_,_) => (msg, e_ori_, []))
4.999 + else
4.1000 + if member op = (map #4 ori) d
4.1001 + then seek_oridts ctxt sel (d, ts) ori
4.1002 + else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
4.1003 + end
4.1004
4.1005 -(*. for return-value of appl_add .*)
4.1006 +
4.1007 datatype additm =
4.1008 - Add of itm
4.1009 - | Err of string; (*error-message*)
4.1010 + Add of itm (* return-value of appl_add *)
4.1011 +| Err of string (* error-message *)
4.1012
4.1013 +(* add an item to the model; check wrt. oris and pbt.
4.1014 + in contrary to oris<>[] below, this part handles user-input
4.1015 + extremely acceptive, i.e. accept input instead error-msg *)
4.1016 +fun appl_add ctxt sel [] ppc pbt ct =
4.1017 + let
4.1018 + val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl)
4.1019 + in
4.1020 + case parseNEW ctxt ct of
4.1021 + NONE => Add (i, [], false, sel, Syn ct)
4.1022 + | SOME t =>
4.1023 + let val (d, ts) = split_dts t
4.1024 + in
4.1025 + if d = e_term
4.1026 + then Add (i, [], false, sel, Mis (dsc_unknown, hd ts))
4.1027 + else
4.1028 + (case find_first (eq1 d) pbt of
4.1029 + NONE => Add (i, [], true, sel, Sup (d,ts))
4.1030 + | SOME (f, (_, id)) =>
4.1031 + let fun eq2 d (i, _, _, _, itm_) = d = (d_in itm_) andalso i <> 0
4.1032 + in case find_first (eq2 d) ppc of
4.1033 + NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
4.1034 + | SOME (i', _, _, _, itm_) =>
4.1035 + if is_list_dsc d
4.1036 + then
4.1037 + let
4.1038 + val in_itm = ts_in itm_
4.1039 + val ts' = union op = ts in_itm
4.1040 + val i'' = if in_itm = [] then i else i'
4.1041 + in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts')))end
4.1042 + else Add (i', [], true, f, Cor ((d, ts), (id, pbl_ids' d ts)))
4.1043 + end)
4.1044 + end
4.1045 + end
4.1046 + | appl_add ctxt sel oris ppc pbt str =
4.1047 + case parseNEW ctxt str of
4.1048 + NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
4.1049 + | SOME t =>
4.1050 + case is_known ctxt sel oris t of
4.1051 + ("", ori', all) =>
4.1052 + (case is_notyet_input ctxt ppc all ori' pbt of
4.1053 + ("", itm) => Add itm
4.1054 + | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
4.1055 + | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
4.1056
4.1057 -(** add an item to the model; check wrt. oris and pbt **)
4.1058 -(* in contrary to oris<>[] below, this part handles user-input
4.1059 - extremely acceptive, i.e. accept input instead error-msg *)
4.1060 -fun appl_add ctxt sel [] ppc pbt ct =
4.1061 - let
4.1062 - val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
4.1063 - in
4.1064 - case parseNEW ctxt ct of
4.1065 - NONE => Add (i, [], false, sel, Syn ct)
4.1066 - | SOME t =>
4.1067 - let val (d, ts) = split_dts t;
4.1068 - in
4.1069 - if d = e_term
4.1070 - then Add (i, [], false, sel, Mis (dsc_unknown, hd ts))
4.1071 - else
4.1072 - (case find_first (eq1 d) pbt of
4.1073 - NONE => Add (i, [], true, sel, Sup (d,ts))
4.1074 - | SOME (f, (_, id)) =>
4.1075 - let fun eq2 d (i, _, _, _, itm_) =
4.1076 - d = (d_in itm_) andalso i <> 0;
4.1077 - in case find_first (eq2 d) ppc of
4.1078 - NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
4.1079 - | SOME (i', _, _, _, itm_) =>
4.1080 - if is_list_dsc d
4.1081 - then
4.1082 - let
4.1083 - val in_itm = ts_in itm_;
4.1084 - val ts' = union op = ts in_itm;
4.1085 - val i'' = if in_itm = [] then i else i';
4.1086 - in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts'))) end
4.1087 - else Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
4.1088 - end)
4.1089 - end
4.1090 - end
4.1091 - | appl_add ctxt sel oris ppc pbt str =
4.1092 - case parseNEW ctxt str of
4.1093 - NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
4.1094 - | SOME t =>
4.1095 - case is_known ctxt sel oris t of
4.1096 - ("", ori', all) =>
4.1097 - (case is_notyet_input ctxt ppc all ori' pbt of
4.1098 - ("", itm) => Add itm
4.1099 - | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
4.1100 - | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
4.1101 +(* make oris from args of the stac SubProblem and from pbt.
4.1102 + can this formal argument (of a model-pattern) be omitted in the arg-list
4.1103 + of a SubProblem ? see calcelems.sml 'type met ' *)
4.1104 +fun is_copy_named_idstr str =
4.1105 + case (rev o Symbol.explode) str of
4.1106 + "'" :: _ :: "'" :: _ =>
4.1107 + (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " T"); true)
4.1108 + | _ =>
4.1109 + (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " F"); false)
4.1110 +fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t
4.1111
4.1112 +(* should this formal argument (of a model-pattern) create a new identifier? *)
4.1113 +fun is_copy_named_generating_idstr str =
4.1114 + if is_copy_named_idstr str
4.1115 + then
4.1116 + case (rev o Symbol.explode) str of
4.1117 + "'" :: "'" :: "'" :: _ => false
4.1118 + | _ => true
4.1119 + else false
4.1120 +fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o free2str) t
4.1121
4.1122 -(** make oris from args of the stac SubProblem and from pbt **)
4.1123 -(* can this formal argument (of a model-pattern) be omitted in the arg-list
4.1124 - of a SubProblem ? see calcelems.sml 'type met ' *)
4.1125 -fun is_copy_named_idstr str =
4.1126 - case (rev o Symbol.explode) str of
4.1127 - "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
4.1128 - "is_copy_named_idstr: " ^ str ^ " T"); true)
4.1129 - | _ => (tracing ((strs2str o (rev o Symbol.explode))
4.1130 - "is_copy_named_idstr: " ^ str ^ " F"); false);
4.1131 -fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
4.1132 +(* split type-wrapper from scr-arg and build part of an ori;
4.1133 + an type-error is reported immediately, raises an exn,
4.1134 + subsequent handling of exn provides 2nd part of error message *)
4.1135 +fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
4.1136 + ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
4.1137 + SOME ((([1], str, dsc, (*[var]*)
4.1138 + split_dts' (dsc, var))): preori)(*:ori without leading #*))
4.1139 + handle e as TYPE _ =>
4.1140 + (tracing (dashs 70 ^ "\n"
4.1141 + ^ "*** ERROR while creating the items for the model of the ->problem\n"
4.1142 + ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
4.1143 + ^ "*** item (->description ->value): " ^ term2str dsc ^ " " ^ term2str var ^ "\n"
4.1144 + ^ "*** description: " ^ term_detail2str dsc
4.1145 + ^ "*** value: " ^ term_detail2str var
4.1146 + ^ "*** typeconstructor in script: " ^ term_detail2str ty
4.1147 + ^ "*** checked by theory: " ^ theory2str thy ^ "\n"
4.1148 + ^ "*** " ^ dots 66);
4.1149 + writeln (PolyML.makestring e);
4.1150 + reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
4.1151 + NONE))
4.1152 + | mtc _ _ t = error ("mtc: uncovered case with" ^ term2str t)
4.1153
4.1154 -(*.should this formal argument (of a model-pattern) create a new identifier?.*)
4.1155 -fun is_copy_named_generating_idstr str =
4.1156 - if is_copy_named_idstr str
4.1157 - then case (rev o Symbol.explode) str of
4.1158 - "'"::"'"::"'"::_ => false
4.1159 - | _ => true
4.1160 - else false;
4.1161 -fun is_copy_named_generating (_, (_, t)) =
4.1162 - (is_copy_named_generating_idstr o free2str) t;
4.1163 -
4.1164 -(*.split type-wrapper from scr-arg and build part of an ori;
4.1165 - an type-error is reported immediately, raises an exn,
4.1166 - subsequent handling of exn provides 2nd part of error message.*)
4.1167 -fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
4.1168 - (* val (thy, (str, (dsc, _)), (ty $ var)) =
4.1169 - (thy, p, a);
4.1170 - *)
4.1171 - (Thm.global_cterm_of thy (dsc $ var);(*type check*)
4.1172 - SOME ((([1], str, dsc, (*[var]*)
4.1173 - split_dts' (dsc, var))): preori)(*:ori without leading #*))
4.1174 - handle e as TYPE _ =>
4.1175 - (tracing (dashs 70 ^ "\n"
4.1176 - ^"*** ERROR while creating the items for the model of the ->problem\n"
4.1177 - ^"*** from the ->stac with ->typeconstructor in arglist:\n"
4.1178 - ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
4.1179 - ^"*** description: "^(term_detail2str dsc)
4.1180 - ^"*** value: "^(term_detail2str var)
4.1181 - ^"*** typeconstructor in script: "^(term_detail2str ty)
4.1182 - ^"*** checked by theory: "^(theory2str thy)^"\n"
4.1183 - ^"*** " ^ dots 66);
4.1184 - (*OldGoals.print_exn e; raises exn again*)
4.1185 - writeln (PolyML.makestring e);
4.1186 - reraise e;
4.1187 - (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
4.1188 - NONE);
4.1189 -
4.1190 -(*.match each pat of the model-pattern with an actual argument;
4.1191 - precondition: copy-named vars are filtered out.*)
4.1192 -fun matc thy ([]:pat list) _ (oris:preori list) = oris
4.1193 - | matc thy pbt [] _ =
4.1194 +(* match each pat of the model-pattern with an actual argument;
4.1195 + precondition: copy-named vars are filtered out *)
4.1196 +fun matc _ ([]:pat list) _ (oris:preori list) = oris
4.1197 + | matc _ pbt [] _ =
4.1198 (tracing (dashs 70);
4.1199 - error ("actual arg(s) missing for '"^pats2str pbt
4.1200 - ^"' i.e. should be 'copy-named' by '*_._'"))
4.1201 - | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
4.1202 - (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
4.1203 - (thy, pbt', ags, []);
4.1204 - (*recursion..*)
4.1205 - val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
4.1206 - (thy, pbt, ags, (oris @ [ori]));
4.1207 - *)
4.1208 + error ("actual arg(s) missing for '" ^ pats2str pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
4.1209 + | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
4.1210 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
4.1211 - else(*..del?*) let val opt = mtc thy p a;
4.1212 - in case opt of
4.1213 - (* val SOME ori = mtc thy p a;
4.1214 - *)
4.1215 - SOME ori => matc thy pbt ags (oris @ [ori])
4.1216 + else(*..del?*)
4.1217 + let val opt = mtc thy p a
4.1218 + in
4.1219 + case opt of
4.1220 + SOME ori => matc thy pbt ags (oris @ [ori])
4.1221 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
4.1222 - end;
4.1223 -(* run subp-rooteq.sml until Init_Proof before ...
4.1224 -> val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
4.1225 -> fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
4.1226 -
4.1227 - other vars as in mtc ..
4.1228 -> matc thy (drop_last pbt) ags [];
4.1229 -val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
4.1230 -
4.1231 -
4.1232 -(* generate a new variable "x_i" name from a related given one "x"
4.1233 - by use of oris relating "v_i_" (is_copy_named!) to "v_"
4.1234 - e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
4.1235 + end
4.1236
4.1237 (* generate a new variable "x_i" name from a related given one "x"
4.1238 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
4.1239 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
4.1240 but leave is_copy_named_generating as is, e.t. ss''' *)
4.1241 -fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
4.1242 +fun cpy_nam (pbt: pat list) (oris: preori list) (p as (field, (dsc, t)): pat) =
4.1243 (if is_copy_named_generating p
4.1244 then (*WN051014 kept strange old code ...*)
4.1245 - let fun sel (_,_,d,ts) = comp_ts (d, ts)
4.1246 - val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
4.1247 - val ext = (last_elem o drop_last o Symbol.explode o free2str) t
4.1248 - val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
4.1249 - val vals = map sel oris
4.1250 - val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
4.1251 - in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
4.1252 + let fun sel (_,_,d,ts) = comp_ts (d, ts)
4.1253 + val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
4.1254 + val ext = (last_elem o drop_last o Symbol.explode o free2str) t
4.1255 + val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
4.1256 + val vals = map sel oris
4.1257 + val cy_ext = (free2str o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
4.1258 + in ([1], field, dsc, [mk_free (type_of t) cy_ext]): preori end
4.1259 else ([1], field, dsc, [t])
4.1260 - )
4.1261 - handle _ => error ("cpy_nam: for "^(term2str t));
4.1262 + ) handle _ => error ("cpy_nam: for "^(term2str t))
4.1263
4.1264 -(*.match the actual arguments of a SubProblem with a model-pattern
4.1265 +(* match the actual arguments of a SubProblem with a model-pattern
4.1266 and create an ori list (in root-pbl created from formalization).
4.1267 expects ags:pats = 1:1, while copy-named are filtered out of pats;
4.1268 if no 1:1 the exn raised by matc/mtc and handled at call.
4.1269 - copy-named pats are appended in order to get them into the model-items.*)
4.1270 -fun match_ags thy (pbt:pat list) ags =
4.1271 - let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
4.1272 - val pbt' = filter_out is_copy_named pbt;
4.1273 - val cy = filter is_copy_named pbt;
4.1274 - val oris' = matc thy pbt' ags [];
4.1275 - val cy' = map (cpy_nam pbt' oris') cy;
4.1276 - val ors = add_id (oris' @ cy');
4.1277 - (*appended in order to get ^^^^^ into the model-items*)
4.1278 - in (map flattup ors):ori list end;
4.1279 + copy-named pats are appended in order to get them into the model-items *)
4.1280 +fun match_ags thy (pbt: pat list) ags =
4.1281 + let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_)
4.1282 + val pbt' = filter_out is_copy_named pbt
4.1283 + val cy = filter is_copy_named pbt
4.1284 + val oris' = matc thy pbt' ags []
4.1285 + val cy' = map (cpy_nam pbt' oris') cy
4.1286 + val ors = add_id (oris' @ cy') (*...appended in order to get into the model-items *)
4.1287 + in (map flattup ors): ori list end
4.1288
4.1289 -(*.report part of the error-msg which is not available in match_args.*)
4.1290 +(* report part of the error-msg which is not available in match_args *)
4.1291 fun match_ags_msg pI stac ags =
4.1292 - let (*val s = !show_types
4.1293 - val _ = show_types:= true*)
4.1294 - val pats = (#ppc o get_pbt) pI
4.1295 - val msg = (dots 70^"\n"
4.1296 - ^"*** problem "^strs2str pI^" has the ...\n"
4.1297 - ^"*** model-pattern "^pats2str pats^"\n"
4.1298 - ^"*** stac '"^term2str stac^"' has the ...\n"
4.1299 - ^"*** arg-list "^terms2str ags^"\n"
4.1300 - ^dashs 70)
4.1301 - (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
4.1302 - (*val _ = show_types:= s*)
4.1303 - in tracing msg end;
4.1304 + let
4.1305 + val pats = (#ppc o get_pbt) pI
4.1306 + val msg = (dots 70^"\n"
4.1307 + ^ "*** problem "^strs2str pI ^ " has the ...\n"
4.1308 + ^ "*** model-pattern "^pats2str pats ^ "\n"
4.1309 + ^ "*** stac '"^term2str stac ^ "' has the ...\n"
4.1310 + ^ "*** arg-list "^terms2str ags ^ "\n"
4.1311 + ^ dashs 70)
4.1312 + (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
4.1313 + in tracing msg end
4.1314
4.1315 -
4.1316 -(*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
4.1317 +(* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
4.1318 fun vars_of_pbl_ pbl_ =
4.1319 - let fun var_of_pbl_ (gfr,(dsc,t)) = t
4.1320 - in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
4.1321 + let
4.1322 + fun var_of_pbl_ (_, (_, t)) = t
4.1323 + in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end
4.1324 fun vars_of_pbl_' pbl_ =
4.1325 - let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
4.1326 - in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
4.1327 + let
4.1328 + fun var_of_pbl_ (_, (_, t)) = t: term
4.1329 + in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
4.1330
4.1331 fun overwrite_ppc thy itm ppc =
4.1332 let
4.1333 - fun repl ppc' (_,_,_,_,itm_) [] =
4.1334 - error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
4.1335 - " not found")
4.1336 - | repl ppc' itm (p::ppc) =
4.1337 - if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
4.1338 - else repl (ppc' @ [p]) itm ppc
4.1339 - in repl [] itm ppc end;
4.1340 + fun repl _ (_, _, _, _, itm_) [] =
4.1341 + error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^ " not found")
4.1342 + | repl ppc' itm (p :: ppc) =
4.1343 + if (#1 itm) = (#1 (p: itm))
4.1344 + then ppc' @ [itm] @ ppc
4.1345 + else repl (ppc' @ [p]) itm ppc
4.1346 + in repl [] itm ppc end
4.1347
4.1348 -(*10.3.00: insert the already compiled itm into model;
4.1349 +(* 10.3.00: insert the already compiled itm into model;
4.1350 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
4.1351 -(* val ppc=pbl;
4.1352 - *)
4.1353 fun insert_ppc thy itm ppc =
4.1354 - let
4.1355 - fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
4.1356 - | eq_untouched _ _ = false;
4.1357 - val ppc' =
4.1358 - (
4.1359 - (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
4.1360 - case seek_ppc (#1 itm) ppc of
4.1361 - (* val SOME xxx = seek_ppc (#1 itm) ppc;
4.1362 - *)
4.1363 - SOME _ => (*itm updated in is_notyet_input WN.11.03*)
4.1364 - overwrite_ppc thy itm ppc
4.1365 - | NONE => (ppc @ [itm]));
4.1366 - in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
4.1367 + let
4.1368 + fun eq_untouched d ((0, _, _, _, itm_): itm) = (d = d_in itm_)
4.1369 + | eq_untouched _ _ = false
4.1370 + val ppc' = case seek_ppc (#1 itm) ppc of
4.1371 + SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
4.1372 + | NONE => (ppc @ [itm])
4.1373 + in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end
4.1374
4.1375 -(*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
4.1376 -fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
4.1377 +fun eq_dsc ((_, _, _, _, itm_): itm, (_, _, _, _, iitm_): itm) = (d_in itm_ = d_in iitm_)
4.1378
4.1379 -fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
4.1380 - (d_in itm_) = (d_in iitm_);
4.1381 -(*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
4.1382 - handles superfluous items carelessly*)
4.1383 -fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
4.1384 -(* val eee = op=;
4.1385 - > gen_ins' eee (4,[1,3,5,7]);
4.1386 -val it = [1, 3, 5, 7, 4] : int list*)
4.1387 +(* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
4.1388 + handles superfluous items carelessly *)
4.1389 +fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
4.1390
4.1391 +(* output the headline to a ppc *)
4.1392 +fun header p_ pI mI =
4.1393 + case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
4.1394 + | Met => Method mI
4.1395 + | pos => error ("header called with "^ pos_2str pos)
4.1396
4.1397 -(*. output the headline to a ppc .*)
4.1398 -fun header p_ pI mI =
4.1399 - case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
4.1400 - | Met => Method mI
4.1401 - | pos => error ("header called with "^ pos_2str pos);
4.1402 -
4.1403 -
4.1404 -fun specify_additem sel (ct,_) (p, Met) c pt =
4.1405 +fun specify_additem sel (ct, _) (p, Met) _ pt =
4.1406 + let
4.1407 + val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
4.1408 + (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
4.1409 + => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
4.1410 + | _ => error "specify_additem: uncovered case of get_obj I pt p"
4.1411 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
4.1412 + val cpI = if pI = e_pblID then pI' else pI
4.1413 + val cmI = if mI = e_metID then mI' else mI
4.1414 + val {ppc, pre, prls, ...} = get_met cmI
4.1415 + in
4.1416 + case appl_add ctxt sel oris met ppc ct of
4.1417 + Add itm => (*..union old input *)
4.1418 + let
4.1419 + val met' = insert_ppc thy itm met
4.1420 + val arg = case sel of
4.1421 + "#Given" => Add_Given' (ct, met')
4.1422 + | "#Find" => Add_Find' (ct, met')
4.1423 + | "#Relate"=> Add_Relation'(ct, met')
4.1424 + | str => error ("specify_additem: uncovered case with " ^ str)
4.1425 + val (p, Met, pt') = case generate1 thy arg (Uistate, ctxt) (p, Met) pt of
4.1426 + ((p, Met), _, _, pt') => (p, Met, pt')
4.1427 + | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"
4.1428 + val pre' = check_preconds thy prls pre met'
4.1429 + val pb = foldl and_ (true, map fst pre')
4.1430 + val (p_, nxt) =
4.1431 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
4.1432 + ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
4.1433 + in ((p, p_), ((p, p_), Uistate),
4.1434 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
4.1435 + (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
4.1436 + end
4.1437 + | Err msg =>
4.1438 + let
4.1439 + val pre' = check_preconds thy prls pre met
4.1440 + val pb = foldl and_ (true, map fst pre')
4.1441 + val (p_, nxt) =
4.1442 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
4.1443 + ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
4.1444 + in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
4.1445 + end
4.1446 + | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
4.1447 let
4.1448 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
4.1449 - probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
4.1450 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
4.1451 - val cpI = if pI = e_pblID then pI' else pI;
4.1452 - val cmI = if mI = e_metID then mI' else mI;
4.1453 - val {ppc,pre,prls,...} = get_met cmI;
4.1454 - in
4.1455 - case appl_add ctxt sel oris met ppc ct of
4.1456 - Add itm (*..union old input *) =>
4.1457 - let
4.1458 - val met' = insert_ppc thy itm met;
4.1459 - val ((p, Met), _, _, pt') =
4.1460 - generate1 thy (case sel of
4.1461 - "#Given" => Add_Given' (ct, met')
4.1462 - | "#Find" => Add_Find' (ct, met')
4.1463 - | "#Relate"=> Add_Relation'(ct, met'))
4.1464 - (Uistate, ctxt) (p, Met) pt
4.1465 - val pre' = check_preconds thy prls pre met'
4.1466 - val pb = foldl and_ (true, map fst pre')
4.1467 - val (p_, nxt) =
4.1468 - nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
4.1469 - ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
4.1470 - in ((p, p_), ((p, p_), Uistate),
4.1471 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
4.1472 - (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
4.1473 - end
4.1474 - | Err msg =>
4.1475 - let
4.1476 - val pre' = check_preconds thy prls pre met
4.1477 - val pb = foldl and_ (true, map fst pre')
4.1478 - val (p_, nxt) =
4.1479 - nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
4.1480 - ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
4.1481 - in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
4.1482 - end
4.1483 -
4.1484 - | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt =
4.1485 - let
4.1486 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
4.1487 - probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
4.1488 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
4.1489 - val cpI = if pI = e_pblID then pI' else pI;
4.1490 - val cmI = if mI = e_metID then mI' else mI;
4.1491 - val {ppc,where_,prls,...} = get_pbt cpI;
4.1492 + val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
4.1493 + (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
4.1494 + => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
4.1495 + | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
4.1496 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
4.1497 + val cpI = if pI = e_pblID then pI' else pI
4.1498 + val cmI = if mI = e_metID then mI' else mI
4.1499 + val {ppc, where_, prls, ...} = get_pbt cpI
4.1500 in
4.1501 case appl_add ctxt sel oris pbl ppc ct of
4.1502 - Add itm (*..union old input *) =>
4.1503 + Add itm => (*..union old input *)
4.1504 let
4.1505 val pbl' = insert_ppc thy itm pbl
4.1506 - val ((p, Pbl), _, _, pt') =
4.1507 - generate1 thy (case sel of
4.1508 - "#Given" => Add_Given' (ct, pbl')
4.1509 - | "#Find" => Add_Find' (ct, pbl')
4.1510 - | "#Relate"=> Add_Relation'(ct, pbl'))
4.1511 - (Uistate, ctxt) (p,Pbl) pt
4.1512 + val arg = case sel of
4.1513 + "#Given" => Add_Given' (ct, pbl')
4.1514 + | "#Find" => Add_Find' (ct, pbl')
4.1515 + | "#Relate"=> Add_Relation'(ct, pbl')
4.1516 + | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
4.1517 + val ((p, Pbl), _, _, pt') = generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
4.1518 val pre = check_preconds thy prls where_ pbl'
4.1519 val pb = foldl and_ (true, map fst pre)
4.1520 val (p_, nxt) =
4.1521 - nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
4.1522 - (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
4.1523 - val ppc = if p_= Pbl then pbl' else met;
4.1524 - in ((p,p_), ((p,p_),Uistate),
4.1525 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
4.1526 - (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt,Safe,pt')
4.1527 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
4.1528 + val ppc = if p_= Pbl then pbl' else met
4.1529 + in
4.1530 + ((p, p_), ((p, p_), Uistate),
4.1531 + Form' (PpcKF (0, EdUndef, (length p), Nundef,
4.1532 + (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt, Safe, pt')
4.1533 end
4.1534 | Err msg =>
4.1535 let
4.1536 val pre = check_preconds thy prls where_ pbl
4.1537 val pb = foldl and_ (true, map fst pre)
4.1538 val (p_, nxt) =
4.1539 - nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
4.1540 - (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
4.1541 - in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
4.1542 - end;
4.1543 + nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
4.1544 + (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
4.1545 + in ((p, p_), ((p, p_), Uistate), Error' (Error_ msg), nxt, Safe,pt) end
4.1546 + end
4.1547
4.1548 -fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
4.1549 +fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
4.1550 let (* either """"""""""""""" all empty or complete *)
4.1551 - val thy = assoc_thy dI';
4.1552 + val thy = assoc_thy dI'
4.1553 val (oris, ctxt) =
4.1554 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
4.1555 then ([], e_ctxt)
4.1556 else pI' |> #ppc o get_pbt |> prep_ori fmz thy
4.1557 - val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
4.1558 + val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec')
4.1559 (oris, (dI',pI',mI'), e_term)
4.1560 val pt = update_ctxt pt [] ctxt
4.1561 - val {ppc, prls, where_, ...} = get_pbt pI'
4.1562 - val (pbl, pre, pb) = ([], [], false)
4.1563 + val (pbl, pre) = ([], [])
4.1564 in
4.1565 case mI' of
4.1566 ["no_met"] =>
4.1567 (([], Pbl), (([], Pbl), Uistate),
4.1568 - Form' (PpcKF (0, EdUndef, (length []), Nundef,
4.1569 - (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
4.1570 + Form' (PpcKF (0, EdUndef, (length []), Nundef, (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
4.1571 Refine_Tacitly pI', Safe, pt)
4.1572 | _ =>
4.1573 (([], Pbl), (([], Pbl), Uistate),
4.1574 - Form' (PpcKF (0, EdUndef, (length []), Nundef,
4.1575 - (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
4.1576 + Form' (PpcKF (0, EdUndef, (length []), Nundef, (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
4.1577 Model_Problem, Safe, pt)
4.1578 - end
4.1579 -
4.1580 - (*ONLY for STARTING modeling phase*)
4.1581 - | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
4.1582 - let
4.1583 - val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_), ctxt, ...}) = get_obj I pt p
4.1584 - val thy' = if dI = e_domID then dI' else dI
4.1585 - val thy = assoc_thy thy'
4.1586 - val {ppc,prls,where_,...} = get_pbt pI'
4.1587 - val pre = check_preconds thy prls where_ pbl
4.1588 - val pb = foldl and_ (true, map fst pre)
4.1589 - val ((p,_),_,_,pt) =
4.1590 - generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
4.1591 - val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
4.1592 - (ppc,(#ppc o get_met) mI') (dI',pI',mI');
4.1593 - in ((p, Pbl), ((p, p_), Uistate),
4.1594 - Form' (PpcKF (0, EdUndef, length p, Nundef,
4.1595 - (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
4.1596 - nxt, Safe, pt)
4.1597 - end
4.1598 -
4.1599 - (*. called only if no_met is specified .*)
4.1600 - | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
4.1601 + end
4.1602 + (* ONLY for STARTING modeling phase *)
4.1603 + | specify (Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt =
4.1604 + let
4.1605 + val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
4.1606 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
4.1607 + (oris, dI',pI',mI', dI, ctxt)
4.1608 + | _ => error "specify (Model_Problem': uncovered case get_obj"
4.1609 + val thy' = if dI = e_domID then dI' else dI
4.1610 + val thy = assoc_thy thy'
4.1611 + val {ppc, prls, where_, ...} = get_pbt pI'
4.1612 + val pre = check_preconds thy prls where_ pbl
4.1613 + val pb = foldl and_ (true, map fst pre)
4.1614 + val ((p, _), _, _, pt) =
4.1615 + generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
4.1616 + val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
4.1617 + (ppc,(#ppc o get_met) mI') (dI',pI',mI');
4.1618 + in
4.1619 + ((p, Pbl), ((p, p_), Uistate),
4.1620 + Form' (PpcKF (0, EdUndef, length p, Nundef, (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
4.1621 + nxt, Safe, pt)
4.1622 + end
4.1623 + (* called only if no_met is specified *)
4.1624 + | specify (Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt =
4.1625 let
4.1626 - val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ctxt, ...}) = get_obj I pt p;
4.1627 - val {prls,met,ppc,thy,where_,...} = get_pbt pIre
4.1628 - val (domID, metID) =
4.1629 - (string_of_thy thy, if length met = 0 then e_metID else hd met)
4.1630 - val ((p,_),_,_,pt) =
4.1631 - generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
4.1632 - (Uistate, ctxt) pos pt
4.1633 - val (pbl, pre, pb) = ([], [], false)
4.1634 + val (dI', ctxt) = case get_obj I pt p of
4.1635 + PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
4.1636 + | _ => error "specify (Refine_Tacitly': uncovered case get_obj"
4.1637 + val {met, thy,...} = get_pbt pIre
4.1638 + val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
4.1639 + val ((p,_), _, _, pt) =
4.1640 + generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
4.1641 + val (pbl, pre, _) = ([], [], false)
4.1642 in ((p, Pbl), (pos, Uistate),
4.1643 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
4.1644 - (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
4.1645 + Form' (PpcKF (0, EdUndef, length p, Nundef, (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
4.1646 Model_Problem, Safe, pt)
4.1647 end
4.1648 -
4.1649 - | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
4.1650 + | specify (Refine_Problem' rfd) pos _ pt =
4.1651 let
4.1652 val ctxt = get_ctxt pt pos
4.1653 - val (pos,_,_,pt) =
4.1654 + val (pos, _, _, pt) =
4.1655 generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
4.1656 - in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
4.1657 - Model_Problem, Safe, pt)
4.1658 + in
4.1659 + (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Problems (RefinedKF rfd), Model_Problem, Safe, pt)
4.1660 end
4.1661 (*WN110515 initialise ctxt again from itms and add preconds*)
4.1662 - | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
4.1663 + | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
4.1664 let
4.1665 - val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
4.1666 - meth=met, ctxt, ...}) = get_obj I pt p;
4.1667 + val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of
4.1668 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
4.1669 + (oris, dI', pI', mI', dI, mI, ctxt, met)
4.1670 + | _ => error "specify (Specify_Problem': uncovered case get_obj"
4.1671 val thy = assoc_thy dI
4.1672 - val ((p,Pbl),_,_,pt)=
4.1673 - generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt
4.1674 - val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
4.1675 - val mI'' = if mI=e_metID then mI' else mI;
4.1676 - val (_, nxt) =
4.1677 - nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
4.1678 - ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
4.1679 - in ((p,Pbl), (pos,Uistate),
4.1680 + val (p, Pbl, pt) =
4.1681 + case generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
4.1682 + ((p, Pbl), _, _, pt) => (p, Pbl, pt)
4.1683 + | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
4.1684 + val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
4.1685 + val mI'' = if mI=e_metID then mI' else mI
4.1686 + val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o get_pbt) pI,
4.1687 + (#ppc o get_met) mI'') (dI, pI, mI);
4.1688 + in
4.1689 + ((p,Pbl), (pos,Uistate),
4.1690 Form' (PpcKF (0,EdUndef,(length p),Nundef, (Problem pI, itms2itemppc dI'' itms pre))),
4.1691 - nxt, Safe, pt)
4.1692 + nxt, Safe, pt)
4.1693 end
4.1694 (*WN110515 initialise ctxt again from itms and add preconds*)
4.1695 - | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
4.1696 + | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) _ pt =
4.1697 let
4.1698 - val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
4.1699 - meth=met, ctxt, ...}) = get_obj I pt p;
4.1700 + val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
4.1701 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
4.1702 + (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
4.1703 + | _ => error "specify (Specify_Problem': uncovered case get_obj"
4.1704 val {ppc,pre,prls,...} = get_met mID
4.1705 val thy = assoc_thy dI
4.1706 - val oris = add_field' thy ppc oris;
4.1707 - val dI'' = if dI=e_domID then dI' else dI;
4.1708 - val pI'' = if pI = e_pblID then pI' else pI;
4.1709 - val met = if met=[] then pbl else met;
4.1710 - val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
4.1711 + val oris = add_field' thy ppc oris
4.1712 + val dI'' = if dI=e_domID then dI' else dI
4.1713 + val pI'' = if pI = e_pblID then pI' else pI
4.1714 + val met = if met = [] then pbl else met
4.1715 + val (_, (itms, pre')) = match_itms_oris thy met (ppc, pre, prls ) oris
4.1716 val (pos, _, _, pt) =
4.1717 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
4.1718 - val (_,nxt) =
4.1719 - nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
4.1720 - ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
4.1721 - in (pos, (pos,Uistate),
4.1722 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
4.1723 - (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
4.1724 - nxt, Safe, pt)
4.1725 + val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
4.1726 + ((#ppc o get_pbt) pI'', ppc) (dI'', pI'', mID)
4.1727 + in
4.1728 + (pos, (pos,Uistate),
4.1729 + Form' (PpcKF (0, EdUndef, length p, Nundef, (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
4.1730 + nxt, Safe, pt)
4.1731 end
4.1732 -
4.1733 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
4.1734 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
4.1735 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
4.1736 -
4.1737 - | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
4.1738 + | specify (Specify_Theory' domID) (pos as (p,p_)) _ pt =
4.1739 let
4.1740 val p_ = case p_ of Met => Met | _ => Pbl
4.1741 - val thy = assoc_thy domID;
4.1742 - val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
4.1743 - probl=pbl, spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
4.1744 - val mppc = case p_ of Met => met | _ => pbl;
4.1745 - val cpI = if pI = e_pblID then pI' else pI;
4.1746 - val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
4.1747 - val cmI = if mI = e_metID then mI' else mI;
4.1748 - val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
4.1749 - val pre =
4.1750 - case p_ of
4.1751 - Met => (check_preconds thy mer mwh met)
4.1752 - | _ => (check_preconds thy per pwh pbl)
4.1753 + val thy = assoc_thy domID
4.1754 + val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
4.1755 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
4.1756 + (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
4.1757 + | _ => error "specify (Specify_Theory': uncovered case get_obj"
4.1758 + val mppc = case p_ of Met => met | _ => pbl
4.1759 + val cpI = if pI = e_pblID then pI' else pI
4.1760 + val {prls = per, ppc, where_ = pwh, ...} = get_pbt cpI
4.1761 + val cmI = if mI = e_metID then mI' else mI
4.1762 + val {prls = mer, ppc = mpc, pre= mwh, ...} = get_met cmI
4.1763 + val pre = case p_ of
4.1764 + Met => (check_preconds thy mer mwh met)
4.1765 + | _ => (check_preconds thy per pwh pbl)
4.1766 val pb = foldl and_ (true, map fst pre)
4.1767 in
4.1768 if domID = dI
4.1769 then
4.1770 - let val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
4.1771 - (pbl,met) (ppc,mpc) (dI,pI,mI);
4.1772 - in ((p,p_), (pos,Uistate),
4.1773 - Form'(PpcKF (0,EdUndef,(length p), Nundef,
4.1774 - (header p_ pI cmI, itms2itemppc thy mppc pre))),
4.1775 - nxt,Safe,pt)
4.1776 + let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
4.1777 + in
4.1778 + ((p, p_), (pos, Uistate),
4.1779 + Form'(PpcKF (0, EdUndef, length p, Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
4.1780 + nxt, Safe, pt)
4.1781 end
4.1782 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
4.1783 let
4.1784 - val ((p,p_),_,_,pt) =
4.1785 - generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
4.1786 - val (p_,nxt) =
4.1787 - nxt_spec p_ pb oris (dI',pI',mI') (pbl,met) (ppc,mpc) (domID,pI,mI);
4.1788 - in ((p,p_), (pos,Uistate),
4.1789 - Form' (PpcKF (0, EdUndef, (length p),Nundef,
4.1790 - (header p_ pI cmI, itms2itemppc thy mppc pre))),
4.1791 - nxt, Safe,pt)
4.1792 + val ((p, p_), _, _, pt) = generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
4.1793 + val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
4.1794 + in
4.1795 + ((p,p_), (pos,Uistate),
4.1796 + Form' (PpcKF (0, EdUndef, length p, Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
4.1797 + nxt, Safe, pt)
4.1798 end
4.1799 end
4.1800 -
4.1801 - | specify m' _ _ _ =
4.1802 - error ("specify: not impl. for " ^ tac_2str m');
4.1803 + | specify m' _ _ _ = error ("specify: not impl. for " ^ tac_2str m')
4.1804
4.1805 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
4.1806 -- for input from scratch*)
4.1807 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
4.1808 - let
4.1809 - val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
4.1810 - probl=pbl,spec=(dI,pI,_), ctxt, ...}) = get_obj I pt p;
4.1811 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
4.1812 - val cpI = if pI = e_pblID then pI' else pI;
4.1813 - in
4.1814 - case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
4.1815 - Add itm (*..union old input *) =>
4.1816 - let
4.1817 - (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
4.1818 - val pbl' = insert_ppc thy itm pbl
4.1819 - val (tac,tac_) =
4.1820 - case sel of
4.1821 - "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
4.1822 - | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
4.1823 - | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
4.1824 - val ((p,Pbl),c,_,pt') =
4.1825 - generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt
4.1826 - in ([(tac,tac_,((p,Pbl),(Uistate, ctxt)))], c, (pt',(p,Pbl))):calcstate'
4.1827 - end
4.1828 - | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
4.1829 - FIXME ..and dont abuse a tactic for that purpose*)
4.1830 - ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
4.1831 - (e_pos', (e_istate, e_ctxt)))], [], ptp)
4.1832 - end
4.1833 + let
4.1834 + val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of
4.1835 + PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
4.1836 + (oris, dI', pI', dI, pI, pbl, ctxt)
4.1837 + | _ => error "specify (Specify_Theory': uncovered case get_obj"
4.1838 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
4.1839 + val cpI = if pI = e_pblID then pI' else pI;
4.1840 + in
4.1841 + case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
4.1842 + Add itm (*..union old input *) =>
4.1843 + let
4.1844 + val pbl' = insert_ppc thy itm pbl
4.1845 + val (tac, tac_) = case sel of
4.1846 + "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
4.1847 + | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
4.1848 + | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
4.1849 + | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
4.1850 + val (p, Pbl, c, pt') = case generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
4.1851 + ((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
4.1852 + | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
4.1853 + in
4.1854 + ([(tac, tac_, ((p, Pbl), (Uistate, ctxt)))], c, (pt', (p, Pbl))) : calcstate'
4.1855 + end
4.1856 + | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
4.1857 + FIXME ..and dont abuse a tactic for that purpose*)
4.1858 + ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
4.1859 + (e_pos', (e_istate, e_ctxt)))], [], ptp)
4.1860 + end
4.1861 + | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
4.1862 + let
4.1863 + val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of
4.1864 + PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
4.1865 + (oris, dI', mI', dI, mI, met, ctxt)
4.1866 + | _ => error "nxt_specif_additem Met: uncovered case get_obj"
4.1867 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
4.1868 + val cmI = if mI = e_metID then mI' else mI;
4.1869 + in
4.1870 + case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
4.1871 + Add itm (*..union old input *) =>
4.1872 + let
4.1873 + val met' = insert_ppc thy itm met;
4.1874 + val (tac,tac_) = case sel of
4.1875 + "#Given" => (Add_Given ct, Add_Given' (ct, met'))
4.1876 + | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
4.1877 + | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
4.1878 + | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
4.1879 + val (p, Met, c, pt') = case generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
4.1880 + ((p, Met), c, _, pt') => (p, Met, c, pt')
4.1881 + | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
4.1882 + in
4.1883 + ([(tac, tac_, ((p, Met), (Uistate, ctxt)))], c, (pt', (p, Met)))
4.1884 + end
4.1885 + | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
4.1886 + end
4.1887 + | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)
4.1888
4.1889 - | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
4.1890 - let
4.1891 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
4.1892 - probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
4.1893 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
4.1894 - val cmI = if mI = e_metID then mI' else mI;
4.1895 - in
4.1896 - case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
4.1897 - Add itm (*..union old input *) =>
4.1898 - let
4.1899 - val met' = insert_ppc thy itm met;
4.1900 - val (tac,tac_) =
4.1901 - case sel of
4.1902 - "#Given" => (Add_Given ct, Add_Given' (ct, met'))
4.1903 - | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
4.1904 - | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
4.1905 - val ((p,Met),c,_,pt') =
4.1906 - generate1 thy tac_ (Uistate, ctxt) (p,Met) pt
4.1907 - in ([(tac,tac_,((p,Met), (Uistate, ctxt)))], c, (pt',(p,Met))) end
4.1908 - | Err msg => ([(*tacis*)], [], ptp)
4.1909 - (*nxt_me collects tacis until not hide; here just no progress*)
4.1910 - end;
4.1911 +fun ori2Coritm (pbt : pat list) ((i, v, f, d, ts) : ori) =
4.1912 + ((i, v, true, f, Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts))) : itm)
4.1913 + handle _ => ((i, v, true, f, Cor ((d, ts), (d, ts))) : itm)
4.1914 + (*dsc in oris, but not in pbl pat list: keep this dsc*)
4.1915
4.1916 -fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
4.1917 - (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
4.1918 - handle _ => error ("ori2Coritm: dsc "^
4.1919 - term2str d^
4.1920 - "in ori, but not in pbt")
4.1921 - ,ts))):itm;
4.1922 -fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
4.1923 - ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
4.1924 - (find_first (eq1 d))) pbt,ts))):itm)
4.1925 - handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
4.1926 - ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
4.1927 -
4.1928 -
4.1929 -(*filter out oris which have same description in itms*)
4.1930 +(* filter out oris which have same description in itms *)
4.1931 fun filter_outs oris [] = oris
4.1932 | filter_outs oris (i::itms) =
4.1933 - let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
4.1934 - (#4:ori -> term)) oris;
4.1935 - in filter_outs ors itms end;
4.1936 + let
4.1937 + val ors = filter_out ((curry op = ((d_in o #5) (i:itm))) o (#4 : ori -> term)) oris
4.1938 + in
4.1939 + filter_outs ors itms
4.1940 + end
4.1941
4.1942 -fun memI a b = member op = a b;
4.1943 -(*filter oris which are in pbt, too*)
4.1944 +(* filter oris which are in pbt, too *)
4.1945 fun filter_pbt oris pbt =
4.1946 - let val dscs = map (fst o snd) pbt
4.1947 - in filter ((memI dscs) o (#4: ori -> term)) oris end;
4.1948 + let
4.1949 + val dscs = map (fst o snd) pbt
4.1950 + in
4.1951 + filter ((member op= dscs) o (#4 : ori -> term)) oris
4.1952 + end
4.1953
4.1954 -(*.combine itms from pbl + met and complete them wrt. pbt.*)
4.1955 -(*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
4.1956 -local infix mem;
4.1957 -fun x mem [] = false
4.1958 - | x mem (y :: ys) = x = y orelse x mem ys;
4.1959 -in
4.1960 -fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
4.1961 -(* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
4.1962 - *)
4.1963 - let val vat = max_vt pits;
4.1964 - val itms = pits @
4.1965 - (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
4.1966 - val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
4.1967 - val os = filter_outs ors itms;
4.1968 - (*WN.12.03?: does _NOT_ add itms from met ?!*)
4.1969 - in itms @ (map (ori2Coritm met) os) end
4.1970 -end;
4.1971 +(* combine itms from pbl + met and complete them wrt. pbt *)
4.1972 +(* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
4.1973 +fun complete_metitms (oris : ori list) (pits : itm list) (mits: itm list) met =
4.1974 + let
4.1975 + val vat = max_vt pits;
4.1976 + val itms = pits @ (filter ((member_swap op = vat) o (#2 : itm -> int list)) mits)
4.1977 + val ors = filter ((member_swap op= vat) o (#2 : ori -> int list)) oris
4.1978 + val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
4.1979 + in
4.1980 + itms @ (map (ori2Coritm met) os)
4.1981 + end
4.1982
4.1983 +(* complete model and guard of a calc-head *)
4.1984 +fun complete_mod_ (oris, mpc, ppc, probl) =
4.1985 + let
4.1986 + val pits = filter_out ((curry op= false) o (#3 : itm -> bool)) probl
4.1987 + val vat = if probl = [] then 1 else max_vt probl
4.1988 + val pors = filter ((member_swap op = vat) o (#2 : ori -> int list)) oris
4.1989 + val pors = filter_outs pors pits (*which are in pbl already*)
4.1990 + val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
4.1991 + val pits = pits @ (map (ori2Coritm ppc) pors)
4.1992 + val mits = complete_metitms oris pits [] mpc
4.1993 + in (pits, mits) end
4.1994
4.1995 +fun some_spec ((odI, opI, omI) : spec) ((dI, pI, mI) : spec) =
4.1996 + (if dI = e_domID then odI else dI,
4.1997 + if pI = e_pblID then opI else pI,
4.1998 + if mI = e_metID then omI else mI) : spec
4.1999
4.2000 -(*.complete model and guard of a calc-head .*)
4.2001 -local infix mem;
4.2002 -fun x mem [] = false
4.2003 - | x mem (y :: ys) = x = y orelse x mem ys;
4.2004 -in
4.2005 -fun complete_mod_ (oris, mpc, ppc, probl) =
4.2006 - let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
4.2007 - val vat = if probl = [] then 1 else max_vt probl
4.2008 - val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
4.2009 - val pors = filter_outs pors pits (*which are in pbl already*)
4.2010 - val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
4.2011 -
4.2012 - val pits = pits @ (map (ori2Coritm ppc) pors)
4.2013 - val mits = complete_metitms oris pits [] mpc
4.2014 - in (pits, mits) end
4.2015 -end;
4.2016 -
4.2017 -fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
4.2018 - (if dI = e_domID then odI else dI,
4.2019 - if pI = e_pblID then opI else pI,
4.2020 - if mI = e_metID then omI else mI):spec;
4.2021 -
4.2022 -
4.2023 -(*.find a next applicable tac (for calcstate) and update ptree
4.2024 - (for ev. finding several more tacs due to hide).*)
4.2025 -(*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
4.2026 -(*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
4.2027 -(*WN.24.10.03 fun nxt_solv = ...................................??*)
4.2028 -fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
4.2029 +(* find a next applicable tac (for calcstate) and update ptree
4.2030 + (for ev. finding several more tacs due to hide) *)
4.2031 +(* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
4.2032 +(* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
4.2033 +(* WN.24.10.03 fun nxt_solv = ...................................?? *)
4.2034 +fun nxt_specif (tac as Model_Problem) (pt, pos as (p, _)) =
4.2035 let
4.2036 - val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p
4.2037 + val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
4.2038 + PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
4.2039 + | _ => error "nxt_specif Model_Problem; uncovered case get_obj"
4.2040 val (dI, pI, mI) = some_spec ospec spec
4.2041 val thy = assoc_thy dI
4.2042 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
4.2043 @@ -1343,525 +970,426 @@
4.2044 val pbl = init_pbl ppc (* fill in descriptions *)
4.2045 (*----------------if you think, this should be done by the Dialog
4.2046 in the java front-end, search there for WN060225-modelProblem----*)
4.2047 - val (pbl, met) =
4.2048 - case cas of NONE => (pbl, [])
4.2049 - | _ => complete_mod_ (oris, mpc, ppc, probl)
4.2050 + val (pbl, met) = case cas of
4.2051 + NONE => (pbl, [])
4.2052 + | _ => complete_mod_ (oris, mpc, ppc, probl)
4.2053 (*----------------------------------------------------------------*)
4.2054 val tac_ = Model_Problem' (pI, pbl, met)
4.2055 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, ctxt) pos pt
4.2056 - in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
4.2057 -
4.2058 + in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
4.2059 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
4.2060 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
4.2061 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
4.2062 -
4.2063 (*. called only if no_met is specified .*)
4.2064 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
4.2065 - let
4.2066 - val (PblObj {origin = (oris, (dI,_,_),_), ctxt, ...}) = get_obj I pt p
4.2067 - val opt = refine_ori oris pI
4.2068 - in
4.2069 - case opt of
4.2070 - SOME pI' =>
4.2071 - let
4.2072 - val {met,ppc,...} = get_pbt pI'
4.2073 - val pbl = init_pbl ppc
4.2074 - (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
4.2075 - val mI = if length met = 0 then e_metID else hd met
4.2076 - val thy = assoc_thy dI
4.2077 - val (pos,c,_,pt) =
4.2078 - generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
4.2079 - (Uistate, ctxt) pos pt
4.2080 - in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
4.2081 - (pos, (Uistate, e_ctxt)))], c, (pt,pos))
4.2082 - end
4.2083 - | NONE => ([], [], ptp)
4.2084 - end
4.2085 -
4.2086 + let
4.2087 + val (oris, dI, ctxt) = case get_obj I pt p of
4.2088 + (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
4.2089 + | _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj"
4.2090 + val opt = refine_ori oris pI
4.2091 + in
4.2092 + case opt of
4.2093 + SOME pI' =>
4.2094 + let
4.2095 + val {met, ...} = get_pbt pI'
4.2096 + (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
4.2097 + val mI = if length met = 0 then e_metID else hd met
4.2098 + val thy = assoc_thy dI
4.2099 + val (pos, c, _, pt) =
4.2100 + generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
4.2101 + in
4.2102 + ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
4.2103 + (pos, (Uistate, e_ctxt)))], c, (pt,pos))
4.2104 + end
4.2105 + | NONE => ([], [], ptp)
4.2106 + end
4.2107 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
4.2108 - let
4.2109 - val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), probl, ctxt, ...}) = get_obj I pt p
4.2110 - val thy = if dI' = e_domID then dI else dI'
4.2111 - in
4.2112 - case refine_pbl (assoc_thy thy) pI probl of
4.2113 - NONE => ([], [], ptp)
4.2114 - | SOME (rfd as (pI',_)) =>
4.2115 - let
4.2116 - val (pos,c,_,pt) = generate1 (assoc_thy thy)
4.2117 - (Refine_Problem' rfd) (Uistate, ctxt) pos pt
4.2118 - in ([(Refine_Problem pI, Refine_Problem' rfd,
4.2119 - (pos, (Uistate, e_ctxt)))], c, (pt,pos))
4.2120 - end
4.2121 - end
4.2122 -
4.2123 + let
4.2124 + val (dI, dI', probl, ctxt) = case get_obj I pt p of
4.2125 + PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
4.2126 + (dI, dI', probl, ctxt)
4.2127 + | _ => error "nxt_specif Refine_Problem: uncovered case get_obj"
4.2128 + val thy = if dI' = e_domID then dI else dI'
4.2129 + in
4.2130 + case refine_pbl (assoc_thy thy) pI probl of
4.2131 + NONE => ([], [], ptp)
4.2132 + | SOME rfd =>
4.2133 + let
4.2134 + val (pos,c,_,pt) = generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
4.2135 + in
4.2136 + ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))
4.2137 + end
4.2138 + end
4.2139 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
4.2140 - let
4.2141 - val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...}) = get_obj I pt p;
4.2142 - val thy = assoc_thy (if dI' = e_domID then dI else dI');
4.2143 - val {ppc,where_,prls,...} = get_pbt pI
4.2144 - val pbl as (_,(itms,_)) =
4.2145 - if pI'=e_pblID andalso pI=e_pblID
4.2146 - then (false, (init_pbl ppc, []))
4.2147 - else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
4.2148 - (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
4.2149 - val ((p,Pbl),c,_,pt) =
4.2150 - generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt
4.2151 - in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
4.2152 - (pos,(Uistate, e_ctxt)))], c, (pt,pos))
4.2153 - end
4.2154 -
4.2155 - (*transfers oris (not required in pbl) to met-model for script-env
4.2156 - FIXME.WN.8.03: application of several mIDs to SAME model?*)
4.2157 - | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
4.2158 - let
4.2159 - val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
4.2160 - meth=met, ctxt, ...}) = get_obj I pt p;
4.2161 - val {ppc,pre,prls,...} = get_met mID
4.2162 - val thy = assoc_thy dI
4.2163 - val oris = add_field' thy ppc oris;
4.2164 - val dI'' = if dI=e_domID then dI' else dI;
4.2165 - val pI'' = if pI = e_pblID then pI' else pI;
4.2166 - val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
4.2167 - val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
4.2168 - val (pos,c,_,pt)=
4.2169 - generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
4.2170 - in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
4.2171 - (pos,(Uistate, e_ctxt)))], c, (pt,pos))
4.2172 - end
4.2173 -
4.2174 - | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
4.2175 - let
4.2176 - val ctxt = get_ctxt pt pos
4.2177 - val (dI',_,_) = get_obj g_spec pt p
4.2178 - val (pos,c,_,pt) =
4.2179 - generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
4.2180 - in (*FIXXXME: check if pbl can still be parsed*)
4.2181 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
4.2182 - (pt, pos))
4.2183 - end
4.2184 -
4.2185 - | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
4.2186 - let
4.2187 - val ctxt = get_ctxt pt pos
4.2188 - val (dI',_,_) = get_obj g_spec pt p
4.2189 - val (pos,c,_,pt) =
4.2190 - generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
4.2191 - in (*FIXXXME: check if met can still be parsed*)
4.2192 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
4.2193 - (pt, pos))
4.2194 - end
4.2195 -
4.2196 - | nxt_specif m' _ =
4.2197 - error ("nxt_specif: not impl. for "^tac2str m');
4.2198 + let
4.2199 + val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
4.2200 + PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...} =>
4.2201 + (oris, dI, dI', pI', probl, ctxt)
4.2202 + | _ => error ""
4.2203 + val thy = assoc_thy (if dI' = e_domID then dI else dI');
4.2204 + val {ppc,where_,prls,...} = get_pbt pI
4.2205 + val pbl =
4.2206 + if pI' = e_pblID andalso pI = e_pblID
4.2207 + then (false, (init_pbl ppc, []))
4.2208 + else match_itms_oris thy probl (ppc,where_,prls) oris
4.2209 + (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
4.2210 + val (c, pt) = case generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
4.2211 + ((_, Pbl), c, _, pt) => (c, pt)
4.2212 + | _ => error ""
4.2213 + in
4.2214 + ([(Specify_Problem pI, Specify_Problem' (pI, pbl), (pos, (Uistate, e_ctxt)))], c, (pt,pos))
4.2215 + end
4.2216 + (* transfers oris (not required in pbl) to met-model for script-env
4.2217 + FIXME.WN.8.03: application of several mIDs to SAME model? *)
4.2218 + | nxt_specif (Specify_Method mID) (pt, pos as (p,_)) =
4.2219 + let
4.2220 + val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of
4.2221 + PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
4.2222 + => (oris, pbl, dI, met, ctxt)
4.2223 + | _ => error "nxt_specif Specify_Method: uncovered case get_obj"
4.2224 + val {ppc,pre,prls,...} = get_met mID
4.2225 + val thy = assoc_thy dI
4.2226 + val oris = add_field' thy ppc oris
4.2227 + val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
4.2228 + val (_, (itms, _)) = match_itms_oris thy met (ppc,pre,prls ) oris
4.2229 + val (pos, c, _, pt) =
4.2230 + generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
4.2231 + in
4.2232 + ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos))
4.2233 + end
4.2234 + | nxt_specif (Specify_Theory dI) (pt, pos as (_, Pbl)) =
4.2235 + let
4.2236 + val ctxt = get_ctxt pt pos
4.2237 + val (pos, c, _, pt) =
4.2238 + generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
4.2239 + in (*FIXXXME: check if pbl can still be parsed*)
4.2240 + ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,
4.2241 + (pt, pos))
4.2242 + end
4.2243 + | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =
4.2244 + let
4.2245 + val ctxt = get_ctxt pt pos
4.2246 + val (pos, c, _, pt) = generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
4.2247 + in (*FIXXXME: check if met can still be parsed*)
4.2248 + ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))
4.2249 + end
4.2250 + | nxt_specif m' _ = error ("nxt_specif: not impl. for "^tac2str m')
4.2251
4.2252 (* get the values from oris; handle the term list w.r.t. penv *)
4.2253 -local infix mem;
4.2254 -fun x mem [] = false
4.2255 - | x mem (y :: ys) = x = y orelse x mem ys;
4.2256 -in
4.2257 fun vals_of_oris oris =
4.2258 - ((map (mkval' o (#5:ori -> term list))) o
4.2259 - (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
4.2260 -end;
4.2261 + ((map (mkval' o (#5 : ori -> term list))) o
4.2262 + (filter ((member_swap op= 1) o (#2 : ori -> int list)))) oris
4.2263
4.2264 (* create a calc-tree with oris via an cas.refined pbl *)
4.2265 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
4.2266 - if pI <> []
4.2267 - then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
4.2268 + if pI <> []
4.2269 + then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
4.2270 + let
4.2271 + val {cas, met, ppc, thy, ...} = get_pbt pI
4.2272 + val dI = if dI = "" then theory2theory' thy else dI
4.2273 + val mI = if mI = [] then hd met else mI
4.2274 + val hdl = case cas of NONE => pblterm dI pI | SOME t => t
4.2275 + val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
4.2276 + ([], (dI,pI,mI), hdl)
4.2277 + val pt = update_spec pt [] (dI, pI, mI)
4.2278 + val pits = init_pbl' ppc
4.2279 + val pt = update_pbl pt [] pits
4.2280 + in ((pt, ([] , Pbl)), []) : calcstate end
4.2281 + else
4.2282 + if mI <> []
4.2283 + then (* from met-browser *)
4.2284 let
4.2285 - val {cas, met, ppc, thy, ...} = get_pbt pI
4.2286 - val dI = if dI = "" then theory2theory' thy else dI
4.2287 - val thy = assoc_thy dI
4.2288 - val mI = if mI = [] then hd met else mI
4.2289 - val hdl = case cas of NONE => pblterm dI pI | SOME t => t
4.2290 - val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
4.2291 - ([], (dI,pI,mI), hdl)
4.2292 - val pt = update_spec pt [] (dI,pI,mI)
4.2293 - val pits = init_pbl' ppc
4.2294 - val pt = update_pbl pt [] pits
4.2295 - in ((pt, ([] ,Pbl)), []) : calcstate end
4.2296 - else
4.2297 - if mI <> []
4.2298 - then (* from met-browser *)
4.2299 - let
4.2300 - val {ppc,...} = get_met mI
4.2301 - val dI = if dI = "" then "Isac" else dI
4.2302 - val thy = assoc_thy dI;
4.2303 - val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
4.2304 - ([], (dI,pI,mI), e_term(*FIXME met*));
4.2305 - val pt = update_spec pt [] (dI,pI,mI);
4.2306 - val mits = init_pbl' ppc;
4.2307 - val pt = update_met pt [] mits;
4.2308 - in ((pt, ([], Met)), []) : calcstate end
4.2309 - else (* new example, pepare for interactive modeling *)
4.2310 - let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
4.2311 - ([], e_spec, e_term)
4.2312 - in ((pt, ([], Pbl)), []) : calcstate end
4.2313 + val {ppc, ...} = get_met mI
4.2314 + val dI = if dI = "" then "Isac" else dI
4.2315 + val (pt, _) =
4.2316 + cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
4.2317 + val pt = update_spec pt [] (dI, pI, mI)
4.2318 + val mits = init_pbl' ppc
4.2319 + val pt = update_met pt [] mits
4.2320 + in ((pt, ([], Met)), []) end
4.2321 + else (* new example, pepare for interactive modeling *)
4.2322 + let
4.2323 + val (pt, _) =
4.2324 + cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term)
4.2325 + in ((pt, ([], Pbl)), []) end
4.2326 + | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
4.2327 + let (* both """"""""""""""""""""""""" either empty or complete *)
4.2328 + val thy = assoc_thy dI
4.2329 + val (pI, (pors, pctxt), mI) =
4.2330 + if mI = ["no_met"]
4.2331 + then
4.2332 + let
4.2333 + val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
4.2334 + val pI' = refine_ori' pors pI;
4.2335 + in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
4.2336 + (hd o #met o get_pbt) pI')
4.2337 + end
4.2338 + else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
4.2339 + val {cas, ppc, thy = thy', ...} = get_pbt pI (*take dI from _refined_ pbl*)
4.2340 + val dI = theory2theory' (maxthy thy thy')
4.2341 + val hdl = case cas of
4.2342 + NONE => pblterm dI pI
4.2343 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
4.2344 + val (pt, _) =
4.2345 + cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
4.2346 + val pt = update_ctxt pt [] pctxt
4.2347 + in
4.2348 + ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
4.2349 + end
4.2350
4.2351 - | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
4.2352 - let (* both """"""""""""""""""""""""" either empty or complete *)
4.2353 - val thy = assoc_thy dI
4.2354 - val (pI, (pors, pctxt), mI) =
4.2355 - if mI = ["no_met"]
4.2356 - then
4.2357 - let
4.2358 - val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
4.2359 - val pI' = refine_ori' pors pI;
4.2360 - in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
4.2361 - (hd o #met o get_pbt) pI') end
4.2362 - else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
4.2363 - val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
4.2364 - val dI = theory2theory' (maxthy thy thy')
4.2365 - val hdl =
4.2366 - case cas of
4.2367 - NONE => pblterm dI pI
4.2368 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
4.2369 - val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
4.2370 - (pors, (dI, pI, mI), hdl)
4.2371 - val pt = update_ctxt pt [] pctxt
4.2372 - in ((pt, ([], Pbl)),
4.2373 - fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
4.2374 - end;
4.2375 +fun get_spec_form m ((p, p_) : pos') pt =
4.2376 + let val (_, _, f, _, _, _) = specify m (p, p_) [] pt
4.2377 + in f end
4.2378
4.2379 -
4.2380 -
4.2381 -(*18.12.99*)
4.2382 -fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
4.2383 -(* case appl_spec p pt m of /// 19.1.00
4.2384 - Notappl e => Error' (Error_ e)
4.2385 - | Appl =>
4.2386 -*) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
4.2387 - in f end;
4.2388 -
4.2389 -
4.2390 -(*fun tag_form thy (formal, given) = Thm.global_cterm_of thy
4.2391 - (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819*)
4.2392 +(* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
4.2393 + (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
4.2394 fun tag_form thy (formal, given) =
4.2395 (let
4.2396 val gf = (head_of given) $ formal;
4.2397 val _ = Thm.global_cterm_of thy gf
4.2398 in gf end)
4.2399 handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
4.2400 - " .. " ^ term_to_string''' thy formal ^ " ..types do not match");
4.2401 -(* val formal = (the o (parse thy)) "[R::real]";
4.2402 -> val given = (the o (parse thy)) "fixed_values (cs::real list)";
4.2403 -> tag_form thy (formal, given);
4.2404 -val it = "fixed_values [R]" : cterm
4.2405 -*)
4.2406 + " .. " ^ term_to_string''' thy formal ^ " ..types do not match")
4.2407
4.2408 fun chktyp thy (n, fs, gs) =
4.2409 ((writeln o (term_to_string''' thy) o (nth n)) fs;
4.2410 (writeln o (term_to_string''' thy) o (nth n)) gs;
4.2411 - tag_form thy (nth n fs, nth n gs));
4.2412 -fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
4.2413 -
4.2414 -(* #####################################################
4.2415 - find the failing item:
4.2416 -> val n = 2;
4.2417 -> val tag__form = chktyp (n,formals,givens);
4.2418 -> (type_of o Thm.term_of o (nth n)) formals;
4.2419 -> (type_of o Thm.term_of o (nth n)) givens;
4.2420 -> atomty ((Thm.term_of o (nth n)) formals);
4.2421 -> atomty ((Thm.term_of o (nth n)) givens);
4.2422 -> atomty (Thm.term_of tag__form);
4.2423 -> use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
4.2424 - ##################################################### *)
4.2425 -
4.2426 -(* #####################################################
4.2427 - testdata setup
4.2428 -val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
4.2429 -val formals = map (the o (parse thy)) origin;
4.2430 -
4.2431 -val given = ["equation (lhs=rhs)",
4.2432 - "bound_variable bdv", (* TODO type *)
4.2433 - "error_bound apx"];
4.2434 -val where_ = ["e is_root_equation_in bdv",
4.2435 - "bdv is_var",
4.2436 - "apx is_const_expr"];
4.2437 -val find = ["L::rat set"];
4.2438 -val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
4.2439 -val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
4.2440 -val givens = map (the o (parse thy)) given;
4.2441 -
4.2442 -val tag__forms = chktyps (formals, givens);
4.2443 -map ((atomty) o Thm.term_of) tag__forms;
4.2444 - ##################################################### *)
4.2445 -
4.2446 + tag_form thy (nth n fs, nth n gs))
4.2447 +fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
4.2448
4.2449 (* check pbltypes, announces one failure a time *)
4.2450 -(*fun chk_vars ctppc =
4.2451 - let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
4.2452 - appc flat (mappc (vars o Thm.term_of) ctppc)
4.2453 - in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
4.2454 - else if (re\\(gi union fi)) <> []
4.2455 - then ("re\\(gi union fi)",re\\(gi union fi))
4.2456 - else ("ok",[]) end;*)
4.2457 fun chk_vars ctppc =
4.2458 - let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
4.2459 - appc flat (mappc vars ctppc)
4.2460 - val chked = subtract op = gi wh
4.2461 - in if chked <> [] then ("wh\\gi", chked)
4.2462 - else let val chked = subtract op = (union op = gi fi) re
4.2463 - in if chked <> []
4.2464 - then ("re\\(gi union fi)", chked)
4.2465 - else ("ok", [])
4.2466 - end
4.2467 - end;
4.2468 + let
4.2469 + val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = appc flat (mappc vars ctppc)
4.2470 + val chked = subtract op = gi wh
4.2471 + in
4.2472 + if chked <> [] then ("wh\\gi", chked)
4.2473 + else
4.2474 + let val chked = subtract op = (union op = gi fi) re
4.2475 + in
4.2476 + if chked <> []
4.2477 + then ("re\\(gi union fi)", chked)
4.2478 + else ("ok", [])
4.2479 + end
4.2480 + end
4.2481
4.2482 (* check a new pbltype: variables (Free) unbound by given, find*)
4.2483 fun unbound_ppc ctppc =
4.2484 - let val {Given=gi,Find=fi,Relate=re,...} =
4.2485 - appc flat (mappc vars ctppc)
4.2486 - in distinct (*re\\(gi union fi)*)
4.2487 - (subtract op = (union op = gi fi) re) end;
4.2488 -(*
4.2489 -> val org = {Given=["[R=(R::real)]"],Where=[],
4.2490 - Find=["[A::real]"],With=[],
4.2491 - Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
4.2492 - }:string ppc;
4.2493 -> val ctppc = mappc (the o (parse thy)) org;
4.2494 -> unbound_ppc ctppc;
4.2495 -val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
4.2496 -*)
4.2497 + let
4.2498 + val {Given = gi, Find = fi, Relate = re, ...} = appc flat (mappc vars ctppc)
4.2499 + in
4.2500 + distinct (subtract op = (union op = gi fi) re)
4.2501 + end
4.2502
4.2503 -
4.2504 -(* f, a binary operator, is nested rightassociative *)
4.2505 +(* f, a binary operator, is nested right associative *)
4.2506 fun foldr1 f xs =
4.2507 let
4.2508 - fun fld f (x::[]) = x
4.2509 - | fld f (x::x'::[]) = f (x',x)
4.2510 - | fld f (x::x'::xs) = f (fld f (x'::xs),x);
4.2511 - in ((fld f) o rev) xs end;
4.2512 -(*
4.2513 -> val (SOME ct) = parse thy "[a=b,c=d,e=f]";
4.2514 -> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
4.2515 -> val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
4.2516 -> Thm.global_cterm_of thy conj;
4.2517 -val it = "(a = b & c = d) & e = f" : cterm
4.2518 -*)
4.2519 + fun fld _ (x :: []) = x
4.2520 + | fld f (x :: x' :: []) = f (x', x)
4.2521 + | fld f (x :: x' :: xs) = f (fld f (x' :: xs), x)
4.2522 + | fld _ _ = error "foldr1 uncovered definition"
4.2523 + in ((fld f) o rev) xs end
4.2524
4.2525 (* f, a binary operator, is nested leftassociative *)
4.2526 -fun foldl1 f (x::[]) = x
4.2527 - | foldl1 f (x::x'::[]) = f (x,x')
4.2528 - | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
4.2529 -(*
4.2530 -> val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
4.2531 -> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
4.2532 -> val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
4.2533 -> Thm.global_cterm_of thy conj;
4.2534 -val it = "a = b & c = d & e = f & g = h" : cterm
4.2535 -*)
4.2536 -
4.2537 +fun foldl1 _ (x :: []) = x
4.2538 + | foldl1 f (x :: x' :: []) = f (x, x')
4.2539 + | foldl1 f (x :: x' :: xs) = f (x, foldl1 f (x' :: xs))
4.2540 + | foldl1 _ _ = error "foldl1 uncovered definition"
4.2541
4.2542 (* called only once, if a Subproblem has been located in the script*)
4.2543 -fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_,_)) ptp =
4.2544 - (case metID of
4.2545 - ["no_met"] =>
4.2546 - (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
4.2547 - | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
4.2548 - (*all stored in tac_ itms^^^^^^^^^^*)
4.2549 - | nxt_model_pbl tac_ _ =
4.2550 - error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_);
4.2551 +fun nxt_model_pbl (Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp =
4.2552 + (case metID of
4.2553 + ["no_met"] => (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
4.2554 + | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
4.2555 + (*all stored in tac_ itms^^^^^^^^^^*)
4.2556 + | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_)
4.2557
4.2558 -(*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
4.2559 -fun eq4 v (_,vts,_,_,_) = member op = vts v;
4.2560 -fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
4.2561 +(* fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml *)
4.2562 +fun eq4 v (_, vts, _, _, _) = member op = vts v
4.2563 +fun eq5 (_, _, _, _, itm_) (_, _, _, d, _) = d_in itm_ = d
4.2564
4.2565 -
4.2566 -(*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
4.2567 - + met from fmz; assumes pos on PblObj, meth = [].*)
4.2568 -fun complete_mod (pt, pos as (p, p_):pos') =
4.2569 -(* val (pt, (p, _)) = (pt, p);
4.2570 - val (pt, (p, _)) = (pt, pos);
4.2571 - *)
4.2572 - let val _= if p_ <> Pbl
4.2573 - then tracing("###complete_mod: only impl.for Pbl, called with "^
4.2574 - pos'2str pos) else ()
4.2575 - val (PblObj{origin=(oris, ospec, hdl), probl, spec, ...}) =
4.2576 - get_obj I pt p
4.2577 - val (dI,pI,mI) = some_spec ospec spec
4.2578 - val mpc = (#ppc o get_met) mI
4.2579 - val ppc = (#ppc o get_pbt) pI
4.2580 - val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
4.2581 - val pt = update_pblppc pt p pits
4.2582 - val pt = update_metppc pt p mits
4.2583 - in (pt, (p,Met):pos') end
4.2584 -;
4.2585 -(*| complete_mod (pt, pos as (p, Met):pos') =
4.2586 - error ("###complete_mod: only impl.for Pbl, called with "^
4.2587 - pos'2str pos);*)
4.2588 +(* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
4.2589 + + met from fmz; assumes pos on PblObj, meth = [] *)
4.2590 +fun complete_mod (pt, pos as (p, p_) : pos') =
4.2591 + let
4.2592 + val _ = if p_ <> Pbl
4.2593 + then error ("###complete_mod: only impl.for Pbl, called with " ^ pos'2str pos)
4.2594 + else ()
4.2595 + val (oris, ospec, probl, spec) = case get_obj I pt p of
4.2596 + PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
4.2597 + | _ => error "complete_mod: unvered case get_obj"
4.2598 + val (_, pI, mI) = some_spec ospec spec
4.2599 + val mpc = (#ppc o get_met) mI
4.2600 + val ppc = (#ppc o get_pbt) pI
4.2601 + val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
4.2602 + val pt = update_pblppc pt p pits
4.2603 + val pt = update_metppc pt p mits
4.2604 + in (pt, (p, Met) : pos') end
4.2605
4.2606 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
4.2607 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
4.2608 -fun all_modspec (pt, (p,_):pos') =
4.2609 - let
4.2610 - val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
4.2611 - val thy = assoc_thy dI;
4.2612 - val {ppc, ...} = get_met mI;
4.2613 - val (fmz_, vals) = oris2fmz_vals pors;
4.2614 +fun all_modspec (pt, (p, _) : pos') =
4.2615 + let
4.2616 + val (pors, dI, pI, mI) = case get_obj I pt p of
4.2617 + PblObj {origin = (pors, (dI, pI, mI), _), ...} => (pors, dI, pI, mI)
4.2618 + | _ => error "all_modspec: uncovered case get_obj"
4.2619 + val {ppc, ...} = get_met mI
4.2620 + val (_, vals) = oris2fmz_vals pors
4.2621 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
4.2622 |> declare_constraints' vals
4.2623 - val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
4.2624 - val pt = update_metppc pt p (map (ori2Coritm ppc) pors); (*WN110716 = _pblppc ?!?*)
4.2625 - val pt = update_spec pt p (dI,pI,mI);
4.2626 + val pt = update_pblppc pt p (map (ori2Coritm ppc) pors)
4.2627 + val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*)
4.2628 + val pt = update_spec pt p (dI, pI, mI)
4.2629 val pt = update_ctxt pt p ctxt
4.2630 -(*
4.2631 - val mors = prep_ori fmz_ thy ppc |> #1;
4.2632 - val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
4.2633 - val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
4.2634 - (*WN110715: why pors, mors handled so differently?*)
4.2635 - val pt = update_spec pt p (dI,pI,mI);
4.2636 -*)
4.2637 - in (pt, (p,Met): pos') end;
4.2638 + in
4.2639 + (pt, (p, Met) : pos')
4.2640 + end
4.2641
4.2642 -(*WN0312: use in nxt_spec, too ? what about variants ???*)
4.2643 -fun is_complete_mod_ ([]: itm list) = false
4.2644 - | is_complete_mod_ itms =
4.2645 - foldl and_ (true, (map #3 itms));
4.2646 +(* WN0312: use in nxt_spec, too ? what about variants ??? *)
4.2647 +fun is_complete_mod_ ([] : itm list) = false
4.2648 + | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
4.2649
4.2650 -fun is_complete_mod (pt, pos as (p, Pbl): pos') =
4.2651 - if (is_pblobj o (get_obj I pt)) p
4.2652 - then (is_complete_mod_ o (get_obj g_pbl pt)) p
4.2653 - else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
4.2654 +fun is_complete_mod (pt, pos as (p, Pbl) : pos') =
4.2655 + if (is_pblobj o (get_obj I pt)) p
4.2656 + then (is_complete_mod_ o (get_obj g_pbl pt)) p
4.2657 + else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
4.2658 | is_complete_mod (pt, pos as (p, Met)) =
4.2659 - if (is_pblobj o (get_obj I pt)) p
4.2660 - then (is_complete_mod_ o (get_obj g_met pt)) p
4.2661 - else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
4.2662 + if (is_pblobj o (get_obj I pt)) p
4.2663 + then (is_complete_mod_ o (get_obj g_met pt)) p
4.2664 + else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
4.2665 | is_complete_mod (_, pos) =
4.2666 - error ("is_complete_mod called by " ^ pos'2str pos ^
4.2667 - " (should be Pbl or Met)");
4.2668 + error ("is_complete_mod called by " ^ pos'2str pos ^ " (should be Pbl or Met)")
4.2669
4.2670 -(*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
4.2671 -fun is_complete_spec (pt, pos as (p,_): pos') =
4.2672 - if (not o is_pblobj o (get_obj I pt)) p
4.2673 - then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
4.2674 - else let val (dI,pI,mI) = get_obj g_spec pt p
4.2675 - in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
4.2676 -(*.complete empty items in specification from origin (pbl, met ev.refined);
4.2677 - assumes 'is_complete_mod'.*)
4.2678 -fun complete_spec (pt, pos as (p,_): pos') =
4.2679 - let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
4.2680 - val pt = update_spec pt p (some_spec ospec spec)
4.2681 - in (pt, pos) end;
4.2682 +(* have (thy, pbl, met) _all_ been specified explicitly ? *)
4.2683 +fun is_complete_spec (pt, pos as (p, _) : pos') =
4.2684 + if (not o is_pblobj o (get_obj I pt)) p
4.2685 + then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
4.2686 + else
4.2687 + let val (dI,pI,mI) = get_obj g_spec pt p
4.2688 + in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end
4.2689
4.2690 -fun is_complete_modspec ptp =
4.2691 - is_complete_mod ptp andalso is_complete_spec ptp;
4.2692 +(* complete empty items in specification from origin (pbl, met ev.refined);
4.2693 + assumes 'is_complete_mod' *)
4.2694 +fun complete_spec (pt, pos as (p, _) : pos') =
4.2695 + let
4.2696 + val (ospec, spec) = case get_obj I pt p of
4.2697 + PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
4.2698 + | _ => error "complete_spec: uncovered case get_obj"
4.2699 + val pt = update_spec pt p (some_spec ospec spec)
4.2700 + in
4.2701 + (pt, pos)
4.2702 + end
4.2703
4.2704 +fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
4.2705
4.2706 +fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =
4.2707 + let
4.2708 + val (_, _, metID) = get_somespec' spec spec'
4.2709 + val pre = if metID = e_metID then []
4.2710 + else
4.2711 + let
4.2712 + val {prls, pre= where_, ...} = get_met metID
4.2713 + val pre = check_preconds' prls where_ meth 0
4.2714 + in pre end
4.2715 + val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
4.2716 + in
4.2717 + ModSpec (allcorrect, Met, hdl, meth, pre, spec)
4.2718 + end
4.2719 + | pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
4.2720 + let
4.2721 + val (_, pI, _) = get_somespec' spec spec'
4.2722 + val pre = if pI = e_pblID then []
4.2723 + else
4.2724 + let
4.2725 + val {prls, where_, ...} = get_pbt pI
4.2726 + val pre = check_preconds' prls where_ probl 0
4.2727 + in pre end
4.2728 + val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
4.2729 + in
4.2730 + ModSpec (allcorrect, Pbl, hdl, probl, pre, spec)
4.2731 + end
4.2732 + | pt_model _ _ = error "pt_model: uncovered definition"
4.2733
4.2734 +fun pt_form (PrfObj {form, ...}) = Form form
4.2735 + | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) =
4.2736 + let
4.2737 + val (dI, pI, _) = get_somespec' spec spec'
4.2738 + val {cas, ...} = get_pbt pI
4.2739 + in case cas of
4.2740 + NONE => Form (pblterm dI pI)
4.2741 + | SOME t => Form (subst_atomic (mk_env probl) t)
4.2742 + end
4.2743
4.2744 -fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
4.2745 -(* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
4.2746 - *)
4.2747 - let val (_,_,metID) = get_somespec' spec spec'
4.2748 - val pre =
4.2749 - if metID = e_metID then []
4.2750 - else let val {prls,pre=where_,...} = get_met metID
4.2751 - val pre = check_preconds' prls where_ meth 0
4.2752 - in pre end
4.2753 - val allcorrect = is_complete_mod_ meth
4.2754 - andalso foldl and_ (true, (map #1 pre))
4.2755 - in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
4.2756 - | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
4.2757 -(* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
4.2758 - *)
4.2759 - let val (_,pI,_) = get_somespec' spec spec'
4.2760 - val pre =
4.2761 - if pI = e_pblID then []
4.2762 - else let val {prls,where_,cas,...} = get_pbt pI
4.2763 - val pre = check_preconds' prls where_ probl 0
4.2764 - in pre end
4.2765 - val allcorrect = is_complete_mod_ probl
4.2766 - andalso foldl and_ (true, (map #1 pre))
4.2767 - in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
4.2768 -
4.2769 -
4.2770 -fun pt_form (PrfObj {form,...}) = Form form
4.2771 - | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
4.2772 - let val (dI, pI, _) = get_somespec' spec spec'
4.2773 - val {cas,...} = get_pbt pI
4.2774 - in case cas of
4.2775 - NONE => Form (pblterm dI pI)
4.2776 - | SOME t => Form (subst_atomic (mk_env probl) t)
4.2777 - end;
4.2778 -(*vvv takes the tac _generating_ the formula=result, asm ok....
4.2779 -fun pt_result (PrfObj {result=(t,asm), tac,...}) =
4.2780 - (Form t,
4.2781 - if null asm then NONE else SOME asm,
4.2782 - SOME tac)
4.2783 - | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
4.2784 - let val (_,_,metID) = some_spec ospec spec
4.2785 - in (Form t,
4.2786 - if null asm then NONE else SOME asm,
4.2787 - if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
4.2788 --------------------------------------------------------------------------*)
4.2789 -
4.2790 -
4.2791 -(*.pt_extract returns
4.2792 +(* pt_extract returns
4.2793 # the formula at pos
4.2794 # the tactic applied to this formula
4.2795 # the list of assumptions generated at this formula
4.2796 (by application of another tac to the preceding formula !)
4.2797 - pos is assumed to come from the frontend, ie. generated by moveDown.*)
4.2798 -(*cannot be in ctree.sml, because ModSpec has to be calculated*)
4.2799 -fun pt_extract (pt,([],Res)) = (* WN120512: --returns--> Check_Postcondition WRONGLY
4.2800 - see --- build fun is_exactly_equal*)
4.2801 - (* ML_TODO 110417 get assumptions from ctxt !? *)
4.2802 - let val (f, asm) = get_obj g_result pt []
4.2803 - in (Form f, NONE, asm) end
4.2804 + pos is assumed to come from the frontend, ie. generated by moveDown.
4.2805 + Notes: cannot be in ctree.sml, because ModSpec has to be calculated.
4.2806 + TODO 110417 get assumptions from ctxt !?
4.2807 +*)
4.2808 +fun pt_extract (pt, ([], Res)) =
4.2809 + (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)
4.2810 + let
4.2811 + val (f, asm) = get_obj g_result pt []
4.2812 + in (Form f, NONE, asm) end
4.2813 | pt_extract (pt,(p,Res)) =
4.2814 - let
4.2815 - val (f, asm) = get_obj g_result pt p
4.2816 - val tac =
4.2817 - if last_onlev pt p
4.2818 + let
4.2819 + val (f, asm) = get_obj g_result pt p
4.2820 + val tac =
4.2821 + if last_onlev pt p
4.2822 + then
4.2823 + if is_pblobj' pt (lev_up p)
4.2824 then
4.2825 - if is_pblobj' pt (lev_up p)
4.2826 - then
4.2827 - let
4.2828 - val (PblObj{spec=(_,pI,_),...}) = get_obj I pt (lev_up p)
4.2829 - in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
4.2830 - else SOME End_Trans (*WN0502 TODO for other branches*)
4.2831 - else
4.2832 - let val p' = lev_on p
4.2833 - in
4.2834 - if is_pblobj' pt p'
4.2835 - then
4.2836 - let val (PblObj{origin = (_,(dI,pI,_),_),...}) = get_obj I pt p'
4.2837 - in SOME (Subproblem (dI, pI)) end
4.2838 - else
4.2839 - if f = get_obj g_form pt p'
4.2840 - then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
4.2841 - else SOME (Take (term2str (get_obj g_form pt p')))
4.2842 - end
4.2843 - in (Form f, tac, asm) end
4.2844 - | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
4.2845 + let
4.2846 + val pI = case get_obj I pt (lev_up p) of
4.2847 + PblObj{spec = (_, pI, _), ...} => pI
4.2848 + | _ => error "pt_extract last_onlev: uncovered case get_obj"
4.2849 + in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
4.2850 + else SOME End_Trans (* WN0502 TODO for other branches *)
4.2851 + else
4.2852 + let val p' = lev_on p
4.2853 + in
4.2854 + if is_pblobj' pt p'
4.2855 + then
4.2856 + let
4.2857 + val (dI ,pI) = case get_obj I pt p' of
4.2858 + PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)
4.2859 + | _ => error "pt_extract \<not>last_onlev: uncovered case get_obj"
4.2860 + in SOME (Subproblem (dI, pI)) end
4.2861 + else
4.2862 + if f = get_obj g_form pt p'
4.2863 + then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
4.2864 + else SOME (Take (term2str (get_obj g_form pt p')))
4.2865 + end
4.2866 + in (Form f, tac, asm) end
4.2867 + | pt_extract (pt, (p,p_(*Frm,Pbl*))) =
4.2868 let
4.2869 val ppobj = get_obj I pt p
4.2870 val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
4.2871 val tac = g_tac ppobj
4.2872 - in (f, SOME tac, []) end;
4.2873 + in (f, SOME tac, []) end
4.2874
4.2875 +(** get the formula from a ctree-node:
4.2876 + take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
4.2877 + take res from all other PrfObj's
4.2878 + Designed for interSteps, outcommented 04 in favour of calcChangedEvent **)
4.2879 +fun formres p (Nd (PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
4.2880 + [("headline", (p, Frm), h), ("stepform", (p, Res), r)]
4.2881 + | formres p (Nd (PrfObj {form, result = (r, _), ...}, _)) =
4.2882 + [("stepform", (p, Frm), form), ("stepform", (p, Res), r)]
4.2883 + | formres _ _ = error "formres: uncovered definition"
4.2884 +fun form p (Nd (PrfObj {result = (r, _), ...}, _)) =
4.2885 + [("stepform", (p, Res), r)]
4.2886 + | form _ _ = error "form: uncovered definition"
4.2887
4.2888 -(**. get the formula from a ctree-node:
4.2889 - take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
4.2890 - take res from all other PrfObj's .**)
4.2891 -(*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
4.2892 -fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
4.2893 - [("headline", (p, Frm), h),
4.2894 - ("stepform", (p, Res), r)]
4.2895 - | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
4.2896 - [("stepform", (p, Frm), form),
4.2897 - ("stepform", (p, Res), r)];
4.2898 -
4.2899 -fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
4.2900 - [("stepform", (p, Res), r)]
4.2901 -
4.2902 -(*assumes to take whole level, in particular hd -- for use in interSteps*)
4.2903 -fun get_formress fs p [] = flat fs
4.2904 +(* assumes to take whole level, in particular hd -- for use in interSteps *)
4.2905 +fun get_formress fs _ [] = flat fs
4.2906 | get_formress fs p (nd::nds) =
4.2907 (* start with 'form+res' and continue with trying 'res' only*)
4.2908 get_forms (fs @ [formres p nd]) (lev_on p) nds
4.2909 -and get_forms fs p [] = flat fs
4.2910 +and get_forms fs _ [] = flat fs
4.2911 | get_forms fs p (nd::nds) =
4.2912 if is_pblnd nd
4.2913 (* start again with 'form+res' ///ugly repeat with Check_elementwise
4.2914 @@ -1870,28 +1398,17 @@
4.2915 (* continue with trying 'res' only*)
4.2916 else get_forms (fs @ [form p nd]) (lev_on p) nds;
4.2917
4.2918 -(**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
4.2919 -(*WN050219 made robust against _'to' below or after Complete nodes
4.2920 - by handling exn caused by move_dn*)
4.2921 -(*WN0401 this functionality belongs to ctree.sml,
4.2922 -but fetching a calc_head requires calculations defined in modspec.sml
4.2923 -transfer to ME/me.sml !!!
4.2924 -WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
4.2925 -is returned !!!!!!!!!!!!!
4.2926 -*)
4.2927 -fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
4.2928 - | eq_pos' (p1,Res) (p2,Res) = p1 = p2
4.2929 - | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
4.2930 - Pbl => true
4.2931 - | Met => true
4.2932 - | _ => false)
4.2933 - | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
4.2934 - Pbl => true
4.2935 - | Met => true
4.2936 - | _ => false)
4.2937 +(** get an 'interval' 'from' 'to' of formulae from a ptree **)
4.2938 +(* WN0401 this functionality belongs to ctree.sml *)
4.2939 +fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2
4.2940 + | eq_pos' (p1, Res) (p2, Res) = p1 = p2
4.2941 + | eq_pos' (p1, Pbl) (p2, p2_) =
4.2942 + p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
4.2943 + | eq_pos' (p1, Met) (p2, p2_) =
4.2944 + p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
4.2945 | eq_pos' _ _ = false;
4.2946
4.2947 -(*.get an 'interval' from the ctree; 'interval' is w.r.t. the
4.2948 +(* get an 'interval' from the ctree; 'interval' is w.r.t. the
4.2949 total ordering Position#compareTo(Position p) in the java-code
4.2950 val get_interval = fn
4.2951 : pos' -> : from is "move_up 1st-element" to return
4.2952 @@ -1901,23 +1418,16 @@
4.2953 ptree -> :
4.2954 (pos' * : of the formula
4.2955 Term.term) : the formula
4.2956 - list
4.2957 -.*)
4.2958 + list *)
4.2959 fun get_interval from to level pt =
4.2960 let
4.2961 - fun get_inter c (from:pos') (to:pos') lev pt =
4.2962 - if eq_pos' from to orelse from = ([],Res)
4.2963 - (*orelse ... avoids Exception- PTREE "end of calculation" raised,
4.2964 - if 'to' has values NOT generated by move_dn, see systest/me.sml
4.2965 - TODO.WN0501: introduce an order on pos' and check "from > to"..
4.2966 - ...there is an order in Java!
4.2967 - WN051224 the hack got worse with returning term instead ptform*)
4.2968 + fun get_inter c (from : pos') (to : pos') lev pt =
4.2969 + if eq_pos' from to orelse from = ([], Res)
4.2970 then
4.2971 - let val (f,_,_) = pt_extract (pt, from)
4.2972 - in
4.2973 - case f of
4.2974 - ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
4.2975 - | Form t => c @ [(from, t)]
4.2976 + let val (f, _, _) = pt_extract (pt, from)
4.2977 + in case f of
4.2978 + ModSpec (_,_,headline, _, _, _) => c @ [(from, headline)]
4.2979 + | Form t => c @ [(from, t)]
4.2980 end
4.2981 else
4.2982 if lev < lev_of from
4.2983 @@ -1925,60 +1435,62 @@
4.2984 handle (PTREE _(*from move_dn too far*)) => c
4.2985 else
4.2986 let
4.2987 - val (f,_,_) = pt_extract (pt, from)
4.2988 + val (f, _, _) = pt_extract (pt, from)
4.2989 val term = case f of
4.2990 ModSpec (_,_,headline,_,_,_) => headline
4.2991 | Form t => t
4.2992 in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)
4.2993 handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]
4.2994 end
4.2995 - in get_inter [] from to level pt end;
4.2996 + in get_inter [] from to level pt end
4.2997
4.2998 -(*for tests*)
4.2999 -fun posform2str (pos:pos', form) =
4.3000 - "("^ pos'2str pos ^", "^
4.3001 - (case form of
4.3002 - Form f => term2str f
4.3003 - | ModSpec c => term2str (#3 c(*the headline*)))
4.3004 - ^")";
4.3005 -fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
4.3006 - (map posform2str)) pfs;
4.3007 -fun posterm2str (pos:pos', t) =
4.3008 - "("^ pos'2str pos ^", "^term2str t^")";
4.3009 -fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
4.3010 - (map posterm2str)) pfs;
4.3011 +(* for tests *)
4.3012 +fun posform2str (pos : pos', form) =
4.3013 + "(" ^ pos'2str pos ^ ", " ^
4.3014 + (case form of Form f => term2str f | ModSpec c => term2str (#3 c(*the headline*))) ^
4.3015 + ")"
4.3016 +fun posforms2str pfs =
4.3017 + (strs2str' o (map (curry op ^ "\n")) o (map posform2str)) pfs
4.3018 +fun posterm2str (pos:pos', t) = "(" ^ pos'2str pos ^ ", " ^ term2str t ^ ")"
4.3019 +fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
4.3020
4.3021 +(* WN050225 omits the last step, if pt is incomplete *)
4.3022 +fun show_pt pt = tracing (posterms2str (get_interval ([], Frm) ([], Res) 99999 pt))
4.3023
4.3024 -(*WN050225 omits the last step, if pt is incomplete*)
4.3025 -fun show_pt pt =
4.3026 - tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
4.3027 +(* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
4.3028 +fun get_ocalhd (pt, (p, Pbl) : pos') =
4.3029 + let
4.3030 + val (ospec, hdf', spec, probl) = case get_obj I pt p of
4.3031 + PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
4.3032 + | _ => error "get_ocalhd Pbl: uncovered case get_obj"
4.3033 + val {prls, where_, ...} = get_pbt (#2 (some_spec ospec spec))
4.3034 + val pre = check_preconds (assoc_thy"Isac") prls where_ probl
4.3035 + in
4.3036 + (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
4.3037 + end
4.3038 + | get_ocalhd (pt, (p, Met)) =
4.3039 + let
4.3040 + val (ospec, hdf', spec, meth) = case get_obj I pt p of
4.3041 + PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
4.3042 + | _ => error "get_ocalhd Met: uncovered case get_obj"
4.3043 + val {prls, pre, ...} = get_met (#3 (some_spec ospec spec))
4.3044 + val pre = check_preconds (assoc_thy"Isac") prls pre meth
4.3045 + in
4.3046 + (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
4.3047 + end
4.3048 + | get_ocalhd _ = error "get_ocalhd: uncovered definition"
4.3049
4.3050 -(*.get a calchead from a PblObj-node in the ctree;
4.3051 - preconditions must be calculated.*)
4.3052 -fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
4.3053 - let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
4.3054 - get_obj I pt p
4.3055 - val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
4.3056 - val pre = check_preconds (assoc_thy"Isac") prls where_ probl
4.3057 - in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
4.3058 -| get_ocalhd (pt, pos' as (p,Met):pos') =
4.3059 - let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
4.3060 - spec, meth, ...} =
4.3061 - get_obj I pt p
4.3062 - val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
4.3063 - val pre = check_preconds (assoc_thy"Isac") prls pre meth
4.3064 - in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
4.3065 +(* at the activeFormula set the Model, the Guard and the Specification
4.3066 + to empty and return a CalcHead;
4.3067 + the 'origin' remains (for reconstructing all that) *)
4.3068 +fun reset_calchead (pt, (p,_) : pos') =
4.3069 + let
4.3070 + val () = case get_obj I pt p of
4.3071 + PblObj _ => ()
4.3072 + | _ => error "reset_calchead: uncovered case get_obj"
4.3073 + val pt = update_pbl pt p []
4.3074 + val pt = update_met pt p []
4.3075 + val pt = update_spec pt p e_spec
4.3076 + in (pt, (p, Pbl) : pos') end
4.3077
4.3078 -(*.at the activeFormula set the Model, the Guard and the Specification
4.3079 - to empty and return a CalcHead;
4.3080 - the 'origin' remains (for reconstructing all that).*)
4.3081 -fun reset_calchead (pt, pos' as (p,_):pos') =
4.3082 - let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
4.3083 - val pt = update_pbl pt p []
4.3084 - val pt = update_met pt p []
4.3085 - val pt = update_spec pt p e_spec
4.3086 - in (pt, (p,Pbl):pos') end;
4.3087 -
4.3088 -end
4.3089 -
4.3090 -open CalcHead;
4.3091 +end
4.3092 \ No newline at end of file
5.1 --- a/src/Tools/isac/Interpret/inform.sml Wed Nov 30 13:05:08 2016 +0100
5.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Dec 12 18:08:13 2016 +0100
5.3 @@ -11,7 +11,7 @@
5.4 type icalhd = pos' * cterm' * imodel * pos_ * spec
5.5 val fetchErrorpatterns : tac -> errpatID list
5.6 val input_icalhd : ptree -> icalhd -> ptree * ocalhd
5.7 - val inform : calcstate' -> string -> string * calcstate'
5.8 + val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
5.9 val find_fillpatterns : ptree * pos' -> errpatID -> (fillpatID * term * thm * subs option) list
5.10 val is_exactly_equal : ptree * (pos * pos_) -> string -> string * tac
5.11
5.12 @@ -19,7 +19,7 @@
5.13 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
5.14 val cas_input : term -> (ptree * ocalhd) option
5.15 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
5.16 - val compare_step : taci list * pos' list * (ptree * pos') -> term -> string * calcstate'
5.17 + val compare_step : taci list * pos' list * (ptree * pos') -> term -> string * Chead.calcstate'
5.18 val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
5.19 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
5.20 rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
5.21 @@ -182,9 +182,9 @@
5.22 case parseNEW ctxt ct of
5.23 NONE => (0,[],false,sel, Syn ct):itm
5.24 | SOME t =>
5.25 - (case is_known ctxt sel oris t of
5.26 + (case Chead.is_known ctxt sel oris t of
5.27 ("", ori', all) =>
5.28 - (case is_notyet_input ctxt ppc all ori' pbt of
5.29 + (case Chead.is_notyet_input ctxt ppc all ori' pbt of
5.30 ("",itm) => itm
5.31 | (msg,_) => error ("appl_add': " ^ msg))
5.32 | (_, (i, v, _, d, ts), _) =>
5.33 @@ -232,7 +232,7 @@
5.34 | appl_adds _ _ ppc _ [] = ppc
5.35 | appl_adds dI oris ppc pbt (selct :: ss) =
5.36 let val itm = appl_add' dI oris ppc pbt selct;
5.37 - in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end
5.38 + in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end
5.39
5.40 fun oris2itms _ _ [] = ([] : itm list) (* WN161130: similar in ptyps ?!? *)
5.41 | oris2itms pbt vat ((i, v, f, d, ts) :: (os: ori list)) =
5.42 @@ -273,38 +273,38 @@
5.43 if dI <> sdI
5.44 then let val its = map (parsitm (assoc_thy dI)) probl;
5.45 val (its, trms) = filter_sep is_Par its;
5.46 - val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec));
5.47 + val pbt = (#ppc o get_pbt) (#2 (Chead.some_spec ospec sspec))
5.48 in (Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
5.49 else
5.50 if pI <> spI
5.51 then if pI = snd3 ospec then (Pbl, probl, meth)
5.52 else
5.53 let val pbt = (#ppc o get_pbt) pI
5.54 - val dI' = #1 (some_spec ospec spec)
5.55 + val dI' = #1 (Chead.some_spec ospec spec)
5.56 val oris = if pI = #2 ospec then oris
5.57 else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
5.58 in (Pbl, appl_adds dI' oris probl pbt
5.59 (map itms2fstr probl), meth) end
5.60 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
5.61 then let val met = (#ppc o get_met) mI
5.62 - val mits = complete_metitms oris probl meth met
5.63 + val mits = Chead.complete_metitms oris probl meth met
5.64 in if foldl and_ (true, map #3 mits)
5.65 then (Pbl, probl, mits) else (Met, probl, mits)
5.66 end
5.67 - else (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
5.68 - ((#ppc o get_pbt) (#2 (some_spec ospec spec)))
5.69 + else (Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
5.70 + ((#ppc o get_pbt) (#2 (Chead.some_spec ospec spec)))
5.71 (imodel2fstr imodel), meth)
5.72 val pt = update_spec pt p spec;
5.73 in if pos_ = Pbl
5.74 - then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
5.75 + then let val {prls,where_,...} = get_pbt (#2 (Chead.some_spec ospec spec))
5.76 val pre =check_preconds(assoc_thy"Isac")prls where_ pits
5.77 in (update_pbl pt p pits,
5.78 - (ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd)
5.79 + (Chead.ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd)
5.80 end
5.81 - else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
5.82 + else let val {prls,pre,...} = get_met (#3 (Chead.some_spec ospec spec))
5.83 val pre = check_preconds (assoc_thy"Isac") prls pre mits
5.84 in (update_met pt p mits,
5.85 - (ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec):ocalhd)
5.86 + (Chead.ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec) : ocalhd)
5.87 end
5.88 end
5.89 end
5.90 @@ -374,7 +374,7 @@
5.91 (* structure copied from complete_solve
5.92 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
5.93 all_modspec etc. has to be inserted at Subproblem'*)
5.94 -fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): calcstate') ifo =
5.95 +fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =
5.96 let
5.97 val fo =
5.98 case p_ of
5.99 @@ -393,21 +393,21 @@
5.100 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
5.101 else
5.102 if pos = ([], Res) (*TODO: we should stop earlier with trying subproblems *)
5.103 - then ("no derivation found", (tacis, c, ptp): calcstate')
5.104 + then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
5.105 else
5.106 let
5.107 val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*)
5.108 val (tacis, c'', ptp) = case tacis of
5.109 ((Subproblem _, _, _)::_) =>
5.110 let
5.111 - val ptp as (pt, (p,_)) = all_modspec ptp (*<--------------------*)
5.112 + val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
5.113 val mI = get_obj g_metID pt p
5.114 in
5.115 nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
5.116 end
5.117 | _ => cs';
5.118 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
5.119 - end;
5.120 + end
5.121
5.122 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
5.123 fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls =
5.124 @@ -455,7 +455,7 @@
5.125 collect all the tacs applied by the way;
5.126 if "no derivation found" then check_error_patterns.
5.127 ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
5.128 -fun inform (cs as (_, _, (pt, pos as (p, _))): calcstate') istr =
5.129 +fun inform (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
5.130 case parse (assoc_thy "Isac") istr of
5.131 SOME f_in =>
5.132 let
5.133 @@ -492,7 +492,7 @@
5.134 | _ => msg_calcstate'
5.135 end
5.136 end
5.137 - | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate')
5.138 + | NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate')
5.139
5.140 (* fill-in patterns an forms.
5.141 returns thm required by "fun in_fillform *)
5.142 @@ -545,8 +545,8 @@
5.143 val tac = get_obj g_tac pt p';
5.144 in
5.145 case applicable_in pos pt tac of
5.146 - Notappl msg => (msg, Tac "")
5.147 - | Appl rew =>
5.148 + Chead.Notappl msg => (msg, Tac "")
5.149 + | Chead.Appl rew =>
5.150 let
5.151 val res = case rew of
5.152 Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
6.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed Nov 30 13:05:08 2016 +0100
6.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Mon Dec 12 18:08:13 2016 +0100
6.3 @@ -14,7 +14,7 @@
6.4 pos' list -> pos' -> (ptree * pos') * taci list -> auto -> string * pos' list * (ptree * pos')
6.5 val locatetac :
6.6 tac -> ptree * (posel list * pos_) -> string * (taci list * pos' list * (ptree * pos'))
6.7 - val step : pos' -> calcstate -> string * calcstate'
6.8 + val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
6.9 val detailstep :
6.10 ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
6.11
6.12 @@ -54,13 +54,13 @@
6.13 (* introduced for test only *)
6.14 val e_tac_ = Tac_ (Pure.thy, "", "", "");
6.15 datatype lOc_ =
6.16 - ERror of string (*after loc_specify, loc_solve*)
6.17 -| UNsafe of calcstate' (*after loc_specify, loc_solve*)
6.18 -| Updated of calcstate'; (*after loc_specify, loc_solve*)
6.19 + ERror of string (*after loc_specify, loc_solve*)
6.20 +| UNsafe of Chead.calcstate' (*after loc_specify, loc_solve*)
6.21 +| Updated of Chead.calcstate' (*after loc_specify, loc_solve*)
6.22
6.23 fun loc_specify_ m (pt,pos) =
6.24 let
6.25 - val (p, _, f, _, _, pt) = specify m pos [] pt;
6.26 + val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
6.27 in
6.28 case f of (Error' (Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
6.29 end
6.30 @@ -75,7 +75,7 @@
6.31
6.32 datatype nxt_ =
6.33 HElpless (**)
6.34 -| Nexts of calcstate; (**)
6.35 +| Nexts of Chead.calcstate (**)
6.36
6.37 (* locate a tactic in a script and apply it if possible;
6.38 report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
6.39 @@ -85,8 +85,8 @@
6.40 val (mI, m) = mk_tac'_ tac;
6.41 in
6.42 case applicable_in p pt m of
6.43 - Notappl _ => ("not-applicable", ([],[], ptp):calcstate')
6.44 - | Appl m =>
6.45 + Chead.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
6.46 + | Chead.Appl m =>
6.47 let
6.48 val x = if member op = specsteps mI
6.49 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
6.50 @@ -114,8 +114,8 @@
6.51 if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
6.52 then
6.53 case mI' of
6.54 - ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
6.55 - | _ => nxt_specif Model_Problem (pt, (p,Pbl))
6.56 + ["no_met"] => Chead.nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
6.57 + | _ => Chead.nxt_specif Model_Problem (pt, (p,Pbl))
6.58 else
6.59 let
6.60 val cpI = if pI = e_pblID then pI' else pI;
6.61 @@ -125,12 +125,12 @@
6.62 val pb = foldl and_ (true, map fst pre);
6.63 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
6.64 val (_, tac) =
6.65 - nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
6.66 + Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
6.67 in
6.68 case tac of
6.69 Apply_Method mI =>
6.70 nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
6.71 - | _ => nxt_specif tac ptp
6.72 + | _ => Chead.nxt_specif tac ptp
6.73 end
6.74 end
6.75
6.76 @@ -138,7 +138,7 @@
6.77 fun set_method (mI:metID) ptp =
6.78 let
6.79 val (mits, pt, p) =
6.80 - case nxt_specif (Specify_Method mI) ptp of
6.81 + case Chead.nxt_specif (Specify_Method mI) ptp of
6.82 ([(_, Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p)
6.83 | _ => error "set_method: case 1 uncovered"
6.84 val pre = [] (*...from Specify_Method'*)
6.85 @@ -156,7 +156,7 @@
6.86 fun set_problem pI (ptp: ptree * pos') =
6.87 let
6.88 val (complete, pits, pre, pt, p) =
6.89 - case nxt_specif (Specify_Problem pI) ptp of
6.90 + case Chead.nxt_specif (Specify_Problem pI) ptp of
6.91 ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
6.92 => (complete, pits, pre, pt, p)
6.93 | _ => error "set_problem: case 1 uncovered"
6.94 @@ -172,7 +172,7 @@
6.95 fun set_theory (tI:thyID) (ptp: ptree * pos') =
6.96 let
6.97 val (complete, pits, pre, pt, p) =
6.98 - case nxt_specif (Specify_Theory tI) ptp of
6.99 + case Chead.nxt_specif (Specify_Theory tI) ptp of
6.100 ([(_, Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
6.101 => (complete, pits, pre, pt, p)
6.102 | _ => error "set_theory: case 1 uncovered"
6.103 @@ -185,11 +185,11 @@
6.104
6.105 (* does a step forward; returns tactic used, ctree updated.
6.106 TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
6.107 -fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
6.108 +fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis): Chead.calcstate) =
6.109 let val pIopt = get_pblID (pt,ip);
6.110 in
6.111 if ip = ([],Res)
6.112 - then ("end-of-calculation", (tacis, [], ptp):calcstate')
6.113 + then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate')
6.114 else
6.115 case tacis of
6.116 (_::_) =>
6.117 @@ -236,29 +236,29 @@
6.118 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
6.119 if autoord auto > 3 andalso just_created (pt, pos)
6.120 then
6.121 - let val ptp = all_modspec (pt, pos);
6.122 + let val ptp = Chead.all_modspec (pt, pos);
6.123 in all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
6.124 else
6.125 if member op = [Pbl, Met] p_
6.126 then
6.127 - if not (is_complete_mod (pt, pos))
6.128 + if not (Chead.is_complete_mod (pt, pos))
6.129 then
6.130 - let val ptp = complete_mod (pt, pos) (*... auto = 2 | 3 *)
6.131 + let val ptp = Chead.complete_mod (pt, pos) (*... auto = 2 | 3 *)
6.132 in
6.133 if autoord auto < 3 then ("ok", c, ptp)
6.134 else
6.135 - if not (is_complete_spec ptp)
6.136 + if not (Chead.is_complete_spec ptp)
6.137 then
6.138 - let val ptp = complete_spec ptp
6.139 + let val ptp = Chead.complete_spec ptp
6.140 in
6.141 if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
6.142 end
6.143 else if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
6.144 end
6.145 else
6.146 - if not (is_complete_spec (pt,pos))
6.147 + if not (Chead.is_complete_spec (pt,pos))
6.148 then
6.149 - let val ptp = complete_spec (pt, pos)
6.150 + let val ptp = Chead.complete_spec (pt, pos)
6.151 in
6.152 if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
6.153 end
6.154 @@ -365,7 +365,7 @@
6.155 delete as soon as TESTg_form -> _mout_ dropped *)
6.156 fun TESTg_form ptp =
6.157 let
6.158 - val (form, _, _) = pt_extract ptp
6.159 + val (form, _, _) = Chead.pt_extract ptp
6.160 in
6.161 case form of
6.162 Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
6.163 @@ -379,7 +379,7 @@
6.164 compare "fun CalcTree" which DOES decode *)
6.165 fun CalcTreeTEST [(fmz, sp)] =
6.166 let
6.167 - val ((pt, p), tacis) = nxt_specify_init_calc (fmz, sp)
6.168 + val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
6.169 val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
6.170 val f = TESTg_form (pt,p)
6.171 in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end
7.1 --- a/src/Tools/isac/Interpret/mstools.sml Wed Nov 30 13:05:08 2016 +0100
7.2 +++ b/src/Tools/isac/Interpret/mstools.sml Mon Dec 12 18:08:13 2016 +0100
7.3 @@ -591,7 +591,14 @@
7.4
7.5 (*. given the input value (from split_dts)
7.6 make the value in a problem-env according to description-type .*)
7.7 -(*28.8.01: .nam and .una impl. properly, others copied .. TODO*)
7.8 +(*28.8.01: .nam and .una impl. properly, others copied .. TODO.
7.9 + 19/03/15 17:33, Makarius wrote:
7.10 + >>> val i = case HOLogic.dest_number t of
7.11 + >>> (Type ("Nat.nat", []), i) => i
7.12 + >>
7.13 + >> Formal names should never be hardwired as ML string constants. Use
7.14 + >> @{type_name nat} above, or better @{typ nat} for the whole type
7.15 +*)
7.16 fun pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v =
7.17 if is_list v
7.18 then [v] (*eg. [r=Arbfix]*)
8.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Nov 30 13:05:08 2016 +0100
8.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Mon Dec 12 18:08:13 2016 +0100
8.3 @@ -347,14 +347,14 @@
8.4 let val thm_deriv = deriv_of_thm'' thm''
8.5 in
8.6 (case applicable_in pos pt tac of
8.7 - Appl (Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
8.8 + Chead.Appl (Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
8.9 ContThm
8.10 {thyID = theory'2thyID thy',
8.11 thm = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
8.12 applto = f, applat = e_term, reword = ord',
8.13 asms = [](*asms ~~ asms'*), lhs = (e_term, e_term)(*(lhs, lhs')*), rhs = (e_term, e_term)(*(rhs, rhs')*),
8.14 result = res, resasms = asm, asmrls = id_rls erls}
8.15 - | Notappl _ =>
8.16 + | Chead.Notappl _ =>
8.17 let
8.18 val pp = par_pblobj pt p
8.19 val thy' = get_obj g_domID pt pp
8.20 @@ -374,7 +374,7 @@
8.21 let val thm = Global_Theory.get_thm (Isac ()) thmID
8.22 in
8.23 (case applicable_in pos pt tac of
8.24 - Appl (Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
8.25 + Chead.Appl (Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
8.26 let
8.27 val thm_deriv = Thm.get_name_hint thm
8.28 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
8.29 @@ -387,7 +387,7 @@
8.30 asms = [](*asms ~~ asms'*), lhs = (e_term, e_term)(*(lhs, lhs')*), rhs = (e_term, e_term)(*(rhs, rhs')*),
8.31 result = res, resasms = asm, asmrls = id_rls erls}
8.32 end
8.33 - | Notappl _ =>
8.34 + | Chead.Notappl _ =>
8.35 let
8.36 val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
8.37 val thm_deriv = Thm.get_name_hint thm
8.38 @@ -408,20 +408,20 @@
8.39 end
8.40 | context_thy (pt, p) (tac as Rewrite_Set rls') =
8.41 (case applicable_in p pt tac of
8.42 - Appl (Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
8.43 + Chead.Appl (Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
8.44 ContRls
8.45 {thyID = theory'2thyID thy',
8.46 rls = rls2guh (thy_containing_rls thy' rls') rls',
8.47 applto = f, result = res, asms = asm}
8.48 - | _ => error ("context_thy Rewrite_Set: not for Notappl"))
8.49 + | _ => error ("context_thy Rewrite_Set: not for Chead.Notappl"))
8.50 | context_thy (pt,p) (tac as Rewrite_Set_Inst (_(*subs*), rls')) =
8.51 (case applicable_in p pt tac of
8.52 - Appl (Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
8.53 + Chead.Appl (Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
8.54 ContRlsInst
8.55 {thyID = theory'2thyID thy',
8.56 rls = rls2guh (thy_containing_rls thy' rls') rls',
8.57 bdvs = subst, applto = f, result = res, asms = asm}
8.58 - | _ => error ("context_thy Rewrite_Set_Inst: not for Notappl"))
8.59 + | _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl"))
8.60 | context_thy (_, p) tac =
8.61 error ("context_thy: not for tac " ^ tac2str tac ^ " at " ^ pos'2str p)
8.62
9.1 --- a/src/Tools/isac/Interpret/script.sml Wed Nov 30 13:05:08 2016 +0100
9.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Dec 12 18:08:13 2016 +0100
9.3 @@ -254,16 +254,16 @@
9.4 if mI = ["no_met"]
9.5 then
9.6 let
9.7 - val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
9.8 + val pors = (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
9.9 handle ERROR "actual args do not match formal args"
9.10 - => (match_ags_msg pI stac ags(*raise exn*); [])
9.11 + => (Chead.match_ags_msg pI stac ags(*raise exn*); [])
9.12 val pI' = refine_ori' pors pI;
9.13 in (pI', pors (* refinement over models with diff.prec only *),
9.14 (hd o #met o get_pbt) pI') end
9.15 - else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
9.16 + else (pI, (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
9.17 handle ERROR "actual args do not match formal args"
9.18 - => (match_ags_msg pI stac ags(*raise exn*); []), mI);
9.19 - val (fmz_, vals) = oris2fmz_vals pors;
9.20 + => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
9.21 + val (fmz_, vals) = Chead.oris2fmz_vals pors;
9.22 val {cas,ppc,thy,...} = get_pbt pI
9.23 val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
9.24 val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
9.25 @@ -271,7 +271,7 @@
9.26 val hdl =
9.27 case cas of
9.28 NONE => pblterm dI pI
9.29 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
9.30 + | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
9.31 val f = subpbl (strip_thy dI) pI
9.32 in (Subproblem (dI, pI), Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
9.33 end
9.34 @@ -416,16 +416,16 @@
9.35 if mI = ["no_met"]
9.36 then
9.37 let
9.38 - val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
9.39 + val pors = (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
9.40 handle ERROR "actual args do not match formal args"
9.41 - => (match_ags_msg pI stac ags(*raise exn*);[]);
9.42 + => (Chead.match_ags_msg pI stac ags(*raise exn*);[]);
9.43 val pI' = refine_ori' pors pI;
9.44 in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o get_pbt) pI')
9.45 end
9.46 - else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
9.47 + else (pI, (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
9.48 handle ERROR "actual args do not match formal args"
9.49 - => (match_ags_msg pI stac ags(*raise exn*); []), mI);
9.50 - val (fmz_, vals) = oris2fmz_vals pors;
9.51 + => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
9.52 + val (fmz_, vals) = Chead.oris2fmz_vals pors;
9.53 val {cas, ppc, thy, ...} = get_pbt pI
9.54 val dI = theory2theory' thy (*take dI from _refined_ pbl*)
9.55 val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
9.56 @@ -433,7 +433,7 @@
9.57 val hdl =
9.58 case cas of
9.59 NONE => pblterm dI pI
9.60 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
9.61 + | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
9.62 val f = subpbl (strip_thy dI) pI
9.63 in
9.64 if domID = dI andalso pblID = pI
9.65 @@ -676,13 +676,13 @@
9.66 AssOnly => (NasNap (v, E))
9.67 | _ =>
9.68 (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
9.69 - Appl m' =>
9.70 + Chead.Appl m' =>
9.71 let
9.72 val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
9.73 val (p'',c',f',pt') =
9.74 generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt;
9.75 in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
9.76 - | Notappl _ => (NasNap (v, E))
9.77 + | Chead.Notappl _ => (NasNap (v, E))
9.78 )
9.79 )
9.80 end)
9.81 @@ -929,7 +929,7 @@
9.82 Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
9.83 | _ =>
9.84 (case applicable_in p pt m of
9.85 - Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
9.86 + Chead.Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
9.87 | _ => Napp E)
9.88 end
9.89 (*GOON*)
10.1 --- a/src/Tools/isac/Interpret/solve.sml Wed Nov 30 13:05:08 2016 +0100
10.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Dec 12 18:08:13 2016 +0100
10.3 @@ -157,7 +157,7 @@
10.4 generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
10.5 (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
10.6 in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
10.7 - ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate')
10.8 + ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)) : Chead.calcstate')
10.9 end
10.10 | NONE => (*execute the first tac in the Script, compare solve m*)
10.11 let
10.12 @@ -276,7 +276,7 @@
10.13 let
10.14 val {srls,ppc,...} = get_met mI;
10.15 val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p;
10.16 - val itms = if itms <> [] then itms else complete_metitms oris probl [] ppc
10.17 + val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
10.18 val thy' = get_obj g_domID pt p;
10.19 val thy = assoc_thy thy';
10.20 val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = Lucin.init_scrstate thy itms mI;
10.21 @@ -289,7 +289,7 @@
10.22 val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
10.23 val (pos,c,_,pt) = (*implicit Take*)
10.24 generate1 thy tac_ (is, ctxt) pos pt
10.25 - in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end
10.26 + in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)) : Chead.calcstate' end
10.27 | NONE =>
10.28 let
10.29 val pt = update_env pt (fst pos) (SOME (is, ctxt))
10.30 @@ -355,7 +355,7 @@
10.31 (* find the next tac from the script, nxt_solv will update the ptree *)
10.32 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
10.33 if e_metID = get_obj g_metID pt (par_pblobj pt p)
10.34 - then ([], [], (pt,(p,p_))):calcstate'
10.35 + then ([], [], (pt, (p, p_))) : Chead.calcstate'
10.36 else
10.37 let
10.38 val thy' = get_obj g_domID pt (par_pblobj pt p);
10.39 @@ -395,7 +395,7 @@
10.40 if member op = [Pbl,Met] p_
10.41 then
10.42 let
10.43 - val ptp = all_modspec ptp
10.44 + val ptp = Chead.all_modspec ptp
10.45 val (_, c', ptp) = all_solve auto c ptp
10.46 in complete_solve auto (c @ c') ptp end
10.47 else
10.48 @@ -405,7 +405,7 @@
10.49 then ("ok", c @ c', ptp)
10.50 else
10.51 let
10.52 - val ptp = all_modspec ptp'
10.53 + val ptp = Chead.all_modspec ptp'
10.54 val (_, c'', ptp) = all_solve auto (c @ c') ptp
10.55 in complete_solve auto (c @ c'@ c'') ptp end
10.56 | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
10.57 @@ -469,12 +469,12 @@
10.58 *)
10.59 fun get_form ((mI,m):tac'_) ((p,p_):pos') pt =
10.60 case applicable_in (p,p_) pt m of
10.61 - Notappl e => Error' (Error_ e)
10.62 - | Appl m =>
10.63 + Chead.Notappl e => Error' (Error_ e)
10.64 + | Chead.Appl m =>
10.65 (* val Appl m=applicable_in (p,p_) pt m;
10.66 *)
10.67 if member op = specsteps mI
10.68 - then let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
10.69 + then let val (_,_,f,_,_,_) = Chead.specify m (p,p_) [] pt
10.70 in f end
10.71 else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
10.72 in (*f*) EmptyMout end;
11.1 --- a/src/Tools/isac/library.sml Wed Nov 30 13:05:08 2016 +0100
11.2 +++ b/src/Tools/isac/library.sml Mon Dec 12 18:08:13 2016 +0100
11.3 @@ -36,6 +36,7 @@
11.4 fun last_elem [] = error "last_elem" (*FIXME.2009*)
11.5 | last_elem [x] = x
11.6 | last_elem (_ :: xs) = last_elem xs;
11.7 +fun member_swap eq x xs = member eq xs x
11.8
11.9 fun gen_mem eq (x, []) = false (*FIXME.2009*)
11.10 | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
11.11 @@ -369,3 +370,10 @@
11.12 | enum i (s :: ss) = (s ^ "--" ^ string_of_int i) :: (enum (i + 1) ss)
11.13 in enum 1 strs end
11.14
11.15 +fun maxl [] = error "maxl of []"
11.16 + | maxl (y :: ys) =
11.17 + let
11.18 + fun mx x [] = x
11.19 + | mx x (y :: ys) = if x < (y: int) then mx y ys else mx x ys
11.20 + in mx y ys end
11.21 +
12.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Wed Nov 30 13:05:08 2016 +0100
12.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Mon Dec 12 18:08:13 2016 +0100
12.3 @@ -136,7 +136,7 @@
12.4 *}
12.5
12.6 ML {*
12.7 - show_pt pt;
12.8 + Chead.show_pt pt;
12.9 *}
12.10
12.11 end
12.12 \ No newline at end of file
13.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy Wed Nov 30 13:05:08 2016 +0100
13.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy Mon Dec 12 18:08:13 2016 +0100
13.3 @@ -37,7 +37,7 @@
13.4
13.5 ML{*
13.6 f2str f;
13.7 - show_pt pt;
13.8 + Chead.show_pt pt;
13.9 *}
13.10
13.11 end
14.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Nov 30 13:05:08 2016 +0100
14.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Dec 12 18:08:13 2016 +0100
14.3 @@ -321,7 +321,7 @@
14.4 (*
14.5 * [z = 1 / 2, z = -1 / 4]
14.6 *)
14.7 - show_pt pt;
14.8 + Chead.show_pt pt;
14.9 val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
14.10 *}
14.11
14.12 @@ -1502,7 +1502,7 @@
14.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.14 *}
14.15 ML {*
14.16 -show_pt pt;
14.17 +Chead.show_pt pt;
14.18 *}
14.19 ML {*
14.20 *}
15.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Wed Nov 30 13:05:08 2016 +0100
15.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Mon Dec 12 18:08:13 2016 +0100
15.3 @@ -133,7 +133,7 @@
15.4 With 'show_pt' the calculation can be inspected (in a more or less readable
15.5 format) by clicking the checkbox <Tracing> on top of the <Output> window:
15.6 *}
15.7 -ML {* show_pt pt *}
15.8 +ML {* Chead.show_pt pt *}
15.9
15.10
15.11 section {* Test further examples *}
16.1 --- a/test/Tools/isac/Interpret/calchead.sml Wed Nov 30 13:05:08 2016 +0100
16.2 +++ b/test/Tools/isac/Interpret/calchead.sml Mon Dec 12 18:08:13 2016 +0100
16.3 @@ -18,6 +18,12 @@
16.4 "--------- regr.test fun cpy_nam ------------------------";
16.5 "--------- check specify phase --------------------------";
16.6 "--------- check: fmz matches pbt -----------------------";
16.7 +"--------- fun typeless ---------------------------------";
16.8 +"--------- fun variants_in ------------------------------";
16.9 +"--------- fun is_list_type -----------------------------";
16.10 +"--------- fun has_list_type ----------------------------";
16.11 +"--------- fun tag_form ---------------------------------";
16.12 +"--------- fun foldr1, foldl1 ---------------------------";
16.13 "--------------------------------------------------------";
16.14 "--------------------------------------------------------";
16.15 "--------------------------------------------------------";
16.16 @@ -861,3 +867,89 @@
16.17 val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
16.18 ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;
16.19
16.20 +"--------- fun typeless ---------------------------------";
16.21 +"--------- fun typeless ---------------------------------";
16.22 +"--------- fun typeless ---------------------------------";
16.23 +(*
16.24 +> val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
16.25 +> val (_,t1) = split_dsc_t hs (Thm.term_of ct);
16.26 +> val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
16.27 +> val (_,t2) = split_dsc_t hs (Thm.term_of ct);
16.28 +> typeless t1 = typeless t2;
16.29 +val it = true : bool
16.30 +*)
16.31 +"--------- fun variants_in ------------------------------";
16.32 +"--------- fun variants_in ------------------------------";
16.33 +"--------- fun variants_in ------------------------------";
16.34 +(*
16.35 +> cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
16.36 +val it = ([3],[4,5,5,5,5,5]) : int list * int list
16.37 +> coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
16.38 +val it = [1,3,1,5] : int list
16.39 +*)
16.40 +"--------- fun is_list_type -----------------------------";
16.41 +"--------- fun is_list_type -----------------------------";
16.42 +"--------- fun is_list_type -----------------------------";
16.43 +(* fun destr (Type(str,sort)) = (str,sort);
16.44 +> val (SOME ct) = parse thy "lll::real list";
16.45 +> val ty = (#T o rep_cterm) ct;
16.46 +> is_list_type ty;
16.47 +val it = true : bool
16.48 +> destr ty;
16.49 +val it = ("List.list",["RealDef.real"]) : string * typ list
16.50 +> atomty ((#t o rep_cterm) ct);
16.51 +*** -------------
16.52 +*** Free ( lll, real list)
16.53 +val it = () : unit
16.54 +
16.55 +> val (SOME ct) = parse thy "[lll::real]";
16.56 +> val ty = (#T o rep_cterm) ct;
16.57 +> is_list_type ty;
16.58 +val it = true : bool
16.59 +> destr ty;
16.60 +val it = ("List.list",["'a"]) : string * typ list
16.61 +> atomty ((#t o rep_cterm) ct);
16.62 +*** -------------
16.63 +*** Const ( List.list.Cons, [real, real list] => real list)
16.64 +*** Free ( lll, real)
16.65 +*** Const ( List.list.Nil, real list)
16.66 +
16.67 +> val (SOME ct) = parse thy "lll";
16.68 +> val ty = (#T o rep_cterm) ct;
16.69 +> is_list_type ty;
16.70 +val it = false : bool *)
16.71 +"--------- fun has_list_type ----------------------------";
16.72 +"--------- fun has_list_type ----------------------------";
16.73 +"--------- fun has_list_type ----------------------------";
16.74 +(*
16.75 +> val (SOME ct) = parse thy "lll::real list";
16.76 +> has_list_type (Thm.term_of ct);
16.77 +val it = true : bool
16.78 +> val (SOME ct) = parse thy "[lll::real]";
16.79 +> has_list_type (Thm.term_of ct);
16.80 +val it = false : bool *)
16.81 +"--------- fun tag_form ---------------------------------";
16.82 +"--------- fun tag_form ---------------------------------";
16.83 +"--------- fun tag_form ---------------------------------";
16.84 +(* val formal = (the o (parse thy)) "[R::real]";
16.85 +> val given = (the o (parse thy)) "fixed_values (cs::real list)";
16.86 +> tag_form thy (formal, given);
16.87 +val it = "fixed_values [R]" : cterm
16.88 +*)
16.89 +"--------- fun foldr1, foldl1 ---------------------------";
16.90 +"--------- fun foldr1, foldl1 ---------------------------";
16.91 +"--------- fun foldr1, foldl1 ---------------------------";
16.92 +(*
16.93 +> val (SOME ct) = parse thy "[a=b,c=d,e=f]";
16.94 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
16.95 +> val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
16.96 +> Thm.global_cterm_of thy conj;
16.97 +val it = "(a = b & c = d) & e = f" : cterm
16.98 +*)
16.99 +(*
16.100 +> val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
16.101 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
16.102 +> val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
16.103 +> Thm.global_cterm_of thy conj;
16.104 +val it = "a = b & c = d & e = f & g = h" : cterm
16.105 +*)
17.1 --- a/test/Tools/isac/Test_Isac.thy Wed Nov 30 13:05:08 2016 +0100
17.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Dec 12 18:08:13 2016 +0100
17.3 @@ -74,6 +74,7 @@
17.4 open Lucin; appy;
17.5 open Inform; cas_input;
17.6 open Rtools; trtas2str;
17.7 + open Chead; pt_extract;
17.8 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
17.9 *}
17.10 ML {*
18.1 --- a/test/Tools/isac/Test_Some.thy Wed Nov 30 13:05:08 2016 +0100
18.2 +++ b/test/Tools/isac/Test_Some.thy Mon Dec 12 18:08:13 2016 +0100
18.3 @@ -1,6 +1,18 @@
18.4 -theory Test_Some imports Build_Thydata begin
18.5 +theory Test_Some imports Build_Thydata
18.6 +begin
18.7 +ML {*
18.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
18.9 + (* these vvv test, if additional funs intermediately added to structure *)
18.10 + open Kernel;
18.11 + open Math_Engine; CalcTreeTEST;
18.12 + open Lucin; appy;
18.13 + open Inform; cas_input;
18.14 + open Rtools; trtas2str;
18.15 + open Chead; pt_extract;
18.16 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
18.17 +*}
18.18 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
18.19 -ML_file "Frontend/use-cases.sml"
18.20 +ML_file "Interpret/calchead.sml"
18.21
18.22 section {* code for copy & paste ===============================================================*}
18.23 ML {*