Theory CupCake_Env

section ‹CupCake environments›

theory CupCake_Env
imports "../Utils/CakeML_Utils"
begin

fun cake_no_abs :: "v ⇒ bool" where
"cake_no_abs (Conv _ vs) ⟷ list_all cake_no_abs vs" |
"cake_no_abs _ ⟷ False"

fun is_cupcake_pat :: "Ast.pat ⇒ bool" where
"is_cupcake_pat (Ast.Pvar _) ⟷ True" |
"is_cupcake_pat (Ast.Pcon (Some (Short _)) xs) ⟷ list_all is_cupcake_pat xs" |
"is_cupcake_pat _ ⟷ False"

fun is_cupcake_exp :: "exp ⇒ bool" where
"is_cupcake_exp (Ast.Var (Short _)) ⟷ True" |
"is_cupcake_exp (Ast.App oper es) ⟷ oper = Ast.Opapp ∧ list_all is_cupcake_exp es" |
"is_cupcake_exp (Ast.Con (Some (Short _)) es) ⟷ list_all is_cupcake_exp es" |
"is_cupcake_exp (Ast.Fun _ e) ⟷ is_cupcake_exp e" |
"is_cupcake_exp (Ast.Mat e cs) ⟷ is_cupcake_exp e ∧ list_all (λ(p, e). is_cupcake_pat p ∧ is_cupcake_exp e) cs ∧ cake_linear_clauses cs" |
"is_cupcake_exp _ ⟷ False"

abbreviation cupcake_clauses :: "(Ast.pat × exp) list ⇒ bool" where
"cupcake_clauses ≡ list_all (λ(p, e). is_cupcake_pat p ∧ is_cupcake_exp e)"

fun cupcake_c_ns :: "c_ns ⇒ bool" where
"cupcake_c_ns (Bind cs mods) ⟷
  mods = [] ∧ list_all (λ(_, _, tid). case tid of TypeId (Short _) ⇒ True | _ ⇒ False) cs"

locale cakeml_static_env =
  fixes static_cenv :: c_ns
  assumes static_cenv: "cupcake_c_ns static_cenv"
begin

definition empty_sem_env :: "v sem_env" where
"empty_sem_env = ⦇ sem_env.v = nsEmpty, sem_env.c = static_cenv ⦈"

lemma v_of_empty_sem_env[simp]: "sem_env.v empty_sem_env = nsEmpty"
unfolding empty_sem_env_def by simp

lemma c_of_empty_sem_env[simp]: "c empty_sem_env = static_cenv"
unfolding empty_sem_env_def by simp

fun is_cupcake_value :: "SemanticPrimitives.v ⇒ bool"
and is_cupcake_all_env :: "all_env ⇒ bool" where
"is_cupcake_value (Conv (Some (_, TypeId (Short _))) vs) ⟷ list_all is_cupcake_value vs" |
"is_cupcake_value (Closure env _ e) ⟷ is_cupcake_exp e ∧ is_cupcake_all_env env" |
"is_cupcake_value (Recclosure env es _) ⟷ list_all (λ(_, _, e). is_cupcake_exp e) es ∧ is_cupcake_all_env env" |
"is_cupcake_value _ ⟷ False" |
"is_cupcake_all_env ⦇ sem_env.v = Bind v0 [], sem_env.c = c0 ⦈ ⟷ c0 = static_cenv ∧ list_all (is_cupcake_value ∘ snd) v0" |
"is_cupcake_all_env _ ⟷ False"

lemma is_cupcake_all_envE:
  assumes "is_cupcake_all_env env"
  obtains v c where "env = ⦇ sem_env.v = Bind v [], sem_env.c = c ⦈" "c = static_cenv" "list_all (is_cupcake_value ∘ snd) v"
using assms
by (auto elim!: is_cupcake_all_env.elims)

fun is_cupcake_ns :: "v_ns ⇒ bool" where
"is_cupcake_ns (Bind v0 []) ⟷ list_all (is_cupcake_value ∘ snd) v0" |
"is_cupcake_ns _ ⟷ False"

lemma is_cupcake_nsE:
  assumes "is_cupcake_ns ns"
  obtains v where "ns = Bind v []" "list_all (is_cupcake_value ∘ snd) v"
using assms by (rule is_cupcake_ns.elims)

lemma is_cupcake_all_envD:
  assumes "is_cupcake_all_env env"
  shows "is_cupcake_ns (sem_env.v env)" "cupcake_c_ns (c env)"
using assms static_cenv by (auto elim!: is_cupcake_all_envE)

lemma is_cupcake_all_envI:
  assumes "is_cupcake_ns (sem_env.v env)" "sem_env.c env = static_cenv"
  shows "is_cupcake_all_env env"
using assms static_cenv
apply (cases env)
apply simp
subgoal for v c
  apply (cases v)
  apply simp
  subgoal for x1 x2
    by (cases x2) auto
  done
done

end

end