151 |
151 |
152 (* split type-wrapper from program-arg and build part of an ori; |
152 (* split type-wrapper from program-arg and build part of an ori; |
153 an type-error is reported immediately, raises an exn, |
153 an type-error is reported immediately, raises an exn, |
154 subsequent handling of exn provides 2nd part of error message *) |
154 subsequent handling of exn provides 2nd part of error message *) |
155 fun mtc thy (str, (dsc, _)) (ty $ var) = |
155 fun mtc thy (str, (dsc, _)) (ty $ var) = |
|
156 let val ctxt = Proof_Context.init_global thy |
|
157 in |
156 ((Thm.global_cterm_of thy (dsc $ var);(*type check*) |
158 ((Thm.global_cterm_of thy (dsc $ var);(*type check*) |
157 SOME (([1], str, dsc, (*[var]*) |
159 SOME (([1], str, dsc, (*[var]*) |
158 Input_Descript.split' (dsc, var))) (*:ori without leading #*)) |
160 Input_Descript.split' (dsc, var))) (*:ori without leading #*)) |
159 handle e as TYPE _ => |
161 handle e as TYPE _ => |
160 (tracing (dashs 70 ^ "\n" |
162 (tracing (dashs 70 ^ "\n" |
161 ^ "*** ERROR while creating the items for the model of the ->problem\n" |
163 ^ "*** ERROR while creating the items for the model of the ->problem\n" |
162 ^ "*** from the ->stac with ->typeconstructor in arglist:\n" |
164 ^ "*** from the ->stac with ->typeconstructor in arglist:\n" |
163 ^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n" |
165 ^ "*** item (->description ->value): " ^ UnparseC.term_in_ctxt ctxt dsc ^ " " ^ UnparseC.term_in_ctxt ctxt var ^ "\n" |
164 ^ "*** description: " ^ TermC.term_detail2str dsc |
166 ^ "*** description: " ^ TermC.string_of_detail ctxt dsc |
165 ^ "*** value: " ^ TermC.term_detail2str var |
167 ^ "*** value: " ^ TermC.string_of_detail ctxt var |
166 ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty |
168 ^ "*** typeconstructor in script: " ^ TermC.string_of_detail ctxt ty |
167 ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n" |
169 ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n" |
168 ^ "*** " ^ dots 66); |
170 ^ "*** " ^ dots 66); |
169 writeln (@{make_string} e); |
171 writeln (@{make_string} e); |
170 Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*) |
172 Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*) |
171 NONE)) |
173 NONE)) |
172 | mtc _ _ t = raise ERROR ("mtc: uncovered case with" ^ UnparseC.term t) |
174 end |
|
175 | mtc thy _ t = |
|
176 let val ctxt = Proof_Context.init_global thy |
|
177 in raise ERROR ("mtc: uncovered case with" ^ UnparseC.term_in_ctxt ctxt t) end |
173 |
178 |
174 (* match each pat of the model-pattern with an actual argument; |
179 (* match each pat of the model-pattern with an actual argument; |
175 precondition: copy-named vars are filtered out *) |
180 precondition: copy-named vars are filtered out *) |
176 fun matc _ [] _ oris = oris |
181 fun matc _ [] _ oris = oris |
177 | matc _ pbt [] _ = |
182 | matc _ pbt [] _ = |