Theory Matching

chapter "Matching adaptation"

theory Matching
imports Semantic_Extras
begin

context begin

qualified fun fold2 where
"fold2 f err [] [] init = init" |
"fold2 f err (x # xs) (y # ys) init = fold2 f err xs ys (f x y init)" |
"fold2 _ err _  _ _ = err"

qualified lemma fold2_cong[fundef_cong]:
  assumes "init1 = init2" "err1 = err2" "xs1 = xs2" "ys1 = ys2"
  assumes "⋀init x y. x ∈ set xs1 ⟹ y ∈ set ys1 ⟹ f x y init = g x y init"
  shows "fold2 f err1 xs1 ys1 init1 = fold2 g err2 xs2 ys2 init2"
using assms
by (induction f err1 xs1 ys1 init1 arbitrary: init2 xs2 ys2 rule: fold2.induct) auto

fun pmatch_single :: "((string),(string),(nat*tid_or_exn))namespace ⇒((v)store_v)list ⇒ pat ⇒ v ⇒(string*v)list ⇒((string*v)list)match_result " where
"pmatch_single envC s Pany v' env = ( Match env )" |
"pmatch_single envC s (Pvar x) v' env = ( Match ((x,v')# env))" |
"pmatch_single envC s (Plit l) (Litv l') env = (
  if l = l' then
    Match env
  else if lit_same_type l l' then
    No_match
  else
    Match_type_error )" |
"pmatch_single envC s (Pcon (Some n) ps) (Conv (Some (n', t')) vs) env =
  (case  nsLookup envC n of
      Some (l, t1) =>
        if same_tid t1 t' ∧ (List.length ps = l) then
          if same_ctor (id_to_n n, t1) (n',t') then
            fold2 (λp v m. case m of
               Match env ⇒ pmatch_single envC s p v env 
            | m ⇒ m) Match_type_error ps vs (Match env)
          else
            No_match
        else
          Match_type_error
    | _ => Match_type_error
  )" |
"pmatch_single envC s (Pcon None ps) (Conv None vs) env = (
  if List.length ps = List.length vs then
    fold2 (λp v m. case m of
       Match env ⇒ pmatch_single envC s p v env 
        | m ⇒ m)
         Match_type_error ps vs (Match env)
  else
    Match_type_error )" |
"pmatch_single envC s (Pref p) (Loc lnum) env =
  (case  store_lookup lnum s of
      Some (Refv v2) => pmatch_single envC s p v2 env
    | Some _ => Match_type_error
    | None => Match_type_error
  )" |
"pmatch_single envC s (Ptannot p t1) v2 env = pmatch_single envC s p v2 env" |
"pmatch_single envC _ _ _ env = Match_type_error"

private lemma pmatch_list_length_neq:
  "length vs ≠ length ps ⟹ fold2(λp v m. case m of
       Match env ⇒ pmatch_single cenv s p v env 
        | m ⇒ m) Match_type_error ps vs m = Match_type_error"
  by (induction ps vs arbitrary:m rule:List.list_induct2') auto

private lemma pmatch_list_nomatch:
  "length vs = length ps ⟹ fold2(λp v m. case m of
       Match env ⇒ pmatch_single cenv s p v env 
        | m ⇒ m) Match_type_error ps vs No_match = No_match"
  by (induction ps vs  rule:List.list_induct2') auto

private lemma pmatch_list_typerr:
  "length vs = length ps ⟹ fold2(λp v m. case m of
       Match env ⇒ pmatch_single cenv s p v env 
        | m ⇒ m) Match_type_error ps vs Match_type_error = Match_type_error"
  by (induction ps vs  rule:List.list_induct2') auto

private lemma pmatch_single_eq0:
  "length ps = length vs ⟹ pmatch_list cenv s ps vs env = fold2(λp v m. case m of
       Match env ⇒ pmatch_single cenv s p v env 
        | m ⇒ m) Match_type_error ps vs (Match env)"
  "pmatch cenv s p v0 env = pmatch_single cenv s p v0 env"
proof (induction rule: pmatch_list_pmatch.induct)
  case (4 envC s n ps n' t' vs env)
  then show ?case
    by (auto split:option.splits match_result.splits dest!:pmatch_list_length_neq[where m = "Match env" and cenv = envC and s = s])
qed (auto split:option.splits match_result.splits store_v.splits simp:pmatch_list_nomatch pmatch_list_typerr)

lemma pmatch_single_equiv: "pmatch = pmatch_single"
by (rule ext)+ (simp add: pmatch_single_eq0)

end

export_code pmatch_single checking SML

end