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
2.1 --- a/src/Tools/isac/Interpret/generate.sml Wed Dec 14 09:37:01 2016 +0100
2.2 +++ b/src/Tools/isac/Interpret/generate.sml Wed Dec 14 10:45:41 2016 +0100
2.3 @@ -10,10 +10,12 @@
2.4 eqtype indent
2.5 datatype nest = Closed | Nundef | Open
2.6 datatype pblmet = Method of metID | Problem of pblID | Upblmet
2.7 - datatype inout
2.8 - = Error_ of string | FormKF of cellID * edit * indent * nest * cterm'
2.9 - | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) | RefineKF of match list
2.10 - | RefinedKF of pblID * (itm list * (bool * term) list)
2.11 + datatype inout =
2.12 + Error_ of string
2.13 + | FormKF of cellID * edit * indent * nest * cterm'
2.14 + | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc)
2.15 + | RefineKF of match list
2.16 + | RefinedKF of pblID * (itm list * (bool * term) list)
2.17 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
2.18 val generate1 : theory -> tac_ -> istate * Proof.context ->
2.19 posel list * pos_ -> ptree -> pos' * pos' list * mout * ptree
2.20 @@ -38,7 +40,7 @@
2.21 end
2.22
2.23 (**)
2.24 -structure Ctree(**): CALC_TREE(**) =
2.25 +structure Ctree(*: CALC_TREE*) =
2.26 (**)
2.27 struct
2.28 (* initialize istate for Detail_Set *)
2.29 @@ -153,16 +155,21 @@
2.30 | inout2str _ = error "inout2str: uncovered definition"
2.31 fun inouts2str ios = (strs2str' o (map inout2str)) ios
2.32
2.33 +(*
2.34 + datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
2.35 +*)
2.36 datatype mout =
2.37 - Form' of inout (* packing cterm' | cterm' ppc *)
2.38 -| Problems of inout (* passes specify (and solve) *)
2.39 -| Error' of inout
2.40 -| EmptyMout;
2.41 + FormKF of cterm'
2.42 +| PpcKF of (pblmet * item ppc)
2.43 +| RefinedKF of pblID * (itm list * (bool * term) list)
2.44 +| Error' of string
2.45 +| EmptyMout
2.46
2.47 -fun mout2str (Form' inout) ="Form' "^(inout2str inout)
2.48 - | mout2str (Error' inout) ="Error' "^(inout2str inout)
2.49 - | mout2str (EmptyMout ) ="EmptyMout"
2.50 - | mout2str _ = error "mout2str: uncovered definition"
2.51 +fun mout2str (FormKF cterm') = "FormKF " ^ cterm'
2.52 + | mout2str (PpcKF (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ itemppc2str itemppc ^ ")"
2.53 + | mout2str (RefinedKF (pblID, ls)) = "mout2str: RefinedKF not impl."
2.54 + | mout2str (Error' str) = "Error' " ^ str
2.55 + | mout2str (EmptyMout ) = "EmptyMout"
2.56
2.57 (* init pbl with ...,dsc,empty | [] *)
2.58 fun init_pbl pbt =
2.59 @@ -179,7 +186,7 @@
2.60 (*generate 1 ppobj in ptree*)
2.61 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
2.62 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt =
2.63 - (pos:pos',[],Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [][]))),
2.64 + (pos: pos', [], PpcKF (Upblmet, itms2itemppc thy [][]),
2.65 case p_ of
2.66 Pbl => update_pbl pt p itmlist
2.67 | Met => update_met pt p itmlist
2.68 @@ -187,27 +194,27 @@
2.69 (* WN110515 probably declare_constraints with input item (without dsc) --
2.70 -- important when specifying without formalisation *)
2.71 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt =
2.72 - (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
2.73 + (pos, [], (PpcKF (Upblmet, itms2itemppc thy [] [])),
2.74 case p_ of
2.75 Pbl => update_pbl pt p itmlist
2.76 | Met => update_met pt p itmlist
2.77 | _ => error ("uncovered case " ^ pos_2str p_))
2.78 (*WN110515 probably declare_constraints with input item (without dsc)*)
2.79 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt =
2.80 - (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
2.81 + (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []),
2.82 case p_ of
2.83 Pbl => update_pbl pt p itmlist
2.84 | Met => update_met pt p itmlist
2.85 | _ => error ("uncovered case " ^ pos_2str p_))
2.86 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
2.87 - (pos, [] ,Form' (PpcKF (0 ,EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
2.88 + (pos, [] , PpcKF (Upblmet, itms2itemppc thy [] []),
2.89 update_domID pt p domID)
2.90 | generate1 thy (Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt =
2.91 let
2.92 val pt = update_pbl pt p itms
2.93 val pt = update_pblID pt p pI
2.94 in
2.95 - ((p, Pbl), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
2.96 + ((p, Pbl), [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
2.97 end
2.98 | generate1 thy (Specify_Method' (mID, oris, itms)) _ (p, _) pt =
2.99 let
2.100 @@ -215,28 +222,28 @@
2.101 val pt = update_met pt p itms
2.102 val pt = update_metID pt p mID
2.103 in
2.104 - ((p, Met), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
2.105 + ((p, Met), [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
2.106 end
2.107 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
2.108 let
2.109 val pt = update_pbl pt p itms
2.110 val pt = update_met pt p met
2.111 in
2.112 - (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
2.113 + (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
2.114 end
2.115 | generate1 thy (Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt =
2.116 let
2.117 val pt = update_pbl pt p pbl
2.118 val pt = update_orispec pt p (domID, pIre, metID)
2.119 in
2.120 - (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
2.121 + (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
2.122 end
2.123 | generate1 thy (Refine_Problem' (pI, _)) _ (pos as (p, _)) pt =
2.124 let
2.125 val (dI, _, mI) = get_obj g_spec pt p
2.126 val pt = update_spec pt p (dI, pI, mI)
2.127 in
2.128 - (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
2.129 + (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
2.130 end
2.131 | generate1 _ (Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt =
2.132 (case topt of
2.133 @@ -251,7 +258,7 @@
2.134 in if p' = 0 then ps @ [1] else p end
2.135 val (pt, c) = cappend_form pt p l t
2.136 in
2.137 - ((p, Frm): pos', c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
2.138 + ((p, Frm): pos', c, FormKF (term2str t), pt)
2.139 end
2.140 | generate1 _ (Begin_Trans' t) l (p, Frm) pt =
2.141 let
2.142 @@ -261,7 +268,7 @@
2.143 val p = (lev_on o lev_dn (* starts with [...,0] *)) p
2.144 val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*)
2.145 in
2.146 - ((p, Frm), c @ c', Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
2.147 + ((p, Frm), c @ c', FormKF (term2str t), pt)
2.148 end
2.149 | generate1 thy (Begin_Trans' t) l (p, Res) pt =
2.150 (*append after existing PrfObj vvvvvvvvvvvvv*)
2.151 @@ -271,21 +278,23 @@
2.152 val p' = lev_up p
2.153 val (pt, c) = append_result pt p' l tasm Complete
2.154 in
2.155 - ((p', Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
2.156 + ((p', Res), c, FormKF (term2str t), pt)
2.157 end
2.158 | generate1 _ (Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt =
2.159 let
2.160 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
2.161 (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;
2.162 val pt = update_branch pt p TransitiveB
2.163 - in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt) end
2.164 + in
2.165 + ((p, Res), c, FormKF (term2str f'), pt)
2.166 + end
2.167 | generate1 _ (Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =
2.168 let
2.169 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
2.170 (Rewrite thm') (f', asm) Complete
2.171 val pt = update_branch pt p TransitiveB
2.172 in
2.173 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
2.174 + ((p, Res), c, FormKF (term2str f'), pt)
2.175 end
2.176 | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
2.177 | generate1 _ (Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt =
2.178 @@ -294,7 +303,7 @@
2.179 (Rewrite_Set_Inst (subst2subs subs', id_rls rls')) (f', asm) Complete
2.180 val pt = update_branch pt p TransitiveB
2.181 in
2.182 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
2.183 + ((p, Res), c, FormKF (term2str f'), pt)
2.184 end
2.185 | generate1 thy (Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
2.186 let
2.187 @@ -313,7 +322,7 @@
2.188 (Rewrite_Set (id_rls rls')) (f',asm) Complete
2.189 val pt = update_branch pt p TransitiveB
2.190 in
2.191 - ((p, Res), c, Form' (FormKF (~1 ,EdUndef, length p, Nundef, term2str f')), pt)
2.192 + ((p, Res), c, FormKF (term2str f'), pt)
2.193 end
2.194 | generate1 thy (Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
2.195 let
2.196 @@ -330,37 +339,37 @@
2.197 let
2.198 val (pt, c) = append_result pt p l (scval, asm) Complete
2.199 in
2.200 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str scval)), pt)
2.201 + ((p, Res), c, FormKF (term2str scval), pt)
2.202 end
2.203 | generate1 _ (Calculate' (_, op_, f, (f', _))) l (p, _) pt =
2.204 let
2.205 val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f', []) Complete
2.206 in
2.207 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
2.208 + ((p, Res), c, FormKF (term2str f'), pt)
2.209 end
2.210 | generate1 _ (Check_elementwise' (consts, pred, (f', asm))) l (p, _) pt =
2.211 let
2.212 val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete
2.213 in
2.214 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
2.215 + ((p, Res), c, FormKF (term2str f'), pt)
2.216 end
2.217 | generate1 _ (Or_to_List' (ors, list)) l (p, _) pt =
2.218 let
2.219 val (pt,c) = cappend_atomic pt p l ors Or_to_List (list, []) Complete
2.220 in
2.221 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str list)), pt)
2.222 + ((p, Res), c, FormKF (term2str list), pt)
2.223 end
2.224 | generate1 _ (Substitute' (_, _, subte, t, t')) l (p, _) pt =
2.225 let
2.226 val (pt,c) =
2.227 cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete
2.228 - in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t')), pt)
2.229 + in ((p, Res), c, FormKF (term2str t'), pt)
2.230 end
2.231 | generate1 _ (Tac_ (_, f, id, f')) l (p, _) pt =
2.232 let
2.233 val (pt, c) = cappend_atomic pt p l (str2term f) (Tac id) (str2term f', []) Complete
2.234 in
2.235 - ((p,Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f')), pt)
2.236 + ((p,Res), c, FormKF f', pt)
2.237 end
2.238 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p, _) pt =
2.239 let
2.240 @@ -368,7 +377,7 @@
2.241 val pt = update_ctxt pt p ctxt
2.242 val f = Syntax.string_of_term (thy2ctxt thy) f
2.243 in
2.244 - ((p, Pbl), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f)), pt)
2.245 + ((p, Pbl), c, FormKF f, pt)
2.246 end
2.247 | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ tac_2str m')
2.248
3.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed Dec 14 09:37:01 2016 +0100
3.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed Dec 14 10:45:41 2016 +0100
3.3 @@ -62,7 +62,7 @@
3.4 let
3.5 val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
3.6 in
3.7 - case f of (Ctree.Error' (Ctree.Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
3.8 + case f of (Ctree.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
3.9 end
3.10
3.11 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
3.12 @@ -368,12 +368,12 @@
3.13 val (form, _, _) = Chead.pt_extract ptp
3.14 in
3.15 case form of
3.16 - Form t => Ctree.Form' (Ctree.FormKF (~1,Ctree.EdUndef,0,Ctree.Nundef,term2str t))
3.17 - | ModSpec (_,p_, _, gfr, pre, _) =>
3.18 - Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, 0, Ctree.Nundef,
3.19 - (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method [] | _ => error "TESTg_form: uncovered case",
3.20 - itms2itemppc (assoc_thy"Isac") gfr pre)))
3.21 - end;
3.22 + Form t => Ctree.FormKF (term2str t)
3.23 + | ModSpec (_,p_, _, gfr, pre, _) => Ctree.PpcKF (
3.24 + (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method []
3.25 + | _ => error "TESTg_form: uncovered case",
3.26 + itms2itemppc (assoc_thy"Isac") gfr pre))
3.27 + end
3.28
3.29 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
3.30 compare "fun CalcTree" which DOES decode *)
3.31 @@ -421,6 +421,6 @@
3.32 end
3.33
3.34 (* for quick test-print-out, until 'type inout' is removed *)
3.35 -fun f2str (Ctree.Form' (Ctree.FormKF (_, _, _, _, cterm'))) = cterm';
3.36 +fun f2str (Ctree.FormKF cterm') = cterm';
3.37
3.38 end
4.1 --- a/src/Tools/isac/Interpret/solve.sml Wed Dec 14 09:37:01 2016 +0100
4.2 +++ b/src/Tools/isac/Interpret/solve.sml Wed Dec 14 10:45:41 2016 +0100
4.3 @@ -469,7 +469,7 @@
4.4 *)
4.5 fun get_form ((mI,m):tac'_) ((p,p_):pos') pt =
4.6 case applicable_in (p,p_) pt m of
4.7 - Chead.Notappl e => Ctree.Error' (Ctree.Error_ e)
4.8 + Chead.Notappl e => Ctree.Error' e
4.9 | Chead.Appl m =>
4.10 (* val Appl m=applicable_in (p,p_) pt m;
4.11 *)
5.1 --- a/test/Tools/isac/Interpret/calchead.sml Wed Dec 14 09:37:01 2016 +0100
5.2 +++ b/test/Tools/isac/Interpret/calchead.sml Wed Dec 14 10:45:41 2016 +0100
5.3 @@ -80,15 +80,15 @@
5.4
5.5 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.6 val nxt = tac2tac_ pt p nxt;
5.7 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.8 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.9 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
5.10
5.11 val nxt = tac2tac_ pt p nxt;
5.12 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.13 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.14 (**)
5.15
5.16 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]");
5.17 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.18 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.19 if ppc<>(Problem [],
5.20 {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
5.21 Given=[Correct "fixedValues [r = Arbfix]"],
5.22 @@ -102,18 +102,18 @@
5.23 Some tests have been broken much earlier,
5.24 see test/../calchead.sml "inhibit exn 010830". *)
5.25 (*========== inhibit exn WN1130630 maximum example broken =========================
5.26 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.27 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.28 ============ inhibit exn WN1130630 maximum example broken =======================*)
5.29
5.30 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+");
5.31 (*========== inhibit exn WN1130630 maximum example broken =========================
5.32 (* ERROR: Exception Bind raised *)
5.33 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.34 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.35 ============ inhibit exn WN1130630 maximum example broken =======================*)
5.36
5.37 val m = Specify_Problem ["maximum_of","function"];
5.38 val nxt = tac2tac_ pt p m;
5.39 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.40 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.41 (*========== inhibit exn WN1130630 maximum example broken =========================
5.42 if ppc<>(Problem ["maximum_of","function"],
5.43 {Find=[Incompl "maximum",Incompl "valuesFor"],
5.44 @@ -131,7 +131,7 @@
5.45 ============ inhibit exn WN1130630 maximum example broken =======================*)
5.46
5.47 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
5.48 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.49 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.50 (*========== inhibit exn WN1130630 maximum example broken =========================
5.51 if ppc<>(Method ["DiffApp","max_by_calculus"],
5.52 {Find=[Incompl "maximum",Incompl "valuesFor"],
5.53 @@ -173,29 +173,29 @@
5.54 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.55
5.56 val nxt = tac2tac_ pt p nxt;
5.57 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
5.58 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] pt;
5.59 val nxt = tac2tac_ pt p nxt;
5.60 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.61 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.62 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
5.63
5.64 val nxt = tac2tac_ pt p nxt;
5.65 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.66 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.67 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
5.68
5.69 val nxt = tac2tac_ pt p nxt;
5.70 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.71 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.72 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
5.73
5.74 val nxt = tac2tac_ pt p nxt;
5.75 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.76 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.77 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
5.78
5.79 val nxt = tac2tac_ pt p nxt;
5.80 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.81 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.82 (*val nxt = Add_Relation "relations [A = a * b]" *)
5.83
5.84 val nxt = tac2tac_ pt p nxt;
5.85 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.86 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.87 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
5.88
5.89 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
5.90 @@ -206,7 +206,7 @@
5.91 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
5.92
5.93 val nxt = tac2tac_ pt p nxt;
5.94 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.95 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.96 ------------------------------ FIXXXXME.meNEW !!! ---*)
5.97
5.98 (*val nxt = Specify_Theory "DiffApp" : tac*)
5.99 @@ -214,27 +214,27 @@
5.100 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
5.101
5.102 val nxt = tac2tac_ pt p nxt;
5.103 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.104 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.105 (*val nxt = Specify_Problem ["maximum_of","function"]*)
5.106
5.107 val nxt = tac2tac_ pt p nxt;
5.108 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.109 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.110 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
5.111
5.112 val nxt = tac2tac_ pt p nxt;
5.113 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.114 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.115 (*val nxt = Add_Given "boundVariable a" : tac*)
5.116
5.117 val nxt = tac2tac_ pt p nxt;
5.118 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.119 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.120 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
5.121
5.122 val nxt = tac2tac_ pt p nxt;
5.123 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.124 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.125 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
5.126
5.127 val nxt = tac2tac_ pt p nxt;
5.128 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.129 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.130 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
5.131 case nxt of (Apply_Method ["DiffApp","max_by_calculus"]) => ()
5.132 | _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";
5.133 @@ -249,37 +249,37 @@
5.134
5.135 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
5.136 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
5.137 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
5.138 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' []
5.139 EmptyPtree;
5.140 val nxt = tac2tac_ pt p nxt;
5.141 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.142 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.143 (*val nxt = Specify_Theory "e_domID" : tac*)
5.144
5.145 val nxt = Specify_Theory "DiffApp";
5.146 val nxt = tac2tac_ pt p nxt;
5.147 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.148 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.149 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
5.150
5.151 val nxt = Specify_Problem ["maximum_of","function"];
5.152 val nxt = tac2tac_ pt p nxt;
5.153 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.154 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.155 (*val nxt = Add_Given "fixedValues" : tac*)
5.156
5.157 val nxt = Add_Given "fixedValues [r=Arbfix]";
5.158 val nxt = tac2tac_ pt p nxt;
5.159 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.160 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.161 (*val nxt = Add_Find "maximum" : tac*)
5.162
5.163 val nxt = Add_Find "maximum A";
5.164 val nxt = tac2tac_ pt p nxt;
5.165
5.166
5.167 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.168 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.169 (*val nxt = Add_Find "valuesFor" : tac*)
5.170
5.171 val nxt = Add_Find "valuesFor [a]";
5.172 val nxt = tac2tac_ pt p nxt;
5.173 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.174 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.175 (*val nxt = Add_Relation "relations" ---
5.176 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
5.177
5.178 @@ -293,27 +293,27 @@
5.179
5.180 val nxt = Add_Relation "relations [(A=a+b)]";
5.181 val nxt = tac2tac_ pt p nxt;
5.182 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.183 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.184 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
5.185
5.186 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
5.187 val nxt = tac2tac_ pt p nxt;
5.188 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.189 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.190 (*val nxt = Add_Given "boundVariable" : tac*)
5.191
5.192 val nxt = Add_Given "boundVariable alpha";
5.193 val nxt = tac2tac_ pt p nxt;
5.194 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.195 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.196 (*val nxt = Add_Given "interval" : tac*)
5.197
5.198 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
5.199 val nxt = tac2tac_ pt p nxt;
5.200 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.201 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.202 (*val nxt = Add_Given "errorBound" : tac*)
5.203
5.204 val nxt = Add_Given "errorBound (eps=999)";
5.205 val nxt = tac2tac_ pt p nxt;
5.206 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
5.207 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
5.208 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
5.209
5.210 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
5.211 @@ -323,7 +323,7 @@
5.212 *)
5.213 (* 2.4.00 nach Transfer specify -> hard_gen
5.214 val nxt = Apply_Method ("DiffApp","max_by_calculus");
5.215 -val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
5.216 +val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; *)
5.217 (*val nxt = Empty_Tac : tac*)
5.218
5.219 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
6.1 --- a/test/Tools/isac/Interpret/ctree.sml Wed Dec 14 09:37:01 2016 +0100
6.2 +++ b/test/Tools/isac/Interpret/ctree.sml Wed Dec 14 10:45:41 2016 +0100
6.3 @@ -131,7 +131,7 @@
6.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);
6.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
6.6 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
6.7 -val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
6.8 +val FormKF res = f;
6.9 if res = "[x = 1]"
6.10 then case nxt of ("End_Proof'", End_Proof') => ()
6.11 | _ => error "new behaviour in test: miniscript with mini-subpbl 1"
7.1 --- a/test/Tools/isac/Interpret/ptyps.sml Wed Dec 14 09:37:01 2016 +0100
7.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Wed Dec 14 10:45:41 2016 +0100
7.3 @@ -329,11 +329,11 @@
7.4 (*=== specify a not-matching problem ------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
7.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.6 val www =
7.7 -case f of Form' (PpcKF (0, EdUndef, 0, Nundef, (Problem [],
7.8 +case f of PpcKF (Problem [],
7.9 {Find = [Incompl "solutions"], With = [],
7.10 Given = [Correct "equality ((x + 1) * (x + 2) = x ^^^ 2 + 8)", Correct "solveFor x"],
7.11 Where = [False www],
7.12 - Relate = [],...}))) => www
7.13 + Relate = [],...}) => www
7.14 | _ => error "--- Refine_Problem broken 1";
7.15 if www = "matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)"
7.16 then () else error "--- Refine_Problem broken 2";
7.17 @@ -402,7 +402,7 @@
7.18 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.19 (*Check_Postcond ["normalize","univariate","equation","test"])*)
7.20 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.21 -val Form' (FormKF (~1,EdUndef,_,Nundef,res)) = f;
7.22 +val FormKF res = f;
7.23
7.24 if res = "[x = 2]"
7.25 then case nxt of ("End_Proof'", End_Proof') => ()
8.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Wed Dec 14 09:37:01 2016 +0100
8.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Wed Dec 14 10:45:41 2016 +0100
8.3 @@ -272,7 +272,7 @@
8.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.7 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
8.8 +case f of FormKF "[x = 2, x = -1]" => ()
8.9 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
8.10
8.11
8.12 @@ -310,7 +310,7 @@
8.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.14 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.16 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
8.17 +case f of FormKF "[x = 1, x = -2]" => ()
8.18 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
8.19
8.20 "----- d2_pqformula3_neg ------";
8.21 @@ -343,7 +343,7 @@
8.22 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.23 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.24 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.25 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
8.26 +case f of FormKF "[x = 1, x = -2]" => ()
8.27 | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
8.28
8.29 "----- d2_pqformula4_neg ------";
8.30 @@ -374,7 +374,7 @@
8.31 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.32 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.33 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.34 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
8.35 +case f of FormKF "[x = 0, x = -1]" => ()
8.36 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
8.37
8.38 "----- d2_pqformula6 ------";
8.39 @@ -390,7 +390,7 @@
8.40 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.41 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.42 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.43 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
8.44 +case f of FormKF "[x = 0, x = -1]" => ()
8.45 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
8.46
8.47 "----- d2_pqformula7 ------";
8.48 @@ -407,7 +407,7 @@
8.49 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.50 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.51 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.52 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
8.53 +case f of FormKF "[x = 0, x = -1]" => ()
8.54 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
8.55
8.56 "----- d2_pqformula8 ------";
8.57 @@ -423,7 +423,7 @@
8.58 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.59 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.60 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.61 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
8.62 +case f of FormKF "[x = 0, x = -1]" => ()
8.63 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
8.64
8.65 "----- d2_pqformula9 ------";
8.66 @@ -438,7 +438,7 @@
8.67 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.68 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.69 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.70 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
8.71 +case f of FormKF "[x = 2, x = -2]" => ()
8.72 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
8.73
8.74
8.75 @@ -470,7 +470,7 @@
8.76 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.77 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.78 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.79 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
8.80 +case f of FormKF "[x = 2, x = -2]" => ()
8.81 | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
8.82
8.83 "----- d2_pqformula9_neg ------";
8.84 @@ -503,7 +503,7 @@
8.85 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.86 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.87 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.88 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
8.89 +case f of FormKF "[x = 1, x = -1 / 2]" => ()
8.90 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
8.91
8.92 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
8.93 @@ -532,7 +532,7 @@
8.94 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.95 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.96 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.97 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
8.98 +case f of FormKF "[x = 1 / 2, x = -1]" => ()
8.99 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
8.100
8.101 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
8.102 @@ -561,7 +561,7 @@
8.103 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.104 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.105 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.106 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
8.107 +case f of FormKF "[x = 1, x = -2]" => ()
8.108 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
8.109
8.110 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
8.111 @@ -591,7 +591,7 @@
8.112 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.113 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.114 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.115 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
8.116 +case f of FormKF "[x = 1, x = -2]" => ()
8.117 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
8.118
8.119 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
8.120 @@ -621,7 +621,7 @@
8.121 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.122 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.123 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.124 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
8.125 +case f of FormKF "[x = 2, x = -2]" => ()
8.126 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
8.127
8.128 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
8.129 @@ -649,7 +649,7 @@
8.130 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.131 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.132 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.133 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
8.134 +case f of FormKF "[x = 2, x = -2]" => ()
8.135 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
8.136
8.137
8.138 @@ -678,7 +678,7 @@
8.139 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.140 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.141 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.142 -case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
8.143 +case f of FormKF "[x = 0, x = -1]" => ()
8.144 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
8.145
8.146 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
8.147 @@ -692,7 +692,7 @@
8.148 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.149 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.150 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.151 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
8.152 +case f of FormKF "[x = 0, x = -1]" => ()
8.153 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
8.154
8.155 (*EP-16*)
8.156 @@ -707,7 +707,7 @@
8.157 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.158 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.159 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.160 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
8.161 +case f of FormKF "[x = 0, x = -1 / 2]" => ()
8.162 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
8.163
8.164 (*EP-//*)
8.165 @@ -722,7 +722,7 @@
8.166 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.167 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.168 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.169 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
8.170 +case f of FormKF "[x = 0, x = -1]" => ()
8.171 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
8.172
8.173 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
8.174 @@ -1014,7 +1014,7 @@
8.175 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
8.176 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
8.177 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
8.178 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
8.179 +case f of FormKF "[x = 2]" => ()
8.180 | _ => error "polyeq.sml: diff.behav. in [x = 2]";
8.181
8.182
8.183 @@ -1054,7 +1054,7 @@
8.184 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
8.185 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
8.186 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
8.187 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
8.188 +case f of FormKF "[x = 2 / 15, x = 1]" => ()
8.189 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
8.190
8.191
8.192 @@ -1078,7 +1078,7 @@
8.193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
8.194 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
8.195 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
8.196 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
8.197 +case f of FormKF "[x = 2, x = -2]" => ()
8.198 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
8.199
8.200 "----------------- polyeq.sml end ------------------";
9.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Dec 14 09:37:01 2016 +0100
9.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Dec 14 10:45:41 2016 +0100
9.3 @@ -244,7 +244,7 @@
9.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.6 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.7 -case f of Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0")) => ()
9.8 +case f of FormKF "-6 * x + 5 * x ^^^ 2 = 0" => ()
9.9 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
9.10 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.1 --- a/test/Tools/isac/ProgLang/calculate.sml Wed Dec 14 09:37:01 2016 +0100
10.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Wed Dec 14 10:45:41 2016 +0100
10.3 @@ -102,7 +102,7 @@
10.4 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
10.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.6 (*nxt = ("End_Proof'",End_Proof')*)
10.7 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"16")) => () | _ =>
10.8 +case f of FormKF "16" => () | _ =>
10.9 error "calculate.sml: script test_calculate changed behaviour";
10.10
10.11