1.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed Oct 06 15:12:41 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Fri Oct 08 18:51:23 2010 +0200
1.3 @@ -1,11 +1,8 @@
1.4 -(* Specify-phase: specifying and modeling a problem or a subproblem. The
1.5 - most important types are declared in mstools.sml.
1.6 - author: Walther Neuper
1.7 - 991122
1.8 +(* Title: Specify-phase: specifying and modeling a problem or a subproblem. The
1.9 + most important types are declared in mstools.sml.
1.10 + Author: Walther Neuper 991122
1.11 (c) due to copyright terms
1.12
1.13 -use"ME/calchead.sml";
1.14 -use"calchead.sml";
1.15 12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.16 10 20 30 40 50 60 70 80
1.17 *)
1.18 @@ -481,29 +478,22 @@
1.19 (*.get the first term in ts from ori.*)
1.20 (* val (_,_,fd,d,ts) = hd miss;
1.21 *)
1.22 -fun getr_ct thy ((_,_,fd,d,ts):ori) =
1.23 - (fd, ((Syntax.string_of_term (thy2ctxt thy)) o
1.24 - (comp_dts thy)) (d,[hd ts]):cterm');
1.25 +fun getr_ct thy ((_, _, fd, d, ts) : ori) =
1.26 + (fd, ((Syntax.string_of_term (thy2ctxt thy)) o
1.27 + (comp_dts thy)) (d,[hd ts]) : cterm');
1.28 (* val t = comp_dts thy (d,[hd ts]);
1.29 *)
1.30
1.31 -(* get a term from ori, notyet input in itm *)
1.32 -fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) =
1.33 +(* get a term from ori, notyet input in itm.
1.34 + the term from ori is thrown back to a string in order to reuse
1.35 + machinery for immediate input by the user. *)
1.36 +fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.37 (fd, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy))
1.38 - (d, subtract op = (ts_in itm_) ts):cterm');
1.39 -(* test-maximum.sml fmy <> [], Init_Proof ...
1.40 - val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl;
1.41 - val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
1.42 - atomty d;
1.43 - atomty d';
1.44 - atomty (hd ts);
1.45 - atomty ts';
1.46 - cterm_of thy (d $ (hd ts));
1.47 - cterm_of thy (d' $ ts');
1.48 -
1.49 - comp_dts thy (d,ts);
1.50 - *)
1.51 -
1.52 + (d, subtract op = (ts_in itm_) ts) : cterm');
1.53 +fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.54 + (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
1.55 + (comp_dts thy))
1.56 + (d, subtract op = (ts_in itm_) ts) : cterm');
1.57
1.58 (* in FE dsc, not dat: this is in itms ...*)
1.59 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
1.60 @@ -537,8 +527,6 @@
1.61 andalso (#3 ori) <>"#undef";
1.62 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
1.63 fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
1.64 -(* val itm = hd icl; val (_,_,_,d,ts) = v6;
1.65 - *)
1.66 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
1.67 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
1.68 fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
1.69 @@ -579,83 +567,50 @@
1.70 error ("mk_additem: called with field '"^str^"'");
1.71
1.72
1.73 -
1.74 -
1.75 -
1.76 -(* find the next tac in specify (except nxt_model_pbl)
1.77 - 4.00.: TODO: do not return a pos !!!
1.78 - (sind from DG comes the _OLD_ writepos)*)
1.79 -(*
1.80 -> val (pbl,pbt,mpc) =(pbl',get_pbt cpI,(#ppc o get_met) cmI);
1.81 -> val (dI,pI,mI) = empty_spec;
1.82 -> nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*))
1.83 - ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec);
1.84 -
1.85 -at Init_Proof:
1.86 -> val met = [];val (pbt,mpc) = (get_pbt pI',(#ppc o get_met) mI');
1.87 -> val (dI,pI,mI) = empty_spec;
1.88 -> nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*))
1.89 - ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec);
1.90 - *)
1.91 -
1.92 -(*. determine the next step of specification;
1.93 - not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
1.94 -eg. in rootpbl 'no_met':
1.95 +(* determine the next step of specification;
1.96 + not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
1.97 + eg. in rootpbl 'no_met':
1.98 args:
1.99 - preok predicates are _all_ ok, or problem matches completely
1.100 + preok predicates are _all_ ok (and problem matches completely)
1.101 oris immediately from formalization
1.102 (dI',pI',mI') specification coming from author/parent-problem
1.103 (pbl, item lists specified by user
1.104 met) -"-, tacitly completed by copy_probl
1.105 (dI,pI,mI) specification explicitly done by the user
1.106 (pbt, mpc) problem type, guard of method
1.107 -.*)
1.108 -(* val (preok,pbl,pbt,mpc)=(pb,pbl',(#ppc o get_pbt) cpI,(#ppc o get_met) cmI);
1.109 - val (preok,pbl,pbt,mpc)=(pb,pbl',ppc,(#ppc o get_met) cmI);
1.110 - val (Pbl, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) =
1.111 - (p_, pb, oris, (dI',pI',mI'), (probl,meth),
1.112 - (ppc, (#ppc o get_met) cmI), (dI,pI,mI));
1.113 - *)
1.114 -fun nxt_spec Pbl preok (oris:ori list) ((dI',pI',mI'):spec)
1.115 - ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec) =
1.116 - ((*tracing"### nxt_spec Pbl";*)
1.117 - if dI'=e_domID andalso dI=e_domID then (Pbl, Specify_Theory dI')
1.118 - else if pI'=e_pblID andalso pI=e_pblID then (Pbl, Specify_Problem pI')
1.119 - else case find_first (is_error o #5) (pbl:itm list) of
1.120 - SOME (_,_,_,fd,itm_) =>
1.121 +*)
1.122 +fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
1.123 + ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
1.124 + ((*tracing"### nxt_spec Pbl";*)
1.125 + if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
1.126 + else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
1.127 + else case find_first (is_error o #5) (pbl:itm list) of
1.128 + SOME (_, _, _, fd, itm_) =>
1.129 (Pbl, mk_delete
1.130 - (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
1.131 - | NONE =>
1.132 - ((*tracing"### nxt_spec is_error NONE";*)
1.133 - case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))
1.134 - oris pbt pbl of
1.135 -(* val SOME (fd,ct') = nxt_add (assoc_thy (if dI=e_domID then dI' else dI))
1.136 - oris pbt pbl;
1.137 - *)
1.138 - SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
1.139 - (Pbl, mk_additem fd ct'))
1.140 - | NONE => (*pbl-items complete*)
1.141 - if not preok then (Pbl, Refine_Problem pI')
1.142 - else
1.143 - if dI = e_domID then (Pbl, Specify_Theory dI')
1.144 - else if pI = e_pblID then (Pbl, Specify_Problem pI')
1.145 - else if mI = e_metID then (Pbl, Specify_Method mI')
1.146 - else
1.147 - case find_first (is_error o #5) met of
1.148 + (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
1.149 + | NONE =>
1.150 + ((*tracing"### nxt_spec is_error NONE";*)
1.151 + case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
1.152 + oris pbt pbl of
1.153 + SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
1.154 + (Pbl, mk_additem fd ct'))
1.155 + | NONE => (*pbl-items complete*)
1.156 + if not preok then (Pbl, Refine_Problem pI')
1.157 + else
1.158 + if dI = e_domID then (Pbl, Specify_Theory dI')
1.159 + else if pI = e_pblID then (Pbl, Specify_Problem pI')
1.160 + else if mI = e_metID then (Pbl, Specify_Method mI')
1.161 + else
1.162 + case find_first (is_error o #5) met of
1.163 SOME (_,_,_,fd,itm_) =>
1.164 - (Met, mk_delete (assoc_thy dI) fd itm_)
1.165 + (Met, mk_delete (assoc_thy dI) fd itm_)
1.166 | NONE =>
1.167 - (case nxt_add (assoc_thy dI) oris mpc met of
1.168 - SOME (fd,ct') => (*30.8.01: pre?!?*)
1.169 - (Met, mk_additem fd ct')
1.170 - | NONE =>
1.171 - ((*Solv 3.4.00*)Met, Apply_Method mI))))
1.172 -(* val preok=pb; val (pbl, met) = (pbl,met');
1.173 - val (pbt,mpc)=((#ppc o get_pbt) cpI,(#ppc o get_met) cmI);
1.174 - val (Met, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) =
1.175 - (p_, pb, oris, (dI',pI',mI'), (probl,meth),
1.176 - (ppc, (#ppc o get_met) cmI), (dI,pI,mI));
1.177 - *)
1.178 + (case nxt_add (assoc_thy dI) oris mpc met of
1.179 + SOME (fd,ct') => (*30.8.01: pre?!?*)
1.180 + (Met, mk_additem fd ct')
1.181 + | NONE =>
1.182 + ((*Solv 3.4.00*)Met, Apply_Method mI))))
1.183 +
1.184 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
1.185 ((*tracing"### nxt_spec Met"; *)
1.186 case find_first (is_error o #5) met of
1.187 @@ -843,8 +798,7 @@
1.188 | Err of string; (*error-message*)
1.189
1.190
1.191 -(*. add an item; check wrt. oris and pbt .*)
1.192 -
1.193 +(** add an item to the model; check wrt. oris and pbt **)
1.194 (* in contrary to oris<>[] below, this part handles user-input
1.195 extremely acceptive, i.e. accept input instead error-msg *)
1.196 fun appl_add thy sel ([]:ori list) ppc pbt ct' =
1.197 @@ -891,29 +845,17 @@
1.198 )
1.199 end
1.200 end
1.201 -(*. add ct to ppc .*)
1.202 +(* add ct to ppc *)
1.203 (*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*)
1.204 -(* val (ppc,pbt) = (pbl, ppc);
1.205 - val (ppc,pbt) = (met, (#ppc o get_met) cmI);
1.206 -
1.207 - val (ppc,pbt) = (pbl, (#ppc o get_pbt) cpI);
1.208 - *)
1.209 - | appl_add thy sel oris ppc pbt(*only for upd_envv*) ct =
1.210 - let
1.211 - val ctopt = parse thy ct;
1.212 - in case ctopt of
1.213 - NONE => Err ("syntax error in "^ct)
1.214 - | SOME ct =>(* val SOME ct = ctopt;
1.215 - val (msg,ori',all) = is_known thy sel oris (term_of ct);
1.216 - val (msg,itm) = is_notyet_input thy ppc all ori' pbt;
1.217 - *)
1.218 - (case is_known thy sel oris (term_of ct) of
1.219 - ("",ori'(*ts='ct'*), all) =>
1.220 - (case is_notyet_input thy ppc all ori' pbt of
1.221 - ("",itm) => Add itm
1.222 - | (msg,_) => Err msg)
1.223 - | (msg,_,_) => Err msg)
1.224 - end;
1.225 + | appl_add thy sel oris ppc pbt (*only for upd_envv*) str =
1.226 + case parse thy str of
1.227 + NONE => Err ("syntax error in " ^ str)
1.228 + | SOME t => case is_known thy sel oris (term_of t) of
1.229 + ("", ori', all) =>
1.230 + (case is_notyet_input thy ppc all ori' pbt of
1.231 + ("", itm) => Add itm
1.232 + | (msg, _) => Err msg)
1.233 + | (msg, _, _) => Err msg;
1.234 (*
1.235 > val (msg,itm) = is_notyet_input thy ppc all ori';
1.236 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
1.237 @@ -1400,7 +1342,7 @@
1.238 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1.239 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1.240 *)
1.241 -fun nxt_specif_additem sel ct (ptp as (pt,(p,Pbl))) =
1.242 +fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1.243 let
1.244 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1.245 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1.246 @@ -1540,15 +1482,15 @@
1.247 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1.248 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1.249 let
1.250 - val (PblObj{origin=(oris,ospec,_),probl,spec,...}) = get_obj I pt p
1.251 - val (dI,pI,mI) = some_spec ospec spec
1.252 + val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1.253 + val (dI, pI, mI) = some_spec ospec spec
1.254 val thy = assoc_thy dI
1.255 - val mpc = (#ppc o get_met) mI (*just for reuse complete_mod_*)
1.256 - val {cas,ppc,...} = get_pbt pI
1.257 - val pbl = init_pbl ppc (*fill in descriptions*)
1.258 - (*--------------if you think, this should be done by the Dialog
1.259 + val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1.260 + val {cas, ppc, ...} = get_pbt pI
1.261 + val pbl = init_pbl ppc (* fill in descriptions *)
1.262 + (*----------------if you think, this should be done by the Dialog
1.263 in the java front-end, search there for WN060225-modelProblem----*)
1.264 - val (pbl,met) = case cas of NONE => (pbl,[])
1.265 + val (pbl, met) = case cas of NONE => (pbl, [])
1.266 | _ => complete_mod_ (oris, mpc, ppc, probl)
1.267 (*----------------------------------------------------------------*)
1.268 val tac_ = Model_Problem' (pI, pbl, met)
1.269 @@ -1692,28 +1634,25 @@
1.270 in ((pt,([],Pbl)), []) end
1.271 (* val (fmz, (dI,pI,mI)) = (fmz, sp);
1.272 *)
1.273 - | nxt_specify_init_calc (fmz:fmz_,(dI,pI,mI):spec) =
1.274 - let (* either """"""""""""""" all empty or complete *)
1.275 + | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1.276 + let (* both """"""""""""""""""""""""" either empty or complete *)
1.277 val thy = assoc_thy dI
1.278 val (pI, pors, mI) =
1.279 if mI = ["no_met"]
1.280 then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI)
1.281 val pI' = refine_ori' pors pI;
1.282 - in (pI', pors (*refinement over models with diff.prec only*),
1.283 + in (pI', pors(*refinement over models with diff.precond only*),
1.284 (hd o #met o get_pbt) pI') end
1.285 else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI)
1.286 - val {cas,ppc,thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1.287 + val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1.288 val dI = theory2theory' (maxthy thy thy');
1.289 val hdl = case cas of
1.290 NONE => pblterm dI pI
1.291 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1.292 ~~~ vals_of_oris pors) t
1.293 - val (pt,_) = cappend_problem e_ptree [] e_istate (fmz,(dI,pI,mI))
1.294 - (pors,(dI,pI,mI),hdl)
1.295 - (*val pbl = init_pbl ppc WN.9.03: done by Model/Refine_Problem
1.296 - val pt = update_pbl pt [] pbl*)
1.297 - in ((pt,([],Pbl)), fst3 (nxt_specif Model_Problem (pt, ([],Pbl))))
1.298 - end;
1.299 + val (pt, _) = cappend_problem e_ptree [] e_istate (fmz, (dI, pI, mI))
1.300 + (pors, (dI, pI, mI), hdl)
1.301 + in ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) end;
1.302
1.303
1.304