Theory Phi_Logic_Programming_Reasoner.PLPR_error_msg

(*There is still a design under consideration.

It intends to give a rich way with term quotations to represent and report
  error messages in the logic programming based reasoning.
*)

theory PLPR_error_msg
  imports Phi_Logic_Programming_Reasoner
begin

section ‹Error Reporting›

subsection ‹Encoding of Text›

typedecl "text"

setup ‹Sign.mandatory_path "text"›

consts literal :: ‹(text ⇒ text) ⇒ text›
       "term"  :: ‹'a::{} ⇒ text›
       type    :: ‹'a::{} itself ⇒ text›
       cat     :: ‹text ⇒ text ⇒ text›
       newline :: ‹text›
      "text"    :: ‹text ⇒ text›

setup ‹Sign.parent_path›

text ‹We use the name of a lambda variable to encode an arbitrary string text.›

nonterminal "text_"
syntax "_text_" :: ‹text_ ⇒ text› ("TEXT'(_')" [1] 1000)
syntax "_text_literal_" :: ‹cartouche ⇒ text_› ("_")
syntax "_text_term_" :: ‹logic ⇒ text_› ("_" [1000] 999)
syntax "_text_prop_" :: ‹prop ⇒ text_› ("_" [1000] 999)
syntax "_text_newline_" :: ‹text_› ("⏎")
syntax "_text_cat_" :: ‹text_ ⇒ text_ ⇒ text_› ("_ _" [1,2] 1)

ML ‹
structure Text_Encoding = struct

val escape_string   = String.translate (fn #"." => "\001" | x => str x)
val recovery_string = String.translate (fn #"\001" => "." | x => str x)

local open Ast
  fun dest_literal (Appl [Constant \<^syntax_const>‹_constrain›, x, _]) = dest_literal x
    | dest_literal (Appl [Constant \<^syntax_const>‹_bound›, x]) = dest_literal x
    | dest_literal (Variable x) = recovery_string x

fun decode_text_ast' ret (Appl [Constant \<^const_syntax>‹text.literal›,
      Appl [Constant \<^syntax_const>‹_abs›, x, _]])
      = Variable (cartouche (dest_literal x))::ret
  | decode_text_ast' ret (Appl [Constant \<^const_syntax>‹text.term›, tm])
      = tm::ret
  | decode_text_ast' ret (Appl [Constant \<^const_syntax>‹text.type›, tm])
      = tm::ret
  | decode_text_ast' ret (Constant \<^const_syntax>‹text.newline›)
      = (Constant \<^syntax_const>‹_text_newline_›)::ret
  | decode_text_ast' ret (Appl [Constant \<^const_syntax>‹text.cat›, tmA, tmB])
      = decode_text_ast' (decode_text_ast' ret tmB) tmA
  | decode_text_ast' _ ast = raise AST ("decode_text_ast", [ast])

in

fun decode_text _ (\<^const>‹text.literal› $ Abs (text, _, _)) = [Pretty.str (recovery_string text)]
  | decode_text ctxt (Const (\<^const_name>‹text.term›, _) $ x) = [Syntax.pretty_term ctxt x]
  | decode_text ctxt (Const (\<^const_name>‹text.type›, _) $ \<^Const_>‹Pure.type T›) =
      [Syntax.pretty_typ ctxt T]
  | decode_text ctxt (\<^const>‹text.cat› $ A $ B) =
      decode_text ctxt A @ decode_text ctxt B
  | decode_text _ (\<^const>‹text.newline›) = [Pretty.brk 0]
  | decode_text ctxt (\<^const>‹text.text› $ X) = decode_text ctxt X
  | decode_text _ tm = raise TERM ("decode_text", [tm])

fun decode_text_pretty ctxt X = Pretty.block (Pretty.separate "" (decode_text ctxt X))
fun decode_text_str ctxt X = Pretty.string_of (decode_text_pretty ctxt X)

fun decode_text_ast ast =
  case decode_text_ast' [] ast
    of [] => Variable ""
     | [x] => x
     | l => Appl l

end
end
›

