Theory LLVM_Checker

theory LLVM_Checker
imports SEG_XML_Parser
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