theory LLVM_Checker imports SEG_XML_Parser LLVM_Termination_Prover begin definition llvm_termination_parser where "llvm_termination_parser = XMLdo STR ''certificationProblem'' { (fn, p) ← xml_do STR ''input'' (xml_take (xml_do STR ''llvm'' llvm_input_parser) xml_return); version ←? xml_text (STR ''cpfVersion''); proof ← xml_do STR ''proof'' (xml_take (xml_do STR ''llvmTerminationProof'' llvm_termination_proof_parser) xml_return); orig ←? xml_any; xml_return (fn, p, proof) }" definition llvm_seg_represents_cpf_parser where "llvm_seg_represents_cpf_parser = XMLdo STR ''certificationProblem'' { (fn, p) ← xml_do STR ''input'' (xml_take (xml_do STR ''llvm'' llvm_input_parser) xml_return); version ←? xml_text (STR ''cpfVersion''); seg ← xml_do STR ''proof'' (xml_take (xml_do STR ''llvmTerminationProof'' llvm_represents_seg_parser) xml_return); orig ←? xml_any; xml_return (fn, p, seg) }" definition llvm_lts_represents_cpf_parser where "llvm_lts_represents_cpf_parser = XMLdo STR ''certificationProblem'' { (fn, p) ← xml_do STR ''input'' (xml_take (xml_do STR ''llvm'' llvm_input_parser) xml_return); version ←? xml_text (STR ''cpfVersion''); (seg, renaming, lts) ← xml_do STR ''proof'' (xml_take (xml_do STR ''llvmTerminationProof'' llvm_represents_lts_parser) xml_return); orig ←? xml_any; xml_return (fn, p, seg, renaming, lts) }" definition "parse_llvm_cert_problem = parse_xmlfile llvm_termination_parser" fun llvm_termination_checker where "llvm_termination_checker s = (case parse_xmlfile llvm_termination_parser (String.explode s) of Left s ⇒ (showsl ''FAILED⏎Error message:⏎'' ∘ showsl s) STR '''' | Right (fn, p, llvm_proof) ⇒ case llvm_check_termination p fn llvm_proof of Inl l ⇒ (showsl ''FAILED⏎Error message:⏎'' ∘ l) STR '''' | Inr r ⇒ STR ''CERTIFIED'')" fun llvm_seg_represents_checker where "llvm_seg_represents_checker s = (case parse_xmlfile llvm_seg_represents_cpf_parser (String.explode s) of Left s ⇒ (showsl ''FAILED⏎Error message:⏎'' ∘ showsl s) STR '''' | Right (fn, p, seg) ⇒ case llvm_check_represents_seg p fn seg of Inl l ⇒ (showsl ''FAILED⏎Error message:⏎'' ∘ l) STR '''' | Inr r ⇒ STR ''CERTIFIED'')" fun llvm_lts_represents_checker where "llvm_lts_represents_checker s = (case parse_xmlfile llvm_lts_represents_cpf_parser (String.explode s) of Left s ⇒ (showsl ''FAILED⏎Error message:⏎'' ∘ showsl s) STR '''' | Right (fn, p, seg, renaming, l) ⇒ case llvm_check_represents_lts p fn seg l renaming of Inl l ⇒ (showsl ''FAILED⏎Error message:⏎'' ∘ l) STR '''' | Inr r ⇒ STR ''CERTIFIED'')" end