13 |
13 |
14 |
14 |
15 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*) |
15 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*) |
16 |
16 |
17 fun itm_2item thy (Cor ((d,ts),_)) = |
17 fun itm_2item thy (Cor ((d,ts),_)) = |
18 Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) |
18 Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) |
19 | itm_2item _ (Syn c) = SyntaxE c |
19 | itm_2item _ (Syn c) = SyntaxE c |
20 | itm_2item _ (Typ c) = TypeE c |
20 | itm_2item _ (Typ c) = TypeE c |
21 | itm_2item thy (Inc ((d,ts),_)) = |
21 | itm_2item thy (Inc ((d,ts),_)) = |
22 Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) |
22 Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) |
23 | itm_2item thy (Sup (d,ts)) = |
23 | itm_2item thy (Sup (d,ts)) = |
24 Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) |
24 Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) |
25 | itm_2item _ (Mis (d,pid)) = |
25 | itm_2item _ (Mis (d,pid)) = |
26 Missing (Syntax.string_of_term (ctxt_Isac"") d ^" "^ |
26 Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ |
27 Syntax.string_of_term (ctxt_Isac"") pid); |
27 Syntax.string_of_term (thy2ctxt' "Isac") pid); |
28 |
28 |
29 |
29 |
30 (* --- 8.3.00 |
30 (* --- 8.3.00 |
31 fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list) |
31 fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list) |
32 handle _ => error ("get_dsc_in not for "^sel); |
32 handle _ => error ("get_dsc_in not for "^sel); |
97 in if is_dsc hd |
97 in if is_dsc hd |
98 then (hd, args) |
98 then (hd, args) |
99 else (e_term, [t]) (*??? 9.01 just copied*) |
99 else (e_term, [t]) (*??? 9.01 just copied*) |
100 end) |
100 end) |
101 handle _ => raise error ("split_dsc: called with "^ |
101 handle _ => raise error ("split_dsc: called with "^ |
102 (Syntax.string_of_term (ctxt_Isac"") t)); |
102 (Syntax.string_of_term (thy2ctxt' "Isac") t)); |
103 (* |
103 (* |
104 > val t1 = (term_of o the o (parse thy)) "errorBound err_"; |
104 > val t1 = (term_of o the o (parse thy)) "errorBound err_"; |
105 > split_dsc t1; |
105 > split_dsc t1; |
106 (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool")) |
106 (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool")) |
107 : term * term |
107 : term * term |
132 ^(Syntax.string_of_term (thy2ctxt' "Script") t)); |
132 ^(Syntax.string_of_term (thy2ctxt' "Script") t)); |
133 |
133 |
134 |
134 |
135 |
135 |
136 (*create output-string for itm_*) |
136 (*create output-string for itm_*) |
137 fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
137 fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
138 | itm_out thy (Syn c) = c |
138 | itm_out thy (Syn c) = c |
139 | itm_out thy (Typ c) = c |
139 | itm_out thy (Typ c) = c |
140 | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
140 | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
141 | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
141 | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
142 | itm_out thy (Mis (d,pid)) = |
142 | itm_out thy (Mis (d,pid)) = |
143 Syntax.string_of_term (ctxt_Isac"") d ^" "^ |
143 Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ |
144 Syntax.string_of_term (ctxt_Isac"") pid; |
144 Syntax.string_of_term (thy2ctxt' "Isac") pid; |
145 |
145 |
146 (*22.11.00 unused |
146 (*22.11.00 unused |
147 fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*) |
147 fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*) |
148 |
148 |
149 |
149 |
161 | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms |
161 | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms |
162 in coll [] itms end; |
162 in coll [] itms end; |
163 *) |
163 *) |
164 (*--3.3.00 |
164 (*--3.3.00 |
165 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = |
165 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = |
166 Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
166 Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
167 | itm2item (_,_,_,_,Syn (c)) = SyntaxE c |
167 | itm2item (_,_,_,_,Syn (c)) = SyntaxE c |
168 | itm2item (_,_,_,_,Typ (c)) = TypeE c |
168 | itm2item (_,_,_,_,Typ (c)) = TypeE c |
169 | itm2item (_,_,_,_,Fal (d,ts)) = |
169 | itm2item (_,_,_,_,Fal (d,ts)) = |
170 False (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
170 False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
171 | itm2item (_,_,_,_,Inc (d,ts)) = |
171 | itm2item (_,_,_,_,Inc (d,ts)) = |
172 Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
172 Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
173 | itm2item (_,_,_,_,Sup (d,ts)) = |
173 | itm2item (_,_,_,_,Sup (d,ts)) = |
174 Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))); |
174 Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))); |
175 *) |
175 *) |
176 |
176 |
177 fun boolterm2item (true, term) = Correct (term2str term) |
177 fun boolterm2item (true, term) = Correct (term2str term) |
178 | boolterm2item (false, term) = False (term2str term); |
178 | boolterm2item (false, term) = False (term2str term); |
179 |
179 |
197 then ("#Find",d,ts) |
197 then ("#Find",d,ts) |
198 else if d mem (get_dsc_in dscs "#Relate") |
198 else if d mem (get_dsc_in dscs "#Relate") |
199 then ("#Relate",d,ts) |
199 then ("#Relate",d,ts) |
200 else ("#undef",d,ts); |
200 else ("#undef",d,ts); |
201 (* 28.1.00 raise error ("add_field: '"^ |
201 (* 28.1.00 raise error ("add_field: '"^ |
202 (Syntax.string_of_term (ctxt_Isac"") d)^ |
202 (Syntax.string_of_term (thy2ctxt' "Isac") d)^ |
203 "' not in ppc-description "); *) |
203 "' not in ppc-description "); *) |
204 ------9.3. *) |
204 ------9.3. *) |
205 |
205 |
206 (* 9.3.00 |
206 (* 9.3.00 |
207 compare d and dsc in pbt and transfer field to pre-ori *) |
207 compare d and dsc in pbt and transfer field to pre-ori *) |
209 let fun eq d pt = (d = (fst o snd) pt); |
209 let fun eq d pt = (d = (fst o snd) pt); |
210 in case filter (eq d) pbt of |
210 in case filter (eq d) pbt of |
211 [(fi,(dsc,_))] => (fi,d,ts) |
211 [(fi,(dsc,_))] => (fi,d,ts) |
212 | [] => ("#undef",d,ts) (*may come with met.ppc*) |
212 | [] => ("#undef",d,ts) (*may come with met.ppc*) |
213 | _ => raise error ("add_field: "^ |
213 | _ => raise error ("add_field: "^ |
214 (Syntax.string_of_term (ctxt_Isac"") d)^ |
214 (Syntax.string_of_term (thy2ctxt' "Isac") d)^ |
215 " more than once in pbt") |
215 " more than once in pbt") |
216 end; |
216 end; |
217 |
217 |
218 (*. take over field from met.ppc at 'Specify_Method' into ori, |
218 (*. take over field from met.ppc at 'Specify_Method' into ori, |
219 i.e. also removes "#undef" fields .*) |
219 i.e. also removes "#undef" fields .*) |
224 fun repl mpc (i,v,_,d,ts) = |
224 fun repl mpc (i,v,_,d,ts) = |
225 case filter (eq d) mpc of |
225 case filter (eq d) mpc of |
226 [(fi,(dsc,_))] => [(i,v,fi,d,ts)] |
226 [(fi,(dsc,_))] => [(i,v,fi,d,ts)] |
227 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*) |
227 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*) |
228 (*raise error ("add_field': "^ |
228 (*raise error ("add_field': "^ |
229 (Syntax.string_of_term (ctxt_Isac"") d)^ |
229 (Syntax.string_of_term (thy2ctxt' "Isac") d)^ |
230 " not in met"*) |
230 " not in met"*) |
231 | _ => raise error ("add_field': "^ |
231 | _ => raise error ("add_field': "^ |
232 (Syntax.string_of_term (ctxt_Isac"") d)^ |
232 (Syntax.string_of_term (thy2ctxt' "Isac") d)^ |
233 " more than once in met"); |
233 " more than once in met"); |
234 in (flat ((map (repl mpc)) ori)):ori list end; |
234 in (flat ((map (repl mpc)) ori)):ori list end; |
235 |
235 |
236 |
236 |
237 (*.mark an element with the position within a plateau; |
237 (*.mark an element with the position within a plateau; |