1.1 --- a/src/sml/ME/script.sml Fri Dec 12 14:29:36 2003 +0100
1.2 +++ b/src/sml/ME/script.sml Sat Dec 13 15:53:13 2003 +0100
1.3 @@ -392,7 +392,13 @@
1.4 ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
1.5 *)
1.6
1.7 -
1.8 +(*["bool_ (1+x=2)","real_ x"] --match_ags--> oris
1.9 + --oris2fmz_--> ["equality (1+x=2)","boundVariable x","solutions L"]*)
1.10 +fun oris2fmz_vals oris =
1.11 + let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) =
1.12 + ((term2str o comp_dts') (dsc, ts), last_elem ts)
1.13 + handle _ => raise error ("ori2fmz_env called with "^terms2str ts)
1.14 + in (split_list o (map ori2fmz_vals)) oris end;
1.15
1.16 (*detour necessary, because generate1 delivers a string-result*)
1.17 fun mout2term thy (Form' (FormKF (_,_,_,_,res))) =
1.18 @@ -449,23 +455,40 @@
1.19 (*L_ will come from pt in appl_in*)
1.20
1.21 (*3.12.03 copied from assod SubProblem*)
1.22 +(* val Const ("Script.SubProblem",_) $
1.23 + (Const ("Pair",_) $
1.24 + Free (dI',_) $
1.25 + (Const ("Pair",_) $ pI' $ mI')) $ ags' =
1.26 + str2term
1.27 + "SubProblem (Test_,[linear,univariate,equation,test],[Test,solve_linear])\
1.28 + \ [bool_ (-1+x=0), real_ x]";
1.29 +*)
1.30 | stac2tac_ thy (Const ("Script.SubProblem",_) $
1.31 (Const ("Pair",_) $
1.32 Free (dI',_) $
1.33 (Const ("Pair",_) $ pI' $ mI')) $ ags') =
1.34 +(*compare "| assod _ (Subproblem'"*)
1.35 let val dI = ((implode o drop_last o explode) dI')^".thy";
1.36 val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.37 val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.38 - val {cas, ppc,...} = get_pbt pI
1.39 - val ags = isalist2list ags' (*"bool_ (-1+x=0) FIXXXXXME: equality !!*)
1.40 - val fmz_ = map term2str ags
1.41 + val ags = isalist2list ags';
1.42 + val thy = assoc_thy dI;
1.43 + val (pI, pors, mI) =
1.44 + if mI = ["no_met"]
1.45 + then let val pors = match_ags thy ((#ppc o get_pbt) pI) ags;
1.46 + val pI' = refine_ori' pors pI;
1.47 + in (pI', pors (*refinement over models with diff.prec only*),
1.48 + (hd o #met o get_pbt) pI') end
1.49 + else (pI, match_ags thy ((#ppc o get_pbt) pI) ags, mI);
1.50 + val (fmz_, vals) = oris2fmz_vals pors;
1.51 + val {cas,ppc,thy,...} = get_pbt pI
1.52 + val dI = theory2theory' thy (*take dI from _refined_ pbl*)
1.53 val hdl = case cas of
1.54 None => pblterm dI pI
1.55 - | Some t => subst_atomic ((vars_of_pbl_ ppc)~~ ags) t
1.56 - val oris = match_ags (assoc_thy dI) ppc ags;
1.57 - val f = subpbl dI' pI
1.58 + | Some t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
1.59 + val f = subpbl (strip_thy dI) pI
1.60 in (Subproblem (dI, pI),
1.61 - Subproblem' ((dI, pI, mI), oris, hdl, fmz_, f))
1.62 + Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f))
1.63 end
1.64
1.65 | stac2tac_ thy t = raise error
1.66 @@ -840,29 +863,30 @@
1.67 (Const ("Pair",_) $
1.68 Free (dI',_) $
1.69 (Const ("Pair",_) $ pI' $ mI')) $ ags') =
1.70 - let (*val _= writeln "### assod Subproblem";*)
1.71 - val domID' = ((implode o drop_last o explode) dI')^".thy";
1.72 - val pblID' = ((map (de_esc_underscore o free2str))
1.73 - o isalist2list) pI';
1.74 - val metID' = ((map (de_esc_underscore o free2str))
1.75 - o isalist2list) mI';
1.76 - (*val metID' as (dI',_) = (((implode o drop_last o explode) mI1')^".thy",
1.77 - de_esc_underscore mI2');*)
1.78 - (*5.8.02: really take domID for metID ?
1.79 - val _= writeln "### assod: vor match_ags";*)
1.80 - val {cas, ppc,...} = get_pbt pblID
1.81 - val ags = isalist2list ags'
1.82 - val fmz_ = map term2str ags
1.83 +(*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
1.84 + let val dI = ((implode o drop_last o explode) dI')^".thy";
1.85 + val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.86 + val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.87 + val ags = isalist2list ags';
1.88 + val thy = assoc_thy dI;
1.89 + val (pI, pors, mI) =
1.90 + if mI = ["no_met"]
1.91 + then let val pors = match_ags thy ((#ppc o get_pbt) pI) ags;
1.92 + val pI' = refine_ori' pors pI;
1.93 + in (pI', pors (*refinement over models with diff.prec only*),
1.94 + (hd o #met o get_pbt) pI') end
1.95 + else (pI, match_ags thy ((#ppc o get_pbt) pI) ags, mI);
1.96 + val (fmz_, vals) = oris2fmz_vals pors;
1.97 + val {cas, ppc,...} = get_pbt pI
1.98 + val {cas, ppc, thy,...} = get_pbt pI
1.99 + val dI = theory2theory' thy (*take dI from _refined_ pbl*)
1.100 val hdl = case cas of
1.101 - None => pblterm domID pblID
1.102 - | Some t => subst_atomic ((vars_of_pbl_ ppc)~~ ags) t
1.103 - val oris = match_ags (assoc_thy domID) ppc ags;
1.104 - (*val _= writeln "### assod: nach match_ags";*)
1.105 - in
1.106 -(*writeln("##### assoc: metID' = "^(metID2str metID'));*)
1.107 - if domID = domID' andalso pblID = pblID'
1.108 - then Ass (Subproblem' ((domID, pblID, metID'), oris, hdl, fmz_, f), f)
1.109 - else NotAss
1.110 + None => pblterm dI pI
1.111 + | Some t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
1.112 + val f = subpbl (strip_thy dI) pI
1.113 + in if domID = dI andalso pblID = pI
1.114 + then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f), f)
1.115 + else NotAss
1.116 end
1.117
1.118 | assod d m t =