Theory FTAnnotatedListImpl

section ‹\isaheader{Implementation of Annotated Lists by 2-3 Finger Trees}›
theory FTAnnotatedListImpl
imports 
  "Finger-Trees.FingerTree" 
  "../tools/Locale_Code"
  "../tools/Record_Intf"
  "../spec/AnnotatedListSpec"
begin

(*@impl AnnotatedList
  @type ('a,'b::monoid_add) ft
  @abbrv ft
  Annotated lists implemented by 2-3 finger trees.
*)

type_synonym ('a,'b) ft = "('a,'b) FingerTree"
subsection "Definitions"

definition ft_α where
  "ft_α ≡ FingerTree.toList"
abbreviation (input) ft_invar :: "('a,'b) FingerTree ⇒ bool" where 
  "ft_invar ≡ λ_. True"
definition ft_empty where
  "ft_empty ≡ λ_::unit. FingerTree.empty"
definition ft_isEmpty where
  "ft_isEmpty ≡ FingerTree.isEmpty"
definition ft_count where
  "ft_count ≡ FingerTree.count"
definition ft_consl where
  "ft_consl e a s = FingerTree.lcons (e,a) s"
definition ft_consr where
  "ft_consr s e a = FingerTree.rcons s (e,a)"
definition ft_head where
  "ft_head ≡ FingerTree.head"
definition ft_tail where
  "ft_tail ≡ FingerTree.tail"
definition ft_headR where
  "ft_headR ≡ FingerTree.headR"
definition ft_tailR where
  "ft_tailR ≡ FingerTree.tailR"
definition ft_foldl where
  "ft_foldl ≡ FingerTree.foldl"
definition ft_foldr where
  "ft_foldr ≡ FingerTree.foldr"
definition ft_app where
  "ft_app ≡ FingerTree.app"
definition ft_annot where
  "ft_annot ≡ FingerTree.annot"
definition ft_splits where 
  "ft_splits ≡ FingerTree.splitTree"

lemmas ft_defs =
  ft_α_def
  ft_empty_def
  ft_isEmpty_def
  ft_count_def
  ft_consl_def
  ft_consr_def
  ft_head_def
  ft_tail_def
  ft_headR_def
  ft_tailR_def
  ft_foldl_def
  ft_foldr_def
  ft_app_def
  ft_annot_def
  ft_splits_def

lemma ft_empty_impl: "al_empty ft_α ft_invar ft_empty"
  apply unfold_locales
  apply (auto simp add: ft_defs FingerTree.empty_correct)
  done

lemma ft_consl_impl: "al_consl ft_α ft_invar ft_consl"
  apply unfold_locales
  apply (auto simp add: ft_defs FingerTree.lcons_correct)
done

lemma ft_consr_impl: "al_consr ft_α ft_invar ft_consr"
  apply unfold_locales
  apply (auto simp add: ft_defs FingerTree.rcons_correct)
done

lemma ft_isEmpty_impl: "al_isEmpty ft_α ft_invar ft_isEmpty" 
  apply unfold_locales
  apply (auto simp add: ft_defs FingerTree.isEmpty_correct FingerTree.empty_correct)
  done

lemma ft_count_impl: "al_count ft_α ft_invar ft_count"
  apply unfold_locales
  apply (auto simp add: ft_defs FingerTree.count_correct)
  done

lemma ft_head_impl: "al_head ft_α ft_invar ft_head"
    apply unfold_locales
    apply (auto simp add: ft_defs FingerTree.head_correct FingerTree.empty_correct)
done

lemma ft_tail_impl: "al_tail ft_α ft_invar ft_tail"
    apply unfold_locales
    apply (auto simp add: ft_defs FingerTree.tail_correct FingerTree.empty_correct)
done

lemma ft_headR_impl: "al_headR ft_α ft_invar ft_headR"
    apply unfold_locales
    apply (auto simp add: ft_defs FingerTree.headR_correct FingerTree.empty_correct)
done

lemma ft_tailR_impl: "al_tailR ft_α ft_invar ft_tailR"
    apply unfold_locales
    apply (auto simp add: ft_defs FingerTree.tailR_correct FingerTree.empty_correct)
    done

lemma ft_foldl_impl: "al_foldl ft_α ft_invar ft_foldl"
  apply unfold_locales
  apply (auto simp add: ft_defs FingerTree.foldl_correct)
  done 

lemma ft_foldr_impl: "al_foldr ft_α ft_invar ft_foldr"
  apply unfold_locales
  apply (auto simp add: ft_defs FingerTree.foldr_correct)
  done 

lemma ft_foldl_cunfold[code_unfold]:
  "List.foldl f σ (ft_α t) = ft_foldl f σ t"
  apply (auto simp add: ft_defs FingerTree.foldl_correct)
  done 

lemma ft_foldr_cunfold[code_unfold]:
  "List.foldr f (ft_α t) σ = ft_foldr f t σ"
  apply (auto simp add: ft_defs FingerTree.foldr_correct)
  done 

lemma ft_app_impl: "al_app ft_α ft_invar ft_app"
  apply unfold_locales
  apply (auto simp add: ft_defs FingerTree.app_correct)
  done

lemma ft_annot_impl: "al_annot ft_α ft_invar ft_annot"
  apply unfold_locales 
  apply (auto simp add: ft_defs FingerTree.annot_correct)
  done

lemma ft_splits_impl: "al_splits ft_α ft_invar ft_splits"
  apply unfold_locales
  apply (unfold ft_defs)
  apply (simp only: FingerTree.annot_correct[symmetric])
  apply (frule (3) FingerTree.splitTree_correct(1))
  apply (frule (3) FingerTree.splitTree_correct(2))
  apply (frule (3) FingerTree.splitTree_correct(3))
  apply (simp only: FingerTree.annot_correct[symmetric])
  apply simp
  done

subsubsection "Record Based Implementation"

definition [icf_rec_def]: "ft_ops = ⦇
  alist_op_α = ft_α,
  alist_op_invar = ft_invar,
  alist_op_empty = ft_empty,
  alist_op_isEmpty = ft_isEmpty,
  alist_op_count = ft_count,
  alist_op_consl = ft_consl,
  alist_op_consr = ft_consr,
  alist_op_head = ft_head,
  alist_op_tail = ft_tail,
  alist_op_headR = ft_headR,
  alist_op_tailR = ft_tailR,
  alist_op_app = ft_app,
  alist_op_annot = ft_annot,
  alist_op_splits = ft_splits
  ⦈"

setup Locale_Code.open_block
interpretation ft: StdAL ft_ops
  apply (rule StdAL.intro)
  apply (simp_all add: icf_rec_unf)
  apply (rule 
    ft_empty_impl
    ft_consl_impl
    ft_consr_impl
    ft_isEmpty_impl
    ft_count_impl
    ft_head_impl
    ft_tail_impl
    ft_headR_impl
    ft_tailR_impl
    ft_foldl_impl
    ft_foldr_impl
    ft_app_impl
    ft_annot_impl
    ft_splits_impl
  )+
  done
interpretation ft: StdAL_no_invar ft_ops
  by (unfold_locales) (simp add: icf_rec_unf)
setup Locale_Code.close_block

setup ‹ICF_Tools.revert_abbrevs "ft"›


definition "test_codegen ≡ (
  ft.empty,
  ft.isEmpty,
  ft.count,
  ft.consl,
  ft.consr,
  ft.head,
  ft.tail,
  ft.headR,
  ft.tailR,
  ft.app,
  ft.annot,
  ft.splits,
  ft.foldl,
  ft.foldr
)"

export_code test_codegen checking SML

end