700 |
700 |
701 definition new_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd" |
701 definition new_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd" |
702 where |
702 where |
703 "new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)" |
703 "new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)" |
704 |
704 |
705 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_fname set" |
705 definition all_fname_under_dir:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_fname set" |
706 where |
706 where |
707 "all_fname_under_dir d \<tau> fs = {fn. \<exists> f. fn # d = f \<and> f \<in> (current_files \<tau> \<union> fs)}" |
707 "all_fname_under_dir d fs = {fn. fn # d \<in> fs}" |
708 |
708 |
709 fun fname_all_a:: "nat \<Rightarrow> t_fname" |
709 fun fname_all_a:: "nat \<Rightarrow> t_fname" |
710 where |
710 where |
711 "fname_all_a 0 = []" | |
711 "fname_all_a 0 = []" | |
712 "fname_all_a (Suc n) = ''a''@(fname_all_a n)" |
712 "fname_all_a (Suc n) = ''a''@(fname_all_a n)" |
713 |
713 |
714 definition fname_length_set :: "t_fname set \<Rightarrow> nat set" |
714 definition fname_length_set :: "t_fname set \<Rightarrow> nat set" |
715 where |
715 where |
716 "fname_length_set fns = length`fns" |
716 "fname_length_set fns = length`fns" |
717 |
717 |
718 definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_fname" |
718 definition next_fname:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_fname" |
719 where |
719 where |
720 "next_fname pf \<tau> fs = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau> fs))) + 1)" |
720 "next_fname pf fs = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf fs))) + 1)" |
721 |
721 |
722 definition new_childf_general:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_file" |
722 definition new_childf_general:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_file" |
723 where |
723 where |
724 "new_childf_general pf \<tau> fs = next_fname pf \<tau> fs # pf" |
724 "new_childf_general pf fs = next_fname pf fs # pf" |
725 |
725 |
726 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file" |
726 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file" |
727 where |
727 where |
728 "new_childf pf \<tau> = new_childf_general pf \<tau> {}" |
728 "new_childf pf \<tau> = new_childf_general pf (current_files \<tau>)" |
729 |
729 |
730 end |
730 end |
731 |
731 |
732 end |
732 end |