Require Import Arith. Require Import Bool. Require Import List. Require Import Natmap. Require Import FMaps. Require Import EqNat. Require Import lj_definitions. Require Import lj_constraint_definitions. Require Import lj_constraint_infrastructure. Inductive rmb : Set := rmb_def : list s -> list s -> x -> rmb. Inductive rmd : Set := rmd_def : ms -> rmb -> rmd. Inductive rcld : Set := refines_cld_def : dcl -> cl -> list fd -> list md -> list rmd -> rcld. Inductive FD : Set := feature_def : list rcld -> list cld -> FD. Definition FT : Set := list FD. Definition PSpec : Set := list nat. Definition PSel : Set := list FD. Inductive comp_constraint : Set := | introduced_method_constr : ms -> dcl -> nat -> comp_constraint | introduced_class_constr : dcl -> nat -> comp_constraint. Inductive unique_constraint : Set := | unique_fields_constraint : dcl -> fd -> unique_constraint | unique_methods_constraint : dcl -> ms -> unique_constraint. Inductive feature_constraint : Set := feature_constr : nat -> list comp_constraint -> list unique_constraint -> list ty_constraint -> feature_constraint. Coercion cl_dcl : dcl >-> cl. Coercion ty_def : cl >-> ty. Inductive wf_refined_meth_constr : nat -> ty -> rmd -> comp_constraint -> list ty_constraint -> Prop := wf_method_constr : forall (dcl' : dcl) (ty' ty'': ty) (m' : m) (vd_list : list vd) (y : x) (s_list1 s_list2 : list s) (g : G) (c_list1 c_list2 c_list3 : list ty_constraint) (n : nat), 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_def (cl_dcl dcl')) (XMap.empty ty))) -> distinct _ (map (fun vd' : vd => match vd' with | vd_def _ var' => var' end) vd_list) -> c_list3 = map (fun vd' : vd => match vd' with | vd_def (ty_def cl') _ => in_prog_constr cl' end) vd_list -> wf_stmt_list_constr g (make_list_s s_list1) c_list1 -> wf_stmt_list_constr g (make_list_s s_list2) c_list2 -> XMap.find y g = Some ty'' -> wf_refined_meth_constr n dcl' (rmd_def (ms_def ty' m' vd_list) (rmb_def s_list1 s_list2 y)) (introduced_method_constr (ms_def ty' m' vd_list) dcl' n) ((sty_cl_constr ty'' ty') :: (c_list3 ++ c_list1 ++ c_list2)). Inductive wf_refined_meth_list_constr (n : nat) (ty' : ty) : list rmd -> list comp_constraint -> list ty_constraint -> Prop := | wf_refined_meth_nil_constr : wf_refined_meth_list_constr n ty' nil nil nil | wf_refined_meth_cons_constr : forall (rmd' : rmd) (rmds : list rmd) (cc : comp_constraint) (cc_list : list comp_constraint) (tyc_list1 tyc_list2 : list ty_constraint), wf_refined_meth_constr n ty' rmd' cc tyc_list1 -> wf_refined_meth_list_constr n ty' rmds cc_list tyc_list2 -> wf_refined_meth_list_constr n ty' (rmd' :: rmds) (cc :: cc_list) (tyc_list1 ++ tyc_list2). Inductive wf_cld_constr : cld -> list unique_constraint -> list ty_constraint -> Prop := | wf_class_constraint : forall (dcl' dcl'' : dcl) (fds : list fd) (fs : list f) (ms : list m) (mds : list md) (tyc_list : list ty_constraint) (uc_list1 uc_list2 : list unique_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 tyc_list -> uc_list1 = fold_right (fun (fd' : fd) (m : list unique_constraint) => unique_fields_constraint dcl' fd' :: m) (nil : list unique_constraint) fds -> uc_list2 = fold_right (fun (md' : md) (m : list unique_constraint) => match md' with md_def ms' _ => unique_methods_constraint dcl' ms' :: m end) (nil : list unique_constraint) mds -> wf_cld_constr (cld_def dcl' (cl_dcl dcl'') fds mds) (uc_list1 ++ uc_list2) ((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) ++ tyc_list)) | wf_class_constraint_obj : forall (dcl' : dcl) (fds : list fd) (fs : list f) (ms : list m) (mds : list md) (tyc_list : list ty_constraint) (uc_list1 uc_list2 : list unique_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 tyc_list -> uc_list1 = fold_right (fun (fd' : fd) (m : list unique_constraint) => unique_fields_constraint dcl' fd' :: m) (nil : list unique_constraint) fds -> uc_list2 = fold_right (fun (md' : md) (m : list unique_constraint) => match md' with md_def ms' _ => unique_methods_constraint dcl' ms' :: m end) (nil : list unique_constraint) mds -> wf_cld_constr (cld_def dcl' cl_object fds mds) (uc_list1 ++ uc_list2) ((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) ++ tyc_list). Inductive wf_cld_constr_list : P -> list unique_constraint -> list ty_constraint -> Prop := | wf_cld_list_nil : wf_cld_constr_list nil nil nil | wf_cld_list_cons : forall (cld' : cld) (p : P) (uc_list1 uc_list2 : list unique_constraint) (tyc_list1 tyc_list2 : list ty_constraint), wf_cld_constr cld' uc_list1 tyc_list1 -> wf_cld_constr_list p uc_list2 tyc_list2 -> wf_cld_constr_list (cld' :: p) (uc_list1 ++ uc_list2) (tyc_list1 ++ tyc_list2). Inductive wf_rcld_constr (n : nat) : rcld -> list comp_constraint -> list unique_constraint -> list ty_constraint -> Prop := | wf_refined_class_constraint : forall (dcl' dcl'' : dcl) (fds : list fd) (fs : list f) (mds : list md) (rmds : list rmd) (cc_list : list comp_constraint) (uc_list1 uc_list2 : list unique_constraint) (tyc_list1 tyc_list2 : list ty_constraint), dcl' <> dcl'' -> fs = (map (fun (fd' : fd) => match fd' with fd_def ty' f'=> f' end) fds) -> wf_meth_list_constr dcl' mds tyc_list1 -> wf_refined_meth_list_constr n dcl' rmds cc_list tyc_list2 -> uc_list1 = fold_right (fun (fd' : fd) (m : list unique_constraint) => unique_fields_constraint dcl' fd' :: m) (nil : list unique_constraint) fds -> uc_list2 = fold_right (fun (md' : md) (m : list unique_constraint) => match md' with md_def ms' _ => unique_methods_constraint dcl' ms' :: m end) (nil : list unique_constraint) mds -> wf_rcld_constr n (refines_cld_def dcl' (cl_dcl dcl'') fds mds rmds) (introduced_class_constr dcl' n :: cc_list) (uc_list1 ++ uc_list2) ((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) ++ tyc_list1 ++ tyc_list2)) | wf_refined_class_constraint_obj : forall (dcl' : dcl) (fds : list fd) (fs : list f) (mds : list md) (rmds : list rmd) (cc_list : list comp_constraint) (uc_list1 uc_list2 : list unique_constraint) (tyc_list1 tyc_list2 : list ty_constraint), fs = (map (fun (fd' : fd) => match fd' with fd_def ty' f'=> f' end) fds) -> wf_meth_list_constr dcl' mds tyc_list1 -> wf_refined_meth_list_constr n dcl' rmds cc_list tyc_list2 -> uc_list1 = fold_right (fun (fd' : fd) (m : list unique_constraint) => unique_fields_constraint dcl' fd' :: m) (nil : list unique_constraint) fds -> uc_list2 = fold_right (fun (md' : md) (m : list unique_constraint) => match md' with md_def ms' _ => unique_methods_constraint dcl' ms' :: m end) (nil : list unique_constraint) mds -> wf_rcld_constr n (refines_cld_def dcl' cl_object fds mds rmds) (introduced_class_constr dcl' n :: cc_list) (uc_list1 ++ uc_list2) (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) ++ tyc_list1 ++ tyc_list2). Inductive wf_rcld_constr_list (n : nat) : list rcld -> list comp_constraint -> list unique_constraint -> list ty_constraint -> Prop := | wf_rcld_list_nil : wf_rcld_constr_list n nil nil nil nil | wf_rcld_list_cons : forall (rcld' : rcld) (rclds : list rcld) (cc_list1 cc_list2 : list comp_constraint) (uc_list1 uc_list2 : list unique_constraint) (tyc_list1 tyc_list2 : list ty_constraint), wf_rcld_constr n rcld' cc_list1 uc_list1 tyc_list1 -> wf_rcld_constr_list n rclds cc_list2 uc_list2 tyc_list2 -> wf_rcld_constr_list n (rcld' :: rclds) (cc_list1 ++ cc_list2) (uc_list1 ++ uc_list2) (tyc_list1 ++ tyc_list2). Inductive wf_feature (n : nat) : FD -> feature_constraint -> Prop := wf_FD : forall (clds : list cld) (rclds : list rcld) (cc_list : list comp_constraint) (uc_list1 uc_list2 : list unique_constraint) (tyc_list1 tyc_list2 : list ty_constraint), wf_cld_constr_list clds uc_list1 tyc_list1 -> wf_rcld_constr_list n rclds cc_list uc_list2 tyc_list2 -> wf_feature n (feature_def rclds clds) (feature_constr n cc_list (uc_list2 ++ uc_list1) (tyc_list2 ++ tyc_list1)). Inductive wf_FT : nat -> FT -> list feature_constraint -> Prop := | wf_FT_nil : forall n, wf_FT n nil nil | wf_FT_cons : forall (n : nat) (fd : FD) (fds : list FD) (fc : feature_constraint) (fc_list : list feature_constraint), ~ In fd fds -> wf_feature n fd fc -> wf_FT (S n) fds fc_list -> wf_FT n (fd :: fds) (fc :: fc_list). Inductive wf_PSpec (ft : FT) : PSpec -> Prop := WF_PSpec_Cons : forall (ps : PSpec) (n : nat), n < length ft -> ~ In n ps -> wf_PSpec ft ps -> wf_PSpec ft (n :: ps) | WF_PSPec_Nil : wf_PSpec ft nil. Definition cons_option (A : Type) (a : A) (l : option (list A)) : option (list A) := match l with Some l' => Some (a :: l') | _ => None end. Implicit Arguments cons_option [A]. Fixpoint build_PSel (ft : FT) (Psp : PSpec) : option PSel := match Psp with fd' :: Psp' => match (nth_error ft fd') with Some a => cons_option a (build_PSel ft Psp') | _ => None end | _ => Some nil end. Section Feature_Composition. Fixpoint vd_list_eq (vd_list1 vd_list2 : list vd) {struct vd_list1}: bool := match vd_list1, vd_list2 with (vd_def (ty_def cl1) var1) :: vd_list1', (vd_def (ty_def cl2) var2) :: vd_list2' => if (eq_nat_dec var1 var2) then cl_eq cl1 cl2 && (vd_list_eq vd_list1' vd_list2') else false | nil, nil => true | _, _ => false end. Definition ms_eq (ms1 ms2 : ms) : bool := match ms1, ms2 with ms_def (ty_def cl1) m1 list_vd1, ms_def (ty_def cl2) m2 list_vd2 => if (eq_nat_dec m1 m2) then (cl_eq cl1 cl2) && (vd_list_eq list_vd1 list_vd2) else false end. Fixpoint compose_refined_md (mds : list md) (rmd : rmd) {struct mds}: option (list md) := match mds, rmd with cons (md_def ms' (mb_def Ss' x')) mds', rmd_def ms'' (rmb_def before_s after_s y) => if (ms_eq ms' ms'') then Some (cons (md_def ms' (mb_def (before_s ++ Ss' ++ after_s) y)) mds') else cons_option (md_def ms' (mb_def Ss' x')) (compose_refined_md mds' rmd) | nil, _ => None end. Fixpoint introduce_field (fds' : list fd) (fd' : fd) {struct fds'} : list fd := match fds', fd' with (fd_def (ty_def cl') f') :: fds'', fd_def (ty_def cl'') f'' => if (eq_nat_dec f' f'') then if (cl_eq cl' cl'') then fds' else (fd_def (ty_def cl') f') :: (introduce_field fds'' fd') else (fd_def (ty_def cl') f') :: (introduce_field fds'' fd') | _, _ => fd' :: nil end. Fixpoint introduce_method (mds' : list md) (md' : md) {struct mds'} : list md := match mds', md' with (md_def ms' mb') :: mds'', md_def ms'' mb'' => if (ms_eq ms' ms'') then md' :: mds'' else (md_def ms' mb') :: (introduce_method mds'' md') | _, _ => md' :: nil end. Fixpoint rm_dcl (cld_list : list cld) (cld' : cld) {struct cld_list} : list cld := match cld_list, cld' with (cld_def dcl'' cl' fds' mds) :: cld_list', cld_def dcl' _ _ _ => if (eq_nat_dec dcl' dcl'') then rm_dcl cld_list' cld' else (cld_def dcl'' cl' fds' mds) :: (rm_dcl cld_list' cld') | _, _ => nil end. Fixpoint introduce_class (cld_list : list cld) (cld' : cld) {struct cld_list} : list cld := match cld_list, cld' with (cld_def dcl' cl' fds mds) :: cld_list', cld_def dcl'' cl'' fds' mds' => if (eq_nat_dec dcl' dcl'') then cld' :: cld_list' else (cld_def dcl' cl' fds mds) :: (introduce_class cld_list' cld') | _, _ => cld' :: nil end. Definition introduce_fields (fds' fds'' : list fd) : list fd := fold_right (fun (fd' : fd) (lfd : list fd) => introduce_field lfd fd') fds' fds''. Definition introduce_methods (mds' mds'' : list md) : list md := fold_right (fun (md' : md) (lmd : list md) => introduce_method lmd md') mds' mds''. Definition introduce_classes (cld_list' cld_list'' : list cld) : list cld := fold_right (fun (cld' : cld) (list_cld : list cld) => cld' :: (rm_dcl list_cld cld')) cld_list' cld_list''. Definition compose_refined_mds (mds' : list md) (rmds : list rmd) : option (list md) := fold_right (fun (rmd' : rmd) (lmd : option (list md)) => match lmd with Some lmd' => compose_refined_md lmd' rmd' | None => None end) (Some mds') rmds. Fixpoint compose_refines_class (p : P) (rcld' : rcld) {struct p}: option P := match p, rcld' with cons (cld_def dcl' cl' fds' mds') p', refines_cld_def dcl'' cl'' fds'' mds'' rmds => if (eq_nat_dec dcl' dcl'') then match compose_refined_mds mds' rmds with Some mds''' => Some (cons (cld_def dcl' cl'' (introduce_fields fds' fds'') (introduce_methods mds''' mds'') ) p') | None => None end else cons_option (cld_def dcl' cl' fds' mds') (compose_refines_class p' rcld') | _, _ => None end. Definition compose_fd (fd : FD) (p : P) : option P := match fd with feature_def rclds clds => match (fold_right (fun (rcld' : rcld) (op : option P) => match op with Some p' => compose_refines_class p' rcld' | None => None end) (Some p) rclds) with Some p' => Some (introduce_classes p' clds) | None => None end end. Fixpoint compose (ps : PSel) : option P := match ps with fd :: ps' => match compose ps' with Some p => compose_fd fd p | None => None end | nil => Some nil end. Definition build_p (ft : FT) (ps : PSpec) : option P := match build_PSel ft ps with Some ps' => compose ps' | None => None end. End Feature_Composition. Section Sat_Composition_Constraint. Fixpoint meth_in_mds (mds : list md) (ms' : ms) {struct mds} : bool := match mds with (md_def ms'' _ ) :: mds' => if (ms_eq ms' ms'') then true else meth_in_mds mds' ms' | nil => false end. Fixpoint sat_meth_constr_rclds (rclds : list rcld) (dcl' : dcl) (ms' : ms) {struct rclds} : bool := match rclds with (refines_cld_def dcl'' _ _ mds' _) :: rclds'=> if (eq_nat_dec dcl' dcl'') then if (meth_in_mds mds' ms') then true else sat_meth_constr_rclds rclds' dcl' ms' else sat_meth_constr_rclds rclds' dcl' ms' | nil => false end. Definition sat_meth_constr_clds (clds : list cld) (dcl' : dcl) (ms' : ms) : bool := match head (path clds (cl_dcl dcl')) with Some (cld_def _ _ _ mds') => meth_in_mds mds' ms' | None => false end. Fixpoint sat_meth_constr_PSel (dcl' : dcl) (ms' : ms) (ps : PSel) {struct ps}: bool := match ps with (feature_def rclds clds) :: ps' => if (in_path clds dcl') then sat_meth_constr_clds clds dcl' ms' else if sat_meth_constr_rclds rclds dcl' ms' then true else sat_meth_constr_PSel dcl' ms' ps' | nil => false end. Definition in_clds (dcl' : dcl) (clds : list cld) : bool := match head (path clds (cl_dcl dcl')) with Some (cld_def _ _ _ _) => true | None => false end. Fixpoint sat_cld_constr_PSel (dcl' : dcl) (ps : PSel) {struct ps} : bool := match ps with (feature_def _ clds) :: ps' => if (in_clds dcl' clds) then true else sat_cld_constr_PSel dcl' ps' | nil => false end. Fixpoint sat_meth_constr_PSpec (n : nat) (ft : FT) (dcl' : dcl) (ms' : ms) (ps : PSpec) {struct ps}: bool := match ps with F' :: ps' => if (eq_nat_dec F' n) then match (build_PSel ft ps') with Some ps'' => sat_meth_constr_PSel dcl' ms' ps'' | _ => false end else sat_meth_constr_PSpec n ft dcl' ms' ps' | nil => false end. Fixpoint sat_cld_constr_PSpec (n : nat) (ft : FT) (dcl' : dcl) (ps : PSpec) {struct ps} : bool := match ps with F' :: ps' => if (eq_nat_dec F' n) then match (build_PSel ft ps') with Some ps'' => sat_cld_constr_PSel dcl' ps'' | _ => false end else sat_cld_constr_PSpec n ft dcl' ps' | nil => false end. Fixpoint sat_comp_constr_ps (ft : FT) (ps: PSpec) (c_list : list comp_constraint) : bool := match c_list with (introduced_method_constr ms' dcl' n) :: c_list' => sat_meth_constr_PSpec n ft dcl' ms' ps && (sat_comp_constr_ps ft ps c_list') | (introduced_class_constr dcl' n) :: c_list' => sat_cld_constr_PSpec n ft dcl' ps && (sat_comp_constr_ps ft ps c_list') | nil => true end. Inductive sat_feature_comp_constr (ft : FT) (ps : PSpec) : list feature_constraint -> Prop := Cons_sfcc : forall (n : nat) (cc_list : list comp_constraint) (uc_list : list unique_constraint) (tyc_list : list ty_constraint) (fc_list : list feature_constraint), In n ps -> sat_comp_constr_ps ft ps cc_list = true -> sat_feature_comp_constr ft ps fc_list -> sat_feature_comp_constr ft ps (feature_constr n cc_list uc_list tyc_list :: fc_list) | Nin_Cons_sfcc : forall (n : nat) (cc_list : list comp_constraint) (uc_list : list unique_constraint) (tyc_list : list ty_constraint) (fc_list : list feature_constraint), ~ In n ps -> sat_feature_comp_constr ft ps fc_list -> sat_feature_comp_constr ft ps (feature_constr n cc_list uc_list tyc_list :: fc_list) | Nil_sfcc : sat_feature_comp_constr ft ps nil. End Sat_Composition_Constraint. Definition Sound_Composition := forall (ft : FT) (ps : PSpec) (c_list : list feature_constraint), wf_FT 0 ft c_list -> sat_feature_comp_constr ft ps c_list -> wf_PSpec ft ps -> exists p, build_p ft ps = Some p. Section Sat_Unique_Constraint. Fixpoint f_repeated (dcl' : dcl) (cl' : cl) (f' : f) (uc_list : list unique_constraint) {struct uc_list} : bool := match uc_list with unique_fields_constraint dcl'' (fd_def (ty_def cl'') f'') :: uc_list' => if (eq_nat_dec dcl' dcl'') then if (eq_nat_dec f' f'') then if (cl_eq cl' cl'') then f_repeated dcl' cl' f' uc_list' else true else f_repeated dcl' cl' f' uc_list' else f_repeated dcl' cl' f' uc_list' | _ :: uc_list' => f_repeated dcl' cl' f' uc_list' | nil => false end. Fixpoint sat_f_unique_constraint (dcl' : dcl) (uc_list : list unique_constraint) {struct uc_list} : bool := match uc_list with unique_fields_constraint dcl'' (fd_def (ty_def cl') f') :: uc_list' => if (eq_nat_dec dcl' dcl'') then if f_repeated dcl' cl' f' uc_list' then false else sat_f_unique_constraint dcl' uc_list' else sat_f_unique_constraint dcl' uc_list' | _ :: uc_list' => sat_f_unique_constraint dcl' uc_list' | nil => true end. Fixpoint ms_repeated (dcl' : dcl) (ty' : ty) (m' : m) (vd_list' : list vd) (uc_list : list unique_constraint) {struct uc_list} : bool := match uc_list with unique_methods_constraint dcl'' (ms_def ty'' m'' vd_list'') :: uc_list' => if (eq_nat_dec dcl' dcl'') then if (eq_nat_dec m' m'') then if ms_eq (ms_def ty'' m'' vd_list'') (ms_def ty' m' vd_list') then ms_repeated dcl' ty' m' vd_list' uc_list' else true else ms_repeated dcl' ty' m' vd_list' uc_list' else ms_repeated dcl' ty' m' vd_list' uc_list' | _ :: uc_list' => ms_repeated dcl' ty' m' vd_list' uc_list' | nil => false end. Fixpoint sat_ms_unique_constraint (dcl' : dcl) (uc_list : list unique_constraint) {struct uc_list} : bool := match uc_list with unique_methods_constraint dcl'' (ms_def ty' m' vd_list') :: uc_list' => if (eq_nat_dec dcl' dcl'') then if ms_repeated dcl' ty' m' vd_list' uc_list' then false else sat_ms_unique_constraint dcl' uc_list' else sat_ms_unique_constraint dcl' uc_list' | _ :: uc_list' => sat_ms_unique_constraint dcl' uc_list' | nil => true end. Fixpoint sat_unique_constraint (uc_list : list unique_constraint) {struct uc_list} : bool := match uc_list with unique_fields_constraint dcl' _ :: uc_list' => sat_f_unique_constraint dcl' uc_list && sat_unique_constraint uc_list' | unique_methods_constraint dcl' _ :: uc_list' => sat_ms_unique_constraint dcl' uc_list && sat_unique_constraint uc_list' | nil => true end. Inductive sat_feature_unique_constr (ps : PSpec) : list feature_constraint -> Prop := Cons_sfuc : forall (n : nat) (cc_list : list comp_constraint) (uc_list : list unique_constraint) (tyc_list : list ty_constraint) (fc_list : list feature_constraint), In n ps -> (forall (cc_list' : list comp_constraint) (uc_list' : list unique_constraint) (tyc_list' : list ty_constraint) (n' : nat), In (feature_constr n' cc_list' uc_list' tyc_list') fc_list-> In n' ps -> sat_unique_constraint (uc_list ++ uc_list') = true) -> sat_unique_constraint uc_list = true -> sat_feature_unique_constr ps fc_list -> sat_feature_unique_constr ps (feature_constr n cc_list uc_list tyc_list :: fc_list) | Nil_sfuc : sat_feature_unique_constr ps nil. End Sat_Unique_Constraint. Definition Typeable_Composition := forall (ft : FT) (ps : PSpec) (c_list : list feature_constraint) (p : P), wf_FT 0 ft c_list -> wf_PSpec ft ps -> sat_feature_unique_constr ps c_list -> build_p ft ps = Some p -> exists c_list, wf_prog_constr p c_list. Section Well_Formed_Composition. Definition build_refined_class (cld' : cld) (rcld' : rcld) : cld := match cld', rcld' with cld_def dcl' cl' fds' mds', refines_cld_def dcl'' cl'' fds'' mds'' rmds => if (eq_nat_dec dcl' dcl'') then match compose_refined_mds mds' rmds with Some mds''' => cld_def dcl' cl'' (introduce_fields fds' fds'') (introduce_methods mds''' mds'') | None => cld_def dcl' cl'' (introduce_fields fds' fds'') mds' end else cld' end. Definition build_refined_classes (cld' : cld) (list_rcld' : list rcld) : cld := fold_right (fun (rcld' : rcld) (cld'' : cld) => build_refined_class cld'' rcld') cld' list_rcld'. Fixpoint get_refined_cld (ps : PSel) (cl' : cl) {struct ps} : option cld := match ps with | cons (feature_def refined_cld introed_cld) ps' => let path_frag := (path introed_cld cl') in match path_frag with nil => match get_refined_cld ps' cl' with Some cld'=> Some (build_refined_classes cld' refined_cld) | None => None end | cons cld' _ => Some cld' end | _ => None end. Fixpoint f_path (ps : PSel) (cl' : cl) (n : nat) {struct n} : list cld := match n, (get_refined_cld ps cl') with S n', Some (cld_def dcl'' cl'' fds'' mds'') => (cld_def dcl'' cl'' fds'' mds'') :: (f_path ps cl'' n') | _, _ => nil end. Definition get_cld (p : P) (cl' : cl) : option cld := head (path p cl'). Fixpoint path' (p : P) (cl' : cl) (n : nat) {struct n} : list cld := match n, get_cld p cl' with S n', Some (cld_def dcl'' cl'' fds'' mds'') => (cld_def dcl'' cl'' fds'' mds'') :: (path' p cl'' n') | _, _ => nil end. Definition ps_ftype (ps : PSel) (cl' : cl) (f' : f) (n :nat) : option ty := ext_fty (f_path ps cl' n) f'. Definition ps_get_md (ps : PSel) (cl' : cl) ( m' : m) (n : nat) : option md := head (filter_mds (get_all_mds (f_path ps cl' n)) m'). Definition ps_mtype (ps : PSel) (cl' : cl) ( m' : m) (n : nat) : option mty := match (ps_get_md ps cl' m' n) with Some x => Some (ext_mty x) | None => None end. Definition ps_fields (ps : PSel) (cl' : cl) (n : nat) : list f := ext_fs (f_path ps cl' n). Definition ps_methods (ps : PSel) (cl' : cl) (n: nat): list m := ext_ms (f_path ps cl' n). Definition get_ps_parent (ps : PSel) (cl' : cl) : option cl := match get_refined_cld ps cl' with Some cld' => Some (get_parent cld') | None => None end. Definition ps_sat_constr (ps : PSel) (c : ty_constraint) (n : nat) : bool := match c with | sty_field_rconstr cl' f' (ty_def cl'') => match cl'', (ps_ftype ps cl' f' n) with cl_dcl dcl', Some (ty_def (cl_dcl dcl'')) => in_path (f_path ps (cl_dcl dcl'') n) dcl' | cl_object, Some (ty_def (cl_dcl dcl'')) => in_path (f_path ps (cl_dcl dcl'') n) dcl'' | cl_object, Some (ty_def cl_object) => true | _, _ => false end | sty_field_wconstr (ty_def cl') cl'' f' => match cl', (ps_ftype ps cl'' f' n) with cl_dcl dcl'', Some (ty_def (cl_dcl dcl')) => in_path (f_path ps (cl_dcl dcl'') n) dcl' | cl_dcl dcl'', Some (ty_def cl_object) => in_path (f_path ps (cl_dcl dcl'') n) dcl'' | cl_object, Some (ty_def cl_object) => true | _, _ => false end | sty_meth_constr cl' m' (ty_def cl'') ty_list => match (ps_mtype ps cl' m' n), 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 (f_path ps (cl_dcl dcl'') n) dcl') && (fold_right (fun (x : ty*ty) (m : bool) => match x with ((ty_def (cl_dcl dcl2)), (ty_def (cl_dcl dcl1))) => (in_path (f_path ps (cl_dcl dcl2) n) dcl1) && m | ((ty_def (cl_dcl dcl1)), (ty_def cl_object)) => (in_path (f_path ps (cl_dcl dcl1) n) 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 (f_path ps (cl_dcl dcl'') n) dcl'') && (fold_right (fun (x : ty*ty) (m : bool) => match x with ((ty_def (cl_dcl dcl2)), (ty_def (cl_dcl dcl1))) => (in_path (f_path ps (cl_dcl dcl2) n) dcl1) && m | ((ty_def (cl_dcl dcl1)), (ty_def cl_object)) => (in_path (f_path ps (cl_dcl dcl1) n) 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 (f_path ps (cl_dcl dcl2) n) dcl1) && m | ((ty_def (cl_dcl dcl1)), (ty_def cl_object)) => (in_path (f_path ps (cl_dcl dcl1) n) 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 (f_path ps cl' n) dcl' | ty_def cl_object, ty_def cl_object => true | ty_def (cl_dcl dcl'), ty_def cl_object => in_path (f_path ps (cl_dcl dcl') n) dcl' end | sty_if_constr (ty_def cl1) (ty_def cl2) => match cl1, cl2 with cl_dcl dcl1, cl_dcl dcl2 => in_path (f_path ps (cl_dcl dcl1) n) dcl2 || in_path (f_path ps (cl_dcl dcl2) n) dcl1 | cl_object, cl_dcl dcl2 => in_path (f_path ps (cl_dcl dcl2) n) dcl2 | cl_dcl dcl1, cl_object => in_path (f_path ps (cl_dcl dcl1) n) dcl1 | cl_object, cl_object => true end | in_prog_constr cl' => match cl' with cl_dcl dcl' => in_path (f_path ps (cl_dcl dcl') n) dcl' | cl_object => true end | inherited_fields_constr fds' cl' => match (get_ps_parent ps cl') with Some cl'' => match (list_inter _ fds' (ps_fields ps cl'' n) in_nat_list) with nil => true | _ => false end | None => false end | inherited_methods_constr mds' cl' => match (get_ps_parent ps cl') with Some cl'' => let pmds' := ps_methods ps cl'' n 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 (ps_mtype ps cl'' m' n) 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' | None => false end end. Fixpoint ps_sat_constr_list (ps : PSel) (c_list : list ty_constraint) (n : nat) {struct c_list}: bool := match c_list with constr :: c_list' => ps_sat_constr ps constr n && ps_sat_constr_list ps c_list' n | nil => true end. Fixpoint introduce_all (ps : PSel) : list cld := match ps with nil => nil | feature_def _ l :: ps' => introduce_classes (introduce_all ps') l end. Inductive sat_feature_ty_constr (ft : FT) (ps : PSpec) : list feature_constraint -> Prop := Cons_sftc : forall (n : nat) (cc_list : list comp_constraint) (uc_list : list unique_constraint) (tyc_list : list ty_constraint) (fc_list : list feature_constraint) (ps' : PSel), build_PSel ft ps = Some ps' -> In n ps -> ps_sat_constr_list ps' tyc_list (length (introduce_all ps')) = true -> sat_feature_ty_constr ft ps fc_list -> sat_feature_ty_constr ft ps (feature_constr n cc_list uc_list tyc_list :: fc_list) | Nin_Cons_sftc : forall (n : nat) (cc_list : list comp_constraint) (uc_list : list unique_constraint) (tyc_list : list ty_constraint) (fc_list : list feature_constraint), ~ In n ps -> sat_feature_ty_constr ft ps fc_list -> sat_feature_ty_constr ft ps (feature_constr n cc_list uc_list tyc_list :: fc_list) | Nil_sftc : sat_feature_ty_constr ft ps nil. Definition WF_Composition := forall (ft : FT) (ps : PSpec) (fc_list : list feature_constraint), wf_FT 0 ft fc_list -> wf_PSpec ft ps -> sat_feature_comp_constr ft ps fc_list -> sat_feature_unique_constr ps fc_list -> sat_feature_ty_constr ft ps fc_list -> exists p, build_p ft ps = Some p /\ (forall p', Permutation p p' -> acyclic_hierarchy p' -> wf_prog p'). End Well_Formed_Composition.