diff -r 4c52ad406c20 -r efdeff9df986 src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Wed Oct 06 15:12:41 2010 +0200 +++ b/src/Tools/isac/Interpret/calchead.sml Fri Oct 08 18:51:23 2010 +0200 @@ -1,11 +1,8 @@ -(* Specify-phase: specifying and modeling a problem or a subproblem. The - most important types are declared in mstools.sml. - author: Walther Neuper - 991122 +(* Title: Specify-phase: specifying and modeling a problem or a subproblem. The + most important types are declared in mstools.sml. + Author: Walther Neuper 991122 (c) due to copyright terms -use"ME/calchead.sml"; -use"calchead.sml"; 12345678901234567890123456789012345678901234567890123456789012345678901234567890 10 20 30 40 50 60 70 80 *) @@ -481,29 +478,22 @@ (*.get the first term in ts from ori.*) (* val (_,_,fd,d,ts) = hd miss; *) -fun getr_ct thy ((_,_,fd,d,ts):ori) = - (fd, ((Syntax.string_of_term (thy2ctxt thy)) o - (comp_dts thy)) (d,[hd ts]):cterm'); +fun getr_ct thy ((_, _, fd, d, ts) : ori) = + (fd, ((Syntax.string_of_term (thy2ctxt thy)) o + (comp_dts thy)) (d,[hd ts]) : cterm'); (* val t = comp_dts thy (d,[hd ts]); *) -(* get a term from ori, notyet input in itm *) -fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) = +(* get a term from ori, notyet input in itm. + the term from ori is thrown back to a string in order to reuse + machinery for immediate input by the user. *) +fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) = (fd, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy)) - (d, subtract op = (ts_in itm_) ts):cterm'); -(* test-maximum.sml fmy <> [], Init_Proof ... - val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl; - val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; - atomty d; - atomty d'; - atomty (hd ts); - atomty ts'; - cterm_of thy (d $ (hd ts)); - cterm_of thy (d' $ ts'); - - comp_dts thy (d,ts); - *) - + (d, subtract op = (ts_in itm_) ts) : cterm'); +fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) = + (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o + (comp_dts thy)) + (d, subtract op = (ts_in itm_) ts) : cterm'); (* in FE dsc, not dat: this is in itms ...*) fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true @@ -537,8 +527,6 @@ andalso (#3 ori) <>"#undef"; fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm)); fun test_id ids r = curry (op mem) (#1 (r:ori)) ids; -(* val itm = hd icl; val (_,_,_,d,ts) = v6; - *) fun test_subset (itm:itm) ((_,_,_,d,ts):ori) = (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts); fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false @@ -579,83 +567,50 @@ error ("mk_additem: called with field '"^str^"'"); - - - -(* find the next tac in specify (except nxt_model_pbl) - 4.00.: TODO: do not return a pos !!! - (sind from DG comes the _OLD_ writepos)*) -(* -> val (pbl,pbt,mpc) =(pbl',get_pbt cpI,(#ppc o get_met) cmI); -> val (dI,pI,mI) = empty_spec; -> nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*)) - ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec); - -at Init_Proof: -> val met = [];val (pbt,mpc) = (get_pbt pI',(#ppc o get_met) mI'); -> val (dI,pI,mI) = empty_spec; -> nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*)) - ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec); - *) - -(*. determine the next step of specification; - not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met)) -eg. in rootpbl 'no_met': +(* determine the next step of specification; + not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met)) + eg. in rootpbl 'no_met': args: - preok predicates are _all_ ok, or problem matches completely + preok predicates are _all_ ok (and problem matches completely) oris immediately from formalization (dI',pI',mI') specification coming from author/parent-problem (pbl, item lists specified by user met) -"-, tacitly completed by copy_probl (dI,pI,mI) specification explicitly done by the user (pbt, mpc) problem type, guard of method -.*) -(* val (preok,pbl,pbt,mpc)=(pb,pbl',(#ppc o get_pbt) cpI,(#ppc o get_met) cmI); - val (preok,pbl,pbt,mpc)=(pb,pbl',ppc,(#ppc o get_met) cmI); - val (Pbl, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) = - (p_, pb, oris, (dI',pI',mI'), (probl,meth), - (ppc, (#ppc o get_met) cmI), (dI,pI,mI)); - *) -fun nxt_spec Pbl preok (oris:ori list) ((dI',pI',mI'):spec) - ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec) = - ((*tracing"### nxt_spec Pbl";*) - if dI'=e_domID andalso dI=e_domID then (Pbl, Specify_Theory dI') - else if pI'=e_pblID andalso pI=e_pblID then (Pbl, Specify_Problem pI') - else case find_first (is_error o #5) (pbl:itm list) of - SOME (_,_,_,fd,itm_) => +*) +fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec) + ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) = + ((*tracing"### nxt_spec Pbl";*) + if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI') + else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI') + else case find_first (is_error o #5) (pbl:itm list) of + SOME (_, _, _, fd, itm_) => (Pbl, mk_delete - (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_) - | NONE => - ((*tracing"### nxt_spec is_error NONE";*) - case nxt_add (assoc_thy (if dI=e_domID then dI' else dI)) - oris pbt pbl of -(* val SOME (fd,ct') = nxt_add (assoc_thy (if dI=e_domID then dI' else dI)) - oris pbt pbl; - *) - SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*) - (Pbl, mk_additem fd ct')) - | NONE => (*pbl-items complete*) - if not preok then (Pbl, Refine_Problem pI') - else - if dI = e_domID then (Pbl, Specify_Theory dI') - else if pI = e_pblID then (Pbl, Specify_Problem pI') - else if mI = e_metID then (Pbl, Specify_Method mI') - else - case find_first (is_error o #5) met of + (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_) + | NONE => + ((*tracing"### nxt_spec is_error NONE";*) + case nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) + oris pbt pbl of + SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*) + (Pbl, mk_additem fd ct')) + | NONE => (*pbl-items complete*) + if not preok then (Pbl, Refine_Problem pI') + else + if dI = e_domID then (Pbl, Specify_Theory dI') + else if pI = e_pblID then (Pbl, Specify_Problem pI') + else if mI = e_metID then (Pbl, Specify_Method mI') + else + case find_first (is_error o #5) met of SOME (_,_,_,fd,itm_) => - (Met, mk_delete (assoc_thy dI) fd itm_) + (Met, mk_delete (assoc_thy dI) fd itm_) | NONE => - (case nxt_add (assoc_thy dI) oris mpc met of - SOME (fd,ct') => (*30.8.01: pre?!?*) - (Met, mk_additem fd ct') - | NONE => - ((*Solv 3.4.00*)Met, Apply_Method mI)))) -(* val preok=pb; val (pbl, met) = (pbl,met'); - val (pbt,mpc)=((#ppc o get_pbt) cpI,(#ppc o get_met) cmI); - val (Met, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) = - (p_, pb, oris, (dI',pI',mI'), (probl,meth), - (ppc, (#ppc o get_met) cmI), (dI,pI,mI)); - *) + (case nxt_add (assoc_thy dI) oris mpc met of + SOME (fd,ct') => (*30.8.01: pre?!?*) + (Met, mk_additem fd ct') + | NONE => + ((*Solv 3.4.00*)Met, Apply_Method mI)))) + | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) = ((*tracing"### nxt_spec Met"; *) case find_first (is_error o #5) met of @@ -843,8 +798,7 @@ | Err of string; (*error-message*) -(*. add an item; check wrt. oris and pbt .*) - +(** add an item to the model; check wrt. oris and pbt **) (* in contrary to oris<>[] below, this part handles user-input extremely acceptive, i.e. accept input instead error-msg *) fun appl_add thy sel ([]:ori list) ppc pbt ct' = @@ -891,29 +845,17 @@ ) end end -(*. add ct to ppc .*) +(* add ct to ppc *) (*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*) -(* val (ppc,pbt) = (pbl, ppc); - val (ppc,pbt) = (met, (#ppc o get_met) cmI); - - val (ppc,pbt) = (pbl, (#ppc o get_pbt) cpI); - *) - | appl_add thy sel oris ppc pbt(*only for upd_envv*) ct = - let - val ctopt = parse thy ct; - in case ctopt of - NONE => Err ("syntax error in "^ct) - | SOME ct =>(* val SOME ct = ctopt; - val (msg,ori',all) = is_known thy sel oris (term_of ct); - val (msg,itm) = is_notyet_input thy ppc all ori' pbt; - *) - (case is_known thy sel oris (term_of ct) of - ("",ori'(*ts='ct'*), all) => - (case is_notyet_input thy ppc all ori' pbt of - ("",itm) => Add itm - | (msg,_) => Err msg) - | (msg,_,_) => Err msg) - end; + | appl_add thy sel oris ppc pbt (*only for upd_envv*) str = + case parse thy str of + NONE => Err ("syntax error in " ^ str) + | SOME t => case is_known thy sel oris (term_of t) of + ("", ori', all) => + (case is_notyet_input thy ppc all ori' pbt of + ("", itm) => Add itm + | (msg, _) => Err msg) + | (msg, _, _) => Err msg; (* > val (msg,itm) = is_notyet_input thy ppc all ori'; val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm @@ -1400,7 +1342,7 @@ (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp); val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp); *) -fun nxt_specif_additem sel ct (ptp as (pt,(p,Pbl))) = +fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) = let val (PblObj{meth=met,origin=(oris,(dI',pI',_),_), probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p; @@ -1540,15 +1482,15 @@ (*WN.24.10.03 fun nxt_solv = ...................................??*) fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) = let - val (PblObj{origin=(oris,ospec,_),probl,spec,...}) = get_obj I pt p - val (dI,pI,mI) = some_spec ospec spec + val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p + val (dI, pI, mI) = some_spec ospec spec val thy = assoc_thy dI - val mpc = (#ppc o get_met) mI (*just for reuse complete_mod_*) - val {cas,ppc,...} = get_pbt pI - val pbl = init_pbl ppc (*fill in descriptions*) - (*--------------if you think, this should be done by the Dialog + val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *) + val {cas, ppc, ...} = get_pbt pI + val pbl = init_pbl ppc (* fill in descriptions *) + (*----------------if you think, this should be done by the Dialog in the java front-end, search there for WN060225-modelProblem----*) - val (pbl,met) = case cas of NONE => (pbl,[]) + val (pbl, met) = case cas of NONE => (pbl, []) | _ => complete_mod_ (oris, mpc, ppc, probl) (*----------------------------------------------------------------*) val tac_ = Model_Problem' (pI, pbl, met) @@ -1692,28 +1634,25 @@ in ((pt,([],Pbl)), []) end (* val (fmz, (dI,pI,mI)) = (fmz, sp); *) - | nxt_specify_init_calc (fmz:fmz_,(dI,pI,mI):spec) = - let (* either """"""""""""""" all empty or complete *) + | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = + let (* both """"""""""""""""""""""""" either empty or complete *) val thy = assoc_thy dI val (pI, pors, mI) = if mI = ["no_met"] then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI) val pI' = refine_ori' pors pI; - in (pI', pors (*refinement over models with diff.prec only*), + in (pI', pors(*refinement over models with diff.precond only*), (hd o #met o get_pbt) pI') end else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI) - val {cas,ppc,thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*) + val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*) val dI = theory2theory' (maxthy thy thy'); val hdl = case cas of NONE => pblterm dI pI | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t - val (pt,_) = cappend_problem e_ptree [] e_istate (fmz,(dI,pI,mI)) - (pors,(dI,pI,mI),hdl) - (*val pbl = init_pbl ppc WN.9.03: done by Model/Refine_Problem - val pt = update_pbl pt [] pbl*) - in ((pt,([],Pbl)), fst3 (nxt_specif Model_Problem (pt, ([],Pbl)))) - end; + val (pt, _) = cappend_problem e_ptree [] e_istate (fmz, (dI, pI, mI)) + (pors, (dI, pI, mI), hdl) + in ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) end;