Hi,
I'm writing an interface between a proprietary model checker and the theorem prover Isabelle. For this, I need to parse some XML and I've been carrying around a record with different data I need for this. After trying to exend this record, I get
InternalError: addFieldToGeneric: Not a labelled record raised while compiling
when trying to load my XML parser. Unfortunately, I'm somewhat restrained when it comes to posting my code, but maybe someone can help me locate the problem anyway.
The working version of the program had the functions
fun update_typs {typs,thy} typs' = {typs=typs',thy=thy } fun update_thy {typs,thy} thy' = {typs=typs ,thy=thy'}
and the main function was just
fun import_file filename thy = let val body = body_of (parse_file filename) val typs = Symtab.update_new(("t",Free("t",timeT)),Symtab.empty) in #thy (parse_itl body {typs=typs,thy=thy}) end
all code reachable from the function parse_itl only accesses/manipulates the record through functions #thy, #typs, update_typs, and update_thy, and this worked fine. I then needed an extra field, and thefore extended the record:
fun update_typs {macs,typs,thy} typs' = {macs=macs,typs=typs',thy=thy } fun update_thy {macs,typs,thy} thy' = {macs=macs,typs=typs ,thy=thy'}
fun import_file filename thy = let val body = body_of (parse_file filename) val typs = Symtab.update_new(("t",Free("t",timeT)),Symtab.empty) in #thy (parse_itl body {macs=Symtab.empty,typs=typs,thy=thy}) end
with the rest of the program unchanged; This provokes the aforementioned "internal error". I've tried to isolate the problem, but so far without success. Any ideas?
Best,
- Sebastian