77 is_known ctxt sel oris t; |
77 is_known ctxt sel oris t; |
78 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t); |
78 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t); |
79 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t); |
79 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t); |
80 val ots = (Library.distinct op = o flat o (map #5)) (ori:O_Model.T); |
80 val ots = (Library.distinct op = o flat o (map #5)) (ori:O_Model.T); |
81 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots; |
81 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots; |
82 val (d, ts) = I_Model.split_dts t; |
82 val (d, ts) = O_Model.split_dts t; |
83 "~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t; |
83 "~~~~~ fun O_Model.split_dts, args:"; val (t as d $ arg) = t; |
84 (*if is_dsc d then () else error "TODO";*) |
84 (*if is_dsc d then () else error "TODO";*) |
85 if is_dsc d then () else error "TODO"; |
85 if is_dsc d then () else error "TODO"; |
86 "----- these were the errors (call hierarchy from bottom up)"; |
86 "----- these were the errors (call hierarchy from bottom up)"; |
87 appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS |
87 appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS |
88 Err "[error] appl_add: is_known: identifiers [equality] not in example"*) |
88 Err "[error] appl_add: is_known: identifiers [equality] not in example"*) |
94 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) |
94 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) |
95 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS |
95 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS |
96 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) |
96 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) |
97 ========== inhibit exn AK110725 ================================================*) |
97 ========== inhibit exn AK110725 ================================================*) |
98 |
98 |
99 "----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; |
99 "----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------"; |
100 "----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; |
100 "----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------"; |
101 "----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; |
101 "----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------"; |
102 (*val t = str2term "maximum A"; |
102 (*val t = str2term "maximum A"; |
103 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
103 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
104 val it = "maximum A" : cterm |
104 val it = "maximum A" : cterm |
105 > val t = str2term "fixedValues [r=Arbfix]"; |
105 > val t = str2term "fixedValues [r=Arbfix]"; |
106 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
106 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
107 "fixedValues [r = Arbfix]" |
107 "fixedValues [r = Arbfix]" |
108 > val t = str2term "valuesFor [a]"; |
108 > val t = str2term "valuesFor [a]"; |
109 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
109 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
110 "valuesFor [a]" |
110 "valuesFor [a]" |
111 > val t = str2term "valuesFor [a,b]"; |
111 > val t = str2term "valuesFor [a,b]"; |
112 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
112 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
113 "valuesFor [a, b]" |
113 "valuesFor [a, b]" |
114 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"; |
114 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"; |
115 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
115 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
116 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]" |
116 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]" |
117 > val t = str2term "boundVariable a"; |
117 > val t = str2term "boundVariable a"; |
118 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
118 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
119 "boundVariable a" |
119 "boundVariable a" |
120 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}"; |
120 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}"; |
121 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
121 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
122 "interval {x. 0 <= x & x <= 2 * r}" |
122 "interval {x. 0 <= x & x <= 2 * r}" |
123 |
123 |
124 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; |
124 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; |
125 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
125 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
126 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))" |
126 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))" |
127 > val t = str2term "solveFor x"; |
127 > val t = str2term "solveFor x"; |
128 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
128 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
129 "solveFor x" |
129 "solveFor x" |
130 > val t = str2term "errorBound (eps=0)"; |
130 > val t = str2term "errorBound (eps=0)"; |
131 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
131 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
132 "errorBound (eps = 0)" |
132 "errorBound (eps = 0)" |
133 > val t = str2term "solutions L"; |
133 > val t = str2term "solutions L"; |
134 > val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); |
134 > val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts); |
135 "solutions L" |
135 "solutions L" |
136 |
136 |
137 before 6.5.03: |
137 before 6.5.03: |
138 > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]"; |
138 > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]"; |
139 > val (d,ts) = I_Model.split_dts t; |
139 > val (d,ts) = O_Model.split_dts t; |
140 > comp_dts thy (d,ts); |
140 > comp_dts thy (d,ts); |
141 val it = "testdscforlist [#1]" : cterm |
141 val it = "testdscforlist [#1]" : cterm |
142 |
142 |
143 > val t = (Thm.term_of o the o (parse thy)) "(A::real)"; |
143 > val t = (Thm.term_of o the o (parse thy)) "(A::real)"; |
144 > val (d,ts) = I_Model.split_dts t; |
144 > val (d,ts) = O_Model.split_dts t; |
145 val d = Const ("empty","empty") : term |
145 val d = Const ("empty","empty") : term |
146 val ts = [Free ("A","RealDef.real")] : term list |
146 val ts = [Free ("A","RealDef.real")] : term list |
147 > val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]"; |
147 > val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]"; |
148 > val (d,ts) = I_Model.split_dts t; |
148 > val (d,ts) = O_Model.split_dts t; |
149 val d = Const ("empty","empty") : term |
149 val d = Const ("empty","empty") : term |
150 val ts = [Const # $ Free # $ Free (#,#)] : term list |
150 val ts = [Const # $ Free # $ Free (#,#)] : term list |
151 > val t = (Thm.term_of o the o (parse thy)) "[#1,#2]"; |
151 > val t = (Thm.term_of o the o (parse thy)) "[#1,#2]"; |
152 > val (d,ts) = I_Model.split_dts t; |
152 > val (d,ts) = O_Model.split_dts t; |
153 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED |
153 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED |
154 *) |
154 *) |
155 "----------- type penv -------------------------------------------------------------------------"; |
155 "----------- type penv -------------------------------------------------------------------------"; |
156 "----------- type penv -------------------------------------------------------------------------"; |
156 "----------- type penv -------------------------------------------------------------------------"; |
157 "----------- type penv -------------------------------------------------------------------------"; |
157 "----------- type penv -------------------------------------------------------------------------"; |
187 val t as t1 $ t2 = str2term "antiDerivativeName M_b"; |
187 val t as t1 $ t2 = str2term "antiDerivativeName M_b"; |
188 pbl_ids ctxt t1 t2; |
188 pbl_ids ctxt t1 t2; |
189 |
189 |
190 val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; |
190 val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; |
191 val (d,argl) = strip_comb t; |
191 val (d,argl) = strip_comb t; |
192 is_dsc d; (*see I_Model.split_dts*) |
192 is_dsc d; (*see O_Model.split_dts*) |
193 dest_list (d,argl); |
193 dest_list (d,argl); |
194 val (_ $ v) = t; |
194 val (_ $ v) = t; |
195 is_list v; |
195 is_list v; |
196 pbl_ids ctxt d v; |
196 pbl_ids ctxt d v; |
197 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $ |
197 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $ |
198 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List.. |
198 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List.. |
199 |
199 |
200 val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x"; |
200 val (dsc,vl) = (O_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x"; |
201 val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term |
201 val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term |
202 val vl = Free ("x","RealDef.real") : term |
202 val vl = Free ("x","RealDef.real") : term |
203 |
203 |
204 val (dsc,id) = (split_did o Thm.term_of o the o (parse thy)) "solveFor v_"; |
204 val (dsc,id) = (split_did o Thm.term_of o the o (parse thy)) "solveFor v_"; |
205 pbl_ids ctxt dsc vl; |
205 pbl_ids ctxt dsc vl; |
206 val it = [Free ("x","RealDef.real")] : term list |
206 val it = [Free ("x","RealDef.real")] : term list |
207 |
207 |
208 val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o(parse thy)) |
208 val (dsc,vl) = (O_Model.split_dts o Thm.term_of o the o(parse thy)) |
209 "errorBound (eps=#0)"; |
209 "errorBound (eps=#0)"; |
210 val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_"; |
210 val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_"; |
211 pbl_ids ctxt dsc vl; |
211 pbl_ids ctxt dsc vl; |
212 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *) |
212 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *) |
213 "----------- fun upd_penv ----------------------------------------------------------------------"; |
213 "----------- fun upd_penv ----------------------------------------------------------------------"; |