95 (*Like "interpret_problem" above, but it is given a filename rather than |
95 (*Like "interpret_problem" above, but it is given a filename rather than |
96 a parsed problem.*) |
96 a parsed problem.*) |
97 val interpret_file : bool -> Path.T -> Path.T -> type_map -> const_map -> |
97 val interpret_file : bool -> Path.T -> Path.T -> type_map -> const_map -> |
98 theory -> tptp_general_meaning * theory |
98 theory -> tptp_general_meaning * theory |
99 |
99 |
|
100 type position = string * int * int |
|
101 exception MISINTERPRET of position list * exn |
100 exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula |
102 exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula |
101 exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol |
103 exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol |
102 exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term |
104 exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term |
103 exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type |
105 exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type |
104 |
106 |
117 |
119 |
118 structure TPTP_Interpret : TPTP_INTERPRET = |
120 structure TPTP_Interpret : TPTP_INTERPRET = |
119 struct |
121 struct |
120 |
122 |
121 open TPTP_Syntax |
123 open TPTP_Syntax |
|
124 type position = string * int * int |
|
125 exception MISINTERPRET of position list * exn |
122 exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula |
126 exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula |
123 exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol |
127 exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol |
124 exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term |
128 exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term |
125 exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type |
129 exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type |
126 |
130 |
670 ((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str |
674 ((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str |
671 fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str |
675 fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str |
672 |
676 |
673 fun interpret_line config inc_list type_map const_map path_prefix line thy = |
677 fun interpret_line config inc_list type_map const_map path_prefix line thy = |
674 case line of |
678 case line of |
675 Include (quoted_path, inc_list) => |
679 Include (_, quoted_path, inc_list) => |
676 interpret_file' |
680 interpret_file' |
677 config |
681 config |
678 inc_list |
682 inc_list |
679 path_prefix |
683 path_prefix |
680 (Path.append |
684 (Path.append |
683 |> unenclose |
687 |> unenclose |
684 |> Path.explode)) |
688 |> Path.explode)) |
685 type_map |
689 type_map |
686 const_map |
690 const_map |
687 thy |
691 thy |
688 | Annotated_Formula (pos, lang, label, role, tptp_formula, annotation_opt) => |
692 | Annotated_Formula (_, lang, label, role, tptp_formula, annotation_opt) => |
689 (*interpret a line only if "label" is in "inc_list", or if "inc_list" is |
693 (*interpret a line only if "label" is in "inc_list", or if "inc_list" is |
690 empty (in which case interpret all lines)*) |
694 empty (in which case interpret all lines)*) |
691 (*FIXME could work better if inc_list were sorted*) |
695 (*FIXME could work better if inc_list were sorted*) |
692 if null inc_list orelse is_some (List.find (fn x => x = label) inc_list) then |
696 if null inc_list orelse is_some (List.find (fn x => x = label) inc_list) then |
693 case role of |
697 case role of |
777 Syntax.check_term (Proof_Context.init_global thy') t, |
781 Syntax.check_term (Proof_Context.init_global thy') t, |
778 TPTP_Proof.extract_inference_info annotation_opt)]), thy') |
782 TPTP_Proof.extract_inference_info annotation_opt)]), thy') |
779 end |
783 end |
780 else (*do nothing if we're not to includ this AF*) |
784 else (*do nothing if we're not to includ this AF*) |
781 ((type_map, const_map, []), thy) |
785 ((type_map, const_map, []), thy) |
|
786 |
782 and interpret_problem config inc_list path_prefix lines type_map const_map thy = |
787 and interpret_problem config inc_list path_prefix lines type_map const_map thy = |
783 let |
788 let |
784 val thy_name = Context.theory_name thy |
789 val thy_name = Context.theory_name thy |
785 in |
790 in |
786 fold (fn line => |
791 fold (fn line => |
787 fn ((type_map, const_map, lines), thy) => |
792 fn ((type_map, const_map, lines), thy) => |
788 let |
793 let |
789 (*process the line, ignoring the type-context for variables*) |
794 (*process the line, ignoring the type-context for variables*) |
790 val ((type_map', const_map', l'), thy') = |
795 val ((type_map', const_map', l'), thy') = |
791 interpret_line config inc_list type_map const_map path_prefix line thy |
796 interpret_line config inc_list type_map const_map path_prefix line thy |
|
797 handle |
|
798 (*package all exceptions to include position information, |
|
799 even relating to multiple levels of "include"ed files*) |
|
800 (*FIXME "exn" contents may appear garbled due to markup |
|
801 FIXME this appears as ML source position *) |
|
802 MISINTERPRET (pos_list, exn) => |
|
803 raise MISINTERPRET |
|
804 (TPTP_Syntax.pos_of_line line :: pos_list, exn) |
|
805 | exn => raise MISINTERPRET |
|
806 ([TPTP_Syntax.pos_of_line line], exn) |
792 in |
807 in |
793 ((type_map', |
808 ((type_map', |
794 const_map', |
809 const_map', |
795 l' @ lines),(*append is sufficient, union would be overkill*) |
810 l' @ lines),(*append is sufficient, union would be overkill*) |
796 thy') |
811 thy') |