Theory PhSm_Ag_Base

theory PhSm_Ag_Base
  imports PhiSem_Common_Int PhiSem_Symbol
  keywords "⦃" "⦄" "‣" :: quasi_command
  abbrevs "|>"  = "‣"
begin

text ‹The base for aggregate values which have inner structures and whose members can be
  accessed using indexes.›

section ‹Semantics›

debt_axiomatization
        valid_idx_step :: ‹TY ⇒ aggregate_index ⇒ bool›
    and idx_step_type  :: ‹aggregate_index ⇒ TY ⇒ TY›
    and idx_step_value :: ‹aggregate_index ⇒ VAL ⇒ VAL›
    and idx_step_mod_value :: ‹aggregate_index ⇒ (VAL ⇒ VAL) ⇒ VAL ⇒ VAL›
    and type_measure :: ‹TY ⇒ nat›
where welltyp_subject_idx_step:
           ‹valid_idx_step T i
        ⟹ v ∈ Well_Type T
        ⟹ idx_step_value i v ∈ Well_Type (idx_step_type i T)›
and   valid_idx_not_poison:
           ‹valid_idx_step T i ⟹ T ≠ 𝗉𝗈𝗂𝗌𝗈𝗇 ⟹ idx_step_type i T ≠ 𝗉𝗈𝗂𝗌𝗈𝗇›
and   idx_step_mod_value :
           ‹valid_idx_step T i
        ⟹ valid_idx_step T j
        ⟹ v ∈ Well_Type T
        ⟹ idx_step_value i (idx_step_mod_value j f v) =
              (if i = j then f (idx_step_value j v) else idx_step_value i v) ›
and   idx_step_mod_value_unchanged :
          ‹ valid_idx_step T i
        ⟹ u ∈ Well_Type T
        ⟹ f (idx_step_value i u) = idx_step_value i u
        ⟹ idx_step_mod_value i f u = u ›
and   idx_step_mod_value_welltyp:
           ‹valid_idx_step T i
        ⟹ v ∈ Well_Type T
        ⟹ f (idx_step_value i v) ∈ Well_Type (idx_step_type i T)
        ⟹ idx_step_mod_value i f v ∈ Well_Type T›
and   idx_step_type_measure:
           ‹valid_idx_step T i ⟹ type_measure (idx_step_type i T) < type_measure T›

text ‹We first formalize the behavior of indexing one-step inside one level of the inner structures,
  and upon them indexing of multiple steps is successively playing each step.

  \<^const>‹valid_idx_step› asserts whether an index is valid on the type.
  \<^const>‹idx_step_type› steps into the inner type of the given type.
  \<^const>‹idx_step_value› gives the inner structure of a given value, and \<^const>‹idx_step_mod_value›
    enables to modify the inner structure.
  \<^const>‹type_measure› is a scaffold giving a decreasing measurement when indexing inside,
    such as the size of the term. It helps induction over the indexing. 
›

ML_file ‹library/ag_semantics.ML›

abbreviation ‹index_value ≡ fold idx_step_value› (*TODO: rename → get_element_of_value*)
abbreviation ‹index_type  ≡ fold idx_step_type›  (* get_element_of_type *)
abbreviation ‹index_mod_value ≡ foldr idx_step_mod_value› (* modify_value_element *)

