1.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed Dec 14 09:37:01 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed Dec 14 10:45:41 2016 +0100
1.3 @@ -90,7 +90,7 @@
1.4 val e_calcstate' = ([Ctree.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
1.5
1.6 (* FIXXXME.WN020430 intermediate hack for fun ass_up *)
1.7 -fun f_mout thy (Ctree.Form' (Ctree.FormKF (_, _, _, _, f))) = (Thm.term_of o the o (parse thy)) f
1.8 +fun f_mout thy (Ctree.FormKF f) = (Thm.term_of o the o (parse thy)) f
1.9 | f_mout _ _ = error "f_mout: not called with formula";
1.10
1.11 (* is the calchead complete ? *)
1.12 @@ -639,8 +639,7 @@
1.13 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.14 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1.15 in ((p, p_), ((p, p_), Uistate),
1.16 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef,
1.17 - (Ctree.Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
1.18 + Ctree.PpcKF (Ctree.Method cmI, itms2itemppc thy met' pre'), nxt, Safe, pt')
1.19 end
1.20 | Err msg =>
1.21 let
1.22 @@ -649,7 +648,7 @@
1.23 val (p_, nxt) =
1.24 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.25 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1.26 - in ((p,p_), ((p,p_),Uistate), Ctree.Error' (Ctree.Error_ msg), nxt, Safe,pt) end
1.27 + in ((p,p_), ((p,p_),Uistate), Ctree.Error' msg, nxt, Safe,pt) end
1.28 end
1.29 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
1.30 let
1.31 @@ -679,8 +678,7 @@
1.32 val ppc = if p_= Pbl then pbl' else met
1.33 in
1.34 ((p, p_), ((p, p_), Uistate),
1.35 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef,
1.36 - (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt, Safe, pt')
1.37 + Ctree.PpcKF (header p_ pI cmI, itms2itemppc thy ppc pre), nxt, Safe, pt')
1.38 end
1.39 | Err msg =>
1.40 let
1.41 @@ -689,7 +687,7 @@
1.42 val (p_, nxt) =
1.43 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.44 (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
1.45 - in ((p, p_), ((p, p_), Uistate), Ctree.Error' (Ctree.Error_ msg), nxt, Safe,pt) end
1.46 + in ((p, p_), ((p, p_), Uistate), Ctree.Error' msg, nxt, Safe,pt) end
1.47 end
1.48
1.49 fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
1.50 @@ -707,11 +705,11 @@
1.51 case mI' of
1.52 ["no_met"] =>
1.53 (([], Pbl), (([], Pbl), Uistate),
1.54 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length [], Ctree.Nundef, (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.55 + Ctree.PpcKF (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre),
1.56 Refine_Tacitly pI', Safe, pt)
1.57 | _ =>
1.58 (([], Pbl), (([], Pbl), Uistate),
1.59 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length [], Ctree.Nundef, (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.60 + Ctree.PpcKF (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre),
1.61 Model_Problem, Safe, pt)
1.62 end
1.63 (* ONLY for STARTING modeling phase *)
1.64 @@ -732,7 +730,7 @@
1.65 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1.66 in
1.67 ((p, Pbl), ((p, p_), Uistate),
1.68 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1.69 + Ctree.PpcKF (Ctree.Problem pI', itms2itemppc (assoc_thy dI') pbl pre),
1.70 nxt, Safe, pt)
1.71 end
1.72 (* called only if no_met is specified *)
1.73 @@ -747,7 +745,7 @@
1.74 Ctree.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
1.75 val (pbl, pre, _) = ([], [], false)
1.76 in ((p, Pbl), (pos, Uistate),
1.77 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1.78 + Ctree.PpcKF (Ctree.Problem pIre, itms2itemppc (assoc_thy dI') pbl pre),
1.79 Model_Problem, Safe, pt)
1.80 end
1.81 | specify (Refine_Problem' rfd) pos _ pt =
1.82 @@ -756,7 +754,7 @@
1.83 val (pos, _, _, pt) =
1.84 Ctree.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.85 in
1.86 - (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Ctree.Problems (Ctree.RefinedKF rfd), Model_Problem, Safe, pt)
1.87 + (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Ctree.RefinedKF rfd, Model_Problem, Safe, pt)
1.88 end
1.89 (*WN110515 initialise ctxt again from itms and add preconds*)
1.90 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
1.91 @@ -776,7 +774,7 @@
1.92 (#ppc o get_met) mI'') (dI, pI, mI);
1.93 in
1.94 ((p,Pbl), (pos,Uistate),
1.95 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pI, itms2itemppc dI'' itms pre))),
1.96 + Ctree.PpcKF (Ctree.Problem pI, itms2itemppc dI'' itms pre),
1.97 nxt, Safe, pt)
1.98 end
1.99 (*WN110515 initialise ctxt again from itms and add preconds*)
1.100 @@ -799,7 +797,7 @@
1.101 ((#ppc o get_pbt) pI'', ppc) (dI'', pI'', mID)
1.102 in
1.103 (pos, (pos,Uistate),
1.104 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1.105 + Ctree.PpcKF (Ctree.Method mID, itms2itemppc (assoc_thy dI'') itms pre'),
1.106 nxt, Safe, pt)
1.107 end
1.108 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1.109 @@ -828,7 +826,7 @@
1.110 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
1.111 in
1.112 ((p, p_), (pos, Uistate),
1.113 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.114 + Ctree.PpcKF (header p_ pI cmI, itms2itemppc thy mppc pre),
1.115 nxt, Safe, pt)
1.116 end
1.117 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.118 @@ -837,7 +835,7 @@
1.119 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
1.120 in
1.121 ((p,p_), (pos,Uistate),
1.122 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.123 + Ctree.PpcKF (header p_ pI cmI, itms2itemppc thy mppc pre),
1.124 nxt, Safe, pt)
1.125 end
1.126 end