Theory Phi_BI.PhiTool_Symbol

theory PhiTool_Symbol
  imports Main
begin

section ‹Symbol Identifier unique in Isabelle Runtime and Its Persistent Image›

text ‹When the runtime system uses N symbols in total, the length of the representation
      consumes at most 2 + log2(N) terms.
TODO: don't use nat but make a numeral so we don't need the mk_symbol wrapper›

typedef symbol = ‹UNIV::nat set›
  morphisms Abs_symbol mk_symbol
  by auto

hide_const Abs_symbol

declare mk_symbol_inject[simplified, iff]

lemma mk_symbol_cong[cong]:
  ‹mk_symbol A ≡ mk_symbol A› .

ML_file ‹./library/syntax/PhiTool_Symbol_syntax.ML›
ML_file ‹PhiTool_Symbol.ML›

nonterminal "φ_symbol_"

syntax "_ID_SYMBOL_" :: ‹id ⇒ φ_symbol_› ("_")
       "_LOG_EXPR_SYMBOL_" :: ‹logic ⇒ φ_symbol_› ("SYMBOL'_VAR'(_')")
       "_MK_SYMBOL_" :: ‹φ_symbol_ ⇒ symbol› ("SYMBOL'(_')")

ML ‹
structure Phi_Tool_Symbol = struct
open Phi_Tool_Symbol

fun parse (Free (id, _)) = Phi_Tool_Symbol.mk_symbol id
  | parse tm = (@{print} tm; error "Expect an identifier.")

fun print tm =
  case Option.map Phi_Tool_Symbol.revert_symbol (try dest_synt_numeral tm)
    of SOME (SOME id) => Free(id, dummyT)
     | SOME NONE => error ("Phi_Tool_Symbol: " ^ string_of_int (dest_synt_numeral tm) ^ " is not a known symbol!")
     | NONE => tm

end
›

parse_translation ‹[
  (\<^syntax_const>‹_ID_SYMBOL_›, (fn ctxt => fn [x] => Phi_Tool_Symbol.parse x)),
  (\<^syntax_const>‹_LOG_EXPR_SYMBOL_›, (fn ctxt => fn [x] =>
        Const (\<^syntax_const>‹_constrain›, dummyT) $ x $ Const(\<^type_syntax>‹symbol›, dummyT))),
  (\<^syntax_const>‹_MK_SYMBOL_›, (fn ctxt => fn [x] => x))
]›


print_translation ‹[
  (\<^const_syntax>‹mk_symbol›, (fn ctxt => fn [tm] => Const (\<^syntax_const>‹_MK_SYMBOL_›, dummyT) $ Phi_Tool_Symbol.print tm))
]›

ML ‹@{term ‹SYMBOL(xxx)›}›


end