parse_ast_translation ‹
let open Ast
  fun dest_literal (Appl [Constant \<^syntax_const>‹_constrain›, x, _]) = dest_literal x
    | dest_literal (Appl [Constant \<^syntax_const>‹_text_literal_›, x]) = dest_literal x
    | dest_literal (Variable x) = String.substring (x, 7, size x - 15)
        (*7 for size of \ <open> and 15 for size of \ <open> \ <close>*)
  fun encode_literal str =
    Appl [Constant \<^const_syntax>‹text.literal›,
    Appl [Constant \<^syntax_const>‹_abs›,
      Appl [Constant \<^syntax_const>‹_constrain›,
            Variable (Text_Encoding.escape_string str),
            Constant \<^type_syntax>‹text›],
      Appl [Constant \<^syntax_const>‹_constrain›,
            Constant \<^const_syntax>‹undefined›,
            Constant \<^type_syntax>‹text›]]]
  fun parse (Appl [Constant \<^syntax_const>‹_text_literal_›, tm]) = encode_literal (dest_literal tm)
    | parse (Appl [Constant \<^syntax_const>‹_text_prop_›, tm]) =
        parse (Appl [Constant \<^syntax_const>‹_text_term_›, tm])
    | parse (Appl [Constant \<^syntax_const>‹_text_term_›,
                       (tm as Appl [Constant \<^syntax_const>‹_TYPE›, _])]) =
        Appl [Constant \<^const_syntax>‹text.type›, tm]
    | parse (Appl [Constant \<^syntax_const>‹_text_term_›, tm]) =
        Appl [Constant \<^const_syntax>‹text.term›, tm]
    | parse (Constant \<^syntax_const>‹_text_newline_›) = Constant \<^const_syntax>‹text.newline›
    | parse (Appl [Constant \<^syntax_const>‹_text_cat_›, tmA, tmB]) =
        Appl [Constant \<^const_syntax>‹text.cat›, parse tmA, parse tmB]
in
  [(\<^syntax_const>‹_text_›, (fn ctxt => fn [ast] =>
        Appl [Constant \<^const_syntax>‹text.text›, parse ast]))]
end›

print_ast_translation ‹[(\<^const_syntax>‹text.text›, (fn ctxt => fn [ast] =>
  Ast.Appl [Ast.Constant \<^syntax_const>‹_text_›, Text_Encoding.decode_text_ast ast]))]›


subsection ‹Reasoners for Printing Message›

subsubsection ‹Tracing›

definition TRACING :: ‹text ⇒ bool›
  where [iff]: ‹TRACING x ⟷ True›

lemma TRACING_I: ‹TRACING x›
  unfolding TRACING_def ..

φreasoner_ML TRACING 1200 (‹TRACING ?x›) = ‹fn (ctxt,sequent) =>
  let
    val \<^const>‹Trueprop› $ (\<^const>‹TRACING› $ text)
          = Thm.major_prem_of sequent
    val str = Text_Encoding.decode_text_str ctxt text
    val _ = tracing str
  in Seq.single (ctxt, @{thm TRACING_I} RS sequent)
  end›

subsubsection ‹Warning›

definition WARNING :: ‹text ⇒ bool›
  where [iff]: ‹WARNING x ⟷ True›

lemma WARNING_I: ‹WARNING x›
  unfolding WARNING_def ..

φreasoner_ML WARNING 1200 (‹WARNING ?x›) = ‹fn (ctxt,sequent) =>
  let
    val \<^const>‹Trueprop› $ (\<^const>‹WARNING› $ text)
          = Thm.major_prem_of sequent
    val str = Text_Encoding.decode_text_str ctxt text
    val _ = warning str
  in Seq.single (ctxt, @{thm WARNING_I} RS sequent)
  end›

subsubsection ‹Fail›

text ‹Fail ends the current search branch but does not terminate
 the whole reasoning.›

definition FAIL :: ‹text ⇒ bool›
  where [iff]: ‹FAIL x ⟷ False›

definition FAIL' :: ‹text ⇒ prop›
  where [iff]: ‹FAIL' x ≡ (⋀P. PROP P)›

φreasoner_ML FAIL 1200 (‹FAIL ?x› | ‹PROP FAIL' ?x'›) = ‹fn (ctxt,sequent) =>
  let
    val text = case Thm.major_prem_of sequent
                 of \<^const>‹Trueprop› $ (\<^const>‹FAIL› $ X) => X
                  | \<^const>‹FAIL'› $ X => X
    val str = Text_Encoding.decode_text_str ctxt text
    val _ = warning str
  in Seq.empty
  end›


subsubsection ‹Error›

text ‹Fail terminates the whole reasoning.›

definition ERROR :: ‹text ⇒ bool›
  where [iff]: ‹ERROR x ⟷ False›

definition ERROR' :: ‹text ⇒ prop›
  where [iff]: ‹ERROR' x ≡ (⋀P. PROP P)›

φreasoner_ML ERROR 1200 (‹ERROR ?x› | ‹PROP ERROR' ?x'›) = ‹fn (ctxt,sequent) =>
  let
    val text = case Thm.major_prem_of sequent
                 of \<^const>‹Trueprop› $ (\<^const>‹ERROR› $ X) => X
                  | \<^const>‹ERROR'› $ X => X
    val str = Text_Encoding.decode_text_str ctxt text
    val _ = error str
  in Seq.empty
  end›

end