primrec valid_index :: ‹TY ⇒ aggregate_path ⇒ bool›
  where ‹valid_index T [] ⟷ True›
      | ‹valid_index T (i#idx) ⟷ valid_idx_step T i ∧ valid_index (idx_step_type i T) idx›

declare [[φreason_default_pattern ‹valid_index ?T ?idx› ⇒ ‹valid_index ?T ?idx› (100)]]

φreasoner_group chk_sem_ele_idx_all = (1000, [0, 2000]) for (‹is_valid_step_idx_of idx T U›,
                                                              ‹is_valid_index_of idx T U›)
    ‹check whether the given element index ‹idx› is valid against semantic type ‹T››
  and chk_sem_ele_idx = (1010, [1000,1030]) in chk_sem_ele_idx_all
    ‹cutting rules›
  and chk_sem_ele_idx_fail = (0, [0,0]) in chk_sem_ele_idx_all
    ‹failure›

lemma [φreason %chk_sem_ele_idx]: ‹valid_index T []› by simp

lemma valid_index_tail[iff]:
  ‹valid_index T (idx@[i]) ⟷ valid_index T idx ∧ valid_idx_step (index_type idx T) i›
  by (induct idx arbitrary: T; simp)

lemma [φreason %chk_sem_ele_idx_fail]:
  ‹ FAIL TEXT(‹Fail to show the validity of index› idx ‹on type› T)
⟹ valid_index T idx›
  unfolding FAIL_def
  by blast

lemma valid_index_cat: ‹valid_index T (a@b) ⟹ valid_index T a ∧ valid_index (index_type a T) b›
  by (induct a arbitrary: T; simp)

lemma valid_index_cons: ‹valid_index T [i] ⟷ valid_idx_step T i› by simp

lemma index_value_welltyp:
  ‹valid_index T idx ⟹ v ∈ Well_Type T ⟹ index_value idx v ∈ Well_Type (index_type idx T)›
  apply (induct idx arbitrary: v T; simp)
  using welltyp_subject_idx_step
  by blast

lemma index_type_measure:
  ‹valid_index T idx ⟹ idx ≠ [] ⟹ type_measure (index_type idx T) < type_measure T›
  apply (induct idx arbitrary: T; simp)
  by (metis dual_order.strict_trans fold_simps(1) idx_step_type_measure)

lemma index_type_neq:
  ‹ valid_index T idx ⟹ idx ≠ [] ⟹ index_type idx T ≠ T ›
  using index_type_measure by fastforce

lemma index_mod_value_welltyp:
   ‹valid_index T idx
⟹ v ∈ Well_Type T
⟹ f (index_value idx v) ∈ Well_Type (index_type idx T)
⟹ index_mod_value idx f v ∈ Well_Type T›
  apply (induct idx arbitrary: T v; simp)
  using idx_step_mod_value_welltyp welltyp_subject_idx_step by blast

lemma index_type_idem:
  ‹valid_index T idx ⟹ index_type idx T = T ⟷ idx = []›
  apply (cases idx; simp; rule)
  using index_type_measure
  by (metis fold_simps(2) list.discI order_less_irrefl valid_index.simps(2))

lemma index_mod_value_unchanged:
  ‹ valid_index T idx
⟹ u ∈ Well_Type T
⟹ f (index_value idx u) = (index_value idx u)
⟹ index_mod_value idx f u = u ›
  by (induct idx arbitrary: T u f; clarsimp simp add: idx_step_mod_value_unchanged welltyp_subject_idx_step)
  

subsection ‹Semantics of aggregate path›

definition ‹AgIdx_VN v = AgIdx_N (the (φSem_int_to_logic_nat (φarg.dest v)))›

subsubsection ‹Reasoning Rules›

paragraph ‹Syntactical Check of Semantics Validity of Aggregate Path›

lemma [φreason 1000]:
  ‹chk_semantics_validity ([]::aggregate_path)›
  unfolding chk_semantics_validity_def ..

lemma [φreason 1000]:
  ‹ chk_semantics_validity [X]
⟹ chk_semantics_validity R
⟹ chk_semantics_validity (X#R)›
  for R :: aggregate_path
  unfolding chk_semantics_validity_def ..

lemma [φreason 1020]:
  ‹chk_semantics_validity [AgIdx_VN v]›
  unfolding chk_semantics_validity_def ..

lemma [φreason 1020]:
  ‹chk_semantics_validity [AgIdx_S s]›
  unfolding chk_semantics_validity_def ..

lemma [φreason 1020]:
  ‹ Is_Literal n
⟹ chk_semantics_validity [AgIdx_N n]›
  unfolding chk_semantics_validity_def ..



section ‹Instructions›

(* definition op_cons_tuple :: "'TY list ⇒ (VAL list) proc'"
  where "op_cons_tuple tys = (λ(vs,res).
    let N = length tys in
    if N ≤ length vs ∧ list_all2 (λv t. v ∈ Well_Type t) (take N vs) tys
    then Success (sem_mk_tup (take N vs) # drop N vs, res)
    else Fail)" *)


definition op_get_aggregate :: "aggregate_path ⇒ TY ⇒ (VAL, VAL) proc'"
  where "op_get_aggregate idx T = (λv.
    φM_getV T id v (λv'.
    φM_assert (valid_index T idx) ⪢
    Return (φarg (index_value idx v'))
))"

debt_axiomatization allow_assigning_different_typ :: ‹TY ⇒ aggregate_path ⇒ bool›

definition op_set_aggregate :: "TY ⇒ TY ⇒ aggregate_path ⇒ (VAL × VAL, VAL) proc'"
  where "op_set_aggregate Tt Tv idx = 
    φM_caseV (λtup v.
    φM_assert (valid_index Tt idx ∧ (index_type idx Tt = Tv ∨ allow_assigning_different_typ Tt idx)) ⪢
    φM_getV Tt id tup (λtup'.
    φM_getV Tv id v (λv'.
    Return (φarg (index_mod_value idx (λ_. v') tup'))
)))"


section ‹Reasoning›

text ‹All the reasoning rules below are for semantic properties.
      All reasoning rules for transformations and SL are derived automatically›

subsection ‹Index Validation›

definition ‹is_valid_step_idx_of idx T U ⟷ valid_idx_step T idx ∧ U = idx_step_type idx T›
definition ‹is_valid_index_of idx T U ⟷ valid_index T idx ∧ U = index_type idx T›

declare [[
  φreason_default_pattern ‹is_valid_index_of ?idx ?T _› ⇒ ‹is_valid_index_of ?idx ?T _› (100)
                      and ‹is_valid_step_idx_of ?idx ?T _ › ⇒ ‹is_valid_step_idx_of ?idx ?T _ › (100),
  φpremise_attribute once? [φreason? %local] for ‹is_valid_index_of _ _ _›     (%φattr),
  φpremise_attribute once? [φreason? %local] for ‹is_valid_step_idx_of _ _ _›  (%φattr)
]]

lemma is_valid_index_of_Nil:
  ‹is_valid_index_of [] TY TY' ⟷ TY = TY'›
  unfolding is_valid_index_of_def by simp blast

lemma [φreason %chk_sem_ele_idx]:
  ‹ is_valid_index_of idx T U
⟹ valid_index T idx›
  unfolding is_valid_index_of_def by blast

lemma [φreason %chk_sem_ele_idx]:
  ‹ is_valid_index_of [] T T ›
  unfolding is_valid_index_of_def by simp

lemma [φreason %chk_sem_ele_idx]:
  ‹ is_valid_step_idx_of i T W
⟹ is_valid_index_of idx W U
⟹ is_valid_index_of (i # idx) T U ›
  unfolding is_valid_index_of_def is_valid_step_idx_of_def
  by simp

subsection ‹parse_ele_idx› ― ‹Parse Element Index Input by Semantic Type›

consts 𝒜parse_eleidx :: action

definition ‹parse_eleidx_input TY (input::element_index_input) semantic_idx spec_idx (reject::element_index_input)
    ⟷ valid_index TY spec_idx ∧ semantic_idx = spec_idx›

definition ‹parse_eleidx_input_least1 TY input sem_idx spec_idx reject
    ⟷ parse_eleidx_input TY input sem_idx spec_idx reject ∧
        (input ≠ [] ⟶ spec_idx ≠ [])›

declare [[
  φreason_default_pattern
      ‹parse_eleidx_input ?TY ?input _ _ _ › ⇒ ‹parse_eleidx_input ?TY ?input _ _ _ › (100)
  and ‹parse_eleidx_input_least1 ?TY ?input _ _ _ › ⇒ ‹parse_eleidx_input_least1 ?TY ?input _ _ _ › (100),

  φpremise_attribute once? [φreason? %local] for ‹parse_eleidx_input _ _ _ _ _›         (%φattr),
  φpremise_attribute once? [φreason? %local] for ‹parse_eleidx_input_least1 _ _ _ _ _›  (%φattr)
]]

φreasoner_group 𝒜parse_eleidx = (1000, [1000,1000]) for ‹φarg.dest v ⊨ S @tag 𝒜parse_eleidx›
      ‹rules giving abstract specifiction of the values of an element index›
  and parse_eleidx_input_all = (1000, [1, 2000]) for ‹parse_eleidx_input TY input semantic_idx spec_idx reject›
      ‹reasoning parsing source of element index›
  and parse_eleidx_input_success = (2000, [2000, 2000]) in parse_eleidx_input_all
      ‹direct success›
  and parse_eleidx_literal_symbol = (1700, [1700, 1700]) in parse_eleidx_input_all and < parse_eleidx_input_success
      ‹literal index›
  and parse_eleidx_literal_number = (1600, [1600, 1600]) in parse_eleidx_input_all and < parse_eleidx_literal_symbol
      ‹literal number›
  and parse_eleidx_input = (1000, [1000, 1200]) in parse_eleidx_input_all and < parse_eleidx_literal_number
      ‹usual rules›
  and parse_eleidx_number = (700, [700,899]) in parse_eleidx_input_all and < parse_eleidx_input ‹›
  and parse_eleidx_val = (500, [500,699]) in parse_eleidx_input_all and < parse_eleidx_number ‹›
  and parse_eleidx_input_fallback = (1, [1,1]) in parse_eleidx_input_all and < parse_eleidx_val
      ‹rejecting all input, meaning the parsing fails›

lemma [φreason %parse_eleidx_input]:
  ‹ parse_eleidx_input TY input sem_idx spec_idx reject
⟹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 input = [] ∨ spec_idx ≠ []
⟹ parse_eleidx_input_least1 TY input sem_idx spec_idx reject›
  unfolding parse_eleidx_input_least1_def Premise_def by simp blast

lemma [φreason %parse_eleidx_input_success]:
  ‹parse_eleidx_input TY [] [] [] []›
  unfolding parse_eleidx_input_def
  by simp

lemma [φreason default %parse_eleidx_input_fallback]:
  ‹parse_eleidx_input TY input [] [] input›
  unfolding parse_eleidx_input_def
  by simp

lemma [φreason %parse_eleidx_literal_symbol]:
  ‹ 𝗀𝗎𝖺𝗋𝖽 is_valid_step_idx_of (AgIdx_S s) TY U
⟹ parse_eleidx_input U input sem_idx spec_idx reject
⟹ parse_eleidx_input TY
      ((φarg.dest (semantic_literal (sem_mk_symbol s)), S) # input)
      (AgIdx_S s # sem_idx) (AgIdx_S s # spec_idx) reject ›
  unfolding parse_eleidx_input_def is_valid_step_idx_of_def 𝗋Guard_def Ant_Seq_def
  by clarsimp

lemma [φreason %parse_eleidx_number]:
  ‹ 𝗀𝗎𝖺𝗋𝖽 (φarg.dest v ⊨ S @tag 𝒜parse_eleidx) ∧⇩𝗋
          get_logical_nat_from_semantic_int S n ∧⇩𝗋
          is_valid_step_idx_of (AgIdx_N n) TY U
⟹ parse_eleidx_input U input sem_idx spec_idx reject
⟹ parse_eleidx_input TY              
      ((φarg.dest v, S) # input) (AgIdx_VN v # sem_idx) (AgIdx_N n # spec_idx) reject ›
  unfolding parse_eleidx_input_def Action_Tag_def
            get_logical_nat_from_semantic_int_def AgIdx_VN_def is_valid_step_idx_of_def
            𝗋nat_to_suc_nat_def 𝗋Guard_def Ant_Seq_def
  by (cases v; clarsimp; metis option.sel)

lemma [φreason %parse_eleidx_literal_number]:
  ‹ 𝗀𝗎𝖺𝗋𝖽 (φarg.dest (semantic_literal v) ⊨ S @tag 𝒜parse_eleidx) ∧⇩𝗋
          get_logical_nat_from_semantic_int (v ⦂ Itself) n ∧⇩𝗋
          is_valid_step_idx_of (AgIdx_N n) TY U
⟹ parse_eleidx_input U input sem_idx spec_idx reject
⟹ parse_eleidx_input TY
      ((φarg.dest (semantic_literal v), S) # input) (AgIdx_N n # sem_idx) (AgIdx_N n # spec_idx) reject ›
  unfolding parse_eleidx_input_def Action_Tag_def
            get_logical_nat_from_semantic_int_def AgIdx_VN_def is_valid_step_idx_of_def
            𝗋nat_to_suc_nat_def 𝗋Guard_def Ant_Seq_def
  by (clarsimp; metis option.sel)


subsection ‹Evaluate Index›

consts eval_aggregate_path :: mode

ML ‹
structure Eval_Sem_Idx_SS = Simpset (
  val initial_ss = Simpset_Configure.Minimal_SS
  val binding = SOME \<^binding>‹eval_aggregate_path›
  val comment = "Rules evaluating indexing of semantic type and value"
  val attribute = NONE
  val post_merging = I
)›

setup ‹Context.theory_map (Eval_Sem_Idx_SS.map (
  Simplifier.add_cong @{thm' mk_symbol_cong}
))›

φreasoner_ML eval_aggregate_path 1300 ( ‹𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[eval_aggregate_path] ?X' : ?X›
                                      | ‹𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇[eval_aggregate_path] ?P› )
  = ‹Phi_Reasoners.wrap (
      PLPR_Simplifier.simplifier_by_ss' (K Seq.empty) Eval_Sem_Idx_SS.get' {fix_vars=false}) o snd›


lemmas [eval_aggregate_path] = nth_Cons_0 nth_Cons_Suc fold_simps list.size simp_thms

declare [[
  φpremise_attribute       [THEN Premise_D] for ‹𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇[eval_aggregate_path] _›  (%φattr_late_normalize),
  φpremise_attribute once? [useful]         for ‹𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇[eval_aggregate_path] _›  (%φattr) (*TODO: use EIF instead of this?*)
]]


subsection ‹Index to Fields of Structures›

definition ‹φType_Mapping T U f g ⟷ (∀v x. v ⊨ (x ⦂ T) ⟶ g v ⊨ (f x ⦂ U))›

definition φAggregate_Getter :: ‹aggregate_path ⇒ (VAL,'a) φ ⇒ (VAL,'b) φ ⇒ ('a ⇒ 'b) ⇒ bool›
  where ‹φAggregate_Getter idx T U g ⟷ φType_Mapping T U g (index_value idx) ›

definition φAggregate_Mapper :: ‹aggregate_path ⇒ (VAL,'a) φ ⇒ (VAL,'a2) φ ⇒ (VAL,'b) φ ⇒ (VAL,'b2) φ ⇒ (('b ⇒ 'b2) ⇒ 'a ⇒ 'a2) ⇒ bool›
  where ‹φAggregate_Mapper idx T T' U U' f
    ⟷ (∀g g'. φType_Mapping U U' g' g ⟶ φType_Mapping T T' (f g') (index_mod_value idx g)) ›

definition φAggregate_Constructor_Synth :: ‹(VAL list ⇒ VAL) ⇒ VAL list BI ⇒ TY ⇒ VAL BI ⇒ bool›
  where ‹φAggregate_Constructor_Synth constructor Args TY Spec
    ⟷ (∀args. args ⊨ Args ⟶ constructor args ⊨ Spec ∧ constructor args ∈ Well_Type TY)›

definition φAggregate_Constructor :: ‹(VAL list ⇒ VAL) ⇒ VAL φarg list ⇒ TY ⇒ VAL BI ⇒ bool›
  where ‹φAggregate_Constructor constructor args TY Spec
    ⟷ constructor (map φarg.dest args) ⊨ Spec ∧ constructor (map φarg.dest args) ∈ Well_Type TY›

consts 𝒜ctr_arg :: ‹symbol + nat ⇒ action›

declare [[φreason_default_pattern
    ‹φAggregate_Getter ?idx ?T _ _ › ⇒ ‹φAggregate_Getter ?idx ?T _ _ › (100)
and ‹φAggregate_Mapper ?idx ?T _ _ _ _ › ⇒ ‹φAggregate_Mapper ?idx ?T _ _ _ _ › (100)
and ‹φAggregate_Constructor_Synth _ _ _ ?T› ⇒ ‹φAggregate_Constructor_Synth _ _ _ ?T› (100)
and ‹φAggregate_Constructor ?ctor ?args _ _› ⇒ ‹φAggregate_Constructor ?ctor ?args _ _› (100),


    φpremise_attribute once? [φreason? %local] for ‹φAggregate_Getter _ _ _ _›       (%φattr),
    φpremise_attribute once? [φreason? %local] for ‹φAggregate_Mapper _ _ _ _ _ _›   (%φattr),
    φpremise_attribute once? [φreason? %local] for ‹φAggregate_Constructor _ _ _ _›  (%φattr)
]]

φreasoner_group aggregate_access_all = (100, [1, 2000]) for (‹φAggregate_Getter idx T U g›,
                                                         ‹φAggregate_Mapper idx T T' U U' f›)
      ‹Rules lifting semantic access of aggregate structures onto abstract domain›
  and aggregate_access = (1010, [1000,1030]) in aggregate_access_all
      ‹cutting rules›

(*
lemma [φreason 1]:
  ‹φAggregate_Getter [] T T id›
  unfolding φAggregate_Getter_def φType_Mapping_def
  by simp
*)

lemma φAggregate_Getter_Nil[φreason %aggregate_access]:
  ‹φAggregate_Getter [] T T id›
  unfolding φAggregate_Getter_def φType_Mapping_def
  by simp

(*
lemma [φreason 1]:
  ‹φAggregate_Mapper [] T T' T T' id›
  unfolding φAggregate_Mapper_def φType_Mapping_def
  by simp
*)

lemma [φreason %aggregate_access]:
  ‹φAggregate_Mapper [] T T' T T' id›
  unfolding φAggregate_Mapper_def φType_Mapping_def
  by simp


subsection ‹Is Aggregate›

definition Is_Aggregate :: ‹('c,'a) φ ⇒ bool›
  where ‹Is_Aggregate T ⟷ True›

φreasoner_group is_aggregate_all = (1000, [1, 2000]) for ‹Is_Aggregate T›
      ‹checking whether the given φtype specifies an aggregate›
  and is_aggregate = (1000, [1000, 1030]) in is_aggregate_all
      ‹cutting rules›

φproperty_deriver Is_Aggregate 555 for (‹Is_Aggregate _›)
  = ‹Phi_Type_Derivers.meta_Synt_Deriver
      ("Is_Aggregate", @{lemma' ‹Is_Aggregate T› by (simp add: Is_Aggregate_def)},
       SOME @{reasoner_group %is_aggregate})›

lemma [φreason %is_aggregate]:
  ‹ Is_Aggregate T
⟹ Is_Aggregate U
⟹ Is_Aggregate (T ∗ U)›
  unfolding Is_Aggregate_def ..

(*
subsection ‹IDE-Interfaces›

term ParamTag

definition Index_Param_Tag :: ‹aggregate_path ⇒ bool› ("𝗂𝗇𝖽𝖾𝗑 𝗉𝖺𝗋𝖺𝗆 _" [1000] 26)
  where "𝗂𝗇𝖽𝖾𝗑 𝗉𝖺𝗋𝖺𝗆 x ≡ True"

lemma Index_Param_Tag_Swap:
  ‹ 𝗉𝖺𝗋𝖺𝗆 P ⟹ 𝗂𝗇𝖽𝖾𝗑 𝗉𝖺𝗋𝖺𝗆 P ›
  unfolding Index_Param_Tag_def ..

ML_file ‹syntax/index_param.ML›

φlang_parser set_index_param 5000 (premises ‹𝗂𝗇𝖽𝖾𝗑 𝗉𝖺𝗋𝖺𝗆 _›) ‹fn (ctxt,sequent) =>
  Scan.pass (Context.Proof ctxt) Synt_Index_Param.index_term_parser >> (fn term => fn _ =>
      Phi_Sys.set_param term (ctxt, @{thm Index_Param_Tag_Swap} RS sequent))›
*)

subsection ‹Size Less or Equal›

definition Size_LEQ :: ‹TY ⇒ TY ⇒ bool› where ‹Size_LEQ _ _ = True›

φreasoner_ML Size_LEQ %cutting (‹Size_LEQ _ _›) = ‹
  fn (_, (ctxt,sequent)) => let
       val rule = @{lemma ‹Size_LEQ A B› by (simp add: Size_LEQ_def)}
       val (bvtys, \<^Const>‹Trueprop› $ (\<^Const>‹Size_LEQ› $ A $ B))
            = Phi_Help.strip_meta_hhf_bvtys (Phi_Help.leading_antecedent' sequent)
    in if Ag_Semantics.size bvtys A <= Ag_Semantics.size bvtys B
       then Seq.single (ctxt, rule RS' (ctxt, sequent))
       else Seq.empty
   end›

hide_const (open) Size_LEQ

section ‹First-level Abstraction of Instructions›

lemma op_get_aggregate:
  ‹ Is_Aggregate T
⟹ Semantic_Type' (x ⦂ T) TY
⟹ parse_eleidx_input_least1 TY input_index sem_idx spec_idx reject
⟹ φAggregate_Getter spec_idx T U f
⟹ report_unprocessed_element_index reject ℰℐℋ𝒪𝒪𝒦_none
⟹ 𝗉𝗋𝗈𝖼 op_get_aggregate sem_idx TY rv ⦃ x ⦂ 𝗏𝖺𝗅[rv] T ⟼ f x ⦂ 𝗏𝖺𝗅 U ⦄›
  unfolding op_get_aggregate_def Semantic_Type'_def subset_iff φAggregate_Getter_def
            parse_eleidx_input_def
            parse_eleidx_input_least1_def
  by (cases rv; simp, rule, simp, rule, simp add: φType_Mapping_def)

lemma "_op_set_aggregate_":
  ‹ Semantic_Type' (x ⦂ T) TY
⟹ parse_eleidx_input_least1 TY input_index sem_idx idx reject
⟹ Semantic_Type' (y ⦂ U) TY⇩U
⟹ is_valid_index_of idx TY TY⇩U'
⟹ Premise eval_aggregate_path (TY⇩U' = TY⇩U ∨ allow_assigning_different_typ TY idx)
⟹ φAggregate_Mapper idx T T' U' U f
⟹ report_unprocessed_element_index reject ℰℐℋ𝒪𝒪𝒦_none
⟹ 𝗉𝗋𝗈𝖼 op_set_aggregate TY TY⇩U sem_idx (rv❙,ru)
      ⦃ x ⦂ 𝗏𝖺𝗅[rv] T❟ y ⦂ 𝗏𝖺𝗅[ru] U ⟼ λret. f (λ_. y) x ⦂ 𝗏𝖺𝗅[ret] T'
        𝗌𝗎𝖻𝗃 (TY⇩U' = TY⇩U ⟶ φarg.dest ret ∈ Well_Type TY) ⦄›
  unfolding op_set_aggregate_def Semantic_Type'_def subset_iff φAggregate_Mapper_def Premise_def
            parse_eleidx_input_def is_valid_index_of_def
            parse_eleidx_input_least1_def
  by (cases rv; cases ru; simp, rule, rule, simp, rule, simp,
      rule φM_Success_P[where X=1, simplified], simp add: φType_Mapping_def,
      simp add: index_mod_value_welltyp)

lemma op_set_aggregate:
  ‹ Is_Aggregate T
⟹ Semantic_Type' (x ⦂ T) TY
⟹ parse_eleidx_input_least1 TY input_index sem_idx idx reject
⟹ Semantic_Type' (y ⦂ U) TY2
⟹ is_valid_index_of idx TY TY2'
⟹ Premise eval_aggregate_path (TY2' = TY2 ∨ allow_assigning_different_typ TY idx)
⟹ φAggregate_Mapper idx T T' U' U f
⟹ report_unprocessed_element_index reject ℰℐℋ𝒪𝒪𝒦_none
⟹ 𝗉𝗋𝗈𝖼 op_set_aggregate TY TY2 sem_idx (rv❙, ru) ⦃ x ⦂ 𝗏𝖺𝗅[rv] T❟ y ⦂ 𝗏𝖺𝗅[ru] U ⟼ f (λ_. y) x ⦂ 𝗏𝖺𝗅 T' ⦄›
  by ((rule φCONSEQ[OF "_op_set_aggregate_" view_shift_refl view_shift_by_implication view_shift_refl]; simp?),
      simp add: Transformation_def, blast)

hide_fact "_op_set_aggregate_"

proc op_construct_aggregate:
  input  ‹Void›
  requires C[unfolded φAggregate_Constructor_def, useful]:
            ‹φAggregate_Constructor constructor args TY (x ⦂ T)›
  output ‹x ⦂ 𝗏𝖺𝗅 T›
  ❴
    semantic_assert ‹constructor (map φarg.dest args) ∈ Well_Type TY›
    semantic_return ‹constructor (map φarg.dest args) ⊨ (x ⦂ T)›
  ❵ .


proc synthesis_construct_aggregate:
  requires [unfolded φAggregate_Constructor_def, useful]:
           ‹φAggregate_Constructor_Synth constructor (y ⦂ U) TY (x ⦂ T)›
       and C: ‹𝗉𝗋𝗈𝖼 C ⦃ R⇩0 ⟼ λret. y ⦂ 𝗏𝖺𝗅𝗌[ret] U 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R⇩1 ⦄ @tag synthesis›
  input  ‹R⇩0›
  output ‹x ⦂ 𝗏𝖺𝗅 T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R⇩1›
  @tag synthesis
  ❴
    C semantic_local_values_nochk
    semantic_assert ‹constructor (φarg.dest 𝗏0) ∈ Well_Type TY›
    semantic_return ‹constructor (φarg.dest 𝗏0) ⊨ (x ⦂ T)›
  ❵ .

φreasoner_group φsynthesis_ag = (%φsynthesis_cut, [%φsynthesis_cut, %φsynthesis_cut+300])
  ‹synthesis for aggregate structures›



section ‹Syntax Base›

subsection ‹Structure and Tuple›

nonterminal "φ_tuple_args_" and "φ_tuple_arg_"

consts φ_Empty_Tuple_sugar :: ‹(VAL, 'any) φ› ("⦃ ⦄") ― ‹A syntax sugar to be overloaded›

syntax "_φTuple" :: ‹φ_tuple_args_ ⇒ logic› ("⦃ _ ⦄")
       "_φtuple_arg"  :: "φ_tuple_arg_ ⇒ φ_tuple_args_" ("_")
       "_φtuple_args" :: "φ_tuple_arg_ ⇒ φ_tuple_args_ ⇒ φ_tuple_args_" ("_,/ _")

translations
  "_φTuple (_φtuple_args y z)" ⇌ "CONST φProd (_φTuple (_φtuple_arg y)) (_φTuple z)"

ML ‹fun strip_phi_tuple_args (Const(\<^syntax_const>‹_φtuple_args›, _) $ x $ L)
          = x :: strip_phi_tuple_args L
      | strip_phi_tuple_args (Const(\<^syntax_const>‹_φtuple_arg›, _) $ x) = [x]
      | strip_phi_tuple_args _ = error "Bad Syntax"›


subsection ‹Access to Element Field›

consts access_to_ele_synt :: ‹'a ⇒ 'b ⇒ 'c›
    ― ‹A syntax sugar to be overloaded›
syntax "_access_to_ele_synt_" :: ‹logic ⇒ φ_ag_idx_ ⇒ logic› (infixl "‣" 55)

parse_translation ‹[
  (\<^syntax_const>‹_access_to_ele_synt_›, fn ctxt => fn [a,x] =>
      Const(\<^const_syntax>‹access_to_ele_synt›, dummyT) $ a $ Phi_Aggregate_Syntax.parse_index x)
]›

print_translation ‹[
  (\<^const_syntax>‹access_to_ele_synt›, fn ctxt => fn [a,x] =>
      Const(\<^syntax_const>‹_access_to_ele_synt_›, dummyT) $ a $ Phi_Aggregate_Syntax.print_index x )
]›
 
text ‹We can use \<^term>‹p ‣ field› to access the address of the element named ‹field› in the
  object pointed by ‹p›.
  We may also use \<^term>‹p ‣ 2› to access the address of the 2nd element.
  Use \<^term>‹p ‣ LOGIC_IDX(var)› to access the element ‹var› which is a logical variable›



section ‹IDE Interface›

(* declare_φlang_operator infix 40 := *)

φoverloads "‣" and ":="

declare op_get_aggregate[φoverload "‣"]
        op_set_aggregate[φoverload ":="]

φreasoner_group φparser_lbrack = (500, [500,500]) ‹›
  and φparser_rbrack = (500,[500,500]) ‹›

ML_file ‹library/generic_element_access.ML›

φlang_parser aggregate_getter_setter (%φparser_lbrack, %φlang_top) ["["] (‹PROP _›)
‹ fn s => Parse.position \<^keyword>‹[› >> (fn (_, pos) => fn cfg =>
    Generic_Element_Access.open_bracket_opr pos cfg s) ›

φlang_parser aggregate_getter_end (%φparser_rbrack, %φlang_top) ["]"] (‹PROP _›)
‹ fn opr_ctxt => Parse.position \<^keyword>‹]› >> (fn (_, pos) => fn cfg => (
    Generic_Element_Access.close_bracket pos cfg opr_ctxt
)) ›

φlang_parser construct_aggregate (%φparser_lbrack, %φlang_top) ["⦃"] (‹PROP _›)
‹ fn s => Parse.position \<^keyword>‹⦃› -- Scan.option (Parse.short_ident --| \<^keyword>‹:›)
>> (fn ((_, pos), arg_name) => fn cfg =>
    Generic_Element_Access.gen_constructor "" (("⦃",pos), (arg_name, pos)) cfg s) ›

φlang_parser construct_aggregate_end (%φparser_rbrack, %φlang_top) ["⦄"] (‹PROP _›)
‹ fn opr_ctxt => Parse.position \<^keyword>‹⦄› >> (fn (_, pos) => fn cfg => (
    Phi_Opr_Stack.check_meta_apply_balance "⦃" pos (#1 (#1 opr_ctxt)) ;
    Phi_Opr_Stack.close_parenthesis (cfg, NONE, false) opr_ctxt
)) ›

φlang_parser triangle_operator (%φparser_unique, %φlang_top) ["‣"] (‹PROP _›)
‹ fn opr_ctxt => Parse.position \<^keyword>‹‣› >> (fn (_, pos) => fn cfg => (
  Phi_Opr_Stack.push_meta_operator cfg
            (Generic_Element_Access.mk_dot_opr pos (#1 (#1 opr_ctxt))) opr_ctxt
)) ›

text ‹We differentiate ‹←› and ‹:=›.
  ‹←› is used to update the value of a local variable.
  ‹:=› is used to change the value of a memory object.
  Without this differentiation, ambiguity occurs when we have a local variable of a pointer
  pointing to a memory object which also stores a pointer, and an assignment can ambiguously refer
  to updating the variable or writing to the memory object.
›

ML ‹
fun dot_opr_chk_left_precedence prio pos oprs =
  let open Phi_Opr_Stack
      fun prec_of first (Meta_Opr (_,_,("$",_),_,_,_,_) :: L) =
            let val p = precedence_of L
             in if p >= @{priority %φlang_dot_opr}
                then prec_of false L
                else if p < prio
                then if first
                  then @{priority loose %φlang_push_val+1}
                  else @{priority loose %φlang_dot_opr+1}
                else prio
            end
        | prec_of first [] =
            if first
            then @{priority loose %φlang_push_val+1}
            else @{priority loose %φlang_dot_opr+1}
        | prec_of _ (Meta_Opr (_,_,("‣",_),_,_,_,_) :: L) = prec_of false L
        | prec_of _ (Meta_Opr (pr,_,_,_,_,_,_) :: L) =
            if pr > @{priority %φlang_app}
            then prec_of false L
            else Generic_Element_Access.err_assignment pos
        | prec_of _ (Opr (pr,_,_,_,_,_) :: L) =
            if pr > @{priority %φlang_app}
            then prec_of false L
            else Generic_Element_Access.err_assignment pos
        | prec_of _ _ = prio
   in prec_of true oprs
  end
›

φlang_parser assignment_opr (%φparser_left_arrow, %φlang_top) ["←"] (‹PROP _›)
‹ fn opr_ctxt => Parse.position \<^keyword>‹←› >> (fn (_, pos) => fn cfg => (
let open Phi_Opr_Stack
    val prio = dot_opr_chk_left_precedence @{priority %φlang_assignment} pos (#1 (#1 opr_ctxt))
 in push_meta_operator cfg ((prio, @{priority %φlang_assignment}, (VAR_ARITY_IN_OPSTACK,1)), ("←", pos), NONE,
                       Generic_Element_Access.dot_triangle_assignment) opr_ctxt
end
)) ›

φlang_parser update_opr (%φparser_left_arrow, %φlang_top) [":="] (‹PROP _›)
‹ fn opr_ctxt => Parse.position \<^keyword>‹:=› >> (fn (_, pos) => fn cfg => (
let open Phi_Opr_Stack
    val prio = dot_opr_chk_left_precedence @{priority %φlang_update_opr} pos (#1 (#1 opr_ctxt))
 in push_meta_operator cfg ((prio, @{priority %φlang_update_opr}, (VAR_ARITY_IN_OPSTACK,1)), (":=", pos), NONE,
                       Generic_Element_Access.dot_triangle_update_opr) opr_ctxt
end
)) ›

φlang_parser literal_symbol_in_eleidx (%φparser_app-250, %φlang_push_val) [""]
                                      (‹CurrentConstruction programming_mode ?blk ?H ?S›) ‹
fn (oprs,(ctxt,sequent)) =>
  case #1 oprs
    of Phi_Opr_Stack.Meta_Opr (_,_,("‣",_),_,_,_,_) :: _ => (
        Parse.name >> (fn s => fn _ =>
        (oprs, (ctxt, #transformation_rule Phi_Working_Mode.programming
                  OF [sequent, Thm.instantiate
                                  (TVars.empty, Vars.make [((("s",0),\<^typ>‹symbol›),
                                                           Thm.cterm_of ctxt (Phi_Tool_Symbol.mk_symbol s))])
                                  @{thm "_intro_symbol_"}]))))
     | _ => Scan.fail
›



end