src/Tools/isac/Interpret/calchead.sml
branchdecompose-isar
changeset 41988 0a13bda82a57
parent 41983 4c49adbfadab
child 41990 99e83a0bea44
     1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri May 13 10:26:44 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri May 13 11:45:07 2011 +0200
     1.3 @@ -1000,7 +1000,7 @@
     1.4  fun specify_additem sel (ct,_) (p,Met) c pt = 
     1.5      let
     1.6        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
     1.7 -		  probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
     1.8 +		    probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
     1.9        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.10      (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
    1.11        val cpI = if pI = e_pblID then pI' else pI;
    1.12 @@ -1043,7 +1043,7 @@
    1.13  | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt = 
    1.14      let
    1.15        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    1.16 -		  probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.17 +		    probl=pbl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.18        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.19        val cpI = if pI = e_pblID then pI' else pI;
    1.20        val cmI = if mI = e_metID then mI' else mI;
    1.21 @@ -1113,7 +1113,7 @@
    1.22      (*ONLY for STARTING modeling phase*)
    1.23    | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
    1.24        let 
    1.25 -        val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) = get_obj I pt p
    1.26 +        val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_), ...}) = get_obj I pt p
    1.27          val thy' = if dI = e_domID then dI' else dI
    1.28          val thy = assoc_thy thy'
    1.29          val {ppc,prls,where_,...} = get_pbt pI'
    1.30 @@ -1156,8 +1156,6 @@
    1.31    | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
    1.32    let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI), 
    1.33  		   meth=met, ...}) = get_obj I pt p;
    1.34 -    (*val pt = update_pbl pt p itms;
    1.35 -    val pt = update_pblID pt p pI;*)
    1.36      val thy = assoc_thy dI
    1.37      val ((p,Pbl),_,_,pt)= 
    1.38  	generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
    1.39 @@ -1208,7 +1206,7 @@
    1.40      let val p_ = case p_ of Met => Met | _ => Pbl
    1.41        val thy = assoc_thy domID;
    1.42        val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
    1.43 -		  probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.44 +		    probl=pbl, spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.45        val mppc = case p_ of Met => met | _ => pbl;
    1.46        val cpI = if pI = e_pblID then pI' else pI;
    1.47        val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
    1.48 @@ -1249,7 +1247,7 @@
    1.49  fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) = 
    1.50        let
    1.51          val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
    1.52 -		      probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
    1.53 +		      probl=pbl,spec=(dI,pI,_), ...}) = get_obj I pt p;
    1.54          val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.55          val cpI = if pI = e_pblID then pI' else pI;
    1.56          val ctxt = get_ctxt pt (p, Pbl); (*FIXME.WN110511 repair*)
    1.57 @@ -1277,7 +1275,7 @@
    1.58    | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) = 
    1.59        let
    1.60          val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    1.61 -		      probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.62 +		      probl=pbl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.63          val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.64          val cmI = if mI = e_metID then mI' else mI;
    1.65          val ctxt = get_ctxt pt (p,Met); (*FIXME.WN110511 repair*)
    1.66 @@ -1453,7 +1451,8 @@
    1.67      FIXME.WN.8.03: application of several mIDs to SAME model?*)
    1.68    | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) = 
    1.69        let
    1.70 -        val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), meth=met, ...}) = get_obj I pt p;
    1.71 +        val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), 
    1.72 +          meth=met, ...}) = get_obj I pt p;
    1.73          val {ppc,pre,prls,...} = get_met mID
    1.74          val thy = assoc_thy dI
    1.75          val oris = add_field' thy ppc oris;
    1.76 @@ -1719,7 +1718,7 @@
    1.77      let val _= if p_ <> Pbl 
    1.78  	       then tracing("###complete_mod: only impl.for Pbl, called with "^
    1.79  			    pos'2str pos) else ()
    1.80 -	val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
    1.81 +	val (PblObj{origin=(oris, ospec, hdl), probl, spec, ...}) =
    1.82  	    get_obj I pt p
    1.83  	val (dI,pI,mI) = some_spec ospec spec
    1.84  	val mpc = (#ppc o get_met) mI
    1.85 @@ -2003,7 +2002,7 @@
    1.86      in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
    1.87  | get_ocalhd (pt, pos' as (p,Met):pos') = 
    1.88      let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 
    1.89 -		    spec, meth,...} = 
    1.90 +		    spec, meth, ...} = 
    1.91  	    get_obj I pt p
    1.92  	val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
    1.93  	val pre = check_preconds (assoc_thy"Isac") prls pre meth