Require Import Arith. Require Import Bool. Require Import List. Require Import Natmap. Require Import FMaps. Require Import EqNat. Require Import lj_definitions. Inductive ty_constraint : Set := | in_prog_constr : cl -> ty_constraint | sty_field_rconstr : cl -> f -> ty -> ty_constraint | sty_field_wconstr : ty -> cl -> f -> ty_constraint | sty_meth_constr : cl -> m -> ty -> list ty -> ty_constraint | sty_cl_constr : ty -> ty -> ty_constraint | sty_if_constr : ty -> ty -> ty_constraint | inherited_fields_constr : list f -> cl -> ty_constraint | inherited_methods_constr : list md -> cl -> ty_constraint. Inductive wf_stmt_constr (g : G) : s -> (list ty_constraint) -> Prop := | wf_new_constr : forall (var' : var) (cl' : cl) (ty' : ty), XMap.find (x_var var') g = Some ty' -> wf_stmt_constr g (s_new var' cl') ((sty_cl_constr (ty_def cl') ty') :: nil) | wf_var_assign_constr : forall (var' : var) (x' : x) (ty' ty'' :ty), XMap.find x' g = Some ty' -> XMap.find (x_var var') g = Some ty'' -> wf_stmt_constr g (s_ass var' x') ((sty_cl_constr ty' ty'') :: nil) | wf_field_read_constr : forall (var' : var) (x' : x) (f' : f) (cl' : cl) (ty' :ty), XMap.find x' g = Some (ty_def cl') -> XMap.find (x_var var') g = Some ty' -> wf_stmt_constr g (s_read var' x' f') ((sty_field_rconstr cl' f' ty') :: nil) | wf_field_write_constr : forall (x' y': x) (f' : f) (cl' : cl) (ty' :ty), XMap.find x' g = Some (ty_def cl') -> XMap.find y' g = Some ty' -> wf_stmt_constr g (s_write x' f' y') ((sty_field_wconstr ty' cl' f') :: nil) | wf_mcall_constr : forall (var' : var) (x' : x) (m' : m) (param_list : list x) (cl' : cl) (ty' : ty) (ty_list : list ty), XMap.find x' g = Some (ty_def cl') -> XMap.find (x_var var') g = Some ty' -> (fold_right (fun (y : x) (m: option (list ty)) => match (XMap.find y g), m with Some ty', Some m' => Some (ty' :: m') | _, _ => None end) (Some nil) param_list) = Some ty_list -> wf_stmt_constr g (s_call var' x' m' param_list) ((sty_meth_constr cl' m' ty' ty_list) :: nil) | wf_if_constr : forall (x' y' : x) (ty' ty'' : ty) (s1 s2 : s) (c_list1 c_list2 : list ty_constraint), XMap.find x' g = Some ty' -> XMap.find y' g = Some ty'' -> wf_stmt_constr g s1 c_list1 -> wf_stmt_constr g s2 c_list2 -> wf_stmt_constr g (s_if x' y' s1 s2) (sty_if_constr ty' ty'' :: (c_list1 ++ c_list2)) | wf_block_constr : forall (s_list : list_s) (c_list : list ty_constraint), wf_stmt_list_constr g s_list c_list -> wf_stmt_constr g (s_block s_list) c_list with wf_stmt_list_constr (g : G) : list_s -> (list ty_constraint) -> Prop := | wf_nil_list_constr : wf_stmt_list_constr g Nil_list_s nil | wf_cons_list_constr : forall (stmt : s) (s_list : list_s) (c_list1 c_list2 : list ty_constraint), wf_stmt_constr g stmt c_list1 -> wf_stmt_list_constr g s_list c_list2 -> wf_stmt_list_constr g (Cons_list_s stmt s_list) (c_list1 ++ c_list2). Inductive wf_meth_constr : ty -> md -> list ty_constraint -> Prop := wf_method_constr : forall (ty' ty'' ty''': ty) (m' : m) (vd_list : list vd) (y : x) (s_list : list s) (g : G) (c_list : list ty_constraint), distinct _ (map (fun (vd' : vd) => match vd' with vd_def ty' var' => var' end) vd_list) -> g = (fold_left (fun (m : XMap.t ty) (p : x*ty) => XMap.add (fst p) (snd p) m) ( (map (fun (vd' : vd) => match vd' with vd_def ty' var' => (x_var var', ty') end) vd_list)) (XMap.add x_this ty''' (XMap.empty ty))) -> wf_stmt_list_constr g (make_list_s s_list) c_list -> XMap.find y g = Some ty'' -> wf_meth_constr ty''' (md_def (ms_def ty' m' vd_list) (mb_def s_list y)) ((sty_cl_constr ty'' ty') :: ( (map (fun (vd' : vd) => match vd' with vd_def (ty_def cl') var' => in_prog_constr cl' end) vd_list) ++ c_list)). Inductive wf_meth_list_constr (ty' : ty) : list md -> (list ty_constraint) -> Prop := | wf_meth_nil_constr : wf_meth_list_constr ty' nil nil | wf_meth_cons_constr : forall (md' : md) (mds : list md) (c_list1 c_list2 : list ty_constraint), wf_meth_constr ty' md' c_list1 -> wf_meth_list_constr ty' mds c_list2 -> wf_meth_list_constr ty' (md' :: mds) (c_list1 ++ c_list2). Inductive wf_cld_constr : cld -> list ty_constraint -> Prop := | wf_class_constraint : forall (dcl' dcl'' : dcl) (fds : list fd) (fs : list f) (ms : list m) (mds : list md) (c_list : list ty_constraint), dcl' <> dcl'' -> fs = (map (fun (fd' : fd) => match fd' with fd_def ty' f'=> f' end) fds) -> ms = (map (fun (md' : md) => match md' with md_def (ms_def _ m' _) _=> m' end) mds) -> distinct _ fs -> distinct _ ms -> wf_meth_list_constr (ty_def (cl_dcl dcl')) mds c_list -> wf_cld_constr (cld_def dcl' (cl_dcl dcl'') fds mds) ((in_prog_constr (cl_dcl dcl'')) :: (inherited_fields_constr fs (cl_dcl dcl'')) :: (inherited_methods_constr mds (cl_dcl dcl'')) :: ((map (fun (fd' : fd) => match fd' with fd_def (ty_def cl') _ => in_prog_constr cl' end) fds) ++ c_list)) | wf_class_constraint_obj : forall (dcl' : dcl) (fds : list fd) (fs : list f) (ms : list m) (mds : list md) (c_list : list ty_constraint), fs = (map (fun (fd' : fd) => match fd' with fd_def ty' f'=> f' end) fds) -> ms = (map (fun (md' : md) => match md' with md_def (ms_def _ m' _) _=> m' end) mds) -> distinct _ fs -> distinct _ ms -> wf_meth_list_constr (ty_def (cl_dcl dcl')) mds c_list -> wf_cld_constr (cld_def dcl' cl_object fds mds) ((map (fun (fd' : fd) => match fd' with fd_def (ty_def cl') _ => in_prog_constr cl' end) fds) ++ c_list). Inductive wf_cld_constr_list : P -> list ty_constraint -> Prop := | wf_cld_list_nil : wf_cld_constr_list nil nil | wf_cld_list_cons : forall (cld' : cld) (p : P) (c_list c_list' : list ty_constraint), wf_cld_constr cld' c_list -> wf_cld_constr_list p c_list' -> wf_cld_constr_list (cld' :: p) (c_list ++ c_list'). Inductive wf_prog_constr : P -> list ty_constraint -> Prop := | WF_prog_constr : forall (p : P) (c_list : list ty_constraint), distinct _ (names p) -> wf_cld_constr_list p c_list -> acyclic_hierarchy p -> wf_prog_constr p c_list. Fixpoint in_path (cl_path : list cld) (dcl' : dcl) {struct cl_path}: bool := match cl_path with nil => false | (cld_def dcl'' cl' fds' mds') :: cl'_path => if (eq_nat_dec dcl' dcl'') then true else in_path cl'_path dcl' end. Definition eq_ty (ty1 ty2 : ty) : bool := match ty1, ty2 with ty_def (cl_dcl dcl1), ty_def (cl_dcl dcl2) => if (eq_nat_dec dcl1 dcl2) then true else false | ty_def cl_object, ty_def cl_object => true | _, _ => false end. Definition mty_eq (mty1 mty2 : mty) : bool := match mty1, mty2 with mty_def tys1 ty1, mty_def tys2 ty2 => if eq_ty ty1 ty2 then if (eq_nat_dec (length tys1) (length tys2)) then fold_right (fun (ty' : ty*ty) (b : bool) => eq_ty (fst ty') (snd ty') && b) true (combine tys1 tys2) else false else false end. Definition match_nat (var1 var2 : nat) : bool := if (eq_nat_dec var1 var2) then false else true. Definition not_in_list (var' : nat) (v_list : list nat) : bool := forallb (match_nat var') v_list. Definition sat_constr (p : P) (c : ty_constraint) : bool := match c with | sty_field_rconstr cl' f' (ty_def cl'') => match cl'', (ftype p cl' f') with cl_dcl dcl', Some (ty_def (cl_dcl dcl'')) => in_path (path p (cl_dcl dcl'')) dcl' | cl_object, Some (ty_def (cl_dcl dcl'')) => in_path (path p (cl_dcl dcl'')) dcl'' | cl_object, Some (ty_def cl_object) => true | _, _ => false end | sty_field_wconstr (ty_def cl') cl'' f' => match cl', (ftype p cl'' f') with cl_dcl dcl'', Some (ty_def (cl_dcl dcl')) => in_path (path p (cl_dcl dcl'')) dcl' | cl_dcl dcl'', Some (ty_def cl_object) => in_path (path p (cl_dcl dcl'')) dcl'' | cl_object, Some (ty_def cl_object) => true | _, _ => false end | sty_meth_constr cl' m' (ty_def cl'') ty_list => match (mtype p cl' m'), cl'' with Some (mty_def (ty_list') (ty_def (cl_dcl dcl''))), cl_dcl dcl' => if (eq_nat_dec (length ty_list) (length ty_list')) then (in_path (path p (cl_dcl dcl'')) dcl') && (fold_right (fun (x : ty*ty) (m : bool) => match x with ((ty_def (cl_dcl dcl2)), (ty_def (cl_dcl dcl1))) => (in_path (path p (cl_dcl dcl2)) dcl1) && m | ((ty_def (cl_dcl dcl1)), (ty_def cl_object)) => (in_path (path p (cl_dcl dcl1)) dcl1) && m | ((ty_def cl_object), (ty_def cl_object)) => m | _ => false end) true (combine ty_list ty_list')) else false | Some (mty_def (ty_list') (ty_def (cl_dcl dcl''))), cl_object => if (eq_nat_dec (length ty_list) (length ty_list')) then (in_path (path p (cl_dcl dcl'')) dcl'') && (fold_right (fun (x : ty*ty) (m : bool) => match x with ((ty_def (cl_dcl dcl2)), (ty_def (cl_dcl dcl1))) => (in_path (path p (cl_dcl dcl2)) dcl1) && m | ((ty_def (cl_dcl dcl1)), (ty_def cl_object)) => (in_path (path p (cl_dcl dcl1)) dcl1) && m | ((ty_def cl_object), (ty_def cl_object)) => m | _ => false end) true (combine ty_list ty_list')) else false | Some (mty_def (ty_list') (ty_def cl_object)), cl_object => if (eq_nat_dec (length ty_list) (length ty_list')) then (fold_right (fun (x : ty*ty) (m : bool) => match x with ((ty_def (cl_dcl dcl2)), (ty_def (cl_dcl dcl1))) => (in_path (path p (cl_dcl dcl2)) dcl1) && m | ((ty_def (cl_dcl dcl1)), (ty_def cl_object)) => (in_path (path p (cl_dcl dcl1)) dcl1) && m | ((ty_def cl_object), (ty_def cl_object)) => m | _ => false end) true (combine ty_list ty_list')) else false | _, _ => false end | sty_cl_constr ty1 ty2 => match ty1, ty2 with ty_def cl', ty_def (cl_dcl dcl') => in_path (path p cl') dcl' | ty_def cl_object, ty_def cl_object => true | ty_def (cl_dcl dcl'), ty_def cl_object => in_path (path p (cl_dcl dcl')) dcl' end | sty_if_constr (ty_def cl1) (ty_def cl2) => match cl1, cl2 with cl_dcl dcl1, cl_dcl dcl2 => in_path (path p (cl_dcl dcl1)) dcl2 || in_path (path p (cl_dcl dcl2)) dcl1 | cl_object, cl_dcl dcl2 => in_path (path p (cl_dcl dcl2)) dcl2 | cl_dcl dcl1, cl_object => in_path (path p (cl_dcl dcl1)) dcl1 | cl_object, cl_object => true end | in_prog_constr cl' => match cl' with cl_dcl dcl' => in_path p dcl' | cl_object => true end | inherited_fields_constr fds' cl' => match (list_inter _ fds' (fields p cl') in_nat_list) with nil => true | _ => false end | inherited_methods_constr mds' cl' => let pmds' := methods p cl' in fold_right (fun (md' : md) (b : bool) => match md' with md_def (ms_def ty' m' vd_list ) _ => if (negb (not_in_list m' pmds')) then match (mtype p cl' m') with Some mty' => (mty_eq mty' (mty_def (map (fun (vd' : vd) => match vd' with vd_def ty'' _ => ty'' end) vd_list) ty')) && b | None => false end else true && b end) true mds' end. Fixpoint sat_constr_list (p : P) (c_list : list ty_constraint) : bool := match c_list with constr :: c_list' => sat_constr p constr && sat_constr_list p c_list' | nil => true end. Definition sat_constr_iff_wf := forall (p : P) (c_list : list ty_constraint), (wf_prog_constr p c_list /\ sat_constr_list p c_list = true) <-> wf_prog p. Definition lj_constraint_sound := forall (p : P), wf_prog p <-> (exists c_list, wf_prog_constr p c_list /\ sat_constr_list p c_list = true).