Theory Phi_Element_Path

theory Phi_Element_Path
  imports Phi_System.Calculus_of_Programming Phi_BI.PhiTool_Symbol
begin

section ‹Path of Elements in an Aggregate Structure›

unspecified_type sVAL ― ‹small Value›

debt_axiomatization sVAL_emb :: ‹sVAL ⇒ VAL›  ― ‹embedding small value›
                and is_sTY   :: ‹TY ⇒ bool›   ― ‹is small type›
  where sVAL_emb_inj: ‹sVAL_emb x = sVAL_emb y ⟷ x = y›
    and is_sTY: ‹is_sTY T ⟹ v ∈ Well_Type T ⟹ v ∈ range sVAL_emb›
    and is_sTY_poison: ‹is_sTY 𝗉𝗈𝗂𝗌𝗈𝗇›

lemma inj_sVAL_emb:
  ‹inj sVAL_emb›
  by (meson injI sVAL_emb_inj)


datatype 'val aggregate_index' = AgIdx_N nat | AgIdx_S symbol | AgIdx_V 'val

declare aggregate_index'.simps[φsafe_simp]

type_synonym aggregate_index = ‹sVAL aggregate_index'›
type_synonym aggregate_path = ‹aggregate_index list›

nonterminal "φ_ag_idx_"

syntax "_ID_ag_idx_"  :: ‹φ_symbol_ ⇒ φ_ag_idx_› ("_")
       "_0_ag_idx_"   :: ‹φ_ag_idx_› ("0")
       "_1_ag_idx_"   :: ‹φ_ag_idx_› ("1")
       "_num_ag_idx_" :: ‹num_token ⇒ φ_ag_idx_› ("_")
       "_log_ag_idx_" :: ‹logic ⇒ φ_ag_idx_› ("LOGIC'_IDX'(_')")
       "_log_num_ag_idx_" :: ‹logic ⇒ φ_ag_idx_› ("_⇧𝗍⇧𝗁" [1000] 999)
       "_log_num_ag_idx'_" :: ‹logic ⇒ φ_ag_idx_› ("'(_')⇧𝗍⇧𝗁")
       "_log_num_ag_idx_ascii_" :: ‹logic ⇒ φ_ag_idx_› ("#_" [1000] 999)
       "_log_num_ag_idx_ascii'_" :: ‹logic ⇒ φ_ag_idx_› ("#'(_')")
       "_MK_ag_idx_"  :: ‹φ_ag_idx_ ⇒ aggregate_index› ("AG'_IDX'(_')")

ML ‹
structure Phi_Aggregate_Syntax = struct

fun parse_index (Const(\<^syntax_const>‹_ID_ag_idx_› , _) $ id) =
        Const(\<^const_name>‹AgIdx_S›, dummyT) $ id
  | parse_index (Const(\<^syntax_const>‹_num_ag_idx_›, _) $ Free (n, _)) =
        Const(\<^const_name>‹AgIdx_N›, dummyT) $ mk_numeral_nat (Value.parse_nat n)
  | parse_index (Const(\<^syntax_const>‹_log_ag_idx_›, _) $ tm) = tm
  | parse_index (Const(\<^syntax_const>‹_log_num_ag_idx_›, _) $ tm) =
        Const(\<^const_name>‹AgIdx_N›, dummyT) $ tm
  | parse_index (Const(\<^syntax_const>‹_log_num_ag_idx'_›, _) $ tm) =
        Const(\<^const_name>‹AgIdx_N›, dummyT) $ tm
  | parse_index (Const(\<^syntax_const>‹_log_num_ag_idx_ascii_›, _) $ tm) =
        Const(\<^const_name>‹AgIdx_N›, dummyT) $ tm
  | parse_index (Const(\<^syntax_const>‹_log_num_ag_idx_ascii'_›, _) $ tm) =
        Const(\<^const_name>‹AgIdx_N›, dummyT) $ tm
  | parse_index (Const(\<^syntax_const>‹_0_ag_idx_›, _)) =
        Const(\<^const_name>‹AgIdx_N›, dummyT) $ mk_numeral_nat 0
  | parse_index (Const(\<^syntax_const>‹_1_ag_idx_›, _)) =
        Const(\<^const_name>‹AgIdx_N›, dummyT) $ mk_numeral_nat 1
  | parse_index x = (@{print} x; error "SYNTAX ERROR #ee2e77a2-b6d7-4acf-ae18-5d266dc2f06e")

fun is_atom (Const ("_free", _) $ X) = is_atom X
  | is_atom (Const ("_var", _) $ X) = is_atom X
  | is_atom (_ $ _) = false
  | is_atom _ = true

fun print_index (Const(\<^const_syntax>‹AgIdx_S›, _) $ (Const(\<^const_syntax>‹mk_symbol›, _) $ tm)) =
     (case Phi_Tool_Symbol.revert_symbol (dest_synt_numeral tm)
        of SOME id => Free(id, dummyT)
         | NONE => tm)
  | print_index (Const(\<^const_syntax>‹AgIdx_S›, _) $ tm) =
     Const (\<^syntax_const>‹_LOG_EXPR_SYMBOL_›, dummyT) $ tm
  | print_index (Const (\<^const_syntax>‹AgIdx_N›, _) $ tm) =
      (case try dest_synt_numeral tm
         of SOME N => Const(\<^syntax_const>‹_log_num_ag_idx_›, dummyT) $ Free(string_of_int N, dummyT)
          | _ => if is_atom tm
                 then Const(\<^syntax_const>‹_log_num_ag_idx_›, dummyT) $ tm
                 else Const(\<^syntax_const>‹_log_num_ag_idx'_›, dummyT) $ tm)
  | print_index tm = Const(\<^syntax_const>‹_log_ag_idx_›, dummyT) $ tm

end
›

parse_translation ‹[
  (\<^syntax_const>‹_MK_ag_idx_›, fn ctxt => fn [x] => Phi_Aggregate_Syntax.parse_index x)
]›

print_translation ‹[
  (\<^const_syntax>‹AgIdx_S›, (fn ctxt => fn [Const(\<^const_syntax>‹mk_symbol›, _) $ tm] =>
      case Phi_Tool_Symbol.revert_symbol (dest_synt_numeral tm)
        of SOME id => Const (\<^syntax_const>‹_MK_ag_idx_›, dummyT) $ Free(id, dummyT)
         | NONE => tm)),
  (\<^const_syntax>‹AgIdx_N›, (fn ctxt => fn [tm] =>
      case try dest_synt_numeral tm
        of SOME N => Const (\<^syntax_const>‹_MK_ag_idx_›, dummyT) $
                        (Const(\<^syntax_const>‹_log_num_ag_idx_›, dummyT) $ Free(string_of_int N, dummyT))
         | NONE => Const (\<^syntax_const>‹_MK_ag_idx_›, dummyT) $ (
            if Phi_Aggregate_Syntax.is_atom tm
            then Const (\<^syntax_const>‹_log_num_ag_idx_›, dummyT) $ tm
            else Const (\<^syntax_const>‹_log_num_ag_idx'_›, dummyT) $ tm)))
]›






end